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/frb30-15-opb/normalized-frb30-15-1.opb
MD5SUM	84d0b0ba659c599a6c66454cd956a06b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
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	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04684
Number of variables	450
Total number of constraints	17827
Number of constraints which are clauses	17827
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 5230

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-13 22:43:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3698 boxname=wulflinc8 idbench=314 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  84d0b0ba659c599a6c66454cd956a06b  /oldhome/oroussel/tmp/wulflinc8/normalized-frb30-15-1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-frb30-15-1.opb /oldhome/oroussel/tmp/wulflinc8/normalized-frb30-15-1.opb
IDLAUNCH: 3698
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        907224 kB
Buffers:         36768 kB
Cached:          71216 kB
SwapCached:          0 kB
Active:          73196 kB
Inactive:        37728 kB
HighTotal:      131008 kB
HighFree:        55860 kB
LowTotal:       903652 kB
LowFree:        851364 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11040 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:03:49 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3698 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17827 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 |   17827    35654 |    5942       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 883   maxlim: 22   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23850    57184 |    7950       0        0     nan |  0.000 % |
c |       101 |   23850    57184 |    8745     101      952     9.4 |  0.309 % |
c |       251 |   23826    57102 |    9619     246     2731    11.1 |  0.604 % |
c |       476 |   23817    57071 |   10581     470     4734    10.1 |  0.604 % |
c |       813 |   23748    56834 |   11639     791     7665     9.7 |  1.215 % |
c |      1319 |   23377    55559 |   12803    1215    13908    11.4 |  4.981 % |
c |      2078 |   22954    54106 |   14083    1866    23656    12.7 |  9.811 % |
c |      3217 |   22734    53344 |   15492    2942    54567    18.5 | 12.528 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4209 |   22338    51973 |    7446    3779    84306    22.3 | 12.528 % |
c |      4309 |   22332    51953 |    8190    3875    86516    22.3 | 17.860 % |
c |      4459 |   22231    51604 |    9009    3984    88409    22.2 | 19.292 % |
c |      4685 |   22146    51307 |    9910    4185    94033    22.5 | 20.497 % |
c |      5022 |   22113    51190 |   10901    4509   100338    22.3 | 20.950 % |
c |      5528 |   22065    51026 |   11991    4937   113092    22.9 | 21.402 % |
c |      6287 |   21950    50625 |   13191    5588   140550    25.2 | 22.992 % |
c |      7428 |   21837    50228 |   14510    6612   184195    27.9 | 24.642 % |
c |      9137 |   21763    49970 |   15961    8256   251981    30.5 | 25.555 % |
c |     11699 |   21731    49858 |   17557   10773   398361    37.0 | 25.848 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14131 |   21705    49773 |    7235   13150   526178    40.0 | 25.848 % |
c |     14231 |   21705    49773 |    7958    6675   271304    40.6 | 26.205 % |
c |     14382 |   21705    49773 |    8754    6826   276380    40.5 | 26.205 % |
c |     14607 |   21705    49773 |    9629    7051   285837    40.5 | 26.205 % |
c |     14945 |   21631    49517 |   10592    7358   295094    40.1 | 27.417 % |
c |     15451 |   21631    49517 |   11652    7864   317235    40.3 | 27.410 % |
c |     16210 |   21581    49343 |   12817    8606   344935    40.1 | 28.170 % |
c |     17349 |   21581    49343 |   14098    9745   412523    42.3 | 28.170 % |
c |     19057 |   21474    48978 |   15508   11389   489167    43.0 | 29.744 % |
c |     21619 |   21410    48752 |   17059   13928   588621    42.3 | 30.723 % |
c |     25463 |   21410    48752 |   18765   17772   851770    47.9 | 30.723 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 26   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29876 |   21411    48759 |    7137   12369   622703    50.3 | 30.723 % |
c |     29976 |   21411    48759 |    7850    6285   299600    47.7 | 30.775 % |
c |     30126 |   21402    48728 |    8635    6432   302584    47.0 | 30.850 % |
c |     30352 |   21402    48728 |    9499    6658   314870    47.3 | 30.857 % |
c |     30689 |   21402    48728 |   10449    6995   327320    46.8 | 30.850 % |
c |     31196 |   21402    48728 |   11494    7502   359826    48.0 | 30.850 % |
c |     31955 |   21381    48657 |   12643    8251   394063    47.8 | 31.076 % |
c |     33094 |   21381    48657 |   13907    9390   454229    48.4 | 31.076 % |
c |     34802 |   21381    48657 |   15298   11098   572881    51.6 | 31.076 % |
c |     37365 |   21346    48540 |   16828   13650   718443    52.6 | 31.533 % |
c |     41209 |   21346    48540 |   18511   17494   880672    50.3 | 31.528 % |
c |     46975 |   21232    48140 |   20362   13686   547533    40.0 | 33.265 % |
c |     55624 |   21192    47996 |   22398   11805   437019    37.0 | 34.011 % |
c |     68598 |   21175    47937 |   24638   13135   711071    54.1 | 34.242 % |
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 |     82707 |   21176    47942 |    7058   14560   713317    49.0 | 34.242 % |
c |     82808 |   21176    47942 |    7763    7381   309515    41.9 | 34.292 % |
c |     82959 |   21176    47942 |    8540    7532   311301    41.3 | 34.286 % |
c |     83184 |   21176    47942 |    9394    7757   319471    41.2 | 34.292 % |
c |     83522 |   21176    47942 |   10333    8095   332847    41.1 | 34.286 % |
c |     84028 |   21176    47942 |   11366    8601   350841    40.8 | 34.286 % |
c |     84787 |   21158    47878 |   12503    9345   382777    41.0 | 34.662 % |
c |     85928 |   21158    47878 |   13754   10486   426559    40.7 | 34.662 % |
c |     87636 |   21158    47878 |   15129   12194   499599    41.0 | 34.662 % |
c |     90198 |   21158    47878 |   16642   14756   644432    43.7 | 34.662 % |
c |     94042 |   21158    47878 |   18306    9890   387270    39.2 | 34.662 % |
c |     99809 |   21158    47878 |   20137   15657   566329    36.2 | 34.667 % |
c |    108458 |   21158    47878 |   22151   13840   395050    28.5 | 34.662 % |
c |    121433 |   21158    47878 |   24366   15367   326906    21.3 | 34.662 % |
c |    140896 |   21158    47878 |   26802   22257   627716    28.2 | 34.662 % |
c |    170088 |   21158    47878 |   29483   23913   590021    24.7 | 34.662 % |
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 |    189122 |   21159    47885 |    7053   27796   659058    23.7 | 34.662 % |
c |    189223 |   21159    47885 |    7758    7050   136110    19.3 | 34.717 % |
c |    189374 |   21159    47885 |    8534    7201   139546    19.4 | 34.711 % |
c |    189601 |   21159    47885 |    9387    7428   145536    19.6 | 34.711 % |
c |    189939 |   21159    47885 |   10326    7766   156267    20.1 | 34.717 % |
c |    190445 |   21159    47885 |   11358    8272   174309    21.1 | 34.711 % |
c |    191205 |   21159    47885 |   12494    9032   210816    23.3 | 34.711 % |
c |    192344 |   21159    47885 |   13744   10171   259932    25.6 | 34.711 % |
c |    194053 |   21159    47885 |   15118   11880   298732    25.1 | 34.711 % |
c |    196615 |   21136    47804 |   16630   14426   386854    26.8 | 35.086 % |
c |    200461 |   21136    47804 |   18293    9512   342147    36.0 | 35.093 % |
c |    206227 |   21136    47804 |   20123   15278   588641    38.5 | 35.086 % |
c |    214877 |   21136    47804 |   22135   13500   516894    38.3 | 35.092 % |
c |    227852 |   21136    47804 |   24348   15060   334115    22.2 | 35.087 % |
c |    247313 |   21136    47804 |   26783   21997   575676    26.2 | 35.086 % |
c |    276506 |   21136    47804 |   29462   23740   434761    18.3 | 35.092 % |
c |    320295 |   21136    47804 |   32408   22261   445847    20.0 | 35.092 % |
c |    385980 |   21136    47804 |   35649   19546   317329    16.2 | 35.092 % |
c |    484506 |   21136    47804 |   39214   24858   458182    18.4 | 35.092 % |
c |    632295 |   21136    47804 |   43135   23692   425727    18.0 | 35.092 % |
c |    853978 |   21136    47804 |   47449   40466   896483    22.2 | 35.092 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.91 1/54 30365
Raw data (stat): 30365 (runsolver) R 30364 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 407858339 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 1303 0 0 0 994 4 0 0 25 0 1 0 407858339 6901760 1281 4294967295 134512640 134672761 3221224560 3221223664 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1685 1281 603 41 0 1644 0
vsize: 6740
[startup+20.0021 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 1824 0 0 0 1992 6 0 0 25 0 1 0 407858339 9142272 1802 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1802 603 41 0 2191 0
vsize: 8928
[startup+30.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 1844 0 0 0 2991 6 0 0 25 0 1 0 407858339 9142272 1822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1822 603 41 0 2191 0
vsize: 8928
[startup+40.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 1848 0 0 0 3991 6 0 0 25 0 1 0 407858339 9142272 1826 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1826 603 41 0 2191 0
vsize: 8928
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2115 0 0 0 4990 6 0 0 25 0 1 0 407858339 10240000 2093 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2500 2093 603 41 0 2459 0
vsize: 10000
[startup+60.0038 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2298 0 0 0 5990 7 0 0 25 0 1 0 407858339 11046912 2276 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2697 2276 603 41 0 2656 0
vsize: 10788
[startup+70.0051 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2447 0 0 0 6988 8 0 0 25 0 1 0 407858339 11718656 2425 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2861 2425 603 41 0 2820 0
vsize: 11444
[startup+80.0056 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2447 0 0 0 7988 8 0 0 25 0 1 0 407858339 11718656 2425 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2425 603 41 0 2820 0
vsize: 11444
[startup+90.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2447 0 0 0 8988 8 0 0 25 0 1 0 407858339 11718656 2425 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2425 603 41 0 2820 0
vsize: 11444
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2447 0 0 0 9988 8 0 0 25 0 1 0 407858339 11718656 2425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2425 603 41 0 2820 0
vsize: 11444
[startup+110.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2447 0 0 0 10989 8 0 0 25 0 1 0 407858339 11718656 2425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2425 603 41 0 2820 0
vsize: 11444
[startup+120.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2450 0 0 0 11989 8 0 0 25 0 1 0 407858339 11718656 2428 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2428 603 41 0 2820 0
vsize: 11444
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2450 0 0 0 12989 8 0 0 25 0 1 0 407858339 11718656 2428 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2428 603 41 0 2820 0
vsize: 11444
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2452 0 0 0 13989 8 0 0 25 0 1 0 407858339 11718656 2430 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2430 603 41 0 2820 0
vsize: 11444
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2452 0 0 0 14990 8 0 0 25 0 1 0 407858339 11718656 2430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2430 603 41 0 2820 0
vsize: 11444
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2452 0 0 0 15990 8 0 0 25 0 1 0 407858339 11718656 2430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2430 603 41 0 2820 0
vsize: 11444
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2452 0 0 0 16990 8 0 0 25 0 1 0 407858339 11718656 2430 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2430 603 41 0 2820 0
vsize: 11444
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2452 0 0 0 17990 8 0 0 25 0 1 0 407858339 11718656 2430 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2430 603 41 0 2820 0
vsize: 11444
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2454 0 0 0 18990 8 0 0 25 0 1 0 407858339 11718656 2432 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2432 603 41 0 2820 0
vsize: 11444
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2454 0 0 0 19990 8 0 0 25 0 1 0 407858339 11718656 2432 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2432 603 41 0 2820 0
vsize: 11444
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2454 0 0 0 20991 8 0 0 25 0 1 0 407858339 11718656 2432 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2432 603 41 0 2820 0
vsize: 11444
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2456 0 0 0 21991 8 0 0 25 0 1 0 407858339 11718656 2434 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2434 603 41 0 2820 0
vsize: 11444
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2456 0 0 0 22991 8 0 0 25 0 1 0 407858339 11718656 2434 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2434 603 41 0 2820 0
vsize: 11444
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2456 0 0 0 23991 8 0 0 25 0 1 0 407858339 11718656 2434 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2434 603 41 0 2820 0
vsize: 11444
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2456 0 0 0 24991 8 0 0 25 0 1 0 407858339 11718656 2434 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2434 603 41 0 2820 0
vsize: 11444
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2491 0 0 0 25991 8 0 0 25 0 1 0 407858339 11980800 2469 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2469 603 41 0 2884 0
vsize: 11700
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2491 0 0 0 26991 8 0 0 25 0 1 0 407858339 11980800 2469 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2469 603 41 0 2884 0
vsize: 11700
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2491 0 0 0 27992 8 0 0 25 0 1 0 407858339 11980800 2469 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2469 603 41 0 2884 0
vsize: 11700
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2491 0 0 0 28992 8 0 0 25 0 1 0 407858339 11980800 2469 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2469 603 41 0 2884 0
vsize: 11700
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2491 0 0 0 29992 8 0 0 25 0 1 0 407858339 11980800 2469 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2469 603 41 0 2884 0
vsize: 11700
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2491 0 0 0 30992 8 0 0 25 0 1 0 407858339 11980800 2469 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2469 603 41 0 2884 0
vsize: 11700
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2492 0 0 0 31992 8 0 0 25 0 1 0 407858339 11980800 2470 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2470 603 41 0 2884 0
vsize: 11700
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2495 0 0 0 32993 8 0 0 25 0 1 0 407858339 11980800 2473 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2473 603 41 0 2884 0
vsize: 11700
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2495 0 0 0 33993 8 0 0 25 0 1 0 407858339 11980800 2473 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2473 603 41 0 2884 0
vsize: 11700
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2495 0 0 0 34993 8 0 0 25 0 1 0 407858339 11980800 2473 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2473 603 41 0 2884 0
vsize: 11700
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2495 0 0 0 35993 8 0 0 25 0 1 0 407858339 11980800 2473 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2473 603 41 0 2884 0
vsize: 11700
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2495 0 0 0 36993 8 0 0 25 0 1 0 407858339 11980800 2473 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2473 603 41 0 2884 0
vsize: 11700
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2496 0 0 0 37994 8 0 0 25 0 1 0 407858339 11980800 2474 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2474 603 41 0 2884 0
vsize: 11700
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2496 0 0 0 38994 8 0 0 25 0 1 0 407858339 11980800 2474 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2474 603 41 0 2884 0
vsize: 11700
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2496 0 0 0 39994 8 0 0 25 0 1 0 407858339 11980800 2474 4294967295 134512640 134672761 3221224560 3221223708 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2474 603 41 0 2884 0
vsize: 11700
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2496 0 0 0 40994 8 0 0 25 0 1 0 407858339 11980800 2474 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2474 603 41 0 2884 0
vsize: 11700
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2500 0 0 0 41994 8 0 0 25 0 1 0 407858339 11980800 2478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2478 603 41 0 2884 0
vsize: 11700
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2500 0 0 0 42994 8 0 0 25 0 1 0 407858339 11980800 2478 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2478 603 41 0 2884 0
vsize: 11700
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2516 0 0 0 43995 8 0 0 25 0 1 0 407858339 11980800 2494 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2925 2494 603 41 0 2884 0
vsize: 11700
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2532 0 0 0 44995 8 0 0 25 0 1 0 407858339 12115968 2510 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2510 603 41 0 2917 0
vsize: 11832
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2539 0 0 0 45995 8 0 0 25 0 1 0 407858339 12115968 2517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2517 603 41 0 2917 0
vsize: 11832
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2549 0 0 0 46995 8 0 0 25 0 1 0 407858339 12255232 2527 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2527 603 41 0 2951 0
vsize: 11968
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2549 0 0 0 47996 8 0 0 25 0 1 0 407858339 12255232 2527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2527 603 41 0 2951 0
vsize: 11968
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2555 0 0 0 48996 8 0 0 25 0 1 0 407858339 12255232 2533 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2533 603 41 0 2951 0
vsize: 11968
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2555 0 0 0 49996 8 0 0 25 0 1 0 407858339 12255232 2533 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2533 603 41 0 2951 0
vsize: 11968
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2566 0 0 0 50996 8 0 0 25 0 1 0 407858339 12255232 2544 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2544 603 41 0 2951 0
vsize: 11968
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2567 0 0 0 51996 8 0 0 25 0 1 0 407858339 12255232 2545 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2545 603 41 0 2951 0
vsize: 11968
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2576 0 0 0 52996 8 0 0 25 0 1 0 407858339 12419072 2554 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3032 2554 603 41 0 2991 0
vsize: 12128
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2590 0 0 0 53996 9 0 0 25 0 1 0 407858339 12419072 2568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3032 2568 603 41 0 2991 0
vsize: 12128
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2590 0 0 0 54997 9 0 0 25 0 1 0 407858339 12419072 2568 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3032 2568 603 41 0 2991 0
vsize: 12128
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2608 0 0 0 55997 9 0 0 25 0 1 0 407858339 12582912 2586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2586 603 41 0 3031 0
vsize: 12288
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2630 0 0 0 56996 9 0 0 25 0 1 0 407858339 12582912 2608 4294967295 134512640 134672761 3221224560 3221223760 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3072 2608 603 41 0 3031 0
vsize: 12288
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2630 0 0 0 57996 9 0 0 25 0 1 0 407858339 12582912 2608 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2608 603 41 0 3031 0
vsize: 12288
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2632 0 0 0 58996 9 0 0 25 0 1 0 407858339 12582912 2610 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2610 603 41 0 3031 0
vsize: 12288
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2633 0 0 0 59996 9 0 0 25 0 1 0 407858339 12582912 2611 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2611 603 41 0 3031 0
vsize: 12288
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2633 0 0 0 60997 9 0 0 25 0 1 0 407858339 12582912 2611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2611 603 41 0 3031 0
vsize: 12288
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2650 0 0 0 61997 9 0 0 25 0 1 0 407858339 12746752 2628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2628 603 41 0 3071 0
vsize: 12448
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2651 0 0 0 62997 9 0 0 25 0 1 0 407858339 12746752 2629 4294967295 134512640 134672761 3221224560 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2629 603 41 0 3071 0
vsize: 12448
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2651 0 0 0 63997 9 0 0 25 0 1 0 407858339 12746752 2629 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2629 603 41 0 3071 0
vsize: 12448
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2660 0 0 0 64997 9 0 0 25 0 1 0 407858339 12746752 2638 4294967295 134512640 134672761 3221224560 3221223744 134559280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2638 603 41 0 3071 0
vsize: 12448
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2669 0 0 0 65997 9 0 0 25 0 1 0 407858339 12910592 2647 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2647 603 41 0 3111 0
vsize: 12608
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2669 0 0 0 66998 9 0 0 25 0 1 0 407858339 12910592 2647 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2647 603 41 0 3111 0
vsize: 12608
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2669 0 0 0 67998 9 0 0 25 0 1 0 407858339 12910592 2647 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2647 603 41 0 3111 0
vsize: 12608
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2669 0 0 0 68998 9 0 0 25 0 1 0 407858339 12910592 2647 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2647 603 41 0 3111 0
vsize: 12608
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2669 0 0 0 69998 9 0 0 25 0 1 0 407858339 12910592 2647 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2647 603 41 0 3111 0
vsize: 12608
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2682 0 0 0 70998 9 0 0 25 0 1 0 407858339 12910592 2660 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2660 603 41 0 3111 0
vsize: 12608
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2689 0 0 0 71999 9 0 0 25 0 1 0 407858339 12910592 2667 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2667 603 41 0 3111 0
vsize: 12608
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2702 0 0 0 72999 9 0 0 25 0 1 0 407858339 13074432 2680 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3192 2680 603 41 0 3151 0
vsize: 12768
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2704 0 0 0 73999 9 0 0 25 0 1 0 407858339 13074432 2682 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3192 2682 603 41 0 3151 0
vsize: 12768
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2710 0 0 0 74999 9 0 0 25 0 1 0 407858339 13074432 2688 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3192 2688 603 41 0 3151 0
vsize: 12768
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2710 0 0 0 75999 9 0 0 25 0 1 0 407858339 13074432 2688 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3192 2688 603 41 0 3151 0
vsize: 12768
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2711 0 0 0 76999 9 0 0 25 0 1 0 407858339 13074432 2689 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3192 2689 603 41 0 3151 0
vsize: 12768
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2711 0 0 0 78000 9 0 0 25 0 1 0 407858339 13074432 2689 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3192 2689 603 41 0 3151 0
vsize: 12768
[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2726 0 0 0 79002 9 0 0 25 0 1 0 407858339 13238272 2704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3232 2704 603 41 0 3191 0
vsize: 12928
[startup+800.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2726 0 0 0 80003 9 0 0 25 0 1 0 407858339 13238272 2704 4294967295 134512640 134672761 3221224560 3221223728 134559063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3232 2704 603 41 0 3191 0
vsize: 12928
[startup+810.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2726 0 0 0 81003 9 0 0 25 0 1 0 407858339 13238272 2704 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3232 2704 603 41 0 3191 0
vsize: 12928
[startup+820.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2732 0 0 0 82003 9 0 0 25 0 1 0 407858339 13238272 2710 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3232 2710 603 41 0 3191 0
vsize: 12928
[startup+830.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2834 0 0 0 83003 9 0 0 25 0 1 0 407858339 13639680 2812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3330 2812 603 41 0 3289 0
vsize: 13320
[startup+840.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2980 0 0 0 84002 10 0 0 25 0 1 0 407858339 14176256 2958 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2958 603 41 0 3420 0
vsize: 13844
[startup+850.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 2996 0 0 0 85003 10 0 0 25 0 1 0 407858339 14311424 2974 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3494 2974 603 41 0 3453 0
vsize: 13976
[startup+860.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3021 0 0 0 86003 10 0 0 25 0 1 0 407858339 14475264 2999 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 2999 603 41 0 3493 0
vsize: 14136
[startup+870.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3022 0 0 0 87003 10 0 0 25 0 1 0 407858339 14475264 3000 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3000 603 41 0 3493 0
vsize: 14136
[startup+880.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3022 0 0 0 88003 10 0 0 25 0 1 0 407858339 14475264 3000 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3000 603 41 0 3493 0
vsize: 14136
[startup+890.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3022 0 0 0 89003 10 0 0 25 0 1 0 407858339 14475264 3000 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3000 603 41 0 3493 0
vsize: 14136
[startup+900.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3022 0 0 0 90004 10 0 0 25 0 1 0 407858339 14475264 3000 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3000 603 41 0 3493 0
vsize: 14136
[startup+910.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3057 0 0 0 91004 10 0 0 25 0 1 0 407858339 14639104 3035 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3035 603 41 0 3533 0
vsize: 14296
[startup+920.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3057 0 0 0 92004 10 0 0 25 0 1 0 407858339 14639104 3035 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3035 603 41 0 3533 0
vsize: 14296
[startup+930.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3057 0 0 0 93004 10 0 0 25 0 1 0 407858339 14639104 3035 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3035 603 41 0 3533 0
vsize: 14296
[startup+940.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3059 0 0 0 94004 10 0 0 25 0 1 0 407858339 14639104 3037 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3037 603 41 0 3533 0
vsize: 14296
[startup+950.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3059 0 0 0 95004 10 0 0 25 0 1 0 407858339 14639104 3037 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3037 603 41 0 3533 0
vsize: 14296
[startup+960.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3059 0 0 0 96005 10 0 0 25 0 1 0 407858339 14639104 3037 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3037 603 41 0 3533 0
vsize: 14296
[startup+970.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30365
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3059 0 0 0 97005 10 0 0 25 0 1 0 407858339 14639104 3037 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3037 603 41 0 3533 0
vsize: 14296
[startup+980.058 s]
Raw data (loadavg): 0.99 0.97 0.91 4/59 30417
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3059 0 0 0 98005 10 0 0 25 0 1 0 407858339 14639104 3037 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3037 603 41 0 3533 0
vsize: 14296
[startup+990.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30418
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3059 0 0 0 99005 10 0 0 25 0 1 0 407858339 14639104 3037 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3037 603 41 0 3533 0
vsize: 14296
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30418
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3059 0 0 0 100005 11 0 0 25 0 1 0 407858339 14639104 3037 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3037 603 41 0 3533 0
vsize: 14296
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30418
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3064 0 0 0 101005 11 0 0 25 0 1 0 407858339 14639104 3042 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3042 603 41 0 3533 0
vsize: 14296
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30418
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3064 0 0 0 102005 11 0 0 25 0 1 0 407858339 14639104 3042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3042 603 41 0 3533 0
vsize: 14296
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30418
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3064 0 0 0 103005 11 0 0 25 0 1 0 407858339 14639104 3042 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3042 603 41 0 3533 0
vsize: 14296
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30418
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3064 0 0 0 104005 11 0 0 25 0 1 0 407858339 14639104 3042 4294967295 134512640 134672761 3221224560 3221223712 134565121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3042 603 41 0 3533 0
vsize: 14296
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3073 0 0 0 105005 12 0 0 25 0 1 0 407858339 14639104 3051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3051 603 41 0 3533 0
vsize: 14296
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3074 0 0 0 106005 12 0 0 25 0 1 0 407858339 14639104 3052 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3052 603 41 0 3533 0
vsize: 14296
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3074 0 0 0 107005 12 0 0 25 0 1 0 407858339 14639104 3052 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3052 603 41 0 3533 0
vsize: 14296
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3074 0 0 0 108004 13 0 0 25 0 1 0 407858339 14639104 3052 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3052 603 41 0 3533 0
vsize: 14296
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3075 0 0 0 109004 13 0 0 25 0 1 0 407858339 14639104 3053 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3053 603 41 0 3533 0
vsize: 14296
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3076 0 0 0 110004 13 0 0 25 0 1 0 407858339 14639104 3054 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3054 603 41 0 3533 0
vsize: 14296
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3076 0 0 0 111004 13 0 0 25 0 1 0 407858339 14639104 3054 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3054 603 41 0 3533 0
vsize: 14296
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3084 0 0 0 112004 13 0 0 25 0 1 0 407858339 14639104 3062 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3574 3062 603 41 0 3533 0
vsize: 14296
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3086 0 0 0 113005 13 0 0 25 0 1 0 407858339 14802944 3064 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3064 603 41 0 3573 0
vsize: 14456
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3087 0 0 0 114004 14 0 0 25 0 1 0 407858339 14802944 3065 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3065 603 41 0 3573 0
vsize: 14456
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3087 0 0 0 115004 14 0 0 25 0 1 0 407858339 14802944 3065 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3065 603 41 0 3573 0
vsize: 14456
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3092 0 0 0 116004 14 0 0 25 0 1 0 407858339 14802944 3070 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3070 603 41 0 3573 0
vsize: 14456
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3093 0 0 0 117004 14 0 0 25 0 1 0 407858339 14802944 3071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3071 603 41 0 3573 0
vsize: 14456
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3093 0 0 0 118004 15 0 0 25 0 1 0 407858339 14802944 3071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3071 603 41 0 3573 0
vsize: 14456
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3102 0 0 0 119004 15 0 0 25 0 1 0 407858339 14802944 3080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3080 603 41 0 3573 0
vsize: 14456
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30420
Raw data (stat): 30365 (minisat+) R 30364 26667 26666 0 -1 0 3113 0 0 0 120004 16 0 0 25 0 1 0 407858339 14802944 3091 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3614 3091 603 41 0 3573 0
vsize: 14456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30420
Raw data (stat): 30365 (minisat+) Z 30364 26667 26666 0 -1 12 3116 0 0 0 120004 16 0 0 25 0 1 0 407858339 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.07
CPU time (s): 1200.21
CPU user time (s): 1200.04
CPU system time (s): 0.167974
CPU usage (%): 100.011
Max. virtual memory (Kb): 14456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####