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/MIPLIB/miplib3/normalized-mps-v2-13-7-p0282.opb
MD5SUM	1a8deb577df7e72871b7e1004c098336
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.02084
Number of variables	282
Total number of constraints	523
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	282
Number of constraints which are nor clauses,nor cardinality constraints	64
Minimum length of a constraint	1
Maximum length of a constraint	57
Trace number 31227

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-25 23:15:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22624 boxname=wulflinc15 idbench=1440 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  1a8deb577df7e72871b7e1004c098336  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-p0282.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-p0282.opb
IDLAUNCH: 22624
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        902244 kB
Buffers:         32500 kB
Cached:          78616 kB
SwapCached:        608 kB
Active:          24156 kB
Inactive:        89060 kB
HighTotal:      131008 kB
HighFree:        67144 kB
LowTotal:       903652 kB
LowFree:        835100 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5084 kB
Slab:            13596 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:35:56 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22624 7 1229.87 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 ---[ 223]---> Sorter-cost:  850     Base: 5 2 3 3
c ---[ 222]---> Sorter-cost:  712     Base: 5 2 3 3
c ---[ 221]---> Sorter-cost: 1135     Base: 2 5 5
c ---[ 220]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 219]---> Sorter-cost: 1099     Base: 2 5 3 2
c ---[ 218]---> Sorter-cost:  882     Base: 2 5 3 3
c ---[ 217]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 216]---> Sorter-cost:  909     Base: 2 5 5
c ---[ 215]---> Sorter-cost: 1016     Base: 2 5 3
c ---[ 214]---> Sorter-cost:  898     Base: 2 5 3 3
c ---[ 213]---> Sorter-cost: 1146     Base: 2 5 3 3
c ---[ 211]---> Sorter-cost:  996     Base: 2 5 3 3
c ---[ 209]---> Sorter-cost:  943     Base: 2 5 3 3
c ---[ 208]---> Sorter-cost:  760     Base: 2 5 3 3
c ---[ 207]---> Sorter-cost:  769     Base: 5 2 3 3
c ---[ 206]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[ 205]---> Sorter-cost: 1005     Base: 2 5 5
c ---[ 204]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 203]---> Sorter-cost: 1072     Base: 2 5 3
c ---[ 202]---> Sorter-cost:  885     Base: 2 5 3 2
c ---[ 201]---> Sorter-cost:  712     Base: 5 2 3 3
c ---[ 199]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 198]---> Sorter-cost:  909     Base: 2 5 5
c ---[ 197]---> Sorter-cost:  938     Base: 2 5 3 2
c ---[ 196]---> Sorter-cost:  852     Base: 2 5 3 3
c ---[ 195]---> Sorter-cost: 1059     Base: 2 5 3 3
c ---[ 194]---> Sorter-cost:  949     Base: 2 5 3 3
c ---[ 193]---> Sorter-cost:  844     Base: 2 5 3 3
c ---[ 192]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[ 191]---> Sorter-cost: 1081     Base: 2 5 3 3
c ---[ 190]---> Sorter-cost:  996     Base: 2 5 3 2
c ---[ 189]---> Sorter-cost:  995     Base: 2 5 3 3
c ---[ 188]---> Sorter-cost:  985     Base: 2 5 3 2
c ---[ 187]---> BDD-cost:   56
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   56
c ---[ 184]---> BDD-cost:   56
c ---[ 183]---> BDD-cost:   16
c ---[ 182]---> BDD-cost:   26
c ---[ 181]---> BDD-cost:    8
c ---[ 180]---> BDD-cost:    4
c ---[   2]---> Sorter-cost:  678     Base: 2 5 3
c ---[   1]---> Sorter-cost:  694     Base: 2 5 3
c ---[   0]---> BDD-cost:   12
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 ==============================================================================
c [1mFound solution: 881867[0m
c ---[   0]---> Sorter-cost:77310     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 |        94 |  288858   675684 |   96286      88      654     7.4 |  0.000 % |
c |       195 |  288627   675172 |  105914     184     1358     7.4 |  0.198 % |
c |       347 |  288591   675094 |  116506     333     2602     7.8 |  0.208 % |
c |       573 |  288578   675066 |  128156     558     4285     7.7 |  0.212 % |
c ==============================================================================
c [1mFound solution: 798158[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 |       595 |  289292   677295 |   96430     580     4464     7.7 |  0.212 % |
c |       695 |  289229   677156 |  106073     677     5230     7.7 |  0.228 % |
c |       845 |  289229   677156 |  116680     827    11071    13.4 |  0.228 % |
c |      1070 |  289229   677156 |  128348    1052    12272    11.7 |  0.228 % |
c |      1407 |  289229   677156 |  141183    1389    16783    12.1 |  0.228 % |
c |      1913 |  289229   677156 |  155301    1895    22562    11.9 |  0.228 % |
c |      2673 |  289075   676811 |  170831    2651    36393    13.7 |  0.268 % |
c ==============================================================================
c [1mFound solution: 491204[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 |      3485 |  289830   678675 |   96610    3463    53869    15.6 |  0.268 % |
c |      3588 |  289830   678675 |  106271    3566    56114    15.7 |  0.268 % |
c |      3738 |  289830   678675 |  116898    3716    57041    15.4 |  0.268 % |
c |      3964 |  289830   678675 |  128587    3942    58762    14.9 |  0.268 % |
c |      4302 |  289497   677924 |  141446    4259    65556    15.4 |  0.359 % |
c |      4808 |  289486   677901 |  155591    4764    76531    16.1 |  0.362 % |
c |      5570 |  289486   677901 |  171150    5526    92145    16.7 |  0.362 % |
c |      6709 |  289269   677414 |  188265    6660   147337    22.1 |  0.421 % |
c |      8420 |  289226   677317 |  207092    8370   195883    23.4 |  0.433 % |
c |     10982 |  288502   675683 |  227801   10882   251129    23.1 |  0.639 % |
c |     14827 |  288119   674823 |  250581   14713   432249    29.4 |  0.746 % |
c ==============================================================================
c [1mFound solution: 436562[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 |     16547 |  288672   676183 |   96224   16433   539492    32.8 |  0.746 % |
c |     16647 |  288672   676183 |  105846   16533   540183    32.7 |  0.744 % |
c |     16798 |  288672   676183 |  116431   16684   541629    32.5 |  0.744 % |
c |     17024 |  288672   676183 |  128074   16910   550880    32.6 |  0.744 % |
c |     17362 |  288672   676183 |  140881   17248   558318    32.4 |  0.744 % |
c |     17868 |  288672   676183 |  154969   17754   566864    31.9 |  0.744 % |
c |     18629 |  288542   675891 |  170466   18512   573030    31.0 |  0.778 % |
c |     19768 |  288542   675891 |  187513   19651   616919    31.4 |  0.778 % |
c |     21478 |  288517   675836 |  206264   21359   721335    33.8 |  0.785 % |
c ==============================================================================
c [1mFound solution: 435105[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 |     22186 |  288522   676084 |   96174   22015   748548    34.0 |  0.785 % |
c |     22286 |  288522   676084 |  105791   22115   750097    33.9 |  0.886 % |
c |     22437 |  288522   676084 |  116370   22266   750817    33.7 |  0.886 % |
c |     22662 |  288522   676084 |  128007   22491   752052    33.4 |  0.886 % |
c |     22999 |  288522   676084 |  140808   22828   754156    33.0 |  0.886 % |
c |     23505 |  288522   676084 |  154889   23334   777295    33.3 |  0.886 % |
c |     24266 |  288458   675940 |  170378   24094   804215    33.4 |  0.902 % |
c |     25405 |  288430   675876 |  187415   25231   822738    32.6 |  0.910 % |
c |     27116 |  288321   675631 |  206157   26937   846652    31.4 |  0.940 % |
c |     29681 |  288251   675472 |  226773   29492  1007488    34.2 |  0.960 % |
c ==============================================================================
c [1mFound solution: 376947[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 |     31856 |  288251   675561 |   96083   31666  1138561    36.0 |  0.960 % |
c |     31957 |  288251   675561 |  105691   31767  1139909    35.9 |  0.971 % |
c |     32108 |  288251   675561 |  116260   31918  1140918    35.7 |  0.971 % |
c |     32333 |  288145   675322 |  127886   32142  1144235    35.6 |  1.000 % |
c |     32670 |  287939   674860 |  140675   32454  1155638    35.6 |  1.055 % |
c |     33176 |  287939   674860 |  154742   32960  1220439    37.0 |  1.056 % |
c |     33936 |  287939   674860 |  170216   33720  1267260    37.6 |  1.055 % |
c |     35075 |  287807   674558 |  187238   34853  1287014    36.9 |  1.095 % |
c ==============================================================================
c [1mFound solution: 376622[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 |     35698 |  287822   674602 |   95940   35476  1359098    38.3 |  1.095 % |
c |     35798 |  287822   674602 |  105534   35576  1365673    38.4 |  1.096 % |
c |     35949 |  287822   674602 |  116087   35727  1372000    38.4 |  1.096 % |
c |     36174 |  287822   674602 |  127696   35952  1376958    38.3 |  1.096 % |
c |     36512 |  287822   674602 |  140465   36290  1395290    38.4 |  1.096 % |
c ==============================================================================
c [1mFound solution: 354913[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 |     36822 |  287792   674547 |   95930   36599  1404305    38.4 |  1.096 % |
c |     36922 |  287792   674547 |  105523   36699  1405521    38.3 |  1.108 % |
c |     37073 |  287792   674547 |  116075   36850  1406497    38.2 |  1.108 % |
c |     37300 |  287792   674547 |  127682   37077  1420087    38.3 |  1.108 % |
c |     37637 |  287792   674547 |  140451   37414  1438814    38.5 |  1.108 % |
c |     38143 |  287792   674547 |  154496   37920  1448278    38.2 |  1.108 % |
c |     38902 |  287682   674299 |  169945   38677  1480337    38.3 |  1.138 % |
c |     40042 |  287644   674215 |  186940   39816  1638384    41.1 |  1.148 % |
c |     41750 |  287644   674215 |  205634   41524  1686397    40.6 |  1.148 % |
c |     44312 |  287644   674215 |  226197   44086  1953984    44.3 |  1.148 % |
c |     48157 |  287510   673913 |  248817   47929  2297892    47.9 |  1.183 % |
c ==============================================================================
c [1mFound solution: 354908[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 |     48837 |  287329   673517 |   95776   48605  2325753    47.9 |  1.183 % |
c |     48937 |  287329   673517 |  105353   48705  2331070    47.9 |  1.232 % |
c |     49087 |  287329   673517 |  115888   48855  2338335    47.9 |  1.232 % |
c |     49312 |  287325   673508 |  127477   49079  2340723    47.7 |  1.233 % |
c |     49649 |  287289   673426 |  140225   49415  2349449    47.5 |  1.244 % |
c |     50156 |  287289   673426 |  154248   49922  2366434    47.4 |  1.244 % |
c |     50915 |  287289   673426 |  169673   50681  2372878    46.8 |  1.244 % |
c |     52055 |  287289   673426 |  186640   51821  2416696    46.6 |  1.244 % |
c |     53763 |  287265   673372 |  205304   53528  2515819    47.0 |  1.252 % |
c ==============================================================================
c [1mFound solution: 354907[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 |     54985 |  287199   673349 |   95733   54748  2617771    47.8 |  1.252 % |
c |     55087 |  287199   673349 |  105306   54850  2618381    47.7 |  1.274 % |
c |     55238 |  287102   673132 |  115836   54999  2628353    47.8 |  1.302 % |
c |     55463 |  287102   673132 |  127420   55224  2648900    48.0 |  1.302 % |
c |     55800 |  287102   673132 |  140162   55561  2658612    47.9 |  1.302 % |
c |     56308 |  286962   672814 |  154178   56048  2666934    47.6 |  1.342 % |
c |     57068 |  286958   672805 |  169596   56807  2740203    48.2 |  1.343 % |
c |     58207 |  286941   672768 |  186556   57945  2841513    49.0 |  1.348 % |
c |     59916 |  286941   672768 |  205212   59654  2921875    49.0 |  1.348 % |
c |     62478 |  286920   672722 |  225733   62215  3171421    51.0 |  1.354 % |
c ==============================================================================
c [1mFound solution: 354893[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 |     64209 |  286932   672754 |   95644   63946  3295032    51.5 |  1.354 % |
c |     64310 |  286932   672754 |  105208   64047  3295611    51.5 |  1.355 % |
c |     64461 |  286932   672754 |  115729   64198  3303094    51.5 |  1.355 % |
c |     64686 |  286932   672754 |  127302   64423  3312052    51.4 |  1.355 % |
c |     65024 |  286932   672754 |  140032   64761  3314663    51.2 |  1.355 % |
c |     65533 |  286932   672754 |  154035   65270  3354188    51.4 |  1.355 % |
c |     66292 |  286932   672754 |  169439   66029  3386946    51.3 |  1.355 % |
c |     67432 |  286932   672754 |  186383   67169  3429370    51.1 |  1.355 % |
c |     69140 |  286932   672754 |  205021   68877  3498751    50.8 |  1.355 % |
c ==============================================================================
c [1mFound solution: 351999[0m
c ---[   0]---> Sorter-cost:    5     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 |     69370 |  286939   672772 |   95646   69107  3514837    50.9 |  1.355 % |
c |     69470 |  286939   672772 |  105210   69207  3517481    50.8 |  1.356 % |
c ==============================================================================
c [1mFound solution: 325754[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 |     69603 |  286918   672729 |   95639   69339  3525718    50.8 |  1.356 % |
c |     69703 |  286892   672670 |  105202   69438  3526373    50.8 |  1.370 % |
c |     69853 |  286892   672670 |  115723   69588  3547742    51.0 |  1.370 % |
c |     70079 |  286892   672670 |  127295   69814  3569348    51.1 |  1.370 % |
c |     70416 |  286892   672670 |  140025   70151  3584009    51.1 |  1.370 % |
c |     70924 |  286892   672670 |  154027   70659  3654183    51.7 |  1.370 % |
c |     71683 |  286892   672670 |  169430   71418  3667043    51.3 |  1.370 % |
c |     72822 |  286847   672568 |  186373   72554  3696020    50.9 |  1.382 % |
c |     74530 |  286730   672304 |  205010   74256  3740046    50.4 |  1.415 % |
c |     77092 |  286632   672083 |  225511   76816  4009626    52.2 |  1.440 % |
c ==============================================================================
c [1mFound solution: 325267[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 |     79868 |  286603   672024 |   95534   79590  4117132    51.7 |  1.440 % |
c |     79968 |  286505   671805 |  105087   79688  4120996    51.7 |  1.482 % |
c |     80118 |  286505   671805 |  115596   79838  4127671    51.7 |  1.482 % |
c |     80345 |  286505   671805 |  127155   80065  4142188    51.7 |  1.482 % |
c ==============================================================================
c [1mFound solution: 324891[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 |     80640 |  286523   671924 |   95507   80360  4169092    51.9 |  1.482 % |
c |     80740 |  286523   671924 |  105057   80460  4169528    51.8 |  1.483 % |
c |     80890 |  286523   671924 |  115563   80610  4174709    51.8 |  1.483 % |
c |     81115 |  286523   671924 |  127119   80835  4178907    51.7 |  1.483 % |
c |     81452 |  286523   671924 |  139831   81172  4190033    51.6 |  1.483 % |
c |     81958 |  286523   671924 |  153814   81678  4215423    51.6 |  1.483 % |
c |     82717 |  286523   671924 |  169196   82437  4248696    51.5 |  1.483 % |
c |     83856 |  286523   671924 |  186116   83576  4378185    52.4 |  1.483 % |
c |     85565 |  286472   671808 |  204727   85284  4571724    53.6 |  1.496 % |
c |     88129 |  286472   671808 |  225200   87848  4870692    55.4 |  1.496 % |
c |     91973 |  286472   671808 |  247720   91692  5330851    58.1 |  1.496 % |
c ==============================================================================
c [1mFound solution: 324675[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 |     94793 |  286465   671793 |   95488   94511  5591844    59.2 |  1.496 % |
c |     94894 |  286465   671793 |  105036   94612  5592545    59.1 |  1.504 % |
c |     95044 |  286465   671793 |  115540   94762  5594717    59.0 |  1.504 % |
c |     95269 |  286465   671793 |  127094   94987  5596716    58.9 |  1.504 % |
c |     95606 |  286465   671793 |  139803   95324  5616092    58.9 |  1.504 % |
c |     96113 |  286465   671793 |  153784   95831  5651619    59.0 |  1.504 % |
c |     96872 |  286465   671793 |  169162   96590  5684967    58.9 |  1.504 % |
c ==============================================================================
c [1mFound solution: 322839[0m
c ---[   0]---> Sorter-cost:    5     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 |     97234 |  286471   671807 |   95490   96952  5711630    58.9 |  1.504 % |
c |     97334 |  286471   671807 |  105039   97052  5717178    58.9 |  1.505 % |
c |     97484 |  286471   671807 |  115542   97202  5734519    59.0 |  1.505 % |
c |     97709 |  286471   671807 |  127097   97427  5742109    58.9 |  1.505 % |
c |     98046 |  286471   671807 |  139806   97764  5793815    59.3 |  1.505 % |
c |     98554 |  286471   671807 |  153787   98272  5827995    59.3 |  1.505 % |
c |     99315 |  286471   671807 |  169166   99033  5883452    59.4 |  1.505 % |
c |    100454 |  286471   671807 |  186082  100172  5970295    59.6 |  1.505 % |
c |    102162 |  286471   671807 |  204691  101880  6133092    60.2 |  1.505 % |
c ==============================================================================
c [1mFound solution: 322838[0m
c ---[   0]---> Sorter-cost:    4     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 |    102452 |  286404   671657 |   95468  102169  6157887    60.3 |  1.505 % |
c |    102552 |  286404   671657 |  105014   31986  1235638    38.6 |  1.526 % |
c |    102705 |  286404   671657 |  115516   32139  1236710    38.5 |  1.526 % |
c |    102930 |  286404   671657 |  127067   32364  1251376    38.7 |  1.526 % |
c |    103267 |  286404   671657 |  139774   32701  1270087    38.8 |  1.526 % |
c ==============================================================================
c [1mFound solution: 322837[0m
c ---[   0]---> Sorter-cost:    5     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 |    103418 |  286367   671574 |   95455   32851  1280341    39.0 |  1.526 % |
c |    103519 |  286367   671574 |  105000   32952  1293027    39.2 |  1.540 % |
c |    103669 |  286367   671574 |  115500   33102  1300251    39.3 |  1.540 % |
c |    103895 |  286367   671574 |  127050   33328  1319175    39.6 |  1.540 % |
c |    104232 |  286367   671574 |  139755   33665  1337270    39.7 |  1.540 % |
c ==============================================================================
c [1mFound solution: 322815[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 |    104482 |  286377   671676 |   95459   33915  1366281    40.3 |  1.540 % |
c |    104582 |  286377   671676 |  105004   34015  1372203    40.3 |  1.541 % |
c |    104734 |  286377   671676 |  115505   34167  1378933    40.4 |  1.541 % |
c |    104959 |  286377   671676 |  127055   34392  1386271    40.3 |  1.541 % |
c |    105297 |  286377   671676 |  139761   34730  1407505    40.5 |  1.541 % |
c |    105805 |  286377   671676 |  153737   35238  1445714    41.0 |  1.541 % |
c ==============================================================================
c [1mFound solution: 322803[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 |    106109 |  286389   671708 |   95463   35542  1464879    41.2 |  1.541 % |
c |    106209 |  286389   671708 |  105009   35642  1465756    41.1 |  1.542 % |
c |    106359 |  286389   671708 |  115510   35792  1466498    41.0 |  1.542 % |
c |    106585 |  286389   671708 |  127061   36018  1486837    41.3 |  1.542 % |
c |    106923 |  286389   671708 |  139767   36356  1523724    41.9 |  1.542 % |
c |    107429 |  286389   671708 |  153744   36862  1551729    42.1 |  1.542 % |
c |    108189 |  286389   671708 |  169118   37622  1594362    42.4 |  1.542 % |
c |    109329 |  286389   671708 |  186030   38762  1800693    46.5 |  1.542 % |
c |    111038 |  286389   671708 |  204633   40471  1924175    47.5 |  1.542 % |
c ==============================================================================
c [1mFound solution: 322758[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 |    111639 |  286398   671731 |   95466   41072  1983502    48.3 |  1.542 % |
c |    111741 |  286398   671731 |  105012   41174  1991568    48.4 |  1.543 % |
c |    111892 |  286398   671731 |  115513   41325  1999481    48.4 |  1.543 % |
c |    112120 |  286398   671731 |  127065   41553  2036891    49.0 |  1.543 % |
c |    112460 |  286392   671717 |  139771   41892  2039196    48.7 |  1.545 % |
c |    112967 |  286249   671395 |  153748   42358  2072777    48.9 |  1.583 % |
c ==============================================================================
c [1mFound solution: 322756[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 |    113407 |  286258   671420 |   95419   42798  2163613    50.6 |  1.583 % |
c |    113507 |  286258   671420 |  104960   42898  2164127    50.4 |  1.583 % |
c |    113658 |  286258   671420 |  115456   43049  2168960    50.4 |  1.583 % |
c |    113884 |  286258   671420 |  127002   43275  2185067    50.5 |  1.583 % |
c ==============================================================================
c [1mFound solution: 322749[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 |    114012 |  286267   671443 |   95422   43403  2215288    51.0 |  1.583 % |
c |    114113 |  286267   671443 |  104964   43504  2217181    51.0 |  1.584 % |
c |    114264 |  286237   671377 |  115460   43654  2230119    51.1 |  1.592 % |
c |    114490 |  286237   671377 |  127006   43880  2242532    51.1 |  1.592 % |
c |    114829 |  286237   671377 |  139707   44219  2259868    51.1 |  1.592 % |
c |    115337 |  286233   671369 |  153678   44726  2305115    51.5 |  1.594 % |
c ==============================================================================
c [1mFound solution: 321363[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 |    115687 |  286244   671397 |   95414   45076  2358047    52.3 |  1.594 % |
c |    115787 |  286244   671397 |  104955   45176  2358575    52.2 |  1.595 % |
c |    115938 |  286244   671397 |  115450   45327  2365104    52.2 |  1.595 % |
c ==============================================================================
c [1mFound solution: 321360[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 |    116085 |  286258   671432 |   95419   45474  2385540    52.5 |  1.595 % |
c |    116185 |  286258   671432 |  104960   45574  2387910    52.4 |  1.596 % |
c |    116337 |  286258   671432 |  115456   45726  2399983    52.5 |  1.596 % |
c |    116563 |  286258   671432 |  127002   45952  2434724    53.0 |  1.596 % |
c |    116900 |  286237   671386 |  139702   46288  2472885    53.4 |  1.602 % |
c |    117406 |  286237   671386 |  153673   46794  2485584    53.1 |  1.602 % |
c ==============================================================================
c [1mFound solution: 319923[0m
c ---[   0]---> Sorter-cost:    5     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 |    118136 |  286211   671329 |   95403   47523  2581249    54.3 |  1.602 % |
c |    118237 |  286211   671329 |  104943   47624  2582560    54.2 |  1.612 % |
c |    118389 |  286211   671329 |  115437   47776  2590145    54.2 |  1.612 % |
c |    118614 |  286211   671329 |  126981   48001  2612706    54.4 |  1.612 % |
c |    118956 |  286211   671329 |  139679   48343  2625316    54.3 |  1.612 % |
c |    119463 |  286211   671329 |  153647   48850  2652967    54.3 |  1.612 % |
c |    120223 |  286211   671329 |  169012   49610  2714939    54.7 |  1.612 % |
c |    121362 |  286211   671329 |  185913   50749  2870613    56.6 |  1.612 % |
c ==============================================================================
c [1mFound solution: 318464[0m
c ---[   0]---> Sorter-cost:    2     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 |    122535 |  286224   671362 |   95408   51922  2972933    57.3 |  1.612 % |
c |    122636 |  286224   671362 |  104948   52023  2978542    57.3 |  1.613 % |
c |    122786 |  286224   671362 |  115443   52173  2987829    57.3 |  1.613 % |
c |    123011 |  286224   671362 |  126988   52398  3006530    57.4 |  1.613 % |
c |    123348 |  286224   671362 |  139686   52735  3030391    57.5 |  1.613 % |
c |    123854 |  286224   671362 |  153655   53241  3057847    57.4 |  1.613 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 13415 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.85 0.95 0.90 2/54 13411
Raw data (stat): 13411 (runsolver) R 13410 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784535489 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0004 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0013 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0013 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0018 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.026 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.027 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.72 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 13415
Raw data (stat): 13411 (minisat+_script) S 13410 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784535489 2174976 226 4294967295 134512640 135087896 3221224544 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.72
CPU time (s): 1229.87
CPU user time (s): 1229.3
CPU system time (s): 0.565913
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####