diff --git a/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.env b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.env new file mode 100644 index 000000000..9e4ff8ffe --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.env @@ -0,0 +1,60 @@ +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-5.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 +- -i 0 +- -F 115 +- -T 115 +configuration: + fixedHorizon: true + id: gc-ta1-tt1-single-shot + 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 + - -i 0 +exitCode: 0 +instance: + domain: barman-sequential-satisficing + instance: 5 + ipc: ipc-2011 + planLength: 115 +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-single-shot/ipc-2011_barman-sequential-satisficing_5.err b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.err new file mode 100644 index 000000000..3a6591bf1 --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.err @@ -0,0 +1,8 @@ +# configuration: {'id': 'gc-ta1-tt1-single-shot', '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', '-i 0'], 'instanceSets': ['rintanen-aij-2012-interesting'], 'fixedHorizon': True} +# instance: {'ipc': 'ipc-2011', 'domain': 'barman-sequential-satisficing', 'instance': 5, 'planLength': 115} +# 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-5.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', '-i 0', '-F 115', '-T 115'] +# working directory: /home/pluehne/Documents/ASP/plasp-javier/encodings/planner +# exit code: 0 +TIMEOUT CPU 900.06 MEM 1000296 MAXMEM 1000296 STALE 0 MAXMEM_RSS 879204 + + diff --git a/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.out b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.out new file mode 100644 index 000000000..b072a407c --- /dev/null +++ b/gc-ta1-tt1-single-shot/ipc-2011_barman-sequential-satisficing_5.out @@ -0,0 +1,1828 @@ +INFO Running translator. +INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-5.pddl'] +INFO translator arguments: [] +INFO translator time limit: None +INFO translator memory limit: None +INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-5.pddl +Parsing... +Parsing: [0.030s CPU, 0.039s wall-clock] +Normalizing task... [0.010s CPU, 0.003s wall-clock] +Instantiating... +Generating Datalog program... [0.010s CPU, 0.010s wall-clock] +Normalizing Datalog program... +Normalizing Datalog program: [0.050s CPU, 0.050s wall-clock] +Preparing model... [0.020s CPU, 0.026s wall-clock] +Generated 115 rules. +Computing model... [0.380s CPU, 0.372s wall-clock] +2300 relevant atoms +2393 auxiliary atoms +4693 final queue length +8087 total queue pushes +Completing instantiation... [0.680s CPU, 0.682s wall-clock] +Instantiating: [1.150s CPU, 1.146s wall-clock] +Computing fact groups... +Finding invariants... +24 initial candidates +Finding invariants: [0.140s CPU, 0.139s wall-clock] +Checking invariant weight... [0.000s CPU, 0.001s wall-clock] +Instantiating groups... [0.010s CPU, 0.007s wall-clock] +Collecting mutex groups... [0.000s CPU, 0.001s wall-clock] +Choosing groups... +238 uncovered facts +Choosing groups: [0.000s CPU, 0.001s wall-clock] +Building translation key... [0.000s CPU, 0.009s wall-clock] +Computing fact groups: [0.170s CPU, 0.175s wall-clock] +Building STRIPS to SAS dictionary... [0.000s CPU, 0.002s wall-clock] +Building dictionary for full mutex groups... [0.010s CPU, 0.002s 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.040s CPU, 0.038s wall-clock] +Translating task: [0.730s CPU, 0.727s wall-clock] +2672 effect conditions simplified +0 implied preconditions added +Detecting unreachable propositions... +0 operators removed +0 axioms removed +3 propositions removed +Detecting unreachable propositions: [0.350s CPU, 0.355s wall-clock] +Reordering and filtering variables... +241 of 241 variables necessary. +12 of 15 mutex groups necessary. +1596 of 1596 operators necessary. +0 of 0 axiom rules necessary. +Reordering and filtering variables: [0.240s CPU, 0.239s wall-clock] +Translator variables: 241 +Translator derived variables: 0 +Translator facts: 505 +Translator goal facts: 10 +Translator mutex groups: 12 +Translator total mutex groups size: 36 +Translator operators: 1596 +Translator axioms: 0 +Translator task size: 15302 +Translator peak memory: 45260 KB +Writing output... [0.260s CPU, 0.281s wall-clock] +Done! [2.980s CPU, 3.003s wall-clock] +planner.py version 0.0.1 + +Time: 0.62s +Memory: 91MB + +Iteration 1 +Queue: [(0,115,0,True)] +Grounded Until: 0 +Expected Memory: 91MB +Grounding... [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])] +Grounding Time: 5.30s +Memory: 572MB (+481MB) +Unblocking actions... +Solving... +[start: stats after solve call] + +Models : 1+ +Calls : 1 +Time : 9.188s (Solving: 0.10s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 9.072s + +Choices : 6189 (Domain: 6157) +Conflicts : 8 (Analyzed: 8) +Restarts : 0 +Model-Level : 4466.0 +Problems : 1 (Average Length: 117.00 Splits: 0) +Lemmas : 8 (Deleted: 0) + Binary : 1 (Ratio: 12.50%) + Ternary : 4 (Ratio: 50.00%) + Conflict : 8 (Average Length: 16.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: 230.00 Max: 1745 Sum: 1840) + Executed : 8 (Average: 230.00 Max: 1745 Sum: 1840 Ratio: 100.00%) + Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%) + +Rules : 0 +Atoms : 0 +Bodies : 0 +Tight : Yes +Variables : 322152 (Eliminated: 0 Frozen: 2990) +Constraints : 2576091 (Binary: 95.7% Ternary: 3.2% Other: 1.1%) + +Memory Peak : 815MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 0.32s +Memory: 751MB (+179MB) +SAT +Testing... +NOT SERIALIZABLE +Testing Time: 2.80s +Memory: 765MB (+14MB) +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 2 +Time : 39.094s (Solving: 26.91s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 38.992s + +Choices : 2133383 (Domain: 2097739) +Conflicts : 25874 (Analyzed: 25874) +Restarts : 100 (Average: 258.74 Last: 156) +Model-Level : 4466.0 +Problems : 2 (Average Length: 117.00 Splits: 0) +Lemmas : 25874 (Deleted: 18497) + Binary : 2111 (Ratio: 8.16%) + Ternary : 813 (Ratio: 3.14%) + Conflict : 25874 (Average Length: 265.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 25874 (Average: 81.50 Max: 1745 Sum: 2108747) + Executed : 25820 (Average: 81.26 Max: 1745 Sum: 2102512 Ratio: 99.70%) + Bounded : 54 (Average: 115.46 Max: 117 Sum: 6235 Ratio: 0.30%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4250110 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 0 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 27.79s +Memory: 872MB (+107MB) +UNKNOWN +Iteration Time: 39.08s + +Iteration 2 +Queue: [(0,115,1,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 3 +Time : 66.031s (Solving: 53.70s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 65.940s + +Choices : 3592360 (Domain: 3540319) +Conflicts : 52716 (Analyzed: 52716) +Restarts : 200 (Average: 263.58 Last: 156) +Model-Level : 4466.0 +Problems : 3 (Average Length: 117.00 Splits: 0) +Lemmas : 52716 (Deleted: 42645) + Binary : 3073 (Ratio: 5.83%) + Ternary : 1009 (Ratio: 1.91%) + Conflict : 52716 (Average Length: 388.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 52716 (Average: 67.30 Max: 1745 Sum: 3547571) + Executed : 52659 (Average: 67.17 Max: 1745 Sum: 3540999 Ratio: 99.81%) + Bounded : 57 (Average: 115.30 Max: 117 Sum: 6572 Ratio: 0.19%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212577 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 26.95s +Memory: 875MB (+3MB) +UNKNOWN +Iteration Time: 26.95s + +Iteration 3 +Queue: [(0,115,2,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 4 +Time : 89.334s (Solving: 76.91s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 89.256s + +Choices : 4719442 (Domain: 4657797) +Conflicts : 78831 (Analyzed: 78831) +Restarts : 300 (Average: 262.77 Last: 339) +Model-Level : 4466.0 +Problems : 4 (Average Length: 117.00 Splits: 0) +Lemmas : 78831 (Deleted: 68311) + Binary : 3612 (Ratio: 4.58%) + Ternary : 1085 (Ratio: 1.38%) + Conflict : 78831 (Average Length: 507.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 78831 (Average: 59.05 Max: 1745 Sum: 4654789) + Executed : 78773 (Average: 58.96 Max: 1745 Sum: 4648100 Ratio: 99.86%) + Bounded : 58 (Average: 115.33 Max: 117 Sum: 6689 Ratio: 0.14%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212577 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.32s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 23.32s + +Iteration 4 +Queue: [(0,115,3,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 5 +Time : 111.274s (Solving: 98.73s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 111.204s + +Choices : 5715653 (Domain: 5647385) +Conflicts : 104923 (Analyzed: 104923) +Restarts : 400 (Average: 262.31 Last: 339) +Model-Level : 4466.0 +Problems : 5 (Average Length: 117.00 Splits: 0) +Lemmas : 104923 (Deleted: 93304) + Binary : 4106 (Ratio: 3.91%) + Ternary : 1133 (Ratio: 1.08%) + Conflict : 104923 (Average Length: 555.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 104923 (Average: 53.64 Max: 1745 Sum: 5628395) + Executed : 104864 (Average: 53.58 Max: 1745 Sum: 5621594 Ratio: 99.88%) + Bounded : 59 (Average: 115.27 Max: 117 Sum: 6801 Ratio: 0.12%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212563 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.95s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 21.95s + +Iteration 5 +Queue: [(0,115,4,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 6 +Time : 130.725s (Solving: 118.09s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 130.660s + +Choices : 6496876 (Domain: 6423720) +Conflicts : 130445 (Analyzed: 130445) +Restarts : 500 (Average: 260.89 Last: 339) +Model-Level : 4466.0 +Problems : 6 (Average Length: 117.00 Splits: 0) +Lemmas : 130445 (Deleted: 118206) + Binary : 4416 (Ratio: 3.39%) + Ternary : 1169 (Ratio: 0.90%) + Conflict : 130445 (Average Length: 586.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 130445 (Average: 48.97 Max: 1745 Sum: 6388184) + Executed : 130382 (Average: 48.92 Max: 1745 Sum: 6380932 Ratio: 99.89%) + Bounded : 63 (Average: 115.11 Max: 117 Sum: 7252 Ratio: 0.11%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212563 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 19.46s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 19.46s + +Iteration 6 +Queue: [(0,115,5,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 7 +Time : 157.943s (Solving: 145.21s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 157.888s + +Choices : 8173024 (Domain: 8074630) +Conflicts : 158923 (Analyzed: 158923) +Restarts : 600 (Average: 264.87 Last: 345) +Model-Level : 4466.0 +Problems : 7 (Average Length: 117.00 Splits: 0) +Lemmas : 158923 (Deleted: 141638) + Binary : 5755 (Ratio: 3.62%) + Ternary : 1484 (Ratio: 0.93%) + Conflict : 158923 (Average Length: 659.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 158923 (Average: 50.48 Max: 1745 Sum: 8023177) + Executed : 158860 (Average: 50.44 Max: 1745 Sum: 8015925 Ratio: 99.91%) + Bounded : 63 (Average: 115.11 Max: 117 Sum: 7252 Ratio: 0.09%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212563 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 27.23s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 27.23s + +Iteration 7 +Queue: [(0,115,6,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 8 +Time : 180.606s (Solving: 167.77s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 180.560s + +Choices : 9191355 (Domain: 9068099) +Conflicts : 184721 (Analyzed: 184721) +Restarts : 700 (Average: 263.89 Last: 345) +Model-Level : 4466.0 +Problems : 8 (Average Length: 117.00 Splits: 0) +Lemmas : 184721 (Deleted: 165754) + Binary : 6446 (Ratio: 3.49%) + Ternary : 1597 (Ratio: 0.86%) + Conflict : 184721 (Average Length: 727.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 184721 (Average: 48.78 Max: 2299 Sum: 9011473) + Executed : 184657 (Average: 48.74 Max: 2299 Sum: 9004104 Ratio: 99.92%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.08%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212563 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 892MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.68s +Memory: 875MB (+0MB) +UNKNOWN +Iteration Time: 22.68s + +Iteration 8 +Queue: [(0,115,7,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 9 +Time : 205.867s (Solving: 192.91s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 205.832s + +Choices : 10192683 (Domain: 10058357) +Conflicts : 210253 (Analyzed: 210253) +Restarts : 800 (Average: 262.82 Last: 345) +Model-Level : 4466.0 +Problems : 9 (Average Length: 117.00 Splits: 0) +Lemmas : 210253 (Deleted: 189829) + Binary : 7404 (Ratio: 3.52%) + Ternary : 1862 (Ratio: 0.89%) + Conflict : 210253 (Average Length: 792.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 210253 (Average: 47.43 Max: 2299 Sum: 9972151) + Executed : 210189 (Average: 47.39 Max: 2299 Sum: 9964782 Ratio: 99.93%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.07%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.27s +Memory: 939MB (+64MB) +UNKNOWN +Iteration Time: 25.28s + +Iteration 9 +Queue: [(0,115,8,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 10 +Time : 229.612s (Solving: 216.55s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 229.588s + +Choices : 11011573 (Domain: 10868721) +Conflicts : 236516 (Analyzed: 236516) +Restarts : 900 (Average: 262.80 Last: 345) +Model-Level : 4466.0 +Problems : 10 (Average Length: 117.00 Splits: 0) +Lemmas : 236516 (Deleted: 214363) + Binary : 8134 (Ratio: 3.44%) + Ternary : 1958 (Ratio: 0.83%) + Conflict : 236516 (Average Length: 865.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 236516 (Average: 45.46 Max: 2299 Sum: 10751171) + Executed : 236452 (Average: 45.43 Max: 2299 Sum: 10743802 Ratio: 99.93%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.07%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.76s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.76s + +Iteration 10 +Queue: [(0,115,9,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 11 +Time : 255.490s (Solving: 242.33s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 255.476s + +Choices : 12134117 (Domain: 11981885) +Conflicts : 264866 (Analyzed: 264866) +Restarts : 1000 (Average: 264.87 Last: 345) +Model-Level : 4466.0 +Problems : 11 (Average Length: 117.00 Splits: 0) +Lemmas : 264866 (Deleted: 240799) + Binary : 8946 (Ratio: 3.38%) + Ternary : 2035 (Ratio: 0.77%) + Conflict : 264866 (Average Length: 882.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 264866 (Average: 44.66 Max: 2299 Sum: 11827972) + Executed : 264802 (Average: 44.63 Max: 2299 Sum: 11820603 Ratio: 99.94%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.06%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.89s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 25.89s + +Iteration 11 +Queue: [(0,115,10,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 12 +Time : 276.187s (Solving: 262.92s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 276.184s + +Choices : 13145023 (Domain: 12983493) +Conflicts : 289757 (Analyzed: 289757) +Restarts : 1100 (Average: 263.42 Last: 345) +Model-Level : 4466.0 +Problems : 12 (Average Length: 117.00 Splits: 0) +Lemmas : 289757 (Deleted: 264611) + Binary : 9605 (Ratio: 3.31%) + Ternary : 2151 (Ratio: 0.74%) + Conflict : 289757 (Average Length: 908.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 289757 (Average: 44.15 Max: 2299 Sum: 12793945) + Executed : 289693 (Average: 44.13 Max: 2299 Sum: 12786576 Ratio: 99.94%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.06%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 20.71s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 20.71s + +Iteration 12 +Queue: [(0,115,11,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 13 +Time : 297.570s (Solving: 284.19s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 297.576s + +Choices : 13867835 (Domain: 13702389) +Conflicts : 316124 (Analyzed: 316124) +Restarts : 1200 (Average: 263.44 Last: 345) +Model-Level : 4466.0 +Problems : 13 (Average Length: 117.00 Splits: 0) +Lemmas : 316124 (Deleted: 288287) + Binary : 10102 (Ratio: 3.20%) + Ternary : 2207 (Ratio: 0.70%) + Conflict : 316124 (Average Length: 920.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 316124 (Average: 42.64 Max: 2299 Sum: 13478811) + Executed : 316060 (Average: 42.61 Max: 2299 Sum: 13471442 Ratio: 99.95%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.39s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.39s + +Iteration 13 +Queue: [(0,115,12,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 14 +Time : 319.295s (Solving: 305.82s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 319.308s + +Choices : 14618194 (Domain: 14449498) +Conflicts : 342225 (Analyzed: 342225) +Restarts : 1300 (Average: 263.25 Last: 345) +Model-Level : 4466.0 +Problems : 14 (Average Length: 117.00 Splits: 0) +Lemmas : 342225 (Deleted: 313377) + Binary : 10770 (Ratio: 3.15%) + Ternary : 2307 (Ratio: 0.67%) + Conflict : 342225 (Average Length: 924.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 342225 (Average: 41.46 Max: 2299 Sum: 14188074) + Executed : 342161 (Average: 41.44 Max: 2299 Sum: 14180705 Ratio: 99.95%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.74s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.74s + +Iteration 14 +Queue: [(0,115,13,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 15 +Time : 342.774s (Solving: 329.17s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 342.800s + +Choices : 15499142 (Domain: 15328181) +Conflicts : 367783 (Analyzed: 367783) +Restarts : 1400 (Average: 262.70 Last: 345) +Model-Level : 4466.0 +Problems : 15 (Average Length: 117.00 Splits: 0) +Lemmas : 367783 (Deleted: 337702) + Binary : 11427 (Ratio: 3.11%) + Ternary : 2434 (Ratio: 0.66%) + Conflict : 367783 (Average Length: 933.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 367783 (Average: 40.85 Max: 2299 Sum: 15025408) + Executed : 367719 (Average: 40.83 Max: 2299 Sum: 15018039 Ratio: 99.95%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.49s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.49s + +Iteration 15 +Queue: [(0,115,14,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 16 +Time : 366.465s (Solving: 352.76s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 366.500s + +Choices : 16107734 (Domain: 15935706) +Conflicts : 396758 (Analyzed: 396758) +Restarts : 1500 (Average: 264.51 Last: 345) +Model-Level : 4466.0 +Problems : 16 (Average Length: 117.00 Splits: 0) +Lemmas : 396758 (Deleted: 364893) + Binary : 11898 (Ratio: 3.00%) + Ternary : 2519 (Ratio: 0.63%) + Conflict : 396758 (Average Length: 938.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 396758 (Average: 39.30 Max: 2299 Sum: 15591823) + Executed : 396694 (Average: 39.28 Max: 2299 Sum: 15584454 Ratio: 99.95%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.70s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.70s + +Iteration 16 +Queue: [(0,115,15,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 17 +Time : 390.182s (Solving: 376.38s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 390.224s + +Choices : 16739525 (Domain: 16565937) +Conflicts : 422718 (Analyzed: 422718) +Restarts : 1600 (Average: 264.20 Last: 345) +Model-Level : 4466.0 +Problems : 17 (Average Length: 117.00 Splits: 0) +Lemmas : 422718 (Deleted: 390159) + Binary : 12259 (Ratio: 2.90%) + Ternary : 2588 (Ratio: 0.61%) + Conflict : 422718 (Average Length: 959.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 422718 (Average: 38.28 Max: 2299 Sum: 16180692) + Executed : 422654 (Average: 38.26 Max: 2299 Sum: 16173323 Ratio: 99.95%) + Bounded : 64 (Average: 115.14 Max: 117 Sum: 7369 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.73s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.73s + +Iteration 17 +Queue: [(0,115,16,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 18 +Time : 411.396s (Solving: 397.48s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 411.448s + +Choices : 17156817 (Domain: 16982929) +Conflicts : 448096 (Analyzed: 448096) +Restarts : 1700 (Average: 263.59 Last: 345) +Model-Level : 4466.0 +Problems : 18 (Average Length: 117.00 Splits: 0) +Lemmas : 448096 (Deleted: 415234) + Binary : 12511 (Ratio: 2.79%) + Ternary : 2639 (Ratio: 0.59%) + Conflict : 448096 (Average Length: 963.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 448096 (Average: 36.97 Max: 2299 Sum: 16564912) + Executed : 448031 (Average: 36.95 Max: 2299 Sum: 16557426 Ratio: 99.95%) + Bounded : 65 (Average: 115.17 Max: 117 Sum: 7486 Ratio: 0.05%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212537 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.23s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.23s + +Iteration 18 +Queue: [(0,115,17,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 19 +Time : 436.768s (Solving: 422.75s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 436.832s + +Choices : 17946567 (Domain: 17769301) +Conflicts : 476299 (Analyzed: 476299) +Restarts : 1800 (Average: 264.61 Last: 345) +Model-Level : 4466.0 +Problems : 19 (Average Length: 117.00 Splits: 0) +Lemmas : 476299 (Deleted: 442480) + Binary : 12863 (Ratio: 2.70%) + Ternary : 2761 (Ratio: 0.58%) + Conflict : 476299 (Average Length: 962.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 476299 (Average: 36.34 Max: 2299 Sum: 17309468) + Executed : 476233 (Average: 36.33 Max: 2299 Sum: 17301865 Ratio: 99.96%) + Bounded : 66 (Average: 115.20 Max: 117 Sum: 7603 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212523 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.39s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 25.39s + +Iteration 19 +Queue: [(0,115,18,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 20 +Time : 461.391s (Solving: 447.24s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 461.464s + +Choices : 18517178 (Domain: 18337584) +Conflicts : 503460 (Analyzed: 503460) +Restarts : 1900 (Average: 264.98 Last: 345) +Model-Level : 4466.0 +Problems : 20 (Average Length: 117.00 Splits: 0) +Lemmas : 503460 (Deleted: 466662) + Binary : 13212 (Ratio: 2.62%) + Ternary : 2831 (Ratio: 0.56%) + Conflict : 503460 (Average Length: 974.2 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 503460 (Average: 35.43 Max: 2299 Sum: 17838578) + Executed : 503394 (Average: 35.42 Max: 2299 Sum: 17830975 Ratio: 99.96%) + Bounded : 66 (Average: 115.20 Max: 117 Sum: 7603 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212509 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.64s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 24.64s + +Iteration 20 +Queue: [(0,115,19,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 21 +Time : 483.733s (Solving: 469.46s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 483.816s + +Choices : 19184717 (Domain: 19002019) +Conflicts : 530493 (Analyzed: 530493) +Restarts : 2000 (Average: 265.25 Last: 345) +Model-Level : 4466.0 +Problems : 21 (Average Length: 117.00 Splits: 0) +Lemmas : 530493 (Deleted: 492739) + Binary : 13687 (Ratio: 2.58%) + Ternary : 2938 (Ratio: 0.55%) + Conflict : 530493 (Average Length: 972.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 530493 (Average: 34.79 Max: 2299 Sum: 18457248) + Executed : 530426 (Average: 34.78 Max: 2299 Sum: 18449528 Ratio: 99.96%) + Bounded : 67 (Average: 115.22 Max: 117 Sum: 7720 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212509 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.35s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 22.35s + +Iteration 21 +Queue: [(0,115,20,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 22 +Time : 507.038s (Solving: 492.67s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 507.128s + +Choices : 19656696 (Domain: 19473467) +Conflicts : 557755 (Analyzed: 557755) +Restarts : 2100 (Average: 265.60 Last: 345) +Model-Level : 4466.0 +Problems : 22 (Average Length: 117.00 Splits: 0) +Lemmas : 557755 (Deleted: 518963) + Binary : 13986 (Ratio: 2.51%) + Ternary : 3002 (Ratio: 0.54%) + Conflict : 557755 (Average Length: 981.6 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 557755 (Average: 33.85 Max: 2299 Sum: 18879810) + Executed : 557687 (Average: 33.84 Max: 2299 Sum: 18871973 Ratio: 99.96%) + Bounded : 68 (Average: 115.25 Max: 117 Sum: 7837 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212495 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.32s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.32s + +Iteration 22 +Queue: [(0,115,21,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 23 +Time : 531.517s (Solving: 517.03s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 531.616s + +Choices : 20100299 (Domain: 19916754) +Conflicts : 587313 (Analyzed: 587313) +Restarts : 2200 (Average: 266.96 Last: 345) +Model-Level : 4466.0 +Problems : 23 (Average Length: 117.00 Splits: 0) +Lemmas : 587313 (Deleted: 547984) + Binary : 14185 (Ratio: 2.42%) + Ternary : 3070 (Ratio: 0.52%) + Conflict : 587313 (Average Length: 989.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 587313 (Average: 32.84 Max: 2299 Sum: 19286332) + Executed : 587245 (Average: 32.82 Max: 2299 Sum: 19278495 Ratio: 99.96%) + Bounded : 68 (Average: 115.25 Max: 117 Sum: 7837 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212469 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.49s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 24.49s + +Iteration 23 +Queue: [(0,115,22,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 24 +Time : 554.100s (Solving: 539.50s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 554.208s + +Choices : 20472528 (Domain: 20288804) +Conflicts : 618263 (Analyzed: 618263) +Restarts : 2300 (Average: 268.81 Last: 345) +Model-Level : 4466.0 +Problems : 24 (Average Length: 117.00 Splits: 0) +Lemmas : 618263 (Deleted: 579807) + Binary : 14407 (Ratio: 2.33%) + Ternary : 3110 (Ratio: 0.50%) + Conflict : 618263 (Average Length: 992.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 618263 (Average: 31.75 Max: 2299 Sum: 19627268) + Executed : 618195 (Average: 31.73 Max: 2299 Sum: 19619431 Ratio: 99.96%) + Bounded : 68 (Average: 115.25 Max: 117 Sum: 7837 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212469 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 22.60s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 22.60s + +Iteration 24 +Queue: [(0,115,23,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 25 +Time : 575.787s (Solving: 561.08s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 575.904s + +Choices : 20917484 (Domain: 20733356) +Conflicts : 645648 (Analyzed: 645648) +Restarts : 2400 (Average: 269.02 Last: 345) +Model-Level : 4466.0 +Problems : 25 (Average Length: 117.00 Splits: 0) +Lemmas : 645648 (Deleted: 604293) + Binary : 14550 (Ratio: 2.25%) + Ternary : 3156 (Ratio: 0.49%) + Conflict : 645648 (Average Length: 991.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 645648 (Average: 31.02 Max: 2299 Sum: 20027314) + Executed : 645579 (Average: 31.01 Max: 2299 Sum: 20019360 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212469 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.70s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.70s + +Iteration 25 +Queue: [(0,115,24,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 26 +Time : 596.786s (Solving: 581.98s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 596.912s + +Choices : 21267185 (Domain: 21082920) +Conflicts : 671917 (Analyzed: 671917) +Restarts : 2500 (Average: 268.77 Last: 345) +Model-Level : 4466.0 +Problems : 26 (Average Length: 117.00 Splits: 0) +Lemmas : 671917 (Deleted: 631109) + Binary : 14673 (Ratio: 2.18%) + Ternary : 3182 (Ratio: 0.47%) + Conflict : 671917 (Average Length: 998.3 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 671917 (Average: 30.26 Max: 2299 Sum: 20333368) + Executed : 671848 (Average: 30.25 Max: 2299 Sum: 20325414 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.01s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.01s + +Iteration 26 +Queue: [(0,115,25,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 27 +Time : 618.444s (Solving: 603.54s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 618.580s + +Choices : 21613850 (Domain: 21429541) +Conflicts : 699621 (Analyzed: 699621) +Restarts : 2600 (Average: 269.08 Last: 345) +Model-Level : 4466.0 +Problems : 27 (Average Length: 117.00 Splits: 0) +Lemmas : 699621 (Deleted: 659727) + Binary : 14832 (Ratio: 2.12%) + Ternary : 3218 (Ratio: 0.46%) + Conflict : 699621 (Average Length: 1001.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 699621 (Average: 29.51 Max: 2299 Sum: 20643824) + Executed : 699552 (Average: 29.50 Max: 2299 Sum: 20635870 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.67s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.67s + +Iteration 27 +Queue: [(0,115,26,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 28 +Time : 642.427s (Solving: 627.40s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 642.576s + +Choices : 21972968 (Domain: 21788462) +Conflicts : 729958 (Analyzed: 729958) +Restarts : 2700 (Average: 270.35 Last: 345) +Model-Level : 4466.0 +Problems : 28 (Average Length: 117.00 Splits: 0) +Lemmas : 729958 (Deleted: 686747) + Binary : 15031 (Ratio: 2.06%) + Ternary : 3261 (Ratio: 0.45%) + Conflict : 729958 (Average Length: 999.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 729958 (Average: 28.73 Max: 2299 Sum: 20971312) + Executed : 729889 (Average: 28.72 Max: 2299 Sum: 20963358 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 24.00s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 24.00s + +Iteration 28 +Queue: [(0,115,27,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 29 +Time : 663.975s (Solving: 648.81s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 664.132s + +Choices : 22377991 (Domain: 22193166) +Conflicts : 759042 (Analyzed: 759042) +Restarts : 2800 (Average: 271.09 Last: 345) +Model-Level : 4466.0 +Problems : 29 (Average Length: 117.00 Splits: 0) +Lemmas : 759042 (Deleted: 716410) + Binary : 15199 (Ratio: 2.00%) + Ternary : 3292 (Ratio: 0.43%) + Conflict : 759042 (Average Length: 997.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 759042 (Average: 28.12 Max: 2299 Sum: 21342594) + Executed : 758973 (Average: 28.11 Max: 2299 Sum: 21334640 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.56s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.56s + +Iteration 29 +Queue: [(0,115,28,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 30 +Time : 687.237s (Solving: 671.96s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 687.404s + +Choices : 22729550 (Domain: 22544685) +Conflicts : 789570 (Analyzed: 789570) +Restarts : 2900 (Average: 272.27 Last: 345) +Model-Level : 4466.0 +Problems : 30 (Average Length: 117.00 Splits: 0) +Lemmas : 789570 (Deleted: 744943) + Binary : 15333 (Ratio: 1.94%) + Ternary : 3343 (Ratio: 0.42%) + Conflict : 789570 (Average Length: 998.9 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 789570 (Average: 27.43 Max: 2299 Sum: 21656550) + Executed : 789501 (Average: 27.42 Max: 2299 Sum: 21648596 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.27s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.27s + +Iteration 30 +Queue: [(0,115,29,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 31 +Time : 710.240s (Solving: 694.83s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 710.416s + +Choices : 23046388 (Domain: 22861480) +Conflicts : 818292 (Analyzed: 818292) +Restarts : 3000 (Average: 272.76 Last: 345) +Model-Level : 4466.0 +Problems : 31 (Average Length: 117.00 Splits: 0) +Lemmas : 818292 (Deleted: 774597) + Binary : 15555 (Ratio: 1.90%) + Ternary : 3394 (Ratio: 0.41%) + Conflict : 818292 (Average Length: 1000.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 818292 (Average: 26.81 Max: 2299 Sum: 21937536) + Executed : 818223 (Average: 26.80 Max: 2299 Sum: 21929582 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.02s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.02s + +Iteration 31 +Queue: [(0,115,30,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 32 +Time : 733.927s (Solving: 718.39s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 734.112s + +Choices : 23355859 (Domain: 23170922) +Conflicts : 848627 (Analyzed: 848627) +Restarts : 3100 (Average: 273.75 Last: 345) +Model-Level : 4466.0 +Problems : 32 (Average Length: 117.00 Splits: 0) +Lemmas : 848627 (Deleted: 802783) + Binary : 15664 (Ratio: 1.85%) + Ternary : 3444 (Ratio: 0.41%) + Conflict : 848627 (Average Length: 1003.4 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 848627 (Average: 26.18 Max: 2299 Sum: 22214435) + Executed : 848558 (Average: 26.17 Max: 2299 Sum: 22206481 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.70s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.70s + +Iteration 32 +Queue: [(0,115,31,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 33 +Time : 755.642s (Solving: 739.99s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 755.836s + +Choices : 23688301 (Domain: 23503066) +Conflicts : 876777 (Analyzed: 876777) +Restarts : 3200 (Average: 273.99 Last: 345) +Model-Level : 4466.0 +Problems : 33 (Average Length: 117.00 Splits: 0) +Lemmas : 876777 (Deleted: 832350) + Binary : 15881 (Ratio: 1.81%) + Ternary : 3488 (Ratio: 0.40%) + Conflict : 876777 (Average Length: 1005.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 876777 (Average: 25.68 Max: 2299 Sum: 22517045) + Executed : 876708 (Average: 25.67 Max: 2299 Sum: 22509091 Ratio: 99.96%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.04%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.73s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.73s + +Iteration 33 +Queue: [(0,115,32,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 34 +Time : 779.125s (Solving: 763.35s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 779.328s + +Choices : 24039130 (Domain: 23853830) +Conflicts : 906758 (Analyzed: 906758) +Restarts : 3300 (Average: 274.78 Last: 345) +Model-Level : 4466.0 +Problems : 34 (Average Length: 117.00 Splits: 0) +Lemmas : 906758 (Deleted: 860016) + Binary : 16010 (Ratio: 1.77%) + Ternary : 3517 (Ratio: 0.39%) + Conflict : 906758 (Average Length: 1006.1 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 906758 (Average: 25.18 Max: 2299 Sum: 22832224) + Executed : 906689 (Average: 25.17 Max: 2299 Sum: 22824270 Ratio: 99.97%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.50s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.50s + +Iteration 34 +Queue: [(0,115,33,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 35 +Time : 804.748s (Solving: 788.84s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 804.960s + +Choices : 24938156 (Domain: 24739047) +Conflicts : 938720 (Analyzed: 938720) +Restarts : 3400 (Average: 276.09 Last: 345) +Model-Level : 4466.0 +Problems : 35 (Average Length: 117.00 Splits: 0) +Lemmas : 938720 (Deleted: 890714) + Binary : 17055 (Ratio: 1.82%) + Ternary : 3797 (Ratio: 0.40%) + Conflict : 938720 (Average Length: 1005.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 938720 (Average: 25.23 Max: 2299 Sum: 23685471) + Executed : 938651 (Average: 25.22 Max: 2299 Sum: 23677517 Ratio: 99.97%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.64s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 25.64s + +Iteration 35 +Queue: [(0,115,34,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 36 +Time : 827.856s (Solving: 811.85s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 828.076s + +Choices : 25374412 (Domain: 25172627) +Conflicts : 967277 (Analyzed: 967277) +Restarts : 3500 (Average: 276.36 Last: 345) +Model-Level : 4466.0 +Problems : 36 (Average Length: 117.00 Splits: 0) +Lemmas : 967277 (Deleted: 919155) + Binary : 17304 (Ratio: 1.79%) + Ternary : 3835 (Ratio: 0.40%) + Conflict : 967277 (Average Length: 1011.5 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 967277 (Average: 24.89 Max: 2299 Sum: 24075359) + Executed : 967208 (Average: 24.88 Max: 2299 Sum: 24067405 Ratio: 99.97%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 23.12s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 23.12s + +Iteration 36 +Queue: [(0,115,35,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 37 +Time : 853.276s (Solving: 837.14s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 853.508s + +Choices : 25805718 (Domain: 25602562) +Conflicts : 1000896 (Analyzed: 1000896) +Restarts : 3600 (Average: 278.03 Last: 345) +Model-Level : 4466.0 +Problems : 37 (Average Length: 117.00 Splits: 0) +Lemmas : 1000896 (Deleted: 949749) + Binary : 17560 (Ratio: 1.75%) + Ternary : 3893 (Ratio: 0.39%) + Conflict : 1000896 (Average Length: 1008.0 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1000896 (Average: 24.45 Max: 2299 Sum: 24467080) + Executed : 1000827 (Average: 24.44 Max: 2299 Sum: 24459126 Ratio: 99.97%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 25.43s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 25.43s + +Iteration 37 +Queue: [(0,115,36,True)] +Grounded Until: 115 +Solving... +[start: stats after solve call] + +Models : 0+ +Calls : 38 +Time : 874.951s (Solving: 858.72s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 875.192s + +Choices : 26246723 (Domain: 26041627) +Conflicts : 1029913 (Analyzed: 1029913) +Restarts : 3700 (Average: 278.35 Last: 345) +Model-Level : 4466.0 +Problems : 38 (Average Length: 117.00 Splits: 0) +Lemmas : 1029913 (Deleted: 979384) + Binary : 17925 (Ratio: 1.74%) + Ternary : 3969 (Ratio: 0.39%) + Conflict : 1029913 (Average Length: 1005.7 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1029913 (Average: 24.14 Max: 2299 Sum: 24865814) + Executed : 1029844 (Average: 24.14 Max: 2299 Sum: 24857860 Ratio: 99.97%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +[endof: stats after solve call] +Solving Time: 21.69s +Memory: 939MB (+0MB) +UNKNOWN +Iteration Time: 21.69s + +Iteration 38 +Queue: [(0,115,37,True)] +Grounded Until: 115 +Solving... +*** Info : (planner): INTERRUPTED by signal! +UNKNOWN + +INTERRUPTED : 1 + +Models : 0+ +Calls : 39 +Time : 894.432s (Solving: 878.06s 1st Model: 0.08s Unsat: 0.00s) +CPU Time : 894.664s + +Choices : 26520286 (Domain: 26315166) +Conflicts : 1055029 (Analyzed: 1055029) +Restarts : 3793 (Average: 278.15 Last: 345) +Model-Level : 4466.0 +Problems : 39 (Average Length: 117.00 Splits: 0) +Lemmas : 1055029 (Deleted: 1004987) + Binary : 18003 (Ratio: 1.71%) + Ternary : 4008 (Ratio: 0.38%) + Conflict : 1055029 (Average Length: 1002.8 Ratio: 100.00%) + Loop : 0 (Average Length: 0.0 Ratio: 0.00%) + Other : 0 (Average Length: 0.0 Ratio: 0.00%) +Backjumps : 1055029 (Average: 23.79 Max: 2299 Sum: 25100043) + Executed : 1054960 (Average: 23.78 Max: 2299 Sum: 25092089 Ratio: 99.97%) + Bounded : 69 (Average: 115.28 Max: 117 Sum: 7954 Ratio: 0.03%) + +Rules : 1028283 (Original: 843628) +Atoms : 59257 +Bodies : 791604 (Original: 606949) + Count : 9712 (Original: 27041) +Equivalences : 188391 (Atom=Atom: 172 Body=Body: 0 Other: 188219) +Tight : Yes +Variables : 578204 (Eliminated: 0 Frozen: 191082) +Constraints : 4212455 (Binary: 91.4% Ternary: 7.1% Other: 1.6%) + +Memory Peak : 1003MB +Max. Length : 115 steps +Models : 1 + +