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-chnl30_31_pb.cnf.cr.opb
MD5SUM79bafd08ddd684356ab9abc8fabf88a7
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 32
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.05399
Number of variables1860
Total number of constraints122
Number of constraints which are clauses62
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint31

Trace number 4581 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-13 19:24:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3395 boxname=wulflinc8 idbench=11 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  79bafd08ddd684356ab9abc8fabf88a7  /oldhome/oroussel/tmp/wulflinc8/normalized-chnl30_31_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-chnl30_31_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc8/normalized-chnl30_31_pb.cnf.cr.opb
IDLAUNCH: 3395
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        914988 kB
Buffers:         36496 kB
Cached:          64144 kB
SwapCached:          0 kB
Active:          72088 kB
Inactive:        31396 kB
HighTotal:      131008 kB
HighFree:        62944 kB
LowTotal:       903652 kB
LowFree:        852044 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            10584 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:44:29 (client local time) WITH STATUS 0 IN 1200.09 SECONDS
stats: 3395 7 1200.09 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 122 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................
c ---[  59]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  58]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  57]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  56]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  55]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  54]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  53]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  52]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  51]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  50]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  49]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  48]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  47]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  46]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  45]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  44]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  43]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  42]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  41]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  40]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  39]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  38]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  37]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  36]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  35]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  34]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  33]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  32]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  31]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  30]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  29]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  28]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  27]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  26]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  25]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  24]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  23]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  22]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  21]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  20]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  19]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  18]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  17]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  16]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  15]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  14]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  13]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  12]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  11]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  10]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   9]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   8]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   7]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   6]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   5]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   4]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   3]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   2]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   1]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[   0]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20522    74520 |    6840       0        0     nan |  0.000 % |
c |       100 |   20497    74431 |    7524      96      360     3.8 |  8.314 % |
c |       250 |   20425    74185 |    8276     236     1171     5.0 |  8.549 % |
c |       475 |   20300    73758 |    9104     444     2608     5.9 |  8.941 % |
c |       812 |   20009    72759 |   10014     742     4044     5.5 |  9.824 % |
c |      1319 |   19392    70630 |   11015    1156     6220     5.4 | 11.882 % |
c |      2078 |   17255    63175 |   12117    1595     9329     5.8 | 19.098 % |
c |      3217 |   12288    46134 |   13329    1908    13225     6.9 | 36.431 % |
c |      4928 |   11526    43576 |   14662    3476   544654   156.7 | 39.235 % |
c |      7490 |   11526    43576 |   16128    6038  1324412   219.3 | 39.235 % |
c |     11334 |   11526    43576 |   17741    9882  2473986   250.4 | 39.235 % |
c |     17100 |   11526    43576 |   19515   15648  3951299   252.5 | 39.235 % |
c |     25749 |   11526    43576 |   21466   13112  3178928   242.4 | 39.235 % |
c |     38725 |   11483    43437 |   23613   13270  6986484   526.5 | 39.412 % |
c |     58186 |   11483    43437 |   25974   18681  9571338   512.4 | 39.412 % |
c |     87378 |   11483    43437 |   28572   15850  8029932   506.6 | 39.412 % |
c |    131172 |   11442    43304 |   31429   22638 13072135   577.4 | 39.569 % |
#### 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.13 0.05 0.01 2/54 28200
Raw data (stat): 28200 (runsolver) R 28199 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 406662240 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99975 s]
Raw data (loadavg): 0.27 0.08 0.02 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 1299 0 1 0 983 4 0 0 25 0 1 0 406662240 6946816 1278 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1696 1278 603 41 0 1655 0
vsize: 6784
[startup+19.9997 s]
Raw data (loadavg): 0.38 0.11 0.03 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 3332 0 1 0 1976 10 0 0 25 0 1 0 406662240 15380480 3311 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3755 3311 603 41 0 3714 0
vsize: 15020
[startup+30.0003 s]
Raw data (loadavg): 0.47 0.14 0.04 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 5267 0 1 0 2971 15 0 0 25 0 1 0 406662240 23384064 5246 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5709 5246 603 41 0 5668 0
vsize: 22836
[startup+40 s]
Raw data (loadavg): 0.55 0.17 0.05 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 6655 0 1 0 3968 18 0 0 25 0 1 0 406662240 29052928 6634 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7093 6634 603 41 0 7052 0
vsize: 28372
[startup+50.0011 s]
Raw data (loadavg): 0.62 0.20 0.06 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 6968 0 1 0 4967 19 0 0 25 0 1 0 406662240 30269440 6947 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7390 6947 603 41 0 7349 0
vsize: 29560
[startup+60.0005 s]
Raw data (loadavg): 0.68 0.22 0.07 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 6968 0 1 0 5967 19 0 0 25 0 1 0 406662240 30269440 6947 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7390 6947 603 41 0 7349 0
vsize: 29560
[startup+70.0003 s]
Raw data (loadavg): 0.73 0.25 0.08 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 7757 0 1 0 6965 21 0 0 25 0 1 0 406662240 33505280 7736 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8180 7736 603 41 0 8139 0
vsize: 32720
[startup+80.0014 s]
Raw data (loadavg): 0.77 0.27 0.09 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 9012 0 1 0 7963 24 0 0 25 0 1 0 406662240 38772736 8991 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9466 8991 603 41 0 9425 0
vsize: 37864
[startup+90.0009 s]
Raw data (loadavg): 0.80 0.29 0.10 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 10170 0 1 0 8961 26 0 0 25 0 1 0 406662240 43511808 10149 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10623 10149 603 41 0 10582 0
vsize: 42492
[startup+100.001 s]
Raw data (loadavg): 0.83 0.32 0.11 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 10879 0 1 0 9960 27 0 0 25 0 1 0 406662240 46477312 10858 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11347 10858 603 41 0 11306 0
vsize: 45388
[startup+110.001 s]
Raw data (loadavg): 0.86 0.34 0.12 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 10879 0 1 0 10960 27 0 0 25 0 1 0 406662240 46477312 10858 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11347 10858 603 41 0 11306 0
vsize: 45388
[startup+120.001 s]
Raw data (loadavg): 0.88 0.36 0.13 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 10879 0 1 0 11960 27 0 0 25 0 1 0 406662240 46477312 10858 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11347 10858 603 41 0 11306 0
vsize: 45388
[startup+130.001 s]
Raw data (loadavg): 0.90 0.38 0.14 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 10879 0 1 0 12961 27 0 0 25 0 1 0 406662240 46477312 10858 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11347 10858 603 41 0 11306 0
vsize: 45388
[startup+140.001 s]
Raw data (loadavg): 0.91 0.40 0.14 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 11774 0 1 0 13959 29 0 0 25 0 1 0 406662240 50118656 11753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12236 11753 603 41 0 12195 0
vsize: 48944
[startup+150.002 s]
Raw data (loadavg): 0.93 0.42 0.15 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 12653 0 1 0 14957 31 0 0 25 0 1 0 406662240 53751808 12632 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13123 12632 603 41 0 13082 0
vsize: 52492
[startup+160.001 s]
Raw data (loadavg): 0.94 0.44 0.16 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 13491 0 1 0 15955 34 0 0 25 0 1 0 406662240 57131008 13470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13948 13470 603 41 0 13907 0
vsize: 55792
[startup+170.002 s]
Raw data (loadavg): 0.95 0.46 0.17 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 14410 0 1 0 16953 36 0 0 25 0 1 0 406662240 60915712 14389 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14872 14389 603 41 0 14831 0
vsize: 59488
[startup+180.002 s]
Raw data (loadavg): 0.95 0.47 0.18 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 15340 0 1 0 17951 38 0 0 25 0 1 0 406662240 64700416 15319 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15796 15319 603 41 0 15755 0
vsize: 63184
[startup+190.002 s]
Raw data (loadavg): 0.96 0.49 0.19 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16203 0 1 0 18949 40 0 0 25 0 1 0 406662240 68395008 16182 4294967295 134512640 134672761 3221224544 3221223544 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16182 603 41 0 16657 0
vsize: 66792
[startup+200.002 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16203 0 1 0 19949 40 0 0 25 0 1 0 406662240 68395008 16182 4294967295 134512640 134672761 3221224544 3221223696 134565212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16182 603 41 0 16657 0
vsize: 66792
[startup+210.001 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16203 0 1 0 20949 40 0 0 25 0 1 0 406662240 68395008 16182 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16182 603 41 0 16657 0
vsize: 66792
[startup+220.001 s]
Raw data (loadavg): 0.98 0.54 0.21 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16203 0 1 0 21949 40 0 0 25 0 1 0 406662240 68395008 16182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16182 603 41 0 16657 0
vsize: 66792
[startup+230.001 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16203 0 1 0 22949 40 0 0 25 0 1 0 406662240 68395008 16182 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16182 603 41 0 16657 0
vsize: 66792
[startup+240.001 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16203 0 1 0 23949 40 0 0 25 0 1 0 406662240 68395008 16182 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16182 603 41 0 16657 0
vsize: 66792
[startup+250 s]
Raw data (loadavg): 0.98 0.58 0.23 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16203 0 1 0 24949 40 0 0 25 0 1 0 406662240 68395008 16182 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16182 603 41 0 16657 0
vsize: 66792
[startup+260 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16204 0 1 0 25949 40 0 0 25 0 1 0 406662240 68395008 16183 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16698 16183 603 41 0 16657 0
vsize: 66792
[startup+270 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16515 0 1 0 26949 41 0 0 25 0 1 0 406662240 69611520 16494 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16995 16494 603 41 0 16954 0
vsize: 67980
[startup+280 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16805 0 1 0 27948 41 0 0 25 0 1 0 406662240 70828032 16784 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17292 16784 603 41 0 17251 0
vsize: 69168
[startup+290 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16805 0 1 0 28949 41 0 0 25 0 1 0 406662240 70828032 16784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17292 16784 603 41 0 17251 0
vsize: 69168
[startup+300 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16806 0 1 0 29949 41 0 0 25 0 1 0 406662240 70828032 16785 4294967295 134512640 134672761 3221224544 3221223728 134559588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17292 16785 603 41 0 17251 0
vsize: 69168
[startup+310 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16806 0 1 0 30949 41 0 0 25 0 1 0 406662240 70828032 16785 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17292 16785 603 41 0 17251 0
vsize: 69168
[startup+320 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16806 0 1 0 31949 41 0 0 25 0 1 0 406662240 70828032 16785 4294967295 134512640 134672761 3221224544 3221223728 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17292 16785 603 41 0 17251 0
vsize: 69168
[startup+330.001 s]
Raw data (loadavg): 0.99 0.68 0.29 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16940 0 1 0 32949 42 0 0 25 0 1 0 406662240 71368704 16919 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17424 16919 603 41 0 17383 0
vsize: 69696
[startup+340 s]
Raw data (loadavg): 0.99 0.69 0.30 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16940 0 1 0 33949 42 0 0 25 0 1 0 406662240 71368704 16919 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17424 16919 603 41 0 17383 0
vsize: 69696
[startup+350.002 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16940 0 1 0 34948 42 0 0 25 0 1 0 406662240 71368704 16919 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17424 16919 603 41 0 17383 0
vsize: 69696
[startup+360.002 s]
Raw data (loadavg): 0.99 0.71 0.31 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16940 0 1 0 35948 42 0 0 25 0 1 0 406662240 71368704 16919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17424 16919 603 41 0 17383 0
vsize: 69696
[startup+370.002 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16940 0 1 0 36947 42 0 0 25 0 1 0 406662240 71368704 16919 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17424 16919 603 41 0 17383 0
vsize: 69696
[startup+380.002 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16940 0 1 0 37947 42 0 0 25 0 1 0 406662240 71368704 16919 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17424 16919 603 41 0 17383 0
vsize: 69696
[startup+390.001 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16940 0 1 0 38947 42 0 0 25 0 1 0 406662240 71368704 16919 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17424 16919 603 41 0 17383 0
vsize: 69696
[startup+400.002 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 16941 0 1 0 39948 42 0 0 25 0 1 0 406662240 71368704 16920 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17424 16920 603 41 0 17383 0
vsize: 69696
[startup+410.002 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 17679 0 1 0 40946 44 0 0 25 0 1 0 406662240 74342400 17658 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18150 17658 603 41 0 18109 0
vsize: 72600
[startup+420.002 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 18331 0 1 0 41944 46 0 0 25 0 1 0 406662240 77045760 18310 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 18310 603 41 0 18769 0
vsize: 75240
[startup+430.003 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19049 0 1 0 42942 48 0 0 25 0 1 0 406662240 80019456 19028 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19536 19028 603 41 0 19495 0
vsize: 78144
[startup+440.003 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19637 0 1 0 43941 49 0 0 25 0 1 0 406662240 82452480 19616 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20130 19616 603 41 0 20089 0
vsize: 80520
[startup+450.003 s]
Raw data (loadavg): 0.99 0.78 0.37 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19725 0 1 0 44941 50 0 0 25 0 1 0 406662240 82857984 19704 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19704 603 41 0 20188 0
vsize: 80916
[startup+460.003 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19726 0 1 0 45941 50 0 0 25 0 1 0 406662240 82857984 19705 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19705 603 41 0 20188 0
vsize: 80916
[startup+470.003 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19727 0 1 0 46941 50 0 0 25 0 1 0 406662240 82857984 19706 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19706 603 41 0 20188 0
vsize: 80916
[startup+480.003 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19727 0 1 0 47941 50 0 0 25 0 1 0 406662240 82857984 19706 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19706 603 41 0 20188 0
vsize: 80916
[startup+490.003 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19727 0 1 0 48942 50 0 0 25 0 1 0 406662240 82857984 19706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19706 603 41 0 20188 0
vsize: 80916
[startup+500.004 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19729 0 1 0 49942 50 0 0 25 0 1 0 406662240 82857984 19708 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19708 603 41 0 20188 0
vsize: 80916
[startup+510.004 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 50942 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+520.004 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 51942 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+530.005 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 52942 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+540.005 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 53942 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+550.005 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 54943 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+560.005 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 55943 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+570.004 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 56943 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+580.005 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 57943 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+590.005 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19730 0 1 0 58943 50 0 0 25 0 1 0 406662240 82857984 19709 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19709 603 41 0 20188 0
vsize: 80916
[startup+600.005 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19731 0 1 0 59943 50 0 0 25 0 1 0 406662240 82857984 19710 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19710 603 41 0 20188 0
vsize: 80916
[startup+610.005 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19731 0 1 0 60944 50 0 0 25 0 1 0 406662240 82857984 19710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19710 603 41 0 20188 0
vsize: 80916
[startup+620.005 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19731 0 1 0 61944 50 0 0 25 0 1 0 406662240 82857984 19710 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19710 603 41 0 20188 0
vsize: 80916
[startup+630.005 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19731 0 1 0 62944 50 0 0 25 0 1 0 406662240 82857984 19710 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19710 603 41 0 20188 0
vsize: 80916
[startup+640.005 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19731 0 1 0 63944 50 0 0 25 0 1 0 406662240 82857984 19710 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19710 603 41 0 20188 0
vsize: 80916
[startup+650.006 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19732 0 1 0 64944 50 0 0 25 0 1 0 406662240 82857984 19711 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19711 603 41 0 20188 0
vsize: 80916
[startup+660.006 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19732 0 1 0 65945 50 0 0 25 0 1 0 406662240 82857984 19711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19711 603 41 0 20188 0
vsize: 80916
[startup+670.006 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19813 0 1 0 66945 50 0 0 25 0 1 0 406662240 83136512 19792 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20297 19792 603 41 0 20256 0
vsize: 81188
[startup+680.007 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 19956 0 1 0 67945 50 0 0 25 0 1 0 406662240 83677184 19935 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20429 19935 603 41 0 20388 0
vsize: 81716
[startup+690.007 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 20078 0 1 0 68945 50 0 0 25 0 1 0 406662240 84217856 20057 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20561 20057 603 41 0 20520 0
vsize: 82244
[startup+700.007 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 20194 0 1 0 69945 50 0 0 25 0 1 0 406662240 84766720 20173 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20695 20173 603 41 0 20654 0
vsize: 82780
[startup+710.008 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 20377 0 1 0 70945 51 0 0 25 0 1 0 406662240 85463040 20356 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20865 20356 603 41 0 20824 0
vsize: 83460
[startup+720.007 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 20567 0 1 0 71944 52 0 0 25 0 1 0 406662240 86274048 20546 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21063 20546 603 41 0 21022 0
vsize: 84252
[startup+730.007 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 20792 0 1 0 72944 52 0 0 25 0 1 0 406662240 87220224 20771 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21294 20771 603 41 0 21253 0
vsize: 85176
[startup+740.008 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21008 0 1 0 73943 53 0 0 25 0 1 0 406662240 88068096 20987 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21501 20987 603 41 0 21460 0
vsize: 86004
[startup+750.009 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21238 0 1 0 74943 53 0 0 25 0 1 0 406662240 89153536 21217 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21766 21217 603 41 0 21725 0
vsize: 87064
[startup+760.009 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21397 0 1 0 75943 54 0 0 25 0 1 0 406662240 89694208 21376 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21898 21376 603 41 0 21857 0
vsize: 87592
[startup+770.009 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 76943 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+780.009 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 77943 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+790.009 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 78943 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+800.009 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 79943 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+810.009 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 80943 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+820.009 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 81944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+830.01 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 82944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+840.01 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 83944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+850.012 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 84944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+860.011 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 85945 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+870.011 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 86944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+880.012 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 87944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+890.012 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 88944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+900.012 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 89944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+910.012 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 90944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+920.012 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 91944 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+930.013 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 92945 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+940.013 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 93945 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+950.014 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21458 0 1 0 94945 54 0 0 25 0 1 0 406662240 89964544 21437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21964 21437 603 41 0 21923 0
vsize: 87856
[startup+960.014 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 21673 0 1 0 95945 55 0 0 25 0 1 0 406662240 91033600 21652 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21652 603 41 0 22184 0
vsize: 88900
[startup+970.014 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22260 0 1 0 96943 56 0 0 25 0 1 0 406662240 93462528 22239 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22818 22239 603 41 0 22777 0
vsize: 91272
[startup+980.015 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22459 0 1 0 97943 56 0 0 25 0 1 0 406662240 94273536 22438 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22438 603 41 0 22975 0
vsize: 92064
[startup+990.015 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22459 0 1 0 98944 56 0 0 25 0 1 0 406662240 94273536 22438 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22438 603 41 0 22975 0
vsize: 92064
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22459 0 1 0 99944 56 0 0 25 0 1 0 406662240 94273536 22438 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22438 603 41 0 22975 0
vsize: 92064
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22459 0 1 0 100944 56 0 0 25 0 1 0 406662240 94273536 22438 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22438 603 41 0 22975 0
vsize: 92064
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22459 0 1 0 101944 56 0 0 25 0 1 0 406662240 94273536 22438 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22438 603 41 0 22975 0
vsize: 92064
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22459 0 1 0 102944 56 0 0 25 0 1 0 406662240 94273536 22438 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22438 603 41 0 22975 0
vsize: 92064
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22459 0 1 0 103944 56 0 0 25 0 1 0 406662240 94273536 22438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22438 603 41 0 22975 0
vsize: 92064
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 104945 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 105945 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 106945 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 107945 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 108945 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 109946 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 110946 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 111946 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22461 0 1 0 112946 56 0 0 25 0 1 0 406662240 94273536 22440 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22440 603 41 0 22975 0
vsize: 92064
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22462 0 1 0 113946 56 0 0 25 0 1 0 406662240 94273536 22441 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22441 603 41 0 22975 0
vsize: 92064
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22462 0 1 0 114947 56 0 0 25 0 1 0 406662240 94273536 22441 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23016 22441 603 41 0 22975 0
vsize: 92064
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22462 0 1 0 115947 56 0 0 25 0 1 0 406662240 94162944 22437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22989 22437 603 41 0 22948 0
vsize: 91956
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22462 0 1 0 116947 56 0 0 25 0 1 0 406662240 94162944 22437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22989 22437 603 41 0 22948 0
vsize: 91956
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22462 0 1 0 117947 56 0 0 25 0 1 0 406662240 94162944 22437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22989 22437 603 41 0 22948 0
vsize: 91956
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22462 0 1 0 118948 56 0 0 25 0 1 0 406662240 94162944 22437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22989 22437 603 41 0 22948 0
vsize: 91956
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 28200
Raw data (stat): 28200 (minisat+) R 28199 26667 26666 0 -1 0 22462 0 1 0 119948 56 0 0 25 0 1 0 406662240 94162944 22437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22989 22437 603 41 0 22948 0
vsize: 91956
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 28200
Raw data (stat): 28200 (minisat+) Z 28199 26667 26666 0 -1 12 22464 0 1 0 119948 61 0 0 25 0 1 0 406662240 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.07
CPU time (s): 1200.09
CPU user time (s): 1199.48
CPU system time (s): 0.610907
CPU usage (%): 100.002
Max. virtual memory (Kb): 92064
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####