PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10a.opb
MD5SUM	133d42fd76e8bbd92509939943f41498
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	398336
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	539671039
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	539671039
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	913.784
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 31258

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-05-25 23:36:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22661 boxname=wulflinc29 idbench=1477 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  133d42fd76e8bbd92509939943f41498  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran10x10a.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran10x10a.opb
IDLAUNCH: 22661
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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	: 3
cpu MHz		: 451.020
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:        773172 kB
Buffers:         32188 kB
Cached:         207672 kB
SwapCached:        452 kB
Active:          24412 kB
Inactive:       217744 kB
HighTotal:      131008 kB
HighFree:        65240 kB
LowTotal:       903652 kB
LowFree:        707932 kB
SwapTotal:     2097892 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5612 kB
Slab:            13788 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 23:56:38 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22661 7 1229.89 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]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 136]---> Adder-cost: 178   maxlim: 8694   bits: 14/14
c ---[ 134]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 2042     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 194   maxlim: 16374   bits: 15/14
c ---[ 112]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 194   maxlim: 16246   bits: 15/14
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   10
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   12
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   12
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   12
c ---[  17]---> BDD-cost:   12
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   12
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78256   193024 |   26085       0        0     nan |  0.000 % |
c |       100 |   78239   192973 |   28693      99      396     4.0 |  7.452 % |
c |       250 |   77991   192412 |   31562     220      889     4.0 |  7.702 % |
c |       475 |   77683   191705 |   34719     430     1908     4.4 |  8.048 % |
c |       812 |   77639   191604 |   38191     765     3590     4.7 |  8.096 % |
c |      1318 |   77639   191604 |   42010    1271     6232     4.9 |  8.096 % |
c |      2077 |   77341   190885 |   46211    2004    10094     5.0 |  8.415 % |
c |      3216 |   76891   189822 |   50832    3109    15662     5.0 |  8.886 % |
c |      4924 |   76891   189822 |   55915    4817    25706     5.3 |  8.886 % |
c ==============================================================================
c [1mFound solution: 1787021[0m
c ---[   0]---> Adder-cost: 3925   maxlim: 638322   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5301 |  104280   287702 |   34760    5194    27799     5.4 |  8.886 % |
c |      5401 |  104255   287621 |   38236    5290    28190     5.3 |  7.820 % |
c |      5551 |  104239   287569 |   42059    5437    28861     5.3 |  7.830 % |
c |      5776 |  104232   287546 |   46265    5661    29929     5.3 |  7.833 % |
c |      6113 |  103995   286987 |   50892    5994    31788     5.3 |  8.077 % |
c |      6619 |  103847   286624 |   55981    6495    34774     5.4 |  8.234 % |
c |      7378 |  103847   286624 |   61579    7254    39864     5.5 |  8.234 % |
c ==============================================================================
c [1mFound solution: 1639947[0m
c ---[   0]---> Adder-cost: 0   maxlim: 785396   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7986 |  103687   286434 |   34562    7855    45201     5.8 |  8.234 % |
c |      8086 |  103687   286434 |   38018    7955    45711     5.7 |  8.455 % |
c |      8236 |  103687   286434 |   41820    8105    46914     5.8 |  8.455 % |
c |      8462 |  103687   286434 |   46002    8331    48139     5.8 |  8.455 % |
c |      8799 |  103687   286434 |   50602    8668    50201     5.8 |  8.455 % |
c |      9305 |  103687   286434 |   55662    9174    53245     5.8 |  8.455 % |
c |     10065 |  103553   286131 |   61228    9914    65909     6.6 |  8.576 % |
c |     11204 |  103520   286028 |   67351   11049    72961     6.6 |  8.599 % |
c |     12912 |  103520   286028 |   74086   12757   118605     9.3 |  8.599 % |
c |     15474 |  103352   285610 |   81495   15296   143125     9.4 |  8.756 % |
c ==============================================================================
c [1mFound solution: 1439526[0m
c ---[   0]---> Adder-cost: 0   maxlim: 985817   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16409 |  103347   285690 |   34449   16227   151742     9.4 |  8.756 % |
c |     16510 |  103113   285154 |   37893   16307   152338     9.3 |  9.007 % |
c |     16660 |  103042   284993 |   41683   16451   154734     9.4 |  9.074 % |
c |     16885 |  103042   284993 |   45851   16676   156389     9.4 |  9.074 % |
c |     17223 |  102735   284280 |   50436   16991   158183     9.3 |  9.363 % |
c |     17729 |  102735   284280 |   55480   17497   192784    11.0 |  9.363 % |
c |     18488 |  102693   284175 |   61028   18252   199424    10.9 |  9.404 % |
c |     19628 |  102693   284175 |   67131   19392   239276    12.3 |  9.404 % |
c |     21337 |  102517   283735 |   73844   21069   275781    13.1 |  9.568 % |
c |     23899 |  102456   283571 |   81228   23623   359017    15.2 |  9.623 % |
c ==============================================================================
c [1mFound solution: 1386828[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1038515   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27508 |  102358   283435 |   34119   27207   726320    26.7 |  9.623 % |
c |     27608 |  102358   283435 |   37530   27307   726860    26.6 |  9.748 % |
c |     27758 |  102358   283435 |   41283   27457   731543    26.6 |  9.748 % |
c |     27983 |  102237   283154 |   45412   27657   732755    26.5 |  9.873 % |
c |     28320 |  102237   283154 |   49953   27994   740165    26.4 |  9.873 % |
c |     28826 |  102237   283154 |   54948   28500   772931    27.1 |  9.873 % |
c |     29585 |  102209   283092 |   60443   29253   808194    27.6 |  9.898 % |
c |     30725 |  102209   283092 |   66488   30393   866889    28.5 |  9.898 % |
c |     32434 |  102209   283092 |   73137   32102   927142    28.9 |  9.898 % |
c |     34996 |  102209   283092 |   80450   34664  1252280    36.1 |  9.898 % |
c |     38840 |  102209   283092 |   88495   38508  1419350    36.9 |  9.898 % |
c ==============================================================================
c [1mFound solution: 1383134[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1042209   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39478 |  102081   282870 |   34027   39135  1452696    37.1 |  9.898 % |
c |     39579 |  102081   282870 |   37429   18435   739171    40.1 | 10.043 % |
c |     39729 |  101986   282653 |   41172   18564   739799    39.9 | 10.127 % |
c |     39954 |  101986   282653 |   45289   18789   741338    39.5 | 10.127 % |
c |     40291 |  101920   282500 |   49818   19123   743044    38.9 | 10.200 % |
c |     40800 |  101920   282500 |   54800   19632   774357    39.4 | 10.200 % |
c |     41559 |  101664   281901 |   60280   20378   793484    38.9 | 10.463 % |
c |     42698 |  101551   281639 |   66308   21502   875383    40.7 | 10.569 % |
c |     44406 |  101551   281639 |   72939   23210  1142802    49.2 | 10.569 % |
c ==============================================================================
c [1mFound solution: 1272901[0m
c ---[   0]---> Adder-cost: 2   maxlim: 1152442   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44655 |  101580   281856 |   33860   23459  1147685    48.9 | 10.569 % |
c |     44755 |  101548   281783 |   37246   23556  1148298    48.7 | 10.629 % |
c |     44906 |  101472   281607 |   40970   23706  1149373    48.5 | 10.700 % |
c |     45131 |  101472   281607 |   45067   23931  1151026    48.1 | 10.700 % |
c |     45468 |  101472   281607 |   49574   24268  1154330    47.6 | 10.700 % |
c |     45974 |  101472   281607 |   54531   24774  1165653    47.1 | 10.700 % |
c |     46733 |  101472   281607 |   59985   25533  1194292    46.8 | 10.700 % |
c |     47874 |  101472   281607 |   65983   26674  1320673    49.5 | 10.700 % |
c ==============================================================================
c [1mFound solution: 1071477[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1353866   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48273 |  101484   281730 |   33828   27073  1349463    49.8 | 10.700 % |
c |     48374 |  101484   281730 |   37210   27174  1351300    49.7 | 10.721 % |
c |     48524 |  101434   281615 |   40931   27312  1352183    49.5 | 10.766 % |
c |     48749 |  101434   281615 |   45025   27537  1359198    49.4 | 10.766 % |
c ==============================================================================
c [1mFound solution: 788737[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1636606   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48964 |  101444   281806 |   33814   27750  1367751    49.3 | 10.766 % |
c |     49064 |  101285   281440 |   37195   27843  1368576    49.2 | 10.989 % |
c |     49214 |  101285   281440 |   40914   27993  1370353    49.0 | 10.989 % |
c |     49439 |  101285   281440 |   45006   28218  1384131    49.1 | 10.989 % |
c |     49776 |  101278   281420 |   49507   28456  1385192    48.7 | 10.992 % |
c ==============================================================================
c [1mFound solution: 659299[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1766044   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49924 |  101297   281590 |   33765   28604  1400768    49.0 | 10.992 % |
c |     50024 |  101264   281517 |   37141   28701  1401288    48.8 | 11.052 % |
c |     50174 |  101264   281517 |   40855   28851  1402110    48.6 | 11.052 % |
c |     50399 |  101226   281428 |   44941   29074  1404538    48.3 | 11.094 % |
c |     50738 |  101226   281428 |   49435   29413  1408586    47.9 | 11.094 % |
c |     51245 |  101226   281428 |   54378   29920  1461313    48.8 | 11.094 % |
c |     52005 |  101226   281428 |   59816   30680  1505950    49.1 | 11.094 % |
c |     53144 |  101226   281428 |   65798   31819  1541320    48.4 | 11.094 % |
c |     54852 |  101226   281428 |   72378   33527  1648247    49.2 | 11.094 % |
c |     57414 |  101226   281428 |   79616   36089  1721769    47.7 | 11.094 % |
c |     61258 |  101221   281417 |   87577   39932  1850180    46.3 | 11.100 % |
c |     67024 |  101151   281251 |   96335   45656  2366915    51.8 | 11.164 % |
c |     75674 |  101018   280948 |  105969   54297  2728916    50.3 | 11.283 % |
c |     88651 |  101018   280948 |  116565   67274  6239872    92.8 | 11.283 % |
c |    108112 |  100838   280531 |  128222   86703 11448514   132.0 | 11.459 % |
c |    137307 |  100616   280022 |  141044  115877 14414127   124.4 | 11.673 % |
c |    181096 |  100587   279956 |  155149   25399  4141424   163.1 | 11.702 % |
c |    246781 |  100354   279418 |  170664   91058 12693154   139.4 | 11.951 % |
c |    345308 |  100064   278749 |  187730   26575  1057745    39.8 | 12.236 % |
c ==============================================================================
c [1mFound solution: 467356[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1957987   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    362478 |  100031   278747 |   33343   43741  2964852    67.8 | 12.236 % |
c |    362578 |  100019   278719 |   36677   18288  1527137    83.5 | 12.324 % |
c |    362730 |  100019   278719 |   40345   18440  1527940    82.9 | 12.324 % |
c |    362956 |  100019   278719 |   44379   18666  1529106    81.9 | 12.324 % |
c |    363293 |   99853   278334 |   48817   18994  1530964    80.6 | 12.494 % |
c |    363799 |   99853   278334 |   53699   19500  1548356    79.4 | 12.494 % |
c |    364559 |   99853   278334 |   59069   20260  1586950    78.3 | 12.494 % |
c |    365698 |   99803   278214 |   64976   21397  1596629    74.6 | 12.545 % |
c |    367406 |   99803   278214 |   71473   23105  1786753    77.3 | 12.545 % |
c |    369969 |   99775   278150 |   78621   25667  1849032    72.0 | 12.574 % |
c |    373814 |   99770   278139 |   86483   29511  1960065    66.4 | 12.580 % |
c |    379581 |   99694   277967 |   95131   35273  2402215    68.1 | 12.653 % |
c |    388232 |   99694   277967 |  104644   43924  2804050    63.8 | 12.653 % |
c |    401206 |   99653   277873 |  115109   56889  4266349    75.0 | 12.692 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  6154 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.94 2/54 6150
Raw data (stat): 6150 (runsolver) R 6149 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842882733 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.0011 s]
Raw data (loadavg): 0.94 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.0022 s]
Raw data (loadavg): 0.95 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.002 s]
Raw data (loadavg): 0.95 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.0025 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.0025 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.0024 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.0029 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.0029 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 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.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.76 s]
Raw data (loadavg): 0.99 0.97 0.94 1/53 6154
Raw data (stat): 6150 (minisat+_script) S 6149 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842882733 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.76
CPU time (s): 1229.89
CPU user time (s): 1228.82
CPU system time (s): 1.07284
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####