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/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-9symml.opb
MD5SUM	48809ba02390b1184dab90aed89aff8e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4517
Optimality of the best value was proved	NO
Number of terms in the objective function	651
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	28138
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	28138
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	651
Total number of constraints	1658
Number of constraints which are clauses	1656
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 6339

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        873036 kB
Buffers:         28780 kB
Cached:         112932 kB
SwapCached:          0 kB
Active:          47612 kB
Inactive:        97000 kB
HighTotal:      131008 kB
HighFree:        14784 kB
LowTotal:       903652 kB
LowFree:        858252 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11348 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:41:43 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4758 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1579 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1552     6592 |     517       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6227[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:101537     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  279605   656998 |   93201       0        0     nan |  0.000 % |
c |       101 |  278250   653912 |  102521      92      397     4.3 |  0.389 % |
c |       251 |  278002   653347 |  112773     241     1458     6.0 |  0.464 % |
c |       477 |  277925   653170 |  124050     466     3433     7.4 |  0.490 % |
c |       814 |  277925   653170 |  136455     803     6582     8.2 |  0.490 % |
c |      1320 |  277925   653170 |  150101    1309    41682    31.8 |  0.490 % |
c |      2079 |  277890   653092 |  165111    2067    64329    31.1 |  0.499 % |
c |      3219 |  277720   652704 |  181622    3204    82101    25.6 |  0.552 % |
c |      4927 |  277720   652704 |  199784    4912   105336    21.4 |  0.552 % |
c |      7489 |  277636   652516 |  219763    7472   284608    38.1 |  0.576 % |
c |     11336 |  277636   652516 |  241739   11319   361142    31.9 |  0.576 % |
c |     17103 |  277353   651872 |  265913   17077   552676    32.4 |  0.662 % |
c |     25752 |  276839   650705 |  292504   25681   803126    31.3 |  0.816 % |
c |     38727 |  275986   648760 |  321755   38588  1273218    33.0 |  1.077 % |
c ==============================================================================
c [1mFound solution: 6197[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:81755     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55566 |  494343  1159810 |  164781   55426  2103376    37.9 |  1.077 % |
c |     55666 |  494343  1159810 |  181259   55526  2104490    37.9 |  0.674 % |
c |     55816 |  494343  1159810 |  199385   55676  2110303    37.9 |  0.674 % |
c |     56043 |  494343  1159810 |  219323   55903  2115396    37.8 |  0.674 % |
c |     56382 |  494343  1159810 |  241255   56242  2117392    37.6 |  0.674 % |
c |     56888 |  494343  1159810 |  265381   56748  2123459    37.4 |  0.674 % |
c |     57648 |  494343  1159810 |  291919   57508  2132867    37.1 |  0.674 % |
c |     58787 |  494343  1159810 |  321111   58647  2164470    36.9 |  0.674 % |
c |     60495 |  494343  1159810 |  353222   60355  2199982    36.5 |  0.674 % |
c |     63057 |  493978  1158974 |  388544   62789  2244296    35.7 |  0.738 % |
c |     66901 |  493978  1158974 |  427399   66633  2462795    37.0 |  0.738 % |
c |     72667 |  493978  1158974 |  470139   72399  2699174    37.3 |  0.738 % |
c |     81317 |  492669  1156002 |  517153   80957  3204576    39.6 |  0.955 % |
c ==============================================================================
c [1mFound solution: 6190[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87074 |  495326  1162645 |  165108   86714  4111781    47.4 |  0.955 % |
c |     87174 |  495326  1162645 |  181618   86814  4113071    47.4 |  0.956 % |
c |     87324 |  495326  1162645 |  199780   86964  4114363    47.3 |  0.956 % |
c |     87549 |  495278  1162535 |  219758   87186  4118174    47.2 |  0.965 % |
c |     87886 |  495278  1162535 |  241734   87523  4120333    47.1 |  0.965 % |
c |     88393 |  495278  1162535 |  265908   88030  4126436    46.9 |  0.965 % |
c |     89152 |  495278  1162535 |  292498   88789  4135162    46.6 |  0.965 % |
c |     90292 |  495278  1162535 |  321748   89929  4278437    47.6 |  0.965 % |
c |     92000 |  495266  1162508 |  353923   91635  4365648    47.6 |  0.967 % |
c |     94562 |  495266  1162508 |  389316   94197  4421944    46.9 |  0.967 % |
c |     98408 |  495218  1162401 |  428247   98029  4468493    45.6 |  0.974 % |
c |    104176 |  495106  1162147 |  471072  103795  4739047    45.7 |  0.991 % |
c |    112825 |  495106  1162147 |  518179  112444  5122762    45.6 |  0.991 % |
c |    125801 |  495099  1162131 |  569997  125418  6011386    47.9 |  0.993 % |
c |    145263 |  495052  1162026 |  626997  144879  6906685    47.7 |  1.000 % |
c ==============================================================================
c [1mFound solution: 6188[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    152076 |  495196  1162452 |  165065  151692  8009871    52.8 |  1.000 % |
c |    152177 |  495196  1162452 |  181571  151793  8010582    52.8 |  1.001 % |
c |    152328 |  495196  1162452 |  199728  151944  8011442    52.7 |  1.001 % |
c |    152553 |  495196  1162452 |  219701  152169  8013019    52.7 |  1.001 % |
c |    152890 |  495196  1162452 |  241671  152506  8023737    52.6 |  1.001 % |
c |    153396 |  495169  1162390 |  265838  153009  8030216    52.5 |  1.006 % |
c |    154156 |  495169  1162390 |  292422  153769  8035635    52.3 |  1.006 % |
c |    155295 |  495169  1162390 |  321664  154908  8050682    52.0 |  1.006 % |
c |    157003 |  495035  1162082 |  353831  156613  8146673    52.0 |  1.030 % |
c |    159565 |  495035  1162082 |  389214  159175  8212062    51.6 |  1.030 % |
c |    163410 |  494989  1161974 |  428136  163010  8431726    51.7 |  1.040 % |
c |    169177 |  494989  1161974 |  470949  168777  8646344    51.2 |  1.040 % |
c |    177827 |  494866  1161690 |  518044  177414  9307750    52.5 |  1.063 % |
#### 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.93 2/55 5340
Raw data (stat): 5340 (runsolver) R 5339 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358935202 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99984 s]
Raw data (loadavg): 0.92 0.95 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8309 0 0 0 980 18 0 0 25 0 1 0 358935202 37474304 7849 4294967295 134512640 134672761 3221224576 3221223760 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9149 7849 603 41 0 9108 0
vsize: 36596
[startup+20.0001 s]
Raw data (loadavg): 0.93 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8380 0 0 0 1980 18 0 0 25 0 1 0 358935202 37875712 7920 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 7920 603 41 0 9206 0
vsize: 36988
[startup+30.0008 s]
Raw data (loadavg): 0.94 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8500 0 0 0 2980 19 0 0 25 0 1 0 358935202 38281216 8040 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9346 8040 603 41 0 9305 0
vsize: 37384
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8566 0 0 0 3980 19 0 0 25 0 1 0 358935202 38551552 8106 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9412 8106 603 41 0 9371 0
vsize: 37648
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8666 0 0 0 4979 20 0 0 25 0 1 0 358935202 38948864 8206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9509 8206 603 41 0 9468 0
vsize: 38036
[startup+60.0018 s]
Raw data (loadavg): 0.96 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8784 0 0 0 5979 20 0 0 25 0 1 0 358935202 39489536 8324 4294967295 134512640 134672761 3221224576 3221223712 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9641 8324 603 41 0 9600 0
vsize: 38564
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8884 0 0 0 6978 21 0 0 25 0 1 0 358935202 39976960 8424 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 8424 603 41 0 9719 0
vsize: 39040
[startup+80.0032 s]
Raw data (loadavg): 0.97 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 8962 0 0 0 7978 21 0 0 25 0 1 0 358935202 40243200 8502 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9825 8502 603 41 0 9784 0
vsize: 39300
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9094 0 0 0 8977 22 0 0 25 0 1 0 358935202 40775680 8634 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9955 8634 603 41 0 9914 0
vsize: 39820
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9227 0 0 0 9977 22 0 0 25 0 1 0 358935202 41312256 8767 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10086 8767 603 41 0 10045 0
vsize: 40344
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9311 0 0 0 10977 23 0 0 25 0 1 0 358935202 41578496 8851 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10151 8851 603 41 0 10110 0
vsize: 40604
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9357 0 0 0 11977 23 0 0 25 0 1 0 358935202 41840640 8897 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10215 8897 603 41 0 10174 0
vsize: 40860
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9491 0 0 0 12977 23 0 0 25 0 1 0 358935202 42373120 9031 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10345 9031 603 41 0 10304 0
vsize: 41380
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9616 0 0 0 13976 24 0 0 25 0 1 0 358935202 42913792 9156 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10477 9156 603 41 0 10436 0
vsize: 41908
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9735 0 0 0 14976 24 0 0 25 0 1 0 358935202 43450368 9275 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10608 9275 603 41 0 10567 0
vsize: 42432
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9831 0 0 0 15976 25 0 0 25 0 1 0 358935202 43851776 9371 4294967295 134512640 134672761 3221224576 3221223680 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 9371 603 41 0 10665 0
vsize: 42824
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 9925 0 0 0 16976 25 0 0 25 0 1 0 358935202 44118016 9465 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 9465 603 41 0 10730 0
vsize: 43084
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 10027 0 0 0 17975 26 0 0 25 0 1 0 358935202 44523520 9567 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10870 9567 603 41 0 10829 0
vsize: 43480
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 10129 0 0 0 18975 26 0 0 25 0 1 0 358935202 44929024 9669 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10969 9669 603 41 0 10928 0
vsize: 43876
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 10414 0 0 0 19974 28 0 0 25 0 1 0 358935202 46149632 9954 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11267 9954 603 41 0 11226 0
vsize: 45068
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 10666 0 0 0 20973 29 0 0 25 0 1 0 358935202 47087616 10206 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11496 10206 603 41 0 11455 0
vsize: 45984
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17121 0 0 0 21958 43 0 0 25 0 1 0 358935202 75722752 16206 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18487 16206 603 41 0 18446 0
vsize: 73948
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17166 0 0 0 22957 44 0 0 25 0 1 0 358935202 75853824 16251 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18519 16251 603 41 0 18478 0
vsize: 74076
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17214 0 0 0 23957 44 0 0 25 0 1 0 358935202 75988992 16299 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18552 16299 603 41 0 18511 0
vsize: 74208
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17267 0 0 0 24957 45 0 0 25 0 1 0 358935202 76255232 16352 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18617 16352 603 41 0 18576 0
vsize: 74468
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17285 0 0 0 25957 45 0 0 25 0 1 0 358935202 76390400 16370 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18650 16370 603 41 0 18609 0
vsize: 74600
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17308 0 0 0 26957 45 0 0 25 0 1 0 358935202 76390400 16393 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18650 16393 603 41 0 18609 0
vsize: 74600
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17353 0 0 0 27957 45 0 0 25 0 1 0 358935202 76660736 16438 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18716 16438 603 41 0 18675 0
vsize: 74864
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17556 0 0 0 28957 46 0 0 25 0 1 0 358935202 77733888 16641 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18978 16641 603 41 0 18937 0
vsize: 75912
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17650 0 0 0 29957 46 0 0 25 0 1 0 358935202 78004224 16735 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19044 16735 603 41 0 19003 0
vsize: 76176
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17701 0 0 0 30957 46 0 0 25 0 1 0 358935202 78274560 16786 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19110 16786 603 41 0 19069 0
vsize: 76440
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17725 0 0 0 31956 46 0 0 25 0 1 0 358935202 78405632 16810 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19142 16810 603 41 0 19101 0
vsize: 76568
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17755 0 0 0 32956 46 0 0 25 0 1 0 358935202 78536704 16840 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19174 16840 603 41 0 19133 0
vsize: 76696
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17782 0 0 0 33956 47 0 0 25 0 1 0 358935202 78536704 16867 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19174 16867 603 41 0 19133 0
vsize: 76696
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17818 0 0 0 34956 47 0 0 25 0 1 0 358935202 78671872 16903 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19207 16903 603 41 0 19166 0
vsize: 76828
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17847 0 0 0 35956 47 0 0 25 0 1 0 358935202 78807040 16932 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19240 16932 603 41 0 19199 0
vsize: 76960
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 17987 0 0 0 36956 48 0 0 25 0 1 0 358935202 79343616 17072 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19371 17072 603 41 0 19330 0
vsize: 77484
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18091 0 0 0 37955 48 0 0 25 0 1 0 358935202 79769600 17176 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19475 17176 603 41 0 19434 0
vsize: 77900
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18251 0 0 0 38955 49 0 0 25 0 1 0 358935202 80416768 17336 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19633 17336 603 41 0 19592 0
vsize: 78532
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18392 0 0 0 39954 49 0 0 25 0 1 0 358935202 80957440 17477 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19765 17477 603 41 0 19724 0
vsize: 79060
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18439 0 0 0 40954 50 0 0 25 0 1 0 358935202 81219584 17524 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19829 17524 603 41 0 19788 0
vsize: 79316
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18455 0 0 0 41954 50 0 0 25 0 1 0 358935202 81219584 17540 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19829 17540 603 41 0 19788 0
vsize: 79316
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18475 0 0 0 42954 50 0 0 25 0 1 0 358935202 81354752 17560 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19862 17560 603 41 0 19821 0
vsize: 79448
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18568 0 0 0 43953 51 0 0 25 0 1 0 358935202 81760256 17653 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19961 17653 603 41 0 19920 0
vsize: 79844
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 18893 0 0 0 44953 52 0 0 25 0 1 0 358935202 83103744 17978 4294967295 134512640 134672761 3221224576 3221223680 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20289 17978 603 41 0 20248 0
vsize: 81156
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 19282 0 0 0 45952 53 0 0 25 0 1 0 358935202 84594688 18367 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20653 18367 603 41 0 20612 0
vsize: 82612
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 19714 0 0 0 46950 54 0 0 25 0 1 0 358935202 85512192 18674 4294967295 134512640 134672761 3221224576 3221223744 134561272 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20877 18674 603 41 0 20836 0
vsize: 83508
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 19799 0 0 0 47951 54 0 0 25 0 1 0 358935202 85774336 18759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20941 18759 603 41 0 20900 0
vsize: 83764
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 19911 0 0 0 48950 55 0 0 25 0 1 0 358935202 86315008 18871 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21073 18871 603 41 0 21032 0
vsize: 84292
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 19972 0 0 0 49950 55 0 0 25 0 1 0 358935202 86450176 18932 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21106 18932 603 41 0 21065 0
vsize: 84424
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20022 0 0 0 50950 55 0 0 25 0 1 0 358935202 86720512 18982 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21172 18982 603 41 0 21131 0
vsize: 84688
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20080 0 0 0 51950 56 0 0 25 0 1 0 358935202 86855680 19040 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21205 19040 603 41 0 21164 0
vsize: 84820
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20142 0 0 0 52949 56 0 0 25 0 1 0 358935202 87130112 19102 4294967295 134512640 134672761 3221224576 3221223712 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21272 19102 603 41 0 21231 0
vsize: 85088
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20235 0 0 0 53949 56 0 0 25 0 1 0 358935202 87531520 19195 4294967295 134512640 134672761 3221224576 3221223760 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21370 19195 603 41 0 21329 0
vsize: 85480
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20312 0 0 0 54949 57 0 0 25 0 1 0 358935202 87855104 19272 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21449 19272 603 41 0 21408 0
vsize: 85796
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20373 0 0 0 55949 57 0 0 25 0 1 0 358935202 88125440 19333 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21515 19333 603 41 0 21474 0
vsize: 86060
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20419 0 0 0 56949 57 0 0 25 0 1 0 358935202 88260608 19379 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21548 19379 603 41 0 21507 0
vsize: 86192
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20471 0 0 0 57948 58 0 0 25 0 1 0 358935202 88518656 19431 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21611 19431 603 41 0 21570 0
vsize: 86444
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20540 0 0 0 58948 58 0 0 25 0 1 0 358935202 88788992 19500 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21677 19500 603 41 0 21636 0
vsize: 86708
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20598 0 0 0 59948 58 0 0 25 0 1 0 358935202 89059328 19558 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21743 19558 603 41 0 21702 0
vsize: 86972
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20674 0 0 0 60948 59 0 0 25 0 1 0 358935202 89325568 19634 4294967295 134512640 134672761 3221224576 3221223712 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21808 19634 603 41 0 21767 0
vsize: 87232
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20756 0 0 0 61947 59 0 0 25 0 1 0 358935202 89722880 19716 4294967295 134512640 134672761 3221224576 3221223776 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21905 19716 603 41 0 21864 0
vsize: 87620
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20807 0 0 0 62947 60 0 0 25 0 1 0 358935202 89853952 19767 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21937 19767 603 41 0 21896 0
vsize: 87748
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20867 0 0 0 63947 60 0 0 25 0 1 0 358935202 90124288 19827 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22003 19827 603 41 0 21962 0
vsize: 88012
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 20964 0 0 0 64947 60 0 0 25 0 1 0 358935202 90529792 19924 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22102 19924 603 41 0 22061 0
vsize: 88408
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21079 0 0 0 65947 60 0 0 25 0 1 0 358935202 90931200 20039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22200 20039 603 41 0 22159 0
vsize: 88800
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21138 0 0 0 66947 61 0 0 25 0 1 0 358935202 91201536 20098 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22266 20098 603 41 0 22225 0
vsize: 89064
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21267 0 0 0 67946 62 0 0 25 0 1 0 358935202 91717632 20227 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22392 20227 603 41 0 22351 0
vsize: 89568
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21409 0 0 0 68946 62 0 0 25 0 1 0 358935202 92254208 20369 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22523 20369 603 41 0 22482 0
vsize: 90092
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21475 0 0 0 69945 62 0 0 25 0 1 0 358935202 92524544 20435 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22589 20435 603 41 0 22548 0
vsize: 90356
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21625 0 0 0 70945 63 0 0 25 0 1 0 358935202 93196288 20585 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22753 20585 603 41 0 22712 0
vsize: 91012
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21741 0 0 0 71945 63 0 0 25 0 1 0 358935202 93585408 20701 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22848 20701 603 41 0 22807 0
vsize: 91392
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21824 0 0 0 72945 63 0 0 25 0 1 0 358935202 93986816 20784 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22946 20784 603 41 0 22905 0
vsize: 91784
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21883 0 0 0 73944 64 0 0 25 0 1 0 358935202 94257152 20843 4294967295 134512640 134672761 3221224576 3221223680 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23012 20843 603 41 0 22971 0
vsize: 92048
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 21932 0 0 0 74944 64 0 0 25 0 1 0 358935202 94388224 20892 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23044 20892 603 41 0 23003 0
vsize: 92176
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22010 0 0 0 75943 65 0 0 25 0 1 0 358935202 94789632 20970 4294967295 134512640 134672761 3221224576 3221223776 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23142 20970 603 41 0 23101 0
vsize: 92568
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22132 0 0 0 76943 65 0 0 25 0 1 0 358935202 95715328 21092 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23368 21092 603 41 0 23327 0
vsize: 93472
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22232 0 0 0 77943 66 0 0 25 0 1 0 358935202 96120832 21192 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23467 21192 603 41 0 23426 0
vsize: 93868
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22299 0 0 0 78942 67 0 0 25 0 1 0 358935202 96387072 21259 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23532 21259 603 41 0 23491 0
vsize: 94128
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22377 0 0 0 79942 67 0 0 25 0 1 0 358935202 96792576 21337 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23631 21337 603 41 0 23590 0
vsize: 94524
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22413 0 0 0 80942 67 0 0 25 0 1 0 358935202 96927744 21373 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23664 21373 603 41 0 23623 0
vsize: 94656
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22492 0 0 0 81942 68 0 0 25 0 1 0 358935202 97198080 21452 4294967295 134512640 134672761 3221224576 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23730 21452 603 41 0 23689 0
vsize: 94920
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22601 0 0 0 82941 68 0 0 25 0 1 0 358935202 97599488 21561 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23828 21561 603 41 0 23787 0
vsize: 95312
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22653 0 0 0 83941 68 0 0 25 0 1 0 358935202 97865728 21613 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23893 21613 603 41 0 23852 0
vsize: 95572
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22713 0 0 0 84941 69 0 0 25 0 1 0 358935202 98136064 21673 4294967295 134512640 134672761 3221224576 3221223712 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23959 21673 603 41 0 23918 0
vsize: 95836
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22753 0 0 0 85940 69 0 0 25 0 1 0 358935202 98271232 21713 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23992 21713 603 41 0 23951 0
vsize: 95968
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22809 0 0 0 86940 70 0 0 25 0 1 0 358935202 98406400 21769 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24025 21769 603 41 0 23984 0
vsize: 96100
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22882 0 0 0 87940 70 0 0 25 0 1 0 358935202 98803712 21842 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24122 21842 603 41 0 24081 0
vsize: 96488
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 22998 0 0 0 88939 71 0 0 25 0 1 0 358935202 99209216 21958 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24221 21958 603 41 0 24180 0
vsize: 96884
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 23052 0 0 0 89939 71 0 0 25 0 1 0 358935202 99475456 22012 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24286 22012 603 41 0 24245 0
vsize: 97144
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 23115 0 0 0 90939 71 0 0 25 0 1 0 358935202 99745792 22075 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24352 22075 603 41 0 24311 0
vsize: 97408
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 23170 0 0 0 91939 72 0 0 25 0 1 0 358935202 99876864 22130 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24384 22130 603 41 0 24343 0
vsize: 97536
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 23296 0 0 0 92939 72 0 0 25 0 1 0 358935202 100421632 22256 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24517 22256 603 41 0 24476 0
vsize: 98068
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 23439 0 0 0 93938 73 0 0 25 0 1 0 358935202 100962304 22399 4294967295 134512640 134672761 3221224576 3221223744 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24649 22399 603 41 0 24608 0
vsize: 98596
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 23645 0 0 0 94938 73 0 0 25 0 1 0 358935202 101896192 22605 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24877 22605 603 41 0 24836 0
vsize: 99508
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 23845 0 0 0 95937 74 0 0 25 0 1 0 358935202 102719488 22805 4294967295 134512640 134672761 3221224576 3221223712 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25078 22805 603 41 0 25037 0
vsize: 100312
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24001 0 0 0 96937 74 0 0 25 0 1 0 358935202 103374848 22961 4294967295 134512640 134672761 3221224576 3221223700 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25238 22961 603 41 0 25197 0
vsize: 100952
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24220 0 0 0 97936 75 0 0 25 0 1 0 358935202 103714816 23055 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25321 23055 603 41 0 25280 0
vsize: 101284
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24291 0 0 0 98936 76 0 0 25 0 1 0 358935202 103985152 23126 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25387 23126 603 41 0 25346 0
vsize: 101548
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24357 0 0 0 99935 76 0 0 25 0 1 0 358935202 104255488 23192 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25453 23192 603 41 0 25412 0
vsize: 101812
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24429 0 0 0 100935 77 0 0 25 0 1 0 358935202 104521728 23264 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25518 23264 603 41 0 25477 0
vsize: 102072
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24628 0 0 0 101935 77 0 0 25 0 1 0 358935202 105324544 23463 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25714 23463 603 41 0 25673 0
vsize: 102856
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24657 0 0 0 102935 77 0 0 25 0 1 0 358935202 105459712 23492 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25747 23492 603 41 0 25706 0
vsize: 102988
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24789 0 0 0 103935 77 0 0 25 0 1 0 358935202 105992192 23624 4294967295 134512640 134672761 3221224576 3221223776 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25877 23624 603 41 0 25836 0
vsize: 103508
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24850 0 0 0 104935 78 0 0 25 0 1 0 358935202 106254336 23685 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25941 23685 603 41 0 25900 0
vsize: 103764
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 24932 0 0 0 105934 78 0 0 25 0 1 0 358935202 106520576 23767 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26006 23767 603 41 0 25965 0
vsize: 104024
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25076 0 0 0 106934 79 0 0 25 0 1 0 358935202 107204608 23911 4294967295 134512640 134672761 3221224576 3221223760 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26173 23911 603 41 0 26132 0
vsize: 104692
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25166 0 0 0 107933 79 0 0 25 0 1 0 358935202 107474944 24001 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26239 24001 603 41 0 26198 0
vsize: 104956
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25240 0 0 0 108933 80 0 0 25 0 1 0 358935202 107745280 24075 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26305 24075 603 41 0 26264 0
vsize: 105220
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25327 0 0 0 109933 80 0 0 25 0 1 0 358935202 108146688 24162 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26403 24162 603 41 0 26362 0
vsize: 105612
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25404 0 0 0 110933 80 0 0 25 0 1 0 358935202 108417024 24239 4294967295 134512640 134672761 3221224576 3221223760 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26469 24239 603 41 0 26428 0
vsize: 105876
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25519 0 0 0 111932 81 0 0 25 0 1 0 358935202 108957696 24354 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26601 24354 603 41 0 26560 0
vsize: 106404
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25609 0 0 0 112932 82 0 0 25 0 1 0 358935202 109223936 24444 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26666 24444 603 41 0 26625 0
vsize: 106664
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25687 0 0 0 113931 82 0 0 25 0 1 0 358935202 109625344 24522 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26764 24522 603 41 0 26723 0
vsize: 107056
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25702 0 0 0 114931 83 0 0 25 0 1 0 358935202 109625344 24537 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26764 24537 603 41 0 26723 0
vsize: 107056
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25710 0 0 0 115931 83 0 0 25 0 1 0 358935202 109625344 24545 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26764 24545 603 41 0 26723 0
vsize: 107056
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25718 0 0 0 116931 83 0 0 25 0 1 0 358935202 109756416 24553 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26796 24553 603 41 0 26755 0
vsize: 107184
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25731 0 0 0 117931 83 0 0 25 0 1 0 358935202 109756416 24566 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26796 24566 603 41 0 26755 0
vsize: 107184
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25742 0 0 0 118931 83 0 0 25 0 1 0 358935202 109756416 24577 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26796 24577 603 41 0 26755 0
vsize: 107184
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5340
Raw data (stat): 5340 (minisat+) R 5339 30927 30926 0 -1 0 25768 0 0 0 119930 84 0 0 25 0 1 0 358935202 109887488 24603 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26828 24603 603 41 0 26787 0
vsize: 107312
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.93 1/55 5340
Raw data (stat): 5340 (minisat+) Z 5339 30927 30926 0 -1 12 25771 0 0 0 119930 88 0 0 25 0 1 0 358935202 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.08
CPU time (s): 1200.2
CPU user time (s): 1199.31
CPU system time (s): 0.886865
CPU usage (%): 100.009
Max. virtual memory (Kb): 107312
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####