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 4672

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-13 19:47:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3513 boxname=wulflinc26 idbench=129 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fdec182582ed31d1ae371090f6cc5c1  /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb
IDLAUNCH: 3513
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        861044 kB
Buffers:         33536 kB
Cached:          99920 kB
SwapCached:       2476 kB
Active:          48016 kB
Inactive:        90736 kB
HighTotal:      131008 kB
HighFree:        27972 kB
LowTotal:       903652 kB
LowFree:        833072 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6944 kB
Slab:            29236 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:07:06 (client local time) WITH STATUS 0 IN 1200.11 SECONDS
stats: 3513 7 1200.11 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.53 0.84 0.66 2/54 24958
Raw data (stat): 24958 (runsolver) R 24957 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478588472 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.60 0.84 0.67 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 629 0 0 0 996 1 0 0 25 0 1 0 478588472 4100096 607 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.0022 s]
Raw data (loadavg): 0.66 0.85 0.67 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 683 0 0 0 1996 2 0 0 25 0 1 0 478588472 4366336 661 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.0025 s]
Raw data (loadavg): 0.71 0.85 0.67 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 734 0 0 0 2996 2 0 0 25 0 1 0 478588472 4501504 712 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1099 712 603 41 0 1058 0
vsize: 4396
[startup+40.0036 s]
Raw data (loadavg): 0.76 0.86 0.67 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 784 0 0 0 3995 3 0 0 25 0 1 0 478588472 4767744 762 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1164 762 603 41 0 1123 0
vsize: 4656
[startup+50.0043 s]
Raw data (loadavg): 0.79 0.86 0.68 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 825 0 0 0 4994 4 0 0 25 0 1 0 478588472 4902912 803 4294967295 134512640 134672761 3221224576 3221223760 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1197 803 603 41 0 1156 0
vsize: 4788
[startup+60.0045 s]
Raw data (loadavg): 0.83 0.86 0.68 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 864 0 0 0 5994 4 0 0 25 0 1 0 478588472 5038080 842 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1230 842 603 41 0 1189 0
vsize: 4920
[startup+70.0056 s]
Raw data (loadavg): 0.85 0.87 0.68 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 883 0 0 0 6994 5 0 0 25 0 1 0 478588472 5173248 861 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1263 861 603 41 0 1222 0
vsize: 5052
[startup+80.0064 s]
Raw data (loadavg): 0.87 0.87 0.69 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 923 0 0 0 7993 5 0 0 25 0 1 0 478588472 5308416 901 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1296 901 603 41 0 1255 0
vsize: 5184
[startup+90.0065 s]
Raw data (loadavg): 0.89 0.88 0.69 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 938 0 0 0 8992 6 0 0 25 0 1 0 478588472 5308416 916 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.007 s]
Raw data (loadavg): 0.91 0.88 0.69 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 946 0 0 0 9992 6 0 0 25 0 1 0 478588472 5443584 924 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1329 924 603 41 0 1288 0
vsize: 5316
[startup+110.007 s]
Raw data (loadavg): 0.92 0.88 0.69 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 957 0 0 0 10991 6 0 0 25 0 1 0 478588472 5443584 935 4294967295 134512640 134672761 3221224576 3221223760 134558557 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.008 s]
Raw data (loadavg): 0.93 0.89 0.70 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1013 0 0 0 11991 7 0 0 25 0 1 0 478588472 5709824 991 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1394 991 603 41 0 1353 0
vsize: 5576
[startup+130.008 s]
Raw data (loadavg): 0.94 0.89 0.70 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1027 0 0 0 12990 8 0 0 25 0 1 0 478588472 5713920 1005 4294967295 134512640 134672761 3221224576 3221223576 1075349780 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.008 s]
Raw data (loadavg): 0.95 0.89 0.70 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1048 0 0 0 13990 8 0 0 25 0 1 0 478588472 5844992 1026 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1427 1026 603 41 0 1386 0
vsize: 5708
[startup+150.009 s]
Raw data (loadavg): 0.96 0.90 0.71 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1065 0 0 0 14989 8 0 0 25 0 1 0 478588472 5844992 1043 4294967295 134512640 134672761 3221224576 3221223680 134555114 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.01 s]
Raw data (loadavg): 0.96 0.90 0.71 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1079 0 0 0 15988 9 0 0 25 0 1 0 478588472 5984256 1057 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1461 1057 603 41 0 1420 0
vsize: 5844
[startup+170.01 s]
Raw data (loadavg): 0.97 0.90 0.71 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1088 0 0 0 16988 9 0 0 25 0 1 0 478588472 5984256 1066 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.01 s]
Raw data (loadavg): 0.97 0.90 0.72 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1102 0 0 0 17987 10 0 0 25 0 1 0 478588472 5984256 1080 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1461 1080 603 41 0 1420 0
vsize: 5844
[startup+190.011 s]
Raw data (loadavg): 0.98 0.91 0.72 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1147 0 0 0 18987 10 0 0 25 0 1 0 478588472 6254592 1125 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1527 1125 603 41 0 1486 0
vsize: 6108
[startup+200.011 s]
Raw data (loadavg): 0.98 0.91 0.72 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1156 0 0 0 19987 11 0 0 25 0 1 0 478588472 6254592 1134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1527 1134 603 41 0 1486 0
vsize: 6108
[startup+210.012 s]
Raw data (loadavg): 0.98 0.91 0.72 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1166 0 0 0 20986 11 0 0 25 0 1 0 478588472 6254592 1144 4294967295 134512640 134672761 3221224576 3221223744 134561115 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.013 s]
Raw data (loadavg): 0.98 0.91 0.73 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1184 0 0 0 21986 11 0 0 25 0 1 0 478588472 6389760 1162 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1560 1162 603 41 0 1519 0
vsize: 6240
[startup+230.013 s]
Raw data (loadavg): 0.99 0.92 0.73 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1192 0 0 0 22985 12 0 0 25 0 1 0 478588472 6389760 1170 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1560 1170 603 41 0 1519 0
vsize: 6240
[startup+240.013 s]
Raw data (loadavg): 0.99 0.92 0.73 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1209 0 0 0 23985 12 0 0 25 0 1 0 478588472 6524928 1187 4294967295 134512640 134672761 3221224576 3221223776 134557836 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.014 s]
Raw data (loadavg): 0.99 0.92 0.73 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1220 0 0 0 24985 12 0 0 25 0 1 0 478588472 6524928 1198 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1593 1198 603 41 0 1552 0
vsize: 6372
[startup+260.015 s]
Raw data (loadavg): 0.99 0.92 0.74 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1236 0 0 0 25984 13 0 0 25 0 1 0 478588472 6672384 1214 4294967295 134512640 134672761 3221224576 3221223744 134561229 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.015 s]
Raw data (loadavg): 0.99 0.92 0.74 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1246 0 0 0 26983 13 0 0 25 0 1 0 478588472 6672384 1224 4294967295 134512640 134672761 3221224576 3221223668 1075346528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1224 603 41 0 1588 0
vsize: 6516
[startup+280.015 s]
Raw data (loadavg): 0.99 0.93 0.74 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1259 0 0 0 27983 14 0 0 25 0 1 0 478588472 6672384 1237 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1237 603 41 0 1588 0
vsize: 6516
[startup+290.016 s]
Raw data (loadavg): 0.99 0.93 0.74 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1276 0 0 0 28982 14 0 0 25 0 1 0 478588472 6807552 1254 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1662 1254 603 41 0 1621 0
vsize: 6648
[startup+300.016 s]
Raw data (loadavg): 0.99 0.93 0.74 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1289 0 0 0 29982 15 0 0 25 0 1 0 478588472 6807552 1267 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1662 1267 603 41 0 1621 0
vsize: 6648
[startup+310.017 s]
Raw data (loadavg): 0.99 0.93 0.75 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1303 0 0 0 30982 15 0 0 25 0 1 0 478588472 6942720 1281 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1695 1281 603 41 0 1654 0
vsize: 6780
[startup+320.018 s]
Raw data (loadavg): 0.99 0.93 0.75 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1322 0 0 0 31981 16 0 0 25 0 1 0 478588472 6942720 1300 4294967295 134512640 134672761 3221224576 3221223760 134558903 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.017 s]
Raw data (loadavg): 0.99 0.94 0.75 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1322 0 0 0 32980 16 0 0 25 0 1 0 478588472 6942720 1300 4294967295 134512640 134672761 3221224576 3221223680 134554636 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.018 s]
Raw data (loadavg): 0.99 0.94 0.75 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1326 0 0 0 33980 16 0 0 25 0 1 0 478588472 6942720 1304 4294967295 134512640 134672761 3221224576 3221223744 134561218 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.019 s]
Raw data (loadavg): 0.99 0.94 0.75 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1330 0 0 0 34979 17 0 0 25 0 1 0 478588472 6942720 1308 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1695 1308 603 41 0 1654 0
vsize: 6780
[startup+360.02 s]
Raw data (loadavg): 0.99 0.94 0.75 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1338 0 0 0 35979 17 0 0 25 0 1 0 478588472 7090176 1316 4294967295 134512640 134672761 3221224576 3221223744 134561151 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.02 s]
Raw data (loadavg): 0.99 0.94 0.76 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1343 0 0 0 36979 17 0 0 25 0 1 0 478588472 7090176 1321 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1731 1321 603 41 0 1690 0
vsize: 6924
[startup+380.02 s]
Raw data (loadavg): 0.99 0.94 0.76 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1357 0 0 0 37979 18 0 0 25 0 1 0 478588472 7090176 1335 4294967295 134512640 134672761 3221224576 3221223728 134565056 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.02 s]
Raw data (loadavg): 0.99 0.94 0.76 3/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1359 0 0 0 38978 18 0 0 25 0 1 0 478588472 7090176 1337 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1731 1337 603 41 0 1690 0
vsize: 6924
[startup+400.02 s]
Raw data (loadavg): 0.99 0.95 0.76 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1370 0 0 0 39978 18 0 0 25 0 1 0 478588472 7225344 1348 4294967295 134512640 134672761 3221224576 3221223744 134561193 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.021 s]
Raw data (loadavg): 0.99 0.95 0.76 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1370 0 0 0 40977 19 0 0 25 0 1 0 478588472 7225344 1348 4294967295 134512640 134672761 3221224576 3221223744 134561218 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.021 s]
Raw data (loadavg): 0.99 0.95 0.77 3/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1372 0 0 0 41977 19 0 0 25 0 1 0 478588472 7225344 1350 4294967295 134512640 134672761 3221224576 3221223760 134559385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1350 603 41 0 1723 0
vsize: 7056
[startup+430.022 s]
Raw data (loadavg): 0.99 0.95 0.77 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1385 0 0 0 42977 19 0 0 25 0 1 0 478588472 7225344 1363 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1764 1363 603 41 0 1723 0
vsize: 7056
[startup+440.022 s]
Raw data (loadavg): 0.99 0.95 0.77 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1417 0 0 0 43977 19 0 0 25 0 1 0 478588472 7360512 1395 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1797 1395 603 41 0 1756 0
vsize: 7188
[startup+450.024 s]
Raw data (loadavg): 0.99 0.95 0.77 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1431 0 0 0 44977 19 0 0 25 0 1 0 478588472 7495680 1409 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1830 1409 603 41 0 1789 0
vsize: 7320
[startup+460.026 s]
Raw data (loadavg): 0.99 0.95 0.77 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1447 0 0 0 45978 19 0 0 25 0 1 0 478588472 7495680 1425 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1830 1425 603 41 0 1789 0
vsize: 7320
[startup+470.025 s]
Raw data (loadavg): 0.99 0.95 0.78 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1466 0 0 0 46978 19 0 0 25 0 1 0 478588472 7630848 1444 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1863 1444 603 41 0 1822 0
vsize: 7452
[startup+480.026 s]
Raw data (loadavg): 0.99 0.95 0.78 3/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1470 0 0 0 47978 19 0 0 25 0 1 0 478588472 7630848 1448 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1863 1448 603 41 0 1822 0
vsize: 7452
[startup+490.026 s]
Raw data (loadavg): 0.99 0.95 0.78 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1487 0 0 0 48978 19 0 0 25 0 1 0 478588472 7630848 1465 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1863 1465 603 41 0 1822 0
vsize: 7452
[startup+500.027 s]
Raw data (loadavg): 0.99 0.96 0.78 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1490 0 0 0 49978 19 0 0 25 0 1 0 478588472 7770112 1468 4294967295 134512640 134672761 3221224576 3221223712 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1468 603 41 0 1856 0
vsize: 7588
[startup+510.027 s]
Raw data (loadavg): 0.99 0.96 0.78 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1495 0 0 0 50978 19 0 0 25 0 1 0 478588472 7770112 1473 4294967295 134512640 134672761 3221224576 3221223760 134559161 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.027 s]
Raw data (loadavg): 0.99 0.96 0.79 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1498 0 0 0 51979 19 0 0 25 0 1 0 478588472 7770112 1476 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.027 s]
Raw data (loadavg): 0.99 0.96 0.79 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1501 0 0 0 52979 19 0 0 25 0 1 0 478588472 7770112 1479 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1897 1479 603 41 0 1856 0
vsize: 7588
[startup+540.027 s]
Raw data (loadavg): 0.99 0.96 0.79 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1524 0 0 0 53979 20 0 0 25 0 1 0 478588472 7901184 1502 4294967295 134512640 134672761 3221224576 3221223712 134565036 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.027 s]
Raw data (loadavg): 0.99 0.96 0.79 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1527 0 0 0 54979 20 0 0 25 0 1 0 478588472 7901184 1505 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1505 603 41 0 1888 0
vsize: 7716
[startup+560.028 s]
Raw data (loadavg): 0.99 0.96 0.79 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1534 0 0 0 55979 20 0 0 25 0 1 0 478588472 7901184 1512 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1512 603 41 0 1888 0
vsize: 7716
[startup+570.028 s]
Raw data (loadavg): 0.99 0.96 0.80 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1544 0 0 0 56979 20 0 0 25 0 1 0 478588472 7901184 1522 4294967295 134512640 134672761 3221224576 3221223680 134560235 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.028 s]
Raw data (loadavg): 0.99 0.96 0.80 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1544 0 0 0 57979 20 0 0 25 0 1 0 478588472 7901184 1522 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1522 603 41 0 1888 0
vsize: 7716
[startup+590.029 s]
Raw data (loadavg): 0.99 0.96 0.80 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1546 0 0 0 58980 20 0 0 25 0 1 0 478588472 7901184 1524 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1929 1524 603 41 0 1888 0
vsize: 7716
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1556 0 0 0 59980 20 0 0 25 0 1 0 478588472 8036352 1534 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1534 603 41 0 1921 0
vsize: 7848
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1568 0 0 0 60980 20 0 0 25 0 1 0 478588472 8036352 1546 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1546 603 41 0 1921 0
vsize: 7848
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1576 0 0 0 61980 20 0 0 25 0 1 0 478588472 8036352 1554 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1962 1554 603 41 0 1921 0
vsize: 7848
[startup+630.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1585 0 0 0 62981 20 0 0 25 0 1 0 478588472 8175616 1563 4294967295 134512640 134672761 3221224576 3221223744 134560917 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.03 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1585 0 0 0 63981 20 0 0 25 0 1 0 478588472 8175616 1563 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.03 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1589 0 0 0 64981 20 0 0 25 0 1 0 478588472 8175616 1567 4294967295 134512640 134672761 3221224576 3221223744 134561151 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.03 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1594 0 0 0 65981 20 0 0 25 0 1 0 478588472 8175616 1572 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1572 603 41 0 1955 0
vsize: 7984
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1600 0 0 0 66981 20 0 0 25 0 1 0 478588472 8175616 1578 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1578 603 41 0 1955 0
vsize: 7984
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1621 0 0 0 67981 20 0 0 25 0 1 0 478588472 8310784 1599 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2029 1599 603 41 0 1988 0
vsize: 8116
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1633 0 0 0 68981 20 0 0 25 0 1 0 478588472 8310784 1611 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2029 1611 603 41 0 1988 0
vsize: 8116
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1649 0 0 0 69980 21 0 0 25 0 1 0 478588472 8458240 1627 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1656 0 0 0 70980 21 0 0 25 0 1 0 478588472 8458240 1634 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1634 603 41 0 2024 0
vsize: 8260
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1664 0 0 0 71980 21 0 0 25 0 1 0 478588472 8458240 1642 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1642 603 41 0 2024 0
vsize: 8260
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1671 0 0 0 72980 21 0 0 25 0 1 0 478588472 8458240 1649 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1649 603 41 0 2024 0
vsize: 8260
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1673 0 0 0 73980 21 0 0 25 0 1 0 478588472 8458240 1651 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2065 1651 603 41 0 2024 0
vsize: 8260
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1678 0 0 0 74980 21 0 0 25 0 1 0 478588472 8597504 1656 4294967295 134512640 134672761 3221224576 3221223712 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1656 603 41 0 2058 0
vsize: 8396
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1682 0 0 0 75981 21 0 0 25 0 1 0 478588472 8597504 1660 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1660 603 41 0 2058 0
vsize: 8396
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 24958
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1698 0 0 0 76981 21 0 0 25 0 1 0 478588472 8597504 1676 4294967295 134512640 134672761 3221224576 3221223760 134559411 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.033 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 24959
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1698 0 0 0 77981 21 0 0 25 0 1 0 478588472 8597504 1676 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1676 603 41 0 2058 0
vsize: 8396
[startup+790.033 s]
Raw data (loadavg): 1.07 0.99 0.83 2/54 25011
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1701 0 0 0 78981 21 0 0 25 0 1 0 478588472 8597504 1679 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2099 1679 603 41 0 2058 0
vsize: 8396
[startup+800.033 s]
Raw data (loadavg): 1.06 0.99 0.83 2/54 25011
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1710 0 0 0 79981 21 0 0 25 0 1 0 478588472 8732672 1688 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1688 603 41 0 2091 0
vsize: 8528
[startup+810.034 s]
Raw data (loadavg): 1.05 0.99 0.84 2/54 25011
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1721 0 0 0 80981 21 0 0 25 0 1 0 478588472 8732672 1699 4294967295 134512640 134672761 3221224576 3221223152 134565852 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.033 s]
Raw data (loadavg): 1.04 0.99 0.84 2/54 25011
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1725 0 0 0 81981 22 0 0 25 0 1 0 478588472 8732672 1703 4294967295 134512640 134672761 3221224576 3221223744 134560830 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.033 s]
Raw data (loadavg): 1.03 0.99 0.84 2/54 25011
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1725 0 0 0 82981 22 0 0 25 0 1 0 478588472 8732672 1703 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1703 603 41 0 2091 0
vsize: 8528
[startup+840.032 s]
Raw data (loadavg): 1.03 0.99 0.84 2/54 25011
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1729 0 0 0 83981 22 0 0 25 0 1 0 478588472 8732672 1707 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1707 603 41 0 2091 0
vsize: 8528
[startup+850.032 s]
Raw data (loadavg): 1.02 0.99 0.84 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1737 0 0 0 84980 22 0 0 25 0 1 0 478588472 8732672 1715 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2132 1715 603 41 0 2091 0
vsize: 8528
[startup+860.033 s]
Raw data (loadavg): 1.02 0.99 0.84 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1744 0 0 0 85980 23 0 0 25 0 1 0 478588472 8867840 1722 4294967295 134512640 134672761 3221224576 3221223744 134560909 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.034 s]
Raw data (loadavg): 1.02 0.99 0.84 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1744 0 0 0 86980 23 0 0 25 0 1 0 478588472 8867840 1722 4294967295 134512640 134672761 3221224576 3221223744 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+880.034 s]
Raw data (loadavg): 1.01 0.99 0.84 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1747 0 0 0 87980 24 0 0 25 0 1 0 478588472 8867840 1725 4294967295 134512640 134672761 3221224576 3221223744 134561151 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.034 s]
Raw data (loadavg): 1.01 0.99 0.84 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1756 0 0 0 88979 24 0 0 25 0 1 0 478588472 8867840 1734 4294967295 134512640 134672761 3221224576 3221223744 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+900.034 s]
Raw data (loadavg): 1.01 0.99 0.84 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1759 0 0 0 89979 24 0 0 25 0 1 0 478588472 8867840 1737 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1737 603 41 0 2124 0
vsize: 8660
[startup+910.035 s]
Raw data (loadavg): 1.01 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1765 0 0 0 90979 25 0 0 25 0 1 0 478588472 8867840 1743 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2165 1743 603 41 0 2124 0
vsize: 8660
[startup+920.034 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1777 0 0 0 91979 26 0 0 25 0 1 0 478588472 9007104 1755 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2199 1755 603 41 0 2158 0
vsize: 8796
[startup+930.034 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1796 0 0 0 92978 26 0 0 25 0 1 0 478588472 9007104 1774 4294967295 134512640 134672761 3221224576 3221223680 134560180 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.035 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1798 0 0 0 93978 26 0 0 25 0 1 0 478588472 9142272 1776 4294967295 134512640 134672761 3221224576 3221223744 134560964 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.034 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1801 0 0 0 94978 27 0 0 25 0 1 0 478588472 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.035 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1801 0 0 0 95978 27 0 0 25 0 1 0 478588472 9142272 1779 4294967295 134512640 134672761 3221224576 3221223744 134561278 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.036 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1801 0 0 0 96978 28 0 0 25 0 1 0 478588472 9142272 1779 4294967295 134512640 134672761 3221224576 3221223744 134561161 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.035 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1805 0 0 0 97977 28 0 0 25 0 1 0 478588472 9142272 1783 4294967295 134512640 134672761 3221224576 3221223712 134560709 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.035 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1805 0 0 0 98977 29 0 0 25 0 1 0 478588472 9142272 1783 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1783 603 41 0 2191 0
vsize: 8928
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1812 0 0 0 99977 29 0 0 25 0 1 0 478588472 9142272 1790 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1790 603 41 0 2191 0
vsize: 8928
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1814 0 0 0 100977 29 0 0 25 0 1 0 478588472 9142272 1792 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1792 603 41 0 2191 0
vsize: 8928
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1817 0 0 0 101977 29 0 0 25 0 1 0 478588472 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+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1821 0 0 0 102976 30 0 0 25 0 1 0 478588472 9142272 1799 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1799 603 41 0 2191 0
vsize: 8928
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1829 0 0 0 103976 30 0 0 25 0 1 0 478588472 9277440 1807 4294967295 134512640 134672761 3221224576 3221223744 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2265 1807 603 41 0 2224 0
vsize: 9060
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1839 0 0 0 104976 30 0 0 25 0 1 0 478588472 9277440 1817 4294967295 134512640 134672761 3221224576 3221223680 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2265 1817 603 41 0 2224 0
vsize: 9060
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1844 0 0 0 105976 31 0 0 25 0 1 0 478588472 9277440 1822 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2265 1822 603 41 0 2224 0
vsize: 9060
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1871 0 0 0 106976 32 0 0 25 0 1 0 478588472 9412608 1849 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1849 603 41 0 2257 0
vsize: 9192
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1885 0 0 0 107975 32 0 0 25 0 1 0 478588472 9412608 1863 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1863 603 41 0 2257 0
vsize: 9192
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1889 0 0 0 108975 32 0 0 25 0 1 0 478588472 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.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1889 0 0 0 109975 33 0 0 25 0 1 0 478588472 9412608 1867 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1867 603 41 0 2257 0
vsize: 9192
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1893 0 0 0 110975 33 0 0 25 0 1 0 478588472 9412608 1871 4294967295 134512640 134672761 3221224576 3221223328 134565852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2298 1871 603 41 0 2257 0
vsize: 9192
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25013
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1901 0 0 0 111975 33 0 0 25 0 1 0 478588472 9551872 1879 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1879 603 41 0 2291 0
vsize: 9328
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1910 0 0 0 112974 34 0 0 25 0 1 0 478588472 9551872 1888 4294967295 134512640 134672761 3221224576 3221223680 134555333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1888 603 41 0 2291 0
vsize: 9328
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1911 0 0 0 113974 34 0 0 25 0 1 0 478588472 9551872 1889 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1889 603 41 0 2291 0
vsize: 9328
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1919 0 0 0 114974 35 0 0 25 0 1 0 478588472 9551872 1897 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1897 603 41 0 2291 0
vsize: 9328
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1923 0 0 0 115974 35 0 0 25 0 1 0 478588472 9551872 1901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1901 603 41 0 2291 0
vsize: 9328
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1931 0 0 0 116973 36 0 0 25 0 1 0 478588472 9699328 1909 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1909 603 41 0 2327 0
vsize: 9472
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1934 0 0 0 117973 36 0 0 25 0 1 0 478588472 9699328 1912 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1912 603 41 0 2327 0
vsize: 9472
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1938 0 0 0 118973 36 0 0 25 0 1 0 478588472 9699328 1916 4294967295 134512640 134672761 3221224576 3221223760 134559340 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.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25015
Raw data (stat): 24958 (minisat+) R 24957 22612 22611 0 -1 0 1938 0 0 0 119973 37 0 0 25 0 1 0 478588472 9699328 1916 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1916 603 41 0 2327 0
vsize: 9472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.87 1/54 25015
Raw data (stat): 24958 (minisat+) Z 24957 22612 22611 0 -1 12 1940 0 0 0 119973 37 0 0 25 0 1 0 478588472 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.11
CPU user time (s): 1199.73
CPU system time (s): 0.375942
CPU usage (%): 100.006
Max. virtual memory (Kb): 9472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####