diff --git a/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.env b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.env new file mode 100644 index 000000000..656f0547b --- /dev/null +++ b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.env @@ -0,0 +1,59 @@ +command: +- timeout +- -m=9216000 +- -t=900 +- python3 +- /home/pluehne/Documents/ASP/plasp-javier/encodings/planner/runplanner.py +- --domain=/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-10.pddl +- --stats +- --stats-iter +- --verbose +- --print-call +- -m 8192 +- --translate +- -B 0.9 +- --parallel=0 +- --shallow +- --use-heuristic +- --test-until-not-sat +- --test=0 +- --test-add=1 +- --test-times=1 +- --configuration=trendy +- -i 0 +configuration: + id: gc-ta1-tt1-trendy + instanceSets: + - rintanen-aij-2012-interesting + options: + - --stats + - --stats-iter + - --verbose + - --print-call + - -m 8192 + - --translate + - -B 0.9 + - --parallel=0 + - --shallow + - --use-heuristic + - --test-until-not-sat + - --test=0 + - --test-add=1 + - --test-times=1 + - --configuration=trendy + - -i 0 +exitCode: 0 +instance: + domain: barman-sequential-satisficing + instance: 10 + ipc: ipc-2011 + planLength: null +versions: + clingo: 5.2.2 + fastDownward: 10997:847cdf0069cab0c8841a9958e783d1a7340fe2e9 (2017-11-02 15:10 +0100) + planner: f090434475c02dbccc3811039498f2a63a357ddc (2018-02-01 18:15:39 +0100) + plasp: 3.1.1 + python: 3.6.3 +workingDirectory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner + diff --git a/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.err b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.err new file mode 100644 index 000000000..bc34694c6 --- /dev/null +++ b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.err @@ -0,0 +1,8 @@ +# configuration: {'id': 'gc-ta1-tt1-trendy', 'options': ['--stats', '--stats-iter', '--verbose', '--print-call', '-m 8192', '--translate', '-B 0.9', '--parallel=0', '--shallow', '--use-heuristic', '--test-until-not-sat', '--test=0', '--test-add=1', '--test-times=1', '--configuration=trendy', '-i 0'], 'instanceSets': ['rintanen-aij-2012-interesting']} +# instance: {'ipc': 'ipc-2011', 'domain': 'barman-sequential-satisficing', 'instance': 10, 'planLength': None} +# command: ['timeout', '-m=9216000', '-t=900', 'python3', '/home/pluehne/Documents/ASP/plasp-javier/encodings/planner/runplanner.py', '--domain=/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-10.pddl', '--stats', '--stats-iter', '--verbose', '--print-call', '-m 8192', '--translate', '-B 0.9', '--parallel=0', '--shallow', '--use-heuristic', '--test-until-not-sat', '--test=0', '--test-add=1', '--test-times=1', '--configuration=trendy', '-i 0'] +# working directory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner +# exit code: 0 +TIMEOUT CPU 900.09 MEM 956892 MAXMEM 975692 STALE 1 MAXMEM_RSS 832408 + + diff --git a/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.out b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.out new file mode 100644 index 000000000..dac66d19f --- /dev/null +++ b/gc-ta1-tt1-trendy/ipc-2011_barman-sequential-satisficing_10.out @@ -0,0 +1,1193 @@ +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-10.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-10.pddl +Parsing... +Parsing: [0.040s CPU, 0.046s wall-clock] +Normalizing task... [0.010s CPU, 0.004s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.012s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.050s CPU, 0.054s wall-clock] +Preparing model... [0.030s CPU, 0.029s wall-clock] +Generated 115 rules. +Computing model... [0.460s CPU, 0.454s wall-clock] +2784 relevant atoms +2893 auxiliary atoms +5677 final queue length +9793 total queue pushes +Completing instantiation... [0.860s CPU, 0.861s wall-clock] +Instantiating: [1.420s CPU, 1.417s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.120s CPU, 0.122s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.000s CPU, 0.008s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] +Choosing groups... +292 uncovered facts +Choosing groups: [0.000s CPU, 0.002s wall-clock] +Building translation key... [0.010s CPU, 0.011s wall-clock] +Computing fact groups: [0.160s CPU, 0.168s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] +Building dictionary for full mutex groups... [0.010s CPU, 0.005s wall-clock] +Building mutex information... +Building mutex information: [0.000s CPU, 0.003s wall-clock] +Translating task... +Processing axioms... +Simplifying axioms... [0.000s CPU, 0.000s wall-clock] +Processing axioms: [0.050s CPU, 0.046s wall-clock] +Translating task: [0.890s CPU, 0.885s wall-clock] +3276 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.430s CPU, 0.433s wall-clock] +Reordering and filtering variables... +295 of 295 variables necessary. +14 of 17 mutex groups necessary. +1958 of 1958 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.310s CPU, 0.302s wall-clock] +Translator variables: 295 +Translator derived variables: 0 +Translator facts: 617 +Translator goal facts: 12 +Translator mutex groups: 14 +Translator total mutex groups size: 42 +Translator operators: 1958 +Translator axioms: 0 +Translator task size: 18764 +Translator peak memory: 47308 KB +Writing output... [0.360s CPU, 0.390s wall-clock] +Done! [3.660s CPU, 3.692s wall-clock] +planner.py version 0.0.1 + +Time: 0.75s +Memory: 101MB + +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.884s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.756s + +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 : 54149 +Atoms : 54149 +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 : 237MB +Max. Length : 0 steps +Models : 0 + +[endof: stats after solve call] +Solving Time: 0.01s +Memory: 173MB (+72MB) +UNSAT +Iteration Time: 0.01s + +Iteration 2 +Queue: [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 0 +Expected Memory: 173MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])] +Grounding Time: 0.23s +Memory: 173MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 2 +Time : 1.399s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.272s + +Choices : 220 (Domain: 94) +Conflicts : 2 (Analyzed: 2) +Restarts : 0 +Model-Level : 212.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: 28.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: 7.50 Max: 14 Sum: 15) + Executed : 2 (Average: 7.50 Max: 14 Sum: 15 Ratio: 100.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + +Rules : 54149 +Atoms : 54149 +Bodies : 1 (Original: 0) +Tight : Yes +Variables : 14506 (Eliminated: 0 Frozen: 14506) +Constraints : 48947 (Binary: 95.2% Ternary: 3.3% Other: 1.4%) + +Memory Peak : 237MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.18s +Memory: 176MB (+3MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 0.76s +Memory: 202MB (+26MB) +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 3 +Time : 1.539s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 1.416s + +Choices : 233 (Domain: 99) +Conflicts : 8 (Analyzed: 7) +Restarts : 0 +Model-Level : 212.0 +Problems : 3 (Average Length: 5.33 Splits: 0) +Lemmas : 7 (Deleted: 0) + Binary : 3 (Ratio: 42.86%) + Ternary : 2 (Ratio: 28.57%) + Conflict : 7 (Average Length: 9.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 7 (Average: 4.43 Max: 14 Sum: 31) + Executed : 4 (Average: 4.00 Max: 14 Sum: 28 Ratio: 90.32%) + Bounded : 3 (Average: 1.00 Max: 1 Sum: 3 Ratio: 9.68%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 17794 (Eliminated: 2052 Frozen: 15742) +Constraints : 68211 (Binary: 90.3% Ternary: 5.8% Other: 3.9%) + +Memory Peak : 237MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.04s +Memory: 202MB (+0MB) +UNSAT +Iteration Time: 1.32s + +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: 205.0MB +Grounding... [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])] +Grounding Time: 0.46s +Memory: 202MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 4 +Time : 3.192s (Solving: 0.48s 1st Model: 0.00s Unsat: 0.48s) +CPU Time : 3.072s + +Choices : 22339 (Domain: 15348) +Conflicts : 1931 (Analyzed: 1929) +Restarts : 6 (Average: 321.50 Last: 609) +Model-Level : 212.0 +Problems : 4 (Average Length: 7.00 Splits: 0) +Lemmas : 1929 (Deleted: 0) + Binary : 256 (Ratio: 13.27%) + Ternary : 256 (Ratio: 13.27%) + Conflict : 1929 (Average Length: 47.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1929 (Average: 11.51 Max: 138 Sum: 22198) + Executed : 1903 (Average: 11.37 Max: 138 Sum: 21930 Ratio: 98.79%) + Bounded : 26 (Average: 10.31 Max: 12 Sum: 268 Ratio: 1.21%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 50740 (Eliminated: 2052 Frozen: 36958) +Constraints : 317796 (Binary: 91.1% Ternary: 6.7% Other: 2.3%) + +Memory Peak : 237MB +Max. Length : 5 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 1.03s +Memory: 216MB (+14MB) +UNSAT +Iteration Time: 1.66s + +Iteration 4 +Queue: [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 10 +Expected Memory: 230.0MB +Grounding... [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])] +Grounding Time: 0.43s +Memory: 223MB (+7MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 5 +Time : 10.060s (Solving: 6.19s 1st Model: 0.00s Unsat: 6.19s) +CPU Time : 9.944s + +Choices : 166935 (Domain: 119013) +Conflicts : 18691 (Analyzed: 18688) +Restarts : 48 (Average: 389.33 Last: 2758) +Model-Level : 212.0 +Problems : 5 (Average Length: 9.00 Splits: 0) +Lemmas : 18688 (Deleted: 5004) + Binary : 1076 (Ratio: 5.76%) + Ternary : 535 (Ratio: 2.86%) + Conflict : 18688 (Average Length: 179.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 18688 (Average: 8.77 Max: 539 Sum: 163918) + Executed : 18631 (Average: 8.73 Max: 539 Sum: 163197 Ratio: 99.56%) + Bounded : 57 (Average: 12.65 Max: 17 Sum: 721 Ratio: 0.44%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 83686 (Eliminated: 2052 Frozen: 69904) +Constraints : 535212 (Binary: 91.4% Ternary: 6.6% Other: 2.0%) + +Memory Peak : 243MB +Max. Length : 10 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 6.26s +Memory: 243MB (+20MB) +UNSAT +Iteration Time: 6.88s + +Iteration 5 +Queue: [(4,20,0,True), (5,25,0,True), (6,30,0,True)] +Grounded Until: 15 +Expected Memory: 270.0MB +Grounding... [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])] +Grounding Time: 0.44s +Memory: 247MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0 +Calls : 6 +Time : 53.521s (Solving: 48.43s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 53.424s + +Choices : 480680 (Domain: 402891) +Conflicts : 67011 (Analyzed: 67007) +Restarts : 93 (Average: 720.51 Last: 6556) +Model-Level : 212.0 +Problems : 6 (Average Length: 11.17 Splits: 0) +Lemmas : 67007 (Deleted: 37889) + Binary : 2345 (Ratio: 3.50%) + Ternary : 1077 (Ratio: 1.61%) + Conflict : 67007 (Average Length: 511.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 67007 (Average: 7.03 Max: 539 Sum: 471307) + Executed : 66933 (Average: 7.02 Max: 539 Sum: 470323 Ratio: 99.79%) + Bounded : 74 (Average: 13.30 Max: 22 Sum: 984 Ratio: 0.21%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 116632 (Eliminated: 2052 Frozen: 102850) +Constraints : 757133 (Binary: 91.3% Ternary: 6.7% Other: 2.0%) + +Memory Peak : 398MB +Max. Length : 15 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 42.84s +Memory: 334MB (+87MB) +UNSAT +Iteration Time: 43.49s + +Iteration 6 +Queue: [(5,25,0,True), (6,30,0,True)] +Grounded Until: 20 +Expected Memory: 425.0MB +Grounding... [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])] +Grounding Time: 0.68s +Memory: 347MB (+13MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 95.929s (Solving: 89.08s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 95.852s + +Choices : 881977 (Domain: 751212) +Conflicts : 114209 (Analyzed: 114205) +Restarts : 193 (Average: 591.74 Last: 6556) +Model-Level : 212.0 +Problems : 7 (Average Length: 13.43 Splits: 0) +Lemmas : 114205 (Deleted: 82191) + Binary : 3844 (Ratio: 3.37%) + Ternary : 1478 (Ratio: 1.29%) + Conflict : 114205 (Average Length: 797.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 114205 (Average: 7.47 Max: 561 Sum: 853548) + Executed : 114119 (Average: 7.46 Max: 561 Sum: 852260 Ratio: 99.85%) + Bounded : 86 (Average: 14.98 Max: 27 Sum: 1288 Ratio: 0.15%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 149578 (Eliminated: 2052 Frozen: 135796) +Constraints : 1006620 (Binary: 91.3% Ternary: 6.7% Other: 2.0%) + +Memory Peak : 424MB +Max. Length : 20 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 41.45s +Memory: 424MB (+77MB) +UNKNOWN +Iteration Time: 42.44s + +Iteration 7 +Queue: [(6,30,0,True)] +Grounded Until: 25 +Expected Memory: 515.0MB +Grounding... [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])] +Grounding Time: 0.46s +Memory: 428MB (+4MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 131.961s (Solving: 123.77s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 131.900s + +Choices : 1276998 (Domain: 1120172) +Conflicts : 152105 (Analyzed: 152101) +Restarts : 293 (Average: 519.12 Last: 6556) +Model-Level : 212.0 +Problems : 8 (Average Length: 15.75 Splits: 0) +Lemmas : 152101 (Deleted: 126483) + Binary : 5375 (Ratio: 3.53%) + Ternary : 1850 (Ratio: 1.22%) + Conflict : 152101 (Average Length: 897.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 152101 (Average: 8.08 Max: 584 Sum: 1228309) + Executed : 152008 (Average: 8.07 Max: 584 Sum: 1226822 Ratio: 99.88%) + Bounded : 93 (Average: 15.99 Max: 32 Sum: 1487 Ratio: 0.12%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 2052 Frozen: 168742) +Constraints : 1256093 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 455MB +Max. Length : 25 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 35.32s +Memory: 455MB (+27MB) +UNKNOWN +Iteration Time: 36.06s + +Iteration 8 +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), (18,90,0,True)] +Grounded Until: 30 +Blocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 9 +Time : 236.512s (Solving: 228.26s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 236.496s + +Choices : 1574118 (Domain: 1414916) +Conflicts : 223083 (Analyzed: 223079) +Restarts : 393 (Average: 567.63 Last: 6556) +Model-Level : 212.0 +Problems : 9 (Average Length: 17.56 Splits: 0) +Lemmas : 223079 (Deleted: 194712) + Binary : 5749 (Ratio: 2.58%) + Ternary : 1935 (Ratio: 0.87%) + Conflict : 223079 (Average Length: 1249.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 223079 (Average: 6.78 Max: 584 Sum: 1512566) + Executed : 222983 (Average: 6.77 Max: 584 Sum: 1510988 Ratio: 99.90%) + Bounded : 96 (Average: 16.44 Max: 32 Sum: 1578 Ratio: 0.10%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 2052 Frozen: 180472) +Constraints : 1256065 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 583MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 104.57s +Memory: 583MB (+128MB) +UNKNOWN +Iteration Time: 104.60s + +Iteration 9 +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), (18,90,0,True)] +Grounded Until: 30 +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 279.217s (Solving: 270.88s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 279.220s + +Choices : 2016831 (Domain: 1837992) +Conflicts : 270169 (Analyzed: 270165) +Restarts : 493 (Average: 548.00 Last: 6556) +Model-Level : 212.0 +Problems : 10 (Average Length: 19.00 Splits: 0) +Lemmas : 270165 (Deleted: 241176) + Binary : 6838 (Ratio: 2.53%) + Ternary : 2089 (Ratio: 0.77%) + Conflict : 270165 (Average Length: 1275.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 270165 (Average: 7.15 Max: 584 Sum: 1931861) + Executed : 270064 (Average: 7.14 Max: 584 Sum: 1930134 Ratio: 99.91%) + Bounded : 101 (Average: 17.10 Max: 32 Sum: 1727 Ratio: 0.09%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 182524 (Eliminated: 2052 Frozen: 180472) +Constraints : 1256034 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 583MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 42.67s +Memory: 583MB (+0MB) +UNKNOWN +Iteration Time: 42.73s + +Iteration 10 +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), (18,90,0,True)] +Grounded Until: 30 +Expected Memory: 674.0MB +Grounding... [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])] +Grounding Time: 0.45s +Memory: 584MB (+1MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 322.243s (Solving: 312.60s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 322.264s + +Choices : 2450156 (Domain: 2254044) +Conflicts : 316597 (Analyzed: 316593) +Restarts : 593 (Average: 533.88 Last: 6556) +Model-Level : 212.0 +Problems : 11 (Average Length: 20.64 Splits: 0) +Lemmas : 316593 (Deleted: 278646) + Binary : 8059 (Ratio: 2.55%) + Ternary : 2395 (Ratio: 0.76%) + Conflict : 316593 (Average Length: 1281.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 316593 (Average: 7.39 Max: 584 Sum: 2340269) + Executed : 316490 (Average: 7.39 Max: 584 Sum: 2338468 Ratio: 99.92%) + Bounded : 103 (Average: 17.49 Max: 37 Sum: 1801 Ratio: 0.08%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 215470 (Eliminated: 2052 Frozen: 201688) +Constraints : 1505591 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 616MB +Max. Length : 30 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 42.34s +Memory: 604MB (+20MB) +UNKNOWN +Iteration Time: 43.05s + +Iteration 11 +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), (18,90,0,True)] +Grounded Until: 35 +Expected Memory: 695.0MB +Grounding... [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])] +Grounding Time: 0.46s +Memory: 604MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 368.547s (Solving: 357.56s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 368.584s + +Choices : 2872143 (Domain: 2662461) +Conflicts : 364596 (Analyzed: 364592) +Restarts : 693 (Average: 526.11 Last: 6556) +Model-Level : 212.0 +Problems : 12 (Average Length: 22.42 Splits: 0) +Lemmas : 364592 (Deleted: 321756) + Binary : 9720 (Ratio: 2.67%) + Ternary : 2819 (Ratio: 0.77%) + Conflict : 364592 (Average Length: 1313.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 364592 (Average: 7.50 Max: 584 Sum: 2735201) + Executed : 364489 (Average: 7.50 Max: 584 Sum: 2733400 Ratio: 99.93%) + Bounded : 103 (Average: 17.49 Max: 37 Sum: 1801 Ratio: 0.07%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 248416 (Eliminated: 2052 Frozen: 234634) +Constraints : 1755148 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 639MB +Max. Length : 35 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 45.58s +Memory: 625MB (+21MB) +UNKNOWN +Iteration Time: 46.34s + +Iteration 12 +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), (18,90,0,True)] +Grounded Until: 40 +Expected Memory: 716.0MB +Grounding... [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])] +Grounding Time: 0.47s +Memory: 625MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 426.226s (Solving: 413.84s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 426.284s + +Choices : 3449985 (Domain: 3223950) +Conflicts : 422956 (Analyzed: 422952) +Restarts : 793 (Average: 533.36 Last: 6556) +Model-Level : 212.0 +Problems : 13 (Average Length: 24.31 Splits: 0) +Lemmas : 422952 (Deleted: 381589) + Binary : 11338 (Ratio: 2.68%) + Ternary : 3087 (Ratio: 0.73%) + Conflict : 422952 (Average Length: 1331.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 422952 (Average: 7.76 Max: 584 Sum: 3281145) + Executed : 422849 (Average: 7.75 Max: 584 Sum: 3279344 Ratio: 99.95%) + Bounded : 103 (Average: 17.49 Max: 37 Sum: 1801 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 281362 (Eliminated: 2052 Frozen: 267580) +Constraints : 2004733 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 665MB +Max. Length : 40 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 56.93s +Memory: 659MB (+34MB) +UNKNOWN +Iteration Time: 57.72s + +Iteration 13 +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), (18,90,0,True)] +Grounded Until: 45 +Expected Memory: 750.0MB +Grounding... [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])] +Grounding Time: 0.50s +Memory: 659MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 470.863s (Solving: 457.05s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 470.936s + +Choices : 3973235 (Domain: 3732797) +Conflicts : 468077 (Analyzed: 468073) +Restarts : 893 (Average: 524.16 Last: 6556) +Model-Level : 212.0 +Problems : 14 (Average Length: 26.29 Splits: 0) +Lemmas : 468073 (Deleted: 423318) + Binary : 12562 (Ratio: 2.68%) + Ternary : 3303 (Ratio: 0.71%) + Conflict : 468073 (Average Length: 1344.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 468073 (Average: 8.06 Max: 584 Sum: 3773761) + Executed : 467969 (Average: 8.06 Max: 584 Sum: 3771908 Ratio: 99.95%) + Bounded : 104 (Average: 17.82 Max: 52 Sum: 1853 Ratio: 0.05%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 314308 (Eliminated: 2052 Frozen: 300526) +Constraints : 2254318 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 704MB +Max. Length : 45 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 43.84s +Memory: 680MB (+21MB) +UNKNOWN +Iteration Time: 44.66s + +Iteration 14 +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), (18,90,0,True)] +Grounded Until: 50 +Expected Memory: 771.0MB +Grounding... [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])] +Grounding Time: 0.62s +Memory: 692MB (+12MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 522.558s (Solving: 507.20s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 522.652s + +Choices : 4533941 (Domain: 4290629) +Conflicts : 519435 (Analyzed: 519431) +Restarts : 993 (Average: 523.09 Last: 6556) +Model-Level : 212.0 +Problems : 15 (Average Length: 28.33 Splits: 0) +Lemmas : 519431 (Deleted: 466616) + Binary : 13618 (Ratio: 2.62%) + Ternary : 3425 (Ratio: 0.66%) + Conflict : 519431 (Average Length: 1355.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 519431 (Average: 8.29 Max: 584 Sum: 4307333) + Executed : 519327 (Average: 8.29 Max: 584 Sum: 4305480 Ratio: 99.96%) + Bounded : 104 (Average: 17.82 Max: 52 Sum: 1853 Ratio: 0.04%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 347254 (Eliminated: 2052 Frozen: 333472) +Constraints : 2503889 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 741MB +Max. Length : 50 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 50.80s +Memory: 714MB (+22MB) +UNKNOWN +Iteration Time: 51.73s + +Iteration 15 +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), (18,90,0,True)] +Grounded Until: 55 +Expected Memory: 805.0MB +Grounding... [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])] +Grounding Time: 0.47s +Memory: 714MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 568.648s (Solving: 551.85s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 568.760s + +Choices : 5111517 (Domain: 4860847) +Conflicts : 564810 (Analyzed: 564806) +Restarts : 1093 (Average: 516.75 Last: 6556) +Model-Level : 212.0 +Problems : 16 (Average Length: 30.44 Splits: 0) +Lemmas : 564806 (Deleted: 515272) + Binary : 14861 (Ratio: 2.63%) + Ternary : 3632 (Ratio: 0.64%) + Conflict : 564806 (Average Length: 1356.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 564806 (Average: 8.59 Max: 584 Sum: 4854015) + Executed : 564702 (Average: 8.59 Max: 584 Sum: 4852162 Ratio: 99.96%) + Bounded : 104 (Average: 17.82 Max: 52 Sum: 1853 Ratio: 0.04%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 380200 (Eliminated: 2052 Frozen: 366418) +Constraints : 2753474 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 766MB +Max. Length : 55 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 45.30s +Memory: 736MB (+22MB) +UNKNOWN +Iteration Time: 46.12s + +Iteration 16 +Queue: [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True)] +Grounded Until: 60 +Expected Memory: 827.0MB +Grounding... [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])] +Grounding Time: 0.47s +Memory: 736MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 626.166s (Solving: 607.92s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 626.304s + +Choices : 5976521 (Domain: 5716549) +Conflicts : 625442 (Analyzed: 625438) +Restarts : 1193 (Average: 524.26 Last: 6556) +Model-Level : 212.0 +Problems : 17 (Average Length: 32.59 Splits: 0) +Lemmas : 625438 (Deleted: 573134) + Binary : 16821 (Ratio: 2.69%) + Ternary : 4007 (Ratio: 0.64%) + Conflict : 625438 (Average Length: 1339.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 625438 (Average: 9.09 Max: 678 Sum: 5687043) + Executed : 625333 (Average: 9.09 Max: 678 Sum: 5685123 Ratio: 99.97%) + Bounded : 105 (Average: 18.29 Max: 67 Sum: 1920 Ratio: 0.03%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 413146 (Eliminated: 2052 Frozen: 399364) +Constraints : 3003059 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 792MB +Max. Length : 60 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 56.72s +Memory: 783MB (+47MB) +UNKNOWN +Iteration Time: 57.55s + +Iteration 17 +Queue: [(14,70,0,True), (15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True)] +Grounded Until: 65 +Expected Memory: 874.0MB +Grounding... [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])] +Grounding Time: 0.49s +Memory: 783MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 672.036s (Solving: 652.30s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 672.192s + +Choices : 6613763 (Domain: 6350686) +Conflicts : 673848 (Analyzed: 673844) +Restarts : 1293 (Average: 521.15 Last: 6556) +Model-Level : 212.0 +Problems : 18 (Average Length: 34.78 Splits: 0) +Lemmas : 673844 (Deleted: 614613) + Binary : 18005 (Ratio: 2.67%) + Ternary : 4270 (Ratio: 0.63%) + Conflict : 673844 (Average Length: 1329.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 673844 (Average: 9.34 Max: 678 Sum: 6295176) + Executed : 673735 (Average: 9.34 Max: 678 Sum: 6292968 Ratio: 99.96%) + Bounded : 109 (Average: 20.26 Max: 72 Sum: 2208 Ratio: 0.04%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 446092 (Eliminated: 2052 Frozen: 432310) +Constraints : 3252630 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 838MB +Max. Length : 65 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 45.04s +Memory: 801MB (+18MB) +UNKNOWN +Iteration Time: 45.90s + +Iteration 18 +Queue: [(15,75,0,True), (16,80,0,True), (17,85,0,True), (18,90,0,True)] +Grounded Until: 70 +Expected Memory: 892.0MB +Grounding... [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])] +Grounding Time: 0.48s +Memory: 801MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 721.960s (Solving: 700.72s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 722.136s + +Choices : 7343206 (Domain: 7077794) +Conflicts : 722608 (Analyzed: 722604) +Restarts : 1393 (Average: 518.74 Last: 6556) +Model-Level : 212.0 +Problems : 19 (Average Length: 37.00 Splits: 0) +Lemmas : 722604 (Deleted: 660141) + Binary : 19478 (Ratio: 2.70%) + Ternary : 4524 (Ratio: 0.63%) + Conflict : 722604 (Average Length: 1315.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 722604 (Average: 9.67 Max: 678 Sum: 6984308) + Executed : 722495 (Average: 9.66 Max: 678 Sum: 6982100 Ratio: 99.97%) + Bounded : 109 (Average: 20.26 Max: 72 Sum: 2208 Ratio: 0.03%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 479038 (Eliminated: 2052 Frozen: 465256) +Constraints : 3502157 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 863MB +Max. Length : 70 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 49.10s +Memory: 820MB (+19MB) +UNKNOWN +Iteration Time: 49.96s + +Iteration 19 +Queue: [(16,80,0,True), (17,85,0,True), (18,90,0,True)] +Grounded Until: 75 +Expected Memory: 911.0MB +Grounding... [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])] +Grounding Time: 0.46s +Memory: 820MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 774.130s (Solving: 751.41s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 774.328s + +Choices : 7918028 (Domain: 7651768) +Conflicts : 774028 (Analyzed: 774024) +Restarts : 1493 (Average: 518.44 Last: 6556) +Model-Level : 212.0 +Problems : 20 (Average Length: 39.25 Splits: 0) +Lemmas : 774024 (Deleted: 706795) + Binary : 20297 (Ratio: 2.62%) + Ternary : 4649 (Ratio: 0.60%) + Conflict : 774024 (Average Length: 1322.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 774024 (Average: 9.72 Max: 678 Sum: 7523929) + Executed : 773914 (Average: 9.72 Max: 678 Sum: 7521639 Ratio: 99.97%) + Bounded : 110 (Average: 20.82 Max: 82 Sum: 2290 Ratio: 0.03%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 511984 (Eliminated: 2052 Frozen: 498202) +Constraints : 3751742 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 888MB +Max. Length : 75 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 51.36s +Memory: 843MB (+23MB) +UNKNOWN +Iteration Time: 52.20s + +Iteration 20 +Queue: [(17,85,0,True), (18,90,0,True)] +Grounded Until: 80 +Expected Memory: 934.0MB +Grounding... [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])] +Grounding Time: 0.47s +Memory: 843MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 820.785s (Solving: 796.54s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 821.000s + +Choices : 8415116 (Domain: 8148281) +Conflicts : 820437 (Analyzed: 820433) +Restarts : 1593 (Average: 515.02 Last: 6556) +Model-Level : 212.0 +Problems : 21 (Average Length: 41.52 Splits: 0) +Lemmas : 820433 (Deleted: 756590) + Binary : 20842 (Ratio: 2.54%) + Ternary : 4743 (Ratio: 0.58%) + Conflict : 820433 (Average Length: 1328.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 820433 (Average: 9.73 Max: 678 Sum: 7986310) + Executed : 820322 (Average: 9.73 Max: 678 Sum: 7983938 Ratio: 99.97%) + Bounded : 111 (Average: 21.37 Max: 82 Sum: 2372 Ratio: 0.03%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 544930 (Eliminated: 2052 Frozen: 531148) +Constraints : 4001308 (Binary: 91.3% Ternary: 6.8% Other: 1.9%) + +Memory Peak : 915MB +Max. Length : 80 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 45.82s +Memory: 864MB (+21MB) +UNKNOWN +Iteration Time: 46.69s + +Iteration 21 +Queue: [(18,90,0,True)] +Grounded Until: 85 +Expected Memory: 955.0MB +Grounding... [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])] +Grounding Time: 0.47s +Memory: 864MB (+0MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 869.186s (Solving: 843.40s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 869.424s + +Choices : 8796028 (Domain: 8529193) +Conflicts : 865716 (Analyzed: 865712) +Restarts : 1693 (Average: 511.35 Last: 6556) +Model-Level : 212.0 +Problems : 22 (Average Length: 43.82 Splits: 0) +Lemmas : 865712 (Deleted: 801138) + Binary : 21262 (Ratio: 2.46%) + Ternary : 4810 (Ratio: 0.56%) + Conflict : 865712 (Average Length: 1341.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 865712 (Average: 9.62 Max: 678 Sum: 8326350) + Executed : 865600 (Average: 9.62 Max: 678 Sum: 8323886 Ratio: 99.97%) + Bounded : 112 (Average: 22.00 Max: 92 Sum: 2464 Ratio: 0.03%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 577876 (Eliminated: 2052 Frozen: 564094) +Constraints : 4250893 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 940MB +Max. Length : 85 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 47.54s +Memory: 890MB (+26MB) +UNKNOWN +Iteration Time: 48.43s + +Iteration 22 +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,1,True), (19,95,0,True), (20,100,0,True), (21,105,0,True), (22,110,0,True)] +Grounded Until: 90 +Blocking actions... +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 23 +Time : 893.798s (Solving: 867.86s 1st Model: 0.00s Unsat: 48.43s) +CPU Time : 894.028s + +Choices : 8861867 (Domain: 8595032) +Conflicts : 880634 (Analyzed: 880630) +Restarts : 1713 (Average: 514.09 Last: 6556) +Model-Level : 212.0 +Problems : 23 (Average Length: 45.91 Splits: 0) +Lemmas : 880630 (Deleted: 819906) + Binary : 21307 (Ratio: 2.42%) + Ternary : 4818 (Ratio: 0.55%) + Conflict : 880630 (Average Length: 1360.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 880630 (Average: 9.53 Max: 678 Sum: 8388770) + Executed : 880518 (Average: 9.52 Max: 678 Sum: 8386306 Ratio: 99.97%) + Bounded : 112 (Average: 22.00 Max: 92 Sum: 2464 Ratio: 0.03%) + +Rules : 76935 (Original: 75225) +Atoms : 61653 +Bodies : 14003 (Original: 12292) + Count : 291 (Original: 633) +Equivalences : 3885 (Atom=Atom: 72 Body=Body: 0 Other: 3813) +Tight : Yes +Variables : 577876 (Eliminated: 2052 Frozen: 575824) +Constraints : 4250874 (Binary: 91.3% Ternary: 6.8% Other: 1.8%) + +Memory Peak : 940MB +Max. Length : 90 steps +Models : 1 + +