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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-egout.opb
MD5SUM	9f6abccf92594d7ee18b1409c45097d3
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	471047168
Optimality of the best value was proved	NO
Number of terms in the objective function	1615
Biggest coefficient in the objective function	545997717504
Number of bits for the biggest coefficient in the objective function	39
Sum of the numbers in the objective function	15186728411329
Number of bits of the sum of numbers in the objective function	44
Biggest number in a constraint	545997717504
Number of bits of the biggest number in a constraint	39
Biggest sum of numbers in a constraint	15186728411329
Number of bits of the biggest sum of numbers	44
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1098.43
Number of variables	1705
Total number of constraints	153
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	98
Minimum length of a constraint	1
Maximum length of a constraint	420
Trace number 31880

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-05-27 06:37:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23264 boxname=wulflinc1 idbench=908 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9f6abccf92594d7ee18b1409c45097d3  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-egout.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-egout.opb
IDLAUNCH: 23264
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        916648 kB
Buffers:           160 kB
Cached:          93400 kB
SwapCached:        688 kB
Active:          27108 kB
Inactive:        68600 kB
HighTotal:      131008 kB
HighFree:        34524 kB
LowTotal:       903652 kB
LowFree:        882124 kB
SwapTotal:     2097136 kB
SwapFree:      2095364 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            16396 kB
Committed_AS:    92716 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 06:57:41 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23264 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 115 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 113]---> BDD-cost: 2699
c ---[ 111]---> BDD-cost:   55
c ---[ 109]---> BDD-cost:   34
c ---[ 107]---> BDD-cost:   60
c ---[ 105]---> BDD-cost:  110
c ---[ 101]---> BDD-cost:   48
c ---[  99]---> BDD-cost:  127
c ---[  97]---> BDD-cost:   43
c ---[  91]---> BDD-cost:   70
c ---[  89]---> BDD-cost:   49
c ---[  85]---> BDD-cost:  155
c ---[  83]---> BDD-cost:   49
c ---[  81]---> BDD-cost:  139
c ---[  79]---> BDD-cost:   58
c ---[  75]---> BDD-cost:   60
c ---[  73]---> BDD-cost:   37
c ---[  71]---> BDD-cost:  268
c ---[  69]---> BDD-cost:   70
c ---[  67]---> BDD-cost:  150
c ---[  65]---> BDD-cost:  145
c ---[  59]---> BDD-cost:   60
c ---[  57]---> BDD-cost:   49
c ---[  55]---> BDD-cost:   49
c ---[  53]---> BDD-cost:   60
c ---[  49]---> BDD-cost:  162
c ---[  47]---> BDD-cost:  162
c ---[  45]---> BDD-cost:   58
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   12
c ---[  42]---> BDD-cost:   12
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   31
c ---[  26]---> BDD-cost:   31
c ---[  25]---> BDD-cost:   31
c ---[  24]---> BDD-cost:   31
c ---[  23]---> BDD-cost:   31
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   13
c ---[  18]---> BDD-cost:   31
c ---[  17]---> BDD-cost:   31
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   31
c ---[  13]---> BDD-cost:   31
c ---[  12]---> BDD-cost:   31
c ---[   9]---> BDD-cost:   31
c ---[   8]---> BDD-cost:   31
c ---[   7]---> BDD-cost:   31
c ---[   6]---> BDD-cost:   31
c ---[   4]---> BDD-cost:   31
c ---[   3]---> BDD-cost:   31
c ---[   2]---> BDD-cost:   31
c ---[   1]---> BDD-cost:   31
c ---[   0]---> BDD-cost:   31
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   14369    39481 |    4789       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 805141925[0m
c ---[   0]---> Sorter-cost:119958     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        66 |  355558   835931 |  118519      66      785    11.9 |  0.000 % |
c |       167 |  355542   835899 |  130370     159     2931    18.4 |  0.951 % |
c |       318 |  355003   834675 |  143407     288     4900    17.0 |  1.077 % |
c |       543 |  354997   834663 |  157748     510     7075    13.9 |  1.080 % |
c |       880 |  354997   834663 |  173523     847    12212    14.4 |  1.080 % |
c |      1387 |  354995   834659 |  190876    1353    17267    12.8 |  1.080 % |
c |      2146 |  354995   834659 |  209963    2112    25677    12.2 |  1.080 % |
c |      3286 |  354971   834609 |  230960    3241    43817    13.5 |  1.089 % |
c |      4995 |  346831   816058 |  254056    4839    60219    12.4 |  3.036 % |
c ==============================================================================
c [1mFound solution: 693433625[0m
c ---[   0]---> Sorter-cost:67441     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6169 |  534495  1254643 |  178165    5988    87967    14.7 |  3.036 % |
c ==============================================================================
c [1mFound solution: 627044928[0m
c ---[   0]---> Sorter-cost:58228     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6263 |  693189  1625507 |  231063    6075    89176    14.7 |  3.036 % |
c |      6363 |  689034  1616068 |  254169    6139    90613    14.8 |  2.477 % |
c |      6513 |  687417  1612376 |  279586    6281    95396    15.2 |  2.670 % |
c |      6738 |  687041  1611532 |  307544    6505    98615    15.2 |  2.716 % |
c |      7075 |  686697  1610744 |  338299    6840   101272    14.8 |  2.764 % |
c |      7582 |  686412  1610101 |  372129    7339   104530    14.2 |  2.796 % |
c |      8341 |  686168  1609544 |  409342    8080   115844    14.3 |  2.826 % |
c |      9480 |  685646  1608363 |  450276    9196   144194    15.7 |  2.885 % |
c |     11188 |  682193  1600515 |  495304   10784   172874    16.0 |  3.306 % |
c ==============================================================================
c [1mFound solution: 610226178[0m
c ---[   0]---> Sorter-cost:51898     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12467 |  822654  1928511 |  274218   12048   238829    19.8 |  3.306 % |
c |     12567 |  822654  1928511 |  301639   12148   241728    19.9 |  2.929 % |
c |     12718 |  822644  1928491 |  331803   12294   251104    20.4 |  2.930 % |
c ==============================================================================
c [1mFound solution: 595489984[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12807 |  823836  1931939 |  274612   12381   256199    20.7 |  2.930 % |
c |     12908 |  823808  1931880 |  302073   12481   259601    20.8 |  2.939 % |
c |     13058 |  823542  1931285 |  332280   12627   261381    20.7 |  2.965 % |
c |     13286 |  823301  1930744 |  365508   12853   283130    22.0 |  2.986 % |
c |     13623 |  822985  1930038 |  402059   13184   285402    21.6 |  3.017 % |
c |     14131 |  822789  1929591 |  442265   13681   288469    21.1 |  3.037 % |
c |     14890 |  822789  1929591 |  486491   14440   381052    26.4 |  3.037 % |
c ==============================================================================
c [1mFound solution: 592788480[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15731 |  822681  1929510 |  274227   15271   441411    28.9 |  3.037 % |
c |     15832 |  822681  1929510 |  301649   15372   447790    29.1 |  3.054 % |
c |     15982 |  822681  1929510 |  331814   15522   453780    29.2 |  3.054 % |
c |     16209 |  822385  1928851 |  364996   15742   457293    29.0 |  3.088 % |
c |     16547 |  822200  1928432 |  401495   16073   462639    28.8 |  3.107 % |
c |     17053 |  821563  1926986 |  441645   16574   503787    30.4 |  3.172 % |
c ==============================================================================
c [1mFound solution: 592786453[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17623 |  821241  1926252 |  273747   17142   537030    31.3 |  3.172 % |
c |     17725 |  821140  1926027 |  301121   17238   537734    31.2 |  3.217 % |
c |     17877 |  821140  1926027 |  331233   17390   539810    31.0 |  3.217 % |
c |     18102 |  821140  1926027 |  364357   17615   542981    30.8 |  3.217 % |
c |     18439 |  821140  1926027 |  400792   17952   544950    30.4 |  3.217 % |
c |     18945 |  821128  1926000 |  440872   18457   550774    29.8 |  3.218 % |
c |     19704 |  821128  1926000 |  484959   19216   558479    29.1 |  3.218 % |
c |     20843 |  820989  1925687 |  533455   20351   581791    28.6 |  3.231 % |
c ==============================================================================
c [1mFound solution: 585102784[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21112 |  821558  1927129 |  273852   20619   587623    28.5 |  3.231 % |
c |     21212 |  821558  1927129 |  301237   20719   591749    28.6 |  3.268 % |
c ==============================================================================
c [1mFound solution: 582696448[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21251 |  821576  1927266 |  273858   20758   593004    28.6 |  3.268 % |
c |     21354 |  821576  1927266 |  301243   20861   602977    28.9 |  3.268 % |
c |     21505 |  821576  1927266 |  331368   21012   614923    29.3 |  3.268 % |
c |     21731 |  821389  1926845 |  364504   21199   618333    29.2 |  3.292 % |
c |     22068 |  821206  1926435 |  400955   21531   623248    28.9 |  3.311 % |
c ==============================================================================
c [1mFound solution: 580180606[0m
c ---[   0]---> Sorter-cost:   23     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22508 |  820467  1924863 |  273489   21949   641546    29.2 |  3.311 % |
c |     22608 |  820467  1924863 |  300837   22049   643153    29.2 |  3.389 % |
c |     22758 |  820467  1924863 |  330921   22199   650135    29.3 |  3.389 % |
c ==============================================================================
c [1mFound solution: 580136448[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22918 |  820404  1924726 |  273468   22350   659384    29.5 |  3.389 % |
c |     23018 |  820404  1924726 |  300814   22450   662910    29.5 |  3.397 % |
c |     23168 |  820404  1924726 |  330896   22600   670277    29.7 |  3.397 % |
c ==============================================================================
c [1mFound solution: 564539392[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23391 |  820419  1924766 |  273473   22823   685329    30.0 |  3.397 % |
c |     23491 |  820419  1924766 |  300820   22923   689534    30.1 |  3.398 % |
c |     23641 |  820210  1924292 |  330902   23072   691554    30.0 |  3.418 % |
c |     23866 |  820210  1924292 |  363992   23297   700592    30.1 |  3.418 % |
c ==============================================================================
c [1mFound solution: 562189312[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24053 |  820228  1924332 |  273409   23484   704972    30.0 |  3.418 % |
c |     24153 |  819990  1923796 |  300749   23490   706040    30.1 |  3.443 % |
c |     24304 |  819990  1923796 |  330824   23641   707828    29.9 |  3.443 % |
c |     24529 |  819990  1923796 |  363907   23866   712262    29.8 |  3.443 % |
c |     24866 |  819847  1923472 |  400298   24195   718187    29.7 |  3.458 % |
c |     25373 |  819794  1923351 |  440327   24698   740958    30.0 |  3.463 % |
c ==============================================================================
c [1mFound solution: 560797696[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25956 |  819806  1923387 |  273268   25274   773320    30.6 |  3.463 % |
c |     26058 |  819806  1923387 |  300594   25376   776753    30.6 |  3.466 % |
c |     26210 |  819684  1923108 |  330654   25527   777601    30.5 |  3.478 % |
c |     26438 |  819607  1922935 |  363719   25754   782252    30.4 |  3.486 % |
c |     26775 |  819437  1922551 |  400091   26084   785386    30.1 |  3.500 % |
c |     27282 |  819437  1922551 |  440100   26591   811735    30.5 |  3.500 % |
c |     28041 |  819437  1922551 |  484110   27350   847855    31.0 |  3.500 % |
c ==============================================================================
c [1mFound solution: 559447136[0m
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29005 |  817206  1917496 |  272402   28245   873188    30.9 |  3.500 % |
c |     29105 |  817206  1917496 |  299642   28345   879692    31.0 |  3.720 % |
c |     29255 |  817206  1917496 |  329606   28495   886613    31.1 |  3.720 % |
c |     29480 |  815964  1914652 |  362567   28595   894072    31.3 |  3.850 % |
c |     29817 |  815964  1914652 |  398823   28932  1039160    35.9 |  3.850 % |
c |     30323 |  815964  1914652 |  438706   29438  1044635    35.5 |  3.850 % |
c |     31084 |  815862  1914420 |  482576   30197  1065775    35.3 |  3.860 % |
c |     32223 |  815526  1913651 |  530834   31331  1124877    35.9 |  3.895 % |
c ==============================================================================
c [1mFound solution: 556216273[0m
c ---[   0]---> Sorter-cost:   22     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32682 |  815552  1913715 |  271850   31790  1169685    36.8 |  3.895 % |
c |     32782 |  815455  1913496 |  299035   31874  1170446    36.7 |  3.906 % |
c |     32932 |  815455  1913496 |  328938   32024  1173372    36.6 |  3.906 % |
c ==============================================================================
c [1mFound solution: 548503552[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32963 |  815474  1913541 |  271824   32055  1176260    36.7 |  3.906 % |
c |     33063 |  815474  1913541 |  299006   32155  1181197    36.7 |  3.906 % |
c |     33213 |  815474  1913541 |  328907   32305  1194425    37.0 |  3.906 % |
c |     33439 |  815474  1913541 |  361797   32531  1198698    36.8 |  3.906 % |
c |     33776 |  815474  1913541 |  397977   32868  1206913    36.7 |  3.906 % |
c |     34282 |  815474  1913541 |  437775   33374  1227916    36.8 |  3.906 % |
c |     35042 |  815130  1912758 |  481552   34063  1234813    36.3 |  3.942 % |
c |     36183 |  815040  1912556 |  529708   35202  1244070    35.3 |  3.952 % |
c ==============================================================================
c [1mFound solution: 548432896[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36758 |  814995  1912453 |  271665   35776  1298628    36.3 |  3.952 % |
c |     36858 |  814351  1910981 |  298831   35864  1299110    36.2 |  4.024 % |
c ==============================================================================
c [1mFound solution: 546178560[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36951 |  813913  1909990 |  271304   35922  1309640    36.5 |  4.024 % |
c |     37051 |  813913  1909990 |  298434   36022  1313569    36.5 |  4.069 % |
c |     37201 |  813913  1909990 |  328277   36172  1323156    36.6 |  4.069 % |
c |     37426 |  813913  1909990 |  361105   36397  1344937    37.0 |  4.069 % |
c |     37764 |  813913  1909990 |  397216   36735  1381101    37.6 |  4.069 % |
c |     38270 |  813913  1909990 |  436937   37241  1444694    38.8 |  4.069 % |
c |     39033 |  813547  1909160 |  480631   38000  1505281    39.6 |  4.102 % |
c |     40172 |  813547  1909160 |  528694   39139  1578641    40.3 |  4.102 % |
c ==============================================================================
c [1mFound solution: 545742121[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40316 |  813567  1909216 |  271189   39283  1591101    40.5 |  4.102 % |
c ==============================================================================
c [1mFound solution: 544784974[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40362 |  813586  1909266 |  271195   39329  1593196    40.5 |  4.102 % |
c |     40462 |  813586  1909266 |  298314   39429  1595666    40.5 |  4.103 % |
c |     40612 |  813586  1909266 |  328145   39579  1600674    40.4 |  4.103 % |
c |     40837 |  813586  1909266 |  360960   39804  1605202    40.3 |  4.103 % |
c |     41178 |  813586  1909266 |  397056   40145  1620456    40.4 |  4.103 % |
c ==============================================================================
c [1mFound solution: 512092672[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41342 |  813620  1909354 |  271206   40309  1631697    40.5 |  4.103 % |
c |     41442 |  813620  1909354 |  298326   40409  1633743    40.4 |  4.103 % |
c |     41593 |  813620  1909354 |  328159   40560  1640638    40.4 |  4.103 % |
c |     41819 |  813620  1909354 |  360975   40786  1649495    40.4 |  4.103 % |
c |     42157 |  813620  1909354 |  397072   41124  1664682    40.5 |  4.103 % |
c |     42663 |  813620  1909354 |  436779   41630  1698789    40.8 |  4.103 % |
c |     43422 |  813620  1909354 |  480457   42389  1719587    40.6 |  4.103 % |
c |     44562 |  813459  1908986 |  528503   43527  1769643    40.7 |  4.120 % |
c ==============================================================================
c [1mFound solution: 510765936[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44845 |  813482  1909044 |  271160   43810  1781223    40.7 |  4.120 % |
c ==============================================================================
c [1mFound solution: 510470144[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44904 |  813496  1909077 |  271165   43869  1789181    40.8 |  4.120 % |
c |     45004 |  813339  1908722 |  298281   43957  1794998    40.8 |  4.135 % |
c |     45154 |  813339  1908722 |  328109   44107  1800249    40.8 |  4.135 % |
c |     45381 |  813339  1908722 |  360920   44334  1812993    40.9 |  4.135 % |
c ==============================================================================
c [1mFound solution: 510071808[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45690 |  813353  1908757 |  271117   44643  1834092    41.1 |  4.135 % |
c |     45790 |  813353  1908757 |  298228   44743  1837794    41.1 |  4.135 % |
c |     45940 |  813353  1908757 |  328051   44893  1843014    41.1 |  4.135 % |
c ==============================================================================
c [1mFound solution: 509352280[0m
c ---[   0]---> Sorter-cost:   22     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46143 |  813379  1908820 |  271126   45096  1852102    41.1 |  4.135 % |
c |     46244 |  813379  1908820 |  298238   45197  1856933    41.1 |  4.135 % |
c ==============================================================================
c [1mFound solution: 509258240[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46391 |  813398  1908867 |  271132   45344  1868804    41.2 |  4.135 % |
c |     46491 |  813398  1908867 |  298245   45444  1870803    41.2 |  4.136 % |
c |     46641 |  813398  1908867 |  328069   45594  1887724    41.4 |  4.136 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  2189 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/55 2185
Raw data (stat): 2185 (runsolver) R 2184 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 738977198 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.88 0.94 0.90 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.0012 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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): 0.91 0.94 0.90 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.0016 s]
Raw data (loadavg): 0.93 0.95 0.90 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.0014 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.0022 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.0019 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.98 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.98 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.96 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.72 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2189
Raw data (stat): 2185 (minisat+_script) S 2184 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738977198 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.72
CPU time (s): 1229.88
CPU user time (s): 1229.12
CPU system time (s): 0.764883
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####