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-chnl40_50_pb.cnf.cr.opb
MD5SUM2cb05b3a6451c60276a625949666f14e
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 51
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.12498
Number of variables4000
Total number of constraints180
Number of constraints which are clauses100
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint40
Maximum length of a constraint50

Trace number 4605 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        747984 kB
Buffers:         37024 kB
Cached:         209476 kB
SwapCached:          0 kB
Active:          78812 kB
Inactive:       170536 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        747732 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            31748 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:46:19 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 3403 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................
c ---[  79]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  78]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  77]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  76]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  75]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  74]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  73]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  72]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  71]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  70]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  69]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  68]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  67]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  66]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  65]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  64]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  63]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  62]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  61]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  60]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  59]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  58]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  57]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  56]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  55]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  54]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  53]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  52]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  51]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  50]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  49]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  48]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  47]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  46]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  45]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  44]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  43]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  42]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  41]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  40]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  39]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  38]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  37]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  36]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  35]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  34]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  33]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  32]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  31]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  30]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  29]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  28]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  27]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  26]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  25]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  24]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  23]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  22]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  21]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  20]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  19]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  18]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  17]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  16]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  15]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  14]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  13]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  12]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  11]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[  10]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   9]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   8]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   7]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   6]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   5]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   4]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   3]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   2]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   1]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[   0]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   49780   180400 |   16593       0        0     nan |  0.000 % |
c |       100 |   48377   175609 |   18252       0        0     nan |  5.548 % |
c |       250 |   46400   168846 |   20077      12       37     3.1 |  9.469 % |
c |       477 |   46379   168777 |   22085     236     1111     4.7 |  9.495 % |
c |       814 |   46243   168315 |   24293     554     3036     5.5 |  9.700 % |
c |      1320 |   45867   167039 |   26723     996     4934     5.0 | 10.240 % |
c |      2081 |   44078   160907 |   29395    1501     7768     5.2 | 12.979 % |
c |      3220 |   40127   147363 |   32335    2001    11351     5.7 | 18.784 % |
c |      4928 |   35541   131617 |   35568    2990    19765     6.6 | 25.651 % |
c |      7490 |   27216   103188 |   39125    4218   149272    35.4 | 38.236 % |
c |     11336 |   24878    95224 |   43037    7701  1206017   156.6 | 41.918 % |
c |     17102 |   24349    93431 |   47341   13380  3136488   234.4 | 42.774 % |
c |     25751 |   24186    92896 |   52075   22007  8710205   395.8 | 43.065 % |
c |     38725 |   24081    92536 |   57283   34962 20595056   589.1 | 43.228 % |
c |     58186 |   24081    92536 |   63011   54423 35799615   657.8 | 43.228 % |
c |     87381 |   24067    92486 |   69313   28867 17082070   591.8 | 43.245 % |
#### 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 13138
Raw data (stat): 13138 (runsolver) R 13137 11931 11930 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 478456491 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 1388 0 1 0 984 4 0 0 25 0 1 0 478456491 7593984 1364 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1854 1364 603 41 0 1813 0
vsize: 7416
[startup+20.0015 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 1393 0 1 0 1984 4 0 0 25 0 1 0 478456491 7593984 1369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1854 1369 603 41 0 1813 0
vsize: 7416
[startup+30.0017 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 1398 0 1 0 2984 4 0 0 25 0 1 0 478456491 7593984 1374 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1854 1374 603 41 0 1813 0
vsize: 7416
[startup+40.0024 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 1474 0 1 0 3983 5 0 0 25 0 1 0 478456491 7995392 1450 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1952 1450 603 41 0 1911 0
vsize: 7808
[startup+50.0028 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 2642 0 1 0 4980 8 0 0 25 0 1 0 478456491 12726272 2618 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3107 2618 603 41 0 3066 0
vsize: 12428
[startup+60.004 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 4408 0 1 0 5977 11 0 0 25 0 1 0 478456491 20000768 4384 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4883 4384 603 41 0 4842 0
vsize: 19532
[startup+70.0048 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 5867 0 1 0 6974 15 0 0 25 0 1 0 478456491 26005504 5843 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6349 5843 603 41 0 6308 0
vsize: 25396
[startup+80.0052 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 8775 0 1 0 7968 20 0 0 25 0 1 0 478456491 37908480 8751 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9255 8751 603 41 0 9214 0
vsize: 37020
[startup+90.0053 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 10633 0 1 0 8966 23 0 0 25 0 1 0 478456491 45481984 10609 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11104 10609 603 41 0 11063 0
vsize: 44416
[startup+100.005 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 12724 0 1 0 9962 27 0 0 25 0 1 0 478456491 54099968 12700 4294967295 134512640 134672761 3221224544 3221223728 134559601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13208 12700 603 41 0 13167 0
vsize: 52832
[startup+110.006 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 14504 0 1 0 10958 30 0 0 25 0 1 0 478456491 61378560 14480 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14985 14480 603 41 0 14944 0
vsize: 59940
[startup+120.007 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 16474 0 1 0 11955 34 0 0 25 0 1 0 478456491 69496832 16450 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16967 16450 603 41 0 16926 0
vsize: 67868
[startup+130.006 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 18022 0 1 0 12950 39 0 0 25 0 1 0 478456491 75718656 17998 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18486 17998 603 41 0 18445 0
vsize: 73944
[startup+140.007 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 19627 0 1 0 13946 43 0 0 25 0 1 0 478456491 82305024 19603 4294967295 134512640 134672761 3221224544 3221223552 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20094 19603 603 41 0 20053 0
vsize: 80376
[startup+150.008 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 20885 0 1 0 14944 45 0 0 25 0 1 0 478456491 87687168 20861 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21408 20861 603 41 0 21367 0
vsize: 85632
[startup+160.009 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 21928 0 1 0 15941 49 0 0 25 0 1 0 478456491 91869184 21904 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22429 21904 603 41 0 22388 0
vsize: 89716
[startup+170.01 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 22689 0 1 0 16939 51 0 0 25 0 1 0 478456491 94986240 22665 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23190 22665 603 41 0 23149 0
vsize: 92760
[startup+180.009 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 23337 0 1 0 17938 52 0 0 25 0 1 0 478456491 97656832 23313 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23842 23313 603 41 0 23801 0
vsize: 95368
[startup+190.01 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 23954 0 1 0 18936 54 0 0 25 0 1 0 478456491 100216832 23930 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24467 23930 603 41 0 24426 0
vsize: 97868
[startup+200.01 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 24693 0 1 0 19934 56 0 0 25 0 1 0 478456491 103301120 24669 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 24669 603 41 0 25179 0
vsize: 100880
[startup+210.011 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 25350 0 1 0 20932 58 0 0 25 0 1 0 478456491 105963520 25326 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25870 25326 603 41 0 25829 0
vsize: 103480
[startup+220.012 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 26095 0 1 0 21931 60 0 0 25 0 1 0 478456491 109060096 26071 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26626 26071 603 41 0 26585 0
vsize: 106504
[startup+230.011 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 26695 0 1 0 22930 61 0 0 25 0 1 0 478456491 111435776 26671 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27206 26671 603 41 0 27165 0
vsize: 108824
[startup+240.012 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 27303 0 1 0 23929 62 0 0 25 0 1 0 478456491 113979392 27279 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27827 27279 603 41 0 27786 0
vsize: 111308
[startup+250.013 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 27903 0 1 0 24927 63 0 0 25 0 1 0 478456491 116396032 27879 4294967295 134512640 134672761 3221224544 3221223728 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28417 27879 603 41 0 28376 0
vsize: 113668
[startup+260.013 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 28897 0 1 0 25924 66 0 0 25 0 1 0 478456491 120549376 28873 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29431 28873 603 41 0 29390 0
vsize: 117724
[startup+270.014 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 30353 0 1 0 26921 70 0 0 25 0 1 0 478456491 126427136 30329 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30866 30329 603 41 0 30825 0
vsize: 123464
[startup+280.013 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 31250 0 1 0 27918 72 0 0 25 0 1 0 478456491 130142208 31226 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31773 31226 603 41 0 31732 0
vsize: 127092
[startup+290.014 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 31918 0 1 0 28918 73 0 0 25 0 1 0 478456491 132886528 31894 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32443 31894 603 41 0 32402 0
vsize: 129772
[startup+300.014 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 32605 0 1 0 29916 75 0 0 25 0 1 0 478456491 135720960 32581 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33135 32581 603 41 0 33094 0
vsize: 132540
[startup+310.015 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 33197 0 1 0 30914 77 0 0 25 0 1 0 478456491 138113024 33173 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33719 33173 603 41 0 33678 0
vsize: 134876
[startup+320.015 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 33846 0 1 0 31913 78 0 0 25 0 1 0 478456491 140853248 33822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34388 33822 603 41 0 34347 0
vsize: 137552
[startup+330.016 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 34356 0 1 0 32911 80 0 0 25 0 1 0 478456491 143007744 34332 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34914 34332 603 41 0 34873 0
vsize: 139656
[startup+340.017 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 34928 0 1 0 33910 81 0 0 25 0 1 0 478456491 145297408 34904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35473 34904 603 41 0 35432 0
vsize: 141892
[startup+350.017 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 35459 0 1 0 34909 83 0 0 25 0 1 0 478456491 147492864 35435 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36009 35435 603 41 0 35968 0
vsize: 144036
[startup+360.018 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 36003 0 1 0 35907 84 0 0 25 0 1 0 478456491 149782528 35979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36568 35979 603 41 0 36527 0
vsize: 146272
[startup+370.018 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 36766 0 1 0 36905 86 0 0 25 0 1 0 478456491 152997888 36742 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37353 36742 603 41 0 37312 0
vsize: 149412
[startup+380.018 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 37498 0 1 0 37903 89 0 0 25 0 1 0 478456491 155971584 37474 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38079 37474 603 41 0 38038 0
vsize: 152316
[startup+390.019 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 38093 0 1 0 38902 90 0 0 25 0 1 0 478456491 158400512 38069 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38672 38069 603 41 0 38631 0
vsize: 154688
[startup+400.02 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 38673 0 1 0 39899 93 0 0 25 0 1 0 478456491 160825344 38649 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39264 38649 603 41 0 39223 0
vsize: 157056
[startup+410.02 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 39327 0 1 0 40898 94 0 0 25 0 1 0 478456491 163553280 39303 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39930 39303 603 41 0 39889 0
vsize: 159720
[startup+420.02 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 39674 0 1 0 41896 96 0 0 25 0 1 0 478456491 164913152 39650 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40262 39650 603 41 0 40221 0
vsize: 161048
[startup+430.021 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 40145 0 1 0 42896 97 0 0 25 0 1 0 478456491 166891520 40121 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40745 40121 603 41 0 40704 0
vsize: 162980
[startup+440.022 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 40632 0 1 0 43895 98 0 0 25 0 1 0 478456491 168927232 40608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41242 40608 603 41 0 41201 0
vsize: 164968
[startup+450.021 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 41145 0 1 0 44894 98 0 0 25 0 1 0 478456491 170954752 41121 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41737 41121 603 41 0 41696 0
vsize: 166948
[startup+460.021 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 41516 0 1 0 45893 99 0 0 25 0 1 0 478456491 172580864 41492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42134 41492 603 41 0 42093 0
vsize: 168536
[startup+470.022 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 41984 0 1 0 46893 100 0 0 25 0 1 0 478456491 174497792 41960 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42602 41960 603 41 0 42561 0
vsize: 170408
[startup+480.022 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 42407 0 1 0 47891 102 0 0 25 0 1 0 478456491 176214016 42383 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43021 42383 603 41 0 42980 0
vsize: 172084
[startup+490.023 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 42755 0 1 0 48891 103 0 0 25 0 1 0 478456491 177561600 42731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43350 42731 603 41 0 43309 0
vsize: 173400
[startup+500.023 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 43142 0 1 0 49889 105 0 0 25 0 1 0 478456491 179175424 43118 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43744 43118 603 41 0 43703 0
vsize: 174976
[startup+510.023 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 43570 0 1 0 50888 106 0 0 25 0 1 0 478456491 180940800 43546 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44175 43546 603 41 0 44134 0
vsize: 176700
[startup+520.023 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 44070 0 1 0 51887 107 0 0 25 0 1 0 478456491 183083008 44046 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44698 44046 603 41 0 44657 0
vsize: 178792
[startup+530.023 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 44601 0 1 0 52886 108 0 0 25 0 1 0 478456491 185245696 44577 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45226 44577 603 41 0 45185 0
vsize: 180904
[startup+540.024 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 45214 0 1 0 53885 109 0 0 25 0 1 0 478456491 187928576 45190 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45881 45190 603 41 0 45840 0
vsize: 183524
[startup+550.023 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 45712 0 1 0 54884 110 0 0 25 0 1 0 478456491 190140416 45688 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46421 45688 603 41 0 46380 0
vsize: 185684
[startup+560.023 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 46007 0 1 0 55884 111 0 0 25 0 1 0 478456491 191356928 45983 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46718 45983 603 41 0 46677 0
vsize: 186872
[startup+570.024 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 46551 0 1 0 56883 112 0 0 25 0 1 0 478456491 193503232 46527 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47242 46527 603 41 0 47201 0
vsize: 188968
[startup+580.024 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 46895 0 1 0 57881 114 0 0 25 0 1 0 478456491 194973696 46871 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47601 46871 603 41 0 47560 0
vsize: 190404
[startup+590.025 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47277 0 1 0 58881 115 0 0 25 0 1 0 478456491 196460544 47253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47964 47253 603 41 0 47923 0
vsize: 191856
[startup+600.025 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47592 0 1 0 59880 115 0 0 25 0 1 0 478456491 197804032 47568 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48292 47568 603 41 0 48251 0
vsize: 193168
[startup+610.025 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47934 0 1 0 60879 116 0 0 25 0 1 0 478456491 199151616 47910 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47910 603 41 0 48580 0
vsize: 194484
[startup+620.025 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47934 0 1 0 61879 116 0 0 25 0 1 0 478456491 199151616 47910 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47910 603 41 0 48580 0
vsize: 194484
[startup+630.025 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47935 0 1 0 62879 116 0 0 25 0 1 0 478456491 199151616 47911 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47911 603 41 0 48580 0
vsize: 194484
[startup+640.025 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47935 0 1 0 63880 116 0 0 25 0 1 0 478456491 199151616 47911 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47911 603 41 0 48580 0
vsize: 194484
[startup+650.025 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47942 0 1 0 64880 116 0 0 25 0 1 0 478456491 199151616 47918 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47918 603 41 0 48580 0
vsize: 194484
[startup+660.025 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47945 0 1 0 65880 116 0 0 25 0 1 0 478456491 199151616 47921 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47921 603 41 0 48580 0
vsize: 194484
[startup+670.026 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47953 0 1 0 66880 116 0 0 25 0 1 0 478456491 199151616 47929 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47929 603 41 0 48580 0
vsize: 194484
[startup+680.025 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 67880 116 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+690.025 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 68880 116 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+700.026 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 69881 116 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+710.026 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 70880 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+720.027 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 71881 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+730.027 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 72881 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+740.027 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 73881 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+750.027 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 74881 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+760.027 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 75881 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+770.028 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 76882 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+780.027 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 77882 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+790.028 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 78882 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+800.029 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 79882 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+810.029 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 80882 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+820.029 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 81882 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+830.029 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 82883 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+840.029 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 83883 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+850.029 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 84883 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+860.029 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 85883 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+870.029 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 86883 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+880.029 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 87884 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+890.03 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 88884 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+900.031 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 89884 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+910.03 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 90884 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+920.03 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 91884 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+930.03 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 92884 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+940.031 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 47959 0 1 0 93885 117 0 0 25 0 1 0 478456491 199151616 47935 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48621 47935 603 41 0 48580 0
vsize: 194484
[startup+950.031 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 48444 0 1 0 94883 118 0 0 25 0 1 0 478456491 201191424 48420 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49119 48420 603 41 0 49078 0
vsize: 196476
[startup+960.032 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 48902 0 1 0 95882 120 0 0 25 0 1 0 478456491 203120640 48878 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49590 48878 603 41 0 49549 0
vsize: 198360
[startup+970.032 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 49720 0 1 0 96880 122 0 0 25 0 1 0 478456491 206512128 49696 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50418 49696 603 41 0 50377 0
vsize: 201672
[startup+980.032 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 50293 0 1 0 97879 124 0 0 25 0 1 0 478456491 208826368 50269 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50983 50269 603 41 0 50942 0
vsize: 203932
[startup+990.033 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 50576 0 1 0 98878 124 0 0 25 0 1 0 478456491 210042880 50552 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51280 50552 603 41 0 51239 0
vsize: 205120
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 51170 0 1 0 99877 125 0 0 25 0 1 0 478456491 212484096 51146 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51876 51146 603 41 0 51835 0
vsize: 207504
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 52004 0 1 0 100875 127 0 0 25 0 1 0 478456491 215863296 51980 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52701 51980 603 41 0 52660 0
vsize: 210804
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 52430 0 1 0 101875 128 0 0 25 0 1 0 478456491 217624576 52406 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53131 52406 603 41 0 53090 0
vsize: 212524
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 52880 0 1 0 102874 129 0 0 25 0 1 0 478456491 219521024 52856 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53594 52856 603 41 0 53553 0
vsize: 214376
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 53260 0 1 0 103873 130 0 0 25 0 1 0 478456491 221007872 53236 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53957 53236 603 41 0 53916 0
vsize: 215828
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 53794 0 1 0 104873 131 0 0 25 0 1 0 478456491 223170560 53770 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54485 53770 603 41 0 54444 0
vsize: 217940
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 54388 0 1 0 105871 133 0 0 25 0 1 0 478456491 225607680 54364 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55080 54364 603 41 0 55039 0
vsize: 220320
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 54788 0 1 0 106870 134 0 0 25 0 1 0 478456491 227364864 54764 4294967295 134512640 134672761 3221224544 3221223648 134555133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55509 54764 603 41 0 55468 0
vsize: 222036
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 55276 0 1 0 107869 135 0 0 25 0 1 0 478456491 229269504 55252 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55974 55252 603 41 0 55933 0
vsize: 223896
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 55763 0 1 0 108868 137 0 0 25 0 1 0 478456491 231309312 55739 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56472 55739 603 41 0 56431 0
vsize: 225888
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 56245 0 1 0 109866 138 0 0 25 0 1 0 478456491 233332736 56221 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56966 56222 603 41 0 56925 0
vsize: 227864
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 56806 0 1 0 110866 139 0 0 25 0 1 0 478456491 235634688 56782 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57528 56782 603 41 0 57487 0
vsize: 230112
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 57472 0 1 0 111864 140 0 0 25 0 1 0 478456491 238354432 57448 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58192 57448 603 41 0 58151 0
vsize: 232768
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 58096 0 1 0 112863 142 0 0 25 0 1 0 478456491 240934912 58072 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58822 58072 603 41 0 58781 0
vsize: 235288
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 58797 0 1 0 113862 143 0 0 25 0 1 0 478456491 243781632 58773 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59517 58773 603 41 0 59476 0
vsize: 238068
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 59390 0 1 0 114861 145 0 0 25 0 1 0 478456491 246235136 59366 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60116 59366 603 41 0 60075 0
vsize: 240464
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 59974 0 1 0 115860 146 0 0 25 0 1 0 478456491 248541184 59950 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60679 59950 603 41 0 60638 0
vsize: 242716
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 60491 0 1 0 116859 147 0 0 25 0 1 0 478456491 250736640 60467 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61215 60467 603 41 0 61174 0
vsize: 244860
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 61030 0 1 0 117857 148 0 0 25 0 1 0 478456491 252960768 61006 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61758 61006 603 41 0 61717 0
vsize: 247032
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 61278 0 1 0 118857 149 0 0 25 0 1 0 478456491 253906944 61254 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61989 61254 603 41 0 61948 0
vsize: 247956
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 13138
Raw data (stat): 13138 (minisat+) R 13137 11931 11930 0 -1 0 61755 0 1 0 119856 150 0 0 25 0 1 0 478456491 255934464 61731 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62484 61731 603 41 0 62443 0
vsize: 249936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 13138
Raw data (stat): 13138 (minisat+) Z 13137 11931 11930 0 -1 12 61757 0 1 0 119856 162 0 0 25 0 1 0 478456491 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.15
CPU time (s): 1200.19
CPU user time (s): 1198.57
CPU system time (s): 1.62275
CPU usage (%): 100.003
Max. virtual memory (Kb): 249936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####