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_44_sat_pb.cnf.cr.opb
MD5SUM	c501a04dd091dbe678ec2743021adc30
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	15.2037
Number of variables	2970
Total number of constraints	2113
Number of constraints which are clauses	2024
Number of constraints which are cardinality constraints (but not clauses)	89
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 4651

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 19:28:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3440 boxname=wulflinc12 idbench=56 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c501a04dd091dbe678ec2743021adc30  /oldhome/oroussel/tmp/wulflinc12/normalized-fpga45_44_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-fpga45_44_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc12/normalized-fpga45_44_sat_pb.cnf.cr.opb
IDLAUNCH: 3440
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        921792 kB
Buffers:         34580 kB
Cached:          59108 kB
SwapCached:         16 kB
Active:          58396 kB
Inactive:        38064 kB
HighTotal:      131008 kB
HighFree:        68040 kB
LowTotal:       903652 kB
LowFree:        853752 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10796 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:49:10 (client local time) WITH STATUS 0 IN 1210.08 SECONDS
stats: 3440 7 1210.08 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  88]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  87]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  86]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  85]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  84]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  83]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  82]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  81]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  80]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  79]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  78]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  77]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  76]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  75]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  74]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  73]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  72]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  71]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  70]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  69]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  68]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  67]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  66]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  65]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  64]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  63]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  62]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  61]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  60]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  59]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  58]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  57]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  56]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  55]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  54]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  53]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  52]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  51]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  50]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  49]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  48]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  47]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  46]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  45]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  44]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[  43]---> Adder-cost: 38   maxlim: 20   bits: 5/5
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 |   36084   168809 |   12028       0        0     nan |  0.000 % |
c |       100 |   35929   168284 |   13230      80      250     3.1 |  8.379 % |
c |       250 |   35635   167298 |   14553     178      658     3.7 |  8.895 % |
c |       475 |   35446   166671 |   16009     367     1855     5.1 |  9.211 % |
c |       812 |   35201   165822 |   17610     670     3802     5.7 |  9.668 % |
c |      1319 |   34450   163195 |   19371    1079     5870     5.4 | 11.133 % |
c |      2078 |   33621   160323 |   21308    1719     8506     4.9 | 12.668 % |
c |      3217 |   31802   154101 |   23439    2598    12589     4.8 | 16.395 % |
c |      4925 |   29513   146263 |   25783    3897    18975     4.9 | 20.931 % |
c |      7488 |   23252   124855 |   28361    5231   170699    32.6 | 33.447 % |
c |     11334 |   21909   120281 |   31197    8823  1328722   150.6 | 36.224 % |
c |     17102 |   21228   117953 |   34317   14448  3323941   230.1 | 37.642 % |
c |     25753 |   21008   117201 |   37749   23059  6454532   279.9 | 38.111 % |
c |     38727 |   20905   116851 |   41523   36016 16193204   449.6 | 38.334 % |
c |     58190 |   20754   116347 |   45676   20822 10909211   523.9 | 38.662 % |
c |     87382 |   19325   111438 |   50243   49803 28134392   564.9 | 41.556 % |
c |    131172 |   19101   110696 |   55268   53809 35298621   656.0 | 42.060 % |
#### 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 27509
Raw data (stat): 27509 (runsolver) R 27508 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420250763 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99986 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 1222 0 1 0 972 4 0 0 25 0 1 0 420250763 7020544 1200 4294967295 134512640 134672761 3221224528 3221223652 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1714 1200 603 41 0 1673 0
vsize: 6856
[startup+20.0012 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 1228 0 1 0 1972 4 0 0 25 0 1 0 420250763 7020544 1206 4294967295 134512640 134672761 3221224528 3221223728 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1714 1206 603 41 0 1673 0
vsize: 6856
[startup+30.0018 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 1235 0 1 0 2971 4 0 0 25 0 1 0 420250763 7020544 1213 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1714 1213 603 41 0 1673 0
vsize: 6856
[startup+40.0023 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 2336 0 1 0 3969 6 0 0 25 0 1 0 420250763 11616256 2314 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2314 603 41 0 2795 0
vsize: 11344
[startup+50.0034 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 4127 0 1 0 4965 11 0 0 25 0 1 0 420250763 18952192 4105 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4627 4105 603 41 0 4586 0
vsize: 18508
[startup+60.0032 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 5530 0 1 0 5961 15 0 0 25 0 1 0 420250763 24784896 5508 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6051 5508 603 41 0 6010 0
vsize: 24204
[startup+70.0038 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 6947 0 1 0 6958 18 0 0 25 0 1 0 420250763 30466048 6925 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7438 6925 603 41 0 7397 0
vsize: 29752
[startup+80.0042 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 8059 0 1 0 7955 21 0 0 25 0 1 0 420250763 35049472 8037 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8557 8037 603 41 0 8516 0
vsize: 34228
[startup+90.0047 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 9916 0 1 0 8951 25 0 0 25 0 1 0 420250763 42618880 9894 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10405 9894 603 41 0 10364 0
vsize: 41620
[startup+100.004 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 11844 0 1 0 9949 27 0 0 25 0 1 0 420250763 50593792 11822 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12352 11822 603 41 0 12311 0
vsize: 49408
[startup+110.004 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 13447 0 1 0 10946 30 0 0 25 0 1 0 420250763 57184256 13425 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13961 13425 603 41 0 13920 0
vsize: 55844
[startup+120.005 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 15015 0 1 0 11943 34 0 0 25 0 1 0 420250763 63541248 14993 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15513 14993 603 41 0 15472 0
vsize: 62052
[startup+130.005 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 16408 0 1 0 12938 39 0 0 25 0 1 0 420250763 69345280 16386 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16930 16386 603 41 0 16889 0
vsize: 67720
[startup+140.005 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 17807 0 1 0 13934 43 0 0 25 0 1 0 420250763 75153408 17785 4294967295 134512640 134672761 3221224528 3221223632 134555091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18348 17785 603 41 0 18307 0
vsize: 73392
[startup+150.006 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 18582 0 1 0 14932 45 0 0 25 0 1 0 420250763 78286848 18560 4294967295 134512640 134672761 3221224528 3221223712 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19113 18560 603 41 0 19072 0
vsize: 76452
[startup+160.006 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 19654 0 1 0 15929 48 0 0 25 0 1 0 420250763 82735104 19632 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20199 19632 603 41 0 20158 0
vsize: 80796
[startup+170.006 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 20839 0 1 0 16928 50 0 0 25 0 1 0 420250763 87580672 20817 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21382 20817 603 41 0 21341 0
vsize: 85528
[startup+180.006 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 21796 0 1 0 17925 53 0 0 25 0 1 0 420250763 91488256 21774 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22336 21774 603 41 0 22295 0
vsize: 89344
[startup+190.007 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 22671 0 1 0 18923 56 0 0 25 0 1 0 420250763 95043584 22649 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23204 22649 603 41 0 23163 0
vsize: 92816
[startup+200.007 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 23448 0 1 0 19921 57 0 0 25 0 1 0 420250763 98304000 23426 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24000 23426 603 41 0 23959 0
vsize: 96000
[startup+210.007 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 24167 0 1 0 20920 59 0 0 25 0 1 0 420250763 101273600 24145 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24725 24145 603 41 0 24684 0
vsize: 98900
[startup+220.007 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 24919 0 1 0 21919 60 0 0 25 0 1 0 420250763 104366080 24897 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25480 24897 603 41 0 25439 0
vsize: 101920
[startup+230.007 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25126 0 1 0 22919 60 0 0 25 0 1 0 420250763 105177088 25104 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25104 603 41 0 25637 0
vsize: 102712
[startup+240.008 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25132 0 1 0 23919 60 0 0 25 0 1 0 420250763 105177088 25110 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25110 603 41 0 25637 0
vsize: 102712
[startup+250.009 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 24919 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+260.009 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 25919 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+270.01 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 26919 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+280.009 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 27919 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+290.01 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 28919 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+300.01 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 29919 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+310.01 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 30919 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+320.011 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 31920 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+330.012 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 32920 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+340.012 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 33920 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+350.013 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 34920 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+360.013 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 35921 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+370.014 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 36921 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+380.014 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 37921 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+390.015 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 38921 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+400.015 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25133 0 1 0 39921 60 0 0 25 0 1 0 420250763 105177088 25111 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 25111 603 41 0 25637 0
vsize: 102712
[startup+410.015 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 25531 0 1 0 40921 61 0 0 25 0 1 0 420250763 106799104 25509 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26074 25509 603 41 0 26033 0
vsize: 104296
[startup+420.016 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 26931 0 1 0 41919 64 0 0 25 0 1 0 420250763 112611328 26909 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27493 26909 603 41 0 27452 0
vsize: 109972
[startup+430.017 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 28223 0 1 0 42916 66 0 0 25 0 1 0 420250763 117882880 28201 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28780 28201 603 41 0 28739 0
vsize: 115120
[startup+440.018 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 29551 0 1 0 43913 69 0 0 25 0 1 0 420250763 123310080 29529 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30105 29529 603 41 0 30064 0
vsize: 120420
[startup+450.018 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 30573 0 1 0 44911 72 0 0 25 0 1 0 420250763 127508480 30551 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31130 30551 603 41 0 31089 0
vsize: 124520
[startup+460.018 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 31434 0 1 0 45909 73 0 0 25 0 1 0 420250763 131022848 31412 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31988 31412 603 41 0 31947 0
vsize: 127952
[startup+470.019 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 32621 0 1 0 46906 77 0 0 25 0 1 0 420250763 135884800 32599 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33175 32599 603 41 0 33134 0
vsize: 132700
[startup+480.019 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 47904 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+490.02 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 48905 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+500.021 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 49905 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+510.02 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 50905 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223632 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+520.021 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 51905 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+530.021 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 52905 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+540.022 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 53906 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+550.022 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 54906 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+560.022 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 55906 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+570.022 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 56906 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+580.022 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 57906 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+590.023 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 58907 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+600.023 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 59907 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+610.023 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 60907 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223712 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+620.024 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33473 0 1 0 61907 78 0 0 25 0 1 0 420250763 139378688 33451 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33451 603 41 0 33987 0
vsize: 136112
[startup+630.024 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 33526 0 1 0 62907 78 0 0 25 0 1 0 420250763 139649024 33504 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34094 33504 603 41 0 34053 0
vsize: 136376
[startup+640.025 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 34498 0 1 0 63906 80 0 0 25 0 1 0 420250763 143687680 34476 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35080 34476 603 41 0 35039 0
vsize: 140320
[startup+650.025 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 35046 0 1 0 64905 81 0 0 25 0 1 0 420250763 146014208 35024 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35648 35024 603 41 0 35607 0
vsize: 142592
[startup+660.025 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 35503 0 1 0 65904 83 0 0 25 0 1 0 420250763 147931136 35481 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36116 35481 603 41 0 36075 0
vsize: 144464
[startup+670.026 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 36134 0 1 0 66903 83 0 0 25 0 1 0 420250763 150495232 36112 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36742 36112 603 41 0 36701 0
vsize: 146968
[startup+680.027 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 36893 0 1 0 67902 85 0 0 25 0 1 0 420250763 153645056 36871 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37511 36871 603 41 0 37470 0
vsize: 150044
[startup+690.027 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 37646 0 1 0 68900 87 0 0 25 0 1 0 420250763 156758016 37624 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38271 37624 603 41 0 38230 0
vsize: 153084
[startup+700.027 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 38353 0 1 0 69899 89 0 0 25 0 1 0 420250763 159641600 38331 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38975 38331 603 41 0 38934 0
vsize: 155900
[startup+710.027 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 39137 0 1 0 70898 90 0 0 25 0 1 0 420250763 162988032 39115 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39792 39115 603 41 0 39751 0
vsize: 159168
[startup+720.028 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 40209 0 1 0 71894 92 0 0 25 0 1 0 420250763 167321600 40187 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40850 40187 603 41 0 40809 0
vsize: 163400
[startup+730.028 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 43251 0 1 0 72887 100 0 0 25 0 1 0 420250763 179773440 43229 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43890 43230 603 41 0 43849 0
vsize: 175560
[startup+740.029 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 73883 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223632 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+750.029 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 74884 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+760.029 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 75884 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+770.03 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 76884 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+780.03 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 77884 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+790.032 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 78884 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+800.032 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 79884 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+810.031 s]
Raw data (loadavg): 1.15 0.95 0.57 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 80885 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+820.032 s]
Raw data (loadavg): 1.12 0.95 0.57 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 81885 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+830.032 s]
Raw data (loadavg): 1.10 0.95 0.57 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 82885 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+840.032 s]
Raw data (loadavg): 1.09 0.95 0.58 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 83885 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+850.034 s]
Raw data (loadavg): 1.07 0.96 0.58 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 84885 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+860.034 s]
Raw data (loadavg): 1.06 0.96 0.59 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 85886 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+870.034 s]
Raw data (loadavg): 1.05 0.96 0.59 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 86886 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+880.034 s]
Raw data (loadavg): 1.04 0.96 0.59 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 87886 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+890.035 s]
Raw data (loadavg): 1.04 0.96 0.60 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 88886 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+900.034 s]
Raw data (loadavg): 1.03 0.96 0.60 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 89886 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+910.034 s]
Raw data (loadavg): 1.03 0.96 0.61 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 90886 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+920.036 s]
Raw data (loadavg): 1.02 0.96 0.61 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 91887 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+930.036 s]
Raw data (loadavg): 1.02 0.96 0.61 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 92887 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+940.043 s]
Raw data (loadavg): 1.01 0.96 0.62 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 93888 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+950.043 s]
Raw data (loadavg): 1.01 0.97 0.62 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 94888 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+960.042 s]
Raw data (loadavg): 1.01 0.97 0.62 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 95888 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+970.042 s]
Raw data (loadavg): 1.01 0.97 0.63 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 96888 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+980.043 s]
Raw data (loadavg): 1.01 0.97 0.63 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 97888 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+990.044 s]
Raw data (loadavg): 1.08 0.99 0.64 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 98889 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1000.04 s]
Raw data (loadavg): 1.07 0.99 0.64 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 99889 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1010.04 s]
Raw data (loadavg): 1.06 0.99 0.65 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 100889 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1020.04 s]
Raw data (loadavg): 1.05 0.99 0.65 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 101889 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1030.04 s]
Raw data (loadavg): 1.04 0.99 0.65 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 102889 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1040.05 s]
Raw data (loadavg): 1.03 0.99 0.66 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 103889 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1050.05 s]
Raw data (loadavg): 1.03 0.99 0.66 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 104890 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1060.05 s]
Raw data (loadavg): 1.02 0.99 0.66 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 105890 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1070.05 s]
Raw data (loadavg): 1.02 0.99 0.66 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 106890 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1080.05 s]
Raw data (loadavg): 1.02 0.99 0.67 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 107890 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1090.06 s]
Raw data (loadavg): 1.01 0.99 0.67 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 108891 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1100.06 s]
Raw data (loadavg): 1.01 0.99 0.67 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 109891 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1110.06 s]
Raw data (loadavg): 1.01 0.99 0.68 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 110892 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1120.06 s]
Raw data (loadavg): 1.01 0.99 0.68 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 111892 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.68 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 112892 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.69 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 113892 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.69 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 114893 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.69 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45170 0 1 0 115893 104 0 0 25 0 1 0 420250763 187604992 45148 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45802 45148 603 41 0 45761 0
vsize: 183208
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.69 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 45953 0 1 0 116891 106 0 0 25 0 1 0 420250763 190877696 45931 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46601 45931 603 41 0 46560 0
vsize: 186404
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.70 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 46953 0 1 0 117889 108 0 0 25 0 1 0 420250763 194940928 46931 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47593 46931 603 41 0 47552 0
vsize: 190372
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.70 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 48131 0 1 0 118886 111 0 0 25 0 1 0 420250763 199860224 48109 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48794 48109 603 41 0 48753 0
vsize: 195176
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.70 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 48764 0 1 0 119885 113 0 0 25 0 1 0 420250763 202448896 48742 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49426 48742 603 41 0 49385 0
vsize: 197704
[startup+1210.06 s]
Raw data (loadavg): 1.00 0.99 0.71 2/54 27509
Raw data (stat): 27509 (minisat+) R 27508 25285 25284 0 -1 0 49432 0 1 0 120883 115 0 0 25 0 1 0 420250763 205168640 49410 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50090 49410 603 41 0 50049 0
vsize: 200360
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.15 s]
Raw data (loadavg): 1.00 0.99 0.71 1/54 27509
Raw data (stat): 27509 (minisat+) Z 27508 25285 25284 0 -1 12 49434 0 1 0 120883 124 0 0 25 0 1 0 420250763 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.15
CPU time (s): 1210.08
CPU user time (s): 1208.84
CPU system time (s): 1.24281
CPU usage (%): 99.994
Max. virtual memory (Kb): 200360
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####