tplp-planning-benchmark/gc-ta1-tt1/ipc-2011_barman-sequential-satisficing_20.out

4802 lines
176 KiB
Plaintext

INFO Running translator.
INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-20.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/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-20.pddl
Parsing...
Parsing: [0.040s CPU, 0.043s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.012s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.050s CPU, 0.053s wall-clock]
Preparing model... [0.030s CPU, 0.030s wall-clock]
Generated 115 rules.
Computing model... [0.540s CPU, 0.544s wall-clock]
3296 relevant atoms
3425 auxiliary atoms
6721 final queue length
11595 total queue pushes
Completing instantiation... [1.030s CPU, 1.030s wall-clock]
Instantiating: [1.680s CPU, 1.676s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.140s CPU, 0.142s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.010s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
350 uncovered facts
Choosing groups: [0.000s CPU, 0.002s wall-clock]
Building translation key... [0.010s CPU, 0.014s wall-clock]
Computing fact groups: [0.190s CPU, 0.197s wall-clock]
Building STRIPS to SAS dictionary... [0.010s CPU, 0.006s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.003s wall-clock]
Building mutex information...
Building mutex information: [0.010s CPU, 0.004s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.050s CPU, 0.056s wall-clock]
Translating task: [1.060s CPU, 1.070s wall-clock]
3920 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.590s CPU, 0.591s wall-clock]
Reordering and filtering variables...
353 of 353 variables necessary.
16 of 19 mutex groups necessary.
2344 of 2344 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.380s CPU, 0.379s wall-clock]
Translator variables: 353
Translator derived variables: 0
Translator facts: 737
Translator goal facts: 14
Translator mutex groups: 16
Translator total mutex groups size: 48
Translator operators: 2344
Translator axioms: 0
Translator task size: 22454
Translator peak memory: 49100 KB
Writing output... [0.370s CPU, 0.407s wall-clock]
Done! [4.380s CPU, 4.422s wall-clock]
planner.py version 0.0.1
Time: 0.92s
Memory: 111MB
Iteration 1
Queue: [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 0
Solving...
[start: stats after solve call]
Models : 0
Calls : 1
Time : 1.109s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.924s
Choices : 0
Conflicts : 0 (Analyzed: 0)
Restarts : 0
Problems : 1 (Average Length: 2.00 Splits: 0)
Lemmas : 0 (Deleted: 0)
Binary : 0 (Ratio: 0.00%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 0 (Average Length: 0.0 Ratio: 0.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0)
Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%)
Rules : 64767
Atoms : 64767
Bodies : 1 (Original: 0)
Tight : Yes
Variables : 0 (Eliminated: 0 Frozen: 0)
Constraints : 0 (Binary: 0.0% Ternary: 0.0% Other: 0.0%)
Memory Peak : 247MB
Max. Length : 0 steps
Models : 0
[endof: stats after solve call]
Solving Time: 0.01s
Memory: 183MB (+72MB)
UNSAT
Iteration Time: 0.01s
Iteration 2
Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 0
Expected Memory: 183MB
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
Grounding Time: 0.28s
Memory: 183MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 1+
Calls : 2
Time : 1.543s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 1.360s
Choices : 195 (Domain: 36)
Conflicts : 4 (Analyzed: 4)
Restarts : 0
Model-Level : 183.0
Problems : 2 (Average Length: 4.50 Splits: 0)
Lemmas : 4 (Deleted: 0)
Binary : 2 (Ratio: 50.00%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 4 (Average Length: 16.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 4 (Average: 5.00 Max: 16 Sum: 20)
Executed : 3 (Average: 4.75 Max: 16 Sum: 19 Ratio: 95.00%)
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 5.00%)
Rules : 64767
Atoms : 64767
Bodies : 1 (Original: 0)
Tight : Yes
Variables : 17354 (Eliminated: 0 Frozen: 170)
Constraints : 57355 (Binary: 95.3% Ternary: 3.3% Other: 1.4%)
Memory Peak : 247MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.02s
Memory: 187MB (+4MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time: 1.00s
Memory: 218MB (+31MB)
Solving...
[start: stats after solve call]
Models : 0
Calls : 3
Time : 1.696s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 1.516s
Choices : 212 (Domain: 37)
Conflicts : 13 (Analyzed: 12)
Restarts : 0
Model-Level : 183.0
Problems : 3 (Average Length: 5.33 Splits: 0)
Lemmas : 12 (Deleted: 0)
Binary : 4 (Ratio: 33.33%)
Ternary : 4 (Ratio: 33.33%)
Conflict : 12 (Average Length: 7.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 12 (Average: 3.25 Max: 16 Sum: 39)
Executed : 9 (Average: 3.00 Max: 16 Sum: 36 Ratio: 92.31%)
Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 7.69%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 21236 (Eliminated: 0 Frozen: 4444)
Constraints : 86170 (Binary: 92.4% Ternary: 5.4% Other: 2.2%)
Memory Peak : 247MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.02s
Memory: 218MB (+0MB)
UNSAT
Iteration Time: 1.46s
Iteration 3
Queue: [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 5
Expected Memory: 222.0MB
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
Grounding Time: 0.55s
Memory: 218MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 4
Time : 3.582s (Solving: 1.11s 1st Model: 0.00s Unsat: 1.11s)
CPU Time : 3.408s
Choices : 36338 (Domain: 29490)
Conflicts : 3123 (Analyzed: 3121)
Restarts : 36 (Average: 86.69 Last: 26)
Model-Level : 183.0
Problems : 4 (Average Length: 7.00 Splits: 0)
Lemmas : 3121 (Deleted: 570)
Binary : 325 (Ratio: 10.41%)
Ternary : 504 (Ratio: 16.15%)
Conflict : 3121 (Average Length: 42.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 3121 (Average: 11.58 Max: 265 Sum: 36155)
Executed : 3080 (Average: 11.44 Max: 265 Sum: 35707 Ratio: 98.76%)
Bounded : 41 (Average: 10.93 Max: 12 Sum: 448 Ratio: 1.24%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 61312 (Eliminated: 0 Frozen: 16894)
Constraints : 388150 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 247MB
Max. Length : 5 steps
Models : 1
[endof: stats after solve call]
Solving Time: 1.14s
Memory: 230MB (+12MB)
UNSAT
Iteration Time: 1.89s
Iteration 4
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 10
Expected Memory: 242.0MB
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
Grounding Time: 0.53s
Memory: 242MB (+12MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 5
Time : 8.918s (Solving: 5.65s 1st Model: 0.00s Unsat: 1.11s)
CPU Time : 8.748s
Choices : 115133 (Domain: 89050)
Conflicts : 12082 (Analyzed: 12080)
Restarts : 136 (Average: 88.82 Last: 101)
Model-Level : 183.0
Problems : 5 (Average Length: 9.00 Splits: 0)
Lemmas : 12080 (Deleted: 7160)
Binary : 775 (Ratio: 6.42%)
Ternary : 845 (Ratio: 7.00%)
Conflict : 12080 (Average Length: 130.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 12080 (Average: 9.19 Max: 265 Sum: 110997)
Executed : 12022 (Average: 9.13 Max: 265 Sum: 110262 Ratio: 99.34%)
Bounded : 58 (Average: 12.67 Max: 17 Sum: 735 Ratio: 0.66%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 101388 (Eliminated: 0 Frozen: 29344)
Constraints : 645808 (Binary: 91.4% Ternary: 6.7% Other: 1.9%)
Memory Peak : 262MB
Max. Length : 10 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.58s
Memory: 262MB (+20MB)
UNKNOWN
Iteration Time: 5.35s
Iteration 5
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 15
Expected Memory: 294.0MB
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
Grounding Time: 0.64s
Memory: 276MB (+14MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 6
Time : 14.138s (Solving: 9.94s 1st Model: 0.00s Unsat: 1.11s)
CPU Time : 13.968s
Choices : 157868 (Domain: 131138)
Conflicts : 19485 (Analyzed: 19483)
Restarts : 236 (Average: 82.56 Last: 101)
Model-Level : 183.0
Problems : 6 (Average Length: 11.17 Splits: 0)
Lemmas : 19483 (Deleted: 13053)
Binary : 1076 (Ratio: 5.52%)
Ternary : 912 (Ratio: 4.68%)
Conflict : 19483 (Average Length: 181.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 19483 (Average: 7.64 Max: 265 Sum: 148779)
Executed : 19423 (Average: 7.60 Max: 265 Sum: 148003 Ratio: 99.48%)
Bounded : 60 (Average: 12.93 Max: 22 Sum: 776 Ratio: 0.52%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 141464 (Eliminated: 0 Frozen: 41794)
Constraints : 941310 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
Memory Peak : 302MB
Max. Length : 15 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.33s
Memory: 302MB (+26MB)
UNKNOWN
Iteration Time: 5.23s
Iteration 6
Queue: [(5,25,0,True), (6,30,0,True)]
Grounded Until: 20
Expected Memory: 342.0MB
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
Grounding Time: 0.54s
Memory: 308MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 7
Time : 20.394s (Solving: 15.35s 1st Model: 0.00s Unsat: 1.11s)
CPU Time : 20.224s
Choices : 331212 (Domain: 285212)
Conflicts : 28062 (Analyzed: 28060)
Restarts : 336 (Average: 83.51 Last: 131)
Model-Level : 183.0
Problems : 7 (Average Length: 13.43 Splits: 0)
Lemmas : 28060 (Deleted: 18557)
Binary : 1903 (Ratio: 6.78%)
Ternary : 1288 (Ratio: 4.59%)
Conflict : 28060 (Average Length: 175.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 28060 (Average: 11.25 Max: 782 Sum: 315796)
Executed : 27986 (Average: 11.21 Max: 782 Sum: 314642 Ratio: 99.63%)
Bounded : 74 (Average: 15.59 Max: 27 Sum: 1154 Ratio: 0.37%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 181540 (Eliminated: 0 Frozen: 54244)
Constraints : 1240231 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
Memory Peak : 336MB
Max. Length : 20 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.47s
Memory: 322MB (+14MB)
UNKNOWN
Iteration Time: 6.27s
Iteration 7
Queue: [(6,30,0,True)]
Grounded Until: 25
Expected Memory: 362.0MB
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
Grounding Time: 0.58s
Memory: 334MB (+12MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 8
Time : 27.275s (Solving: 21.30s 1st Model: 0.00s Unsat: 1.11s)
CPU Time : 27.108s
Choices : 464738 (Domain: 402252)
Conflicts : 36744 (Analyzed: 36742)
Restarts : 436 (Average: 84.27 Last: 131)
Model-Level : 183.0
Problems : 8 (Average Length: 15.75 Splits: 0)
Lemmas : 36742 (Deleted: 27143)
Binary : 2231 (Ratio: 6.07%)
Ternary : 1421 (Ratio: 3.87%)
Conflict : 36742 (Average Length: 201.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 36742 (Average: 11.94 Max: 782 Sum: 438868)
Executed : 36653 (Average: 11.90 Max: 782 Sum: 437244 Ratio: 99.63%)
Bounded : 89 (Average: 18.25 Max: 32 Sum: 1624 Ratio: 0.37%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 221616 (Eliminated: 0 Frozen: 66694)
Constraints : 1520780 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
Memory Peak : 368MB
Max. Length : 25 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.02s
Memory: 368MB (+34MB)
UNKNOWN
Iteration Time: 6.89s
Iteration 8
Queue: [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 9
Time : 28.615s (Solving: 22.59s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 28.448s
Choices : 467550 (Domain: 405060)
Conflicts : 37906 (Analyzed: 37903)
Restarts : 450 (Average: 84.23 Last: 131)
Model-Level : 183.0
Problems : 9 (Average Length: 17.56 Splits: 0)
Lemmas : 37903 (Deleted: 27143)
Binary : 2261 (Ratio: 5.97%)
Ternary : 1439 (Ratio: 3.80%)
Conflict : 37903 (Average Length: 202.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 37903 (Average: 11.65 Max: 782 Sum: 441640)
Executed : 37813 (Average: 11.61 Max: 782 Sum: 440015 Ratio: 99.63%)
Bounded : 90 (Average: 18.06 Max: 32 Sum: 1625 Ratio: 0.37%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 221616 (Eliminated: 0 Frozen: 66694)
Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
Memory Peak : 368MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 1.32s
Memory: 368MB (+0MB)
UNSAT
Iteration Time: 1.34s
Iteration 9
Queue: [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 10
Time : 34.297s (Solving: 28.21s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 34.132s
Choices : 529904 (Domain: 452412)
Conflicts : 46631 (Analyzed: 46628)
Restarts : 550 (Average: 84.78 Last: 131)
Model-Level : 183.0
Problems : 10 (Average Length: 19.00 Splits: 0)
Lemmas : 46628 (Deleted: 36484)
Binary : 2472 (Ratio: 5.30%)
Ternary : 1508 (Ratio: 3.23%)
Conflict : 46628 (Average Length: 244.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 46628 (Average: 10.67 Max: 782 Sum: 497348)
Executed : 46537 (Average: 10.63 Max: 782 Sum: 495696 Ratio: 99.67%)
Bounded : 91 (Average: 18.15 Max: 32 Sum: 1652 Ratio: 0.33%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 221616 (Eliminated: 0 Frozen: 66694)
Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
Memory Peak : 368MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.66s
Memory: 368MB (+0MB)
UNKNOWN
Iteration Time: 5.69s
Iteration 10
Queue: [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 11
Time : 41.774s (Solving: 35.64s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 41.612s
Choices : 633897 (Domain: 541048)
Conflicts : 55908 (Analyzed: 55905)
Restarts : 650 (Average: 86.01 Last: 131)
Model-Level : 183.0
Problems : 11 (Average Length: 20.18 Splits: 0)
Lemmas : 55905 (Deleted: 42997)
Binary : 3035 (Ratio: 5.43%)
Ternary : 1728 (Ratio: 3.09%)
Conflict : 55905 (Average Length: 289.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 55905 (Average: 10.58 Max: 782 Sum: 591368)
Executed : 55806 (Average: 10.54 Max: 782 Sum: 589465 Ratio: 99.68%)
Bounded : 99 (Average: 19.22 Max: 32 Sum: 1903 Ratio: 0.32%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 221616 (Eliminated: 0 Frozen: 66694)
Constraints : 1503174 (Binary: 91.3% Ternary: 6.8% Other: 1.8%)
Memory Peak : 368MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.46s
Memory: 368MB (+0MB)
UNKNOWN
Iteration Time: 7.48s
Iteration 11
Queue: [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 12
Time : 49.815s (Solving: 43.63s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 49.656s
Choices : 743498 (Domain: 635142)
Conflicts : 65194 (Analyzed: 65191)
Restarts : 750 (Average: 86.92 Last: 131)
Model-Level : 183.0
Problems : 12 (Average Length: 21.17 Splits: 0)
Lemmas : 65191 (Deleted: 51200)
Binary : 3305 (Ratio: 5.07%)
Ternary : 1857 (Ratio: 2.85%)
Conflict : 65191 (Average Length: 330.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 65191 (Average: 10.52 Max: 782 Sum: 685498)
Executed : 65090 (Average: 10.49 Max: 782 Sum: 683531 Ratio: 99.71%)
Bounded : 101 (Average: 19.48 Max: 32 Sum: 1967 Ratio: 0.29%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 221616 (Eliminated: 0 Frozen: 66694)
Constraints : 1497569 (Binary: 91.3% Ternary: 6.8% Other: 1.9%)
Memory Peak : 368MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.03s
Memory: 368MB (+0MB)
UNKNOWN
Iteration Time: 8.05s
Iteration 12
Queue: [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 30
Expected Memory: 414.0MB
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time: 0.56s
Memory: 368MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 13
Time : 59.310s (Solving: 52.21s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 59.156s
Choices : 881351 (Domain: 756871)
Conflicts : 74031 (Analyzed: 74028)
Restarts : 850 (Average: 87.09 Last: 157)
Model-Level : 183.0
Problems : 13 (Average Length: 22.38 Splits: 0)
Lemmas : 74028 (Deleted: 59920)
Binary : 3488 (Ratio: 4.71%)
Ternary : 1914 (Ratio: 2.59%)
Conflict : 74028 (Average Length: 407.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 74028 (Average: 10.85 Max: 782 Sum: 803239)
Executed : 73919 (Average: 10.82 Max: 782 Sum: 800976 Ratio: 99.72%)
Bounded : 109 (Average: 20.76 Max: 37 Sum: 2263 Ratio: 0.28%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 261692 (Eliminated: 0 Frozen: 79144)
Constraints : 1799341 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
Memory Peak : 405MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.65s
Memory: 381MB (+13MB)
UNKNOWN
Iteration Time: 9.51s
Iteration 13
Queue: [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 35
Expected Memory: 427.0MB
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time: 0.57s
Memory: 392MB (+11MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 14
Time : 68.733s (Solving: 60.68s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 68.584s
Choices : 1039739 (Domain: 899452)
Conflicts : 82621 (Analyzed: 82618)
Restarts : 950 (Average: 86.97 Last: 157)
Model-Level : 183.0
Problems : 14 (Average Length: 23.79 Splits: 0)
Lemmas : 82618 (Deleted: 66758)
Binary : 3639 (Ratio: 4.40%)
Ternary : 1978 (Ratio: 2.39%)
Conflict : 82618 (Average Length: 425.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 82618 (Average: 11.38 Max: 782 Sum: 940232)
Executed : 82507 (Average: 11.35 Max: 782 Sum: 937886 Ratio: 99.75%)
Bounded : 111 (Average: 21.14 Max: 42 Sum: 2346 Ratio: 0.25%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 301768 (Eliminated: 0 Frozen: 91594)
Constraints : 2101210 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
Memory Peak : 436MB
Max. Length : 35 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.55s
Memory: 407MB (+15MB)
UNKNOWN
Iteration Time: 9.44s
Iteration 14
Queue: [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 40
Expected Memory: 453.0MB
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time: 0.72s
Memory: 431MB (+24MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 15
Time : 79.407s (Solving: 70.22s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 79.264s
Choices : 1223417 (Domain: 1070592)
Conflicts : 91188 (Analyzed: 91185)
Restarts : 1050 (Average: 86.84 Last: 157)
Model-Level : 183.0
Problems : 15 (Average Length: 25.33 Splits: 0)
Lemmas : 91185 (Deleted: 74522)
Binary : 3852 (Ratio: 4.22%)
Ternary : 2045 (Ratio: 2.24%)
Conflict : 91185 (Average Length: 444.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 91185 (Average: 12.09 Max: 794 Sum: 1102182)
Executed : 91068 (Average: 12.06 Max: 794 Sum: 1099554 Ratio: 99.76%)
Bounded : 117 (Average: 22.46 Max: 47 Sum: 2628 Ratio: 0.24%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 341844 (Eliminated: 0 Frozen: 104044)
Constraints : 2403164 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
Memory Peak : 482MB
Max. Length : 40 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.63s
Memory: 481MB (+50MB)
UNKNOWN
Iteration Time: 10.69s
Iteration 15
Queue: [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 45
Expected Memory: 555.0MB
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time: 0.60s
Memory: 481MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 16
Time : 90.472s (Solving: 80.24s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 90.336s
Choices : 1429024 (Domain: 1264883)
Conflicts : 100027 (Analyzed: 100024)
Restarts : 1150 (Average: 86.98 Last: 157)
Model-Level : 183.0
Problems : 16 (Average Length: 27.00 Splits: 0)
Lemmas : 100024 (Deleted: 84018)
Binary : 3987 (Ratio: 3.99%)
Ternary : 2087 (Ratio: 2.09%)
Conflict : 100024 (Average Length: 472.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 100024 (Average: 12.81 Max: 794 Sum: 1281367)
Executed : 99905 (Average: 12.78 Max: 794 Sum: 1278640 Ratio: 99.79%)
Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.21%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 381920 (Eliminated: 0 Frozen: 116494)
Constraints : 2702017 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
Memory Peak : 527MB
Max. Length : 45 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.12s
Memory: 490MB (+9MB)
UNKNOWN
Iteration Time: 11.08s
Iteration 16
Queue: [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 50
Expected Memory: 564.0MB
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time: 0.57s
Memory: 493MB (+3MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 17
Time : 100.209s (Solving: 88.95s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 100.076s
Choices : 1577246 (Domain: 1405775)
Conflicts : 108978 (Analyzed: 108975)
Restarts : 1250 (Average: 87.18 Last: 157)
Model-Level : 183.0
Problems : 17 (Average Length: 28.76 Splits: 0)
Lemmas : 108975 (Deleted: 93155)
Binary : 4109 (Ratio: 3.77%)
Ternary : 2118 (Ratio: 1.94%)
Conflict : 108975 (Average Length: 513.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 108975 (Average: 12.71 Max: 794 Sum: 1384883)
Executed : 108856 (Average: 12.68 Max: 794 Sum: 1382156 Ratio: 99.80%)
Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.20%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 421996 (Eliminated: 0 Frozen: 128944)
Constraints : 3003983 (Binary: 91.3% Ternary: 6.9% Other: 1.8%)
Memory Peak : 552MB
Max. Length : 50 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.80s
Memory: 513MB (+20MB)
UNKNOWN
Iteration Time: 9.75s
Iteration 17
Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 55
Expected Memory: 587.0MB
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
Grounding Time: 0.56s
Memory: 518MB (+5MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 18
Time : 110.217s (Solving: 97.92s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 110.088s
Choices : 1776257 (Domain: 1595430)
Conflicts : 117090 (Analyzed: 117087)
Restarts : 1350 (Average: 86.73 Last: 157)
Model-Level : 183.0
Problems : 18 (Average Length: 30.61 Splits: 0)
Lemmas : 117087 (Deleted: 99028)
Binary : 4216 (Ratio: 3.60%)
Ternary : 2159 (Ratio: 1.84%)
Conflict : 117087 (Average Length: 523.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 117087 (Average: 13.30 Max: 910 Sum: 1557696)
Executed : 116968 (Average: 13.28 Max: 910 Sum: 1554969 Ratio: 99.82%)
Bounded : 119 (Average: 22.92 Max: 52 Sum: 2727 Ratio: 0.18%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 462072 (Eliminated: 0 Frozen: 141394)
Constraints : 3305963 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
Memory Peak : 586MB
Max. Length : 55 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.07s
Memory: 542MB (+24MB)
UNKNOWN
Iteration Time: 10.02s
Iteration 18
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 60
Expected Memory: 616.0MB
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
Grounding Time: 0.56s
Memory: 549MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 19
Time : 120.307s (Solving: 106.94s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 120.184s
Choices : 1952515 (Domain: 1767971)
Conflicts : 125373 (Analyzed: 125370)
Restarts : 1450 (Average: 86.46 Last: 157)
Model-Level : 183.0
Problems : 19 (Average Length: 32.53 Splits: 0)
Lemmas : 125370 (Deleted: 107415)
Binary : 4297 (Ratio: 3.43%)
Ternary : 2186 (Ratio: 1.74%)
Conflict : 125370 (Average Length: 544.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 125370 (Average: 13.53 Max: 910 Sum: 1696732)
Executed : 125248 (Average: 13.51 Max: 910 Sum: 1693804 Ratio: 99.83%)
Bounded : 122 (Average: 24.00 Max: 67 Sum: 2928 Ratio: 0.17%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 502148 (Eliminated: 0 Frozen: 153844)
Constraints : 3607943 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
Memory Peak : 618MB
Max. Length : 60 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.13s
Memory: 610MB (+61MB)
UNKNOWN
Iteration Time: 10.11s
Iteration 19
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until: 65
Expected Memory: 684.0MB
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
Grounding Time: 0.56s
Memory: 610MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 20
Time : 130.946s (Solving: 116.50s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 130.828s
Choices : 2197548 (Domain: 2008753)
Conflicts : 133633 (Analyzed: 133630)
Restarts : 1550 (Average: 86.21 Last: 157)
Model-Level : 183.0
Problems : 20 (Average Length: 34.50 Splits: 0)
Lemmas : 133630 (Deleted: 114772)
Binary : 4403 (Ratio: 3.29%)
Ternary : 2221 (Ratio: 1.66%)
Conflict : 133630 (Average Length: 539.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 133630 (Average: 14.40 Max: 910 Sum: 1924414)
Executed : 133505 (Average: 14.38 Max: 910 Sum: 1921270 Ratio: 99.84%)
Bounded : 125 (Average: 25.15 Max: 72 Sum: 3144 Ratio: 0.16%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 542224 (Eliminated: 0 Frozen: 166294)
Constraints : 3909881 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
Memory Peak : 676MB
Max. Length : 65 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.67s
Memory: 615MB (+5MB)
UNKNOWN
Iteration Time: 10.66s
Iteration 20
Queue: [(15,75,0,True), (16,80,0,True)]
Grounded Until: 70
Expected Memory: 689.0MB
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
Grounding Time: 0.57s
Memory: 616MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 21
Time : 143.234s (Solving: 127.68s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 143.120s
Choices : 2401935 (Domain: 2211433)
Conflicts : 141844 (Analyzed: 141841)
Restarts : 1650 (Average: 85.96 Last: 157)
Model-Level : 183.0
Problems : 21 (Average Length: 36.52 Splits: 0)
Lemmas : 141841 (Deleted: 122531)
Binary : 4527 (Ratio: 3.19%)
Ternary : 2257 (Ratio: 1.59%)
Conflict : 141841 (Average Length: 531.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 141841 (Average: 14.90 Max: 910 Sum: 2113516)
Executed : 141713 (Average: 14.88 Max: 910 Sum: 2110141 Ratio: 99.84%)
Bounded : 128 (Average: 26.37 Max: 77 Sum: 3375 Ratio: 0.16%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 582300 (Eliminated: 0 Frozen: 178744)
Constraints : 4211821 (Binary: 91.2% Ternary: 6.9% Other: 1.8%)
Memory Peak : 698MB
Max. Length : 70 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.29s
Memory: 643MB (+27MB)
UNKNOWN
Iteration Time: 12.30s
Iteration 21
Queue: [(16,80,0,True)]
Grounded Until: 75
Expected Memory: 717.0MB
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
Grounding Time: 0.57s
Memory: 643MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 22
Time : 153.637s (Solving: 136.96s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 153.528s
Choices : 2605196 (Domain: 2410332)
Conflicts : 150017 (Analyzed: 150014)
Restarts : 1750 (Average: 85.72 Last: 157)
Model-Level : 183.0
Problems : 22 (Average Length: 38.59 Splits: 0)
Lemmas : 150014 (Deleted: 130452)
Binary : 4621 (Ratio: 3.08%)
Ternary : 2282 (Ratio: 1.52%)
Conflict : 150014 (Average Length: 525.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 150014 (Average: 15.26 Max: 1010 Sum: 2289293)
Executed : 149883 (Average: 15.24 Max: 1010 Sum: 2285672 Ratio: 99.84%)
Bounded : 131 (Average: 27.64 Max: 82 Sum: 3621 Ratio: 0.16%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513760 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 75 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.41s
Memory: 668MB (+25MB)
UNKNOWN
Iteration Time: 10.42s
Iteration 22
Queue: [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 23
Time : 162.246s (Solving: 145.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 162.144s
Choices : 2670865 (Domain: 2470369)
Conflicts : 158594 (Analyzed: 158591)
Restarts : 1850 (Average: 85.72 Last: 157)
Model-Level : 183.0
Problems : 23 (Average Length: 40.48 Splits: 0)
Lemmas : 158591 (Deleted: 138588)
Binary : 4772 (Ratio: 3.01%)
Ternary : 2342 (Ratio: 1.48%)
Conflict : 158591 (Average Length: 525.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 158591 (Average: 14.81 Max: 1010 Sum: 2348653)
Executed : 158458 (Average: 14.79 Max: 1010 Sum: 2344949 Ratio: 99.84%)
Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.16%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513718 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.56s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 8.62s
Iteration 23
Queue: [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 24
Time : 169.973s (Solving: 153.03s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 169.876s
Choices : 2743021 (Domain: 2537527)
Conflicts : 167336 (Analyzed: 167333)
Restarts : 1950 (Average: 85.81 Last: 157)
Model-Level : 183.0
Problems : 24 (Average Length: 42.21 Splits: 0)
Lemmas : 167333 (Deleted: 148243)
Binary : 4901 (Ratio: 2.93%)
Ternary : 2416 (Ratio: 1.44%)
Conflict : 167333 (Average Length: 533.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 167333 (Average: 14.39 Max: 1010 Sum: 2407912)
Executed : 167200 (Average: 14.37 Max: 1010 Sum: 2404208 Ratio: 99.85%)
Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.15%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.69s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 7.73s
Iteration 24
Queue: [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 25
Time : 176.838s (Solving: 159.75s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 176.748s
Choices : 2793194 (Domain: 2586360)
Conflicts : 175654 (Analyzed: 175651)
Restarts : 2050 (Average: 85.68 Last: 157)
Model-Level : 183.0
Problems : 25 (Average Length: 43.80 Splits: 0)
Lemmas : 175651 (Deleted: 154469)
Binary : 4994 (Ratio: 2.84%)
Ternary : 2449 (Ratio: 1.39%)
Conflict : 175651 (Average Length: 523.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 175651 (Average: 13.95 Max: 1010 Sum: 2449845)
Executed : 175518 (Average: 13.93 Max: 1010 Sum: 2446141 Ratio: 99.85%)
Bounded : 133 (Average: 27.85 Max: 82 Sum: 3704 Ratio: 0.15%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.82s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 6.87s
Iteration 25
Queue: [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 26
Time : 184.556s (Solving: 167.33s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 184.468s
Choices : 2881735 (Domain: 2673125)
Conflicts : 183975 (Analyzed: 183972)
Restarts : 2150 (Average: 85.57 Last: 157)
Model-Level : 183.0
Problems : 26 (Average Length: 45.27 Splits: 0)
Lemmas : 183972 (Deleted: 162565)
Binary : 5040 (Ratio: 2.74%)
Ternary : 2464 (Ratio: 1.34%)
Conflict : 183972 (Average Length: 518.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 183972 (Average: 13.72 Max: 1010 Sum: 2524861)
Executed : 183837 (Average: 13.70 Max: 1010 Sum: 2520998 Ratio: 99.85%)
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.15%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513705 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.67s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 7.72s
Iteration 26
Queue: [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 27
Time : 192.272s (Solving: 174.90s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 192.188s
Choices : 2993870 (Domain: 2779772)
Conflicts : 192077 (Analyzed: 192074)
Restarts : 2250 (Average: 85.37 Last: 157)
Model-Level : 183.0
Problems : 27 (Average Length: 46.63 Splits: 0)
Lemmas : 192074 (Deleted: 170725)
Binary : 5110 (Ratio: 2.66%)
Ternary : 2477 (Ratio: 1.29%)
Conflict : 192074 (Average Length: 519.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 192074 (Average: 13.64 Max: 1010 Sum: 2620085)
Executed : 191939 (Average: 13.62 Max: 1010 Sum: 2616222 Ratio: 99.85%)
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.15%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.66s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 7.72s
Iteration 27
Queue: [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 28
Time : 204.351s (Solving: 186.86s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 204.272s
Choices : 3317666 (Domain: 3078914)
Conflicts : 201174 (Analyzed: 201171)
Restarts : 2350 (Average: 85.60 Last: 157)
Model-Level : 183.0
Problems : 28 (Average Length: 47.89 Splits: 0)
Lemmas : 201171 (Deleted: 180087)
Binary : 5501 (Ratio: 2.73%)
Ternary : 2562 (Ratio: 1.27%)
Conflict : 201171 (Average Length: 536.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 201171 (Average: 14.49 Max: 1010 Sum: 2915539)
Executed : 201036 (Average: 14.47 Max: 1010 Sum: 2911676 Ratio: 99.87%)
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.13%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 12.04s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 12.09s
Iteration 28
Queue: [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 29
Time : 211.665s (Solving: 194.04s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 211.588s
Choices : 3439190 (Domain: 3199143)
Conflicts : 208925 (Analyzed: 208922)
Restarts : 2450 (Average: 85.27 Last: 157)
Model-Level : 183.0
Problems : 29 (Average Length: 49.07 Splits: 0)
Lemmas : 208922 (Deleted: 186770)
Binary : 5579 (Ratio: 2.67%)
Ternary : 2572 (Ratio: 1.23%)
Conflict : 208922 (Average Length: 528.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 208922 (Average: 14.47 Max: 1010 Sum: 3023317)
Executed : 208787 (Average: 14.45 Max: 1010 Sum: 3019454 Ratio: 99.87%)
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.13%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.27s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 7.32s
Iteration 29
Queue: [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 30
Time : 217.857s (Solving: 200.09s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 217.784s
Choices : 3520051 (Domain: 3279560)
Conflicts : 216107 (Analyzed: 216104)
Restarts : 2550 (Average: 84.75 Last: 157)
Model-Level : 183.0
Problems : 30 (Average Length: 50.17 Splits: 0)
Lemmas : 216104 (Deleted: 194246)
Binary : 5641 (Ratio: 2.61%)
Ternary : 2593 (Ratio: 1.20%)
Conflict : 216104 (Average Length: 523.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 216104 (Average: 14.31 Max: 1010 Sum: 3091425)
Executed : 215969 (Average: 14.29 Max: 1010 Sum: 3087562 Ratio: 99.88%)
Bounded : 135 (Average: 28.61 Max: 82 Sum: 3863 Ratio: 0.12%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.14s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 6.20s
Iteration 30
Queue: [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 31
Time : 224.621s (Solving: 206.70s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 224.548s
Choices : 3585219 (Domain: 3344599)
Conflicts : 224007 (Analyzed: 224004)
Restarts : 2650 (Average: 84.53 Last: 157)
Model-Level : 183.0
Problems : 31 (Average Length: 51.19 Splits: 0)
Lemmas : 224004 (Deleted: 201238)
Binary : 5663 (Ratio: 2.53%)
Ternary : 2601 (Ratio: 1.16%)
Conflict : 224004 (Average Length: 515.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 224004 (Average: 14.05 Max: 1010 Sum: 3146534)
Executed : 223868 (Average: 14.03 Max: 1010 Sum: 3142594 Ratio: 99.87%)
Bounded : 136 (Average: 28.97 Max: 82 Sum: 3940 Ratio: 0.13%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.71s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 6.77s
Iteration 31
Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 32
Time : 233.395s (Solving: 215.32s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 233.328s
Choices : 3731353 (Domain: 3489030)
Conflicts : 232313 (Analyzed: 232310)
Restarts : 2750 (Average: 84.48 Last: 157)
Model-Level : 183.0
Problems : 32 (Average Length: 52.16 Splits: 0)
Lemmas : 232310 (Deleted: 208952)
Binary : 5741 (Ratio: 2.47%)
Ternary : 2619 (Ratio: 1.13%)
Conflict : 232310 (Average Length: 509.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 232310 (Average: 14.11 Max: 1010 Sum: 3277720)
Executed : 232173 (Average: 14.09 Max: 1010 Sum: 3273698 Ratio: 99.88%)
Bounded : 137 (Average: 29.36 Max: 82 Sum: 4022 Ratio: 0.12%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513691 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.72s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 8.78s
Iteration 32
Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 33
Time : 243.720s (Solving: 225.52s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 243.660s
Choices : 3939332 (Domain: 3695182)
Conflicts : 240640 (Analyzed: 240637)
Restarts : 2850 (Average: 84.43 Last: 157)
Model-Level : 183.0
Problems : 33 (Average Length: 53.06 Splits: 0)
Lemmas : 240637 (Deleted: 216962)
Binary : 5848 (Ratio: 2.43%)
Ternary : 2635 (Ratio: 1.10%)
Conflict : 240637 (Average Length: 505.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 240637 (Average: 14.41 Max: 1010 Sum: 3468650)
Executed : 240499 (Average: 14.40 Max: 1010 Sum: 3464546 Ratio: 99.88%)
Bounded : 138 (Average: 29.74 Max: 82 Sum: 4104 Ratio: 0.12%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513693 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.29s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 10.33s
Iteration 33
Queue: [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 34
Time : 252.404s (Solving: 234.05s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 252.348s
Choices : 4104662 (Domain: 3859160)
Conflicts : 248722 (Analyzed: 248719)
Restarts : 2950 (Average: 84.31 Last: 157)
Model-Level : 183.0
Problems : 34 (Average Length: 53.91 Splits: 0)
Lemmas : 248719 (Deleted: 224964)
Binary : 5921 (Ratio: 2.38%)
Ternary : 2653 (Ratio: 1.07%)
Conflict : 248719 (Average Length: 500.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 248719 (Average: 14.54 Max: 1044 Sum: 3617011)
Executed : 248579 (Average: 14.53 Max: 1044 Sum: 3612747 Ratio: 99.88%)
Bounded : 140 (Average: 30.46 Max: 82 Sum: 4264 Ratio: 0.12%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513679 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.63s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 8.69s
Iteration 34
Queue: [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 35
Time : 260.213s (Solving: 241.73s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 260.160s
Choices : 4269250 (Domain: 4022750)
Conflicts : 256518 (Analyzed: 256515)
Restarts : 3050 (Average: 84.10 Last: 157)
Model-Level : 183.0
Problems : 35 (Average Length: 54.71 Splits: 0)
Lemmas : 256515 (Deleted: 232812)
Binary : 5995 (Ratio: 2.34%)
Ternary : 2672 (Ratio: 1.04%)
Conflict : 256515 (Average Length: 496.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 256515 (Average: 14.68 Max: 1044 Sum: 3765684)
Executed : 256374 (Average: 14.66 Max: 1044 Sum: 3761338 Ratio: 99.88%)
Bounded : 141 (Average: 30.82 Max: 82 Sum: 4346 Ratio: 0.12%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 622376 (Eliminated: 0 Frozen: 191194)
Constraints : 4513665 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 727MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.77s
Memory: 668MB (+0MB)
UNKNOWN
Iteration Time: 7.82s
Iteration 35
Queue: [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 80
Expected Memory: 742.0MB
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
Grounding Time: 0.60s
Memory: 668MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 36
Time : 267.786s (Solving: 248.11s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 267.736s
Choices : 4348686 (Domain: 4101788)
Conflicts : 264283 (Analyzed: 264280)
Restarts : 3150 (Average: 83.90 Last: 157)
Model-Level : 183.0
Problems : 36 (Average Length: 55.61 Splits: 0)
Lemmas : 264280 (Deleted: 240259)
Binary : 6036 (Ratio: 2.28%)
Ternary : 2685 (Ratio: 1.02%)
Conflict : 264280 (Average Length: 490.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 264280 (Average: 14.49 Max: 1044 Sum: 3830386)
Executed : 264137 (Average: 14.48 Max: 1044 Sum: 3825871 Ratio: 99.88%)
Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.12%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 662452 (Eliminated: 0 Frozen: 203644)
Constraints : 4815631 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 755MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.51s
Memory: 691MB (+23MB)
UNKNOWN
Iteration Time: 7.59s
Iteration 36
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Expected Memory: 765.0MB
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
Grounding Time: 0.59s
Memory: 691MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 37
Time : 280.324s (Solving: 259.44s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 280.280s
Choices : 4806070 (Domain: 4550562)
Conflicts : 272656 (Analyzed: 272653)
Restarts : 3250 (Average: 83.89 Last: 157)
Model-Level : 183.0
Problems : 37 (Average Length: 56.59 Splits: 0)
Lemmas : 272653 (Deleted: 247693)
Binary : 6270 (Ratio: 2.30%)
Ternary : 2729 (Ratio: 1.00%)
Conflict : 272653 (Average Length: 500.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 272653 (Average: 15.62 Max: 1044 Sum: 4257604)
Executed : 272510 (Average: 15.60 Max: 1044 Sum: 4253089 Ratio: 99.89%)
Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.11%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 702528 (Eliminated: 0 Frozen: 216094)
Constraints : 5114549 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 790MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.47s
Memory: 763MB (+72MB)
UNKNOWN
Iteration Time: 12.56s
Iteration 37
Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 90
Expected Memory: 837.0MB
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
Grounding Time: 0.95s
Memory: 813MB (+50MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 38
Time : 296.936s (Solving: 274.46s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 296.896s
Choices : 5382955 (Domain: 5117111)
Conflicts : 281712 (Analyzed: 281709)
Restarts : 3350 (Average: 84.09 Last: 157)
Model-Level : 183.0
Problems : 38 (Average Length: 57.66 Splits: 0)
Lemmas : 281709 (Deleted: 257600)
Binary : 6538 (Ratio: 2.32%)
Ternary : 2790 (Ratio: 0.99%)
Conflict : 281709 (Average Length: 525.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 281709 (Average: 17.02 Max: 1044 Sum: 4793424)
Executed : 281566 (Average: 17.00 Max: 1044 Sum: 4788909 Ratio: 99.91%)
Bounded : 143 (Average: 31.57 Max: 87 Sum: 4515 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 742604 (Eliminated: 0 Frozen: 228544)
Constraints : 5416529 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 946MB
Max. Length : 90 steps
Models : 1
[endof: stats after solve call]
Solving Time: 15.16s
Memory: 882MB (+69MB)
UNKNOWN
Iteration Time: 16.63s
Iteration 38
Queue: [(20,100,0,True), (21,105,0,True)]
Grounded Until: 95
Expected Memory: 1001.0MB
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
Grounding Time: 0.56s
Memory: 882MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 39
Time : 305.801s (Solving: 282.12s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 305.764s
Choices : 5562451 (Domain: 5295760)
Conflicts : 289712 (Analyzed: 289709)
Restarts : 3450 (Average: 83.97 Last: 157)
Model-Level : 183.0
Problems : 39 (Average Length: 58.79 Splits: 0)
Lemmas : 289709 (Deleted: 264065)
Binary : 6653 (Ratio: 2.30%)
Ternary : 2806 (Ratio: 0.97%)
Conflict : 289709 (Average Length: 519.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 289709 (Average: 17.11 Max: 1273 Sum: 4955544)
Executed : 289565 (Average: 17.09 Max: 1273 Sum: 4950927 Ratio: 99.91%)
Bounded : 144 (Average: 32.06 Max: 102 Sum: 4617 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 782680 (Eliminated: 0 Frozen: 240994)
Constraints : 5718509 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 977MB
Max. Length : 95 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.81s
Memory: 888MB (+6MB)
UNKNOWN
Iteration Time: 8.88s
Iteration 39
Queue: [(21,105,0,True)]
Grounded Until: 100
Expected Memory: 1007.0MB
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
Grounding Time: 0.55s
Memory: 889MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 40
Time : 314.321s (Solving: 289.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 314.288s
Choices : 5768001 (Domain: 5500320)
Conflicts : 297542 (Analyzed: 297539)
Restarts : 3550 (Average: 83.81 Last: 157)
Model-Level : 183.0
Problems : 40 (Average Length: 60.00 Splits: 0)
Lemmas : 297539 (Deleted: 271686)
Binary : 6728 (Ratio: 2.26%)
Ternary : 2824 (Ratio: 0.95%)
Conflict : 297539 (Average Length: 515.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 297539 (Average: 17.28 Max: 1374 Sum: 5142263)
Executed : 297394 (Average: 17.27 Max: 1374 Sum: 5137542 Ratio: 99.91%)
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 100 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.46s
Memory: 914MB (+25MB)
UNKNOWN
Iteration Time: 8.54s
Iteration 40
Queue: [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 41
Time : 321.643s (Solving: 296.58s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 321.616s
Choices : 5826604 (Domain: 5558923)
Conflicts : 305230 (Analyzed: 305227)
Restarts : 3650 (Average: 83.62 Last: 157)
Model-Level : 183.0
Problems : 41 (Average Length: 61.15 Splits: 0)
Lemmas : 305227 (Deleted: 279254)
Binary : 6823 (Ratio: 2.24%)
Ternary : 2826 (Ratio: 0.93%)
Conflict : 305227 (Average Length: 512.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 305227 (Average: 17.02 Max: 1374 Sum: 5195791)
Executed : 305082 (Average: 17.01 Max: 1374 Sum: 5191070 Ratio: 99.91%)
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.27s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 7.33s
Iteration 41
Queue: [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 42
Time : 330.430s (Solving: 305.20s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 330.408s
Choices : 5896868 (Domain: 5623680)
Conflicts : 313655 (Analyzed: 313652)
Restarts : 3750 (Average: 83.64 Last: 157)
Model-Level : 183.0
Problems : 42 (Average Length: 62.24 Splits: 0)
Lemmas : 313652 (Deleted: 286601)
Binary : 6949 (Ratio: 2.22%)
Ternary : 2855 (Ratio: 0.91%)
Conflict : 313652 (Average Length: 518.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 313652 (Average: 16.75 Max: 1374 Sum: 5252391)
Executed : 313507 (Average: 16.73 Max: 1374 Sum: 5247670 Ratio: 99.91%)
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.73s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 8.79s
Iteration 42
Queue: [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 43
Time : 335.159s (Solving: 309.74s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 335.140s
Choices : 5947391 (Domain: 5673356)
Conflicts : 321491 (Analyzed: 321488)
Restarts : 3850 (Average: 83.50 Last: 157)
Model-Level : 183.0
Problems : 43 (Average Length: 63.28 Splits: 0)
Lemmas : 321488 (Deleted: 294702)
Binary : 6992 (Ratio: 2.17%)
Ternary : 2866 (Ratio: 0.89%)
Conflict : 321488 (Average Length: 514.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 321488 (Average: 16.47 Max: 1374 Sum: 5294129)
Executed : 321343 (Average: 16.45 Max: 1374 Sum: 5289408 Ratio: 99.91%)
Bounded : 145 (Average: 32.56 Max: 104 Sum: 4721 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.66s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 4.74s
Iteration 43
Queue: [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 44
Time : 342.312s (Solving: 316.69s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 342.296s
Choices : 6036512 (Domain: 5760556)
Conflicts : 329836 (Analyzed: 329833)
Restarts : 3950 (Average: 83.50 Last: 185)
Model-Level : 183.0
Problems : 44 (Average Length: 64.27 Splits: 0)
Lemmas : 329833 (Deleted: 302258)
Binary : 7076 (Ratio: 2.15%)
Ternary : 2884 (Ratio: 0.87%)
Conflict : 329833 (Average Length: 510.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 329833 (Average: 16.29 Max: 1374 Sum: 5372439)
Executed : 329685 (Average: 16.27 Max: 1374 Sum: 5367404 Ratio: 99.91%)
Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020476 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.08s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 7.16s
Iteration 44
Queue: [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 45
Time : 350.390s (Solving: 324.61s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 350.380s
Choices : 6168437 (Domain: 5888804)
Conflicts : 338780 (Analyzed: 338777)
Restarts : 4050 (Average: 83.65 Last: 185)
Model-Level : 183.0
Problems : 45 (Average Length: 65.22 Splits: 0)
Lemmas : 338777 (Deleted: 312440)
Binary : 7165 (Ratio: 2.11%)
Ternary : 2895 (Ratio: 0.85%)
Conflict : 338777 (Average Length: 510.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 338777 (Average: 16.20 Max: 1374 Sum: 5488988)
Executed : 338629 (Average: 16.19 Max: 1374 Sum: 5483953 Ratio: 99.91%)
Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.03s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 8.09s
Iteration 45
Queue: [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 46
Time : 357.056s (Solving: 331.11s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 357.048s
Choices : 6280639 (Domain: 5999286)
Conflicts : 346955 (Analyzed: 346952)
Restarts : 4150 (Average: 83.60 Last: 185)
Model-Level : 183.0
Problems : 46 (Average Length: 66.13 Splits: 0)
Lemmas : 346952 (Deleted: 318946)
Binary : 7213 (Ratio: 2.08%)
Ternary : 2904 (Ratio: 0.84%)
Conflict : 346952 (Average Length: 509.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 346952 (Average: 16.10 Max: 1374 Sum: 5586987)
Executed : 346804 (Average: 16.09 Max: 1374 Sum: 5581952 Ratio: 99.91%)
Bounded : 148 (Average: 34.02 Max: 107 Sum: 5035 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.61s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 6.67s
Iteration 46
Queue: [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 47
Time : 364.389s (Solving: 338.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 364.384s
Choices : 6439253 (Domain: 6155618)
Conflicts : 355230 (Analyzed: 355227)
Restarts : 4250 (Average: 83.58 Last: 185)
Model-Level : 183.0
Problems : 47 (Average Length: 67.00 Splits: 0)
Lemmas : 355227 (Deleted: 326815)
Binary : 7410 (Ratio: 2.09%)
Ternary : 3010 (Ratio: 0.85%)
Conflict : 355227 (Average Length: 506.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 355227 (Average: 16.13 Max: 1374 Sum: 5731234)
Executed : 355078 (Average: 16.12 Max: 1374 Sum: 5726095 Ratio: 99.91%)
Bounded : 149 (Average: 34.49 Max: 107 Sum: 5139 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.28s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 7.34s
Iteration 47
Queue: [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 48
Time : 372.105s (Solving: 345.82s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 372.104s
Choices : 6631973 (Domain: 6346310)
Conflicts : 363365 (Analyzed: 363362)
Restarts : 4350 (Average: 83.53 Last: 185)
Model-Level : 183.0
Problems : 48 (Average Length: 67.83 Splits: 0)
Lemmas : 363362 (Deleted: 334432)
Binary : 7577 (Ratio: 2.09%)
Ternary : 3087 (Ratio: 0.85%)
Conflict : 363362 (Average Length: 504.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 363362 (Average: 16.26 Max: 1374 Sum: 5907978)
Executed : 363212 (Average: 16.24 Max: 1374 Sum: 5902732 Ratio: 99.91%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020462 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.65s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 7.72s
Iteration 48
Queue: [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 49
Time : 379.766s (Solving: 353.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 379.768s
Choices : 6831592 (Domain: 6541482)
Conflicts : 371683 (Analyzed: 371680)
Restarts : 4450 (Average: 83.52 Last: 185)
Model-Level : 183.0
Problems : 49 (Average Length: 68.63 Splits: 0)
Lemmas : 371680 (Deleted: 342205)
Binary : 7672 (Ratio: 2.06%)
Ternary : 3104 (Ratio: 0.84%)
Conflict : 371680 (Average Length: 503.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 371680 (Average: 16.37 Max: 1374 Sum: 6084055)
Executed : 371530 (Average: 16.35 Max: 1374 Sum: 6078809 Ratio: 99.91%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.09%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.59s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 7.67s
Iteration 49
Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 50
Time : 389.333s (Solving: 362.66s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 389.340s
Choices : 7114481 (Domain: 6821255)
Conflicts : 380450 (Analyzed: 380447)
Restarts : 4550 (Average: 83.61 Last: 185)
Model-Level : 183.0
Problems : 50 (Average Length: 69.40 Splits: 0)
Lemmas : 380447 (Deleted: 352305)
Binary : 7803 (Ratio: 2.05%)
Ternary : 3142 (Ratio: 0.83%)
Conflict : 380447 (Average Length: 502.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 380447 (Average: 16.68 Max: 1374 Sum: 6346973)
Executed : 380297 (Average: 16.67 Max: 1374 Sum: 6341727 Ratio: 99.92%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.08%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.49s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 9.57s
Iteration 50
Queue: [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 51
Time : 399.271s (Solving: 372.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 399.276s
Choices : 7405815 (Domain: 7110612)
Conflicts : 388712 (Analyzed: 388709)
Restarts : 4650 (Average: 83.59 Last: 185)
Model-Level : 183.0
Problems : 51 (Average Length: 70.14 Splits: 0)
Lemmas : 388709 (Deleted: 358623)
Binary : 7858 (Ratio: 2.02%)
Ternary : 3160 (Ratio: 0.81%)
Conflict : 388709 (Average Length: 504.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 388709 (Average: 17.02 Max: 1374 Sum: 6614005)
Executed : 388559 (Average: 17.00 Max: 1374 Sum: 6608759 Ratio: 99.92%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.08%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.88s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 9.94s
Iteration 51
Queue: [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 52
Time : 412.928s (Solving: 385.89s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 412.936s
Choices : 7920513 (Domain: 7620183)
Conflicts : 397908 (Analyzed: 397905)
Restarts : 4750 (Average: 83.77 Last: 185)
Model-Level : 183.0
Problems : 52 (Average Length: 70.85 Splits: 0)
Lemmas : 397905 (Deleted: 368777)
Binary : 8035 (Ratio: 2.02%)
Ternary : 3185 (Ratio: 0.80%)
Conflict : 397905 (Average Length: 510.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 397905 (Average: 17.84 Max: 1374 Sum: 7097953)
Executed : 397755 (Average: 17.83 Max: 1374 Sum: 7092707 Ratio: 99.93%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 13.58s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 13.67s
Iteration 52
Queue: [(19,95,1,True), (20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 53
Time : 420.742s (Solving: 393.51s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 420.752s
Choices : 8140639 (Domain: 7838774)
Conflicts : 405543 (Analyzed: 405540)
Restarts : 4850 (Average: 83.62 Last: 185)
Model-Level : 183.0
Problems : 53 (Average Length: 71.53 Splits: 0)
Lemmas : 405540 (Deleted: 375482)
Binary : 8079 (Ratio: 1.99%)
Ternary : 3192 (Ratio: 0.79%)
Conflict : 405540 (Average Length: 509.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 405540 (Average: 18.00 Max: 1374 Sum: 7298202)
Executed : 405390 (Average: 17.98 Max: 1374 Sum: 7292956 Ratio: 99.93%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.74s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 7.82s
Iteration 53
Queue: [(20,100,1,True), (21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 54
Time : 428.666s (Solving: 401.27s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 428.676s
Choices : 8438795 (Domain: 8135512)
Conflicts : 413601 (Analyzed: 413598)
Restarts : 4950 (Average: 83.56 Last: 185)
Model-Level : 183.0
Problems : 54 (Average Length: 72.19 Splits: 0)
Lemmas : 413598 (Deleted: 382895)
Binary : 8130 (Ratio: 1.97%)
Ternary : 3219 (Ratio: 0.78%)
Conflict : 413598 (Average Length: 507.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 413598 (Average: 18.30 Max: 1374 Sum: 7570763)
Executed : 413448 (Average: 18.29 Max: 1374 Sum: 7565517 Ratio: 99.93%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.07%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.87s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 7.93s
Iteration 54
Queue: [(21,105,1,True), (22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 55
Time : 440.515s (Solving: 412.95s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 440.516s
Choices : 9046151 (Domain: 8739101)
Conflicts : 422005 (Analyzed: 422002)
Restarts : 5050 (Average: 83.56 Last: 185)
Model-Level : 183.0
Problems : 55 (Average Length: 72.82 Splits: 0)
Lemmas : 422002 (Deleted: 390171)
Binary : 8341 (Ratio: 1.98%)
Ternary : 3405 (Ratio: 0.81%)
Conflict : 422002 (Average Length: 505.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 422002 (Average: 19.31 Max: 1374 Sum: 8148974)
Executed : 421852 (Average: 19.30 Max: 1374 Sum: 8143728 Ratio: 99.94%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 822756 (Eliminated: 0 Frozen: 253444)
Constraints : 6020448 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1005MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.77s
Memory: 914MB (+0MB)
UNKNOWN
Iteration Time: 11.84s
Iteration 55
Queue: [(22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Expected Memory: 1033.0MB
Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])]
Grounding Time: 0.56s
Memory: 914MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 56
Time : 453.155s (Solving: 424.33s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 453.164s
Choices : 9387514 (Domain: 9078824)
Conflicts : 430106 (Analyzed: 430103)
Restarts : 5150 (Average: 83.52 Last: 185)
Model-Level : 183.0
Problems : 56 (Average Length: 73.52 Splits: 0)
Lemmas : 430103 (Deleted: 397920)
Binary : 8438 (Ratio: 1.96%)
Ternary : 3434 (Ratio: 0.80%)
Conflict : 430103 (Average Length: 503.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 430103 (Average: 19.67 Max: 1374 Sum: 8461648)
Executed : 429953 (Average: 19.66 Max: 1374 Sum: 8456402 Ratio: 99.94%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 862832 (Eliminated: 0 Frozen: 265894)
Constraints : 6322428 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1037MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.54s
Memory: 946MB (+32MB)
UNKNOWN
Iteration Time: 12.66s
Iteration 56
Queue: [(23,115,0,True)]
Grounded Until: 110
Expected Memory: 1065.0MB
Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])]
Grounding Time: 0.56s
Memory: 946MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 57
Time : 477.954s (Solving: 447.85s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 477.940s
Choices : 10831659 (Domain: 10511735)
Conflicts : 440818 (Analyzed: 440815)
Restarts : 5250 (Average: 83.96 Last: 185)
Model-Level : 183.0
Problems : 57 (Average Length: 74.28 Splits: 0)
Lemmas : 440815 (Deleted: 406854)
Binary : 9271 (Ratio: 2.10%)
Ternary : 3822 (Ratio: 0.87%)
Conflict : 440815 (Average Length: 505.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 440815 (Average: 22.35 Max: 1455 Sum: 9854382)
Executed : 440665 (Average: 22.34 Max: 1455 Sum: 9849136 Ratio: 99.95%)
Bounded : 150 (Average: 34.97 Max: 107 Sum: 5246 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 110 steps
Models : 1
[endof: stats after solve call]
Solving Time: 23.66s
Memory: 975MB (+29MB)
UNKNOWN
Iteration Time: 24.79s
Iteration 57
Queue: [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 58
Time : 484.554s (Solving: 454.27s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 484.544s
Choices : 10879063 (Domain: 10559139)
Conflicts : 448316 (Analyzed: 448313)
Restarts : 5350 (Average: 83.80 Last: 185)
Model-Level : 183.0
Problems : 58 (Average Length: 75.02 Splits: 0)
Lemmas : 448313 (Deleted: 413945)
Binary : 9333 (Ratio: 2.08%)
Ternary : 3831 (Ratio: 0.85%)
Conflict : 448313 (Average Length: 501.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 448313 (Average: 22.07 Max: 1455 Sum: 9895935)
Executed : 448161 (Average: 22.06 Max: 1455 Sum: 9890455 Ratio: 99.94%)
Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624408 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.54s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 6.61s
Iteration 58
Queue: [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 59
Time : 490.556s (Solving: 460.05s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 490.548s
Choices : 10924947 (Domain: 10605023)
Conflicts : 456079 (Analyzed: 456076)
Restarts : 5450 (Average: 83.68 Last: 185)
Model-Level : 183.0
Problems : 59 (Average Length: 75.73 Splits: 0)
Lemmas : 456076 (Deleted: 421159)
Binary : 9367 (Ratio: 2.05%)
Ternary : 3833 (Ratio: 0.84%)
Conflict : 456076 (Average Length: 501.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 456076 (Average: 21.78 Max: 1455 Sum: 9932435)
Executed : 455924 (Average: 21.77 Max: 1455 Sum: 9926955 Ratio: 99.94%)
Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.92s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 6.01s
Iteration 59
Queue: [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 60
Time : 496.094s (Solving: 465.39s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 496.088s
Choices : 10986705 (Domain: 10665581)
Conflicts : 463289 (Analyzed: 463286)
Restarts : 5550 (Average: 83.47 Last: 185)
Model-Level : 183.0
Problems : 60 (Average Length: 76.42 Splits: 0)
Lemmas : 463286 (Deleted: 428631)
Binary : 9475 (Ratio: 2.05%)
Ternary : 3846 (Ratio: 0.83%)
Conflict : 463286 (Average Length: 499.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 463286 (Average: 21.55 Max: 1455 Sum: 9982573)
Executed : 463134 (Average: 21.54 Max: 1455 Sum: 9977093 Ratio: 99.95%)
Bounded : 152 (Average: 36.05 Max: 117 Sum: 5480 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.47s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 5.54s
Iteration 60
Queue: [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 61
Time : 501.089s (Solving: 470.18s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 501.084s
Choices : 11030102 (Domain: 10708956)
Conflicts : 470556 (Analyzed: 470553)
Restarts : 5650 (Average: 83.28 Last: 185)
Model-Level : 183.0
Problems : 61 (Average Length: 77.08 Splits: 0)
Lemmas : 470553 (Deleted: 435488)
Binary : 9548 (Ratio: 2.03%)
Ternary : 3868 (Ratio: 0.82%)
Conflict : 470553 (Average Length: 497.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 470553 (Average: 21.29 Max: 1455 Sum: 10017916)
Executed : 470400 (Average: 21.28 Max: 1455 Sum: 10012323 Ratio: 99.94%)
Bounded : 153 (Average: 36.56 Max: 117 Sum: 5593 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.92s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 5.00s
Iteration 61
Queue: [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 62
Time : 514.305s (Solving: 483.22s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 514.304s
Choices : 11142025 (Domain: 10817712)
Conflicts : 479227 (Analyzed: 479224)
Restarts : 5750 (Average: 83.34 Last: 185)
Model-Level : 183.0
Problems : 62 (Average Length: 77.73 Splits: 0)
Lemmas : 479224 (Deleted: 444388)
Binary : 9753 (Ratio: 2.04%)
Ternary : 3905 (Ratio: 0.81%)
Conflict : 479224 (Average Length: 509.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 479224 (Average: 21.08 Max: 1455 Sum: 10102920)
Executed : 479071 (Average: 21.07 Max: 1455 Sum: 10097327 Ratio: 99.94%)
Bounded : 153 (Average: 36.56 Max: 117 Sum: 5593 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 13.16s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 13.22s
Iteration 62
Queue: [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 63
Time : 521.554s (Solving: 490.28s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 521.548s
Choices : 11217424 (Domain: 10892754)
Conflicts : 486729 (Analyzed: 486726)
Restarts : 5850 (Average: 83.20 Last: 185)
Model-Level : 183.0
Problems : 63 (Average Length: 78.35 Splits: 0)
Lemmas : 486726 (Deleted: 450665)
Binary : 9882 (Ratio: 2.03%)
Ternary : 3947 (Ratio: 0.81%)
Conflict : 486726 (Average Length: 506.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 486726 (Average: 20.89 Max: 1455 Sum: 10166930)
Executed : 486569 (Average: 20.88 Max: 1455 Sum: 10160874 Ratio: 99.94%)
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624381 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.18s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 7.25s
Iteration 63
Queue: [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 64
Time : 532.779s (Solving: 501.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 532.780s
Choices : 11414476 (Domain: 11087229)
Conflicts : 495018 (Analyzed: 495015)
Restarts : 5950 (Average: 83.20 Last: 185)
Model-Level : 183.0
Problems : 64 (Average Length: 78.95 Splits: 0)
Lemmas : 495015 (Deleted: 457334)
Binary : 10090 (Ratio: 2.04%)
Ternary : 4014 (Ratio: 0.81%)
Conflict : 495015 (Average Length: 511.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 495015 (Average: 20.89 Max: 1455 Sum: 10341849)
Executed : 494858 (Average: 20.88 Max: 1455 Sum: 10335793 Ratio: 99.94%)
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.14s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 11.23s
Iteration 64
Queue: [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 65
Time : 544.248s (Solving: 512.57s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 544.256s
Choices : 11668016 (Domain: 11339143)
Conflicts : 503596 (Analyzed: 503593)
Restarts : 6050 (Average: 83.24 Last: 185)
Model-Level : 183.0
Problems : 65 (Average Length: 79.54 Splits: 0)
Lemmas : 503593 (Deleted: 465102)
Binary : 10213 (Ratio: 2.03%)
Ternary : 4053 (Ratio: 0.80%)
Conflict : 503593 (Average Length: 512.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 503593 (Average: 20.99 Max: 1455 Sum: 10572702)
Executed : 503436 (Average: 20.98 Max: 1455 Sum: 10566646 Ratio: 99.94%)
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.41s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 11.48s
Iteration 65
Queue: [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 66
Time : 555.128s (Solving: 523.24s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 555.144s
Choices : 11937161 (Domain: 11606955)
Conflicts : 512151 (Analyzed: 512148)
Restarts : 6150 (Average: 83.28 Last: 185)
Model-Level : 183.0
Problems : 66 (Average Length: 80.11 Splits: 0)
Lemmas : 512148 (Deleted: 473103)
Binary : 10319 (Ratio: 2.01%)
Ternary : 4077 (Ratio: 0.80%)
Conflict : 512148 (Average Length: 514.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 512148 (Average: 21.12 Max: 1455 Sum: 10816985)
Executed : 511991 (Average: 21.11 Max: 1455 Sum: 10810929 Ratio: 99.94%)
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.06%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.80s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 10.89s
Iteration 66
Queue: [(22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 67
Time : 565.666s (Solving: 533.58s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 565.688s
Choices : 12317914 (Domain: 11986494)
Conflicts : 520221 (Analyzed: 520218)
Restarts : 6250 (Average: 83.23 Last: 185)
Model-Level : 183.0
Problems : 67 (Average Length: 80.66 Splits: 0)
Lemmas : 520218 (Deleted: 481326)
Binary : 10396 (Ratio: 2.00%)
Ternary : 4130 (Ratio: 0.79%)
Conflict : 520218 (Average Length: 517.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 520218 (Average: 21.47 Max: 1455 Sum: 11168194)
Executed : 520061 (Average: 21.46 Max: 1455 Sum: 11162138 Ratio: 99.95%)
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.47s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 10.55s
Iteration 67
Queue: [(23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 68
Time : 582.335s (Solving: 550.02s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 582.364s
Choices : 13088569 (Domain: 12752469)
Conflicts : 528948 (Analyzed: 528945)
Restarts : 6350 (Average: 83.30 Last: 185)
Model-Level : 183.0
Problems : 68 (Average Length: 81.19 Splits: 0)
Lemmas : 528945 (Deleted: 490920)
Binary : 10750 (Ratio: 2.03%)
Ternary : 4323 (Ratio: 0.82%)
Conflict : 528945 (Average Length: 519.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 528945 (Average: 22.49 Max: 1562 Sum: 11896548)
Executed : 528788 (Average: 22.48 Max: 1562 Sum: 11890492 Ratio: 99.95%)
Bounded : 157 (Average: 38.57 Max: 117 Sum: 6056 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 16.59s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 16.68s
Iteration 68
Queue: [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 69
Time : 588.065s (Solving: 555.53s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 588.088s
Choices : 13146278 (Domain: 12810178)
Conflicts : 536554 (Analyzed: 536551)
Restarts : 6450 (Average: 83.19 Last: 185)
Model-Level : 183.0
Problems : 69 (Average Length: 81.71 Splits: 0)
Lemmas : 536551 (Deleted: 496486)
Binary : 10836 (Ratio: 2.02%)
Ternary : 4334 (Ratio: 0.81%)
Conflict : 536551 (Average Length: 518.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 536551 (Average: 22.27 Max: 1562 Sum: 11946514)
Executed : 536393 (Average: 22.25 Max: 1562 Sum: 11940342 Ratio: 99.95%)
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.64s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 5.73s
Iteration 69
Queue: [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 70
Time : 592.454s (Solving: 559.74s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 592.476s
Choices : 13186477 (Domain: 12850377)
Conflicts : 544160 (Analyzed: 544157)
Restarts : 6550 (Average: 83.08 Last: 185)
Model-Level : 183.0
Problems : 70 (Average Length: 82.21 Splits: 0)
Lemmas : 544157 (Deleted: 503845)
Binary : 10858 (Ratio: 2.00%)
Ternary : 4336 (Ratio: 0.80%)
Conflict : 544157 (Average Length: 517.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 544157 (Average: 22.01 Max: 1562 Sum: 11978079)
Executed : 543999 (Average: 22.00 Max: 1562 Sum: 11971907 Ratio: 99.95%)
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.33s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 4.39s
Iteration 70
Queue: [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 71
Time : 600.560s (Solving: 567.65s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 600.584s
Choices : 13260918 (Domain: 12920098)
Conflicts : 552886 (Analyzed: 552883)
Restarts : 6650 (Average: 83.14 Last: 185)
Model-Level : 183.0
Problems : 71 (Average Length: 82.70 Splits: 0)
Lemmas : 552883 (Deleted: 513368)
Binary : 10965 (Ratio: 1.98%)
Ternary : 4358 (Ratio: 0.79%)
Conflict : 552883 (Average Length: 520.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 552883 (Average: 21.77 Max: 1562 Sum: 12034743)
Executed : 552725 (Average: 21.76 Max: 1562 Sum: 12028571 Ratio: 99.95%)
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.04s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 8.11s
Iteration 71
Queue: [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 72
Time : 605.272s (Solving: 572.15s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 605.296s
Choices : 13317430 (Domain: 12975523)
Conflicts : 560480 (Analyzed: 560477)
Restarts : 6750 (Average: 83.03 Last: 185)
Model-Level : 183.0
Problems : 72 (Average Length: 83.18 Splits: 0)
Lemmas : 560477 (Deleted: 519465)
Binary : 11030 (Ratio: 1.97%)
Ternary : 4396 (Ratio: 0.78%)
Conflict : 560477 (Average Length: 517.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 560477 (Average: 21.55 Max: 1562 Sum: 12080644)
Executed : 560319 (Average: 21.54 Max: 1562 Sum: 12074472 Ratio: 99.95%)
Bounded : 158 (Average: 39.06 Max: 117 Sum: 6172 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.63s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 4.72s
Iteration 72
Queue: [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 73
Time : 612.491s (Solving: 579.19s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 612.516s
Choices : 13399866 (Domain: 13057114)
Conflicts : 568275 (Analyzed: 568272)
Restarts : 6850 (Average: 82.96 Last: 185)
Model-Level : 183.0
Problems : 73 (Average Length: 83.64 Splits: 0)
Lemmas : 568272 (Deleted: 526626)
Binary : 11227 (Ratio: 1.98%)
Ternary : 4486 (Ratio: 0.79%)
Conflict : 568272 (Average Length: 517.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 568272 (Average: 21.38 Max: 1562 Sum: 12150356)
Executed : 568113 (Average: 21.37 Max: 1562 Sum: 12144071 Ratio: 99.95%)
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.16s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 7.23s
Iteration 73
Queue: [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 74
Time : 624.730s (Solving: 591.24s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 624.756s
Choices : 13550436 (Domain: 13206308)
Conflicts : 576763 (Analyzed: 576760)
Restarts : 6950 (Average: 82.99 Last: 185)
Model-Level : 183.0
Problems : 74 (Average Length: 84.09 Splits: 0)
Lemmas : 576760 (Deleted: 533795)
Binary : 11402 (Ratio: 1.98%)
Ternary : 4562 (Ratio: 0.79%)
Conflict : 576760 (Average Length: 523.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 576760 (Average: 21.29 Max: 1562 Sum: 12278204)
Executed : 576601 (Average: 21.28 Max: 1562 Sum: 12271919 Ratio: 99.95%)
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 12.17s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 12.24s
Iteration 74
Queue: [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 75
Time : 639.378s (Solving: 605.69s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 639.408s
Choices : 13754428 (Domain: 13408461)
Conflicts : 585767 (Analyzed: 585764)
Restarts : 7050 (Average: 83.09 Last: 185)
Model-Level : 183.0
Problems : 75 (Average Length: 84.53 Splits: 0)
Lemmas : 585764 (Deleted: 543773)
Binary : 11646 (Ratio: 1.99%)
Ternary : 4656 (Ratio: 0.79%)
Conflict : 585764 (Average Length: 531.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 585764 (Average: 21.26 Max: 1562 Sum: 12452649)
Executed : 585605 (Average: 21.25 Max: 1562 Sum: 12446364 Ratio: 99.95%)
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 14.58s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 14.66s
Iteration 75
Queue: [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 76
Time : 653.162s (Solving: 619.29s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 653.196s
Choices : 13957281 (Domain: 13609805)
Conflicts : 594135 (Analyzed: 594132)
Restarts : 7150 (Average: 83.10 Last: 185)
Model-Level : 183.0
Problems : 76 (Average Length: 84.96 Splits: 0)
Lemmas : 594132 (Deleted: 550302)
Binary : 11820 (Ratio: 1.99%)
Ternary : 4704 (Ratio: 0.79%)
Conflict : 594132 (Average Length: 541.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 594132 (Average: 21.25 Max: 1562 Sum: 12625961)
Executed : 593973 (Average: 21.24 Max: 1562 Sum: 12619676 Ratio: 99.95%)
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 13.73s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 13.79s
Iteration 76
Queue: [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 77
Time : 667.620s (Solving: 633.54s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 667.660s
Choices : 14229081 (Domain: 13878957)
Conflicts : 602414 (Analyzed: 602411)
Restarts : 7250 (Average: 83.09 Last: 185)
Model-Level : 183.0
Problems : 77 (Average Length: 85.38 Splits: 0)
Lemmas : 602411 (Deleted: 558174)
Binary : 12049 (Ratio: 2.00%)
Ternary : 4758 (Ratio: 0.79%)
Conflict : 602411 (Average Length: 551.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 602411 (Average: 21.36 Max: 1562 Sum: 12866776)
Executed : 602252 (Average: 21.35 Max: 1562 Sum: 12860491 Ratio: 99.95%)
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 14.38s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 14.47s
Iteration 77
Queue: [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 78
Time : 688.445s (Solving: 654.18s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 688.492s
Choices : 14711711 (Domain: 14353351)
Conflicts : 611580 (Analyzed: 611577)
Restarts : 7350 (Average: 83.21 Last: 185)
Model-Level : 183.0
Problems : 78 (Average Length: 85.78 Splits: 0)
Lemmas : 611577 (Deleted: 567670)
Binary : 12557 (Ratio: 2.05%)
Ternary : 4895 (Ratio: 0.80%)
Conflict : 611577 (Average Length: 564.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 611577 (Average: 21.74 Max: 1562 Sum: 13295201)
Executed : 611418 (Average: 21.73 Max: 1562 Sum: 13288916 Ratio: 99.95%)
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 20.77s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 20.84s
Iteration 78
Queue: [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 79
Time : 694.262s (Solving: 659.80s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 694.312s
Choices : 14768725 (Domain: 14410365)
Conflicts : 620106 (Analyzed: 620103)
Restarts : 7450 (Average: 83.24 Last: 185)
Model-Level : 183.0
Problems : 79 (Average Length: 86.18 Splits: 0)
Lemmas : 620103 (Deleted: 574044)
Binary : 12611 (Ratio: 2.03%)
Ternary : 4906 (Ratio: 0.79%)
Conflict : 620103 (Average Length: 561.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 620103 (Average: 21.52 Max: 1562 Sum: 13342839)
Executed : 619944 (Average: 21.51 Max: 1562 Sum: 13336554 Ratio: 99.95%)
Bounded : 159 (Average: 39.53 Max: 117 Sum: 6285 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.75s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 5.82s
Iteration 79
Queue: [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 80
Time : 697.964s (Solving: 663.32s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 698.016s
Choices : 14803436 (Domain: 14445076)
Conflicts : 627340 (Analyzed: 627337)
Restarts : 7550 (Average: 83.09 Last: 185)
Model-Level : 183.0
Problems : 80 (Average Length: 86.56 Splits: 0)
Lemmas : 627337 (Deleted: 582303)
Binary : 12618 (Ratio: 2.01%)
Ternary : 4907 (Ratio: 0.78%)
Conflict : 627337 (Average Length: 561.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 627337 (Average: 21.31 Max: 1562 Sum: 13368084)
Executed : 627177 (Average: 21.30 Max: 1562 Sum: 13361682 Ratio: 99.95%)
Bounded : 160 (Average: 40.01 Max: 117 Sum: 6402 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624341 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.64s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 3.71s
Iteration 80
Queue: [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 81
Time : 705.316s (Solving: 670.46s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 705.372s
Choices : 14876037 (Domain: 14517677)
Conflicts : 635476 (Analyzed: 635473)
Restarts : 7650 (Average: 83.07 Last: 185)
Model-Level : 183.0
Problems : 81 (Average Length: 86.94 Splits: 0)
Lemmas : 635473 (Deleted: 589436)
Binary : 12660 (Ratio: 1.99%)
Ternary : 4927 (Ratio: 0.78%)
Conflict : 635473 (Average Length: 561.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 635473 (Average: 21.13 Max: 1562 Sum: 13427038)
Executed : 635312 (Average: 21.12 Max: 1562 Sum: 13420519 Ratio: 99.95%)
Bounded : 161 (Average: 40.49 Max: 117 Sum: 6519 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624315 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.27s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 7.36s
Iteration 81
Queue: [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 82
Time : 714.196s (Solving: 679.16s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 714.240s
Choices : 14964621 (Domain: 14606225)
Conflicts : 644276 (Analyzed: 644273)
Restarts : 7750 (Average: 83.13 Last: 185)
Model-Level : 183.0
Problems : 82 (Average Length: 87.30 Splits: 0)
Lemmas : 644273 (Deleted: 598824)
Binary : 12774 (Ratio: 1.98%)
Ternary : 4948 (Ratio: 0.77%)
Conflict : 644273 (Average Length: 560.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 644273 (Average: 20.95 Max: 1562 Sum: 13499468)
Executed : 644112 (Average: 20.94 Max: 1562 Sum: 13492949 Ratio: 99.95%)
Bounded : 161 (Average: 40.49 Max: 117 Sum: 6519 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.80s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 8.87s
Iteration 82
Queue: [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 83
Time : 721.282s (Solving: 686.07s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 721.328s
Choices : 15037395 (Domain: 14677670)
Conflicts : 652050 (Analyzed: 652047)
Restarts : 7850 (Average: 83.06 Last: 185)
Model-Level : 183.0
Problems : 83 (Average Length: 87.66 Splits: 0)
Lemmas : 652047 (Deleted: 605184)
Binary : 12879 (Ratio: 1.98%)
Ternary : 4985 (Ratio: 0.76%)
Conflict : 652047 (Average Length: 564.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 652047 (Average: 20.79 Max: 1562 Sum: 13555664)
Executed : 651885 (Average: 20.78 Max: 1562 Sum: 13549032 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.03s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 7.09s
Iteration 83
Queue: [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 84
Time : 735.705s (Solving: 700.30s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 735.756s
Choices : 15211825 (Domain: 14851226)
Conflicts : 660424 (Analyzed: 660421)
Restarts : 7950 (Average: 83.07 Last: 185)
Model-Level : 183.0
Problems : 84 (Average Length: 88.01 Splits: 0)
Lemmas : 660421 (Deleted: 612860)
Binary : 13052 (Ratio: 1.98%)
Ternary : 5021 (Ratio: 0.76%)
Conflict : 660421 (Average Length: 574.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 660421 (Average: 20.75 Max: 1562 Sum: 13701359)
Executed : 660259 (Average: 20.74 Max: 1562 Sum: 13694727 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 14.36s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 14.43s
Iteration 84
Queue: [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 85
Time : 749.084s (Solving: 713.49s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 749.124s
Choices : 15373876 (Domain: 15012894)
Conflicts : 668679 (Analyzed: 668676)
Restarts : 8050 (Average: 83.07 Last: 185)
Model-Level : 183.0
Problems : 85 (Average Length: 88.35 Splits: 0)
Lemmas : 668676 (Deleted: 620912)
Binary : 13146 (Ratio: 1.97%)
Ternary : 5041 (Ratio: 0.75%)
Conflict : 668676 (Average Length: 586.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 668676 (Average: 20.69 Max: 1562 Sum: 13833507)
Executed : 668514 (Average: 20.68 Max: 1562 Sum: 13826875 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 13.30s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 13.37s
Iteration 85
Queue: [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 86
Time : 763.386s (Solving: 727.61s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 763.432s
Choices : 15536270 (Domain: 15175157)
Conflicts : 677036 (Analyzed: 677033)
Restarts : 8150 (Average: 83.07 Last: 185)
Model-Level : 183.0
Problems : 86 (Average Length: 88.69 Splits: 0)
Lemmas : 677033 (Deleted: 628936)
Binary : 13199 (Ratio: 1.95%)
Ternary : 5046 (Ratio: 0.75%)
Conflict : 677033 (Average Length: 605.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 677033 (Average: 20.62 Max: 1562 Sum: 13957955)
Executed : 676871 (Average: 20.61 Max: 1562 Sum: 13951323 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 14.24s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 14.31s
Iteration 86
Queue: [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 87
Time : 769.775s (Solving: 733.81s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 769.828s
Choices : 15591549 (Domain: 15230434)
Conflicts : 684391 (Analyzed: 684388)
Restarts : 8250 (Average: 82.96 Last: 185)
Model-Level : 183.0
Problems : 87 (Average Length: 89.01 Splits: 0)
Lemmas : 684388 (Deleted: 637148)
Binary : 13249 (Ratio: 1.94%)
Ternary : 5048 (Ratio: 0.74%)
Conflict : 684388 (Average Length: 601.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 684388 (Average: 20.44 Max: 1562 Sum: 13987653)
Executed : 684226 (Average: 20.43 Max: 1562 Sum: 13981021 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.32s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 6.40s
Iteration 87
Queue: [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 88
Time : 773.674s (Solving: 737.53s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 773.728s
Choices : 15625291 (Domain: 15264176)
Conflicts : 691658 (Analyzed: 691655)
Restarts : 8350 (Average: 82.83 Last: 185)
Model-Level : 183.0
Problems : 88 (Average Length: 89.33 Splits: 0)
Lemmas : 691655 (Deleted: 644095)
Binary : 13256 (Ratio: 1.92%)
Ternary : 5049 (Ratio: 0.73%)
Conflict : 691655 (Average Length: 599.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 691655 (Average: 20.26 Max: 1562 Sum: 14012397)
Executed : 691493 (Average: 20.25 Max: 1562 Sum: 14005765 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.84s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 3.90s
Iteration 88
Queue: [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 89
Time : 783.702s (Solving: 747.38s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 783.760s
Choices : 15701115 (Domain: 15340000)
Conflicts : 700133 (Analyzed: 700130)
Restarts : 8450 (Average: 82.86 Last: 185)
Model-Level : 183.0
Problems : 89 (Average Length: 89.64 Splits: 0)
Lemmas : 700130 (Deleted: 651507)
Binary : 13411 (Ratio: 1.92%)
Ternary : 5069 (Ratio: 0.72%)
Conflict : 700130 (Average Length: 605.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 700130 (Average: 20.10 Max: 1562 Sum: 14069643)
Executed : 699968 (Average: 20.09 Max: 1562 Sum: 14063011 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.97s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 10.03s
Iteration 89
Queue: [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 90
Time : 798.822s (Solving: 762.31s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 798.888s
Choices : 15834625 (Domain: 15472834)
Conflicts : 708742 (Analyzed: 708739)
Restarts : 8550 (Average: 82.89 Last: 185)
Model-Level : 183.0
Problems : 90 (Average Length: 89.94 Splits: 0)
Lemmas : 708739 (Deleted: 659396)
Binary : 13646 (Ratio: 1.93%)
Ternary : 5096 (Ratio: 0.72%)
Conflict : 708739 (Average Length: 620.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 708739 (Average: 20.00 Max: 1562 Sum: 14174053)
Executed : 708577 (Average: 19.99 Max: 1562 Sum: 14167421 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 15.06s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 15.13s
Iteration 90
Queue: [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 91
Time : 810.135s (Solving: 773.44s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 810.204s
Choices : 16005985 (Domain: 15642429)
Conflicts : 717486 (Analyzed: 717483)
Restarts : 8650 (Average: 82.95 Last: 185)
Model-Level : 183.0
Problems : 91 (Average Length: 90.24 Splits: 0)
Lemmas : 717483 (Deleted: 669731)
Binary : 13747 (Ratio: 1.92%)
Ternary : 5143 (Ratio: 0.72%)
Conflict : 717483 (Average Length: 620.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 717483 (Average: 19.96 Max: 1562 Sum: 14324454)
Executed : 717321 (Average: 19.96 Max: 1562 Sum: 14317822 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.25s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 11.32s
Iteration 91
Queue: [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 92
Time : 819.691s (Solving: 782.77s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 819.764s
Choices : 16161851 (Domain: 15797917)
Conflicts : 725743 (Analyzed: 725740)
Restarts : 8750 (Average: 82.94 Last: 185)
Model-Level : 183.0
Problems : 92 (Average Length: 90.53 Splits: 0)
Lemmas : 725740 (Deleted: 676141)
Binary : 13781 (Ratio: 1.90%)
Ternary : 5172 (Ratio: 0.71%)
Conflict : 725740 (Average Length: 621.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 725740 (Average: 19.92 Max: 1562 Sum: 14457524)
Executed : 725578 (Average: 19.91 Max: 1562 Sum: 14450892 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.47s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 9.56s
Iteration 92
Queue: [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 93
Time : 826.658s (Solving: 789.53s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 826.736s
Choices : 16291240 (Domain: 15926314)
Conflicts : 733422 (Analyzed: 733419)
Restarts : 8850 (Average: 82.87 Last: 185)
Model-Level : 183.0
Problems : 93 (Average Length: 90.82 Splits: 0)
Lemmas : 733419 (Deleted: 684072)
Binary : 13809 (Ratio: 1.88%)
Ternary : 5182 (Ratio: 0.71%)
Conflict : 733419 (Average Length: 619.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 733419 (Average: 19.86 Max: 1562 Sum: 14566457)
Executed : 733257 (Average: 19.85 Max: 1562 Sum: 14559825 Ratio: 99.95%)
Bounded : 162 (Average: 40.94 Max: 117 Sum: 6632 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.89s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 6.97s
Iteration 93
Queue: [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 94
Time : 835.736s (Solving: 798.43s 1st Model: 0.00s Unsat: 2.40s)
CPU Time : 835.808s
Choices : 16464509 (Domain: 16099110)
Conflicts : 741679 (Analyzed: 741676)
Restarts : 8950 (Average: 82.87 Last: 185)
Model-Level : 183.0
Problems : 94 (Average Length: 91.10 Splits: 0)
Lemmas : 741676 (Deleted: 691616)
Binary : 13833 (Ratio: 1.87%)
Ternary : 5187 (Ratio: 0.70%)
Conflict : 741676 (Average Length: 620.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 741676 (Average: 19.84 Max: 1562 Sum: 14715303)
Executed : 741513 (Average: 19.83 Max: 1562 Sum: 14708554 Ratio: 99.95%)
Bounded : 163 (Average: 41.40 Max: 117 Sum: 6749 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624301 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.01s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 9.07s
Iteration 94
Queue: [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 95
Time : 843.746s (Solving: 806.25s 1st Model: 0.00s Unsat: 10.22s)
CPU Time : 843.820s
Choices : 16496702 (Domain: 16131303)
Conflicts : 746118 (Analyzed: 746114)
Restarts : 9002 (Average: 82.88 Last: 185)
Model-Level : 183.0
Problems : 95 (Average Length: 91.37 Splits: 0)
Lemmas : 746114 (Deleted: 696156)
Binary : 13909 (Ratio: 1.86%)
Ternary : 5196 (Ratio: 0.70%)
Conflict : 746114 (Average Length: 618.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 746114 (Average: 19.76 Max: 1562 Sum: 14746605)
Executed : 745949 (Average: 19.76 Max: 1562 Sum: 14739854 Ratio: 99.95%)
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.94s
Memory: 975MB (+0MB)
UNSAT
Iteration Time: 8.02s
Iteration 95
Queue: [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 96
Time : 846.967s (Solving: 809.29s 1st Model: 0.00s Unsat: 10.22s)
CPU Time : 847.044s
Choices : 16532716 (Domain: 16167317)
Conflicts : 753267 (Analyzed: 753263)
Restarts : 9102 (Average: 82.76 Last: 185)
Model-Level : 183.0
Problems : 96 (Average Length: 91.64 Splits: 0)
Lemmas : 753263 (Deleted: 703244)
Binary : 13916 (Ratio: 1.85%)
Ternary : 5197 (Ratio: 0.69%)
Conflict : 753263 (Average Length: 615.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 753263 (Average: 19.61 Max: 1562 Sum: 14773887)
Executed : 753098 (Average: 19.60 Max: 1562 Sum: 14767136 Ratio: 99.95%)
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.16s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 3.23s
Iteration 96
Queue: [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 97
Time : 860.534s (Solving: 822.67s 1st Model: 0.00s Unsat: 10.22s)
CPU Time : 860.616s
Choices : 16617579 (Domain: 16252173)
Conflicts : 761752 (Analyzed: 761748)
Restarts : 9202 (Average: 82.78 Last: 185)
Model-Level : 183.0
Problems : 97 (Average Length: 91.90 Splits: 0)
Lemmas : 761748 (Deleted: 710889)
Binary : 13978 (Ratio: 1.83%)
Ternary : 5219 (Ratio: 0.69%)
Conflict : 761748 (Average Length: 623.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 761748 (Average: 19.48 Max: 1562 Sum: 14839853)
Executed : 761583 (Average: 19.47 Max: 1562 Sum: 14833102 Ratio: 99.95%)
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 13.50s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 13.57s
Iteration 97
Queue: [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 98
Time : 866.128s (Solving: 828.05s 1st Model: 0.00s Unsat: 10.22s)
CPU Time : 866.212s
Choices : 16671064 (Domain: 16305658)
Conflicts : 769396 (Analyzed: 769392)
Restarts : 9302 (Average: 82.71 Last: 185)
Model-Level : 183.0
Problems : 98 (Average Length: 92.15 Splits: 0)
Lemmas : 769392 (Deleted: 719004)
Binary : 13992 (Ratio: 1.82%)
Ternary : 5225 (Ratio: 0.68%)
Conflict : 769392 (Average Length: 621.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 769392 (Average: 19.34 Max: 1562 Sum: 14878825)
Executed : 769227 (Average: 19.33 Max: 1562 Sum: 14872074 Ratio: 99.95%)
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.51s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 5.60s
Iteration 98
Queue: [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 99
Time : 874.300s (Solving: 836.02s 1st Model: 0.00s Unsat: 10.22s)
CPU Time : 874.388s
Choices : 16771158 (Domain: 16405189)
Conflicts : 777657 (Analyzed: 777653)
Restarts : 9402 (Average: 82.71 Last: 185)
Model-Level : 183.0
Problems : 99 (Average Length: 92.40 Splits: 0)
Lemmas : 777653 (Deleted: 726455)
Binary : 14083 (Ratio: 1.81%)
Ternary : 5235 (Ratio: 0.67%)
Conflict : 777653 (Average Length: 621.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 777653 (Average: 19.23 Max: 1562 Sum: 14957932)
Executed : 777488 (Average: 19.23 Max: 1562 Sum: 14951181 Ratio: 99.95%)
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.05%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.10s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 8.18s
Iteration 99
Queue: [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 100
Time : 888.923s (Solving: 850.46s 1st Model: 0.00s Unsat: 10.22s)
CPU Time : 889.016s
Choices : 16945498 (Domain: 16578149)
Conflicts : 786145 (Analyzed: 786141)
Restarts : 9502 (Average: 82.73 Last: 185)
Model-Level : 183.0
Problems : 100 (Average Length: 92.65 Splits: 0)
Lemmas : 786141 (Deleted: 734313)
Binary : 14299 (Ratio: 1.82%)
Ternary : 5281 (Ratio: 0.67%)
Conflict : 786141 (Average Length: 624.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 786141 (Average: 19.21 Max: 1562 Sum: 15101934)
Executed : 785976 (Average: 19.20 Max: 1562 Sum: 15095183 Ratio: 99.96%)
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.04%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 14.56s
Memory: 975MB (+0MB)
UNKNOWN
Iteration Time: 14.63s
Iteration 100
Queue: [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN
INTERRUPTED : 1
Models : 0+
Calls : 101
Time : 892.583s (Solving: 853.91s 1st Model: 0.00s Unsat: 10.22s)
CPU Time : 892.652s
Choices : 16998304 (Domain: 16630745)
Conflicts : 788629 (Analyzed: 788625)
Restarts : 9529 (Average: 82.76 Last: 185)
Model-Level : 183.0
Problems : 101 (Average Length: 92.89 Splits: 0)
Lemmas : 788625 (Deleted: 738218)
Binary : 14320 (Ratio: 1.82%)
Ternary : 5287 (Ratio: 0.67%)
Conflict : 788625 (Average Length: 624.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 788625 (Average: 19.21 Max: 1562 Sum: 15147547)
Executed : 788460 (Average: 19.20 Max: 1562 Sum: 15140796 Ratio: 99.96%)
Bounded : 165 (Average: 40.92 Max: 117 Sum: 6751 Ratio: 0.04%)
Rules : 91724 (Original: 89679)
Atoms : 73746
Bodies : 16519 (Original: 14473)
Count : 330 (Original: 739)
Equivalences : 4525 (Atom=Atom: 82 Body=Body: 0 Other: 4443)
Tight : Yes
Variables : 902908 (Eliminated: 0 Frozen: 278344)
Constraints : 6624275 (Binary: 91.2% Ternary: 7.0% Other: 1.8%)
Memory Peak : 1071MB
Max. Length : 115 steps
Models : 1