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-chnl50_60_pb.cnf.cr.opb
MD5SUM	6968a43b42bba7df68b13fdfd3b616a1
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	61
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.187971
Number of variables	6000
Total number of constraints	220
Number of constraints which are clauses	120
Number of constraints which are cardinality constraints (but not clauses)	100
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	50
Maximum length of a constraint	60
Trace number 6156

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 03:33:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4534 boxname=wulflinc13 idbench=22 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6968a43b42bba7df68b13fdfd3b616a1  /oldhome/oroussel/tmp/wulflinc13/normalized-chnl50_60_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-chnl50_60_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc13/normalized-chnl50_60_pb.cnf.cr.opb
IDLAUNCH: 4534
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890992 kB
Buffers:         35388 kB
Cached:          88524 kB
SwapCached:        392 kB
Active:          54904 kB
Inactive:        72216 kB
HighTotal:      131008 kB
HighFree:        38612 kB
LowTotal:       903652 kB
LowFree:        852380 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10992 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:53:27 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 4534 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 220 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................
c ---[  99]---> BDD-cost:  117
c ---[  98]---> BDD-cost:  117
c ---[  97]---> BDD-cost:  117
c ---[  96]---> BDD-cost:  117
c ---[  95]---> BDD-cost:  117
c ---[  94]---> BDD-cost:  117
c ---[  93]---> BDD-cost:  117
c ---[  92]---> BDD-cost:  117
c ---[  91]---> BDD-cost:  117
c ---[  90]---> BDD-cost:  117
c ---[  89]---> BDD-cost:  117
c ---[  88]---> BDD-cost:  117
c ---[  87]---> BDD-cost:  117
c ---[  86]---> BDD-cost:  117
c ---[  85]---> BDD-cost:  117
c ---[  84]---> BDD-cost:  117
c ---[  83]---> BDD-cost:  117
c ---[  82]---> BDD-cost:  117
c ---[  81]---> BDD-cost:  117
c ---[  80]---> BDD-cost:  117
c ---[  79]---> BDD-cost:  117
c ---[  78]---> BDD-cost:  117
c ---[  77]---> BDD-cost:  117
c ---[  76]---> BDD-cost:  117
c ---[  75]---> BDD-cost:  117
c ---[  74]---> BDD-cost:  117
c ---[  73]---> BDD-cost:  117
c ---[  72]---> BDD-cost:  117
c ---[  71]---> BDD-cost:  117
c ---[  70]---> BDD-cost:  117
c ---[  69]---> BDD-cost:  117
c ---[  68]---> BDD-cost:  117
c ---[  67]---> BDD-cost:  117
c ---[  66]---> BDD-cost:  117
c ---[  65]---> BDD-cost:  117
c ---[  64]---> BDD-cost:  117
c ---[  63]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  117
c ---[  61]---> BDD-cost:  117
c ---[  60]---> BDD-cost:  117
c ---[  59]---> BDD-cost:  117
c ---[  58]---> BDD-cost:  117
c ---[  57]---> BDD-cost:  117
c ---[  56]---> BDD-cost:  117
c ---[  55]---> BDD-cost:  117
c ---[  54]---> BDD-cost:  117
c ---[  53]---> BDD-cost:  117
c ---[  52]---> BDD-cost:  117
c ---[  51]---> BDD-cost:  117
c ---[  50]---> BDD-cost:  117
c ---[  49]---> BDD-cost:  117
c ---[  48]---> BDD-cost:  117
c ---[  47]---> BDD-cost:  117
c ---[  46]---> BDD-cost:  117
c ---[  45]---> BDD-cost:  117
c ---[  44]---> BDD-cost:  117
c ---[  43]---> BDD-cost:  117
c ---[  42]---> BDD-cost:  117
c ---[  41]---> BDD-cost:  117
c ---[  40]---> BDD-cost:  117
c ---[  39]---> BDD-cost:  117
c ---[  38]---> BDD-cost:  117
c ---[  37]---> BDD-cost:  117
c ---[  36]---> BDD-cost:  117
c ---[  35]---> BDD-cost:  117
c ---[  34]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  117
c ---[  32]---> BDD-cost:  117
c ---[  31]---> BDD-cost:  117
c ---[  30]---> BDD-cost:  117
c ---[  29]---> BDD-cost:  117
c ---[  28]---> BDD-cost:  117
c ---[  27]---> BDD-cost:  117
c ---[  26]---> BDD-cost:  117
c ---[  25]---> BDD-cost:  117
c ---[  24]---> BDD-cost:  117
c ---[  23]---> BDD-cost:  117
c ---[  22]---> BDD-cost:  117
c ---[  21]---> BDD-cost:  117
c ---[  20]---> BDD-cost:  117
c ---[  19]---> BDD-cost:  117
c ---[  18]---> BDD-cost:  117
c ---[  17]---> BDD-cost:  117
c ---[  16]---> BDD-cost:  117
c ---[  15]---> BDD-cost:  117
c ---[  14]---> BDD-cost:  117
c ---[  13]---> BDD-cost:  117
c ---[  12]---> BDD-cost:  117
c ---[  11]---> BDD-cost:  117
c ---[  10]---> BDD-cost:  117
c ---[   9]---> BDD-cost:  117
c ---[   8]---> BDD-cost:  117
c ---[   7]---> BDD-cost:  117
c ---[   6]---> BDD-cost:  117
c ---[   5]---> BDD-cost:  117
c ---[   4]---> BDD-cost:  117
c ---[   3]---> BDD-cost:  117
c ---[   2]---> BDD-cost:  117
c ---[   1]---> BDD-cost:  117
c ---[   0]---> BDD-cost:  117
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   52320   150800 |   17440       0        0     nan |  0.000 % |
c |       100 |   52120   150200 |   19184      21       70     3.3 |  0.797 % |
c |       250 |   51825   149315 |   21102      59      275     4.7 |  1.124 % |
c |       475 |   51250   147590 |   23212      58      178     3.1 |  1.780 % |
c |       814 |   50480   145280 |   25533      69      207     3.0 |  2.650 % |
c |      1320 |   49236   141550 |   28087     132     5156    39.1 |  4.056 % |
c |      2080 |   48841   140365 |   30896     788   184217   233.8 |  4.497 % |
c |      3221 |   47786   137200 |   33985    1559   386219   247.7 |  5.689 % |
c |      4931 |   46506   133360 |   37384    2856   781496   273.6 |  7.136 % |
c |      7493 |   44641   127765 |   41122    4788  1484263   310.0 |  9.243 % |
c |     11338 |   41436   118150 |   45234    7554  2311239   306.0 | 12.864 % |
c |     17109 |   39331   111835 |   49758   12673  4512736   356.1 | 15.243 % |
c |     25760 |   34751    98095 |   54734   19839  7182049   362.0 | 20.418 % |
c |     38734 |   31701    88945 |   60207   31859 12451796   390.8 | 23.864 % |
c |     58198 |   30341    84865 |   66228   50932 20580185   404.1 | 25.401 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 5455
Raw data (stat): 5455 (runsolver) R 5454 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423164625 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+10.0002 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 1862 0 0 0 994 4 0 0 25 0 1 0 423164625 9670656 1781 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2361 1781 603 41 0 2320 0
vsize: 9444
[startup+19.9998 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 2167 0 0 0 1992 5 0 0 25 0 1 0 423164625 11022336 2086 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2691 2086 603 41 0 2650 0
vsize: 10764
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 2544 0 0 0 2991 6 0 0 25 0 1 0 423164625 12500992 2463 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3052 2463 603 41 0 3011 0
vsize: 12208
[startup+40.0011 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3210 0 0 0 3989 8 0 0 25 0 1 0 423164625 15200256 3129 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3711 3129 603 41 0 3670 0
vsize: 14844
[startup+50.0007 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3341 0 0 0 4989 9 0 0 25 0 1 0 423164625 15740928 3260 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3260 603 41 0 3802 0
vsize: 15372
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3515 0 0 0 5989 9 0 0 25 0 1 0 423164625 16551936 3434 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4041 3434 603 41 0 4000 0
vsize: 16164
[startup+70.0011 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3703 0 0 0 6988 10 0 0 25 0 1 0 423164625 17227776 3622 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4206 3622 603 41 0 4165 0
vsize: 16824
[startup+80.0007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3973 0 0 0 7988 10 0 0 25 0 1 0 423164625 18440192 3892 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4502 3892 603 41 0 4461 0
vsize: 18008
[startup+90.0007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4304 0 0 0 8987 11 0 0 25 0 1 0 423164625 19787776 4223 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4831 4223 603 41 0 4790 0
vsize: 19324
[startup+100 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4367 0 0 0 9987 11 0 0 25 0 1 0 423164625 19922944 4286 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4864 4286 603 41 0 4823 0
vsize: 19456
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4461 0 0 0 10988 11 0 0 25 0 1 0 423164625 20328448 4380 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4963 4380 603 41 0 4922 0
vsize: 19852
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4627 0 0 0 11987 11 0 0 25 0 1 0 423164625 21004288 4546 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5128 4546 603 41 0 5087 0
vsize: 20512
[startup+130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5529 0 0 0 12986 13 0 0 25 0 1 0 423164625 24788992 5448 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6052 5448 603 41 0 6011 0
vsize: 24208
[startup+140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5624 0 0 0 13985 14 0 0 25 0 1 0 423164625 25194496 5543 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6151 5543 603 41 0 6110 0
vsize: 24604
[startup+150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5853 0 0 0 14985 14 0 0 25 0 1 0 423164625 26140672 5772 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6382 5772 603 41 0 6341 0
vsize: 25528
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5892 0 0 0 15985 14 0 0 25 0 1 0 423164625 26275840 5811 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5811 603 41 0 6374 0
vsize: 25660
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 6814 0 0 0 16984 16 0 0 25 0 1 0 423164625 30052352 6733 4294967295 134512640 134672761 3221224544 3221223692 1074733099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7337 6733 603 41 0 7296 0
vsize: 29348
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 6898 0 0 0 17983 16 0 0 25 0 1 0 423164625 30322688 6817 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6817 603 41 0 7362 0
vsize: 29612
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7000 0 0 0 18982 17 0 0 25 0 1 0 423164625 30728192 6919 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7502 6919 603 41 0 7461 0
vsize: 30008
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7059 0 0 0 19982 17 0 0 25 0 1 0 423164625 30998528 6978 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7568 6978 603 41 0 7527 0
vsize: 30272
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7432 0 0 0 20981 18 0 0 25 0 1 0 423164625 32485376 7351 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7931 7351 603 41 0 7890 0
vsize: 31724
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7444 0 0 0 21981 18 0 0 25 0 1 0 423164625 32616448 7363 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7963 7363 603 41 0 7922 0
vsize: 31852
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7517 0 0 0 22981 18 0 0 25 0 1 0 423164625 32882688 7436 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8028 7436 603 41 0 7987 0
vsize: 32112
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7598 0 0 0 23981 19 0 0 25 0 1 0 423164625 33280000 7517 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8125 7517 603 41 0 8084 0
vsize: 32500
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7746 0 0 0 24981 19 0 0 25 0 1 0 423164625 33816576 7665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8256 7665 603 41 0 8215 0
vsize: 33024
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7746 0 0 0 25981 19 0 0 25 0 1 0 423164625 33816576 7665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8256 7665 603 41 0 8215 0
vsize: 33024
[startup+270 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7884 0 0 0 26981 19 0 0 25 0 1 0 423164625 34353152 7803 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8387 7803 603 41 0 8346 0
vsize: 33548
[startup+279.999 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 8208 0 0 0 27980 20 0 0 25 0 1 0 423164625 35696640 8127 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8715 8127 603 41 0 8674 0
vsize: 34860
[startup+290 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 8777 0 0 0 28979 21 0 0 25 0 1 0 423164625 38043648 8696 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9288 8696 603 41 0 9247 0
vsize: 37152
[startup+300 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 8851 0 0 0 29979 21 0 0 25 0 1 0 423164625 38449152 8770 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9387 8770 603 41 0 9346 0
vsize: 37548
[startup+310 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9185 0 0 0 30979 22 0 0 25 0 1 0 423164625 39800832 9104 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9717 9104 603 41 0 9676 0
vsize: 38868
[startup+320 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9293 0 0 0 31979 22 0 0 25 0 1 0 423164625 40206336 9212 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9212 603 41 0 9775 0
vsize: 39264
[startup+330 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9294 0 0 0 32979 22 0 0 25 0 1 0 423164625 40206336 9213 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9213 603 41 0 9775 0
vsize: 39264
[startup+340 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9543 0 0 0 33979 22 0 0 25 0 1 0 423164625 41287680 9462 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10080 9462 603 41 0 10039 0
vsize: 40320
[startup+350 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9680 0 0 0 34978 23 0 0 25 0 1 0 423164625 41828352 9599 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10212 9599 603 41 0 10171 0
vsize: 40848
[startup+360.001 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9779 0 0 0 35978 23 0 0 25 0 1 0 423164625 42233856 9698 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10311 9698 603 41 0 10270 0
vsize: 41244
[startup+370 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9782 0 0 0 36978 23 0 0 25 0 1 0 423164625 42233856 9701 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10311 9701 603 41 0 10270 0
vsize: 41244
[startup+380 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9813 0 0 0 37978 23 0 0 25 0 1 0 423164625 42369024 9732 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10344 9732 603 41 0 10303 0
vsize: 41376
[startup+390.001 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 10508 0 0 0 38976 25 0 0 25 0 1 0 423164625 45203456 10427 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11036 10427 603 41 0 10995 0
vsize: 44144
[startup+400.001 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11214 0 0 0 39973 27 0 0 25 0 1 0 423164625 48029696 11133 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11726 11133 603 41 0 11685 0
vsize: 46904
[startup+410.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11249 0 0 0 40973 27 0 0 25 0 1 0 423164625 48164864 11168 4294967295 134512640 134672761 3221224544 3221223796 134562232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11759 11168 603 41 0 11718 0
vsize: 47036
[startup+420 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11472 0 0 0 41973 28 0 0 25 0 1 0 423164625 49111040 11391 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11990 11391 603 41 0 11949 0
vsize: 47960
[startup+430 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11849 0 0 0 42972 28 0 0 25 0 1 0 423164625 50724864 11768 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12384 11768 603 41 0 12343 0
vsize: 49536
[startup+440 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12820 0 0 0 43970 31 0 0 25 0 1 0 423164625 54640640 12739 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12739 603 41 0 13299 0
vsize: 53360
[startup+450 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12823 0 0 0 44970 31 0 0 25 0 1 0 423164625 54640640 12742 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12742 603 41 0 13299 0
vsize: 53360
[startup+460 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12824 0 0 0 45970 31 0 0 25 0 1 0 423164625 54640640 12743 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12743 603 41 0 13299 0
vsize: 53360
[startup+470 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12824 0 0 0 46971 31 0 0 25 0 1 0 423164625 54640640 12743 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12743 603 41 0 13299 0
vsize: 53360
[startup+479.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12824 0 0 0 47971 31 0 0 25 0 1 0 423164625 54640640 12743 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12743 603 41 0 13299 0
vsize: 53360
[startup+490 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12825 0 0 0 48971 31 0 0 25 0 1 0 423164625 54640640 12744 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12744 603 41 0 13299 0
vsize: 53360
[startup+500 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12827 0 0 0 49971 31 0 0 25 0 1 0 423164625 54640640 12746 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12746 603 41 0 13299 0
vsize: 53360
[startup+510 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12919 0 0 0 50971 31 0 0 25 0 1 0 423164625 55046144 12838 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13439 12838 603 41 0 13398 0
vsize: 53756
[startup+520 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13248 0 0 0 51971 32 0 0 25 0 1 0 423164625 56397824 13167 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13769 13167 603 41 0 13728 0
vsize: 55076
[startup+530 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13357 0 0 0 52971 32 0 0 25 0 1 0 423164625 56803328 13276 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13868 13276 603 41 0 13827 0
vsize: 55472
[startup+540 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13838 0 0 0 53970 33 0 0 25 0 1 0 423164625 58826752 13757 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14362 13757 603 41 0 14321 0
vsize: 57448
[startup+550 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13847 0 0 0 54970 33 0 0 25 0 1 0 423164625 58826752 13766 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14362 13766 603 41 0 14321 0
vsize: 57448
[startup+560.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13932 0 0 0 55970 34 0 0 25 0 1 0 423164625 59232256 13851 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14461 13851 603 41 0 14420 0
vsize: 57844
[startup+570.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13949 0 0 0 56970 34 0 0 25 0 1 0 423164625 59232256 13868 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14461 13868 603 41 0 14420 0
vsize: 57844
[startup+580.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14296 0 0 0 57969 35 0 0 25 0 1 0 423164625 60715008 14215 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14823 14215 603 41 0 14782 0
vsize: 59292
[startup+590.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14308 0 0 0 58969 35 0 0 25 0 1 0 423164625 60715008 14227 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14823 14227 603 41 0 14782 0
vsize: 59292
[startup+600.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14309 0 0 0 59969 35 0 0 25 0 1 0 423164625 60715008 14228 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14823 14228 603 41 0 14782 0
vsize: 59292
[startup+610.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14505 0 0 0 60969 35 0 0 25 0 1 0 423164625 61526016 14424 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 14424 603 41 0 14980 0
vsize: 60084
[startup+620.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 15094 0 0 0 61969 36 0 0 25 0 1 0 423164625 63946752 15013 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15612 15013 603 41 0 15571 0
vsize: 62448
[startup+630.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 15250 0 0 0 62969 36 0 0 25 0 1 0 423164625 64618496 15169 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15776 15169 603 41 0 15735 0
vsize: 63104
[startup+640.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 16043 0 0 0 63966 38 0 0 25 0 1 0 423164625 67981312 15962 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16597 15962 603 41 0 16556 0
vsize: 66388
[startup+650.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 17033 0 0 0 64964 41 0 0 25 0 1 0 423164625 72036352 16952 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17587 16952 603 41 0 17546 0
vsize: 70348
[startup+660.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 17339 0 0 0 65963 42 0 0 25 0 1 0 423164625 73232384 17258 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17879 17258 603 41 0 17838 0
vsize: 71516
[startup+670.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 18013 0 0 0 66962 43 0 0 25 0 1 0 423164625 75927552 17932 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18537 17932 603 41 0 18496 0
vsize: 74148
[startup+680.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19107 0 0 0 67960 45 0 0 25 0 1 0 423164625 80502784 19026 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19654 19026 603 41 0 19613 0
vsize: 78616
[startup+690.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19320 0 0 0 68960 46 0 0 25 0 1 0 423164625 81309696 19239 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19851 19239 603 41 0 19810 0
vsize: 79404
[startup+700.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19524 0 0 0 69960 46 0 0 25 0 1 0 423164625 82120704 19443 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20049 19443 603 41 0 20008 0
vsize: 80196
[startup+710.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19524 0 0 0 70960 46 0 0 25 0 1 0 423164625 82120704 19443 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20049 19443 603 41 0 20008 0
vsize: 80196
[startup+720.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19783 0 0 0 71959 47 0 0 25 0 1 0 423164625 83202048 19702 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20313 19702 603 41 0 20272 0
vsize: 81252
[startup+730.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 20260 0 0 0 72958 48 0 0 25 0 1 0 423164625 85229568 20179 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20808 20179 603 41 0 20767 0
vsize: 83232
[startup+740.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 21168 0 0 0 73957 50 0 0 25 0 1 0 423164625 88870912 21087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21697 21087 603 41 0 21656 0
vsize: 86788
[startup+750.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 21880 0 0 0 74956 51 0 0 25 0 1 0 423164625 91844608 21799 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22423 21799 603 41 0 22382 0
vsize: 89692
[startup+760.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22551 0 0 0 75954 53 0 0 25 0 1 0 423164625 94535680 22470 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23080 22470 603 41 0 23039 0
vsize: 92320
[startup+770.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22823 0 0 0 76954 53 0 0 25 0 1 0 423164625 95621120 22742 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23345 22742 603 41 0 23304 0
vsize: 93380
[startup+780.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22824 0 0 0 77954 53 0 0 25 0 1 0 423164625 95621120 22743 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23345 22743 603 41 0 23304 0
vsize: 93380
[startup+790.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22873 0 0 0 78954 53 0 0 25 0 1 0 423164625 95891456 22792 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23411 22792 603 41 0 23370 0
vsize: 93644
[startup+800.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23154 0 0 0 79953 54 0 0 25 0 1 0 423164625 96976896 23073 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23676 23073 603 41 0 23635 0
vsize: 94704
[startup+810.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23367 0 0 0 80953 55 0 0 25 0 1 0 423164625 97927168 23286 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23908 23286 603 41 0 23867 0
vsize: 95632
[startup+820.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23603 0 0 0 81953 56 0 0 25 0 1 0 423164625 98869248 23522 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24138 23522 603 41 0 24097 0
vsize: 96552
[startup+830.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23723 0 0 0 82952 56 0 0 25 0 1 0 423164625 99274752 23642 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24237 23642 603 41 0 24196 0
vsize: 96948
[startup+840.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23733 0 0 0 83953 56 0 0 25 0 1 0 423164625 99409920 23652 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24270 23652 603 41 0 24229 0
vsize: 97080
[startup+850.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23733 0 0 0 84953 56 0 0 25 0 1 0 423164625 99409920 23652 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24270 23652 603 41 0 24229 0
vsize: 97080
[startup+860.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23743 0 0 0 85953 56 0 0 25 0 1 0 423164625 99409920 23662 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24270 23662 603 41 0 24229 0
vsize: 97080
[startup+870.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23745 0 0 0 86953 56 0 0 25 0 1 0 423164625 99409920 23664 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24270 23664 603 41 0 24229 0
vsize: 97080
[startup+880.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 24219 0 0 0 87951 58 0 0 25 0 1 0 423164625 101294080 24138 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24730 24138 603 41 0 24689 0
vsize: 98920
[startup+890.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 24758 0 0 0 88950 59 0 0 25 0 1 0 423164625 103587840 24677 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25290 24677 603 41 0 25249 0
vsize: 101160
[startup+900.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25195 0 0 0 89949 60 0 0 25 0 1 0 423164625 105345024 25114 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25719 25114 603 41 0 25678 0
vsize: 102876
[startup+910.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25621 0 0 0 90948 61 0 0 25 0 1 0 423164625 107098112 25540 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26147 25540 603 41 0 26106 0
vsize: 104588
[startup+920.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25812 0 0 0 91948 61 0 0 25 0 1 0 423164625 107909120 25731 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26345 25731 603 41 0 26304 0
vsize: 105380
[startup+930.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25889 0 0 0 92948 61 0 0 25 0 1 0 423164625 108175360 25808 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26410 25808 603 41 0 26369 0
vsize: 105640
[startup+940.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 26131 0 0 0 93948 62 0 0 25 0 1 0 423164625 109256704 26050 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26674 26050 603 41 0 26633 0
vsize: 106696
[startup+950.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 26274 0 0 0 94947 62 0 0 25 0 1 0 423164625 109797376 26193 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26806 26193 603 41 0 26765 0
vsize: 107224
[startup+960.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 26706 0 0 0 95947 63 0 0 25 0 1 0 423164625 111534080 26625 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27230 26625 603 41 0 27189 0
vsize: 108920
[startup+970.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 27464 0 0 0 96946 64 0 0 25 0 1 0 423164625 114626560 27383 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27985 27383 603 41 0 27944 0
vsize: 111940
[startup+980.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 28085 0 0 0 97944 66 0 0 25 0 1 0 423164625 117190656 28004 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28611 28004 603 41 0 28570 0
vsize: 114444
[startup+990.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 29052 0 0 0 98941 69 0 0 25 0 1 0 423164625 121102336 28971 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29566 28971 603 41 0 29525 0
vsize: 118264
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 29909 0 0 0 99939 72 0 0 25 0 1 0 423164625 124727296 29828 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30451 29828 603 41 0 30410 0
vsize: 121804
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30243 0 0 0 100939 72 0 0 25 0 1 0 423164625 126070784 30162 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30779 30162 603 41 0 30738 0
vsize: 123116
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30382 0 0 0 101938 73 0 0 25 0 1 0 423164625 126611456 30301 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30911 30301 603 41 0 30870 0
vsize: 123644
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30713 0 0 0 102938 73 0 0 25 0 1 0 423164625 127954944 30632 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31239 30632 603 41 0 31198 0
vsize: 124956
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30759 0 0 0 103938 73 0 0 25 0 1 0 423164625 128225280 30678 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31305 30678 603 41 0 31264 0
vsize: 125220
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30779 0 0 0 104938 74 0 0 25 0 1 0 423164625 128225280 30698 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31305 30698 603 41 0 31264 0
vsize: 125220
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30779 0 0 0 105938 74 0 0 25 0 1 0 423164625 128225280 30698 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31305 30698 603 41 0 31264 0
vsize: 125220
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30872 0 0 0 106938 74 0 0 25 0 1 0 423164625 128630784 30791 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31404 30791 603 41 0 31363 0
vsize: 125616
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 31729 0 0 0 107936 76 0 0 25 0 1 0 423164625 132407296 31648 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32326 31648 603 41 0 32285 0
vsize: 129304
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 31994 0 0 0 108935 77 0 0 25 0 1 0 423164625 133505024 31913 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32594 31913 603 41 0 32553 0
vsize: 130376
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32147 0 0 0 109935 77 0 0 25 0 1 0 423164625 134184960 32066 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32760 32066 603 41 0 32719 0
vsize: 131040
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32183 0 0 0 110935 77 0 0 25 0 1 0 423164625 134320128 32102 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32793 32102 603 41 0 32752 0
vsize: 131172
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32195 0 0 0 111935 77 0 0 25 0 1 0 423164625 134320128 32114 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32793 32114 603 41 0 32752 0
vsize: 131172
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32546 0 0 0 112935 78 0 0 25 0 1 0 423164625 135802880 32465 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33155 32465 603 41 0 33114 0
vsize: 132620
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32958 0 0 0 113935 78 0 0 25 0 1 0 423164625 137412608 32877 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33548 32877 603 41 0 33507 0
vsize: 134192
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 33437 0 0 0 114934 80 0 0 25 0 1 0 423164625 139436032 33356 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34042 33356 603 41 0 34001 0
vsize: 136168
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 33887 0 0 0 115933 81 0 0 25 0 1 0 423164625 141193216 33806 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34471 33806 603 41 0 34430 0
vsize: 137884
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34297 0 0 0 116932 82 0 0 25 0 1 0 423164625 142950400 34216 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34900 34216 603 41 0 34859 0
vsize: 139600
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34445 0 0 0 117932 82 0 0 25 0 1 0 423164625 143495168 34364 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35033 34364 603 41 0 34992 0
vsize: 140132
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34445 0 0 0 118932 82 0 0 25 0 1 0 423164625 143495168 34364 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35033 34364 603 41 0 34992 0
vsize: 140132
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 5455
Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34445 0 0 0 119932 82 0 0 25 0 1 0 423164625 143495168 34364 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35033 34364 603 41 0 34992 0
vsize: 140132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 5455
Raw data (stat): 5455 (minisat+) Z 5454 30701 30700 0 -1 12 34447 0 0 0 119932 89 0 0 25 0 1 0 423164625 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): 1200.07
CPU time (s): 1200.22
CPU user time (s): 1199.33
CPU system time (s): 0.890864
CPU usage (%): 100.012
Max. virtual memory (Kb): 140132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####