PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare2.opb
MD5SUM	b54bb080800e2327586cd478559c04ff
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10368
Optimality of the best value was proved	NO
Number of terms in the objective function	140
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	200
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	80
Trace number 15120

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-21 02:58:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18524 boxname=wulflinc9 idbench=1425 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b54bb080800e2327586cd478559c04ff  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-markshare2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-markshare2.opb /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-markshare2.opb
IDLAUNCH: 18524
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        568528 kB
Buffers:         35432 kB
Cached:         408192 kB
SwapCached:          8 kB
Active:          97772 kB
Inactive:       348628 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        568276 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            13968 kB
Committed_AS:    63624 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:18:12 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 18524 7 1200.22 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]---> BDD-cost:33297
c ---[  10]---> BDD-cost:39178
c ---[   8]---> BDD-cost:34986
c ---[   6]---> BDD-cost:41587
c ---[   4]---> BDD-cost:41667
c ---[   2]---> BDD-cost:41235
c ---[   0]---> BDD-cost:35324
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  774400  2270366 |  258133       0        0     nan |  0.000 % |
c |       100 |  774400  2270366 |  283946     100     9452    94.5 |  0.008 % |
c ==============================================================================
c [1mFound solution: 1159424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       103 |  779065  2281260 |  259688     103     9521    92.4 |  0.008 % |
c ==============================================================================
c [1mFound solution: 1091328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       106 |  779085  2281332 |  259695     106     9583    90.4 |  0.008 % |
c ==============================================================================
c [1mFound solution: 1085440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       135 |  779100  2281371 |  259700     135    10953    81.1 |  0.008 % |
c |       236 |  779100  2281371 |  285670     236    16182    68.6 |  0.009 % |
c |       388 |  779100  2281371 |  314237     388    24371    62.8 |  0.009 % |
c ==============================================================================
c [1mFound solution: 1079936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       505 |  779117  2281412 |  259705     505    30585    60.6 |  0.009 % |
c ==============================================================================
c [1mFound solution: 1076480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       532 |  779128  2281439 |  259709     532    32305    60.7 |  0.009 % |
c ==============================================================================
c [1mFound solution: 1060480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       625 |  779138  2281463 |  259712     625    37233    59.6 |  0.009 % |
c ==============================================================================
c [1mFound solution: 1056384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       712 |  779146  2281481 |  259715     712    41686    58.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 961664[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       713 |  779162  2281520 |  259720     713    41751    58.6 |  0.009 % |
c |       813 |  779162  2281520 |  285692     813    46693    57.4 |  0.011 % |
c |       965 |  779162  2281520 |  314261     965    54953    56.9 |  0.011 % |
c ==============================================================================
c [1mFound solution: 953600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       992 |  779170  2281538 |  259723     992    56372    56.8 |  0.011 % |
c ==============================================================================
c [1mFound solution: 948480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1064 |  779178  2281559 |  259726    1064    59130    55.6 |  0.011 % |
c ==============================================================================
c [1mFound solution: 928256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1068 |  779193  2281593 |  259731    1068    59470    55.7 |  0.011 % |
c |      1168 |  779193  2281593 |  285704    1168    64070    54.9 |  0.012 % |
c |      1318 |  779193  2281593 |  314274    1318    70952    53.8 |  0.012 % |
c |      1543 |  779193  2281593 |  345701    1543    84455    54.7 |  0.012 % |
c |      1880 |  779193  2281593 |  380272    1880   104095    55.4 |  0.012 % |
c ==============================================================================
c [1mFound solution: 907904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1929 |  779212  2281644 |  259737    1929   106696    55.3 |  0.012 % |
c |      2031 |  779212  2281644 |  285710    2031   110666    54.5 |  0.012 % |
c |      2183 |  779212  2281644 |  314281    2183   119905    54.9 |  0.012 % |
c |      2408 |  779212  2281644 |  345709    2408   131349    54.5 |  0.012 % |
c ==============================================================================
c [1mFound solution: 876032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2411 |  779223  2281675 |  259741    2411   131543    54.6 |  0.012 % |
c |      2511 |  779223  2281675 |  285715    2511   137169    54.6 |  0.013 % |
c |      2663 |  779223  2281675 |  314286    2663   144243    54.2 |  0.013 % |
c |      2888 |  779223  2281675 |  345715    2888   158492    54.9 |  0.013 % |
c ==============================================================================
c [1mFound solution: 864000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2918 |  779234  2281701 |  259744    2918   160062    54.9 |  0.013 % |
c |      3018 |  779234  2281701 |  285718    3018   165023    54.7 |  0.013 % |
c ==============================================================================
c [1mFound solution: 848384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3047 |  779241  2281720 |  259747    3047   166723    54.7 |  0.013 % |
c ==============================================================================
c [1mFound solution: 845440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3141 |  779250  2281743 |  259750    3141   171715    54.7 |  0.013 % |
c |      3242 |  779250  2281743 |  285725    3242   177415    54.7 |  0.014 % |
c |      3392 |  779250  2281743 |  314297    3392   186259    54.9 |  0.014 % |
c |      3617 |  779250  2281743 |  345727    3617   199709    55.2 |  0.014 % |
c |      3954 |  779250  2281743 |  380299    3954   219820    55.6 |  0.014 % |
c ==============================================================================
c [1mFound solution: 839552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4285 |  779259  2281768 |  259753    4285   236652    55.2 |  0.014 % |
c |      4385 |  779259  2281768 |  285728    4385   241366    55.0 |  0.014 % |
c |      4535 |  779259  2281768 |  314301    4535   250113    55.2 |  0.014 % |
c |      4760 |  779259  2281768 |  345731    4760   262030    55.0 |  0.014 % |
c ==============================================================================
c [1mFound solution: 825344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4866 |  779271  2281796 |  259757    4866   267684    55.0 |  0.014 % |
c |      4966 |  779271  2281796 |  285732    4966   272049    54.8 |  0.015 % |
c |      5116 |  779271  2281796 |  314305    5116   282890    55.3 |  0.015 % |
c |      5341 |  779271  2281796 |  345736    5341   296320    55.5 |  0.015 % |
c |      5678 |  779271  2281796 |  380310    5678   313256    55.2 |  0.015 % |
c |      6184 |  779271  2281796 |  418341    6184   341829    55.3 |  0.015 % |
c |      6943 |  779271  2281796 |  460175    6943   391438    56.4 |  0.015 % |
c |      8084 |  779271  2281796 |  506192    8084   471022    58.3 |  0.015 % |
c |      9792 |  779271  2281796 |  556812    9792   607154    62.0 |  0.015 % |
c |     12355 |  779271  2281796 |  612493   12355   771229    62.4 |  0.015 % |
c |     16199 |  779271  2281796 |  673742   16199  1017250    62.8 |  0.015 % |
#### 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.94 2/54 32615
Raw data (stat): 32615 (runsolver) R 32614 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483437673 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.0006 s]
Raw data (loadavg): 0.93 0.95 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 24239 0 0 0 942 55 0 0 25 0 1 0 483437673 117608448 22668 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28713 22668 603 41 0 28672 0
vsize: 114852
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 24918 0 0 0 1941 57 0 0 25 0 1 0 483437673 121098240 23320 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29565 23320 603 41 0 29524 0
vsize: 118260
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 24964 0 0 0 2941 57 0 0 25 0 1 0 483437673 121581568 23366 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29683 23366 603 41 0 29642 0
vsize: 118732
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 24981 0 0 0 3941 57 0 0 25 0 1 0 483437673 121716736 23383 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29716 23383 603 41 0 29675 0
vsize: 118864
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25002 0 0 0 4941 57 0 0 25 0 1 0 483437673 121716736 23404 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29716 23404 603 41 0 29675 0
vsize: 118864
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25014 0 0 0 5941 57 0 0 25 0 1 0 483437673 121847808 23416 4294967295 134512640 134672761 3221224528 3221223632 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29748 23416 603 41 0 29707 0
vsize: 118992
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25024 0 0 0 6941 57 0 0 25 0 1 0 483437673 121847808 23426 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29748 23426 603 41 0 29707 0
vsize: 118992
[startup+80.0033 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25040 0 0 0 7941 57 0 0 25 0 1 0 483437673 121982976 23442 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29781 23442 603 41 0 29740 0
vsize: 119124
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25050 0 0 0 8941 57 0 0 25 0 1 0 483437673 121982976 23452 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29781 23452 603 41 0 29740 0
vsize: 119124
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25063 0 0 0 9942 57 0 0 25 0 1 0 483437673 121982976 23465 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29781 23465 603 41 0 29740 0
vsize: 119124
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 32615
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25072 0 0 0 10942 57 0 0 25 0 1 0 483437673 122114048 23474 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29813 23474 603 41 0 29772 0
vsize: 119252
[startup+120.005 s]
Raw data (loadavg): 1.37 1.05 0.97 2/54 32668
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25080 0 0 0 11942 57 0 0 25 0 1 0 483437673 122114048 23482 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29813 23482 603 41 0 29772 0
vsize: 119252
[startup+130.005 s]
Raw data (loadavg): 1.32 1.05 0.97 2/54 32668
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25095 0 0 0 12942 57 0 0 25 0 1 0 483437673 122114048 23497 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29813 23497 603 41 0 29772 0
vsize: 119252
[startup+140.005 s]
Raw data (loadavg): 1.27 1.04 0.97 2/54 32668
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25104 0 0 0 13942 57 0 0 25 0 1 0 483437673 122245120 23506 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29845 23506 603 41 0 29804 0
vsize: 119380
[startup+150.005 s]
Raw data (loadavg): 1.22 1.04 0.97 2/54 32668
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25115 0 0 0 14942 57 0 0 25 0 1 0 483437673 122245120 23517 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29845 23517 603 41 0 29804 0
vsize: 119380
[startup+160.006 s]
Raw data (loadavg): 1.19 1.04 0.97 2/54 32668
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25125 0 0 0 15942 57 0 0 25 0 1 0 483437673 122245120 23527 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29845 23527 603 41 0 29804 0
vsize: 119380
[startup+170.006 s]
Raw data (loadavg): 1.16 1.04 0.97 2/54 32668
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25133 0 0 0 16942 57 0 0 25 0 1 0 483437673 122245120 23535 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29845 23535 603 41 0 29804 0
vsize: 119380
[startup+180.006 s]
Raw data (loadavg): 1.14 1.04 0.97 2/54 32668
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25145 0 0 0 17942 57 0 0 25 0 1 0 483437673 122380288 23547 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29878 23547 603 41 0 29837 0
vsize: 119512
[startup+190.007 s]
Raw data (loadavg): 1.11 1.03 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25155 0 0 0 18943 57 0 0 25 0 1 0 483437673 122380288 23557 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29878 23557 603 41 0 29837 0
vsize: 119512
[startup+200.007 s]
Raw data (loadavg): 1.10 1.03 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25162 0 0 0 19943 57 0 0 25 0 1 0 483437673 122380288 23564 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29878 23564 603 41 0 29837 0
vsize: 119512
[startup+210.006 s]
Raw data (loadavg): 1.08 1.03 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25173 0 0 0 20943 57 0 0 25 0 1 0 483437673 122515456 23575 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29911 23575 603 41 0 29870 0
vsize: 119644
[startup+220.007 s]
Raw data (loadavg): 1.07 1.03 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25182 0 0 0 21943 58 0 0 25 0 1 0 483437673 122515456 23584 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29911 23584 603 41 0 29870 0
vsize: 119644
[startup+230.007 s]
Raw data (loadavg): 1.06 1.03 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25191 0 0 0 22943 58 0 0 25 0 1 0 483437673 122515456 23593 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29911 23593 603 41 0 29870 0
vsize: 119644
[startup+240.008 s]
Raw data (loadavg): 1.05 1.03 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25200 0 0 0 23943 58 0 0 25 0 1 0 483437673 122515456 23602 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29911 23602 603 41 0 29870 0
vsize: 119644
[startup+250.007 s]
Raw data (loadavg): 1.04 1.03 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25211 0 0 0 24943 58 0 0 25 0 1 0 483437673 122650624 23613 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29944 23613 603 41 0 29903 0
vsize: 119776
[startup+260.008 s]
Raw data (loadavg): 1.03 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25222 0 0 0 25943 58 0 0 25 0 1 0 483437673 122650624 23624 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29944 23624 603 41 0 29903 0
vsize: 119776
[startup+270.008 s]
Raw data (loadavg): 1.03 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25234 0 0 0 26943 58 0 0 25 0 1 0 483437673 122798080 23636 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29980 23636 603 41 0 29939 0
vsize: 119920
[startup+280.008 s]
Raw data (loadavg): 1.02 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25243 0 0 0 27944 58 0 0 25 0 1 0 483437673 122798080 23645 4294967295 134512640 134672761 3221224528 3221223632 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29980 23645 603 41 0 29939 0
vsize: 119920
[startup+290.009 s]
Raw data (loadavg): 1.02 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25253 0 0 0 28944 58 0 0 25 0 1 0 483437673 122798080 23655 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29980 23655 603 41 0 29939 0
vsize: 119920
[startup+300.009 s]
Raw data (loadavg): 1.02 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25265 0 0 0 29944 58 0 0 25 0 1 0 483437673 122798080 23667 4294967295 134512640 134672761 3221224528 3221223664 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29980 23667 603 41 0 29939 0
vsize: 119920
[startup+310.009 s]
Raw data (loadavg): 1.01 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25276 0 0 0 30944 58 0 0 25 0 1 0 483437673 122933248 23678 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30013 23678 603 41 0 29972 0
vsize: 120052
[startup+320.009 s]
Raw data (loadavg): 1.01 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25287 0 0 0 31944 58 0 0 25 0 1 0 483437673 122933248 23689 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30013 23689 603 41 0 29972 0
vsize: 120052
[startup+330.01 s]
Raw data (loadavg): 1.01 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25302 0 0 0 32944 58 0 0 25 0 1 0 483437673 122933248 23704 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30013 23704 603 41 0 29972 0
vsize: 120052
[startup+340.01 s]
Raw data (loadavg): 1.01 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25312 0 0 0 33945 58 0 0 25 0 1 0 483437673 123064320 23714 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30045 23714 603 41 0 30004 0
vsize: 120180
[startup+350.01 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25323 0 0 0 34945 58 0 0 25 0 1 0 483437673 123064320 23725 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30045 23725 603 41 0 30004 0
vsize: 120180
[startup+360.01 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25334 0 0 0 35945 58 0 0 25 0 1 0 483437673 123064320 23736 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30045 23736 603 41 0 30004 0
vsize: 120180
[startup+370.011 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25343 0 0 0 36945 58 0 0 25 0 1 0 483437673 123199488 23745 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30078 23745 603 41 0 30037 0
vsize: 120312
[startup+380.011 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25353 0 0 0 37945 58 0 0 25 0 1 0 483437673 123199488 23755 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30078 23755 603 41 0 30037 0
vsize: 120312
[startup+390.012 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25362 0 0 0 38945 58 0 0 25 0 1 0 483437673 123199488 23764 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30078 23764 603 41 0 30037 0
vsize: 120312
[startup+400.011 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25373 0 0 0 39945 58 0 0 25 0 1 0 483437673 123330560 23775 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30110 23775 603 41 0 30069 0
vsize: 120440
[startup+410.012 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25384 0 0 0 40946 58 0 0 25 0 1 0 483437673 123330560 23786 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30110 23786 603 41 0 30069 0
vsize: 120440
[startup+420.013 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25393 0 0 0 41946 58 0 0 25 0 1 0 483437673 123330560 23795 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30110 23795 603 41 0 30069 0
vsize: 120440
[startup+430.014 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32670
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25404 0 0 0 42946 58 0 0 25 0 1 0 483437673 123461632 23806 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30142 23806 603 41 0 30101 0
vsize: 120568
[startup+440.014 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25413 0 0 0 43946 58 0 0 25 0 1 0 483437673 123461632 23815 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30142 23815 603 41 0 30101 0
vsize: 120568
[startup+450.013 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25422 0 0 0 44946 58 0 0 25 0 1 0 483437673 123461632 23824 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30142 23824 603 41 0 30101 0
vsize: 120568
[startup+460.014 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25432 0 0 0 45946 58 0 0 25 0 1 0 483437673 123461632 23834 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30142 23834 603 41 0 30101 0
vsize: 120568
[startup+470.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25443 0 0 0 46947 58 0 0 25 0 1 0 483437673 123592704 23845 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30174 23845 603 41 0 30133 0
vsize: 120696
[startup+480.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25453 0 0 0 47947 58 0 0 25 0 1 0 483437673 123592704 23855 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30174 23855 603 41 0 30133 0
vsize: 120696
[startup+490.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25464 0 0 0 48947 58 0 0 25 0 1 0 483437673 123592704 23866 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30174 23866 603 41 0 30133 0
vsize: 120696
[startup+500.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25473 0 0 0 49947 58 0 0 25 0 1 0 483437673 123723776 23875 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30206 23875 603 41 0 30165 0
vsize: 120824
[startup+510.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25484 0 0 0 50947 58 0 0 25 0 1 0 483437673 123723776 23886 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30206 23886 603 41 0 30165 0
vsize: 120824
[startup+520.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25497 0 0 0 51947 59 0 0 25 0 1 0 483437673 123871232 23899 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30242 23899 603 41 0 30201 0
vsize: 120968
[startup+530.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25505 0 0 0 52948 59 0 0 25 0 1 0 483437673 123871232 23907 4294967295 134512640 134672761 3221224528 3221223728 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30242 23907 603 41 0 30201 0
vsize: 120968
[startup+540.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25517 0 0 0 53947 59 0 0 25 0 1 0 483437673 123871232 23919 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30242 23919 603 41 0 30201 0
vsize: 120968
[startup+550.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25530 0 0 0 54947 59 0 0 25 0 1 0 483437673 124026880 23932 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30280 23932 603 41 0 30239 0
vsize: 121120
[startup+560.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25543 0 0 0 55947 59 0 0 25 0 1 0 483437673 124026880 23945 4294967295 134512640 134672761 3221224528 3221223712 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30280 23945 603 41 0 30239 0
vsize: 121120
[startup+570.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25555 0 0 0 56947 59 0 0 25 0 1 0 483437673 124026880 23957 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30280 23957 603 41 0 30239 0
vsize: 121120
[startup+580.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25567 0 0 0 57947 59 0 0 25 0 1 0 483437673 124157952 23969 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30312 23969 603 41 0 30271 0
vsize: 121248
[startup+590.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25578 0 0 0 58948 59 0 0 25 0 1 0 483437673 124157952 23980 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30312 23980 603 41 0 30271 0
vsize: 121248
[startup+600.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25591 0 0 0 59948 59 0 0 25 0 1 0 483437673 124157952 23993 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30312 23993 603 41 0 30271 0
vsize: 121248
[startup+610.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25602 0 0 0 60948 60 0 0 25 0 1 0 483437673 124289024 24004 4294967295 134512640 134672761 3221224528 3221223632 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30344 24004 603 41 0 30303 0
vsize: 121376
[startup+620.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25614 0 0 0 61948 60 0 0 25 0 1 0 483437673 124289024 24016 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30344 24016 603 41 0 30303 0
vsize: 121376
[startup+630.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25627 0 0 0 62948 60 0 0 25 0 1 0 483437673 124424192 24029 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30377 24029 603 41 0 30336 0
vsize: 121508
[startup+640.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25637 0 0 0 63948 60 0 0 25 0 1 0 483437673 124424192 24039 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30377 24039 603 41 0 30336 0
vsize: 121508
[startup+650.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25651 0 0 0 64948 60 0 0 25 0 1 0 483437673 124424192 24053 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30377 24053 603 41 0 30336 0
vsize: 121508
[startup+660.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25663 0 0 0 65948 60 0 0 25 0 1 0 483437673 124555264 24065 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30409 24065 603 41 0 30368 0
vsize: 121636
[startup+670.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25673 0 0 0 66948 60 0 0 25 0 1 0 483437673 124555264 24075 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30409 24075 603 41 0 30368 0
vsize: 121636
[startup+680.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25688 0 0 0 67948 60 0 0 25 0 1 0 483437673 124555264 24090 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30409 24090 603 41 0 30368 0
vsize: 121636
[startup+690.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25694 0 0 0 68948 60 0 0 25 0 1 0 483437673 124686336 24096 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30441 24096 603 41 0 30400 0
vsize: 121764
[startup+700.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25705 0 0 0 69949 60 0 0 25 0 1 0 483437673 124686336 24107 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30441 24107 603 41 0 30400 0
vsize: 121764
[startup+710.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25715 0 0 0 70949 60 0 0 25 0 1 0 483437673 124686336 24117 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30441 24117 603 41 0 30400 0
vsize: 121764
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25725 0 0 0 71949 60 0 0 25 0 1 0 483437673 124821504 24127 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30474 24127 603 41 0 30433 0
vsize: 121896
[startup+730.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25735 0 0 0 72949 60 0 0 25 0 1 0 483437673 124821504 24137 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30474 24137 603 41 0 30433 0
vsize: 121896
[startup+740.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25745 0 0 0 73949 60 0 0 25 0 1 0 483437673 124821504 24147 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30474 24147 603 41 0 30433 0
vsize: 121896
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25754 0 0 0 74950 60 0 0 25 0 1 0 483437673 124821504 24156 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30474 24156 603 41 0 30433 0
vsize: 121896
[startup+760.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25766 0 0 0 75950 60 0 0 25 0 1 0 483437673 124952576 24168 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30506 24168 603 41 0 30465 0
vsize: 122024
[startup+770.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25774 0 0 0 76950 60 0 0 25 0 1 0 483437673 124952576 24176 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30506 24176 603 41 0 30465 0
vsize: 122024
[startup+780.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25785 0 0 0 77950 60 0 0 25 0 1 0 483437673 124952576 24187 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30506 24187 603 41 0 30465 0
vsize: 122024
[startup+790.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25792 0 0 0 78950 60 0 0 25 0 1 0 483437673 125083648 24194 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30538 24194 603 41 0 30497 0
vsize: 122152
[startup+800.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25803 0 0 0 79950 60 0 0 25 0 1 0 483437673 125083648 24205 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30538 24205 603 41 0 30497 0
vsize: 122152
[startup+810.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25812 0 0 0 80950 60 0 0 25 0 1 0 483437673 125083648 24214 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30538 24214 603 41 0 30497 0
vsize: 122152
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25821 0 0 0 81951 60 0 0 25 0 1 0 483437673 125210624 24223 4294967295 134512640 134672761 3221224528 3221223664 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30569 24223 603 41 0 30528 0
vsize: 122276
[startup+830.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25829 0 0 0 82951 60 0 0 25 0 1 0 483437673 125210624 24231 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30569 24231 603 41 0 30528 0
vsize: 122276
[startup+840.022 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25838 0 0 0 83951 60 0 0 25 0 1 0 483437673 125210624 24240 4294967295 134512640 134672761 3221224528 3221223632 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30569 24240 603 41 0 30528 0
vsize: 122276
[startup+850.022 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25847 0 0 0 84951 60 0 0 25 0 1 0 483437673 125210624 24249 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30569 24249 603 41 0 30528 0
vsize: 122276
[startup+860.022 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25854 0 0 0 85950 60 0 0 25 0 1 0 483437673 125345792 24256 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30602 24256 603 41 0 30561 0
vsize: 122408
[startup+870.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25866 0 0 0 86950 60 0 0 25 0 1 0 483437673 125345792 24268 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30602 24268 603 41 0 30561 0
vsize: 122408
[startup+880.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25876 0 0 0 87950 60 0 0 25 0 1 0 483437673 125345792 24278 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30602 24278 603 41 0 30561 0
vsize: 122408
[startup+890.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25885 0 0 0 88950 60 0 0 25 0 1 0 483437673 125480960 24287 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30635 24287 603 41 0 30594 0
vsize: 122540
[startup+900.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25895 0 0 0 89951 60 0 0 25 0 1 0 483437673 125480960 24297 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30635 24297 603 41 0 30594 0
vsize: 122540
[startup+910.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25904 0 0 0 90951 60 0 0 25 0 1 0 483437673 125480960 24306 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30635 24306 603 41 0 30594 0
vsize: 122540
[startup+920.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25913 0 0 0 91951 60 0 0 25 0 1 0 483437673 125480960 24315 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30635 24315 603 41 0 30594 0
vsize: 122540
[startup+930.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25921 0 0 0 92951 60 0 0 25 0 1 0 483437673 125612032 24323 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30667 24323 603 41 0 30626 0
vsize: 122668
[startup+940.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25931 0 0 0 93951 61 0 0 25 0 1 0 483437673 125612032 24333 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30667 24333 603 41 0 30626 0
vsize: 122668
[startup+950.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25940 0 0 0 94951 61 0 0 25 0 1 0 483437673 125612032 24342 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30667 24342 603 41 0 30626 0
vsize: 122668
[startup+960.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25958 0 0 0 95951 61 0 0 25 0 1 0 483437673 125755392 24360 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30702 24360 603 41 0 30661 0
vsize: 122808
[startup+970.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25967 0 0 0 96951 61 0 0 25 0 1 0 483437673 125755392 24369 4294967295 134512640 134672761 3221224528 3221223728 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30702 24369 603 41 0 30661 0
vsize: 122808
[startup+980.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25975 0 0 0 97952 61 0 0 25 0 1 0 483437673 125755392 24377 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30702 24377 603 41 0 30661 0
vsize: 122808
[startup+990.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 25988 0 0 0 98952 61 0 0 25 0 1 0 483437673 125886464 24390 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30734 24390 603 41 0 30693 0
vsize: 122936
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26000 0 0 0 99952 61 0 0 25 0 1 0 483437673 125886464 24402 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30734 24402 603 41 0 30693 0
vsize: 122936
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26011 0 0 0 100952 61 0 0 25 0 1 0 483437673 125886464 24413 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30734 24413 603 41 0 30693 0
vsize: 122936
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26022 0 0 0 101952 61 0 0 25 0 1 0 483437673 126021632 24424 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30767 24424 603 41 0 30726 0
vsize: 123068
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26032 0 0 0 102952 61 0 0 25 0 1 0 483437673 126021632 24434 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30767 24434 603 41 0 30726 0
vsize: 123068
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26040 0 0 0 103952 61 0 0 25 0 1 0 483437673 126021632 24442 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30767 24442 603 41 0 30726 0
vsize: 123068
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26049 0 0 0 104953 61 0 0 25 0 1 0 483437673 126152704 24451 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30799 24451 603 41 0 30758 0
vsize: 123196
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26057 0 0 0 105953 61 0 0 25 0 1 0 483437673 126152704 24459 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30799 24459 603 41 0 30758 0
vsize: 123196
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26066 0 0 0 106953 61 0 0 25 0 1 0 483437673 126152704 24468 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30799 24468 603 41 0 30758 0
vsize: 123196
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26074 0 0 0 107953 61 0 0 25 0 1 0 483437673 126152704 24476 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30799 24476 603 41 0 30758 0
vsize: 123196
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26083 0 0 0 108953 61 0 0 25 0 1 0 483437673 126287872 24485 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30832 24485 603 41 0 30791 0
vsize: 123328
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26091 0 0 0 109953 61 0 0 25 0 1 0 483437673 126287872 24493 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30832 24493 603 41 0 30791 0
vsize: 123328
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26100 0 0 0 110953 61 0 0 25 0 1 0 483437673 126287872 24502 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30832 24502 603 41 0 30791 0
vsize: 123328
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26111 0 0 0 111953 61 0 0 25 0 1 0 483437673 126418944 24513 4294967295 134512640 134672761 3221224528 3221223712 134559166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30864 24513 603 41 0 30823 0
vsize: 123456
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26121 0 0 0 112954 61 0 0 25 0 1 0 483437673 126418944 24523 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30864 24523 603 41 0 30823 0
vsize: 123456
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26135 0 0 0 113954 62 0 0 25 0 1 0 483437673 126418944 24537 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30864 24537 603 41 0 30823 0
vsize: 123456
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26159 0 0 0 114954 62 0 0 25 0 1 0 483437673 126685184 24561 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30929 24561 603 41 0 30888 0
vsize: 123716
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26160 0 0 0 115954 62 0 0 25 0 1 0 483437673 126685184 24562 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30929 24562 603 41 0 30888 0
vsize: 123716
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26165 0 0 0 116954 62 0 0 25 0 1 0 483437673 126685184 24567 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30929 24567 603 41 0 30888 0
vsize: 123716
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26177 0 0 0 117954 62 0 0 25 0 1 0 483437673 126685184 24579 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30929 24579 603 41 0 30888 0
vsize: 123716
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26188 0 0 0 118954 62 0 0 25 0 1 0 483437673 126685184 24590 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30929 24590 603 41 0 30888 0
vsize: 123716
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 32672
Raw data (stat): 32615 (minisat+) R 32614 30854 30853 0 -1 0 26200 0 0 0 119954 62 0 0 25 0 1 0 483437673 126820352 24602 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30962 24602 603 41 0 30921 0
vsize: 123848
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.97 1/54 32672
Raw data (stat): 32615 (minisat+) Z 32614 30854 30853 0 -1 12 26203 0 0 0 119954 67 0 0 25 0 1 0 483437673 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.08
CPU time (s): 1200.22
CPU user time (s): 1199.55
CPU system time (s): 0.672897
CPU usage (%): 100.012
Max. virtual memory (Kb): 123848
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####