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-chnl15_16_pb.cnf.cr.opb
MD5SUM3f8902c4e8af50006f671e2bddb3e9aa
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 17
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.013997
Number of variables480
Total number of constraints62
Number of constraints which are clauses32
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint16

Trace number 4575 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        919524 kB
Buffers:         36552 kB
Cached:          59736 kB
SwapCached:          0 kB
Active:          71728 kB
Inactive:        27388 kB
HighTotal:      131008 kB
HighFree:        67368 kB
LowTotal:       903652 kB
LowFree:        852156 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10400 kB
Committed_AS:    63468 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:42:47 (client local time) WITH STATUS 0 IN 1200.07 SECONDS
stats: 3389 7 1200.07 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 62 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................
c ---[  29]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  28]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  27]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  26]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  25]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  24]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  23]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  22]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  21]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  20]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  19]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  18]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  17]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  16]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  15]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  14]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  13]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  12]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  11]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  10]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   9]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   8]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   7]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   6]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   5]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   4]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   3]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   2]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   1]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[   0]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5522    19530 |    1840       0        0     nan |  0.000 % |
c |       100 |    5522    19530 |    2024     100      428     4.3 |  8.000 % |
c |       251 |    5435    19244 |    2226     232     1002     4.3 |  8.800 % |
c |       476 |    5246    18617 |    2449     411     2262     5.5 | 10.800 % |
c |       813 |    4951    17638 |    2693     689     5071     7.4 | 14.200 % |
c |      1319 |    4740    16933 |    2963    1108    41529    37.5 | 16.600 % |
c |      2079 |    4740    16933 |    3259    1868   126580    67.8 | 16.600 % |
c |      3218 |    4714    16843 |    3585    2996   271165    90.5 | 16.867 % |
c |      4926 |    4714    16843 |    3944    2633   303511   115.3 | 16.867 % |
c |      7488 |    4698    16791 |    4338    2951   364080   123.4 | 17.067 % |
c |     11334 |    4698    16791 |    4772    4346   582670   134.1 | 17.067 % |
c |     17101 |    4698    16791 |    5249    4803   640839   133.4 | 17.067 % |
c |     25752 |    4698    16791 |    5774    4798   595069   124.0 | 17.067 % |
c |     38727 |    4685    16747 |    6352    5159   670367   129.9 | 17.200 % |
c |     58189 |    4685    16747 |    6987    3906   506841   129.8 | 17.200 % |
c |     87387 |    4679    16727 |    7686    6647   845476   127.2 | 17.267 % |
c |    131176 |    4679    16727 |    8454    5161   568064   110.1 | 17.267 % |
c |    196863 |    4664    16676 |    9300    7798   943887   121.0 | 17.400 % |
c |    295389 |    4589    16428 |   10230    7949   934938   117.6 | 18.267 % |
c |    443180 |    4589    16428 |   11253   10600  1287678   121.5 | 18.267 % |
c |    664863 |    4582    16404 |   12378    7940   848139   106.8 | 18.333 % |
#### 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.00 0.00 0.00 2/54 24756
Raw data (stat): 24756 (runsolver) R 24755 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420220838 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99918 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1225 0 1 0 983 3 0 0 25 0 1 0 420220838 6598656 1204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1611 1204 603 41 0 1570 0
vsize: 6444
[startup+19.9998 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1352 0 1 0 1983 4 0 0 25 0 1 0 420220838 7139328 1331 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1331 603 41 0 1702 0
vsize: 6972
[startup+29.9998 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1425 0 1 0 2982 4 0 0 25 0 1 0 420220838 7409664 1404 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1809 1404 603 41 0 1768 0
vsize: 7236
[startup+40 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1572 0 1 0 3982 4 0 0 25 0 1 0 420220838 7950336 1551 4294967295 134512640 134672761 3221224544 3221223728 134559342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1941 1551 603 41 0 1900 0
vsize: 7764
[startup+49.9997 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1689 0 1 0 4981 5 0 0 25 0 1 0 420220838 8491008 1668 4294967295 134512640 134672761 3221224544 3221223728 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1668 603 41 0 2032 0
vsize: 8292
[startup+59.9993 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1716 0 1 0 5981 5 0 0 25 0 1 0 420220838 8626176 1695 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1695 603 41 0 2065 0
vsize: 8424
[startup+69.9999 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1846 0 1 0 6981 5 0 0 25 0 1 0 420220838 9170944 1825 4294967295 134512640 134672761 3221224544 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2239 1825 603 41 0 2198 0
vsize: 8956
[startup+79.9996 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1906 0 1 0 7981 6 0 0 25 0 1 0 420220838 9453568 1885 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1885 603 41 0 2267 0
vsize: 9232
[startup+89.9995 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1914 0 1 0 8981 6 0 0 25 0 1 0 420220838 9453568 1893 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1893 603 41 0 2267 0
vsize: 9232
[startup+99.9988 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1927 0 1 0 9981 6 0 0 25 0 1 0 420220838 9453568 1906 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1906 603 41 0 2267 0
vsize: 9232
[startup+109.998 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1967 0 1 0 10981 6 0 0 25 0 1 0 420220838 9723904 1946 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2374 1946 603 41 0 2333 0
vsize: 9496
[startup+119.999 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 1999 0 1 0 11981 6 0 0 25 0 1 0 420220838 9867264 1978 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2409 1978 603 41 0 2368 0
vsize: 9636
[startup+129.999 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2002 0 1 0 12981 6 0 0 25 0 1 0 420220838 9867264 1981 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2409 1981 603 41 0 2368 0
vsize: 9636
[startup+139.998 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2011 0 1 0 13981 6 0 0 25 0 1 0 420220838 9867264 1990 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2409 1990 603 41 0 2368 0
vsize: 9636
[startup+149.998 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2011 0 1 0 14981 6 0 0 25 0 1 0 420220838 9867264 1990 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2409 1990 603 41 0 2368 0
vsize: 9636
[startup+159.998 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2059 0 1 0 15981 6 0 0 25 0 1 0 420220838 10137600 2038 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2038 603 41 0 2434 0
vsize: 9900
[startup+169.997 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2153 0 1 0 16981 7 0 0 25 0 1 0 420220838 10543104 2132 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2574 2132 603 41 0 2533 0
vsize: 10296
[startup+179.997 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2170 0 1 0 17981 7 0 0 25 0 1 0 420220838 10543104 2149 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2574 2149 603 41 0 2533 0
vsize: 10296
[startup+189.997 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2208 0 1 0 18982 7 0 0 25 0 1 0 420220838 10678272 2187 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2607 2187 603 41 0 2566 0
vsize: 10428
[startup+199.997 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2210 0 1 0 19982 7 0 0 25 0 1 0 420220838 10678272 2189 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2607 2189 603 41 0 2566 0
vsize: 10428
[startup+209.997 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2249 0 1 0 20982 7 0 0 25 0 1 0 420220838 10969088 2228 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2678 2228 603 41 0 2637 0
vsize: 10712
[startup+219.997 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2363 0 1 0 21982 7 0 0 25 0 1 0 420220838 11374592 2342 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2777 2342 603 41 0 2736 0
vsize: 11108
[startup+229.997 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2458 0 1 0 22982 8 0 0 25 0 1 0 420220838 11796480 2437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2880 2437 603 41 0 2839 0
vsize: 11520
[startup+239.997 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2475 0 1 0 23982 8 0 0 25 0 1 0 420220838 11939840 2454 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2454 603 41 0 2874 0
vsize: 11660
[startup+249.996 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2475 0 1 0 24982 8 0 0 25 0 1 0 420220838 11939840 2454 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2454 603 41 0 2874 0
vsize: 11660
[startup+259.996 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2488 0 1 0 25982 8 0 0 25 0 1 0 420220838 11939840 2467 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2467 603 41 0 2874 0
vsize: 11660
[startup+269.996 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2493 0 1 0 26982 8 0 0 25 0 1 0 420220838 11939840 2472 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2472 603 41 0 2874 0
vsize: 11660
[startup+279.995 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2493 0 1 0 27982 8 0 0 25 0 1 0 420220838 11939840 2472 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2472 603 41 0 2874 0
vsize: 11660
[startup+289.996 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2493 0 1 0 28982 8 0 0 25 0 1 0 420220838 11939840 2472 4294967295 134512640 134672761 3221224544 3221223728 134559599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2472 603 41 0 2874 0
vsize: 11660
[startup+299.995 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2493 0 1 0 29982 8 0 0 25 0 1 0 420220838 11939840 2472 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2472 603 41 0 2874 0
vsize: 11660
[startup+309.995 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2494 0 1 0 30983 8 0 0 25 0 1 0 420220838 11939840 2473 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2915 2473 603 41 0 2874 0
vsize: 11660
[startup+319.995 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2526 0 1 0 31983 8 0 0 25 0 1 0 420220838 12099584 2505 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2954 2505 603 41 0 2913 0
vsize: 11816
[startup+329.995 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2589 0 1 0 32982 8 0 0 25 0 1 0 420220838 12386304 2568 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3024 2568 603 41 0 2983 0
vsize: 12096
[startup+339.995 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2617 0 1 0 33982 8 0 0 25 0 1 0 420220838 12546048 2596 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2596 603 41 0 3022 0
vsize: 12252
[startup+349.995 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2642 0 1 0 34982 9 0 0 25 0 1 0 420220838 12681216 2621 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3096 2621 603 41 0 3055 0
vsize: 12384
[startup+359.994 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2671 0 1 0 35982 9 0 0 25 0 1 0 420220838 12816384 2650 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2650 603 41 0 3088 0
vsize: 12516
[startup+369.994 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2671 0 1 0 36982 9 0 0 25 0 1 0 420220838 12816384 2650 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2650 603 41 0 3088 0
vsize: 12516
[startup+379.993 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2677 0 1 0 37983 9 0 0 25 0 1 0 420220838 12816384 2656 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2656 603 41 0 3088 0
vsize: 12516
[startup+389.993 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2677 0 1 0 38983 9 0 0 25 0 1 0 420220838 12816384 2656 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2656 603 41 0 3088 0
vsize: 12516
[startup+399.994 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2677 0 1 0 39983 9 0 0 25 0 1 0 420220838 12816384 2656 4294967295 134512640 134672761 3221224544 3221223728 134559604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2656 603 41 0 3088 0
vsize: 12516
[startup+409.993 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2677 0 1 0 40983 9 0 0 25 0 1 0 420220838 12816384 2656 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2656 603 41 0 3088 0
vsize: 12516
[startup+419.993 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2683 0 1 0 41983 9 0 0 25 0 1 0 420220838 12816384 2662 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2662 603 41 0 3088 0
vsize: 12516
[startup+429.993 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2688 0 1 0 42983 9 0 0 25 0 1 0 420220838 12816384 2667 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3129 2667 603 41 0 3088 0
vsize: 12516
[startup+439.992 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2694 0 1 0 43984 9 0 0 25 0 1 0 420220838 12963840 2673 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3165 2673 603 41 0 3124 0
vsize: 12660
[startup+449.992 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2694 0 1 0 44984 9 0 0 25 0 1 0 420220838 12963840 2673 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3165 2673 603 41 0 3124 0
vsize: 12660
[startup+459.991 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2706 0 1 0 45984 9 0 0 25 0 1 0 420220838 12963840 2685 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3165 2685 603 41 0 3124 0
vsize: 12660
[startup+469.992 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2859 0 1 0 46983 9 0 0 25 0 1 0 420220838 13639680 2838 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3330 2838 603 41 0 3289 0
vsize: 13320
[startup+479.992 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2953 0 1 0 47983 10 0 0 25 0 1 0 420220838 14045184 2932 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2932 603 41 0 3388 0
vsize: 13716
[startup+489.991 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 2967 0 1 0 48983 10 0 0 25 0 1 0 420220838 14045184 2946 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2946 603 41 0 3388 0
vsize: 13716
[startup+499.992 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3009 0 1 0 49983 10 0 0 25 0 1 0 420220838 14319616 2988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2988 603 41 0 3455 0
vsize: 13984
[startup+509.992 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3017 0 1 0 50983 10 0 0 25 0 1 0 420220838 14319616 2996 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2996 603 41 0 3455 0
vsize: 13984
[startup+519.992 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3017 0 1 0 51983 10 0 0 25 0 1 0 420220838 14319616 2996 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2996 603 41 0 3455 0
vsize: 13984
[startup+529.992 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3017 0 1 0 52984 10 0 0 25 0 1 0 420220838 14319616 2996 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2996 603 41 0 3455 0
vsize: 13984
[startup+539.993 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3017 0 1 0 53984 10 0 0 25 0 1 0 420220838 14319616 2996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2996 603 41 0 3455 0
vsize: 13984
[startup+549.992 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3017 0 1 0 54984 10 0 0 25 0 1 0 420220838 14319616 2996 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2996 603 41 0 3455 0
vsize: 13984
[startup+559.992 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3017 0 1 0 55984 10 0 0 25 0 1 0 420220838 14319616 2996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2996 603 41 0 3455 0
vsize: 13984
[startup+569.993 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3019 0 1 0 56984 10 0 0 25 0 1 0 420220838 14319616 2998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2998 603 41 0 3455 0
vsize: 13984
[startup+579.993 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3020 0 1 0 57985 10 0 0 25 0 1 0 420220838 14319616 2999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2999 603 41 0 3455 0
vsize: 13984
[startup+589.993 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3034 0 1 0 58985 10 0 0 25 0 1 0 420220838 14319616 3013 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 3013 603 41 0 3455 0
vsize: 13984
[startup+599.993 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3080 0 1 0 59985 10 0 0 25 0 1 0 420220838 14483456 3059 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3059 603 41 0 3495 0
vsize: 14144
[startup+609.992 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3096 0 1 0 60985 10 0 0 25 0 1 0 420220838 14626816 3075 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3571 3075 603 41 0 3530 0
vsize: 14284
[startup+619.992 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3097 0 1 0 61985 10 0 0 25 0 1 0 420220838 14626816 3076 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3571 3076 603 41 0 3530 0
vsize: 14284
[startup+629.992 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3205 0 1 0 62985 11 0 0 25 0 1 0 420220838 15032320 3184 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3184 603 41 0 3629 0
vsize: 14680
[startup+639.992 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3206 0 1 0 63985 11 0 0 25 0 1 0 420220838 15032320 3185 4294967295 134512640 134672761 3221224544 3221223648 134554673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3185 603 41 0 3629 0
vsize: 14680
[startup+649.991 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3207 0 1 0 64985 11 0 0 25 0 1 0 420220838 15032320 3186 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3186 603 41 0 3629 0
vsize: 14680
[startup+659.991 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3207 0 1 0 65985 11 0 0 25 0 1 0 420220838 15032320 3186 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3186 603 41 0 3629 0
vsize: 14680
[startup+669.992 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3210 0 1 0 66985 11 0 0 25 0 1 0 420220838 15032320 3189 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3189 603 41 0 3629 0
vsize: 14680
[startup+679.991 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3212 0 1 0 67986 11 0 0 25 0 1 0 420220838 15032320 3191 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3191 603 41 0 3629 0
vsize: 14680
[startup+689.992 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3213 0 1 0 68986 11 0 0 25 0 1 0 420220838 15032320 3192 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3192 603 41 0 3629 0
vsize: 14680
[startup+699.992 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3213 0 1 0 69986 11 0 0 25 0 1 0 420220838 15032320 3192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3192 603 41 0 3629 0
vsize: 14680
[startup+709.991 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3213 0 1 0 70986 11 0 0 25 0 1 0 420220838 15032320 3192 4294967295 134512640 134672761 3221224544 3221223728 134558764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3192 603 41 0 3629 0
vsize: 14680
[startup+719.991 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3213 0 1 0 71986 11 0 0 25 0 1 0 420220838 15032320 3192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3192 603 41 0 3629 0
vsize: 14680
[startup+729.99 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3218 0 1 0 72986 11 0 0 25 0 1 0 420220838 15167488 3197 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3197 603 41 0 3662 0
vsize: 14812
[startup+739.99 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3218 0 1 0 73986 11 0 0 25 0 1 0 420220838 15167488 3197 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3703 3197 603 41 0 3662 0
vsize: 14812
[startup+749.992 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3247 0 1 0 74986 11 0 0 25 0 1 0 420220838 15306752 3226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3737 3226 603 41 0 3696 0
vsize: 14948
[startup+759.991 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3252 0 1 0 75985 11 0 0 25 0 1 0 420220838 15306752 3231 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3737 3231 603 41 0 3696 0
vsize: 14948
[startup+769.991 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3350 0 1 0 76985 12 0 0 25 0 1 0 420220838 15728640 3329 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3840 3329 603 41 0 3799 0
vsize: 15360
[startup+779.991 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3385 0 1 0 77985 12 0 0 25 0 1 0 420220838 15863808 3364 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3873 3364 603 41 0 3832 0
vsize: 15492
[startup+789.991 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3394 0 1 0 78985 12 0 0 25 0 1 0 420220838 15863808 3373 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3873 3373 603 41 0 3832 0
vsize: 15492
[startup+799.991 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3414 0 1 0 79985 12 0 0 25 0 1 0 420220838 16011264 3393 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3909 3393 603 41 0 3868 0
vsize: 15636
[startup+809.991 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3431 0 1 0 80985 12 0 0 25 0 1 0 420220838 16171008 3410 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3948 3410 603 41 0 3907 0
vsize: 15792
[startup+819.991 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3431 0 1 0 81986 12 0 0 25 0 1 0 420220838 16171008 3410 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3948 3410 603 41 0 3907 0
vsize: 15792
[startup+829.991 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3431 0 1 0 82986 12 0 0 25 0 1 0 420220838 16171008 3410 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3948 3410 603 41 0 3907 0
vsize: 15792
[startup+839.991 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3433 0 1 0 83986 12 0 0 25 0 1 0 420220838 16171008 3412 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3948 3412 603 41 0 3907 0
vsize: 15792
[startup+849.991 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3433 0 1 0 84986 12 0 0 25 0 1 0 420220838 16171008 3412 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3948 3412 603 41 0 3907 0
vsize: 15792
[startup+859.991 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3477 0 1 0 85986 12 0 0 25 0 1 0 420220838 16322560 3456 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3456 603 41 0 3944 0
vsize: 15940
[startup+869.991 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3488 0 1 0 86986 12 0 0 25 0 1 0 420220838 16322560 3467 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3467 603 41 0 3944 0
vsize: 15940
[startup+879.991 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3488 0 1 0 87986 12 0 0 25 0 1 0 420220838 16322560 3467 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3467 603 41 0 3944 0
vsize: 15940
[startup+889.992 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3490 0 1 0 88987 12 0 0 25 0 1 0 420220838 16322560 3469 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3469 603 41 0 3944 0
vsize: 15940
[startup+899.991 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3490 0 1 0 89987 12 0 0 25 0 1 0 420220838 16322560 3469 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3469 603 41 0 3944 0
vsize: 15940
[startup+909.991 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3490 0 1 0 90987 12 0 0 25 0 1 0 420220838 16322560 3469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3469 603 41 0 3944 0
vsize: 15940
[startup+919.991 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3502 0 1 0 91987 12 0 0 25 0 1 0 420220838 16486400 3481 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3481 603 41 0 3984 0
vsize: 16100
[startup+929.992 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3503 0 1 0 92987 12 0 0 25 0 1 0 420220838 16486400 3482 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3482 603 41 0 3984 0
vsize: 16100
[startup+939.992 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3503 0 1 0 93988 12 0 0 25 0 1 0 420220838 16486400 3482 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3482 603 41 0 3984 0
vsize: 16100
[startup+949.991 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3518 0 1 0 94988 12 0 0 25 0 1 0 420220838 16486400 3497 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3497 603 41 0 3984 0
vsize: 16100
[startup+959.991 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3518 0 1 0 95988 12 0 0 25 0 1 0 420220838 16486400 3497 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3497 603 41 0 3984 0
vsize: 16100
[startup+969.992 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3527 0 1 0 96988 12 0 0 25 0 1 0 420220838 16486400 3506 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3506 603 41 0 3984 0
vsize: 16100
[startup+979.991 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3527 0 1 0 97988 12 0 0 25 0 1 0 420220838 16486400 3506 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3506 603 41 0 3984 0
vsize: 16100
[startup+989.992 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3528 0 1 0 98988 12 0 0 25 0 1 0 420220838 16486400 3507 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3507 603 41 0 3984 0
vsize: 16100
[startup+999.992 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3528 0 1 0 99989 12 0 0 25 0 1 0 420220838 16486400 3507 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3507 603 41 0 3984 0
vsize: 16100
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3530 0 1 0 100989 12 0 0 25 0 1 0 420220838 16486400 3509 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3509 603 41 0 3984 0
vsize: 16100
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3530 0 1 0 101989 12 0 0 25 0 1 0 420220838 16486400 3509 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3509 603 41 0 3984 0
vsize: 16100
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3530 0 1 0 102989 12 0 0 25 0 1 0 420220838 16486400 3509 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3509 603 41 0 3984 0
vsize: 16100
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3530 0 1 0 103989 12 0 0 25 0 1 0 420220838 16486400 3509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3509 603 41 0 3984 0
vsize: 16100
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3530 0 1 0 104990 12 0 0 25 0 1 0 420220838 16486400 3509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3509 603 41 0 3984 0
vsize: 16100
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3540 0 1 0 105990 12 0 0 25 0 1 0 420220838 16650240 3519 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3519 603 41 0 4024 0
vsize: 16260
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3540 0 1 0 106990 12 0 0 25 0 1 0 420220838 16650240 3519 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3519 603 41 0 4024 0
vsize: 16260
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3540 0 1 0 107990 12 0 0 25 0 1 0 420220838 16650240 3519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3519 603 41 0 4024 0
vsize: 16260
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3542 0 1 0 108990 12 0 0 25 0 1 0 420220838 16650240 3521 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3521 603 41 0 4024 0
vsize: 16260
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3542 0 1 0 109990 12 0 0 25 0 1 0 420220838 16650240 3521 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3521 603 41 0 4024 0
vsize: 16260
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3542 0 1 0 110991 12 0 0 25 0 1 0 420220838 16650240 3521 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3521 603 41 0 4024 0
vsize: 16260
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3542 0 1 0 111991 12 0 0 25 0 1 0 420220838 16650240 3521 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3521 603 41 0 4024 0
vsize: 16260
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3542 0 1 0 112991 12 0 0 25 0 1 0 420220838 16650240 3521 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3521 603 41 0 4024 0
vsize: 16260
[startup+1140 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3542 0 1 0 113991 12 0 0 25 0 1 0 420220838 16650240 3521 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3521 603 41 0 4024 0
vsize: 16260
[startup+1150 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3544 0 1 0 114992 12 0 0 25 0 1 0 420220838 16650240 3523 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3523 603 41 0 4024 0
vsize: 16260
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3544 0 1 0 115992 12 0 0 25 0 1 0 420220838 16650240 3523 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3523 603 41 0 4024 0
vsize: 16260
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3544 0 1 0 116992 12 0 0 25 0 1 0 420220838 16650240 3523 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3523 603 41 0 4024 0
vsize: 16260
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3551 0 1 0 117992 13 0 0 25 0 1 0 420220838 16650240 3530 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3530 603 41 0 4024 0
vsize: 16260
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3552 0 1 0 118992 13 0 0 25 0 1 0 420220838 16650240 3531 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3531 603 41 0 4024 0
vsize: 16260
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 24756
Raw data (stat): 24756 (minisat+) R 24755 22932 22931 0 -1 0 3565 0 1 0 119992 13 0 0 25 0 1 0 420220838 16650240 3544 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3544 603 41 0 4024 0
vsize: 16260
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 24756
Raw data (stat): 24756 (minisat+) Z 24755 22932 22931 0 -1 12 3567 0 1 0 119992 13 0 0 25 0 1 0 420220838 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.01
CPU time (s): 1200.07
CPU user time (s): 1199.93
CPU system time (s): 0.138978
CPU usage (%): 100.005
Max. virtual memory (Kb): 16260
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####