PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-05-27 09:17:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23733 boxname=wulflinc25 idbench=1377 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9c5126d785c8d5465220e290c5fc25a6  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 23733
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901312 kB
Buffers:           352 kB
Cached:         113668 kB
SwapCached:        900 kB
Active:          18788 kB
Inactive:        97204 kB
HighTotal:      131008 kB
HighFree:        14420 kB
LowTotal:       903652 kB
LowFree:        886892 kB
SwapTotal:     2097892 kB
SwapFree:      2095960 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4916 kB
Slab:            11592 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 09:38:16 (client local time) WITH STATUS 152 IN 1229.91 SECONDS
stats: 23733 7 1229.91 152
#### 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 ---[   0]---> Sorter-cost:  181     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1317281  3864081 |  439093       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 610640[0m
c ---[   0]---> Sorter-cost:  101     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 | 1317484  3864555 |  439161       0        0     nan |  0.000 % |
c |       100 | 1317484  3864555 |  483077     100     2510    25.1 |  0.010 % |
c |       250 | 1317484  3864555 |  531384     250     4585    18.3 |  0.010 % |
c ==============================================================================
c [1mFound solution: 526860[0m
c ---[   0]---> Sorter-cost:  115     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 |       440 | 1317707  3865073 |  439235     440     7815    17.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 524800[0m
c ---[   0]---> Sorter-cost:   63     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 |       496 | 1317818  3865330 |  439272     496     8766    17.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 275028[0m
c ---[   0]---> Sorter-cost:  112     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 |       504 | 1317623  3864731 |  439207     470     8556    18.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 105044[0m
c ---[   0]---> Sorter-cost:  149     Base: 2 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 |       508 | 1317041  3863134 |  439013     439     8464    19.3 |  0.010 % |
c ==============================================================================
c [1mFound solution: 102998[0m
c ---[   0]---> Sorter-cost:  158     Base: 2 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 |       519 | 1317373  3863912 |  439124     450     8633    19.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 102996[0m
c ---[   0]---> Sorter-cost:   48     Base: 2 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 |       520 | 1317465  3864130 |  439155     451     8635    19.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 101014[0m
c ---[   0]---> Sorter-cost:  120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       520 | 1317684  3864649 |  439228     451     8635    19.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 100948[0m
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       526 | 1317729  3864762 |  439243     457     8708    19.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 98918[0m
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 |       526 | 1318048  3865514 |  439349     457     8708    19.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 98900[0m
c ---[   0]---> Sorter-cost:   62     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 |       526 | 1318142  3865741 |  439380     457     8708    19.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 98454[0m
c ---[   0]---> Sorter-cost:  106     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 |       527 | 1318341  3866212 |  439447     458     8720    19.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 96804[0m
c ---[   0]---> Sorter-cost:   87     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 |       527 | 1318508  3866605 |  439502     458     8720    19.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 95270[0m
c ---[   0]---> Sorter-cost:   86     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 |       529 | 1318666  3866976 |  439555     460     8736    19.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 95268[0m
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 |       530 | 1318726  3867119 |  439575     461     8738    19.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 95264[0m
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 |       530 | 1318830  3867364 |  439610     461     8738    19.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 95236[0m
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 |       530 | 1318944  3867631 |  439648     461     8738    19.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 95234[0m
c ---[   0]---> Sorter-cost:   85     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 |       531 | 1319097  3867988 |  439699     462     8740    18.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 95232[0m
c ---[   0]---> Sorter-cost:   26     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 |       531 | 1319137  3868084 |  439712     462     8740    18.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 94710[0m
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 |       531 | 1319235  3868319 |  439745     462     8740    18.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 94708[0m
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 |       534 | 1319334  3868556 |  439778     465     8746    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 94214[0m
c ---[   0]---> Sorter-cost:   67     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 |       535 | 1319451  3868830 |  439817     466     8750    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 94212[0m
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 |       535 | 1319503  3868954 |  439834     466     8750    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 94210[0m
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 |       535 | 1319555  3869078 |  439851     466     8750    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 94208[0m
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 |       535 | 1319580  3869139 |  439860     466     8750    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 93572[0m
c ---[   0]---> Sorter-cost:   44     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 |       535 | 1319658  3869324 |  439886     466     8750    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 93570[0m
c ---[   0]---> Sorter-cost:   44     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 |       535 | 1319737  3869511 |  439912     466     8750    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 93568[0m
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 |       535 | 1319806  3869675 |  439935     466     8750    18.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 92164[0m
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 |       594 | 1319848  3869775 |  439949     525     9946    18.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 92162[0m
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 |       678 | 1319890  3869875 |  439963     609    12092    19.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 92160[0m
c ---[   0]---> Sorter-cost:   22     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 |       689 | 1319924  3869956 |  439974     620    12431    20.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 91142[0m
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 |       689 | 1319983  3870094 |  439994     620    12431    20.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 91140[0m
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 |       690 | 1320016  3870173 |  440005     621    12462    20.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 91138[0m
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 |       690 | 1320049  3870252 |  440016     621    12462    20.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 91136[0m
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 |       692 | 1320082  3870331 |  440027     623    12501    20.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90884[0m
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 |       726 | 1320156  3870506 |  440052     657    13356    20.3 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90882[0m
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 |       767 | 1320230  3870681 |  440076     698    14436    20.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90880[0m
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 |       768 | 1320298  3870841 |  440099     699    14440    20.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90758[0m
c ---[   0]---> Sorter-cost:   50     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 |       768 | 1320388  3871052 |  440129     699    14440    20.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90756[0m
c ---[   0]---> Sorter-cost:   46     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 |       768 | 1320469  3871243 |  440156     699    14440    20.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90754[0m
c ---[   0]---> Sorter-cost:   46     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 |       768 | 1320550  3871434 |  440183     699    14440    20.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90752[0m
c ---[   0]---> Sorter-cost:   46     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 |       768 | 1320630  3871622 |  440210     699    14440    20.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90626[0m
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 |       771 | 1320698  3871782 |  440232     702    14453    20.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90370[0m
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 |       773 | 1320771  3871954 |  440257     704    14497    20.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90368[0m
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 |       774 | 1320843  3872123 |  440281     705    14504    20.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90246[0m
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 |       812 | 1320915  3872292 |  440305     743    15138    20.4 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90118[0m
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 |       853 | 1320948  3872371 |  440316     784    16156    20.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 90114[0m
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 |       882 | 1320981  3872450 |  440327     813    16938    20.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 89606[0m
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 |       926 | 1321042  3872596 |  440347     857    17500    20.4 |  0.010 % |
c ==============================================================================
c [1mFound solution: 88066[0m
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 |       963 | 1321076  3872677 |  440358     894    18026    20.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 88064[0m
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 |       990 | 1321112  3872762 |  440370     921    18489    20.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 87044[0m
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 |      1026 | 1321140  3872829 |  440380     957    19300    20.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 87040[0m
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 |      1061 | 1321168  3872896 |  440389     992    19987    20.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 86660[0m
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 |      1074 | 1321205  3872983 |  440401    1005    20415    20.3 |  0.010 % |
c ==============================================================================
c [1mFound solution: 86658[0m
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 |      1096 | 1321242  3873070 |  440414    1027    21102    20.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 86148[0m
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 |      1122 | 1321316  3873243 |  440438    1053    21620    20.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 86146[0m
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 |      1136 | 1321390  3873416 |  440463    1067    21864    20.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 86144[0m
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 |      1146 | 1321464  3873589 |  440488    1077    22101    20.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 85378[0m
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 |      1166 | 1321491  3873653 |  440497    1097    22509    20.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 85126[0m
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 |      1180 | 1321546  3873783 |  440515    1111    22896    20.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 83076[0m
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 |      1191 | 1321608  3873928 |  440536    1122    23099    20.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 83074[0m
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 |      1197 | 1321670  3874073 |  440556    1128    23235    20.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 83072[0m
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 |      1216 | 1321732  3874218 |  440577    1147    23880    20.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 82948[0m
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 |      1233 | 1321759  3874282 |  440586    1164    24195    20.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 79618[0m
c ---[   0]---> Sorter-cost:   34     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 |      1253 | 1321818  3874422 |  440606    1184    24795    20.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 79366[0m
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 |      1262 | 1321865  3874535 |  440621    1193    24944    20.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 78978[0m
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 |      1279 | 1321899  3874616 |  440633    1210    25387    21.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 75398[0m
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 |      1297 | 1321959  3874757 |  440653    1228    25887    21.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 75396[0m
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 |      1308 | 1322019  3874898 |  440673    1239    26231    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 75394[0m
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 |      1315 | 1322079  3875039 |  440693    1246    26394    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 75392[0m
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 |      1317 | 1322139  3875180 |  440713    1248    26452    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 75010[0m
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 |      1329 | 1322201  3875325 |  440733    1260    26684    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 74756[0m
c ---[   0]---> Sorter-cost:   13     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 |      1345 | 1322221  3875373 |  440740    1276    27105    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 74754[0m
c ---[   0]---> Sorter-cost:   13     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 |      1390 | 1322241  3875421 |  440747    1321    28044    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 74372[0m
c ---[   0]---> Sorter-cost:   13     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 |      1414 | 1322261  3875469 |  440753    1345    28364    21.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 73728[0m
c ---[   0]---> Sorter-cost:   14     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 |      1429 | 1322281  3875516 |  440760    1360    28786    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 72962[0m
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 |      1448 | 1322326  3875623 |  440775    1379    29154    21.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 72834[0m
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 |      1459 | 1322371  3875730 |  440790    1390    29284    21.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 71808[0m
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 |      1474 | 1322418  3875841 |  440806    1405    29729    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 71680[0m
c ---[   0]---> Sorter-cost:   13     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 |      1491 | 1322437  3875886 |  440812    1422    30248    21.3 |  0.010 % |
c ==============================================================================
c [1mFound solution: 71172[0m
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 |      1501 | 1322505  3876046 |  440835    1432    30414    21.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 69636[0m
c ---[   0]---> Sorter-cost:   20     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 |      1508 | 1322538  3876124 |  440846    1439    30644    21.3 |  0.010 % |
c ==============================================================================
c [1mFound solution: 69634[0m
c ---[   0]---> Sorter-cost:   20     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 |      1532 | 1322571  3876202 |  440857    1463    31425    21.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 69632[0m
c ---[   0]---> Sorter-cost:   20     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 |      1543 | 1322603  3876277 |  440867    1474    31720    21.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 68484[0m
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 |      1558 | 1322676  3876448 |  440892    1489    32087    21.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 67076[0m
c ---[   0]---> Sorter-cost:   27     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 |      1573 | 1322721  3876553 |  440907    1504    32461    21.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 65406[0m
c ---[   0]---> Sorter-cost:  158     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1590 | 1321926  3874479 |  440642    1210    21560    17.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 64382[0m
c ---[   0]---> Sorter-cost:  131     Base: 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1603 | 1322174  3875070 |  440724    1223    21878    17.9 |  0.010 % |
c ==============================================================================
c [1mFound solution: 63678[0m
c ---[   0]---> Sorter-cost:  124     Base: 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1617 | 1322396  3875603 |  440798    1237    22298    18.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 63280[0m
c ---[   0]---> Sorter-cost:  224     Base: 2 2 2 2 2 2 7 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1624 | 1322797  3876554 |  440932    1244    22395    18.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 63248[0m
c ---[   0]---> Sorter-cost:  242     Base: 2 2 2 2 2 2 7 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1631 | 1323247  3877617 |  441082    1251    22531    18.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 62960[0m
c ---[   0]---> Sorter-cost:   56     Base: 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1637 | 1323321  3877799 |  441107    1257    22601    18.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 62768[0m
c ---[   0]---> Sorter-cost:  143     Base: 2 2 2 2 2 2 2 7 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1639 | 1323568  3878383 |  441189    1259    22648    18.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 62000[0m
c ---[   0]---> Sorter-cost:  169     Base: 2 2 2 2 2 2 5 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1652 | 1323799  3878937 |  441266    1272    22883    18.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 61808[0m
c ---[   0]---> Sorter-cost:  105     Base: 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1679 | 1323983  3879373 |  441327    1299    23392    18.0 |  0.010 % |
c ==============================================================================
c [1mFound solution: 61744[0m
c ---[   0]---> Sorter-cost:  122     Base: 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1686 | 1324207  3879902 |  441402    1306    23620    18.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 49072[0m
c ---[   0]---> Sorter-cost:   46     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 |      1690 | 1324279  3880077 |  441426    1310    23773    18.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 48368[0m
c ---[   0]---> Sorter-cost:   44     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 |      1693 | 1324350  3880248 |  441450    1313    23794    18.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 48304[0m
c ---[   0]---> Sorter-cost:   36     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 |      1694 | 1324409  3880390 |  441469    1314    23810    18.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 48272[0m
c ---[   0]---> Sorter-cost:   54     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 |      1694 | 1324501  3880608 |  441500    1314    23810    18.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 48256[0m
c ---[   0]---> Sorter-cost:   37     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 |      1694 | 1324560  3880749 |  441520    1314    23810    18.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 47408[0m
c ---[   0]---> Sorter-cost:   43     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 |      1698 | 1324633  3880922 |  441544    1318    23946    18.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 47026[0m
c ---[   0]---> Sorter-cost:   67     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 |      1712 | 1324746  3881191 |  441582    1332    24134    18.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 31744[0m
c ---[   0]---> Sorter-cost:    9     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 |      1718 | 1323525  3878146 |  441175    1209    20232    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 31464[0m
c ---[   0]---> Sorter-cost:  128     Base: 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1733 | 1323773  3878732 |  441257    1224    20446    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 31456[0m
c ---[   0]---> Sorter-cost:   77     Base: 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1740 | 1323898  3879031 |  441299    1231    20593    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 31440[0m
c ---[   0]---> Sorter-cost:  108     Base: 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1741 | 1324092  3879490 |  441364    1232    20652    16.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 31240[0m
c ---[   0]---> Sorter-cost:  278     Base: 2 2 2 2 5 3 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1751 | 1324685  3880887 |  441561    1242    20816    16.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 31232[0m
c ---[   0]---> Sorter-cost:   13     Base: 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 |      1758 | 1324690  3880901 |  441563    1249    20898    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 30992[0m
c ---[   0]---> Sorter-cost:  118     Base: 2 2 2 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1775 | 1324912  3881429 |  441637    1266    21130    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 30984[0m
c ---[   0]---> Sorter-cost:  237     Base: 2 2 2 2 2 5 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1783 | 1325322  3882404 |  441774    1274    21276    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 22482[0m
c ---[   0]---> Sorter-cost:   73     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 |      1787 | 1325457  3882724 |  441819    1278    21347    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 22418[0m
c ---[   0]---> Sorter-cost:   42     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 |      1795 | 1325529  3882896 |  441843    1286    21439    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 22290[0m
c ---[   0]---> Sorter-cost:   38     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 |      1800 | 1325595  3883053 |  441865    1291    21472    16.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 21842[0m
c ---[   0]---> Sorter-cost:   41     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 |      1808 | 1325671  3883232 |  441890    1299    21691    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 21778[0m
c ---[   0]---> Sorter-cost:   28     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 |      1819 | 1325720  3883348 |  441906    1310    21816    16.7 |  0.010 % |
c ==============================================================================
c [1mFound solution: 21714[0m
c ---[   0]---> Sorter-cost:   37     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 |      1833 | 1325788  3883508 |  441929    1324    22075    16.7 |  0.010 % |
c |      1933 | 1325788  3883508 |  486121    1424    27875    19.6 |  0.295 % |
c ==============================================================================
c [1mFound solution: 21586[0m
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 |      1952 | 1325849  3883651 |  441949    1443    28262    19.6 |  0.295 % |
c ==============================================================================
c [1mFound solution: 21034[0m
c ---[   0]---> Sorter-cost:   68     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 |      1964 | 1325979  3883954 |  441993    1455    28408    19.5 |  0.295 % |
c ==============================================================================
c [1mFound solution: 20754[0m
c ---[   0]---> Sorter-cost:   24     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 |      1968 | 1326019  3884048 |  442006    1459    28528    19.6 |  0.295 % |
c ==============================================================================
c [1mFound solution: 15830[0m
c ---[   0]---> Sorter-cost:  157     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 |      1980 | 1324744  3880736 |  441581    1426    28088    19.7 |  0.295 % |
c ==============================================================================
c [1mFound solution: 15766[0m
c ---[   0]---> Sorter-cost:  100     Base: 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2066 | 1324925  3881167 |  441641    1512    31281    20.7 |  0.295 % |
c ==============================================================================
c [1mFound solution: 14760[0m
c ---[   0]---> Sorter-cost:  102     Base: 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 |      2072 | 1325126  3881640 |  441708    1518    31379    20.7 |  0.295 % |
c ==============================================================================
c [1mFound solution: 13952[0m
c ---[   0]---> Sorter-cost:   43     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 |      2081 | 1325204  3881825 |  441734    1527    31572    20.7 |  0.295 % |
c ==============================================================================
c [1mFound solution: 13920[0m
c ---[   0]---> Sorter-cost:   66     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 |      2093 | 1325331  3882125 |  441777    1539    31856    20.7 |  0.295 % |
c ==============================================================================
c [1mFound solution: 13704[0m
c ---[   0]---> Sorter-cost:  108     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 |      2148 | 1325558  3882657 |  441852    1594    33944    21.3 |  0.295 % |
c ==============================================================================
c [1mFound solution: 13224[0m
c ---[   0]---> Sorter-cost:   56     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 |      2183 | 1325659  3882898 |  441886    1629    35606    21.9 |  0.295 % |
c ==============================================================================
c [1mFound solution: 13218[0m
c ---[   0]---> Sorter-cost:  120     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 |      2267 | 1325907  3883481 |  441969    1713    38851    22.7 |  0.295 % |
c ==============================================================================
c [1mFound solution: 13098[0m
c ---[   0]---> Sorter-cost:   94     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 |      2286 | 1326096  3883926 |  442032    1732    39433    22.8 |  0.295 % |
c |      2386 | 1326096  3883926 |  486235    1832    45443    24.8 |  0.378 % |
c |      2536 | 1326096  3883926 |  534858    1982    53071    26.8 |  0.378 % |
c ==============================================================================
c [1mFound solution: 12930[0m
c ---[   0]---> Sorter-cost:   90     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 |      2539 | 1326282  3884363 |  442094    1985    53106    26.8 |  0.378 % |
c ==============================================================================
c [1mFound solution: 12928[0m
c ---[   0]---> Sorter-cost:   18     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 |      2540 | 1326308  3884428 |  442102    1986    53156    26.8 |  0.378 % |
c ==============================================================================
c [1mFound solution: 12800[0m
c ---[   0]---> Sorter-cost:   24     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 |      2627 | 1326344  3884515 |  442114    2073    55973    27.0 |  0.378 % |
c ==============================================================================
c [1mFound solution: 12682[0m
c ---[   0]---> Sorter-cost:   95     Base: 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2718 | 1326506  3884900 |  442168    2164    59094    27.3 |  0.378 % |
c |      2818 | 1326506  3884900 |  486384    2264    63044    27.8 |  0.379 % |
c ==============================================================================
c [1mFound solution: 12560[0m
c ---[   0]---> Sorter-cost:  109     Base: 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2870 | 1326700  3885358 |  442233    2316    64846    28.0 |  0.379 % |
c |      2970 | 1326700  3885358 |  486456    2416    68663    28.4 |  0.379 % |
c |      3120 | 1326700  3885358 |  535101    2566    74363    29.0 |  0.379 % |
c ==============================================================================
c [1mFound solution: 12544[0m
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3262 | 1326751  3885483 |  442250    2708    79036    29.2 |  0.379 % |
c |      3362 | 1326751  3885483 |  486475    2808    83351    29.7 |  0.379 % |
c |      3514 | 1326751  3885483 |  535122    2960    89476    30.2 |  0.379 % |
c |      3740 | 1326751  3885483 |  588634    3186    98465    30.9 |  0.379 % |
c |      4078 | 1326751  3885483 |  647498    3524   110682    31.4 |  0.379 % |
c ==============================================================================
c [1mFound solution: 12416[0m
c ---[   0]---> Sorter-cost:   55     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 |      4256 | 1326830  3885675 |  442276    3702   116683    31.5 |  0.379 % |
c ==============================================================================
c [1mFound solution: 12392[0m
c ---[   0]---> Sorter-cost:   78     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 |      4259 | 1326958  3885981 |  442319    3705   116708    31.5 |  0.379 % |
c ==============================================================================
c [1mFound solution: 12290[0m
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 |      4260 | 1327102  3886324 |  442367    3706   116712    31.5 |  0.379 % |
c ==============================================================================
c [1mFound solution: 12288[0m
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 |      4261 | 1327103  3886327 |  442367    3707   116716    31.5 |  0.379 % |
c |      4361 | 1327103  3886327 |  486603    3807   121547    31.9 |  0.380 % |
c ==============================================================================
c [1mFound solution: 12122[0m
c ---[   0]---> Sorter-cost:   64     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 |      4384 | 1327219  3886603 |  442406    3830   123645    32.3 |  0.380 % |
c |      4484 | 1327219  3886603 |  486646    3930   131187    33.4 |  0.380 % |
c |      4634 | 1327219  3886603 |  535311    4080   138996    34.1 |  0.380 % |
c |      4860 | 1327219  3886603 |  588842    4306   150030    34.8 |  0.380 % |
c |      5197 | 1327219  3886603 |  647726    4643   166071    35.8 |  0.380 % |
c |      5703 | 1327219  3886603 |  712499    5149   196403    38.1 |  0.380 % |
c ==============================================================================
c [1mFound solution: 12120[0m
c ---[   0]---> Sorter-cost:   47     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 |      5738 | 1327298  3886792 |  442432    5184   199210    38.4 |  0.380 % |
c ==============================================================================
c [1mFound solution: 11952[0m
c ---[   0]---> Sorter-cost:   47     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 |      5756 | 1327383  3886994 |  442461    5202   200381    38.5 |  0.380 % |
c |      5856 | 1327383  3886994 |  486707    5302   204813    38.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11946[0m
c ---[   0]---> Sorter-cost:   47     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 |      5899 | 1327467  3887193 |  442489    5345   206871    38.7 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11926[0m
c ---[   0]---> Sorter-cost:   58     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 |      5912 | 1327572  3887440 |  442524    5358   207336    38.7 |  0.381 % |
c |      6012 | 1327572  3887440 |  486776    5458   213986    39.2 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11842[0m
c ---[   0]---> Sorter-cost:   57     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 |      6092 | 1327671  3887673 |  442557    5538   217693    39.3 |  0.381 % |
c |      6192 | 1327671  3887673 |  486812    5638   222540    39.5 |  0.381 % |
c |      6342 | 1327671  3887673 |  535493    5788   232090    40.1 |  0.381 % |
c |      6567 | 1327671  3887673 |  589043    6013   246123    40.9 |  0.381 % |
c |      6904 | 1327671  3887673 |  647947    6350   269378    42.4 |  0.381 % |
c |      7411 | 1327671  3887673 |  712742    6857   296199    43.2 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11768[0m
c ---[   0]---> Sorter-cost:   39     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 |      7646 | 1327735  3887828 |  442578    7092   309239    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11720[0m
c ---[   0]---> Sorter-cost:   47     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 |      7648 | 1327814  3888016 |  442604    7094   309299    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11672[0m
c ---[   0]---> Sorter-cost:   36     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 |      7648 | 1327874  3888159 |  442624    7094   309299    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11658[0m
c ---[   0]---> Sorter-cost:   43     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 |      7648 | 1327947  3888332 |  442649    7094   309299    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11652[0m
c ---[   0]---> Sorter-cost:   58     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 |      7648 | 1328047  3888567 |  442682    7094   309299    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 11648[0m
c ---[   0]---> Sorter-cost:   26     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 |      7648 | 1328089  3888667 |  442696    7094   309299    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 10384[0m
c ---[   0]---> Sorter-cost:   51     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 |      7658 | 1328182  3888884 |  442727    7104   309585    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 10378[0m
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 |      7659 | 1328236  3889011 |  442745    7105   309614    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 10376[0m
c ---[   0]---> Sorter-cost:   42     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 |      7659 | 1328310  3889184 |  442770    7105   309614    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 10370[0m
c ---[   0]---> Sorter-cost:   42     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 |      7659 | 1328384  3889357 |  442794    7105   309614    43.6 |  0.381 % |
c ==============================================================================
c [1mFound solution: 10368[0m
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 |      7659 | 1328437  3889481 |  442812    7105   309614    43.6 |  0.381 % |
c |      7760 | 1328437  3889481 |  487093    7206   313329    43.5 |  0.383 % |
c ==============================================================================
c [1mFound solution: 10258[0m
c ---[   0]---> Sorter-cost:   56     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 |      7823 | 1328538  3889716 |  442846    7269   316276    43.5 |  0.383 % |
c |      7923 | 1328538  3889716 |  487130    7369   320534    43.5 |  0.383 % |
c |      8073 | 1328538  3889716 |  535843    7519   335818    44.7 |  0.383 % |
c |      8298 | 1328538  3889716 |  589428    7744   344578    44.5 |  0.383 % |
c |      8635 | 1328538  3889716 |  648370    8081   358616    44.4 |  0.383 % |
c ==============================================================================
c [1mFound solution: 10248[0m
c ---[   0]---> Sorter-cost:   38     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 |      8807 | 1328604  3889870 |  442868    8253   364671    44.2 |  0.383 % |
c |      8907 | 1328604  3889870 |  487154    8353   369039    44.2 |  0.384 % |
c |      9057 | 1328604  3889870 |  535870    8503   375291    44.1 |  0.384 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 29262 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.91 0.95 0.90 2/54 29258
Raw data (stat): 29258 (runsolver) R 29257 1586 1585 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855033440 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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+9.99971 s]
Raw data (loadavg): 0.92 0.95 0.90 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0003 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0005 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0012 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.73 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 29262
Raw data (stat): 29258 (minisat+_script) S 29257 1586 1585 0 -1 0 275 239 0 0 0 1 0 0 19 0 1 0 855033440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.73
CPU time (s): 1229.91
CPU user time (s): 1228.75
CPU system time (s): 1.16382
CPU usage (%): 100.015
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####