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-ran10x12.opb
MD5SUM	ddd1f838c1e3a248aad1987162b1d40d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	656964
Optimality of the best value was proved	NO
Number of terms in the objective function	2520
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	666682247
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	666682247
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	1175.04
Number of variables	2520
Total number of constraints	142
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	142
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 31261

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-05-25 23:37:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22664 boxname=wulflinc8 idbench=1480 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  ddd1f838c1e3a248aad1987162b1d40d  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x12.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x12.opb
IDLAUNCH: 22664
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        348160 kB
Buffers:         37668 kB
Cached:         622612 kB
SwapCached:          0 kB
Active:          33684 kB
Inactive:       633572 kB
HighTotal:      131008 kB
HighFree:         7812 kB
LowTotal:       903652 kB
LowFree:        340348 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7068 kB
Slab:            13704 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:57:36 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22664 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 164 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 162]---> Adder-cost: 222   maxlim: 13044   bits: 14/14
c ---[ 160]---> Adder-cost: 230   maxlim: 20340   bits: 15/15
c ---[ 158]---> Adder-cost: 230   maxlim: 19188   bits: 15/15
c ---[ 156]---> Adder-cost: 230   maxlim: 20852   bits: 15/15
c ---[ 154]---> Adder-cost: 222   maxlim: 13812   bits: 14/14
c ---[ 152]---> Adder-cost: 222   maxlim: 13556   bits: 14/14
c ---[ 150]---> Adder-cost: 230   maxlim: 19444   bits: 15/15
c ---[ 148]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 146]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 144]---> Adder-cost: 222   maxlim: 13300   bits: 14/14
c ---[ 142]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Adder-cost: 196   maxlim: 16758   bits: 15/15
c ---[ 132]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   10
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   10
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   13
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   10
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   10
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   16
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   10
c ---[  60]---> BDD-cost:   17
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   10
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   10
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71854   188428 |   23951       0        0     nan |  0.000 % |
c |       100 |   71772   188245 |   26346      89      483     5.4 |  9.032 % |
c |       250 |   71292   187145 |   28980     231     1112     4.8 |  9.655 % |
c |       475 |   71276   187093 |   31878     454     2215     4.9 |  9.667 % |
c |       813 |   70929   186305 |   35066     770     3716     4.8 | 10.075 % |
c |      1319 |   70929   186305 |   38573    1276     5968     4.7 | 10.075 % |
c |      2078 |   70905   186237 |   42430    2030     9447     4.7 | 10.096 % |
c |      3218 |   70582   185459 |   46673    3157    14875     4.7 | 10.467 % |
c |      4926 |   69741   183406 |   51341    4815    24261     5.0 | 11.489 % |
c |      7489 |   69312   182361 |   56475    7343    37294     5.1 | 11.994 % |
c |     11333 |   67979   179228 |   62122   11074    58131     5.2 | 13.681 % |
c ==============================================================================
c [1mFound solution: 2950330[0m
c ---[   0]---> Adder-cost: 4798   maxlim: 969933   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12019 |  101372   298643 |   33790   11740    62732     5.3 | 13.681 % |
c |     12123 |  101372   298643 |   37169   11843    63303     5.3 | 11.519 % |
c |     12273 |  101354   298595 |   40885   11991    63970     5.3 | 11.529 % |
c |     12498 |  101354   298595 |   44974   12216    65070     5.3 | 11.529 % |
c |     12836 |  101354   298595 |   49471   12554    66909     5.3 | 11.529 % |
c |     13344 |  101354   298595 |   54419   13062    70190     5.4 | 11.529 % |
c |     14106 |  101211   298233 |   59861   13816    74433     5.4 | 11.666 % |
c |     15245 |  101183   298163 |   65847   14952    82206     5.5 | 11.690 % |
c |     16953 |  100955   297597 |   72431   16641    94324     5.7 | 11.939 % |
c ==============================================================================
c [1mFound solution: 2802740[0m
c ---[   0]---> Adder-cost: 2   maxlim: 1117523   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19039 |  100956   297694 |   33652   18719   117106     6.3 | 11.939 % |
c |     19139 |  100956   297694 |   37017   18819   117642     6.3 | 11.986 % |
c |     19289 |  100901   297552 |   40718   18950   118739     6.3 | 12.042 % |
c |     19515 |  100901   297552 |   44790   19176   120894     6.3 | 12.042 % |
c |     19852 |  100892   297523 |   49269   19512   123644     6.3 | 12.049 % |
c |     20358 |  100884   297497 |   54196   20017   127585     6.4 | 12.053 % |
c |     21117 |  100855   297402 |   59616   20772   133416     6.4 | 12.074 % |
c |     22256 |  100772   297187 |   65578   21903   141784     6.5 | 12.165 % |
c |     23964 |  100686   296943 |   72136   23604   178358     7.6 | 12.242 % |
c |     26526 |  100686   296943 |   79349   26166   454561    17.4 | 12.242 % |
c ==============================================================================
c [1mFound solution: 2698613[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1221650   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28013 |  100583   296801 |   33527   27634   489957    17.7 | 12.242 % |
c |     28113 |  100583   296801 |   36879   27734   490588    17.7 | 12.381 % |
c |     28263 |  100583   296801 |   40567   27884   491780    17.6 | 12.381 % |
c |     28488 |  100583   296801 |   44624   28109   495046    17.6 | 12.381 % |
c |     28825 |  100583   296801 |   49086   28446   497849    17.5 | 12.381 % |
c |     29332 |  100564   296756 |   53995   28951   536007    18.5 | 12.406 % |
c ==============================================================================
c [1mFound solution: 2585248[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1335015   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29494 |  100563   296875 |   33521   29112   538417    18.5 | 12.406 % |
c |     29594 |  100531   296804 |   36873   29209   539003    18.5 | 12.488 % |
c |     29744 |  100258   296174 |   40560   29291   539674    18.4 | 12.796 % |
c |     29969 |  100112   295837 |   44616   29515   542606    18.4 | 12.974 % |
c |     30306 |  100112   295837 |   49078   29852   566780    19.0 | 12.974 % |
c |     30812 |  100036   295655 |   53985   30352   571159    18.8 | 13.044 % |
c |     31571 |  100027   295624 |   59384   31109   579760    18.6 | 13.047 % |
c |     32710 |   99680   294794 |   65322   32222   596929    18.5 | 13.432 % |
c |     34419 |   99680   294794 |   71855   33931   787069    23.2 | 13.432 % |
c ==============================================================================
c [1mFound solution: 2443672[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1476591   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35364 |   99607   294718 |   33202   34864   807217    23.2 | 13.432 % |
c |     35464 |   99591   294683 |   36522   34960   807928    23.1 | 13.556 % |
c |     35615 |   99591   294683 |   40174   35111   809396    23.1 | 13.556 % |
c |     35841 |   99591   294683 |   44191   35337   811724    23.0 | 13.556 % |
c |     36178 |   99521   294521 |   48611   35662   819237    23.0 | 13.632 % |
c ==============================================================================
c [1mFound solution: 2165210[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1755053   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36647 |   99542   294703 |   33180   36131   829323    23.0 | 13.632 % |
c |     36747 |   99440   294473 |   36498   36221   829993    22.9 | 13.769 % |
c |     36897 |   99440   294473 |   40147   36371   833862    22.9 | 13.769 % |
c |     37122 |   99440   294473 |   44162   36596   837156    22.9 | 13.769 % |
c |     37459 |   99440   294473 |   48578   36933   843815    22.8 | 13.769 % |
c |     37965 |   99386   294332 |   53436   37432   854608    22.8 | 13.811 % |
c |     38726 |   99386   294332 |   58780   38193   896115    23.5 | 13.811 % |
c |     39865 |   99386   294332 |   64658   39332  1011513    25.7 | 13.811 % |
c |     41574 |   99386   294332 |   71124   41041  1057780    25.8 | 13.811 % |
c |     44138 |   99386   294332 |   78236   43605  1391279    31.9 | 13.811 % |
c ==============================================================================
c [1mFound solution: 1277552[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2642711   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45814 |   99350   293826 |   33116   45272  1454878    32.1 | 13.811 % |
c |     45914 |   99334   293789 |   36427   20561   707515    34.4 | 13.851 % |
c |     46065 |   99313   293740 |   40070   20711   708554    34.2 | 13.872 % |
c |     46291 |   99313   293740 |   44077   20937   709806    33.9 | 13.872 % |
c |     46628 |   99313   293740 |   48485   21274   712617    33.5 | 13.872 % |
c |     47136 |   99313   293740 |   53333   21782   718896    33.0 | 13.872 % |
c |     47895 |   99299   293708 |   58667   22539   743656    33.0 | 13.886 % |
c |     49035 |   99299   293708 |   64533   23679   808196    34.1 | 13.886 % |
c |     50744 |   99189   293451 |   70987   25365   833733    32.9 | 13.998 % |
c |     53306 |   99178   293426 |   78085   27926   960091    34.4 | 14.009 % |
c |     57150 |   99154   293371 |   85894   31769  1101818    34.7 | 14.033 % |
c |     62916 |   99067   293155 |   94483   37525  1251382    33.3 | 14.120 % |
c |     71566 |   99010   293022 |  103932   46168  1559284    33.8 | 14.190 % |
c |     84540 |   98894   292754 |  114325   59139  2427787    41.1 | 14.330 % |
c |    104002 |   98880   292723 |  125757   78598  3347089    42.6 | 14.344 % |
c |    133197 |   98880   292723 |  138333  107793  6808231    63.2 | 14.344 % |
c |    176986 |   98485   291804 |  152167   27387   873164    31.9 | 14.790 % |
c |    242670 |   98447   291705 |  167383   93066  6833293    73.4 | 14.832 % |
c |    341196 |   98154   291024 |  184122   28531  1620958    56.8 | 15.143 % |
c ==============================================================================
c [1mFound solution: 1084717[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2835546   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    441705 |   97687   290039 |   32562  128961  7360631    57.1 | 15.143 % |
c |    441805 |   97687   290039 |   35818   23728   802967    33.8 | 15.693 % |
c |    441955 |   97640   289931 |   39400   23874   803609    33.7 | 15.753 % |
c |    442180 |   97640   289931 |   43340   24099   809907    33.6 | 15.753 % |
c |    442517 |   97640   289931 |   47674   24436   819386    33.5 | 15.753 % |
c |    443025 |   97640   289931 |   52441   24944   825160    33.1 | 15.753 % |
c |    443784 |   97640   289931 |   57685   25703   905240    35.2 | 15.753 % |
c |    444925 |   97640   289931 |   63454   26844   928234    34.6 | 15.753 % |
c |    446633 |   97640   289931 |   69799   28552  1071065    37.5 | 15.753 % |
c |    449196 |   97640   289931 |   76779   31115  1200456    38.6 | 15.753 % |
c |    453041 |   97640   289931 |   84457   34960  1387575    39.7 | 15.753 % |
c |    458807 |   97632   289912 |   92903   40725  1545545    38.0 | 15.763 % |
c |    467460 |   97568   289764 |  102193   49372  2122274    43.0 | 15.836 % |
c |    480434 |   97495   289591 |  112412   62341  4299541    69.0 | 15.920 % |
c |    499895 |   97467   289527 |  123654   81800  5459223    66.7 | 15.952 % |
c |    529087 |   97399   289369 |  136019  110985  7534881    67.9 | 16.039 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 23432 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.98 0.92 2/54 23428
Raw data (stat): 23428 (runsolver) R 23427 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 771105757 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0009 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0032 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0044 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0056 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0063 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.034 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.035 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.035 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.035 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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): 1.02 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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): 1.01 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.039 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.039 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.84 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 23432
Raw data (stat): 23428 (minisat+_script) S 23427 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 771105757 2174976 226 4294967295 134512640 135087896 3221224544 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.84
CPU time (s): 1229.87
CPU user time (s): 1228.83
CPU system time (s): 1.03684
CPU usage (%): 100.003
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####