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/submitted/een/normalized-p0282.opb
MD5SUM	dd62132555621025f45a5a6099c90742
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	258411
Optimality of the best value was proved	NO
Number of terms in the objective function	282
Biggest coefficient in the objective function	160646
Number of bits for the biggest coefficient in the objective function	18
Sum of the numbers in the objective function	1302615
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	160646
Number of bits of the biggest number in a constraint	18
Biggest sum of numbers in a constraint	1302615
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	282
Total number of constraints	221
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	44
Minimum length of a constraint	2
Maximum length of a constraint	57
Trace number 30590

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        163900 kB
Buffers:         38232 kB
Cached:         802484 kB
SwapCached:        716 kB
Active:          79460 kB
Inactive:       768040 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        163648 kB
SwapTotal:     2097892 kB
SwapFree:      2096336 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5068 kB
Slab:            17556 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 18:16:00 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 21971 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................sss
c ---[  46]---> BDD-cost:    4
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:   10
c ---[  43]---> BDD-cost:   16
c ---[  42]---> Sorter-cost: 1109     Base: 2 5 3 3
c ---[  41]---> Sorter-cost:  898     Base: 2 5 3 2
c ---[  40]---> Sorter-cost: 1116     Base: 2 5 5
c ---[  38]---> Sorter-cost: 1010     Base: 2 5 5
c ---[  37]---> Sorter-cost:  909     Base: 2 5 5
c ---[  36]---> Sorter-cost:  998     Base: 2 5 3 2
c ---[  35]---> Sorter-cost:  852     Base: 2 5 3 3
c ---[  34]---> Sorter-cost:  842     Base: 5 2 3 3
c ---[  33]---> Sorter-cost:  712     Base: 5 2 3 3
c ---[  32]---> Sorter-cost:  946     Base: 2 5 3 3
c ---[  31]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[  30]---> Sorter-cost:  909     Base: 2 5 5
c ---[  29]---> Sorter-cost:  935     Base: 2 5 3 2
c ---[  28]---> Sorter-cost:  998     Base: 2 5 3
c ---[  27]---> Sorter-cost:  762     Base: 5 2 3 3
c ---[  26]---> Sorter-cost:  908     Base: 2 5 5
c ---[  25]---> Sorter-cost:  907     Base: 2 5 5
c ---[  24]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[  23]---> Sorter-cost:  908     Base: 2 5 5
c ---[  22]---> Sorter-cost:  909     Base: 2 5 5
c ---[  21]---> Sorter-cost: 1008     Base: 2 5 3
c ---[  20]---> Sorter-cost:  898     Base: 2 5 3 3
c ---[  19]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[  18]---> Sorter-cost:  760     Base: 2 5 3 3
c ---[  17]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[  16]---> Sorter-cost: 1071     Base: 2 5 3 3
c ---[  15]---> Sorter-cost:  949     Base: 2 5 3 3
c ---[  14]---> BDD-cost:   26
c ---[  13]---> Sorter-cost: 1108     Base: 2 5 3 3
c ---[  11]---> Sorter-cost: 1081     Base: 2 5 3 3
c ---[  10]---> Sorter-cost:  999     Base: 2 5 3 2
c ---[   9]---> Sorter-cost:  995     Base: 2 5 3 3
c ---[   8]---> Sorter-cost:  982     Base: 2 5 3 2
c ---[   7]---> Sorter-cost:  996     Base: 2 5 3 3
c ---[   5]---> BDD-cost:   56
c ---[   4]---> BDD-cost:   56
c ---[   3]---> BDD-cost:   56
c ---[   2]---> BDD-cost:   12
c ---[   1]---> Sorter-cost:  717     Base: 2 5 3
c ---[   0]---> Sorter-cost:  655     Base: 2 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   70255   164891 |   23418       0        0     nan |  0.000 % |
c |       100 |   69917   164139 |   25759      93      577     6.2 |  0.539 % |
c ==============================================================================
c [1mFound solution: 628263[0m
c ---[   0]---> Sorter-cost:77312     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       154 |  289324   676780 |   96441     145     1012     7.0 |  0.539 % |
c |       254 |  289196   676496 |  106085     241     7343    30.5 |  0.195 % |
c |       404 |  289140   676372 |  116693     389     8935    23.0 |  0.210 % |
c |       629 |  289026   676117 |  128362     613    10286    16.8 |  0.239 % |
c |       967 |  288994   676045 |  141199     949    19599    20.7 |  0.248 % |
c |      1473 |  288994   676045 |  155319    1455    26362    18.1 |  0.248 % |
c |      2232 |  288994   676045 |  170851    2214    33093    14.9 |  0.248 % |
c |      3371 |  288854   675733 |  187936    3345   114434    34.2 |  0.285 % |
c |      5080 |  288563   675077 |  206729    5053   138020    27.3 |  0.356 % |
c ==============================================================================
c [1mFound solution: 566001[0m
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5423 |  288839   675889 |   96279    5395   169300    31.4 |  0.356 % |
c |      5523 |  288839   675889 |  105906    5495   170399    31.0 |  0.359 % |
c |      5674 |  288839   675889 |  116497    5646   171301    30.3 |  0.359 % |
c |      5899 |  288743   675673 |  128147    5869   175852    30.0 |  0.384 % |
c |      6236 |  288743   675673 |  140962    6206   177830    28.7 |  0.384 % |
c |      6742 |  288688   675549 |  155058    6711   181373    27.0 |  0.399 % |
c |      7501 |  288688   675549 |  170564    7470   186837    25.0 |  0.399 % |
c |      8640 |  288688   675549 |  187620    8609   216152    25.1 |  0.399 % |
c ==============================================================================
c [1mFound solution: 484674[0m
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10092 |  288996   676700 |   96332   10053   237028    23.6 |  0.399 % |
c |     10193 |  288996   676700 |  105965   10154   237467    23.4 |  0.473 % |
c |     10343 |  288996   676700 |  116561   10304   238188    23.1 |  0.473 % |
c |     10568 |  288996   676700 |  128217   10529   239895    22.8 |  0.473 % |
c |     10905 |  288996   676700 |  141039   10866   248577    22.9 |  0.473 % |
c |     11412 |  288996   676700 |  155143   11373   259298    22.8 |  0.473 % |
c |     12171 |  288851   676374 |  170658   12127   270935    22.3 |  0.512 % |
c |     13310 |  288847   676365 |  187723   13265   320224    24.1 |  0.513 % |
c ==============================================================================
c [1mFound solution: 445249[0m
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14034 |  289183   677345 |   96394   13931   345351    24.8 |  0.513 % |
c |     14134 |  289183   677345 |  106033   14031   345862    24.6 |  0.575 % |
c |     14285 |  289162   677300 |  116636   14181   351345    24.8 |  0.582 % |
c |     14510 |  289162   677300 |  128300   14406   356420    24.7 |  0.582 % |
c |     14847 |  289100   677161 |  141130   14740   360896    24.5 |  0.601 % |
c |     15353 |  288611   676053 |  155243   15228   370340    24.3 |  0.741 % |
c |     16112 |  288611   676053 |  170767   15987   409928    25.6 |  0.741 % |
c |     17255 |  288391   675554 |  187844   17122   447923    26.2 |  0.803 % |
c |     18963 |  288078   674859 |  206629   18820   529203    28.1 |  0.890 % |
c |     21525 |  288034   674761 |  227292   21380   570591    26.7 |  0.902 % |
c |     25371 |  288034   674761 |  250021   25226   640379    25.4 |  0.902 % |
c ==============================================================================
c [1mFound solution: 444335[0m
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26271 |  288407   675860 |   96135   26126   763005    29.2 |  0.902 % |
c |     26371 |  288407   675860 |  105748   26226   763504    29.1 |  0.901 % |
c |     26521 |  288407   675860 |  116323   26375   770197    29.2 |  0.907 % |
c |     26746 |  288386   675814 |  127955   26600   778032    29.2 |  0.907 % |
c |     27085 |  288363   675762 |  140751   26938   780776    29.0 |  0.915 % |
c |     27591 |  288316   675654 |  154826   27443   802878    29.3 |  0.930 % |
c |     28350 |  288316   675654 |  170309   28202   825991    29.3 |  0.930 % |
c |     29489 |  288316   675654 |  187339   29341   845911    28.8 |  0.930 % |
c ==============================================================================
c [1mFound solution: 436563[0m
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30056 |  288324   675691 |   96108   29908   872577    29.2 |  0.930 % |
c |     30156 |  288275   675585 |  105718   30004   876794    29.2 |  0.945 % |
c |     30306 |  288275   675585 |  116290   30154   888553    29.5 |  0.945 % |
c |     30532 |  288203   675424 |  127919   30379   901516    29.7 |  0.964 % |
c |     30870 |  288163   675336 |  140711   30716   915078    29.8 |  0.975 % |
c |     31376 |  288163   675336 |  154782   31222   924876    29.6 |  0.975 % |
c |     32137 |  287950   674856 |  170261   31949   937478    29.3 |  1.036 % |
c |     33276 |  287871   674673 |  187287   33082   954844    28.9 |  1.063 % |
c |     34984 |  287756   674415 |  206016   34788   981681    28.2 |  1.093 % |
c |     37548 |  287736   674370 |  226617   37351  1248671    33.4 |  1.098 % |
c |     41392 |  287637   674148 |  249279   41193  1343488    32.6 |  1.123 % |
c ==============================================================================
c [1mFound solution: 436402[0m
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43764 |  287605   674082 |   95868   43564  1447376    33.2 |  1.123 % |
c |     43867 |  287605   674082 |  105454   43667  1448737    33.2 |  1.133 % |
c |     44018 |  287605   674082 |  116000   43818  1449657    33.1 |  1.133 % |
c |     44244 |  287605   674082 |  127600   44044  1460157    33.2 |  1.133 % |
c |     44581 |  287560   673982 |  140360   44380  1479136    33.3 |  1.145 % |
c |     45088 |  287560   673982 |  154396   44887  1496111    33.3 |  1.145 % |
c |     45848 |  287223   673220 |  169836   45621  1520809    33.3 |  1.238 % |
c |     46988 |  287163   673084 |  186819   46758  1538696    32.9 |  1.256 % |
c |     48697 |  287039   672805 |  205501   48465  1592787    32.9 |  1.289 % |
c |     51261 |  286990   672696 |  226051   51028  1898314    37.2 |  1.303 % |
c |     55105 |  286990   672696 |  248656   54872  2298636    41.9 |  1.303 % |
c |     60871 |  286990   672696 |  273522   60638  2869733    47.3 |  1.303 % |
c ==============================================================================
c [1mFound solution: 435910[0m
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63492 |  286856   672401 |   95618   63256  3040113    48.1 |  1.303 % |
c |     63592 |  286856   672401 |  105179   63356  3040956    48.0 |  1.340 % |
c |     63743 |  286856   672401 |  115697   63507  3046265    48.0 |  1.340 % |
c |     63968 |  286856   672401 |  127267   63732  3058484    48.0 |  1.340 % |
c |     64306 |  286815   672308 |  139994   64069  3075581    48.0 |  1.350 % |
c ==============================================================================
c [1mFound solution: 435909[0m
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64468 |  286827   672341 |   95609   64231  3084273    48.0 |  1.350 % |
c |     64568 |  286827   672341 |  105169   64331  3085548    48.0 |  1.351 % |
c |     64718 |  286452   671488 |  115686   64436  3086303    47.9 |  1.456 % |
c |     64943 |  286452   671488 |  127255   64661  3088405    47.8 |  1.456 % |
c |     65280 |  286452   671488 |  139981   64998  3091356    47.6 |  1.456 % |
c |     65786 |  286440   671461 |  153979   65501  3105468    47.4 |  1.459 % |
c ==============================================================================
c [1mFound solution: 433675[0m
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66530 |  286450   671528 |   95483   66245  3144016    47.5 |  1.459 % |
c |     66630 |  286450   671528 |  105031   66345  3144764    47.4 |  1.460 % |
c |     66780 |  286450   671528 |  115534   66495  3147292    47.3 |  1.460 % |
c |     67005 |  286450   671528 |  127087   66720  3168130    47.5 |  1.460 % |
c |     67342 |  286396   671405 |  139796   67054  3206859    47.8 |  1.474 % |
c |     67848 |  286396   671405 |  153776   67560  3222948    47.7 |  1.474 % |
c |     68607 |  286396   671405 |  169153   68319  3233174    47.3 |  1.474 % |
c |     69746 |  286396   671405 |  186069   69458  3332574    48.0 |  1.474 % |
c |     71454 |  286372   671351 |  204676   71165  3432460    48.2 |  1.482 % |
c ==============================================================================
c [1mFound solution: 429382[0m
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72160 |  286384   671380 |   95461   71871  3458870    48.1 |  1.482 % |
c |     72260 |  286384   671380 |  105007   71971  3461748    48.1 |  1.483 % |
c |     72411 |  286340   671278 |  115507   72120  3463828    48.0 |  1.497 % |
c |     72636 |  286340   671278 |  127058   72345  3469925    48.0 |  1.497 % |
c |     72973 |  286340   671278 |  139764   72682  3483184    47.9 |  1.497 % |
c |     73479 |  286340   671278 |  153740   73188  3502426    47.9 |  1.497 % |
c |     74238 |  286340   671278 |  169114   73947  3510471    47.5 |  1.497 % |
c |     75377 |  286340   671278 |  186026   75086  3755391    50.0 |  1.497 % |
c |     77086 |  286143   670826 |  204629   76775  3812101    49.7 |  1.558 % |
c |     79648 |  286064   670648 |  225092   79322  3887526    49.0 |  1.579 % |
c ==============================================================================
c [1mFound solution: 389989[0m
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82574 |  286093   670721 |   95364   82248  4017147    48.8 |  1.579 % |
c |     82675 |  286093   670721 |  104900   82349  4018604    48.8 |  1.580 % |
c |     82827 |  285926   670342 |  115390   82480  4019751    48.7 |  1.627 % |
c |     83052 |  285926   670342 |  126929   82705  4020916    48.6 |  1.627 % |
c |     83389 |  285926   670342 |  139622   83042  4067516    49.0 |  1.627 % |
c |     83895 |  285926   670342 |  153584   83548  4081876    48.9 |  1.627 % |
c |     84654 |  285906   670297 |  168943   84306  4136077    49.1 |  1.633 % |
c |     85794 |  285906   670297 |  185837   85446  4266042    49.9 |  1.633 % |
c |     87505 |  285861   670194 |  204421   87135  4307281    49.4 |  1.647 % |
c ==============================================================================
c [1mFound solution: 380037[0m
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88132 |  285880   670357 |   95293   87762  4424781    50.4 |  1.647 % |
c |     88233 |  285880   670357 |  104822   87863  4425663    50.4 |  1.647 % |
c |     88383 |  285880   670357 |  115304   88013  4426722    50.3 |  1.647 % |
c |     88608 |  285880   670357 |  126834   88238  4434089    50.3 |  1.647 % |
c |     88947 |  285880   670357 |  139518   88577  4448639    50.2 |  1.647 % |
c |     89453 |  285880   670357 |  153470   89083  4552809    51.1 |  1.647 % |
c |     90212 |  285880   670357 |  168817   89842  4625864    51.5 |  1.647 % |
c |     91351 |  285880   670357 |  185699   90981  4649981    51.1 |  1.647 % |
c |     93061 |  285809   670195 |  204269   92673  4689988    50.6 |  1.668 % |
c |     95623 |  285809   670195 |  224695   95235  4809300    50.5 |  1.668 % |
c |     99467 |  285809   670195 |  247165   99079  5424523    54.7 |  1.668 % |
c ==============================================================================
c [1mFound solution: 376742[0m
c ---[   0]---> Sorter-cost:   15     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102944 |  285767   670104 |   95255  102555  5563757    54.3 |  1.668 % |
c |    103044 |  285767   670104 |  104780   31949  1034771    32.4 |  1.684 % |
c ==============================================================================
c [1mFound solution: 370710[0m
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103120 |  285749   670068 |   95249   32023  1036273    32.4 |  1.684 % |
c |    103221 |  285749   670068 |  104773   32124  1038051    32.3 |  1.693 % |
c |    103371 |  285749   670068 |  115251   32274  1038728    32.2 |  1.693 % |
c |    103596 |  285749   670068 |  126776   32499  1055537    32.5 |  1.693 % |
c |    103933 |  285749   670068 |  139454   32836  1067491    32.5 |  1.693 % |
c |    104439 |  285749   670068 |  153399   33342  1100316    33.0 |  1.693 % |
c |    105198 |  285749   670068 |  168739   34101  1126293    33.0 |  1.693 % |
c |    106337 |  285698   669949 |  185613   35239  1187793    33.7 |  1.708 % |
c ==============================================================================
c [1mFound solution: 369981[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107949 |  285682   669915 |   95227   36850  1504973    40.8 |  1.708 % |
c |    108052 |  285682   669915 |  104749   36953  1506173    40.8 |  1.717 % |
c |    108202 |  285682   669915 |  115224   37103  1507610    40.6 |  1.717 % |
c |    108428 |  285682   669915 |  126747   37329  1515140    40.6 |  1.717 % |
c |    108765 |  285682   669915 |  139421   37666  1529271    40.6 |  1.717 % |
c |    109271 |  285682   669915 |  153364   38172  1556483    40.8 |  1.717 % |
c |    110032 |  285682   669915 |  168700   38933  1603181    41.2 |  1.717 % |
c ==============================================================================
c [1mFound solution: 369979[0m
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110278 |  285690   669939 |   95230   39179  1612569    41.2 |  1.717 % |
c |    110379 |  285633   669810 |  104753   39279  1615846    41.1 |  1.732 % |
c |    110529 |  285633   669810 |  115228   39429  1617918    41.0 |  1.732 % |
c |    110755 |  285506   669522 |  126751   39644  1619251    40.8 |  1.767 % |
c |    111094 |  285506   669522 |  139426   39983  1642570    41.1 |  1.767 % |
c |    111600 |  285506   669522 |  153368   40489  1711038    42.3 |  1.767 % |
c |    112359 |  285506   669522 |  168705   41248  1757059    42.6 |  1.767 % |
c ==============================================================================
c [1mFound solution: 366578[0m
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113082 |  285514   669547 |   95171   41971  1829234    43.6 |  1.767 % |
c |    113183 |  285468   669444 |  104688   42069  1831438    43.5 |  1.780 % |
c |    113335 |  285468   669444 |  115156   42221  1834165    43.4 |  1.780 % |
c |    113561 |  285468   669444 |  126672   42447  1845787    43.5 |  1.780 % |
c |    113899 |  285449   669402 |  139339   42784  1869641    43.7 |  1.785 % |
c |    114406 |  285430   669360 |  153273   43290  1904924    44.0 |  1.790 % |
c |    115165 |  285430   669360 |  168601   44049  1959172    44.5 |  1.790 % |
c |    116304 |  285430   669360 |  185461   45188  2046279    45.3 |  1.790 % |
c |    118014 |  285430   669360 |  204007   46898  2170140    46.3 |  1.790 % |
c |    120577 |  285430   669360 |  224408   49461  2316819    46.8 |  1.790 % |
c |    124422 |  285317   669105 |  246849   53304  2510434    47.1 |  1.818 % |
c |    130188 |  285317   669105 |  271533   59070  2821596    47.8 |  1.818 % |
c ==============================================================================
c [1mFound solution: 366570[0m
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131845 |  285328   669136 |   95109   60727  2949783    48.6 |  1.818 % |
c |    131946 |  285328   669136 |  104619   60828  2953165    48.5 |  1.819 % |
c |    132096 |  285328   669136 |  115081   60978  2961053    48.6 |  1.819 % |
c |    132321 |  285328   669136 |  126590   61203  2971592    48.6 |  1.819 % |
c |    132658 |  285328   669136 |  139249   61540  2979009    48.4 |  1.819 % |
c |    133164 |  285328   669136 |  153173   62046  3021918    48.7 |  1.819 % |
c |    133924 |  285298   669070 |  168491   62805  3109161    49.5 |  1.827 % |
c |    135063 |  285298   669070 |  185340   63944  3194490    50.0 |  1.827 % |
c |    136771 |  285204   668861 |  203874   65650  3399419    51.8 |  1.853 % |
c ==============================================================================
c [1mFound solution: 365125[0m
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137522 |  285218   668892 |   95072   66401  3415093    51.4 |  1.853 % |
c |    137623 |  285218   668892 |  104579   66502  3415717    51.4 |  1.854 % |
c |    137773 |  285218   668892 |  115037   66652  3416706    51.3 |  1.854 % |
c |    137999 |  285218   668892 |  126540   66878  3418322    51.1 |  1.854 % |
c |    138336 |  285218   668892 |  139194   67215  3440255    51.2 |  1.854 % |
c |    138842 |  285218   668892 |  153114   67721  3480470    51.4 |  1.854 % |
c |    139602 |  285218   668892 |  168425   68481  3545219    51.8 |  1.854 % |
c ==============================================================================
c [1mFound solution: 360746[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    139957 |  285208   668877 |   95069   68835  3617548    52.6 |  1.854 % |
c |    140057 |  285208   668877 |  104575   68935  3621012    52.5 |  1.861 % |
c |    140207 |  285208   668877 |  115033   69085  3622746    52.4 |  1.861 % |
c |    140432 |  285208   668877 |  126536   69310  3635414    52.5 |  1.861 % |
c |    140769 |  285208   668877 |  139190   69647  3648677    52.4 |  1.861 % |
c |    141275 |  285208   668877 |  153109   70153  3672456    52.3 |  1.861 % |
c |    142035 |  285208   668877 |  168420   70913  3706877    52.3 |  1.861 % |
c |    143174 |  285208   668877 |  185262   72052  3785458    52.5 |  1.861 % |
c ==============================================================================
c [1mFound solution: 360742[0m
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    144337 |  285217   668899 |   95072   73215  4058790    55.4 |  1.861 % |
c |    144437 |  285143   668734 |  104579   73314  4068235    55.5 |  1.882 % |
c |    144587 |  285143   668734 |  115037   73464  4074190    55.5 |  1.882 % |
c |    144812 |  285143   668734 |  126540   73689  4106029    55.7 |  1.882 % |
c |    145150 |  285048   668520 |  139194   74026  4140679    55.9 |  1.906 % |
c |    145659 |  285048   668520 |  153114   74535  4194085    56.3 |  1.906 % |
c |    146419 |  285048   668520 |  168425   75295  4256282    56.5 |  1.906 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  7585 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.93 2/54 7581
Raw data (stat): 7581 (runsolver) R 7580 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840842864 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.002 s]
Raw data (loadavg): 0.95 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0035 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0042 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7585
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7638
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.133 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.133 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.134 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.135 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.139 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.14 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.14 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.14 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.14 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.14 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7640
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.141 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.14 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.142 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.143 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.143 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.147 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.154 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.154 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.154 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.154 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.154 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.154 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.154 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.155 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.156 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.157 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.157 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.157 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.157 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.158 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.159 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.159 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.158 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.159 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.159 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.158 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.159 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.159 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.159 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.189 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.189 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.189 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.189 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.19 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 0.99 0.98 0.93 1/53 7642
Raw data (stat): 7581 (minisat+_script) S 7580 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842864 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.86
CPU user time (s): 1229.38
CPU system time (s): 0.477927
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####