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_15_pb.cnf.cr.opb
MD5SUM	ba9cd165dfff9daff67f98334a7b589e
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	16
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.009997
Number of variables	300
Total number of constraints	50
Number of constraints which are clauses	30
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	15

Trace number 6027

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 03:19:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4515 boxname=wulflinc20 idbench=3 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ba9cd165dfff9daff67f98334a7b589e  /oldhome/oroussel/tmp/wulflinc20/normalized-chnl10_15_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc20/normalized-chnl10_15_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc20/normalized-chnl10_15_pb.cnf.cr.opb
IDLAUNCH: 4515
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        876488 kB
Buffers:         35216 kB
Cached:          87344 kB
SwapCached:       2628 kB
Active:          49784 kB
Inactive:        78208 kB
HighTotal:      131008 kB
HighFree:        39956 kB
LowTotal:       903652 kB
LowFree:        836532 kB
SwapTotal:     2097892 kB
SwapFree:      2095264 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24564 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:26:53 (client local time) WITH STATUS 20 IN 434.738 SECONDS
stats: 4515 7 434.738 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 50 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   27
c ---[  16]---> BDD-cost:   27
c ---[  15]---> BDD-cost:   27
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   27
c ---[  10]---> BDD-cost:   27
c ---[   9]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   27
c ---[   4]---> BDD-cost:   27
c ---[   3]---> BDD-cost:   27
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2370     6760 |     790       0        0     nan |  0.000 % |
c |       100 |    2370     6760 |     869     100     2863    28.6 |  2.381 % |
c |       250 |    2360     6730 |     955     241     9633    40.0 |  2.619 % |
c |       476 |    2350     6700 |    1051     461    21095    45.8 |  2.857 % |
c |       814 |    2350     6700 |    1156     799    37977    47.5 |  2.857 % |
c |      1323 |    2345     6685 |    1272     695    30265    43.5 |  2.976 % |
c |      2082 |    2340     6670 |    1399     753    32174    42.7 |  3.095 % |
c |      3224 |    2340     6670 |    1539    1166    51557    44.2 |  3.095 % |
c |      4932 |    2340     6670 |    1693    1191    49367    41.5 |  3.095 % |
c |      7496 |    2280     6490 |    1862     998    42985    43.1 |  4.524 % |
c |     11342 |    2265     6445 |    2049    1829    73664    40.3 |  4.881 % |
c |     17109 |    2260     6430 |    2253    2061    81713    39.6 |  5.000 % |
c |     25759 |    2235     6355 |    2479    2332    92564    39.7 |  5.595 % |
c |     38734 |    2180     6190 |    2727    2102    80050    38.1 |  6.905 % |
c |     58196 |    2061     5835 |    3000    2440   110736    45.4 |  9.762 % |
c |     87388 |    1827     5135 |    3300    2417   105346    43.6 | 15.357 % |
c |    131181 |    1599     4455 |    3630    3110   137052    44.1 | 20.833 % |
c |    196866 |    1426     3940 |    3993    3788   149405    39.4 | 25.000 % |
c |    295393 |    1212     3300 |    4392    2550   103267    40.5 | 30.119 % |
c |    443182 |    1168     3170 |    4831    2848   114507    40.2 | 31.191 % |
c |    664865 |    1130     3060 |    5314    3017   105178    34.9 | 32.143 % |
c ==============================================================================
c [1mUNSATISFIABLE[0m
s UNKNOWN
c _______________________________________________________________________________
c 
c restarts              : 21
c conflicts             : 965292         (2221 /sec)
c decisions             : 1138147        (2619 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 434.528 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.92 0.96 0.91 2/54 2574
Raw data (stat): 2574 (runsolver) R 2573 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481298795 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0011 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 583 0 0 0 997 1 0 0 25 0 1 0 481298795 3883008 561 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 948 561 603 41 0 907 0
vsize: 3792
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 691 0 0 0 1996 2 0 0 25 0 1 0 481298795 4427776 669 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1081 669 603 41 0 1040 0
vsize: 4324
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 752 0 0 0 2996 2 0 0 25 0 1 0 481298795 4698112 730 4294967295 134512640 134672761 3221224544 3221223728 134558290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1147 730 603 41 0 1106 0
vsize: 4588
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 801 0 0 0 3995 2 0 0 25 0 1 0 481298795 4833280 779 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1180 779 603 41 0 1139 0
vsize: 4720
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 838 0 0 0 4995 3 0 0 25 0 1 0 481298795 4968448 816 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1213 816 603 41 0 1172 0
vsize: 4852
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 876 0 0 0 5994 3 0 0 25 0 1 0 481298795 5251072 854 4294967295 134512640 134672761 3221224544 3221223728 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1282 854 603 41 0 1241 0
vsize: 5128
[startup+70.0044 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 911 0 0 0 6993 4 0 0 25 0 1 0 481298795 5398528 889 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1318 889 603 41 0 1277 0
vsize: 5272
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 944 0 0 0 7993 4 0 0 25 0 1 0 481298795 5533696 922 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1351 922 603 41 0 1310 0
vsize: 5404
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 970 0 0 0 8992 5 0 0 25 0 1 0 481298795 5681152 948 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1387 948 603 41 0 1346 0
vsize: 5548
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1008 0 0 0 9991 6 0 0 25 0 1 0 481298795 5824512 986 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1422 986 603 41 0 1381 0
vsize: 5688
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1046 0 0 0 10991 7 0 0 25 0 1 0 481298795 5959680 1024 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1455 1024 603 41 0 1414 0
vsize: 5820
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1049 0 0 0 11990 7 0 0 25 0 1 0 481298795 5959680 1027 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1455 1027 603 41 0 1414 0
vsize: 5820
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1062 0 0 0 12989 8 0 0 25 0 1 0 481298795 6098944 1040 4294967295 134512640 134672761 3221224544 3221223784 134541793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1489 1040 603 41 0 1448 0
vsize: 5956
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1072 0 0 0 13989 8 0 0 25 0 1 0 481298795 6098944 1050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1489 1050 603 41 0 1448 0
vsize: 5956
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1082 0 0 0 14988 9 0 0 25 0 1 0 481298795 6098944 1060 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1489 1060 603 41 0 1448 0
vsize: 5956
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1104 0 0 0 15988 9 0 0 25 0 1 0 481298795 6242304 1082 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1524 1082 603 41 0 1483 0
vsize: 6096
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1134 0 0 0 16987 10 0 0 25 0 1 0 481298795 6377472 1112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1557 1112 603 41 0 1516 0
vsize: 6228
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1151 0 0 0 17987 10 0 0 25 0 1 0 481298795 6377472 1129 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1557 1129 603 41 0 1516 0
vsize: 6228
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1160 0 0 0 18986 11 0 0 25 0 1 0 481298795 6524928 1138 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1593 1138 603 41 0 1552 0
vsize: 6372
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1178 0 0 0 19986 11 0 0 25 0 1 0 481298795 6524928 1156 4294967295 134512640 134672761 3221224544 3221223728 134558909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1593 1156 603 41 0 1552 0
vsize: 6372
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1187 0 0 0 20986 11 0 0 25 0 1 0 481298795 6672384 1165 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1165 603 41 0 1588 0
vsize: 6516
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1196 0 0 0 21985 12 0 0 25 0 1 0 481298795 6672384 1174 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1174 603 41 0 1588 0
vsize: 6516
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1218 0 0 0 22985 12 0 0 25 0 1 0 481298795 6672384 1196 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1196 603 41 0 1588 0
vsize: 6516
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1252 0 0 0 23984 13 0 0 25 0 1 0 481298795 6938624 1230 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1230 603 41 0 1653 0
vsize: 6776
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1267 0 0 0 24984 13 0 0 25 0 1 0 481298795 6938624 1245 4294967295 134512640 134672761 3221224544 3221223600 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1245 603 41 0 1653 0
vsize: 6776
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1275 0 0 0 25983 14 0 0 25 0 1 0 481298795 6938624 1253 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1253 603 41 0 1653 0
vsize: 6776
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1276 0 0 0 26983 14 0 0 25 0 1 0 481298795 6938624 1254 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1254 603 41 0 1653 0
vsize: 6776
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1283 0 0 0 27982 15 0 0 25 0 1 0 481298795 6938624 1261 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1261 603 41 0 1653 0
vsize: 6776
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1287 0 0 0 28982 15 0 0 25 0 1 0 481298795 6938624 1265 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1265 603 41 0 1653 0
vsize: 6776
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1293 0 0 0 29981 15 0 0 25 0 1 0 481298795 7073792 1271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1727 1271 603 41 0 1686 0
vsize: 6908
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1319 0 0 0 30981 16 0 0 25 0 1 0 481298795 7073792 1297 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1727 1297 603 41 0 1686 0
vsize: 6908
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1325 0 0 0 31980 16 0 0 25 0 1 0 481298795 7073792 1303 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1727 1303 603 41 0 1686 0
vsize: 6908
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1334 0 0 0 32980 17 0 0 25 0 1 0 481298795 7213056 1312 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1312 603 41 0 1720 0
vsize: 7044
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1336 0 0 0 33979 17 0 0 25 0 1 0 481298795 7213056 1314 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1314 603 41 0 1720 0
vsize: 7044
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1337 0 0 0 34979 18 0 0 25 0 1 0 481298795 7213056 1315 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1315 603 41 0 1720 0
vsize: 7044
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1338 0 0 0 35978 18 0 0 25 0 1 0 481298795 7213056 1316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1316 603 41 0 1720 0
vsize: 7044
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1339 0 0 0 36978 19 0 0 25 0 1 0 481298795 7213056 1317 4294967295 134512640 134672761 3221224544 3221223744 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1317 603 41 0 1720 0
vsize: 7044
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1339 0 0 0 37977 19 0 0 25 0 1 0 481298795 7213056 1317 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1317 603 41 0 1720 0
vsize: 7044
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1344 0 0 0 38977 19 0 0 25 0 1 0 481298795 7213056 1322 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1322 603 41 0 1720 0
vsize: 7044
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1346 0 0 0 39977 20 0 0 25 0 1 0 481298795 7213056 1324 4294967295 134512640 134672761 3221224544 3221223640 134555595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1324 603 41 0 1720 0
vsize: 7044
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1354 0 0 0 40976 20 0 0 25 0 1 0 481298795 7213056 1332 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1332 603 41 0 1720 0
vsize: 7044
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1354 0 0 0 41976 20 0 0 25 0 1 0 481298795 7213056 1332 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1332 603 41 0 1720 0
vsize: 7044
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1360 0 0 0 42976 20 0 0 25 0 1 0 481298795 7213056 1338 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1338 603 41 0 1720 0
vsize: 7044
[startup+434.791 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 2574
Raw data (stat): 2574 (minisat+) R 2573 27565 27564 0 -1 0 1360 0 0 0 42976 20 0 0 25 0 1 0 481298795 7213056 1338 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1338 603 41 0 1720 0
vsize: 0

Child status: 20
Real time (s): 434.79
CPU time (s): 434.738
CPU user time (s): 434.528
CPU system time (s): 0.209968
CPU usage (%): 99.9879
Max. virtual memory (Kb): 7044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####