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_20_pb.cnf.cr.opb
MD5SUM	f6063d1ff7b0ba7c7cab7a438daedff8
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	21
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.013997
Number of variables	400
Total number of constraints	60
Number of constraints which are clauses	40
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	20

Trace number 4693

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-13 20:08:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=32 boxname=wulflinc29 idbench=4 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  f6063d1ff7b0ba7c7cab7a438daedff8  /oldhome/oroussel/tmp/wulflinc29/normalized-chnl10_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-chnl10_20_pb.cnf.cr.opb
IDLAUNCH: 32
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        861488 kB
Buffers:         35536 kB
Cached:         100248 kB
SwapCached:         12 kB
Active:          51912 kB
Inactive:        86732 kB
HighTotal:      131008 kB
HighFree:        27300 kB
LowTotal:       903652 kB
LowFree:        834188 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            28876 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:15:53 (client local time) WITH STATUS 20 IN 442.568 SECONDS
stats: 32 7 442.568 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1860     5140 |     620       0        0     nan |  0.000 % |
c |       105 |    1860     5140 |     682     105     3115    29.7 |  1.754 % |
c |       255 |    1860     5140 |     750     255     9122    35.8 |  1.754 % |
c |       483 |    1860     5140 |     825     483    17860    37.0 |  1.757 % |
c |       827 |    1860     5140 |     907     827    34782    42.1 |  1.754 % |
c |      1336 |    1860     5140 |     998     794    35805    45.1 |  1.754 % |
c |      2095 |    1860     5140 |    1098     963    46131    47.9 |  1.755 % |
c |      3236 |    1860     5140 |    1208     855    38655    45.2 |  1.754 % |
c |      4945 |    1860     5140 |    1329    1223    54808    44.8 |  1.754 % |
c |      7507 |    1860     5140 |    1461    1529    70881    46.4 |  1.754 % |
c |     11351 |    1860     5140 |    1608    1297    60011    46.3 |  1.754 % |
c |     17122 |    1860     5140 |    1768     913    38075    41.7 |  1.754 % |
c |     25774 |    1860     5140 |    1945    1876    79748    42.5 |  1.754 % |
c |     38751 |    1860     5140 |    2140    2159    98991    45.9 |  1.754 % |
c |     58213 |    1860     5140 |    2354    1826    83310    45.6 |  1.754 % |
c |     87405 |    1860     5140 |    2589    1714    82979    48.4 |  1.754 % |
c |    131197 |    1860     5140 |    2848    2605   131009    50.3 |  1.754 % |
c |    196881 |    1860     5140 |    3133    2788   128801    46.2 |  1.754 % |
c |    295409 |    1860     5140 |    3447    2681   117056    43.7 |  1.754 % |
c |    443198 |    1860     5140 |    3791    2782   140828    50.6 |  1.754 % |
c |    664881 |    1860     5140 |    4171    3279   124739    38.0 |  1.754 % |
c |    997406 |    1860     5140 |    4588    3602   150963    41.9 |  1.758 % |
c ==============================================================================
c [1mUNSATISFIABLE[0m
s UNKNOWN
c _______________________________________________________________________________
c 
c restarts              : 22
c conflicts             : 1137344        (2570 /sec)
c decisions             : 1289572        (2914 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 442.51 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.97 0.89 2/54 29372
Raw data (stat): 29372 (runsolver) R 29371 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478709701 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0001 s]
Raw data (loadavg): 0.93 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 594 0 0 0 996 1 0 0 25 0 1 0 478709701 3928064 572 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 959 572 603 41 0 918 0
vsize: 3836
[startup+20 s]
Raw data (loadavg): 0.94 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 660 0 0 0 1995 2 0 0 25 0 1 0 478709701 4198400 638 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1025 638 603 41 0 984 0
vsize: 4100
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 704 0 0 0 2994 2 0 0 25 0 1 0 478709701 4476928 682 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1093 682 603 41 0 1052 0
vsize: 4372
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 728 0 0 0 3994 2 0 0 25 0 1 0 478709701 4476928 706 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1093 706 603 41 0 1052 0
vsize: 4372
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 762 0 0 0 4994 2 0 0 25 0 1 0 478709701 4612096 740 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1126 740 603 41 0 1085 0
vsize: 4504
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 774 0 0 0 5994 2 0 0 25 0 1 0 478709701 4747264 752 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1159 752 603 41 0 1118 0
vsize: 4636
[startup+70.0017 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 803 0 0 0 6994 3 0 0 25 0 1 0 478709701 4886528 781 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1193 781 603 41 0 1152 0
vsize: 4772
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 814 0 0 0 7994 3 0 0 25 0 1 0 478709701 4886528 792 4294967295 134512640 134672761 3221224624 3221223776 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1193 792 603 41 0 1152 0
vsize: 4772
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 835 0 0 0 8994 3 0 0 25 0 1 0 478709701 5029888 813 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1228 813 603 41 0 1187 0
vsize: 4912
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 844 0 0 0 9995 3 0 0 25 0 1 0 478709701 5029888 822 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1228 822 603 41 0 1187 0
vsize: 4912
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 876 0 0 0 10994 3 0 0 25 0 1 0 478709701 5165056 854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1261 854 603 41 0 1220 0
vsize: 5044
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 936 0 0 0 11994 4 0 0 25 0 1 0 478709701 5443584 914 4294967295 134512640 134672761 3221224624 3221223728 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1329 914 603 41 0 1288 0
vsize: 5316
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 947 0 0 0 12994 4 0 0 25 0 1 0 478709701 5443584 925 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1329 925 603 41 0 1288 0
vsize: 5316
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 952 0 0 0 13994 4 0 0 25 0 1 0 478709701 5443584 930 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1329 930 603 41 0 1288 0
vsize: 5316
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 985 0 0 0 14995 4 0 0 25 0 1 0 478709701 5578752 963 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1362 963 603 41 0 1321 0
vsize: 5448
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1004 0 0 0 15995 4 0 0 25 0 1 0 478709701 5713920 982 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1395 982 603 41 0 1354 0
vsize: 5580
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1016 0 0 0 16995 4 0 0 25 0 1 0 478709701 5713920 994 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1395 994 603 41 0 1354 0
vsize: 5580
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1035 0 0 0 17995 4 0 0 25 0 1 0 478709701 5853184 1013 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1429 1013 603 41 0 1388 0
vsize: 5716
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1063 0 0 0 18995 4 0 0 25 0 1 0 478709701 5996544 1041 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1464 1041 603 41 0 1423 0
vsize: 5856
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1073 0 0 0 19995 4 0 0 25 0 1 0 478709701 5996544 1051 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1464 1051 603 41 0 1423 0
vsize: 5856
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1086 0 0 0 20995 4 0 0 25 0 1 0 478709701 5996544 1064 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1464 1064 603 41 0 1423 0
vsize: 5856
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1087 0 0 0 21995 4 0 0 25 0 1 0 478709701 5996544 1065 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1464 1065 603 41 0 1423 0
vsize: 5856
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1091 0 0 0 22995 4 0 0 25 0 1 0 478709701 5996544 1069 4294967295 134512640 134672761 3221224624 3221223808 134558553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1464 1069 603 41 0 1423 0
vsize: 5856
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1097 0 0 0 23995 4 0 0 25 0 1 0 478709701 6144000 1075 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1500 1075 603 41 0 1459 0
vsize: 6000
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1109 0 0 0 24996 4 0 0 25 0 1 0 478709701 6144000 1087 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1500 1087 603 41 0 1459 0
vsize: 6000
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1125 0 0 0 25996 4 0 0 25 0 1 0 478709701 6291456 1103 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1103 603 41 0 1495 0
vsize: 6144
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1126 0 0 0 26996 4 0 0 25 0 1 0 478709701 6291456 1104 4294967295 134512640 134672761 3221224624 3221223728 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1104 603 41 0 1495 0
vsize: 6144
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1144 0 0 0 27996 4 0 0 25 0 1 0 478709701 6291456 1122 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1122 603 41 0 1495 0
vsize: 6144
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1155 0 0 0 28996 4 0 0 25 0 1 0 478709701 6291456 1133 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1133 603 41 0 1495 0
vsize: 6144
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1172 0 0 0 29996 4 0 0 25 0 1 0 478709701 6434816 1150 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1571 1150 603 41 0 1530 0
vsize: 6284
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1184 0 0 0 30997 4 0 0 25 0 1 0 478709701 6434816 1162 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1571 1162 603 41 0 1530 0
vsize: 6284
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1199 0 0 0 31997 4 0 0 25 0 1 0 478709701 6569984 1177 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1604 1177 603 41 0 1563 0
vsize: 6416
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1206 0 0 0 32997 4 0 0 25 0 1 0 478709701 6569984 1184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1604 1184 603 41 0 1563 0
vsize: 6416
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1230 0 0 0 33997 4 0 0 25 0 1 0 478709701 6717440 1208 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1208 603 41 0 1599 0
vsize: 6560
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1242 0 0 0 34997 4 0 0 25 0 1 0 478709701 6717440 1220 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1220 603 41 0 1599 0
vsize: 6560
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1250 0 0 0 35997 4 0 0 25 0 1 0 478709701 6852608 1228 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1673 1228 603 41 0 1632 0
vsize: 6692
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1250 0 0 0 36997 4 0 0 25 0 1 0 478709701 6852608 1228 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1673 1228 603 41 0 1632 0
vsize: 6692
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1262 0 0 0 37997 5 0 0 25 0 1 0 478709701 6852608 1240 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1673 1240 603 41 0 1632 0
vsize: 6692
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1270 0 0 0 38997 5 0 0 25 0 1 0 478709701 6852608 1248 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1673 1248 603 41 0 1632 0
vsize: 6692
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1284 0 0 0 39997 5 0 0 25 0 1 0 478709701 6987776 1262 4294967295 134512640 134672761 3221224624 3221223788 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1706 1262 603 41 0 1665 0
vsize: 6824
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1297 0 0 0 40997 5 0 0 25 0 1 0 478709701 6987776 1275 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1706 1275 603 41 0 1665 0
vsize: 6824
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1301 0 0 0 41997 5 0 0 25 0 1 0 478709701 6987776 1279 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1706 1279 603 41 0 1665 0
vsize: 6824
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1305 0 0 0 42997 5 0 0 25 0 1 0 478709701 6987776 1283 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1706 1283 603 41 0 1665 0
vsize: 6824
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1312 0 0 0 43997 5 0 0 25 0 1 0 478709701 6987776 1290 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1706 1290 603 41 0 1665 0
vsize: 6824
[startup+442.544 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 29372
Raw data (stat): 29372 (minisat+) R 29371 27222 27221 0 -1 0 1312 0 0 0 43997 5 0 0 25 0 1 0 478709701 6987776 1290 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1706 1290 603 41 0 1665 0
vsize: 0

Child status: 20
Real time (s): 442.544
CPU time (s): 442.568
CPU user time (s): 442.51
CPU system time (s): 0.057991
CPU usage (%): 100.005
Max. virtual memory (Kb): 6824
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####