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/frb35-17-opb/normalized-frb35-17-4.opb
MD5SUM	e3892e1941a878802a8ccbbd36201a02
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-27
Optimality of the best value was proved	NO
Number of terms in the objective function	595
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	595
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	595
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.05
Number of variables	595
Total number of constraints	27842
Number of constraints which are clauses	27842
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 5238

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-13 22:50:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3706 boxname=wulflinc2 idbench=322 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e3892e1941a878802a8ccbbd36201a02  /oldhome/oroussel/tmp/wulflinc2/normalized-frb35-17-4.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc2/normalized-frb35-17-4.opb /oldhome/oroussel/tmp/wulflinc2/normalized-frb35-17-4.opb
IDLAUNCH: 3706
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        906128 kB
Buffers:         33928 kB
Cached:          74120 kB
SwapCached:          4 kB
Active:          56024 kB
Inactive:        54860 kB
HighTotal:      131008 kB
HighFree:        53116 kB
LowTotal:       903652 kB
LowFree:        853012 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12180 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:10:27 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3706 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27842 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 |   27842    55684 |    9280       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1165   maxlim: 26   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35809    84177 |   11936       0        0     nan |  0.000 % |
c |       100 |   35800    84146 |   13129      98      948     9.7 |  0.291 % |
c |       250 |   35791    84115 |   14442     245     3018    12.3 |  0.348 % |
c |       475 |   35755    83991 |   15886     460     5483    11.9 |  0.577 % |
c |       813 |   35719    83867 |   17475     789     9779    12.4 |  0.801 % |
c |      1319 |   35573    83365 |   19223    1258    16152    12.8 |  1.831 % |
c |      2078 |   35431    82879 |   21145    1979    27964    14.1 |  2.860 % |
c |      3218 |   35193    82063 |   23259    3022    44067    14.6 |  4.691 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 27   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3831 |   35077    81669 |   11692    3607    78430    21.7 |  4.691 % |
c |      3931 |   35062    81618 |   12861    3703    80358    21.7 |  5.832 % |
c |      4081 |   35042    81548 |   14147    3843    83780    21.8 |  6.009 % |
c |      4306 |   34949    81227 |   15562    4044    90952    22.5 |  6.807 % |
c |      4644 |   34917    81117 |   17118    4374   101577    23.2 |  7.090 % |
c |      5150 |   34744    80524 |   18830    4829   111282    23.0 |  8.463 % |
c |      5909 |   34665    80255 |   20713    5548   142470    25.7 |  9.151 % |
c |      7048 |   34616    80084 |   22784    6646   189597    28.5 |  9.548 % |
c |      8756 |   34258    78850 |   25062    8234   275221    33.4 | 12.756 % |
c |     11318 |   34101    78311 |   27569   10753   394884    36.7 | 14.351 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 28   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12578 |   34104    78324 |   11368   12013   487312    40.6 | 14.351 % |
c |     12678 |   34104    78324 |   12504    6107   255684    41.9 | 14.400 % |
c |     12829 |   34104    78324 |   13755    6258   262425    41.9 | 14.400 % |
c |     13054 |   34104    78324 |   15130    6483   275073    42.4 | 14.406 % |
c |     13391 |   34095    78293 |   16643    6810   286046    42.0 | 14.457 % |
c |     13897 |   34034    78082 |   18308    7303   307698    42.1 | 15.086 % |
c |     14656 |   33985    77911 |   20139    8048   370757    46.1 | 15.600 % |
c |     15795 |   33928    77712 |   22153    9155   425135    46.4 | 16.114 % |
c |     17503 |   33911    77653 |   24368   10859   603060    55.5 | 16.286 % |
c |     20066 |   33803    77281 |   26805   13393   811373    60.6 | 17.371 % |
c |     23912 |   33735    77043 |   29485   17226  1182265    68.6 | 18.114 % |
c |     29679 |   33718    76984 |   32434   22989  1682159    73.2 | 18.286 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33508 |   33670    76821 |   11223   26789  1925849    71.9 | 18.286 % |
c |     33608 |   33661    76790 |   12345    6793   279541    41.2 | 18.846 % |
c |     33758 |   33598    76569 |   13579    6935   285000    41.1 | 19.589 % |
c |     33983 |   33589    76538 |   14937    7156   295679    41.3 | 19.653 % |
c |     34320 |   33553    76412 |   16431    7485   310857    41.5 | 20.049 % |
c |     34827 |   33544    76381 |   18074    7984   339233    42.5 | 20.103 % |
c |     35588 |   33544    76381 |   19882    8745   389804    44.6 | 20.103 % |
c |     36727 |   33544    76381 |   21870    9884   471270    47.7 | 20.103 % |
c |     38436 |   33538    76361 |   24057   11589   592998    51.2 | 20.160 % |
c |     41000 |   33493    76208 |   26463   14146   826112    58.4 | 20.679 % |
c |     44844 |   33466    76115 |   29109   17980  1108297    61.6 | 20.845 % |
c |     50610 |   33460    76095 |   32020   23742  1502312    63.3 | 20.902 % |
c |     59259 |   33460    76095 |   35222   32391  2186630    67.5 | 20.907 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68187 |   33390    75859 |   11130   20805  1396742    67.1 | 20.907 % |
c |     68287 |   33390    75859 |   12243   10503   655226    62.4 | 21.632 % |
c |     68437 |   33363    75766 |   13467   10649   663758    62.3 | 21.918 % |
c |     68662 |   33363    75766 |   14814   10874   673386    61.9 | 21.918 % |
c |     68999 |   33363    75766 |   16295   11211   692514    61.8 | 21.918 % |
c |     69505 |   33257    75396 |   17924   11699   718240    61.4 | 23.059 % |
c |     70264 |   33257    75396 |   19717   12458   772855    62.0 | 23.059 % |
c |     71404 |   33248    75365 |   21689   13594   849734    62.5 | 23.122 % |
c |     73112 |   33223    75278 |   23858   15295   923359    60.4 | 23.402 % |
c |     75675 |   33203    75208 |   26243   17846  1176636    65.9 | 23.578 % |
c |     79519 |   33181    75130 |   28868   21680  1463853    67.5 | 23.801 % |
c |     85286 |   33138    74981 |   31755   27430  2023150    73.8 | 24.201 % |
c |     93935 |   33102    74855 |   34930   17802  1167827    65.6 | 24.600 % |
c |    106910 |   33072    74753 |   38423   30759  2279239    74.1 | 24.829 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    116306 |   33064    74708 |   11021   15080  1196400    79.3 | 24.829 % |
c |    116406 |   33064    74708 |   12123    7640   624320    81.7 | 24.890 % |
c |    116556 |   33056    74680 |   13335    7785   628008    80.7 | 25.004 % |
c |    116781 |   33056    74680 |   14668    8010   638444    79.7 | 25.000 % |
c |    117118 |   33056    74680 |   16135    8347   655341    78.5 | 25.004 % |
c |    117624 |   33056    74680 |   17749    8853   684038    77.3 | 25.003 % |
c |    118383 |   32998    74480 |   19524    9603   710657    74.0 | 25.685 % |
c |    119524 |   32974    74398 |   21476   10736   776813    72.4 | 25.860 % |
c |    121232 |   32974    74398 |   23624   12444   879061    70.6 | 25.856 % |
c |    123794 |   32948    74312 |   25986   14981  1040475    69.5 | 26.142 % |
c |    127639 |   32919    74209 |   28585   18818  1312549    69.7 | 26.541 % |
c |    133405 |   32919    74209 |   31444   24584  1794025    73.0 | 26.541 % |
c |    142054 |   32896    74130 |   34588   14685  1224425    83.4 | 26.769 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    152772 |   32962    74340 |   10987   25394  2124004    83.6 | 26.769 % |
c |    152872 |   32962    74340 |   12085    6449   409230    63.5 | 26.963 % |
c |    153022 |   32962    74340 |   13294    6599   413771    62.7 | 26.964 % |
c |    153247 |   32937    74253 |   14623    6822   426309    62.5 | 27.242 % |
c |    153584 |   32937    74253 |   16086    7159   436530    61.0 | 27.242 % |
c |    154091 |   32916    74182 |   17694    7654   456141    59.6 | 27.416 % |
c |    154852 |   32916    74182 |   19464    8415   510217    60.6 | 27.414 % |
c |    155991 |   32907    74151 |   21410    9532   578737    60.7 | 27.471 % |
c |    157700 |   32907    74151 |   23551   11241   690693    61.4 | 27.471 % |
c |    160262 |   32907    74151 |   25906   13803   898288    65.1 | 27.468 % |
c |    164106 |   32907    74151 |   28497   17647  1352466    76.6 | 27.471 % |
c |    169872 |   32907    74151 |   31347   23413  1733540    74.0 | 27.468 % |
c |    178522 |   32890    74092 |   34481   32059  2630457    82.1 | 27.637 % |
c |    191496 |   32890    74092 |   37930   23764  2113609    88.9 | 27.637 % |
c |    210957 |   32890    74092 |   41723   18571  1444564    77.8 | 27.637 % |
c |    240149 |   32890    74092 |   45895   19877  2471636   124.3 | 27.637 % |
c |    283939 |   32881    74061 |   50484   31898  3199608   100.3 | 27.698 % |
c |    349623 |   32881    74061 |   55533   26474  1799438    68.0 | 27.693 % |
c |    448150 |   32881    74061 |   61086   43927  6779193   154.3 | 27.698 % |
c |    595941 |   32803    73799 |   67195   52551  5088489    96.8 | 28.426 % |
#### 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.95 0.90 2/54 23516
Raw data (stat): 23516 (runsolver) R 23515 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421464489 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 1524 0 0 0 993 5 0 0 25 0 1 0 421464489 7823360 1502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1910 1502 603 41 0 1869 0
vsize: 7640
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 2511 0 0 0 1990 7 0 0 25 0 1 0 421464489 11878400 2489 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2900 2489 603 41 0 2859 0
vsize: 11600
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3069 0 0 0 2988 9 0 0 25 0 1 0 421464489 14123008 3047 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3448 3047 603 41 0 3407 0
vsize: 13792
[startup+40 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3069 0 0 0 3988 9 0 0 25 0 1 0 421464489 14123008 3047 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3448 3047 603 41 0 3407 0
vsize: 13792
[startup+50.0007 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3337 0 0 0 4987 10 0 0 25 0 1 0 421464489 15196160 3315 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3710 3315 603 41 0 3669 0
vsize: 14840
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3677 0 0 0 5986 11 0 0 25 0 1 0 421464489 16666624 3655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4069 3655 603 41 0 4028 0
vsize: 16276
[startup+70.0005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3677 0 0 0 6986 11 0 0 25 0 1 0 421464489 16666624 3655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4069 3655 603 41 0 4028 0
vsize: 16276
[startup+80.0008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3677 0 0 0 7986 11 0 0 25 0 1 0 421464489 16666624 3655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4069 3655 603 41 0 4028 0
vsize: 16276
[startup+90.0005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3711 0 0 0 8986 11 0 0 25 0 1 0 421464489 16797696 3689 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4101 3689 603 41 0 4060 0
vsize: 16404
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3711 0 0 0 9986 11 0 0 25 0 1 0 421464489 16797696 3689 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4101 3689 603 41 0 4060 0
vsize: 16404
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 3718 0 0 0 10986 11 0 0 25 0 1 0 421464489 16932864 3696 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4134 3696 603 41 0 4093 0
vsize: 16536
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4287 0 0 0 11985 12 0 0 25 0 1 0 421464489 19193856 4265 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4686 4265 603 41 0 4645 0
vsize: 18744
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 12984 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 13984 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 14984 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 15984 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 16985 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 17985 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 18985 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 19985 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 20985 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223656 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4595 0 0 0 21985 14 0 0 25 0 1 0 421464489 20389888 4573 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4573 603 41 0 4937 0
vsize: 19912
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4829 0 0 0 22985 14 0 0 25 0 1 0 421464489 21467136 4807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5241 4807 603 41 0 5200 0
vsize: 20964
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4914 0 0 0 23985 15 0 0 25 0 1 0 421464489 21733376 4892 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5306 4892 603 41 0 5265 0
vsize: 21224
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 4914 0 0 0 24985 15 0 0 25 0 1 0 421464489 21733376 4892 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5306 4892 603 41 0 5265 0
vsize: 21224
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 5128 0 0 0 25985 15 0 0 25 0 1 0 421464489 22679552 5106 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5537 5106 603 41 0 5496 0
vsize: 22148
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 5772 0 0 0 26983 17 0 0 25 0 1 0 421464489 25382912 5750 4294967295 134512640 134672761 3221224560 3221223744 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5750 603 41 0 6155 0
vsize: 24788
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 6381 0 0 0 27981 19 0 0 25 0 1 0 421464489 27795456 6359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6786 6359 603 41 0 6745 0
vsize: 27144
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 6523 0 0 0 28981 20 0 0 25 0 1 0 421464489 28459008 6501 4294967295 134512640 134672761 3221224560 3221223696 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6501 603 41 0 6907 0
vsize: 27792
[startup+299.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 6523 0 0 0 29981 20 0 0 25 0 1 0 421464489 28459008 6501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6501 603 41 0 6907 0
vsize: 27792
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 6523 0 0 0 30981 20 0 0 25 0 1 0 421464489 28459008 6501 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6501 603 41 0 6907 0
vsize: 27792
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 6523 0 0 0 31981 20 0 0 25 0 1 0 421464489 28459008 6501 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6501 603 41 0 6907 0
vsize: 27792
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 6547 0 0 0 32981 20 0 0 25 0 1 0 421464489 28459008 6525 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6948 6525 603 41 0 6907 0
vsize: 27792
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 6951 0 0 0 33980 21 0 0 25 0 1 0 421464489 30195712 6929 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7372 6929 603 41 0 7331 0
vsize: 29488
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7009 0 0 0 34981 21 0 0 25 0 1 0 421464489 30461952 6987 4294967295 134512640 134672761 3221224560 3221223664 134554919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 6987 603 41 0 7396 0
vsize: 29748
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7010 0 0 0 35981 21 0 0 25 0 1 0 421464489 30461952 6988 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 6988 603 41 0 7396 0
vsize: 29748
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7011 0 0 0 36981 21 0 0 25 0 1 0 421464489 30461952 6989 4294967295 134512640 134672761 3221224560 3221223632 134553557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 6989 603 41 0 7396 0
vsize: 29748
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7011 0 0 0 37981 21 0 0 25 0 1 0 421464489 30461952 6989 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 6989 603 41 0 7396 0
vsize: 29748
[startup+390 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7012 0 0 0 38981 21 0 0 25 0 1 0 421464489 30461952 6990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 6990 603 41 0 7396 0
vsize: 29748
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7012 0 0 0 39982 21 0 0 25 0 1 0 421464489 30461952 6990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 6990 603 41 0 7396 0
vsize: 29748
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 40982 21 0 0 25 0 1 0 421464489 30461952 6994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 6994 603 41 0 7396 0
vsize: 29748
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 41982 21 0 0 25 0 1 0 421464489 30445568 6994 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7433 6994 603 41 0 7392 0
vsize: 29732
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 42982 21 0 0 25 0 1 0 421464489 30445568 6994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7433 6994 603 41 0 7392 0
vsize: 29732
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 43982 21 0 0 25 0 1 0 421464489 30445568 6994 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7433 6994 603 41 0 7392 0
vsize: 29732
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 44983 21 0 0 25 0 1 0 421464489 30445568 6994 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7433 6994 603 41 0 7392 0
vsize: 29732
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 45983 21 0 0 25 0 1 0 421464489 30445568 6994 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7433 6994 603 41 0 7392 0
vsize: 29732
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 46983 21 0 0 25 0 1 0 421464489 30445568 6994 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7433 6994 603 41 0 7392 0
vsize: 29732
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 47983 21 0 0 25 0 1 0 421464489 30425088 6994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7428 6994 603 41 0 7387 0
vsize: 29712
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 48983 21 0 0 25 0 1 0 421464489 30425088 6994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7428 6994 603 41 0 7387 0
vsize: 29712
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 49983 21 0 0 25 0 1 0 421464489 30425088 6994 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7428 6994 603 41 0 7387 0
vsize: 29712
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 50983 21 0 0 25 0 1 0 421464489 30425088 6994 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7428 6994 603 41 0 7387 0
vsize: 29712
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 51983 21 0 0 25 0 1 0 421464489 30425088 6994 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7428 6994 603 41 0 7387 0
vsize: 29712
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7016 0 0 0 52983 21 0 0 25 0 1 0 421464489 30425088 6994 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7428 6994 603 41 0 7387 0
vsize: 29712
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7502 0 0 0 53982 22 0 0 25 0 1 0 421464489 32440320 7480 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7920 7480 603 41 0 7879 0
vsize: 31680
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7883 0 0 0 54981 24 0 0 25 0 1 0 421464489 33939456 7861 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8286 7861 603 41 0 8245 0
vsize: 33144
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7883 0 0 0 55981 24 0 0 25 0 1 0 421464489 33939456 7861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8286 7861 603 41 0 8245 0
vsize: 33144
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23516
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7883 0 0 0 56981 24 0 0 25 0 1 0 421464489 33939456 7861 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8286 7861 603 41 0 8245 0
vsize: 33144
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23520
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7893 0 0 0 57981 24 0 0 25 0 1 0 421464489 33939456 7871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8286 7871 603 41 0 8245 0
vsize: 33144
[startup+590.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 23569
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7895 0 0 0 58981 24 0 0 25 0 1 0 421464489 33939456 7873 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8286 7873 603 41 0 8245 0
vsize: 33144
[startup+600.004 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 23569
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 7905 0 0 0 59980 24 0 0 25 0 1 0 421464489 34074624 7883 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8319 7883 603 41 0 8278 0
vsize: 33276
[startup+610.004 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 23569
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 8541 0 0 0 60978 27 0 0 25 0 1 0 421464489 36630528 8519 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8519 603 41 0 8902 0
vsize: 35772
[startup+620.004 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23569
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 9117 0 0 0 61976 29 0 0 25 0 1 0 421464489 39055360 9095 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9535 9095 603 41 0 9494 0
vsize: 38140
[startup+630.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23569
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 9679 0 0 0 62974 31 0 0 25 0 1 0 421464489 41361408 9657 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10098 9657 603 41 0 10057 0
vsize: 40392
[startup+640.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23569
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10219 0 0 0 63973 33 0 0 25 0 1 0 421464489 43511808 10197 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10623 10197 603 41 0 10582 0
vsize: 42492
[startup+650.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10248 0 0 0 64973 33 0 0 25 0 1 0 421464489 43646976 10226 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10226 603 41 0 10615 0
vsize: 42624
[startup+660.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10248 0 0 0 65972 34 0 0 25 0 1 0 421464489 43646976 10226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10226 603 41 0 10615 0
vsize: 42624
[startup+670.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10248 0 0 0 66972 34 0 0 25 0 1 0 421464489 43646976 10226 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10226 603 41 0 10615 0
vsize: 42624
[startup+680.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10249 0 0 0 67972 34 0 0 25 0 1 0 421464489 43646976 10227 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10227 603 41 0 10615 0
vsize: 42624
[startup+690.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10250 0 0 0 68972 35 0 0 25 0 1 0 421464489 43646976 10228 4294967295 134512640 134672761 3221224560 3221223664 134560364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10228 603 41 0 10615 0
vsize: 42624
[startup+700.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10250 0 0 0 69971 35 0 0 25 0 1 0 421464489 43646976 10228 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10228 603 41 0 10615 0
vsize: 42624
[startup+710.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10250 0 0 0 70971 36 0 0 25 0 1 0 421464489 43646976 10228 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10228 603 41 0 10615 0
vsize: 42624
[startup+720.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10250 0 0 0 71971 36 0 0 25 0 1 0 421464489 43646976 10228 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10228 603 41 0 10615 0
vsize: 42624
[startup+730.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10298 0 0 0 72971 36 0 0 25 0 1 0 421464489 43917312 10276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10722 10276 603 41 0 10681 0
vsize: 42888
[startup+740.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 10737 0 0 0 73969 38 0 0 25 0 1 0 421464489 45662208 10715 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11148 10715 603 41 0 11107 0
vsize: 44592
[startup+750.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11156 0 0 0 74968 39 0 0 25 0 1 0 421464489 47415296 11134 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11576 11134 603 41 0 11535 0
vsize: 46304
[startup+760.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 75967 40 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+770.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 76967 40 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+780.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 77967 41 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+790.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 78967 41 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+800.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 79967 41 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+810.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 80967 42 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+820.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 81967 42 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+830.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 82967 42 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+840.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 83966 43 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+850.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 84966 43 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+860.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 85966 43 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+870.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 86966 44 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+880.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 87966 44 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+890.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 88966 44 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+900.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 89966 44 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+910.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 90965 45 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+920.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23571
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 91966 45 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+930.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 92965 46 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+940.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 93965 46 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+950.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 94965 46 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+960.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 95965 46 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223664 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+970.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 96965 47 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+980.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 97965 47 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+990.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 98965 47 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223724 134559748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 99965 48 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 100964 48 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 101964 48 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11309 0 0 0 102964 48 0 0 25 0 1 0 421464489 48087040 11287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11287 603 41 0 11699 0
vsize: 46960
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11312 0 0 0 103964 48 0 0 25 0 1 0 421464489 48087040 11290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11740 11290 603 41 0 11699 0
vsize: 46960
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11316 0 0 0 104964 49 0 0 25 0 1 0 421464489 48349184 11294 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11294 603 41 0 11763 0
vsize: 47216
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11316 0 0 0 105964 49 0 0 25 0 1 0 421464489 48349184 11294 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11294 603 41 0 11763 0
vsize: 47216
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11316 0 0 0 106964 50 0 0 25 0 1 0 421464489 48349184 11294 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11294 603 41 0 11763 0
vsize: 47216
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11316 0 0 0 107963 50 0 0 25 0 1 0 421464489 48349184 11294 4294967295 134512640 134672761 3221224560 3221223664 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11294 603 41 0 11763 0
vsize: 47216
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 108963 50 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 109963 51 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 110963 51 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 111963 51 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 112963 51 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 113963 52 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 114963 52 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 115963 52 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 116963 53 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 117962 53 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 118962 53 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23573
Raw data (stat): 23516 (minisat+) R 23515 20937 20936 0 -1 0 11321 0 0 0 119962 53 0 0 25 0 1 0 421464489 48349184 11299 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11299 603 41 0 11763 0
vsize: 47216
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 23573
Raw data (stat): 23516 (minisat+) Z 23515 20937 20936 0 -1 12 11324 0 0 0 119963 55 0 0 25 0 1 0 421464489 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.19
CPU user time (s): 1199.63
CPU system time (s): 0.556915
CPU usage (%): 100.013
Max. virtual memory (Kb): 47216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####