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-chnl50_60_pb.cnf.cr.opb
MD5SUM6968a43b42bba7df68b13fdfd3b616a1
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 61
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.187971
Number of variables6000
Total number of constraints220
Number of constraints which are clauses120
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint60

Trace number 5773 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 01:41:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4158 boxname=wulflinc12 idbench=22 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6968a43b42bba7df68b13fdfd3b616a1  /oldhome/oroussel/tmp/wulflinc12/normalized-chnl50_60_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc12/normalized-chnl50_60_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc12/normalized-chnl50_60_pb.cnf.cr.opb
IDLAUNCH: 4158
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        907452 kB
Buffers:         35760 kB
Cached:          72004 kB
SwapCached:         16 kB
Active:          61444 kB
Inactive:        49224 kB
HighTotal:      131008 kB
HighFree:        55020 kB
LowTotal:       903652 kB
LowFree:        852432 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10888 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:01:38 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 4158 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 220 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................
c ---[  99]---> BDD-cost:  117
c ---[  98]---> BDD-cost:  117
c ---[  97]---> BDD-cost:  117
c ---[  96]---> BDD-cost:  117
c ---[  95]---> BDD-cost:  117
c ---[  94]---> BDD-cost:  117
c ---[  93]---> BDD-cost:  117
c ---[  92]---> BDD-cost:  117
c ---[  91]---> BDD-cost:  117
c ---[  90]---> BDD-cost:  117
c ---[  89]---> BDD-cost:  117
c ---[  88]---> BDD-cost:  117
c ---[  87]---> BDD-cost:  117
c ---[  86]---> BDD-cost:  117
c ---[  85]---> BDD-cost:  117
c ---[  84]---> BDD-cost:  117
c ---[  83]---> BDD-cost:  117
c ---[  82]---> BDD-cost:  117
c ---[  81]---> BDD-cost:  117
c ---[  80]---> BDD-cost:  117
c ---[  79]---> BDD-cost:  117
c ---[  78]---> BDD-cost:  117
c ---[  77]---> BDD-cost:  117
c ---[  76]---> BDD-cost:  117
c ---[  75]---> BDD-cost:  117
c ---[  74]---> BDD-cost:  117
c ---[  73]---> BDD-cost:  117
c ---[  72]---> BDD-cost:  117
c ---[  71]---> BDD-cost:  117
c ---[  70]---> BDD-cost:  117
c ---[  69]---> BDD-cost:  117
c ---[  68]---> BDD-cost:  117
c ---[  67]---> BDD-cost:  117
c ---[  66]---> BDD-cost:  117
c ---[  65]---> BDD-cost:  117
c ---[  64]---> BDD-cost:  117
c ---[  63]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  117
c ---[  61]---> BDD-cost:  117
c ---[  60]---> BDD-cost:  117
c ---[  59]---> BDD-cost:  117
c ---[  58]---> BDD-cost:  117
c ---[  57]---> BDD-cost:  117
c ---[  56]---> BDD-cost:  117
c ---[  55]---> BDD-cost:  117
c ---[  54]---> BDD-cost:  117
c ---[  53]---> BDD-cost:  117
c ---[  52]---> BDD-cost:  117
c ---[  51]---> BDD-cost:  117
c ---[  50]---> BDD-cost:  117
c ---[  49]---> BDD-cost:  117
c ---[  48]---> BDD-cost:  117
c ---[  47]---> BDD-cost:  117
c ---[  46]---> BDD-cost:  117
c ---[  45]---> BDD-cost:  117
c ---[  44]---> BDD-cost:  117
c ---[  43]---> BDD-cost:  117
c ---[  42]---> BDD-cost:  117
c ---[  41]---> BDD-cost:  117
c ---[  40]---> BDD-cost:  117
c ---[  39]---> BDD-cost:  117
c ---[  38]---> BDD-cost:  117
c ---[  37]---> BDD-cost:  117
c ---[  36]---> BDD-cost:  117
c ---[  35]---> BDD-cost:  117
c ---[  34]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  117
c ---[  32]---> BDD-cost:  117
c ---[  31]---> BDD-cost:  117
c ---[  30]---> BDD-cost:  117
c ---[  29]---> BDD-cost:  117
c ---[  28]---> BDD-cost:  117
c ---[  27]---> BDD-cost:  117
c ---[  26]---> BDD-cost:  117
c ---[  25]---> BDD-cost:  117
c ---[  24]---> BDD-cost:  117
c ---[  23]---> BDD-cost:  117
c ---[  22]---> BDD-cost:  117
c ---[  21]---> BDD-cost:  117
c ---[  20]---> BDD-cost:  117
c ---[  19]---> BDD-cost:  117
c ---[  18]---> BDD-cost:  117
c ---[  17]---> BDD-cost:  117
c ---[  16]---> BDD-cost:  117
c ---[  15]---> BDD-cost:  117
c ---[  14]---> BDD-cost:  117
c ---[  13]---> BDD-cost:  117
c ---[  12]---> BDD-cost:  117
c ---[  11]---> BDD-cost:  117
c ---[  10]---> BDD-cost:  117
c ---[   9]---> BDD-cost:  117
c ---[   8]---> BDD-cost:  117
c ---[   7]---> BDD-cost:  117
c ---[   6]---> BDD-cost:  117
c ---[   5]---> BDD-cost:  117
c ---[   4]---> BDD-cost:  117
c ---[   3]---> BDD-cost:  117
c ---[   2]---> BDD-cost:  117
c ---[   1]---> BDD-cost:  117
c ---[   0]---> BDD-cost:  117
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29220    81700 |    9740       0        0     nan |  0.000 % |
c |       104 |   29220    81700 |   10714     104    19328   185.8 |  0.565 % |
c |       256 |   29220    81700 |   11785     256    51373   200.7 |  0.565 % |
c |       482 |   29220    81700 |   12963     482   102298   212.2 |  0.565 % |
c |       824 |   29220    81700 |   14260     824   174285   211.5 |  0.565 % |
c |      1330 |   29220    81700 |   15686    1330   314613   236.6 |  0.565 % |
c |      2091 |   29220    81700 |   17255    2091   547467   261.8 |  0.565 % |
c |      3231 |   29220    81700 |   18980    3231   973163   301.2 |  0.565 % |
c |      4940 |   29220    81700 |   20878    4940  1825691   369.6 |  0.565 % |
c |      7502 |   29220    81700 |   22966    7502  3300948   440.0 |  0.565 % |
c |     11349 |   29220    81700 |   25263   11349  4927293   434.2 |  0.565 % |
c |     17116 |   29220    81700 |   27789   17116  7830885   457.5 |  0.565 % |
c |     25776 |   29220    81700 |   30568   25776 12693138   492.4 |  0.565 % |
c |     38750 |   29220    81700 |   33625   12745  7008530   549.9 |  0.565 % |
c |     58211 |   29220    81700 |   36987   32206 21026723   652.9 |  0.565 % |
c |     87408 |   29220    81700 |   40686   27744 13222109   476.6 |  0.565 % |
c |    131200 |   29220    81700 |   44755   36115 20717915   573.7 |  0.565 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 30200
Raw data (stat): 30200 (runsolver) R 30199 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422486914 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99986 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 3633 0 0 0 987 10 0 0 25 0 1 0 422486914 16920576 3552 4294967295 134512640 134672761 3221224528 3221223652 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4131 3552 603 41 0 4090 0
vsize: 16524
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 5381 0 0 0 1983 14 0 0 25 0 1 0 422486914 24072192 5300 4294967295 134512640 134672761 3221224528 3221223632 134555225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5877 5300 603 41 0 5836 0
vsize: 23508
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 6868 0 0 0 2980 17 0 0 25 0 1 0 422486914 30298112 6787 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7397 6787 603 41 0 7356 0
vsize: 29588
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 8417 0 0 0 3976 20 0 0 25 0 1 0 422486914 36626432 8336 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8942 8336 603 41 0 8901 0
vsize: 35768
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 9923 0 0 0 4972 25 0 0 25 0 1 0 422486914 42803200 9842 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10450 9842 603 41 0 10409 0
vsize: 41800
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 11252 0 0 0 5969 28 0 0 25 0 1 0 422486914 48201728 11171 4294967295 134512640 134672761 3221224528 3221223624 1075347383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11768 11171 603 41 0 11727 0
vsize: 47072
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 12748 0 0 0 6965 32 0 0 25 0 1 0 422486914 54276096 12667 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13251 12667 603 41 0 13210 0
vsize: 53004
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 13960 0 0 0 7962 35 0 0 25 0 1 0 422486914 59285504 13879 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14474 13879 603 41 0 14433 0
vsize: 57896
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 15259 0 0 0 8959 39 0 0 25 0 1 0 422486914 64679936 15178 4294967295 134512640 134672761 3221224528 3221223544 1075353077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15791 15178 603 41 0 15750 0
vsize: 63164
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 16789 0 0 0 9956 42 0 0 25 0 1 0 422486914 70897664 16708 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17309 16708 603 41 0 17268 0
vsize: 69236
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 18206 0 0 0 10953 45 0 0 25 0 1 0 422486914 76697600 18125 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18725 18125 603 41 0 18684 0
vsize: 74900
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 19351 0 0 0 11950 48 0 0 25 0 1 0 422486914 81420288 19270 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19878 19270 603 41 0 19837 0
vsize: 79512
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 20194 0 0 0 12948 51 0 0 25 0 1 0 422486914 84930560 20113 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20735 20113 603 41 0 20694 0
vsize: 82940
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 20928 0 0 0 13946 52 0 0 25 0 1 0 422486914 87904256 20847 4294967295 134512640 134672761 3221224528 3221223632 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21461 20847 603 41 0 21420 0
vsize: 85844
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21615 0 0 0 14944 55 0 0 25 0 1 0 422486914 90738688 21534 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22153 21534 603 41 0 22112 0
vsize: 88612
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21899 0 0 0 15943 56 0 0 25 0 1 0 422486914 91947008 21818 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21818 603 41 0 22407 0
vsize: 89792
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 16943 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 17942 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 18942 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 19942 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 20942 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223632 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+220.007 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 21942 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+230.007 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 22942 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223696 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+240.007 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 23943 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223632 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+250.008 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 24943 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223712 134558843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+260.008 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 21900 0 0 0 25943 56 0 0 25 0 1 0 422486914 91947008 21819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21819 603 41 0 22407 0
vsize: 89792
[startup+270.009 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 22734 0 0 0 26940 60 0 0 25 0 1 0 422486914 95309824 22653 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23269 22653 603 41 0 23228 0
vsize: 93076
[startup+280.008 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 23667 0 0 0 27938 62 0 0 25 0 1 0 422486914 99184640 23586 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24215 23586 603 41 0 24174 0
vsize: 96860
[startup+290.008 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 25028 0 0 0 28935 65 0 0 25 0 1 0 422486914 104878080 24947 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25605 24947 603 41 0 25564 0
vsize: 102420
[startup+300.008 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 26156 0 0 0 29933 67 0 0 25 0 1 0 422486914 109461504 26075 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26724 26075 603 41 0 26683 0
vsize: 106896
[startup+310.008 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 27005 0 0 0 30931 69 0 0 25 0 1 0 422486914 112971776 26924 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27581 26924 603 41 0 27540 0
vsize: 110324
[startup+320.009 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 27809 0 0 0 31929 71 0 0 25 0 1 0 422486914 116207616 27728 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 27728 603 41 0 28330 0
vsize: 113484
[startup+330.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 28617 0 0 0 32928 73 0 0 25 0 1 0 422486914 119623680 28536 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29205 28536 603 41 0 29164 0
vsize: 116820
[startup+340.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 29343 0 0 0 33926 75 0 0 25 0 1 0 422486914 122634240 29262 4294967295 134512640 134672761 3221224528 3221223632 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29940 29262 603 41 0 29899 0
vsize: 119760
[startup+350.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30175 0 0 0 34925 76 0 0 25 0 1 0 422486914 126009344 30094 4294967295 134512640 134672761 3221224528 3221223632 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30094 603 41 0 30723 0
vsize: 123056
[startup+360.009 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30177 0 0 0 35925 76 0 0 25 0 1 0 422486914 126009344 30096 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30096 603 41 0 30723 0
vsize: 123056
[startup+370.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30178 0 0 0 36926 76 0 0 25 0 1 0 422486914 126009344 30097 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30097 603 41 0 30723 0
vsize: 123056
[startup+380.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30179 0 0 0 37926 76 0 0 25 0 1 0 422486914 126009344 30098 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30098 603 41 0 30723 0
vsize: 123056
[startup+390.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30179 0 0 0 38926 76 0 0 25 0 1 0 422486914 126009344 30098 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30098 603 41 0 30723 0
vsize: 123056
[startup+400.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30180 0 0 0 39926 76 0 0 25 0 1 0 422486914 126009344 30099 4294967295 134512640 134672761 3221224528 3221223632 134555214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30099 603 41 0 30723 0
vsize: 123056
[startup+410.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30181 0 0 0 40926 76 0 0 25 0 1 0 422486914 126009344 30100 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30100 603 41 0 30723 0
vsize: 123056
[startup+420.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30181 0 0 0 41927 76 0 0 25 0 1 0 422486914 126009344 30100 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30100 603 41 0 30723 0
vsize: 123056
[startup+430.012 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 42927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+440.012 s]
Raw data (loadavg): 1.14 1.03 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 43927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+450.013 s]
Raw data (loadavg): 1.12 1.03 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 44927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+460.012 s]
Raw data (loadavg): 1.10 1.03 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 45927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+470.013 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 46927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+480.013 s]
Raw data (loadavg): 1.07 1.03 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 47927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+490.013 s]
Raw data (loadavg): 1.06 1.03 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 48927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+500.014 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 49927 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+510.014 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 50928 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+520.014 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 51928 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+530.014 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 52928 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223632 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+540.014 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30182 0 0 0 53928 76 0 0 25 0 1 0 422486914 126009344 30101 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 30101 603 41 0 30723 0
vsize: 123056
[startup+550.015 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 54928 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+560.015 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 55928 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+570.016 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 56929 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+580.015 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 57929 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+590.015 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 58929 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+600.015 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 59929 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+610.016 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 60929 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+620.017 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 61930 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+630.018 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 62930 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+640.018 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 63930 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+650.017 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 64930 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+660.017 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 65930 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+670.017 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 66930 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+680.017 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 67931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+690.017 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 68931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+700.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 69931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+710.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 70931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+720.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 71931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+730.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 72931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+740.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 73931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 74931 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223696 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+760.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30184 0 0 0 75932 76 0 0 25 0 1 0 422486914 125927424 30103 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30744 30103 603 41 0 30703 0
vsize: 122976
[startup+770.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 30596 0 0 0 76931 77 0 0 25 0 1 0 422486914 127680512 30515 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31172 30515 603 41 0 31131 0
vsize: 124688
[startup+780.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 31368 0 0 0 77929 80 0 0 25 0 1 0 422486914 130785280 31287 4294967295 134512640 134672761 3221224528 3221223440 1075352290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31930 31287 603 41 0 31889 0
vsize: 127720
[startup+790.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32035 0 0 0 78927 82 0 0 25 0 1 0 422486914 133500928 31954 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32593 31954 603 41 0 32552 0
vsize: 130372
[startup+800.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 79926 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+810.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 80926 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+820.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 81926 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+830.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 82926 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+840.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 83927 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+850.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 84927 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+860.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 85927 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+870.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 86927 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+880.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 87927 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+890.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 88927 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+900.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 89928 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+910.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 90928 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 91928 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+930.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 92928 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+940.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 93928 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+950.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 94928 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+960.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 95929 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+970.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 96929 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+980.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 97929 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+990.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32695 0 0 0 98929 83 0 0 25 0 1 0 422486914 136200192 32614 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32614 603 41 0 33211 0
vsize: 133008
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 99929 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 100929 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 101930 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 102930 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 103930 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 104930 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 105930 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 106931 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 107931 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 108931 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30200
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 109931 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 3/57 30235
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 110931 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1120.02 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 30253
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 111931 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1130.02 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 30253
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 112931 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1140.02 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 30253
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 113932 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1150.02 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 30253
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 114932 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1160.02 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 30253
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32696 0 0 0 115932 83 0 0 25 0 1 0 422486914 136200192 32615 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32615 603 41 0 33211 0
vsize: 133008
[startup+1170.02 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 30253
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32697 0 0 0 116932 83 0 0 25 0 1 0 422486914 136200192 32616 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32616 603 41 0 33211 0
vsize: 133008
[startup+1180.02 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 30253
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32697 0 0 0 117932 83 0 0 25 0 1 0 422486914 136200192 32616 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32616 603 41 0 33211 0
vsize: 133008
[startup+1190.02 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 30255
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32698 0 0 0 118933 83 0 0 25 0 1 0 422486914 136200192 32617 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32617 603 41 0 33211 0
vsize: 133008
[startup+1200.02 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 30255
Raw data (stat): 30200 (minisat+) R 30199 25285 25284 0 -1 0 32698 0 0 0 119933 83 0 0 25 0 1 0 422486914 136200192 32617 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33252 32617 603 41 0 33211 0
vsize: 133008
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.02 1.01 0.94 1/54 30255
Raw data (stat): 30200 (minisat+) Z 30199 25285 25284 0 -1 12 32700 0 0 0 119933 89 0 0 25 0 1 0 422486914 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.09
CPU time (s): 1200.23
CPU user time (s): 1199.33
CPU system time (s): 0.892864
CPU usage (%): 100.012
Max. virtual memory (Kb): 133008
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####