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 5714 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-14 01:38:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4151 boxname=wulflinc1 idbench=15 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  85d4e2fa5fd7a61a85d3ecb1e311bddb  /oldhome/oroussel/tmp/wulflinc1/normalized-chnl35_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-chnl35_40_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc1/normalized-chnl35_40_pb.cnf.cr.opb
IDLAUNCH: 4151
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        851208 kB
Buffers:         40912 kB
Cached:         118344 kB
SwapCached:          0 kB
Active:         110612 kB
Inactive:        51792 kB
HighTotal:      131008 kB
HighFree:        19964 kB
LowTotal:       903652 kB
LowFree:        831244 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15360 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:58:14 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 4151 7 1200.21 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): 0.91 0.95 0.90 2/56 19147
Raw data (stat): 19147 (runsolver) R 19146 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 365614815 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 2866 0 0 0 993 6 0 0 25 0 1 0 365614815 13611008 2840 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3323 2840 603 41 0 3282 0
vsize: 13292
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 4151 0 0 0 1989 9 0 0 25 0 1 0 365614815 18894848 4125 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4613 4125 603 41 0 4572 0
vsize: 18452
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 4288 0 0 0 2989 9 0 0 25 0 1 0 365614815 19435520 4262 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4745 4262 603 41 0 4704 0
vsize: 18980
[startup+40.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 5371 0 0 0 3987 11 0 0 25 0 1 0 365614815 23941120 5345 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5845 5345 603 41 0 5804 0
vsize: 23380
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 5413 0 0 0 4987 12 0 0 25 0 1 0 365614815 24076288 5387 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5878 5387 603 41 0 5837 0
vsize: 23512
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 6056 0 0 0 5985 14 0 0 25 0 1 0 365614815 26890240 6030 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6565 6030 603 41 0 6524 0
vsize: 26260
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 6231 0 0 0 6985 14 0 0 25 0 1 0 365614815 27570176 6205 4294967295 134512640 134672761 3221224544 3221223696 134541817 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.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 6231 0 0 0 7984 14 0 0 25 0 1 0 365614815 27570176 6205 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6731 6205 603 41 0 6690 0
vsize: 26924
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 6729 0 0 0 8984 15 0 0 25 0 1 0 365614815 29614080 6703 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7230 6703 603 41 0 7189 0
vsize: 28920
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7095 0 0 0 9982 17 0 0 25 0 1 0 365614815 31100928 7069 4294967295 134512640 134672761 3221224544 3221223648 134560160 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): 0.98 0.96 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7234 0 0 0 10982 18 0 0 25 0 1 0 365614815 31653888 7208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7728 7208 603 41 0 7687 0
vsize: 30912
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7880 0 0 0 11980 20 0 0 25 0 1 0 365614815 34349056 7854 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7854 603 41 0 8345 0
vsize: 33544
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7880 0 0 0 12980 20 0 0 25 0 1 0 365614815 34349056 7854 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7854 603 41 0 8345 0
vsize: 33544
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7881 0 0 0 13980 20 0 0 25 0 1 0 365614815 34349056 7855 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7855 603 41 0 8345 0
vsize: 33544
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7881 0 0 0 14980 20 0 0 25 0 1 0 365614815 34349056 7855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7855 603 41 0 8345 0
vsize: 33544
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7881 0 0 0 15980 20 0 0 25 0 1 0 365614815 34349056 7855 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7855 603 41 0 8345 0
vsize: 33544
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7881 0 0 0 16980 20 0 0 25 0 1 0 365614815 34349056 7855 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7855 603 41 0 8345 0
vsize: 33544
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19147
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 7882 0 0 0 17980 21 0 0 25 0 1 0 365614815 34349056 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7856 603 41 0 8345 0
vsize: 33544
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 8276 0 0 0 18978 22 0 0 25 0 1 0 365614815 35971072 8250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8782 8250 603 41 0 8741 0
vsize: 35128
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 8690 0 0 0 19977 23 0 0 25 0 1 0 365614815 37588992 8664 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9177 8664 603 41 0 9136 0
vsize: 36708
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 8690 0 0 0 20977 23 0 0 25 0 1 0 365614815 37588992 8664 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9177 8664 603 41 0 9136 0
vsize: 36708
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 8703 0 0 0 21977 24 0 0 25 0 1 0 365614815 37785600 8677 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9225 8677 603 41 0 9184 0
vsize: 36900
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 8717 0 0 0 22977 24 0 0 25 0 1 0 365614815 37785600 8691 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9225 8691 603 41 0 9184 0
vsize: 36900
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9012 0 0 0 23976 25 0 0 25 0 1 0 365614815 39002112 8986 4294967295 134512640 134672761 3221224544 3221223728 134558880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9522 8986 603 41 0 9481 0
vsize: 38088
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9012 0 0 0 24976 25 0 0 25 0 1 0 365614815 39002112 8986 4294967295 134512640 134672761 3221224544 3221223648 134560128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9522 8986 603 41 0 9481 0
vsize: 38088
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9012 0 0 0 25976 25 0 0 25 0 1 0 365614815 39002112 8986 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9522 8986 603 41 0 9481 0
vsize: 38088
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9384 0 0 0 26976 26 0 0 25 0 1 0 365614815 40624128 9358 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9358 603 41 0 9877 0
vsize: 39672
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9384 0 0 0 27976 26 0 0 25 0 1 0 365614815 40624128 9358 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9358 603 41 0 9877 0
vsize: 39672
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9384 0 0 0 28976 26 0 0 25 0 1 0 365614815 40624128 9358 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9358 603 41 0 9877 0
vsize: 39672
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9404 0 0 0 29976 26 0 0 25 0 1 0 365614815 40624128 9378 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9918 9378 603 41 0 9877 0
vsize: 39672
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9416 0 0 0 30976 26 0 0 25 0 1 0 365614815 40820736 9390 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9966 9390 603 41 0 9925 0
vsize: 39864
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9620 0 0 0 31975 27 0 0 25 0 1 0 365614815 41631744 9594 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9594 603 41 0 10123 0
vsize: 40656
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9620 0 0 0 32975 27 0 0 25 0 1 0 365614815 41631744 9594 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9594 603 41 0 10123 0
vsize: 40656
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9629 0 0 0 33975 28 0 0 25 0 1 0 365614815 41631744 9603 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9603 603 41 0 10123 0
vsize: 40656
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9629 0 0 0 34975 28 0 0 25 0 1 0 365614815 41631744 9603 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9603 603 41 0 10123 0
vsize: 40656
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9629 0 0 0 35976 28 0 0 25 0 1 0 365614815 41631744 9603 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9603 603 41 0 10123 0
vsize: 40656
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9638 0 0 0 36975 28 0 0 25 0 1 0 365614815 41803776 9612 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10206 9612 603 41 0 10165 0
vsize: 40824
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9638 0 0 0 37976 28 0 0 25 0 1 0 365614815 41803776 9612 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10206 9612 603 41 0 10165 0
vsize: 40824
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 9721 0 0 0 38975 29 0 0 25 0 1 0 365614815 42082304 9695 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10274 9695 603 41 0 10233 0
vsize: 41096
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 10638 0 0 0 39973 31 0 0 25 0 1 0 365614815 45883392 10612 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11202 10612 603 41 0 11161 0
vsize: 44808
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 10638 0 0 0 40973 31 0 0 25 0 1 0 365614815 45883392 10612 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11202 10612 603 41 0 11161 0
vsize: 44808
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 10723 0 0 0 41973 31 0 0 25 0 1 0 365614815 46153728 10697 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11268 10697 603 41 0 11227 0
vsize: 45072
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11061 0 0 0 42972 32 0 0 25 0 1 0 365614815 47636480 11035 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11630 11035 603 41 0 11589 0
vsize: 46520
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11061 0 0 0 43972 32 0 0 25 0 1 0 365614815 47636480 11035 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11630 11035 603 41 0 11589 0
vsize: 46520
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11061 0 0 0 44972 32 0 0 25 0 1 0 365614815 47636480 11035 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11630 11035 603 41 0 11589 0
vsize: 46520
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11061 0 0 0 45972 33 0 0 25 0 1 0 365614815 47636480 11035 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11630 11035 603 41 0 11589 0
vsize: 46520
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11061 0 0 0 46972 33 0 0 25 0 1 0 365614815 47636480 11035 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11630 11035 603 41 0 11589 0
vsize: 46520
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19149
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11341 0 0 0 47971 34 0 0 25 0 1 0 365614815 48717824 11315 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11894 11315 603 41 0 11853 0
vsize: 47576
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11341 0 0 0 48971 35 0 0 25 0 1 0 365614815 48717824 11315 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11894 11315 603 41 0 11853 0
vsize: 47576
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11341 0 0 0 49971 35 0 0 25 0 1 0 365614815 48717824 11315 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11894 11315 603 41 0 11853 0
vsize: 47576
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11341 0 0 0 50971 35 0 0 25 0 1 0 365614815 48717824 11315 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11894 11315 603 41 0 11853 0
vsize: 47576
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 51969 36 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 52969 36 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 53969 37 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 54970 37 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 55970 37 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 56970 37 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 57970 37 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223728 134558673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 58969 37 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 59969 38 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 60969 38 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 61969 38 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 62969 38 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 63970 38 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 64970 38 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 65970 39 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 11816 0 0 0 66970 39 0 0 25 0 1 0 365614815 50606080 11790 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12355 11790 603 41 0 12314 0
vsize: 49420
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12199 0 0 0 67969 40 0 0 25 0 1 0 365614815 52248576 12173 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12756 12173 603 41 0 12715 0
vsize: 51024
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12287 0 0 0 68968 40 0 0 25 0 1 0 365614815 52654080 12261 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12855 12261 603 41 0 12814 0
vsize: 51420
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12287 0 0 0 69969 40 0 0 25 0 1 0 365614815 52654080 12261 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12855 12261 603 41 0 12814 0
vsize: 51420
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12299 0 0 0 70969 40 0 0 25 0 1 0 365614815 52654080 12273 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12855 12273 603 41 0 12814 0
vsize: 51420
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12311 0 0 0 71969 41 0 0 25 0 1 0 365614815 52834304 12285 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12899 12285 603 41 0 12858 0
vsize: 51596
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12339 0 0 0 72969 41 0 0 25 0 1 0 365614815 52834304 12313 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12899 12313 603 41 0 12858 0
vsize: 51596
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12340 0 0 0 73969 41 0 0 25 0 1 0 365614815 52834304 12314 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12899 12314 603 41 0 12858 0
vsize: 51596
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12484 0 0 0 74969 41 0 0 25 0 1 0 365614815 53571584 12458 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13079 12458 603 41 0 13038 0
vsize: 52316
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 75968 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 76968 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19151
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 77968 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 78968 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 79969 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 80969 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 81969 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 12967 0 0 0 82969 42 0 0 25 0 1 0 365614815 55463936 12941 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12941 603 41 0 13500 0
vsize: 54164
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13287 0 0 0 83969 42 0 0 25 0 1 0 365614815 56815616 13261 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13871 13261 603 41 0 13830 0
vsize: 55484
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13287 0 0 0 84969 42 0 0 25 0 1 0 365614815 56815616 13261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13871 13261 603 41 0 13830 0
vsize: 55484
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13287 0 0 0 85969 42 0 0 25 0 1 0 365614815 56815616 13261 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13871 13261 603 41 0 13830 0
vsize: 55484
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13287 0 0 0 86969 42 0 0 25 0 1 0 365614815 56815616 13261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13871 13261 603 41 0 13830 0
vsize: 55484
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13287 0 0 0 87969 42 0 0 25 0 1 0 365614815 56815616 13261 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13871 13261 603 41 0 13830 0
vsize: 55484
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13287 0 0 0 88969 42 0 0 25 0 1 0 365614815 56815616 13261 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13871 13261 603 41 0 13830 0
vsize: 55484
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13299 0 0 0 89970 42 0 0 25 0 1 0 365614815 56954880 13273 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13905 13273 603 41 0 13864 0
vsize: 55620
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13590 0 0 0 90969 44 0 0 25 0 1 0 365614815 58032128 13564 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14168 13564 603 41 0 14127 0
vsize: 56672
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13590 0 0 0 91969 44 0 0 25 0 1 0 365614815 58032128 13564 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14168 13564 603 41 0 14127 0
vsize: 56672
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13590 0 0 0 92969 44 0 0 25 0 1 0 365614815 58032128 13564 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14168 13564 603 41 0 14127 0
vsize: 56672
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13590 0 0 0 93969 44 0 0 25 0 1 0 365614815 58032128 13564 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14168 13564 603 41 0 14127 0
vsize: 56672
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13590 0 0 0 94969 44 0 0 25 0 1 0 365614815 58032128 13564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14168 13564 603 41 0 14127 0
vsize: 56672
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13590 0 0 0 95970 44 0 0 25 0 1 0 365614815 58032128 13564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14168 13564 603 41 0 14127 0
vsize: 56672
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 13720 0 0 0 96969 44 0 0 25 0 1 0 365614815 58748928 13694 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14343 13694 603 41 0 14302 0
vsize: 57372
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14186 0 0 0 97969 45 0 0 25 0 1 0 365614815 60633088 14160 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14803 14160 603 41 0 14762 0
vsize: 59212
[startup+990.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14197 0 0 0 98969 45 0 0 25 0 1 0 365614815 60633088 14171 4294967295 134512640 134672761 3221224544 3221223500 1075350763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14803 14171 603 41 0 14762 0
vsize: 59212
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14198 0 0 0 99969 45 0 0 25 0 1 0 365614815 60633088 14172 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14803 14172 603 41 0 14762 0
vsize: 59212
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14210 0 0 0 100969 45 0 0 25 0 1 0 365614815 60780544 14184 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14839 14184 603 41 0 14798 0
vsize: 59356
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 101969 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 102970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 103970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223728 134558903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 104970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 105970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 106970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19153
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 107970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 108970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 109970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14211 0 0 0 110970 45 0 0 25 0 1 0 365614815 60780544 14185 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14839 14185 603 41 0 14798 0
vsize: 59356
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 14852 0 0 0 111968 47 0 0 25 0 1 0 365614815 63336448 14826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15463 14826 603 41 0 15422 0
vsize: 61852
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 112967 48 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 113967 48 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 114967 49 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 115967 49 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223728 134559079 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 116968 49 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 117968 49 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 118968 49 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 19155
Raw data (stat): 19147 (minisat+) R 19146 12452 12451 0 -1 0 15473 0 0 0 119968 49 0 0 25 0 1 0 365614815 65892352 15447 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16087 15447 603 41 0 16046 0
vsize: 64348
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 19155
Raw data (stat): 19147 (minisat+) Z 19146 12452 12451 0 -1 12 15475 0 0 0 119968 51 0 0 25 0 1 0 365614815 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.05
CPU time (s): 1200.21
CPU user time (s): 1199.69
CPU system time (s): 0.51992
CPU usage (%): 100.013
Max. virtual memory (Kb): 64348
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####