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/aloul/FPGA_SAT05/normalized-chnl10_11_pb.cnf.cr.opb
MD5SUM	49b1c3edd36dd2ed7e6daee563a7bd24
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	12
Number of bits of the biggest sum of numbers	4
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.008998
Number of variables	220
Total number of constraints	42
Number of constraints which are clauses	22
Number of constraints which are cardinality constraints (but not clauses)	20
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	10
Maximum length of a constraint	11

Trace number 4544

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 19:21:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3386 boxname=wulflinc31 idbench=2 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  49b1c3edd36dd2ed7e6daee563a7bd24  /oldhome/oroussel/tmp/wulflinc31/normalized-chnl10_11_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-chnl10_11_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc31/normalized-chnl10_11_pb.cnf.cr.opb
IDLAUNCH: 3386
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        913912 kB
Buffers:         34184 kB
Cached:          48180 kB
SwapCached:        392 kB
Active:          44072 kB
Inactive:        41432 kB
HighTotal:      131008 kB
HighFree:        79156 kB
LowTotal:       903652 kB
LowFree:        834756 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29584 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:26:51 (client local time) WITH STATUS 20 IN 315.757 SECONDS
stats: 3386 7 315.757 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 42 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................
c ---[  19]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  18]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  17]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  16]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  15]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  14]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  13]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  12]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  11]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  10]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   9]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   8]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   7]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   6]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   5]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   4]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   3]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   2]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   1]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[   0]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1622     5900 |     540       0        0     nan |  0.000 % |
c |       100 |    1558     5676 |     594      90      671     7.5 | 24.259 % |
c |       252 |    1517     5535 |     653     236     5696    24.1 | 25.371 % |
c |       477 |    1517     5535 |     718     461    18580    40.3 | 25.371 % |
c |       814 |    1409     5173 |     790     780    37042    47.5 | 29.074 % |
c |      1322 |    1409     5173 |     869     762    37129    48.7 | 29.074 % |
c |      2081 |    1382     5078 |     956     952    46738    49.1 | 30.000 % |
c |      3220 |    1366     5026 |    1052     876    36963    42.2 | 30.556 % |
c |      4929 |    1350     4974 |    1157    1270    57944    45.6 | 31.111 % |
c |      7491 |    1334     4922 |    1273    1029    43237    42.0 | 31.667 % |
c |     11335 |    1334     4922 |    1400    1066    41910    39.3 | 31.667 % |
c |     17101 |    1325     4893 |    1540    1029    39341    38.2 | 32.037 % |
c |     25750 |    1325     4893 |    1694    1629    62467    38.3 | 32.037 % |
c |     38727 |    1325     4893 |    1864    1051    37519    35.7 | 32.037 % |
c |     58188 |    1325     4893 |    2050    1536    55946    36.4 | 32.037 % |
c |     87380 |    1325     4893 |    2255    2035    84467    41.5 | 32.037 % |
c |    131172 |    1325     4893 |    2481    2025    79055    39.0 | 32.038 % |
c |    196862 |    1300     4812 |    2729    1969    72442    36.8 | 32.963 % |
c |    295388 |    1284     4760 |    3002    1958    76193    38.9 | 33.519 % |
c |    443179 |    1284     4760 |    3302    3085   107128    34.7 | 33.519 % |
c |    664864 |    1284     4760 |    3632    2408    84215    35.0 | 33.519 % |
c |    997391 |    1284     4760 |    3996    2435    76476    31.4 | 33.519 % |
c ==============================================================================
c [1mUNSATISFIABLE[0m
s UNKNOWN
c _______________________________________________________________________________
c 
c restarts              : 22
c conflicts             : 1156218        (3662 /sec)
c decisions             : 1292090        (4093 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 315.718 s
c _______________________________________________________________________________
#### 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.00 0.00 0.04 2/54 24558
Raw data (stat): 24558 (runsolver) R 24557 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478418090 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0007 s]
Raw data (loadavg): 0.15 0.03 0.05 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 521 0 0 0 997 1 0 0 25 0 1 0 478418090 3604480 499 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 880 499 603 41 0 839 0
vsize: 3520
[startup+20.0019 s]
Raw data (loadavg): 0.28 0.06 0.06 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 590 0 0 0 1997 1 0 0 25 0 1 0 478418090 3878912 568 4294967295 134512640 134672761 3221224544 3221223728 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 947 568 603 41 0 906 0
vsize: 3788
[startup+30.0017 s]
Raw data (loadavg): 0.39 0.09 0.07 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 626 0 0 0 2997 1 0 0 25 0 1 0 478418090 4149248 604 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1013 604 603 41 0 972 0
vsize: 4052
[startup+40.0025 s]
Raw data (loadavg): 0.49 0.12 0.08 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 652 0 0 0 3996 1 0 0 25 0 1 0 478418090 4149248 630 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1013 630 603 41 0 972 0
vsize: 4052
[startup+50.0027 s]
Raw data (loadavg): 0.56 0.15 0.09 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 676 0 0 0 4997 1 0 0 25 0 1 0 478418090 4292608 654 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1048 654 603 41 0 1007 0
vsize: 4192
[startup+60.0033 s]
Raw data (loadavg): 0.63 0.18 0.10 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 685 0 0 0 5997 1 0 0 25 0 1 0 478418090 4292608 663 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1048 663 603 41 0 1007 0
vsize: 4192
[startup+70.0036 s]
Raw data (loadavg): 0.69 0.21 0.10 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 697 0 0 0 6997 2 0 0 25 0 1 0 478418090 4431872 675 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1082 675 603 41 0 1041 0
vsize: 4328
[startup+80.0032 s]
Raw data (loadavg): 0.73 0.23 0.11 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 730 0 0 0 7997 2 0 0 25 0 1 0 478418090 4571136 708 4294967295 134512640 134672761 3221224544 3221223720 134559059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1116 708 603 41 0 1075 0
vsize: 4464
[startup+90.0031 s]
Raw data (loadavg): 0.77 0.26 0.12 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 742 0 0 0 8997 2 0 0 25 0 1 0 478418090 4571136 720 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1116 720 603 41 0 1075 0
vsize: 4464
[startup+100.004 s]
Raw data (loadavg): 0.81 0.28 0.13 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 745 0 0 0 9997 2 0 0 25 0 1 0 478418090 4571136 723 4294967295 134512640 134672761 3221224544 3221223648 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1116 723 603 41 0 1075 0
vsize: 4464
[startup+110.004 s]
Raw data (loadavg): 0.84 0.30 0.14 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 754 0 0 0 10997 2 0 0 25 0 1 0 478418090 4718592 732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1152 732 603 41 0 1111 0
vsize: 4608
[startup+120.005 s]
Raw data (loadavg): 0.86 0.33 0.15 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 783 0 0 0 11997 2 0 0 25 0 1 0 478418090 4718592 761 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1152 761 603 41 0 1111 0
vsize: 4608
[startup+130.005 s]
Raw data (loadavg): 0.88 0.35 0.16 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 811 0 0 0 12998 2 0 0 25 0 1 0 478418090 4866048 789 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1188 789 603 41 0 1147 0
vsize: 4752
[startup+140.006 s]
Raw data (loadavg): 0.90 0.37 0.17 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 814 0 0 0 13998 2 0 0 25 0 1 0 478418090 5013504 792 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1224 792 603 41 0 1183 0
vsize: 4896
[startup+150.006 s]
Raw data (loadavg): 0.92 0.39 0.17 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 826 0 0 0 14998 2 0 0 25 0 1 0 478418090 5013504 804 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1224 804 603 41 0 1183 0
vsize: 4896
[startup+160.007 s]
Raw data (loadavg): 0.93 0.41 0.18 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 832 0 0 0 15998 2 0 0 25 0 1 0 478418090 5013504 810 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1224 810 603 41 0 1183 0
vsize: 4896
[startup+170.008 s]
Raw data (loadavg): 0.94 0.43 0.19 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 835 0 0 0 16998 2 0 0 25 0 1 0 478418090 5013504 813 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1224 813 603 41 0 1183 0
vsize: 4896
[startup+180.007 s]
Raw data (loadavg): 0.95 0.45 0.20 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 838 0 0 0 17998 2 0 0 25 0 1 0 478418090 5013504 816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1224 816 603 41 0 1183 0
vsize: 4896
[startup+190.009 s]
Raw data (loadavg): 0.95 0.46 0.21 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 858 0 0 0 18999 2 0 0 25 0 1 0 478418090 5160960 836 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1260 836 603 41 0 1219 0
vsize: 5040
[startup+200.008 s]
Raw data (loadavg): 0.96 0.48 0.21 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 862 0 0 0 19999 2 0 0 25 0 1 0 478418090 5160960 840 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1260 840 603 41 0 1219 0
vsize: 5040
[startup+210.009 s]
Raw data (loadavg): 0.97 0.50 0.22 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 875 0 0 0 20999 2 0 0 25 0 1 0 478418090 5308416 853 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1296 853 603 41 0 1255 0
vsize: 5184
[startup+220.011 s]
Raw data (loadavg): 0.97 0.51 0.23 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 893 0 0 0 21999 2 0 0 25 0 1 0 478418090 5308416 871 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1296 871 603 41 0 1255 0
vsize: 5184
[startup+230.01 s]
Raw data (loadavg): 0.98 0.53 0.24 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 909 0 0 0 22999 2 0 0 25 0 1 0 478418090 5451776 887 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1331 887 603 41 0 1290 0
vsize: 5324
[startup+240.01 s]
Raw data (loadavg): 0.98 0.54 0.25 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 920 0 0 0 23999 2 0 0 25 0 1 0 478418090 5451776 898 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1331 898 603 41 0 1290 0
vsize: 5324
[startup+250.01 s]
Raw data (loadavg): 0.98 0.56 0.25 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 927 0 0 0 24999 2 0 0 25 0 1 0 478418090 5451776 905 4294967295 134512640 134672761 3221224544 3221223728 134559055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1331 905 603 41 0 1290 0
vsize: 5324
[startup+260.011 s]
Raw data (loadavg): 0.98 0.57 0.26 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 937 0 0 0 26000 2 0 0 25 0 1 0 478418090 5599232 915 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1367 915 603 41 0 1326 0
vsize: 5468
[startup+270.011 s]
Raw data (loadavg): 0.99 0.59 0.27 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 938 0 0 0 27000 2 0 0 25 0 1 0 478418090 5599232 916 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1367 916 603 41 0 1326 0
vsize: 5468
[startup+280.012 s]
Raw data (loadavg): 0.99 0.60 0.28 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 957 0 0 0 27999 3 0 0 25 0 1 0 478418090 5599232 935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1367 935 603 41 0 1326 0
vsize: 5468
[startup+290.013 s]
Raw data (loadavg): 0.99 0.61 0.28 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 957 0 0 0 28998 3 0 0 25 0 1 0 478418090 5599232 935 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1367 935 603 41 0 1326 0
vsize: 5468
[startup+300.013 s]
Raw data (loadavg): 0.99 0.62 0.29 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 969 0 0 0 29997 3 0 0 25 0 1 0 478418090 5746688 947 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1403 947 603 41 0 1362 0
vsize: 5612
[startup+310.014 s]
Raw data (loadavg): 0.99 0.64 0.30 2/54 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 969 0 0 0 30997 3 0 0 25 0 1 0 478418090 5746688 947 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1403 947 603 41 0 1362 0
vsize: 5612
[startup+315.758 s]
Raw data (loadavg): 0.99 0.64 0.30 1/53 24558
Raw data (stat): 24558 (minisat+) R 24557 23176 23175 0 -1 0 969 0 0 0 30997 3 0 0 25 0 1 0 478418090 5746688 947 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1403 947 603 41 0 1362 0
vsize: 0

Child status: 20
Real time (s): 315.757
CPU time (s): 315.757
CPU user time (s): 315.719
CPU system time (s): 0.037994
CPU usage (%): 99.9999
Max. virtual memory (Kb): 5612
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####