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-gt2.opb
MD5SUM	f1382105ee9fb79777762a53cf6a73c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	21166
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	62376
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	3092598
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	62376
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	3092598
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.14
Number of variables	556
Total number of constraints	217
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	191
Minimum length of a constraint	1
Maximum length of a constraint	48
Trace number 32397

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-27 09:37:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23775 boxname=wulflinc23 idbench=1419 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-gt2.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-gt2.opb
IDLAUNCH: 23775
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        857416 kB
Buffers:         10936 kB
Cached:         146088 kB
SwapCached:        736 kB
Active:          17384 kB
Inactive:       141728 kB
HighTotal:      131008 kB
HighFree:        28728 kB
LowTotal:       903652 kB
LowFree:        828688 kB
SwapTotal:     2097136 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4936 kB
Slab:            12428 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 09:57:48 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 23775 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  71]---> BDD-cost:    2
c ---[  70]---> BDD-cost:    2
c ---[  68]---> BDD-cost:    2
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  37]---> BDD-cost:  107
c ---[  36]---> BDD-cost:  231
c ---[  35]---> BDD-cost:  231
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> BDD-cost:  126
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> BDD-cost:  185
c ---[  25]---> BDD-cost:  111
c ---[  24]---> BDD-cost:  105
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:   54
c ---[  21]---> BDD-cost:   21
c ---[  15]---> BDD-cost: 7378
c ---[   9]---> BDD-cost:  669
c ---[   8]---> BDD-cost:   76
c ---[   7]---> BDD-cost: 1557
c ---[   6]---> BDD-cost: 1215
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> BDD-cost: 2937
c ---[   1]---> BDD-cost: 1052
c ---[   0]---> BDD-cost:   92
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   45289   134500 |   15096       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 228152[0m
c ---[   0]---> Sorter-cost:92447     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |  298890   726329 |   99630       2       12     6.0 |  0.000 % |
c |       105 |  298124   724597 |  109593     101      535     5.3 |  0.281 % |
c |       255 |  297317   722773 |  120552     250     5224    20.9 |  0.486 % |
c |       480 |  295636   718946 |  132607     471    10583    22.5 |  0.945 % |
c |       817 |  293957   715105 |  145868     806    24487    30.4 |  1.417 % |
c |      1325 |  287505   700303 |  160455    1282    27144    21.2 |  3.285 % |
c |      2086 |  274412   670155 |  176500    1959    41217    21.0 |  7.185 % |
c ==============================================================================
c [1mFound solution: 228107[0m
c ---[   0]---> Sorter-cost:72978     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2182 |  455370  1091535 |  151790    2051    43708    21.3 |  7.185 % |
c |      2282 |  455370  1091535 |  166969    2151    45808    21.3 |  7.218 % |
c |      2432 |  450153  1079714 |  183665    2295    49252    21.5 |  8.191 % |
c |      2657 |  450153  1079714 |  202032    2520    53000    21.0 |  8.191 % |
c |      2994 |  441724  1060467 |  222235    2817    56525    20.1 |  9.728 % |
c |      3500 |  441049  1058922 |  244459    3317    64078    19.3 |  9.849 % |
c |      4259 |  441049  1058922 |  268905    4076    70538    17.3 |  9.849 % |
c |      5398 |  441049  1058922 |  295795    5215    81194    15.6 |  9.849 % |
c |      7108 |  440946  1058682 |  325375    6924   102009    14.7 |  9.869 % |
c ==============================================================================
c [1mFound solution: 228003[0m
c ---[   0]---> Sorter-cost:68318     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7782 |  598189  1424680 |  199396    7400   107739    14.6 |  9.869 % |
c |      7883 |  598038  1424335 |  219335    7499   109071    14.5 | 11.279 % |
c |      8033 |  593293  1413534 |  241269    7260   106197    14.6 | 11.923 % |
c |      8260 |  593279  1413501 |  265396    7440   120478    16.2 | 11.925 % |
c ==============================================================================
c [1mFound solution: 226571[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8298 |  593064  1413790 |  197688    7476   124044    16.6 | 11.925 % |
c |      8398 |  592851  1413314 |  217456    7572   125841    16.6 | 11.979 % |
c |      8548 |  592248  1411977 |  239202    7719   126514    16.4 | 12.064 % |
c ==============================================================================
c [1mFound solution: 225156[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8610 |  589147  1404947 |  196382    7720   126643    16.4 | 12.064 % |
c |      8710 |  589147  1404947 |  216020    7820   127668    16.3 | 12.483 % |
c |      8861 |  589147  1404947 |  237622    7971   128755    16.2 | 12.483 % |
c |      9086 |  587881  1402070 |  261384    8192   130321    15.9 | 12.657 % |
c |      9424 |  581084  1386553 |  287522    8444   131552    15.6 | 13.585 % |
c |      9930 |  577887  1379236 |  316275    8856   141272    16.0 | 14.021 % |
c |     10689 |  575421  1373584 |  347902    9496   146897    15.5 | 14.357 % |
c |     11828 |  574402  1371278 |  382692   10609   187884    17.7 | 14.493 % |
c |     13538 |  570586  1362558 |  420962   12281   264267    21.5 | 15.004 % |
c |     16101 |  569103  1359156 |  463058   14831   402467    27.1 | 15.208 % |
c |     19945 |  567496  1355462 |  509364   18667   828516    44.4 | 15.426 % |
c ==============================================================================
c [1mFound solution: 224882[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20299 |  567509  1355605 |  189169   19021   836114    44.0 | 15.426 % |
c |     20399 |  567509  1355605 |  208085   19121   840088    43.9 | 15.426 % |
c |     20549 |  567329  1355202 |  228894   19269   844134    43.8 | 15.446 % |
c |     20774 |  564229  1348123 |  251783   19421   844924    43.5 | 15.867 % |
c |     21111 |  564229  1348123 |  276962   19758   850448    43.0 | 15.867 % |
c |     21617 |  564126  1347891 |  304658   20263   857199    42.3 | 15.882 % |
c |     22378 |  563650  1346812 |  335124   21011   862862    41.1 | 15.947 % |
c |     23517 |  561569  1342052 |  368636   22103   881716    39.9 | 16.231 % |
c ==============================================================================
c [1mFound solution: 222653[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24619 |  558563  1335130 |  186187   22960   956712    41.7 | 16.231 % |
c |     24719 |  558563  1335130 |  204805   23060   958791    41.6 | 16.639 % |
c |     24871 |  558539  1335075 |  225286   23211   963417    41.5 | 16.642 % |
c |     25098 |  556797  1331061 |  247814   23357   966618    41.4 | 16.880 % |
c |     25435 |  551457  1318704 |  272596   23537   966536    41.1 | 17.622 % |
c |     25941 |  551302  1318351 |  299856   24037   977475    40.7 | 17.643 % |
c |     26703 |  551302  1318351 |  329841   24799  1021116    41.2 | 17.643 % |
c ==============================================================================
c [1mFound solution: 120481[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26816 |  551347  1318463 |  183782   24912  1024011    41.1 | 17.643 % |
c |     26918 |  551301  1318356 |  202160   25013  1025225    41.0 | 17.649 % |
c |     27068 |  551301  1318356 |  222376   25163  1031087    41.0 | 17.649 % |
c |     27296 |  551301  1318356 |  244613   25391  1065796    42.0 | 17.649 % |
c |     27633 |  549875  1315069 |  269075   25550  1084183    42.4 | 17.844 % |
c |     28139 |  549517  1314253 |  295982   26053  1088933    41.8 | 17.889 % |
c |     28899 |  548230  1311311 |  325581   26791  1097334    41.0 | 18.056 % |
c |     30038 |  543493  1300399 |  358139   27750  1115651    40.2 | 18.701 % |
c ==============================================================================
c [1mFound solution: 119791[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30534 |  543495  1300408 |  181165   28245  1134636    40.2 | 18.701 % |
c |     30634 |  542867  1298964 |  199281   28327  1137163    40.1 | 18.787 % |
c |     30787 |  542867  1298964 |  219209   28480  1140643    40.1 | 18.787 % |
c |     31012 |  542867  1298964 |  241130   28705  1152607    40.2 | 18.787 % |
c |     31349 |  538587  1289074 |  265243   28715  1156875    40.3 | 19.378 % |
c |     31855 |  538397  1288634 |  291768   29217  1161472    39.8 | 19.404 % |
c |     32614 |  537715  1287065 |  320944   29869  1170464    39.2 | 19.497 % |
c |     33753 |  537468  1286494 |  353039   30995  1187597    38.3 | 19.532 % |
c |     35462 |  533253  1276753 |  388343   32596  1263680    38.8 | 20.112 % |
c ==============================================================================
c [1mFound solution: 118096[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35657 |  533267  1276787 |  177755   32791  1284635    39.2 | 20.112 % |
c |     35757 |  533267  1276787 |  195530   32891  1287773    39.2 | 20.112 % |
c |     35907 |  532417  1274825 |  215083   32963  1288290    39.1 | 20.229 % |
c |     36132 |  532417  1274825 |  236591   33188  1299883    39.2 | 20.229 % |
c |     36469 |  532417  1274825 |  260251   33525  1302922    38.9 | 20.229 % |
c |     36975 |  531944  1273732 |  286276   33906  1320618    38.9 | 20.296 % |
c |     37734 |  531944  1273732 |  314903   34665  1341440    38.7 | 20.296 % |
c |     38874 |  531861  1273544 |  346394   35803  1419556    39.6 | 20.307 % |
c |     40582 |  530900  1271335 |  381033   37504  1515069    40.4 | 20.437 % |
c ==============================================================================
c [1mFound solution: 116340[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41153 |  530748  1270984 |  176916   38066  1536021    40.4 | 20.437 % |
c |     41253 |  529765  1268705 |  194607   38156  1537843    40.3 | 20.596 % |
c |     41404 |  527957  1264539 |  214068   38170  1538217    40.3 | 20.841 % |
c |     41629 |  526967  1262274 |  235475   38379  1546527    40.3 | 20.973 % |
c |     41967 |  526967  1262274 |  259022   38717  1552391    40.1 | 20.973 % |
c |     42473 |  526311  1260774 |  284924   39078  1554205    39.8 | 21.060 % |
c |     43233 |  526311  1260774 |  313417   39838  1564762    39.3 | 21.060 % |
c |     44374 |  525407  1258697 |  344759   40934  1610696    39.3 | 21.184 % |
c |     46082 |  524738  1257157 |  379235   42622  1729510    40.6 | 21.277 % |
c ==============================================================================
c [1mFound solution: 112950[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46141 |  524322  1256197 |  174774   42680  1736911    40.7 | 21.277 % |
c |     46241 |  524322  1256197 |  192251   42780  1740112    40.7 | 21.336 % |
c |     46394 |  524322  1256197 |  211476   42933  1741348    40.6 | 21.336 % |
c |     46620 |  524322  1256197 |  232624   43159  1743123    40.4 | 21.336 % |
c |     46957 |  524322  1256197 |  255886   43496  1745234    40.1 | 21.336 % |
c |     47463 |  524322  1256197 |  281475   44002  1749672    39.8 | 21.336 % |
c |     48222 |  523760  1254895 |  309622   44748  1761216    39.4 | 21.416 % |
c |     49365 |  523760  1254895 |  340585   45891  1789036    39.0 | 21.416 % |
c |     51074 |  523451  1254182 |  374643   47542  1918282    40.3 | 21.460 % |
c |     53637 |  523230  1253676 |  412107   50100  2089988    41.7 | 21.489 % |
c |     57482 |  519536  1245170 |  453318   53663  2331890    43.5 | 21.985 % |
c ==============================================================================
c [1mFound solution: 110854[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57516 |  519310  1244651 |  173103   53695  2336515    43.5 | 21.985 % |
c |     57616 |  519310  1244651 |  190413   53795  2338342    43.5 | 22.016 % |
c |     57766 |  519310  1244651 |  209454   53945  2342960    43.4 | 22.016 % |
c |     57993 |  519310  1244651 |  230400   54172  2346033    43.3 | 22.016 % |
c |     58330 |  518541  1242880 |  253440   54482  2350570    43.1 | 22.121 % |
c |     58836 |  517156  1239688 |  278784   54936  2353957    42.8 | 22.311 % |
c |     59595 |  516045  1237127 |  306662   55665  2377705    42.7 | 22.463 % |
c |     60735 |  515589  1236076 |  337328   56771  2459751    43.3 | 22.526 % |
c ==============================================================================
c [1mFound solution: 76236[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61651 |  515612  1236131 |  171870   57687  2565392    44.5 | 22.526 % |
c |     61751 |  515374  1235581 |  189057   57781  2570479    44.5 | 22.557 % |
c |     61902 |  515374  1235581 |  207962   57932  2584955    44.6 | 22.557 % |
c |     62127 |  515374  1235581 |  228758   58157  2599969    44.7 | 22.557 % |
c |     62464 |  514964  1234631 |  251634   58440  2615640    44.8 | 22.615 % |
c |     62971 |  513351  1230928 |  276798   58582  2619291    44.7 | 22.835 % |
c |     63731 |  513351  1230928 |  304478   59342  2647464    44.6 | 22.835 % |
c |     64870 |  513351  1230928 |  334926   60481  2666471    44.1 | 22.835 % |
c ==============================================================================
c [1mFound solution: 75858[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66316 |  511544  1226747 |  170514   61832  2879140    46.6 | 22.835 % |
c |     66417 |  511305  1226189 |  187565   61914  2889868    46.7 | 23.122 % |
c |     66567 |  510740  1224874 |  206321   62053  2891563    46.6 | 23.203 % |
c |     66792 |  510726  1224842 |  226954   62276  2898742    46.5 | 23.205 % |
c ==============================================================================
c [1mFound solution: 75739[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66892 |  510498  1224314 |  170166   62374  2904417    46.6 | 23.205 % |
c |     66992 |  510498  1224314 |  187182   62474  2909023    46.6 | 23.240 % |
c |     67142 |  510498  1224314 |  205900   62624  2912865    46.5 | 23.240 % |
c |     67369 |  508841  1220497 |  226490   62692  2913240    46.5 | 23.466 % |
c |     67706 |  508821  1220450 |  249140   63016  2927307    46.5 | 23.469 % |
c |     68213 |  507776  1218035 |  274054   63512  2993275    47.1 | 23.610 % |
c ==============================================================================
c [1mFound solution: 74881[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68289 |  507789  1218067 |  169263   63588  3002926    47.2 | 23.610 % |
c |     68392 |  507789  1218067 |  186189   63691  3017355    47.4 | 23.610 % |
c |     68542 |  507323  1216992 |  204808   63828  3022418    47.4 | 23.677 % |
c |     68767 |  506850  1215908 |  225289   63984  3030816    47.4 | 23.739 % |
c ==============================================================================
c [1mFound solution: 71337[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69043 |  506863  1215947 |  168954   64260  3055644    47.6 | 23.739 % |
c |     69145 |  505567  1212960 |  185849   64309  3057894    47.6 | 23.915 % |
c ==============================================================================
c [1mFound solution: 71054[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69209 |  505562  1212956 |  168520   64372  3059874    47.5 | 23.915 % |
c ==============================================================================
c [1mFound solution: 69614[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69239 |  505572  1212982 |  168524   64402  3061029    47.5 | 23.915 % |
c |     69339 |  505572  1212982 |  185376   64502  3066241    47.5 | 23.916 % |
c |     69490 |  505572  1212982 |  203914   64653  3070609    47.5 | 23.916 % |
c |     69715 |  505572  1212982 |  224305   64878  3077896    47.4 | 23.916 % |
c |     70053 |  505202  1212131 |  246735   65195  3100673    47.6 | 23.963 % |
c ==============================================================================
c [1mFound solution: 68795[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70179 |  505216  1212166 |  168405   65321  3114607    47.7 | 23.963 % |
c |     70279 |  505216  1212166 |  185245   65421  3115979    47.6 | 23.962 % |
c |     70429 |  505123  1211953 |  203770   65570  3118930    47.6 | 23.974 % |
c |     70654 |  504188  1209790 |  224147   65759  3121473    47.5 | 24.104 % |
c |     70991 |  504188  1209790 |  246561   66096  3138484    47.5 | 24.104 % |
c ==============================================================================
c [1mFound solution: 68554[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71011 |  504200  1209821 |  168066   66116  3141878    47.5 | 24.104 % |
c |     71111 |  503917  1209163 |  184872   66212  3164635    47.8 | 24.146 % |
c |     71263 |  503917  1209163 |  203359   66364  3167458    47.7 | 24.146 % |
c |     71488 |  503842  1208992 |  223695   66584  3171024    47.6 | 24.156 % |
c |     71827 |  503415  1208009 |  246065   66702  3173054    47.6 | 24.215 % |
c |     72333 |  503138  1207370 |  270671   67017  3179237    47.4 | 24.254 % |
c |     73093 |  502444  1205777 |  297739   67381  3200953    47.5 | 24.347 % |
c ==============================================================================
c [1mFound solution: 64777[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73150 |  501869  1204457 |  167289   67422  3205237    47.5 | 24.347 % |
c |     73251 |  501809  1204320 |  184017   67522  3216871    47.6 | 24.433 % |
c |     73402 |  499991  1200109 |  202419   66414  3131920    47.2 | 24.681 % |
c |     73627 |  498522  1196710 |  222661   66154  3130036    47.3 | 24.886 % |
c |     73965 |  498515  1196695 |  244927   66489  3135457    47.2 | 24.887 % |
c |     74471 |  497408  1194129 |  269420   66921  3147606    47.0 | 25.043 % |
c |     75232 |  497216  1193682 |  296362   67677  3167750    46.8 | 25.070 % |
c |     76371 |  497216  1193682 |  325998   68816  3212914    46.7 | 25.070 % |
c |     78079 |  497210  1193668 |  358598   70520  3372262    47.8 | 25.071 % |
c ==============================================================================
c [1mFound solution: 64343[0m
c ---[   0]---> Sorter-cost:52219     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78296 |  595370  1421212 |  198456   70737  3420063    48.3 | 25.071 % |
c ==============================================================================
c [1mFound solution: 64308[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78341 |  595405  1421588 |  198468   70782  3424089    48.4 | 25.071 % |
c |     78441 |  594640  1419832 |  218314   70873  3426664    48.3 | 25.761 % |
c |     78591 |  593992  1418326 |  240146   70954  3430454    48.3 | 25.836 % |
c |     78817 |  593992  1418326 |  264160   71180  3442997    48.4 | 25.836 % |
c |     79155 |  593920  1418160 |  290576   71517  3478608    48.6 | 25.844 % |
c |     79661 |  593836  1417966 |  319634   72015  3515965    48.8 | 25.853 % |
c |     80421 |  591282  1412194 |  351598   72537  3570749    49.2 | 26.139 % |
c |     81561 |  590980  1411521 |  386757   73670  3649538    49.5 | 26.173 % |
c |     83270 |  590798  1411120 |  425433   75378  4503969    59.8 | 26.194 % |
c |     85834 |  586920  1402191 |  467977   77813  4694498    60.3 | 26.638 % |
c |     89678 |  586213  1400603 |  514774   81607  5103308    62.5 | 26.720 % |
c ==============================================================================
c [1mFound solution: 52018[0m
c ---[   0]---> Sorter-cost:65838     Base: 2 2 2 2 3 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90997 |  719458  1709984 |  239819   82576  5331159    64.6 | 26.720 % |
c |     91097 |  718738  1708328 |  263800   82666  5337543    64.6 | 26.453 % |
c |     91249 |  718738  1708328 |  290180   82818  5381999    65.0 | 26.453 % |
c |     91475 |  718738  1708328 |  319199   83044  5413728    65.2 | 26.453 % |
c |     91812 |  718383  1707517 |  351118   83376  5435360    65.2 | 26.486 % |
c |     92318 |  718383  1707517 |  386230   83882  5443883    64.9 | 26.486 % |
c |     93077 |  718383  1707517 |  424853   84641  5494325    64.9 | 26.486 % |
c |     94219 |  716739  1703848 |  467339   85767  5575556    65.0 | 26.637 % |
c |     95929 |  716739  1703848 |  514073   87477  5774198    66.0 | 26.637 % |
c |     98491 |  715748  1701587 |  565480   90000  5988895    66.5 | 26.732 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 30030 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.97 0.91 2/54 30026
Raw data (stat): 30026 (runsolver) R 30025 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855138178 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.001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.0017 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.0018 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.0022 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.0027 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.0027 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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): 0.98 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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): 0.99 0.97 0.91 1/53 30030
Raw data (stat): 30026 (minisat+_script) S 30025 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855138178 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.9
CPU user time (s): 1228.85
CPU system time (s): 1.05284
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####