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 4813

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 20:24:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=194 boxname=wulflinc6 idbench=22 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6968a43b42bba7df68b13fdfd3b616a1  /oldhome/oroussel/tmp/wulflinc6/normalized-chnl50_60_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc6/normalized-chnl50_60_pb.cnf.cr.opb
IDLAUNCH: 194
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        922448 kB
Buffers:         34256 kB
Cached:          56328 kB
SwapCached:       2644 kB
Active:          49076 kB
Inactive:        46988 kB
HighTotal:      131008 kB
HighFree:        70784 kB
LowTotal:       903652 kB
LowFree:        851664 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10648 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:44:09 (client local time) WITH STATUS 0 IN 1200.41 SECONDS
stats: 194 7 1200.41 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 |   29220    81700 |    9740       0        0     nan |  0.000 % |
c |       104 |   29220    81700 |   10714     104    19328   185.8 |  0.565 % |
c |       256 |   29220    81700 |   11785     256    51373   200.7 |  0.565 % |
c |       482 |   29220    81700 |   12963     482   102298   212.2 |  0.565 % |
c |       824 |   29220    81700 |   14260     824   174285   211.5 |  0.565 % |
c |      1330 |   29220    81700 |   15686    1330   314613   236.6 |  0.565 % |
c |      2091 |   29220    81700 |   17255    2091   547467   261.8 |  0.565 % |
c |      3231 |   29220    81700 |   18980    3231   973163   301.2 |  0.565 % |
c |      4940 |   29220    81700 |   20878    4940  1825691   369.6 |  0.565 % |
c |      7502 |   29220    81700 |   22966    7502  3300948   440.0 |  0.565 % |
c |     11349 |   29220    81700 |   25263   11349  4927293   434.2 |  0.565 % |
c |     17116 |   29220    81700 |   27789   17116  7830885   457.5 |  0.565 % |
c |     25776 |   29220    81700 |   30568   25776 12693138   492.4 |  0.565 % |
c |     38750 |   29220    81700 |   33625   12745  7008530   549.9 |  0.565 % |
c |     58211 |   29220    81700 |   36987   32206 21026723   652.9 |  0.565 % |
c |     87408 |   29220    81700 |   40686   27744 13222109   476.6 |  0.565 % |
c |    131200 |   29220    81700 |   44755   36115 20717915   573.7 |  0.565 % |
#### 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.91 0.95 0.90 2/54 31674
Raw data (stat): 31674 (runsolver) R 31673 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420584260 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.95 0.90 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 3607 0 0 0 989 9 0 0 25 0 1 0 420584260 16920576 3526 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4131 3526 603 41 0 4090 0
vsize: 16524
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 5335 0 0 0 1985 13 0 0 25 0 1 0 420584260 23937024 5254 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5844 5254 603 41 0 5803 0
vsize: 23376
[startup+30.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 6831 0 0 0 2982 16 0 0 25 0 1 0 420584260 30027776 6750 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7331 6750 603 41 0 7290 0
vsize: 29324
[startup+40.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 8361 0 0 0 3978 19 0 0 25 0 1 0 420584260 36356096 8280 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8876 8280 603 41 0 8835 0
vsize: 35504
[startup+50.0037 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 9842 0 0 0 4973 25 0 0 25 0 1 0 420584260 42397696 9761 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10351 9761 603 41 0 10310 0
vsize: 41404
[startup+60.0042 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 11205 0 0 0 5969 29 0 0 25 0 1 0 420584260 48066560 11124 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11735 11124 603 41 0 11694 0
vsize: 46940
[startup+70.0053 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 12685 0 0 0 6965 34 0 0 25 0 1 0 420584260 54140928 12604 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13218 12604 603 41 0 13177 0
vsize: 52872
[startup+80.0061 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 13899 0 0 0 7961 38 0 0 25 0 1 0 420584260 59015168 13818 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14408 13818 603 41 0 14367 0
vsize: 57632
[startup+90.0066 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 15170 0 0 0 8957 41 0 0 25 0 1 0 420584260 64274432 15089 4294967295 134512640 134672761 3221224624 3221223728 134554926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15692 15089 603 41 0 15651 0
vsize: 62768
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 16647 0 0 0 9953 45 0 0 25 0 1 0 420584260 70356992 16566 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17177 16566 603 41 0 17136 0
vsize: 68708
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 18116 0 0 0 10950 49 0 0 25 0 1 0 420584260 76292096 18035 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18626 18035 603 41 0 18585 0
vsize: 74504
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 19261 0 0 0 11948 51 0 0 25 0 1 0 420584260 81149952 19180 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19812 19180 603 41 0 19771 0
vsize: 79248
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 20127 0 0 0 12945 54 0 0 25 0 1 0 420584260 84664320 20046 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20670 20046 603 41 0 20629 0
vsize: 82680
[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 20890 0 0 0 13944 55 0 0 25 0 1 0 420584260 87769088 20809 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21428 20809 603 41 0 21387 0
vsize: 85712
[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21568 0 0 0 14942 57 0 0 25 0 1 0 420584260 90603520 21487 4294967295 134512640 134672761 3221224624 3221223728 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22120 21487 603 41 0 22079 0
vsize: 88480
[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21899 0 0 0 15942 58 0 0 25 0 1 0 420584260 91955200 21818 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21818 603 41 0 22409 0
vsize: 89800
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 16941 58 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 17941 59 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223836 1075346912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 18941 59 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 19941 59 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 20941 59 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 21941 60 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 22941 60 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 23941 60 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 24941 60 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 21900 0 0 0 25941 61 0 0 25 0 1 0 420584260 91955200 21819 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21819 603 41 0 22409 0
vsize: 89800
[startup+270.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 22572 0 0 0 26939 63 0 0 25 0 1 0 420584260 94658560 22491 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23110 22491 603 41 0 23069 0
vsize: 92440
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 23575 0 0 0 27937 65 0 0 25 0 1 0 420584260 98906112 23494 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24147 23494 603 41 0 24106 0
vsize: 96588
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 24834 0 0 0 28935 67 0 0 25 0 1 0 420584260 104071168 24753 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25408 24753 603 41 0 25367 0
vsize: 101632
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 26020 0 0 0 29931 71 0 0 25 0 1 0 420584260 108920832 25939 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26592 25939 603 41 0 26551 0
vsize: 106368
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 26872 0 0 0 30929 74 0 0 25 0 1 0 420584260 112431104 26791 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26791 603 41 0 27408 0
vsize: 109796
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 27712 0 0 0 31927 76 0 0 25 0 1 0 420584260 115937280 27631 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28305 27631 603 41 0 28264 0
vsize: 113220
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 28534 0 0 0 32926 77 0 0 25 0 1 0 420584260 119209984 28453 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29104 28453 603 41 0 29063 0
vsize: 116416
[startup+340.023 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 29264 0 0 0 33925 79 0 0 25 0 1 0 420584260 122204160 29183 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29835 29183 603 41 0 29794 0
vsize: 119340
[startup+350.023 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30111 0 0 0 34923 80 0 0 25 0 1 0 420584260 125743104 30030 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30699 30030 603 41 0 30658 0
vsize: 122796
[startup+360.023 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30177 0 0 0 35924 81 0 0 25 0 1 0 420584260 126009344 30096 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30096 603 41 0 30723 0
vsize: 123056
[startup+370.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30178 0 0 0 36924 81 0 0 25 0 1 0 420584260 126009344 30097 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30097 603 41 0 30723 0
vsize: 123056
[startup+380.023 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30179 0 0 0 37924 81 0 0 25 0 1 0 420584260 126009344 30098 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30098 603 41 0 30723 0
vsize: 123056
[startup+390.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30179 0 0 0 38925 81 0 0 25 0 1 0 420584260 126009344 30098 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30098 603 41 0 30723 0
vsize: 123056
[startup+400.025 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30180 0 0 0 39925 81 0 0 25 0 1 0 420584260 126009344 30099 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30099 603 41 0 30723 0
vsize: 123056
[startup+410.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30181 0 0 0 40925 81 0 0 25 0 1 0 420584260 126009344 30100 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30100 603 41 0 30723 0
vsize: 123056
[startup+420.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30181 0 0 0 41926 81 0 0 25 0 1 0 420584260 126009344 30100 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30100 603 41 0 30723 0
vsize: 123056
[startup+430.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 42926 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+440.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 43927 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+450.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 44927 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+460.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 45927 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+470.029 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 46927 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223808 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+480.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 47928 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+490.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 48928 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+500.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 49928 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+510.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 50929 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+520.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 51929 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+530.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30182 0 0 0 52929 81 0 0 25 0 1 0 420584260 126009344 30101 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+540.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30183 0 0 0 53930 81 0 0 25 0 1 0 420584260 126009344 30102 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30764 30102 603 41 0 30723 0
vsize: 123056
[startup+550.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 54930 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+560.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 55930 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+570.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 56931 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+580.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 57931 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+590.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 58932 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+600.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 59932 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+610.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 60932 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+620.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 61933 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+630.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 62933 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+640.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 63934 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+650.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 64934 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+660.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 65934 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+670.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 66935 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223808 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+680.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 67935 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+690.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 68936 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+700.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 69936 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+710.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 70936 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+720.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 71936 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223728 134560480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+730.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 72936 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+740.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 73937 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+750.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 74937 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+760.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30184 0 0 0 75938 81 0 0 25 0 1 0 420584260 125927424 30103 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+770.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 30829 0 0 0 76936 83 0 0 25 0 1 0 420584260 128626688 30748 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31403 30748 603 41 0 31362 0
vsize: 125612
[startup+780.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 31495 0 0 0 77935 84 0 0 25 0 1 0 420584260 131325952 31414 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32062 31414 603 41 0 32021 0
vsize: 128248
[startup+790.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32248 0 0 0 78934 86 0 0 25 0 1 0 420584260 134443008 32167 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32823 32167 603 41 0 32782 0
vsize: 131292
[startup+800.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 79933 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+810.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 80934 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+820.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 81934 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+830.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 82935 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+840.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 83935 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+850.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 84935 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+860.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 85936 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+870.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 86936 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+880.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 87937 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+890.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 88937 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+900.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 89937 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+910.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 90938 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+920.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 91938 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+930.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 92938 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+940.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 93939 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+950.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 94939 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+960.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 95939 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+970.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 96940 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+980.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32695 0 0 0 97940 87 0 0 25 0 1 0 420584260 136200192 32614 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+990.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 98940 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 99941 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 100941 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 101941 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 102941 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 103942 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 104942 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 105942 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 106943 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 107943 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 108943 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 109944 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 110944 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 111944 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 112945 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 113945 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 114946 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32696 0 0 0 115946 87 0 0 25 0 1 0 420584260 136200192 32615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32697 0 0 0 116946 87 0 0 25 0 1 0 420584260 136200192 32616 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32616 603 41 0 33211 0
vsize: 133008
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32698 0 0 0 117947 87 0 0 25 0 1 0 420584260 136200192 32617 4294967295 134512640 134672761 3221224624 3221223728 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32617 603 41 0 33211 0
vsize: 133008
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32698 0 0 0 118947 87 0 0 25 0 1 0 420584260 136200192 32617 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32617 603 41 0 33211 0
vsize: 133008
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31674
Raw data (stat): 31674 (minisat+) R 31673 29653 29652 0 -1 0 32698 0 0 0 119947 87 0 0 25 0 1 0 420584260 136200192 32617 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32617 603 41 0 33211 0
vsize: 133008
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 31674
Raw data (stat): 31674 (minisat+) Z 31673 29653 29652 0 -1 12 32700 0 0 0 119947 93 0 0 25 0 1 0 420584260 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.12
CPU time (s): 1200.41
CPU user time (s): 1199.48
CPU system time (s): 0.934857
CPU usage (%): 100.025
Max. virtual memory (Kb): 133008
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####