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 32416

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-27 09:46:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23796 boxname=wulflinc10 idbench=1440 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1a8deb577df7e72871b7e1004c098336  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-p0282.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-p0282.opb
IDLAUNCH: 23796
/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:        852112 kB
Buffers:          8908 kB
Cached:         153128 kB
SwapCached:         76 kB
Active:          19200 kB
Inactive:       145508 kB
HighTotal:      131008 kB
HighFree:          364 kB
LowTotal:       903652 kB
LowFree:        851748 kB
SwapTotal:     2097136 kB
SwapFree:      2096764 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6396 kB
Slab:            12228 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 10:07:26 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 23796 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 ---[ 223]---> BDD-cost:  580
c ---[ 222]---> BDD-cost:  587
c ---[ 221]---> BDD-cost:  540
c ---[ 220]---> BDD-cost:  394
c ---[ 219]---> BDD-cost:  497
c ---[ 218]---> BDD-cost:  370
c ---[ 217]---> BDD-cost:  386
c ---[ 216]---> BDD-cost:  415
c ---[ 215]---> BDD-cost:  348
c ---[ 214]---> BDD-cost:  385
c ---[ 213]---> BDD-cost:  744
c ---[ 211]---> BDD-cost:  791
c ---[ 209]---> BDD-cost:  828
c ---[ 208]---> BDD-cost:  473
c ---[ 207]---> BDD-cost:  492
c ---[ 206]---> BDD-cost:  528
c ---[ 205]---> BDD-cost:  310
c ---[ 204]---> BDD-cost:  347
c ---[ 203]---> BDD-cost:  219
c ---[ 202]---> BDD-cost:  267
c ---[ 201]---> BDD-cost:  593
c ---[ 199]---> BDD-cost:  396
c ---[ 198]---> BDD-cost:  448
c ---[ 197]---> BDD-cost:  323
c ---[ 196]---> BDD-cost:  369
c ---[ 195]---> BDD-cost:  578
c ---[ 194]---> BDD-cost:  602
c ---[ 193]---> BDD-cost:  659
c ---[ 192]---> BDD-cost:  350
c ---[ 191]---> BDD-cost:  872
c ---[ 190]---> BDD-cost:  362
c ---[ 189]---> BDD-cost:  897
c ---[ 188]---> BDD-cost:  423
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]---> BDD-cost:   87
c ---[   1]---> BDD-cost:  143
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41898   123412 |   13966       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 513010[0m
c ---[   0]---> Sorter-cost:77326     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 |         0 |  259193   631180 |   86397       0        0     nan |  0.000 % |
c |       101 |  259155   631099 |   95036      98     3620    36.9 |  0.064 % |
c |       251 |  259139   631065 |  104540     247     4873    19.7 |  0.069 % |
c |       478 |  259124   631032 |  114994     473     6580    13.9 |  0.073 % |
c |       815 |  259124   631032 |  126493     810     8587    10.6 |  0.073 % |
c |      1321 |  259099   630977 |  139143    1314    13473    10.3 |  0.081 % |
c |      2081 |  258740   630169 |  153057    2065    21521    10.4 |  0.191 % |
c ==============================================================================
c [1mFound solution: 498997[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 |      2156 |  259176   631678 |   86392    2136    22949    10.7 |  0.191 % |
c ==============================================================================
c [1mFound solution: 494881[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 |      2205 |  261090   636467 |   87030    2185    25546    11.7 |  0.191 % |
c |      2305 |  261090   636467 |   95733    2285    26048    11.4 |  0.223 % |
c |      2455 |  261084   636455 |  105306    2434    29181    12.0 |  0.227 % |
c |      2680 |  261020   636313 |  115836    2656    31234    11.8 |  0.245 % |
c ==============================================================================
c [1mFound solution: 489052[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 |      2929 |  260996   636263 |   86998    2900    37163    12.8 |  0.245 % |
c |      3029 |  260996   636263 |   95697    3000    38487    12.8 |  0.257 % |
c |      3184 |  260996   636263 |  105267    3155    41943    13.3 |  0.257 % |
c |      3409 |  260996   636263 |  115794    3380    46827    13.9 |  0.257 % |
c |      3746 |  260984   636236 |  127373    3716    51764    13.9 |  0.260 % |
c |      4252 |  260744   635700 |  140111    4216    58764    13.9 |  0.328 % |
c ==============================================================================
c [1mFound solution: 476792[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 |      4639 |  261607   638147 |   87202    4597    65258    14.2 |  0.328 % |
c |      4739 |  261607   638147 |   95922    4697    66637    14.2 |  0.387 % |
c |      4891 |  261599   638131 |  105514    4848    69883    14.4 |  0.391 % |
c |      5117 |  261265   637377 |  116065    5015    72749    14.5 |  0.494 % |
c |      5455 |  261153   637126 |  127672    5351    97792    18.3 |  0.530 % |
c |      5961 |  261134   637088 |  140439    5855   107474    18.4 |  0.540 % |
c |      6723 |  261021   636832 |  154483    6607   114145    17.3 |  0.578 % |
c ==============================================================================
c [1mFound solution: 467587[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 |      7001 |  261035   636870 |   87011    6884   118219    17.2 |  0.578 % |
c |      7101 |  261035   636870 |   95712    6984   118768    17.0 |  0.581 % |
c |      7252 |  261035   636870 |  105283    7135   119612    16.8 |  0.581 % |
c |      7479 |  260920   636614 |  115811    7354   126675    17.2 |  0.619 % |
c |      7816 |  260920   636614 |  127392    7691   132194    17.2 |  0.619 % |
c |      8322 |  260920   636614 |  140132    8197   136987    16.7 |  0.619 % |
c |      9082 |  260781   636299 |  154145    8950   145188    16.2 |  0.663 % |
c |     10222 |  260781   636299 |  169559   10090   163514    16.2 |  0.663 % |
c |     11930 |  260761   636254 |  186515   11797   203194    17.2 |  0.668 % |
c |     14495 |  260761   636254 |  205167   14362   283870    19.8 |  0.668 % |
c |     18339 |  260629   635955 |  225684   18171   377969    20.8 |  0.707 % |
c ==============================================================================
c [1mFound solution: 467586[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 |     21468 |  260976   636813 |   86992   21297   478405    22.5 |  0.707 % |
c |     21569 |  260976   636813 |   95691   21398   478954    22.4 |  0.714 % |
c |     21719 |  260976   636813 |  105260   21548   482573    22.4 |  0.714 % |
c |     21946 |  260976   636813 |  115786   21775   484743    22.3 |  0.714 % |
c |     22283 |  260976   636813 |  127364   22112   489498    22.1 |  0.714 % |
c |     22789 |  260976   636813 |  140101   22618   493010    21.8 |  0.714 % |
c |     23549 |  260976   636813 |  154111   23378   530738    22.7 |  0.714 % |
c |     24688 |  260976   636813 |  169522   24517   549168    22.4 |  0.714 % |
c ==============================================================================
c [1mFound solution: 467532[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 |     26257 |  260882   636798 |   86960   26083   636622    24.4 |  0.714 % |
c |     26357 |  260882   636798 |   95656   26183   638086    24.4 |  0.750 % |
c |     26507 |  260882   636798 |  105221   26333   639047    24.3 |  0.750 % |
c |     26732 |  260882   636798 |  115743   26558   641632    24.2 |  0.750 % |
c |     27069 |  260850   636726 |  127318   26891   643701    23.9 |  0.759 % |
c |     27575 |  260731   636457 |  140049   27392   678269    24.8 |  0.794 % |
c |     28337 |  260680   636355 |  154054   28148   751900    26.7 |  0.821 % |
c |     29477 |  260680   636355 |  169460   29288   771207    26.3 |  0.821 % |
c |     31185 |  260261   635403 |  186406   30951   792866    25.6 |  0.955 % |
c ==============================================================================
c [1mFound solution: 467181[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 |     31818 |  260268   635423 |   86756   31584   808504    25.6 |  0.955 % |
c |     31918 |  260164   635187 |   95431   31682   809278    25.5 |  0.986 % |
c |     32069 |  260164   635187 |  104974   31833   810098    25.4 |  0.986 % |
c ==============================================================================
c [1mFound solution: 416148[0m
c ---[   0]---> Sorter-cost:   14     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 |     32194 |  260182   635428 |   86727   31958   813972    25.5 |  0.986 % |
c |     32296 |  260166   635396 |   95399   32059   815997    25.5 |  0.996 % |
c |     32448 |  260067   635173 |  104939   32176   820443    25.5 |  1.025 % |
c ==============================================================================
c [1mFound solution: 397360[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 |     32537 |  260074   635188 |   86691   32265   825831    25.6 |  1.025 % |
c |     32639 |  260074   635188 |   95360   32367   826753    25.5 |  1.026 % |
c |     32789 |  260074   635188 |  104896   32517   828781    25.5 |  1.026 % |
c |     33014 |  260034   635098 |  115385   32740   830243    25.4 |  1.038 % |
c |     33354 |  260034   635098 |  126924   33080   844043    25.5 |  1.038 % |
c |     33860 |  259805   634578 |  139616   33569   849366    25.3 |  1.119 % |
c |     34619 |  259715   634373 |  153578   34324   860826    25.1 |  1.149 % |
c ==============================================================================
c [1mFound solution: 397197[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 |     35604 |  259582   634080 |   86527   35085   904152    25.8 |  1.149 % |
c |     35706 |  259582   634080 |   95179   35187   905576    25.7 |  1.198 % |
c |     35856 |  259306   633454 |  104697   35277   919906    26.1 |  1.287 % |
c |     36081 |  259301   633444 |  115167   35501   932688    26.3 |  1.290 % |
c |     36419 |  259275   633392 |  126684   35836   945651    26.4 |  1.304 % |
c |     36925 |  259261   633364 |  139352   36340   982345    27.0 |  1.312 % |
c |     37686 |  259253   633348 |  153287   37099  1006608    27.1 |  1.316 % |
c |     38825 |  259019   632824 |  168616   38175  1033078    27.1 |  1.393 % |
c |     40534 |  259000   632786 |  185478   39882  1082583    27.1 |  1.403 % |
c ==============================================================================
c [1mFound solution: 392796[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 |     41981 |  258785   632307 |   86261   41144  1137670    27.7 |  1.403 % |
c |     42081 |  258785   632307 |   94887   41244  1138188    27.6 |  1.478 % |
c |     42231 |  258785   632307 |  104375   41394  1143754    27.6 |  1.478 % |
c |     42456 |  258779   632295 |  114813   41618  1153246    27.7 |  1.481 % |
c |     42793 |  258779   632295 |  126294   41955  1179844    28.1 |  1.481 % |
c |     43299 |  258779   632295 |  138924   42461  1184039    27.9 |  1.481 % |
c |     44058 |  258779   632295 |  152816   43220  1269904    29.4 |  1.481 % |
c ==============================================================================
c [1mFound solution: 392794[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 |     44949 |  258789   632325 |   86263   44111  1320493    29.9 |  1.481 % |
c |     45049 |  258789   632325 |   94889   44211  1321370    29.9 |  1.482 % |
c |     45199 |  258755   632247 |  104378   44358  1323938    29.8 |  1.493 % |
c |     45425 |  258755   632247 |  114816   44584  1337792    30.0 |  1.493 % |
c ==============================================================================
c [1mFound solution: 392793[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 |     45627 |  258765   632277 |   86255   44786  1357005    30.3 |  1.493 % |
c |     45728 |  258765   632277 |   94880   44887  1357995    30.3 |  1.494 % |
c |     45878 |  258765   632277 |  104368   45037  1358984    30.2 |  1.494 % |
c |     46103 |  258761   632269 |  114805   45261  1362350    30.1 |  1.496 % |
c ==============================================================================
c [1mFound solution: 374086[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 |     46345 |  258768   632288 |   86256   45502  1379989    30.3 |  1.496 % |
c |     46445 |  258768   632288 |   94881   45602  1380818    30.3 |  1.502 % |
c |     46595 |  258768   632288 |  104369   45752  1382275    30.2 |  1.502 % |
c |     46822 |  258768   632288 |  114806   45979  1395722    30.4 |  1.502 % |
c |     47161 |  258747   632246 |  126287   46315  1408436    30.4 |  1.513 % |
c |     47668 |  258710   632169 |  138916   46815  1426244    30.5 |  1.528 % |
c |     48427 |  258675   632088 |  152807   47571  1435198    30.2 |  1.540 % |
c |     49568 |  258675   632088 |  168088   48712  1479350    30.4 |  1.540 % |
c |     51277 |  258657   632052 |  184897   50419  1567140    31.1 |  1.550 % |
c ==============================================================================
c [1mFound solution: 357831[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 |     51793 |  258550   631822 |   86183   50893  1588490    31.2 |  1.550 % |
c |     51895 |  258550   631822 |   94801   50995  1589403    31.2 |  1.596 % |
c |     52045 |  258550   631822 |  104281   51145  1601493    31.3 |  1.596 % |
c ==============================================================================
c [1mFound solution: 357615[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 |     52195 |  258559   631847 |   86186   51295  1619191    31.6 |  1.596 % |
c |     52295 |  258559   631847 |   94804   51395  1621879    31.6 |  1.597 % |
c |     52446 |  258559   631847 |  104285   51546  1622727    31.5 |  1.597 % |
c |     52672 |  258559   631847 |  114713   51772  1639746    31.7 |  1.597 % |
c |     53010 |  258559   631847 |  126184   52110  1676953    32.2 |  1.597 % |
c |     53516 |  258559   631847 |  138803   52616  1708554    32.5 |  1.597 % |
c |     54275 |  258559   631847 |  152683   53375  1728919    32.4 |  1.597 % |
c |     55417 |  258559   631847 |  167952   54517  1772591    32.5 |  1.597 % |
c ==============================================================================
c [1mFound solution: 357593[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 |     55733 |  258574   632077 |   86191   54833  1797621    32.8 |  1.597 % |
c |     55834 |  258574   632077 |   94810   54934  1799112    32.8 |  1.598 % |
c |     55984 |  258574   632077 |  104291   55084  1800225    32.7 |  1.598 % |
c |     56209 |  258574   632077 |  114720   55309  1804322    32.6 |  1.598 % |
c |     56546 |  258574   632077 |  126192   55646  1822043    32.7 |  1.598 % |
c |     57052 |  258574   632077 |  138811   56152  1826483    32.5 |  1.598 % |
c |     57812 |  258368   631609 |  152692   56905  1861025    32.7 |  1.657 % |
c |     58952 |  258368   631609 |  167961   58045  1955617    33.7 |  1.657 % |
c ==============================================================================
c [1mFound solution: 357592[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 |     59279 |  258368   631616 |   86122   58371  1972295    33.8 |  1.657 % |
c |     59379 |  258302   631467 |   94734   58470  1973365    33.8 |  1.685 % |
c |     59531 |  258302   631467 |  104207   58622  1980332    33.8 |  1.685 % |
c |     59756 |  258302   631467 |  114628   58847  1987941    33.8 |  1.685 % |
c |     60094 |  258286   631435 |  126091   59183  2017275    34.1 |  1.694 % |
c |     60602 |  258280   631423 |  138700   59690  2060743    34.5 |  1.697 % |
c |     61362 |  258147   631118 |  152570   60442  2075956    34.3 |  1.747 % |
c |     62501 |  258147   631118 |  167827   61581  2207444    35.8 |  1.747 % |
c |     64209 |  258147   631118 |  184610   63289  2399678    37.9 |  1.747 % |
c |     66772 |  258141   631106 |  203071   65851  2498520    37.9 |  1.749 % |
c |     70616 |  258141   631106 |  223378   69695  2740735    39.3 |  1.749 % |
c |     76384 |  258119   631056 |  245716   75460  2861887    37.9 |  1.755 % |
c ==============================================================================
c [1mFound solution: 356984[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 |     76768 |  258133   631093 |   86044   75844  2869388    37.8 |  1.755 % |
c |     76868 |  258133   631093 |   94648   75944  2870090    37.8 |  1.756 % |
c |     77020 |  258133   631093 |  104113   76096  2871039    37.7 |  1.756 % |
c |     77246 |  258133   631093 |  114524   76322  2872290    37.6 |  1.756 % |
c ==============================================================================
c [1mFound solution: 353456[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 |     77410 |  258140   631115 |   86046   76486  2880896    37.7 |  1.756 % |
c ==============================================================================
c [1mFound solution: 353455[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 |     77489 |  258147   631133 |   86049   76565  2882170    37.6 |  1.756 % |
c |     77589 |  258147   631133 |   94653   76665  2886845    37.7 |  1.758 % |
c |     77741 |  258147   631133 |  104119   76817  2895212    37.7 |  1.758 % |
c |     77966 |  258147   631133 |  114531   77042  2917655    37.9 |  1.758 % |
c |     78303 |  258133   631105 |  125984   77378  2942805    38.0 |  1.764 % |
c |     78809 |  258129   631097 |  138582   77883  2981995    38.3 |  1.766 % |
c |     79569 |  258129   631097 |  152441   78643  3027838    38.5 |  1.766 % |
c ==============================================================================
c [1mFound solution: 352971[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 |     79610 |  258139   631124 |   86046   78684  3029287    38.5 |  1.766 % |
c ==============================================================================
c [1mFound solution: 352970[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 |     79652 |  258149   631152 |   86049   78726  3033329    38.5 |  1.766 % |
c |     79752 |  258149   631152 |   94653   78826  3036444    38.5 |  1.768 % |
c |     79902 |  258149   631152 |  104119   78976  3047309    38.6 |  1.768 % |
c |     80127 |  258149   631152 |  114531   79201  3065589    38.7 |  1.768 % |
c |     80466 |  258149   631152 |  125984   79540  3098858    39.0 |  1.768 % |
c |     80972 |  258149   631152 |  138582   80046  3136188    39.2 |  1.768 % |
c |     81731 |  258149   631152 |  152441   80805  3264922    40.4 |  1.768 % |
c |     82870 |  258145   631144 |  167685   81943  3333338    40.7 |  1.770 % |
c |     84578 |  258141   631136 |  184453   83650  3569773    42.7 |  1.772 % |
c |     87140 |  258141   631136 |  202899   86212  3850183    44.7 |  1.772 % |
c |     90984 |  258141   631136 |  223188   90056  4371306    48.5 |  1.772 % |
c ==============================================================================
c [1mFound solution: 352969[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 |     94738 |  258139   631140 |   86046   93809  4816374    51.3 |  1.772 % |
c |     94841 |  258139   631140 |   94650   26654  1588476    59.6 |  1.780 % |
c |     94991 |  258139   631140 |  104115   26804  1595613    59.5 |  1.780 % |
c ==============================================================================
c [1mFound solution: 331113[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 |     95154 |  258152   631171 |   86050   26967  1597361    59.2 |  1.780 % |
c |     95255 |  258152   631171 |   94655   27068  1597893    59.0 |  1.781 % |
c |     95406 |  258152   631171 |  104120   27219  1617892    59.4 |  1.781 % |
c |     95632 |  258145   631157 |  114532   27444  1633120    59.5 |  1.784 % |
c |     95969 |  258138   631143 |  125985   27780  1653086    59.5 |  1.787 % |
c |     96476 |  258138   631143 |  138584   28287  1674392    59.2 |  1.787 % |
c |     97235 |  258138   631143 |  152442   29046  1708620    58.8 |  1.787 % |
c |     98375 |  258138   631143 |  167687   30186  1789788    59.3 |  1.787 % |
c |    100087 |  258138   631143 |  184455   31898  1905905    59.7 |  1.787 % |
c ==============================================================================
c [1mFound solution: 330534[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 |    102099 |  258141   631152 |   86047   33908  2049525    60.4 |  1.787 % |
c |    102201 |  258141   631152 |   94651   34010  2050464    60.3 |  1.791 % |
c |    102351 |  258141   631152 |  104116   34160  2054690    60.1 |  1.791 % |
c |    102576 |  258141   631152 |  114528   34385  2064233    60.0 |  1.791 % |
c |    102914 |  258132   631134 |  125981   34721  2096107    60.4 |  1.795 % |
c |    103420 |  258123   631116 |  138579   35225  2138135    60.7 |  1.799 % |
c |    104180 |  258123   631116 |  152437   35985  2168832    60.3 |  1.799 % |
c |    105320 |  258123   631116 |  167681   37125  2265246    61.0 |  1.799 % |
c |    107028 |  258123   631116 |  184449   38833  2578414    66.4 |  1.799 % |
c |    109591 |  258105   631080 |  202894   41395  2715872    65.6 |  1.808 % |
c ==============================================================================
c [1mFound solution: 330532[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 |    110485 |  258116   631107 |   86038   42289  2828505    66.9 |  1.808 % |
c |    110586 |  258099   631073 |   94641   42389  2840524    67.0 |  1.818 % |
c |    110736 |  258088   631051 |  104105   42536  2846739    66.9 |  1.822 % |
c |    110964 |  258088   631051 |  114516   42764  2848455    66.6 |  1.822 % |
c |    111301 |  258088   631051 |  125968   43101  2852967    66.2 |  1.822 % |
c |    111808 |  258088   631051 |  138565   43608  2867535    65.8 |  1.822 % |
c ==============================================================================
c [1mFound solution: 330344[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 |    112455 |  258096   631071 |   86032   44254  2898369    65.5 |  1.822 % |
c |    112555 |  258096   631071 |   94635   44354  2898888    65.4 |  1.825 % |
c |    112705 |  258090   631059 |  104098   44503  2907865    65.3 |  1.828 % |
c |    112930 |  258086   631051 |  114508   44727  2920418    65.3 |  1.830 % |
c |    113270 |  258086   631051 |  125959   45067  2944898    65.3 |  1.830 % |
c |    113778 |  258086   631051 |  138555   45575  2997382    65.8 |  1.830 % |
c |    114541 |  258058   630995 |  152410   46335  3026520    65.3 |  1.844 % |
c |    115680 |  258032   630943 |  167652   47470  3094584    65.2 |  1.856 % |
c |    117388 |  258023   630925 |  184417   49177  3249344    66.1 |  1.861 % |
c ==============================================================================
c [1mFound solution: 327168[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 |    118671 |  258035   630957 |   86011   50460  3384068    67.1 |  1.861 % |
c |    118772 |  258035   630957 |   94612   50561  3384947    66.9 |  1.862 % |
c |    118922 |  258035   630957 |  104073   50711  3385943    66.8 |  1.862 % |
c |    119147 |  258035   630957 |  114480   50936  3393108    66.6 |  1.862 % |
c |    119485 |  257975   630822 |  125928   51270  3408370    66.5 |  1.880 % |
c |    119991 |  257973   630818 |  138521   51775  3435578    66.4 |  1.882 % |
c |    120751 |  257967   630806 |  152373   52534  3481224    66.3 |  1.885 % |
c ==============================================================================
c [1mFound solution: 327087[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 |    121845 |  257978   630834 |   85992   53628  3589608    66.9 |  1.885 % |
c |    121945 |  257978   630834 |   94591   53728  3590157    66.8 |  1.886 % |
c |    122095 |  257978   630834 |  104050   53878  3590947    66.6 |  1.886 % |
c |    122320 |  257968   630814 |  114455   54102  3595243    66.5 |  1.891 % |
c |    122657 |  257968   630814 |  125900   54439  3621169    66.5 |  1.891 % |
c |    123163 |  257968   630814 |  138490   54945  3657376    66.6 |  1.891 % |
c |    123922 |  257962   630802 |  152340   55702  3697323    66.4 |  1.895 % |
c ==============================================================================
c [1mFound solution: 326761[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 |    124101 |  257978   630840 |   85992   55881  3725280    66.7 |  1.895 % |
c |    124201 |  257973   630830 |   94591   55980  3736888    66.8 |  1.898 % |
c |    124353 |  257973   630830 |  104050   56132  3744535    66.7 |  1.898 % |
c ==============================================================================
c [1mFound solution: 325755[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 |    124528 |  257984   630856 |   85994   56307  3761684    66.8 |  1.898 % |
c |    124628 |  257984   630856 |   94593   56407  3762535    66.7 |  1.899 % |
c |    124780 |  257984   630856 |  104052   56559  3765066    66.6 |  1.899 % |
c |    125005 |  257984   630856 |  114458   56784  3767067    66.3 |  1.899 % |
c |    125342 |  257976   630840 |  125903   57120  3790584    66.4 |  1.903 % |
c ==============================================================================
c [1mFound solution: 324296[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 |    125572 |  257985   630861 |   85995   57350  3807964    66.4 |  1.903 % |
c |    125675 |  257985   630861 |   94594   57453  3816308    66.4 |  1.904 % |
c |    125827 |  257985   630861 |  104053   57605  3827887    66.5 |  1.904 % |
c |    126052 |  257985   630861 |  114459   57830  3843328    66.5 |  1.904 % |
c |    126389 |  257985   630861 |  125905   58167  3869622    66.5 |  1.904 % |
c |    126897 |  257985   630861 |  138495   58675  3926248    66.9 |  1.904 % |
c |    127657 |  257985   630861 |  152345   59435  3970340    66.8 |  1.904 % |
c |    128797 |  257985   630861 |  167579   60575  4091789    67.5 |  1.904 % |
c ==============================================================================
c [1mFound solution: 324294[0m
c ---[   0]---> Sorter-cost:    3     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 |    129958 |  257989   630870 |   85996   61736  4150369    67.2 |  1.904 % |
c |    130058 |  257989   630870 |   94595   61836  4156458    67.2 |  1.905 % |
c |    130208 |  257989   630870 |  104055   61986  4157553    67.1 |  1.905 % |
c |    130435 |  257989   630870 |  114460   62213  4163857    66.9 |  1.905 % |
c |    130773 |  257989   630870 |  125906   62551  4212703    67.3 |  1.905 % |
c |    131280 |  257989   630870 |  138497   63058  4277068    67.8 |  1.905 % |
c ==============================================================================
c [1mFound solution: 324261[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 |    131425 |  258003   630905 |   86001   63203  4296758    68.0 |  1.905 % |
c |    131527 |  258003   630905 |   94601   63305  4297414    67.9 |  1.906 % |
c |    131678 |  258003   630905 |  104061   63456  4298367    67.7 |  1.906 % |
c |    131903 |  258003   630905 |  114467   63681  4317691    67.8 |  1.906 % |
c |    132241 |  258003   630905 |  125914   64019  4334770    67.7 |  1.906 % |
c |    132748 |  258003   630905 |  138505   64526  4366368    67.7 |  1.906 % |
c ==============================================================================
c [1mFound solution: 323811[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 |    133502 |  258012   630926 |   86004   65280  4440378    68.0 |  1.906 % |
c |    133603 |  258012   630926 |   94604   65381  4449184    68.1 |  1.907 % |
c |    133753 |  258012   630926 |  104064   65531  4485658    68.5 |  1.907 % |
c |    133979 |  258012   630926 |  114471   65757  4494120    68.3 |  1.907 % |
c |    134316 |  258012   630926 |  125918   66094  4535646    68.6 |  1.907 % |
c ==============================================================================
c [1mFound solution: 323792[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 |    134432 |  258026   630960 |   86008   66210  4546111    68.7 |  1.907 % |
c |    134532 |  258026   630960 |   94608   66310  4548959    68.6 |  1.908 % |
c |    134683 |  258018   630942 |  104069   66460  4550008    68.5 |  1.910 % |
c |    134908 |  258018   630942 |  114476   66685  4553484    68.3 |  1.910 % |
c |    135245 |  258018   630942 |  125924   67022  4569647    68.2 |  1.910 % |
c |    135751 |  258018   630942 |  138516   67528  4644702    68.8 |  1.910 % |
c ==============================================================================
c [1mFound solution: 274665[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 |    136125 |  258042   631003 |   86014   67902  4677304    68.9 |  1.910 % |
c |    136225 |  257923   630734 |   94615   67999  4677961    68.8 |  1.947 % |
c |    136375 |  257905   630693 |  104076   68147  4678723    68.7 |  1.953 % |
c |    136600 |  257883   630643 |  114484   68367  4683640    68.5 |  1.959 % |
c ==============================================================================
c [1mFound solution: 265977[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 |    136819 |  257890   630660 |   85963   68586  4707183    68.6 |  1.959 % |
c |    136919 |  257890   630660 |   94559   68686  4708971    68.6 |  1.960 % |
c ==============================================================================
c [1mFound solution: 265974[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 |    137059 |  257897   630678 |   85965   68826  4713599    68.5 |  1.960 % |
c |    137159 |  257880   630640 |   94561   68923  4714256    68.4 |  1.969 % |
c |    137309 |  257880   630640 |  104017   69073  4717909    68.3 |  1.969 % |
c ==============================================================================
c [1mFound solution: 265005[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 |    137468 |  257889   630662 |   85963   69232  4721996    68.2 |  1.969 % |
c |    137568 |  257889   630662 |   94559   69332  4726681    68.2 |  1.970 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11938 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): 1.00 0.97 0.91 2/54 11934
Raw data (stat): 11934 (runsolver) R 11933 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796985870 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.0015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.0017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.0027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.0036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.0034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.0044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 11938
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.075 s]
Raw data (loadavg): 1.08 0.99 0.91 2/57 11979
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.075 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 11991
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.075 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 11991
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.075 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 11991
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 11991
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 11991
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.075 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 11991
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11991
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.073 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.073 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.073 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11993
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 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.75 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 11995
Raw data (stat): 11934 (minisat+_script) S 11933 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796985870 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.75
CPU time (s): 1229.86
CPU user time (s): 1229.16
CPU system time (s): 0.702893
CPU usage (%): 100.009
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####