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/miplib3/normalized-mps-v2-20-10-mod008.opb
MD5SUM	581d778a36086562107993896110e0a2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	22000
Number of bits of the biggest number in a constraint	15
Biggest sum of numbers in a constraint	1027256
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01784
Number of variables	319
Total number of constraints	325
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	319
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	231
Trace number 21218

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 23:09:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13634 boxname=wulflinc19 idbench=1049 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-mod008.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 13634
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        617856 kB
Buffers:         29844 kB
Cached:         363316 kB
SwapCached:        560 kB
Active:         135456 kB
Inactive:       259780 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        617604 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5168 kB
Slab:            15900 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:29:23 (client local time) WITH STATUS 10 IN 1200.07 SECONDS
stats: 13634 7 1200.07 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> Adder-cost: 2481   maxlim: 21999   bits: 16/15
c ---[   5]---> Adder-cost: 2052   maxlim: 4999   bits: 14/13
c ---[   4]---> Adder-cost: 2306   maxlim: 11999   bits: 15/14
c ---[   2]---> Adder-cost: 1315   maxlim: 1199   bits: 12/11
c ---[   1]---> Adder-cost: 1522   maxlim: 2099   bits: 13/12
c ---[   0]---> Adder-cost: 1797   maxlim: 3999   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   76857   275259 |   25619       0        0     nan |  0.000 % |
c |       100 |   76857   275259 |   28180     100      349     3.5 |  0.295 % |
c |       250 |   76857   275259 |   30998     250      989     4.0 |  0.295 % |
c |       475 |   76857   275259 |   34098     475     2362     5.0 |  0.295 % |
c |       812 |   76857   275259 |   37508     812     5564     6.9 |  0.295 % |
c |      1318 |   76857   275259 |   41259    1318     9284     7.0 |  0.295 % |
c |      2078 |   76857   275259 |   45385    2078    19038     9.2 |  0.295 % |
c ==============================================================================
c [1mFound solution: 1931[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1828   maxlim: 21623   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2678 |   89543   320552 |   29847    2678    24935     9.3 |  0.295 % |
c |      2778 |   89543   320552 |   32831    2778    26152     9.4 |  0.337 % |
c |      2929 |   89543   320552 |   36114    2929    27633     9.4 |  0.337 % |
c |      3154 |   89543   320552 |   39726    3154    29393     9.3 |  0.337 % |
c |      3491 |   89543   320552 |   43698    3491    32994     9.5 |  0.337 % |
c |      3997 |   89543   320552 |   48068    3997    37843     9.5 |  0.337 % |
c |      4756 |   89543   320552 |   52875    4756    49159    10.3 |  0.337 % |
c |      5897 |   89543   320552 |   58163    5897   168561    28.6 |  0.337 % |
c |      7605 |   89510   320441 |   63979    7600   178160    23.4 |  0.382 % |
c |     10168 |   89510   320441 |   70377   10163   226253    22.3 |  0.382 % |
c |     14012 |   89510   320441 |   77415   14007   371624    26.5 |  0.382 % |
c |     19778 |   89510   320441 |   85156   19773   607932    30.7 |  0.382 % |
c |     28428 |   89510   320441 |   93672   28423  1292382    45.5 |  0.382 % |
c |     41403 |   89510   320441 |  103039   41398  2357260    56.9 |  0.382 % |
c ==============================================================================
c [1mFound solution: 1848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21706   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54059 |   89531   320545 |   29843   54054  3961992    73.3 |  0.382 % |
c |     54162 |   89531   320545 |   32827   15292  1592576   104.1 |  0.420 % |
c |     54312 |   89531   320545 |   36110   15442  1593483   103.2 |  0.420 % |
c |     54537 |   89531   320545 |   39721   15667  1596982   101.9 |  0.420 % |
c |     54875 |   89531   320545 |   43693   16005  1602668   100.1 |  0.420 % |
c |     55381 |   89531   320545 |   48062   16511  1613704    97.7 |  0.420 % |
c |     56143 |   89531   320545 |   52868   17273  1650155    95.5 |  0.420 % |
c |     57282 |   89531   320545 |   58155   18412  1696606    92.1 |  0.420 % |
c |     58991 |   89531   320545 |   63971   20121  1829381    90.9 |  0.420 % |
c |     61553 |   89531   320545 |   70368   22683  1980310    87.3 |  0.420 % |
c |     65398 |   89531   320545 |   77405   26528  2168363    81.7 |  0.420 % |
c ==============================================================================
c [1mFound solution: 1769[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21785   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70558 |   89538   320589 |   29846   31688  2707051    85.4 |  0.420 % |
c |     70660 |   89538   320589 |   32830   15536   898016    57.8 |  0.449 % |
c |     70810 |   89538   320589 |   36113   15686   900279    57.4 |  0.449 % |
c |     71035 |   89529   320558 |   39725   15901   904385    56.9 |  0.457 % |
c |     71372 |   89529   320558 |   43697   16238   915276    56.4 |  0.457 % |
c |     71880 |   89529   320558 |   48067   16746   927203    55.4 |  0.457 % |
c |     72639 |   89529   320558 |   52874   17505   959636    54.8 |  0.457 % |
c |     73779 |   89529   320558 |   58161   18645  1023755    54.9 |  0.457 % |
c |     75487 |   89529   320558 |   63977   20353  1113996    54.7 |  0.457 % |
c |     78049 |   89529   320558 |   70375   22915  1190720    52.0 |  0.457 % |
c |     81894 |   89529   320558 |   77412   26760  1574240    58.8 |  0.457 % |
c |     87661 |   89529   320558 |   85154   32527  1806448    55.5 |  0.457 % |
c |     96312 |   89529   320558 |   93669   41178  2513161    61.0 |  0.457 % |
c |    109286 |   89529   320558 |  103036   54152  3635289    67.1 |  0.457 % |
c |    128747 |   89529   320558 |  113340   73613  5739322    78.0 |  0.457 % |
c ==============================================================================
c [1mFound solution: 1739[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21815   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133466 |   89533   320587 |   29844   78332  6147778    78.5 |  0.457 % |
c |    133567 |   89533   320587 |   32828   18672  1409334    75.5 |  0.479 % |
c |    133717 |   89533   320587 |   36111   18822  1410854    75.0 |  0.479 % |
c |    133942 |   89524   320556 |   39722   19041  1414922    74.3 |  0.487 % |
c |    134279 |   89524   320556 |   43694   19378  1422933    73.4 |  0.487 % |
c |    134788 |   89498   320466 |   48064   19875  1449674    72.9 |  0.517 % |
c |    135547 |   89498   320466 |   52870   20634  1490582    72.2 |  0.517 % |
c |    136686 |   89498   320466 |   58157   21773  1505141    69.1 |  0.517 % |
c |    138396 |   89498   320466 |   63973   23483  1570444    66.9 |  0.517 % |
c |    140960 |   89498   320466 |   70370   26047  1682244    64.6 |  0.517 % |
c |    144804 |   89498   320466 |   77407   29891  1991777    66.6 |  0.517 % |
c |    150570 |   89498   320466 |   85148   35657  2263637    63.5 |  0.517 % |
c |    159219 |   89498   320466 |   93663   44306  2944918    66.5 |  0.517 % |
c |    172196 |   89498   320466 |  103029   57283  4042943    70.6 |  0.517 % |
c |    191659 |   89498   320466 |  113332   76746  5737800    74.8 |  0.517 % |
c ==============================================================================
c [1mFound solution: 946[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22608   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    196345 |   89445   320200 |   29815   63587  4160391    65.4 |  0.517 % |
c |    196445 |   89445   320200 |   32796   14131   678279    48.0 |  0.621 % |
c |    196596 |   89445   320200 |   36076   14282   680874    47.7 |  0.621 % |
c |    196821 |   89445   320200 |   39683   14507   688020    47.4 |  0.621 % |
c |    197158 |   89445   320200 |   43652   14844   710964    47.9 |  0.621 % |
c |    197664 |   89445   320200 |   48017   15350   728038    47.4 |  0.621 % |
c |    198423 |   89445   320200 |   52819   16109   791575    49.1 |  0.621 % |
c |    199563 |   89445   320200 |   58101   17249   880814    51.1 |  0.621 % |
c |    201271 |   89445   320200 |   63911   18957  1016739    53.6 |  0.621 % |
c |    203833 |   89445   320200 |   70302   21519  1242229    57.7 |  0.621 % |
c |    207677 |   89445   320200 |   77332   25363  1594865    62.9 |  0.621 % |
c |    213445 |   89445   320200 |   85065   31131  2149941    69.1 |  0.621 % |
c |    222096 |   89445   320200 |   93572   39782  3063330    77.0 |  0.621 % |
c |    235070 |   89445   320200 |  102929   52756  4470065    84.7 |  0.621 % |
c ==============================================================================
c [1mFound solution: 911[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22643   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    251560 |   89450   320229 |   29816   69246  6339367    91.5 |  0.621 % |
c |    251660 |   89450   320229 |   32797   18390  1432400    77.9 |  0.643 % |
c |    251810 |   89450   320229 |   36077   18540  1436537    77.5 |  0.644 % |
c |    252040 |   89450   320229 |   39685   18770  1451042    77.3 |  0.643 % |
c |    252378 |   89450   320229 |   43653   19108  1466905    76.8 |  0.643 % |
c |    252885 |   89450   320229 |   48018   19615  1504665    76.7 |  0.643 % |
c |    253644 |   89450   320229 |   52820   20374  1560056    76.6 |  0.643 % |
c |    254783 |   89450   320229 |   58102   21513  1654788    76.9 |  0.643 % |
c |    256493 |   89450   320229 |   63913   23223  1785510    76.9 |  0.643 % |
c |    259055 |   89450   320229 |   70304   25785  1958197    75.9 |  0.643 % |
c |    262900 |   89450   320229 |   77335   29630  2239296    75.6 |  0.643 % |
c |    268666 |   89450   320229 |   85068   35396  2714258    76.7 |  0.643 % |
c |    277315 |   89450   320229 |   93575   44045  3376127    76.7 |  0.643 % |
c ==============================================================================
c [1mFound solution: 770[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22784   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    279769 |   89453   320247 |   29817   46499  3620727    77.9 |  0.643 % |
c |    279869 |   89427   320157 |   32798   16830  1006352    59.8 |  0.688 % |
c |    280019 |   89427   320157 |   36078   16980  1012513    59.6 |  0.688 % |
c |    280248 |   89427   320157 |   39686   17209  1028073    59.7 |  0.688 % |
c |    280588 |   89427   320157 |   43655   17549  1053941    60.1 |  0.688 % |
c |    281097 |   89341   319859 |   48020   18011  1088494    60.4 |  0.793 % |
c |    281856 |   89341   319859 |   52822   18770  1143730    60.9 |  0.793 % |
c |    282995 |   89341   319859 |   58104   19909  1244248    62.5 |  0.793 % |
c ==============================================================================
c [1mFound solution: 749[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22805   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    284349 |   89348   319898 |   29782   21263  1345616    63.3 |  0.793 % |
c |    284450 |   89348   319898 |   32760   21364  1352753    63.3 |  0.815 % |
c |    284604 |   89348   319898 |   36036   21518  1361183    63.3 |  0.815 % |
c |    284829 |   89348   319898 |   39639   21743  1377474    63.4 |  0.815 % |
c |    285166 |   89348   319898 |   43603   22080  1390687    63.0 |  0.815 % |
c |    285672 |   89348   319898 |   47964   22586  1414527    62.6 |  0.815 % |
c ==============================================================================
c [1mFound solution: 741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22813   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    286300 |   89352   319930 |   29784   23214  1454021    62.6 |  0.815 % |
c |    286400 |   89352   319930 |   32762   23314  1458066    62.5 |  0.837 % |
c |    286551 |   89352   319930 |   36038   23465  1467784    62.6 |  0.837 % |
c |    286776 |   89352   319930 |   39642   23690  1481349    62.5 |  0.837 % |
c |    287116 |   89352   319930 |   43606   24030  1500314    62.4 |  0.837 % |
c |    287622 |   89352   319930 |   47967   24536  1529161    62.3 |  0.837 % |
c |    288382 |   89352   319930 |   52764   25296  1584096    62.6 |  0.837 % |
c |    289521 |   89352   319930 |   58040   26435  1669747    63.2 |  0.837 % |
c |    291229 |   89352   319930 |   63844   28143  1799237    63.9 |  0.837 % |
c |    293792 |   89352   319930 |   70229   30706  1972225    64.2 |  0.837 % |
c |    297636 |   89352   319930 |   77252   34550  2247972    65.1 |  0.837 % |
c |    303402 |   89352   319930 |   84977   40316  2660851    66.0 |  0.837 % |
c |    312052 |   89352   319930 |   93474   48966  3274473    66.9 |  0.837 % |
c |    325028 |   89352   319930 |  102822   61942  4241149    68.5 |  0.837 % |
c ==============================================================================
c [1mFound solution: 689[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22865   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    328455 |   89356   319957 |   29785   65369  4571282    69.9 |  0.837 % |
c |    328557 |   89356   319957 |   32763   18757  1074267    57.3 |  0.859 % |
c |    328708 |   89356   319957 |   36039   18908  1086451    57.5 |  0.859 % |
c |    328935 |   89356   319957 |   39643   19135  1100616    57.5 |  0.859 % |
c |    329272 |   89356   319957 |   43608   19472  1127436    57.9 |  0.859 % |
c |    329782 |   89356   319957 |   47969   19982  1166638    58.4 |  0.859 % |
c |    330542 |   89356   319957 |   52765   20742  1214476    58.6 |  0.859 % |
c |    331681 |   89356   319957 |   58042   21881  1299360    59.4 |  0.859 % |
c |    333390 |   89356   319957 |   63846   23590  1448384    61.4 |  0.859 % |
c |    335955 |   89356   319957 |   70231   26155  1643941    62.9 |  0.859 % |
c ==============================================================================
c [1mFound solution: 681[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22873   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    338761 |   89360   319980 |   29786   28961  1945896    67.2 |  0.859 % |
c |    338862 |   89360   319980 |   32764   29062  1947465    67.0 |  0.874 % |
c |    339012 |   89360   319980 |   36041   29212  1953623    66.9 |  0.874 % |
c |    339237 |   89360   319980 |   39645   29437  1975036    67.1 |  0.874 % |
c |    339574 |   89360   319980 |   43609   29774  1988516    66.8 |  0.874 % |
c |    340080 |   89360   319980 |   47970   30280  2027818    67.0 |  0.874 % |
c |    340839 |   89360   319980 |   52767   31039  2085626    67.2 |  0.874 % |
c ==============================================================================
c [1mFound solution: 657[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22897   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    341314 |   89366   320012 |   29788   31514  2129230    67.6 |  0.874 % |
c |    341414 |   89366   320012 |   32766   15857   930079    58.7 |  0.896 % |
c |    341564 |   89366   320012 |   36043   16007   946090    59.1 |  0.896 % |
c |    341789 |   89366   320012 |   39647   16232   967115    59.6 |  0.896 % |
c |    342127 |   89366   320012 |   43612   16570   997471    60.2 |  0.896 % |
c |    342633 |   89366   320012 |   47973   17076  1035864    60.7 |  0.896 % |
c |    343394 |   89366   320012 |   52771   17837  1106067    62.0 |  0.896 % |
c ==============================================================================
c [1mFound solution: 636[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22918   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    343979 |   89371   320052 |   29790   18422  1157747    62.8 |  0.896 % |
c |    344081 |   89371   320052 |   32769   18524  1160795    62.7 |  0.926 % |
c |    344231 |   89371   320052 |   36045   18674  1169790    62.6 |  0.926 % |
c |    344459 |   89371   320052 |   39650   18902  1185454    62.7 |  0.926 % |
c |    344797 |   89371   320052 |   43615   19240  1215432    63.2 |  0.926 % |
c |    345303 |   89371   320052 |   47977   19746  1248021    63.2 |  0.926 % |
c |    346062 |   89371   320052 |   52774   20505  1318239    64.3 |  0.926 % |
c ==============================================================================
c [1mFound solution: 635[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22919   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    347023 |   89373   320063 |   29791   21466  1395363    65.0 |  0.926 % |
c |    347123 |   89373   320063 |   32770   21566  1399600    64.9 |  0.933 % |
c |    347275 |   89373   320063 |   36047   21718  1410545    64.9 |  0.933 % |
c |    347501 |   89373   320063 |   39651   21944  1431487    65.2 |  0.933 % |
c |    347839 |   89373   320063 |   43617   22282  1446347    64.9 |  0.933 % |
c |    348347 |   89373   320063 |   47978   22790  1487027    65.2 |  0.933 % |
c |    349106 |   89373   320063 |   52776   23549  1551551    65.9 |  0.933 % |
c ==============================================================================
c [1mFound solution: 563[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22991   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    349336 |   89376   320079 |   29792   23779  1570821    66.1 |  0.933 % |
c |    349436 |   89376   320079 |   32771   23879  1572338    65.8 |  0.948 % |
c |    349587 |   89376   320079 |   36048   24030  1584564    65.9 |  0.948 % |
c |    349812 |   89376   320079 |   39653   24255  1595306    65.8 |  0.948 % |
c ==============================================================================
c [1mFound solution: 546[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23008   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    349973 |   89330   319927 |   29776   24379  1607855    66.0 |  0.948 % |
c |    350076 |   89330   319927 |   32753   24482  1613253    65.9 |  1.022 % |
c |    350227 |   89330   319927 |   36028   24633  1624363    65.9 |  1.022 % |
c |    350454 |   89330   319927 |   39631   24860  1638779    65.9 |  1.022 % |
c |    350791 |   89330   319927 |   43595   25197  1660811    65.9 |  1.022 % |
c |    351297 |   89330   319927 |   47954   25703  1706767    66.4 |  1.022 % |
c |    352058 |   89330   319927 |   52750   26464  1768930    66.8 |  1.022 % |
c ==============================================================================
c [1mFound solution: 520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23034   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    352787 |   89338   319969 |   29779   27193  1832145    67.4 |  1.022 % |
c |    352887 |   89338   319969 |   32756   27293  1835973    67.3 |  1.051 % |
c |    353037 |   89338   319969 |   36032   27443  1851592    67.5 |  1.051 % |
c |    353263 |   89338   319969 |   39635   27669  1862417    67.3 |  1.051 % |
c |    353600 |   89338   319969 |   43599   28006  1873654    66.9 |  1.051 % |
c |    354106 |   89338   319969 |   47959   28512  1912744    67.1 |  1.051 % |
c |    354865 |   89338   319969 |   52755   29271  1963916    67.1 |  1.051 % |
c |    356004 |   89338   319969 |   58030   30410  2080531    68.4 |  1.051 % |
c |    357712 |   89338   319969 |   63833   32118  2225201    69.3 |  1.051 % |
c |    360276 |   89338   319969 |   70217   34682  2431286    70.1 |  1.051 % |
c |    364123 |   89338   319969 |   77239   38529  2599173    67.5 |  1.051 % |
c ==============================================================================
c [1mFound solution: 480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23074   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    364642 |   89281   319630 |   29760   33995  2124305    62.5 |  1.051 % |
c |    364744 |   89281   319630 |   32736   17100   816807    47.8 |  1.148 % |
c ==============================================================================
c [1mFound solution: 420[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23134   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    364775 |   89293   319683 |   29764   17131   820083    47.9 |  1.148 % |
c |    364875 |   89293   319683 |   32740   17231   823221    47.8 |  1.191 % |
c |    365025 |   89293   319683 |   36014   17381   839441    48.3 |  1.191 % |
c |    365251 |   89293   319683 |   39615   17607   854651    48.5 |  1.191 % |
c |    365588 |   89293   319683 |   43577   17944   879981    49.0 |  1.191 % |
c |    366097 |   89293   319683 |   47935   18453   907479    49.2 |  1.191 % |
c |    366856 |   89293   319683 |   52728   19212   939227    48.9 |  1.191 % |
c |    367995 |   89293   319683 |   58001   20351   990808    48.7 |  1.191 % |
c |    369705 |   89293   319683 |   63801   22061  1077728    48.9 |  1.191 % |
c ==============================================================================
c [1mFound solution: 416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23138   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    371892 |   89299   319710 |   29766   24248  1354947    55.9 |  1.191 % |
c |    371992 |   89299   319710 |   32742   24348  1356814    55.7 |  1.213 % |
c |    372146 |   89299   319710 |   36016   24502  1373796    56.1 |  1.213 % |
c |    372373 |   89299   319710 |   39618   24729  1377921    55.7 |  1.213 % |
c |    372710 |   89299   319710 |   43580   25066  1380528    55.1 |  1.213 % |
c |    373221 |   89299   319710 |   47938   25577  1432054    56.0 |  1.213 % |
c |    373980 |   89299   319710 |   52732   26336  1501098    57.0 |  1.213 % |
c |    375119 |   89299   319710 |   58005   27475  1638401    59.6 |  1.213 % |
c ==============================================================================
c [1mFound solution: 413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23141   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    375458 |   89303   319730 |   29767   27814  1668063    60.0 |  1.213 % |
c |    375561 |   89303   319730 |   32743   27917  1672575    59.9 |  1.228 % |
c |    375713 |   89303   319730 |   36018   28069  1677890    59.8 |  1.228 % |
c |    375938 |   89303   319730 |   39619   28294  1700111    60.1 |  1.228 % |
c |    376275 |   89303   319730 |   43581   28631  1721049    60.1 |  1.228 % |
c |    376783 |   89303   319730 |   47940   29139  1748205    60.0 |  1.228 % |
c |    377542 |   89303   319730 |   52734   29898  1852194    62.0 |  1.228 % |
c |    378681 |   89303   319730 |   58007   31037  1926161    62.1 |  1.228 % |
c ==============================================================================
c [1mFound solution: 391[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23163   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    379305 |   89309   319753 |   29769   31661  1997107    63.1 |  1.228 % |
c |    379405 |   89309   319753 |   32745   15931   987289    62.0 |  1.249 % |
c |    379555 |   89309   319753 |   36020   16081  1004207    62.4 |  1.249 % |
c |    379780 |   89309   319753 |   39622   16306  1021903    62.7 |  1.249 % |
c |    380118 |   89309   319753 |   43584   16644  1068892    64.2 |  1.249 % |
c |    380624 |   89309   319753 |   47943   17150  1124282    65.6 |  1.249 % |
c |    381384 |   89309   319753 |   52737   17910  1177065    65.7 |  1.249 % |
c |    382527 |   89309   319753 |   58011   19053  1260747    66.2 |  1.249 % |
c ==============================================================================
c [1mFound solution: 383[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23171   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    382559 |   89312   319765 |   29770   19085  1263820    66.2 |  1.249 % |
c |    382660 |   89312   319765 |   32747   19186  1279973    66.7 |  1.264 % |
c |    382811 |   89312   319765 |   36021   19337  1281662    66.3 |  1.264 % |
c |    383036 |   89312   319765 |   39623   19562  1283347    65.6 |  1.264 % |
c |    383373 |   89312   319765 |   43586   19899  1286470    64.6 |  1.264 % |
c |    383879 |   89303   319734 |   47944   20374  1292598    63.4 |  1.271 % |
c |    384638 |   89303   319734 |   52739   21133  1426918    67.5 |  1.271 % |
c |    385777 |   89303   319734 |   58013   22272  1442431    64.8 |  1.271 % |
c |    387487 |   89303   319734 |   63814   23982  1652277    68.9 |  1.271 % |
c |    390053 |   89303   319734 |   70196   26548  1847144    69.6 |  1.271 % |
c |    393901 |   89303   319734 |   77215   30396  2175956    71.6 |  1.271 % |
c ==============================================================================
c [1mFound solution: 379[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23175   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    396154 |   89305   319742 |   29768   32649  2348259    71.9 |  1.271 % |
c |    396255 |   89305   319742 |   32744   16426   957663    58.3 |  1.279 % |
c |    396406 |   89305   319742 |   36019   16577   968527    58.4 |  1.279 % |
c |    396631 |   89305   319742 |   39621   16802   981575    58.4 |  1.279 % |
c |    396968 |   89305   319742 |   43583   17139  1003150    58.5 |  1.279 % |
c |    397475 |   89305   319742 |   47941   17646  1038658    58.9 |  1.279 % |
c ==============================================================================
c [1mFound solution: 377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23177   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    398085 |   89307   319752 |   29769   18256  1129253    61.9 |  1.279 % |
c |    398186 |   89307   319752 |   32745   18357  1130922    61.6 |  1.286 % |
c |    398339 |   89307   319752 |   36020   18510  1154631    62.4 |  1.286 % |
c |    398566 |   89307   319752 |   39622   18737  1170433    62.5 |  1.286 % |
c |    398905 |   89307   319752 |   43584   19076  1225864    64.3 |  1.286 % |
c |    399412 |   89307   319752 |   47943   19583  1307495    66.8 |  1.286 % |
c |    400171 |   89307   319752 |   52737   20342  1394079    68.5 |  1.286 % |
c ==============================================================================
c [1mFound solution: 375[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23179   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    400829 |   89308   319760 |   29769   21000  1479193    70.4 |  1.286 % |
c |    400929 |   89308   319760 |   32745   21100  1491899    70.7 |  1.293 % |
c |    401080 |   89308   319760 |   36020   21251  1511648    71.1 |  1.293 % |
c |    401305 |   89308   319760 |   39622   21476  1514293    70.5 |  1.293 % |
c |    401643 |   89222   319462 |   43584   21776  1525877    70.1 |  1.397 % |
c |    402150 |   89222   319462 |   47943   22283  1553678    69.7 |  1.397 % |
c |    402913 |   89222   319462 |   52737   23046  1660939    72.1 |  1.397 % |
c |    404052 |   89222   319462 |   58011   24185  1951488    80.7 |  1.397 % |
c |    405760 |   89222   319462 |   63812   25893  2007780    77.5 |  1.397 % |
c |    408322 |   89222   319462 |   70193   28455  2637423    92.7 |  1.397 % |
c |    412166 |   89222   319462 |   77213   32299  2783887    86.2 |  1.397 % |
c |    417938 |   89222   319462 |   84934   38071  3926319   103.1 |  1.397 % |
c ==============================================================================
c [1mFound solution: 371[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23183   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    426578 |   89224   319470 |   29741   46711  6220556   133.2 |  1.397 % |
c |    426678 |   89224   319470 |   32715   16779  3072475   183.1 |  1.404 % |
c |    426828 |   89224   319470 |   35986   16929  3075611   181.7 |  1.404 % |
c |    427055 |   89224   319470 |   39585   17156  3079240   179.5 |  1.404 % |
c |    427392 |   89224   319470 |   43543   17493  3088913   176.6 |  1.404 % |
c |    427898 |   89224   319470 |   47898   17999  3093916   171.9 |  1.404 % |
c |    428657 |   89224   319470 |   52687   18758  3106406   165.6 |  1.404 % |
c |    429797 |   89189   319349 |   57956   19885  3128940   157.4 |  1.442 % |
c |    431505 |   89189   319349 |   63752   21593  3412504   158.0 |  1.442 % |
c |    434069 |   89175   319301 |   70127   24154  3816541   158.0 |  1.464 % |
c |    437914 |   89098   319034 |   77140   27975  4441778   158.8 |  1.561 % |
c |    443684 |   89040   318834 |   84854   33726  5149734   152.7 |  1.627 % |
c |    452334 |   88999   318693 |   93339   42368  6815244   160.9 |  1.672 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 -C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 -C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 -C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 -C86_0x2e__bit0 -C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 -C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 -C112_0x2e__bit0 -C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 C118_0x2e__bit0 -C119_0x2e__bit0 -C120_0x2e__bit0 -C121_0x2e__bit0 -C122_0x2e__bit0 -C123_0x2e__bit0 C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 -C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 -C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172_0x2e__bit0 -C173_0x2e__bit0 -C174_0x2e__bit0 -C175_0x2e__bit0 -C176_0x2e__bit0 -C177_0x2e__bit0 -C178_0x2e__bit0 -C179_0x2e__bit0 -C180_0x2e__bit0 -C181_0x2e__bit0 -C182_0x2e__bit0 -C183_0x2e__bit0 -C184_0x2e__bit0 -C185_0x2e__bit0 -C186_0x2e__bit0 -C187_0x2e__bit0 -C188_0x2e__bit0 -C189_0x2e__bit0 -C190_0x2e__bit0 -C191_0x2e__bit0 -C192_0x2e__bit0 -C193_0x2e__bit0 -C194_0x2e__bit0 -C195_0x2e__bit0 -C196_0x2e__bit0 -C197_0x2e__bit0 -C198_0x2e__bit0 -C199_0x2e__bit0 -C200_0x2e__bit0 -C201_0x2e__bit0 -C202_0x2e__bit0 -C203_0x2e__bit0 -C204_0x2e__bit0 -C205_0x2e__bit0 -C206_0x2e__bit0 -C207_0x2e__bit0 -C208_0x2e__bit0 -C209_0x2e__bit0 -C210_0x2e__bit0 -C211_0x2e__bit0 -C212_0x2e__bit0 -C213_0x2e__bit0 -C214_0x2e__bit0 -C215_0x2e__bit0 -C216_0x2e__bit0 -C217_0x2e__bit0 -C218_0x2e__bit0 -C219_0x2e__bit0 -C220_0x2e__bit0 -C221_0x2e__bit0 -C222_0x2e__bit0 -C223_0x2e__bit0 -C224_0x2e__bit0 -C225_0x2e__bit0 -C226_0x2e__bit0 -C227_0x2e__bit0 -C228_0x2e__bit0 -C229_0x2e__bit0 -C230_0x2e__bit0 -C231_0x2e__bit0 -C232_0x2e__bit0 -C233_0x2e__bit0 -C234_0x2e__bit0 -C235_0x2e__bit0 -C236_0x2e__bit0 -C237_0x2e__bit0 -C238_0x2e__bit0 -C239_0x2e__bit0 -C240_0x2e__bit0 -C241_0x2e__bit0 -C242_0x2e__bit0 -C243_0x2e__bit0 -C244_0x2e__bit0 -C245_0x2e__bit0 -C246_0x2e__bit0 -C2#### 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.84 0.94 0.90 2/55 10424
Raw data (stat): 10424 (runsolver) R 10423 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548921872 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 10424
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 2393 0 0 0 993 5 0 0 25 0 1 0 548921872 11661312 2364 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2847 2364 603 41 0 2806 0
vsize: 11388
[startup+20.002 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 10424
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 3172 0 0 0 1991 8 0 0 25 0 1 0 548921872 14888960 3143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3635 3143 603 41 0 3594 0
vsize: 14540
[startup+30.0028 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 3878 0 0 0 2989 10 0 0 25 0 1 0 548921872 17842176 3849 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4356 3849 603 41 0 4315 0
vsize: 17424
[startup+40.0036 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 4452 0 0 0 3988 11 0 0 25 0 1 0 548921872 20127744 4423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4914 4423 603 41 0 4873 0
vsize: 19656
[startup+50.0045 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 5063 0 0 0 4985 14 0 0 25 0 1 0 548921872 22675456 5034 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5536 5034 603 41 0 5495 0
vsize: 22144
[startup+60.0049 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 5710 0 0 0 5983 16 0 0 25 0 1 0 548921872 25219072 5681 4294967295 134512640 134672761 3221224544 3221223728 134559383 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5681 603 41 0 6116 0
vsize: 24628
[startup+70.0051 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6311 0 0 0 6981 18 0 0 25 0 1 0 548921872 27774976 6282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6781 6282 603 41 0 6740 0
vsize: 27124
[startup+80.0059 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6338 0 0 0 7980 19 0 0 25 0 1 0 548921872 27930624 6309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6309 603 41 0 6778 0
vsize: 27276
[startup+90.0063 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6338 0 0 0 8980 20 0 0 25 0 1 0 548921872 27930624 6309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6309 603 41 0 6778 0
vsize: 27276
[startup+100.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 9980 20 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 10979 20 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+120.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 11979 21 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223760 134557633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+130.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 12979 21 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 13979 22 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+150.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6341 0 0 0 14979 22 0 0 25 0 1 0 548921872 27930624 6312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6312 603 41 0 6778 0
vsize: 27276
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6757 0 0 0 15977 23 0 0 25 0 1 0 548921872 29528064 6728 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6728 603 41 0 7168 0
vsize: 28836
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 7073 0 0 0 16976 25 0 0 25 0 1 0 548921872 30851072 7044 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7532 7044 603 41 0 7491 0
vsize: 30128
[startup+180.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 7443 0 0 0 17974 27 0 0 25 0 1 0 548921872 32583680 7414 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7955 7414 603 41 0 7914 0
vsize: 31820
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 7846 0 0 0 18973 28 0 0 25 0 1 0 548921872 34185216 7817 4294967295 134512640 134672761 3221224544 3221223792 134562614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8346 7817 603 41 0 8305 0
vsize: 33384
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8216 0 0 0 19972 29 0 0 25 0 1 0 548921872 35778560 8187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8735 8187 603 41 0 8694 0
vsize: 34940
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8589 0 0 0 20971 30 0 0 25 0 1 0 548921872 37249024 8560 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9094 8560 603 41 0 9053 0
vsize: 36376
[startup+220.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 21970 31 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+230.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 22970 32 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+240.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 23969 32 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+250.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 24969 32 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 25969 33 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 26969 33 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 27968 34 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 28968 34 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 29968 35 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 30967 35 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10426
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 31967 35 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 32967 36 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8986 0 0 0 33966 37 0 0 25 0 1 0 548921872 38862848 8957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9488 8957 603 41 0 9447 0
vsize: 37952
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9257 0 0 0 34965 38 0 0 25 0 1 0 548921872 39936000 9228 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9750 9228 603 41 0 9709 0
vsize: 39000
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 35965 39 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 36964 39 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223696 134564785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 37964 40 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 38964 40 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 39964 40 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 40953 41 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 41952 41 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 42952 42 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 43951 43 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 44951 43 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 45951 43 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 46950 44 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 47950 44 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9481 0 0 0 48949 46 0 0 25 0 1 0 548921872 40878080 9452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9980 9452 603 41 0 9939 0
vsize: 39920
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9587 0 0 0 49948 47 0 0 25 0 1 0 548921872 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9558 603 41 0 10038 0
vsize: 40316
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9587 0 0 0 50947 48 0 0 25 0 1 0 548921872 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9558 603 41 0 10038 0
vsize: 40316
[startup+520.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 51946 48 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 52946 49 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 53946 49 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 54945 50 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 55945 50 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+570.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 56945 50 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 57944 51 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 58944 51 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 59944 52 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+610.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 60943 52 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+620.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10428
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 61943 53 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 62943 53 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 63942 54 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 64942 54 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 65942 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 66942 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 67941 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 68941 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 69941 56 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+710.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 70941 56 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 71940 57 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 72940 57 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 73940 58 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+750.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 74939 58 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+760.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 75939 58 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+770.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 76939 59 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 77938 60 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 78938 60 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 79938 60 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 80938 61 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 81938 61 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+830.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 82937 62 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+840.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 83937 62 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 84937 62 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 85936 63 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 86936 63 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+880.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 87936 64 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 88935 64 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 89935 65 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 90935 65 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10430
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 91934 66 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+930.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 92934 66 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+940.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 93934 67 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 94933 67 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+960.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 95933 68 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 96932 68 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 97932 69 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 98931 70 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 99930 70 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 100930 71 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 101930 71 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 102930 72 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 103929 72 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 104929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 105929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 106929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 107929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 108928 74 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 109928 75 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10006 0 0 0 110927 75 0 0 25 0 1 0 548921872 43003904 9977 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10499 9977 603 41 0 10458 0
vsize: 41996
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10247 0 0 0 111927 76 0 0 25 0 1 0 548921872 44064768 10218 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 10218 603 41 0 10717 0
vsize: 43032
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10581 0 0 0 112926 77 0 0 25 0 1 0 548921872 45363200 10552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11075 10552 603 41 0 11034 0
vsize: 44300
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10834 0 0 0 113925 78 0 0 25 0 1 0 548921872 46424064 10805 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 10805 603 41 0 11293 0
vsize: 45336
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 11204 0 0 0 114923 80 0 0 25 0 1 0 548921872 47882240 11175 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11690 11175 603 41 0 11649 0
vsize: 46760
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 11585 0 0 0 115922 81 0 0 25 0 1 0 548921872 49451008 11556 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12073 11556 603 41 0 12032 0
vsize: 48292
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 11929 0 0 0 116921 83 0 0 25 0 1 0 548921872 50913280 11900 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12430 11900 603 41 0 12389 0
vsize: 49720
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 12189 0 0 0 117920 84 0 0 25 0 1 0 548921872 51978240 12160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12690 12160 603 41 0 12649 0
vsize: 50760
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 12465 0 0 0 118919 85 0 0 25 0 1 0 548921872 53166080 12436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12980 12436 603 41 0 12939 0
vsize: 51920
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10432
Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 12795 0 0 0 119918 86 0 0 25 0 1 0 548921872 54460416 12766 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12766 603 41 0 13255 0
vsize: 53184
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 10432
Raw data (stat): 10424 (minisat+) Z 10423 22929 22928 0 -1 12 12798 0 0 0 119918 88 0 0 25 0 1 0 548921872 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.09
CPU time (s): 1200.07
CPU user time (s): 1199.18
CPU system time (s): 0.889864
CPU usage (%): 99.9987
Max. virtual memory (Kb): 53184
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####