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 5819

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 01:59:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4265 boxname=wulflinc2 idbench=129 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fdec182582ed31d1ae371090f6cc5c1  /oldhome/oroussel/tmp/wulflinc2/normalized-f600.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc2/normalized-f600.opb /oldhome/oroussel/tmp/wulflinc2/normalized-f600.opb
IDLAUNCH: 4265
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        898876 kB
Buffers:         35376 kB
Cached:          79608 kB
SwapCached:          4 kB
Active:          57684 kB
Inactive:        60136 kB
HighTotal:      131008 kB
HighFree:        47600 kB
LowTotal:       903652 kB
LowFree:        851276 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12212 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:19:29 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 4265 7 1200.16 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.52 0.84 0.87 2/54 25498
Raw data (stat): 25498 (runsolver) R 25497 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422598901 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.001 s]
Raw data (loadavg): 0.59 0.84 0.87 2/54 25498
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 629 0 0 0 996 2 0 0 25 0 1 0 422598901 4100096 607 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1001 607 603 41 0 960 0
vsize: 4004
[startup+20.0016 s]
Raw data (loadavg): 0.65 0.85 0.87 2/54 25498
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 684 0 0 0 1995 3 0 0 25 0 1 0 422598901 4370432 662 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1067 662 603 41 0 1026 0
vsize: 4268
[startup+30.0028 s]
Raw data (loadavg): 0.71 0.85 0.87 2/54 25498
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 736 0 0 0 2994 3 0 0 25 0 1 0 422598901 4505600 714 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1100 714 603 41 0 1059 0
vsize: 4400
[startup+40.0033 s]
Raw data (loadavg): 0.83 0.87 0.88 3/57 25536
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 787 0 0 0 3992 4 0 0 25 0 1 0 422598901 4771840 765 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1165 765 603 41 0 1124 0
vsize: 4660
[startup+50.004 s]
Raw data (loadavg): 0.86 0.88 0.88 2/54 25551
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 828 0 0 0 4993 4 0 0 25 0 1 0 422598901 4907008 806 4294967295 134512640 134672761 3221224560 3221223664 134555126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1198 806 603 41 0 1157 0
vsize: 4792
[startup+60.0045 s]
Raw data (loadavg): 0.88 0.88 0.88 2/54 25551
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 866 0 0 0 5993 4 0 0 25 0 1 0 422598901 5042176 844 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1231 844 603 41 0 1190 0
vsize: 4924
[startup+70.0055 s]
Raw data (loadavg): 0.90 0.89 0.88 2/54 25551
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 887 0 0 0 6993 4 0 0 25 0 1 0 422598901 5177344 865 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1264 865 603 41 0 1223 0
vsize: 5056
[startup+80.0059 s]
Raw data (loadavg): 0.91 0.89 0.88 2/54 25551
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 925 0 0 0 7993 4 0 0 25 0 1 0 422598901 5312512 903 4294967295 134512640 134672761 3221224560 3221223744 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1297 903 603 41 0 1256 0
vsize: 5188
[startup+90.0056 s]
Raw data (loadavg): 0.92 0.89 0.88 2/54 25551
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 939 0 0 0 8993 4 0 0 25 0 1 0 422598901 5312512 917 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1297 917 603 41 0 1256 0
vsize: 5188
[startup+100.005 s]
Raw data (loadavg): 0.94 0.89 0.88 2/54 25551
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 952 0 0 0 9993 4 0 0 25 0 1 0 422598901 5447680 930 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1330 930 603 41 0 1289 0
vsize: 5320
[startup+110.006 s]
Raw data (loadavg): 0.95 0.90 0.88 2/54 25551
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 961 0 0 0 10993 4 0 0 25 0 1 0 422598901 5447680 939 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1330 939 603 41 0 1289 0
vsize: 5320
[startup+120.006 s]
Raw data (loadavg): 0.95 0.90 0.88 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1020 0 0 0 11993 5 0 0 25 0 1 0 422598901 5713920 998 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1395 998 603 41 0 1354 0
vsize: 5580
[startup+130.007 s]
Raw data (loadavg): 0.96 0.90 0.88 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1031 0 0 0 12993 5 0 0 25 0 1 0 422598901 5713920 1009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1395 1009 603 41 0 1354 0
vsize: 5580
[startup+140.007 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1060 0 0 0 13993 5 0 0 25 0 1 0 422598901 5844992 1038 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1427 1038 603 41 0 1386 0
vsize: 5708
[startup+150.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1065 0 0 0 14994 5 0 0 25 0 1 0 422598901 5844992 1043 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1427 1043 603 41 0 1386 0
vsize: 5708
[startup+160.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1081 0 0 0 15994 5 0 0 25 0 1 0 422598901 5984256 1059 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1461 1059 603 41 0 1420 0
vsize: 5844
[startup+170.006 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1093 0 0 0 16994 5 0 0 25 0 1 0 422598901 5984256 1071 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1461 1071 603 41 0 1420 0
vsize: 5844
[startup+180.007 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1125 0 0 0 17994 5 0 0 25 0 1 0 422598901 6119424 1103 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1494 1103 603 41 0 1453 0
vsize: 5976
[startup+190.007 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1151 0 0 0 18994 5 0 0 25 0 1 0 422598901 6254592 1129 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1527 1129 603 41 0 1486 0
vsize: 6108
[startup+200.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1161 0 0 0 19994 5 0 0 25 0 1 0 422598901 6254592 1139 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1527 1139 603 41 0 1486 0
vsize: 6108
[startup+210.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1168 0 0 0 20994 5 0 0 25 0 1 0 422598901 6254592 1146 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1527 1146 603 41 0 1486 0
vsize: 6108
[startup+220.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1188 0 0 0 21994 5 0 0 25 0 1 0 422598901 6389760 1166 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1560 1166 603 41 0 1519 0
vsize: 6240
[startup+230.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1200 0 0 0 22995 5 0 0 25 0 1 0 422598901 6389760 1178 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1560 1178 603 41 0 1519 0
vsize: 6240
[startup+240.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1211 0 0 0 23995 5 0 0 25 0 1 0 422598901 6524928 1189 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1593 1189 603 41 0 1552 0
vsize: 6372
[startup+250.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1224 0 0 0 24995 5 0 0 25 0 1 0 422598901 6524928 1202 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1593 1202 603 41 0 1552 0
vsize: 6372
[startup+260.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1238 0 0 0 25995 5 0 0 25 0 1 0 422598901 6672384 1216 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1629 1216 603 41 0 1588 0
vsize: 6516
[startup+270.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1254 0 0 0 26995 5 0 0 25 0 1 0 422598901 6672384 1232 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1629 1232 603 41 0 1588 0
vsize: 6516
[startup+280.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1272 0 0 0 27995 5 0 0 25 0 1 0 422598901 6807552 1250 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1662 1250 603 41 0 1621 0
vsize: 6648
[startup+290.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1282 0 0 0 28995 5 0 0 25 0 1 0 422598901 6807552 1260 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1662 1260 603 41 0 1621 0
vsize: 6648
[startup+300.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1297 0 0 0 29995 5 0 0 25 0 1 0 422598901 6807552 1275 4294967295 134512640 134672761 3221224560 3221223744 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1662 1275 603 41 0 1621 0
vsize: 6648
[startup+310.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1314 0 0 0 30995 5 0 0 25 0 1 0 422598901 6942720 1292 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1695 1292 603 41 0 1654 0
vsize: 6780
[startup+320.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1322 0 0 0 31995 5 0 0 25 0 1 0 422598901 6942720 1300 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1695 1300 603 41 0 1654 0
vsize: 6780
[startup+330.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1326 0 0 0 32996 5 0 0 25 0 1 0 422598901 6942720 1304 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1695 1304 603 41 0 1654 0
vsize: 6780
[startup+340.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1328 0 0 0 33996 5 0 0 25 0 1 0 422598901 6942720 1306 4294967295 134512640 134672761 3221224560 3221223632 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1695 1306 603 41 0 1654 0
vsize: 6780
[startup+350.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1332 0 0 0 34996 5 0 0 25 0 1 0 422598901 6942720 1310 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1695 1310 603 41 0 1654 0
vsize: 6780
[startup+360.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1340 0 0 0 35996 5 0 0 25 0 1 0 422598901 7090176 1318 4294967295 134512640 134672761 3221224560 3221223744 134559683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1731 1318 603 41 0 1690 0
vsize: 6924
[startup+370.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1352 0 0 0 36996 5 0 0 25 0 1 0 422598901 7090176 1330 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1731 1330 603 41 0 1690 0
vsize: 6924
[startup+380.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25553
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1359 0 0 0 37996 5 0 0 25 0 1 0 422598901 7090176 1337 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1731 1337 603 41 0 1690 0
vsize: 6924
[startup+390.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1370 0 0 0 38997 5 0 0 25 0 1 0 422598901 7225344 1348 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1764 1348 603 41 0 1723 0
vsize: 7056
[startup+400.007 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1370 0 0 0 39997 5 0 0 25 0 1 0 422598901 7225344 1348 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1764 1348 603 41 0 1723 0
vsize: 7056
[startup+410.008 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1372 0 0 0 40996 6 0 0 25 0 1 0 422598901 7225344 1350 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1350 603 41 0 1723 0
vsize: 7056
[startup+420.008 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1381 0 0 0 41996 6 0 0 25 0 1 0 422598901 7225344 1359 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1764 1359 603 41 0 1723 0
vsize: 7056
[startup+430.01 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1409 0 0 0 42996 6 0 0 25 0 1 0 422598901 7360512 1387 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1797 1387 603 41 0 1756 0
vsize: 7188
[startup+440.01 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1428 0 0 0 43995 6 0 0 25 0 1 0 422598901 7495680 1406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1830 1406 603 41 0 1789 0
vsize: 7320
[startup+450.009 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1445 0 0 0 44995 6 0 0 25 0 1 0 422598901 7495680 1423 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1830 1423 603 41 0 1789 0
vsize: 7320
[startup+460.01 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1466 0 0 0 45995 6 0 0 25 0 1 0 422598901 7630848 1444 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1863 1444 603 41 0 1822 0
vsize: 7452
[startup+470.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1470 0 0 0 46995 6 0 0 25 0 1 0 422598901 7630848 1448 4294967295 134512640 134672761 3221224560 3221223664 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1863 1448 603 41 0 1822 0
vsize: 7452
[startup+480.011 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1487 0 0 0 47996 6 0 0 25 0 1 0 422598901 7630848 1465 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1863 1465 603 41 0 1822 0
vsize: 7452
[startup+490.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1490 0 0 0 48996 6 0 0 25 0 1 0 422598901 7770112 1468 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1468 603 41 0 1856 0
vsize: 7588
[startup+500.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1495 0 0 0 49996 6 0 0 25 0 1 0 422598901 7770112 1473 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1473 603 41 0 1856 0
vsize: 7588
[startup+510.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1498 0 0 0 50996 6 0 0 25 0 1 0 422598901 7770112 1476 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1476 603 41 0 1856 0
vsize: 7588
[startup+520.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1501 0 0 0 51996 6 0 0 25 0 1 0 422598901 7770112 1479 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1479 603 41 0 1856 0
vsize: 7588
[startup+530.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1524 0 0 0 52996 7 0 0 25 0 1 0 422598901 7901184 1502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1502 603 41 0 1888 0
vsize: 7716
[startup+540.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1527 0 0 0 53996 7 0 0 25 0 1 0 422598901 7901184 1505 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1505 603 41 0 1888 0
vsize: 7716
[startup+550.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1538 0 0 0 54996 7 0 0 25 0 1 0 422598901 7901184 1516 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1516 603 41 0 1888 0
vsize: 7716
[startup+560.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1544 0 0 0 55997 7 0 0 25 0 1 0 422598901 7901184 1522 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1522 603 41 0 1888 0
vsize: 7716
[startup+570.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1544 0 0 0 56997 7 0 0 25 0 1 0 422598901 7901184 1522 4294967295 134512640 134672761 3221224560 3221223728 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.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1548 0 0 0 57997 7 0 0 25 0 1 0 422598901 7901184 1526 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1526 603 41 0 1888 0
vsize: 7716
[startup+590.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1562 0 0 0 58997 7 0 0 25 0 1 0 422598901 8036352 1540 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1540 603 41 0 1921 0
vsize: 7848
[startup+600.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1570 0 0 0 59997 7 0 0 25 0 1 0 422598901 8036352 1548 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1548 603 41 0 1921 0
vsize: 7848
[startup+610.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1581 0 0 0 60997 7 0 0 25 0 1 0 422598901 8036352 1559 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1559 603 41 0 1921 0
vsize: 7848
[startup+620.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1585 0 0 0 61997 7 0 0 25 0 1 0 422598901 8175616 1563 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1563 603 41 0 1955 0
vsize: 7984
[startup+630.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1585 0 0 0 62998 7 0 0 25 0 1 0 422598901 8175616 1563 4294967295 134512640 134672761 3221224560 3221223728 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.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1589 0 0 0 63998 7 0 0 25 0 1 0 422598901 8175616 1567 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1567 603 41 0 1955 0
vsize: 7984
[startup+650.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1600 0 0 0 64998 7 0 0 25 0 1 0 422598901 8175616 1578 4294967295 134512640 134672761 3221224560 3221223516 1075349791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1578 603 41 0 1955 0
vsize: 7984
[startup+660.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1601 0 0 0 65998 7 0 0 25 0 1 0 422598901 8175616 1579 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1579 603 41 0 1955 0
vsize: 7984
[startup+670.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1630 0 0 0 66998 7 0 0 25 0 1 0 422598901 8310784 1608 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2029 1608 603 41 0 1988 0
vsize: 8116
[startup+680.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1643 0 0 0 67998 7 0 0 25 0 1 0 422598901 8310784 1621 4294967295 134512640 134672761 3221224560 3221223516 1075349975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2029 1621 603 41 0 1988 0
vsize: 8116
[startup+690.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1649 0 0 0 68998 7 0 0 25 0 1 0 422598901 8458240 1627 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1627 603 41 0 2024 0
vsize: 8260
[startup+700.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1664 0 0 0 69998 7 0 0 25 0 1 0 422598901 8458240 1642 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1642 603 41 0 2024 0
vsize: 8260
[startup+710.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1667 0 0 0 70998 7 0 0 25 0 1 0 422598901 8458240 1645 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1645 603 41 0 2024 0
vsize: 8260
[startup+720.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1673 0 0 0 71999 7 0 0 25 0 1 0 422598901 8458240 1651 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1651 603 41 0 2024 0
vsize: 8260
[startup+730.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1676 0 0 0 72999 7 0 0 25 0 1 0 422598901 8597504 1654 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1654 603 41 0 2058 0
vsize: 8396
[startup+740.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1682 0 0 0 73999 7 0 0 25 0 1 0 422598901 8597504 1660 4294967295 134512640 134672761 3221224560 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1660 603 41 0 2058 0
vsize: 8396
[startup+750.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1698 0 0 0 74999 7 0 0 25 0 1 0 422598901 8597504 1676 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1676 603 41 0 2058 0
vsize: 8396
[startup+760.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1698 0 0 0 75999 7 0 0 25 0 1 0 422598901 8597504 1676 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1701 0 0 0 77000 7 0 0 25 0 1 0 422598901 8597504 1679 4294967295 134512640 134672761 3221224560 3221223744 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1679 603 41 0 2058 0
vsize: 8396
[startup+780.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1710 0 0 0 78000 7 0 0 25 0 1 0 422598901 8732672 1688 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1688 603 41 0 2091 0
vsize: 8528
[startup+790.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1721 0 0 0 79000 7 0 0 25 0 1 0 422598901 8732672 1699 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1699 603 41 0 2091 0
vsize: 8528
[startup+800.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1725 0 0 0 80000 7 0 0 25 0 1 0 422598901 8732672 1703 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1703 603 41 0 2091 0
vsize: 8528
[startup+810.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1725 0 0 0 81000 7 0 0 25 0 1 0 422598901 8732672 1703 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1703 603 41 0 2091 0
vsize: 8528
[startup+820.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1729 0 0 0 82001 7 0 0 25 0 1 0 422598901 8732672 1707 4294967295 134512640 134672761 3221224560 3221223664 134554907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1707 603 41 0 2091 0
vsize: 8528
[startup+830.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1737 0 0 0 83001 7 0 0 25 0 1 0 422598901 8732672 1715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1715 603 41 0 2091 0
vsize: 8528
[startup+840.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1744 0 0 0 84001 7 0 0 25 0 1 0 422598901 8867840 1722 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1722 603 41 0 2124 0
vsize: 8660
[startup+850.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1744 0 0 0 85001 7 0 0 25 0 1 0 422598901 8867840 1722 4294967295 134512640 134672761 3221224560 3221223656 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1722 603 41 0 2124 0
vsize: 8660
[startup+860.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1747 0 0 0 86001 7 0 0 25 0 1 0 422598901 8867840 1725 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1725 603 41 0 2124 0
vsize: 8660
[startup+870.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1756 0 0 0 87001 7 0 0 25 0 1 0 422598901 8867840 1734 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1734 603 41 0 2124 0
vsize: 8660
[startup+880.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1762 0 0 0 88002 7 0 0 25 0 1 0 422598901 8867840 1740 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1740 603 41 0 2124 0
vsize: 8660
[startup+890.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1772 0 0 0 89002 7 0 0 25 0 1 0 422598901 9007104 1750 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2199 1750 603 41 0 2158 0
vsize: 8796
[startup+900.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1778 0 0 0 90002 7 0 0 25 0 1 0 422598901 9007104 1756 4294967295 134512640 134672761 3221224560 3221223728 134559131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2199 1756 603 41 0 2158 0
vsize: 8796
[startup+910.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1796 0 0 0 91002 7 0 0 25 0 1 0 422598901 9007104 1774 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2199 1774 603 41 0 2158 0
vsize: 8796
[startup+920.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1798 0 0 0 92002 7 0 0 25 0 1 0 422598901 9142272 1776 4294967295 134512640 134672761 3221224560 3221223744 134559604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1776 603 41 0 2191 0
vsize: 8928
[startup+930.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1801 0 0 0 93003 7 0 0 25 0 1 0 422598901 9142272 1779 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1779 603 41 0 2191 0
vsize: 8928
[startup+940.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1801 0 0 0 94003 7 0 0 25 0 1 0 422598901 9142272 1779 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1779 603 41 0 2191 0
vsize: 8928
[startup+950.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1801 0 0 0 95003 7 0 0 25 0 1 0 422598901 9142272 1779 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1805 0 0 0 96003 7 0 0 25 0 1 0 422598901 9142272 1783 4294967295 134512640 134672761 3221224560 3221223664 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1783 603 41 0 2191 0
vsize: 8928
[startup+970.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1812 0 0 0 97003 7 0 0 25 0 1 0 422598901 9142272 1790 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1790 603 41 0 2191 0
vsize: 8928
[startup+980.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1814 0 0 0 98004 7 0 0 25 0 1 0 422598901 9142272 1792 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1792 603 41 0 2191 0
vsize: 8928
[startup+990.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1817 0 0 0 99004 7 0 0 25 0 1 0 422598901 9142272 1795 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1795 603 41 0 2191 0
vsize: 8928
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1819 0 0 0 100004 7 0 0 25 0 1 0 422598901 9142272 1797 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1797 603 41 0 2191 0
vsize: 8928
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1827 0 0 0 101004 7 0 0 25 0 1 0 422598901 9142272 1805 4294967295 134512640 134672761 3221224560 3221223760 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1805 603 41 0 2191 0
vsize: 8928
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1837 0 0 0 102004 7 0 0 25 0 1 0 422598901 9277440 1815 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2265 1815 603 41 0 2224 0
vsize: 9060
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1844 0 0 0 103005 7 0 0 25 0 1 0 422598901 9277440 1822 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2265 1822 603 41 0 2224 0
vsize: 9060
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1871 0 0 0 104004 7 0 0 25 0 1 0 422598901 9412608 1849 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1849 603 41 0 2257 0
vsize: 9192
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1885 0 0 0 105004 7 0 0 25 0 1 0 422598901 9412608 1863 4294967295 134512640 134672761 3221224560 3221223744 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1863 603 41 0 2257 0
vsize: 9192
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1889 0 0 0 106005 7 0 0 25 0 1 0 422598901 9412608 1867 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1867 603 41 0 2257 0
vsize: 9192
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1889 0 0 0 107005 7 0 0 25 0 1 0 422598901 9412608 1867 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1867 603 41 0 2257 0
vsize: 9192
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1895 0 0 0 108005 7 0 0 25 0 1 0 422598901 9551872 1873 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1873 603 41 0 2291 0
vsize: 9328
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1902 0 0 0 109005 7 0 0 25 0 1 0 422598901 9551872 1880 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1880 603 41 0 2291 0
vsize: 9328
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1911 0 0 0 110005 7 0 0 25 0 1 0 422598901 9551872 1889 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1889 603 41 0 2291 0
vsize: 9328
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1911 0 0 0 111006 7 0 0 25 0 1 0 422598901 9551872 1889 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1889 603 41 0 2291 0
vsize: 9328
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1920 0 0 0 112006 7 0 0 25 0 1 0 422598901 9551872 1898 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1898 603 41 0 2291 0
vsize: 9328
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1927 0 0 0 113006 7 0 0 25 0 1 0 422598901 9551872 1905 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1905 603 41 0 2291 0
vsize: 9328
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1931 0 0 0 114006 7 0 0 25 0 1 0 422598901 9699328 1909 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1909 603 41 0 2327 0
vsize: 9472
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1934 0 0 0 115006 7 0 0 25 0 1 0 422598901 9699328 1912 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1912 603 41 0 2327 0
vsize: 9472
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1938 0 0 0 116007 7 0 0 25 0 1 0 422598901 9699328 1916 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1916 603 41 0 2327 0
vsize: 9472
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1941 0 0 0 117007 7 0 0 25 0 1 0 422598901 9699328 1919 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1919 603 41 0 2327 0
vsize: 9472
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1954 0 0 0 118007 8 0 0 25 0 1 0 422598901 9699328 1932 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1932 603 41 0 2327 0
vsize: 9472
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1955 0 0 0 119007 8 0 0 25 0 1 0 422598901 9699328 1933 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1933 603 41 0 2327 0
vsize: 9472
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25555
Raw data (stat): 25498 (minisat+) R 25497 20937 20936 0 -1 0 1965 0 0 0 120007 8 0 0 25 0 1 0 422598901 9834496 1943 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2401 1943 603 41 0 2360 0
vsize: 9604
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 25555
Raw data (stat): 25498 (minisat+) Z 25497 20937 20936 0 -1 12 1967 0 0 0 120007 8 0 0 25 0 1 0 422598901 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.03
CPU time (s): 1200.16
CPU user time (s): 1200.08
CPU system time (s): 0.084987
CPU usage (%): 100.011
Max. virtual memory (Kb): 9604
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####