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/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10b.opb
MD5SUM	c76102ddcf7f5ab3b2677033d320eaa3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	756736
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	502612132
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	502612132
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	422.405
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 31259

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-05-25 23:36:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22662 boxname=wulflinc1 idbench=1478 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  c76102ddcf7f5ab3b2677033d320eaa3  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-ran10x10b.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-ran10x10b.opb
IDLAUNCH: 22662
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        896968 kB
Buffers:         25404 kB
Cached:          87652 kB
SwapCached:        640 kB
Active:          19572 kB
Inactive:        95740 kB
HighTotal:      131008 kB
HighFree:        54348 kB
LowTotal:       903652 kB
LowFree:        842620 kB
SwapTotal:     2097136 kB
SwapFree:      2095444 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            16588 kB
Committed_AS:    92720 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:57:21 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22662 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 180   maxlim: 8950   bits: 14/14
c ---[ 112]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   12
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   94440   224184 |   31480       0        0     nan |  0.000 % |
c |       101 |   94437   224178 |   34628     100      570     5.7 |  7.012 % |
c |       252 |   94437   224178 |   38090     251     1345     5.4 |  7.012 % |
c |       477 |   94437   224178 |   41899     476     2436     5.1 |  7.012 % |
c |       815 |   94437   224178 |   46089     814     4318     5.3 |  7.012 % |
c |      1321 |   94364   224012 |   50698    1315     7319     5.6 |  7.070 % |
c |      2080 |   94364   224012 |   55768    2074    13413     6.5 |  7.070 % |
c ==============================================================================
c [1mFound solution: 3361005[0m
c ---[   0]---> Adder-cost: 3932   maxlim: 748215   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2827 |  121769   321931 |   40589    2820    18795     6.7 |  7.070 % |
c |      2927 |  121769   321931 |   44647    2920    19181     6.6 |  6.370 % |
c |      3077 |  121769   321931 |   49112    3070    19960     6.5 |  6.370 % |
c |      3302 |  121759   321908 |   54023    3294    21345     6.5 |  6.378 % |
c |      3639 |  121712   321803 |   59426    3629    22935     6.3 |  6.412 % |
c |      4146 |  121626   321610 |   65368    4125    28733     7.0 |  6.475 % |
c |      4905 |  121542   321421 |   71905    4876    34042     7.0 |  6.536 % |
c |      6044 |  121474   321266 |   79096    6005    39965     6.7 |  6.586 % |
c ==============================================================================
c [1mFound solution: 3321878[0m
c ---[   0]---> Adder-cost: 0   maxlim: 787342   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6703 |  121285   320978 |   40428    6639    58563     8.8 |  6.586 % |
c |      6804 |  121285   320978 |   44470    6740    59057     8.8 |  6.766 % |
c |      6957 |  121285   320978 |   48917    6893    62729     9.1 |  6.766 % |
c |      7182 |  121285   320978 |   53809    7118    64454     9.1 |  6.766 % |
c |      7519 |  121169   320707 |   59190    7417    65940     8.9 |  6.859 % |
c |      8026 |  121169   320707 |   65109    7924    68826     8.7 |  6.859 % |
c ==============================================================================
c [1mFound solution: 3034933[0m
c ---[   0]---> Adder-cost: 2   maxlim: 1074287   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8656 |  121194   320855 |   40398    8552    75550     8.8 |  6.859 % |
c |      8756 |  121194   320855 |   44437    8652    76113     8.8 |  6.878 % |
c |      8908 |  121194   320855 |   48881    8804    77091     8.8 |  6.878 % |
c |      9133 |  121152   320760 |   53769    9024    78322     8.7 |  6.912 % |
c |      9470 |  121152   320760 |   59146    9361    80758     8.6 |  6.912 % |
c |      9977 |  121143   320731 |   65061    9867    83509     8.5 |  6.917 % |
c |     10738 |  120912   320196 |   71567   10605   108938    10.3 |  7.102 % |
c |     11878 |  120790   319922 |   78724   11737   136105    11.6 |  7.192 % |
c |     13586 |  120728   319779 |   86596   13439   318010    23.7 |  7.239 % |
c ==============================================================================
c [1mFound solution: 2741413[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1367807   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14526 |  120415   319084 |   40138   14363   328514    22.9 |  7.239 % |
c |     14626 |  120291   318801 |   44151   14448   328931    22.8 |  7.599 % |
c |     14776 |  120291   318801 |   48566   14598   329878    22.6 |  7.599 % |
c |     15001 |  120291   318801 |   53423   14823   331411    22.4 |  7.599 % |
c |     15339 |  120196   318579 |   58766   15153   334444    22.1 |  7.668 % |
c |     15845 |  120196   318579 |   64642   15659   358958    22.9 |  7.668 % |
c ==============================================================================
c [1mFound solution: 2139517[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1969703   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16297 |  120178   318611 |   40059   16106   369090    22.9 |  7.668 % |
c |     16397 |  120178   318611 |   44064   16206   369595    22.8 |  7.711 % |
c |     16548 |  120151   318551 |   48471   16356   370428    22.6 |  7.729 % |
c |     16774 |  120151   318551 |   53318   16582   372967    22.5 |  7.729 % |
c |     17111 |  120151   318551 |   58650   16919   375249    22.2 |  7.729 % |
c |     17618 |  120109   318454 |   64515   17425   380618    21.8 |  7.758 % |
c |     18377 |  119996   318197 |   70966   18169   391139    21.5 |  7.843 % |
c |     19517 |  119952   318097 |   78063   19307   426757    22.1 |  7.874 % |
c |     21226 |  119894   317962 |   85870   20993   569764    27.1 |  7.916 % |
c |     23789 |  119764   317666 |   94457   23537   682312    29.0 |  8.025 % |
c |     27633 |  119564   317200 |  103902   27363   825435    30.2 |  8.170 % |
c ==============================================================================
c [1mFound solution: 2113156[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1996064   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28733 |  119550   317247 |   39850   28462   885214    31.1 |  8.170 % |
c |     28834 |  119550   317247 |   43835   28563   887914    31.1 |  8.204 % |
c |     28986 |  119550   317247 |   48218   28715   892015    31.1 |  8.204 % |
c |     29211 |  119536   317215 |   53040   28939   893555    30.9 |  8.215 % |
c |     29548 |  119536   317215 |   58344   29276   897025    30.6 |  8.215 % |
c |     30054 |  119520   317163 |   64178   29779   900477    30.2 |  8.223 % |
c |     30814 |  119510   317141 |   70596   30538   959301    31.4 |  8.231 % |
c |     31957 |  119364   316810 |   77656   31665  1002720    31.7 |  8.336 % |
c |     33666 |  119141   316297 |   85422   33358  1184902    35.5 |  8.526 % |
c |     36229 |  119138   316291 |   93964   35920  1272971    35.4 |  8.529 % |
c |     40073 |  119138   316291 |  103360   39764  1694680    42.6 |  8.529 % |
c ==============================================================================
c [1mFound solution: 1952025[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2157195   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42094 |  118990   315750 |   39663   41553  1778469    42.8 |  8.529 % |
c |     42195 |  118990   315750 |   43629   41654  1779031    42.7 |  8.644 % |
c |     42345 |  118990   315750 |   47992   41804  1779955    42.6 |  8.644 % |
c |     42570 |  118969   315702 |   52791   42028  1784395    42.5 |  8.660 % |
c |     42908 |  118969   315702 |   58070   42366  1801515    42.5 |  8.660 % |
c |     43416 |  118969   315702 |   63877   42874  1808231    42.2 |  8.660 % |
c |     44176 |  118969   315702 |   70265   43634  1870338    42.9 |  8.660 % |
c |     45315 |  118962   315687 |   77291   44772  2076825    46.4 |  8.665 % |
c |     47023 |  118910   315571 |   85021   46476  2136601    46.0 |  8.707 % |
c |     49586 |  118762   315232 |   93523   49028  2291729    46.7 |  8.820 % |
c |     53430 |  118565   314772 |  102875   52851  2489507    47.1 |  8.971 % |
c |     59197 |  118420   314432 |  113163   58590  2915808    49.8 |  9.084 % |
c |     67846 |  118390   314365 |  124479   67236  3610523    53.7 |  9.108 % |
c |     80821 |  118313   314184 |  136927   80197  4438935    55.4 |  9.174 % |
c |    100283 |  118144   313795 |  150620   99633 11034769   110.8 |  9.316 % |
c |    129476 |  117905   313241 |  165682  128795 13936639   108.2 |  9.492 % |
c ==============================================================================
c [1mFound solution: 1916946[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2192274   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168420 |  117896   313332 |   39298  167734 22410520   133.6 |  9.492 % |
c |    168520 |  117870   313270 |   43227   20819  4079432   195.9 |  9.560 % |
c |    168670 |  117870   313270 |   47550   20969  4081339   194.6 |  9.560 % |
c |    168898 |  117870   313270 |   52305   21197  4084562   192.7 |  9.560 % |
c |    169236 |  117870   313270 |   57536   21535  4086594   189.8 |  9.560 % |
c |    169742 |  117870   313270 |   63289   22041  4089391   185.5 |  9.560 % |
c |    170501 |  117870   313270 |   69618   22800  4104055   180.0 |  9.560 % |
c |    171640 |  117791   313088 |   76580   23934  4125283   172.4 |  9.615 % |
c |    173349 |  117745   312985 |   84238   25638  4191141   163.5 |  9.649 % |
c |    175911 |  117704   312889 |   92662   28195  4449613   157.8 |  9.683 % |
c |    179755 |  117577   312586 |  101928   32025  4659052   145.5 |  9.770 % |
c |    185522 |  117567   312564 |  112121   37791  5194372   137.4 |  9.778 % |
c ==============================================================================
c [1mFound solution: 1886130[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2223090   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187250 |  117587   312745 |   39195   39519  5355132   135.5 |  9.778 % |
c |    187350 |  117587   312745 |   43114   39619  5357166   135.2 |  9.805 % |
c |    187500 |  117576   312721 |   47425   39768  5357889   134.7 |  9.813 % |
c |    187725 |  117576   312721 |   52168   39993  5364068   134.1 |  9.813 % |
c |    188062 |  117576   312721 |   57385   40330  5376881   133.3 |  9.813 % |
c |    188568 |  117576   312721 |   63123   40836  5393883   132.1 |  9.813 % |
c |    189327 |  117513   312554 |   69436   41584  5416974   130.3 |  9.857 % |
c |    190467 |  117513   312554 |   76379   42724  5452110   127.6 |  9.857 % |
c |    192177 |  117478   312474 |   84017   44432  5499810   123.8 |  9.884 % |
c ==============================================================================
c [1mFound solution: 1389200[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2720020   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192899 |  117488   312570 |   39162   45154  5579341   123.6 |  9.884 % |
c |    192999 |  117488   312570 |   43078   19622   904548    46.1 |  9.899 % |
c |    193151 |  117488   312570 |   47386   19774   905793    45.8 |  9.899 % |
c |    193377 |  117488   312570 |   52124   20000   909419    45.5 |  9.899 % |
c |    193715 |  117488   312570 |   57337   20338   941855    46.3 |  9.899 % |
c |    194222 |  117477   312545 |   63070   20844   952724    45.7 |  9.907 % |
c |    194982 |  117427   312430 |   69377   21600   987252    45.7 |  9.947 % |
c |    196123 |  117427   312430 |   76315   22741  1022205    44.9 |  9.947 % |
c |    197831 |  117364   312288 |   83947   24439  1119745    45.8 |  9.999 % |
c |    200393 |  117364   312288 |   92341   27001  1354141    50.2 |  9.999 % |
c |    204237 |  117322   312184 |  101576   30832  1677457    54.4 | 10.031 % |
c |    210003 |  117322   312184 |  111733   36598  2155397    58.9 | 10.031 % |
c |    218653 |  117306   312147 |  122907   45247  2729443    60.3 | 10.044 % |
c |    231629 |  117306   312147 |  135197   58223  7709688   132.4 | 10.044 % |
c |    251090 |  117271   312067 |  148717   77678  8752573   112.7 | 10.073 % |
c |    280282 |  117139   311758 |  163589  106864 12479821   116.8 | 10.178 % |
c |    324072 |  116978   311385 |  179948  150630 17457633   115.9 | 10.302 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 26908 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.90 2/55 26904
Raw data (stat): 26904 (runsolver) R 26903 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 727813670 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0005 s]
Raw data (loadavg): 0.93 0.95 0.90 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0007 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+219.999 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+229.999 s]
Raw data (loadavg): 1.14 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+239.999 s]
Raw data (loadavg): 1.11 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+249.999 s]
Raw data (loadavg): 1.10 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+259.999 s]
Raw data (loadavg): 1.08 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+269.998 s]
Raw data (loadavg): 1.07 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+279.998 s]
Raw data (loadavg): 1.06 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+289.999 s]
Raw data (loadavg): 1.05 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+299.999 s]
Raw data (loadavg): 1.04 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+309.999 s]
Raw data (loadavg): 1.03 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+319.998 s]
Raw data (loadavg): 1.03 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+329.998 s]
Raw data (loadavg): 1.02 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+339.998 s]
Raw data (loadavg): 1.02 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+349.998 s]
Raw data (loadavg): 1.02 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+359.999 s]
Raw data (loadavg): 1.01 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+369.998 s]
Raw data (loadavg): 1.01 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+379.998 s]
Raw data (loadavg): 1.01 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+389.999 s]
Raw data (loadavg): 1.01 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+399.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+419.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.108 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.108 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.109 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.112 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.111 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.116 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.116 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.117 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.116 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.116 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.116 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.116 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.117 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/56 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.76 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 26908
Raw data (stat): 26904 (minisat+_script) S 26903 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 727813670 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.76
CPU time (s): 1229.88
CPU user time (s): 1229.01
CPU system time (s): 0.877866
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####