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/miplib3/normalized-mps-v2-13-7-pk1.opb
MD5SUM	b6007187ad037f56a5e2b97a0b86cea8
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.03
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 17963

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 12:54:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18758 boxname=wulflinc7 idbench=1443 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6007187ad037f56a5e2b97a0b86cea8  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pk1.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 18758
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        663328 kB
Buffers:         18652 kB
Cached:         330932 kB
SwapCached:          4 kB
Active:         167100 kB
Inactive:       185320 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        663076 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            13172 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:14:25 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 18758 7 1200.28 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 |      7917 | 1331420  3896674 |  590705    7398   306091    41.4 |  0.531 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -d_bit_7 -d_bit_6 d_bit_5 d_bit_4 -d_bit_3 d_bit_2 d_bit_1 -d_bit0 d_bit1 -d_bit2 d_bit3 -d_bit4 -d_bit5 d_bit6 -d_bit7 -d_bit8 -d_bit9 -d_bit10 -d_bit11 -d_bit12 X1_bit0 -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 -S1_bit_7 S1_bit_6 S1_bit_5 -S1_bit_4 -S1_bit_3 S1_bit_2 S1_bit_1 -S1_bit0 -S1_bit1 -S1_bit2 -S1_bit3 -S1_bit4 -S1_bit5 S1_bit6 -S1_bit7 -S1_bit8 -S1_bit9 -S1_bit10 -S1_bit11 -S1_bit12 -T1_bit_7 T1_bit_6 T1_bit_5 -T1_bit_4 -T1_bit_3 T1_bit_2 T1_bit_1 -T1_bit0 -T1_bit1 -T1_bit2 -T1_bit3 T1_bit4 -T1_bit5 -T1_bit6 -T1_bit7 -T1_bit8 -T1_bit9 -T1_bit10 -T1_bit11 -T1_bit12 -S10_bit_7 S10_bit_6 -S10_bit_5 S10_bit_4 -S10_bit_3 S10_bit_2 S10_bit_1 -S10_bit0 S10_bit1 -S10_bit2 S10_bit3 -S10_bit4 S10_bit5 -S10_bit6 -S10_bit7 -S10_bit8 -S10_bit9 -S10_bit10 -S10_bit11 -S10_bit12 -T10_bit_7 T10_bit_6 -T10_bit_5 T10_bit_4 -T10_bit_3 T10_bit_2 T10_bit_1 T10_bit0 -T10_bit1 -T10_bit2 -T10_bit3 -T10_bit4 -T10_bit5 T10_bit6 -T10_bit7 -T10_bit8 -T10_bit9 -T10_bit10 -T10_bit11 -T10_bit12 -S11_bit_7 S11_bit_6 -S11_bit_5 S11_bit_4 S11_bit_3 S11_bit_2 -S11_bit_1 -S11_bit0 S11_bit1 -S11_bit2 S11_bit3 -S11_bit4 -S11_bit5 S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -T11_bit_7 T11_bit_6 -T11_bit_5 T11_bit_4 T11_bit_3 T11_bit_2 -T11_bit_1 -T11_bit0 -T11_bit1 -T11_bit2 -T11_bit3 -T11_bit4 -T11_bit5 -T11_bit6 -T11_bit7 -T11_bit8 -T11_bit9 -T11_bit10 -T11_bit11 -T11_bit12 -S12_bit_7 S12_bit_6 S12_bit_5 S12_bit_4 -S12_bit_3 S12_bit_2 -S12_bit_1 -S12_bit0 -S12_bit1 -S12_bit2 -S12_bit3 -S12_bit4 S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 -T12_bit_7 T12_bit_6 T12_bit_5 T12_bit_4 -T12_bit_3 T12_bit_2 -T12_bit_1 T12_bit0 T12_bit1 T12_bit2 -T12_bit3 -T12_bit4 -T12_bit5 T12_bit6 -T12_bit7 -T12_bit8 -T12_bit9 -T12_bit10 -T12_bit11 -T12_bit12 -S13_bit_7 S13_bit_6 S13_bit_5 S13_bit_4 S13_bit_3 S13_bit_2 S13_bit_1 -S13_bit0 -S13_bit1 S13_bit2 S13_bit3 S13_bit4 S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -T13_bit_7 T13_bit_6 T13_bit_5 T13_bit_4 T13_bit_3 T13_bit_2 T13_bit_1 -T13_bit0 -T13_bit1 -T13_bit2 -T13_bit3 -T13_bit4 -T13_bit5 T13_bit6 -T13_bit7 -T13_bit8 -T13_bit9 -T13_bit10 -T13_bit11 -T13_bit12 -S14_bit_7 S14_bit_6 -S14_bit_5 S14_bit_4 S14_bit_3 S14_bit_2 S14_bit_1 -S14_bit0 -S14_bit1 -S14_bit2 -S14_bit3 -S14_bit4 S14_bit5 -S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 -T14_bit_7 T14_bit_6 -T14_bit_5 T14_bit_4 T14_bit_3 T14_bit_2 T14_bit_1 -T14_bit0 -T14_bit1 -T14_bit2 -T14_bit3 -T14_bit4 -T14_bit5 T14_bit6 -T14_bit7 -T14_bit8 -T14_bit9 -T14_bit10 -T14_bit11 -T14_bit12 -S15_bit_7 -S15_bit_6 -S15_bit_5 -S15_bit_4 -S15_bit_3 S15_bit_2 -S15_bit_1 -S15_bit0 S15_bit1 S15_bit2 -S15_bit3 S15_bit4 S15_bit5 -S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 -T15_bit_7 -T15_bit_6 -T15_bit_5 -T15_bit_4 -T15_bit_3 T15_bit_2 -T15_bit_1 -T15_bit0 -T15_bit1 -T15_bit2 T15_bit3 -T15_bit4 -T15_bit5 T15_bit6 -T15_bit7 -T15_bit8 -T15_bit9 -T15_bit10 -T15_bit11 -T15_bit12 -S2_bit_7 -S2_bit_6 -S2_bit_5 S2_bit_4 S2_bit_3 -S2_bit_2 -S2_bit_1 -S2_bit0 -S2_bit1 S2_bit2 -S2_bit3 -S2_bit4 S2_bit5 -S2_bit6 -S2_bit7 -S2_bit8 -S2_bit9 -S2_bit10 -S2_bit11 -S2_bit12 -T2_bit_7 -T2_bit_6 -T2_bit_5 T2_bit_4 T2_bit_3 -T2_bit_2 -T2_bit_1 -T2_bit0 -T2_bit1 -T2_bit2 -T2_bit3 -T2_bit4 -T2_bit5 -T2_bit6 -T2_bit7 -T2_bit8 -T2_bit9 -T2_bit10 -T2_bit11 -T2_bit12 -S3_bit_7 -S3_bit_6 S3_bit_5 -S3_bit_4 -S3_bit_3 -S3_bit_2 S3_bit_1 S3_bit0 S3_bit1 S3_bit2 -S3_bit3 -S3_bit4 -S3_bit5 S3_bit6 -S3_bit7 -S3_bit8 -S3_bit9 -S3_bit10 -S3_bit11 -S3_bit12 -T3#### 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.85 0.97 0.94 2/54 6672
Raw data (stat): 6672 (runsolver) R 6671 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487020310 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s]
Raw data (loadavg): 0.87 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42349 0 0 0 899 99 0 0 25 0 1 0 487020310 173289472 39143 4294967295 134512640 134672761 3221224544 3221223688 134560630 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.0015 s]
Raw data (loadavg): 0.89 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42409 0 0 0 1899 99 0 0 25 0 1 0 487020310 175239168 39203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42783 39203 603 41 0 42742 0
vsize: 171132
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42551 0 0 0 2899 100 0 0 25 0 1 0 487020310 175906816 39338 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.0021 s]
Raw data (loadavg): 0.92 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42568 0 0 0 3898 100 0 0 25 0 1 0 487020310 176041984 39355 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42979 39355 603 41 0 42938 0
vsize: 171916
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42588 0 0 0 4898 101 0 0 25 0 1 0 487020310 176041984 39375 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42979 39375 603 41 0 42938 0
vsize: 171916
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42642 0 0 0 5898 101 0 0 25 0 1 0 487020310 176275456 39429 4294967295 134512640 134672761 3221224544 3221223844 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43036 39429 603 41 0 42995 0
vsize: 172144
[startup+70.002 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42658 0 0 0 6897 102 0 0 25 0 1 0 487020310 176275456 39445 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43036 39445 603 41 0 42995 0
vsize: 172144
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42703 0 0 0 7897 102 0 0 25 0 1 0 487020310 176406528 39490 4294967295 134512640 134672761 3221224544 3221223844 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43068 39490 603 41 0 43027 0
vsize: 172272
[startup+90.0033 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42742 0 0 0 8897 102 0 0 25 0 1 0 487020310 176537600 39529 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43100 39529 603 41 0 43059 0
vsize: 172400
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42780 0 0 0 9896 103 0 0 25 0 1 0 487020310 176672768 39567 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43133 39567 603 41 0 43092 0
vsize: 172532
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42802 0 0 0 10896 103 0 0 25 0 1 0 487020310 176672768 39589 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43133 39589 603 41 0 43092 0
vsize: 172532
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42819 0 0 0 11896 103 0 0 25 0 1 0 487020310 176807936 39606 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43166 39606 603 41 0 43125 0
vsize: 172664
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42865 0 0 0 12896 104 0 0 25 0 1 0 487020310 176807936 39652 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43166 39652 603 41 0 43125 0
vsize: 172664
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42911 0 0 0 13896 104 0 0 25 0 1 0 487020310 177258496 39698 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43276 39698 603 41 0 43235 0
vsize: 173104
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42931 0 0 0 14896 104 0 0 25 0 1 0 487020310 177258496 39718 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43276 39718 603 41 0 43235 0
vsize: 173104
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42956 0 0 0 15896 104 0 0 25 0 1 0 487020310 177258496 39743 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43276 39743 603 41 0 43235 0
vsize: 173104
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42970 0 0 0 16896 105 0 0 25 0 1 0 487020310 177393664 39757 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43309 39757 603 41 0 43268 0
vsize: 173236
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 42986 0 0 0 17896 105 0 0 25 0 1 0 487020310 177393664 39773 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43309 39773 603 41 0 43268 0
vsize: 173236
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43002 0 0 0 18896 105 0 0 25 0 1 0 487020310 177528832 39789 4294967295 134512640 134672761 3221224544 3221223880 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43342 39789 603 41 0 43301 0
vsize: 173368
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43014 0 0 0 19896 105 0 0 25 0 1 0 487020310 177528832 39801 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43342 39801 603 41 0 43301 0
vsize: 173368
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43034 0 0 0 20896 105 0 0 25 0 1 0 487020310 177528832 39821 4294967295 134512640 134672761 3221224544 3221223844 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43342 39821 603 41 0 43301 0
vsize: 173368
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43050 0 0 0 21896 105 0 0 25 0 1 0 487020310 177664000 39837 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39837 603 41 0 43334 0
vsize: 173500
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43057 0 0 0 22897 105 0 0 25 0 1 0 487020310 177664000 39844 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39844 603 41 0 43334 0
vsize: 173500
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43070 0 0 0 23897 105 0 0 25 0 1 0 487020310 177664000 39857 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39857 603 41 0 43334 0
vsize: 173500
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43082 0 0 0 24897 105 0 0 25 0 1 0 487020310 177664000 39869 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 39869 603 41 0 43334 0
vsize: 173500
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43093 0 0 0 25897 105 0 0 25 0 1 0 487020310 177799168 39880 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43408 39880 603 41 0 43367 0
vsize: 173632
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43105 0 0 0 26897 105 0 0 25 0 1 0 487020310 177799168 39892 4294967295 134512640 134672761 3221224544 3221223668 134566145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43408 39892 603 41 0 43367 0
vsize: 173632
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43121 0 0 0 27897 105 0 0 25 0 1 0 487020310 177799168 39908 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43408 39908 603 41 0 43367 0
vsize: 173632
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43146 0 0 0 28897 105 0 0 25 0 1 0 487020310 177971200 39933 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39933 603 41 0 43409 0
vsize: 173800
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43166 0 0 0 29897 105 0 0 25 0 1 0 487020310 177971200 39953 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39953 603 41 0 43409 0
vsize: 173800
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43174 0 0 0 30898 105 0 0 25 0 1 0 487020310 177971200 39961 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39961 603 41 0 43409 0
vsize: 173800
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43195 0 0 0 31897 106 0 0 25 0 1 0 487020310 177971200 39982 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43450 39982 603 41 0 43409 0
vsize: 173800
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43221 0 0 0 32897 106 0 0 25 0 1 0 487020310 178106368 40008 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43483 40008 603 41 0 43442 0
vsize: 173932
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6672
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43254 0 0 0 33897 106 0 0 25 0 1 0 487020310 178106368 40041 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43483 40041 603 41 0 43442 0
vsize: 173932
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6725
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43283 0 0 0 34897 106 0 0 25 0 1 0 487020310 178241536 40070 4294967295 134512640 134672761 3221224544 3221223872 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43516 40070 603 41 0 43475 0
vsize: 174064
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6725
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43301 0 0 0 35897 106 0 0 25 0 1 0 487020310 178376704 40088 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40088 603 41 0 43508 0
vsize: 174196
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6725
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43314 0 0 0 36897 106 0 0 25 0 1 0 487020310 178376704 40101 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40101 603 41 0 43508 0
vsize: 174196
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6725
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43326 0 0 0 37898 106 0 0 25 0 1 0 487020310 178376704 40113 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40113 603 41 0 43508 0
vsize: 174196
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6725
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43346 0 0 0 38898 106 0 0 25 0 1 0 487020310 178376704 40133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43549 40133 603 41 0 43508 0
vsize: 174196
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6725
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43365 0 0 0 39898 107 0 0 25 0 1 0 487020310 178565120 40152 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40152 603 41 0 43554 0
vsize: 174380
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6725
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43380 0 0 0 40898 107 0 0 25 0 1 0 487020310 178565120 40167 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40167 603 41 0 43554 0
vsize: 174380
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43386 0 0 0 41898 107 0 0 25 0 1 0 487020310 178565120 40173 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40173 603 41 0 43554 0
vsize: 174380
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43388 0 0 0 42898 107 0 0 25 0 1 0 487020310 178565120 40175 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40175 603 41 0 43554 0
vsize: 174380
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43393 0 0 0 43898 107 0 0 25 0 1 0 487020310 178565120 40180 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40180 603 41 0 43554 0
vsize: 174380
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43401 0 0 0 44898 107 0 0 25 0 1 0 487020310 178565120 40188 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40188 603 41 0 43554 0
vsize: 174380
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43407 0 0 0 45898 107 0 0 25 0 1 0 487020310 178565120 40194 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43595 40194 603 41 0 43554 0
vsize: 174380
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43413 0 0 0 46899 107 0 0 25 0 1 0 487020310 178696192 40200 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40200 603 41 0 43586 0
vsize: 174508
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43418 0 0 0 47899 107 0 0 25 0 1 0 487020310 178696192 40205 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40205 603 41 0 43586 0
vsize: 174508
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43421 0 0 0 48899 107 0 0 25 0 1 0 487020310 178696192 40208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40208 603 41 0 43586 0
vsize: 174508
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43426 0 0 0 49899 107 0 0 25 0 1 0 487020310 178696192 40213 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40213 603 41 0 43586 0
vsize: 174508
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43430 0 0 0 50899 107 0 0 25 0 1 0 487020310 178696192 40217 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40217 603 41 0 43586 0
vsize: 174508
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43437 0 0 0 51900 107 0 0 25 0 1 0 487020310 178696192 40224 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43627 40224 603 41 0 43586 0
vsize: 174508
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43441 0 0 0 52900 107 0 0 25 0 1 0 487020310 178823168 40228 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40228 603 41 0 43617 0
vsize: 174632
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43444 0 0 0 53900 107 0 0 25 0 1 0 487020310 178823168 40231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40231 603 41 0 43617 0
vsize: 174632
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43448 0 0 0 54900 107 0 0 25 0 1 0 487020310 178823168 40235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40235 603 41 0 43617 0
vsize: 174632
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43451 0 0 0 55900 107 0 0 25 0 1 0 487020310 178823168 40238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40238 603 41 0 43617 0
vsize: 174632
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43455 0 0 0 56900 107 0 0 25 0 1 0 487020310 178823168 40242 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40242 603 41 0 43617 0
vsize: 174632
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43458 0 0 0 57900 107 0 0 25 0 1 0 487020310 178823168 40245 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40245 603 41 0 43617 0
vsize: 174632
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43463 0 0 0 58901 107 0 0 25 0 1 0 487020310 178823168 40250 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40250 603 41 0 43617 0
vsize: 174632
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43466 0 0 0 59901 107 0 0 25 0 1 0 487020310 178823168 40253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40253 603 41 0 43617 0
vsize: 174632
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43468 0 0 0 60901 107 0 0 25 0 1 0 487020310 178823168 40255 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 40255 603 41 0 43617 0
vsize: 174632
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43473 0 0 0 61901 107 0 0 25 0 1 0 487020310 178954240 40260 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40260 603 41 0 43649 0
vsize: 174760
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43477 0 0 0 62901 107 0 0 25 0 1 0 487020310 178954240 40264 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40264 603 41 0 43649 0
vsize: 174760
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43481 0 0 0 63901 107 0 0 25 0 1 0 487020310 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+650.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43485 0 0 0 64901 108 0 0 25 0 1 0 487020310 178954240 40272 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40272 603 41 0 43649 0
vsize: 174760
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43489 0 0 0 65902 108 0 0 25 0 1 0 487020310 178954240 40276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40276 603 41 0 43649 0
vsize: 174760
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43491 0 0 0 66902 108 0 0 25 0 1 0 487020310 178954240 40278 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40278 603 41 0 43649 0
vsize: 174760
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43494 0 0 0 67902 108 0 0 25 0 1 0 487020310 178954240 40281 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40281 603 41 0 43649 0
vsize: 174760
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43499 0 0 0 68902 108 0 0 25 0 1 0 487020310 178954240 40286 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40286 603 41 0 43649 0
vsize: 174760
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43501 0 0 0 69902 108 0 0 25 0 1 0 487020310 178954240 40288 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43690 40288 603 41 0 43649 0
vsize: 174760
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43506 0 0 0 70903 108 0 0 25 0 1 0 487020310 179081216 40293 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40293 603 41 0 43680 0
vsize: 174884
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6727
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43511 0 0 0 71903 108 0 0 25 0 1 0 487020310 179081216 40298 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40298 603 41 0 43680 0
vsize: 174884
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43516 0 0 0 72903 108 0 0 25 0 1 0 487020310 179081216 40303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40303 603 41 0 43680 0
vsize: 174884
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43519 0 0 0 73903 108 0 0 25 0 1 0 487020310 179081216 40306 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40306 603 41 0 43680 0
vsize: 174884
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43523 0 0 0 74903 108 0 0 25 0 1 0 487020310 179081216 40310 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40310 603 41 0 43680 0
vsize: 174884
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43526 0 0 0 75903 108 0 0 25 0 1 0 487020310 179081216 40313 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40313 603 41 0 43680 0
vsize: 174884
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43531 0 0 0 76903 108 0 0 25 0 1 0 487020310 179081216 40318 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43721 40318 603 41 0 43680 0
vsize: 174884
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43538 0 0 0 77904 108 0 0 25 0 1 0 487020310 179236864 40325 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40325 603 41 0 43718 0
vsize: 175036
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43540 0 0 0 78904 108 0 0 25 0 1 0 487020310 179236864 40327 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40327 603 41 0 43718 0
vsize: 175036
[startup+800.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43542 0 0 0 79904 108 0 0 25 0 1 0 487020310 179236864 40329 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40329 603 41 0 43718 0
vsize: 175036
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43546 0 0 0 80904 108 0 0 25 0 1 0 487020310 179236864 40333 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40333 603 41 0 43718 0
vsize: 175036
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43550 0 0 0 81904 108 0 0 25 0 1 0 487020310 179236864 40337 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40337 603 41 0 43718 0
vsize: 175036
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43553 0 0 0 82904 108 0 0 25 0 1 0 487020310 179236864 40340 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40340 603 41 0 43718 0
vsize: 175036
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43557 0 0 0 83905 108 0 0 25 0 1 0 487020310 179236864 40344 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40344 603 41 0 43718 0
vsize: 175036
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43560 0 0 0 84905 108 0 0 25 0 1 0 487020310 179236864 40347 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40347 603 41 0 43718 0
vsize: 175036
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43565 0 0 0 85905 108 0 0 25 0 1 0 487020310 179236864 40352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40352 603 41 0 43718 0
vsize: 175036
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43568 0 0 0 86905 108 0 0 25 0 1 0 487020310 179236864 40355 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43759 40355 603 41 0 43718 0
vsize: 175036
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43572 0 0 0 87905 108 0 0 25 0 1 0 487020310 179367936 40359 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40359 603 41 0 43750 0
vsize: 175164
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43576 0 0 0 88905 108 0 0 25 0 1 0 487020310 179367936 40363 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40363 603 41 0 43750 0
vsize: 175164
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43580 0 0 0 89905 108 0 0 25 0 1 0 487020310 179367936 40367 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40367 603 41 0 43750 0
vsize: 175164
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43586 0 0 0 90906 108 0 0 25 0 1 0 487020310 179367936 40373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40373 603 41 0 43750 0
vsize: 175164
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43591 0 0 0 91906 108 0 0 25 0 1 0 487020310 179367936 40378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40378 603 41 0 43750 0
vsize: 175164
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43595 0 0 0 92906 108 0 0 25 0 1 0 487020310 179367936 40382 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40382 603 41 0 43750 0
vsize: 175164
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43600 0 0 0 93906 108 0 0 25 0 1 0 487020310 179367936 40387 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43791 40387 603 41 0 43750 0
vsize: 175164
[startup+950.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43604 0 0 0 94906 108 0 0 25 0 1 0 487020310 179486720 40391 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40391 603 41 0 43779 0
vsize: 175280
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43607 0 0 0 95906 108 0 0 25 0 1 0 487020310 179486720 40394 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40394 603 41 0 43779 0
vsize: 175280
[startup+970.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43611 0 0 0 96907 108 0 0 25 0 1 0 487020310 179486720 40398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40398 603 41 0 43779 0
vsize: 175280
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43616 0 0 0 97907 108 0 0 25 0 1 0 487020310 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+990.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43618 0 0 0 98907 108 0 0 25 0 1 0 487020310 179486720 40405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40405 603 41 0 43779 0
vsize: 175280
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43623 0 0 0 99907 108 0 0 25 0 1 0 487020310 179486720 40410 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40410 603 41 0 43779 0
vsize: 175280
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43630 0 0 0 100907 109 0 0 25 0 1 0 487020310 179486720 40417 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 40417 603 41 0 43779 0
vsize: 175280
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43635 0 0 0 101907 109 0 0 25 0 1 0 487020310 179605504 40422 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40422 603 41 0 43808 0
vsize: 175396
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43638 0 0 0 102907 109 0 0 25 0 1 0 487020310 179605504 40425 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40425 603 41 0 43808 0
vsize: 175396
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43640 0 0 0 103907 109 0 0 25 0 1 0 487020310 179605504 40427 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40427 603 41 0 43808 0
vsize: 175396
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43648 0 0 0 104907 109 0 0 25 0 1 0 487020310 179605504 40435 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40435 603 41 0 43808 0
vsize: 175396
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43656 0 0 0 105907 109 0 0 25 0 1 0 487020310 179605504 40443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40443 603 41 0 43808 0
vsize: 175396
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43659 0 0 0 106907 109 0 0 25 0 1 0 487020310 179605504 40446 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40446 603 41 0 43808 0
vsize: 175396
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43664 0 0 0 107907 109 0 0 25 0 1 0 487020310 179605504 40451 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40451 603 41 0 43808 0
vsize: 175396
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43668 0 0 0 108908 109 0 0 25 0 1 0 487020310 179605504 40455 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43849 40455 603 41 0 43808 0
vsize: 175396
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43673 0 0 0 109908 109 0 0 25 0 1 0 487020310 179736576 40460 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40460 603 41 0 43840 0
vsize: 175524
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43678 0 0 0 110908 109 0 0 25 0 1 0 487020310 179736576 40465 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40465 603 41 0 43840 0
vsize: 175524
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43679 0 0 0 111908 110 0 0 25 0 1 0 487020310 179736576 40466 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40466 603 41 0 43840 0
vsize: 175524
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43684 0 0 0 112908 110 0 0 25 0 1 0 487020310 179736576 40471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40471 603 41 0 43840 0
vsize: 175524
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43688 0 0 0 113908 110 0 0 25 0 1 0 487020310 179736576 40475 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40475 603 41 0 43840 0
vsize: 175524
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43693 0 0 0 114908 110 0 0 25 0 1 0 487020310 179736576 40480 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40480 603 41 0 43840 0
vsize: 175524
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43697 0 0 0 115909 110 0 0 25 0 1 0 487020310 179736576 40484 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40484 603 41 0 43840 0
vsize: 175524
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43703 0 0 0 116909 110 0 0 25 0 1 0 487020310 179736576 40490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43881 40490 603 41 0 43840 0
vsize: 175524
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43706 0 0 0 117909 110 0 0 25 0 1 0 487020310 179859456 40493 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43911 40493 603 41 0 43870 0
vsize: 175644
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43710 0 0 0 118909 110 0 0 25 0 1 0 487020310 179859456 40497 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43911 40497 603 41 0 43870 0
vsize: 175644
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 6729
Raw data (stat): 6672 (minisat+) R 6671 22932 22931 0 -1 0 43715 0 0 0 119909 110 0 0 25 0 1 0 487020310 179859456 40502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43911 40502 603 41 0 43870 0
vsize: 175644
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 6729
Raw data (stat): 6672 (minisat+) Z 6671 22932 22931 0 -1 12 43718 0 0 0 119909 118 0 0 25 0 1 0 487020310 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.28
CPU user time (s): 1199.1
CPU system time (s): 1.18382
CPU usage (%): 100.015
Max. virtual memory (Kb): 175644
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####