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/primes-dimacs-cnf/normalized-f600.opb
MD5SUM	4fdec182582ed31d1ae371090f6cc5c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	1200
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1200
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1200
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	1200
Total number of constraints	3150
Number of constraints which are clauses	3150
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	3
Trace number 6192

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 03:47:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4641 boxname=wulflinc12 idbench=129 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fdec182582ed31d1ae371090f6cc5c1  /oldhome/oroussel/tmp/wulflinc12/normalized-f600.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc12/normalized-f600.opb /oldhome/oroussel/tmp/wulflinc12/normalized-f600.opb
IDLAUNCH: 4641
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        900888 kB
Buffers:         35960 kB
Cached:          78332 kB
SwapCached:         16 kB
Active:          62192 kB
Inactive:        54928 kB
HighTotal:      131008 kB
HighFree:        48776 kB
LowTotal:       903652 kB
LowFree:        852112 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11068 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:07:37 (client local time) WITH STATUS 0 IN 1200.09 SECONDS
stats: 4641 7 1200.09 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3150 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 |    3150     8850 |    1050       0        0     nan |  0.000 % |
c |       102 |    3150     8850 |    1155     102     3292    32.3 |  0.000 % |
c |       253 |    3150     8850 |    1270     253     8611    34.0 |  0.000 % |
c |       478 |    3150     8850 |    1397     478    15852    33.2 |  0.000 % |
c |       817 |    3150     8850 |    1537     817    26836    32.8 |  0.000 % |
c |      1324 |    3150     8850 |    1691    1324    41380    31.3 |  0.000 % |
c |      2084 |    3150     8850 |    1860    1198    32243    26.9 |  0.000 % |
c |      3224 |    3150     8850 |    2046    1363    35898    26.3 |  0.000 % |
c |      4932 |    3150     8850 |    2250    2020    52177    25.8 |  0.000 % |
c |      7495 |    3150     8850 |    2475    2231    61073    27.4 |  0.000 % |
c |     11339 |    3150     8850 |    2723    2199    56842    25.8 |  0.000 % |
c |     17106 |    3150     8850 |    2995    2299    59391    25.8 |  0.000 % |
c |     25755 |    3150     8850 |    3295    1606    44453    27.7 |  0.000 % |
c |     38729 |    3150     8850 |    3624    2649    77155    29.1 |  0.000 % |
c |     58190 |    3150     8850 |    3987    3488    99761    28.6 |  0.000 % |
c |     87383 |    3150     8850 |    4386    4024   109027    27.1 |  0.000 % |
c |    131172 |    3150     8850 |    4824    2806    82033    29.2 |  0.000 % |
c |    196857 |    3150     8850 |    5307    4322   119220    27.6 |  0.000 % |
c |    295383 |    3150     8850 |    5837    4888   145414    29.7 |  0.000 % |
c |    443173 |    3150     8850 |    6421    3557   104634    29.4 |  0.000 % |
c |    664858 |    3150     8850 |    7063    5936   187586    31.6 |  0.000 % |
c |    997383 |    3150     8850 |    7770    4394   120752    27.5 |  0.000 % |
c |   1496174 |    3150     8850 |    8547    6921   191716    27.7 |  0.000 % |
c |   2244356 |    3150     8850 |    9402    5643   161794    28.7 |  0.000 % |
#### 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.45 0.81 0.88 2/54 31859
Raw data (stat): 31859 (runsolver) R 31858 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423242896 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+10.0012 s]
Raw data (loadavg): 0.53 0.82 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 629 0 0 0 996 1 0 0 25 0 1 0 423242896 4100096 607 4294967295 134512640 134672761 3221224576 3221223680 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1001 607 603 41 0 960 0
vsize: 4004
[startup+20.002 s]
Raw data (loadavg): 0.61 0.82 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 683 0 0 0 1996 2 0 0 25 0 1 0 423242896 4366336 661 4294967295 134512640 134672761 3221224576 3221223712 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1066 661 603 41 0 1025 0
vsize: 4264
[startup+30.0024 s]
Raw data (loadavg): 0.67 0.83 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 735 0 0 0 2995 2 0 0 25 0 1 0 423242896 4501504 713 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1099 713 603 41 0 1058 0
vsize: 4396
[startup+40.0028 s]
Raw data (loadavg): 0.72 0.83 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 786 0 0 0 3995 2 0 0 25 0 1 0 423242896 4767744 764 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1164 764 603 41 0 1123 0
vsize: 4656
[startup+50.0046 s]
Raw data (loadavg): 0.76 0.84 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 826 0 0 0 4994 3 0 0 25 0 1 0 423242896 4902912 804 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1197 804 603 41 0 1156 0
vsize: 4788
[startup+60.0054 s]
Raw data (loadavg): 0.80 0.84 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 865 0 0 0 5994 3 0 0 25 0 1 0 423242896 5038080 843 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1230 843 603 41 0 1189 0
vsize: 4920
[startup+70.0062 s]
Raw data (loadavg): 0.83 0.85 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 885 0 0 0 6993 4 0 0 25 0 1 0 423242896 5173248 863 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1263 863 603 41 0 1222 0
vsize: 5052
[startup+80.007 s]
Raw data (loadavg): 0.85 0.85 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 924 0 0 0 7993 4 0 0 25 0 1 0 423242896 5308416 902 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1296 902 603 41 0 1255 0
vsize: 5184
[startup+90.0074 s]
Raw data (loadavg): 0.88 0.86 0.88 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 938 0 0 0 8992 5 0 0 25 0 1 0 423242896 5308416 916 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1296 916 603 41 0 1255 0
vsize: 5184
[startup+100.009 s]
Raw data (loadavg): 0.89 0.86 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 951 0 0 0 9992 5 0 0 25 0 1 0 423242896 5443584 929 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1329 929 603 41 0 1288 0
vsize: 5316
[startup+110.01 s]
Raw data (loadavg): 0.91 0.86 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 957 0 0 0 10992 5 0 0 25 0 1 0 423242896 5443584 935 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1329 935 603 41 0 1288 0
vsize: 5316
[startup+120.01 s]
Raw data (loadavg): 0.92 0.87 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1017 0 0 0 11991 6 0 0 25 0 1 0 423242896 5709824 995 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1394 995 603 41 0 1353 0
vsize: 5576
[startup+130.011 s]
Raw data (loadavg): 0.93 0.87 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1027 0 0 0 12991 6 0 0 25 0 1 0 423242896 5713920 1005 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1395 1005 603 41 0 1354 0
vsize: 5580
[startup+140.012 s]
Raw data (loadavg): 0.94 0.88 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1052 0 0 0 13990 7 0 0 25 0 1 0 423242896 5844992 1030 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1427 1030 603 41 0 1386 0
vsize: 5708
[startup+150.013 s]
Raw data (loadavg): 0.95 0.88 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1065 0 0 0 14990 7 0 0 25 0 1 0 423242896 5844992 1043 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1427 1043 603 41 0 1386 0
vsize: 5708
[startup+160.014 s]
Raw data (loadavg): 0.96 0.88 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1081 0 0 0 15990 7 0 0 25 0 1 0 423242896 5984256 1059 4294967295 134512640 134672761 3221224576 3221223532 1075349836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1461 1059 603 41 0 1420 0
vsize: 5844
[startup+170.014 s]
Raw data (loadavg): 0.96 0.89 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1088 0 0 0 16989 8 0 0 25 0 1 0 423242896 5984256 1066 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1461 1066 603 41 0 1420 0
vsize: 5844
[startup+180.014 s]
Raw data (loadavg): 0.97 0.89 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1120 0 0 0 17989 8 0 0 25 0 1 0 423242896 6119424 1098 4294967295 134512640 134672761 3221224576 3221223680 134555244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1494 1098 603 41 0 1453 0
vsize: 5976
[startup+190.022 s]
Raw data (loadavg): 0.97 0.89 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1151 0 0 0 18989 8 0 0 25 0 1 0 423242896 6254592 1129 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1527 1129 603 41 0 1486 0
vsize: 6108
[startup+200.023 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1159 0 0 0 19989 9 0 0 25 0 1 0 423242896 6254592 1137 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1527 1137 603 41 0 1486 0
vsize: 6108
[startup+210.023 s]
Raw data (loadavg): 0.98 0.90 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1166 0 0 0 20988 9 0 0 25 0 1 0 423242896 6254592 1144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1527 1144 603 41 0 1486 0
vsize: 6108
[startup+220.024 s]
Raw data (loadavg): 0.98 0.90 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1186 0 0 0 21988 9 0 0 25 0 1 0 423242896 6389760 1164 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1560 1164 603 41 0 1519 0
vsize: 6240
[startup+230.026 s]
Raw data (loadavg): 0.98 0.90 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1196 0 0 0 22988 10 0 0 25 0 1 0 423242896 6389760 1174 4294967295 134512640 134672761 3221224576 3221223712 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1560 1174 603 41 0 1519 0
vsize: 6240
[startup+240.026 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1209 0 0 0 23987 10 0 0 25 0 1 0 423242896 6524928 1187 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1593 1187 603 41 0 1552 0
vsize: 6372
[startup+250.028 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1222 0 0 0 24987 10 0 0 25 0 1 0 423242896 6524928 1200 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1593 1200 603 41 0 1552 0
vsize: 6372
[startup+260.028 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1236 0 0 0 25987 11 0 0 25 0 1 0 423242896 6672384 1214 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1214 603 41 0 1588 0
vsize: 6516
[startup+270.027 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1249 0 0 0 26986 11 0 0 25 0 1 0 423242896 6672384 1227 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1227 603 41 0 1588 0
vsize: 6516
[startup+280.029 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1262 0 0 0 27986 12 0 0 25 0 1 0 423242896 6672384 1240 4294967295 134512640 134672761 3221224576 3221223532 1075350054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1240 603 41 0 1588 0
vsize: 6516
[startup+290.029 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1280 0 0 0 28985 12 0 0 25 0 1 0 423242896 6807552 1258 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1662 1258 603 41 0 1621 0
vsize: 6648
[startup+300.03 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1291 0 0 0 29985 12 0 0 25 0 1 0 423242896 6807552 1269 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1662 1269 603 41 0 1621 0
vsize: 6648
[startup+310.031 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1312 0 0 0 30984 13 0 0 25 0 1 0 423242896 6942720 1290 4294967295 134512640 134672761 3221224576 3221223712 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1695 1290 603 41 0 1654 0
vsize: 6780
[startup+320.031 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1322 0 0 0 31983 13 0 0 25 0 1 0 423242896 6942720 1300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1695 1300 603 41 0 1654 0
vsize: 6780
[startup+330.031 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1322 0 0 0 32983 13 0 0 25 0 1 0 423242896 6942720 1300 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1695 1300 603 41 0 1654 0
vsize: 6780
[startup+340.033 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1326 0 0 0 33983 14 0 0 25 0 1 0 423242896 6942720 1304 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1695 1304 603 41 0 1654 0
vsize: 6780
[startup+350.033 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1332 0 0 0 34983 14 0 0 25 0 1 0 423242896 6942720 1310 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1695 1310 603 41 0 1654 0
vsize: 6780
[startup+360.034 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1338 0 0 0 35983 14 0 0 25 0 1 0 423242896 7090176 1316 4294967295 134512640 134672761 3221224576 3221223532 1075349761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1731 1316 603 41 0 1690 0
vsize: 6924
[startup+370.034 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1345 0 0 0 36982 15 0 0 25 0 1 0 423242896 7090176 1323 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1731 1323 603 41 0 1690 0
vsize: 6924
[startup+380.035 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1357 0 0 0 37982 15 0 0 25 0 1 0 423242896 7090176 1335 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1731 1335 603 41 0 1690 0
vsize: 6924
[startup+390.034 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1368 0 0 0 38981 15 0 0 25 0 1 0 423242896 7225344 1346 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1346 603 41 0 1723 0
vsize: 7056
[startup+400.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1370 0 0 0 39981 16 0 0 25 0 1 0 423242896 7225344 1348 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1348 603 41 0 1723 0
vsize: 7056
[startup+410.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1370 0 0 0 40981 16 0 0 25 0 1 0 423242896 7225344 1348 4294967295 134512640 134672761 3221224576 3221223712 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1348 603 41 0 1723 0
vsize: 7056
[startup+420.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1375 0 0 0 41980 16 0 0 25 0 1 0 423242896 7225344 1353 4294967295 134512640 134672761 3221224576 3221223680 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1353 603 41 0 1723 0
vsize: 7056
[startup+430.037 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1386 0 0 0 42980 17 0 0 25 0 1 0 423242896 7225344 1364 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1364 603 41 0 1723 0
vsize: 7056
[startup+440.038 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1421 0 0 0 43979 17 0 0 25 0 1 0 423242896 7360512 1399 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1797 1399 603 41 0 1756 0
vsize: 7188
[startup+450.039 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1437 0 0 0 44979 17 0 0 25 0 1 0 423242896 7495680 1415 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1830 1415 603 41 0 1789 0
vsize: 7320
[startup+460.04 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1455 0 0 0 45979 18 0 0 25 0 1 0 423242896 7495680 1433 4294967295 134512640 134672761 3221224576 3221223088 134565831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1830 1433 603 41 0 1789 0
vsize: 7320
[startup+470.039 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1466 0 0 0 46978 19 0 0 25 0 1 0 423242896 7630848 1444 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1863 1444 603 41 0 1822 0
vsize: 7452
[startup+480.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1473 0 0 0 47978 19 0 0 25 0 1 0 423242896 7630848 1451 4294967295 134512640 134672761 3221224576 3221223728 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1863 1451 603 41 0 1822 0
vsize: 7452
[startup+490.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1487 0 0 0 48977 19 0 0 25 0 1 0 423242896 7630848 1465 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1863 1465 603 41 0 1822 0
vsize: 7452
[startup+500.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1490 0 0 0 49977 20 0 0 25 0 1 0 423242896 7770112 1468 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1897 1468 603 41 0 1856 0
vsize: 7588
[startup+510.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1495 0 0 0 50976 20 0 0 25 0 1 0 423242896 7770112 1473 4294967295 134512640 134672761 3221224576 3221223712 134565054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1473 603 41 0 1856 0
vsize: 7588
[startup+520.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1498 0 0 0 51976 20 0 0 25 0 1 0 423242896 7770112 1476 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1476 603 41 0 1856 0
vsize: 7588
[startup+530.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1513 0 0 0 52977 20 0 0 25 0 1 0 423242896 7770112 1491 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1491 603 41 0 1856 0
vsize: 7588
[startup+540.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1524 0 0 0 53977 20 0 0 25 0 1 0 423242896 7901184 1502 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1502 603 41 0 1888 0
vsize: 7716
[startup+550.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1532 0 0 0 54977 20 0 0 25 0 1 0 423242896 7901184 1510 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1510 603 41 0 1888 0
vsize: 7716
[startup+560.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1538 0 0 0 55977 20 0 0 25 0 1 0 423242896 7901184 1516 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1516 603 41 0 1888 0
vsize: 7716
[startup+570.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1544 0 0 0 56977 20 0 0 25 0 1 0 423242896 7901184 1522 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1522 603 41 0 1888 0
vsize: 7716
[startup+580.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1546 0 0 0 57977 20 0 0 25 0 1 0 423242896 7901184 1524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1524 603 41 0 1888 0
vsize: 7716
[startup+590.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1548 0 0 0 58978 20 0 0 25 0 1 0 423242896 7901184 1526 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1526 603 41 0 1888 0
vsize: 7716
[startup+600.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1566 0 0 0 59978 20 0 0 25 0 1 0 423242896 8036352 1544 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1544 603 41 0 1921 0
vsize: 7848
[startup+610.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1572 0 0 0 60978 20 0 0 25 0 1 0 423242896 8036352 1550 4294967295 134512640 134672761 3221224576 3221223616 1075349627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1550 603 41 0 1921 0
vsize: 7848
[startup+620.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1581 0 0 0 61978 20 0 0 25 0 1 0 423242896 8036352 1559 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1559 603 41 0 1921 0
vsize: 7848
[startup+630.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1585 0 0 0 62978 20 0 0 25 0 1 0 423242896 8175616 1563 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1563 603 41 0 1955 0
vsize: 7984
[startup+640.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1585 0 0 0 63978 20 0 0 25 0 1 0 423242896 8175616 1563 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1563 603 41 0 1955 0
vsize: 7984
[startup+650.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1589 0 0 0 64978 20 0 0 25 0 1 0 423242896 8175616 1567 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1567 603 41 0 1955 0
vsize: 7984
[startup+660.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1600 0 0 0 65979 20 0 0 25 0 1 0 423242896 8175616 1578 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1578 603 41 0 1955 0
vsize: 7984
[startup+670.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1601 0 0 0 66979 20 0 0 25 0 1 0 423242896 8175616 1579 4294967295 134512640 134672761 3221224576 3221223672 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1579 603 41 0 1955 0
vsize: 7984
[startup+680.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1630 0 0 0 67977 21 0 0 25 0 1 0 423242896 8310784 1608 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2029 1608 603 41 0 1988 0
vsize: 8116
[startup+690.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1643 0 0 0 68978 21 0 0 25 0 1 0 423242896 8310784 1621 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2029 1621 603 41 0 1988 0
vsize: 8116
[startup+700.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1649 0 0 0 69978 21 0 0 25 0 1 0 423242896 8458240 1627 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1627 603 41 0 2024 0
vsize: 8260
[startup+710.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1661 0 0 0 70978 21 0 0 25 0 1 0 423242896 8458240 1639 4294967295 134512640 134672761 3221224576 3221223532 1075349950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1639 603 41 0 2024 0
vsize: 8260
[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1667 0 0 0 71978 21 0 0 25 0 1 0 423242896 8458240 1645 4294967295 134512640 134672761 3221224576 3221223668 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1645 603 41 0 2024 0
vsize: 8260
[startup+730.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1673 0 0 0 72978 21 0 0 25 0 1 0 423242896 8458240 1651 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1651 603 41 0 2024 0
vsize: 8260
[startup+740.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31859
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1676 0 0 0 73979 21 0 0 25 0 1 0 423242896 8597504 1654 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1654 603 41 0 2058 0
vsize: 8396
[startup+750.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31863
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1680 0 0 0 74979 21 0 0 25 0 1 0 423242896 8597504 1658 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1658 603 41 0 2058 0
vsize: 8396
[startup+760.049 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31912
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1698 0 0 0 75979 21 0 0 25 0 1 0 423242896 8597504 1676 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1676 603 41 0 2058 0
vsize: 8396
[startup+770.049 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31912
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1698 0 0 0 76979 21 0 0 25 0 1 0 423242896 8597504 1676 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1676 603 41 0 2058 0
vsize: 8396
[startup+780.051 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31912
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1699 0 0 0 77979 21 0 0 25 0 1 0 423242896 8597504 1677 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1677 603 41 0 2058 0
vsize: 8396
[startup+790.051 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31912
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1709 0 0 0 78979 21 0 0 25 0 1 0 423242896 8732672 1687 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1687 603 41 0 2091 0
vsize: 8528
[startup+800.052 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31912
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1717 0 0 0 79980 21 0 0 25 0 1 0 423242896 8732672 1695 4294967295 134512640 134672761 3221224576 3221223712 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1695 603 41 0 2091 0
vsize: 8528
[startup+810.052 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31912
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1721 0 0 0 80980 21 0 0 25 0 1 0 423242896 8732672 1699 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1699 603 41 0 2091 0
vsize: 8528
[startup+820.053 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31912
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1725 0 0 0 81980 21 0 0 25 0 1 0 423242896 8732672 1703 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1703 603 41 0 2091 0
vsize: 8528
[startup+830.053 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1729 0 0 0 82980 21 0 0 25 0 1 0 423242896 8732672 1707 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1707 603 41 0 2091 0
vsize: 8528
[startup+840.053 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1737 0 0 0 83980 21 0 0 25 0 1 0 423242896 8732672 1715 4294967295 134512640 134672761 3221224576 3221223760 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1715 603 41 0 2091 0
vsize: 8528
[startup+850.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1740 0 0 0 84980 21 0 0 25 0 1 0 423242896 8867840 1718 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1718 603 41 0 2124 0
vsize: 8660
[startup+860.054 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1744 0 0 0 85981 21 0 0 25 0 1 0 423242896 8867840 1722 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1722 603 41 0 2124 0
vsize: 8660
[startup+870.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1747 0 0 0 86981 21 0 0 25 0 1 0 423242896 8867840 1725 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1725 603 41 0 2124 0
vsize: 8660
[startup+880.055 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1747 0 0 0 87981 21 0 0 25 0 1 0 423242896 8867840 1725 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1725 603 41 0 2124 0
vsize: 8660
[startup+890.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1759 0 0 0 88981 22 0 0 25 0 1 0 423242896 8867840 1737 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1737 603 41 0 2124 0
vsize: 8660
[startup+900.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1765 0 0 0 89981 22 0 0 25 0 1 0 423242896 8867840 1743 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1743 603 41 0 2124 0
vsize: 8660
[startup+910.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1777 0 0 0 90982 22 0 0 25 0 1 0 423242896 9007104 1755 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2199 1755 603 41 0 2158 0
vsize: 8796
[startup+920.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1794 0 0 0 91982 22 0 0 25 0 1 0 423242896 9007104 1772 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2199 1772 603 41 0 2158 0
vsize: 8796
[startup+930.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1796 0 0 0 92982 22 0 0 25 0 1 0 423242896 9007104 1774 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2199 1774 603 41 0 2158 0
vsize: 8796
[startup+940.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1798 0 0 0 93982 22 0 0 25 0 1 0 423242896 9142272 1776 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1776 603 41 0 2191 0
vsize: 8928
[startup+950.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1801 0 0 0 94982 22 0 0 25 0 1 0 423242896 9142272 1779 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1779 603 41 0 2191 0
vsize: 8928
[startup+960.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1801 0 0 0 95982 22 0 0 25 0 1 0 423242896 9142272 1779 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1779 603 41 0 2191 0
vsize: 8928
[startup+970.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1801 0 0 0 96982 22 0 0 25 0 1 0 423242896 9142272 1779 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1779 603 41 0 2191 0
vsize: 8928
[startup+980.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1805 0 0 0 97983 22 0 0 25 0 1 0 423242896 9142272 1783 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1783 603 41 0 2191 0
vsize: 8928
[startup+990.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1812 0 0 0 98983 22 0 0 25 0 1 0 423242896 9142272 1790 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1790 603 41 0 2191 0
vsize: 8928
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1814 0 0 0 99983 22 0 0 25 0 1 0 423242896 9142272 1792 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1792 603 41 0 2191 0
vsize: 8928
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1817 0 0 0 100983 22 0 0 25 0 1 0 423242896 9142272 1795 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1795 603 41 0 2191 0
vsize: 8928
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1819 0 0 0 101983 22 0 0 25 0 1 0 423242896 9142272 1797 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1797 603 41 0 2191 0
vsize: 8928
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1827 0 0 0 102984 22 0 0 25 0 1 0 423242896 9142272 1805 4294967295 134512640 134672761 3221224576 3221223744 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1805 603 41 0 2191 0
vsize: 8928
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1837 0 0 0 103984 22 0 0 25 0 1 0 423242896 9277440 1815 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2265 1815 603 41 0 2224 0
vsize: 9060
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1844 0 0 0 104984 22 0 0 25 0 1 0 423242896 9277440 1822 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2265 1822 603 41 0 2224 0
vsize: 9060
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1866 0 0 0 105984 22 0 0 25 0 1 0 423242896 9412608 1844 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2298 1844 603 41 0 2257 0
vsize: 9192
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1878 0 0 0 106983 22 0 0 25 0 1 0 423242896 9412608 1856 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1856 603 41 0 2257 0
vsize: 9192
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31914
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1889 0 0 0 107983 22 0 0 25 0 1 0 423242896 9412608 1867 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1867 603 41 0 2257 0
vsize: 9192
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1889 0 0 0 108983 22 0 0 25 0 1 0 423242896 9412608 1867 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1867 603 41 0 2257 0
vsize: 9192
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1891 0 0 0 109984 22 0 0 25 0 1 0 423242896 9412608 1869 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1869 603 41 0 2257 0
vsize: 9192
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1895 0 0 0 110984 22 0 0 25 0 1 0 423242896 9551872 1873 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1873 603 41 0 2291 0
vsize: 9328
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1910 0 0 0 111984 22 0 0 25 0 1 0 423242896 9551872 1888 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1888 603 41 0 2291 0
vsize: 9328
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1911 0 0 0 112984 22 0 0 25 0 1 0 423242896 9551872 1889 4294967295 134512640 134672761 3221224576 3221223776 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1889 603 41 0 2291 0
vsize: 9328
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1916 0 0 0 113984 22 0 0 25 0 1 0 423242896 9551872 1894 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1894 603 41 0 2291 0
vsize: 9328
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1923 0 0 0 114984 22 0 0 25 0 1 0 423242896 9551872 1901 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1901 603 41 0 2291 0
vsize: 9328
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1931 0 0 0 115984 23 0 0 25 0 1 0 423242896 9699328 1909 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1909 603 41 0 2327 0
vsize: 9472
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1934 0 0 0 116985 23 0 0 25 0 1 0 423242896 9699328 1912 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1912 603 41 0 2327 0
vsize: 9472
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1938 0 0 0 117985 23 0 0 25 0 1 0 423242896 9699328 1916 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1916 603 41 0 2327 0
vsize: 9472
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1938 0 0 0 118985 23 0 0 25 0 1 0 423242896 9699328 1916 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1916 603 41 0 2327 0
vsize: 9472
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31916
Raw data (stat): 31859 (minisat+) R 31858 25285 25284 0 -1 0 1946 0 0 0 119985 23 0 0 25 0 1 0 423242896 9699328 1924 4294967295 134512640 134672761 3221224576 3221223728 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1924 603 41 0 2327 0
vsize: 9472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 31916
Raw data (stat): 31859 (minisat+) Z 31858 25285 25284 0 -1 12 1948 0 0 0 119985 23 0 0 25 0 1 0 423242896 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: 0
Real time (s): 1200.06
CPU time (s): 1200.09
CPU user time (s): 1199.86
CPU system time (s): 0.233964
CPU usage (%): 100.002
Max. virtual memory (Kb): 9472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####