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-chnl35_40_pb.cnf.cr.opb
MD5SUM85d4e2fa5fd7a61a85d3ecb1e311bddb
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 41
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.083986
Number of variables2800
Total number of constraints150
Number of constraints which are clauses80
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint40

Trace number 4765 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-13 20:12:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=131 boxname=wulflinc28 idbench=15 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  85d4e2fa5fd7a61a85d3ecb1e311bddb  /oldhome/oroussel/tmp/wulflinc28/normalized-chnl35_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc28/normalized-chnl35_40_pb.cnf.cr.opb
IDLAUNCH: 131
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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	: 3
cpu MHz		: 451.077
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:        913096 kB
Buffers:         33860 kB
Cached:          52088 kB
SwapCached:          4 kB
Active:          47288 kB
Inactive:        41524 kB
HighTotal:      131008 kB
HighFree:        75320 kB
LowTotal:       903652 kB
LowFree:        837776 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27296 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:32:46 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 131 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 150 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13450    37590 |    4483       0        0     nan |  0.000 % |
c |       105 |   13450    37590 |    4931     105    13790   131.3 |  0.855 % |
c |       257 |   13450    37590 |    5424     257    35944   139.9 |  0.855 % |
c |       482 |   13450    37590 |    5966     482    76174   158.0 |  0.855 % |
c |       821 |   13450    37590 |    6563     821   135160   164.6 |  0.855 % |
c |      1328 |   13450    37590 |    7219    1328   240970   181.5 |  0.855 % |
c |      2087 |   13450    37590 |    7941    2087   409018   196.0 |  0.855 % |
c |      3228 |   13450    37590 |    8736    3228   633540   196.3 |  0.855 % |
c |      4936 |   13450    37590 |    9609    4936  1078151   218.4 |  0.855 % |
c |      7501 |   13450    37590 |   10570    7501  1705202   227.3 |  0.855 % |
c |     11350 |   13450    37590 |   11627   11350  2634616   232.1 |  0.855 % |
c |     17117 |   13450    37590 |   12790   10826  2688531   248.3 |  0.855 % |
c |     25768 |   13450    37590 |   14069   11465  2829373   246.8 |  0.855 % |
c |     38743 |   13450    37590 |   15476   15813  5417503   342.6 |  0.855 % |
c |     58205 |   13450    37590 |   17024   17974  5112296   284.4 |  0.855 % |
c |     87402 |   13450    37590 |   18726   15116  4555281   301.4 |  0.855 % |
c |    131192 |   13450    37590 |   20599   11825  3888204   328.8 |  0.855 % |
c |    196876 |   13450    37590 |   22659   21414  6424762   300.0 |  0.855 % |
c |    295403 |   13450    37590 |   24925   24280  8845785   364.3 |  0.855 % |
#### 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): 1.01 0.99 0.91 2/54 12231
Raw data (stat): 12231 (runsolver) R 12230 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478742232 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 2881 0 0 0 990 7 0 0 25 0 1 0 478742232 13746176 2856 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3356 2856 603 41 0 3315 0
vsize: 13424
[startup+20.0016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 4149 0 0 0 1986 11 0 0 25 0 1 0 478742232 18894848 4124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4613 4124 603 41 0 4572 0
vsize: 18452
[startup+30.0018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 4312 0 0 0 2985 12 0 0 25 0 1 0 478742232 19570688 4287 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4778 4287 603 41 0 4737 0
vsize: 19112
[startup+40.0023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 5404 0 0 0 3981 15 0 0 25 0 1 0 478742232 24076288 5379 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5878 5379 603 41 0 5837 0
vsize: 23512
[startup+50.0026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 5411 0 0 0 4981 15 0 0 25 0 1 0 478742232 24076288 5386 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5878 5386 603 41 0 5837 0
vsize: 23512
[startup+60.0026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 6098 0 0 0 5981 16 0 0 25 0 1 0 478742232 27025408 6073 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6598 6073 603 41 0 6557 0
vsize: 26392
[startup+70.0033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 6230 0 0 0 6981 16 0 0 25 0 1 0 478742232 27570176 6205 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6731 6205 603 41 0 6690 0
vsize: 26924
[startup+80.0027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 6230 0 0 0 7981 16 0 0 25 0 1 0 478742232 27570176 6205 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6731 6205 603 41 0 6690 0
vsize: 26924
[startup+90.0027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 6738 0 0 0 8980 17 0 0 25 0 1 0 478742232 29614080 6713 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7230 6713 603 41 0 7189 0
vsize: 28920
[startup+100.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7094 0 0 0 9979 18 0 0 25 0 1 0 478742232 31100928 7069 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7069 603 41 0 7552 0
vsize: 30372
[startup+110.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7236 0 0 0 10979 18 0 0 25 0 1 0 478742232 31653888 7211 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7728 7211 603 41 0 7687 0
vsize: 30912
[startup+120.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7878 0 0 0 11977 20 0 0 25 0 1 0 478742232 34349056 7853 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7853 603 41 0 8345 0
vsize: 33544
[startup+130.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7878 0 0 0 12977 20 0 0 25 0 1 0 478742232 34349056 7853 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7853 603 41 0 8345 0
vsize: 33544
[startup+140.004 s]
Raw data (loadavg): 1.08 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7879 0 0 0 13978 20 0 0 25 0 1 0 478742232 34349056 7854 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7854 603 41 0 8345 0
vsize: 33544
[startup+150.004 s]
Raw data (loadavg): 1.07 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7879 0 0 0 14978 20 0 0 25 0 1 0 478742232 34349056 7854 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7854 603 41 0 8345 0
vsize: 33544
[startup+160.004 s]
Raw data (loadavg): 1.06 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7879 0 0 0 15978 20 0 0 25 0 1 0 478742232 34349056 7854 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7854 603 41 0 8345 0
vsize: 33544
[startup+170.004 s]
Raw data (loadavg): 1.05 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7879 0 0 0 16978 20 0 0 25 0 1 0 478742232 34349056 7854 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7854 603 41 0 8345 0
vsize: 33544
[startup+180.004 s]
Raw data (loadavg): 1.04 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 7880 0 0 0 17978 20 0 0 25 0 1 0 478742232 34349056 7855 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7855 603 41 0 8345 0
vsize: 33544
[startup+190.004 s]
Raw data (loadavg): 1.03 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 8244 0 0 0 18977 21 0 0 25 0 1 0 478742232 35835904 8219 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8749 8219 603 41 0 8708 0
vsize: 34996
[startup+200.004 s]
Raw data (loadavg): 1.03 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 8688 0 0 0 19977 22 0 0 25 0 1 0 478742232 37588992 8663 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9177 8663 603 41 0 9136 0
vsize: 36708
[startup+210.004 s]
Raw data (loadavg): 1.02 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 8688 0 0 0 20977 22 0 0 25 0 1 0 478742232 37588992 8663 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9177 8663 603 41 0 9136 0
vsize: 36708
[startup+220.004 s]
Raw data (loadavg): 1.02 1.00 0.91 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 8701 0 0 0 21977 22 0 0 25 0 1 0 478742232 37785600 8676 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9225 8676 603 41 0 9184 0
vsize: 36900
[startup+230.004 s]
Raw data (loadavg): 1.10 1.02 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 8715 0 0 0 22977 22 0 0 25 0 1 0 478742232 37785600 8690 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9225 8690 603 41 0 9184 0
vsize: 36900
[startup+240.004 s]
Raw data (loadavg): 1.08 1.02 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9010 0 0 0 23977 23 0 0 25 0 1 0 478742232 39002112 8985 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9522 8985 603 41 0 9481 0
vsize: 38088
[startup+250.004 s]
Raw data (loadavg): 1.07 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9010 0 0 0 24977 23 0 0 25 0 1 0 478742232 39002112 8985 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9522 8985 603 41 0 9481 0
vsize: 38088
[startup+260.004 s]
Raw data (loadavg): 1.06 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9010 0 0 0 25977 23 0 0 25 0 1 0 478742232 39002112 8985 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9522 8985 603 41 0 9481 0
vsize: 38088
[startup+270.004 s]
Raw data (loadavg): 1.05 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9382 0 0 0 26976 24 0 0 25 0 1 0 478742232 40624128 9357 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9357 603 41 0 9877 0
vsize: 39672
[startup+280.004 s]
Raw data (loadavg): 1.04 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9382 0 0 0 27976 24 0 0 25 0 1 0 478742232 40624128 9357 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9357 603 41 0 9877 0
vsize: 39672
[startup+290.004 s]
Raw data (loadavg): 1.03 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9382 0 0 0 28977 24 0 0 25 0 1 0 478742232 40624128 9357 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9357 603 41 0 9877 0
vsize: 39672
[startup+300.004 s]
Raw data (loadavg): 1.03 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9402 0 0 0 29977 24 0 0 25 0 1 0 478742232 40624128 9377 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9377 603 41 0 9877 0
vsize: 39672
[startup+310.005 s]
Raw data (loadavg): 1.02 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9414 0 0 0 30977 24 0 0 25 0 1 0 478742232 40820736 9389 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9966 9389 603 41 0 9925 0
vsize: 39864
[startup+320.005 s]
Raw data (loadavg): 1.02 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9618 0 0 0 31976 25 0 0 25 0 1 0 478742232 41631744 9593 4294967295 134512640 134672761 3221224624 3221223808 134559569 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9593 603 41 0 10123 0
vsize: 40656
[startup+330.005 s]
Raw data (loadavg): 1.02 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9618 0 0 0 32976 25 0 0 25 0 1 0 478742232 41631744 9593 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9593 603 41 0 10123 0
vsize: 40656
[startup+340.006 s]
Raw data (loadavg): 1.01 1.01 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9627 0 0 0 33976 25 0 0 25 0 1 0 478742232 41631744 9602 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9602 603 41 0 10123 0
vsize: 40656
[startup+350.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9627 0 0 0 34977 25 0 0 25 0 1 0 478742232 41631744 9602 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9602 603 41 0 10123 0
vsize: 40656
[startup+360.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9627 0 0 0 35977 25 0 0 25 0 1 0 478742232 41631744 9602 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9602 603 41 0 10123 0
vsize: 40656
[startup+370.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9636 0 0 0 36977 25 0 0 25 0 1 0 478742232 41803776 9611 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10206 9611 603 41 0 10165 0
vsize: 40824
[startup+380.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9636 0 0 0 37977 25 0 0 25 0 1 0 478742232 41803776 9611 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10206 9611 603 41 0 10165 0
vsize: 40824
[startup+390.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 9636 0 0 0 38977 25 0 0 25 0 1 0 478742232 41803776 9611 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10206 9611 603 41 0 10165 0
vsize: 40824
[startup+400.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 10636 0 0 0 39975 28 0 0 25 0 1 0 478742232 45883392 10611 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11202 10611 603 41 0 11161 0
vsize: 44808
[startup+410.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 10636 0 0 0 40974 28 0 0 25 0 1 0 478742232 45883392 10611 4294967295 134512640 134672761 3221224624 3221223728 134560128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11202 10611 603 41 0 11161 0
vsize: 44808
[startup+420.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 10636 0 0 0 41974 28 0 0 25 0 1 0 478742232 45883392 10611 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11202 10611 603 41 0 11161 0
vsize: 44808
[startup+430.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11061 0 0 0 42974 29 0 0 25 0 1 0 478742232 47640576 11036 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11631 11036 603 41 0 11590 0
vsize: 46524
[startup+440.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11061 0 0 0 43974 29 0 0 25 0 1 0 478742232 47640576 11036 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11631 11036 603 41 0 11590 0
vsize: 46524
[startup+450.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11061 0 0 0 44974 29 0 0 25 0 1 0 478742232 47640576 11036 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11631 11036 603 41 0 11590 0
vsize: 46524
[startup+460.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11061 0 0 0 45974 29 0 0 25 0 1 0 478742232 47640576 11036 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11631 11036 603 41 0 11590 0
vsize: 46524
[startup+470.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11061 0 0 0 46974 29 0 0 25 0 1 0 478742232 47640576 11036 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11631 11036 603 41 0 11590 0
vsize: 46524
[startup+480.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11342 0 0 0 47974 29 0 0 25 0 1 0 478742232 48721920 11317 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11895 11317 603 41 0 11854 0
vsize: 47580
[startup+490.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11342 0 0 0 48974 29 0 0 25 0 1 0 478742232 48721920 11317 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11895 11317 603 41 0 11854 0
vsize: 47580
[startup+500.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11342 0 0 0 49974 29 0 0 25 0 1 0 478742232 48721920 11317 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11895 11317 603 41 0 11854 0
vsize: 47580
[startup+510.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11342 0 0 0 50975 29 0 0 25 0 1 0 478742232 48721920 11317 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11895 11317 603 41 0 11854 0
vsize: 47580
[startup+520.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11624 0 0 0 51974 30 0 0 25 0 1 0 478742232 49938432 11599 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12192 11599 603 41 0 12151 0
vsize: 48768
[startup+530.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 52974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+540.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 53974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+550.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 54974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+560.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 55974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+570.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 56974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+580.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 57974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+590.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 58974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+600.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 59974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+610.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 60973 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+620.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 61973 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+630.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 62973 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+640.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 63974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+650.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 64974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+660.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 65974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+670.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 11810 0 0 0 66974 31 0 0 25 0 1 0 478742232 50614272 11785 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12357 11785 603 41 0 12316 0
vsize: 49428
[startup+680.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12054 0 0 0 67973 32 0 0 25 0 1 0 478742232 51695616 12029 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12621 12029 603 41 0 12580 0
vsize: 50484
[startup+690.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12281 0 0 0 68973 33 0 0 25 0 1 0 478742232 52641792 12256 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12852 12256 603 41 0 12811 0
vsize: 51408
[startup+700.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12281 0 0 0 69973 33 0 0 25 0 1 0 478742232 52641792 12256 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12852 12256 603 41 0 12811 0
vsize: 51408
[startup+710.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12293 0 0 0 70973 33 0 0 25 0 1 0 478742232 52641792 12268 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12852 12268 603 41 0 12811 0
vsize: 51408
[startup+720.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12316 0 0 0 71974 33 0 0 25 0 1 0 478742232 52813824 12291 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12894 12291 603 41 0 12853 0
vsize: 51576
[startup+730.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12329 0 0 0 72974 33 0 0 25 0 1 0 478742232 52813824 12304 4294967295 134512640 134672761 3221224624 3221223728 134555379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12894 12304 603 41 0 12853 0
vsize: 51576
[startup+740.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12346 0 0 0 73974 33 0 0 25 0 1 0 478742232 53010432 12321 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12942 12321 603 41 0 12901 0
vsize: 51768
[startup+750.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12363 0 0 0 74974 33 0 0 25 0 1 0 478742232 53010432 12338 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12942 12338 603 41 0 12901 0
vsize: 51768
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12858 0 0 0 75973 35 0 0 25 0 1 0 478742232 55037952 12833 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13437 12833 603 41 0 13396 0
vsize: 53748
[startup+770.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12964 0 0 0 76972 35 0 0 25 0 1 0 478742232 55578624 12939 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 12939 603 41 0 13528 0
vsize: 54276
[startup+780.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12964 0 0 0 77972 35 0 0 25 0 1 0 478742232 55578624 12939 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 12939 603 41 0 13528 0
vsize: 54276
[startup+790.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12964 0 0 0 78973 35 0 0 25 0 1 0 478742232 55578624 12939 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 12939 603 41 0 13528 0
vsize: 54276
[startup+800.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12964 0 0 0 79973 35 0 0 25 0 1 0 478742232 55578624 12939 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 12939 603 41 0 13528 0
vsize: 54276
[startup+810.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12964 0 0 0 80973 35 0 0 25 0 1 0 478742232 55578624 12939 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 12939 603 41 0 13528 0
vsize: 54276
[startup+820.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12964 0 0 0 81973 35 0 0 25 0 1 0 478742232 55578624 12939 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 12939 603 41 0 13528 0
vsize: 54276
[startup+830.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12964 0 0 0 82973 35 0 0 25 0 1 0 478742232 55578624 12939 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 12939 603 41 0 13528 0
vsize: 54276
[startup+840.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 12996 0 0 0 83973 35 0 0 25 0 1 0 478742232 55713792 12971 4294967295 134512640 134672761 3221224624 3221223624 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13602 12971 603 41 0 13561 0
vsize: 54408
[startup+850.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13275 0 0 0 84973 36 0 0 25 0 1 0 478742232 56795136 13250 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13866 13250 603 41 0 13825 0
vsize: 55464
[startup+860.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13275 0 0 0 85973 36 0 0 25 0 1 0 478742232 56795136 13250 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13866 13250 603 41 0 13825 0
vsize: 55464
[startup+870.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13275 0 0 0 86973 36 0 0 25 0 1 0 478742232 56795136 13250 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13866 13250 603 41 0 13825 0
vsize: 55464
[startup+880.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13275 0 0 0 87973 36 0 0 25 0 1 0 478742232 56795136 13250 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13866 13250 603 41 0 13825 0
vsize: 55464
[startup+890.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13275 0 0 0 88973 36 0 0 25 0 1 0 478742232 56795136 13250 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13866 13250 603 41 0 13825 0
vsize: 55464
[startup+900.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13285 0 0 0 89974 36 0 0 25 0 1 0 478742232 56795136 13260 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13866 13260 603 41 0 13825 0
vsize: 55464
[startup+910.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13433 0 0 0 90973 37 0 0 25 0 1 0 478742232 57475072 13408 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14032 13408 603 41 0 13991 0
vsize: 56128
[startup+920.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13589 0 0 0 91973 38 0 0 25 0 1 0 478742232 58150912 13564 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13564 603 41 0 14156 0
vsize: 56788
[startup+930.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13589 0 0 0 92973 38 0 0 25 0 1 0 478742232 58150912 13564 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13564 603 41 0 14156 0
vsize: 56788
[startup+940.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13589 0 0 0 93973 38 0 0 25 0 1 0 478742232 58150912 13564 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13564 603 41 0 14156 0
vsize: 56788
[startup+950.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13589 0 0 0 94973 38 0 0 25 0 1 0 478742232 58150912 13564 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13564 603 41 0 14156 0
vsize: 56788
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13589 0 0 0 95973 38 0 0 25 0 1 0 478742232 58150912 13564 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13564 603 41 0 14156 0
vsize: 56788
[startup+970.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13589 0 0 0 96974 38 0 0 25 0 1 0 478742232 58150912 13564 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13564 603 41 0 14156 0
vsize: 56788
[startup+980.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 13740 0 0 0 97973 38 0 0 25 0 1 0 478742232 58757120 13715 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14345 13715 603 41 0 14304 0
vsize: 57380
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14181 0 0 0 98972 39 0 0 25 0 1 0 478742232 60649472 14156 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14807 14156 603 41 0 14766 0
vsize: 59228
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14192 0 0 0 99972 39 0 0 25 0 1 0 478742232 60649472 14167 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14807 14167 603 41 0 14766 0
vsize: 59228
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14202 0 0 0 100972 40 0 0 25 0 1 0 478742232 60784640 14177 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14177 603 41 0 14799 0
vsize: 59360
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14204 0 0 0 101972 40 0 0 25 0 1 0 478742232 60784640 14179 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14179 603 41 0 14799 0
vsize: 59360
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 102973 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 103973 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 104973 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 105973 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 106973 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223788 134559748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 107974 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 108974 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 109974 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 110974 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14205 0 0 0 111974 40 0 0 25 0 1 0 478742232 60784640 14180 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14180 603 41 0 14799 0
vsize: 59360
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 14649 0 0 0 112972 41 0 0 25 0 1 0 478742232 62533632 14624 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15267 14624 603 41 0 15226 0
vsize: 61068
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 15465 0 0 0 113969 44 0 0 25 0 1 0 478742232 65884160 15440 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 15440 603 41 0 16044 0
vsize: 64340
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 15465 0 0 0 114970 44 0 0 25 0 1 0 478742232 65884160 15440 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 15440 603 41 0 16044 0
vsize: 64340
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 15465 0 0 0 115970 44 0 0 25 0 1 0 478742232 65884160 15440 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 15440 603 41 0 16044 0
vsize: 64340
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 15465 0 0 0 116970 44 0 0 25 0 1 0 478742232 65884160 15440 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 15440 603 41 0 16044 0
vsize: 64340
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 15465 0 0 0 117970 44 0 0 25 0 1 0 478742232 65884160 15440 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 15440 603 41 0 16044 0
vsize: 64340
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 15465 0 0 0 118970 44 0 0 25 0 1 0 478742232 65884160 15440 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 15440 603 41 0 16044 0
vsize: 64340
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12231
Raw data (stat): 12231 (minisat+) R 12230 10614 10613 0 -1 0 15465 0 0 0 119971 44 0 0 25 0 1 0 478742232 65884160 15440 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 15440 603 41 0 16044 0
vsize: 64340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 12231
Raw data (stat): 12231 (minisat+) Z 12230 10614 10613 0 -1 12 15467 0 0 0 119971 47 0 0 25 0 1 0 478742232 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.05
CPU time (s): 1200.19
CPU user time (s): 1199.71
CPU system time (s): 0.476927
CPU usage (%): 100.012
Max. virtual memory (Kb): 64340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####