2909 lines
98 KiB
Plaintext
2909 lines
98 KiB
Plaintext
|
INFO Running translator.
|
||
|
|
INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-1.pddl']
|
||
|
|
INFO translator arguments: []
|
||
|
|
INFO translator time limit: None
|
||
|
|
INFO translator memory limit: None
|
||
|
|
INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-1.pddl
|
||
|
|
Parsing...
|
||
|
|
Parsing: [0.030s CPU, 0.033s wall-clock]
|
||
|
|
Normalizing task... [0.010s CPU, 0.002s wall-clock]
|
||
|
|
Instantiating...
|
||
|
|
Generating Datalog program... [0.000s CPU, 0.008s wall-clock]
|
||
|
|
Normalizing Datalog program...
|
||
|
|
Normalizing Datalog program: [0.020s CPU, 0.022s wall-clock]
|
||
|
|
Preparing model... [0.030s CPU, 0.024s wall-clock]
|
||
|
|
Generated 46 rules.
|
||
|
|
Computing model... [0.440s CPU, 0.445s wall-clock]
|
||
|
|
3460 relevant atoms
|
||
|
|
2552 auxiliary atoms
|
||
|
|
6012 final queue length
|
||
|
|
11142 total queue pushes
|
||
|
|
Completing instantiation... [1.010s CPU, 1.002s wall-clock]
|
||
|
|
Instantiating: [1.500s CPU, 1.508s wall-clock]
|
||
|
|
Computing fact groups...
|
||
|
|
Finding invariants...
|
||
|
|
12 initial candidates
|
||
|
|
Finding invariants: [0.030s CPU, 0.033s wall-clock]
|
||
|
|
Checking invariant weight... [0.010s CPU, 0.002s wall-clock]
|
||
|
|
Instantiating groups... [0.010s CPU, 0.017s wall-clock]
|
||
|
|
Collecting mutex groups... [0.000s CPU, 0.002s wall-clock]
|
||
|
|
Choosing groups...
|
||
|
|
0 uncovered facts
|
||
|
|
Choosing groups: [0.010s CPU, 0.007s wall-clock]
|
||
|
|
Building translation key... [0.000s CPU, 0.004s wall-clock]
|
||
|
|
Computing fact groups: [0.080s CPU, 0.079s wall-clock]
|
||
|
|
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
|
||
|
|
Building dictionary for full mutex groups... [0.000s CPU, 0.001s wall-clock]
|
||
|
|
Building mutex information...
|
||
|
|
Building mutex information: [0.000s CPU, 0.003s wall-clock]
|
||
|
|
Translating task...
|
||
|
|
Processing axioms...
|
||
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
||
|
|
Processing axioms: [0.050s CPU, 0.044s wall-clock]
|
||
|
|
Translating task: [0.820s CPU, 0.812s wall-clock]
|
||
|
|
0 effect conditions simplified
|
||
|
|
0 implied preconditions added
|
||
|
|
Detecting unreachable propositions...
|
||
|
|
0 operators removed
|
||
|
|
0 axioms removed
|
||
|
|
22 propositions removed
|
||
|
|
Detecting unreachable propositions: [0.400s CPU, 0.404s wall-clock]
|
||
|
|
Reordering and filtering variables...
|
||
|
|
22 of 22 variables necessary.
|
||
|
|
0 of 22 mutex groups necessary.
|
||
|
|
2816 of 2816 operators necessary.
|
||
|
|
0 of 0 axiom rules necessary.
|
||
|
|
Reordering and filtering variables: [0.140s CPU, 0.131s wall-clock]
|
||
|
|
Translator variables: 22
|
||
|
|
Translator derived variables: 0
|
||
|
|
Translator facts: 340
|
||
|
|
Translator goal facts: 14
|
||
|
|
Translator mutex groups: 0
|
||
|
|
Translator total mutex groups size: 0
|
||
|
|
Translator operators: 2816
|
||
|
|
Translator axioms: 0
|
||
|
|
Translator task size: 16720
|
||
|
|
Translator peak memory: 47308 KB
|
||
|
|
Writing output... [0.290s CPU, 0.307s wall-clock]
|
||
|
|
Done! [3.300s CPU, 3.319s wall-clock]
|
||
|
|
planner.py version 0.0.1
|
||
|
|
|
||
|
|
Time: 0.67s
|
||
|
|
Memory: 95MB
|
||
|
|
|
||
|
|
Iteration 1
|
||
|
|
Queue: [(0,30,0,True)]
|
||
|
|
Grounded Until: 0
|
||
|
|
Expected Memory: 95MB
|
||
|
|
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
|
||
|
|
Grounding Time: 1.28s
|
||
|
|
Memory: 205MB (+110MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 1+
|
||
|
|
Calls : 1
|
||
|
|
Time : 2.991s (Solving: 0.07s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 2.888s
|
||
|
|
|
||
|
|
Choices : 3949 (Domain: 3925)
|
||
|
|
Conflicts : 94 (Analyzed: 94)
|
||
|
|
Restarts : 1 (Average: 94.00 Last: 19)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 1 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 94 (Deleted: 0)
|
||
|
|
Binary : 38 (Ratio: 40.43%)
|
||
|
|
Ternary : 20 (Ratio: 21.28%)
|
||
|
|
Conflict : 94 (Average Length: 30.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 94 (Average: 28.99 Max: 359 Sum: 2725)
|
||
|
|
Executed : 94 (Average: 28.99 Max: 359 Sum: 2725 Ratio: 100.00%)
|
||
|
|
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 0
|
||
|
|
Atoms : 0
|
||
|
|
Bodies : 0
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 102462 (Eliminated: 0 Frozen: 9069)
|
||
|
|
Constraints : 679498 (Binary: 97.1% Ternary: 1.4% Other: 1.5%)
|
||
|
|
|
||
|
|
Memory Peak : 376MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.14s
|
||
|
|
Memory: 312MB (+107MB)
|
||
|
|
SAT
|
||
|
|
Testing...
|
||
|
|
NOT SERIALIZABLE
|
||
|
|
Testing Time: 1.14s
|
||
|
|
Memory: 316MB (+4MB)
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 2
|
||
|
|
Time : 28.875s (Solving: 25.29s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 28.784s
|
||
|
|
|
||
|
|
Choices : 1668764 (Domain: 1668740)
|
||
|
|
Conflicts : 31743 (Analyzed: 31743)
|
||
|
|
Restarts : 101 (Average: 314.29 Last: 143)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 2 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 31743 (Deleted: 25656)
|
||
|
|
Binary : 862 (Ratio: 2.72%)
|
||
|
|
Ternary : 707 (Ratio: 2.23%)
|
||
|
|
Conflict : 31743 (Average Length: 569.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 31743 (Average: 51.61 Max: 1535 Sum: 1638358)
|
||
|
|
Executed : 31678 (Average: 51.55 Max: 1535 Sum: 1636371 Ratio: 99.88%)
|
||
|
|
Bounded : 65 (Average: 30.57 Max: 32 Sum: 1987 Ratio: 0.12%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 897395 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 376MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 25.40s
|
||
|
|
Memory: 318MB (+2MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 28.76s
|
||
|
|
|
||
|
|
Iteration 2
|
||
|
|
Queue: [(0,30,1,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 3
|
||
|
|
Time : 43.079s (Solving: 39.46s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 42.996s
|
||
|
|
|
||
|
|
Choices : 2557018 (Domain: 2556994)
|
||
|
|
Conflicts : 61145 (Analyzed: 61145)
|
||
|
|
Restarts : 201 (Average: 304.20 Last: 230)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 3 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 61145 (Deleted: 51706)
|
||
|
|
Binary : 1430 (Ratio: 2.34%)
|
||
|
|
Ternary : 1142 (Ratio: 1.87%)
|
||
|
|
Conflict : 61145 (Average Length: 652.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 61145 (Average: 40.30 Max: 1535 Sum: 2464203)
|
||
|
|
Executed : 61074 (Average: 40.27 Max: 1535 Sum: 2462055 Ratio: 99.91%)
|
||
|
|
Bounded : 71 (Average: 30.25 Max: 32 Sum: 2148 Ratio: 0.09%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 879798 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 376MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.22s
|
||
|
|
Memory: 318MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.22s
|
||
|
|
|
||
|
|
Iteration 3
|
||
|
|
Queue: [(0,30,2,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 4
|
||
|
|
Time : 57.174s (Solving: 53.52s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 57.100s
|
||
|
|
|
||
|
|
Choices : 3090641 (Domain: 3090617)
|
||
|
|
Conflicts : 90647 (Analyzed: 90647)
|
||
|
|
Restarts : 301 (Average: 301.15 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 4 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 90647 (Deleted: 77680)
|
||
|
|
Binary : 1640 (Ratio: 1.81%)
|
||
|
|
Ternary : 1380 (Ratio: 1.52%)
|
||
|
|
Conflict : 90647 (Average Length: 838.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 90647 (Average: 32.23 Max: 1535 Sum: 2921152)
|
||
|
|
Executed : 90573 (Average: 32.20 Max: 1535 Sum: 2919001 Ratio: 99.93%)
|
||
|
|
Bounded : 74 (Average: 29.07 Max: 32 Sum: 2151 Ratio: 0.07%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 877891 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 376MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.11s
|
||
|
|
Memory: 318MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.11s
|
||
|
|
|
||
|
|
Iteration 4
|
||
|
|
Queue: [(0,30,3,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 5
|
||
|
|
Time : 70.461s (Solving: 66.77s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 70.392s
|
||
|
|
|
||
|
|
Choices : 3775179 (Domain: 3775155)
|
||
|
|
Conflicts : 117031 (Analyzed: 117031)
|
||
|
|
Restarts : 401 (Average: 291.85 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 5 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 117031 (Deleted: 102014)
|
||
|
|
Binary : 1764 (Ratio: 1.51%)
|
||
|
|
Ternary : 1519 (Ratio: 1.30%)
|
||
|
|
Conflict : 117031 (Average Length: 935.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 117031 (Average: 30.04 Max: 1535 Sum: 3516182)
|
||
|
|
Executed : 116955 (Average: 30.03 Max: 1535 Sum: 3513967 Ratio: 99.94%)
|
||
|
|
Bounded : 76 (Average: 29.14 Max: 32 Sum: 2215 Ratio: 0.06%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 877891 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 376MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.30s
|
||
|
|
Memory: 318MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.30s
|
||
|
|
|
||
|
|
Iteration 5
|
||
|
|
Queue: [(0,30,4,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 6
|
||
|
|
Time : 88.035s (Solving: 84.31s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 87.972s
|
||
|
|
|
||
|
|
Choices : 4346761 (Domain: 4346737)
|
||
|
|
Conflicts : 146155 (Analyzed: 146155)
|
||
|
|
Restarts : 501 (Average: 291.73 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 6 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 146155 (Deleted: 132485)
|
||
|
|
Binary : 1992 (Ratio: 1.36%)
|
||
|
|
Ternary : 1708 (Ratio: 1.17%)
|
||
|
|
Conflict : 146155 (Average Length: 1219.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 146155 (Average: 27.43 Max: 1535 Sum: 4009477)
|
||
|
|
Executed : 146071 (Average: 27.42 Max: 1535 Sum: 4007099 Ratio: 99.94%)
|
||
|
|
Bounded : 84 (Average: 28.31 Max: 32 Sum: 2378 Ratio: 0.06%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 877867 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 17.59s
|
||
|
|
Memory: 382MB (+64MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 17.59s
|
||
|
|
|
||
|
|
Iteration 6
|
||
|
|
Queue: [(0,30,5,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 7
|
||
|
|
Time : 104.389s (Solving: 100.62s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 104.336s
|
||
|
|
|
||
|
|
Choices : 4884968 (Domain: 4884944)
|
||
|
|
Conflicts : 175894 (Analyzed: 175894)
|
||
|
|
Restarts : 601 (Average: 292.67 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 7 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 175894 (Deleted: 159446)
|
||
|
|
Binary : 2286 (Ratio: 1.30%)
|
||
|
|
Ternary : 1954 (Ratio: 1.11%)
|
||
|
|
Conflict : 175894 (Average Length: 1310.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 175894 (Average: 25.37 Max: 1535 Sum: 4462744)
|
||
|
|
Executed : 175802 (Average: 25.36 Max: 1535 Sum: 4460296 Ratio: 99.95%)
|
||
|
|
Bounded : 92 (Average: 26.61 Max: 32 Sum: 2448 Ratio: 0.05%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 877754 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 16.36s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 16.36s
|
||
|
|
|
||
|
|
Iteration 7
|
||
|
|
Queue: [(0,30,6,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 8
|
||
|
|
Time : 118.877s (Solving: 115.08s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 118.832s
|
||
|
|
|
||
|
|
Choices : 5400238 (Domain: 5400214)
|
||
|
|
Conflicts : 204393 (Analyzed: 204393)
|
||
|
|
Restarts : 701 (Average: 291.57 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 8 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 204393 (Deleted: 187326)
|
||
|
|
Binary : 2553 (Ratio: 1.25%)
|
||
|
|
Ternary : 2172 (Ratio: 1.06%)
|
||
|
|
Conflict : 204393 (Average Length: 1371.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 204393 (Average: 23.90 Max: 1535 Sum: 4885113)
|
||
|
|
Executed : 204297 (Average: 23.89 Max: 1535 Sum: 4882630 Ratio: 99.95%)
|
||
|
|
Bounded : 96 (Average: 25.86 Max: 32 Sum: 2483 Ratio: 0.05%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 877018 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.50s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.50s
|
||
|
|
|
||
|
|
Iteration 8
|
||
|
|
Queue: [(0,30,7,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 9
|
||
|
|
Time : 134.154s (Solving: 130.32s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 134.116s
|
||
|
|
|
||
|
|
Choices : 5842268 (Domain: 5842244)
|
||
|
|
Conflicts : 232860 (Analyzed: 232860)
|
||
|
|
Restarts : 801 (Average: 290.71 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 9 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 232860 (Deleted: 213883)
|
||
|
|
Binary : 2715 (Ratio: 1.17%)
|
||
|
|
Ternary : 2331 (Ratio: 1.00%)
|
||
|
|
Conflict : 232860 (Average Length: 1436.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 232860 (Average: 22.49 Max: 1535 Sum: 5236417)
|
||
|
|
Executed : 232758 (Average: 22.48 Max: 1535 Sum: 5233897 Ratio: 99.95%)
|
||
|
|
Bounded : 102 (Average: 24.71 Max: 32 Sum: 2520 Ratio: 0.05%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 877006 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.29s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.29s
|
||
|
|
|
||
|
|
Iteration 9
|
||
|
|
Queue: [(0,30,8,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 10
|
||
|
|
Time : 149.430s (Solving: 145.57s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 149.400s
|
||
|
|
|
||
|
|
Choices : 6217683 (Domain: 6217659)
|
||
|
|
Conflicts : 260552 (Analyzed: 260552)
|
||
|
|
Restarts : 901 (Average: 289.18 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 10 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 260552 (Deleted: 238946)
|
||
|
|
Binary : 2850 (Ratio: 1.09%)
|
||
|
|
Ternary : 2454 (Ratio: 0.94%)
|
||
|
|
Conflict : 260552 (Average Length: 1441.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 260552 (Average: 21.18 Max: 1535 Sum: 5518379)
|
||
|
|
Executed : 260449 (Average: 21.17 Max: 1535 Sum: 5515858 Ratio: 99.95%)
|
||
|
|
Bounded : 103 (Average: 24.48 Max: 32 Sum: 2521 Ratio: 0.05%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876994 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.29s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.29s
|
||
|
|
|
||
|
|
Iteration 10
|
||
|
|
Queue: [(0,30,9,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 11
|
||
|
|
Time : 162.777s (Solving: 158.89s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 162.752s
|
||
|
|
|
||
|
|
Choices : 6580720 (Domain: 6580696)
|
||
|
|
Conflicts : 287204 (Analyzed: 287204)
|
||
|
|
Restarts : 1001 (Average: 286.92 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 11 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 287204 (Deleted: 262781)
|
||
|
|
Binary : 2952 (Ratio: 1.03%)
|
||
|
|
Ternary : 2553 (Ratio: 0.89%)
|
||
|
|
Conflict : 287204 (Average Length: 1448.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 287204 (Average: 20.14 Max: 1535 Sum: 5783024)
|
||
|
|
Executed : 287099 (Average: 20.13 Max: 1535 Sum: 5780470 Ratio: 99.96%)
|
||
|
|
Bounded : 105 (Average: 24.32 Max: 32 Sum: 2554 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876994 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.36s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.36s
|
||
|
|
|
||
|
|
Iteration 11
|
||
|
|
Queue: [(0,30,10,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 12
|
||
|
|
Time : 176.984s (Solving: 173.07s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 176.964s
|
||
|
|
|
||
|
|
Choices : 6920813 (Domain: 6920789)
|
||
|
|
Conflicts : 313774 (Analyzed: 313774)
|
||
|
|
Restarts : 1101 (Average: 284.99 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 12 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 313774 (Deleted: 288599)
|
||
|
|
Binary : 3030 (Ratio: 0.97%)
|
||
|
|
Ternary : 2633 (Ratio: 0.84%)
|
||
|
|
Conflict : 313774 (Average Length: 1456.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 313774 (Average: 19.21 Max: 1535 Sum: 6026128)
|
||
|
|
Executed : 313667 (Average: 19.20 Max: 1535 Sum: 6023541 Ratio: 99.96%)
|
||
|
|
Bounded : 107 (Average: 24.18 Max: 32 Sum: 2587 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876982 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.22s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.22s
|
||
|
|
|
||
|
|
Iteration 12
|
||
|
|
Queue: [(0,30,11,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 13
|
||
|
|
Time : 191.910s (Solving: 187.97s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 191.896s
|
||
|
|
|
||
|
|
Choices : 7234369 (Domain: 7234345)
|
||
|
|
Conflicts : 342508 (Analyzed: 342508)
|
||
|
|
Restarts : 1201 (Average: 285.19 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 13 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 342508 (Deleted: 317256)
|
||
|
|
Binary : 3117 (Ratio: 0.91%)
|
||
|
|
Ternary : 2681 (Ratio: 0.78%)
|
||
|
|
Conflict : 342508 (Average Length: 1477.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 342508 (Average: 18.22 Max: 1535 Sum: 6239123)
|
||
|
|
Executed : 342401 (Average: 18.21 Max: 1535 Sum: 6236536 Ratio: 99.96%)
|
||
|
|
Bounded : 107 (Average: 24.18 Max: 32 Sum: 2587 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.93s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.93s
|
||
|
|
|
||
|
|
Iteration 13
|
||
|
|
Queue: [(0,30,12,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 14
|
||
|
|
Time : 206.296s (Solving: 202.32s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 206.288s
|
||
|
|
|
||
|
|
Choices : 7569779 (Domain: 7569755)
|
||
|
|
Conflicts : 370015 (Analyzed: 370015)
|
||
|
|
Restarts : 1301 (Average: 284.41 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 14 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 370015 (Deleted: 342379)
|
||
|
|
Binary : 3182 (Ratio: 0.86%)
|
||
|
|
Ternary : 2723 (Ratio: 0.74%)
|
||
|
|
Conflict : 370015 (Average Length: 1498.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 370015 (Average: 17.48 Max: 1535 Sum: 6469458)
|
||
|
|
Executed : 369908 (Average: 17.48 Max: 1535 Sum: 6466871 Ratio: 99.96%)
|
||
|
|
Bounded : 107 (Average: 24.18 Max: 32 Sum: 2587 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.39s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.39s
|
||
|
|
|
||
|
|
Iteration 14
|
||
|
|
Queue: [(0,30,13,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 15
|
||
|
|
Time : 219.254s (Solving: 215.23s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 219.252s
|
||
|
|
|
||
|
|
Choices : 7902024 (Domain: 7902000)
|
||
|
|
Conflicts : 395821 (Analyzed: 395821)
|
||
|
|
Restarts : 1401 (Average: 282.53 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 15 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 395821 (Deleted: 369254)
|
||
|
|
Binary : 3244 (Ratio: 0.82%)
|
||
|
|
Ternary : 2768 (Ratio: 0.70%)
|
||
|
|
Conflict : 395821 (Average Length: 1488.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 395821 (Average: 16.93 Max: 1535 Sum: 6702510)
|
||
|
|
Executed : 395712 (Average: 16.93 Max: 1535 Sum: 6699921 Ratio: 99.96%)
|
||
|
|
Bounded : 109 (Average: 23.75 Max: 32 Sum: 2589 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 12.97s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 12.97s
|
||
|
|
|
||
|
|
Iteration 15
|
||
|
|
Queue: [(0,30,14,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 16
|
||
|
|
Time : 232.422s (Solving: 228.36s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 232.424s
|
||
|
|
|
||
|
|
Choices : 8195399 (Domain: 8195375)
|
||
|
|
Conflicts : 420846 (Analyzed: 420846)
|
||
|
|
Restarts : 1501 (Average: 280.38 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 16 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 420846 (Deleted: 394454)
|
||
|
|
Binary : 3292 (Ratio: 0.78%)
|
||
|
|
Ternary : 2792 (Ratio: 0.66%)
|
||
|
|
Conflict : 420846 (Average Length: 1485.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 420846 (Average: 16.37 Max: 1535 Sum: 6888405)
|
||
|
|
Executed : 420737 (Average: 16.36 Max: 1535 Sum: 6885816 Ratio: 99.96%)
|
||
|
|
Bounded : 109 (Average: 23.75 Max: 32 Sum: 2589 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.17s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.18s
|
||
|
|
|
||
|
|
Iteration 16
|
||
|
|
Queue: [(0,30,15,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 17
|
||
|
|
Time : 246.630s (Solving: 242.55s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 246.636s
|
||
|
|
|
||
|
|
Choices : 8500375 (Domain: 8500351)
|
||
|
|
Conflicts : 446423 (Analyzed: 446423)
|
||
|
|
Restarts : 1601 (Average: 278.84 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 17 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 446423 (Deleted: 418980)
|
||
|
|
Binary : 3337 (Ratio: 0.75%)
|
||
|
|
Ternary : 2837 (Ratio: 0.64%)
|
||
|
|
Conflict : 446423 (Average Length: 1509.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 446423 (Average: 15.86 Max: 1535 Sum: 7080164)
|
||
|
|
Executed : 446313 (Average: 15.85 Max: 1535 Sum: 7077574 Ratio: 99.96%)
|
||
|
|
Bounded : 110 (Average: 23.55 Max: 32 Sum: 2590 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.22s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.22s
|
||
|
|
|
||
|
|
Iteration 17
|
||
|
|
Queue: [(0,30,16,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 18
|
||
|
|
Time : 259.925s (Solving: 255.81s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 259.936s
|
||
|
|
|
||
|
|
Choices : 8829133 (Domain: 8829109)
|
||
|
|
Conflicts : 472161 (Analyzed: 472161)
|
||
|
|
Restarts : 1701 (Average: 277.58 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 18 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 472161 (Deleted: 444020)
|
||
|
|
Binary : 3391 (Ratio: 0.72%)
|
||
|
|
Ternary : 2877 (Ratio: 0.61%)
|
||
|
|
Conflict : 472161 (Average Length: 1502.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 472161 (Average: 15.45 Max: 1535 Sum: 7292678)
|
||
|
|
Executed : 472050 (Average: 15.44 Max: 1535 Sum: 7290087 Ratio: 99.96%)
|
||
|
|
Bounded : 111 (Average: 23.34 Max: 32 Sum: 2591 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.30s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.30s
|
||
|
|
|
||
|
|
Iteration 18
|
||
|
|
Queue: [(0,30,17,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 19
|
||
|
|
Time : 273.349s (Solving: 269.21s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 273.368s
|
||
|
|
|
||
|
|
Choices : 9152743 (Domain: 9152719)
|
||
|
|
Conflicts : 497627 (Analyzed: 497627)
|
||
|
|
Restarts : 1801 (Average: 276.31 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 19 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 497627 (Deleted: 469531)
|
||
|
|
Binary : 3415 (Ratio: 0.69%)
|
||
|
|
Ternary : 2894 (Ratio: 0.58%)
|
||
|
|
Conflict : 497627 (Average Length: 1489.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 497627 (Average: 15.09 Max: 1535 Sum: 7506724)
|
||
|
|
Executed : 497515 (Average: 15.08 Max: 1535 Sum: 7504132 Ratio: 99.97%)
|
||
|
|
Bounded : 112 (Average: 23.14 Max: 32 Sum: 2592 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.43s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.43s
|
||
|
|
|
||
|
|
Iteration 19
|
||
|
|
Queue: [(0,30,18,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 20
|
||
|
|
Time : 286.647s (Solving: 282.48s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 286.676s
|
||
|
|
|
||
|
|
Choices : 9477763 (Domain: 9477739)
|
||
|
|
Conflicts : 524550 (Analyzed: 524550)
|
||
|
|
Restarts : 1901 (Average: 275.93 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 20 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 524550 (Deleted: 494282)
|
||
|
|
Binary : 3454 (Ratio: 0.66%)
|
||
|
|
Ternary : 2917 (Ratio: 0.56%)
|
||
|
|
Conflict : 524550 (Average Length: 1476.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 524550 (Average: 14.72 Max: 1535 Sum: 7719641)
|
||
|
|
Executed : 524437 (Average: 14.71 Max: 1535 Sum: 7717048 Ratio: 99.97%)
|
||
|
|
Bounded : 113 (Average: 22.95 Max: 32 Sum: 2593 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.31s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.31s
|
||
|
|
|
||
|
|
Iteration 20
|
||
|
|
Queue: [(0,30,19,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 21
|
||
|
|
Time : 301.954s (Solving: 297.74s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 301.988s
|
||
|
|
|
||
|
|
Choices : 9819391 (Domain: 9819367)
|
||
|
|
Conflicts : 554951 (Analyzed: 554951)
|
||
|
|
Restarts : 2001 (Average: 277.34 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 21 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 554951 (Deleted: 524093)
|
||
|
|
Binary : 3508 (Ratio: 0.63%)
|
||
|
|
Ternary : 2969 (Ratio: 0.54%)
|
||
|
|
Conflict : 554951 (Average Length: 1479.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 554951 (Average: 14.33 Max: 1535 Sum: 7950725)
|
||
|
|
Executed : 554836 (Average: 14.32 Max: 1535 Sum: 7948130 Ratio: 99.97%)
|
||
|
|
Bounded : 115 (Average: 22.57 Max: 32 Sum: 2595 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.32s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.32s
|
||
|
|
|
||
|
|
Iteration 21
|
||
|
|
Queue: [(0,30,20,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 22
|
||
|
|
Time : 315.880s (Solving: 311.64s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 315.920s
|
||
|
|
|
||
|
|
Choices : 10139241 (Domain: 10139217)
|
||
|
|
Conflicts : 580052 (Analyzed: 580052)
|
||
|
|
Restarts : 2101 (Average: 276.08 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 22 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 580052 (Deleted: 550660)
|
||
|
|
Binary : 3542 (Ratio: 0.61%)
|
||
|
|
Ternary : 2988 (Ratio: 0.52%)
|
||
|
|
Conflict : 580052 (Average Length: 1491.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 580052 (Average: 14.07 Max: 1535 Sum: 8158949)
|
||
|
|
Executed : 579937 (Average: 14.06 Max: 1535 Sum: 8156354 Ratio: 99.97%)
|
||
|
|
Bounded : 115 (Average: 22.57 Max: 32 Sum: 2595 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.93s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.93s
|
||
|
|
|
||
|
|
Iteration 22
|
||
|
|
Queue: [(0,30,21,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 23
|
||
|
|
Time : 329.775s (Solving: 325.51s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 329.820s
|
||
|
|
|
||
|
|
Choices : 10447769 (Domain: 10447745)
|
||
|
|
Conflicts : 607007 (Analyzed: 607007)
|
||
|
|
Restarts : 2201 (Average: 275.79 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 23 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 607007 (Deleted: 575354)
|
||
|
|
Binary : 3569 (Ratio: 0.59%)
|
||
|
|
Ternary : 3006 (Ratio: 0.50%)
|
||
|
|
Conflict : 607007 (Average Length: 1488.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 607007 (Average: 13.76 Max: 1535 Sum: 8355100)
|
||
|
|
Executed : 606892 (Average: 13.76 Max: 1535 Sum: 8352505 Ratio: 99.97%)
|
||
|
|
Bounded : 115 (Average: 22.57 Max: 32 Sum: 2595 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.90s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.90s
|
||
|
|
|
||
|
|
Iteration 23
|
||
|
|
Queue: [(0,30,22,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 24
|
||
|
|
Time : 344.692s (Solving: 340.39s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 344.744s
|
||
|
|
|
||
|
|
Choices : 10768072 (Domain: 10768048)
|
||
|
|
Conflicts : 633821 (Analyzed: 633821)
|
||
|
|
Restarts : 2301 (Average: 275.45 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 24 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 633821 (Deleted: 601851)
|
||
|
|
Binary : 3623 (Ratio: 0.57%)
|
||
|
|
Ternary : 3040 (Ratio: 0.48%)
|
||
|
|
Conflict : 633821 (Average Length: 1504.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 633821 (Average: 13.51 Max: 1535 Sum: 8563515)
|
||
|
|
Executed : 633705 (Average: 13.51 Max: 1535 Sum: 8560919 Ratio: 99.97%)
|
||
|
|
Bounded : 116 (Average: 22.38 Max: 32 Sum: 2596 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.93s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.93s
|
||
|
|
|
||
|
|
Iteration 24
|
||
|
|
Queue: [(0,30,23,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 25
|
||
|
|
Time : 360.194s (Solving: 355.85s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 360.252s
|
||
|
|
|
||
|
|
Choices : 11105100 (Domain: 11105076)
|
||
|
|
Conflicts : 661550 (Analyzed: 661550)
|
||
|
|
Restarts : 2401 (Average: 275.53 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 25 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 661550 (Deleted: 631137)
|
||
|
|
Binary : 3649 (Ratio: 0.55%)
|
||
|
|
Ternary : 3073 (Ratio: 0.46%)
|
||
|
|
Conflict : 661550 (Average Length: 1518.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 661550 (Average: 13.28 Max: 1535 Sum: 8786138)
|
||
|
|
Executed : 661434 (Average: 13.28 Max: 1535 Sum: 8783542 Ratio: 99.97%)
|
||
|
|
Bounded : 116 (Average: 22.38 Max: 32 Sum: 2596 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.51s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.51s
|
||
|
|
|
||
|
|
Iteration 25
|
||
|
|
Queue: [(0,30,24,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 26
|
||
|
|
Time : 375.078s (Solving: 370.70s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 375.144s
|
||
|
|
|
||
|
|
Choices : 11447050 (Domain: 11447026)
|
||
|
|
Conflicts : 689902 (Analyzed: 689902)
|
||
|
|
Restarts : 2501 (Average: 275.85 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 26 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 689902 (Deleted: 658486)
|
||
|
|
Binary : 3686 (Ratio: 0.53%)
|
||
|
|
Ternary : 3082 (Ratio: 0.45%)
|
||
|
|
Conflict : 689902 (Average Length: 1519.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 689902 (Average: 13.06 Max: 1535 Sum: 9010367)
|
||
|
|
Executed : 689783 (Average: 13.06 Max: 1535 Sum: 9007768 Ratio: 99.97%)
|
||
|
|
Bounded : 119 (Average: 21.84 Max: 32 Sum: 2599 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.89s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.89s
|
||
|
|
|
||
|
|
Iteration 26
|
||
|
|
Queue: [(0,30,25,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 27
|
||
|
|
Time : 391.008s (Solving: 386.60s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 391.080s
|
||
|
|
|
||
|
|
Choices : 11768423 (Domain: 11768399)
|
||
|
|
Conflicts : 718070 (Analyzed: 718070)
|
||
|
|
Restarts : 2601 (Average: 276.07 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 27 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 718070 (Deleted: 686479)
|
||
|
|
Binary : 3762 (Ratio: 0.52%)
|
||
|
|
Ternary : 3116 (Ratio: 0.43%)
|
||
|
|
Conflict : 718070 (Average Length: 1521.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 718070 (Average: 12.83 Max: 1535 Sum: 9209651)
|
||
|
|
Executed : 717951 (Average: 12.82 Max: 1535 Sum: 9207052 Ratio: 99.97%)
|
||
|
|
Bounded : 119 (Average: 21.84 Max: 32 Sum: 2599 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.94s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.94s
|
||
|
|
|
||
|
|
Iteration 27
|
||
|
|
Queue: [(0,30,26,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 28
|
||
|
|
Time : 405.208s (Solving: 400.78s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 405.284s
|
||
|
|
|
||
|
|
Choices : 12074394 (Domain: 12074370)
|
||
|
|
Conflicts : 743180 (Analyzed: 743180)
|
||
|
|
Restarts : 2701 (Average: 275.15 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 28 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 743180 (Deleted: 711475)
|
||
|
|
Binary : 3782 (Ratio: 0.51%)
|
||
|
|
Ternary : 3132 (Ratio: 0.42%)
|
||
|
|
Conflict : 743180 (Average Length: 1522.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 743180 (Average: 12.65 Max: 1535 Sum: 9399964)
|
||
|
|
Executed : 743061 (Average: 12.64 Max: 1535 Sum: 9397365 Ratio: 99.97%)
|
||
|
|
Bounded : 119 (Average: 21.84 Max: 32 Sum: 2599 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.21s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.21s
|
||
|
|
|
||
|
|
Iteration 28
|
||
|
|
Queue: [(0,30,27,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 29
|
||
|
|
Time : 420.958s (Solving: 416.51s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 421.040s
|
||
|
|
|
||
|
|
Choices : 12372119 (Domain: 12372095)
|
||
|
|
Conflicts : 769686 (Analyzed: 769686)
|
||
|
|
Restarts : 2801 (Average: 274.79 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 29 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 769686 (Deleted: 736713)
|
||
|
|
Binary : 3862 (Ratio: 0.50%)
|
||
|
|
Ternary : 3177 (Ratio: 0.41%)
|
||
|
|
Conflict : 769686 (Average Length: 1547.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 769686 (Average: 12.45 Max: 1535 Sum: 9579994)
|
||
|
|
Executed : 769566 (Average: 12.44 Max: 1535 Sum: 9577394 Ratio: 99.97%)
|
||
|
|
Bounded : 120 (Average: 21.67 Max: 32 Sum: 2600 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.76s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.76s
|
||
|
|
|
||
|
|
Iteration 29
|
||
|
|
Queue: [(0,30,28,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 30
|
||
|
|
Time : 436.217s (Solving: 431.73s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 436.308s
|
||
|
|
|
||
|
|
Choices : 12745014 (Domain: 12744990)
|
||
|
|
Conflicts : 796882 (Analyzed: 796882)
|
||
|
|
Restarts : 2901 (Average: 274.69 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 30 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 796882 (Deleted: 762166)
|
||
|
|
Binary : 3903 (Ratio: 0.49%)
|
||
|
|
Ternary : 3205 (Ratio: 0.40%)
|
||
|
|
Conflict : 796882 (Average Length: 1545.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 796882 (Average: 12.34 Max: 1535 Sum: 9831281)
|
||
|
|
Executed : 796762 (Average: 12.33 Max: 1535 Sum: 9828681 Ratio: 99.97%)
|
||
|
|
Bounded : 120 (Average: 21.67 Max: 32 Sum: 2600 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.27s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.27s
|
||
|
|
|
||
|
|
Iteration 30
|
||
|
|
Queue: [(0,30,29,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 31
|
||
|
|
Time : 449.609s (Solving: 445.08s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 449.704s
|
||
|
|
|
||
|
|
Choices : 13072022 (Domain: 13071998)
|
||
|
|
Conflicts : 821837 (Analyzed: 821837)
|
||
|
|
Restarts : 3001 (Average: 273.85 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 31 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 821837 (Deleted: 788956)
|
||
|
|
Binary : 3950 (Ratio: 0.48%)
|
||
|
|
Ternary : 3233 (Ratio: 0.39%)
|
||
|
|
Conflict : 821837 (Average Length: 1543.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 821837 (Average: 12.21 Max: 1535 Sum: 10036424)
|
||
|
|
Executed : 821717 (Average: 12.21 Max: 1535 Sum: 10033824 Ratio: 99.97%)
|
||
|
|
Bounded : 120 (Average: 21.67 Max: 32 Sum: 2600 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.40s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.40s
|
||
|
|
|
||
|
|
Iteration 31
|
||
|
|
Queue: [(0,30,30,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 32
|
||
|
|
Time : 464.982s (Solving: 460.42s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 465.084s
|
||
|
|
|
||
|
|
Choices : 13384092 (Domain: 13384068)
|
||
|
|
Conflicts : 848075 (Analyzed: 848075)
|
||
|
|
Restarts : 3101 (Average: 273.48 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 32 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 848075 (Deleted: 813488)
|
||
|
|
Binary : 4016 (Ratio: 0.47%)
|
||
|
|
Ternary : 3273 (Ratio: 0.39%)
|
||
|
|
Conflict : 848075 (Average Length: 1559.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 848075 (Average: 12.06 Max: 1535 Sum: 10229951)
|
||
|
|
Executed : 847954 (Average: 12.06 Max: 1535 Sum: 10227350 Ratio: 99.97%)
|
||
|
|
Bounded : 121 (Average: 21.50 Max: 32 Sum: 2601 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.38s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.38s
|
||
|
|
|
||
|
|
Iteration 32
|
||
|
|
Queue: [(0,30,31,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 33
|
||
|
|
Time : 480.647s (Solving: 476.06s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 480.756s
|
||
|
|
|
||
|
|
Choices : 13708035 (Domain: 13708011)
|
||
|
|
Conflicts : 876603 (Analyzed: 876603)
|
||
|
|
Restarts : 3201 (Average: 273.85 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 33 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 876603 (Deleted: 842286)
|
||
|
|
Binary : 4036 (Ratio: 0.46%)
|
||
|
|
Ternary : 3291 (Ratio: 0.38%)
|
||
|
|
Conflict : 876603 (Average Length: 1563.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 876603 (Average: 11.90 Max: 1535 Sum: 10433637)
|
||
|
|
Executed : 876480 (Average: 11.90 Max: 1535 Sum: 10431034 Ratio: 99.98%)
|
||
|
|
Bounded : 123 (Average: 21.16 Max: 32 Sum: 2603 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.67s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.67s
|
||
|
|
|
||
|
|
Iteration 33
|
||
|
|
Queue: [(0,30,32,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 34
|
||
|
|
Time : 494.767s (Solving: 490.15s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 494.884s
|
||
|
|
|
||
|
|
Choices : 14036749 (Domain: 14036725)
|
||
|
|
Conflicts : 904023 (Analyzed: 904023)
|
||
|
|
Restarts : 3301 (Average: 273.86 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 34 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 904023 (Deleted: 867598)
|
||
|
|
Binary : 4061 (Ratio: 0.45%)
|
||
|
|
Ternary : 3306 (Ratio: 0.37%)
|
||
|
|
Conflict : 904023 (Average Length: 1557.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 904023 (Average: 11.77 Max: 1535 Sum: 10641647)
|
||
|
|
Executed : 903899 (Average: 11.77 Max: 1535 Sum: 10639043 Ratio: 99.98%)
|
||
|
|
Bounded : 124 (Average: 21.00 Max: 32 Sum: 2604 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.13s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.13s
|
||
|
|
|
||
|
|
Iteration 34
|
||
|
|
Queue: [(0,30,33,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 35
|
||
|
|
Time : 509.227s (Solving: 504.56s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 509.348s
|
||
|
|
|
||
|
|
Choices : 14361761 (Domain: 14361737)
|
||
|
|
Conflicts : 930324 (Analyzed: 930324)
|
||
|
|
Restarts : 3401 (Average: 273.54 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 35 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 930324 (Deleted: 894704)
|
||
|
|
Binary : 4096 (Ratio: 0.44%)
|
||
|
|
Ternary : 3318 (Ratio: 0.36%)
|
||
|
|
Conflict : 930324 (Average Length: 1555.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 930324 (Average: 11.66 Max: 1535 Sum: 10848082)
|
||
|
|
Executed : 930199 (Average: 11.66 Max: 1535 Sum: 10845477 Ratio: 99.98%)
|
||
|
|
Bounded : 125 (Average: 20.84 Max: 32 Sum: 2605 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.47s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.47s
|
||
|
|
|
||
|
|
Iteration 35
|
||
|
|
Queue: [(0,30,34,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 36
|
||
|
|
Time : 523.957s (Solving: 519.26s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 524.084s
|
||
|
|
|
||
|
|
Choices : 14665881 (Domain: 14665857)
|
||
|
|
Conflicts : 956807 (Analyzed: 956807)
|
||
|
|
Restarts : 3501 (Average: 273.30 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 36 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 956807 (Deleted: 920700)
|
||
|
|
Binary : 4114 (Ratio: 0.43%)
|
||
|
|
Ternary : 3327 (Ratio: 0.35%)
|
||
|
|
Conflict : 956807 (Average Length: 1552.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 956807 (Average: 11.53 Max: 1535 Sum: 11034020)
|
||
|
|
Executed : 956680 (Average: 11.53 Max: 1535 Sum: 11031413 Ratio: 99.98%)
|
||
|
|
Bounded : 127 (Average: 20.53 Max: 32 Sum: 2607 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.74s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.74s
|
||
|
|
|
||
|
|
Iteration 36
|
||
|
|
Queue: [(0,30,35,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 37
|
||
|
|
Time : 537.897s (Solving: 533.17s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 538.028s
|
||
|
|
|
||
|
|
Choices : 14979466 (Domain: 14979442)
|
||
|
|
Conflicts : 984516 (Analyzed: 984516)
|
||
|
|
Restarts : 3601 (Average: 273.40 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 37 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 984516 (Deleted: 949797)
|
||
|
|
Binary : 4132 (Ratio: 0.42%)
|
||
|
|
Ternary : 3338 (Ratio: 0.34%)
|
||
|
|
Conflict : 984516 (Average Length: 1542.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 984516 (Average: 11.40 Max: 1535 Sum: 11225450)
|
||
|
|
Executed : 984388 (Average: 11.40 Max: 1535 Sum: 11222811 Ratio: 99.98%)
|
||
|
|
Bounded : 128 (Average: 20.62 Max: 32 Sum: 2639 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876970 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.95s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.95s
|
||
|
|
|
||
|
|
Iteration 37
|
||
|
|
Queue: [(0,30,36,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 38
|
||
|
|
Time : 553.847s (Solving: 549.09s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 553.984s
|
||
|
|
|
||
|
|
Choices : 15291010 (Domain: 15290986)
|
||
|
|
Conflicts : 1014439 (Analyzed: 1014439)
|
||
|
|
Restarts : 3701 (Average: 274.10 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 38 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1014439 (Deleted: 977194)
|
||
|
|
Binary : 4165 (Ratio: 0.41%)
|
||
|
|
Ternary : 3351 (Ratio: 0.33%)
|
||
|
|
Conflict : 1014439 (Average Length: 1548.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1014439 (Average: 11.26 Max: 1535 Sum: 11419058)
|
||
|
|
Executed : 1014308 (Average: 11.25 Max: 1535 Sum: 11416385 Ratio: 99.98%)
|
||
|
|
Bounded : 131 (Average: 20.40 Max: 32 Sum: 2673 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876958 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.96s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.96s
|
||
|
|
|
||
|
|
Iteration 38
|
||
|
|
Queue: [(0,30,37,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 39
|
||
|
|
Time : 568.027s (Solving: 563.23s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 568.168s
|
||
|
|
|
||
|
|
Choices : 15577118 (Domain: 15577094)
|
||
|
|
Conflicts : 1040686 (Analyzed: 1040686)
|
||
|
|
Restarts : 3801 (Average: 273.79 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 39 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1040686 (Deleted: 1003935)
|
||
|
|
Binary : 4194 (Ratio: 0.40%)
|
||
|
|
Ternary : 3363 (Ratio: 0.32%)
|
||
|
|
Conflict : 1040686 (Average Length: 1548.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1040686 (Average: 11.14 Max: 1535 Sum: 11593785)
|
||
|
|
Executed : 1040554 (Average: 11.14 Max: 1535 Sum: 11591111 Ratio: 99.98%)
|
||
|
|
Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.19s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.19s
|
||
|
|
|
||
|
|
Iteration 39
|
||
|
|
Queue: [(0,30,38,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 40
|
||
|
|
Time : 582.016s (Solving: 577.20s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 582.164s
|
||
|
|
|
||
|
|
Choices : 15879418 (Domain: 15879394)
|
||
|
|
Conflicts : 1065048 (Analyzed: 1065048)
|
||
|
|
Restarts : 3901 (Average: 273.02 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 40 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1065048 (Deleted: 1027091)
|
||
|
|
Binary : 4223 (Ratio: 0.40%)
|
||
|
|
Ternary : 3384 (Ratio: 0.32%)
|
||
|
|
Conflict : 1065048 (Average Length: 1549.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1065048 (Average: 11.08 Max: 1535 Sum: 11802952)
|
||
|
|
Executed : 1064916 (Average: 11.08 Max: 1535 Sum: 11800278 Ratio: 99.98%)
|
||
|
|
Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.00s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.00s
|
||
|
|
|
||
|
|
Iteration 40
|
||
|
|
Queue: [(0,30,39,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 41
|
||
|
|
Time : 596.192s (Solving: 591.34s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 596.348s
|
||
|
|
|
||
|
|
Choices : 16207654 (Domain: 16207630)
|
||
|
|
Conflicts : 1089862 (Analyzed: 1089862)
|
||
|
|
Restarts : 4001 (Average: 272.40 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 41 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1089862 (Deleted: 1053980)
|
||
|
|
Binary : 4260 (Ratio: 0.39%)
|
||
|
|
Ternary : 3410 (Ratio: 0.31%)
|
||
|
|
Conflict : 1089862 (Average Length: 1550.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1089862 (Average: 11.04 Max: 1535 Sum: 12033198)
|
||
|
|
Executed : 1089730 (Average: 11.04 Max: 1535 Sum: 12030524 Ratio: 99.98%)
|
||
|
|
Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.18s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.18s
|
||
|
|
|
||
|
|
Iteration 41
|
||
|
|
Queue: [(0,30,40,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 42
|
||
|
|
Time : 610.113s (Solving: 605.24s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 610.276s
|
||
|
|
|
||
|
|
Choices : 16541036 (Domain: 16541012)
|
||
|
|
Conflicts : 1116124 (Analyzed: 1116124)
|
||
|
|
Restarts : 4101 (Average: 272.16 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 42 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1116124 (Deleted: 1078393)
|
||
|
|
Binary : 4307 (Ratio: 0.39%)
|
||
|
|
Ternary : 3445 (Ratio: 0.31%)
|
||
|
|
Conflict : 1116124 (Average Length: 1550.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1116124 (Average: 10.99 Max: 1535 Sum: 12263768)
|
||
|
|
Executed : 1115992 (Average: 10.99 Max: 1535 Sum: 12261094 Ratio: 99.98%)
|
||
|
|
Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.93s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.93s
|
||
|
|
|
||
|
|
Iteration 42
|
||
|
|
Queue: [(0,30,41,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 43
|
||
|
|
Time : 624.032s (Solving: 619.12s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 624.200s
|
||
|
|
|
||
|
|
Choices : 16887218 (Domain: 16887194)
|
||
|
|
Conflicts : 1142136 (Analyzed: 1142136)
|
||
|
|
Restarts : 4201 (Average: 271.87 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 43 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1142136 (Deleted: 1104338)
|
||
|
|
Binary : 4326 (Ratio: 0.38%)
|
||
|
|
Ternary : 3467 (Ratio: 0.30%)
|
||
|
|
Conflict : 1142136 (Average Length: 1546.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1142136 (Average: 10.95 Max: 1535 Sum: 12509555)
|
||
|
|
Executed : 1142004 (Average: 10.95 Max: 1535 Sum: 12506881 Ratio: 99.98%)
|
||
|
|
Bounded : 132 (Average: 20.26 Max: 32 Sum: 2674 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.93s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.93s
|
||
|
|
|
||
|
|
Iteration 43
|
||
|
|
Queue: [(0,30,42,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 44
|
||
|
|
Time : 638.509s (Solving: 633.57s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 638.684s
|
||
|
|
|
||
|
|
Choices : 17268384 (Domain: 17268360)
|
||
|
|
Conflicts : 1166754 (Analyzed: 1166754)
|
||
|
|
Restarts : 4301 (Average: 271.28 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 44 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1166754 (Deleted: 1130124)
|
||
|
|
Binary : 4345 (Ratio: 0.37%)
|
||
|
|
Ternary : 3481 (Ratio: 0.30%)
|
||
|
|
Conflict : 1166754 (Average Length: 1545.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1166754 (Average: 10.96 Max: 1535 Sum: 12792440)
|
||
|
|
Executed : 1166621 (Average: 10.96 Max: 1535 Sum: 12789765 Ratio: 99.98%)
|
||
|
|
Bounded : 133 (Average: 20.11 Max: 32 Sum: 2675 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.48s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.48s
|
||
|
|
|
||
|
|
Iteration 44
|
||
|
|
Queue: [(0,30,43,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 45
|
||
|
|
Time : 654.183s (Solving: 649.20s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 654.364s
|
||
|
|
|
||
|
|
Choices : 17574339 (Domain: 17574315)
|
||
|
|
Conflicts : 1194093 (Analyzed: 1194093)
|
||
|
|
Restarts : 4401 (Average: 271.32 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 45 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1194093 (Deleted: 1154414)
|
||
|
|
Binary : 4394 (Ratio: 0.37%)
|
||
|
|
Ternary : 3527 (Ratio: 0.30%)
|
||
|
|
Conflict : 1194093 (Average Length: 1549.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1194093 (Average: 10.89 Max: 1535 Sum: 13002423)
|
||
|
|
Executed : 1193960 (Average: 10.89 Max: 1535 Sum: 12999748 Ratio: 99.98%)
|
||
|
|
Bounded : 133 (Average: 20.11 Max: 32 Sum: 2675 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.68s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.68s
|
||
|
|
|
||
|
|
Iteration 45
|
||
|
|
Queue: [(0,30,44,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 46
|
||
|
|
Time : 668.361s (Solving: 663.34s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 668.548s
|
||
|
|
|
||
|
|
Choices : 17873188 (Domain: 17873164)
|
||
|
|
Conflicts : 1218783 (Analyzed: 1218783)
|
||
|
|
Restarts : 4501 (Average: 270.78 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 46 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1218783 (Deleted: 1181472)
|
||
|
|
Binary : 4416 (Ratio: 0.36%)
|
||
|
|
Ternary : 3555 (Ratio: 0.29%)
|
||
|
|
Conflict : 1218783 (Average Length: 1546.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1218783 (Average: 10.84 Max: 1535 Sum: 13206694)
|
||
|
|
Executed : 1218649 (Average: 10.83 Max: 1535 Sum: 13203987 Ratio: 99.98%)
|
||
|
|
Bounded : 134 (Average: 20.20 Max: 32 Sum: 2707 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876946 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.19s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.19s
|
||
|
|
|
||
|
|
Iteration 46
|
||
|
|
Queue: [(0,30,45,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 47
|
||
|
|
Time : 681.735s (Solving: 676.69s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 681.928s
|
||
|
|
|
||
|
|
Choices : 18161588 (Domain: 18161564)
|
||
|
|
Conflicts : 1243661 (Analyzed: 1243661)
|
||
|
|
Restarts : 4601 (Average: 270.30 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 47 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1243661 (Deleted: 1205793)
|
||
|
|
Binary : 4446 (Ratio: 0.36%)
|
||
|
|
Ternary : 3569 (Ratio: 0.29%)
|
||
|
|
Conflict : 1243661 (Average Length: 1542.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1243661 (Average: 10.77 Max: 1535 Sum: 13391413)
|
||
|
|
Executed : 1243526 (Average: 10.77 Max: 1535 Sum: 13388705 Ratio: 99.98%)
|
||
|
|
Bounded : 135 (Average: 20.06 Max: 32 Sum: 2708 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876934 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.38s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.38s
|
||
|
|
|
||
|
|
Iteration 47
|
||
|
|
Queue: [(0,30,46,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 48
|
||
|
|
Time : 696.387s (Solving: 691.30s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 696.588s
|
||
|
|
|
||
|
|
Choices : 18462804 (Domain: 18462780)
|
||
|
|
Conflicts : 1269171 (Analyzed: 1269171)
|
||
|
|
Restarts : 4701 (Average: 269.98 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 48 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1269171 (Deleted: 1230466)
|
||
|
|
Binary : 4478 (Ratio: 0.35%)
|
||
|
|
Ternary : 3592 (Ratio: 0.28%)
|
||
|
|
Conflict : 1269171 (Average Length: 1547.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1269171 (Average: 10.70 Max: 1535 Sum: 13585959)
|
||
|
|
Executed : 1269035 (Average: 10.70 Max: 1535 Sum: 13583219 Ratio: 99.98%)
|
||
|
|
Bounded : 136 (Average: 20.15 Max: 32 Sum: 2740 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876934 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.66s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.66s
|
||
|
|
|
||
|
|
Iteration 48
|
||
|
|
Queue: [(0,30,47,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 49
|
||
|
|
Time : 710.676s (Solving: 705.56s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 710.884s
|
||
|
|
|
||
|
|
Choices : 18757681 (Domain: 18757657)
|
||
|
|
Conflicts : 1295037 (Analyzed: 1295037)
|
||
|
|
Restarts : 4801 (Average: 269.74 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 49 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1295037 (Deleted: 1255761)
|
||
|
|
Binary : 4498 (Ratio: 0.35%)
|
||
|
|
Ternary : 3597 (Ratio: 0.28%)
|
||
|
|
Conflict : 1295037 (Average Length: 1541.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1295037 (Average: 10.65 Max: 1535 Sum: 13785693)
|
||
|
|
Executed : 1294900 (Average: 10.64 Max: 1535 Sum: 13782952 Ratio: 99.98%)
|
||
|
|
Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.30s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.30s
|
||
|
|
|
||
|
|
Iteration 49
|
||
|
|
Queue: [(0,30,48,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 50
|
||
|
|
Time : 724.048s (Solving: 718.91s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 724.260s
|
||
|
|
|
||
|
|
Choices : 19087757 (Domain: 19087733)
|
||
|
|
Conflicts : 1320354 (Analyzed: 1320354)
|
||
|
|
Restarts : 4901 (Average: 269.41 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 50 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1320354 (Deleted: 1281163)
|
||
|
|
Binary : 4529 (Ratio: 0.34%)
|
||
|
|
Ternary : 3621 (Ratio: 0.27%)
|
||
|
|
Conflict : 1320354 (Average Length: 1534.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1320354 (Average: 10.61 Max: 1535 Sum: 14015035)
|
||
|
|
Executed : 1320217 (Average: 10.61 Max: 1535 Sum: 14012294 Ratio: 99.98%)
|
||
|
|
Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.38s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.38s
|
||
|
|
|
||
|
|
Iteration 50
|
||
|
|
Queue: [(0,30,49,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 51
|
||
|
|
Time : 736.820s (Solving: 731.65s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 737.036s
|
||
|
|
|
||
|
|
Choices : 19402130 (Domain: 19402106)
|
||
|
|
Conflicts : 1343463 (Analyzed: 1343463)
|
||
|
|
Restarts : 5001 (Average: 268.64 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 51 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1343463 (Deleted: 1303436)
|
||
|
|
Binary : 4556 (Ratio: 0.34%)
|
||
|
|
Ternary : 3639 (Ratio: 0.27%)
|
||
|
|
Conflict : 1343463 (Average Length: 1531.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1343463 (Average: 10.59 Max: 1535 Sum: 14224897)
|
||
|
|
Executed : 1343326 (Average: 10.59 Max: 1535 Sum: 14222156 Ratio: 99.98%)
|
||
|
|
Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 12.78s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 12.78s
|
||
|
|
|
||
|
|
Iteration 51
|
||
|
|
Queue: [(0,30,50,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 52
|
||
|
|
Time : 751.174s (Solving: 745.97s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 751.396s
|
||
|
|
|
||
|
|
Choices : 19726312 (Domain: 19726288)
|
||
|
|
Conflicts : 1368998 (Analyzed: 1368998)
|
||
|
|
Restarts : 5101 (Average: 268.38 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 52 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1368998 (Deleted: 1329013)
|
||
|
|
Binary : 4579 (Ratio: 0.33%)
|
||
|
|
Ternary : 3652 (Ratio: 0.27%)
|
||
|
|
Conflict : 1368998 (Average Length: 1532.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1368998 (Average: 10.55 Max: 1535 Sum: 14446001)
|
||
|
|
Executed : 1368861 (Average: 10.55 Max: 1535 Sum: 14443260 Ratio: 99.98%)
|
||
|
|
Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.36s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.36s
|
||
|
|
|
||
|
|
Iteration 52
|
||
|
|
Queue: [(0,30,51,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 53
|
||
|
|
Time : 765.500s (Solving: 760.25s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 765.728s
|
||
|
|
|
||
|
|
Choices : 20091443 (Domain: 20091419)
|
||
|
|
Conflicts : 1395186 (Analyzed: 1395186)
|
||
|
|
Restarts : 5201 (Average: 268.25 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 53 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1395186 (Deleted: 1354356)
|
||
|
|
Binary : 4597 (Ratio: 0.33%)
|
||
|
|
Ternary : 3662 (Ratio: 0.26%)
|
||
|
|
Conflict : 1395186 (Average Length: 1525.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1395186 (Average: 10.54 Max: 1535 Sum: 14710018)
|
||
|
|
Executed : 1395049 (Average: 10.54 Max: 1535 Sum: 14707277 Ratio: 99.98%)
|
||
|
|
Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.33s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.33s
|
||
|
|
|
||
|
|
Iteration 53
|
||
|
|
Queue: [(0,30,52,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 54
|
||
|
|
Time : 778.559s (Solving: 773.28s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 778.792s
|
||
|
|
|
||
|
|
Choices : 20410556 (Domain: 20410532)
|
||
|
|
Conflicts : 1418624 (Analyzed: 1418624)
|
||
|
|
Restarts : 5301 (Average: 267.61 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 54 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1418624 (Deleted: 1377514)
|
||
|
|
Binary : 4602 (Ratio: 0.32%)
|
||
|
|
Ternary : 3663 (Ratio: 0.26%)
|
||
|
|
Conflict : 1418624 (Average Length: 1519.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1418624 (Average: 10.52 Max: 1535 Sum: 14927946)
|
||
|
|
Executed : 1418487 (Average: 10.52 Max: 1535 Sum: 14925205 Ratio: 99.98%)
|
||
|
|
Bounded : 137 (Average: 20.01 Max: 32 Sum: 2741 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.07s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.07s
|
||
|
|
|
||
|
|
Iteration 54
|
||
|
|
Queue: [(0,30,53,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 55
|
||
|
|
Time : 793.323s (Solving: 788.01s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 793.564s
|
||
|
|
|
||
|
|
Choices : 20718909 (Domain: 20718885)
|
||
|
|
Conflicts : 1444592 (Analyzed: 1444592)
|
||
|
|
Restarts : 5401 (Average: 267.47 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 55 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1444592 (Deleted: 1403553)
|
||
|
|
Binary : 4611 (Ratio: 0.32%)
|
||
|
|
Ternary : 3670 (Ratio: 0.25%)
|
||
|
|
Conflict : 1444592 (Average Length: 1515.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1444592 (Average: 10.47 Max: 1535 Sum: 15131324)
|
||
|
|
Executed : 1444454 (Average: 10.47 Max: 1535 Sum: 15128551 Ratio: 99.98%)
|
||
|
|
Bounded : 138 (Average: 20.09 Max: 32 Sum: 2773 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876922 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.77s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.77s
|
||
|
|
|
||
|
|
Iteration 55
|
||
|
|
Queue: [(0,30,54,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 56
|
||
|
|
Time : 807.526s (Solving: 802.19s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 807.776s
|
||
|
|
|
||
|
|
Choices : 21012255 (Domain: 21012231)
|
||
|
|
Conflicts : 1470925 (Analyzed: 1470925)
|
||
|
|
Restarts : 5501 (Average: 267.39 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 56 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1470925 (Deleted: 1429221)
|
||
|
|
Binary : 4658 (Ratio: 0.32%)
|
||
|
|
Ternary : 3684 (Ratio: 0.25%)
|
||
|
|
Conflict : 1470925 (Average Length: 1519.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1470925 (Average: 10.42 Max: 1535 Sum: 15324542)
|
||
|
|
Executed : 1470787 (Average: 10.42 Max: 1535 Sum: 15321769 Ratio: 99.98%)
|
||
|
|
Bounded : 138 (Average: 20.09 Max: 32 Sum: 2773 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.21s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.21s
|
||
|
|
|
||
|
|
Iteration 56
|
||
|
|
Queue: [(0,30,55,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 57
|
||
|
|
Time : 821.013s (Solving: 815.64s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 821.268s
|
||
|
|
|
||
|
|
Choices : 21318347 (Domain: 21318323)
|
||
|
|
Conflicts : 1496657 (Analyzed: 1496657)
|
||
|
|
Restarts : 5601 (Average: 267.21 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 57 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1496657 (Deleted: 1455347)
|
||
|
|
Binary : 4671 (Ratio: 0.31%)
|
||
|
|
Ternary : 3691 (Ratio: 0.25%)
|
||
|
|
Conflict : 1496657 (Average Length: 1516.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1496657 (Average: 10.38 Max: 1535 Sum: 15529417)
|
||
|
|
Executed : 1496518 (Average: 10.37 Max: 1535 Sum: 15526643 Ratio: 99.98%)
|
||
|
|
Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.50s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.50s
|
||
|
|
|
||
|
|
Iteration 57
|
||
|
|
Queue: [(0,30,56,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 58
|
||
|
|
Time : 834.893s (Solving: 829.48s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 835.152s
|
||
|
|
|
||
|
|
Choices : 21631508 (Domain: 21631484)
|
||
|
|
Conflicts : 1520661 (Analyzed: 1520661)
|
||
|
|
Restarts : 5701 (Average: 266.74 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 58 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1520661 (Deleted: 1478049)
|
||
|
|
Binary : 4684 (Ratio: 0.31%)
|
||
|
|
Ternary : 3706 (Ratio: 0.24%)
|
||
|
|
Conflict : 1520661 (Average Length: 1516.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1520661 (Average: 10.35 Max: 1535 Sum: 15736535)
|
||
|
|
Executed : 1520522 (Average: 10.35 Max: 1535 Sum: 15733761 Ratio: 99.98%)
|
||
|
|
Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.89s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.89s
|
||
|
|
|
||
|
|
Iteration 58
|
||
|
|
Queue: [(0,30,57,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 59
|
||
|
|
Time : 848.393s (Solving: 842.94s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 848.656s
|
||
|
|
|
||
|
|
Choices : 21917820 (Domain: 21917796)
|
||
|
|
Conflicts : 1543956 (Analyzed: 1543956)
|
||
|
|
Restarts : 5801 (Average: 266.15 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 59 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1543956 (Deleted: 1501839)
|
||
|
|
Binary : 4701 (Ratio: 0.30%)
|
||
|
|
Ternary : 3718 (Ratio: 0.24%)
|
||
|
|
Conflict : 1543956 (Average Length: 1515.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1543956 (Average: 10.31 Max: 1535 Sum: 15923496)
|
||
|
|
Executed : 1543817 (Average: 10.31 Max: 1535 Sum: 15920722 Ratio: 99.98%)
|
||
|
|
Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.51s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.51s
|
||
|
|
|
||
|
|
Iteration 59
|
||
|
|
Queue: [(0,30,58,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 60
|
||
|
|
Time : 863.223s (Solving: 857.75s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 863.492s
|
||
|
|
|
||
|
|
Choices : 22234122 (Domain: 22234098)
|
||
|
|
Conflicts : 1569941 (Analyzed: 1569941)
|
||
|
|
Restarts : 5901 (Average: 266.05 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 60 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1569941 (Deleted: 1527679)
|
||
|
|
Binary : 4724 (Ratio: 0.30%)
|
||
|
|
Ternary : 3722 (Ratio: 0.24%)
|
||
|
|
Conflict : 1569941 (Average Length: 1513.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1569941 (Average: 10.28 Max: 1535 Sum: 16135091)
|
||
|
|
Executed : 1569802 (Average: 10.28 Max: 1535 Sum: 16132317 Ratio: 99.98%)
|
||
|
|
Bounded : 139 (Average: 19.96 Max: 32 Sum: 2774 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 14.84s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 14.84s
|
||
|
|
|
||
|
|
Iteration 60
|
||
|
|
Queue: [(0,30,59,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 61
|
||
|
|
Time : 876.789s (Solving: 871.29s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 877.064s
|
||
|
|
|
||
|
|
Choices : 22525850 (Domain: 22525826)
|
||
|
|
Conflicts : 1593773 (Analyzed: 1593773)
|
||
|
|
Restarts : 6001 (Average: 265.58 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 61 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1593773 (Deleted: 1550691)
|
||
|
|
Binary : 4735 (Ratio: 0.30%)
|
||
|
|
Ternary : 3733 (Ratio: 0.23%)
|
||
|
|
Conflict : 1593773 (Average Length: 1511.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1593773 (Average: 10.25 Max: 1535 Sum: 16330011)
|
||
|
|
Executed : 1593633 (Average: 10.24 Max: 1535 Sum: 16327236 Ratio: 99.98%)
|
||
|
|
Bounded : 140 (Average: 19.82 Max: 32 Sum: 2775 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 13.57s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 13.58s
|
||
|
|
|
||
|
|
Iteration 61
|
||
|
|
Queue: [(0,30,60,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 62
|
||
|
|
Time : 891.934s (Solving: 886.39s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 892.216s
|
||
|
|
|
||
|
|
Choices : 22805746 (Domain: 22805722)
|
||
|
|
Conflicts : 1619161 (Analyzed: 1619161)
|
||
|
|
Restarts : 6101 (Average: 265.39 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 62 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1619161 (Deleted: 1577125)
|
||
|
|
Binary : 4759 (Ratio: 0.29%)
|
||
|
|
Ternary : 3741 (Ratio: 0.23%)
|
||
|
|
Conflict : 1619161 (Average Length: 1511.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1619161 (Average: 10.19 Max: 1535 Sum: 16505965)
|
||
|
|
Executed : 1619021 (Average: 10.19 Max: 1535 Sum: 16503190 Ratio: 99.98%)
|
||
|
|
Bounded : 140 (Average: 19.82 Max: 32 Sum: 2775 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 15.15s
|
||
|
|
Memory: 382MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 15.15s
|
||
|
|
|
||
|
|
Iteration 62
|
||
|
|
Queue: [(0,30,61,True)]
|
||
|
|
Grounded Until: 30
|
||
|
|
Solving...
|
||
|
|
*** Info : (planner): INTERRUPTED by signal!
|
||
|
|
UNKNOWN
|
||
|
|
|
||
|
|
INTERRUPTED : 1
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 63
|
||
|
|
Time : 894.175s (Solving: 888.60s 1st Model: 0.06s Unsat: 0.00s)
|
||
|
|
CPU Time : 894.440s
|
||
|
|
|
||
|
|
Choices : 22863173 (Domain: 22863149)
|
||
|
|
Conflicts : 1622864 (Analyzed: 1622864)
|
||
|
|
Restarts : 6125 (Average: 264.96 Last: 289)
|
||
|
|
Model-Level : 1229.0
|
||
|
|
Problems : 63 (Average Length: 32.00 Splits: 0)
|
||
|
|
Lemmas : 1622864 (Deleted: 1581658)
|
||
|
|
Binary : 4771 (Ratio: 0.29%)
|
||
|
|
Ternary : 3745 (Ratio: 0.23%)
|
||
|
|
Conflict : 1622864 (Average Length: 1511.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1622864 (Average: 10.19 Max: 1535 Sum: 16537536)
|
||
|
|
Executed : 1622724 (Average: 10.19 Max: 1535 Sum: 16534761 Ratio: 99.98%)
|
||
|
|
Bounded : 140 (Average: 19.82 Max: 32 Sum: 2775 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 222636 (Original: 222598)
|
||
|
|
Atoms : 6829
|
||
|
|
Bodies : 147015 (Original: 146977)
|
||
|
|
Count : 629 (Original: 633)
|
||
|
|
Equivalences : 76243 (Atom=Atom: 36 Body=Body: 0 Other: 76207)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 103790 (Eliminated: 0 Frozen: 85188)
|
||
|
|
Constraints : 876910 (Binary: 97.7% Ternary: 1.0% Other: 1.3%)
|
||
|
|
|
||
|
|
Memory Peak : 446MB
|
||
|
|
Max. Length : 30 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
|