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 30507

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-05-25 17:15:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21910 boxname=wulflinc28 idbench=328 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  38d41fdbe49543e8928c5210e4323f00  /oldhome/oroussel/tmp/wulflinc28/normalized-frb40-19-5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-frb40-19-5.opb
IDLAUNCH: 21910
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        508176 kB
Buffers:         32788 kB
Cached:         471944 kB
SwapCached:       1052 kB
Active:          59840 kB
Inactive:       447424 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        507924 kB
SwapTotal:     2097640 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5468 kB
Slab:            13520 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 17:35:57 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21910 7 1229.85 152
#### 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  7224 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.96 2/54 7220
Raw data (stat): 7220 (runsolver) R 7219 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840609133 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0023 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0014 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.002 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.002 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+389.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+399.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+409.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+429.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+439.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+449.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+459.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+469.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+479.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+489.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+499.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+519.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+529.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+539.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+549.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+559.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+569.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+579.996 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+589.996 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+599.996 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+609.995 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+619.995 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+629.995 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+639.994 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+649.995 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+659.995 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+669.996 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+679.996 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+689.996 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+699.996 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+709.997 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+719.998 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+739.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+749.999 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 0.99 0.97 0.96 1/53 7224
Raw data (stat): 7220 (minisat+_script) S 7219 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840609133 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.85
CPU user time (s): 1229.31
CPU system time (s): 0.543917
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####