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-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran10x10b.opb
MD5SUM	76a1809de3568e1012eb6c6785191a40
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	7588573
Optimality of the best value was proved	NO
Number of terms in the objective function	3100
Biggest coefficient in the objective function	4831838208
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	511129031204
Number of bits of the sum of numbers in the objective function	39
Biggest number in a constraint	4831838208
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	511129031204
Number of bits of the biggest sum of numbers	39
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1217.92
Number of variables	3100
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	31
Maximum length of a constraint	300
Trace number 30875

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        906332 kB
Buffers:          8856 kB
Cached:         100468 kB
SwapCached:         20 kB
Active:          39668 kB
Inactive:        72332 kB
HighTotal:      131008 kB
HighFree:        27300 kB
LowTotal:       903652 kB
LowFree:        879032 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6576 kB
Slab:            10824 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:47:06 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22278 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: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 2492     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2492     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2492     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2633     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2633     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Adder-cost: 216   maxlim: 35830   bits: 16/16
c ---[ 122]---> Sorter-cost: 2492     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 2306     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 234   maxlim: 71670   bits: 17/17
c ---[ 112]---> Sorter-cost: 2731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 2306     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 2731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   18
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:   16
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   16
c ---[  92]---> BDD-cost:   14
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   16
c ---[  89]---> BDD-cost:   12
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:   14
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   14
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   12
c ---[  77]---> BDD-cost:   14
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   20
c ---[  71]---> BDD-cost:   20
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   20
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   12
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   16
c ---[  64]---> BDD-cost:   14
c ---[  63]---> BDD-cost:   16
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   16
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   12
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   14
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   16
c ---[  49]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   18
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   18
c ---[  35]---> BDD-cost:   18
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   18
c ---[  32]---> BDD-cost:   18
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   14
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   12
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   14
c ---[  12]---> BDD-cost:   12
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   18
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   19
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   20
c ---[   2]---> BDD-cost:   18
c ---[   1]---> BDD-cost:   12
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  124542   297125 |   41514       0        0     nan |  0.000 % |
c |       100 |  124542   297125 |   45665     100      426     4.3 |  7.068 % |
c |       250 |  124542   297125 |   50231     250     1125     4.5 |  7.068 % |
c |       476 |  124542   297125 |   55255     476     2274     4.8 |  7.068 % |
c |       813 |  124542   297125 |   60780     813     3951     4.9 |  7.068 % |
c |      1321 |  124542   297125 |   66858    1321     6491     4.9 |  7.068 % |
c |      2080 |  124542   297125 |   73544    2080    10617     5.1 |  7.068 % |
c |      3219 |  124518   297072 |   80899    3218    17426     5.4 |  7.084 % |
c |      4927 |  124494   297019 |   88988    4924    27795     5.6 |  7.099 % |
c |      7489 |  124332   296637 |   97887    7476    43689     5.8 |  7.198 % |
c |     11333 |  123998   295811 |  107676   11295    69975     6.2 |  7.401 % |
c ==============================================================================
c [1mFound solution: 28111120[0m
c ---[   0]---> Adder-cost: 4880   maxlim: 4765972   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15524 |  157854   416987 |   52618   15481    98297     6.3 |  7.401 % |
c |     15624 |  157804   416873 |   57879   15576    98764     6.3 |  6.822 % |
c |     15774 |  157685   416603 |   63667   15718    99598     6.3 |  6.889 % |
c |     15999 |  157685   416603 |   70034   15943   100812     6.3 |  6.889 % |
c |     16336 |  157650   416524 |   77038   16278   102874     6.3 |  6.907 % |
c |     16842 |  157585   416378 |   84741   16781   105881     6.3 |  6.947 % |
c |     17601 |  157576   416349 |   93215   17538   111082     6.3 |  6.951 % |
c |     18741 |  157534   416255 |  102537   18675   118295     6.3 |  6.976 % |
c |     20449 |  157405   415959 |  112791   20379   131439     6.4 |  7.049 % |
c ==============================================================================
c [1mFound solution: 27693382[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5183710   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21557 |  157435   416224 |   52478   21487   139947     6.5 |  7.049 % |
c |     21657 |  157340   416007 |   57725   21579   140459     6.5 |  7.124 % |
c |     21807 |  157340   416007 |   63498   21729   141273     6.5 |  7.124 % |
c |     22032 |  157340   416007 |   69848   21954   142763     6.5 |  7.124 % |
c |     22369 |  157340   416007 |   76833   22291   144704     6.5 |  7.124 % |
c |     22877 |  157333   415991 |   84516   22798   148014     6.5 |  7.130 % |
c |     23638 |  157333   415991 |   92967   23559   153253     6.5 |  7.130 % |
c |     24777 |  157333   415991 |  102264   24698   160889     6.5 |  7.130 % |
c |     26487 |  157195   415676 |  112491   26398   174909     6.6 |  7.211 % |
c ==============================================================================
c [1mFound solution: 27315187[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5561905   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27289 |  157120   415587 |   52373   27193   180346     6.6 |  7.211 % |
c |     27389 |  157120   415587 |   57610   27293   180799     6.6 |  7.276 % |
c |     27539 |  157120   415587 |   63371   27443   181736     6.6 |  7.276 % |
c |     27764 |  157120   415587 |   69708   27668   183289     6.6 |  7.276 % |
c |     28101 |  157120   415587 |   76679   28005   185398     6.6 |  7.276 % |
c ==============================================================================
c [1mFound solution: 25935176[0m
c ---[   0]---> Adder-cost: 0   maxlim: 6941916   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28412 |  157116   415762 |   52372   28314   194022     6.9 |  7.276 % |
c |     28513 |  157116   415762 |   57609   28415   194642     6.8 |  7.318 % |
c |     28664 |  157116   415762 |   63370   28566   195589     6.8 |  7.318 % |
c |     28889 |  157116   415762 |   69707   28791   197508     6.9 |  7.318 % |
c |     29226 |  157116   415762 |   76677   29128   201465     6.9 |  7.318 % |
c |     29732 |  157116   415762 |   84345   29634   205909     6.9 |  7.318 % |
c ==============================================================================
c [1mFound solution: 25822821[0m
c ---[   0]---> Adder-cost: 0   maxlim: 7054271   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30195 |  157125   415873 |   52375   30097   210428     7.0 |  7.318 % |
c |     30295 |  157125   415873 |   57612   30197   210996     7.0 |  7.332 % |
c |     30445 |  157125   415873 |   63373   30347   212079     7.0 |  7.332 % |
c |     30670 |  157125   415873 |   69711   30572   213397     7.0 |  7.332 % |
c |     31007 |  157125   415873 |   76682   30909   215350     7.0 |  7.332 % |
c |     31514 |  157125   415873 |   84350   31416   219927     7.0 |  7.332 % |
c |     32276 |  157097   415811 |   92785   32173   224518     7.0 |  7.349 % |
c |     33417 |  157097   415811 |  102064   33314   273487     8.2 |  7.349 % |
c |     35126 |  157093   415802 |  112270   35022   364603    10.4 |  7.351 % |
c ==============================================================================
c [1mFound solution: 25638121[0m
c ---[   0]---> Adder-cost: 0   maxlim: 7238971   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36486 |  157034   415806 |   52344   36380   389724    10.7 |  7.351 % |
c |     36586 |  157034   415806 |   57578   36480   390283    10.7 |  7.423 % |
c |     36736 |  157034   415806 |   63336   36630   391374    10.7 |  7.423 % |
c |     36961 |  157034   415806 |   69669   36855   393462    10.7 |  7.423 % |
c |     37298 |  157034   415806 |   76636   37192   395916    10.6 |  7.423 % |
c |     37804 |  157024   415784 |   84300   37697   404714    10.7 |  7.429 % |
c |     38563 |  156993   415715 |   92730   38449   423824    11.0 |  7.450 % |
c ==============================================================================
c [1mFound solution: 25246558[0m
c ---[   0]---> Adder-cost: 0   maxlim: 7630534   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39122 |  156861   415568 |   52287   39006   431162    11.1 |  7.450 % |
c |     39222 |  156861   415568 |   57515   39106   431718    11.0 |  7.572 % |
c |     39372 |  156861   415568 |   63267   39256   433253    11.0 |  7.572 % |
c |     39597 |  156861   415568 |   69593   39481   434854    11.0 |  7.572 % |
c |     39935 |  156861   415568 |   76553   39819   437389    11.0 |  7.572 % |
c |     40441 |  156861   415568 |   84208   40325   442109    11.0 |  7.572 % |
c |     41201 |  156861   415568 |   92629   41085   519020    12.6 |  7.572 % |
c |     42342 |  156861   415568 |  101892   42226   611883    14.5 |  7.572 % |
c |     44050 |  156754   415321 |  112081   43930   706973    16.1 |  7.645 % |
c |     46612 |  156615   415002 |  123290   46486   769439    16.6 |  7.734 % |
c ==============================================================================
c [1mFound solution: 19406826[0m
c ---[   0]---> Adder-cost: 2   maxlim: 13470266   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48672 |  156654   415270 |   52218   48546   850884    17.5 |  7.734 % |
c |     48772 |  156654   415270 |   57439   48646   851490    17.5 |  7.757 % |
c |     48922 |  156654   415270 |   63183   48796   853652    17.5 |  7.757 % |
c |     49147 |  156654   415270 |   69502   49021   862061    17.6 |  7.757 % |
c |     49484 |  156654   415270 |   76452   49358   869542    17.6 |  7.757 % |
c |     49990 |  156654   415270 |   84097   49864   884758    17.7 |  7.757 % |
c |     50749 |  156654   415270 |   92507   50623   937500    18.5 |  7.757 % |
c |     51888 |  156654   415270 |  101758   51762  1025023    19.8 |  7.757 % |
c |     53597 |  156651   415264 |  111933   53470  1102804    20.6 |  7.759 % |
c |     56160 |  156641   415241 |  123127   56031  1308236    23.3 |  7.765 % |
c ==============================================================================
c [1mFound solution: 18503008[0m
c ---[   0]---> Adder-cost: 0   maxlim: 14374084   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59312 |  156563   415185 |   52187   59180  1552825    26.2 |  7.765 % |
c |     59412 |  156563   415185 |   57405   24604   789571    32.1 |  7.844 % |
c |     59563 |  156563   415185 |   63146   24755   791901    32.0 |  7.844 % |
c |     59788 |  156544   415142 |   69460   24978   793455    31.8 |  7.854 % |
c |     60125 |  156544   415142 |   76406   25315   796932    31.5 |  7.854 % |
c |     60631 |  156544   415142 |   84047   25821   801519    31.0 |  7.854 % |
c |     61391 |  156544   415142 |   92452   26581   810323    30.5 |  7.854 % |
c |     62530 |  156544   415142 |  101697   27720   840942    30.3 |  7.854 % |
c |     64239 |  156527   415103 |  111867   29427   903763    30.7 |  7.867 % |
c |     66801 |  156527   415103 |  123054   31989   994527    31.1 |  7.867 % |
c |     70647 |  156511   415057 |  135359   35831  1214024    33.9 |  7.873 % |
c |     76414 |  156316   414608 |  148895   41585  1568654    37.7 |  7.984 % |
c |     85065 |  156300   414556 |  163785   50232  2099767    41.8 |  7.990 % |
c |     98040 |  156225   414387 |  180163   63201  3325519    52.6 |  8.036 % |
c ==============================================================================
c [1mFound solution: 10701810[0m
c ---[   0]---> Adder-cost: 0   maxlim: 22175282   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    106481 |  156222   414259 |   52074   68698  4407637    64.2 |  8.036 % |
c |    106581 |  156222   414259 |   57281   22674  1774267    78.3 |  8.059 % |
c |    106732 |  156222   414259 |   63009   22825  1775085    77.8 |  8.059 % |
c |    106957 |  156222   414259 |   69310   23050  1776404    77.1 |  8.059 % |
c |    107295 |  156222   414259 |   76241   23388  1779290    76.1 |  8.059 % |
c |    107801 |  156222   414259 |   83865   23894  1782625    74.6 |  8.059 % |
c |    108560 |  156222   414259 |   92252   24653  1787244    72.5 |  8.059 % |
c |    109700 |  156222   414259 |  101477   25793  1793825    69.5 |  8.059 % |
c |    111409 |  156164   414128 |  111625   27498  1830254    66.6 |  8.093 % |
c |    113971 |  156164   414128 |  122787   30060  1920536    63.9 |  8.093 % |
c |    117817 |  156164   414128 |  135066   33906  2051559    60.5 |  8.093 % |
c |    123585 |  156164   414128 |  148573   39674  2734088    68.9 |  8.093 % |
c |    132236 |  156096   413967 |  163430   48317  3739236    77.4 |  8.134 % |
c |    145210 |  156076   413923 |  179773   61289  4399587    71.8 |  8.146 % |
c |    164671 |  155438   412456 |  197750   80694  5761099    71.4 |  8.524 % |
c |    193863 |  155289   412098 |  217526  109860  7768737    70.7 |  8.611 % |
c |    237652 |  155040   411521 |  239278  153625 11725125    76.3 |  8.758 % |
c |    303336 |  154916   411236 |  263206  219305 17536993    80.0 |  8.829 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  4220 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.92 2/54 4216
Raw data (stat): 4216 (runsolver) R 4215 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783521059 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.95 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0006 s]
Raw data (loadavg): 0.95 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0041 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.075 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.076 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.077 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.077 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.078 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.077 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.079 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.079 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.079 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.079 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.081 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.081 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.202 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.203 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.203 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.203 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.203 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.203 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.204 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.206 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.206 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.76 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 4220
Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 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): 1228.92
CPU system time (s): 0.958854
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####