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-gr4x6.opb
MD5SUM	d90fce7408f7990dccb3ba4f8fa1c8f6
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	23403520
Optimality of the best value was proved	NO
Number of terms in the objective function	744
Biggest coefficient in the objective function	151934468096
Number of bits for the biggest coefficient in the objective function	38
Sum of the numbers in the objective function	3470370333536
Number of bits of the sum of numbers in the objective function	42
Biggest number in a constraint	151934468096
Number of bits of the biggest number in a constraint	38
Biggest sum of numbers in a constraint	3470370333536
Number of bits of the biggest sum of numbers	42
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1247.15
Number of variables	744
Total number of constraints	34
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	34
Minimum length of a constraint	31
Maximum length of a constraint	180
Trace number 30857

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        897276 kB
Buffers:         28472 kB
Cached:          84880 kB
SwapCached:        412 kB
Active:          22096 kB
Inactive:        93584 kB
HighTotal:      131008 kB
HighFree:        55692 kB
LowTotal:       903652 kB
LowFree:        841584 kB
SwapTotal:     2097136 kB
SwapFree:      2096036 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            16084 kB
Committed_AS:    63724 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:37:38 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 22261 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 44 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): (none)
c ---[  42]---> Sorter-cost: 1236     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1236     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost: 1152     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  591     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> BDD-cost:   22
c ---[  22]---> BDD-cost:   19
c ---[  21]---> BDD-cost:   16
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:   18
c ---[  18]---> BDD-cost:   18
c ---[  17]---> BDD-cost:   18
c ---[  16]---> BDD-cost:   18
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   18
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   18
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   22
c ---[   2]---> BDD-cost:   19
c ---[   1]---> BDD-cost:   20
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20089    47581 |    6696       0        0     nan |  0.000 % |
c |       100 |   20089    47581 |    7365     100      393     3.9 | 10.732 % |
c |       250 |   20039    47467 |    8102     246     1058     4.3 | 10.902 % |
c ==============================================================================
c [1mFound solution: 48834098[0m
c ---[   0]---> Sorter-cost:80542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       370 |  245919   574838 |   81973     366     1616     4.4 | 10.902 % |
c |       472 |  245919   574838 |   90170     468     2875     6.1 |  0.987 % |
c |       622 |  245919   574838 |   99187     618     5853     9.5 |  0.987 % |
c |       849 |  245919   574838 |  109106     845    14016    16.6 |  0.987 % |
c |      1186 |  245907   574812 |  120016    1180    28174    23.9 |  0.992 % |
c |      1692 |  245756   574471 |  132018    1682    32367    19.2 |  1.040 % |
c |      2452 |  245756   574471 |  145220    2442    41855    17.1 |  1.040 % |
c |      3591 |  245756   574471 |  159742    3581    60900    17.0 |  1.040 % |
c |      5299 |  245756   574471 |  175716    5289    78968    14.9 |  1.040 % |
c ==============================================================================
c [1mFound solution: 48658918[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6135 |  246491   576704 |   82163    6125    91885    15.0 |  1.040 % |
c |      6235 |  246491   576704 |   90379    6225    92395    14.8 |  1.036 % |
c |      6385 |  246491   576704 |   99417    6375    93090    14.6 |  1.036 % |
c |      6612 |  246491   576704 |  109358    6602    95928    14.5 |  1.036 % |
c |      6950 |  246433   576574 |  120294    6934    99591    14.4 |  1.054 % |
c ==============================================================================
c [1mFound solution: 48585107[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6973 |  246457   576787 |   82152    6957    99867    14.4 |  1.054 % |
c |      7073 |  246457   576787 |   90367    7057   103129    14.6 |  1.055 % |
c ==============================================================================
c [1mFound solution: 47745280[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7205 |  246689   577396 |   82229    7184   104557    14.6 |  1.055 % |
c |      7306 |  246689   577396 |   90451    7285   105083    14.4 |  1.089 % |
c ==============================================================================
c [1mFound solution: 47085915[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7349 |  246710   577456 |   82236    7328   105520    14.4 |  1.089 % |
c |      7452 |  246710   577456 |   90459    7431   107688    14.5 |  1.090 % |
c |      7603 |  246710   577456 |   99505    7582   110295    14.5 |  1.090 % |
c ==============================================================================
c [1mFound solution: 44602157[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7643 |  246761   577605 |   82253    7622   110961    14.6 |  1.090 % |
c |      7744 |  246761   577605 |   90478    7723   111503    14.4 |  1.091 % |
c |      7894 |  246761   577605 |   99526    7873   114029    14.5 |  1.091 % |
c |      8120 |  246761   577605 |  109478    8099   116121    14.3 |  1.091 % |
c |      8458 |  246761   577605 |  120426    8437   121174    14.4 |  1.091 % |
c |      8964 |  246761   577605 |  132469    8943   140295    15.7 |  1.091 % |
c |      9723 |  246713   577497 |  145716    9698   160602    16.6 |  1.105 % |
c ==============================================================================
c [1mFound solution: 43117436[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10758 |  246413   576829 |   82137   10726   172946    16.1 |  1.105 % |
c |     10859 |  246381   576755 |   90350   10825   177797    16.4 |  1.228 % |
c ==============================================================================
c [1mFound solution: 38341632[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10911 |  246445   576993 |   82148   10877   179492    16.5 |  1.228 % |
c |     11011 |  246445   576993 |   90362   10977   189352    17.2 |  1.229 % |
c |     11162 |  246445   576993 |   99399   11128   194545    17.5 |  1.229 % |
c |     11387 |  246445   576993 |  109338   11353   205177    18.1 |  1.229 % |
c ==============================================================================
c [1mFound solution: 35700986[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11451 |  246500   577138 |   82166   11417   206570    18.1 |  1.229 % |
c |     11552 |  246500   577138 |   90382   11518   211394    18.4 |  1.230 % |
c |     11702 |  246473   577079 |   99420   11667   213352    18.3 |  1.239 % |
c |     11928 |  246473   577079 |  109362   11893   217733    18.3 |  1.239 % |
c |     12266 |  246228   576531 |  120299   12227   220451    18.0 |  1.313 % |
c ==============================================================================
c [1mFound solution: 29162936[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12282 |  246318   576755 |   82106   12243   220850    18.0 |  1.313 % |
c ==============================================================================
c [1mFound solution: 28818010[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12306 |  246341   576816 |   82113   12267   221457    18.1 |  1.313 % |
c |     12406 |  246341   576816 |   90324   12367   227128    18.4 |  1.315 % |
c |     12556 |  246341   576816 |   99356   12517   240047    19.2 |  1.315 % |
c |     12781 |  246341   576816 |  109292   12742   249695    19.6 |  1.315 % |
c |     13119 |  246341   576816 |  120221   13080   273178    20.9 |  1.315 % |
c |     13625 |  246305   576737 |  132243   13584   291747    21.5 |  1.326 % |
c |     14385 |  246305   576737 |  145468   14344   421666    29.4 |  1.326 % |
c ==============================================================================
c [1mFound solution: 27811840[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14935 |  246168   576442 |   82056   14861   451718    30.4 |  1.326 % |
c |     15035 |  246168   576442 |   90261   14961   458151    30.6 |  1.387 % |
c |     15185 |  246168   576442 |   99287   15111   473156    31.3 |  1.387 % |
c |     15414 |  246168   576442 |  109216   15340   492350    32.1 |  1.387 % |
c |     15751 |  246168   576442 |  120138   15677   502654    32.1 |  1.387 % |
c |     16259 |  246138   576375 |  132152   16181   514597    31.8 |  1.397 % |
c |     17018 |  246138   576375 |  145367   16940   530603    31.3 |  1.397 % |
c ==============================================================================
c [1mFound solution: 27486201[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17219 |  246181   576484 |   82060   17141   574441    33.5 |  1.397 % |
c ==============================================================================
c [1mFound solution: 26736640[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17237 |  246199   576531 |   82066   17159   580599    33.8 |  1.397 % |
c |     17337 |  246199   576531 |   90272   17259   582604    33.8 |  1.398 % |
c |     17487 |  246199   576531 |   99299   17409   593424    34.1 |  1.398 % |
c |     17712 |  246183   576496 |  109229   17631   634871    36.0 |  1.403 % |
c |     18050 |  246183   576496 |  120152   17969   667698    37.2 |  1.403 % |
c |     18556 |  246183   576496 |  132168   18475   712989    38.6 |  1.403 % |
c |     19315 |  245813   575658 |  145384   19220   766158    39.9 |  1.529 % |
c ==============================================================================
c [1mFound solution: 25860848[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19568 |  245849   575750 |   81949   19473   776405    39.9 |  1.529 % |
c |     19668 |  245849   575750 |   90143   19573   781991    40.0 |  1.530 % |
c |     19818 |  245849   575750 |   99158   19723   793227    40.2 |  1.530 % |
c |     20044 |  245849   575750 |  109074   19949   816105    40.9 |  1.530 % |
c |     20382 |  245755   575540 |  119981   20274   827520    40.8 |  1.559 % |
c |     20890 |  245755   575540 |  131979   20782   939777    45.2 |  1.559 % |
c |     21651 |  245755   575540 |  145177   21543   986826    45.8 |  1.559 % |
c ==============================================================================
c [1mFound solution: 25036840[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21707 |  245768   575574 |   81922   21596   987544    45.7 |  1.559 % |
c ==============================================================================
c [1mFound solution: 24012840[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21712 |  245800   575656 |   81933   21601   988103    45.7 |  1.559 % |
c ==============================================================================
c [1mFound solution: 22640640[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21744 |  245821   575712 |   81940   21633   989391    45.7 |  1.559 % |
c |     21844 |  245821   575712 |   90134   21733   992254    45.7 |  1.566 % |
c |     21994 |  245817   575703 |   99147   21882   992899    45.4 |  1.568 % |
c |     22219 |  245610   575234 |  109062   22102  1004170    45.4 |  1.636 % |
c |     22556 |  245610   575234 |  119968   22439  1034715    46.1 |  1.636 % |
c |     23062 |  245610   575234 |  131965   22945  1065473    46.4 |  1.636 % |
c |     23821 |  245610   575234 |  145161   23704  1114638    47.0 |  1.636 % |
c |     24960 |  245610   575234 |  159677   24843  1137537    45.8 |  1.636 % |
c |     26669 |  245610   575234 |  175645   26552  1257092    47.3 |  1.636 % |
c |     29232 |  245610   575234 |  193210   29115  1377406    47.3 |  1.636 % |
c |     33077 |  245610   575234 |  212531   32960  1607439    48.8 |  1.636 % |
c ==============================================================================
c [1mFound solution: 21642240[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36344 |  245635   575301 |   81878   36227  1831204    50.5 |  1.636 % |
c |     36444 |  245635   575301 |   90065   36327  1835433    50.5 |  1.637 % |
c |     36594 |  245635   575301 |   99072   36477  1849218    50.7 |  1.637 % |
c |     36823 |  245635   575301 |  108979   36706  1861752    50.7 |  1.637 % |
c |     37161 |  245635   575301 |  119877   37044  1892278    51.1 |  1.637 % |
c |     37667 |  245635   575301 |  131865   37550  1918629    51.1 |  1.637 % |
c |     38427 |  245635   575301 |  145051   38310  1970730    51.4 |  1.637 % |
c |     39566 |  245635   575301 |  159557   39449  2053390    52.1 |  1.637 % |
c |     41275 |  245635   575301 |  175512   41158  2249325    54.7 |  1.637 % |
c |     43839 |  245498   574990 |  193064   43717  2344544    53.6 |  1.685 % |
c |     47683 |  245451   574885 |  212370   47558  2554400    53.7 |  1.700 % |
c |     53449 |  245425   574826 |  233607   53322  2987332    56.0 |  1.708 % |
c |     62099 |  245425   574826 |  256968   61972  3566467    57.5 |  1.708 % |
c |     75074 |  245318   574589 |  282665   74924  4460326    59.5 |  1.759 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10896 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.88 0.97 0.94 1/54 10892
Raw data (stat): 10892 (runsolver) R 10891 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783470914 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.90 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.001 s]
Raw data (loadavg): 0.91 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.0017 s]
Raw data (loadavg): 0.93 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.0015 s]
Raw data (loadavg): 0.94 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.0013 s]
Raw data (loadavg): 0.95 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.0013 s]
Raw data (loadavg): 0.95 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.0015 s]
Raw data (loadavg): 0.96 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.0018 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.0013 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+220.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+230.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+240.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+250.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+260.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+270.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+280.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+290.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+300.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+310.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+320 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+330.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+340.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+350.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+360.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+370.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+380.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+390.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+400.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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+420 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.011 s]
Raw data (loadavg): 1.07 0.99 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.011 s]
Raw data (loadavg): 1.06 0.99 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.011 s]
Raw data (loadavg): 1.05 0.99 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.012 s]
Raw data (loadavg): 1.04 0.99 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.03 0.99 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.03 0.99 0.94 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.10 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.08 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.07 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.06 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.05 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.04 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.01 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.5 s]
Raw data (loadavg): 1.00 1.00 0.95 1/53 10896
Raw data (stat): 10892 (minisat+_script) S 10891 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783470914 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.5
CPU time (s): 1229.86
CPU user time (s): 1229.34
CPU system time (s): 0.516921
CPU usage (%): 100.029
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####