PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pk1.opb
MD5SUM	9c5126d785c8d5465220e290c5fc25a6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5120
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	2421502
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.04
Number of variables	675
Total number of constraints	100
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	45
Minimum length of a constraint	1
Maximum length of a constraint	95
Trace number 18508

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 15:16:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17900 boxname=wulflinc24 idbench=1377 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9c5126d785c8d5465220e290c5fc25a6  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-pk1.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 17900
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        801368 kB
Buffers:         26392 kB
Cached:         183000 kB
SwapCached:        524 kB
Active:          68332 kB
Inactive:       143076 kB
HighTotal:      131008 kB
HighFree:         8316 kB
LowTotal:       903652 kB
LowFree:        793052 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16296 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:36:32 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 17900 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############
c   -- Clauses(.)/Splits(s): (none)
c ---[  58]---> BDD-cost:26954
c ---[  56]---> BDD-cost:31488
c ---[  54]---> BDD-cost:23102
c ---[  52]---> BDD-cost:32842
c ---[  50]---> BDD-cost:29911
c ---[  48]---> BDD-cost:34674
c ---[  46]---> BDD-cost:28073
c ---[  45]---> BDD-cost:   58
c ---[  44]---> BDD-cost:   58
c ---[  43]---> BDD-cost:   58
c ---[  42]---> BDD-cost:   58
c ---[  40]---> BDD-cost:31287
c ---[  39]---> BDD-cost:   58
c ---[  38]---> BDD-cost:   58
c ---[  37]---> BDD-cost:   58
c ---[  36]---> BDD-cost:   58
c ---[  35]---> BDD-cost:   58
c ---[  34]---> BDD-cost:   58
c ---[  33]---> BDD-cost:   58
c ---[  32]---> BDD-cost:   58
c ---[  31]---> BDD-cost:   58
c ---[  30]---> BDD-cost:   58
c ---[  28]---> BDD-cost:26642
c ---[  27]---> BDD-cost:   58
c ---[  26]---> BDD-cost:   58
c ---[  25]---> BDD-cost:   58
c ---[  24]---> BDD-cost:   58
c ---[  23]---> BDD-cost:   58
c ---[  22]---> BDD-cost:   58
c ---[  21]---> BDD-cost:   58
c ---[  20]---> BDD-cost:   58
c ---[  19]---> BDD-cost:   58
c ---[  18]---> BDD-cost:   58
c ---[  16]---> BDD-cost:35718
c ---[  15]---> BDD-cost:   58
c ---[  14]---> BDD-cost:   58
c ---[  13]---> BDD-cost:   58
c ---[  12]---> BDD-cost:   58
c ---[  11]---> BDD-cost:   58
c ---[  10]---> BDD-cost:   58
c ---[   8]---> BDD-cost:31281
c ---[   6]---> BDD-cost:32022
c ---[   4]---> BDD-cost:26848
c ---[   2]---> BDD-cost:31458
c ---[   0]---> BDD-cost:30756
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1317134  3863725 |  439044       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1048572[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1317135  3863744 |  439045       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 786428[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   71     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1317241  3864007 |  439080       0        0     nan |  0.000 % |
c |       100 | 1317241  3864007 |  482988     100    16643   166.4 |  0.010 % |
c |       250 | 1317241  3864007 |  531286     250    21002    84.0 |  0.010 % |
c |       475 | 1317231  3863987 |  584415     469    25509    54.4 |  0.011 % |
c ==============================================================================
c [1mFound solution: 747244[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   87     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       585 | 1317395  3864376 |  439131     579    27347    47.2 |  0.011 % |
c ==============================================================================
c [1mFound solution: 335292[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   92     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       602 | 1317231  3863842 |  439077     584    27523    47.1 |  0.011 % |
c ==============================================================================
c [1mFound solution: 270060[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       613 | 1317378  3864191 |  439126     594    27709    46.6 |  0.011 % |
c ==============================================================================
c [1mFound solution: 269302[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   91     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       613 | 1317539  3864573 |  439179     594    27709    46.6 |  0.011 % |
c ==============================================================================
c [1mFound solution: 268908[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   69     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       613 | 1317665  3864869 |  439221     594    27709    46.6 |  0.011 % |
c ==============================================================================
c [1mFound solution: 268758[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   77     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       615 | 1317801  3865190 |  439267     595    27711    46.6 |  0.011 % |
c ==============================================================================
c [1mFound solution: 240294[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   89     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       619 | 1317456  3864261 |  439152     565    27590    48.8 |  0.011 % |
c ==============================================================================
c [1mFound solution: 240278[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   89     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       619 | 1317633  3864677 |  439211     565    27590    48.8 |  0.011 % |
c ==============================================================================
c [1mFound solution: 141548[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   98     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       624 | 1317824  3865125 |  439274     570    27623    48.5 |  0.011 % |
c ==============================================================================
c [1mFound solution: 131820[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   56     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       627 | 1317929  3865369 |  439309     573    27659    48.3 |  0.011 % |
c ==============================================================================
c [1mFound solution: 98994[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  194     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       627 | 1317849  3865060 |  439283     548    27529    50.2 |  0.011 % |
c ==============================================================================
c [1mFound solution: 98988[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  149     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       627 | 1318129  3865721 |  439376     548    27529    50.2 |  0.011 % |
c ==============================================================================
c [1mFound solution: 98986[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  146     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       629 | 1318405  3866372 |  439468     550    27534    50.1 |  0.011 % |
c ==============================================================================
c [1mFound solution: 98964[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  160     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       630 | 1318717  3867107 |  439572     551    27571    50.0 |  0.011 % |
c ==============================================================================
c [1mFound solution: 98850[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  169     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       631 | 1319055  3867902 |  439685     552    27576    50.0 |  0.011 % |
c |       731 | 1319055  3867902 |  483653     652    30426    46.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98578[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  160     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       736 | 1319375  3868656 |  439791     657    30627    46.6 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98514[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  129     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       742 | 1319620  3869235 |  439873     663    30731    46.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98510[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  170     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       742 | 1319952  3870018 |  439984     663    30731    46.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98506[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  150     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       742 | 1320245  3870709 |  440081     663    30731    46.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98498[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  150     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       743 | 1320538  3871400 |  440179     664    30735    46.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  126     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       743 | 1320775  3871960 |  440258     664    30735    46.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98450[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  125     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       743 | 1321014  3872524 |  440338     664    30735    46.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98378[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  137     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       743 | 1321283  3873159 |  440427     664    30735    46.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98370[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  137     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       743 | 1321552  3873794 |  440517     664    30735    46.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 98368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  137     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       744 | 1321821  3874428 |  440607     665    30747    46.2 |  0.139 % |
c ==============================================================================
c [1mFound solution: 95444[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       745 | 1321977  3874796 |  440659     666    30750    46.2 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94388[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       746 | 1322095  3875074 |  440698     667    30753    46.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94386[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       746 | 1322241  3875417 |  440747     667    30753    46.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       747 | 1322353  3875681 |  440784     668    30757    46.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94356[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   57     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       748 | 1322452  3875914 |  440817     669    30761    46.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       748 | 1322565  3876180 |  440855     669    30761    46.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       748 | 1322677  3876443 |  440892     669    30761    46.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   49     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       748 | 1322760  3876639 |  440920     669    30761    46.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94258[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       751 | 1322853  3876857 |  440951     672    30811    45.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       751 | 1322944  3877071 |  440981     672    30811    45.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       751 | 1323035  3877285 |  441011     672    30811    45.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   74     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       751 | 1323167  3877593 |  441055     672    30811    45.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 94208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       751 | 1323192  3877654 |  441064     672    30811    45.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 93360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       791 | 1323243  3877775 |  441081     712    31970    44.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 93348[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       836 | 1323358  3878046 |  441119     757    33220    43.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 93332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       851 | 1323407  3878163 |  441135     772    33440    43.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 93328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       884 | 1323456  3878280 |  441152     805    33955    42.2 |  0.139 % |
c ==============================================================================
c [1mFound solution: 93312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       894 | 1323506  3878399 |  441168     815    34136    41.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 92848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       933 | 1323569  3878548 |  441189     854    35265    41.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 92834[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   58     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       978 | 1323674  3878795 |  441224     899    36456    40.6 |  0.139 % |
c ==============================================================================
c [1mFound solution: 92080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1021 | 1323739  3878951 |  441246     942    37598    39.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 91792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1043 | 1323800  3879096 |  441266     964    38063    39.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 91776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1075 | 1323862  3879243 |  441287     996    39017    39.2 |  0.139 % |
c ==============================================================================
c [1mFound solution: 91234[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   57     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1107 | 1323962  3879478 |  441320    1028    39980    38.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 90928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1134 | 1324036  3879653 |  441345    1055    40891    38.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 90756[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1152 | 1324150  3879920 |  441383    1073    41499    38.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 90720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   58     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1182 | 1324252  3880159 |  441417    1103    42057    38.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 90204[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   75     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1192 | 1324386  3880473 |  441462    1113    42246    38.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 89394[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   42     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1210 | 1324461  3880651 |  441487    1131    42587    37.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 88160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   39     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1237 | 1324528  3880809 |  441509    1158    42995    37.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 87986[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1275 | 1324595  3880969 |  441531    1196    43513    36.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 86112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   28     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1307 | 1324643  3881082 |  441547    1228    44126    35.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 86108[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1332 | 1324683  3881175 |  441561    1253    44851    35.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 86068[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   56     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1367 | 1324783  3881408 |  441594    1288    45694    35.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   69     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1377 | 1324906  3881696 |  441635    1298    46049    35.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83124[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1381 | 1324969  3881843 |  441656    1302    46137    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83122[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1382 | 1325032  3881990 |  441677    1303    46190    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1383 | 1325086  3882117 |  441695    1304    46192    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83100[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1384 | 1325194  3882369 |  441731    1305    46244    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83092[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1385 | 1325248  3882496 |  441749    1306    46249    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83090[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1385 | 1325311  3882643 |  441770    1306    46249    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83088[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1385 | 1325365  3882770 |  441788    1306    46249    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   74     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1385 | 1325499  3883082 |  441833    1306    46249    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83076[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   42     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1385 | 1325573  3883255 |  441857    1306    46249    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83074[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1385 | 1325670  3883481 |  441890    1306    46249    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 83072[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1385 | 1325724  3883608 |  441908    1306    46249    35.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 82612[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   42     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1394 | 1325799  3883783 |  441933    1315    46398    35.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 82484[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   42     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1410 | 1325875  3883960 |  441958    1331    46694    35.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 82482[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   42     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1427 | 1325950  3884135 |  441983    1348    47094    34.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 82100[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1435 | 1325990  3884229 |  441996    1356    47370    34.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 82098[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1457 | 1326030  3884323 |  442010    1378    47942    34.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81972[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1470 | 1326070  3884417 |  442023    1391    48276    34.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81970[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1479 | 1326110  3884511 |  442036    1400    48555    34.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1489 | 1326150  3884605 |  442050    1410    49023    34.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81940[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   59     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1499 | 1326255  3884849 |  442085    1420    49341    34.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81938[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   59     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1507 | 1326360  3885093 |  442120    1428    49579    34.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1512 | 1326400  3885187 |  442133    1433    49826    34.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81932[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   80     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1522 | 1326545  3885524 |  442181    1443    50011    34.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81924[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   59     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1539 | 1326650  3885768 |  442216    1460    50530    34.6 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81922[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1547 | 1326690  3885862 |  442230    1468    50784    34.6 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81920[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1548 | 1326701  3885889 |  442233    1469    50793    34.6 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81844[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1326759  3886030 |  442253    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81842[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1326797  3886122 |  442265    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1326835  3886214 |  442278    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81812[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1326891  3886351 |  442297    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81810[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1326947  3886488 |  442315    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1327003  3886625 |  442334    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81804[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   41     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1327069  3886785 |  442356    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81796[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1327125  3886922 |  442375    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81794[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1327181  3887059 |  442393    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1552 | 1327239  3887200 |  442413    1473    50855    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81460[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1555 | 1327283  3887307 |  442427    1476    50976    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1559 | 1327342  3887449 |  442447    1480    51102    34.5 |  0.139 % |
c ==============================================================================
c [1mFound solution: 81076[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1569 | 1327380  3887541 |  442460    1490    51244    34.4 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80948[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1578 | 1327426  3887652 |  442475    1499    51423    34.3 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80820[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1588 | 1327479  3887779 |  442493    1509    51530    34.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80692[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1594 | 1327546  3887939 |  442515    1515    51554    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80690[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1596 | 1327605  3888080 |  442535    1517    51562    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1327645  3888176 |  442548    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1327712  3888336 |  442570    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80658[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1327779  3888496 |  442593    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80656[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1327846  3888656 |  442615    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   47     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1327925  3888844 |  442641    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80644[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1327992  3889004 |  442664    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80642[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1328059  3889164 |  442686    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 80640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1597 | 1328120  3889309 |  442706    1518    51574    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 79924[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1609 | 1328160  3889405 |  442720    1530    51981    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 79922[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1611 | 1328201  3889503 |  442733    1532    52100    34.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 79792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1620 | 1328235  3889584 |  442745    1541    52221    33.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 79026[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1624 | 1328269  3889665 |  442756    1545    52353    33.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 78388[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1628 | 1328304  3889748 |  442768    1549    52422    33.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 78386[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1629 | 1328339  3889831 |  442779    1550    52469    33.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 77876[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1637 | 1328365  3889893 |  442788    1558    52696    33.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 61524[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   73     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1646 | 1326902  3886228 |  442300    1218    36730    30.2 |  0.139 % |
c ==============================================================================
c [1mFound solution: 58168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   63     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1659 | 1327021  3886510 |  442340    1231    36996    30.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 58008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   68     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1662 | 1327155  3886825 |  442385    1234    37080    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 57764[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   77     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1667 | 1327306  3887180 |  442435    1239    37130    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 53628[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  126     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1672 | 1327569  3887799 |  442523    1244    37301    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 53548[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1676 | 1327873  3888511 |  442624    1248    37435    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 52676[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  121     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1687 | 1328119  3889091 |  442706    1259    37714    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 25998[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  131     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1708 | 1326207  3884488 |  442069    1229    36943    30.1 |  0.139 % |
c ==============================================================================
c [1mFound solution: 25994[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  130     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1722 | 1326477  3885122 |  442159    1243    37278    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 25992[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  115     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1724 | 1326713  3885676 |  442237    1245    37285    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 25990[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  128     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1724 | 1326981  3886305 |  442327    1245    37285    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 25966[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   76     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1731 | 1327127  3886650 |  442375    1252    37450    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24962[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  162     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1742 | 1327456  3887426 |  442485    1263    37773    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24786[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  110     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1748 | 1327654  3887896 |  442551    1269    37897    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24758[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  108     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1754 | 1327846  3888352 |  442615    1275    37920    29.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24754[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   99     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1757 | 1328019  3888763 |  442673    1278    38000    29.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24752[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  105     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1758 | 1328203  3889200 |  442734    1279    38003    29.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24748[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  126     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1760 | 1328432  3889742 |  442810    1281    38052    29.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24730[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  120     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1774 | 1328654  3890267 |  442884    1295    38675    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24716[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  125     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1786 | 1328892  3890829 |  442964    1307    39008    29.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24710[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   74     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1789 | 1329014  3891122 |  443004    1310    39079    29.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24708[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  158     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1794 | 1329328  3891861 |  443109    1315    39305    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24662[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  116     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1802 | 1329544  3892373 |  443181    1323    39617    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24614[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  125     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1803 | 1329783  3892937 |  443261    1324    39674    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24602[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  104     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1806 | 1329976  3893394 |  443325    1327    39761    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24598[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  125     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1807 | 1330218  3893965 |  443406    1328    39836    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24586[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  104     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1807 | 1330411  3894422 |  443470    1328    39836    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24580[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  104     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1807 | 1330604  3894879 |  443534    1328    39836    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24578[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  104     Base: 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1808 | 1330797  3895336 |  443599    1329    39878    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1814 | 1330798  3895339 |  443599    1335    40036    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24518[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   62     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1816 | 1330900  3895584 |  443633    1337    40116    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24516[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   56     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1818 | 1330990  3895800 |  443663    1339    40148    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24262[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1821 | 1331042  3895927 |  443680    1342    40202    30.0 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24006[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1824 | 1331082  3896024 |  443694    1345    40215    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24004[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1824 | 1331122  3896123 |  443707    1345    40215    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24002[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1824 | 1331233  3896386 |  443744    1345    40215    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 24000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   34     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1824 | 1331287  3896516 |  443762    1345    40215    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 23942[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1824 | 1331353  3896674 |  443784    1345    40215    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 23940[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1824 | 1331419  3896832 |  443806    1345    40215    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 23938[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1825 | 1331485  3896990 |  443828    1346    40218    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 23936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   30     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1825 | 1331533  3897105 |  443844    1346    40218    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 23876[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1828 | 1331594  3897251 |  443864    1349    40325    29.9 |  0.139 % |
c ==============================================================================
c [1mFound solution: 23748[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1841 | 1331647  3897378 |  443882    1362    40542    29.8 |  0.139 % |
c ==============================================================================
c [1mFound solution: 23746[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1846 | 1331700  3897506 |  443900    1367    40619    29.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 22980[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1852 | 1331733  3897585 |  443911    1373    40746    29.7 |  0.139 % |
c ==============================================================================
c [1mFound solution: 22596[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1867 | 1331792  3897724 |  443930    1388    41039    29.6 |  0.139 % |
c ==============================================================================
c [1mFound solution: 15986[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   50     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1880 | 1329041  3891027 |  443013    1361    40437    29.7 |  0.139 % |
c |      1980 | 1329041  3891027 |  487314    1461    44466    30.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 15752[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1985 | 1329127  3891232 |  443042    1466    44630    30.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 15242[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   63     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1989 | 1329246  3891514 |  443082    1470    44711    30.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 14300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1995 | 1329360  3891788 |  443120    1476    44807    30.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 14268[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   49     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2003 | 1329445  3891992 |  443148    1484    45040    30.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 14218[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  116     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2008 | 1329684  3892554 |  443228    1489    45159    30.3 |  0.528 % |
c ==============================================================================
c [1mFound solution: 14102[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  110     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2025 | 1329912  3893090 |  443304    1506    45583    30.3 |  0.528 % |
c ==============================================================================
c [1mFound solution: 13842[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  130     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2046 | 1330193  3893748 |  443397    1527    46364    30.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 13202[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2065 | 1330250  3893886 |  443416    1546    47376    30.6 |  0.528 % |
c ==============================================================================
c [1mFound solution: 13186[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   99     Base: 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2070 | 1330452  3894362 |  443484    1551    47555    30.7 |  0.528 % |
c ==============================================================================
c [1mFound solution: 13184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   33     Base: 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2117 | 1330500  3894479 |  443500    1598    49266    30.8 |  0.528 % |
c ==============================================================================
c [1mFound solution: 12306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   70     Base: 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2145 | 1330620  3894766 |  443540    1626    50166    30.9 |  0.528 % |
c ==============================================================================
c [1mFound solution: 12290[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   83     Base: 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2159 | 1330764  3895109 |  443588    1640    50532    30.8 |  0.528 % |
c ==============================================================================
c [1mFound solution: 12288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2180 | 1330765  3895112 |  443588    1661    51272    30.9 |  0.528 % |
c |      2281 | 1330765  3895112 |  487946    1762    56490    32.1 |  0.529 % |
c |      2431 | 1330765  3895112 |  536741    1912    64782    33.9 |  0.529 % |
c ==============================================================================
c [1mFound solution: 12268[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2610 | 1330837  3895287 |  443612    2091    73223    35.0 |  0.529 % |
c ==============================================================================
c [1mFound solution: 12260[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   48     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2699 | 1330913  3895471 |  443637    2180    77684    35.6 |  0.529 % |
c |      2799 | 1330913  3895471 |  488000    2280    81431    35.7 |  0.530 % |
c |      2950 | 1330913  3895471 |  536800    2431    87469    36.0 |  0.530 % |
c ==============================================================================
c [1mFound solution: 11516[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   44     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3097 | 1330984  3895642 |  443661    2578    95087    36.9 |  0.530 % |
c |      3197 | 1330984  3895642 |  488027    2678    99930    37.3 |  0.530 % |
c ==============================================================================
c [1mFound solution: 11244[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3278 | 1331018  3895727 |  443672    2759   103948    37.7 |  0.530 % |
c ==============================================================================
c [1mFound solution: 11012[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3278 | 1331098  3895915 |  443699    2759   103948    37.7 |  0.530 % |
c ==============================================================================
c [1mFound solution: 11008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   22     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3278 | 1331134  3896000 |  443711    2759   103948    37.7 |  0.530 % |
c |      3378 | 1331134  3896000 |  488082    2859   107516    37.6 |  0.531 % |
c |      3528 | 1331134  3896000 |  536890    3009   113729    37.8 |  0.531 % |
c |      3753 | 1331134  3896000 |  590579    3234   122215    37.8 |  0.531 % |
c |      4090 | 1331134  3896000 |  649637    3571   136318    38.2 |  0.531 % |
c |      4596 | 1331134  3896000 |  714601    4077   158689    38.9 |  0.531 % |
c |      5357 | 1331134  3896000 |  786061    4838   191954    39.7 |  0.531 % |
c |      6496 | 1331134  3896000 |  864667    5977   242820    40.6 |  0.531 % |
c ==============================================================================
c [1mFound solution: 10628[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6905 | 1331190  3896132 |  443730    6386   261962    41.0 |  0.531 % |
c |      7005 | 1331190  3896132 |  488103    6486   266829    41.1 |  0.531 % |
c |      7155 | 1331190  3896132 |  536913    6636   272758    41.1 |  0.531 % |
c ==============================================================================
c [1mFound solution: 10372[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7283 | 1331244  3896259 |  443748    6764   279006    41.2 |  0.531 % |
c |      7383 | 1331244  3896259 |  488122    6864   282777    41.2 |  0.531 % |
c ==============================================================================
c [1mFound solution: 9612[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   48     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7397 | 1331330  3896461 |  443776    6878   283270    41.2 |  0.531 % |
c ==============================================================================
c [1mFound solution: 9604[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7403 | 1331358  3896527 |  443786    6884   283479    41.2 |  0.531 % |
c ==============================================================================
c [1mFound solution: 9580[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7442 | 1331420  3896674 |  443806    6923   284990    41.2 |  0.531 % |
c |      7542 | 1331420  3896674 |  488186    7023   290273    41.3 |  0.531 % |
c |      7692 | 1331420  3896674 |  537005    7173   296754    41.4 |  0.531 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit_7 -x1_bit_6 x1_bit_5 x1_bit_4 -x1_bit_3 x1_bit_2 x1_bit_1 -x1_bit0 x1_bit1 -x1_bit2 x1_bit3 -x1_bit4 -x1_bit5 x1_bit6 -x1_bit7 -x1_bit8 -x1_bit9 -x1_bit10 -x1_bit11 -x1_bit12 x2_bit0 -x3_bit0 -x4_bit0 x5_bit0 x6_bit0 x7_bit0 x8_bit0 -x9_bit0 x10_bit0 -x11_bit0 -x12_bit0 x13_bit0 -x14_bit0 x15_bit0 x16_bit0 -x17_bit0 x18_bit0 -x19_bit0 -x20_bit0 -x21_bit0 -x22_bit0 x23_bit0 x24_bit0 -x25_bit0 -x26_bit0 -x27_bit0 x28_bit0 x29_bit0 -x30_bit0 -x31_bit0 -x32_bit0 -x33_bit0 x34_bit0 x35_bit0 x36_bit0 -x37_bit0 -x38_bit0 -x39_bit0 -x40_bit0 -x41_bit0 -x42_bit0 x43_bit0 x44_bit0 x45_bit0 -x46_bit0 -x47_bit0 x48_bit0 -x49_bit0 x50_bit0 x51_bit0 x52_bit0 -x53_bit0 -x54_bit0 -x55_bit0 x56_bit0 -x57_bit_7 x57_bit_6 x57_bit_5 -x57_bit_4 -x57_bit_3 x57_bit_2 x57_bit_1 -x57_bit0 -x57_bit1 -x57_bit2 -x57_bit3 -x57_bit4 -x57_bit5 x57_bit6 -x57_bit7 -x57_bit8 -x57_bit9 -x57_bit10 -x57_bit11 -x57_bit12 -x58_bit_7 x58_bit_6 x58_bit_5 -x58_bit_4 -x58_bit_3 x58_bit_2 x58_bit_1 -x58_bit0 -x58_bit1 -x58_bit2 -x58_bit3 x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x75_bit_7 x75_bit_6 -x75_bit_5 x75_bit_4 -x75_bit_3 x75_bit_2 x75_bit_1 -x75_bit0 x75_bit1 -x75_bit2 x75_bit3 -x75_bit4 x75_bit5 -x75_bit6 -x75_bit7 -x75_bit8 -x75_bit9 -x75_bit10 -x75_bit11 -x75_bit12 -x76_bit_7 x76_bit_6 -x76_bit_5 x76_bit_4 -x76_bit_3 x76_bit_2 x76_bit_1 x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 -x76_bit4 -x76_bit5 x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x77_bit_7 x77_bit_6 -x77_bit_5 x77_bit_4 x77_bit_3 x77_bit_2 -x77_bit_1 -x77_bit0 x77_bit1 -x77_bit2 x77_bit3 -x77_bit4 -x77_bit5 x77_bit6 -x77_bit7 -x77_bit8 -x77_bit9 -x77_bit10 -x77_bit11 -x77_bit12 -x78_bit_7 x78_bit_6 -x78_bit_5 x78_bit_4 x78_bit_3 x78_bit_2 -x78_bit_1 -x78_bit0 -x78_bit1 -x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x79_bit_7 x79_bit_6 x79_bit_5 x79_bit_4 -x79_bit_3 x79_bit_2 -x79_bit_1 -x79_bit0 -x79_bit1 -x79_bit2 -x79_bit3 -x79_bit4 x79_bit5 -x79_bit6 -x79_bit7 -x79_bit8 -x79_bit9 -x79_bit10 -x79_bit11 -x79_bit12 -x80_bit_7 x80_bit_6 x80_bit_5 x80_bit_4 -x80_bit_3 x80_bit_2 -x80_bit_1 x80_bit0 x80_bit1 x80_bit2 -x80_bit3 -x80_bit4 -x80_bit5 x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x81_bit_7 x81_bit_6 x81_bit_5 x81_bit_4 x81_bit_3 x81_bit_2 x81_bit_1 -x81_bit0 -x81_bit1 x81_bit2 x81_bit3 x81_bit4 x81_bit5 -x81_bit6 -x81_bit7 -x81_bit8 -x81_bit9 -x81_bit10 -x81_bit11 -x81_bit12 -x82_bit_7 x82_bit_6 x82_bit_5 x82_bit_4 x82_bit_3 x82_bit_2 x82_bit_1 -x82_bit0 -x82_bit1 -x82_bit2 -x82_bit3 -x82_bit4 -x82_bit5 x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x83_bit_7 x83_bit_6 -x83_bit_5 x83_bit_4 x83_bit_3 x83_bit_2 x83_bit_1 -x83_bit0 -x83_bit1 -x83_bit2 -x83_bit3 -x83_bit4 x83_bit5 -x83_bit6 -x83_bit7 -x83_bit8 -x83_bit9 -x83_bit10 -x83_bit11 -x83_bit12 -x84_bit_7 x84_bit_6 -x84_bit_5 x84_bit_4 x84_bit_3 x84_bit_2 x84_bit_1 -x84_bit0 -x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 -x84_bit5 x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 x85_bit_2 -x85_bit_1 -x85_bit0 x85_bit1 x85_bit2 -x85_bit3 x85_bit4 x85_bit5 -x85_bit6 -x85_bit7 -x85_bit8 -x85_bit9 -x85_bit10 -x85_bit11 -x85_bit12 -x86_bit_7 -x86_bit_6 -x86_bit_5 -x86_bit_4 -x86_bit_3 x86_bit_2 -x86_bit_1 -x86_bit0 -x86_bit1 -x86_bit2 x86_bit3 -x86_bit4 -x86_bit5 x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x59_bit_7 -x59_bit_6 -x59_bit_5 x59_bit_4 x59_bit_3 -x59_bit_2 -x59_bit_1 -x59_bit0 -x59_bit1 x59_bit2 -x59_bit3 -x59_bit4 x59_bit5 -x59_bit6 -x59_bit7 -x59_bit8 -x59_bit9 -x59_bit10 -x59_bit11 -x59_bit12 -x60_bit_7 -x60_bit_6 -x60_bit_5 x60_bit_4 x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 -x60_bit1 -x60_bit2 -x60_bit3 -x60_bit4 -x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x61_bit_7 -x61_bit_6 x61_bit_5 -x61_bit_4 -x61_bit_3 -x61_bit_2 x61_bit_1 x61_bit0 x6#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.94 2/54 11698
Raw data (stat): 11698 (runsolver) R 11697 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546086165 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42349 0 0 0 898 100 0 0 25 0 1 0 546086165 173289472 39143 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42307 39143 603 41 0 42266 0
vsize: 169228
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42409 0 0 0 1898 100 0 0 25 0 1 0 546086165 175239168 39203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42783 39203 603 41 0 42742 0
vsize: 171132
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42551 0 0 0 2898 100 0 0 25 0 1 0 546086165 175906816 39338 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42946 39338 603 41 0 42905 0
vsize: 171784
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42564 0 0 0 3897 101 0 0 25 0 1 0 546086165 176041984 39351 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42979 39351 603 41 0 42938 0
vsize: 171916
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42582 0 0 0 4897 101 0 0 25 0 1 0 546086165 176041984 39369 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42979 39369 603 41 0 42938 0
vsize: 171916
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42616 0 0 0 5897 101 0 0 25 0 1 0 546086165 176177152 39403 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43012 39403 603 41 0 42971 0
vsize: 172048
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42651 0 0 0 6896 101 0 0 25 0 1 0 546086165 176275456 39438 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43036 39438 603 41 0 42995 0
vsize: 172144
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42682 0 0 0 7896 102 0 0 25 0 1 0 546086165 176406528 39469 4294967295 134512640 134672761 3221224544 3221223724 134553584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43068 39469 603 41 0 43027 0
vsize: 172272
[startup+90.004 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42729 0 0 0 8896 102 0 0 25 0 1 0 546086165 176537600 39516 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43100 39516 603 41 0 43059 0
vsize: 172400
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42765 0 0 0 9896 102 0 0 25 0 1 0 546086165 176672768 39552 4294967295 134512640 134672761 3221224544 3221223696 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43133 39552 603 41 0 43092 0
vsize: 172532
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42797 0 0 0 10896 102 0 0 25 0 1 0 546086165 176672768 39584 4294967295 134512640 134672761 3221224544 3221223856 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43133 39584 603 41 0 43092 0
vsize: 172532
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42812 0 0 0 11896 102 0 0 25 0 1 0 546086165 176672768 39599 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43133 39599 603 41 0 43092 0
vsize: 172532
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42858 0 0 0 12896 102 0 0 25 0 1 0 546086165 176807936 39645 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43166 39645 603 41 0 43125 0
vsize: 172664
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42905 0 0 0 13896 102 0 0 25 0 1 0 546086165 177123328 39692 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43243 39692 603 41 0 43202 0
vsize: 172972
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42921 0 0 0 14896 102 0 0 25 0 1 0 546086165 177258496 39708 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43276 39708 603 41 0 43235 0
vsize: 173104
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42949 0 0 0 15896 102 0 0 25 0 1 0 546086165 177258496 39736 4294967295 134512640 134672761 3221224544 3221223856 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43276 39736 603 41 0 43235 0
vsize: 173104
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42961 0 0 0 16897 102 0 0 25 0 1 0 546086165 177393664 39748 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43309 39748 603 41 0 43268 0
vsize: 173236
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42979 0 0 0 17897 102 0 0 25 0 1 0 546086165 177393664 39766 4294967295 134512640 134672761 3221224544 3221223844 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43309 39766 603 41 0 43268 0
vsize: 173236
[startup+190.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 42989 0 0 0 18897 103 0 0 25 0 1 0 546086165 177393664 39776 4294967295 134512640 134672761 3221224544 3221223728 134557999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43309 39776 603 41 0 43268 0
vsize: 173236
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43005 0 0 0 19897 103 0 0 25 0 1 0 546086165 177528832 39792 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43342 39792 603 41 0 43301 0
vsize: 173368
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43017 0 0 0 20897 103 0 0 25 0 1 0 546086165 177528832 39804 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43342 39804 603 41 0 43301 0
vsize: 173368
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43040 0 0 0 21897 103 0 0 25 0 1 0 546086165 177528832 39827 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43342 39827 603 41 0 43301 0
vsize: 173368
[startup+230.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43053 0 0 0 22897 103 0 0 25 0 1 0 546086165 177664000 39840 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39840 603 41 0 43334 0
vsize: 173500
[startup+240.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43064 0 0 0 23897 103 0 0 25 0 1 0 546086165 177664000 39851 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39851 603 41 0 43334 0
vsize: 173500
[startup+250.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43076 0 0 0 24898 103 0 0 25 0 1 0 546086165 177664000 39863 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39863 603 41 0 43334 0
vsize: 173500
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43083 0 0 0 25898 103 0 0 25 0 1 0 546086165 177664000 39870 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39870 603 41 0 43334 0
vsize: 173500
[startup+270.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43095 0 0 0 26898 103 0 0 25 0 1 0 546086165 177799168 39882 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43408 39882 603 41 0 43367 0
vsize: 173632
[startup+280.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43107 0 0 0 27898 103 0 0 25 0 1 0 546086165 177799168 39894 4294967295 134512640 134672761 3221224544 3221223692 134566158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43408 39894 603 41 0 43367 0
vsize: 173632
[startup+290.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43124 0 0 0 28898 103 0 0 25 0 1 0 546086165 177799168 39911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43408 39911 603 41 0 43367 0
vsize: 173632
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43146 0 0 0 29898 103 0 0 25 0 1 0 546086165 177971200 39933 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39933 603 41 0 43409 0
vsize: 173800
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43169 0 0 0 30898 104 0 0 25 0 1 0 546086165 177971200 39956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39956 603 41 0 43409 0
vsize: 173800
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43174 0 0 0 31898 104 0 0 25 0 1 0 546086165 177971200 39961 4294967295 134512640 134672761 3221224544 3221223712 134564682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39961 603 41 0 43409 0
vsize: 173800
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43200 0 0 0 32898 104 0 0 25 0 1 0 546086165 177971200 39987 4294967295 134512640 134672761 3221224544 3221223844 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39987 603 41 0 43409 0
vsize: 173800
[startup+340.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43222 0 0 0 33898 104 0 0 25 0 1 0 546086165 178106368 40009 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43483 40009 603 41 0 43442 0
vsize: 173932
[startup+350.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43254 0 0 0 34898 104 0 0 25 0 1 0 546086165 178106368 40041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43483 40041 603 41 0 43442 0
vsize: 173932
[startup+360.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43283 0 0 0 35899 104 0 0 25 0 1 0 546086165 178241536 40070 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43516 40070 603 41 0 43475 0
vsize: 174064
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43301 0 0 0 36899 104 0 0 25 0 1 0 546086165 178376704 40088 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40088 603 41 0 43508 0
vsize: 174196
[startup+380.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43314 0 0 0 37899 104 0 0 25 0 1 0 546086165 178376704 40101 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40101 603 41 0 43508 0
vsize: 174196
[startup+390.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43326 0 0 0 38899 104 0 0 25 0 1 0 546086165 178376704 40113 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40113 603 41 0 43508 0
vsize: 174196
[startup+400.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43345 0 0 0 39899 104 0 0 25 0 1 0 546086165 178376704 40132 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40132 603 41 0 43508 0
vsize: 174196
[startup+410.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43365 0 0 0 40899 104 0 0 25 0 1 0 546086165 178565120 40152 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40152 603 41 0 43554 0
vsize: 174380
[startup+420.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43380 0 0 0 41899 104 0 0 25 0 1 0 546086165 178565120 40167 4294967295 134512640 134672761 3221224544 3221223844 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40167 603 41 0 43554 0
vsize: 174380
[startup+430.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43386 0 0 0 42899 104 0 0 25 0 1 0 546086165 178565120 40173 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40173 603 41 0 43554 0
vsize: 174380
[startup+440.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43388 0 0 0 43900 104 0 0 25 0 1 0 546086165 178565120 40175 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40175 603 41 0 43554 0
vsize: 174380
[startup+450.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43392 0 0 0 44900 104 0 0 25 0 1 0 546086165 178565120 40179 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40179 603 41 0 43554 0
vsize: 174380
[startup+460.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43400 0 0 0 45900 104 0 0 25 0 1 0 546086165 178565120 40187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40187 603 41 0 43554 0
vsize: 174380
[startup+470.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43405 0 0 0 46900 104 0 0 25 0 1 0 546086165 178565120 40192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40192 603 41 0 43554 0
vsize: 174380
[startup+480.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43412 0 0 0 47900 104 0 0 25 0 1 0 546086165 178696192 40199 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40199 603 41 0 43586 0
vsize: 174508
[startup+490.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43417 0 0 0 48900 104 0 0 25 0 1 0 546086165 178696192 40204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40204 603 41 0 43586 0
vsize: 174508
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43419 0 0 0 49900 104 0 0 25 0 1 0 546086165 178696192 40206 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40206 603 41 0 43586 0
vsize: 174508
[startup+510.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43423 0 0 0 50901 104 0 0 25 0 1 0 546086165 178696192 40210 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40210 603 41 0 43586 0
vsize: 174508
[startup+520.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43428 0 0 0 51901 104 0 0 25 0 1 0 546086165 178696192 40215 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40215 603 41 0 43586 0
vsize: 174508
[startup+530.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43433 0 0 0 52901 104 0 0 25 0 1 0 546086165 178696192 40220 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40220 603 41 0 43586 0
vsize: 174508
[startup+540.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43439 0 0 0 53901 104 0 0 25 0 1 0 546086165 178696192 40226 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40226 603 41 0 43586 0
vsize: 174508
[startup+550.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43443 0 0 0 54901 104 0 0 25 0 1 0 546086165 178823168 40230 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40230 603 41 0 43617 0
vsize: 174632
[startup+560.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43448 0 0 0 55902 104 0 0 25 0 1 0 546086165 178823168 40235 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40235 603 41 0 43617 0
vsize: 174632
[startup+570.01 s]
Raw data (loadavg): 1.07 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43449 0 0 0 56902 104 0 0 25 0 1 0 546086165 178823168 40236 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40236 603 41 0 43617 0
vsize: 174632
[startup+580.01 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43452 0 0 0 57902 104 0 0 25 0 1 0 546086165 178823168 40239 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40239 603 41 0 43617 0
vsize: 174632
[startup+590.011 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43455 0 0 0 58902 104 0 0 25 0 1 0 546086165 178823168 40242 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40242 603 41 0 43617 0
vsize: 174632
[startup+600.011 s]
Raw data (loadavg): 1.12 1.02 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43459 0 0 0 59902 104 0 0 25 0 1 0 546086165 178823168 40246 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40246 603 41 0 43617 0
vsize: 174632
[startup+610.011 s]
Raw data (loadavg): 1.10 1.02 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43465 0 0 0 60902 104 0 0 25 0 1 0 546086165 178823168 40252 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40252 603 41 0 43617 0
vsize: 174632
[startup+620.011 s]
Raw data (loadavg): 1.08 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43466 0 0 0 61902 104 0 0 25 0 1 0 546086165 178823168 40253 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40253 603 41 0 43617 0
vsize: 174632
[startup+630.011 s]
Raw data (loadavg): 1.07 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43470 0 0 0 62903 104 0 0 25 0 1 0 546086165 178823168 40257 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40257 603 41 0 43617 0
vsize: 174632
[startup+640.011 s]
Raw data (loadavg): 1.06 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43475 0 0 0 63903 104 0 0 25 0 1 0 546086165 178954240 40262 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40262 603 41 0 43649 0
vsize: 174760
[startup+650.011 s]
Raw data (loadavg): 1.05 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43478 0 0 0 64903 104 0 0 25 0 1 0 546086165 178954240 40265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40265 603 41 0 43649 0
vsize: 174760
[startup+660.011 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43481 0 0 0 65903 104 0 0 25 0 1 0 546086165 178954240 40268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40268 603 41 0 43649 0
vsize: 174760
[startup+670.011 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43485 0 0 0 66903 104 0 0 25 0 1 0 546086165 178954240 40272 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40272 603 41 0 43649 0
vsize: 174760
[startup+680.01 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43489 0 0 0 67903 104 0 0 25 0 1 0 546086165 178954240 40276 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40276 603 41 0 43649 0
vsize: 174760
[startup+690.01 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43491 0 0 0 68903 105 0 0 25 0 1 0 546086165 178954240 40278 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40278 603 41 0 43649 0
vsize: 174760
[startup+700.01 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43495 0 0 0 69903 105 0 0 25 0 1 0 546086165 178954240 40282 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40282 603 41 0 43649 0
vsize: 174760
[startup+710.01 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43499 0 0 0 70904 105 0 0 25 0 1 0 546086165 178954240 40286 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40286 603 41 0 43649 0
vsize: 174760
[startup+720.01 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43503 0 0 0 71904 105 0 0 25 0 1 0 546086165 178954240 40290 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40290 603 41 0 43649 0
vsize: 174760
[startup+730.01 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43506 0 0 0 72904 105 0 0 25 0 1 0 546086165 179081216 40293 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40293 603 41 0 43680 0
vsize: 174884
[startup+740.01 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43511 0 0 0 73904 105 0 0 25 0 1 0 546086165 179081216 40298 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40298 603 41 0 43680 0
vsize: 174884
[startup+750.01 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43515 0 0 0 74904 105 0 0 25 0 1 0 546086165 179081216 40302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40302 603 41 0 43680 0
vsize: 174884
[startup+760.01 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43519 0 0 0 75904 105 0 0 25 0 1 0 546086165 179081216 40306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40306 603 41 0 43680 0
vsize: 174884
[startup+770.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43522 0 0 0 76905 105 0 0 25 0 1 0 546086165 179081216 40309 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40309 603 41 0 43680 0
vsize: 174884
[startup+780.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43525 0 0 0 77905 105 0 0 25 0 1 0 546086165 179081216 40312 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40312 603 41 0 43680 0
vsize: 174884
[startup+790.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43531 0 0 0 78905 105 0 0 25 0 1 0 546086165 179081216 40318 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40318 603 41 0 43680 0
vsize: 174884
[startup+800.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43533 0 0 0 79905 105 0 0 25 0 1 0 546086165 179081216 40320 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40320 603 41 0 43680 0
vsize: 174884
[startup+810.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43540 0 0 0 80905 105 0 0 25 0 1 0 546086165 179236864 40327 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40327 603 41 0 43718 0
vsize: 175036
[startup+820.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43542 0 0 0 81906 105 0 0 25 0 1 0 546086165 179236864 40329 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40329 603 41 0 43718 0
vsize: 175036
[startup+830.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43545 0 0 0 82906 105 0 0 25 0 1 0 546086165 179236864 40332 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40332 603 41 0 43718 0
vsize: 175036
[startup+840.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43550 0 0 0 83906 105 0 0 25 0 1 0 546086165 179236864 40337 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40337 603 41 0 43718 0
vsize: 175036
[startup+850.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43552 0 0 0 84906 105 0 0 25 0 1 0 546086165 179236864 40339 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40339 603 41 0 43718 0
vsize: 175036
[startup+860.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43555 0 0 0 85906 105 0 0 25 0 1 0 546086165 179236864 40342 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40342 603 41 0 43718 0
vsize: 175036
[startup+870.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43559 0 0 0 86906 105 0 0 25 0 1 0 546086165 179236864 40346 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40346 603 41 0 43718 0
vsize: 175036
[startup+880.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43563 0 0 0 87907 105 0 0 25 0 1 0 546086165 179236864 40350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40350 603 41 0 43718 0
vsize: 175036
[startup+890.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43567 0 0 0 88907 105 0 0 25 0 1 0 546086165 179236864 40354 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40354 603 41 0 43718 0
vsize: 175036
[startup+900.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43570 0 0 0 89907 105 0 0 25 0 1 0 546086165 179236864 40357 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40357 603 41 0 43718 0
vsize: 175036
[startup+910.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43574 0 0 0 90907 105 0 0 25 0 1 0 546086165 179367936 40361 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40361 603 41 0 43750 0
vsize: 175164
[startup+920.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43578 0 0 0 91907 105 0 0 25 0 1 0 546086165 179367936 40365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40365 603 41 0 43750 0
vsize: 175164
[startup+930.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43585 0 0 0 92907 105 0 0 25 0 1 0 546086165 179367936 40372 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40372 603 41 0 43750 0
vsize: 175164
[startup+940.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43589 0 0 0 93908 105 0 0 25 0 1 0 546086165 179367936 40376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40376 603 41 0 43750 0
vsize: 175164
[startup+950.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43593 0 0 0 94908 105 0 0 25 0 1 0 546086165 179367936 40380 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40380 603 41 0 43750 0
vsize: 175164
[startup+960.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43596 0 0 0 95908 105 0 0 25 0 1 0 546086165 179367936 40383 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40383 603 41 0 43750 0
vsize: 175164
[startup+970.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43601 0 0 0 96908 105 0 0 25 0 1 0 546086165 179367936 40388 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40388 603 41 0 43750 0
vsize: 175164
[startup+980.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43605 0 0 0 97908 105 0 0 25 0 1 0 546086165 179486720 40392 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40392 603 41 0 43779 0
vsize: 175280
[startup+990.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43607 0 0 0 98909 105 0 0 25 0 1 0 546086165 179486720 40394 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40394 603 41 0 43779 0
vsize: 175280
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43612 0 0 0 99909 105 0 0 25 0 1 0 546086165 179486720 40399 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40399 603 41 0 43779 0
vsize: 175280
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43616 0 0 0 100909 105 0 0 25 0 1 0 546086165 179486720 40403 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40403 603 41 0 43779 0
vsize: 175280
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43620 0 0 0 101909 105 0 0 25 0 1 0 546086165 179486720 40407 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40407 603 41 0 43779 0
vsize: 175280
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43624 0 0 0 102909 105 0 0 25 0 1 0 546086165 179486720 40411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40411 603 41 0 43779 0
vsize: 175280
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43630 0 0 0 103909 105 0 0 25 0 1 0 546086165 179486720 40417 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40417 603 41 0 43779 0
vsize: 175280
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43635 0 0 0 104909 105 0 0 25 0 1 0 546086165 179605504 40422 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40422 603 41 0 43808 0
vsize: 175396
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43638 0 0 0 105909 105 0 0 25 0 1 0 546086165 179605504 40425 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40425 603 41 0 43808 0
vsize: 175396
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43640 0 0 0 106909 105 0 0 25 0 1 0 546086165 179605504 40427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40427 603 41 0 43808 0
vsize: 175396
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43646 0 0 0 107910 105 0 0 25 0 1 0 546086165 179605504 40433 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40433 603 41 0 43808 0
vsize: 175396
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43655 0 0 0 108910 105 0 0 25 0 1 0 546086165 179605504 40442 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40442 603 41 0 43808 0
vsize: 175396
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43659 0 0 0 109910 105 0 0 25 0 1 0 546086165 179605504 40446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40446 603 41 0 43808 0
vsize: 175396
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43664 0 0 0 110910 105 0 0 25 0 1 0 546086165 179605504 40451 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40451 603 41 0 43808 0
vsize: 175396
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43668 0 0 0 111910 105 0 0 25 0 1 0 546086165 179605504 40455 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40455 603 41 0 43808 0
vsize: 175396
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43672 0 0 0 112910 105 0 0 25 0 1 0 546086165 179736576 40459 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40459 603 41 0 43840 0
vsize: 175524
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43676 0 0 0 113910 105 0 0 25 0 1 0 546086165 179736576 40463 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40463 603 41 0 43840 0
vsize: 175524
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43679 0 0 0 114911 105 0 0 25 0 1 0 546086165 179736576 40466 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40466 603 41 0 43840 0
vsize: 175524
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43682 0 0 0 115911 105 0 0 25 0 1 0 546086165 179736576 40469 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40469 603 41 0 43840 0
vsize: 175524
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43688 0 0 0 116911 105 0 0 25 0 1 0 546086165 179736576 40475 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40475 603 41 0 43840 0
vsize: 175524
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43693 0 0 0 117911 105 0 0 25 0 1 0 546086165 179736576 40480 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40480 603 41 0 43840 0
vsize: 175524
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43696 0 0 0 118911 105 0 0 25 0 1 0 546086165 179736576 40483 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40483 603 41 0 43840 0
vsize: 175524
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 11698
Raw data (stat): 11698 (minisat+) R 11697 28546 28545 0 -1 0 43700 0 0 0 119911 106 0 0 25 0 1 0 546086165 179736576 40487 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40487 603 41 0 43840 0
vsize: 175524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 11698
Raw data (stat): 11698 (minisat+) Z 11697 28546 28545 0 -1 12 43703 0 0 0 119911 114 0 0 25 0 1 0 546086165 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.26
CPU user time (s): 1199.12
CPU system time (s): 1.14183
CPU usage (%): 100.014
Max. virtual memory (Kb): 175524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####