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