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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_51_pb.cnf.cr.opb
MD5SUM00bdc6bb9bafd4b1100d8bfa4f886626
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(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 52
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.156976
Number of variables5100
Total number of constraints202
Number of constraints which are clauses102
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint51

Trace number 5771 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 01:40:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4156 boxname=wulflinc3 idbench=20 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00bdc6bb9bafd4b1100d8bfa4f886626  /oldhome/oroussel/tmp/wulflinc3/normalized-chnl50_51_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-chnl50_51_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc3/normalized-chnl50_51_pb.cnf.cr.opb
IDLAUNCH: 4156
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        870780 kB
Buffers:         36152 kB
Cached:         104732 kB
SwapCached:       3276 kB
Active:          68728 kB
Inactive:        78272 kB
HighTotal:      131008 kB
HighFree:        22372 kB
LowTotal:       903652 kB
LowFree:        848408 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11288 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:00:08 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 4156 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 202 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................
c ---[  99]---> BDD-cost:   99
c ---[  98]---> BDD-cost:   99
c ---[  97]---> BDD-cost:   99
c ---[  96]---> BDD-cost:   99
c ---[  95]---> BDD-cost:   99
c ---[  94]---> BDD-cost:   99
c ---[  93]---> BDD-cost:   99
c ---[  92]---> BDD-cost:   99
c ---[  91]---> BDD-cost:   99
c ---[  90]---> BDD-cost:   99
c ---[  89]---> BDD-cost:   99
c ---[  88]---> BDD-cost:   99
c ---[  87]---> BDD-cost:   99
c ---[  86]---> BDD-cost:   99
c ---[  85]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   99
c ---[  83]---> BDD-cost:   99
c ---[  82]---> BDD-cost:   99
c ---[  81]---> BDD-cost:   99
c ---[  80]---> BDD-cost:   99
c ---[  79]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   99
c ---[  77]---> BDD-cost:   99
c ---[  76]---> BDD-cost:   99
c ---[  75]---> BDD-cost:   99
c ---[  74]---> BDD-cost:   99
c ---[  73]---> BDD-cost:   99
c ---[  72]---> BDD-cost:   99
c ---[  71]---> BDD-cost:   99
c ---[  70]---> BDD-cost:   99
c ---[  69]---> BDD-cost:   99
c ---[  68]---> BDD-cost:   99
c ---[  67]---> BDD-cost:   99
c ---[  66]---> BDD-cost:   99
c ---[  65]---> BDD-cost:   99
c ---[  64]---> BDD-cost:   99
c ---[  63]---> BDD-cost:   99
c ---[  62]---> BDD-cost:   99
c ---[  61]---> BDD-cost:   99
c ---[  60]---> BDD-cost:   99
c ---[  59]---> BDD-cost:   99
c ---[  58]---> BDD-cost:   99
c ---[  57]---> BDD-cost:   99
c ---[  56]---> BDD-cost:   99
c ---[  55]---> BDD-cost:   99
c ---[  54]---> BDD-cost:   99
c ---[  53]---> BDD-cost:   99
c ---[  52]---> BDD-cost:   99
c ---[  51]---> BDD-cost:   99
c ---[  50]---> BDD-cost:   99
c ---[  49]---> BDD-cost:   99
c ---[  48]---> BDD-cost:   99
c ---[  47]---> BDD-cost:   99
c ---[  46]---> BDD-cost:   99
c ---[  45]---> BDD-cost:   99
c ---[  44]---> BDD-cost:   99
c ---[  43]---> BDD-cost:   99
c ---[  42]---> BDD-cost:   99
c ---[  41]---> BDD-cost:   99
c ---[  40]---> BDD-cost:   99
c ---[  39]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   99
c ---[  37]---> BDD-cost:   99
c ---[  36]---> BDD-cost:   99
c ---[  35]---> BDD-cost:   99
c ---[  34]---> BDD-cost:   99
c ---[  33]---> BDD-cost:   99
c ---[  32]---> BDD-cost:   99
c ---[  31]---> BDD-cost:   99
c ---[  30]---> BDD-cost:   99
c ---[  29]---> BDD-cost:   99
c ---[  28]---> BDD-cost:   99
c ---[  27]---> BDD-cost:   99
c ---[  26]---> BDD-cost:   99
c ---[  25]---> BDD-cost:   99
c ---[  24]---> BDD-cost:   99
c ---[  23]---> BDD-cost:   99
c ---[  22]---> BDD-cost:   99
c ---[  21]---> BDD-cost:   99
c ---[  20]---> BDD-cost:   99
c ---[  19]---> BDD-cost:   99
c ---[  18]---> BDD-cost:   99
c ---[  17]---> BDD-cost:   99
c ---[  16]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   99
c ---[  14]---> BDD-cost:   99
c ---[  13]---> BDD-cost:   99
c ---[  12]---> BDD-cost:   99
c ---[  11]---> BDD-cost:   99
c ---[  10]---> BDD-cost:   99
c ---[   9]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   99
c ---[   7]---> BDD-cost:   99
c ---[   6]---> BDD-cost:   99
c ---[   5]---> BDD-cost:   99
c ---[   4]---> BDD-cost:   99
c ---[   3]---> BDD-cost:   99
c ---[   2]---> BDD-cost:   99
c ---[   1]---> BDD-cost:   99
c ---[   0]---> BDD-cost:   99
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   24702    69100 |    8234       0        0     nan |  0.000 % |
c |       103 |   24702    69100 |    9057     103    21251   206.3 |  0.667 % |
c |       257 |   24702    69100 |    9963     257    49705   193.4 |  0.667 % |
c |       483 |   24702    69100 |   10959     483   104379   216.1 |  0.667 % |
c |       820 |   24702    69100 |   12055     820   161617   197.1 |  0.667 % |
c |      1328 |   24702    69100 |   13260    1328   304812   229.5 |  0.667 % |
c |      2087 |   24702    69100 |   14587    2087   499248   239.2 |  0.667 % |
c |      3226 |   24702    69100 |   16045    3226   939931   291.4 |  0.667 % |
c |      4934 |   24702    69100 |   17650    4934  1692679   343.1 |  0.667 % |
c |      7497 |   24702    69100 |   19415    7497  2867483   382.5 |  0.667 % |
c |     11345 |   24702    69100 |   21356   11345  4334050   382.0 |  0.667 % |
c |     17113 |   24702    69100 |   23492   17113  7407340   432.8 |  0.667 % |
c |     25762 |   24702    69100 |   25841   25762 11735963   455.6 |  0.667 % |
c |     38736 |   24702    69100 |   28426   19007  8582103   451.5 |  0.667 % |
c |     58197 |   24702    69100 |   31268   16084  9622847   598.3 |  0.667 % |
c |     87391 |   24702    69100 |   34395   15805  8643661   546.9 |  0.667 % |
c |    131182 |   24702    69100 |   37835   29400 20102392   683.8 |  0.667 % |
#### 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.84 0.94 0.90 2/54 18560
Raw data (stat): 18560 (runsolver) R 18559 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422477062 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 3426 0 0 0 989 9 0 0 25 0 1 0 422477062 15720448 3401 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3401 603 41 0 3797 0
vsize: 15352
[startup+20.0026 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 5219 0 0 0 1983 14 0 0 25 0 1 0 422477062 23150592 5194 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5652 5194 603 41 0 5611 0
vsize: 22608
[startup+30.0028 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 6892 0 0 0 2978 18 0 0 25 0 1 0 422477062 29896704 6867 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7299 6867 603 41 0 7258 0
vsize: 29196
[startup+40.003 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 8638 0 0 0 3975 22 0 0 25 0 1 0 422477062 37216256 8613 4294967295 134512640 134672761 3221224544 3221223648 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9086 8613 603 41 0 9045 0
vsize: 36344
[startup+50.0041 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 10113 0 0 0 4971 25 0 0 25 0 1 0 422477062 43163648 10088 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10538 10088 603 41 0 10497 0
vsize: 42152
[startup+60.0034 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 11354 0 0 0 5968 27 0 0 25 0 1 0 422477062 48291840 11329 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11790 11329 603 41 0 11749 0
vsize: 47160
[startup+70.0042 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 12561 0 0 0 6966 30 0 0 25 0 1 0 422477062 53153792 12536 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12977 12536 603 41 0 12936 0
vsize: 51908
[startup+80.0053 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 13546 0 0 0 7964 32 0 0 25 0 1 0 422477062 57204736 13521 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13966 13521 603 41 0 13925 0
vsize: 55864
[startup+90.0049 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 14912 0 0 0 8961 35 0 0 25 0 1 0 422477062 62865408 14887 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15348 14887 603 41 0 15307 0
vsize: 61392
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 15915 0 0 0 9959 37 0 0 25 0 1 0 422477062 66908160 15890 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16335 15890 603 41 0 16294 0
vsize: 65340
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 10959 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+120.005 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 11959 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+130.005 s]
Raw data (loadavg): 1.12 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 12959 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+140.006 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 13958 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+150.006 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 14958 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+160.006 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 15958 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+170.006 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 16958 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+180.005 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 17958 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+190.005 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 18959 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+200.005 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16217 0 0 0 19959 38 0 0 25 0 1 0 422477062 68263936 16192 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16666 16192 603 41 0 16625 0
vsize: 66664
[startup+210.005 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 16693 0 0 0 20958 39 0 0 25 0 1 0 422477062 70156288 16668 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17128 16669 603 41 0 17087 0
vsize: 68512
[startup+220.006 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 17324 0 0 0 21957 40 0 0 25 0 1 0 422477062 72749056 17299 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17761 17299 603 41 0 17720 0
vsize: 71044
[startup+230.006 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 17859 0 0 0 22956 41 0 0 25 0 1 0 422477062 75046912 17834 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18322 17834 603 41 0 18281 0
vsize: 73288
[startup+240.005 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 18385 0 0 0 23955 42 0 0 25 0 1 0 422477062 77209600 18360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18850 18360 603 41 0 18809 0
vsize: 75400
[startup+250.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 19087 0 0 0 24953 44 0 0 25 0 1 0 422477062 80044032 19062 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19542 19062 603 41 0 19501 0
vsize: 78168
[startup+260.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 19747 0 0 0 25952 45 0 0 25 0 1 0 422477062 83005440 19722 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20265 19722 603 41 0 20224 0
vsize: 81060
[startup+270.006 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20214 0 0 0 26952 46 0 0 25 0 1 0 422477062 84897792 20189 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20727 20189 603 41 0 20686 0
vsize: 82908
[startup+280.006 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20742 0 0 0 27951 47 0 0 25 0 1 0 422477062 87060480 20717 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21255 20717 603 41 0 21214 0
vsize: 85020
[startup+290.006 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 28950 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+300.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 29951 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+310.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 30951 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+320.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 31950 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+330.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 32951 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+340.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 33951 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+350.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 34951 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+360.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 20896 0 0 0 35951 48 0 0 25 0 1 0 422477062 87601152 20871 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21387 20871 603 41 0 21346 0
vsize: 85548
[startup+370.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 21251 0 0 0 36951 48 0 0 25 0 1 0 422477062 89100288 21226 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21753 21226 603 41 0 21712 0
vsize: 87012
[startup+380.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 22384 0 0 0 37949 50 0 0 25 0 1 0 422477062 93831168 22359 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22908 22359 603 41 0 22867 0
vsize: 91632
[startup+390.008 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 23559 0 0 0 38947 52 0 0 25 0 1 0 422477062 98570240 23534 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24065 23534 603 41 0 24024 0
vsize: 96260
[startup+400.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 24647 0 0 0 39946 54 0 0 25 0 1 0 422477062 103067648 24622 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25163 24622 603 41 0 25122 0
vsize: 100652
[startup+410.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 25679 0 0 0 40944 56 0 0 25 0 1 0 422477062 107294720 25654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26195 25654 603 41 0 26154 0
vsize: 104780
[startup+420.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 26691 0 0 0 41943 57 0 0 25 0 1 0 422477062 111566848 26666 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27238 26666 603 41 0 27197 0
vsize: 108952
[startup+430.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 27696 0 0 0 42941 59 0 0 25 0 1 0 422477062 115601408 27671 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28223 27671 603 41 0 28182 0
vsize: 112892
[startup+440.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28704 0 0 0 43939 62 0 0 25 0 1 0 422477062 119795712 28679 4294967295 134512640 134672761 3221224544 3221223500 1075349683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29247 28679 603 41 0 29206 0
vsize: 116988
[startup+450.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28934 0 0 0 44939 62 0 0 25 0 1 0 422477062 120733696 28909 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28909 603 41 0 29435 0
vsize: 117904
[startup+460.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 45938 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+470.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 46938 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+480.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 47938 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+490.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 48938 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223728 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+500.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 49939 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+510.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 50939 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+520.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 51939 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+530.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 52939 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+540.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 53939 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+550.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 54939 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+560.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 55940 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+570.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 56940 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+580.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 57940 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+590.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 58940 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+600.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28936 0 0 0 59940 62 0 0 25 0 1 0 422477062 120733696 28911 4294967295 134512640 134672761 3221224544 3221223640 1075347400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29476 28911 603 41 0 29435 0
vsize: 117904
[startup+610.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 28978 0 0 0 60940 62 0 0 25 0 1 0 422477062 120868864 28953 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29509 28953 603 41 0 29468 0
vsize: 118036
[startup+620.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29598 0 0 0 61939 63 0 0 25 0 1 0 422477062 123432960 29573 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29573 603 41 0 30094 0
vsize: 120540
[startup+630.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29598 0 0 0 62940 63 0 0 25 0 1 0 422477062 123432960 29573 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29573 603 41 0 30094 0
vsize: 120540
[startup+640.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 63940 63 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+650.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 64940 63 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+660.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 65940 63 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+670.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 66940 63 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+680.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 67941 63 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+690.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 68941 64 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+700.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 69941 64 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+710.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 70941 64 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+720.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 71941 64 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+730.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 72941 64 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223728 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+740.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 29599 0 0 0 73941 64 0 0 25 0 1 0 422477062 123432960 29574 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30135 29574 603 41 0 30094 0
vsize: 120540
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 30406 0 0 0 74939 66 0 0 25 0 1 0 422477062 126808064 30381 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30959 30381 603 41 0 30918 0
vsize: 123836
[startup+760.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 31316 0 0 0 75937 68 0 0 25 0 1 0 422477062 130453504 31291 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31849 31291 603 41 0 31808 0
vsize: 127396
[startup+770.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 32277 0 0 0 76935 71 0 0 25 0 1 0 422477062 134369280 32252 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32805 32252 603 41 0 32764 0
vsize: 131220
[startup+780.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 33037 0 0 0 77933 72 0 0 25 0 1 0 422477062 137515008 33012 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33573 33012 603 41 0 33532 0
vsize: 134292
[startup+790.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 33858 0 0 0 78932 74 0 0 25 0 1 0 422477062 141074432 33833 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34442 33833 603 41 0 34401 0
vsize: 137768
[startup+800.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 34652 0 0 0 79930 76 0 0 25 0 1 0 422477062 144326656 34627 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35236 34627 603 41 0 35195 0
vsize: 140944
[startup+810.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35088 0 0 0 80929 77 0 0 25 0 1 0 422477062 146104320 35063 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35063 603 41 0 35629 0
vsize: 142680
[startup+820.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35089 0 0 0 81929 77 0 0 25 0 1 0 422477062 146104320 35064 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35064 603 41 0 35629 0
vsize: 142680
[startup+830.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35090 0 0 0 82929 77 0 0 25 0 1 0 422477062 146104320 35065 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35065 603 41 0 35629 0
vsize: 142680
[startup+840.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35090 0 0 0 83929 77 0 0 25 0 1 0 422477062 146104320 35065 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35065 603 41 0 35629 0
vsize: 142680
[startup+850.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35093 0 0 0 84929 77 0 0 25 0 1 0 422477062 146104320 35068 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35068 603 41 0 35629 0
vsize: 142680
[startup+860.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35096 0 0 0 85930 77 0 0 25 0 1 0 422477062 146104320 35071 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35071 603 41 0 35629 0
vsize: 142680
[startup+870.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35100 0 0 0 86930 77 0 0 25 0 1 0 422477062 146104320 35075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35075 603 41 0 35629 0
vsize: 142680
[startup+880.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35100 0 0 0 87930 77 0 0 25 0 1 0 422477062 146104320 35075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35075 603 41 0 35629 0
vsize: 142680
[startup+890.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35100 0 0 0 88930 77 0 0 25 0 1 0 422477062 146104320 35075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35075 603 41 0 35629 0
vsize: 142680
[startup+900.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35101 0 0 0 89931 77 0 0 25 0 1 0 422477062 146104320 35076 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35076 603 41 0 35629 0
vsize: 142680
[startup+910.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35105 0 0 0 90931 77 0 0 25 0 1 0 422477062 146104320 35080 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35080 603 41 0 35629 0
vsize: 142680
[startup+920.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35105 0 0 0 91931 77 0 0 25 0 1 0 422477062 146104320 35080 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35080 603 41 0 35629 0
vsize: 142680
[startup+930.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35108 0 0 0 92931 77 0 0 25 0 1 0 422477062 146104320 35083 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35083 603 41 0 35629 0
vsize: 142680
[startup+940.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35112 0 0 0 93931 78 0 0 25 0 1 0 422477062 146104320 35087 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35087 603 41 0 35629 0
vsize: 142680
[startup+950.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35114 0 0 0 94932 78 0 0 25 0 1 0 422477062 146104320 35089 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35089 603 41 0 35629 0
vsize: 142680
[startup+960.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35116 0 0 0 95932 78 0 0 25 0 1 0 422477062 146104320 35091 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35091 603 41 0 35629 0
vsize: 142680
[startup+970.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35119 0 0 0 96932 78 0 0 25 0 1 0 422477062 146104320 35094 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35094 603 41 0 35629 0
vsize: 142680
[startup+980.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35120 0 0 0 97932 78 0 0 25 0 1 0 422477062 146104320 35095 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35095 603 41 0 35629 0
vsize: 142680
[startup+990.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35124 0 0 0 98932 78 0 0 25 0 1 0 422477062 146104320 35099 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35099 603 41 0 35629 0
vsize: 142680
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35124 0 0 0 99933 78 0 0 25 0 1 0 422477062 146104320 35099 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35099 603 41 0 35629 0
vsize: 142680
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35124 0 0 0 100933 78 0 0 25 0 1 0 422477062 146104320 35099 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35099 603 41 0 35629 0
vsize: 142680
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35124 0 0 0 101933 78 0 0 25 0 1 0 422477062 146104320 35099 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35099 603 41 0 35629 0
vsize: 142680
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35125 0 0 0 102933 78 0 0 25 0 1 0 422477062 146104320 35100 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35100 603 41 0 35629 0
vsize: 142680
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35125 0 0 0 103933 78 0 0 25 0 1 0 422477062 146104320 35100 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35100 603 41 0 35629 0
vsize: 142680
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35125 0 0 0 104934 78 0 0 25 0 1 0 422477062 146104320 35100 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35100 603 41 0 35629 0
vsize: 142680
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35125 0 0 0 105934 78 0 0 25 0 1 0 422477062 146104320 35100 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35100 603 41 0 35629 0
vsize: 142680
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35125 0 0 0 106934 78 0 0 25 0 1 0 422477062 146104320 35100 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35100 603 41 0 35629 0
vsize: 142680
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35125 0 0 0 107934 78 0 0 25 0 1 0 422477062 146104320 35100 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35100 603 41 0 35629 0
vsize: 142680
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35132 0 0 0 108935 78 0 0 25 0 1 0 422477062 146104320 35107 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35107 603 41 0 35629 0
vsize: 142680
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35133 0 0 0 109935 78 0 0 25 0 1 0 422477062 146104320 35108 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35108 603 41 0 35629 0
vsize: 142680
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35133 0 0 0 110935 78 0 0 25 0 1 0 422477062 146104320 35108 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35108 603 41 0 35629 0
vsize: 142680
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 111935 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 112935 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 113936 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 114936 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 115936 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 116936 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 117936 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18560
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 118937 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 18599
Raw data (stat): 18560 (minisat+) R 18559 10720 10719 0 -1 0 35134 0 0 0 119937 78 0 0 25 0 1 0 422477062 146104320 35109 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35670 35109 603 41 0 35629 0
vsize: 142680
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 18600
Raw data (stat): 18560 (minisat+) Z 18559 10720 10719 0 -1 12 35136 0 0 0 119937 84 0 0 25 0 1 0 422477062 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.11
CPU time (s): 1200.22
CPU user time (s): 1199.37
CPU system time (s): 0.847871
CPU usage (%): 100.009
Max. virtual memory (Kb): 142680
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####