PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-jac3.opb
MD5SUM	43952ea8e0659c6ffd861c99c0b605de
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	15
Optimality of the best value was proved	NO
Number of terms in the objective function	1732
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1732
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1732
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05384
Number of variables	1731
Total number of constraints	1254
Number of constraints which are clauses	1254
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	694
Trace number 6180

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 03:41:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4582 boxname=wulflinc30 idbench=70 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  43952ea8e0659c6ffd861c99c0b605de  /oldhome/oroussel/tmp/wulflinc30/normalized-jac3.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-jac3.opb /oldhome/oroussel/tmp/wulflinc30/normalized-jac3.opb
IDLAUNCH: 4582
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        720176 kB
Buffers:         38260 kB
Cached:         235576 kB
SwapCached:          0 kB
Active:          84780 kB
Inactive:       191912 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        719924 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32128 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:01:20 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 4582 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1254 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1254    24011 |     418       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:97868     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  217946   530878 |   72648       1       48    48.0 |  0.000 % |
c |       101 |  217946   530878 |   79912     101     1091    10.8 |  0.044 % |
c |       252 |  217946   530878 |   87904     252     2742    10.9 |  0.044 % |
c |       478 |  217946   530878 |   96694     478     4415     9.2 |  0.044 % |
c |       815 |  217924   530824 |  106363     814     9029    11.1 |  0.049 % |
c |      1322 |  217565   530007 |  117000    1262    15971    12.7 |  0.174 % |
c |      2084 |  217497   529849 |  128700    2020    34532    17.1 |  0.198 % |
c |      3223 |  217476   529806 |  141570    3153    93393    29.6 |  0.200 % |
c |      4935 |  217476   529806 |  155727    4865   186152    38.3 |  0.200 % |
c |      7497 |  217476   529806 |  171300    7427   524751    70.7 |  0.200 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7534 |  217503   529874 |   72501    7464   528011    70.7 |  0.200 % |
c |      7635 |  217503   529874 |   79751    7565   530942    70.2 |  0.202 % |
c |      7786 |  217287   529387 |   87726    7667   531687    69.3 |  0.282 % |
c |      8011 |  217287   529387 |   96498    7892   534597    67.7 |  0.282 % |
c |      8349 |  217287   529387 |  106148    8230   558633    67.9 |  0.282 % |
c |      8855 |  217256   529318 |  116763    8735   734792    84.1 |  0.293 % |
c |      9614 |  217256   529318 |  128439    9494   794467    83.7 |  0.293 % |
c |     10753 |  216426   527436 |  141283   10439   860131    82.4 |  0.612 % |
c |     12461 |  216181   526875 |  155412   12140   913607    75.3 |  0.715 % |
c |     15024 |  216124   526744 |  170953   14701  1041685    70.9 |  0.740 % |
c |     18869 |  216010   526487 |  188048   18534  1342904    72.5 |  0.782 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20856 |  213713   521228 |   71237   19816  1339195    67.6 |  0.782 % |
c |     20956 |  213713   521228 |   78360   19916  1342622    67.4 |  1.732 % |
c |     21108 |  213713   521228 |   86196   20068  1344605    67.0 |  1.732 % |
c |     21333 |  213713   521228 |   94816   20293  1353156    66.7 |  1.732 % |
c |     21670 |  213713   521228 |  104298   20630  1358722    65.9 |  1.732 % |
c |     22178 |  213713   521228 |  114727   21138  1403034    66.4 |  1.732 % |
c |     22937 |  213673   521137 |  126200   21895  1470055    67.1 |  1.747 % |
c |     24076 |  213673   521137 |  138820   23034  1600410    69.5 |  1.747 % |
c |     25784 |  213673   521137 |  152702   24742  1747750    70.6 |  1.747 % |
c |     28346 |  213673   521137 |  167973   27304  1920433    70.3 |  1.747 % |
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30738 |  213699   521202 |   71233   29696  2025991    68.2 |  1.747 % |
c |     30840 |  213699   521202 |   78356   29798  2035435    68.3 |  1.748 % |
c |     30990 |  213699   521202 |   86191   29948  2051182    68.5 |  1.748 % |
c |     31218 |  213699   521202 |   94811   30176  2079213    68.9 |  1.748 % |
c |     31555 |  213583   520941 |  104292   30500  2093510    68.6 |  1.793 % |
c |     32061 |  213583   520941 |  114721   31006  2132100    68.8 |  1.793 % |
c |     32820 |  213583   520941 |  126193   31765  2173480    68.4 |  1.793 % |
c |     33959 |  213583   520941 |  138812   32904  2267796    68.9 |  1.793 % |
c |     35672 |  213583   520941 |  152694   34617  2564015    74.1 |  1.793 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37247 |  213556   520851 |   71185   36017  2761623    76.7 |  1.793 % |
c |     37347 |  213556   520851 |   78303   36117  2765369    76.6 |  1.808 % |
c |     37497 |  213556   520851 |   86133   36267  2801192    77.2 |  1.808 % |
c |     37722 |  213481   520683 |   94747   36491  2827873    77.5 |  1.834 % |
c |     38059 |  213481   520683 |  104221   36828  2840362    77.1 |  1.834 % |
c |     38565 |  213273   520214 |  114644   37260  2852397    76.6 |  1.909 % |
c |     39324 |  213273   520214 |  126108   38019  2868551    75.5 |  1.909 % |
c |     40463 |  213273   520214 |  138719   39158  3270128    83.5 |  1.909 % |
c |     42172 |  213273   520214 |  152591   40867  3486729    85.3 |  1.909 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43579 |  213299   520279 |   71099   42274  4125742    97.6 |  1.909 % |
c |     43679 |  213299   520279 |   78208   42374  4128553    97.4 |  1.910 % |
c |     43830 |  213299   520279 |   86029   42525  4184859    98.4 |  1.910 % |
c |     44057 |  213299   520279 |   94632   42752  4219489    98.7 |  1.910 % |
c |     44397 |  213299   520279 |  104096   43092  4223400    98.0 |  1.910 % |
c |     44904 |  213299   520279 |  114505   43599  4236666    97.2 |  1.910 % |
c |     45664 |  213299   520279 |  125956   44359  4309053    97.1 |  1.910 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45801 |  171736   424558 |   57245   41213  4016780    97.5 |  1.910 % |
c |     45901 |  171736   424558 |   62969   41313  4024590    97.4 | 19.487 % |
c |     46056 |  171736   424558 |   69266   41468  4045460    97.6 | 19.487 % |
c |     46285 |  171230   423401 |   76193   41641  4050641    97.3 | 19.692 % |
c |     46622 |  171230   423401 |   83812   41978  4081497    97.2 | 19.692 % |
c |     47128 |  171230   423401 |   92193   42484  4160400    97.9 | 19.692 % |
c |     47887 |  171230   423401 |  101413   43243  4311641    99.7 | 19.692 % |
c |     49026 |  171230   423401 |  111554   44382  4671354   105.3 | 19.692 % |
c |     50734 |  171078   423047 |  122709   46074  4794235   104.1 | 19.763 % |
c |     53296 |  171002   422871 |  134980   48607  5102507   105.0 | 19.796 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55455 |  171025   422929 |   57008   50766  5676296   111.8 | 19.796 % |
c |     55555 |  170999   422869 |   62708   50864  5678671   111.6 | 19.806 % |
c |     55705 |  170545   421830 |   68979   50953  5686655   111.6 | 19.987 % |
c |     55930 |  170467   421654 |   75877   51170  5697154   111.3 | 20.014 % |
c |     56270 |  170467   421654 |   83465   51510  5724131   111.1 | 20.014 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56431 |  170438   421559 |   56812   51173  5688457   111.2 | 20.014 % |
c |     56531 |  170438   421559 |   62493   51273  5696577   111.1 | 20.030 % |
c |     56681 |  170348   421356 |   68742   51421  5735832   111.5 | 20.064 % |
c |     56906 |  170348   421356 |   75616   51646  5758270   111.5 | 20.064 % |
c |     57243 |  170348   421356 |   83178   51983  5860349   112.7 | 20.064 % |
c |     57749 |  170302   421250 |   91496   52483  5923275   112.9 | 20.083 % |
c |     58510 |  170224   421074 |  100645   53241  5969184   112.1 | 20.111 % |
c |     59649 |  170224   421074 |  110710   54380  6145038   113.0 | 20.111 % |
c |     61357 |  170224   421074 |  121781   56088  6611455   117.9 | 20.111 % |
c |     63922 |  170224   421074 |  133959   58653  7382010   125.9 | 20.111 % |
c ==============================================================================
c [1mFound solution: 17[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63954 |  170247   421132 |   56749   58685  7391369   125.9 | 20.111 % |
c |     64054 |  170112   420824 |   62423   58774  7398334   125.9 | 20.163 % |
c |     64204 |  169959   420472 |   68666   58915  7404784   125.7 | 20.227 % |
c |     64430 |  169959   420472 |   75532   59141  7463442   126.2 | 20.227 % |
c |     64767 |  169959   420472 |   83086   59478  7526697   126.5 | 20.227 % |
c |     65273 |  169959   420472 |   91394   59984  7786183   129.8 | 20.227 % |
c |     66036 |  169959   420472 |  100534   60747  8006134   131.8 | 20.227 % |
c |     67175 |  169959   420472 |  110587   61886  8090836   130.7 | 20.227 % |
c |     68885 |  169959   420472 |  121646   63596  8370472   131.6 | 20.227 % |
c |     71449 |  169959   420472 |  133811   66160  9026788   136.4 | 20.227 % |
c |     75297 |  169959   420472 |  147192   70008 10129302   144.7 | 20.227 % |
c |     81065 |  169951   420454 |  161911   75775 10863296   143.4 | 20.230 % |
c |     89715 |  169070   418420 |  178102   84376 12942560   153.4 | 20.611 % |
c ==============================================================================
c [1mFound solution: 16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93011 |  168664   417427 |   56221   86938 13938316   160.3 | 20.611 % |
c |     93111 |  167966   415828 |   61843   22794  3499998   153.5 | 21.082 % |
c |     93263 |  167966   415828 |   68027   22946  3508792   152.9 | 21.082 % |
c |     93488 |  167966   415828 |   74830   23171  3514955   151.7 | 21.082 % |
c |     93825 |  167966   415828 |   82313   23508  3577001   152.2 | 21.082 % |
c |     94332 |  167966   415828 |   90544   24015  3700632   154.1 | 21.082 % |
c |     95091 |  167709   415244 |   99598   24753  3925132   158.6 | 21.178 % |
c |     96231 |  167626   415051 |  109558   25891  4129787   159.5 | 21.216 % |
c |     97939 |  167479   414713 |  120514   27594  4403987   159.6 | 21.278 % |
c |    100501 |  167348   414412 |  132566   30152  4677653   155.1 | 21.327 % |
c |    104346 |  167199   414071 |  145822   33982  5537690   163.0 | 21.384 % |
c |    110112 |  167199   414071 |  160405   39748  8683681   218.5 | 21.384 % |
c |    118761 |  166985   413575 |  176445   48390 11479080   237.2 | 21.474 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 x998 -x999 -x1000 -x1001 -x1002 x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x13#### 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.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (runsolver) R 18847 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481427005 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+9.99947 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 6841 0 0 0 981 17 0 0 25 0 1 0 481427005 32317440 6545 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7890 6545 603 41 0 7849 0
vsize: 31560
[startup+20.0008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 6893 0 0 0 1980 17 0 0 25 0 1 0 481427005 32587776 6597 4294967295 134512640 134672761 3221224576 3221223712 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7956 6597 603 41 0 7915 0
vsize: 31824
[startup+30.0013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 6917 0 0 0 2979 18 0 0 25 0 1 0 481427005 32722944 6621 4294967295 134512640 134672761 3221224576 3221223760 134559559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7989 6621 603 41 0 7948 0
vsize: 31956
[startup+40.0018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 6962 0 0 0 3979 18 0 0 25 0 1 0 481427005 32858112 6666 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8022 6666 603 41 0 7981 0
vsize: 32088
[startup+50.0019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7023 0 0 0 4979 18 0 0 25 0 1 0 481427005 33153024 6727 4294967295 134512640 134672761 3221224576 3221223776 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8094 6727 603 41 0 8053 0
vsize: 32376
[startup+60.0017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7119 0 0 0 5978 19 0 0 25 0 1 0 481427005 33554432 6823 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8192 6823 603 41 0 8151 0
vsize: 32768
[startup+70.0022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7243 0 0 0 6978 19 0 0 25 0 1 0 481427005 34091008 6947 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8323 6947 603 41 0 8282 0
vsize: 33292
[startup+80.0023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7339 0 0 0 7978 19 0 0 25 0 1 0 481427005 34492416 7043 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8421 7043 603 41 0 8380 0
vsize: 33684
[startup+90.0031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7397 0 0 0 8978 19 0 0 25 0 1 0 481427005 34627584 7101 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8454 7101 603 41 0 8413 0
vsize: 33816
[startup+100.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7631 0 0 0 9976 21 0 0 25 0 1 0 481427005 36073472 7335 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8807 7335 603 41 0 8766 0
vsize: 35228
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7762 0 0 0 10976 21 0 0 25 0 1 0 481427005 36614144 7466 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8939 7466 603 41 0 8898 0
vsize: 35756
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7861 0 0 0 11976 21 0 0 25 0 1 0 481427005 37015552 7565 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9037 7565 603 41 0 8996 0
vsize: 36148
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 7940 0 0 0 12976 21 0 0 25 0 1 0 481427005 37416960 7644 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9135 7644 603 41 0 9094 0
vsize: 36540
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8013 0 0 0 13976 22 0 0 25 0 1 0 481427005 37687296 7717 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9201 7717 603 41 0 9160 0
vsize: 36804
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8126 0 0 0 14976 22 0 0 25 0 1 0 481427005 38092800 7830 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9300 7830 603 41 0 9259 0
vsize: 37200
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8305 0 0 0 15975 23 0 0 25 0 1 0 481427005 38998016 8009 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9521 8009 603 41 0 9480 0
vsize: 38084
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8353 0 0 0 16976 23 0 0 25 0 1 0 481427005 39133184 8057 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9554 8057 603 41 0 9513 0
vsize: 38216
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8437 0 0 0 17976 23 0 0 25 0 1 0 481427005 39403520 8141 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9620 8141 603 41 0 9579 0
vsize: 38480
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8502 0 0 0 18976 23 0 0 25 0 1 0 481427005 39669760 8206 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9685 8206 603 41 0 9644 0
vsize: 38740
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8611 0 0 0 19976 23 0 0 25 0 1 0 481427005 39964672 8282 4294967295 134512640 134672761 3221224576 3221223712 134560694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9757 8282 603 41 0 9716 0
vsize: 39028
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8611 0 0 0 20976 23 0 0 25 0 1 0 481427005 39964672 8282 4294967295 134512640 134672761 3221224576 3221223712 134560575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9757 8282 603 41 0 9716 0
vsize: 39028
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8646 0 0 0 21976 24 0 0 25 0 1 0 481427005 40230912 8317 4294967295 134512640 134672761 3221224576 3221223680 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9822 8317 603 41 0 9781 0
vsize: 39288
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8753 0 0 0 22975 24 0 0 25 0 1 0 481427005 40636416 8424 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9921 8424 603 41 0 9880 0
vsize: 39684
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8826 0 0 0 23975 25 0 0 25 0 1 0 481427005 40902656 8497 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9986 8497 603 41 0 9945 0
vsize: 39944
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8891 0 0 0 24975 25 0 0 25 0 1 0 481427005 41168896 8562 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10051 8562 603 41 0 10010 0
vsize: 40204
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8943 0 0 0 25975 25 0 0 25 0 1 0 481427005 41439232 8614 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10117 8614 603 41 0 10076 0
vsize: 40468
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 8985 0 0 0 26975 25 0 0 25 0 1 0 481427005 41570304 8656 4294967295 134512640 134672761 3221224576 3221223712 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10149 8656 603 41 0 10108 0
vsize: 40596
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9013 0 0 0 27975 26 0 0 25 0 1 0 481427005 41705472 8684 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10182 8684 603 41 0 10141 0
vsize: 40728
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9073 0 0 0 28975 26 0 0 25 0 1 0 481427005 41840640 8744 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10215 8744 603 41 0 10174 0
vsize: 40860
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9086 0 0 0 29975 26 0 0 25 0 1 0 481427005 41975808 8757 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10248 8757 603 41 0 10207 0
vsize: 40992
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9113 0 0 0 30975 26 0 0 25 0 1 0 481427005 42110976 8784 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10281 8784 603 41 0 10240 0
vsize: 41124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9136 0 0 0 31975 26 0 0 25 0 1 0 481427005 42110976 8807 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10281 8807 603 41 0 10240 0
vsize: 41124
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9159 0 0 0 32975 27 0 0 25 0 1 0 481427005 42246144 8830 4294967295 134512640 134672761 3221224576 3221223712 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10314 8830 603 41 0 10273 0
vsize: 41256
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9185 0 0 0 33975 27 0 0 25 0 1 0 481427005 42381312 8856 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10347 8856 603 41 0 10306 0
vsize: 41388
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9221 0 0 0 34975 27 0 0 25 0 1 0 481427005 42516480 8892 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10380 8892 603 41 0 10339 0
vsize: 41520
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9343 0 0 0 35974 28 0 0 25 0 1 0 481427005 42762240 8979 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10440 8979 603 41 0 10399 0
vsize: 41760
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9431 0 0 0 36974 28 0 0 25 0 1 0 481427005 43163648 9067 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10538 9067 603 41 0 10497 0
vsize: 42152
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9468 0 0 0 37974 28 0 0 25 0 1 0 481427005 43298816 9104 4294967295 134512640 134672761 3221224576 3221223712 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10571 9104 603 41 0 10530 0
vsize: 42284
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9606 0 0 0 38974 28 0 0 25 0 1 0 481427005 43962368 9242 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 9242 603 41 0 10692 0
vsize: 42932
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 9942 0 0 0 39974 29 0 0 25 0 1 0 481427005 45432832 9578 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11092 9578 603 41 0 11051 0
vsize: 44368
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 10185 0 0 0 40973 29 0 0 25 0 1 0 481427005 46182400 9787 4294967295 134512640 134672761 3221224576 3221223724 1074733103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11275 9787 603 41 0 11234 0
vsize: 45100
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 10226 0 0 0 41973 30 0 0 25 0 1 0 481427005 46448640 9828 4294967295 134512640 134672761 3221224576 3221223776 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11340 9828 603 41 0 11299 0
vsize: 45360
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 10262 0 0 0 42973 30 0 0 25 0 1 0 481427005 46579712 9864 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11372 9864 603 41 0 11331 0
vsize: 45488
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 10704 0 0 0 43972 31 0 0 25 0 1 0 481427005 48332800 10306 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11800 10306 603 41 0 11759 0
vsize: 47200
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 10859 0 0 0 44972 32 0 0 25 0 1 0 481427005 48992256 10461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11961 10461 603 41 0 11920 0
vsize: 47844
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 11113 0 0 0 45972 32 0 0 25 0 1 0 481427005 50065408 10715 4294967295 134512640 134672761 3221224576 3221223680 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12223 10715 603 41 0 12182 0
vsize: 48892
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 11677 0 0 0 46970 33 0 0 25 0 1 0 481427005 52137984 11246 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12729 11246 603 41 0 12688 0
vsize: 50916
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 11704 0 0 0 47971 33 0 0 25 0 1 0 481427005 52273152 11273 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12762 11273 603 41 0 12721 0
vsize: 51048
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 11779 0 0 0 48971 34 0 0 25 0 1 0 481427005 52543488 11348 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12828 11348 603 41 0 12787 0
vsize: 51312
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 11863 0 0 0 49970 34 0 0 25 0 1 0 481427005 52748288 11398 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12878 11398 603 41 0 12837 0
vsize: 51512
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 11882 0 0 0 50970 34 0 0 25 0 1 0 481427005 52883456 11417 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12911 11417 603 41 0 12870 0
vsize: 51644
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 12233 0 0 0 51970 35 0 0 25 0 1 0 481427005 54358016 11768 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13271 11768 603 41 0 13230 0
vsize: 53084
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 12280 0 0 0 52970 35 0 0 25 0 1 0 481427005 54493184 11815 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13304 11815 603 41 0 13263 0
vsize: 53216
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 12359 0 0 0 53970 36 0 0 25 0 1 0 481427005 54894592 11894 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13402 11894 603 41 0 13361 0
vsize: 53608
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 12561 0 0 0 54969 37 0 0 25 0 1 0 481427005 55701504 12096 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13599 12096 603 41 0 13558 0
vsize: 54396
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 12651 0 0 0 55968 37 0 0 25 0 1 0 481427005 55967744 12186 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13664 12186 603 41 0 13623 0
vsize: 54656
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 12720 0 0 0 56968 38 0 0 25 0 1 0 481427005 56373248 12255 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13763 12255 603 41 0 13722 0
vsize: 55052
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 13321 0 0 0 57967 39 0 0 25 0 1 0 481427005 58556416 12822 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14296 12822 603 41 0 14255 0
vsize: 57184
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 13351 0 0 0 58967 39 0 0 25 0 1 0 481427005 58691584 12852 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14329 12852 603 41 0 14288 0
vsize: 57316
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 13565 0 0 0 59967 40 0 0 25 0 1 0 481427005 59539456 13033 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13033 603 41 0 14495 0
vsize: 58144
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 13630 0 0 0 60967 40 0 0 25 0 1 0 481427005 59805696 13098 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14601 13098 603 41 0 14560 0
vsize: 58404
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 13836 0 0 0 61966 41 0 0 25 0 1 0 481427005 60604416 13304 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14796 13304 603 41 0 14755 0
vsize: 59184
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 14495 0 0 0 62965 42 0 0 25 0 1 0 481427005 63275008 13963 4294967295 134512640 134672761 3221224576 3221223680 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15448 13963 603 41 0 15407 0
vsize: 61792
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 15190 0 0 0 63963 44 0 0 25 0 1 0 481427005 65908736 14625 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16091 14625 603 41 0 16050 0
vsize: 64364
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 15239 0 0 0 64963 44 0 0 25 0 1 0 481427005 66170880 14674 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16155 14674 603 41 0 16114 0
vsize: 64620
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 15722 0 0 0 65962 46 0 0 25 0 1 0 481427005 68182016 15157 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16646 15157 603 41 0 16605 0
vsize: 66584
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 15811 0 0 0 66962 46 0 0 25 0 1 0 481427005 68448256 15246 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16711 15246 603 41 0 16670 0
vsize: 66844
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 15845 0 0 0 67962 46 0 0 25 0 1 0 481427005 68583424 15280 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16744 15280 603 41 0 16703 0
vsize: 66976
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 16008 0 0 0 68962 46 0 0 25 0 1 0 481427005 69255168 15443 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16908 15443 603 41 0 16867 0
vsize: 67632
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 16194 0 0 0 69962 47 0 0 25 0 1 0 481427005 70049792 15629 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17102 15629 603 41 0 17061 0
vsize: 68408
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 16534 0 0 0 70961 48 0 0 25 0 1 0 481427005 71438336 15969 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17441 15969 603 41 0 17400 0
vsize: 69764
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 16732 0 0 0 71961 48 0 0 25 0 1 0 481427005 72630272 16167 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17732 16167 603 41 0 17691 0
vsize: 70928
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 16945 0 0 0 72960 49 0 0 25 0 1 0 481427005 73428992 16380 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17927 16380 603 41 0 17886 0
vsize: 71708
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 17218 0 0 0 73959 51 0 0 25 0 1 0 481427005 74498048 16653 4294967295 134512640 134672761 3221224576 3221223744 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18188 16653 603 41 0 18147 0
vsize: 72752
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 17997 0 0 0 74957 53 0 0 25 0 1 0 481427005 77676544 17432 4294967295 134512640 134672761 3221224576 3221223724 1074733099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18964 17432 603 41 0 18923 0
vsize: 75856
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18023 0 0 0 75957 53 0 0 25 0 1 0 481427005 77811712 17458 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18997 17458 603 41 0 18956 0
vsize: 75988
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18071 0 0 0 76957 53 0 0 25 0 1 0 481427005 78077952 17506 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19062 17506 603 41 0 19021 0
vsize: 76248
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18095 0 0 0 77957 53 0 0 25 0 1 0 481427005 78077952 17530 4294967295 134512640 134672761 3221224576 3221223720 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19062 17530 603 41 0 19021 0
vsize: 76248
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18179 0 0 0 78957 53 0 0 25 0 1 0 481427005 78483456 17614 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19161 17614 603 41 0 19120 0
vsize: 76644
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18324 0 0 0 79957 54 0 0 25 0 1 0 481427005 79011840 17759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19290 17759 603 41 0 19249 0
vsize: 77160
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18517 0 0 0 80956 54 0 0 25 0 1 0 481427005 79810560 17952 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19485 17952 603 41 0 19444 0
vsize: 77940
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18701 0 0 0 81956 54 0 0 25 0 1 0 481427005 80605184 18136 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19679 18136 603 41 0 19638 0
vsize: 78716
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 18795 0 0 0 82956 55 0 0 25 0 1 0 481427005 81002496 18230 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19776 18230 603 41 0 19735 0
vsize: 79104
[startup+840.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 19026 0 0 0 83956 55 0 0 25 0 1 0 481427005 81924096 18461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20001 18461 603 41 0 19960 0
vsize: 80004
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 19161 0 0 0 84956 56 0 0 25 0 1 0 481427005 82485248 18596 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20138 18596 603 41 0 20097 0
vsize: 80552
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 19566 0 0 0 85954 57 0 0 25 0 1 0 481427005 84201472 19001 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 19001 603 41 0 20516 0
vsize: 82228
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 19897 0 0 0 86953 58 0 0 25 0 1 0 481427005 85532672 19332 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20882 19332 603 41 0 20841 0
vsize: 83528
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 20134 0 0 0 87953 59 0 0 25 0 1 0 481427005 86466560 19569 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21110 19569 603 41 0 21069 0
vsize: 84440
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 20522 0 0 0 88952 60 0 0 25 0 1 0 481427005 88051712 19957 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21497 19957 603 41 0 21456 0
vsize: 85988
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 20951 0 0 0 89951 61 0 0 25 0 1 0 481427005 89776128 20386 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21918 20386 603 41 0 21877 0
vsize: 87672
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 20984 0 0 0 90951 61 0 0 25 0 1 0 481427005 89911296 20419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21951 20419 603 41 0 21910 0
vsize: 87804
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 21053 0 0 0 91951 61 0 0 25 0 1 0 481427005 90181632 20488 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22017 20488 603 41 0 21976 0
vsize: 88068
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 92949 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223876 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 93949 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 94949 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 95949 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 96949 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 97949 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223680 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 98949 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 99950 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 100950 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223756 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 101950 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223760 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 102950 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 103950 64 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223760 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 104950 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 105950 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 106950 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 107950 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 108951 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 109951 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 110951 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18848
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 111951 65 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1130.06 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 18889
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 112952 67 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1140.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 18901
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 113952 67 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223760 134559503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1150.06 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 18901
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22153 0 0 0 114952 67 0 0 25 0 1 0 481427005 94466048 21554 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23063 21554 603 41 0 23022 0
vsize: 92252
[startup+1160.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18901
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22224 0 0 0 115952 67 0 0 25 0 1 0 481427005 94867456 21625 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23161 21625 603 41 0 23120 0
vsize: 92644
[startup+1170.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18901
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22320 0 0 0 116952 68 0 0 25 0 1 0 481427005 95268864 21721 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23259 21721 603 41 0 23218 0
vsize: 93036
[startup+1180.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18901
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22446 0 0 0 117952 68 0 0 25 0 1 0 481427005 95805440 21847 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23390 21847 603 41 0 23349 0
vsize: 93560
[startup+1190.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18901
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22543 0 0 0 118952 69 0 0 25 0 1 0 481427005 96202752 21944 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23487 21944 603 41 0 23446 0
vsize: 93948
[startup+1200.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18903
Raw data (stat): 18848 (minisat+) R 18847 11931 11930 0 -1 0 22589 0 0 0 119952 69 0 0 25 0 1 0 481427005 96337920 21990 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23520 21990 603 41 0 23479 0
vsize: 94080
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.02 0.99 0.91 1/54 18903
Raw data (stat): 18848 (minisat+) Z 18847 11931 11930 0 -1 12 22592 0 0 0 119952 73 0 0 25 0 1 0 481427005 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.26
CPU user time (s): 1199.53
CPU system time (s): 0.735888
CPU usage (%): 100.012
Max. virtual memory (Kb): 94080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####