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

2448 lines
88 KiB
Plaintext
Raw Normal View History

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-2.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-2.pddl
Parsing...
Parsing: [0.040s CPU, 0.037s wall-clock]
Normalizing task... [0.000s CPU, 0.003s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.009s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.050s CPU, 0.049s wall-clock]
Preparing model... [0.020s CPU, 0.025s wall-clock]
Generated 115 rules.
Computing model... [0.330s CPU, 0.330s wall-clock]
2025 relevant atoms
2105 auxiliary atoms
4130 final queue length
7122 total queue pushes
Completing instantiation... [0.600s CPU, 0.598s wall-clock]
Instantiating: [1.010s CPU, 1.018s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.100s CPU, 0.097s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.006s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.000s wall-clock]
Choosing groups...
207 uncovered facts
Choosing groups: [0.000s CPU, 0.001s wall-clock]
Building translation key... [0.010s CPU, 0.008s wall-clock]
Computing fact groups: [0.130s CPU, 0.130s 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.000s CPU, 0.002s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.040s CPU, 0.033s wall-clock]
Translating task: [0.660s CPU, 0.657s wall-clock]
2326 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.310s CPU, 0.308s wall-clock]
Reordering and filtering variables...
210 of 210 variables necessary.
11 of 14 mutex groups necessary.
1390 of 1390 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.210s CPU, 0.207s wall-clock]
Translator variables: 210
Translator derived variables: 0
Translator facts: 441
Translator goal facts: 9
Translator mutex groups: 11
Translator total mutex groups size: 33
Translator operators: 1390
Translator axioms: 0
Translator task size: 13333
Translator peak memory: 43980 KB
Writing output... [0.260s CPU, 0.271s wall-clock]
Done! [2.640s CPU, 2.663s wall-clock]
planner.py version 0.0.1
Time: 0.57s
Memory: 86MB
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.658s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.568s
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 : 38518
Atoms : 38518
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 : 222MB
Max. Length : 0 steps
Models : 0
[endof: stats after solve call]
Solving Time: 0.00s
Memory: 158MB (+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: 158MB
Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
Grounding Time: 0.15s
Memory: 158MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 1+
Calls : 2
Time : 0.982s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.892s
Choices : 152 (Domain: 73)
Conflicts : 2 (Analyzed: 2)
Restarts : 0
Model-Level : 147.0
Problems : 2 (Average Length: 4.50 Splits: 0)
Lemmas : 2 (Deleted: 0)
Binary : 0 (Ratio: 0.00%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 2 (Average Length: 23.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 2 (Average: 6.00 Max: 11 Sum: 12)
Executed : 2 (Average: 6.00 Max: 11 Sum: 12 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Rules : 38518
Atoms : 38518
Bodies : 1 (Original: 0)
Tight : Yes
Variables : 10322 (Eliminated: 0 Frozen: 10322)
Constraints : 36431 (Binary: 95.0% Ternary: 3.5% Other: 1.5%)
Memory Peak : 222MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.10s
Memory: 160MB (+2MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time: 0.58s
Memory: 178MB (+18MB)
Solving...
[start: stats after solve call]
Models : 0
Calls : 3
Time : 1.081s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.992s
Choices : 161 (Domain: 78)
Conflicts : 9 (Analyzed: 8)
Restarts : 0
Model-Level : 147.0
Problems : 3 (Average Length: 5.33 Splits: 0)
Lemmas : 8 (Deleted: 0)
Binary : 1 (Ratio: 12.50%)
Ternary : 2 (Ratio: 25.00%)
Conflict : 8 (Average Length: 8.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 8 (Average: 2.75 Max: 11 Sum: 22)
Executed : 7 (Average: 2.62 Max: 11 Sum: 21 Ratio: 95.45%)
Bounded : 1 (Average: 1.00 Max: 1 Sum: 1 Ratio: 4.55%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 12735 (Eliminated: 1464 Frozen: 11271)
Constraints : 50631 (Binary: 90.2% Ternary: 5.9% Other: 3.9%)
Memory Peak : 222MB
Max. Length : 0 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.02s
Memory: 178MB (+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: 180.0MB
Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
Grounding Time: 0.29s
Memory: 178MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 4
Time : 2.170s (Solving: 0.38s 1st Model: 0.00s Unsat: 0.38s)
CPU Time : 2.080s
Choices : 12799 (Domain: 10798)
Conflicts : 1643 (Analyzed: 1641)
Restarts : 10 (Average: 164.10 Last: 20)
Model-Level : 147.0
Problems : 4 (Average Length: 7.00 Splits: 0)
Lemmas : 1641 (Deleted: 0)
Binary : 185 (Ratio: 11.27%)
Ternary : 187 (Ratio: 11.40%)
Conflict : 1641 (Average Length: 27.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1641 (Average: 7.73 Max: 79 Sum: 12687)
Executed : 1623 (Average: 7.62 Max: 79 Sum: 12504 Ratio: 98.56%)
Bounded : 18 (Average: 10.17 Max: 12 Sum: 183 Ratio: 1.44%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 35311 (Eliminated: 1464 Frozen: 26317)
Constraints : 223676 (Binary: 91.3% Ternary: 6.4% Other: 2.3%)
Memory Peak : 222MB
Max. Length : 5 steps
Models : 1
[endof: stats after solve call]
Solving Time: 0.70s
Memory: 189MB (+11MB)
UNSAT
Iteration Time: 1.10s
Iteration 4
Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 10
Expected Memory: 200.0MB
Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
Grounding Time: 0.38s
Memory: 195MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0
Calls : 5
Time : 6.807s (Solving: 4.20s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 6.720s
Choices : 95323 (Domain: 72132)
Conflicts : 13704 (Analyzed: 13701)
Restarts : 61 (Average: 224.61 Last: 168)
Model-Level : 147.0
Problems : 5 (Average Length: 9.00 Splits: 0)
Lemmas : 13701 (Deleted: 7320)
Binary : 884 (Ratio: 6.45%)
Ternary : 495 (Ratio: 3.61%)
Conflict : 13701 (Average Length: 196.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 13701 (Average: 6.83 Max: 380 Sum: 93639)
Executed : 13664 (Average: 6.80 Max: 380 Sum: 93177 Ratio: 99.51%)
Bounded : 37 (Average: 12.49 Max: 17 Sum: 462 Ratio: 0.49%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 57887 (Eliminated: 1464 Frozen: 48893)
Constraints : 381121 (Binary: 91.6% Ternary: 6.3% Other: 2.1%)
Memory Peak : 222MB
Max. Length : 10 steps
Models : 1
[endof: stats after solve call]
Solving Time: 4.14s
Memory: 209MB (+14MB)
UNSAT
Iteration Time: 4.65s
Iteration 5
Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until: 15
Expected Memory: 229.0MB
Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
Grounding Time: 0.30s
Memory: 212MB (+3MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 6
Time : 21.097s (Solving: 17.72s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 21.012s
Choices : 318692 (Domain: 274484)
Conflicts : 41885 (Analyzed: 41882)
Restarts : 161 (Average: 260.14 Last: 200)
Model-Level : 147.0
Problems : 6 (Average Length: 11.17 Splits: 0)
Lemmas : 41882 (Deleted: 27757)
Binary : 2114 (Ratio: 5.05%)
Ternary : 772 (Ratio: 1.84%)
Conflict : 41882 (Average Length: 420.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 41882 (Average: 7.36 Max: 431 Sum: 308320)
Executed : 41843 (Average: 7.35 Max: 431 Sum: 307814 Ratio: 99.84%)
Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.16%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 80463 (Eliminated: 1464 Frozen: 71469)
Constraints : 538293 (Binary: 91.6% Ternary: 6.4% Other: 2.1%)
Memory Peak : 227MB
Max. Length : 15 steps
Models : 1
[endof: stats after solve call]
Solving Time: 13.86s
Memory: 227MB (+15MB)
UNKNOWN
Iteration Time: 14.30s
Iteration 6
Queue: [(5,25,0,True), (6,30,0,True)]
Grounded Until: 20
Expected Memory: 247.0MB
Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
Grounding Time: 0.31s
Memory: 230MB (+3MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 7
Time : 38.488s (Solving: 34.32s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 38.412s
Choices : 544925 (Domain: 486198)
Conflicts : 70044 (Analyzed: 70041)
Restarts : 261 (Average: 268.36 Last: 203)
Model-Level : 147.0
Problems : 7 (Average Length: 13.43 Splits: 0)
Lemmas : 70041 (Deleted: 53675)
Binary : 3314 (Ratio: 4.73%)
Ternary : 972 (Ratio: 1.39%)
Conflict : 70041 (Average Length: 595.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 70041 (Average: 7.41 Max: 431 Sum: 518924)
Executed : 70002 (Average: 7.40 Max: 431 Sum: 518418 Ratio: 99.90%)
Bounded : 39 (Average: 12.97 Max: 22 Sum: 506 Ratio: 0.10%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 103039 (Eliminated: 1464 Frozen: 94045)
Constraints : 711310 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
Memory Peak : 246MB
Max. Length : 20 steps
Models : 1
[endof: stats after solve call]
Solving Time: 16.94s
Memory: 242MB (+12MB)
UNKNOWN
Iteration Time: 17.40s
Iteration 7
Queue: [(6,30,0,True)]
Grounded Until: 25
Expected Memory: 262.0MB
Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
Grounding Time: 0.36s
Memory: 244MB (+2MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 8
Time : 58.835s (Solving: 53.79s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 58.768s
Choices : 795479 (Domain: 727093)
Conflicts : 98170 (Analyzed: 98167)
Restarts : 361 (Average: 271.93 Last: 203)
Model-Level : 147.0
Problems : 8 (Average Length: 15.75 Splits: 0)
Lemmas : 98167 (Deleted: 80033)
Binary : 4642 (Ratio: 4.73%)
Ternary : 1200 (Ratio: 1.22%)
Conflict : 98167 (Average Length: 701.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 98167 (Average: 7.65 Max: 431 Sum: 751388)
Executed : 98127 (Average: 7.65 Max: 431 Sum: 750850 Ratio: 99.93%)
Bounded : 40 (Average: 13.45 Max: 32 Sum: 538 Ratio: 0.07%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 1464 Frozen: 116621)
Constraints : 884355 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
Memory Peak : 390MB
Max. Length : 25 steps
Models : 1
[endof: stats after solve call]
Solving Time: 19.83s
Memory: 326MB (+82MB)
UNKNOWN
Iteration Time: 20.36s
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 : 73.429s (Solving: 68.35s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 73.368s
Choices : 908988 (Domain: 840602)
Conflicts : 126350 (Analyzed: 126347)
Restarts : 461 (Average: 274.07 Last: 203)
Model-Level : 147.0
Problems : 9 (Average Length: 17.56 Splits: 0)
Lemmas : 126347 (Deleted: 107054)
Binary : 5110 (Ratio: 4.04%)
Ternary : 1272 (Ratio: 1.01%)
Conflict : 126347 (Average Length: 680.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 126347 (Average: 6.80 Max: 431 Sum: 859482)
Executed : 126306 (Average: 6.80 Max: 431 Sum: 858912 Ratio: 99.93%)
Bounded : 41 (Average: 13.90 Max: 32 Sum: 570 Ratio: 0.07%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
Constraints : 884341 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
Memory Peak : 390MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 14.58s
Memory: 326MB (+0MB)
UNKNOWN
Iteration Time: 14.60s
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 : 98.747s (Solving: 93.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 98.696s
Choices : 1039074 (Domain: 970650)
Conflicts : 154469 (Analyzed: 154466)
Restarts : 561 (Average: 275.34 Last: 204)
Model-Level : 147.0
Problems : 10 (Average Length: 19.00 Splits: 0)
Lemmas : 154466 (Deleted: 134626)
Binary : 5352 (Ratio: 3.46%)
Ternary : 1336 (Ratio: 0.86%)
Conflict : 154466 (Average Length: 791.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 154466 (Average: 6.32 Max: 431 Sum: 976481)
Executed : 154424 (Average: 6.32 Max: 431 Sum: 975879 Ratio: 99.94%)
Bounded : 42 (Average: 14.33 Max: 32 Sum: 602 Ratio: 0.06%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
Constraints : 884328 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
Memory Peak : 390MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 25.32s
Memory: 326MB (+0MB)
UNKNOWN
Iteration Time: 25.33s
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 : 121.765s (Solving: 116.61s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 121.724s
Choices : 1259852 (Domain: 1190405)
Conflicts : 182648 (Analyzed: 182645)
Restarts : 661 (Average: 276.32 Last: 204)
Model-Level : 147.0
Problems : 11 (Average Length: 20.18 Splits: 0)
Lemmas : 182645 (Deleted: 161750)
Binary : 5826 (Ratio: 3.19%)
Ternary : 1427 (Ratio: 0.78%)
Conflict : 182645 (Average Length: 840.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 182645 (Average: 6.46 Max: 431 Sum: 1180686)
Executed : 182602 (Average: 6.46 Max: 431 Sum: 1180052 Ratio: 99.95%)
Bounded : 43 (Average: 14.74 Max: 32 Sum: 634 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 125615 (Eliminated: 1464 Frozen: 124151)
Constraints : 884314 (Binary: 91.6% Ternary: 6.4% Other: 2.0%)
Memory Peak : 390MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 23.01s
Memory: 326MB (+0MB)
UNKNOWN
Iteration Time: 23.03s
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: 410.0MB
Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time: 0.32s
Memory: 327MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 12
Time : 140.038s (Solving: 134.04s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 140.004s
Choices : 1469681 (Domain: 1393123)
Conflicts : 210833 (Analyzed: 210830)
Restarts : 761 (Average: 277.04 Last: 204)
Model-Level : 147.0
Problems : 12 (Average Length: 21.58 Splits: 0)
Lemmas : 210830 (Deleted: 188096)
Binary : 6845 (Ratio: 3.25%)
Ternary : 1557 (Ratio: 0.74%)
Conflict : 210830 (Average Length: 847.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 210830 (Average: 6.49 Max: 431 Sum: 1369029)
Executed : 210786 (Average: 6.49 Max: 431 Sum: 1368358 Ratio: 99.95%)
Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.05%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 148191 (Eliminated: 1464 Frozen: 139197)
Constraints : 1057342 (Binary: 91.6% Ternary: 6.5% Other: 2.0%)
Memory Peak : 390MB
Max. Length : 30 steps
Models : 1
[endof: stats after solve call]
Solving Time: 17.78s
Memory: 341MB (+14MB)
UNKNOWN
Iteration Time: 18.29s
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: 425.0MB
Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time: 0.42s
Memory: 348MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 13
Time : 158.318s (Solving: 151.36s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 158.292s
Choices : 1722991 (Domain: 1639840)
Conflicts : 239049 (Analyzed: 239046)
Restarts : 861 (Average: 277.64 Last: 204)
Model-Level : 147.0
Problems : 13 (Average Length: 23.15 Splits: 0)
Lemmas : 239046 (Deleted: 215086)
Binary : 7595 (Ratio: 3.18%)
Ternary : 1618 (Ratio: 0.68%)
Conflict : 239046 (Average Length: 840.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 239046 (Average: 6.70 Max: 431 Sum: 1600769)
Executed : 239002 (Average: 6.69 Max: 431 Sum: 1600098 Ratio: 99.96%)
Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 170767 (Eliminated: 1464 Frozen: 161773)
Constraints : 1230373 (Binary: 91.6% Ternary: 6.5% Other: 2.0%)
Memory Peak : 390MB
Max. Length : 35 steps
Models : 1
[endof: stats after solve call]
Solving Time: 17.68s
Memory: 362MB (+14MB)
UNKNOWN
Iteration Time: 18.29s
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: 446.0MB
Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time: 0.31s
Memory: 366MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 14
Time : 175.477s (Solving: 167.66s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 175.456s
Choices : 1976070 (Domain: 1888390)
Conflicts : 267225 (Analyzed: 267222)
Restarts : 961 (Average: 278.07 Last: 204)
Model-Level : 147.0
Problems : 14 (Average Length: 24.86 Splits: 0)
Lemmas : 267222 (Deleted: 241788)
Binary : 8210 (Ratio: 3.07%)
Ternary : 1715 (Ratio: 0.64%)
Conflict : 267222 (Average Length: 830.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 267222 (Average: 6.86 Max: 431 Sum: 1833630)
Executed : 267178 (Average: 6.86 Max: 431 Sum: 1832959 Ratio: 99.96%)
Bounded : 44 (Average: 15.25 Max: 37 Sum: 671 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 193343 (Eliminated: 1464 Frozen: 184349)
Constraints : 1403418 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 391MB
Max. Length : 40 steps
Models : 1
[endof: stats after solve call]
Solving Time: 16.67s
Memory: 389MB (+23MB)
UNKNOWN
Iteration Time: 17.18s
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: 473.0MB
Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time: 0.32s
Memory: 389MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 15
Time : 193.509s (Solving: 184.81s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 193.496s
Choices : 2212664 (Domain: 2122911)
Conflicts : 295414 (Analyzed: 295411)
Restarts : 1061 (Average: 278.43 Last: 204)
Model-Level : 147.0
Problems : 15 (Average Length: 26.67 Splits: 0)
Lemmas : 295411 (Deleted: 268828)
Binary : 8624 (Ratio: 2.92%)
Ternary : 1761 (Ratio: 0.60%)
Conflict : 295411 (Average Length: 827.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 295411 (Average: 6.94 Max: 431 Sum: 2050016)
Executed : 295365 (Average: 6.94 Max: 431 Sum: 2049241 Ratio: 99.96%)
Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 Ratio: 0.04%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 215919 (Eliminated: 1464 Frozen: 206925)
Constraints : 1576463 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 419MB
Max. Length : 45 steps
Models : 1
[endof: stats after solve call]
Solving Time: 17.51s
Memory: 403MB (+14MB)
UNKNOWN
Iteration Time: 18.05s
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: 487.0MB
Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time: 0.32s
Memory: 403MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 16
Time : 212.232s (Solving: 202.65s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 212.228s
Choices : 2583279 (Domain: 2479786)
Conflicts : 323565 (Analyzed: 323562)
Restarts : 1161 (Average: 278.69 Last: 204)
Model-Level : 147.0
Problems : 16 (Average Length: 28.56 Splits: 0)
Lemmas : 323562 (Deleted: 295387)
Binary : 9565 (Ratio: 2.96%)
Ternary : 1916 (Ratio: 0.59%)
Conflict : 323562 (Average Length: 836.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 323562 (Average: 7.38 Max: 431 Sum: 2387890)
Executed : 323516 (Average: 7.38 Max: 431 Sum: 2387115 Ratio: 99.97%)
Bounded : 46 (Average: 16.85 Max: 52 Sum: 775 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 238495 (Eliminated: 1464 Frozen: 229501)
Constraints : 1749480 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 437MB
Max. Length : 50 steps
Models : 1
[endof: stats after solve call]
Solving Time: 18.21s
Memory: 417MB (+14MB)
UNKNOWN
Iteration Time: 18.74s
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: 501.0MB
Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
Grounding Time: 0.36s
Memory: 417MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 17
Time : 231.016s (Solving: 220.49s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 231.020s
Choices : 2835214 (Domain: 2730967)
Conflicts : 351769 (Analyzed: 351766)
Restarts : 1261 (Average: 278.96 Last: 204)
Model-Level : 147.0
Problems : 17 (Average Length: 30.53 Splits: 0)
Lemmas : 351766 (Deleted: 322486)
Binary : 9951 (Ratio: 2.83%)
Ternary : 1978 (Ratio: 0.56%)
Conflict : 351766 (Average Length: 825.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 351766 (Average: 7.44 Max: 431 Sum: 2618009)
Executed : 351719 (Average: 7.44 Max: 431 Sum: 2617172 Ratio: 99.97%)
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 261071 (Eliminated: 1464 Frozen: 252077)
Constraints : 1922525 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 454MB
Max. Length : 55 steps
Models : 1
[endof: stats after solve call]
Solving Time: 18.21s
Memory: 432MB (+15MB)
UNKNOWN
Iteration Time: 18.80s
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: 516.0MB
Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
Grounding Time: 0.35s
Memory: 432MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 18
Time : 251.557s (Solving: 240.07s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 251.568s
Choices : 3279607 (Domain: 3169584)
Conflicts : 379925 (Analyzed: 379922)
Restarts : 1361 (Average: 279.15 Last: 204)
Model-Level : 147.0
Problems : 18 (Average Length: 32.56 Splits: 0)
Lemmas : 379922 (Deleted: 348956)
Binary : 11063 (Ratio: 2.91%)
Ternary : 2142 (Ratio: 0.56%)
Conflict : 379922 (Average Length: 826.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 379922 (Average: 7.96 Max: 431 Sum: 3025976)
Executed : 379875 (Average: 7.96 Max: 431 Sum: 3025139 Ratio: 99.97%)
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 283647 (Eliminated: 1464 Frozen: 274653)
Constraints : 2095556 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 471MB
Max. Length : 60 steps
Models : 1
[endof: stats after solve call]
Solving Time: 19.96s
Memory: 465MB (+33MB)
UNKNOWN
Iteration Time: 20.56s
Iteration 18
Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until: 65
Expected Memory: 549.0MB
Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
Grounding Time: 0.33s
Memory: 465MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 19
Time : 273.683s (Solving: 261.27s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 273.704s
Choices : 3620280 (Domain: 3509710)
Conflicts : 408106 (Analyzed: 408103)
Restarts : 1461 (Average: 279.33 Last: 204)
Model-Level : 147.0
Problems : 19 (Average Length: 34.63 Splits: 0)
Lemmas : 408103 (Deleted: 375917)
Binary : 11570 (Ratio: 2.84%)
Ternary : 2226 (Ratio: 0.55%)
Conflict : 408103 (Average Length: 829.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 408103 (Average: 8.18 Max: 431 Sum: 3337540)
Executed : 408056 (Average: 8.18 Max: 431 Sum: 3336703 Ratio: 99.97%)
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.03%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 306223 (Eliminated: 1464 Frozen: 297229)
Constraints : 2268601 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 503MB
Max. Length : 65 steps
Models : 1
[endof: stats after solve call]
Solving Time: 21.57s
Memory: 477MB (+12MB)
UNKNOWN
Iteration Time: 22.14s
Iteration 19
Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True)]
Grounded Until: 70
Expected Memory: 561.0MB
Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
Grounding Time: 0.34s
Memory: 477MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 20
Time : 294.476s (Solving: 281.11s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 294.504s
Choices : 4030873 (Domain: 3916810)
Conflicts : 436313 (Analyzed: 436310)
Restarts : 1561 (Average: 279.51 Last: 204)
Model-Level : 147.0
Problems : 20 (Average Length: 36.75 Splits: 0)
Lemmas : 436310 (Deleted: 401371)
Binary : 12272 (Ratio: 2.81%)
Ternary : 2334 (Ratio: 0.53%)
Conflict : 436310 (Average Length: 833.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 436310 (Average: 8.51 Max: 431 Sum: 3714399)
Executed : 436263 (Average: 8.51 Max: 431 Sum: 3713562 Ratio: 99.98%)
Bounded : 47 (Average: 17.81 Max: 62 Sum: 837 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 328799 (Eliminated: 1464 Frozen: 319805)
Constraints : 2441646 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 518MB
Max. Length : 70 steps
Models : 1
[endof: stats after solve call]
Solving Time: 20.23s
Memory: 492MB (+15MB)
UNKNOWN
Iteration Time: 20.81s
Iteration 20
Queue: [(16,80,0,True), (17,85,0,True)]
Grounded Until: 75
Expected Memory: 576.0MB
Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
Grounding Time: 0.48s
Memory: 507MB (+15MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 21
Time : 316.121s (Solving: 301.64s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 316.156s
Choices : 4363980 (Domain: 4249676)
Conflicts : 464504 (Analyzed: 464501)
Restarts : 1661 (Average: 279.65 Last: 204)
Model-Level : 147.0
Problems : 21 (Average Length: 38.90 Splits: 0)
Lemmas : 464501 (Deleted: 429631)
Binary : 12709 (Ratio: 2.74%)
Ternary : 2409 (Ratio: 0.52%)
Conflict : 464501 (Average Length: 830.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 464501 (Average: 8.65 Max: 431 Sum: 4016299)
Executed : 464453 (Average: 8.64 Max: 431 Sum: 4015380 Ratio: 99.98%)
Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 351375 (Eliminated: 1464 Frozen: 342381)
Constraints : 2614691 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 554MB
Max. Length : 75 steps
Models : 1
[endof: stats after solve call]
Solving Time: 20.92s
Memory: 521MB (+14MB)
UNKNOWN
Iteration Time: 21.66s
Iteration 21
Queue: [(17,85,0,True)]
Grounded Until: 80
Expected Memory: 605.0MB
Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
Grounding Time: 0.32s
Memory: 521MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 22
Time : 339.079s (Solving: 323.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 339.124s
Choices : 4698272 (Domain: 4583605)
Conflicts : 492648 (Analyzed: 492645)
Restarts : 1761 (Average: 279.75 Last: 204)
Model-Level : 147.0
Problems : 22 (Average Length: 41.09 Splits: 0)
Lemmas : 492645 (Deleted: 456973)
Binary : 13120 (Ratio: 2.66%)
Ternary : 2458 (Ratio: 0.50%)
Conflict : 492645 (Average Length: 839.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 492645 (Average: 8.75 Max: 431 Sum: 4309179)
Executed : 492597 (Average: 8.75 Max: 431 Sum: 4308260 Ratio: 99.98%)
Bounded : 48 (Average: 19.15 Max: 82 Sum: 919 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 364957)
Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 80 steps
Models : 1
[endof: stats after solve call]
Solving Time: 22.39s
Memory: 535MB (+14MB)
UNKNOWN
Iteration Time: 22.97s
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 : 350.517s (Solving: 334.98s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 350.568s
Choices : 4813255 (Domain: 4698588)
Conflicts : 520838 (Analyzed: 520835)
Restarts : 1861 (Average: 279.87 Last: 204)
Model-Level : 147.0
Problems : 23 (Average Length: 43.09 Splits: 0)
Lemmas : 520835 (Deleted: 484258)
Binary : 13398 (Ratio: 2.57%)
Ternary : 2506 (Ratio: 0.48%)
Conflict : 520835 (Average Length: 826.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 520835 (Average: 8.48 Max: 431 Sum: 4417398)
Executed : 520786 (Average: 8.48 Max: 431 Sum: 4416392 Ratio: 99.98%)
Bounded : 49 (Average: 20.53 Max: 87 Sum: 1006 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787722 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 11.41s
Memory: 537MB (+2MB)
UNKNOWN
Iteration Time: 11.45s
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 : 376.151s (Solving: 360.52s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 376.216s
Choices : 4911678 (Domain: 4797011)
Conflicts : 548996 (Analyzed: 548993)
Restarts : 1961 (Average: 279.96 Last: 204)
Model-Level : 147.0
Problems : 24 (Average Length: 44.92 Splits: 0)
Lemmas : 548993 (Deleted: 511889)
Binary : 13480 (Ratio: 2.46%)
Ternary : 2531 (Ratio: 0.46%)
Conflict : 548993 (Average Length: 846.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 548993 (Average: 8.21 Max: 431 Sum: 4506436)
Executed : 548943 (Average: 8.21 Max: 431 Sum: 4505343 Ratio: 99.98%)
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787708 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 25.61s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 25.65s
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 : 395.354s (Solving: 379.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 395.428s
Choices : 5101516 (Domain: 4986849)
Conflicts : 577235 (Analyzed: 577232)
Restarts : 2061 (Average: 280.07 Last: 204)
Model-Level : 147.0
Problems : 25 (Average Length: 46.60 Splits: 0)
Lemmas : 577232 (Deleted: 539550)
Binary : 13703 (Ratio: 2.37%)
Ternary : 2558 (Ratio: 0.44%)
Conflict : 577232 (Average Length: 861.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 577232 (Average: 8.11 Max: 431 Sum: 4678791)
Executed : 577182 (Average: 8.10 Max: 431 Sum: 4677698 Ratio: 99.98%)
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 19.18s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 19.22s
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 : 413.248s (Solving: 397.41s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 413.328s
Choices : 5288141 (Domain: 5173473)
Conflicts : 605398 (Analyzed: 605395)
Restarts : 2161 (Average: 280.15 Last: 204)
Model-Level : 147.0
Problems : 26 (Average Length: 48.15 Splits: 0)
Lemmas : 605395 (Deleted: 566903)
Binary : 13934 (Ratio: 2.30%)
Ternary : 2601 (Ratio: 0.43%)
Conflict : 605395 (Average Length: 864.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 605395 (Average: 8.01 Max: 431 Sum: 4847208)
Executed : 605345 (Average: 8.00 Max: 431 Sum: 4846115 Ratio: 99.98%)
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 17.85s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 17.90s
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 : 434.403s (Solving: 418.46s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 434.492s
Choices : 5485373 (Domain: 5370691)
Conflicts : 633582 (Analyzed: 633579)
Restarts : 2261 (Average: 280.22 Last: 204)
Model-Level : 147.0
Problems : 27 (Average Length: 49.59 Splits: 0)
Lemmas : 633579 (Deleted: 594155)
Binary : 14225 (Ratio: 2.25%)
Ternary : 2658 (Ratio: 0.42%)
Conflict : 633579 (Average Length: 875.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 633579 (Average: 7.93 Max: 431 Sum: 5022002)
Executed : 633529 (Average: 7.92 Max: 431 Sum: 5020909 Ratio: 99.98%)
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 21.12s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 21.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 : 451.839s (Solving: 435.81s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 451.932s
Choices : 5700364 (Domain: 5584170)
Conflicts : 661765 (Analyzed: 661762)
Restarts : 2361 (Average: 280.29 Last: 204)
Model-Level : 147.0
Problems : 28 (Average Length: 50.93 Splits: 0)
Lemmas : 661762 (Deleted: 621439)
Binary : 14657 (Ratio: 2.21%)
Ternary : 2708 (Ratio: 0.41%)
Conflict : 661762 (Average Length: 872.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 661762 (Average: 7.88 Max: 431 Sum: 5212706)
Executed : 661712 (Average: 7.88 Max: 431 Sum: 5211613 Ratio: 99.98%)
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 17.41s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 17.45s
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 : 468.754s (Solving: 452.63s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 468.856s
Choices : 5892645 (Domain: 5776369)
Conflicts : 689962 (Analyzed: 689959)
Restarts : 2461 (Average: 280.36 Last: 204)
Model-Level : 147.0
Problems : 29 (Average Length: 52.17 Splits: 0)
Lemmas : 689959 (Deleted: 647517)
Binary : 14908 (Ratio: 2.16%)
Ternary : 2759 (Ratio: 0.40%)
Conflict : 689959 (Average Length: 871.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 689959 (Average: 7.80 Max: 431 Sum: 5382814)
Executed : 689909 (Average: 7.80 Max: 431 Sum: 5381721 Ratio: 99.98%)
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 16.89s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 16.93s
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 : 489.515s (Solving: 473.27s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 489.628s
Choices : 6121052 (Domain: 6004694)
Conflicts : 718096 (Analyzed: 718093)
Restarts : 2561 (Average: 280.40 Last: 204)
Model-Level : 147.0
Problems : 30 (Average Length: 53.33 Splits: 0)
Lemmas : 718093 (Deleted: 676101)
Binary : 15186 (Ratio: 2.11%)
Ternary : 2806 (Ratio: 0.39%)
Conflict : 718093 (Average Length: 878.1 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 718093 (Average: 7.78 Max: 431 Sum: 5583729)
Executed : 718043 (Average: 7.77 Max: 431 Sum: 5582636 Ratio: 99.98%)
Bounded : 50 (Average: 21.86 Max: 87 Sum: 1093 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 20.72s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 20.77s
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 : 508.521s (Solving: 492.15s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 508.640s
Choices : 6340515 (Domain: 6223979)
Conflicts : 746262 (Analyzed: 746259)
Restarts : 2661 (Average: 280.44 Last: 204)
Model-Level : 147.0
Problems : 31 (Average Length: 54.42 Splits: 0)
Lemmas : 746259 (Deleted: 703489)
Binary : 15397 (Ratio: 2.06%)
Ternary : 2842 (Ratio: 0.38%)
Conflict : 746259 (Average Length: 881.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 746259 (Average: 7.74 Max: 431 Sum: 5774391)
Executed : 746208 (Average: 7.74 Max: 431 Sum: 5773211 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787694 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 18.96s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 19.02s
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 : 527.510s (Solving: 511.05s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 527.636s
Choices : 6600559 (Domain: 6482924)
Conflicts : 774478 (Analyzed: 774475)
Restarts : 2761 (Average: 280.51 Last: 204)
Model-Level : 147.0
Problems : 32 (Average Length: 55.44 Splits: 0)
Lemmas : 774475 (Deleted: 730698)
Binary : 15878 (Ratio: 2.05%)
Ternary : 2908 (Ratio: 0.38%)
Conflict : 774475 (Average Length: 883.2 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 774475 (Average: 7.75 Max: 431 Sum: 6000830)
Executed : 774424 (Average: 7.75 Max: 431 Sum: 5999650 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 18.96s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 19.00s
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 : 547.765s (Solving: 531.21s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 547.900s
Choices : 6914199 (Domain: 6794643)
Conflicts : 802630 (Analyzed: 802627)
Restarts : 2861 (Average: 280.54 Last: 204)
Model-Level : 147.0
Problems : 33 (Average Length: 56.39 Splits: 0)
Lemmas : 802627 (Deleted: 757893)
Binary : 16327 (Ratio: 2.03%)
Ternary : 2968 (Ratio: 0.37%)
Conflict : 802627 (Average Length: 885.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 802627 (Average: 7.82 Max: 431 Sum: 6279139)
Executed : 802576 (Average: 7.82 Max: 431 Sum: 6277959 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 20.22s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 20.27s
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 : 568.390s (Solving: 551.74s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 568.536s
Choices : 7151395 (Domain: 7031757)
Conflicts : 830822 (Analyzed: 830819)
Restarts : 2961 (Average: 280.59 Last: 204)
Model-Level : 147.0
Problems : 34 (Average Length: 57.29 Splits: 0)
Lemmas : 830819 (Deleted: 785308)
Binary : 16566 (Ratio: 1.99%)
Ternary : 3004 (Ratio: 0.36%)
Conflict : 830819 (Average Length: 889.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 830819 (Average: 7.81 Max: 431 Sum: 6485634)
Executed : 830768 (Average: 7.80 Max: 431 Sum: 6484454 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 20.60s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 20.64s
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 : 589.267s (Solving: 572.51s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 589.420s
Choices : 7441227 (Domain: 7316328)
Conflicts : 858998 (Analyzed: 858995)
Restarts : 3061 (Average: 280.63 Last: 204)
Model-Level : 147.0
Problems : 35 (Average Length: 58.14 Splits: 0)
Lemmas : 858995 (Deleted: 812298)
Binary : 17110 (Ratio: 1.99%)
Ternary : 3091 (Ratio: 0.36%)
Conflict : 858995 (Average Length: 892.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 858995 (Average: 7.85 Max: 431 Sum: 6741586)
Executed : 858944 (Average: 7.85 Max: 431 Sum: 6740406 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 20.85s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 20.89s
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 : 611.139s (Solving: 594.28s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 611.300s
Choices : 7717670 (Domain: 7592616)
Conflicts : 887211 (Analyzed: 887208)
Restarts : 3161 (Average: 280.67 Last: 204)
Model-Level : 147.0
Problems : 36 (Average Length: 58.94 Splits: 0)
Lemmas : 887208 (Deleted: 839899)
Binary : 17380 (Ratio: 1.96%)
Ternary : 3137 (Ratio: 0.35%)
Conflict : 887208 (Average Length: 893.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 887208 (Average: 7.87 Max: 493 Sum: 6983010)
Executed : 887157 (Average: 7.87 Max: 493 Sum: 6981830 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 373951 (Eliminated: 1464 Frozen: 372487)
Constraints : 2787687 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 570MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 21.84s
Memory: 537MB (+0MB)
UNKNOWN
Iteration Time: 21.88s
Iteration 36
Queue: [(18,90,0,True), (19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 85
Expected Memory: 621.0MB
Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
Grounding Time: 0.32s
Memory: 537MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 37
Time : 632.985s (Solving: 615.15s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 633.156s
Choices : 7997616 (Domain: 7872364)
Conflicts : 915441 (Analyzed: 915438)
Restarts : 3261 (Average: 280.72 Last: 204)
Model-Level : 147.0
Problems : 37 (Average Length: 59.84 Splits: 0)
Lemmas : 915438 (Deleted: 867282)
Binary : 17707 (Ratio: 1.93%)
Ternary : 3182 (Ratio: 0.35%)
Conflict : 915438 (Average Length: 893.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 915438 (Average: 7.89 Max: 493 Sum: 7226121)
Executed : 915387 (Average: 7.89 Max: 493 Sum: 7224941 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 396527 (Eliminated: 1464 Frozen: 387533)
Constraints : 2960732 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 587MB
Max. Length : 85 steps
Models : 1
[endof: stats after solve call]
Solving Time: 21.26s
Memory: 549MB (+12MB)
UNKNOWN
Iteration Time: 21.86s
Iteration 37
Queue: [(19,95,0,True), (20,100,0,True), (21,105,0,True)]
Grounded Until: 90
Expected Memory: 633.0MB
Grounding... [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
Grounding Time: 0.32s
Memory: 549MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 38
Time : 654.789s (Solving: 635.95s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 654.972s
Choices : 8272236 (Domain: 8146669)
Conflicts : 943641 (Analyzed: 943638)
Restarts : 3361 (Average: 280.76 Last: 204)
Model-Level : 147.0
Problems : 38 (Average Length: 60.82 Splits: 0)
Lemmas : 943638 (Deleted: 894728)
Binary : 17930 (Ratio: 1.90%)
Ternary : 3210 (Ratio: 0.34%)
Conflict : 943638 (Average Length: 889.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 943638 (Average: 7.92 Max: 493 Sum: 7469400)
Executed : 943587 (Average: 7.91 Max: 493 Sum: 7468220 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 419103 (Eliminated: 1464 Frozen: 410109)
Constraints : 3133777 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 607MB
Max. Length : 90 steps
Models : 1
[endof: stats after solve call]
Solving Time: 21.20s
Memory: 596MB (+47MB)
UNKNOWN
Iteration Time: 21.82s
Iteration 38
Queue: [(20,100,0,True), (21,105,0,True)]
Grounded Until: 95
Expected Memory: 680.0MB
Grounding... [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
Grounding Time: 0.33s
Memory: 596MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 39
Time : 678.370s (Solving: 658.52s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 678.564s
Choices : 8579392 (Domain: 8453731)
Conflicts : 971840 (Analyzed: 971837)
Restarts : 3461 (Average: 280.80 Last: 204)
Model-Level : 147.0
Problems : 39 (Average Length: 61.87 Splits: 0)
Lemmas : 971837 (Deleted: 922125)
Binary : 18257 (Ratio: 1.88%)
Ternary : 3262 (Ratio: 0.34%)
Conflict : 971837 (Average Length: 888.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 971837 (Average: 7.96 Max: 493 Sum: 7736535)
Executed : 971786 (Average: 7.96 Max: 493 Sum: 7735355 Ratio: 99.98%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.02%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 441679 (Eliminated: 1464 Frozen: 432685)
Constraints : 3306822 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 650MB
Max. Length : 95 steps
Models : 1
[endof: stats after solve call]
Solving Time: 22.97s
Memory: 612MB (+16MB)
UNKNOWN
Iteration Time: 23.60s
Iteration 39
Queue: [(21,105,0,True)]
Grounded Until: 100
Expected Memory: 696.0MB
Grounding... [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
Grounding Time: 0.32s
Memory: 612MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]
Models : 0+
Calls : 40
Time : 700.801s (Solving: 679.93s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 701.004s
Choices : 8853119 (Domain: 8727423)
Conflicts : 1000007 (Analyzed: 1000004)
Restarts : 3561 (Average: 280.82 Last: 204)
Model-Level : 147.0
Problems : 40 (Average Length: 63.00 Splits: 0)
Lemmas : 1000004 (Deleted: 946111)
Binary : 18417 (Ratio: 1.84%)
Ternary : 3291 (Ratio: 0.33%)
Conflict : 1000004 (Average Length: 887.8 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1000004 (Average: 7.97 Max: 493 Sum: 7973347)
Executed : 999953 (Average: 7.97 Max: 493 Sum: 7972167 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 455261)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 669MB
Max. Length : 100 steps
Models : 1
[endof: stats after solve call]
Solving Time: 21.82s
Memory: 616MB (+4MB)
UNKNOWN
Iteration Time: 22.45s
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 : 713.054s (Solving: 692.05s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 713.264s
Choices : 9003898 (Domain: 8878202)
Conflicts : 1028184 (Analyzed: 1028181)
Restarts : 3661 (Average: 280.85 Last: 204)
Model-Level : 147.0
Problems : 41 (Average Length: 64.07 Splits: 0)
Lemmas : 1028181 (Deleted: 977173)
Binary : 18547 (Ratio: 1.80%)
Ternary : 3325 (Ratio: 0.32%)
Conflict : 1028181 (Average Length: 876.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1028181 (Average: 7.89 Max: 493 Sum: 8117468)
Executed : 1028130 (Average: 7.89 Max: 493 Sum: 8116288 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 669MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 12.20s
Memory: 616MB (+0MB)
UNKNOWN
Iteration Time: 12.26s
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 : 738.564s (Solving: 717.46s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 738.784s
Choices : 9105606 (Domain: 8979910)
Conflicts : 1056370 (Analyzed: 1056367)
Restarts : 3761 (Average: 280.87 Last: 204)
Model-Level : 147.0
Problems : 42 (Average Length: 65.10 Splits: 0)
Lemmas : 1056367 (Deleted: 1004871)
Binary : 18597 (Ratio: 1.76%)
Ternary : 3363 (Ratio: 0.32%)
Conflict : 1056367 (Average Length: 876.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1056367 (Average: 7.77 Max: 493 Sum: 8209915)
Executed : 1056316 (Average: 7.77 Max: 493 Sum: 8208735 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 669MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 25.48s
Memory: 616MB (+0MB)
UNKNOWN
Iteration Time: 25.52s
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 : 764.452s (Solving: 743.24s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 764.680s
Choices : 9282110 (Domain: 9156414)
Conflicts : 1084555 (Analyzed: 1084552)
Restarts : 3861 (Average: 280.90 Last: 204)
Model-Level : 147.0
Problems : 43 (Average Length: 66.07 Splits: 0)
Lemmas : 1084552 (Deleted: 1032580)
Binary : 18721 (Ratio: 1.73%)
Ternary : 3384 (Ratio: 0.31%)
Conflict : 1084552 (Average Length: 891.5 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1084552 (Average: 7.72 Max: 493 Sum: 8370316)
Executed : 1084501 (Average: 7.72 Max: 493 Sum: 8369136 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 25.86s
Memory: 680MB (+64MB)
UNKNOWN
Iteration Time: 25.90s
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 : 784.115s (Solving: 762.79s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 784.352s
Choices : 9451213 (Domain: 9325517)
Conflicts : 1112727 (Analyzed: 1112724)
Restarts : 3961 (Average: 280.92 Last: 204)
Model-Level : 147.0
Problems : 44 (Average Length: 67.00 Splits: 0)
Lemmas : 1112724 (Deleted: 1060159)
Binary : 18869 (Ratio: 1.70%)
Ternary : 3425 (Ratio: 0.31%)
Conflict : 1112724 (Average Length: 894.9 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1112724 (Average: 7.66 Max: 493 Sum: 8519634)
Executed : 1112673 (Average: 7.66 Max: 493 Sum: 8518454 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 19.63s
Memory: 680MB (+0MB)
UNKNOWN
Iteration Time: 19.67s
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 : 803.797s (Solving: 782.37s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 804.040s
Choices : 9629811 (Domain: 9504115)
Conflicts : 1140953 (Analyzed: 1140950)
Restarts : 4061 (Average: 280.95 Last: 204)
Model-Level : 147.0
Problems : 45 (Average Length: 67.89 Splits: 0)
Lemmas : 1140950 (Deleted: 1087827)
Binary : 19015 (Ratio: 1.67%)
Ternary : 3450 (Ratio: 0.30%)
Conflict : 1140950 (Average Length: 897.3 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1140950 (Average: 7.60 Max: 493 Sum: 8675794)
Executed : 1140899 (Average: 7.60 Max: 493 Sum: 8674614 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 19.65s
Memory: 680MB (+0MB)
UNKNOWN
Iteration Time: 19.69s
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 : 825.313s (Solving: 803.76s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 825.564s
Choices : 9823417 (Domain: 9697580)
Conflicts : 1169150 (Analyzed: 1169147)
Restarts : 4161 (Average: 280.98 Last: 204)
Model-Level : 147.0
Problems : 46 (Average Length: 68.74 Splits: 0)
Lemmas : 1169147 (Deleted: 1115335)
Binary : 19295 (Ratio: 1.65%)
Ternary : 3485 (Ratio: 0.30%)
Conflict : 1169147 (Average Length: 904.0 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1169147 (Average: 7.56 Max: 493 Sum: 8842595)
Executed : 1169096 (Average: 7.56 Max: 493 Sum: 8841415 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 21.47s
Memory: 680MB (+0MB)
UNKNOWN
Iteration Time: 21.53s
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 : 844.567s (Solving: 822.91s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 844.828s
Choices : 10033085 (Domain: 9907237)
Conflicts : 1197341 (Analyzed: 1197338)
Restarts : 4261 (Average: 281.00 Last: 204)
Model-Level : 147.0
Problems : 47 (Average Length: 69.55 Splits: 0)
Lemmas : 1197338 (Deleted: 1142902)
Binary : 19440 (Ratio: 1.62%)
Ternary : 3518 (Ratio: 0.29%)
Conflict : 1197338 (Average Length: 903.7 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1197338 (Average: 7.54 Max: 493 Sum: 9026213)
Executed : 1197287 (Average: 7.54 Max: 493 Sum: 9025033 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 19.22s
Memory: 680MB (+0MB)
UNKNOWN
Iteration Time: 19.26s
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 : 863.330s (Solving: 841.57s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 863.600s
Choices : 10251284 (Domain: 10125432)
Conflicts : 1225502 (Analyzed: 1225499)
Restarts : 4361 (Average: 281.01 Last: 204)
Model-Level : 147.0
Problems : 48 (Average Length: 70.33 Splits: 0)
Lemmas : 1225499 (Deleted: 1170396)
Binary : 19701 (Ratio: 1.61%)
Ternary : 3549 (Ratio: 0.29%)
Conflict : 1225499 (Average Length: 904.6 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1225499 (Average: 7.52 Max: 493 Sum: 9214105)
Executed : 1225448 (Average: 7.52 Max: 493 Sum: 9212925 Ratio: 99.99%)
Bounded : 51 (Average: 23.14 Max: 87 Sum: 1180 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 18.73s
Memory: 680MB (+0MB)
UNKNOWN
Iteration Time: 18.77s
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 : 881.523s (Solving: 859.66s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 881.800s
Choices : 10489316 (Domain: 10363047)
Conflicts : 1253686 (Analyzed: 1253683)
Restarts : 4461 (Average: 281.03 Last: 204)
Model-Level : 147.0
Problems : 49 (Average Length: 71.08 Splits: 0)
Lemmas : 1253683 (Deleted: 1197683)
Binary : 19958 (Ratio: 1.59%)
Ternary : 3584 (Ratio: 0.29%)
Conflict : 1253683 (Average Length: 903.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1253683 (Average: 7.51 Max: 493 Sum: 9421101)
Executed : 1253631 (Average: 7.51 Max: 493 Sum: 9419814 Ratio: 99.99%)
Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479867 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1
[endof: stats after solve call]
Solving Time: 18.16s
Memory: 680MB (+0MB)
UNKNOWN
Iteration Time: 18.20s
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...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN
INTERRUPTED : 1
Models : 0+
Calls : 50
Time : 900.347s (Solving: 878.37s 1st Model: 0.00s Unsat: 4.20s)
CPU Time : 900.616s
Choices : 10729648 (Domain: 10602630)
Conflicts : 1281834 (Analyzed: 1281831)
Restarts : 4561 (Average: 281.04 Last: 204)
Model-Level : 147.0
Problems : 50 (Average Length: 71.80 Splits: 0)
Lemmas : 1281831 (Deleted: 1225188)
Binary : 20176 (Ratio: 1.57%)
Ternary : 3624 (Ratio: 0.28%)
Conflict : 1281831 (Average Length: 903.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 1281831 (Average: 7.51 Max: 493 Sum: 9629023)
Executed : 1281779 (Average: 7.51 Max: 493 Sum: 9627736 Ratio: 99.99%)
Bounded : 52 (Average: 24.75 Max: 107 Sum: 1287 Ratio: 0.01%)
Rules : 55133 (Original: 53913)
Atoms : 43853
Bodies : 10280 (Original: 9059)
Count : 232 (Original: 476)
Equivalences : 2929 (Atom=Atom: 57 Body=Body: 0 Other: 2872)
Tight : Yes
Variables : 464255 (Eliminated: 1464 Frozen: 462791)
Constraints : 3479853 (Binary: 91.6% Ternary: 6.5% Other: 1.9%)
Memory Peak : 744MB
Max. Length : 105 steps
Models : 1