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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare2.opb
MD5SUM	111dddb6adf389a5275ab413feff6076
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	429056
Optimality of the best value was proved	NO
Number of terms in the objective function	210
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	7516192761
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	7516192761
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1201.36
Number of variables	270
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	90
Trace number 21284

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 23:17:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13530 boxname=wulflinc30 idbench=1041 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  111dddb6adf389a5275ab413feff6076  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-markshare2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-markshare2.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-markshare2.opb
IDLAUNCH: 13530
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        636732 kB
Buffers:         27648 kB
Cached:         343468 kB
SwapCached:         28 kB
Active:         186500 kB
Inactive:       187412 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        636480 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18384 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:37:17 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 13530 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 3452927   bits: 23/22
c ---[  10]---> Adder-cost: 380   maxlim: 3689471   bits: 23/22
c ---[   8]---> Adder-cost: 350   maxlim: 3561471   bits: 23/22
c ---[   6]---> Adder-cost: 340   maxlim: 3823615   bits: 23/22
c ---[   4]---> Adder-cost: 390   maxlim: 3614719   bits: 23/22
c ---[   2]---> Adder-cost: 358   maxlim: 3749887   bits: 23/22
c ---[   0]---> Adder-cost: 374   maxlim: 3556351   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17214    61202 |    6314      99      310     3.1 | 12.761 % |
c ==============================================================================
c [1mFound solution: 9929728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 132   maxlim: 4632   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       170 |   18089    64333 |    6029     169      862     5.1 | 12.761 % |
c |       270 |   18089    64333 |    6631     269     1662     6.2 | 12.359 % |
c |       420 |   18089    64333 |    7295     419     3064     7.3 | 12.359 % |
c ==============================================================================
c [1mFound solution: 9165824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5378   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       424 |   18103    64412 |    6034     423     3089     7.3 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8893440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5644   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       505 |   18103    64446 |    6034     503     8679    17.3 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8585216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5945   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       521 |   18112    64516 |    6037     519     9447    18.2 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8474624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6053   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       545 |   18120    64577 |    6040     543    11107    20.5 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8449024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6078   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       592 |   18127    64646 |    6042     590    15887    26.9 | 12.359 % |
c |       692 |   18127    64646 |    6646     690    27246    39.5 | 12.999 % |
c ==============================================================================
c [1mFound solution: 8186880[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6334   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       768 |   18143    64748 |    6047     766    36704    47.9 | 12.999 % |
c ==============================================================================
c [1mFound solution: 6665216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7820   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       770 |   18152    64813 |    6050     768    36712    47.8 | 12.999 % |
c ==============================================================================
c [1mFound solution: 6627328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7857   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       773 |   18158    64851 |    6052     771    36893    47.9 | 12.999 % |
c ==============================================================================
c [1mFound solution: 6550528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7932   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       786 |   18171    64943 |    6057     784    37273    47.5 | 12.999 % |
c |       887 |   18171    64943 |    6662     885    47503    53.7 | 13.569 % |
c |      1037 |   18171    64943 |    7328    1035    61402    59.3 | 13.569 % |
c |      1263 |   18171    64943 |    8061    1261    84278    66.8 | 13.569 % |
c |      1603 |   18171    64943 |    8868    1601   136610    85.3 | 13.569 % |
c ==============================================================================
c [1mFound solution: 6333440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8144   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1667 |   18179    64999 |    6059    1665   137841    82.8 | 13.569 % |
c ==============================================================================
c [1mFound solution: 6005760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8464   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1759 |   18129    64485 |    6043    1757   141693    80.6 | 13.569 % |
c |      1859 |   18129    64485 |    6647    1857   145772    78.5 | 13.796 % |
c ==============================================================================
c [1mFound solution: 5316608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9137   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1929 |   18140    64541 |    6046    1927   153114    79.5 | 13.796 % |
c |      2029 |   18140    64541 |    6650    2027   165895    81.8 | 13.937 % |
c |      2179 |   18140    64541 |    7315    2177   182794    84.0 | 13.937 % |
c |      2404 |   18132    64515 |    8047    2401   203350    84.7 | 13.968 % |
c |      2741 |   18132    64515 |    8851    2738   229940    84.0 | 13.968 % |
c ==============================================================================
c [1mFound solution: 4519936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9915   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2958 |   18137    64547 |    6045    2954   245650    83.2 | 13.968 % |
c |      3059 |   18137    64547 |    6649    3055   251248    82.2 | 14.161 % |
c |      3209 |   18137    64547 |    7314    3205   267630    83.5 | 14.161 % |
c |      3435 |   18137    64547 |    8045    3431   294515    85.8 | 14.161 % |
c |      3775 |   18137    64547 |    8850    3771   332410    88.1 | 14.161 % |
c |      4281 |   18137    64547 |    9735    4277   389277    91.0 | 14.161 % |
c |      5040 |   18137    64547 |   10709    5036   475777    94.5 | 14.161 % |
c |      6179 |   18129    64521 |   11779    6174   614893    99.6 | 14.192 % |
c |      7888 |   18121    64495 |   12957    7882   799962   101.5 | 14.223 % |
c |     10450 |   18113    64469 |   14253   10443  1027905    98.4 | 14.255 % |
c |     14294 |   18113    64469 |   15679   14287  1327207    92.9 | 14.255 % |
c ==============================================================================
c [1mFound solution: 4205568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10222   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18031 |   18128    64560 |    6042    9476   707727    74.7 | 14.255 % |
c |     18135 |   18128    64560 |    6646    4842   330421    68.2 | 14.437 % |
c |     18286 |   18128    64560 |    7310    4993   346139    69.3 | 14.437 % |
c |     18512 |   18128    64560 |    8041    5219   363036    69.6 | 14.437 % |
c |     18850 |   18128    64560 |    8846    5557   391760    70.5 | 14.437 % |
c |     19358 |   18128    64560 |    9730    6065   429329    70.8 | 14.437 % |
c |     20117 |   18128    64560 |   10703    6824   501738    73.5 | 14.437 % |
c |     21257 |   18128    64560 |   11774    7964   631096    79.2 | 14.437 % |
c ==============================================================================
c [1mFound solution: 4191232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10236   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22852 |   18128    64584 |    6042    9558   839302    87.8 | 14.437 % |
c ==============================================================================
c [1mFound solution: 3969024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10453   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22951 |   18132    64627 |    6044    4877   436723    89.5 | 14.437 % |
c |     23051 |   18132    64627 |    6648    4977   446395    89.7 | 14.727 % |
c |     23201 |   18132    64627 |    7313    5127   463974    90.5 | 14.727 % |
c |     23426 |   18132    64627 |    8044    5352   488628    91.3 | 14.727 % |
c |     23764 |   18132    64627 |    8849    5690   527568    92.7 | 14.727 % |
c |     24271 |   18107    64544 |    9733    6194   608379    98.2 | 14.819 % |
c |     25030 |   18093    64500 |   10707    6951   683416    98.3 | 14.881 % |
c |     26171 |   18093    64500 |   11778    8092   804242    99.4 | 14.881 % |
c |     27880 |   18093    64500 |   12955    9801   952250    97.2 | 14.881 % |
c |     30442 |   18093    64500 |   14251   12363  1198119    96.9 | 14.881 % |
c |     34287 |   18077    64448 |   15676    8299   742579    89.5 | 14.943 % |
c |     40053 |   18077    64448 |   17244   14065  1280515    91.0 | 14.943 % |
c |     48702 |   18077    64448 |   18968   13371  1140331    85.3 | 14.943 % |
c |     61677 |   18069    64422 |   20865   16116  1649597   102.4 | 14.974 % |
c |     81140 |   18069    64422 |   22952   13399   899255    67.1 | 14.974 % |
c ==============================================================================
c [1mFound solution: 3134464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11268   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82211 |   18074    64456 |    6024   14470  1003543    69.4 | 14.974 % |
c |     82312 |   18074    64456 |    6626    3719   180113    48.4 | 15.043 % |
c |     82463 |   18074    64456 |    7289    3870   182902    47.3 | 15.043 % |
c |     82689 |   18074    64456 |    8017    4096   195175    47.7 | 15.043 % |
c |     83026 |   18074    64456 |    8819    4433   232223    52.4 | 15.043 % |
c |     83533 |   18066    64430 |    9701    4939   261484    52.9 | 15.074 % |
c |     84293 |   18066    64430 |   10671    5699   315475    55.4 | 15.074 % |
c |     85433 |   18066    64430 |   11739    6839   408332    59.7 | 15.074 % |
c |     87141 |   18058    64404 |   12912    8546   505534    59.2 | 15.105 % |
c ==============================================================================
c [1mFound solution: 3055616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11345   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87258 |   18063    64438 |    6021    8663   506965    58.5 | 15.105 % |
c |     87358 |   18063    64438 |    6623    4432   199222    45.0 | 15.174 % |
c |     87508 |   18063    64438 |    7285    4582   202942    44.3 | 15.174 % |
c |     87733 |   18063    64438 |    8013    4807   220980    46.0 | 15.174 % |
c |     88070 |   18063    64438 |    8815    5144   231440    45.0 | 15.174 % |
c |     88576 |   18063    64438 |    9696    5650   251621    44.5 | 15.174 % |
c |     89336 |   18063    64438 |   10666    6410   304672    47.5 | 15.174 % |
c |     90475 |   18063    64438 |   11733    7549   440866    58.4 | 15.174 % |
c ==============================================================================
c [1mFound solution: 2900992[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11496   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90775 |   18073    64494 |    6024    7849   449484    57.3 | 15.174 % |
c ==============================================================================
c [1mFound solution: 2862080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11534   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90869 |   18083    64552 |    6027    4019   218812    54.4 | 15.174 % |
c ==============================================================================
c [1mFound solution: 2467840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11919   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90902 |   18089    64578 |    6029    4052   220365    54.4 | 15.174 % |
c |     91002 |   18089    64578 |    6631    4152   222408    53.6 | 15.450 % |
c |     91153 |   18089    64578 |    7295    4303   224818    52.2 | 15.450 % |
c |     91379 |   18081    64552 |    8024    4528   237701    52.5 | 15.481 % |
c |     91718 |   18081    64552 |    8827    4867   268324    55.1 | 15.481 % |
c |     92224 |   18081    64552 |    9709    5373   338705    63.0 | 15.481 % |
c |     92983 |   18081    64552 |   10680    6132   365305    59.6 | 15.481 % |
c |     94122 |   18081    64552 |   11748    7271   496447    68.3 | 15.481 % |
c |     95830 |   18081    64552 |   12923    8979   588261    65.5 | 15.481 % |
c |     98392 |   18081    64552 |   14216   11541   868525    75.3 | 15.481 % |
c ==============================================================================
c [1mFound solution: 2396160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11989   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100976 |   18089    64599 |    6029   14125   984272    69.7 | 15.481 % |
c |    101077 |   18089    64599 |    6631    3633   110800    30.5 | 15.565 % |
c |    101230 |   18089    64599 |    7295    3786   119102    31.5 | 15.565 % |
c |    101455 |   18083    64579 |    8024    4010   141048    35.2 | 15.596 % |
c |    101792 |   18083    64579 |    8827    4347   148021    34.1 | 15.596 % |
c |    102298 |   18083    64579 |    9709    4853   171678    35.4 | 15.596 % |
c ==============================================================================
c [1mFound solution: 2342912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12041   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102499 |   18089    64611 |    6029    5054   182823    36.2 | 15.596 % |
c |    102599 |   18089    64611 |    6631    5154   191623    37.2 | 15.658 % |
c |    102750 |   18089    64611 |    7295    5305   201586    38.0 | 15.658 % |
c |    102976 |   18089    64611 |    8024    5531   212618    38.4 | 15.658 % |
c |    103313 |   18089    64611 |    8827    5868   230337    39.3 | 15.658 % |
c |    103819 |   18089    64611 |    9709    6374   273398    42.9 | 15.658 % |
c |    104579 |   18089    64611 |   10680    7134   351701    49.3 | 15.658 % |
c |    105719 |   18089    64611 |   11748    8274   470020    56.8 | 15.658 % |
c |    107428 |   18089    64611 |   12923    9983   608905    61.0 | 15.658 % |
c |    109990 |   18089    64611 |   14216   12545   914049    72.9 | 15.658 % |
c ==============================================================================
c [1mFound solution: 2283520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12099   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111605 |   18092    64632 |    6030   14160   986206    69.6 | 15.658 % |
c ==============================================================================
c [1mFound solution: 2247680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12134   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111651 |   18099    64684 |    6033    3586   126357    35.2 | 15.658 % |
c |    111752 |   18099    64684 |    6636    3687   128317    34.8 | 15.793 % |
c |    111902 |   18099    64684 |    7299    3837   129649    33.8 | 15.793 % |
c ==============================================================================
c [1mFound solution: 2119680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12259   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111915 |   18107    64720 |    6035    3850   129743    33.7 | 15.793 % |
c |    112015 |   18107    64720 |    6638    3950   144109    36.5 | 15.875 % |
c |    112165 |   18107    64720 |    7302    4100   155401    37.9 | 15.875 % |
c |    112390 |   18107    64720 |    8032    4325   162996    37.7 | 15.875 % |
c |    112727 |   18107    64720 |    8835    4662   189457    40.6 | 15.875 % |
c |    113233 |   18107    64720 |    9719    5168   223351    43.2 | 15.875 % |
c |    113993 |   18107    64720 |   10691    5928   274773    46.4 | 15.875 % |
c |    115132 |   18107    64720 |   11760    7067   336663    47.6 | 15.875 % |
c |    116840 |   18107    64720 |   12936    8775   501739    57.2 | 15.875 % |
c |    119403 |   18107    64720 |   14230   11338   727363    64.2 | 15.875 % |
c |    123251 |   18107    64720 |   15653   15186   964162    63.5 | 15.875 % |
c |    129017 |   18107    64720 |   17218   12522   731878    58.4 | 15.875 % |
c |    137666 |   18101    64702 |   18940   11812   658368    55.7 | 15.906 % |
c |    150642 |   18092    64675 |   20834   14699  1106394    75.3 | 15.966 % |
c |    170105 |   18083    64648 |   22917   11849   629813    53.2 | 16.027 % |
c ==============================================================================
c [1mFound solution: 794624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 6385   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    170767 |   18028    64457 |    6009   12489   640194    51.3 | 16.027 % |
c |    170869 |   18028    64457 |    6609    6347   254917    40.2 | 16.546 % |
c |    171020 |   18021    64434 |    7270    6497   258243    39.7 | 16.576 % |
c |    171245 |   17945    64175 |    7997    6146   200674    32.7 | 16.968 % |
c |    171582 |   17945    64175 |    8797    6483   204951    31.6 | 16.968 % |
c |    172088 |   17837    63514 |    9677    6985   214331    30.7 | 17.298 % |
c |    172850 |   17837    63514 |   10645    7747   254029    32.8 | 17.298 % |
c |    173990 |   17837    63514 |   11709    8887   308313    34.7 | 17.298 % |
c |    175699 |   17837    63514 |   12880   10596   367154    34.7 | 17.298 % |
c |    178261 |   17837    63514 |   14168   13158   489550    37.2 | 17.298 % |
c |    182107 |   17837    63514 |   15585    9196   331647    36.1 | 17.298 % |
c |    187873 |   17837    63514 |   17144   14962   596932    39.9 | 17.298 % |
c |    196523 |   17837    63514 |   18858   14503   674566    46.5 | 17.298 % |
c |    209498 |   17837    63514 |   20744   17603   718960    40.8 | 17.298 % |
c |    228959 |   17837    63514 |   22819   15439   827104    53.6 | 17.298 % |
c |    258152 |   17837    63514 |   25101   20843  1033958    49.6 | 17.298 % |
c |    301941 |   17837    63514 |   27611   25464  1404457    55.2 | 17.298 % |
c |    367627 |   17837    63514 |   30372   19056   831599    43.6 | 17.298 % |
c |    466153 |   17829    63488 |   33409   17635   800117    45.4 | 17.329 % |
c |    613943 |   17820    63461 |   36750   30799  1466980    47.6 | 17.389 % |
#### 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.60 0.90 0.89 2/54 32234
Raw data (stat): 32234 (runsolver) R 32233 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548971493 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.66 0.90 0.89 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 1224 0 0 0 995 2 0 0 25 0 1 0 548971493 6594560 1202 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1610 1202 603 41 0 1569 0
vsize: 6440
[startup+20.0012 s]
Raw data (loadavg): 0.71 0.90 0.89 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 1710 0 0 0 1994 4 0 0 25 0 1 0 548971493 8609792 1688 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2102 1688 603 41 0 2061 0
vsize: 8408
[startup+30.0024 s]
Raw data (loadavg): 0.76 0.91 0.89 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2078 0 0 0 2992 6 0 0 25 0 1 0 548971493 10207232 2056 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2492 2056 603 41 0 2451 0
vsize: 9968
[startup+40.0022 s]
Raw data (loadavg): 0.79 0.91 0.89 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2379 0 0 0 3990 8 0 0 25 0 1 0 548971493 11399168 2357 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2783 2357 603 41 0 2742 0
vsize: 11132
[startup+50.0026 s]
Raw data (loadavg): 0.82 0.91 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2499 0 0 0 4990 8 0 0 25 0 1 0 548971493 11988992 2477 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2477 603 41 0 2886 0
vsize: 11708
[startup+60.0029 s]
Raw data (loadavg): 0.85 0.91 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2502 0 0 0 5989 9 0 0 25 0 1 0 548971493 11988992 2480 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2480 603 41 0 2886 0
vsize: 11708
[startup+70.0036 s]
Raw data (loadavg): 0.87 0.92 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2502 0 0 0 6989 9 0 0 25 0 1 0 548971493 11988992 2480 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2480 603 41 0 2886 0
vsize: 11708
[startup+80.004 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2502 0 0 0 7989 9 0 0 25 0 1 0 548971493 11988992 2480 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2480 603 41 0 2886 0
vsize: 11708
[startup+90.0042 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2565 0 0 0 8989 10 0 0 25 0 1 0 548971493 12124160 2543 4294967295 134512640 134672761 3221224528 3221223712 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2960 2543 603 41 0 2919 0
vsize: 11840
[startup+100.005 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2565 0 0 0 9989 10 0 0 25 0 1 0 548971493 12124160 2543 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2960 2543 603 41 0 2919 0
vsize: 11840
[startup+110.005 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2684 0 0 0 10988 11 0 0 25 0 1 0 548971493 12652544 2662 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3089 2662 603 41 0 3048 0
vsize: 12356
[startup+120.007 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2739 0 0 0 11988 11 0 0 25 0 1 0 548971493 12918784 2717 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3154 2717 603 41 0 3113 0
vsize: 12616
[startup+130.007 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2739 0 0 0 12988 11 0 0 25 0 1 0 548971493 12918784 2717 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3154 2717 603 41 0 3113 0
vsize: 12616
[startup+140.008 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 2898 0 0 0 13988 11 0 0 25 0 1 0 548971493 13582336 2876 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3316 2876 603 41 0 3275 0
vsize: 13264
[startup+150.008 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3052 0 0 0 14987 12 0 0 25 0 1 0 548971493 14114816 3030 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3030 603 41 0 3405 0
vsize: 13784
[startup+160.008 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3052 0 0 0 15987 12 0 0 25 0 1 0 548971493 14114816 3030 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3030 603 41 0 3405 0
vsize: 13784
[startup+170.008 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3052 0 0 0 16987 12 0 0 25 0 1 0 548971493 14114816 3030 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3030 603 41 0 3405 0
vsize: 13784
[startup+180.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3206 0 0 0 17987 13 0 0 25 0 1 0 548971493 14782464 3184 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+190.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3206 0 0 0 18987 13 0 0 25 0 1 0 548971493 14782464 3184 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+200.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3206 0 0 0 19987 13 0 0 25 0 1 0 548971493 14782464 3184 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+210.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3206 0 0 0 20987 13 0 0 25 0 1 0 548971493 14782464 3184 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+220.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3206 0 0 0 21988 13 0 0 25 0 1 0 548971493 14782464 3184 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+230.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3206 0 0 0 22988 13 0 0 25 0 1 0 548971493 14782464 3184 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+240.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3206 0 0 0 23988 13 0 0 25 0 1 0 548971493 14782464 3184 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+250.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3207 0 0 0 24988 13 0 0 25 0 1 0 548971493 14782464 3185 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3185 603 41 0 3568 0
vsize: 14436
[startup+260.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 25988 13 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+270.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 26988 13 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+280.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 27988 13 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+290.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 28988 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+300.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 29988 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+310.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 30988 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+320.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 31989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+330.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 32989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223632 134559818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+340.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 33989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223712 134559599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+350.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 34989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+360.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 35989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+370.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 36989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+380.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 37989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223632 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+390.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 38989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+400.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 39989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+410.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 40989 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+420.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 41990 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+430.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 42990 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223712 134559509 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+440.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3208 0 0 0 43990 14 0 0 25 0 1 0 548971493 14782464 3186 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3209 0 0 0 44990 15 0 0 25 0 1 0 548971493 14782464 3187 4294967295 134512640 134672761 3221224528 3221223712 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3187 603 41 0 3568 0
vsize: 14436
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3209 0 0 0 45990 15 0 0 25 0 1 0 548971493 14782464 3187 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3187 603 41 0 3568 0
vsize: 14436
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3209 0 0 0 46990 15 0 0 25 0 1 0 548971493 14782464 3187 4294967295 134512640 134672761 3221224528 3221223624 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3187 603 41 0 3568 0
vsize: 14436
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3209 0 0 0 47991 15 0 0 25 0 1 0 548971493 14782464 3187 4294967295 134512640 134672761 3221224528 3221223664 134565973 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3187 603 41 0 3568 0
vsize: 14436
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3211 0 0 0 48991 15 0 0 25 0 1 0 548971493 14782464 3189 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3189 603 41 0 3568 0
vsize: 14436
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3211 0 0 0 49991 15 0 0 25 0 1 0 548971493 14782464 3189 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3189 603 41 0 3568 0
vsize: 14436
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3211 0 0 0 50991 15 0 0 25 0 1 0 548971493 14782464 3189 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3189 603 41 0 3568 0
vsize: 14436
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3211 0 0 0 51991 15 0 0 25 0 1 0 548971493 14782464 3189 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3189 603 41 0 3568 0
vsize: 14436
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3212 0 0 0 52991 15 0 0 25 0 1 0 548971493 14782464 3190 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3190 603 41 0 3568 0
vsize: 14436
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3212 0 0 0 53992 15 0 0 25 0 1 0 548971493 14782464 3190 4294967295 134512640 134672761 3221224528 3221223632 134560070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3190 603 41 0 3568 0
vsize: 14436
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3239 0 0 0 54992 15 0 0 25 0 1 0 548971493 14917632 3217 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3217 603 41 0 3601 0
vsize: 14568
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3243 0 0 0 55992 15 0 0 25 0 1 0 548971493 14917632 3221 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3221 603 41 0 3601 0
vsize: 14568
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3247 0 0 0 56992 15 0 0 25 0 1 0 548971493 14917632 3225 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3225 603 41 0 3601 0
vsize: 14568
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3264 0 0 0 57992 15 0 0 25 0 1 0 548971493 15060992 3242 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3242 603 41 0 3636 0
vsize: 14708
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3274 0 0 0 58992 15 0 0 25 0 1 0 548971493 15060992 3252 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3252 603 41 0 3636 0
vsize: 14708
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3274 0 0 0 59992 15 0 0 25 0 1 0 548971493 15060992 3252 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3252 603 41 0 3636 0
vsize: 14708
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3289 0 0 0 60993 15 0 0 25 0 1 0 548971493 15060992 3267 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3267 603 41 0 3636 0
vsize: 14708
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3289 0 0 0 61993 15 0 0 25 0 1 0 548971493 15060992 3267 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3267 603 41 0 3636 0
vsize: 14708
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3299 0 0 0 62993 15 0 0 25 0 1 0 548971493 15257600 3277 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3277 603 41 0 3684 0
vsize: 14900
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3302 0 0 0 63993 15 0 0 25 0 1 0 548971493 15257600 3280 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3280 603 41 0 3684 0
vsize: 14900
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3302 0 0 0 64993 15 0 0 25 0 1 0 548971493 15257600 3280 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3280 603 41 0 3684 0
vsize: 14900
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3302 0 0 0 65993 15 0 0 25 0 1 0 548971493 15257600 3280 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3280 603 41 0 3684 0
vsize: 14900
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3359 0 0 0 66993 15 0 0 25 0 1 0 548971493 15392768 3337 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3758 3337 603 41 0 3717 0
vsize: 15032
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3564 0 0 0 67993 16 0 0 25 0 1 0 548971493 16314368 3542 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3983 3542 603 41 0 3942 0
vsize: 15932
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3710 0 0 0 68993 16 0 0 25 0 1 0 548971493 16842752 3688 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4112 3688 603 41 0 4071 0
vsize: 16448
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3712 0 0 0 69993 17 0 0 25 0 1 0 548971493 16842752 3690 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4112 3690 603 41 0 4071 0
vsize: 16448
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3774 0 0 0 70993 17 0 0 25 0 1 0 548971493 17108992 3752 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4177 3752 603 41 0 4136 0
vsize: 16708
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3827 0 0 0 71993 17 0 0 25 0 1 0 548971493 17387520 3805 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3827 0 0 0 72993 17 0 0 25 0 1 0 548971493 17387520 3805 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3827 0 0 0 73993 17 0 0 25 0 1 0 548971493 17387520 3805 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3827 0 0 0 74993 17 0 0 25 0 1 0 548971493 17387520 3805 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3827 0 0 0 75993 17 0 0 25 0 1 0 548971493 17387520 3805 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3827 0 0 0 76993 17 0 0 25 0 1 0 548971493 17387520 3805 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3827 0 0 0 77993 17 0 0 25 0 1 0 548971493 17387520 3805 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3834 0 0 0 78994 17 0 0 25 0 1 0 548971493 17387520 3812 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3812 603 41 0 4204 0
vsize: 16980
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3839 0 0 0 79994 17 0 0 25 0 1 0 548971493 17387520 3817 4294967295 134512640 134672761 3221224528 3221223632 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3817 603 41 0 4204 0
vsize: 16980
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3839 0 0 0 80994 17 0 0 25 0 1 0 548971493 17387520 3817 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3817 603 41 0 4204 0
vsize: 16980
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3845 0 0 0 81994 17 0 0 25 0 1 0 548971493 17387520 3823 4294967295 134512640 134672761 3221224528 3221223712 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3823 603 41 0 4204 0
vsize: 16980
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3849 0 0 0 82994 17 0 0 25 0 1 0 548971493 17387520 3827 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3827 603 41 0 4204 0
vsize: 16980
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3854 0 0 0 83995 18 0 0 25 0 1 0 548971493 17530880 3832 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4280 3832 603 41 0 4239 0
vsize: 17120
[startup+850.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3854 0 0 0 84996 18 0 0 25 0 1 0 548971493 17530880 3832 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3832 603 41 0 4239 0
vsize: 17120
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3887 0 0 0 85996 18 0 0 25 0 1 0 548971493 17793024 3865 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3865 603 41 0 4303 0
vsize: 17376
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3888 0 0 0 86996 18 0 0 25 0 1 0 548971493 17793024 3866 4294967295 134512640 134672761 3221224528 3221223712 134558678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3888 0 0 0 87996 18 0 0 25 0 1 0 548971493 17793024 3866 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3888 0 0 0 88996 18 0 0 25 0 1 0 548971493 17793024 3866 4294967295 134512640 134672761 3221224528 3221223664 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+900.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3888 0 0 0 89996 18 0 0 25 0 1 0 548971493 17793024 3866 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+910.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3891 0 0 0 90997 18 0 0 25 0 1 0 548971493 17793024 3869 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3869 603 41 0 4303 0
vsize: 17376
[startup+920.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3894 0 0 0 91997 18 0 0 25 0 1 0 548971493 17793024 3872 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3872 603 41 0 4303 0
vsize: 17376
[startup+930.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3894 0 0 0 92997 18 0 0 25 0 1 0 548971493 17793024 3872 4294967295 134512640 134672761 3221224528 3221223664 134560579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3872 603 41 0 4303 0
vsize: 17376
[startup+940.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3907 0 0 0 93997 18 0 0 25 0 1 0 548971493 17793024 3885 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3885 603 41 0 4303 0
vsize: 17376
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3914 0 0 0 94997 18 0 0 25 0 1 0 548971493 17793024 3892 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4344 3892 603 41 0 4303 0
vsize: 17376
[startup+960.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3919 0 0 0 95997 18 0 0 25 0 1 0 548971493 17956864 3897 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3897 603 41 0 4343 0
vsize: 17536
[startup+970.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3921 0 0 0 96998 18 0 0 25 0 1 0 548971493 17956864 3899 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3899 603 41 0 4343 0
vsize: 17536
[startup+980.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3926 0 0 0 97998 18 0 0 25 0 1 0 548971493 17956864 3904 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3904 603 41 0 4343 0
vsize: 17536
[startup+990.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3927 0 0 0 98998 18 0 0 25 0 1 0 548971493 17956864 3905 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3905 603 41 0 4343 0
vsize: 17536
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3928 0 0 0 99998 18 0 0 25 0 1 0 548971493 17956864 3906 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3906 603 41 0 4343 0
vsize: 17536
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3928 0 0 0 100998 18 0 0 25 0 1 0 548971493 17956864 3906 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3906 603 41 0 4343 0
vsize: 17536
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3929 0 0 0 101998 18 0 0 25 0 1 0 548971493 17956864 3907 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3907 603 41 0 4343 0
vsize: 17536
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3939 0 0 0 102999 18 0 0 25 0 1 0 548971493 17956864 3917 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3917 603 41 0 4343 0
vsize: 17536
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3955 0 0 0 103999 18 0 0 25 0 1 0 548971493 18120704 3933 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3955 0 0 0 104999 18 0 0 25 0 1 0 548971493 18120704 3933 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3955 0 0 0 105999 18 0 0 25 0 1 0 548971493 18120704 3933 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3955 0 0 0 106999 18 0 0 25 0 1 0 548971493 18120704 3933 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3955 0 0 0 107999 18 0 0 25 0 1 0 548971493 18120704 3933 4294967295 134512640 134672761 3221224528 3221223712 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3955 0 0 0 109000 18 0 0 25 0 1 0 548971493 18120704 3933 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 3955 0 0 0 110000 18 0 0 25 0 1 0 548971493 18120704 3933 4294967295 134512640 134672761 3221224528 3221223696 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4004 0 0 0 110999 18 0 0 25 0 1 0 548971493 18255872 3982 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4457 3982 603 41 0 4416 0
vsize: 17828
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4106 0 0 0 111998 19 0 0 25 0 1 0 548971493 18653184 4084 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4554 4084 603 41 0 4513 0
vsize: 18216
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4112 0 0 0 112998 19 0 0 25 0 1 0 548971493 18653184 4090 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 4090 603 41 0 4513 0
vsize: 18216
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4122 0 0 0 113998 19 0 0 25 0 1 0 548971493 18788352 4100 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4100 603 41 0 4546 0
vsize: 18348
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4135 0 0 0 114998 19 0 0 25 0 1 0 548971493 18788352 4113 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4113 603 41 0 4546 0
vsize: 18348
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4194 0 0 0 115998 20 0 0 25 0 1 0 548971493 19050496 4172 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4172 603 41 0 4610 0
vsize: 18604
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4195 0 0 0 116998 20 0 0 25 0 1 0 548971493 19050496 4173 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4173 603 41 0 4610 0
vsize: 18604
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4202 0 0 0 117998 20 0 0 25 0 1 0 548971493 19050496 4180 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4180 603 41 0 4610 0
vsize: 18604
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4207 0 0 0 118998 20 0 0 25 0 1 0 548971493 19197952 4185 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4185 603 41 0 4646 0
vsize: 18748
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32234
Raw data (stat): 32234 (minisat+) R 32233 11931 11930 0 -1 0 4213 0 0 0 119999 20 0 0 25 0 1 0 548971493 19197952 4191 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4191 603 41 0 4646 0
vsize: 18748
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32234
Raw data (stat): 32234 (minisat+) Z 32233 11931 11930 0 -1 12 4216 0 0 0 119999 21 0 0 25 0 1 0 548971493 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.99
CPU system time (s): 0.211967
CPU usage (%): 100.012
Max. virtual memory (Kb): 18748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####