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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-5.opb
MD5SUM	38d41fdbe49543e8928c5210e4323f00
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
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	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	760
Total number of constraints	41619
Number of constraints which are clauses	41619
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	2
Trace number 5035

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 21:33:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2948 boxname=wulflinc31 idbench=328 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  38d41fdbe49543e8928c5210e4323f00  /oldhome/oroussel/tmp/wulflinc31/normalized-frb40-19-5.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-frb40-19-5.opb
IDLAUNCH: 2948
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        909912 kB
Buffers:         34612 kB
Cached:          51356 kB
SwapCached:        392 kB
Active:          47188 kB
Inactive:        41968 kB
HighTotal:      131008 kB
HighFree:        75908 kB
LowTotal:       903652 kB
LowFree:        834004 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            30052 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:53:06 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 2948 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41619 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 |   41619    83238 |   13873       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77738   168085 |   25912       0        0     nan |  0.000 % |
c |       100 |   77393   167370 |   28503      74      614     8.3 |  0.753 % |
c |       250 |   76571   165604 |   31353     182     1860    10.2 |  2.662 % |
c |       475 |   75416   163089 |   34488     361     3656    10.1 |  5.412 % |
c |       812 |   73469   158808 |   37937     588     7576    12.9 | 10.134 % |
c |      1318 |   71470   154363 |   41731     995    12456    12.5 | 15.052 % |
c |      2077 |   68055   146635 |   45904    1571    21571    13.7 | 23.713 % |
c ==============================================================================
c [1mFound solution: -30[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 |      2368 |   66345   142775 |   22115    1722    23486    13.6 | 23.713 % |
c |      2468 |   65954   141886 |   24326    1798    24101    13.4 | 29.188 % |
c |      2618 |   65428   140687 |   26759    1916    26017    13.6 | 30.521 % |
c |      2843 |   64784   139204 |   29435    2104    29300    13.9 | 32.202 % |
c |      3180 |   63783   136936 |   32378    2343    33178    14.2 | 34.720 % |
c |      3686 |   62671   134380 |   35616    2764    38470    13.9 | 37.600 % |
c |      4445 |   60688   129777 |   39178    3385    46444    13.7 | 42.715 % |
c ==============================================================================
c [1mFound solution: -31[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 |      4942 |   59952   128172 |   19984    3811    62121    16.3 | 42.715 % |
c |      5042 |   59679   127517 |   21982    3894    63964    16.4 | 45.623 % |
c |      5192 |   59303   126633 |   24180    4014    65656    16.4 | 46.620 % |
c |      5417 |   58170   123919 |   26598    4092    67984    16.6 | 49.720 % |
c |      5755 |   57394   122041 |   29258    4355    72331    16.6 | 51.880 % |
c |      6261 |   56683   120374 |   32184    4714    77744    16.5 | 53.783 % |
c |      7020 |   54571   115370 |   35402    5132    87529    17.1 | 59.526 % |
c |      8159 |   53100   111874 |   38943    6005   106837    17.8 | 63.555 % |
c |      9867 |   51361   107721 |   42837    7233   142892    19.8 | 68.277 % |
c ==============================================================================
c [1mFound solution: -32[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 |     11787 |   49479   103125 |   16493    8440   181552    21.5 | 68.277 % |
c |     11887 |   49297   102693 |   18142    8475   182904    21.6 | 74.014 % |
c |     12037 |   49131   102301 |   19956    8543   185298    21.7 | 74.456 % |
c |     12262 |   49025   102033 |   21952    8701   189426    21.8 | 74.770 % |
c |     12602 |   48860   101631 |   24147    8952   197477    22.1 | 75.240 % |
c |     13108 |   48811   101518 |   26562    9438   225449    23.9 | 75.369 % |
c ==============================================================================
c [1mFound solution: -33[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 |     13835 |   48637   101137 |   16212   10042   261315    26.0 | 75.369 % |
c |     13935 |   48570   100975 |   17833   10127   264156    26.1 | 76.055 % |
c |     14085 |   48570   100975 |   19616   10277   269303    26.2 | 76.055 % |
c |     14312 |   48535   100890 |   21578   10475   276829    26.4 | 76.156 % |
c |     14649 |   48224   100143 |   23735   10596   283579    26.8 | 77.024 % |
c |     15155 |   47936    99449 |   26109   10862   295418    27.2 | 77.815 % |
c |     15915 |   47936    99449 |   28720   11622   352382    30.3 | 77.815 % |
c ==============================================================================
c [1mFound solution: -34[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 |     16092 |   47809    99110 |   15936   11694   348286    29.8 | 77.815 % |
c |     16193 |   47809    99110 |   17529   11795   351047    29.8 | 78.162 % |
c |     16343 |   47809    99110 |   19282   11945   358187    30.0 | 78.162 % |
c |     16568 |   47699    98850 |   21210   12069   366809    30.4 | 78.463 % |
c |     16907 |   47699    98850 |   23331   12408   381170    30.7 | 78.463 % |
c |     17413 |   47691    98830 |   25665   12893   410134    31.8 | 78.487 % |
c |     18172 |   47570    98547 |   28231   13507   456879    33.8 | 78.813 % |
c |     19312 |   47514    98418 |   31054   14523   514679    35.4 | 78.957 % |
c |     21020 |   47429    98213 |   34160   16152   617687    38.2 | 79.194 % |
c |     23582 |   47246    97781 |   37576   18577   833388    44.9 | 79.692 % |
c |     27427 |   47199    97655 |   41333   22352  1265776    56.6 | 79.845 % |
c |     33193 |   47092    97395 |   45467   28078  1866446    66.5 | 80.150 % |
c |     41842 |   46935    97003 |   50013   36506  2578978    70.6 | 80.608 % |
c |     54816 |   46775    96601 |   55015   49208  3834743    77.9 | 81.078 % |
c ==============================================================================
c [1mFound solution: -35[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 |     66599 |   46701    96441 |   15567   60446  4917752    81.4 | 81.078 % |
c |     66699 |   46701    96441 |   17123   18649  1166349    62.5 | 81.358 % |
c |     66849 |   46701    96441 |   18836   18799  1175990    62.6 | 81.358 % |
c |     67075 |   46701    96441 |   20719   19025  1183368    62.2 | 81.358 % |
c |     67412 |   46698    96434 |   22791   19361  1203497    62.2 | 81.366 % |
c |     67920 |   46667    96361 |   25070   19848  1238599    62.4 | 81.450 % |
c |     68680 |   46645    96307 |   27577   20600  1270078    61.7 | 81.514 % |
c |     69819 |   46584    96158 |   30335   21676  1347252    62.2 | 81.690 % |
c |     71527 |   46518    95998 |   33369   23343  1512076    64.8 | 81.874 % |
c |     74089 |   46518    95998 |   36706   25905  1789120    69.1 | 81.874 % |
c |     77933 |   46488    95928 |   40376   29711  2161793    72.8 | 81.954 % |
c |     83701 |   46272    95398 |   44414   35390  2699227    76.3 | 82.566 % |
c |     92350 |   46247    95337 |   48855   43978  3619619    82.3 | 82.639 % |
c |    105326 |   46247    95337 |   53741   56954  5420125    95.2 | 82.638 % |
c ==============================================================================
c [1mFound solution: -36[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 |    109573 |   46236    95289 |   15412   61020  6058538    99.3 | 82.638 % |
c |    109673 |   46236    95289 |   16953   17964  1912579   106.5 | 82.676 % |
c |    109824 |   46236    95289 |   18648   18115  1920817   106.0 | 82.676 % |
c |    110050 |   46236    95289 |   20513   18341  1933595   105.4 | 82.676 % |
c |    110387 |   46221    95254 |   22564   18674  1951460   104.5 | 82.716 % |
c |    110894 |   46221    95254 |   24821   19181  1987235   103.6 | 82.716 % |
c |    111653 |   46221    95254 |   27303   19940  2051460   102.9 | 82.716 % |
c |    112792 |   46174    95141 |   30033   21056  2143668   101.8 | 82.844 % |
c |    114503 |   46174    95141 |   33036   22767  2317315   101.8 | 82.844 % |
c |    117066 |   46174    95141 |   36340   25330  2565419   101.3 | 82.844 % |
c |    120910 |   46140    95059 |   39974   29170  2926517   100.3 | 82.940 % |
c |    126676 |   46140    95059 |   43972   34936  3469893    99.3 | 82.940 % |
c ==============================================================================
c [1mFound solution: -37[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 |    128815 |   46161    95117 |   15387   37075  3702991    99.9 | 82.940 % |
c |    128916 |   46161    95117 |   16925   17069  1143112    67.0 | 82.903 % |
c |    129066 |   46161    95117 |   18618   17219  1153278    67.0 | 82.903 % |
c |    129293 |   46161    95117 |   20480   17446  1162668    66.6 | 82.903 % |
c |    129630 |   46126    95028 |   22528   17771  1187614    66.8 | 83.011 % |
c |    130137 |   46126    95028 |   24780   18278  1223931    67.0 | 83.011 % |
c |    130896 |   46051    94848 |   27259   19008  1237330    65.1 | 83.219 % |
c |    132035 |   46015    94758 |   29984   20133  1322301    65.7 | 83.315 % |
c |    133744 |   46015    94758 |   32983   21842  1465933    67.1 | 83.315 % |
c |    136307 |   46015    94758 |   36281   24405  1721914    70.6 | 83.315 % |
c |    140151 |   46015    94758 |   39909   28249  2009666    71.1 | 83.315 % |
c |    145918 |   46013    94754 |   43900   34014  2543986    74.8 | 83.319 % |
c |    154568 |   45959    94626 |   48290   42576  3184772    74.8 | 83.467 % |
c |    167543 |   45913    94520 |   53120   55540  4225297    76.1 | 83.587 % |
c |    187005 |   45913    94520 |   58432   75002  6244640    83.3 | 83.587 % |
c |    216198 |   45876    94429 |   64275   44973  3102677    69.0 | 83.694 % |
c |    259987 |   45876    94429 |   70702   22219  1193746    53.7 | 83.694 % |
c |    325671 |   45838    94339 |   77773   87896  5215189    59.3 | 83.798 % |
c ==============================================================================
c [1mFound solution: -38[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 |    362744 |   45824    94273 |   15274   45452  1802921    39.7 | 83.798 % |
c |    362845 |   45824    94273 |   16801   20765   632823    30.5 | 83.844 % |
c |    362996 |   45824    94273 |   18481   20916   640662    30.6 | 83.844 % |
c |    363222 |   45824    94273 |   20329   21142   649300    30.7 | 83.844 % |
c |    363560 |   45824    94273 |   22362   21480   662066    30.8 | 83.844 % |
c |    364066 |   45824    94273 |   24598   21986   685062    31.2 | 83.844 % |
c |    364826 |   45824    94273 |   27058   22746   727210    32.0 | 83.844 % |
c |    365965 |   45824    94273 |   29764   23885   810735    33.9 | 83.844 % |
c |    367674 |   45824    94273 |   32741   25594   906072    35.4 | 83.844 % |
c |    370236 |   45824    94273 |   36015   28156  1054352    37.4 | 83.844 % |
c |    374082 |   45737    94058 |   39616   31979  1334937    41.7 | 84.083 % |
c |    379848 |   45698    93956 |   43578   37273  1691710    45.4 | 84.203 % |
c |    388498 |   45694    93948 |   47936   45919  2503857    54.5 | 84.211 % |
c |    401472 |   45694    93948 |   52729   58893  3447993    58.5 | 84.211 % |
c |    420934 |   45643    93821 |   58002   23036   699613    30.4 | 84.363 % |
c |    450126 |   45640    93814 |   63803   52227  1837279    35.2 | 84.371 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 C572 -C571 C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 C476 -C475 -C474 -C473 C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 C271 -C270 -C269 -C268 -C267 -C266 C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 25940
Raw data (stat): 25940 (runsolver) R 25939 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479207102 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.93 0.95 0.90 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 2848 0 0 0 991 8 0 0 25 0 1 0 479207102 14106624 2826 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3444 2826 603 41 0 3403 0
vsize: 13776
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 2955 0 0 0 1990 8 0 0 25 0 1 0 479207102 14663680 2933 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 2933 603 41 0 3539 0
vsize: 14320
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 2969 0 0 0 2989 8 0 0 25 0 1 0 479207102 14663680 2947 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3580 2947 603 41 0 3539 0
vsize: 14320
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 3184 0 0 0 3988 9 0 0 25 0 1 0 479207102 15654912 3162 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3822 3162 603 41 0 3781 0
vsize: 15288
[startup+50.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 3682 0 0 0 4987 11 0 0 25 0 1 0 479207102 17825792 3660 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4352 3660 603 41 0 4311 0
vsize: 17408
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 4410 0 0 0 5984 14 0 0 25 0 1 0 479207102 20779008 4388 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5073 4388 603 41 0 5032 0
vsize: 20292
[startup+70.0049 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 4960 0 0 0 6982 16 0 0 25 0 1 0 479207102 22929408 4938 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4938 603 41 0 5557 0
vsize: 22392
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 5460 0 0 0 7981 17 0 0 25 0 1 0 479207102 25075712 5438 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6122 5438 603 41 0 6081 0
vsize: 24488
[startup+90.0054 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 5971 0 0 0 8980 18 0 0 25 0 1 0 479207102 27226112 5949 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6647 5949 603 41 0 6606 0
vsize: 26588
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 6410 0 0 0 9978 20 0 0 25 0 1 0 479207102 28958720 6388 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7070 6388 603 41 0 7029 0
vsize: 28280
[startup+110.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 6900 0 0 0 10977 22 0 0 25 0 1 0 479207102 30961664 6878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7559 6878 603 41 0 7518 0
vsize: 30236
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 7288 0 0 0 11975 24 0 0 25 0 1 0 479207102 32567296 7266 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7951 7266 603 41 0 7910 0
vsize: 31804
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 7684 0 0 0 12974 25 0 0 25 0 1 0 479207102 34181120 7662 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8345 7662 603 41 0 8304 0
vsize: 33380
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 7944 0 0 0 13974 25 0 0 25 0 1 0 479207102 35250176 7922 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8606 7922 603 41 0 8565 0
vsize: 34424
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 14973 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 15973 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 16974 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 17974 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 18974 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 19974 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 20974 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8333 0 0 0 21975 26 0 0 25 0 1 0 479207102 36724736 8311 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8311 603 41 0 8925 0
vsize: 35864
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8378 0 0 0 22975 26 0 0 25 0 1 0 479207102 36995072 8356 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9032 8356 603 41 0 8991 0
vsize: 36128
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 8841 0 0 0 23973 28 0 0 25 0 1 0 479207102 38862848 8819 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9488 8819 603 41 0 9447 0
vsize: 37952
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9328 0 0 0 24972 29 0 0 25 0 1 0 479207102 40865792 9306 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9977 9306 603 41 0 9936 0
vsize: 39908
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 25971 30 0 0 25 0 1 0 479207102 42102784 9620 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10279 9620 603 41 0 10238 0
vsize: 41116
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 26972 30 0 0 25 0 1 0 479207102 42102784 9620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10279 9620 603 41 0 10238 0
vsize: 41116
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 27972 30 0 0 25 0 1 0 479207102 42102784 9620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10279 9620 603 41 0 10238 0
vsize: 41116
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 28972 30 0 0 25 0 1 0 479207102 42102784 9620 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10279 9620 603 41 0 10238 0
vsize: 41116
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 29972 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 30972 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 31972 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 32972 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 33973 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 34973 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 35973 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 36973 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 37973 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9642 0 0 0 38973 30 0 0 25 0 1 0 479207102 42098688 9620 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9620 603 41 0 10237 0
vsize: 41112
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9644 0 0 0 39974 30 0 0 25 0 1 0 479207102 42098688 9622 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10278 9622 603 41 0 10237 0
vsize: 41112
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9647 0 0 0 40974 30 0 0 25 0 1 0 479207102 42360832 9625 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9625 603 41 0 10301 0
vsize: 41368
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9650 0 0 0 41974 30 0 0 25 0 1 0 479207102 42360832 9628 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9628 603 41 0 10301 0
vsize: 41368
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9671 0 0 0 42974 30 0 0 25 0 1 0 479207102 42491904 9649 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10374 9649 603 41 0 10333 0
vsize: 41496
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 9940 0 0 0 43974 31 0 0 25 0 1 0 479207102 43560960 9918 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10635 9918 603 41 0 10594 0
vsize: 42540
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10210 0 0 0 44973 32 0 0 25 0 1 0 479207102 44634112 10188 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10897 10188 603 41 0 10856 0
vsize: 43588
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 45973 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223760 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 46973 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223792 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 47973 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 48973 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 49974 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+510.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 50974 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 51974 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+530.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 52974 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 53974 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 54974 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10386 0 0 0 55975 32 0 0 25 0 1 0 479207102 45432832 10364 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10364 603 41 0 11051 0
vsize: 44368
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10391 0 0 0 56975 32 0 0 25 0 1 0 479207102 45432832 10369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10369 603 41 0 11051 0
vsize: 44368
[startup+580.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10391 0 0 0 57975 32 0 0 25 0 1 0 479207102 45432832 10369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10369 603 41 0 11051 0
vsize: 44368
[startup+590.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10391 0 0 0 58975 32 0 0 25 0 1 0 479207102 45432832 10369 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10369 603 41 0 11051 0
vsize: 44368
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10391 0 0 0 59976 32 0 0 25 0 1 0 479207102 45432832 10369 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10369 603 41 0 11051 0
vsize: 44368
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10391 0 0 0 60976 32 0 0 25 0 1 0 479207102 45432832 10369 4294967295 134512640 134672761 3221224624 3221223808 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10369 603 41 0 11051 0
vsize: 44368
[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10391 0 0 0 61976 32 0 0 25 0 1 0 479207102 45432832 10369 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10369 603 41 0 11051 0
vsize: 44368
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10392 0 0 0 62976 32 0 0 25 0 1 0 479207102 45432832 10370 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10370 603 41 0 11051 0
vsize: 44368
[startup+640.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10400 0 0 0 63976 32 0 0 25 0 1 0 479207102 45432832 10378 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10378 603 41 0 11051 0
vsize: 44368
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10404 0 0 0 64977 33 0 0 25 0 1 0 479207102 45432832 10382 4294967295 134512640 134672761 3221224624 3221223728 134559958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10382 603 41 0 11051 0
vsize: 44368
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 65977 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 66977 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 67977 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 68977 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 69977 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+710.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 70978 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+720.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 71978 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+730.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 72978 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+740.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 73978 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+750.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 74978 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+760.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 75979 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+770.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 76979 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+780.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 77979 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+790.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 78979 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+800.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 79979 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 80980 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 81980 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+830.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 82980 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10406 0 0 0 83980 33 0 0 25 0 1 0 479207102 45432832 10384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11092 10384 603 41 0 11051 0
vsize: 44368
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10407 0 0 0 84980 33 0 0 25 0 1 0 479207102 45432832 10385 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11092 10385 603 41 0 11051 0
vsize: 44368
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10419 0 0 0 85979 33 0 0 25 0 1 0 479207102 45596672 10397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10397 603 41 0 11091 0
vsize: 44528
[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10422 0 0 0 86979 33 0 0 25 0 1 0 479207102 45596672 10400 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10400 603 41 0 11091 0
vsize: 44528
[startup+880.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10425 0 0 0 87980 33 0 0 25 0 1 0 479207102 45596672 10403 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10403 603 41 0 11091 0
vsize: 44528
[startup+890.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10428 0 0 0 88980 33 0 0 25 0 1 0 479207102 45596672 10406 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10406 603 41 0 11091 0
vsize: 44528
[startup+900.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 89980 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+910.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 90980 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+920.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 91980 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 92980 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+940.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 93981 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+950.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 94981 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+960.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 95981 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+970.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 96981 33 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134561091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+980.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 97980 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 98980 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 99980 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 100980 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 101981 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 102981 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 103981 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 104981 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 105981 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 106982 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 107982 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 108982 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 109982 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223728 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 110982 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 111983 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 112983 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 113983 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 114983 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 115983 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 116984 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 117984 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 118984 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25940
Raw data (stat): 25940 (minisat+) R 25939 23176 23175 0 -1 0 10430 0 0 0 119984 34 0 0 25 0 1 0 479207102 45596672 10408 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11132 10408 603 41 0 11091 0
vsize: 44528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25940
Raw data (stat): 25940 (minisat+) Z 25939 23176 23175 0 -1 12 10433 0 0 0 119984 36 0 0 25 0 1 0 479207102 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.08
CPU time (s): 1200.21
CPU user time (s): 1199.85
CPU system time (s): 0.362944
CPU usage (%): 100.011
Max. virtual memory (Kb): 44528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####