PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-05-25 17:39:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21949 boxname=wulflinc11 idbench=367 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  f82b685b64af240616b701a750c82883  /oldhome/oroussel/tmp/wulflinc11/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-10:20:4.5:0.95:100.opb
IDLAUNCH: 21949
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        790336 kB
Buffers:         34332 kB
Cached:         189068 kB
SwapCached:        796 kB
Active:          76616 kB
Inactive:       148912 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        790084 kB
SwapTotal:     2097136 kB
SwapFree:      2095468 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5032 kB
Slab:            13220 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 18:00:26 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21949 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1062 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   20
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   17
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   17
c ---[ 176]---> BDD-cost:   17
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:    5
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   21
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   38
c ---[ 164]---> BDD-cost:   29
c ---[ 163]---> BDD-cost:   29
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   20
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   17
c ---[ 156]---> BDD-cost:   20
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:   35
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   41
c ---[ 149]---> BDD-cost:   38
c ---[ 148]---> BDD-cost:   36
c ---[ 147]---> BDD-cost:   32
c ---[ 146]---> BDD-cost:   32
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   29
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:   21
c ---[ 135]---> BDD-cost:   29
c ---[ 134]---> BDD-cost:   35
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   44
c ---[ 131]---> BDD-cost:   44
c ---[ 130]---> BDD-cost:   44
c ---[ 129]---> BDD-cost:   38
c ---[ 128]---> BDD-cost:   38
c ---[ 127]---> BDD-cost:   32
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   32
c ---[ 124]---> BDD-cost:   38
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   20
c ---[ 120]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:    7
c ---[ 117]---> BDD-cost:    5
c ---[ 116]---> BDD-cost:   29
c ---[ 115]---> BDD-cost:   32
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   44
c ---[ 112]---> BDD-cost:   50
c ---[ 111]---> BDD-cost:   41
c ---[ 110]---> BDD-cost:   42
c ---[ 109]---> BDD-cost:   38
c ---[ 108]---> BDD-cost:   41
c ---[ 107]---> BDD-cost:   35
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:   38
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:   32
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   41
c ---[  93]---> BDD-cost:   41
c ---[  92]---> BDD-cost:   47
c ---[  91]---> BDD-cost:   50
c ---[  90]---> BDD-cost:   53
c ---[  89]---> BDD-cost:   47
c ---[  88]---> BDD-cost:   38
c ---[  87]---> BDD-cost:   38
c ---[  86]---> BDD-cost:   35
c ---[  85]---> BDD-cost:   32
c ---[  84]---> BDD-cost:   32
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   32
c ---[  81]---> BDD-cost:   32
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   29
c ---[  74]---> BDD-cost:   32
c ---[  73]---> BDD-cost:   41
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:   44
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   32
c ---[  66]---> BDD-cost:   32
c ---[  65]---> BDD-cost:   32
c ---[  64]---> BDD-cost:   33
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   38
c ---[  50]---> BDD-cost:   32
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   29
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   20
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   20
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   20
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11765    33737 |    3921       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1032[0m
c ---[   0]---> Adder-cost: 2083   maxlim: 470   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26254    85464 |    8751       0        0     nan |  0.000 % |
c |       100 |   26254    85464 |    9626     100      343     3.4 |  2.467 % |
c |       250 |   26254    85464 |   10588     250     1104     4.4 |  2.467 % |
c |       475 |   26254    85464 |   11647     475     2363     5.0 |  2.467 % |
c ==============================================================================
c [1mFound solution: 181[0m
c ---[   0]---> Adder-cost: 6   maxlim: 1321   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       598 |   26298    85623 |    8766     598     3233     5.4 |  2.467 % |
c |       698 |   26298    85623 |    9642     698     3737     5.4 |  2.528 % |
c |       848 |   26298    85623 |   10606     848     4598     5.4 |  2.528 % |
c ==============================================================================
c [1mFound solution: 163[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1339   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       947 |   26301    85653 |    8767     947     5260     5.6 |  2.528 % |
c |      1047 |   26301    85653 |    9643    1047    10883    10.4 |  2.566 % |
c |      1197 |   26301    85653 |   10608    1197    11640     9.7 |  2.566 % |
c |      1423 |   26301    85653 |   11668    1423    12608     8.9 |  2.566 % |
c |      1761 |   26301    85653 |   12835    1761    20677    11.7 |  2.566 % |
c |      2267 |   26301    85653 |   14119    2267    25319    11.2 |  2.566 % |
c |      3026 |   26301    85653 |   15531    3026    32992    10.9 |  2.566 % |
c |      4165 |   26301    85653 |   17084    4165    76574    18.4 |  2.566 % |
c ==============================================================================
c [1mFound solution: 156[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1346   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5406 |   26304    85685 |    8768    5406   109895    20.3 |  2.566 % |
c |      5506 |   26304    85685 |    9644    5506   110609    20.1 |  2.604 % |
c |      5656 |   26304    85685 |   10609    5656   111837    19.8 |  2.604 % |
c |      5881 |   26304    85685 |   11670    5881   113973    19.4 |  2.604 % |
c |      6218 |   26304    85685 |   12837    6218   131714    21.2 |  2.604 % |
c |      6725 |   26304    85685 |   14120    6725   140326    20.9 |  2.604 % |
c ==============================================================================
c [1mFound solution: 153[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1349   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6834 |   26307    85710 |    8769    6834   141638    20.7 |  2.604 % |
c |      6935 |   26307    85710 |    9645    6935   142296    20.5 |  2.629 % |
c |      7085 |   26307    85710 |   10610    7085   145694    20.6 |  2.629 % |
c |      7311 |   26307    85710 |   11671    7311   150011    20.5 |  2.629 % |
c |      7648 |   26307    85710 |   12838    7648   156902    20.5 |  2.629 % |
c |      8155 |   26307    85710 |   14122    8155   166831    20.5 |  2.629 % |
c ==============================================================================
c [1mFound solution: 149[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1353   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8193 |   26310    85734 |    8770    8193   167205    20.4 |  2.629 % |
c |      8294 |   26310    85734 |    9647    8294   169827    20.5 |  2.653 % |
c |      8444 |   26310    85734 |   10611    8444   173171    20.5 |  2.653 % |
c ==============================================================================
c [1mFound solution: 119[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1383   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8489 |   26313    85754 |    8771    8489   173868    20.5 |  2.653 % |
c |      8589 |   26313    85754 |    9648    8589   175445    20.4 |  2.678 % |
c |      8741 |   26313    85754 |   10612    8741   179565    20.5 |  2.678 % |
c |      8970 |   26313    85754 |   11674    8970   190687    21.3 |  2.678 % |
c ==============================================================================
c [1mFound solution: 115[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1387   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9032 |   26314    85765 |    8771    9032   191792    21.2 |  2.678 % |
c |      9132 |   26314    85765 |    9648    4616    65488    14.2 |  2.691 % |
c |      9282 |   26314    85765 |   10612    4766    68161    14.3 |  2.691 % |
c |      9507 |   26314    85765 |   11674    4991    71384    14.3 |  2.691 % |
c ==============================================================================
c [1mFound solution: 99[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1403   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9579 |   26319    85799 |    8773    5063    72243    14.3 |  2.691 % |
c |      9679 |   26319    85799 |    9650    5163    75617    14.6 |  2.727 % |
c |      9829 |   26319    85799 |   10615    5313    81023    15.2 |  2.727 % |
c |     10054 |   26319    85799 |   11676    5538    85759    15.5 |  2.727 % |
c |     10391 |   26319    85799 |   12844    5875   102244    17.4 |  2.727 % |
c |     10899 |   26319    85799 |   14129    6383   114696    18.0 |  2.727 % |
c |     11660 |   26319    85799 |   15541    7144   153240    21.5 |  2.727 % |
c |     12803 |   26319    85799 |   17096    8287   178552    21.5 |  2.727 % |
c |     14511 |   26319    85799 |   18805    9995   335353    33.6 |  2.727 % |
c |     17073 |   26319    85799 |   20686   12557   429140    34.2 |  2.727 % |
c |     20918 |   26319    85799 |   22754   16402   711043    43.4 |  2.727 % |
c |     26684 |   26319    85799 |   25030   22168  1226739    55.3 |  2.727 % |
c |     35333 |   26319    85799 |   27533   17951  1054818    58.8 |  2.727 % |
c |     48307 |   26319    85799 |   30286   30925  2515081    81.3 |  2.727 % |
c |     67770 |   26319    85799 |   33315   31790  3204216   100.8 |  2.727 % |
c |     96962 |   26319    85799 |   36646   18679  1913143   102.4 |  2.727 % |
c ==============================================================================
c [1mFound solution: 95[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1407   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98583 |   26320    85805 |    8773   20300  1958586    96.5 |  2.727 % |
c |     98683 |   26320    85805 |    9650    5175   155331    30.0 |  2.740 % |
c |     98833 |   26320    85805 |   10615    5325   156444    29.4 |  2.740 % |
c |     99059 |   26320    85805 |   11676    5551   166652    30.0 |  2.740 % |
c |     99396 |   26320    85805 |   12844    5888   171971    29.2 |  2.740 % |
c |     99903 |   26320    85805 |   14129    6395   206962    32.4 |  2.740 % |
c |    100662 |   26320    85805 |   15541    7154   245414    34.3 |  2.740 % |
c |    101801 |   26320    85805 |   17096    8293   299653    36.1 |  2.740 % |
c |    103509 |   26320    85805 |   18805   10001   404090    40.4 |  2.740 % |
c |    106072 |   26320    85805 |   20686   12564   580738    46.2 |  2.740 % |
c |    109916 |   26320    85805 |   22754   16408   859132    52.4 |  2.740 % |
c |    115682 |   26320    85805 |   25030   22174  1205307    54.4 |  2.740 % |
c |    124334 |   26320    85805 |   27533   14392  1232687    85.7 |  2.740 % |
c |    137308 |   26320    85805 |   30286   27366  3191732   116.6 |  2.740 % |
c |    156769 |   26320    85805 |   33315   27184  3327775   122.4 |  2.740 % |
c |    185961 |   26320    85805 |   36646   34727  3023365    87.1 |  2.740 % |
c |    229750 |   26320    85805 |   40311   29036  4174333   143.8 |  2.740 % |
c |    295435 |   26320    85805 |   44342   35733  4821179   134.9 |  2.740 % |
c |    393962 |   26320    85805 |   48777   31245  7114255   227.7 |  2.740 % |
c ==============================================================================
c [1mFound solution: 93[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1409   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    402965 |   26322    85819 |    8774   40248  7669094   190.5 |  2.740 % |
c |    403065 |   26322    85819 |    9651    7692   428249    55.7 |  2.752 % |
c |    403215 |   26322    85819 |   10616    7842   429152    54.7 |  2.752 % |
c |    403440 |   26322    85819 |   11678    8067   430639    53.4 |  2.752 % |
c |    403778 |   26322    85819 |   12846    8405   444954    52.9 |  2.752 % |
c |    404285 |   26322    85819 |   14130    8912   451552    50.7 |  2.752 % |
c |    405044 |   26322    85819 |   15543    9671   460234    47.6 |  2.752 % |
c |    406184 |   26322    85819 |   17098   10811   485817    44.9 |  2.752 % |
c |    407892 |   26322    85819 |   18807   12519   577961    46.2 |  2.752 % |
c |    410455 |   26322    85819 |   20688   15082   703570    46.6 |  2.752 % |
c |    414299 |   26322    85819 |   22757   18926   957487    50.6 |  2.752 % |
c |    420065 |   26322    85819 |   25033   24692  1288839    52.2 |  2.752 % |
c |    428714 |   26322    85819 |   27536   19026  1376838    72.4 |  2.752 % |
c |    441690 |   26322    85819 |   30290   32002  2455886    76.7 |  2.752 % |
c |    461154 |   26322    85819 |   33319   32530  2789845    85.8 |  2.752 % |
c |    490346 |   26322    85819 |   36651   18436  2229327   120.9 |  2.752 % |
c |    534136 |   26322    85819 |   40316   35911  6004074   167.2 |  2.752 % |
c |    599820 |   26322    85819 |   44347   43924  8128207   185.1 |  2.752 % |
c |    698346 |   26322    85819 |   48782   46314  7937399   171.4 |  2.752 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  9923 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.92 0.96 0.92 2/54 9919
Raw data (stat): 9919 (runsolver) R 9918 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782524436 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.0012 s]
Raw data (loadavg): 0.93 0.96 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0021 s]
Raw data (loadavg): 0.95 0.96 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0022 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0027 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0024 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0026 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0028 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.92 2/55 9923
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.92 3/58 9962
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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): 1.07 0.99 0.93 2/55 9976
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.71 s]
Raw data (loadavg): 1.06 0.99 0.93 1/53 9976
Raw data (stat): 9919 (minisat+_script) S 9918 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782524436 2174976 226 4294967295 134512640 135087896 3221224544 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.71
CPU time (s): 1229.85
CPU user time (s): 1229.41
CPU system time (s): 0.446932
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####