1829 lines
64 KiB
Plaintext
1829 lines
64 KiB
Plaintext
|
INFO Running translator.
|
||
|
|
INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-5.pddl']
|
||
|
|
INFO translator arguments: []
|
||
|
|
INFO translator time limit: None
|
||
|
|
INFO translator memory limit: None
|
||
|
|
INFO callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-5.pddl
|
||
|
|
Parsing...
|
||
|
|
Parsing: [0.030s CPU, 0.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
|
||
|
|
|
||
|
|
|