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-fpga45_43_sat_pb.cnf.cr.opb
MD5SUM	f711bed5ebfe5c735a8c12d953afb97c
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	9.61454
Number of variables	2903
Total number of constraints	2066
Number of constraints which are clauses	1978
Number of constraints which are cardinality constraints (but not clauses)	88
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	22
Maximum length of a constraint	45
Trace number 4650

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-13 19:28:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3439 boxname=wulflinc2 idbench=55 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f711bed5ebfe5c735a8c12d953afb97c  /oldhome/oroussel/tmp/wulflinc2/normalized-fpga45_43_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc2/normalized-fpga45_43_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc2/normalized-fpga45_43_sat_pb.cnf.cr.opb
IDLAUNCH: 3439
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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	: 2
cpu MHz		: 451.191
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:        913260 kB
Buffers:         33108 kB
Cached:          67868 kB
SwapCached:          4 kB
Active:          52296 kB
Inactive:        51576 kB
HighTotal:      131008 kB
HighFree:        59248 kB
LowTotal:       903652 kB
LowFree:        854012 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11964 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:49:03 (client local time) WITH STATUS 0 IN 1210.07 SECONDS
stats: 3439 7 1210.07 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2066 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  87]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  86]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  85]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  84]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  83]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  82]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  81]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  80]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  79]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  78]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  77]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  76]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  75]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  74]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  73]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  72]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  71]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  70]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  69]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  68]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  67]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  66]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  65]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  64]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  63]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  62]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  61]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  60]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  59]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  58]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  57]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  56]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  55]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  54]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  53]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  52]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  51]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  50]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  49]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  48]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  47]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  46]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  45]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  44]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  43]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  42]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  41]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  40]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  39]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  38]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  37]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  36]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  35]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  34]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  33]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  32]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  31]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  30]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  29]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  28]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  27]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  26]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  25]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  24]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  23]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  22]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[  21]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  20]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  19]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  18]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  17]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  16]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  15]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  14]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  13]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  12]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  11]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[  10]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   9]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   8]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   7]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   6]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   5]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   4]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   3]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   2]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   1]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[   0]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   34458   161104 |   11486       0        0     nan |  0.000 % |
c |       102 |   33792   158699 |   12634       2        4     2.0 | 10.152 % |
c |       252 |   33666   158244 |   13898     132      468     3.5 | 10.520 % |
c |       477 |   33427   157416 |   15287     320     1316     4.1 | 11.010 % |
c |       814 |   33152   156455 |   16816     612     2366     3.9 | 11.550 % |
c |      1320 |   32915   155620 |   18498    1084     4166     3.8 | 12.040 % |
c |      2079 |   32147   152904 |   20348    1743     7508     4.3 | 13.671 % |
c |      3219 |   30455   146920 |   22382    2635    12019     4.6 | 17.227 % |
c |      4928 |   22065   118374 |   24621    2932    24776     8.5 | 35.802 % |
c |      7491 |   21408   116181 |   27083    5387   570582   105.9 | 37.249 % |
c |     11335 |   21333   115938 |   29791    9218  1598454   173.4 | 37.433 % |
c |     17102 |   21183   115444 |   32770   14963  3571873   238.7 | 37.788 % |
c |     25754 |   21146   115319 |   36047   23610  8208441   347.7 | 37.886 % |
c |     38731 |   20799   114120 |   39652   36531 15115214   413.8 | 38.622 % |
c |     58194 |   19619   110077 |   43618   23976 17442332   727.5 | 41.172 % |
c |     87388 |   18138   105111 |   47979   16378  8725301   532.7 | 44.544 % |
c |    131179 |   18081   104916 |   52777   21287 21661104  1017.6 | 44.654 % |
#### 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.00 2/54 22262
Raw data (stat): 22262 (runsolver) R 22261 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420254976 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+9.99997 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 1145 0 1 0 973 3 0 0 25 0 1 0 420254976 6316032 1123 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1542 1123 603 41 0 1501 0
vsize: 6168
[startup+20.0002 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 1151 0 1 0 1972 3 0 0 25 0 1 0 420254976 6316032 1129 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1542 1129 603 41 0 1501 0
vsize: 6168
[startup+30.0006 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 2438 0 1 0 2967 7 0 0 25 0 1 0 420254976 11591680 2416 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2830 2416 603 41 0 2789 0
vsize: 11320
[startup+40 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 4358 0 1 0 3963 11 0 0 25 0 1 0 420254976 19472384 4336 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4754 4337 603 41 0 4713 0
vsize: 19016
[startup+50.001 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 6164 0 1 0 4961 14 0 0 25 0 1 0 420254976 26894336 6142 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6566 6142 603 41 0 6525 0
vsize: 26264
[startup+60.0007 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 7578 0 1 0 5958 17 0 0 25 0 1 0 420254976 32702464 7556 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7984 7556 603 41 0 7943 0
vsize: 31936
[startup+70.0001 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 8791 0 1 0 6954 21 0 0 25 0 1 0 420254976 37691392 8769 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9202 8769 603 41 0 9161 0
vsize: 36808
[startup+80.0011 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 9742 0 1 0 7952 23 0 0 25 0 1 0 420254976 41611264 9720 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10159 9720 603 41 0 10118 0
vsize: 40636
[startup+90.0008 s]
Raw data (loadavg): 0.85 0.27 0.09 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 11104 0 1 0 8949 26 0 0 25 0 1 0 420254976 47136768 11082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11508 11082 603 41 0 11467 0
vsize: 46032
[startup+100.001 s]
Raw data (loadavg): 0.87 0.30 0.10 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 12619 0 1 0 9946 30 0 0 25 0 1 0 420254976 53350400 12597 4294967295 134512640 134672761 3221224544 3221223728 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13025 12597 603 41 0 12984 0
vsize: 52100
[startup+110.001 s]
Raw data (loadavg): 0.89 0.32 0.11 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 14117 0 1 0 10943 33 0 0 25 0 1 0 420254976 59568128 14095 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14095 603 41 0 14502 0
vsize: 58172
[startup+120.001 s]
Raw data (loadavg): 0.91 0.34 0.12 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 15310 0 1 0 11940 36 0 0 25 0 1 0 420254976 64557056 15288 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15761 15288 603 41 0 15720 0
vsize: 63044
[startup+130.001 s]
Raw data (loadavg): 0.92 0.36 0.13 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 16499 0 1 0 12937 39 0 0 25 0 1 0 420254976 69419008 16477 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16948 16477 603 41 0 16907 0
vsize: 67792
[startup+140.001 s]
Raw data (loadavg): 0.93 0.38 0.14 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 17582 0 1 0 13935 41 0 0 25 0 1 0 420254976 73871360 17560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18035 17560 603 41 0 17994 0
vsize: 72140
[startup+150.002 s]
Raw data (loadavg): 0.94 0.40 0.15 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 18614 0 1 0 14932 44 0 0 25 0 1 0 420254976 78036992 18592 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19052 18592 603 41 0 19011 0
vsize: 76208
[startup+160.003 s]
Raw data (loadavg): 0.95 0.42 0.16 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 19678 0 1 0 15930 46 0 0 25 0 1 0 420254976 82485248 19656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20138 19657 603 41 0 20097 0
vsize: 80552
[startup+170.002 s]
Raw data (loadavg): 0.96 0.44 0.16 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 20647 0 1 0 16928 49 0 0 25 0 1 0 420254976 86401024 20625 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21094 20625 603 41 0 21053 0
vsize: 84376
[startup+180.003 s]
Raw data (loadavg): 0.96 0.46 0.17 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 17926 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+190.003 s]
Raw data (loadavg): 0.97 0.48 0.18 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 18926 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+200.003 s]
Raw data (loadavg): 0.97 0.49 0.19 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 19927 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+210.003 s]
Raw data (loadavg): 0.98 0.51 0.20 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 20927 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+220.003 s]
Raw data (loadavg): 0.98 0.52 0.21 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 21927 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+230.004 s]
Raw data (loadavg): 0.98 0.54 0.21 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 22927 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+240.003 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 23927 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+250.004 s]
Raw data (loadavg): 0.99 0.57 0.23 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 24928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+260.005 s]
Raw data (loadavg): 0.99 0.58 0.24 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 25928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+270.005 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 26928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+280.005 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 27928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+290.005 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 28928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+300.005 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 29929 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+310.005 s]
Raw data (loadavg): 0.99 0.64 0.28 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 30928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+320.005 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 31928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+330.006 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 32928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+340.006 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 33928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+350.007 s]
Raw data (loadavg): 0.99 0.69 0.30 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21408 0 1 0 34928 51 0 0 25 0 1 0 420254976 89513984 21386 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 21386 603 41 0 21813 0
vsize: 87416
[startup+360.007 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 21820 0 1 0 35928 52 0 0 25 0 1 0 420254976 91271168 21798 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22283 21798 603 41 0 22242 0
vsize: 89132
[startup+370.006 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 22100 0 1 0 36928 52 0 0 25 0 1 0 420254976 92360704 22078 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22549 22078 603 41 0 22508 0
vsize: 90196
[startup+380.007 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 22122 0 1 0 37928 52 0 0 25 0 1 0 420254976 92495872 22100 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22582 22100 603 41 0 22541 0
vsize: 90328
[startup+390.007 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 23239 0 1 0 38926 54 0 0 25 0 1 0 420254976 97087488 23217 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23703 23217 603 41 0 23662 0
vsize: 94812
[startup+400.007 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 25238 0 1 0 39922 58 0 0 25 0 1 0 420254976 105197568 25216 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25683 25216 603 41 0 25642 0
vsize: 102732
[startup+410.008 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 26775 0 1 0 40918 63 0 0 25 0 1 0 420254976 111534080 26753 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27230 26753 603 41 0 27189 0
vsize: 108920
[startup+420.008 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 26997 0 1 0 41918 63 0 0 25 0 1 0 420254976 112484352 26975 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27462 26975 603 41 0 27421 0
vsize: 109848
[startup+430.008 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 28060 0 1 0 42915 66 0 0 25 0 1 0 420254976 116809728 28038 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28518 28038 603 41 0 28477 0
vsize: 114072
[startup+440.009 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 30016 0 1 0 43912 69 0 0 25 0 1 0 420254976 124882944 29994 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30489 29994 603 41 0 30448 0
vsize: 121956
[startup+450.01 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 31556 0 1 0 44909 73 0 0 25 0 1 0 420254976 131190784 31534 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32029 31534 603 41 0 31988 0
vsize: 128116
[startup+460.01 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33470 0 1 0 45905 77 0 0 25 0 1 0 420254976 138924032 33448 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33448 603 41 0 33876 0
vsize: 135668
[startup+470.01 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33470 0 1 0 46905 77 0 0 25 0 1 0 420254976 138924032 33448 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33448 603 41 0 33876 0
vsize: 135668
[startup+480.011 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33470 0 1 0 47904 77 0 0 25 0 1 0 420254976 138924032 33448 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33448 603 41 0 33876 0
vsize: 135668
[startup+490.011 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33470 0 1 0 48904 77 0 0 25 0 1 0 420254976 138924032 33448 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33448 603 41 0 33876 0
vsize: 135668
[startup+500.011 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33470 0 1 0 49905 77 0 0 25 0 1 0 420254976 138924032 33448 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33448 603 41 0 33876 0
vsize: 135668
[startup+510.012 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33470 0 1 0 50905 77 0 0 25 0 1 0 420254976 138924032 33448 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33448 603 41 0 33876 0
vsize: 135668
[startup+520.012 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33471 0 1 0 51905 77 0 0 25 0 1 0 420254976 138924032 33449 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33449 603 41 0 33876 0
vsize: 135668
[startup+530.012 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33471 0 1 0 52905 77 0 0 25 0 1 0 420254976 138924032 33449 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33449 603 41 0 33876 0
vsize: 135668
[startup+540.012 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33471 0 1 0 53906 77 0 0 25 0 1 0 420254976 138924032 33449 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33449 603 41 0 33876 0
vsize: 135668
[startup+550.013 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33471 0 1 0 54906 77 0 0 25 0 1 0 420254976 138924032 33449 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33449 603 41 0 33876 0
vsize: 135668
[startup+560.013 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33471 0 1 0 55906 77 0 0 25 0 1 0 420254976 138924032 33449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33449 603 41 0 33876 0
vsize: 135668
[startup+570.013 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33471 0 1 0 56906 77 0 0 25 0 1 0 420254976 138924032 33449 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33449 603 41 0 33876 0
vsize: 135668
[startup+580.013 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 33471 0 1 0 57906 77 0 0 25 0 1 0 420254976 138924032 33449 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33917 33449 603 41 0 33876 0
vsize: 135668
[startup+590.013 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 34607 0 1 0 58903 81 0 0 25 0 1 0 420254976 143556608 34585 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35048 34585 603 41 0 35007 0
vsize: 140192
[startup+600.013 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 35819 0 1 0 59902 82 0 0 25 0 1 0 420254976 148594688 35797 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36278 35797 603 41 0 36237 0
vsize: 145112
[startup+610.013 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 36502 0 1 0 60900 84 0 0 25 0 1 0 420254976 151318528 36480 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36943 36480 603 41 0 36902 0
vsize: 147772
[startup+620.013 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 37593 0 1 0 61899 85 0 0 25 0 1 0 420254976 155803648 37571 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38038 37571 603 41 0 37997 0
vsize: 152152
[startup+630.014 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 39031 0 1 0 62897 88 0 0 25 0 1 0 420254976 161800192 39009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39502 39009 603 41 0 39461 0
vsize: 158008
[startup+640.013 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 40265 0 1 0 63894 90 0 0 25 0 1 0 420254976 166805504 40243 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40724 40243 603 41 0 40683 0
vsize: 162896
[startup+650.014 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 41387 0 1 0 64892 93 0 0 25 0 1 0 420254976 171421696 41365 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41851 41365 603 41 0 41810 0
vsize: 167404
[startup+660.013 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 42373 0 1 0 65891 94 0 0 25 0 1 0 420254976 175476736 42351 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42841 42351 603 41 0 42800 0
vsize: 171364
[startup+670.013 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 43957 0 1 0 66887 98 0 0 25 0 1 0 420254976 182013952 43935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44437 43935 603 41 0 44396 0
vsize: 177748
[startup+680.014 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 44856 0 1 0 67885 100 0 0 25 0 1 0 420254976 185683968 44834 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45333 44834 603 41 0 45292 0
vsize: 181332
[startup+690.015 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 45814 0 1 0 68884 102 0 0 25 0 1 0 420254976 189607936 45792 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46291 45792 603 41 0 46250 0
vsize: 185164
[startup+700.015 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 46843 0 1 0 69882 104 0 0 25 0 1 0 420254976 193826816 46821 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47321 46821 603 41 0 47280 0
vsize: 189284
[startup+710.015 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 48018 0 1 0 70880 106 0 0 25 0 1 0 420254976 198574080 47996 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48480 47996 603 41 0 48439 0
vsize: 193920
[startup+720.015 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 49186 0 1 0 71878 108 0 0 25 0 1 0 420254976 203329536 49164 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49641 49164 603 41 0 49600 0
vsize: 198564
[startup+730.015 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 50496 0 1 0 72876 111 0 0 25 0 1 0 420254976 208748544 50474 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50964 50474 603 41 0 50923 0
vsize: 203856
[startup+740.015 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 50998 0 1 0 73875 111 0 0 25 0 1 0 420254976 210792448 50976 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51463 50976 603 41 0 51422 0
vsize: 205852
[startup+750.016 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 51524 0 1 0 74874 113 0 0 25 0 1 0 420254976 212971520 51502 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51995 51502 603 41 0 51954 0
vsize: 207980
[startup+760.016 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 51915 0 1 0 75874 114 0 0 25 0 1 0 420254976 214609920 51893 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52395 51893 603 41 0 52354 0
vsize: 209580
[startup+770.016 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52330 0 1 0 76873 115 0 0 25 0 1 0 420254976 216244224 52308 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52794 52308 603 41 0 52753 0
vsize: 211176
[startup+780.016 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 77872 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+790.016 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 78873 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+800.017 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 79873 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+810.017 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 80873 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+820.017 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 81873 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+830.017 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 82873 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+840.017 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 83873 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+850.017 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 84874 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+860.017 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52580 0 1 0 85874 115 0 0 25 0 1 0 420254976 217333760 52558 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52558 603 41 0 53019 0
vsize: 212240
[startup+870.017 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52581 0 1 0 86874 115 0 0 25 0 1 0 420254976 217333760 52559 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52559 603 41 0 53019 0
vsize: 212240
[startup+880.018 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 87873 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+890.018 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 88873 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+900.018 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 89873 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+910.018 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 90873 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+920.018 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 91874 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+930.018 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 92874 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+940.018 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 93874 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+950.019 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 94874 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+960.018 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 95874 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+970.018 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 96875 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+980.019 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 97875 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+990.018 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 98875 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 99875 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 100875 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 101876 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 102876 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 103876 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 104876 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223728 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 105876 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 106876 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 107877 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 108877 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223728 134558937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52582 0 1 0 109877 115 0 0 25 0 1 0 420254976 217333760 52560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53060 52560 603 41 0 53019 0
vsize: 212240
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 52949 0 1 0 110877 117 0 0 25 0 1 0 420254976 218832896 52927 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53426 52927 603 41 0 53385 0
vsize: 213704
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 53301 0 1 0 111876 118 0 0 25 0 1 0 420254976 220360704 53279 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53799 53279 603 41 0 53758 0
vsize: 215196
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 53746 0 1 0 112876 118 0 0 25 0 1 0 420254976 222167040 53724 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54240 53724 603 41 0 54199 0
vsize: 216960
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 54210 0 1 0 113875 119 0 0 25 0 1 0 420254976 224067584 54188 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54704 54188 603 41 0 54663 0
vsize: 218816
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 54588 0 1 0 114874 120 0 0 25 0 1 0 420254976 225710080 54566 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55105 54566 603 41 0 55064 0
vsize: 220420
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 55030 0 1 0 115874 120 0 0 25 0 1 0 420254976 227500032 55008 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55542 55008 603 41 0 55501 0
vsize: 222168
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 55406 0 1 0 116873 122 0 0 25 0 1 0 420254976 228990976 55384 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55906 55384 603 41 0 55865 0
vsize: 223624
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 55940 0 1 0 117873 122 0 0 25 0 1 0 420254976 231186432 55918 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56442 55918 603 41 0 56401 0
vsize: 225768
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 56412 0 1 0 118872 123 0 0 25 0 1 0 420254976 233095168 56390 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56908 56390 603 41 0 56867 0
vsize: 227632
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 56944 0 1 0 119871 124 0 0 25 0 1 0 420254976 235294720 56922 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57445 56922 603 41 0 57404 0
vsize: 229780
[startup+1210.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 22262
Raw data (stat): 22262 (minisat+) R 22261 20937 20936 0 -1 0 57390 0 1 0 120870 125 0 0 25 0 1 0 420254976 237199360 57368 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57910 57368 603 41 0 57869 0
vsize: 231640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.14 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 22262
Raw data (stat): 22262 (minisat+) Z 22261 20937 20936 0 -1 12 57392 0 1 0 120870 136 0 0 25 0 1 0 420254976 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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): 1210.14
CPU time (s): 1210.07
CPU user time (s): 1208.71
CPU system time (s): 1.36179
CPU usage (%): 99.9944
Max. virtual memory (Kb): 231640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####