1
0
Fork 0
tplp-planning-benchmark/gc-ta1-tt1/ipc-2011_barman-sequential-...

5952 lines
219 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-5.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-5.pddl
Parsing...
Parsing: [0.030s CPU, 0.031s wall-clock]
Normalizing task... [0.000s CPU, 0.002s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.008s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.030s CPU, 0.041s wall-clock]
Preparing model... [0.030s CPU, 0.022s wall-clock]
Generated 115 rules.
Computing model... [0.370s CPU, 0.373s wall-clock]
2300 relevant atoms
2393 auxiliary atoms
4693 final queue length
8087 total queue pushes
Completing instantiation... [0.690s CPU, 0.690s wall-clock]
Instantiating: [1.130s CPU, 1.139s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.130s CPU, 0.131s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.007s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
238 uncovered facts
Choosing groups: [0.010s CPU, 0.001s wall-clock]
Building translation key... [0.010s CPU, 0.009s wall-clock]
Computing fact groups: [0.170s CPU, 0.167s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock]
Building dictionary for full mutex groups... [0.000s CPU, 0.002s wall-clock]
Building mutex information...
Building mutex information: [0.010s CPU, 0.003s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.030s CPU, 0.039s wall-clock]
Translating task: [0.730s CPU, 0.730s wall-clock]
2672 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.360s CPU, 0.357s wall-clock]
Reordering and filtering variables...
241 of 241 variables necessary.
12 of 15 mutex groups necessary.
1596 of 1596 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.240s CPU, 0.242s wall-clock]
Translator variables: 241
Translator derived variables: 0
Translator facts: 505
Translator goal facts: 10
Translator mutex groups: 12
Translator total mutex groups size: 36
Translator operators: 1596
Translator axioms: 0
Translator task size: 15302
Translator peak memory: 45004 KB
Writing output... [0.300s CPU, 0.321s wall-clock]
Done! [2.990s CPU, 3.026s wall-clock]
planner.py version 0.0.1
Time: 0.61s
Memory: 91MB
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 : 0.713s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.616s
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 : 44183
Atoms : 44183
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 : 227MB
Max. Length : 0 steps
Models : 0
[endof: stats after solve call]
Solving Time: 0.00s
Memory: 163MB (+72MB)
UNSAT
Iteration Time: 0.00s
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: 163MB
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
Grounding Time: 0.19s
Memory: 163MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 1+
Calls : 2
Time : 1.005s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.908s
Choices : 367 (Domain: 28)
Conflicts : 8 (Analyzed: 8)
Restarts : 0
Model-Level : 115.0
Problems : 2 (Average Length: 4.50 Splits: 0)
Lemmas : 8 (Deleted: 0)
Binary : 6 (Ratio: 75.00%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 8 (Average Length: 10.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 8 (Average: 32.62 Max: 84 Sum: 261)
Executed : 6 (Average: 32.38 Max: 84 Sum: 259 Ratio: 99.23%)
Bounded : 2 (Average: 1.00 Max: 1 Sum: 2 Ratio: 0.77%)
Rules : 44183
Atoms : 44183
Bodies : 1 (Original: 0)
Tight : Yes
Variables : 11842 (Eliminated: 0 Frozen: 130)
Constraints : 40811 (Binary: 95.1% Ternary: 3.4% Other: 1.4%)
Memory Peak : 227MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.02s
Memory: 165MB (+2MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time: 0.62s
Memory: 188MB (+23MB)
Solving...
[start: stats after solve call]
Models : 0
Calls : 3
Time : 1.102s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 1.004s
Choices : 368 (Domain: 28)
Conflicts : 10 (Analyzed: 9)
Restarts : 0
Model-Level : 115.0
Problems : 3 (Average Length: 5.33 Splits: 0)
Lemmas : 9 (Deleted: 0)
Binary : 7 (Ratio: 77.78%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 9 (Average Length: 9.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 9 (Average: 29.22 Max: 84 Sum: 263)
Executed : 6 (Average: 28.89 Max: 84 Sum: 260 Ratio: 98.86%)
Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 1.14%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 14564 (Eliminated: 0 Frozen: 3202)
Constraints : 60980 (Binary: 92.3% Ternary: 5.5% Other: 2.3%)
Memory Peak : 227MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.01s
Memory: 188MB (+0MB)
UNSAT
Iteration Time: 0.93s
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: 190.0MB
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
Grounding Time: 0.34s
Memory: 188MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 4
Time : 2.227s (Solving: 0.64s 1st Model: 0.00s Unsat: 0.64s)
CPU Time : 2.128s
Choices : 20428 (Domain: 19268)
Conflicts : 2400 (Analyzed: 2398)
Restarts : 30 (Average: 79.93 Last: 10)
Model-Level : 115.0
Problems : 4 (Average Length: 7.00 Splits: 0)
Lemmas : 2398 (Deleted: 589)
Binary : 334 (Ratio: 13.93%)
Ternary : 293 (Ratio: 12.22%)
Conflict : 2398 (Average Length: 30.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 2398 (Average: 8.56 Max: 84 Sum: 20522)
Executed : 2365 (Average: 8.42 Max: 84 Sum: 20181 Ratio: 98.34%)
Bounded : 33 (Average: 10.33 Max: 12 Sum: 341 Ratio: 1.66%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 40960 (Eliminated: 0 Frozen: 11742)
Constraints : 262050 (Binary: 91.6% Ternary: 6.4% Other: 1.9%)
Memory Peak : 227MB
Max. Length : 5 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.66s
Memory: 197MB (+9MB)
UNSAT
Iteration Time: 1.13s
Iteration 4
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 10
Expected Memory: 206.0MB
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
Grounding Time: 0.38s
Memory: 203MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 5
Time : 5.613s (Solving: 3.47s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 5.516s
Choices : 83668 (Domain: 80839)
Conflicts : 9035 (Analyzed: 9032)
Restarts : 102 (Average: 88.55 Last: 20)
Model-Level : 115.0
Problems : 5 (Average Length: 9.00 Splits: 0)
Lemmas : 9032 (Deleted: 4942)
Binary : 1008 (Ratio: 11.16%)
Ternary : 545 (Ratio: 6.03%)
Conflict : 9032 (Average Length: 125.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 9032 (Average: 9.18 Max: 95 Sum: 82898)
Executed : 8982 (Average: 9.11 Max: 95 Sum: 82286 Ratio: 99.26%)
Bounded : 50 (Average: 12.24 Max: 17 Sum: 612 Ratio: 0.74%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 67356 (Eliminated: 0 Frozen: 20282)
Constraints : 425655 (Binary: 91.7% Ternary: 6.4% Other: 2.0%)
Memory Peak : 227MB
Max. Length : 10 steps
Models : 1
[endof: stats after solve call]
Solving Time: 2.86s
Memory: 216MB (+13MB)
UNSAT
Iteration Time: 3.40s
Iteration 5
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 15
Expected Memory: 235.0MB
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
Grounding Time: 0.40s
Memory: 223MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 6
Time : 11.145s (Solving: 8.41s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 11.048s
Choices : 194835 (Domain: 179881)
Conflicts : 18138 (Analyzed: 18135)
Restarts : 202 (Average: 89.78 Last: 101)
Model-Level : 115.0
Problems : 6 (Average Length: 11.17 Splits: 0)
Lemmas : 18135 (Deleted: 12424)
Binary : 1624 (Ratio: 8.96%)
Ternary : 778 (Ratio: 4.29%)
Conflict : 18135 (Average Length: 297.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 18135 (Average: 10.37 Max: 302 Sum: 188090)
Executed : 18076 (Average: 10.33 Max: 302 Sum: 187289 Ratio: 99.57%)
Bounded : 59 (Average: 13.58 Max: 22 Sum: 801 Ratio: 0.43%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 93752 (Eliminated: 0 Frozen: 28822)
Constraints : 621350 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 239MB
Max. Length : 15 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.97s
Memory: 239MB (+16MB)
UNKNOWN
Iteration Time: 5.54s
Iteration 6
Queue: [(5,25,0,True), (6,30,0,True)]
Grounded Until: 20
Expected Memory: 262.0MB
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
Grounding Time: 0.37s
Memory: 244MB (+5MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 7
Time : 17.906s (Solving: 14.59s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 17.812s
Choices : 327156 (Domain: 302805)
Conflicts : 26901 (Analyzed: 26898)
Restarts : 302 (Average: 89.07 Last: 101)
Model-Level : 115.0
Problems : 7 (Average Length: 13.43 Splits: 0)
Lemmas : 26898 (Deleted: 18459)
Binary : 2330 (Ratio: 8.66%)
Ternary : 962 (Ratio: 3.58%)
Conflict : 26898 (Average Length: 278.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 26898 (Average: 11.69 Max: 357 Sum: 314445)
Executed : 26829 (Average: 11.65 Max: 357 Sum: 313374 Ratio: 99.66%)
Bounded : 69 (Average: 15.52 Max: 27 Sum: 1071 Ratio: 0.34%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 120148 (Eliminated: 0 Frozen: 37362)
Constraints : 815724 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 263MB
Max. Length : 20 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.22s
Memory: 253MB (+9MB)
UNKNOWN
Iteration Time: 6.77s
Iteration 7
Queue: [(6,30,0,True)]
Grounded Until: 25
Expected Memory: 276.0MB
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
Grounding Time: 0.45s
Memory: 267MB (+14MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 8
Time : 25.353s (Solving: 21.36s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 25.264s
Choices : 455849 (Domain: 424072)
Conflicts : 36045 (Analyzed: 36042)
Restarts : 402 (Average: 89.66 Last: 101)
Model-Level : 115.0
Problems : 8 (Average Length: 15.75 Splits: 0)
Lemmas : 36042 (Deleted: 26452)
Binary : 2666 (Ratio: 7.40%)
Ternary : 1049 (Ratio: 2.91%)
Conflict : 36042 (Average Length: 306.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 36042 (Average: 12.05 Max: 357 Sum: 434442)
Executed : 35970 (Average: 12.02 Max: 357 Sum: 433275 Ratio: 99.73%)
Bounded : 72 (Average: 16.21 Max: 32 Sum: 1167 Ratio: 0.27%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 146544 (Eliminated: 0 Frozen: 45902)
Constraints : 1012058 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 291MB
Max. Length : 25 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.81s
Memory: 291MB (+24MB)
UNKNOWN
Iteration Time: 7.46s
Iteration 8
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), (17,85,0,True)]
Grounded Until: 30
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 9
Time : 29.288s (Solving: 25.26s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 29.204s
Choices : 495709 (Domain: 462324)
Conflicts : 43610 (Analyzed: 43607)
Restarts : 502 (Average: 86.87 Last: 101)
Model-Level : 115.0
Problems : 9 (Average Length: 17.56 Splits: 0)
Lemmas : 43607 (Deleted: 34188)
Binary : 2830 (Ratio: 6.49%)
Ternary : 1098 (Ratio: 2.52%)
Conflict : 43607 (Average Length: 347.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 43607 (Average: 10.73 Max: 357 Sum: 467733)
Executed : 43535 (Average: 10.70 Max: 357 Sum: 466566 Ratio: 99.75%)
Bounded : 72 (Average: 16.21 Max: 32 Sum: 1167 Ratio: 0.25%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 146544 (Eliminated: 0 Frozen: 45902)
Constraints : 1012016 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 291MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.93s
Memory: 291MB (+0MB)
UNKNOWN
Iteration Time: 3.94s
Iteration 9
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), (17,85,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 10
Time : 34.868s (Solving: 30.80s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 34.784s
Choices : 585465 (Domain: 547882)
Conflicts : 52309 (Analyzed: 52306)
Restarts : 602 (Average: 86.89 Last: 101)
Model-Level : 115.0
Problems : 10 (Average Length: 19.00 Splits: 0)
Lemmas : 52306 (Deleted: 41407)
Binary : 3164 (Ratio: 6.05%)
Ternary : 1154 (Ratio: 2.21%)
Conflict : 52306 (Average Length: 342.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 52306 (Average: 10.49 Max: 357 Sum: 548691)
Executed : 52232 (Average: 10.47 Max: 357 Sum: 547465 Ratio: 99.78%)
Bounded : 74 (Average: 16.57 Max: 32 Sum: 1226 Ratio: 0.22%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 146544 (Eliminated: 0 Frozen: 45902)
Constraints : 1012016 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 291MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.57s
Memory: 291MB (+0MB)
UNKNOWN
Iteration Time: 5.59s
Iteration 10
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), (17,85,0,True)]
Grounded Until: 30
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 11
Time : 40.323s (Solving: 36.23s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 40.240s
Choices : 678499 (Domain: 638387)
Conflicts : 61022 (Analyzed: 61019)
Restarts : 702 (Average: 86.92 Last: 101)
Model-Level : 115.0
Problems : 11 (Average Length: 20.18 Splits: 0)
Lemmas : 61019 (Deleted: 49566)
Binary : 3372 (Ratio: 5.53%)
Ternary : 1184 (Ratio: 1.94%)
Conflict : 61019 (Average Length: 343.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 61019 (Average: 10.37 Max: 357 Sum: 632788)
Executed : 60943 (Average: 10.35 Max: 357 Sum: 631498 Ratio: 99.80%)
Bounded : 76 (Average: 16.97 Max: 32 Sum: 1290 Ratio: 0.20%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 146544 (Eliminated: 0 Frozen: 45902)
Constraints : 1012003 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 291MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.45s
Memory: 291MB (+0MB)
UNKNOWN
Iteration Time: 5.46s
Iteration 11
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), (17,85,0,True)]
Grounded Until: 30
Expected Memory: 329.0MB
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time: 0.40s
Memory: 291MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 12
Time : 45.860s (Solving: 41.12s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 45.780s
Choices : 779563 (Domain: 736842)
Conflicts : 69781 (Analyzed: 69778)
Restarts : 802 (Average: 87.00 Last: 101)
Model-Level : 115.0
Problems : 12 (Average Length: 21.58 Splits: 0)
Lemmas : 69778 (Deleted: 57819)
Binary : 3502 (Ratio: 5.02%)
Ternary : 1233 (Ratio: 1.77%)
Conflict : 69778 (Average Length: 342.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 69778 (Average: 10.38 Max: 357 Sum: 724277)
Executed : 69699 (Average: 10.36 Max: 357 Sum: 722876 Ratio: 99.81%)
Bounded : 79 (Average: 17.73 Max: 37 Sum: 1401 Ratio: 0.19%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 172940 (Eliminated: 0 Frozen: 54442)
Constraints : 1210969 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 316MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.94s
Memory: 301MB (+10MB)
UNKNOWN
Iteration Time: 5.55s
Iteration 12
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), (17,85,0,True)]
Grounded Until: 35
Expected Memory: 339.0MB
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time: 0.39s
Memory: 307MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 13
Time : 51.131s (Solving: 45.74s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 51.052s
Choices : 867707 (Domain: 823138)
Conflicts : 78104 (Analyzed: 78101)
Restarts : 902 (Average: 86.59 Last: 107)
Model-Level : 115.0
Problems : 13 (Average Length: 23.15 Splits: 0)
Lemmas : 78101 (Deleted: 64093)
Binary : 3639 (Ratio: 4.66%)
Ternary : 1263 (Ratio: 1.62%)
Conflict : 78101 (Average Length: 339.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 78101 (Average: 10.28 Max: 357 Sum: 802547)
Executed : 78022 (Average: 10.26 Max: 357 Sum: 801146 Ratio: 99.83%)
Bounded : 79 (Average: 17.73 Max: 37 Sum: 1401 Ratio: 0.17%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 199336 (Eliminated: 0 Frozen: 62982)
Constraints : 1411993 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 337MB
Max. Length : 35 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.67s
Memory: 320MB (+13MB)
UNKNOWN
Iteration Time: 5.28s
Iteration 13
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), (17,85,0,True)]
Grounded Until: 40
Expected Memory: 358.0MB
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time: 0.40s
Memory: 326MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 14
Time : 56.198s (Solving: 50.12s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 56.112s
Choices : 979870 (Domain: 934167)
Conflicts : 86377 (Analyzed: 86374)
Restarts : 1002 (Average: 86.20 Last: 110)
Model-Level : 115.0
Problems : 14 (Average Length: 24.86 Splits: 0)
Lemmas : 86374 (Deleted: 71864)
Binary : 3834 (Ratio: 4.44%)
Ternary : 1306 (Ratio: 1.51%)
Conflict : 86374 (Average Length: 327.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 86374 (Average: 10.49 Max: 423 Sum: 906136)
Executed : 86293 (Average: 10.47 Max: 423 Sum: 904651 Ratio: 99.84%)
Bounded : 81 (Average: 18.33 Max: 42 Sum: 1485 Ratio: 0.16%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 225732 (Eliminated: 0 Frozen: 71522)
Constraints : 1613063 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 359MB
Max. Length : 40 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.43s
Memory: 354MB (+28MB)
UNKNOWN
Iteration Time: 5.07s
Iteration 14
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), (17,85,0,True)]
Grounded Until: 45
Expected Memory: 392.0MB
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time: 0.37s
Memory: 354MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 15
Time : 61.629s (Solving: 54.90s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 61.544s
Choices : 1103188 (Domain: 1055956)
Conflicts : 94165 (Analyzed: 94162)
Restarts : 1102 (Average: 85.45 Last: 110)
Model-Level : 115.0
Problems : 15 (Average Length: 26.67 Splits: 0)
Lemmas : 94162 (Deleted: 79983)
Binary : 3911 (Ratio: 4.15%)
Ternary : 1326 (Ratio: 1.41%)
Conflict : 94162 (Average Length: 331.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 94162 (Average: 10.79 Max: 423 Sum: 1016477)
Executed : 94081 (Average: 10.78 Max: 423 Sum: 1014992 Ratio: 99.85%)
Bounded : 81 (Average: 18.33 Max: 42 Sum: 1485 Ratio: 0.15%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 252128 (Eliminated: 0 Frozen: 80062)
Constraints : 1814133 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 387MB
Max. Length : 45 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.83s
Memory: 362MB (+8MB)
UNKNOWN
Iteration Time: 5.44s
Iteration 15
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), (17,85,0,True)]
Grounded Until: 50
Expected Memory: 400.0MB
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time: 0.38s
Memory: 367MB (+5MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 16
Time : 67.229s (Solving: 59.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 67.148s
Choices : 1220676 (Domain: 1172081)
Conflicts : 102486 (Analyzed: 102483)
Restarts : 1202 (Average: 85.26 Last: 110)
Model-Level : 115.0
Problems : 16 (Average Length: 28.56 Splits: 0)
Lemmas : 102483 (Deleted: 87348)
Binary : 4006 (Ratio: 3.91%)
Ternary : 1342 (Ratio: 1.31%)
Conflict : 102483 (Average Length: 327.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 102483 (Average: 10.95 Max: 533 Sum: 1122544)
Executed : 102399 (Average: 10.94 Max: 533 Sum: 1120893 Ratio: 99.85%)
Bounded : 84 (Average: 19.65 Max: 57 Sum: 1651 Ratio: 0.15%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 278524 (Eliminated: 0 Frozen: 88602)
Constraints : 2015203 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 410MB
Max. Length : 50 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.99s
Memory: 382MB (+15MB)
UNKNOWN
Iteration Time: 5.61s
Iteration 16
Queue: [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until: 55
Expected Memory: 420.0MB
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
Grounding Time: 0.39s
Memory: 383MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 17
Time : 72.326s (Solving: 64.21s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 72.248s
Choices : 1366534 (Domain: 1315690)
Conflicts : 110475 (Analyzed: 110472)
Restarts : 1302 (Average: 84.85 Last: 110)
Model-Level : 115.0
Problems : 17 (Average Length: 30.53 Splits: 0)
Lemmas : 110472 (Deleted: 95163)
Binary : 4123 (Ratio: 3.73%)
Ternary : 1359 (Ratio: 1.23%)
Conflict : 110472 (Average Length: 325.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 110472 (Average: 11.37 Max: 533 Sum: 1256134)
Executed : 110386 (Average: 11.35 Max: 533 Sum: 1254364 Ratio: 99.86%)
Bounded : 86 (Average: 20.58 Max: 62 Sum: 1770 Ratio: 0.14%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 304920 (Eliminated: 0 Frozen: 97142)
Constraints : 2216234 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 429MB
Max. Length : 55 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.45s
Memory: 400MB (+17MB)
UNKNOWN
Iteration Time: 5.11s
Iteration 17
Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until: 60
Expected Memory: 438.0MB
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
Grounding Time: 0.39s
Memory: 404MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 18
Time : 78.486s (Solving: 69.64s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 78.412s
Choices : 1582259 (Domain: 1528281)
Conflicts : 119385 (Analyzed: 119382)
Restarts : 1402 (Average: 85.15 Last: 110)
Model-Level : 115.0
Problems : 18 (Average Length: 32.56 Splits: 0)
Lemmas : 119382 (Deleted: 104860)
Binary : 4250 (Ratio: 3.56%)
Ternary : 1388 (Ratio: 1.16%)
Conflict : 119382 (Average Length: 332.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 119382 (Average: 12.19 Max: 533 Sum: 1455416)
Executed : 119296 (Average: 12.18 Max: 533 Sum: 1453646 Ratio: 99.88%)
Bounded : 86 (Average: 20.58 Max: 62 Sum: 1770 Ratio: 0.12%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 331316 (Eliminated: 0 Frozen: 105682)
Constraints : 2413082 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 450MB
Max. Length : 60 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.51s
Memory: 448MB (+44MB)
UNKNOWN
Iteration Time: 6.17s
Iteration 18
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until: 65
Expected Memory: 496.0MB
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
Grounding Time: 0.53s
Memory: 460MB (+12MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 19
Time : 85.932s (Solving: 76.22s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 85.860s
Choices : 1785835 (Domain: 1729631)
Conflicts : 127765 (Analyzed: 127762)
Restarts : 1502 (Average: 85.06 Last: 110)
Model-Level : 115.0
Problems : 19 (Average Length: 34.63 Splits: 0)
Lemmas : 127762 (Deleted: 111723)
Binary : 4439 (Ratio: 3.47%)
Ternary : 1427 (Ratio: 1.12%)
Conflict : 127762 (Average Length: 356.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 127762 (Average: 12.82 Max: 641 Sum: 1638063)
Executed : 127673 (Average: 12.81 Max: 641 Sum: 1636080 Ratio: 99.88%)
Bounded : 89 (Average: 22.28 Max: 72 Sum: 1983 Ratio: 0.12%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 357712 (Eliminated: 0 Frozen: 114222)
Constraints : 2614152 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 504MB
Max. Length : 65 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.65s
Memory: 463MB (+3MB)
UNKNOWN
Iteration Time: 7.46s
Iteration 19
Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until: 70
Expected Memory: 511.0MB
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
Grounding Time: 0.37s
Memory: 463MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 20
Time : 93.510s (Solving: 83.07s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 93.440s
Choices : 2058865 (Domain: 1999152)
Conflicts : 136710 (Analyzed: 136707)
Restarts : 1602 (Average: 85.34 Last: 110)
Model-Level : 115.0
Problems : 20 (Average Length: 36.75 Splits: 0)
Lemmas : 136707 (Deleted: 121778)
Binary : 4652 (Ratio: 3.40%)
Ternary : 1445 (Ratio: 1.06%)
Conflict : 136707 (Average Length: 377.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 136707 (Average: 13.82 Max: 671 Sum: 1889318)
Executed : 136616 (Average: 13.80 Max: 671 Sum: 1887181 Ratio: 99.89%)
Bounded : 91 (Average: 23.48 Max: 77 Sum: 2137 Ratio: 0.11%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 384108 (Eliminated: 0 Frozen: 122762)
Constraints : 2815194 (Binary: 91.5% Ternary: 6.6% Other: 1.9%)
Memory Peak : 515MB
Max. Length : 70 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.93s
Memory: 476MB (+13MB)
UNKNOWN
Iteration Time: 7.59s
Iteration 20
Queue: [(16,80,0,True), (17,85,0,True)]
Grounded Until: 75
Expected Memory: 524.0MB
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
Grounding Time: 0.39s
Memory: 479MB (+3MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 21
Time : 101.077s (Solving: 89.87s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 101.008s
Choices : 2377079 (Domain: 2314344)
Conflicts : 145552 (Analyzed: 145549)
Restarts : 1702 (Average: 85.52 Last: 110)
Model-Level : 115.0
Problems : 21 (Average Length: 38.90 Splits: 0)
Lemmas : 145549 (Deleted: 129958)
Binary : 4745 (Ratio: 3.26%)
Ternary : 1465 (Ratio: 1.01%)
Conflict : 145549 (Average Length: 382.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 145549 (Average: 15.03 Max: 671 Sum: 2186977)
Executed : 145456 (Average: 15.01 Max: 671 Sum: 2184676 Ratio: 99.89%)
Bounded : 93 (Average: 24.74 Max: 82 Sum: 2301 Ratio: 0.11%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 410504 (Eliminated: 0 Frozen: 131302)
Constraints : 3016224 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 537MB
Max. Length : 75 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.88s
Memory: 498MB (+19MB)
UNKNOWN
Iteration Time: 7.58s
Iteration 21
Queue: [(17,85,0,True)]
Grounded Until: 80
Expected Memory: 546.0MB
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
Grounding Time: 0.38s
Memory: 498MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 22
Time : 106.918s (Solving: 94.94s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 106.852s
Choices : 2626934 (Domain: 2561282)
Conflicts : 153897 (Analyzed: 153894)
Restarts : 1802 (Average: 85.40 Last: 110)
Model-Level : 115.0
Problems : 22 (Average Length: 41.09 Splits: 0)
Lemmas : 153894 (Deleted: 136518)
Binary : 4815 (Ratio: 3.13%)
Ternary : 1475 (Ratio: 0.96%)
Conflict : 153894 (Average Length: 382.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 153894 (Average: 15.71 Max: 671 Sum: 2418322)
Executed : 153801 (Average: 15.70 Max: 671 Sum: 2416021 Ratio: 99.90%)
Bounded : 93 (Average: 24.74 Max: 82 Sum: 2301 Ratio: 0.10%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3217244 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.17s
Memory: 516MB (+18MB)
UNKNOWN
Iteration Time: 5.86s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 23
Time : 112.628s (Solving: 100.53s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 112.556s
Choices : 2666289 (Domain: 2600637)
Conflicts : 161814 (Analyzed: 161811)
Restarts : 1902 (Average: 85.07 Last: 110)
Model-Level : 115.0
Problems : 23 (Average Length: 43.09 Splits: 0)
Lemmas : 161811 (Deleted: 145241)
Binary : 4883 (Ratio: 3.02%)
Ternary : 1486 (Ratio: 0.92%)
Conflict : 161811 (Average Length: 393.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 161811 (Average: 15.14 Max: 671 Sum: 2450229)
Executed : 161716 (Average: 15.13 Max: 671 Sum: 2447754 Ratio: 99.90%)
Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 Ratio: 0.10%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3217244 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.66s
Memory: 517MB (+1MB)
UNKNOWN
Iteration Time: 5.71s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 24
Time : 117.957s (Solving: 105.77s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 117.888s
Choices : 2734738 (Domain: 2666366)
Conflicts : 171421 (Analyzed: 171418)
Restarts : 2002 (Average: 85.62 Last: 110)
Model-Level : 115.0
Problems : 24 (Average Length: 44.92 Splits: 0)
Lemmas : 171418 (Deleted: 154283)
Binary : 4986 (Ratio: 2.91%)
Ternary : 1509 (Ratio: 0.88%)
Conflict : 171418 (Average Length: 394.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 171418 (Average: 14.63 Max: 671 Sum: 2507902)
Executed : 171323 (Average: 14.62 Max: 671 Sum: 2505427 Ratio: 99.90%)
Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 Ratio: 0.10%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.30s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 5.33s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 25
Time : 123.006s (Solving: 110.73s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 122.940s
Choices : 2815441 (Domain: 2743992)
Conflicts : 180219 (Analyzed: 180216)
Restarts : 2102 (Average: 85.74 Last: 110)
Model-Level : 115.0
Problems : 25 (Average Length: 46.60 Splits: 0)
Lemmas : 180216 (Deleted: 163467)
Binary : 5101 (Ratio: 2.83%)
Ternary : 1532 (Ratio: 0.85%)
Conflict : 180216 (Average Length: 400.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 180216 (Average: 14.29 Max: 671 Sum: 2575753)
Executed : 180121 (Average: 14.28 Max: 671 Sum: 2573278 Ratio: 99.90%)
Bounded : 95 (Average: 26.05 Max: 87 Sum: 2475 Ratio: 0.10%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.02s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 5.05s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 26
Time : 127.926s (Solving: 115.54s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 127.864s
Choices : 2911485 (Domain: 2837581)
Conflicts : 188654 (Analyzed: 188651)
Restarts : 2202 (Average: 85.67 Last: 115)
Model-Level : 115.0
Problems : 26 (Average Length: 48.15 Splits: 0)
Lemmas : 188651 (Deleted: 170310)
Binary : 5219 (Ratio: 2.77%)
Ternary : 1536 (Ratio: 0.81%)
Conflict : 188651 (Average Length: 407.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 188651 (Average: 14.09 Max: 671 Sum: 2658216)
Executed : 188555 (Average: 14.08 Max: 671 Sum: 2655654 Ratio: 99.90%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.10%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214748 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.88s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 4.92s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 27
Time : 135.092s (Solving: 122.60s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 135.036s
Choices : 3062444 (Domain: 2980038)
Conflicts : 197708 (Analyzed: 197705)
Restarts : 2302 (Average: 85.88 Last: 115)
Model-Level : 115.0
Problems : 27 (Average Length: 49.59 Splits: 0)
Lemmas : 197705 (Deleted: 179876)
Binary : 5554 (Ratio: 2.81%)
Ternary : 1614 (Ratio: 0.82%)
Conflict : 197705 (Average Length: 427.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 197705 (Average: 14.10 Max: 671 Sum: 2788038)
Executed : 197609 (Average: 14.09 Max: 671 Sum: 2785476 Ratio: 99.91%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.09%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.13s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 7.17s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 28
Time : 140.467s (Solving: 127.87s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 140.408s
Choices : 3192312 (Domain: 3107985)
Conflicts : 206567 (Analyzed: 206564)
Restarts : 2402 (Average: 86.00 Last: 158)
Model-Level : 115.0
Problems : 28 (Average Length: 50.93 Splits: 0)
Lemmas : 206564 (Deleted: 188498)
Binary : 5755 (Ratio: 2.79%)
Ternary : 1656 (Ratio: 0.80%)
Conflict : 206564 (Average Length: 433.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 206564 (Average: 14.05 Max: 671 Sum: 2901654)
Executed : 206468 (Average: 14.03 Max: 671 Sum: 2899092 Ratio: 99.91%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.09%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.33s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 5.37s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 29
Time : 146.792s (Solving: 134.08s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 146.736s
Choices : 3370471 (Domain: 3279277)
Conflicts : 215484 (Analyzed: 215481)
Restarts : 2502 (Average: 86.12 Last: 170)
Model-Level : 115.0
Problems : 29 (Average Length: 52.17 Splits: 0)
Lemmas : 215481 (Deleted: 196820)
Binary : 6004 (Ratio: 2.79%)
Ternary : 1741 (Ratio: 0.81%)
Conflict : 215481 (Average Length: 441.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 215481 (Average: 14.20 Max: 671 Sum: 3059677)
Executed : 215385 (Average: 14.19 Max: 671 Sum: 3057115 Ratio: 99.92%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.08%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.29s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 6.33s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 30
Time : 152.466s (Solving: 139.67s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 152.412s
Choices : 3523031 (Domain: 3430715)
Conflicts : 224460 (Analyzed: 224457)
Restarts : 2602 (Average: 86.26 Last: 170)
Model-Level : 115.0
Problems : 30 (Average Length: 53.33 Splits: 0)
Lemmas : 224457 (Deleted: 205177)
Binary : 6136 (Ratio: 2.73%)
Ternary : 1758 (Ratio: 0.78%)
Conflict : 224457 (Average Length: 442.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 224457 (Average: 14.24 Max: 671 Sum: 3195230)
Executed : 224361 (Average: 14.22 Max: 671 Sum: 3192668 Ratio: 99.92%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.08%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 5.65s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 5.68s
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,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 31
Time : 159.614s (Solving: 146.73s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 159.564s
Choices : 3763227 (Domain: 3660922)
Conflicts : 233518 (Analyzed: 233515)
Restarts : 2702 (Average: 86.42 Last: 170)
Model-Level : 115.0
Problems : 31 (Average Length: 54.42 Splits: 0)
Lemmas : 233515 (Deleted: 213793)
Binary : 6399 (Ratio: 2.74%)
Ternary : 1833 (Ratio: 0.78%)
Conflict : 233515 (Average Length: 451.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 233515 (Average: 14.60 Max: 671 Sum: 3408356)
Executed : 233419 (Average: 14.58 Max: 671 Sum: 3405794 Ratio: 99.92%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.08%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.12s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 7.15s
Iteration 31
Queue: [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 32
Time : 165.808s (Solving: 152.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 165.764s
Choices : 3968183 (Domain: 3865263)
Conflicts : 242078 (Analyzed: 242075)
Restarts : 2802 (Average: 86.39 Last: 170)
Model-Level : 115.0
Problems : 32 (Average Length: 55.44 Splits: 0)
Lemmas : 242075 (Deleted: 220761)
Binary : 6554 (Ratio: 2.71%)
Ternary : 1852 (Ratio: 0.77%)
Conflict : 242075 (Average Length: 453.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 242075 (Average: 14.85 Max: 671 Sum: 3593818)
Executed : 241979 (Average: 14.84 Max: 671 Sum: 3591256 Ratio: 99.93%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.07%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.16s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 6.20s
Iteration 32
Queue: [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 33
Time : 172.520s (Solving: 159.43s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 172.480s
Choices : 4167486 (Domain: 4063718)
Conflicts : 250408 (Analyzed: 250405)
Restarts : 2902 (Average: 86.29 Last: 170)
Model-Level : 115.0
Problems : 33 (Average Length: 56.39 Splits: 0)
Lemmas : 250405 (Deleted: 228428)
Binary : 6708 (Ratio: 2.68%)
Ternary : 1869 (Ratio: 0.75%)
Conflict : 250405 (Average Length: 456.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 250405 (Average: 15.07 Max: 671 Sum: 3774797)
Executed : 250309 (Average: 15.06 Max: 671 Sum: 3772235 Ratio: 99.93%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.07%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.68s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 6.72s
Iteration 33
Queue: [(15,75,1,True), (16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 34
Time : 180.578s (Solving: 167.39s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 180.544s
Choices : 4486419 (Domain: 4380037)
Conflicts : 259607 (Analyzed: 259604)
Restarts : 3002 (Average: 86.48 Last: 170)
Model-Level : 115.0
Problems : 34 (Average Length: 57.29 Splits: 0)
Lemmas : 259604 (Deleted: 238658)
Binary : 6852 (Ratio: 2.64%)
Ternary : 1890 (Ratio: 0.73%)
Conflict : 259604 (Average Length: 464.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 259604 (Average: 15.67 Max: 671 Sum: 4067138)
Executed : 259508 (Average: 15.66 Max: 671 Sum: 4064576 Ratio: 99.94%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.06%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.02s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 8.06s
Iteration 34
Queue: [(16,80,1,True), (17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 35
Time : 189.102s (Solving: 175.83s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 189.072s
Choices : 4720405 (Domain: 4608522)
Conflicts : 268308 (Analyzed: 268305)
Restarts : 3102 (Average: 86.49 Last: 170)
Model-Level : 115.0
Problems : 35 (Average Length: 58.14 Splits: 0)
Lemmas : 268305 (Deleted: 247041)
Binary : 7140 (Ratio: 2.66%)
Ternary : 1925 (Ratio: 0.72%)
Conflict : 268305 (Average Length: 488.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 268305 (Average: 15.92 Max: 671 Sum: 4271683)
Executed : 268209 (Average: 15.91 Max: 671 Sum: 4269121 Ratio: 99.94%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.06%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.50s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 8.53s
Iteration 35
Queue: [(17,85,1,True), (18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 36
Time : 197.636s (Solving: 184.27s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 197.608s
Choices : 4994690 (Domain: 4881787)
Conflicts : 277279 (Analyzed: 277276)
Restarts : 3202 (Average: 86.59 Last: 170)
Model-Level : 115.0
Problems : 36 (Average Length: 58.94 Splits: 0)
Lemmas : 277276 (Deleted: 255140)
Binary : 7259 (Ratio: 2.62%)
Ternary : 1953 (Ratio: 0.70%)
Conflict : 277276 (Average Length: 492.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 277276 (Average: 16.31 Max: 671 Sum: 4521069)
Executed : 277180 (Average: 16.30 Max: 671 Sum: 4518507 Ratio: 99.94%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.06%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 436900 (Eliminated: 0 Frozen: 139842)
Constraints : 3214722 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 558MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.51s
Memory: 517MB (+0MB)
UNKNOWN
Iteration Time: 8.54s
Iteration 36
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Expected Memory: 565.0MB
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
Grounding Time: 0.37s
Memory: 517MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 37
Time : 208.934s (Solving: 194.79s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 208.908s
Choices : 5343023 (Domain: 5228839)
Conflicts : 287148 (Analyzed: 287145)
Restarts : 3302 (Average: 86.96 Last: 170)
Model-Level : 115.0
Problems : 37 (Average Length: 59.84 Splits: 0)
Lemmas : 287145 (Deleted: 263928)
Binary : 7392 (Ratio: 2.57%)
Ternary : 1987 (Ratio: 0.69%)
Conflict : 287145 (Average Length: 506.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 287145 (Average: 16.85 Max: 671 Sum: 4839070)
Executed : 287049 (Average: 16.84 Max: 671 Sum: 4836508 Ratio: 99.95%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.05%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 463296 (Eliminated: 0 Frozen: 148382)
Constraints : 3415792 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 580MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.62s
Memory: 534MB (+17MB)
UNKNOWN
Iteration Time: 11.31s
Iteration 37
Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 90
Expected Memory: 582.0MB
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
Grounding Time: 0.39s
Memory: 534MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 38
Time : 218.549s (Solving: 203.58s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 218.528s
Choices : 5669012 (Domain: 5553843)
Conflicts : 296063 (Analyzed: 296060)
Restarts : 3402 (Average: 87.03 Last: 170)
Model-Level : 115.0
Problems : 38 (Average Length: 60.82 Splits: 0)
Lemmas : 296060 (Deleted: 273205)
Binary : 7498 (Ratio: 2.53%)
Ternary : 2002 (Ratio: 0.68%)
Conflict : 296060 (Average Length: 512.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 296060 (Average: 17.35 Max: 671 Sum: 5136959)
Executed : 295964 (Average: 17.34 Max: 671 Sum: 5134397 Ratio: 99.95%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.05%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 489692 (Eliminated: 0 Frozen: 156922)
Constraints : 3616862 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 600MB
Max. Length : 90 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.89s
Memory: 590MB (+56MB)
UNKNOWN
Iteration Time: 9.63s
Iteration 38
Queue: [(20,100,0,True), (21,105,0,True)]
Grounded Until: 95
Expected Memory: 646.0MB
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
Grounding Time: 0.39s
Memory: 590MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 39
Time : 229.487s (Solving: 213.68s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 229.468s
Choices : 6023692 (Domain: 5903315)
Conflicts : 304951 (Analyzed: 304948)
Restarts : 3502 (Average: 87.08 Last: 170)
Model-Level : 115.0
Problems : 39 (Average Length: 61.87 Splits: 0)
Lemmas : 304948 (Deleted: 281699)
Binary : 7742 (Ratio: 2.54%)
Ternary : 2044 (Ratio: 0.67%)
Conflict : 304948 (Average Length: 532.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 304948 (Average: 17.88 Max: 804 Sum: 5451933)
Executed : 304852 (Average: 17.87 Max: 804 Sum: 5449371 Ratio: 99.95%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.05%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 516088 (Eliminated: 0 Frozen: 165462)
Constraints : 3817932 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 653MB
Max. Length : 95 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.21s
Memory: 593MB (+3MB)
UNKNOWN
Iteration Time: 10.95s
Iteration 39
Queue: [(21,105,0,True)]
Grounded Until: 100
Expected Memory: 649.0MB
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
Grounding Time: 0.39s
Memory: 593MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 40
Time : 240.042s (Solving: 223.38s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 240.024s
Choices : 6379244 (Domain: 6257912)
Conflicts : 314000 (Analyzed: 313997)
Restarts : 3602 (Average: 87.17 Last: 170)
Model-Level : 115.0
Problems : 40 (Average Length: 63.00 Splits: 0)
Lemmas : 313997 (Deleted: 290078)
Binary : 7969 (Ratio: 2.54%)
Ternary : 2063 (Ratio: 0.66%)
Conflict : 313997 (Average Length: 537.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 313997 (Average: 18.40 Max: 804 Sum: 5776888)
Executed : 313901 (Average: 18.39 Max: 804 Sum: 5774326 Ratio: 99.96%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 100 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.80s
Memory: 601MB (+8MB)
UNKNOWN
Iteration Time: 10.56s
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,2,False), (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 : 243.410s (Solving: 226.62s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 243.396s
Choices : 6430841 (Domain: 6309509)
Conflicts : 321968 (Analyzed: 321965)
Restarts : 3702 (Average: 86.97 Last: 170)
Model-Level : 115.0
Problems : 41 (Average Length: 64.07 Splits: 0)
Lemmas : 321965 (Deleted: 296652)
Binary : 8159 (Ratio: 2.53%)
Ternary : 2097 (Ratio: 0.65%)
Conflict : 321965 (Average Length: 532.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 321965 (Average: 18.09 Max: 804 Sum: 5822997)
Executed : 321869 (Average: 18.08 Max: 804 Sum: 5820435 Ratio: 99.96%)
Bounded : 96 (Average: 26.69 Max: 87 Sum: 2562 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.32s
Memory: 607MB (+6MB)
UNKNOWN
Iteration Time: 3.37s
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,2,False), (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 : 251.218s (Solving: 234.30s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 251.208s
Choices : 6495553 (Domain: 6374179)
Conflicts : 331081 (Analyzed: 331078)
Restarts : 3802 (Average: 87.08 Last: 170)
Model-Level : 115.0
Problems : 42 (Average Length: 65.10 Splits: 0)
Lemmas : 331078 (Deleted: 306175)
Binary : 8297 (Ratio: 2.51%)
Ternary : 2135 (Ratio: 0.64%)
Conflict : 331078 (Average Length: 542.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 331078 (Average: 17.75 Max: 804 Sum: 5876081)
Executed : 330981 (Average: 17.74 Max: 804 Sum: 5873416 Ratio: 99.95%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.05%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.77s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.81s
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,2,False), (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 : 259.001s (Solving: 241.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 258.996s
Choices : 6594146 (Domain: 6472016)
Conflicts : 340237 (Analyzed: 340234)
Restarts : 3902 (Average: 87.19 Last: 170)
Model-Level : 115.0
Problems : 43 (Average Length: 66.07 Splits: 0)
Lemmas : 340234 (Deleted: 315492)
Binary : 8513 (Ratio: 2.50%)
Ternary : 2196 (Ratio: 0.65%)
Conflict : 340234 (Average Length: 558.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 340234 (Average: 17.50 Max: 804 Sum: 5954361)
Executed : 340137 (Average: 17.49 Max: 804 Sum: 5951696 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.74s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.79s
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,2,False), (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 : 266.714s (Solving: 249.54s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 266.712s
Choices : 6710814 (Domain: 6584758)
Conflicts : 349303 (Analyzed: 349300)
Restarts : 4002 (Average: 87.28 Last: 170)
Model-Level : 115.0
Problems : 44 (Average Length: 67.00 Splits: 0)
Lemmas : 349300 (Deleted: 323636)
Binary : 8739 (Ratio: 2.50%)
Ternary : 2291 (Ratio: 0.66%)
Conflict : 349300 (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 : 349300 (Average: 17.32 Max: 804 Sum: 6050827)
Executed : 349203 (Average: 17.32 Max: 804 Sum: 6048162 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.67s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.72s
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,2,False), (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 : 274.357s (Solving: 257.07s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 274.356s
Choices : 6830088 (Domain: 6703845)
Conflicts : 358717 (Analyzed: 358714)
Restarts : 4102 (Average: 87.45 Last: 170)
Model-Level : 115.0
Problems : 45 (Average Length: 67.89 Splits: 0)
Lemmas : 358714 (Deleted: 332178)
Binary : 8867 (Ratio: 2.47%)
Ternary : 2311 (Ratio: 0.64%)
Conflict : 358714 (Average Length: 566.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 358714 (Average: 17.15 Max: 804 Sum: 6150549)
Executed : 358617 (Average: 17.14 Max: 804 Sum: 6147884 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.61s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.65s
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,2,False), (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 : 281.607s (Solving: 264.20s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 281.612s
Choices : 6925774 (Domain: 6799473)
Conflicts : 368019 (Analyzed: 368016)
Restarts : 4202 (Average: 87.58 Last: 170)
Model-Level : 115.0
Problems : 46 (Average Length: 68.74 Splits: 0)
Lemmas : 368016 (Deleted: 341260)
Binary : 8922 (Ratio: 2.42%)
Ternary : 2321 (Ratio: 0.63%)
Conflict : 368016 (Average Length: 570.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 368016 (Average: 16.92 Max: 804 Sum: 6226794)
Executed : 367919 (Average: 16.91 Max: 804 Sum: 6224129 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.21s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.26s
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,2,False), (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 : 289.739s (Solving: 272.19s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 289.748s
Choices : 7038639 (Domain: 6911918)
Conflicts : 377264 (Analyzed: 377261)
Restarts : 4302 (Average: 87.69 Last: 170)
Model-Level : 115.0
Problems : 47 (Average Length: 69.55 Splits: 0)
Lemmas : 377261 (Deleted: 350265)
Binary : 8987 (Ratio: 2.38%)
Ternary : 2340 (Ratio: 0.62%)
Conflict : 377261 (Average Length: 574.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 377261 (Average: 16.75 Max: 804 Sum: 6318417)
Executed : 377164 (Average: 16.74 Max: 804 Sum: 6315752 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.08s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 8.14s
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,2,False), (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 : 297.757s (Solving: 280.06s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 297.768s
Choices : 7160939 (Domain: 7033822)
Conflicts : 386539 (Analyzed: 386536)
Restarts : 4402 (Average: 87.81 Last: 170)
Model-Level : 115.0
Problems : 48 (Average Length: 70.33 Splits: 0)
Lemmas : 386536 (Deleted: 359257)
Binary : 9080 (Ratio: 2.35%)
Ternary : 2363 (Ratio: 0.61%)
Conflict : 386536 (Average Length: 580.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 386536 (Average: 16.60 Max: 804 Sum: 6417714)
Executed : 386439 (Average: 16.60 Max: 804 Sum: 6415049 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.97s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 8.02s
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,2,False), (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 : 305.694s (Solving: 287.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 305.708s
Choices : 7303106 (Domain: 7175841)
Conflicts : 395708 (Analyzed: 395705)
Restarts : 4502 (Average: 87.90 Last: 170)
Model-Level : 115.0
Problems : 49 (Average Length: 71.08 Splits: 0)
Lemmas : 395705 (Deleted: 368259)
Binary : 9116 (Ratio: 2.30%)
Ternary : 2370 (Ratio: 0.60%)
Conflict : 395705 (Average Length: 583.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 395705 (Average: 16.52 Max: 804 Sum: 6537132)
Executed : 395608 (Average: 16.51 Max: 804 Sum: 6534467 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.90s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 7.94s
Iteration 49
Queue: [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,2,False), (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 : 313.828s (Solving: 295.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 313.844s
Choices : 7504335 (Domain: 7375013)
Conflicts : 404707 (Analyzed: 404704)
Restarts : 4602 (Average: 87.94 Last: 170)
Model-Level : 115.0
Problems : 50 (Average Length: 71.80 Splits: 0)
Lemmas : 404704 (Deleted: 377119)
Binary : 9336 (Ratio: 2.31%)
Ternary : 2454 (Ratio: 0.61%)
Conflict : 404704 (Average Length: 585.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 404704 (Average: 16.58 Max: 804 Sum: 6709035)
Executed : 404607 (Average: 16.57 Max: 804 Sum: 6706370 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.09s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 8.14s
Iteration 50
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 : 51
Time : 322.691s (Solving: 304.63s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 322.700s
Choices : 7621989 (Domain: 7492407)
Conflicts : 413223 (Analyzed: 413220)
Restarts : 4702 (Average: 87.88 Last: 170)
Model-Level : 115.0
Problems : 51 (Average Length: 72.49 Splits: 0)
Lemmas : 413220 (Deleted: 384332)
Binary : 9393 (Ratio: 2.27%)
Ternary : 2460 (Ratio: 0.60%)
Conflict : 413220 (Average Length: 597.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 413220 (Average: 16.45 Max: 804 Sum: 6795908)
Executed : 413123 (Average: 16.44 Max: 804 Sum: 6793243 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.81s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 8.86s
Iteration 51
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 : 52
Time : 331.604s (Solving: 313.40s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 331.616s
Choices : 7799647 (Domain: 7669964)
Conflicts : 422499 (Analyzed: 422496)
Restarts : 4802 (Average: 87.98 Last: 170)
Model-Level : 115.0
Problems : 52 (Average Length: 73.15 Splits: 0)
Lemmas : 422496 (Deleted: 394032)
Binary : 9435 (Ratio: 2.23%)
Ternary : 2470 (Ratio: 0.58%)
Conflict : 422496 (Average Length: 599.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 422496 (Average: 16.43 Max: 804 Sum: 6943636)
Executed : 422399 (Average: 16.43 Max: 804 Sum: 6940971 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.86s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 8.92s
Iteration 52
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 : 53
Time : 341.232s (Solving: 322.92s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 341.248s
Choices : 7985443 (Domain: 7854970)
Conflicts : 431998 (Analyzed: 431995)
Restarts : 4902 (Average: 88.13 Last: 170)
Model-Level : 115.0
Problems : 53 (Average Length: 73.79 Splits: 0)
Lemmas : 431995 (Deleted: 403120)
Binary : 9499 (Ratio: 2.20%)
Ternary : 2479 (Ratio: 0.57%)
Conflict : 431995 (Average Length: 604.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 431995 (Average: 16.42 Max: 804 Sum: 7094388)
Executed : 431898 (Average: 16.42 Max: 804 Sum: 7091723 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.59s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 9.64s
Iteration 53
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 : 54
Time : 350.764s (Solving: 332.33s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 350.784s
Choices : 8163807 (Domain: 8032808)
Conflicts : 441246 (Analyzed: 441243)
Restarts : 5002 (Average: 88.21 Last: 170)
Model-Level : 115.0
Problems : 54 (Average Length: 74.41 Splits: 0)
Lemmas : 441243 (Deleted: 412313)
Binary : 9593 (Ratio: 2.17%)
Ternary : 2505 (Ratio: 0.57%)
Conflict : 441243 (Average Length: 606.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 441243 (Average: 16.41 Max: 804 Sum: 7239497)
Executed : 441146 (Average: 16.40 Max: 804 Sum: 7236832 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 542484 (Eliminated: 0 Frozen: 174002)
Constraints : 4019002 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 664MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.49s
Memory: 607MB (+0MB)
UNKNOWN
Iteration Time: 9.54s
Iteration 54
Queue: [(22,110,0,True), (23,115,0,True)]
Grounded Until: 105
Expected Memory: 663.0MB
Grounding... [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])]
Grounding Time: 0.38s
Memory: 607MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 55
Time : 360.243s (Solving: 340.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 360.268s
Choices : 8299406 (Domain: 8168390)
Conflicts : 450657 (Analyzed: 450654)
Restarts : 5102 (Average: 88.33 Last: 170)
Model-Level : 115.0
Problems : 55 (Average Length: 75.09 Splits: 0)
Lemmas : 450654 (Deleted: 421286)
Binary : 9645 (Ratio: 2.14%)
Ternary : 2509 (Ratio: 0.56%)
Conflict : 450654 (Average Length: 609.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 450654 (Average: 16.30 Max: 804 Sum: 7343702)
Executed : 450557 (Average: 16.29 Max: 804 Sum: 7341037 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 568880 (Eliminated: 0 Frozen: 182542)
Constraints : 4220072 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 680MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.74s
Memory: 621MB (+14MB)
UNKNOWN
Iteration Time: 9.49s
Iteration 55
Queue: [(23,115,0,True)]
Grounded Until: 110
Expected Memory: 677.0MB
Grounding... [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])]
Grounding Time: 0.38s
Memory: 621MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 56
Time : 371.728s (Solving: 351.59s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 371.760s
Choices : 8452358 (Domain: 8321303)
Conflicts : 460582 (Analyzed: 460579)
Restarts : 5202 (Average: 88.54 Last: 170)
Model-Level : 115.0
Problems : 56 (Average Length: 75.84 Splits: 0)
Lemmas : 460579 (Deleted: 430544)
Binary : 9673 (Ratio: 2.10%)
Ternary : 2521 (Ratio: 0.55%)
Conflict : 460579 (Average Length: 613.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 460579 (Average: 16.20 Max: 804 Sum: 7460145)
Executed : 460482 (Average: 16.19 Max: 804 Sum: 7457480 Ratio: 99.96%)
Bounded : 97 (Average: 27.47 Max: 103 Sum: 2665 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421142 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 110 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.74s
Memory: 637MB (+16MB)
UNKNOWN
Iteration Time: 11.50s
Iteration 56
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 : 57
Time : 374.767s (Solving: 354.48s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 374.796s
Choices : 8496233 (Domain: 8365178)
Conflicts : 468049 (Analyzed: 468046)
Restarts : 5302 (Average: 88.28 Last: 170)
Model-Level : 115.0
Problems : 57 (Average Length: 76.56 Splits: 0)
Lemmas : 468046 (Deleted: 438008)
Binary : 9722 (Ratio: 2.08%)
Ternary : 2533 (Ratio: 0.54%)
Conflict : 468046 (Average Length: 607.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 468046 (Average: 16.02 Max: 804 Sum: 7496619)
Executed : 467948 (Average: 16.01 Max: 804 Sum: 7493837 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421142 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 2.99s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 3.04s
Iteration 57
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 : 58
Time : 383.726s (Solving: 363.31s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 383.760s
Choices : 8542421 (Domain: 8411366)
Conflicts : 476684 (Analyzed: 476681)
Restarts : 5402 (Average: 88.24 Last: 170)
Model-Level : 115.0
Problems : 58 (Average Length: 77.26 Splits: 0)
Lemmas : 476681 (Deleted: 447362)
Binary : 9760 (Ratio: 2.05%)
Ternary : 2544 (Ratio: 0.53%)
Conflict : 476681 (Average Length: 617.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 476681 (Average: 15.80 Max: 804 Sum: 7529934)
Executed : 476583 (Average: 15.79 Max: 804 Sum: 7527152 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.92s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.97s
Iteration 58
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 : 59
Time : 391.228s (Solving: 370.68s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 391.264s
Choices : 8618700 (Domain: 8487645)
Conflicts : 485737 (Analyzed: 485734)
Restarts : 5502 (Average: 88.28 Last: 170)
Model-Level : 115.0
Problems : 59 (Average Length: 77.93 Splits: 0)
Lemmas : 485734 (Deleted: 455742)
Binary : 9883 (Ratio: 2.03%)
Ternary : 2566 (Ratio: 0.53%)
Conflict : 485734 (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 : 485734 (Average: 15.62 Max: 804 Sum: 7587479)
Executed : 485636 (Average: 15.61 Max: 804 Sum: 7584697 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.46s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.51s
Iteration 59
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 : 60
Time : 398.492s (Solving: 377.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 398.532s
Choices : 8689250 (Domain: 8557293)
Conflicts : 494574 (Analyzed: 494571)
Restarts : 5602 (Average: 88.28 Last: 170)
Model-Level : 115.0
Problems : 60 (Average Length: 78.58 Splits: 0)
Lemmas : 494571 (Deleted: 464538)
Binary : 9965 (Ratio: 2.01%)
Ternary : 2573 (Ratio: 0.52%)
Conflict : 494571 (Average Length: 625.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 494571 (Average: 15.44 Max: 804 Sum: 7637879)
Executed : 494473 (Average: 15.44 Max: 804 Sum: 7635097 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.23s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.27s
Iteration 60
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 : 61
Time : 405.756s (Solving: 384.97s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 405.800s
Choices : 8797588 (Domain: 8660669)
Conflicts : 503822 (Analyzed: 503819)
Restarts : 5702 (Average: 88.36 Last: 170)
Model-Level : 115.0
Problems : 61 (Average Length: 79.21 Splits: 0)
Lemmas : 503819 (Deleted: 472749)
Binary : 10220 (Ratio: 2.03%)
Ternary : 2595 (Ratio: 0.52%)
Conflict : 503819 (Average Length: 627.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 503819 (Average: 15.32 Max: 804 Sum: 7718391)
Executed : 503721 (Average: 15.31 Max: 804 Sum: 7715609 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.23s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.27s
Iteration 61
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 : 62
Time : 413.314s (Solving: 392.40s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 413.360s
Choices : 8880447 (Domain: 8743518)
Conflicts : 512942 (Analyzed: 512939)
Restarts : 5802 (Average: 88.41 Last: 170)
Model-Level : 115.0
Problems : 62 (Average Length: 79.82 Splits: 0)
Lemmas : 512939 (Deleted: 481710)
Binary : 10279 (Ratio: 2.00%)
Ternary : 2607 (Ratio: 0.51%)
Conflict : 512939 (Average Length: 632.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 512939 (Average: 15.17 Max: 804 Sum: 7780418)
Executed : 512841 (Average: 15.16 Max: 804 Sum: 7777636 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.52s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.56s
Iteration 62
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 : 63
Time : 420.951s (Solving: 399.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 421.000s
Choices : 8967467 (Domain: 8830526)
Conflicts : 522172 (Analyzed: 522169)
Restarts : 5902 (Average: 88.47 Last: 170)
Model-Level : 115.0
Problems : 63 (Average Length: 80.41 Splits: 0)
Lemmas : 522169 (Deleted: 490655)
Binary : 10305 (Ratio: 1.97%)
Ternary : 2609 (Ratio: 0.50%)
Conflict : 522169 (Average Length: 632.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 522169 (Average: 15.03 Max: 804 Sum: 7846405)
Executed : 522071 (Average: 15.02 Max: 804 Sum: 7843623 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.58s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 7.64s
Iteration 63
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 : 64
Time : 429.223s (Solving: 408.02s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 429.276s
Choices : 9059058 (Domain: 8922095)
Conflicts : 531500 (Analyzed: 531497)
Restarts : 6002 (Average: 88.55 Last: 170)
Model-Level : 115.0
Problems : 64 (Average Length: 80.98 Splits: 0)
Lemmas : 531497 (Deleted: 499685)
Binary : 10323 (Ratio: 1.94%)
Ternary : 2611 (Ratio: 0.49%)
Conflict : 531497 (Average Length: 634.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 531497 (Average: 14.89 Max: 804 Sum: 7913250)
Executed : 531399 (Average: 14.88 Max: 804 Sum: 7910468 Ratio: 99.96%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.22s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.28s
Iteration 64
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 : 65
Time : 437.536s (Solving: 416.21s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 437.592s
Choices : 9153270 (Domain: 9016300)
Conflicts : 540952 (Analyzed: 540949)
Restarts : 6102 (Average: 88.65 Last: 172)
Model-Level : 115.0
Problems : 65 (Average Length: 81.54 Splits: 0)
Lemmas : 540949 (Deleted: 508794)
Binary : 10347 (Ratio: 1.91%)
Ternary : 2614 (Ratio: 0.48%)
Conflict : 540949 (Average Length: 636.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 540949 (Average: 14.75 Max: 804 Sum: 7981558)
Executed : 540851 (Average: 14.75 Max: 804 Sum: 7978776 Ratio: 99.97%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.27s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.32s
Iteration 65
Queue: [(22,110,1,True), (23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 66
Time : 447.483s (Solving: 426.01s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 447.540s
Choices : 9264003 (Domain: 9126961)
Conflicts : 550781 (Analyzed: 550778)
Restarts : 6202 (Average: 88.81 Last: 172)
Model-Level : 115.0
Problems : 66 (Average Length: 82.08 Splits: 0)
Lemmas : 550778 (Deleted: 518071)
Binary : 10367 (Ratio: 1.88%)
Ternary : 2621 (Ratio: 0.48%)
Conflict : 550778 (Average Length: 640.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 550778 (Average: 14.63 Max: 804 Sum: 8058202)
Executed : 550680 (Average: 14.63 Max: 804 Sum: 8055420 Ratio: 99.97%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.90s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 9.95s
Iteration 66
Queue: [(23,115,1,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 67
Time : 456.370s (Solving: 434.76s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 456.432s
Choices : 9380536 (Domain: 9243485)
Conflicts : 560063 (Analyzed: 560060)
Restarts : 6302 (Average: 88.87 Last: 172)
Model-Level : 115.0
Problems : 67 (Average Length: 82.60 Splits: 0)
Lemmas : 560060 (Deleted: 527755)
Binary : 10416 (Ratio: 1.86%)
Ternary : 2622 (Ratio: 0.47%)
Conflict : 560060 (Average Length: 642.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 560060 (Average: 14.54 Max: 804 Sum: 8141773)
Executed : 559962 (Average: 14.53 Max: 804 Sum: 8138991 Ratio: 99.97%)
Bounded : 98 (Average: 28.39 Max: 117 Sum: 2782 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.84s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 8.89s
Iteration 67
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 : 68
Time : 459.552s (Solving: 437.79s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 459.616s
Choices : 9434154 (Domain: 9297103)
Conflicts : 567639 (Analyzed: 567636)
Restarts : 6402 (Average: 88.67 Last: 172)
Model-Level : 115.0
Problems : 68 (Average Length: 83.10 Splits: 0)
Lemmas : 567636 (Deleted: 534523)
Binary : 10500 (Ratio: 1.85%)
Ternary : 2643 (Ratio: 0.47%)
Conflict : 567636 (Average Length: 637.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 567636 (Average: 14.43 Max: 804 Sum: 8190438)
Executed : 567535 (Average: 14.42 Max: 804 Sum: 8187305 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421128 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 706MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.13s
Memory: 637MB (+0MB)
UNKNOWN
Iteration Time: 3.19s
Iteration 68
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 : 69
Time : 470.051s (Solving: 448.16s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 470.116s
Choices : 9482131 (Domain: 9345080)
Conflicts : 576664 (Analyzed: 576661)
Restarts : 6502 (Average: 88.69 Last: 172)
Model-Level : 115.0
Problems : 69 (Average Length: 83.59 Splits: 0)
Lemmas : 576661 (Deleted: 543859)
Binary : 10552 (Ratio: 1.83%)
Ternary : 2651 (Ratio: 0.46%)
Conflict : 576661 (Average Length: 650.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 576661 (Average: 14.26 Max: 804 Sum: 8224004)
Executed : 576560 (Average: 14.26 Max: 804 Sum: 8220871 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.45s
Memory: 701MB (+64MB)
UNKNOWN
Iteration Time: 10.51s
Iteration 69
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 : 70
Time : 476.594s (Solving: 454.55s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 476.660s
Choices : 9557144 (Domain: 9420093)
Conflicts : 585502 (Analyzed: 585499)
Restarts : 6602 (Average: 88.69 Last: 172)
Model-Level : 115.0
Problems : 70 (Average Length: 84.07 Splits: 0)
Lemmas : 585499 (Deleted: 552610)
Binary : 10648 (Ratio: 1.82%)
Ternary : 2662 (Ratio: 0.45%)
Conflict : 585499 (Average Length: 653.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 585499 (Average: 14.14 Max: 804 Sum: 8280709)
Executed : 585398 (Average: 14.14 Max: 804 Sum: 8277576 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.49s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 6.55s
Iteration 70
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 : 71
Time : 484.082s (Solving: 461.92s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 484.152s
Choices : 9635294 (Domain: 9497946)
Conflicts : 595789 (Analyzed: 595786)
Restarts : 6702 (Average: 88.90 Last: 172)
Model-Level : 115.0
Problems : 71 (Average Length: 84.54 Splits: 0)
Lemmas : 595786 (Deleted: 561289)
Binary : 10713 (Ratio: 1.80%)
Ternary : 2669 (Ratio: 0.45%)
Conflict : 595786 (Average Length: 653.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 595786 (Average: 14.00 Max: 804 Sum: 8340737)
Executed : 595685 (Average: 13.99 Max: 804 Sum: 8337604 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.45s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.49s
Iteration 71
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 : 72
Time : 491.756s (Solving: 469.45s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 491.828s
Choices : 9707894 (Domain: 9570482)
Conflicts : 605018 (Analyzed: 605015)
Restarts : 6802 (Average: 88.95 Last: 172)
Model-Level : 115.0
Problems : 72 (Average Length: 84.99 Splits: 0)
Lemmas : 605015 (Deleted: 571311)
Binary : 10761 (Ratio: 1.78%)
Ternary : 2675 (Ratio: 0.44%)
Conflict : 605015 (Average Length: 657.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 605015 (Average: 13.87 Max: 804 Sum: 8391385)
Executed : 604914 (Average: 13.86 Max: 804 Sum: 8388252 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.63s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.68s
Iteration 72
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 : 73
Time : 499.479s (Solving: 477.02s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 499.552s
Choices : 9782772 (Domain: 9645348)
Conflicts : 615176 (Analyzed: 615173)
Restarts : 6902 (Average: 89.13 Last: 172)
Model-Level : 115.0
Problems : 73 (Average Length: 85.42 Splits: 0)
Lemmas : 615173 (Deleted: 580367)
Binary : 10788 (Ratio: 1.75%)
Ternary : 2675 (Ratio: 0.43%)
Conflict : 615173 (Average Length: 657.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 615173 (Average: 13.73 Max: 804 Sum: 8445699)
Executed : 615072 (Average: 13.72 Max: 804 Sum: 8442566 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.67s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.73s
Iteration 73
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 : 74
Time : 507.094s (Solving: 484.51s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 507.168s
Choices : 9855687 (Domain: 9718221)
Conflicts : 624144 (Analyzed: 624141)
Restarts : 7002 (Average: 89.14 Last: 172)
Model-Level : 115.0
Problems : 74 (Average Length: 85.85 Splits: 0)
Lemmas : 624141 (Deleted: 590302)
Binary : 10814 (Ratio: 1.73%)
Ternary : 2685 (Ratio: 0.43%)
Conflict : 624141 (Average Length: 660.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 624141 (Average: 13.61 Max: 804 Sum: 8495389)
Executed : 624040 (Average: 13.61 Max: 804 Sum: 8492256 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.58s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.62s
Iteration 74
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 : 75
Time : 514.984s (Solving: 492.28s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 515.060s
Choices : 9923181 (Domain: 9785715)
Conflicts : 633437 (Analyzed: 633434)
Restarts : 7102 (Average: 89.19 Last: 172)
Model-Level : 115.0
Problems : 75 (Average Length: 86.27 Splits: 0)
Lemmas : 633434 (Deleted: 599117)
Binary : 10832 (Ratio: 1.71%)
Ternary : 2689 (Ratio: 0.42%)
Conflict : 633434 (Average Length: 663.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 633434 (Average: 13.48 Max: 804 Sum: 8537864)
Executed : 633333 (Average: 13.47 Max: 804 Sum: 8534731 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.85s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.90s
Iteration 75
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 : 76
Time : 523.361s (Solving: 500.52s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 523.440s
Choices : 10023275 (Domain: 9885660)
Conflicts : 643207 (Analyzed: 643204)
Restarts : 7202 (Average: 89.31 Last: 172)
Model-Level : 115.0
Problems : 76 (Average Length: 86.67 Splits: 0)
Lemmas : 643204 (Deleted: 608177)
Binary : 10876 (Ratio: 1.69%)
Ternary : 2695 (Ratio: 0.42%)
Conflict : 643204 (Average Length: 665.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 643204 (Average: 13.38 Max: 804 Sum: 8609242)
Executed : 643103 (Average: 13.38 Max: 804 Sum: 8606109 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.33s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.38s
Iteration 76
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 : 77
Time : 531.762s (Solving: 508.78s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 531.844s
Choices : 10107051 (Domain: 9969435)
Conflicts : 652228 (Analyzed: 652225)
Restarts : 7302 (Average: 89.32 Last: 172)
Model-Level : 115.0
Problems : 77 (Average Length: 87.06 Splits: 0)
Lemmas : 652225 (Deleted: 617783)
Binary : 10887 (Ratio: 1.67%)
Ternary : 2699 (Ratio: 0.41%)
Conflict : 652225 (Average Length: 669.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 652225 (Average: 13.29 Max: 804 Sum: 8665447)
Executed : 652124 (Average: 13.28 Max: 804 Sum: 8662314 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.35s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.41s
Iteration 77
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 : 78
Time : 534.891s (Solving: 511.78s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 534.972s
Choices : 10158302 (Domain: 10020686)
Conflicts : 659798 (Analyzed: 659795)
Restarts : 7402 (Average: 89.14 Last: 172)
Model-Level : 115.0
Problems : 78 (Average Length: 87.45 Splits: 0)
Lemmas : 659795 (Deleted: 624374)
Binary : 10965 (Ratio: 1.66%)
Ternary : 2706 (Ratio: 0.41%)
Conflict : 659795 (Average Length: 663.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 659795 (Average: 13.19 Max: 804 Sum: 8702473)
Executed : 659694 (Average: 13.18 Max: 804 Sum: 8699340 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.08s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 3.13s
Iteration 78
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 : 79
Time : 544.334s (Solving: 521.10s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 544.420s
Choices : 10197256 (Domain: 10059640)
Conflicts : 667894 (Analyzed: 667891)
Restarts : 7502 (Average: 89.03 Last: 172)
Model-Level : 115.0
Problems : 79 (Average Length: 87.82 Splits: 0)
Lemmas : 667891 (Deleted: 631853)
Binary : 10983 (Ratio: 1.64%)
Ternary : 2717 (Ratio: 0.41%)
Conflict : 667891 (Average Length: 675.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 667891 (Average: 13.07 Max: 804 Sum: 8731224)
Executed : 667790 (Average: 13.07 Max: 804 Sum: 8728091 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.41s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 9.45s
Iteration 79
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 : 80
Time : 552.480s (Solving: 529.09s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 552.568s
Choices : 10271487 (Domain: 10133871)
Conflicts : 676239 (Analyzed: 676236)
Restarts : 7602 (Average: 88.96 Last: 172)
Model-Level : 115.0
Problems : 80 (Average Length: 88.19 Splits: 0)
Lemmas : 676236 (Deleted: 639948)
Binary : 11038 (Ratio: 1.63%)
Ternary : 2728 (Ratio: 0.40%)
Conflict : 676236 (Average Length: 679.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 676236 (Average: 13.00 Max: 804 Sum: 8788265)
Executed : 676135 (Average: 12.99 Max: 804 Sum: 8785132 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.08s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.15s
Iteration 80
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 : 81
Time : 559.310s (Solving: 535.80s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 559.400s
Choices : 10337609 (Domain: 10199947)
Conflicts : 685769 (Analyzed: 685766)
Restarts : 7702 (Average: 89.04 Last: 172)
Model-Level : 115.0
Problems : 81 (Average Length: 88.54 Splits: 0)
Lemmas : 685766 (Deleted: 649978)
Binary : 11077 (Ratio: 1.62%)
Ternary : 2735 (Ratio: 0.40%)
Conflict : 685766 (Average Length: 679.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 685766 (Average: 12.89 Max: 804 Sum: 8837229)
Executed : 685665 (Average: 12.88 Max: 804 Sum: 8834096 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.79s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 6.84s
Iteration 81
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 : 82
Time : 566.491s (Solving: 542.86s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 566.584s
Choices : 10402205 (Domain: 10264543)
Conflicts : 694775 (Analyzed: 694772)
Restarts : 7802 (Average: 89.05 Last: 172)
Model-Level : 115.0
Problems : 82 (Average Length: 88.89 Splits: 0)
Lemmas : 694772 (Deleted: 659325)
Binary : 11104 (Ratio: 1.60%)
Ternary : 2740 (Ratio: 0.39%)
Conflict : 694772 (Average Length: 682.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 694772 (Average: 12.78 Max: 804 Sum: 8882600)
Executed : 694671 (Average: 12.78 Max: 804 Sum: 8879467 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.14s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.19s
Iteration 82
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 : 83
Time : 573.665s (Solving: 549.90s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 573.760s
Choices : 10471274 (Domain: 10333596)
Conflicts : 703729 (Analyzed: 703726)
Restarts : 7902 (Average: 89.06 Last: 172)
Model-Level : 115.0
Problems : 83 (Average Length: 89.23 Splits: 0)
Lemmas : 703726 (Deleted: 668164)
Binary : 11147 (Ratio: 1.58%)
Ternary : 2742 (Ratio: 0.39%)
Conflict : 703726 (Average Length: 685.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 703726 (Average: 12.69 Max: 804 Sum: 8929593)
Executed : 703625 (Average: 12.68 Max: 804 Sum: 8926460 Ratio: 99.96%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.04%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.13s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.18s
Iteration 83
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 : 84
Time : 581.706s (Solving: 557.82s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 581.804s
Choices : 10551647 (Domain: 10413967)
Conflicts : 713098 (Analyzed: 713095)
Restarts : 8002 (Average: 89.11 Last: 172)
Model-Level : 115.0
Problems : 84 (Average Length: 89.56 Splits: 0)
Lemmas : 713095 (Deleted: 676932)
Binary : 11170 (Ratio: 1.57%)
Ternary : 2753 (Ratio: 0.39%)
Conflict : 713095 (Average Length: 687.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 713095 (Average: 12.60 Max: 804 Sum: 8986082)
Executed : 712994 (Average: 12.60 Max: 804 Sum: 8982949 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.00s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.05s
Iteration 84
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 : 85
Time : 590.176s (Solving: 566.16s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 590.276s
Choices : 10649622 (Domain: 10511921)
Conflicts : 722224 (Analyzed: 722221)
Restarts : 8102 (Average: 89.14 Last: 172)
Model-Level : 115.0
Problems : 85 (Average Length: 89.88 Splits: 0)
Lemmas : 722221 (Deleted: 686115)
Binary : 11200 (Ratio: 1.55%)
Ternary : 2758 (Ratio: 0.38%)
Conflict : 722221 (Average Length: 688.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 722221 (Average: 12.54 Max: 804 Sum: 9055371)
Executed : 722120 (Average: 12.53 Max: 804 Sum: 9052238 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.43s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.48s
Iteration 85
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 : 86
Time : 593.536s (Solving: 569.38s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 593.636s
Choices : 10709382 (Domain: 10571681)
Conflicts : 730159 (Analyzed: 730156)
Restarts : 8202 (Average: 89.02 Last: 172)
Model-Level : 115.0
Problems : 86 (Average Length: 90.20 Splits: 0)
Lemmas : 730156 (Deleted: 692780)
Binary : 11262 (Ratio: 1.54%)
Ternary : 2768 (Ratio: 0.38%)
Conflict : 730156 (Average Length: 683.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 730156 (Average: 12.47 Max: 804 Sum: 9106231)
Executed : 730055 (Average: 12.47 Max: 804 Sum: 9103098 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.31s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 3.37s
Iteration 86
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 : 87
Time : 602.390s (Solving: 578.09s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 602.496s
Choices : 10752690 (Domain: 10614989)
Conflicts : 738328 (Analyzed: 738325)
Restarts : 8302 (Average: 88.93 Last: 172)
Model-Level : 115.0
Problems : 87 (Average Length: 90.51 Splits: 0)
Lemmas : 738325 (Deleted: 700549)
Binary : 11278 (Ratio: 1.53%)
Ternary : 2776 (Ratio: 0.38%)
Conflict : 738325 (Average Length: 688.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 738325 (Average: 12.38 Max: 804 Sum: 9139428)
Executed : 738224 (Average: 12.37 Max: 804 Sum: 9136295 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.81s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.86s
Iteration 87
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 : 88
Time : 608.995s (Solving: 584.56s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 609.108s
Choices : 10813516 (Domain: 10675815)
Conflicts : 746953 (Analyzed: 746950)
Restarts : 8402 (Average: 88.90 Last: 172)
Model-Level : 115.0
Problems : 88 (Average Length: 90.81 Splits: 0)
Lemmas : 746950 (Deleted: 710805)
Binary : 11291 (Ratio: 1.51%)
Ternary : 2780 (Ratio: 0.37%)
Conflict : 746950 (Average Length: 689.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 746950 (Average: 12.29 Max: 804 Sum: 9180716)
Executed : 746849 (Average: 12.29 Max: 804 Sum: 9177583 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.56s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 6.61s
Iteration 88
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 : 89
Time : 615.995s (Solving: 591.44s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 616.112s
Choices : 10890578 (Domain: 10752791)
Conflicts : 755509 (Analyzed: 755506)
Restarts : 8502 (Average: 88.86 Last: 172)
Model-Level : 115.0
Problems : 89 (Average Length: 91.10 Splits: 0)
Lemmas : 755506 (Deleted: 717125)
Binary : 11326 (Ratio: 1.50%)
Ternary : 2804 (Ratio: 0.37%)
Conflict : 755506 (Average Length: 691.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 755506 (Average: 12.22 Max: 804 Sum: 9234773)
Executed : 755405 (Average: 12.22 Max: 804 Sum: 9231640 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.96s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.01s
Iteration 89
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 : 90
Time : 623.170s (Solving: 598.47s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 623.292s
Choices : 10962157 (Domain: 10824370)
Conflicts : 764947 (Analyzed: 764944)
Restarts : 8602 (Average: 88.93 Last: 172)
Model-Level : 115.0
Problems : 90 (Average Length: 91.39 Splits: 0)
Lemmas : 764944 (Deleted: 727704)
Binary : 11341 (Ratio: 1.48%)
Ternary : 2805 (Ratio: 0.37%)
Conflict : 764944 (Average Length: 692.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 764944 (Average: 12.14 Max: 804 Sum: 9284631)
Executed : 764843 (Average: 12.13 Max: 804 Sum: 9281498 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.12s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.18s
Iteration 90
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 : 91
Time : 632.132s (Solving: 607.28s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 632.256s
Choices : 11167284 (Domain: 11026963)
Conflicts : 774502 (Analyzed: 774499)
Restarts : 8702 (Average: 89.00 Last: 172)
Model-Level : 115.0
Problems : 91 (Average Length: 91.67 Splits: 0)
Lemmas : 774499 (Deleted: 736613)
Binary : 11533 (Ratio: 1.49%)
Ternary : 2817 (Ratio: 0.36%)
Conflict : 774499 (Average Length: 693.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 774499 (Average: 12.21 Max: 804 Sum: 9454212)
Executed : 774398 (Average: 12.20 Max: 804 Sum: 9451079 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.91s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.97s
Iteration 91
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 : 92
Time : 640.000s (Solving: 614.98s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 640.128s
Choices : 11248145 (Domain: 11107823)
Conflicts : 783668 (Analyzed: 783665)
Restarts : 8802 (Average: 89.03 Last: 184)
Model-Level : 115.0
Problems : 92 (Average Length: 91.95 Splits: 0)
Lemmas : 783665 (Deleted: 746031)
Binary : 11547 (Ratio: 1.47%)
Ternary : 2818 (Ratio: 0.36%)
Conflict : 783665 (Average Length: 693.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 783665 (Average: 12.13 Max: 804 Sum: 9509243)
Executed : 783564 (Average: 12.13 Max: 804 Sum: 9506110 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.81s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.88s
Iteration 92
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 : 93
Time : 649.676s (Solving: 624.50s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 649.804s
Choices : 11356158 (Domain: 11215833)
Conflicts : 793553 (Analyzed: 793550)
Restarts : 8902 (Average: 89.14 Last: 184)
Model-Level : 115.0
Problems : 93 (Average Length: 92.22 Splits: 0)
Lemmas : 793550 (Deleted: 755022)
Binary : 11594 (Ratio: 1.46%)
Ternary : 2832 (Ratio: 0.36%)
Conflict : 793550 (Average Length: 693.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 793550 (Average: 12.08 Max: 804 Sum: 9587789)
Executed : 793449 (Average: 12.08 Max: 804 Sum: 9584656 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.62s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 9.68s
Iteration 93
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 : 94
Time : 652.896s (Solving: 627.60s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 653.028s
Choices : 11405512 (Domain: 11265187)
Conflicts : 801159 (Analyzed: 801156)
Restarts : 9002 (Average: 89.00 Last: 184)
Model-Level : 115.0
Problems : 94 (Average Length: 92.48 Splits: 0)
Lemmas : 801156 (Deleted: 762483)
Binary : 11661 (Ratio: 1.46%)
Ternary : 2841 (Ratio: 0.35%)
Conflict : 801156 (Average Length: 689.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 801156 (Average: 12.02 Max: 804 Sum: 9630252)
Executed : 801055 (Average: 12.02 Max: 804 Sum: 9627119 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 3.18s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 3.22s
Iteration 94
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 : 95
Time : 663.475s (Solving: 638.06s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 663.612s
Choices : 11460353 (Domain: 11320028)
Conflicts : 810194 (Analyzed: 810191)
Restarts : 9102 (Average: 89.01 Last: 184)
Model-Level : 115.0
Problems : 95 (Average Length: 92.74 Splits: 0)
Lemmas : 810191 (Deleted: 772040)
Binary : 11690 (Ratio: 1.44%)
Ternary : 2856 (Ratio: 0.35%)
Conflict : 810191 (Average Length: 698.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 810191 (Average: 11.94 Max: 804 Sum: 9673989)
Executed : 810090 (Average: 11.94 Max: 804 Sum: 9670856 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.54s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 10.59s
Iteration 95
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 : 96
Time : 671.564s (Solving: 645.99s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 671.704s
Choices : 11542933 (Domain: 11402608)
Conflicts : 818906 (Analyzed: 818903)
Restarts : 9202 (Average: 88.99 Last: 184)
Model-Level : 115.0
Problems : 96 (Average Length: 92.99 Splits: 0)
Lemmas : 818903 (Deleted: 780806)
Binary : 11741 (Ratio: 1.43%)
Ternary : 2872 (Ratio: 0.35%)
Conflict : 818903 (Average Length: 701.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 818903 (Average: 11.89 Max: 804 Sum: 9739410)
Executed : 818802 (Average: 11.89 Max: 804 Sum: 9736277 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.03s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.09s
Iteration 96
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 : 97
Time : 678.129s (Solving: 652.42s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 678.268s
Choices : 11604353 (Domain: 11464028)
Conflicts : 828070 (Analyzed: 828067)
Restarts : 9302 (Average: 89.02 Last: 184)
Model-Level : 115.0
Problems : 97 (Average Length: 93.24 Splits: 0)
Lemmas : 828067 (Deleted: 789353)
Binary : 11764 (Ratio: 1.42%)
Ternary : 2873 (Ratio: 0.35%)
Conflict : 828067 (Average Length: 701.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 828067 (Average: 11.81 Max: 804 Sum: 9781652)
Executed : 827966 (Average: 11.81 Max: 804 Sum: 9778519 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.52s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 6.57s
Iteration 97
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 : 98
Time : 685.727s (Solving: 659.89s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 685.868s
Choices : 11670203 (Domain: 11529878)
Conflicts : 837340 (Analyzed: 837337)
Restarts : 9402 (Average: 89.06 Last: 184)
Model-Level : 115.0
Problems : 98 (Average Length: 93.48 Splits: 0)
Lemmas : 837337 (Deleted: 798391)
Binary : 11790 (Ratio: 1.41%)
Ternary : 2878 (Ratio: 0.34%)
Conflict : 837337 (Average Length: 705.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 837337 (Average: 11.74 Max: 804 Sum: 9826639)
Executed : 837236 (Average: 11.73 Max: 804 Sum: 9823506 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.56s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.60s
Iteration 98
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 : 99
Time : 693.616s (Solving: 667.62s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 693.764s
Choices : 11743501 (Domain: 11603168)
Conflicts : 846866 (Analyzed: 846863)
Restarts : 9502 (Average: 89.12 Last: 184)
Model-Level : 115.0
Problems : 99 (Average Length: 93.72 Splits: 0)
Lemmas : 846863 (Deleted: 807535)
Binary : 11813 (Ratio: 1.39%)
Ternary : 2879 (Ratio: 0.34%)
Conflict : 846863 (Average Length: 706.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 846863 (Average: 11.67 Max: 804 Sum: 9878846)
Executed : 846762 (Average: 11.66 Max: 804 Sum: 9875713 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.83s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.90s
Iteration 99
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...
[start: stats after solve call]
Models : 0+
Calls : 100
Time : 702.056s (Solving: 675.93s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 702.208s
Choices : 11827741 (Domain: 11687407)
Conflicts : 856967 (Analyzed: 856964)
Restarts : 9602 (Average: 89.25 Last: 184)
Model-Level : 115.0
Problems : 100 (Average Length: 93.95 Splits: 0)
Lemmas : 856964 (Deleted: 816890)
Binary : 11828 (Ratio: 1.38%)
Ternary : 2882 (Ratio: 0.34%)
Conflict : 856964 (Average Length: 708.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 856964 (Average: 11.60 Max: 804 Sum: 9940425)
Executed : 856863 (Average: 11.60 Max: 804 Sum: 9937292 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.40s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.45s
Iteration 100
Queue: [(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 : 101
Time : 710.878s (Solving: 684.61s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 711.032s
Choices : 11924133 (Domain: 11783530)
Conflicts : 866234 (Analyzed: 866231)
Restarts : 9702 (Average: 89.28 Last: 184)
Model-Level : 115.0
Problems : 101 (Average Length: 94.18 Splits: 0)
Lemmas : 866231 (Deleted: 826877)
Binary : 11848 (Ratio: 1.37%)
Ternary : 2889 (Ratio: 0.33%)
Conflict : 866231 (Average Length: 709.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 866231 (Average: 11.56 Max: 804 Sum: 10009326)
Executed : 866130 (Average: 11.55 Max: 804 Sum: 10006193 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.77s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.83s
Iteration 101
Queue: [(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 : 102
Time : 720.063s (Solving: 693.67s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 720.220s
Choices : 12024984 (Domain: 11884377)
Conflicts : 876018 (Analyzed: 876015)
Restarts : 9802 (Average: 89.37 Last: 184)
Model-Level : 115.0
Problems : 102 (Average Length: 94.40 Splits: 0)
Lemmas : 876015 (Deleted: 836030)
Binary : 11857 (Ratio: 1.35%)
Ternary : 2892 (Ratio: 0.33%)
Conflict : 876015 (Average Length: 709.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 876015 (Average: 11.51 Max: 804 Sum: 10081329)
Executed : 875914 (Average: 11.50 Max: 804 Sum: 10078196 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.15s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 9.19s
Iteration 102
Queue: [(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 : 103
Time : 729.881s (Solving: 703.35s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 730.040s
Choices : 12380022 (Domain: 12236675)
Conflicts : 884930 (Analyzed: 884927)
Restarts : 9902 (Average: 89.37 Last: 184)
Model-Level : 115.0
Problems : 103 (Average Length: 94.62 Splits: 0)
Lemmas : 884927 (Deleted: 845293)
Binary : 12077 (Ratio: 1.36%)
Ternary : 2911 (Ratio: 0.33%)
Conflict : 884927 (Average Length: 713.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 884927 (Average: 11.74 Max: 804 Sum: 10387706)
Executed : 884826 (Average: 11.73 Max: 804 Sum: 10384573 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.77s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 9.82s
Iteration 103
Queue: [(4,20,9,True), (5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 104
Time : 732.460s (Solving: 705.81s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 732.620s
Choices : 12414794 (Domain: 12271447)
Conflicts : 892338 (Analyzed: 892335)
Restarts : 10002 (Average: 89.22 Last: 184)
Model-Level : 115.0
Problems : 104 (Average Length: 94.84 Splits: 0)
Lemmas : 892335 (Deleted: 851570)
Binary : 12115 (Ratio: 1.36%)
Ternary : 2915 (Ratio: 0.33%)
Conflict : 892335 (Average Length: 708.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 892335 (Average: 11.67 Max: 804 Sum: 10413513)
Executed : 892234 (Average: 11.67 Max: 804 Sum: 10410380 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 2.54s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 2.58s
Iteration 104
Queue: [(5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 105
Time : 742.371s (Solving: 715.57s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 742.536s
Choices : 12485724 (Domain: 12342377)
Conflicts : 901675 (Analyzed: 901672)
Restarts : 10102 (Average: 89.26 Last: 184)
Model-Level : 115.0
Problems : 105 (Average Length: 95.05 Splits: 0)
Lemmas : 901672 (Deleted: 861412)
Binary : 12151 (Ratio: 1.35%)
Ternary : 2921 (Ratio: 0.32%)
Conflict : 901672 (Average Length: 717.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 901672 (Average: 11.61 Max: 804 Sum: 10470229)
Executed : 901571 (Average: 11.61 Max: 804 Sum: 10467096 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.86s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 9.92s
Iteration 105
Queue: [(6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 106
Time : 751.446s (Solving: 724.50s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 751.616s
Choices : 12572967 (Domain: 12429620)
Conflicts : 910932 (Analyzed: 910929)
Restarts : 10202 (Average: 89.29 Last: 184)
Model-Level : 115.0
Problems : 106 (Average Length: 95.25 Splits: 0)
Lemmas : 910929 (Deleted: 871578)
Binary : 12217 (Ratio: 1.34%)
Ternary : 2928 (Ratio: 0.32%)
Conflict : 910929 (Average Length: 724.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 910929 (Average: 11.57 Max: 804 Sum: 10538307)
Executed : 910828 (Average: 11.57 Max: 804 Sum: 10535174 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 9.03s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 9.08s
Iteration 106
Queue: [(8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 107
Time : 758.286s (Solving: 731.21s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 758.460s
Choices : 12635599 (Domain: 12492247)
Conflicts : 920355 (Analyzed: 920352)
Restarts : 10302 (Average: 89.34 Last: 184)
Model-Level : 115.0
Problems : 107 (Average Length: 95.46 Splits: 0)
Lemmas : 920352 (Deleted: 879581)
Binary : 12233 (Ratio: 1.33%)
Ternary : 2928 (Ratio: 0.32%)
Conflict : 920352 (Average Length: 724.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 920352 (Average: 11.50 Max: 804 Sum: 10581898)
Executed : 920251 (Average: 11.49 Max: 804 Sum: 10578765 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.79s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 6.85s
Iteration 107
Queue: [(9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 108
Time : 765.679s (Solving: 738.45s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 765.856s
Choices : 12704465 (Domain: 12561104)
Conflicts : 929262 (Analyzed: 929259)
Restarts : 10402 (Average: 89.33 Last: 184)
Model-Level : 115.0
Problems : 108 (Average Length: 95.66 Splits: 0)
Lemmas : 929259 (Deleted: 888870)
Binary : 12254 (Ratio: 1.32%)
Ternary : 2936 (Ratio: 0.32%)
Conflict : 929259 (Average Length: 726.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 929259 (Average: 11.44 Max: 804 Sum: 10629083)
Executed : 929158 (Average: 11.43 Max: 804 Sum: 10625950 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.34s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.40s
Iteration 108
Queue: [(11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 109
Time : 773.496s (Solving: 746.11s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 773.676s
Choices : 12791375 (Domain: 12647820)
Conflicts : 938134 (Analyzed: 938131)
Restarts : 10502 (Average: 89.33 Last: 184)
Model-Level : 115.0
Problems : 109 (Average Length: 95.85 Splits: 0)
Lemmas : 938131 (Deleted: 897595)
Binary : 12348 (Ratio: 1.32%)
Ternary : 2947 (Ratio: 0.31%)
Conflict : 938131 (Average Length: 726.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 938131 (Average: 11.40 Max: 804 Sum: 10692359)
Executed : 938030 (Average: 11.39 Max: 804 Sum: 10689226 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.76s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.82s
Iteration 109
Queue: [(13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 110
Time : 781.078s (Solving: 753.54s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 781.260s
Choices : 12865902 (Domain: 12722324)
Conflicts : 947574 (Analyzed: 947571)
Restarts : 10602 (Average: 89.38 Last: 184)
Model-Level : 115.0
Problems : 110 (Average Length: 96.05 Splits: 0)
Lemmas : 947571 (Deleted: 906268)
Binary : 12356 (Ratio: 1.30%)
Ternary : 2949 (Ratio: 0.31%)
Conflict : 947571 (Average Length: 727.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 947571 (Average: 11.34 Max: 804 Sum: 10742954)
Executed : 947470 (Average: 11.33 Max: 804 Sum: 10739821 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.53s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.59s
Iteration 110
Queue: [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 111
Time : 788.621s (Solving: 760.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 788.804s
Choices : 12943246 (Domain: 12799668)
Conflicts : 956305 (Analyzed: 956302)
Restarts : 10702 (Average: 89.36 Last: 184)
Model-Level : 115.0
Problems : 111 (Average Length: 96.23 Splits: 0)
Lemmas : 956302 (Deleted: 915504)
Binary : 12373 (Ratio: 1.29%)
Ternary : 2955 (Ratio: 0.31%)
Conflict : 956302 (Average Length: 729.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 956302 (Average: 11.28 Max: 804 Sum: 10789739)
Executed : 956201 (Average: 11.28 Max: 804 Sum: 10786606 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.51s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.55s
Iteration 111
Queue: [(22,110,2,True), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 112
Time : 798.694s (Solving: 770.88s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 798.880s
Choices : 13040307 (Domain: 12896729)
Conflicts : 966555 (Analyzed: 966552)
Restarts : 10802 (Average: 89.48 Last: 184)
Model-Level : 115.0
Problems : 112 (Average Length: 96.42 Splits: 0)
Lemmas : 966552 (Deleted: 924115)
Binary : 12395 (Ratio: 1.28%)
Ternary : 2957 (Ratio: 0.31%)
Conflict : 966552 (Average Length: 731.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 966552 (Average: 11.23 Max: 804 Sum: 10854853)
Executed : 966451 (Average: 11.23 Max: 804 Sum: 10851720 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.02s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 10.08s
Iteration 112
Queue: [(4,20,10,True), (5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 113
Time : 802.753s (Solving: 774.81s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 802.940s
Choices : 13111674 (Domain: 12968096)
Conflicts : 974599 (Analyzed: 974596)
Restarts : 10902 (Average: 89.40 Last: 184)
Model-Level : 115.0
Problems : 113 (Average Length: 96.60 Splits: 0)
Lemmas : 974596 (Deleted: 931881)
Binary : 12454 (Ratio: 1.28%)
Ternary : 2975 (Ratio: 0.31%)
Conflict : 974596 (Average Length: 728.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 974596 (Average: 11.21 Max: 804 Sum: 10920351)
Executed : 974495 (Average: 11.20 Max: 804 Sum: 10917218 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.02s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 4.06s
Iteration 113
Queue: [(5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 114
Time : 812.869s (Solving: 784.81s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 813.064s
Choices : 13185537 (Domain: 13041959)
Conflicts : 983518 (Analyzed: 983515)
Restarts : 11002 (Average: 89.39 Last: 184)
Model-Level : 115.0
Problems : 114 (Average Length: 96.78 Splits: 0)
Lemmas : 983515 (Deleted: 941911)
Binary : 12505 (Ratio: 1.27%)
Ternary : 2986 (Ratio: 0.30%)
Conflict : 983515 (Average Length: 737.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 983515 (Average: 11.16 Max: 804 Sum: 10979427)
Executed : 983414 (Average: 11.16 Max: 804 Sum: 10976294 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 10.08s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 10.12s
Iteration 114
Queue: [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 115
Time : 820.835s (Solving: 792.64s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 821.036s
Choices : 13255710 (Domain: 13112132)
Conflicts : 992455 (Analyzed: 992452)
Restarts : 11102 (Average: 89.39 Last: 184)
Model-Level : 115.0
Problems : 115 (Average Length: 96.96 Splits: 0)
Lemmas : 992452 (Deleted: 950714)
Binary : 12552 (Ratio: 1.26%)
Ternary : 3001 (Ratio: 0.30%)
Conflict : 992452 (Average Length: 740.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 992452 (Average: 11.12 Max: 804 Sum: 11032012)
Executed : 992351 (Average: 11.11 Max: 804 Sum: 11028879 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.92s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.97s
Iteration 115
Queue: [(7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 116
Time : 827.584s (Solving: 799.26s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 827.788s
Choices : 13320597 (Domain: 13177016)
Conflicts : 1001486 (Analyzed: 1001483)
Restarts : 11202 (Average: 89.40 Last: 184)
Model-Level : 115.0
Problems : 116 (Average Length: 97.13 Splits: 0)
Lemmas : 1001483 (Deleted: 959507)
Binary : 12570 (Ratio: 1.26%)
Ternary : 3008 (Ratio: 0.30%)
Conflict : 1001483 (Average Length: 740.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1001483 (Average: 11.06 Max: 804 Sum: 11079040)
Executed : 1001382 (Average: 11.06 Max: 804 Sum: 11075907 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.71s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 6.75s
Iteration 116
Queue: [(10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 117
Time : 836.118s (Solving: 807.67s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 836.324s
Choices : 13400827 (Domain: 13257219)
Conflicts : 1011715 (Analyzed: 1011712)
Restarts : 11302 (Average: 89.52 Last: 184)
Model-Level : 115.0
Problems : 117 (Average Length: 97.30 Splits: 0)
Lemmas : 1011712 (Deleted: 968327)
Binary : 12615 (Ratio: 1.25%)
Ternary : 3012 (Ratio: 0.30%)
Conflict : 1011712 (Average Length: 742.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1011712 (Average: 11.01 Max: 804 Sum: 11136699)
Executed : 1011611 (Average: 11.00 Max: 804 Sum: 11133566 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.49s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.54s
Iteration 117
Queue: [(12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 118
Time : 843.607s (Solving: 815.01s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 843.812s
Choices : 13473329 (Domain: 13329698)
Conflicts : 1020876 (Analyzed: 1020873)
Restarts : 11402 (Average: 89.53 Last: 184)
Model-Level : 115.0
Problems : 118 (Average Length: 97.47 Splits: 0)
Lemmas : 1020873 (Deleted: 978408)
Binary : 12634 (Ratio: 1.24%)
Ternary : 3018 (Ratio: 0.30%)
Conflict : 1020873 (Average Length: 744.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1020873 (Average: 10.96 Max: 804 Sum: 11186313)
Executed : 1020772 (Average: 10.95 Max: 804 Sum: 11183180 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 7.44s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 7.49s
Iteration 118
Queue: [(14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 119
Time : 851.708s (Solving: 822.96s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 851.916s
Choices : 13557863 (Domain: 13414212)
Conflicts : 1030146 (Analyzed: 1030143)
Restarts : 11502 (Average: 89.56 Last: 184)
Model-Level : 115.0
Problems : 119 (Average Length: 97.63 Splits: 0)
Lemmas : 1030143 (Deleted: 987414)
Binary : 12652 (Ratio: 1.23%)
Ternary : 3032 (Ratio: 0.29%)
Conflict : 1030143 (Average Length: 745.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1030143 (Average: 10.92 Max: 804 Sum: 11244412)
Executed : 1030042 (Average: 10.91 Max: 804 Sum: 11241279 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.05s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.11s
Iteration 119
Queue: [(18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 120
Time : 860.236s (Solving: 831.34s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 860.448s
Choices : 13712973 (Domain: 13568567)
Conflicts : 1039314 (Analyzed: 1039311)
Restarts : 11602 (Average: 89.58 Last: 184)
Model-Level : 115.0
Problems : 120 (Average Length: 97.79 Splits: 0)
Lemmas : 1039311 (Deleted: 996426)
Binary : 12746 (Ratio: 1.23%)
Ternary : 3043 (Ratio: 0.29%)
Conflict : 1039311 (Average Length: 746.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1039311 (Average: 10.94 Max: 804 Sum: 11366683)
Executed : 1039210 (Average: 10.93 Max: 804 Sum: 11363550 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.47s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.53s
Iteration 120
Queue: [(4,20,11,True), (5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until: 115
Blocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 121
Time : 862.239s (Solving: 833.19s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 862.452s
Choices : 13745614 (Domain: 13601208)
Conflicts : 1046538 (Analyzed: 1046535)
Restarts : 11702 (Average: 89.43 Last: 184)
Model-Level : 115.0
Problems : 121 (Average Length: 97.95 Splits: 0)
Lemmas : 1046535 (Deleted: 1002872)
Binary : 12779 (Ratio: 1.22%)
Ternary : 3048 (Ratio: 0.29%)
Conflict : 1046535 (Average Length: 741.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1046535 (Average: 10.88 Max: 804 Sum: 11389452)
Executed : 1046434 (Average: 10.88 Max: 804 Sum: 11386319 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 1.95s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 2.01s
Iteration 121
Queue: [(5,25,11,True), (6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 122
Time : 870.750s (Solving: 841.55s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 870.968s
Choices : 13808870 (Domain: 13664464)
Conflicts : 1054704 (Analyzed: 1054701)
Restarts : 11802 (Average: 89.37 Last: 184)
Model-Level : 115.0
Problems : 122 (Average Length: 98.11 Splits: 0)
Lemmas : 1054701 (Deleted: 1010599)
Binary : 12848 (Ratio: 1.22%)
Ternary : 3058 (Ratio: 0.29%)
Conflict : 1054701 (Average Length: 751.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1054701 (Average: 10.84 Max: 804 Sum: 11436954)
Executed : 1054600 (Average: 10.84 Max: 804 Sum: 11433821 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.46s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.52s
Iteration 122
Queue: [(6,30,10,True), (7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 123
Time : 879.378s (Solving: 850.03s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 879.600s
Choices : 13884685 (Domain: 13740279)
Conflicts : 1063387 (Analyzed: 1063384)
Restarts : 11902 (Average: 89.34 Last: 184)
Model-Level : 115.0
Problems : 123 (Average Length: 98.26 Splits: 0)
Lemmas : 1063384 (Deleted: 1020841)
Binary : 12891 (Ratio: 1.21%)
Ternary : 3083 (Ratio: 0.29%)
Conflict : 1063384 (Average Length: 757.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1063384 (Average: 10.81 Max: 804 Sum: 11494856)
Executed : 1063283 (Average: 10.81 Max: 804 Sum: 11491723 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.57s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.63s
Iteration 123
Queue: [(7,35,9,True), (8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 124
Time : 885.866s (Solving: 856.36s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 886.092s
Choices : 13950526 (Domain: 13806057)
Conflicts : 1072375 (Analyzed: 1072372)
Restarts : 12002 (Average: 89.35 Last: 184)
Model-Level : 115.0
Problems : 124 (Average Length: 98.41 Splits: 0)
Lemmas : 1072372 (Deleted: 1029078)
Binary : 12910 (Ratio: 1.20%)
Ternary : 3093 (Ratio: 0.29%)
Conflict : 1072372 (Average Length: 757.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1072372 (Average: 10.76 Max: 804 Sum: 11541621)
Executed : 1072271 (Average: 10.76 Max: 804 Sum: 11538488 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 6.43s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 6.49s
Iteration 124
Queue: [(8,40,8,True), (9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until: 115
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 125
Time : 894.113s (Solving: 864.48s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 894.344s
Choices : 14023841 (Domain: 13879370)
Conflicts : 1081352 (Analyzed: 1081349)
Restarts : 12102 (Average: 89.35 Last: 184)
Model-Level : 115.0
Problems : 125 (Average Length: 98.56 Splits: 0)
Lemmas : 1081349 (Deleted: 1037874)
Binary : 12991 (Ratio: 1.20%)
Ternary : 3108 (Ratio: 0.29%)
Conflict : 1081349 (Average Length: 760.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1081349 (Average: 10.72 Max: 804 Sum: 11595129)
Executed : 1081248 (Average: 10.72 Max: 804 Sum: 11591996 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1
[endof: stats after solve call]
Solving Time: 8.21s
Memory: 701MB (+0MB)
UNKNOWN
Iteration Time: 8.25s
Iteration 125
Queue: [(9,45,7,True), (10,50,7,False), (11,55,6,True), (12,60,6,False), (13,65,5,True), (14,70,5,False), (15,75,4,True), (16,80,4,False), (17,85,4,False), (18,90,4,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,True)]
Grounded Until: 115
Unblocking actions...
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN
INTERRUPTED : 1
Models : 0+
Calls : 126
Time : 894.335s (Solving: 864.58s 1st Model: 0.00s Unsat: 3.47s)
CPU Time : 894.544s
Choices : 14024340 (Domain: 13879869)
Conflicts : 1081471 (Analyzed: 1081468)
Restarts : 12103 (Average: 89.36 Last: 184)
Model-Level : 115.0
Problems : 126 (Average Length: 98.71 Splits: 0)
Lemmas : 1081468 (Deleted: 1037874)
Binary : 12991 (Ratio: 1.20%)
Ternary : 3108 (Ratio: 0.29%)
Conflict : 1081468 (Average Length: 760.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1081468 (Average: 10.72 Max: 804 Sum: 11595494)
Executed : 1081367 (Average: 10.72 Max: 804 Sum: 11592361 Ratio: 99.97%)
Bounded : 101 (Average: 31.02 Max: 117 Sum: 3133 Ratio: 0.03%)
Rules : 62994 (Original: 61599)
Atoms : 50308
Bodies : 11595 (Original: 10199)
Count : 252 (Original: 531)
Equivalences : 3261 (Atom=Atom: 62 Body=Body: 0 Other: 3199)
Tight : Yes
Variables : 595276 (Eliminated: 0 Frozen: 191082)
Constraints : 4421087 (Binary: 91.5% Ternary: 6.7% Other: 1.9%)
Memory Peak : 765MB
Max. Length : 115 steps
Models : 1