1964 lines
68 KiB
Plaintext
1964 lines
68 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-7.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-7.pddl
|
||
|
|
Parsing...
|
||
|
|
Parsing: [0.040s CPU, 0.041s wall-clock]
|
||
|
|
Normalizing task... [0.000s 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.052s wall-clock]
|
||
|
|
Preparing model... [0.030s CPU, 0.026s wall-clock]
|
||
|
|
Generated 115 rules.
|
||
|
|
Computing model... [0.370s CPU, 0.374s wall-clock]
|
||
|
|
2300 relevant atoms
|
||
|
|
2393 auxiliary atoms
|
||
|
|
4693 final queue length
|
||
|
|
8087 total queue pushes
|
||
|
|
Completing instantiation... [0.690s CPU, 0.687s wall-clock]
|
||
|
|
Instantiating: [1.150s CPU, 1.155s wall-clock]
|
||
|
|
Computing fact groups...
|
||
|
|
Finding invariants...
|
||
|
|
24 initial candidates
|
||
|
|
Finding invariants: [0.120s CPU, 0.117s 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.150s CPU, 0.152s 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.040s wall-clock]
|
||
|
|
Translating task: [0.730s CPU, 0.725s 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.356s 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.250s CPU, 0.241s 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.277s wall-clock]
|
||
|
|
Done! [2.960s CPU, 2.986s wall-clock]
|
||
|
|
planner.py version 0.0.1
|
||
|
|
|
||
|
|
Time: 0.61s
|
||
|
|
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.31s
|
||
|
|
Memory: 572MB (+481MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 1+
|
||
|
|
Calls : 1
|
||
|
|
Time : 9.213s (Solving: 0.13s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 9.112s
|
||
|
|
|
||
|
|
Choices : 21092 (Domain: 20732)
|
||
|
|
Conflicts : 67 (Analyzed: 67)
|
||
|
|
Restarts : 0
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 1 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 67 (Deleted: 0)
|
||
|
|
Binary : 15 (Ratio: 22.39%)
|
||
|
|
Ternary : 0 (Ratio: 0.00%)
|
||
|
|
Conflict : 67 (Average Length: 47.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 67 (Average: 251.30 Max: 1731 Sum: 16837)
|
||
|
|
Executed : 67 (Average: 251.30 Max: 1731 Sum: 16837 Ratio: 100.00%)
|
||
|
|
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 0
|
||
|
|
Atoms : 0
|
||
|
|
Bodies : 0
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 322038 (Eliminated: 0 Frozen: 2990)
|
||
|
|
Constraints : 2575755 (Binary: 95.7% Ternary: 3.2% Other: 1.1%)
|
||
|
|
|
||
|
|
Memory Peak : 816MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.35s
|
||
|
|
Memory: 752MB (+180MB)
|
||
|
|
SAT
|
||
|
|
Testing...
|
||
|
|
NOT SERIALIZABLE
|
||
|
|
Testing Time: 2.79s
|
||
|
|
Memory: 765MB (+13MB)
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 2
|
||
|
|
Time : 35.326s (Solving: 23.14s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 35.236s
|
||
|
|
|
||
|
|
Choices : 2048966 (Domain: 2018629)
|
||
|
|
Conflicts : 24887 (Analyzed: 24887)
|
||
|
|
Restarts : 100 (Average: 248.87 Last: 191)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 2 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 24887 (Deleted: 19122)
|
||
|
|
Binary : 1894 (Ratio: 7.61%)
|
||
|
|
Ternary : 557 (Ratio: 2.24%)
|
||
|
|
Conflict : 24887 (Average Length: 326.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 24887 (Average: 81.42 Max: 1731 Sum: 2026194)
|
||
|
|
Executed : 24853 (Average: 81.26 Max: 1731 Sum: 2022241 Ratio: 99.80%)
|
||
|
|
Bounded : 34 (Average: 116.26 Max: 117 Sum: 3953 Ratio: 0.20%)
|
||
|
|
|
||
|
|
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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4249774 (Binary: 91.4% Ternary: 7.1% Other: 1.5%)
|
||
|
|
|
||
|
|
Memory Peak : 892MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 24.00s
|
||
|
|
Memory: 872MB (+107MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 35.34s
|
||
|
|
|
||
|
|
Iteration 2
|
||
|
|
Queue: [(0,115,1,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 3
|
||
|
|
Time : 60.556s (Solving: 48.23s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 60.476s
|
||
|
|
|
||
|
|
Choices : 3872517 (Domain: 3816021)
|
||
|
|
Conflicts : 51173 (Analyzed: 51173)
|
||
|
|
Restarts : 200 (Average: 255.87 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 3 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 51173 (Deleted: 40835)
|
||
|
|
Binary : 3546 (Ratio: 6.93%)
|
||
|
|
Ternary : 967 (Ratio: 1.89%)
|
||
|
|
Conflict : 51173 (Average Length: 306.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 51173 (Average: 74.73 Max: 1786 Sum: 3824095)
|
||
|
|
Executed : 51131 (Average: 74.63 Max: 1786 Sum: 3819223 Ratio: 99.87%)
|
||
|
|
Bounded : 42 (Average: 116.00 Max: 117 Sum: 4872 Ratio: 0.13%)
|
||
|
|
|
||
|
|
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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4207579 (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: 25.24s
|
||
|
|
Memory: 875MB (+3MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 25.24s
|
||
|
|
|
||
|
|
Iteration 3
|
||
|
|
Queue: [(0,115,2,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 4
|
||
|
|
Time : 78.821s (Solving: 66.40s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 78.748s
|
||
|
|
|
||
|
|
Choices : 4511056 (Domain: 4451872)
|
||
|
|
Conflicts : 76087 (Analyzed: 76087)
|
||
|
|
Restarts : 300 (Average: 253.62 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 4 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 76087 (Deleted: 63602)
|
||
|
|
Binary : 4163 (Ratio: 5.47%)
|
||
|
|
Ternary : 1077 (Ratio: 1.42%)
|
||
|
|
Conflict : 76087 (Average Length: 295.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 76087 (Average: 58.46 Max: 1786 Sum: 4448159)
|
||
|
|
Executed : 76039 (Average: 58.39 Max: 1786 Sum: 4442600 Ratio: 99.88%)
|
||
|
|
Bounded : 48 (Average: 115.81 Max: 117 Sum: 5559 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4207523 (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: 18.28s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 18.28s
|
||
|
|
|
||
|
|
Iteration 4
|
||
|
|
Queue: [(0,115,3,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 5
|
||
|
|
Time : 100.912s (Solving: 88.38s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 100.848s
|
||
|
|
|
||
|
|
Choices : 5900171 (Domain: 5832014)
|
||
|
|
Conflicts : 102155 (Analyzed: 102155)
|
||
|
|
Restarts : 400 (Average: 255.39 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 5 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 102155 (Deleted: 86695)
|
||
|
|
Binary : 5112 (Ratio: 5.00%)
|
||
|
|
Ternary : 1234 (Ratio: 1.21%)
|
||
|
|
Conflict : 102155 (Average Length: 349.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 102155 (Average: 56.91 Max: 1786 Sum: 5814040)
|
||
|
|
Executed : 102102 (Average: 56.85 Max: 1786 Sum: 5807905 Ratio: 99.89%)
|
||
|
|
Bounded : 53 (Average: 115.75 Max: 117 Sum: 6135 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201702 (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.10s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.10s
|
||
|
|
|
||
|
|
Iteration 5
|
||
|
|
Queue: [(0,115,4,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 6
|
||
|
|
Time : 121.772s (Solving: 109.12s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 121.716s
|
||
|
|
|
||
|
|
Choices : 7050553 (Domain: 6975388)
|
||
|
|
Conflicts : 128140 (Analyzed: 128140)
|
||
|
|
Restarts : 500 (Average: 256.28 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 6 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 128140 (Deleted: 113807)
|
||
|
|
Binary : 5766 (Ratio: 4.50%)
|
||
|
|
Ternary : 1295 (Ratio: 1.01%)
|
||
|
|
Conflict : 128140 (Average Length: 452.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 128140 (Average: 54.16 Max: 1786 Sum: 6940222)
|
||
|
|
Executed : 128085 (Average: 54.11 Max: 1786 Sum: 6933860 Ratio: 99.91%)
|
||
|
|
Bounded : 55 (Average: 115.67 Max: 117 Sum: 6362 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201661 (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: 20.87s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.87s
|
||
|
|
|
||
|
|
Iteration 6
|
||
|
|
Queue: [(0,115,5,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 7
|
||
|
|
Time : 145.498s (Solving: 132.72s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 145.452s
|
||
|
|
|
||
|
|
Choices : 8489902 (Domain: 8406773)
|
||
|
|
Conflicts : 154622 (Analyzed: 154622)
|
||
|
|
Restarts : 600 (Average: 257.70 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 7 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 154622 (Deleted: 135874)
|
||
|
|
Binary : 6316 (Ratio: 4.08%)
|
||
|
|
Ternary : 1344 (Ratio: 0.87%)
|
||
|
|
Conflict : 154622 (Average Length: 520.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 154622 (Average: 54.02 Max: 1786 Sum: 8353059)
|
||
|
|
Executed : 154565 (Average: 53.98 Max: 1786 Sum: 8346468 Ratio: 99.92%)
|
||
|
|
Bounded : 57 (Average: 115.63 Max: 117 Sum: 6591 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201661 (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.74s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.74s
|
||
|
|
|
||
|
|
Iteration 7
|
||
|
|
Queue: [(0,115,6,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 8
|
||
|
|
Time : 166.501s (Solving: 153.61s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 166.464s
|
||
|
|
|
||
|
|
Choices : 9706875 (Domain: 9618258)
|
||
|
|
Conflicts : 180223 (Analyzed: 180223)
|
||
|
|
Restarts : 700 (Average: 257.46 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 8 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 180223 (Deleted: 161738)
|
||
|
|
Binary : 6797 (Ratio: 3.77%)
|
||
|
|
Ternary : 1400 (Ratio: 0.78%)
|
||
|
|
Conflict : 180223 (Average Length: 558.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 180223 (Average: 52.96 Max: 1786 Sum: 9545229)
|
||
|
|
Executed : 180165 (Average: 52.93 Max: 1786 Sum: 9538522 Ratio: 99.93%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.01s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.01s
|
||
|
|
|
||
|
|
Iteration 8
|
||
|
|
Queue: [(0,115,7,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 9
|
||
|
|
Time : 187.845s (Solving: 174.84s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 187.816s
|
||
|
|
|
||
|
|
Choices : 10959778 (Domain: 10864511)
|
||
|
|
Conflicts : 206844 (Analyzed: 206844)
|
||
|
|
Restarts : 800 (Average: 258.56 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 9 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 206844 (Deleted: 186023)
|
||
|
|
Binary : 7209 (Ratio: 3.49%)
|
||
|
|
Ternary : 1470 (Ratio: 0.71%)
|
||
|
|
Conflict : 206844 (Average Length: 591.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 206844 (Average: 52.07 Max: 1786 Sum: 10770502)
|
||
|
|
Executed : 206786 (Average: 52.04 Max: 1786 Sum: 10763795 Ratio: 99.94%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.36s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.36s
|
||
|
|
|
||
|
|
Iteration 9
|
||
|
|
Queue: [(0,115,8,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 10
|
||
|
|
Time : 212.388s (Solving: 199.26s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 212.368s
|
||
|
|
|
||
|
|
Choices : 12421955 (Domain: 12315304)
|
||
|
|
Conflicts : 234047 (Analyzed: 234047)
|
||
|
|
Restarts : 900 (Average: 260.05 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 10 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 234047 (Deleted: 210236)
|
||
|
|
Binary : 8240 (Ratio: 3.52%)
|
||
|
|
Ternary : 1663 (Ratio: 0.71%)
|
||
|
|
Conflict : 234047 (Average Length: 635.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 234047 (Average: 52.12 Max: 1786 Sum: 12199350)
|
||
|
|
Executed : 233989 (Average: 52.09 Max: 1786 Sum: 12192643 Ratio: 99.95%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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: 24.56s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.56s
|
||
|
|
|
||
|
|
Iteration 10
|
||
|
|
Queue: [(0,115,9,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 11
|
||
|
|
Time : 235.434s (Solving: 222.18s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 235.424s
|
||
|
|
|
||
|
|
Choices : 13783875 (Domain: 13670603)
|
||
|
|
Conflicts : 260263 (Analyzed: 260263)
|
||
|
|
Restarts : 1000 (Average: 260.26 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 11 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 260263 (Deleted: 235996)
|
||
|
|
Binary : 8858 (Ratio: 3.40%)
|
||
|
|
Ternary : 1738 (Ratio: 0.67%)
|
||
|
|
Conflict : 260263 (Average Length: 643.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 260263 (Average: 51.99 Max: 1786 Sum: 13530807)
|
||
|
|
Executed : 260205 (Average: 51.96 Max: 1786 Sum: 13524100 Ratio: 99.95%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.06s
|
||
|
|
Memory: 875MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.06s
|
||
|
|
|
||
|
|
Iteration 11
|
||
|
|
Queue: [(0,115,10,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 12
|
||
|
|
Time : 259.698s (Solving: 246.34s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 259.696s
|
||
|
|
|
||
|
|
Choices : 14913066 (Domain: 14795788)
|
||
|
|
Conflicts : 285329 (Analyzed: 285329)
|
||
|
|
Restarts : 1100 (Average: 259.39 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 12 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 285329 (Deleted: 260059)
|
||
|
|
Binary : 9956 (Ratio: 3.49%)
|
||
|
|
Ternary : 1947 (Ratio: 0.68%)
|
||
|
|
Conflict : 285329 (Average Length: 677.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 285329 (Average: 51.26 Max: 1786 Sum: 14625644)
|
||
|
|
Executed : 285271 (Average: 51.24 Max: 1786 Sum: 14618937 Ratio: 99.95%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.28s
|
||
|
|
Memory: 939MB (+64MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.28s
|
||
|
|
|
||
|
|
Iteration 12
|
||
|
|
Queue: [(0,115,11,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 13
|
||
|
|
Time : 285.601s (Solving: 272.15s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 285.612s
|
||
|
|
|
||
|
|
Choices : 15585244 (Domain: 15467219)
|
||
|
|
Conflicts : 314350 (Analyzed: 314350)
|
||
|
|
Restarts : 1200 (Average: 261.96 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 13 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 314350 (Deleted: 286524)
|
||
|
|
Binary : 10677 (Ratio: 3.40%)
|
||
|
|
Ternary : 2113 (Ratio: 0.67%)
|
||
|
|
Conflict : 314350 (Average Length: 704.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 314350 (Average: 48.56 Max: 1786 Sum: 15264949)
|
||
|
|
Executed : 314292 (Average: 48.54 Max: 1786 Sum: 15258242 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.92s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 25.92s
|
||
|
|
|
||
|
|
Iteration 13
|
||
|
|
Queue: [(0,115,12,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 14
|
||
|
|
Time : 310.394s (Solving: 296.82s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 310.416s
|
||
|
|
|
||
|
|
Choices : 16324755 (Domain: 16205525)
|
||
|
|
Conflicts : 343275 (Analyzed: 343275)
|
||
|
|
Restarts : 1300 (Average: 264.06 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 14 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 343275 (Deleted: 313472)
|
||
|
|
Binary : 11623 (Ratio: 3.39%)
|
||
|
|
Ternary : 2287 (Ratio: 0.67%)
|
||
|
|
Conflict : 343275 (Average Length: 731.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 343275 (Average: 46.50 Max: 1786 Sum: 15963772)
|
||
|
|
Executed : 343217 (Average: 46.48 Max: 1786 Sum: 15957065 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.81s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.81s
|
||
|
|
|
||
|
|
Iteration 14
|
||
|
|
Queue: [(0,115,13,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 15
|
||
|
|
Time : 333.377s (Solving: 319.68s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 333.408s
|
||
|
|
|
||
|
|
Choices : 16838907 (Domain: 16718886)
|
||
|
|
Conflicts : 370547 (Analyzed: 370547)
|
||
|
|
Restarts : 1400 (Average: 264.68 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 15 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 370547 (Deleted: 338590)
|
||
|
|
Binary : 12054 (Ratio: 3.25%)
|
||
|
|
Ternary : 2361 (Ratio: 0.64%)
|
||
|
|
Conflict : 370547 (Average Length: 743.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 370547 (Average: 44.38 Max: 1786 Sum: 16443188)
|
||
|
|
Executed : 370489 (Average: 44.36 Max: 1786 Sum: 16436481 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.00s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.00s
|
||
|
|
|
||
|
|
Iteration 15
|
||
|
|
Queue: [(0,115,14,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 16
|
||
|
|
Time : 357.105s (Solving: 343.27s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 357.148s
|
||
|
|
|
||
|
|
Choices : 17484833 (Domain: 17362930)
|
||
|
|
Conflicts : 400960 (Analyzed: 400960)
|
||
|
|
Restarts : 1500 (Average: 267.31 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 16 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 400960 (Deleted: 367039)
|
||
|
|
Binary : 12857 (Ratio: 3.21%)
|
||
|
|
Ternary : 2521 (Ratio: 0.63%)
|
||
|
|
Conflict : 400960 (Average Length: 766.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 400960 (Average: 42.50 Max: 1786 Sum: 17042678)
|
||
|
|
Executed : 400902 (Average: 42.49 Max: 1786 Sum: 17035971 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.74s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.74s
|
||
|
|
|
||
|
|
Iteration 16
|
||
|
|
Queue: [(0,115,15,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 17
|
||
|
|
Time : 379.318s (Solving: 365.38s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 379.368s
|
||
|
|
|
||
|
|
Choices : 17981886 (Domain: 17859175)
|
||
|
|
Conflicts : 428497 (Analyzed: 428497)
|
||
|
|
Restarts : 1600 (Average: 267.81 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 17 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 428497 (Deleted: 393449)
|
||
|
|
Binary : 13283 (Ratio: 3.10%)
|
||
|
|
Ternary : 2579 (Ratio: 0.60%)
|
||
|
|
Conflict : 428497 (Average Length: 773.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 428497 (Average: 40.85 Max: 1786 Sum: 17502949)
|
||
|
|
Executed : 428439 (Average: 40.83 Max: 1786 Sum: 17496242 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.22s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.23s
|
||
|
|
|
||
|
|
Iteration 17
|
||
|
|
Queue: [(0,115,16,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 18
|
||
|
|
Time : 402.993s (Solving: 388.95s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 403.052s
|
||
|
|
|
||
|
|
Choices : 18639848 (Domain: 18515837)
|
||
|
|
Conflicts : 457858 (Analyzed: 457858)
|
||
|
|
Restarts : 1700 (Average: 269.33 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 18 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 457858 (Deleted: 422353)
|
||
|
|
Binary : 13992 (Ratio: 3.06%)
|
||
|
|
Ternary : 2713 (Ratio: 0.59%)
|
||
|
|
Conflict : 457858 (Average Length: 799.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 457858 (Average: 39.57 Max: 1786 Sum: 18116027)
|
||
|
|
Executed : 457800 (Average: 39.55 Max: 1786 Sum: 18109320 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.69s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.69s
|
||
|
|
|
||
|
|
Iteration 18
|
||
|
|
Queue: [(0,115,17,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 19
|
||
|
|
Time : 423.787s (Solving: 409.63s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 423.856s
|
||
|
|
|
||
|
|
Choices : 19101847 (Domain: 18977218)
|
||
|
|
Conflicts : 482691 (Analyzed: 482691)
|
||
|
|
Restarts : 1800 (Average: 268.16 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 19 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 482691 (Deleted: 447512)
|
||
|
|
Binary : 14510 (Ratio: 3.01%)
|
||
|
|
Ternary : 2801 (Ratio: 0.58%)
|
||
|
|
Conflict : 482691 (Average Length: 821.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 482691 (Average: 38.39 Max: 1786 Sum: 18532192)
|
||
|
|
Executed : 482633 (Average: 38.38 Max: 1786 Sum: 18525485 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.81s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.81s
|
||
|
|
|
||
|
|
Iteration 19
|
||
|
|
Queue: [(0,115,18,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 20
|
||
|
|
Time : 446.358s (Solving: 432.06s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 446.436s
|
||
|
|
|
||
|
|
Choices : 19727025 (Domain: 19601443)
|
||
|
|
Conflicts : 511410 (Analyzed: 511410)
|
||
|
|
Restarts : 1900 (Average: 269.16 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 20 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 511410 (Deleted: 473835)
|
||
|
|
Binary : 15075 (Ratio: 2.95%)
|
||
|
|
Ternary : 2971 (Ratio: 0.58%)
|
||
|
|
Conflict : 511410 (Average Length: 833.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 511410 (Average: 37.37 Max: 1786 Sum: 19110808)
|
||
|
|
Executed : 511352 (Average: 37.36 Max: 1786 Sum: 19104101 Ratio: 99.96%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.58s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.58s
|
||
|
|
|
||
|
|
Iteration 20
|
||
|
|
Queue: [(0,115,19,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 21
|
||
|
|
Time : 466.661s (Solving: 452.27s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 466.748s
|
||
|
|
|
||
|
|
Choices : 20253628 (Domain: 20127111)
|
||
|
|
Conflicts : 537402 (Analyzed: 537402)
|
||
|
|
Restarts : 2000 (Average: 268.70 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 21 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 537402 (Deleted: 498510)
|
||
|
|
Binary : 15567 (Ratio: 2.90%)
|
||
|
|
Ternary : 3104 (Ratio: 0.58%)
|
||
|
|
Conflict : 537402 (Average Length: 845.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 537402 (Average: 36.45 Max: 1786 Sum: 19587778)
|
||
|
|
Executed : 537344 (Average: 36.44 Max: 1786 Sum: 19581071 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.31s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.31s
|
||
|
|
|
||
|
|
Iteration 21
|
||
|
|
Queue: [(0,115,20,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 22
|
||
|
|
Time : 488.409s (Solving: 473.91s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 488.508s
|
||
|
|
|
||
|
|
Choices : 20680606 (Domain: 20553451)
|
||
|
|
Conflicts : 564339 (Analyzed: 564339)
|
||
|
|
Restarts : 2100 (Average: 268.73 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 22 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 564339 (Deleted: 523616)
|
||
|
|
Binary : 15907 (Ratio: 2.82%)
|
||
|
|
Ternary : 3187 (Ratio: 0.56%)
|
||
|
|
Conflict : 564339 (Average Length: 860.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 564339 (Average: 35.38 Max: 1786 Sum: 19966992)
|
||
|
|
Executed : 564281 (Average: 35.37 Max: 1786 Sum: 19960285 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.76s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.76s
|
||
|
|
|
||
|
|
Iteration 22
|
||
|
|
Queue: [(0,115,21,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 23
|
||
|
|
Time : 509.601s (Solving: 494.96s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 509.708s
|
||
|
|
|
||
|
|
Choices : 21157210 (Domain: 21028550)
|
||
|
|
Conflicts : 590789 (Analyzed: 590789)
|
||
|
|
Restarts : 2200 (Average: 268.54 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 23 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 590789 (Deleted: 549647)
|
||
|
|
Binary : 16276 (Ratio: 2.75%)
|
||
|
|
Ternary : 3277 (Ratio: 0.55%)
|
||
|
|
Conflict : 590789 (Average Length: 876.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 590789 (Average: 34.53 Max: 1786 Sum: 20397175)
|
||
|
|
Executed : 590731 (Average: 34.51 Max: 1786 Sum: 20390468 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.20s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.20s
|
||
|
|
|
||
|
|
Iteration 23
|
||
|
|
Queue: [(0,115,22,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 24
|
||
|
|
Time : 530.103s (Solving: 515.37s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 530.216s
|
||
|
|
|
||
|
|
Choices : 21566865 (Domain: 21437541)
|
||
|
|
Conflicts : 619802 (Analyzed: 619802)
|
||
|
|
Restarts : 2300 (Average: 269.48 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 24 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 619802 (Deleted: 578266)
|
||
|
|
Binary : 16575 (Ratio: 2.67%)
|
||
|
|
Ternary : 3362 (Ratio: 0.54%)
|
||
|
|
Conflict : 619802 (Average Length: 891.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 619802 (Average: 33.51 Max: 1786 Sum: 20768694)
|
||
|
|
Executed : 619744 (Average: 33.50 Max: 1786 Sum: 20761987 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.51s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.51s
|
||
|
|
|
||
|
|
Iteration 24
|
||
|
|
Queue: [(0,115,23,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 25
|
||
|
|
Time : 550.333s (Solving: 535.48s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 550.456s
|
||
|
|
|
||
|
|
Choices : 21982303 (Domain: 21851647)
|
||
|
|
Conflicts : 646020 (Analyzed: 646020)
|
||
|
|
Restarts : 2400 (Average: 269.18 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 25 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 646020 (Deleted: 603231)
|
||
|
|
Binary : 16982 (Ratio: 2.63%)
|
||
|
|
Ternary : 3418 (Ratio: 0.53%)
|
||
|
|
Conflict : 646020 (Average Length: 900.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 646020 (Average: 32.72 Max: 1786 Sum: 21137360)
|
||
|
|
Executed : 645962 (Average: 32.71 Max: 1786 Sum: 21130653 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.24s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.24s
|
||
|
|
|
||
|
|
Iteration 25
|
||
|
|
Queue: [(0,115,24,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 26
|
||
|
|
Time : 569.096s (Solving: 554.14s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 569.228s
|
||
|
|
|
||
|
|
Choices : 22425207 (Domain: 22294014)
|
||
|
|
Conflicts : 670462 (Analyzed: 670462)
|
||
|
|
Restarts : 2500 (Average: 268.18 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 26 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 670462 (Deleted: 625776)
|
||
|
|
Binary : 17232 (Ratio: 2.57%)
|
||
|
|
Ternary : 3491 (Ratio: 0.52%)
|
||
|
|
Conflict : 670462 (Average Length: 900.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 670462 (Average: 32.11 Max: 1786 Sum: 21531352)
|
||
|
|
Executed : 670404 (Average: 32.10 Max: 1786 Sum: 21524645 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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: 18.77s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 18.77s
|
||
|
|
|
||
|
|
Iteration 26
|
||
|
|
Queue: [(0,115,25,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 27
|
||
|
|
Time : 587.844s (Solving: 572.77s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 587.984s
|
||
|
|
|
||
|
|
Choices : 22777286 (Domain: 22645410)
|
||
|
|
Conflicts : 695275 (Analyzed: 695275)
|
||
|
|
Restarts : 2600 (Average: 267.41 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 27 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 695275 (Deleted: 652305)
|
||
|
|
Binary : 17448 (Ratio: 2.51%)
|
||
|
|
Ternary : 3540 (Ratio: 0.51%)
|
||
|
|
Conflict : 695275 (Average Length: 903.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 695275 (Average: 31.41 Max: 1786 Sum: 21841035)
|
||
|
|
Executed : 695217 (Average: 31.40 Max: 1786 Sum: 21834328 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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: 18.76s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 18.76s
|
||
|
|
|
||
|
|
Iteration 27
|
||
|
|
Queue: [(0,115,26,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 28
|
||
|
|
Time : 610.776s (Solving: 595.57s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 610.928s
|
||
|
|
|
||
|
|
Choices : 23214111 (Domain: 23081639)
|
||
|
|
Conflicts : 726046 (Analyzed: 726046)
|
||
|
|
Restarts : 2700 (Average: 268.91 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 28 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 726046 (Deleted: 682038)
|
||
|
|
Binary : 17753 (Ratio: 2.45%)
|
||
|
|
Ternary : 3653 (Ratio: 0.50%)
|
||
|
|
Conflict : 726046 (Average Length: 906.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 726046 (Average: 30.63 Max: 1786 Sum: 22239299)
|
||
|
|
Executed : 725988 (Average: 30.62 Max: 1786 Sum: 22232592 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.94s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.95s
|
||
|
|
|
||
|
|
Iteration 28
|
||
|
|
Queue: [(0,115,27,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 29
|
||
|
|
Time : 632.385s (Solving: 617.03s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 632.548s
|
||
|
|
|
||
|
|
Choices : 23667160 (Domain: 23533806)
|
||
|
|
Conflicts : 753519 (Analyzed: 753519)
|
||
|
|
Restarts : 2800 (Average: 269.11 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 29 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 753519 (Deleted: 706206)
|
||
|
|
Binary : 18045 (Ratio: 2.39%)
|
||
|
|
Ternary : 3715 (Ratio: 0.49%)
|
||
|
|
Conflict : 753519 (Average Length: 910.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 753519 (Average: 30.06 Max: 1786 Sum: 22648817)
|
||
|
|
Executed : 753461 (Average: 30.05 Max: 1786 Sum: 22642110 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.62s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.62s
|
||
|
|
|
||
|
|
Iteration 29
|
||
|
|
Queue: [(0,115,28,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 30
|
||
|
|
Time : 652.470s (Solving: 637.01s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 652.644s
|
||
|
|
|
||
|
|
Choices : 24122919 (Domain: 23988579)
|
||
|
|
Conflicts : 779721 (Analyzed: 779721)
|
||
|
|
Restarts : 2900 (Average: 268.87 Last: 325)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 30 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 779721 (Deleted: 732791)
|
||
|
|
Binary : 18282 (Ratio: 2.34%)
|
||
|
|
Ternary : 3769 (Ratio: 0.48%)
|
||
|
|
Conflict : 779721 (Average Length: 906.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 779721 (Average: 29.57 Max: 1786 Sum: 23054411)
|
||
|
|
Executed : 779663 (Average: 29.56 Max: 1786 Sum: 23047704 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.10s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.10s
|
||
|
|
|
||
|
|
Iteration 30
|
||
|
|
Queue: [(0,115,29,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 31
|
||
|
|
Time : 676.046s (Solving: 660.47s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 676.228s
|
||
|
|
|
||
|
|
Choices : 24597842 (Domain: 24462468)
|
||
|
|
Conflicts : 811224 (Analyzed: 811224)
|
||
|
|
Restarts : 3000 (Average: 270.41 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 31 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 811224 (Deleted: 764109)
|
||
|
|
Binary : 18542 (Ratio: 2.29%)
|
||
|
|
Ternary : 3826 (Ratio: 0.47%)
|
||
|
|
Conflict : 811224 (Average Length: 907.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 811224 (Average: 28.95 Max: 1786 Sum: 23488210)
|
||
|
|
Executed : 811166 (Average: 28.95 Max: 1786 Sum: 23481503 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.59s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.59s
|
||
|
|
|
||
|
|
Iteration 31
|
||
|
|
Queue: [(0,115,30,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 32
|
||
|
|
Time : 697.320s (Solving: 681.63s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 697.512s
|
||
|
|
|
||
|
|
Choices : 24938437 (Domain: 24802939)
|
||
|
|
Conflicts : 839742 (Analyzed: 839742)
|
||
|
|
Restarts : 3100 (Average: 270.88 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 32 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 839742 (Deleted: 791748)
|
||
|
|
Binary : 18814 (Ratio: 2.24%)
|
||
|
|
Ternary : 3884 (Ratio: 0.46%)
|
||
|
|
Conflict : 839742 (Average Length: 911.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 839742 (Average: 28.33 Max: 1786 Sum: 23790263)
|
||
|
|
Executed : 839684 (Average: 28.32 Max: 1786 Sum: 23783556 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.28s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.28s
|
||
|
|
|
||
|
|
Iteration 32
|
||
|
|
Queue: [(0,115,31,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 33
|
||
|
|
Time : 718.490s (Solving: 702.69s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 718.692s
|
||
|
|
|
||
|
|
Choices : 25366137 (Domain: 25230264)
|
||
|
|
Conflicts : 868660 (Analyzed: 868660)
|
||
|
|
Restarts : 3200 (Average: 271.46 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 33 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 868660 (Deleted: 819464)
|
||
|
|
Binary : 19051 (Ratio: 2.19%)
|
||
|
|
Ternary : 3928 (Ratio: 0.45%)
|
||
|
|
Conflict : 868660 (Average Length: 911.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 868660 (Average: 27.83 Max: 1786 Sum: 24175966)
|
||
|
|
Executed : 868602 (Average: 27.82 Max: 1786 Sum: 24169259 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.18s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.18s
|
||
|
|
|
||
|
|
Iteration 33
|
||
|
|
Queue: [(0,115,32,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 34
|
||
|
|
Time : 740.215s (Solving: 724.31s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 740.424s
|
||
|
|
|
||
|
|
Choices : 25730893 (Domain: 25594878)
|
||
|
|
Conflicts : 897958 (Analyzed: 897958)
|
||
|
|
Restarts : 3300 (Average: 272.11 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 34 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 897958 (Deleted: 847731)
|
||
|
|
Binary : 19266 (Ratio: 2.15%)
|
||
|
|
Ternary : 3993 (Ratio: 0.44%)
|
||
|
|
Conflict : 897958 (Average Length: 913.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 897958 (Average: 27.28 Max: 1786 Sum: 24499836)
|
||
|
|
Executed : 897900 (Average: 27.28 Max: 1786 Sum: 24493129 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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 34
|
||
|
|
Queue: [(0,115,33,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 35
|
||
|
|
Time : 761.098s (Solving: 745.08s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 761.316s
|
||
|
|
|
||
|
|
Choices : 26170326 (Domain: 26033413)
|
||
|
|
Conflicts : 926147 (Analyzed: 926147)
|
||
|
|
Restarts : 3400 (Average: 272.40 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 35 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 926147 (Deleted: 876371)
|
||
|
|
Binary : 19483 (Ratio: 2.10%)
|
||
|
|
Ternary : 4055 (Ratio: 0.44%)
|
||
|
|
Conflict : 926147 (Average Length: 916.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 926147 (Average: 26.88 Max: 1786 Sum: 24896913)
|
||
|
|
Executed : 926089 (Average: 26.88 Max: 1786 Sum: 24890206 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.89s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.89s
|
||
|
|
|
||
|
|
Iteration 35
|
||
|
|
Queue: [(0,115,34,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 36
|
||
|
|
Time : 781.678s (Solving: 765.56s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 781.904s
|
||
|
|
|
||
|
|
Choices : 26554069 (Domain: 26416150)
|
||
|
|
Conflicts : 951483 (Analyzed: 951483)
|
||
|
|
Restarts : 3500 (Average: 271.85 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 36 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 951483 (Deleted: 900418)
|
||
|
|
Binary : 19900 (Ratio: 2.09%)
|
||
|
|
Ternary : 4159 (Ratio: 0.44%)
|
||
|
|
Conflict : 951483 (Average Length: 912.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 951483 (Average: 26.53 Max: 1786 Sum: 25243389)
|
||
|
|
Executed : 951425 (Average: 26.52 Max: 1786 Sum: 25236682 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.59s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.59s
|
||
|
|
|
||
|
|
Iteration 36
|
||
|
|
Queue: [(0,115,35,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 37
|
||
|
|
Time : 801.127s (Solving: 784.90s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 801.364s
|
||
|
|
|
||
|
|
Choices : 26892139 (Domain: 26753297)
|
||
|
|
Conflicts : 979217 (Analyzed: 979217)
|
||
|
|
Restarts : 3600 (Average: 272.00 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 37 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 979217 (Deleted: 928036)
|
||
|
|
Binary : 20098 (Ratio: 2.05%)
|
||
|
|
Ternary : 4198 (Ratio: 0.43%)
|
||
|
|
Conflict : 979217 (Average Length: 912.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 979217 (Average: 26.09 Max: 1786 Sum: 25546029)
|
||
|
|
Executed : 979159 (Average: 26.08 Max: 1786 Sum: 25539322 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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: 19.46s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 19.46s
|
||
|
|
|
||
|
|
Iteration 37
|
||
|
|
Queue: [(0,115,36,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 38
|
||
|
|
Time : 818.601s (Solving: 802.27s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 818.848s
|
||
|
|
|
||
|
|
Choices : 27181636 (Domain: 27042680)
|
||
|
|
Conflicts : 1007186 (Analyzed: 1007186)
|
||
|
|
Restarts : 3700 (Average: 272.21 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 38 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 1007186 (Deleted: 955194)
|
||
|
|
Binary : 20322 (Ratio: 2.02%)
|
||
|
|
Ternary : 4254 (Ratio: 0.42%)
|
||
|
|
Conflict : 1007186 (Average Length: 909.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1007186 (Average: 25.61 Max: 1786 Sum: 25796334)
|
||
|
|
Executed : 1007128 (Average: 25.61 Max: 1786 Sum: 25789627 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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: 17.48s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 17.48s
|
||
|
|
|
||
|
|
Iteration 38
|
||
|
|
Queue: [(0,115,37,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 39
|
||
|
|
Time : 838.181s (Solving: 821.75s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 838.436s
|
||
|
|
|
||
|
|
Choices : 27479457 (Domain: 27340496)
|
||
|
|
Conflicts : 1034205 (Analyzed: 1034205)
|
||
|
|
Restarts : 3800 (Average: 272.16 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 39 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 1034205 (Deleted: 979655)
|
||
|
|
Binary : 20519 (Ratio: 1.98%)
|
||
|
|
Ternary : 4287 (Ratio: 0.41%)
|
||
|
|
Conflict : 1034205 (Average Length: 909.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1034205 (Average: 25.20 Max: 1786 Sum: 26058309)
|
||
|
|
Executed : 1034147 (Average: 25.19 Max: 1786 Sum: 26051602 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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: 19.59s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 19.59s
|
||
|
|
|
||
|
|
Iteration 39
|
||
|
|
Queue: [(0,115,38,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 40
|
||
|
|
Time : 860.478s (Solving: 843.93s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 860.744s
|
||
|
|
|
||
|
|
Choices : 27848665 (Domain: 27709206)
|
||
|
|
Conflicts : 1065225 (Analyzed: 1065225)
|
||
|
|
Restarts : 3900 (Average: 273.13 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 40 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 1065225 (Deleted: 1012000)
|
||
|
|
Binary : 20669 (Ratio: 1.94%)
|
||
|
|
Ternary : 4323 (Ratio: 0.41%)
|
||
|
|
Conflict : 1065225 (Average Length: 908.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1065225 (Average: 24.77 Max: 1786 Sum: 26390596)
|
||
|
|
Executed : 1065167 (Average: 24.77 Max: 1786 Sum: 26383889 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.31s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.31s
|
||
|
|
|
||
|
|
Iteration 40
|
||
|
|
Queue: [(0,115,39,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 41
|
||
|
|
Time : 882.690s (Solving: 866.04s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 882.964s
|
||
|
|
|
||
|
|
Choices : 28246722 (Domain: 28106873)
|
||
|
|
Conflicts : 1094300 (Analyzed: 1094300)
|
||
|
|
Restarts : 4000 (Average: 273.57 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 41 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 1094300 (Deleted: 1039235)
|
||
|
|
Binary : 20793 (Ratio: 1.90%)
|
||
|
|
Ternary : 4351 (Ratio: 0.40%)
|
||
|
|
Conflict : 1094300 (Average Length: 905.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1094300 (Average: 24.45 Max: 1786 Sum: 26750286)
|
||
|
|
Executed : 1094242 (Average: 24.44 Max: 1786 Sum: 26743579 Ratio: 99.97%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (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.22s
|
||
|
|
Memory: 939MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.22s
|
||
|
|
|
||
|
|
Iteration 41
|
||
|
|
Queue: [(0,115,40,True)]
|
||
|
|
Grounded Until: 115
|
||
|
|
Solving...
|
||
|
|
*** Info : (planner): INTERRUPTED by signal!
|
||
|
|
UNKNOWN
|
||
|
|
|
||
|
|
INTERRUPTED : 1
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 42
|
||
|
|
Time : 894.406s (Solving: 877.62s 1st Model: 0.11s Unsat: 0.00s)
|
||
|
|
CPU Time : 894.664s
|
||
|
|
|
||
|
|
Choices : 28389015 (Domain: 28249163)
|
||
|
|
Conflicts : 1107975 (Analyzed: 1107975)
|
||
|
|
Restarts : 4057 (Average: 273.10 Last: 326)
|
||
|
|
Model-Level : 4372.0
|
||
|
|
Problems : 42 (Average Length: 117.00 Splits: 0)
|
||
|
|
Lemmas : 1107975 (Deleted: 1054557)
|
||
|
|
Binary : 20823 (Ratio: 1.88%)
|
||
|
|
Ternary : 4364 (Ratio: 0.39%)
|
||
|
|
Conflict : 1107975 (Average Length: 906.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 1107975 (Average: 24.25 Max: 1786 Sum: 26871982)
|
||
|
|
Executed : 1107917 (Average: 24.25 Max: 1786 Sum: 26865275 Ratio: 99.98%)
|
||
|
|
Bounded : 58 (Average: 115.64 Max: 117 Sum: 6707 Ratio: 0.02%)
|
||
|
|
|
||
|
|
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 : 578090 (Eliminated: 0 Frozen: 191082)
|
||
|
|
Constraints : 4201647 (Binary: 91.4% Ternary: 7.1% Other: 1.6%)
|
||
|
|
|
||
|
|
Memory Peak : 1003MB
|
||
|
|
Max. Length : 115 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
|