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 5649

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-14 01:30:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4140 boxname=wulflinc29 idbench=4 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f6063d1ff7b0ba7c7cab7a438daedff8  /oldhome/oroussel/tmp/wulflinc29/normalized-chnl10_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc29/normalized-chnl10_20_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc29/normalized-chnl10_20_pb.cnf.cr.opb
IDLAUNCH: 4140
/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:        821704 kB
Buffers:         36612 kB
Cached:         138748 kB
SwapCached:         12 kB
Active:          53448 kB
Inactive:       124696 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        821452 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29012 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:37:24 (client local time) WITH STATUS 20 IN 442.41 SECONDS
stats: 4140 7 442.41 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        (2571 /sec)
c decisions             : 1289572        (2915 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 442.362 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.99 0.99 0.92 1/54 32737
Raw data (stat): 32737 (runsolver) R 32736 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480639130 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99995 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 594 0 0 0 996 1 0 0 25 0 1 0 480639130 3928064 572 4294967295 134512640 134672761 3221224528 3221223692 134565024 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.0007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 660 0 0 0 1996 1 0 0 25 0 1 0 480639130 4198400 638 4294967295 134512640 134672761 3221224528 3221223664 134566155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1025 638 603 41 0 984 0
vsize: 4100
[startup+30.0011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 704 0 0 0 2996 1 0 0 25 0 1 0 480639130 4476928 682 4294967295 134512640 134672761 3221224528 3221223696 134561001 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.0002 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 728 0 0 0 3996 2 0 0 25 0 1 0 480639130 4476928 706 4294967295 134512640 134672761 3221224528 3221223712 134559340 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 762 0 0 0 4996 2 0 0 25 0 1 0 480639130 4612096 740 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 774 0 0 0 5996 2 0 0 25 0 1 0 480639130 4747264 752 4294967295 134512640 134672761 3221224528 3221223632 134560196 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.0015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 803 0 0 0 6996 2 0 0 25 0 1 0 480639130 4886528 781 4294967295 134512640 134672761 3221224528 3221223696 134561188 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.0013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 814 0 0 0 7996 2 0 0 25 0 1 0 480639130 4886528 792 4294967295 134512640 134672761 3221224528 3221223696 134561218 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.0013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 835 0 0 0 8996 2 0 0 25 0 1 0 480639130 5029888 813 4294967295 134512640 134672761 3221224528 3221223696 134560869 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 844 0 0 0 9996 2 0 0 25 0 1 0 480639130 5029888 822 4294967295 134512640 134672761 3221224528 3221223696 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 876 0 0 0 10997 2 0 0 25 0 1 0 480639130 5165056 854 4294967295 134512640 134672761 3221224528 3221223696 134561008 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.002 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 936 0 0 0 11997 2 0 0 25 0 1 0 480639130 5443584 914 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 947 0 0 0 12997 2 0 0 25 0 1 0 480639130 5443584 925 4294967295 134512640 134672761 3221224528 3221223696 134560942 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 956 0 0 0 13997 2 0 0 25 0 1 0 480639130 5443584 934 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1329 934 603 41 0 1288 0
vsize: 5316
[startup+150.002 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 985 0 0 0 14997 2 0 0 25 0 1 0 480639130 5578752 963 4294967295 134512640 134672761 3221224528 3221223696 134560980 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1006 0 0 0 15997 2 0 0 25 0 1 0 480639130 5713920 984 4294967295 134512640 134672761 3221224528 3221223712 134558248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1395 984 603 41 0 1354 0
vsize: 5580
[startup+170.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1016 0 0 0 16997 2 0 0 25 0 1 0 480639130 5713920 994 4294967295 134512640 134672761 3221224528 3221223696 134560983 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1039 0 0 0 17997 2 0 0 25 0 1 0 480639130 5853184 1017 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1429 1017 603 41 0 1388 0
vsize: 5716
[startup+190.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1063 0 0 0 18997 2 0 0 25 0 1 0 480639130 5996544 1041 4294967295 134512640 134672761 3221224528 3221223696 134560983 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1073 0 0 0 19997 2 0 0 25 0 1 0 480639130 5996544 1051 4294967295 134512640 134672761 3221224528 3221223696 134560903 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1086 0 0 0 20998 2 0 0 25 0 1 0 480639130 5996544 1064 4294967295 134512640 134672761 3221224528 3221223712 134558662 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1087 0 0 0 21998 2 0 0 25 0 1 0 480639130 5996544 1065 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1091 0 0 0 22998 2 0 0 25 0 1 0 480639130 5996544 1069 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1097 0 0 0 23998 2 0 0 25 0 1 0 480639130 6144000 1075 4294967295 134512640 134672761 3221224528 3221223696 134561121 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.002 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1109 0 0 0 24998 2 0 0 25 0 1 0 480639130 6144000 1087 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1500 1087 603 41 0 1459 0
vsize: 6000
[startup+260.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1125 0 0 0 25998 2 0 0 25 0 1 0 480639130 6291456 1103 4294967295 134512640 134672761 3221224528 3221223632 134560289 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1126 0 0 0 26998 3 0 0 25 0 1 0 480639130 6291456 1104 4294967295 134512640 134672761 3221224528 3221223696 134561218 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1144 0 0 0 27998 3 0 0 25 0 1 0 480639130 6291456 1122 4294967295 134512640 134672761 3221224528 3221223696 134560983 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1155 0 0 0 28998 3 0 0 25 0 1 0 480639130 6291456 1133 4294967295 134512640 134672761 3221224528 3221223664 134560688 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.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1172 0 0 0 29998 3 0 0 25 0 1 0 480639130 6434816 1150 4294967295 134512640 134672761 3221224528 3221223696 134560903 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1184 0 0 0 30998 3 0 0 25 0 1 0 480639130 6434816 1162 4294967295 134512640 134672761 3221224528 3221223632 134559866 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1199 0 0 0 31998 3 0 0 25 0 1 0 480639130 6569984 1177 4294967295 134512640 134672761 3221224528 3221223696 134560983 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1206 0 0 0 32999 3 0 0 25 0 1 0 480639130 6569984 1184 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1604 1184 603 41 0 1563 0
vsize: 6416
[startup+339.999 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1230 0 0 0 33999 3 0 0 25 0 1 0 480639130 6717440 1208 4294967295 134512640 134672761 3221224528 3221223688 134559749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1208 603 41 0 1599 0
vsize: 6560
[startup+349.999 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1242 0 0 0 34999 3 0 0 25 0 1 0 480639130 6717440 1220 4294967295 134512640 134672761 3221224528 3221223688 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1220 603 41 0 1599 0
vsize: 6560
[startup+359.999 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1250 0 0 0 35999 3 0 0 25 0 1 0 480639130 6852608 1228 4294967295 134512640 134672761 3221224528 3221223696 134561218 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1253 0 0 0 36999 3 0 0 25 0 1 0 480639130 6852608 1231 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1673 1231 603 41 0 1632 0
vsize: 6692
[startup+379.999 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1262 0 0 0 37999 3 0 0 25 0 1 0 480639130 6852608 1240 4294967295 134512640 134672761 3221224528 3221223696 134560898 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1270 0 0 0 38998 3 0 0 25 0 1 0 480639130 6852608 1248 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1673 1248 603 41 0 1632 0
vsize: 6692
[startup+400 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1284 0 0 0 39999 3 0 0 25 0 1 0 480639130 6987776 1262 4294967295 134512640 134672761 3221224528 3221223632 134560212 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1297 0 0 0 40999 3 0 0 25 0 1 0 480639130 6987776 1275 4294967295 134512640 134672761 3221224528 3221223696 134560898 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1301 0 0 0 41999 3 0 0 25 0 1 0 480639130 6987776 1279 4294967295 134512640 134672761 3221224528 3221223696 134560983 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1305 0 0 0 42999 3 0 0 25 0 1 0 480639130 6987776 1283 4294967295 134512640 134672761 3221224528 3221223696 134560920 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 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1312 0 0 0 43999 4 0 0 25 0 1 0 480639130 6987776 1290 4294967295 134512640 134672761 3221224528 3221223696 134561118 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.377 s]
Raw data (loadavg): 0.99 0.99 0.92 1/53 32737
Raw data (stat): 32737 (minisat+) R 32736 27222 27221 0 -1 0 1312 0 0 0 43999 4 0 0 25 0 1 0 480639130 6987776 1290 4294967295 134512640 134672761 3221224528 3221223696 134561118 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.376
CPU time (s): 442.41
CPU user time (s): 442.363
CPU system time (s): 0.046992
CPU usage (%): 100.008
Max. virtual memory (Kb): 6824
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####