PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:100.opb
MD5SUM	f82b685b64af240616b701a750c82883
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10
Optimality of the best value was proved	NO
Number of terms in the objective function	934
Biggest coefficient in the objective function	546
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2594
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	546
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2594
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	934
Total number of constraints	1996
Number of constraints which are clauses	879
Number of constraints which are cardinality constraints (but not clauses)	1117
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 31740

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-05-27 05:57:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23121 boxname=wulflinc6 idbench=367 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f82b685b64af240616b701a750c82883  /oldhome/oroussel/tmp/wulflinc6/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc6/normalized-10:20:4.5:0.95:100.opb
IDLAUNCH: 23121
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        733172 kB
Buffers:         33360 kB
Cached:         243804 kB
SwapCached:        412 kB
Active:          53748 kB
Inactive:       225700 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        732920 kB
SwapTotal:     2097136 kB
SwapFree:      2096036 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            16332 kB
Committed_AS:    63724 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 06:18:27 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 23121 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1062 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   20
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   17
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   17
c ---[ 176]---> BDD-cost:   17
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:    5
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   21
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   38
c ---[ 164]---> BDD-cost:   29
c ---[ 163]---> BDD-cost:   29
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   20
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   17
c ---[ 156]---> BDD-cost:   20
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:   35
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   41
c ---[ 149]---> BDD-cost:   38
c ---[ 148]---> BDD-cost:   36
c ---[ 147]---> BDD-cost:   32
c ---[ 146]---> BDD-cost:   32
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   29
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:   21
c ---[ 135]---> BDD-cost:   29
c ---[ 134]---> BDD-cost:   35
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   44
c ---[ 131]---> BDD-cost:   44
c ---[ 130]---> BDD-cost:   44
c ---[ 129]---> BDD-cost:   38
c ---[ 128]---> BDD-cost:   38
c ---[ 127]---> BDD-cost:   32
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   32
c ---[ 124]---> BDD-cost:   38
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   20
c ---[ 120]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:    7
c ---[ 117]---> BDD-cost:    5
c ---[ 116]---> BDD-cost:   29
c ---[ 115]---> BDD-cost:   32
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   44
c ---[ 112]---> BDD-cost:   50
c ---[ 111]---> BDD-cost:   41
c ---[ 110]---> BDD-cost:   42
c ---[ 109]---> BDD-cost:   38
c ---[ 108]---> BDD-cost:   41
c ---[ 107]---> BDD-cost:   35
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:   38
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:   32
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   41
c ---[  93]---> BDD-cost:   41
c ---[  92]---> BDD-cost:   47
c ---[  91]---> BDD-cost:   50
c ---[  90]---> BDD-cost:   53
c ---[  89]---> BDD-cost:   47
c ---[  88]---> BDD-cost:   38
c ---[  87]---> BDD-cost:   38
c ---[  86]---> BDD-cost:   35
c ---[  85]---> BDD-cost:   32
c ---[  84]---> BDD-cost:   32
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   32
c ---[  81]---> BDD-cost:   32
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   29
c ---[  74]---> BDD-cost:   32
c ---[  73]---> BDD-cost:   41
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:   44
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   32
c ---[  66]---> BDD-cost:   32
c ---[  65]---> BDD-cost:   32
c ---[  64]---> BDD-cost:   33
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   38
c ---[  50]---> BDD-cost:   32
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   29
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   20
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   20
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   20
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11765    33737 |    3921       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1032[0m
c ---[   0]---> Sorter-cost:70091     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  134745   321365 |   44915       0        0     nan |  0.000 % |
c |       101 |  134745   321365 |   49406     101      378     3.7 |  0.289 % |
c |       254 |  134745   321365 |   54347     254     1916     7.5 |  0.289 % |
c ==============================================================================
c [1mFound solution: 418[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       475 |  138441   330391 |   46147     472     3230     6.8 |  0.289 % |
c |       578 |  137873   329108 |   50761     564     3993     7.1 |  0.705 % |
c |       728 |  137788   328915 |   55837     711     4630     6.5 |  0.743 % |
c |       953 |  137788   328915 |   61421     936     9551    10.2 |  0.743 % |
c |      1291 |  137788   328915 |   67563    1274    13069    10.3 |  0.743 % |
c |      1797 |  137676   328664 |   74320    1779    23364    13.1 |  0.816 % |
c ==============================================================================
c [1mFound solution: 307[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2138 |  137959   329532 |   45986    2119    25259    11.9 |  0.816 % |
c |      2238 |  137959   329532 |   50584    2219    25773    11.6 |  0.865 % |
c ==============================================================================
c [1mFound solution: 159[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2254 |  138434   330777 |   46144    2235    25833    11.6 |  0.865 % |
c ==============================================================================
c [1mFound solution: 152[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2288 |  138490   330942 |   46163    2269    26896    11.9 |  0.865 % |
c |      2388 |  138445   330851 |   50779    2367    29840    12.6 |  0.898 % |
c |      2540 |  138236   330378 |   55857    2515    33411    13.3 |  1.013 % |
c |      2767 |  138236   330378 |   61442    2742    36817    13.4 |  1.013 % |
c ==============================================================================
c [1mFound solution: 107[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2941 |  138428   330891 |   46142    2916    38539    13.2 |  1.013 % |
c |      3041 |  138428   330891 |   50756    3016    40777    13.5 |  1.013 % |
c |      3192 |  138396   330824 |   55831    3165    42582    13.5 |  1.036 % |
c |      3417 |  138191   330372 |   61415    3383    46110    13.6 |  1.160 % |
c |      3755 |  138191   330372 |   67556    3721    49457    13.3 |  1.160 % |
c |      4261 |  137973   329869 |   74312    4216    55318    13.1 |  1.283 % |
c |      5021 |  137973   329869 |   81743    4976    75261    15.1 |  1.283 % |
c |      6160 |  137632   329105 |   89917    6100    90791    14.9 |  1.508 % |
c |      7868 |  137539   328894 |   98909    7805   110430    14.1 |  1.548 % |
c |     10430 |  137496   328803 |  108800   10365   155438    15.0 |  1.584 % |
c |     14275 |  137222   328193 |  119680   14202   275898    19.4 |  1.783 % |
c |     20041 |  137201   328148 |  131648   19967   704798    35.3 |  1.801 % |
c |     28692 |  137197   328139 |  144813   28613   996862    34.8 |  1.802 % |
c ==============================================================================
c [1mFound solution: 88[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34974 |  137098   327977 |   45699   34729  1135011    32.7 |  1.802 % |
c |     35074 |  136972   327695 |   50268   34826  1135981    32.6 |  2.051 % |
c |     35224 |  136972   327695 |   55295   34976  1137159    32.5 |  2.051 % |
c |     35449 |  136937   327620 |   60825   35198  1138927    32.4 |  2.081 % |
c |     35786 |  136937   327620 |   66907   35535  1149633    32.4 |  2.081 % |
c |     36294 |  136937   327620 |   73598   36043  1156248    32.1 |  2.081 % |
c |     37053 |  136937   327620 |   80958   36802  1254425    34.1 |  2.081 % |
c ==============================================================================
c [1mFound solution: 82[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37832 |  136969   327715 |   45656   37581  1268442    33.8 |  2.081 % |
c |     37932 |  136969   327715 |   50221   37681  1268959    33.7 |  2.082 % |
c |     38082 |  136969   327715 |   55243   37831  1271895    33.6 |  2.082 % |
c |     38307 |  136969   327715 |   60768   38056  1273306    33.5 |  2.082 % |
c |     38645 |  136878   327506 |   66844   38390  1280523    33.4 |  2.125 % |
c |     39151 |  136707   327110 |   73529   38894  1286713    33.1 |  2.235 % |
c |     39910 |  136664   327019 |   80882   39652  1301996    32.8 |  2.270 % |
c |     41049 |  136630   326945 |   88970   40691  1321509    32.5 |  2.300 % |
c |     42758 |  136630   326945 |   97867   42400  1363954    32.2 |  2.300 % |
c |     45320 |  136630   326945 |  107654   44962  1451229    32.3 |  2.300 % |
c |     49164 |  136306   326216 |  118419   48769  1554071    31.9 |  2.484 % |
c |     54932 |  136306   326216 |  130261   54537  1926766    35.3 |  2.484 % |
c |     63582 |  136306   326216 |  143288   63187  2438273    38.6 |  2.484 % |
c ==============================================================================
c [1mFound solution: 77[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75735 |  136126   325854 |   45375   75325  3553417    47.2 |  2.484 % |
c |     75835 |  136126   325854 |   49912   20862  1157455    55.5 |  2.637 % |
c |     75987 |  136104   325804 |   54903   21007  1158369    55.1 |  2.646 % |
c |     76212 |  136104   325804 |   60394   21232  1161236    54.7 |  2.646 % |
c |     76550 |  136104   325804 |   66433   21570  1166658    54.1 |  2.646 % |
c |     77056 |  136104   325804 |   73076   22076  1203230    54.5 |  2.646 % |
c |     77816 |  136104   325804 |   80384   22836  1215601    53.2 |  2.646 % |
c |     78955 |  136104   325804 |   88423   23975  1238001    51.6 |  2.646 % |
c |     80663 |  136104   325804 |   97265   25683  1261960    49.1 |  2.646 % |
c |     83225 |  136104   325804 |  106991   28245  1330287    47.1 |  2.646 % |
c ==============================================================================
c [1mFound solution: 74[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83353 |  136111   325827 |   45370   28373  1332445    47.0 |  2.646 % |
c |     83455 |  136111   325827 |   49907   28475  1335456    46.9 |  2.647 % |
c |     83605 |  136111   325827 |   54897   28625  1341423    46.9 |  2.647 % |
c |     83830 |  136111   325827 |   60387   28850  1344077    46.6 |  2.647 % |
c |     84167 |  136111   325827 |   66426   29187  1349710    46.2 |  2.647 % |
c |     84678 |  136111   325827 |   73068   29698  1354687    45.6 |  2.647 % |
c |     85438 |  136111   325827 |   80375   30458  1385841    45.5 |  2.647 % |
c |     86578 |  136111   325827 |   88413   31598  1470539    46.5 |  2.647 % |
c |     88289 |  136111   325827 |   97254   33309  1509109    45.3 |  2.647 % |
c |     90851 |  136111   325827 |  106980   35871  1574590    43.9 |  2.647 % |
c |     94696 |  136101   325804 |  117678   39713  1653312    41.6 |  2.652 % |
c |    100462 |  136101   325804 |  129445   45479  2632354    57.9 |  2.652 % |
c |    109112 |  136101   325804 |  142390   54129  3093113    57.1 |  2.652 % |
c ==============================================================================
c [1mFound solution: 65[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113671 |  136179   326029 |   45393   58688  3937613    67.1 |  2.652 % |
c |    113771 |  136179   326029 |   49932   19316  1305290    67.6 |  2.651 % |
c |    113922 |  136179   326029 |   54925   19467  1308808    67.2 |  2.651 % |
c |    114147 |  136179   326029 |   60418   19692  1327557    67.4 |  2.651 % |
c |    114487 |  136106   325864 |   66459   20031  1335002    66.6 |  2.682 % |
c |    114993 |  136106   325864 |   73105   20537  1351714    65.8 |  2.682 % |
c |    115752 |  136106   325864 |   80416   21296  1374179    64.5 |  2.682 % |
c |    116894 |  136106   325864 |   88458   22438  1418701    63.2 |  2.682 % |
c |    118602 |  136106   325864 |   97303   24146  1569573    65.0 |  2.682 % |
c |    121164 |  136034   325706 |  107034   26665  1664717    62.4 |  2.746 % |
c |    125008 |  135980   325582 |  117737   30508  1739829    57.0 |  2.773 % |
c |    130775 |  135948   325509 |  129511   36267  1862330    51.4 |  2.786 % |
c |    139426 |  135948   325509 |  142462   44918  3368859    75.0 |  2.786 % |
c |    152400 |  135893   325384 |  156708   57883  4159349    71.9 |  2.838 % |
c |    171861 |  135893   325384 |  172379   77344  5629384    72.8 |  2.838 % |
c |    201053 |  135893   325384 |  189617  106536  7633114    71.6 |  2.838 % |
c ==============================================================================
c [1mFound solution: 50[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    229232 |  135966   325588 |   45322  134715 12974184    96.3 |  2.838 % |
c |    229334 |  135966   325588 |   49854   22269  3043851   136.7 |  2.838 % |
c |    229485 |  135966   325588 |   54839   22420  3045543   135.8 |  2.838 % |
c |    229712 |  135966   325588 |   60323   22647  3049706   134.7 |  2.838 % |
c |    230052 |  135966   325588 |   66355   22987  3055255   132.9 |  2.838 % |
c |    230558 |  135966   325588 |   72991   23493  3069007   130.6 |  2.838 % |
c |    231317 |  135966   325588 |   80290   24252  3104267   128.0 |  2.838 % |
c |    232458 |  135966   325588 |   88319   25393  3151730   124.1 |  2.838 % |
c |    234166 |  135870   325356 |   97151   27098  3218727   118.8 |  2.916 % |
c |    236728 |  135870   325356 |  106866   29660  3316097   111.8 |  2.916 % |
c |    240572 |  135870   325356 |  117553   33504  3454662   103.1 |  2.916 % |
c |    246338 |  135862   325337 |  129308   39265  3778497    96.2 |  2.921 % |
c |    254987 |  135862   325337 |  142239   47914  4054928    84.6 |  2.921 % |
c |    267963 |  135862   325337 |  156463   60890  4689436    77.0 |  2.921 % |
c |    287424 |  135862   325337 |  172110   80351  5759564    71.7 |  2.921 % |
c |    316616 |  135862   325337 |  189321  109543  7019224    64.1 |  2.921 % |
c |    360405 |  135862   325337 |  208253  153332  9142712    59.6 |  2.921 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 18045 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.91 2/54 18041
Raw data (stat): 18041 (runsolver) R 18040 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795597421 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0041 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0048 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0054 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0065 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0072 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0078 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 18045
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 3/60 18071
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.124 s]
Raw data (loadavg): 1.14 1.00 0.92 2/55 18098
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.125 s]
Raw data (loadavg): 1.12 1.00 0.92 2/55 18098
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.125 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 18098
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.126 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 18098
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.126 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 18098
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.127 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 18098
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.127 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 18098
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.127 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.128 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.128 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.128 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.128 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.13 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.13 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.13 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.131 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.131 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.131 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18100
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.54 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 18102
Raw data (stat): 18041 (minisat+_script) S 18040 25568 25567 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795597421 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.54
CPU time (s): 1229.87
CPU user time (s): 1229.12
CPU system time (s): 0.749886
CPU usage (%): 100.027
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####