1649 lines
56 KiB
Plaintext
1649 lines
56 KiB
Plaintext
|
INFO Running translator.
|
||
|
|
INFO translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-4.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/elevator-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/elevator-sequential-satisficing/instances/instance-4.pddl
|
||
|
|
Parsing...
|
||
|
|
Parsing: [0.030s CPU, 0.041s wall-clock]
|
||
|
|
Normalizing task... [0.010s CPU, 0.002s wall-clock]
|
||
|
|
Instantiating...
|
||
|
|
Generating Datalog program... [0.010s CPU, 0.011s wall-clock]
|
||
|
|
Normalizing Datalog program...
|
||
|
|
Normalizing Datalog program: [0.020s CPU, 0.024s wall-clock]
|
||
|
|
Preparing model... [0.030s CPU, 0.030s wall-clock]
|
||
|
|
Generated 46 rules.
|
||
|
|
Computing model... [0.710s CPU, 0.712s wall-clock]
|
||
|
|
6004 relevant atoms
|
||
|
|
3524 auxiliary atoms
|
||
|
|
9528 final queue length
|
||
|
|
18930 total queue pushes
|
||
|
|
Completing instantiation... [1.770s CPU, 1.769s wall-clock]
|
||
|
|
Instantiating: [2.550s CPU, 2.555s wall-clock]
|
||
|
|
Computing fact groups...
|
||
|
|
Finding invariants...
|
||
|
|
12 initial candidates
|
||
|
|
Finding invariants: [0.040s CPU, 0.042s wall-clock]
|
||
|
|
Checking invariant weight... [0.010s CPU, 0.003s wall-clock]
|
||
|
|
Instantiating groups... [0.090s CPU, 0.096s wall-clock]
|
||
|
|
Collecting mutex groups... [0.010s CPU, 0.004s wall-clock]
|
||
|
|
Choosing groups...
|
||
|
|
0 uncovered facts
|
||
|
|
Choosing groups: [0.010s CPU, 0.011s wall-clock]
|
||
|
|
Building translation key... [0.010s CPU, 0.007s wall-clock]
|
||
|
|
Computing fact groups: [0.190s CPU, 0.189s wall-clock]
|
||
|
|
Building STRIPS to SAS dictionary... [0.000s CPU, 0.004s wall-clock]
|
||
|
|
Building dictionary for full mutex groups... [0.010s CPU, 0.003s wall-clock]
|
||
|
|
Building mutex information...
|
||
|
|
Building mutex information: [0.000s CPU, 0.004s wall-clock]
|
||
|
|
Translating task...
|
||
|
|
Processing axioms...
|
||
|
|
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
|
||
|
|
Processing axioms: [0.080s CPU, 0.081s wall-clock]
|
||
|
|
Translating task: [1.480s CPU, 1.479s wall-clock]
|
||
|
|
0 effect conditions simplified
|
||
|
|
0 implied preconditions added
|
||
|
|
Detecting unreachable propositions...
|
||
|
|
0 operators removed
|
||
|
|
0 axioms removed
|
||
|
|
34 propositions removed
|
||
|
|
Detecting unreachable propositions: [0.820s CPU, 0.822s wall-clock]
|
||
|
|
Reordering and filtering variables...
|
||
|
|
34 of 34 variables necessary.
|
||
|
|
0 of 34 mutex groups necessary.
|
||
|
|
5072 of 5072 operators necessary.
|
||
|
|
0 of 0 axiom rules necessary.
|
||
|
|
Reordering and filtering variables: [0.240s CPU, 0.238s wall-clock]
|
||
|
|
Translator variables: 34
|
||
|
|
Translator derived variables: 0
|
||
|
|
Translator facts: 592
|
||
|
|
Translator goal facts: 26
|
||
|
|
Translator mutex groups: 0
|
||
|
|
Translator total mutex groups size: 0
|
||
|
|
Translator operators: 5072
|
||
|
|
Translator axioms: 0
|
||
|
|
Translator task size: 30532
|
||
|
|
Translator peak memory: 56012 KB
|
||
|
|
Writing output... [0.520s CPU, 0.559s wall-clock]
|
||
|
|
Done! [5.920s CPU, 5.964s wall-clock]
|
||
|
|
planner.py version 0.0.1
|
||
|
|
|
||
|
|
Time: 1.24s
|
||
|
|
Memory: 133MB
|
||
|
|
|
||
|
|
Iteration 1
|
||
|
|
Queue: [(0,35,0,True)]
|
||
|
|
Grounded Until: 0
|
||
|
|
Expected Memory: 133MB
|
||
|
|
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]), ('check', [35])]
|
||
|
|
Grounding Time: 2.94s
|
||
|
|
Memory: 375MB (+242MB)
|
||
|
|
Unblocking actions...
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 1+
|
||
|
|
Calls : 1
|
||
|
|
Time : 6.516s (Solving: 0.21s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 6.332s
|
||
|
|
|
||
|
|
Choices : 13442 (Domain: 13418)
|
||
|
|
Conflicts : 184 (Analyzed: 184)
|
||
|
|
Restarts : 2 (Average: 92.00 Last: 24)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 1 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 184 (Deleted: 0)
|
||
|
|
Binary : 29 (Ratio: 15.76%)
|
||
|
|
Ternary : 31 (Ratio: 16.85%)
|
||
|
|
Conflict : 184 (Average Length: 166.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 184 (Average: 53.40 Max: 571 Sum: 9825)
|
||
|
|
Executed : 184 (Average: 53.40 Max: 571 Sum: 9825 Ratio: 100.00%)
|
||
|
|
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
|
||
|
|
|
||
|
|
Rules : 0
|
||
|
|
Atoms : 0
|
||
|
|
Bodies : 0
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 214565 (Eliminated: 0 Frozen: 19194)
|
||
|
|
Constraints : 1466315 (Binary: 97.3% Ternary: 1.3% Other: 1.4%)
|
||
|
|
|
||
|
|
Memory Peak : 588MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 0.35s
|
||
|
|
Memory: 524MB (+149MB)
|
||
|
|
SAT
|
||
|
|
Testing...
|
||
|
|
NOT SERIALIZABLE
|
||
|
|
Testing Time: 2.42s
|
||
|
|
Memory: 542MB (+18MB)
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 2
|
||
|
|
Time : 97.973s (Solving: 90.04s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 97.828s
|
||
|
|
|
||
|
|
Choices : 7085552 (Domain: 7085528)
|
||
|
|
Conflicts : 32782 (Analyzed: 32782)
|
||
|
|
Restarts : 102 (Average: 321.39 Last: 305)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 2 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 32782 (Deleted: 24924)
|
||
|
|
Binary : 953 (Ratio: 2.91%)
|
||
|
|
Ternary : 973 (Ratio: 2.97%)
|
||
|
|
Conflict : 32782 (Average Length: 441.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 32782 (Average: 214.59 Max: 3860 Sum: 7034755)
|
||
|
|
Executed : 32697 (Average: 214.50 Max: 3860 Sum: 7031682 Ratio: 99.96%)
|
||
|
|
Bounded : 85 (Average: 36.15 Max: 37 Sum: 3073 Ratio: 0.04%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1940687 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 588MB
|
||
|
|
Max. Length : 0 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 90.21s
|
||
|
|
Memory: 557MB (+15MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 97.73s
|
||
|
|
|
||
|
|
Iteration 2
|
||
|
|
Queue: [(0,35,1,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 3
|
||
|
|
Time : 156.485s (Solving: 148.50s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 156.364s
|
||
|
|
|
||
|
|
Choices : 12327759 (Domain: 12327735)
|
||
|
|
Conflicts : 64198 (Analyzed: 64198)
|
||
|
|
Restarts : 202 (Average: 317.81 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 3 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 64198 (Deleted: 51604)
|
||
|
|
Binary : 1641 (Ratio: 2.56%)
|
||
|
|
Ternary : 1572 (Ratio: 2.45%)
|
||
|
|
Conflict : 64198 (Average Length: 634.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 64198 (Average: 189.56 Max: 4236 Sum: 12169322)
|
||
|
|
Executed : 64098 (Average: 189.50 Max: 4236 Sum: 12165766 Ratio: 99.97%)
|
||
|
|
Bounded : 100 (Average: 35.56 Max: 37 Sum: 3556 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1927277 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 588MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 58.54s
|
||
|
|
Memory: 557MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 58.54s
|
||
|
|
|
||
|
|
Iteration 3
|
||
|
|
Queue: [(0,35,2,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 4
|
||
|
|
Time : 179.449s (Solving: 171.41s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 179.340s
|
||
|
|
|
||
|
|
Choices : 13347525 (Domain: 13347501)
|
||
|
|
Conflicts : 90597 (Analyzed: 90597)
|
||
|
|
Restarts : 302 (Average: 299.99 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 4 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 90597 (Deleted: 74374)
|
||
|
|
Binary : 2014 (Ratio: 2.22%)
|
||
|
|
Ternary : 1911 (Ratio: 2.11%)
|
||
|
|
Conflict : 90597 (Average Length: 834.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 90597 (Average: 144.16 Max: 4236 Sum: 13060353)
|
||
|
|
Executed : 90486 (Average: 144.12 Max: 4236 Sum: 13056606 Ratio: 99.97%)
|
||
|
|
Bounded : 111 (Average: 33.76 Max: 37 Sum: 3747 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1926043 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 588MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.98s
|
||
|
|
Memory: 557MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.98s
|
||
|
|
|
||
|
|
Iteration 4
|
||
|
|
Queue: [(0,35,3,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 5
|
||
|
|
Time : 201.643s (Solving: 193.56s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 201.540s
|
||
|
|
|
||
|
|
Choices : 14095121 (Domain: 14095097)
|
||
|
|
Conflicts : 116349 (Analyzed: 116349)
|
||
|
|
Restarts : 402 (Average: 289.43 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 5 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 116349 (Deleted: 98780)
|
||
|
|
Binary : 2226 (Ratio: 1.91%)
|
||
|
|
Ternary : 2108 (Ratio: 1.81%)
|
||
|
|
Conflict : 116349 (Average Length: 975.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 116349 (Average: 117.55 Max: 4236 Sum: 13676917)
|
||
|
|
Executed : 116233 (Average: 117.52 Max: 4236 Sum: 13673129 Ratio: 99.97%)
|
||
|
|
Bounded : 116 (Average: 32.66 Max: 37 Sum: 3788 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1925001 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 588MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.20s
|
||
|
|
Memory: 557MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.20s
|
||
|
|
|
||
|
|
Iteration 5
|
||
|
|
Queue: [(0,35,4,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 6
|
||
|
|
Time : 225.512s (Solving: 217.38s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 225.420s
|
||
|
|
|
||
|
|
Choices : 15004909 (Domain: 15004885)
|
||
|
|
Conflicts : 144273 (Analyzed: 144273)
|
||
|
|
Restarts : 502 (Average: 287.40 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 6 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 144273 (Deleted: 125657)
|
||
|
|
Binary : 2355 (Ratio: 1.63%)
|
||
|
|
Ternary : 2248 (Ratio: 1.56%)
|
||
|
|
Conflict : 144273 (Average Length: 1056.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 144273 (Average: 100.24 Max: 4236 Sum: 14462250)
|
||
|
|
Executed : 144155 (Average: 100.22 Max: 4236 Sum: 14458424 Ratio: 99.97%)
|
||
|
|
Bounded : 118 (Average: 32.42 Max: 37 Sum: 3826 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1924955 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 588MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 23.88s
|
||
|
|
Memory: 557MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.88s
|
||
|
|
|
||
|
|
Iteration 6
|
||
|
|
Queue: [(0,35,5,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 7
|
||
|
|
Time : 247.414s (Solving: 239.23s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 247.332s
|
||
|
|
|
||
|
|
Choices : 15463363 (Domain: 15463339)
|
||
|
|
Conflicts : 169703 (Analyzed: 169703)
|
||
|
|
Restarts : 602 (Average: 281.90 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 7 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 169703 (Deleted: 149447)
|
||
|
|
Binary : 2451 (Ratio: 1.44%)
|
||
|
|
Ternary : 2356 (Ratio: 1.39%)
|
||
|
|
Conflict : 169703 (Average Length: 1171.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 169703 (Average: 87.17 Max: 4236 Sum: 14793569)
|
||
|
|
Executed : 169581 (Average: 87.15 Max: 4236 Sum: 14789631 Ratio: 99.97%)
|
||
|
|
Bounded : 122 (Average: 32.28 Max: 37 Sum: 3938 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1924943 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 21.91s
|
||
|
|
Memory: 621MB (+64MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.91s
|
||
|
|
|
||
|
|
Iteration 7
|
||
|
|
Queue: [(0,35,6,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 8
|
||
|
|
Time : 273.582s (Solving: 265.36s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 273.508s
|
||
|
|
|
||
|
|
Choices : 16579343 (Domain: 16579319)
|
||
|
|
Conflicts : 197588 (Analyzed: 197588)
|
||
|
|
Restarts : 702 (Average: 281.46 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 8 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 197588 (Deleted: 176631)
|
||
|
|
Binary : 2519 (Ratio: 1.27%)
|
||
|
|
Ternary : 2426 (Ratio: 1.23%)
|
||
|
|
Conflict : 197588 (Average Length: 1240.6 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 197588 (Average: 79.79 Max: 4236 Sum: 15766532)
|
||
|
|
Executed : 197462 (Average: 79.77 Max: 4236 Sum: 15762446 Ratio: 99.97%)
|
||
|
|
Bounded : 126 (Average: 32.43 Max: 37 Sum: 4086 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1923227 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 26.18s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 26.18s
|
||
|
|
|
||
|
|
Iteration 8
|
||
|
|
Queue: [(0,35,7,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 9
|
||
|
|
Time : 295.457s (Solving: 287.16s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 295.392s
|
||
|
|
|
||
|
|
Choices : 17203488 (Domain: 17203464)
|
||
|
|
Conflicts : 222459 (Analyzed: 222459)
|
||
|
|
Restarts : 802 (Average: 277.38 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 9 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 222459 (Deleted: 200364)
|
||
|
|
Binary : 2631 (Ratio: 1.18%)
|
||
|
|
Ternary : 2536 (Ratio: 1.14%)
|
||
|
|
Conflict : 222459 (Average Length: 1278.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 222459 (Average: 73.11 Max: 4236 Sum: 16264223)
|
||
|
|
Executed : 222331 (Average: 73.09 Max: 4236 Sum: 16260135 Ratio: 99.97%)
|
||
|
|
Bounded : 128 (Average: 31.94 Max: 37 Sum: 4088 Ratio: 0.03%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1919040 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 21.89s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.89s
|
||
|
|
|
||
|
|
Iteration 9
|
||
|
|
Queue: [(0,35,8,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 10
|
||
|
|
Time : 315.583s (Solving: 307.24s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 315.528s
|
||
|
|
|
||
|
|
Choices : 17787177 (Domain: 17787153)
|
||
|
|
Conflicts : 246879 (Analyzed: 246879)
|
||
|
|
Restarts : 902 (Average: 273.70 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 10 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 246879 (Deleted: 221392)
|
||
|
|
Binary : 2765 (Ratio: 1.12%)
|
||
|
|
Ternary : 2643 (Ratio: 1.07%)
|
||
|
|
Conflict : 246879 (Average Length: 1290.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 246879 (Average: 67.74 Max: 4236 Sum: 16722395)
|
||
|
|
Executed : 246747 (Average: 67.72 Max: 4236 Sum: 16718231 Ratio: 99.98%)
|
||
|
|
Bounded : 132 (Average: 31.55 Max: 37 Sum: 4164 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1919040 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 20.14s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.14s
|
||
|
|
|
||
|
|
Iteration 10
|
||
|
|
Queue: [(0,35,9,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 11
|
||
|
|
Time : 337.287s (Solving: 328.87s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 337.244s
|
||
|
|
|
||
|
|
Choices : 18437770 (Domain: 18437746)
|
||
|
|
Conflicts : 272239 (Analyzed: 272239)
|
||
|
|
Restarts : 1002 (Average: 271.70 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 11 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 272239 (Deleted: 247627)
|
||
|
|
Binary : 2840 (Ratio: 1.04%)
|
||
|
|
Ternary : 2705 (Ratio: 0.99%)
|
||
|
|
Conflict : 272239 (Average Length: 1302.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 272239 (Average: 63.36 Max: 4236 Sum: 17248757)
|
||
|
|
Executed : 272106 (Average: 63.34 Max: 4236 Sum: 17244556 Ratio: 99.98%)
|
||
|
|
Bounded : 133 (Average: 31.59 Max: 37 Sum: 4201 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1918882 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 21.71s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.72s
|
||
|
|
|
||
|
|
Iteration 11
|
||
|
|
Queue: [(0,35,10,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 12
|
||
|
|
Time : 361.588s (Solving: 353.13s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 361.556s
|
||
|
|
|
||
|
|
Choices : 19105128 (Domain: 19105104)
|
||
|
|
Conflicts : 301753 (Analyzed: 301753)
|
||
|
|
Restarts : 1102 (Average: 273.82 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 12 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 301753 (Deleted: 274821)
|
||
|
|
Binary : 2955 (Ratio: 0.98%)
|
||
|
|
Ternary : 2788 (Ratio: 0.92%)
|
||
|
|
Conflict : 301753 (Average Length: 1304.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 301753 (Average: 58.96 Max: 4236 Sum: 17792302)
|
||
|
|
Executed : 301614 (Average: 58.95 Max: 4236 Sum: 17787915 Ratio: 99.98%)
|
||
|
|
Bounded : 139 (Average: 31.56 Max: 37 Sum: 4387 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1918724 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 24.31s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.32s
|
||
|
|
|
||
|
|
Iteration 12
|
||
|
|
Queue: [(0,35,11,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 13
|
||
|
|
Time : 385.133s (Solving: 376.61s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 385.112s
|
||
|
|
|
||
|
|
Choices : 19941666 (Domain: 19941642)
|
||
|
|
Conflicts : 328035 (Analyzed: 328035)
|
||
|
|
Restarts : 1202 (Average: 272.91 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 13 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 328035 (Deleted: 300181)
|
||
|
|
Binary : 3028 (Ratio: 0.92%)
|
||
|
|
Ternary : 2892 (Ratio: 0.88%)
|
||
|
|
Conflict : 328035 (Average Length: 1291.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 328035 (Average: 56.41 Max: 4236 Sum: 18504961)
|
||
|
|
Executed : 327893 (Average: 56.40 Max: 4236 Sum: 18500571 Ratio: 99.98%)
|
||
|
|
Bounded : 142 (Average: 30.92 Max: 37 Sum: 4390 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1915646 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 23.56s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.56s
|
||
|
|
|
||
|
|
Iteration 13
|
||
|
|
Queue: [(0,35,12,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 14
|
||
|
|
Time : 410.612s (Solving: 402.04s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 410.600s
|
||
|
|
|
||
|
|
Choices : 20857283 (Domain: 20857259)
|
||
|
|
Conflicts : 354236 (Analyzed: 354236)
|
||
|
|
Restarts : 1302 (Average: 272.07 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 14 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 354236 (Deleted: 325452)
|
||
|
|
Binary : 3104 (Ratio: 0.88%)
|
||
|
|
Ternary : 2984 (Ratio: 0.84%)
|
||
|
|
Conflict : 354236 (Average Length: 1288.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 354236 (Average: 54.47 Max: 4236 Sum: 19296688)
|
||
|
|
Executed : 354091 (Average: 54.46 Max: 4236 Sum: 19292187 Ratio: 99.98%)
|
||
|
|
Bounded : 145 (Average: 31.04 Max: 37 Sum: 4501 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1915646 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 25.49s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 25.49s
|
||
|
|
|
||
|
|
Iteration 14
|
||
|
|
Queue: [(0,35,13,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 15
|
||
|
|
Time : 439.750s (Solving: 431.13s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 439.748s
|
||
|
|
|
||
|
|
Choices : 21993118 (Domain: 21993094)
|
||
|
|
Conflicts : 380240 (Analyzed: 380240)
|
||
|
|
Restarts : 1402 (Average: 271.21 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 15 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 380240 (Deleted: 350641)
|
||
|
|
Binary : 3196 (Ratio: 0.84%)
|
||
|
|
Ternary : 3060 (Ratio: 0.80%)
|
||
|
|
Conflict : 380240 (Average Length: 1280.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 380240 (Average: 53.39 Max: 4236 Sum: 20299583)
|
||
|
|
Executed : 380094 (Average: 53.37 Max: 4236 Sum: 20295045 Ratio: 99.98%)
|
||
|
|
Bounded : 146 (Average: 31.08 Max: 37 Sum: 4538 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914737 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 29.15s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 29.15s
|
||
|
|
|
||
|
|
Iteration 15
|
||
|
|
Queue: [(0,35,14,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 16
|
||
|
|
Time : 463.404s (Solving: 454.74s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 463.412s
|
||
|
|
|
||
|
|
Choices : 22701010 (Domain: 22700986)
|
||
|
|
Conflicts : 405744 (Analyzed: 405744)
|
||
|
|
Restarts : 1502 (Average: 270.14 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 16 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 405744 (Deleted: 375967)
|
||
|
|
Binary : 3234 (Ratio: 0.80%)
|
||
|
|
Ternary : 3112 (Ratio: 0.77%)
|
||
|
|
Conflict : 405744 (Average Length: 1293.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 405744 (Average: 51.46 Max: 4236 Sum: 20878849)
|
||
|
|
Executed : 405598 (Average: 51.45 Max: 4236 Sum: 20874311 Ratio: 99.98%)
|
||
|
|
Bounded : 146 (Average: 31.08 Max: 37 Sum: 4538 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914726 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 23.67s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.67s
|
||
|
|
|
||
|
|
Iteration 16
|
||
|
|
Queue: [(0,35,15,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 17
|
||
|
|
Time : 486.608s (Solving: 477.87s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 486.628s
|
||
|
|
|
||
|
|
Choices : 23383420 (Domain: 23383396)
|
||
|
|
Conflicts : 433319 (Analyzed: 433319)
|
||
|
|
Restarts : 1602 (Average: 270.49 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 17 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 433319 (Deleted: 403428)
|
||
|
|
Binary : 3308 (Ratio: 0.76%)
|
||
|
|
Ternary : 3199 (Ratio: 0.74%)
|
||
|
|
Conflict : 433319 (Average Length: 1295.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 433319 (Average: 49.45 Max: 4236 Sum: 21429478)
|
||
|
|
Executed : 433169 (Average: 49.44 Max: 4236 Sum: 21424900 Ratio: 99.98%)
|
||
|
|
Bounded : 150 (Average: 30.52 Max: 37 Sum: 4578 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914726 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 23.22s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.22s
|
||
|
|
|
||
|
|
Iteration 17
|
||
|
|
Queue: [(0,35,16,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 18
|
||
|
|
Time : 508.668s (Solving: 499.87s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 508.700s
|
||
|
|
|
||
|
|
Choices : 24047492 (Domain: 24047468)
|
||
|
|
Conflicts : 458956 (Analyzed: 458956)
|
||
|
|
Restarts : 1702 (Average: 269.66 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 18 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 458956 (Deleted: 427121)
|
||
|
|
Binary : 3405 (Ratio: 0.74%)
|
||
|
|
Ternary : 3283 (Ratio: 0.72%)
|
||
|
|
Conflict : 458956 (Average Length: 1302.9 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 458956 (Average: 47.86 Max: 4236 Sum: 21965539)
|
||
|
|
Executed : 458806 (Average: 47.85 Max: 4236 Sum: 21960961 Ratio: 99.98%)
|
||
|
|
Bounded : 150 (Average: 30.52 Max: 37 Sum: 4578 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.07s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.07s
|
||
|
|
|
||
|
|
Iteration 18
|
||
|
|
Queue: [(0,35,17,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 19
|
||
|
|
Time : 533.888s (Solving: 525.03s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 533.932s
|
||
|
|
|
||
|
|
Choices : 24999411 (Domain: 24999387)
|
||
|
|
Conflicts : 486351 (Analyzed: 486351)
|
||
|
|
Restarts : 1802 (Average: 269.90 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 19 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 486351 (Deleted: 451484)
|
||
|
|
Binary : 3504 (Ratio: 0.72%)
|
||
|
|
Ternary : 3414 (Ratio: 0.70%)
|
||
|
|
Conflict : 486351 (Average Length: 1299.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 486351 (Average: 46.84 Max: 4236 Sum: 22778975)
|
||
|
|
Executed : 486200 (Average: 46.83 Max: 4236 Sum: 22774396 Ratio: 99.98%)
|
||
|
|
Bounded : 151 (Average: 30.32 Max: 37 Sum: 4579 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 25.23s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 25.24s
|
||
|
|
|
||
|
|
Iteration 19
|
||
|
|
Queue: [(0,35,18,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 20
|
||
|
|
Time : 557.377s (Solving: 548.45s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 557.428s
|
||
|
|
|
||
|
|
Choices : 25614063 (Domain: 25614039)
|
||
|
|
Conflicts : 513723 (Analyzed: 513723)
|
||
|
|
Restarts : 1902 (Average: 270.10 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 20 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 513723 (Deleted: 478126)
|
||
|
|
Binary : 3579 (Ratio: 0.70%)
|
||
|
|
Ternary : 3481 (Ratio: 0.68%)
|
||
|
|
Conflict : 513723 (Average Length: 1312.0 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 513723 (Average: 45.28 Max: 4236 Sum: 23259209)
|
||
|
|
Executed : 513572 (Average: 45.27 Max: 4236 Sum: 23254630 Ratio: 99.98%)
|
||
|
|
Bounded : 151 (Average: 30.32 Max: 37 Sum: 4579 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 23.50s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.50s
|
||
|
|
|
||
|
|
Iteration 20
|
||
|
|
Queue: [(0,35,19,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 21
|
||
|
|
Time : 580.249s (Solving: 571.25s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 580.312s
|
||
|
|
|
||
|
|
Choices : 26243658 (Domain: 26243634)
|
||
|
|
Conflicts : 540323 (Analyzed: 540323)
|
||
|
|
Restarts : 2002 (Average: 269.89 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 21 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 540323 (Deleted: 504816)
|
||
|
|
Binary : 3634 (Ratio: 0.67%)
|
||
|
|
Ternary : 3537 (Ratio: 0.65%)
|
||
|
|
Conflict : 540323 (Average Length: 1320.8 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 540323 (Average: 43.94 Max: 4236 Sum: 23743359)
|
||
|
|
Executed : 540169 (Average: 43.93 Max: 4236 Sum: 23738777 Ratio: 99.98%)
|
||
|
|
Bounded : 154 (Average: 29.75 Max: 37 Sum: 4582 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.88s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.88s
|
||
|
|
|
||
|
|
Iteration 21
|
||
|
|
Queue: [(0,35,20,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 22
|
||
|
|
Time : 603.063s (Solving: 594.01s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 603.136s
|
||
|
|
|
||
|
|
Choices : 26930145 (Domain: 26930121)
|
||
|
|
Conflicts : 564784 (Analyzed: 564784)
|
||
|
|
Restarts : 2102 (Average: 268.69 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 22 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 564784 (Deleted: 527985)
|
||
|
|
Binary : 3688 (Ratio: 0.65%)
|
||
|
|
Ternary : 3581 (Ratio: 0.63%)
|
||
|
|
Conflict : 564784 (Average Length: 1329.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 564784 (Average: 43.01 Max: 4236 Sum: 24291955)
|
||
|
|
Executed : 564628 (Average: 43.00 Max: 4236 Sum: 24287335 Ratio: 99.98%)
|
||
|
|
Bounded : 156 (Average: 29.62 Max: 37 Sum: 4620 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914664 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.83s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.83s
|
||
|
|
|
||
|
|
Iteration 22
|
||
|
|
Queue: [(0,35,21,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 23
|
||
|
|
Time : 623.418s (Solving: 614.30s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 623.500s
|
||
|
|
|
||
|
|
Choices : 27541313 (Domain: 27541289)
|
||
|
|
Conflicts : 587825 (Analyzed: 587825)
|
||
|
|
Restarts : 2202 (Average: 266.95 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 23 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 587825 (Deleted: 551879)
|
||
|
|
Binary : 3745 (Ratio: 0.64%)
|
||
|
|
Ternary : 3648 (Ratio: 0.62%)
|
||
|
|
Conflict : 587825 (Average Length: 1331.3 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 587825 (Average: 42.12 Max: 4236 Sum: 24760832)
|
||
|
|
Executed : 587669 (Average: 42.11 Max: 4236 Sum: 24756212 Ratio: 99.98%)
|
||
|
|
Bounded : 156 (Average: 29.62 Max: 37 Sum: 4620 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914652 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 20.37s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 20.37s
|
||
|
|
|
||
|
|
Iteration 23
|
||
|
|
Queue: [(0,35,22,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 24
|
||
|
|
Time : 647.559s (Solving: 638.39s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 647.648s
|
||
|
|
|
||
|
|
Choices : 28240574 (Domain: 28240550)
|
||
|
|
Conflicts : 616674 (Analyzed: 616674)
|
||
|
|
Restarts : 2302 (Average: 267.89 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 24 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 616674 (Deleted: 579373)
|
||
|
|
Binary : 3899 (Ratio: 0.63%)
|
||
|
|
Ternary : 3786 (Ratio: 0.61%)
|
||
|
|
Conflict : 616674 (Average Length: 1344.2 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 616674 (Average: 41.03 Max: 4236 Sum: 25300609)
|
||
|
|
Executed : 616517 (Average: 41.02 Max: 4236 Sum: 25295952 Ratio: 99.98%)
|
||
|
|
Bounded : 157 (Average: 29.66 Max: 37 Sum: 4657 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914652 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 24.15s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.15s
|
||
|
|
|
||
|
|
Iteration 24
|
||
|
|
Queue: [(0,35,23,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 25
|
||
|
|
Time : 670.268s (Solving: 661.05s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 670.368s
|
||
|
|
|
||
|
|
Choices : 28833349 (Domain: 28833325)
|
||
|
|
Conflicts : 645067 (Analyzed: 645067)
|
||
|
|
Restarts : 2402 (Average: 268.55 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 25 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 645067 (Deleted: 606247)
|
||
|
|
Binary : 3946 (Ratio: 0.61%)
|
||
|
|
Ternary : 3861 (Ratio: 0.60%)
|
||
|
|
Conflict : 645067 (Average Length: 1357.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 645067 (Average: 39.92 Max: 4236 Sum: 25751338)
|
||
|
|
Executed : 644910 (Average: 39.91 Max: 4236 Sum: 25746681 Ratio: 99.98%)
|
||
|
|
Bounded : 157 (Average: 29.66 Max: 37 Sum: 4657 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914590 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.72s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.72s
|
||
|
|
|
||
|
|
Iteration 25
|
||
|
|
Queue: [(0,35,24,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 26
|
||
|
|
Time : 693.620s (Solving: 684.36s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 693.732s
|
||
|
|
|
||
|
|
Choices : 29454752 (Domain: 29454728)
|
||
|
|
Conflicts : 673092 (Analyzed: 673092)
|
||
|
|
Restarts : 2502 (Average: 269.02 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 26 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 673092 (Deleted: 634682)
|
||
|
|
Binary : 4087 (Ratio: 0.61%)
|
||
|
|
Ternary : 3942 (Ratio: 0.59%)
|
||
|
|
Conflict : 673092 (Average Length: 1366.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 673092 (Average: 38.98 Max: 4236 Sum: 26234674)
|
||
|
|
Executed : 672934 (Average: 38.97 Max: 4236 Sum: 26230016 Ratio: 99.98%)
|
||
|
|
Bounded : 158 (Average: 29.48 Max: 37 Sum: 4658 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914590 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 23.37s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 23.37s
|
||
|
|
|
||
|
|
Iteration 26
|
||
|
|
Queue: [(0,35,25,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 27
|
||
|
|
Time : 713.201s (Solving: 703.88s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 713.320s
|
||
|
|
|
||
|
|
Choices : 29961334 (Domain: 29961310)
|
||
|
|
Conflicts : 695547 (Analyzed: 695547)
|
||
|
|
Restarts : 2602 (Average: 267.31 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 27 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 695547 (Deleted: 656540)
|
||
|
|
Binary : 4117 (Ratio: 0.59%)
|
||
|
|
Ternary : 3969 (Ratio: 0.57%)
|
||
|
|
Conflict : 695547 (Average Length: 1368.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 695547 (Average: 38.26 Max: 4236 Sum: 26609476)
|
||
|
|
Executed : 695385 (Average: 38.25 Max: 4236 Sum: 26604670 Ratio: 99.98%)
|
||
|
|
Bounded : 162 (Average: 29.67 Max: 37 Sum: 4806 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1914590 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 19.59s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 19.59s
|
||
|
|
|
||
|
|
Iteration 27
|
||
|
|
Queue: [(0,35,26,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 28
|
||
|
|
Time : 734.751s (Solving: 725.38s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 734.876s
|
||
|
|
|
||
|
|
Choices : 30574275 (Domain: 30574251)
|
||
|
|
Conflicts : 720438 (Analyzed: 720438)
|
||
|
|
Restarts : 2702 (Average: 266.63 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 28 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 720438 (Deleted: 680956)
|
||
|
|
Binary : 4197 (Ratio: 0.58%)
|
||
|
|
Ternary : 4046 (Ratio: 0.56%)
|
||
|
|
Conflict : 720438 (Average Length: 1372.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 720438 (Average: 37.58 Max: 4236 Sum: 27077141)
|
||
|
|
Executed : 720276 (Average: 37.58 Max: 4236 Sum: 27072335 Ratio: 99.98%)
|
||
|
|
Bounded : 162 (Average: 29.67 Max: 37 Sum: 4806 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912870 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 21.56s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 21.56s
|
||
|
|
|
||
|
|
Iteration 28
|
||
|
|
Queue: [(0,35,27,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 29
|
||
|
|
Time : 759.120s (Solving: 749.68s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 759.256s
|
||
|
|
|
||
|
|
Choices : 31136210 (Domain: 31136186)
|
||
|
|
Conflicts : 747330 (Analyzed: 747330)
|
||
|
|
Restarts : 2802 (Average: 266.71 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 29 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 747330 (Deleted: 705050)
|
||
|
|
Binary : 4253 (Ratio: 0.57%)
|
||
|
|
Ternary : 4084 (Ratio: 0.55%)
|
||
|
|
Conflict : 747330 (Average Length: 1377.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 747330 (Average: 36.81 Max: 4236 Sum: 27505506)
|
||
|
|
Executed : 747167 (Average: 36.80 Max: 4236 Sum: 27500663 Ratio: 99.98%)
|
||
|
|
Bounded : 163 (Average: 29.71 Max: 37 Sum: 4843 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912870 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 24.38s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.38s
|
||
|
|
|
||
|
|
Iteration 29
|
||
|
|
Queue: [(0,35,28,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 30
|
||
|
|
Time : 782.043s (Solving: 772.52s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 782.188s
|
||
|
|
|
||
|
|
Choices : 31668474 (Domain: 31668450)
|
||
|
|
Conflicts : 774284 (Analyzed: 774284)
|
||
|
|
Restarts : 2902 (Average: 266.81 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 30 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 774284 (Deleted: 731410)
|
||
|
|
Binary : 4372 (Ratio: 0.56%)
|
||
|
|
Ternary : 4152 (Ratio: 0.54%)
|
||
|
|
Conflict : 774284 (Average Length: 1400.4 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 774284 (Average: 36.02 Max: 4236 Sum: 27886633)
|
||
|
|
Executed : 774120 (Average: 36.01 Max: 4236 Sum: 27881753 Ratio: 99.98%)
|
||
|
|
Bounded : 164 (Average: 29.76 Max: 37 Sum: 4880 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912858 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 22.93s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 22.93s
|
||
|
|
|
||
|
|
Iteration 30
|
||
|
|
Queue: [(0,35,29,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 31
|
||
|
|
Time : 806.414s (Solving: 796.81s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 806.568s
|
||
|
|
|
||
|
|
Choices : 32212167 (Domain: 32212143)
|
||
|
|
Conflicts : 803689 (Analyzed: 803689)
|
||
|
|
Restarts : 3002 (Average: 267.72 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 31 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 803689 (Deleted: 759611)
|
||
|
|
Binary : 4460 (Ratio: 0.55%)
|
||
|
|
Ternary : 4225 (Ratio: 0.53%)
|
||
|
|
Conflict : 803689 (Average Length: 1407.5 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 803689 (Average: 35.19 Max: 4236 Sum: 28282702)
|
||
|
|
Executed : 803522 (Average: 35.18 Max: 4236 Sum: 28277711 Ratio: 99.98%)
|
||
|
|
Bounded : 167 (Average: 29.89 Max: 37 Sum: 4991 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912760 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 24.38s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 24.38s
|
||
|
|
|
||
|
|
Iteration 31
|
||
|
|
Queue: [(0,35,30,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 32
|
||
|
|
Time : 834.197s (Solving: 824.53s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 834.360s
|
||
|
|
|
||
|
|
Choices : 32869485 (Domain: 32869461)
|
||
|
|
Conflicts : 831984 (Analyzed: 831984)
|
||
|
|
Restarts : 3102 (Average: 268.21 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 32 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 831984 (Deleted: 788502)
|
||
|
|
Binary : 4614 (Ratio: 0.55%)
|
||
|
|
Ternary : 4330 (Ratio: 0.52%)
|
||
|
|
Conflict : 831984 (Average Length: 1420.1 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 831984 (Average: 34.60 Max: 4236 Sum: 28785801)
|
||
|
|
Executed : 831815 (Average: 34.59 Max: 4236 Sum: 28780808 Ratio: 99.98%)
|
||
|
|
Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 27.80s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 27.80s
|
||
|
|
|
||
|
|
Iteration 32
|
||
|
|
Queue: [(0,35,31,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 33
|
||
|
|
Time : 859.343s (Solving: 849.63s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 859.516s
|
||
|
|
|
||
|
|
Choices : 33454989 (Domain: 33454965)
|
||
|
|
Conflicts : 860485 (Analyzed: 860485)
|
||
|
|
Restarts : 3202 (Average: 268.73 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 33 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 860485 (Deleted: 815642)
|
||
|
|
Binary : 4731 (Ratio: 0.55%)
|
||
|
|
Ternary : 4385 (Ratio: 0.51%)
|
||
|
|
Conflict : 860485 (Average Length: 1428.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 860485 (Average: 33.96 Max: 4236 Sum: 29221017)
|
||
|
|
Executed : 860316 (Average: 33.95 Max: 4236 Sum: 29216024 Ratio: 99.98%)
|
||
|
|
Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 25.16s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 25.16s
|
||
|
|
|
||
|
|
Iteration 33
|
||
|
|
Queue: [(0,35,32,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
[start: stats after solve call]
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 34
|
||
|
|
Time : 886.061s (Solving: 876.29s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 886.244s
|
||
|
|
|
||
|
|
Choices : 34011774 (Domain: 34011750)
|
||
|
|
Conflicts : 890019 (Analyzed: 890019)
|
||
|
|
Restarts : 3302 (Average: 269.54 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 34 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 890019 (Deleted: 843327)
|
||
|
|
Binary : 4809 (Ratio: 0.54%)
|
||
|
|
Ternary : 4427 (Ratio: 0.50%)
|
||
|
|
Conflict : 890019 (Average Length: 1430.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 890019 (Average: 33.30 Max: 4236 Sum: 29634994)
|
||
|
|
Executed : 889850 (Average: 33.29 Max: 4236 Sum: 29630001 Ratio: 99.98%)
|
||
|
|
Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
[endof: stats after solve call]
|
||
|
|
Solving Time: 26.73s
|
||
|
|
Memory: 621MB (+0MB)
|
||
|
|
UNKNOWN
|
||
|
|
Iteration Time: 26.73s
|
||
|
|
|
||
|
|
Iteration 34
|
||
|
|
Queue: [(0,35,33,True)]
|
||
|
|
Grounded Until: 35
|
||
|
|
Solving...
|
||
|
|
*** Info : (planner): INTERRUPTED by signal!
|
||
|
|
UNKNOWN
|
||
|
|
|
||
|
|
INTERRUPTED : 1
|
||
|
|
|
||
|
|
Models : 0+
|
||
|
|
Calls : 35
|
||
|
|
Time : 912.171s (Solving: 902.35s 1st Model: 0.19s Unsat: 0.00s)
|
||
|
|
CPU Time : 912.348s
|
||
|
|
|
||
|
|
Choices : 34615184 (Domain: 34615160)
|
||
|
|
Conflicts : 919629 (Analyzed: 919629)
|
||
|
|
Restarts : 3402 (Average: 270.32 Last: 542)
|
||
|
|
Model-Level : 2483.0
|
||
|
|
Problems : 35 (Average Length: 37.00 Splits: 0)
|
||
|
|
Lemmas : 919629 (Deleted: 872085)
|
||
|
|
Binary : 4880 (Ratio: 0.53%)
|
||
|
|
Ternary : 4472 (Ratio: 0.49%)
|
||
|
|
Conflict : 919629 (Average Length: 1433.7 Ratio: 100.00%)
|
||
|
|
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
|
||
|
|
Backjumps : 919629 (Average: 32.72 Max: 4236 Sum: 30092001)
|
||
|
|
Executed : 919460 (Average: 32.72 Max: 4236 Sum: 30087008 Ratio: 99.98%)
|
||
|
|
Bounded : 169 (Average: 29.54 Max: 37 Sum: 4993 Ratio: 0.02%)
|
||
|
|
|
||
|
|
Rules : 482958 (Original: 482854)
|
||
|
|
Atoms : 12443
|
||
|
|
Bodies : 318208 (Original: 318104)
|
||
|
|
Count : 1137 (Original: 1148)
|
||
|
|
Equivalences : 162277 (Atom=Atom: 48 Body=Body: 0 Other: 162229)
|
||
|
|
Tight : Yes
|
||
|
|
Variables : 216990 (Eliminated: 0 Frozen: 181320)
|
||
|
|
Constraints : 1912041 (Binary: 97.8% Ternary: 1.0% Other: 1.2%)
|
||
|
|
|
||
|
|
Memory Peak : 685MB
|
||
|
|
Max. Length : 35 steps
|
||
|
|
Models : 1
|
||
|
|
|
||
|
|
|