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-3.opb
MD5SUM	063fe125a766c5e46d0ecbf211fd8049
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.04584
Number of variables	450
Total number of constraints	17809
Number of constraints which are clauses	17809
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 5232

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        904908 kB
Buffers:         36728 kB
Cached:          73704 kB
SwapCached:          0 kB
Active:          72488 kB
Inactive:        40804 kB
HighTotal:      131008 kB
HighFree:        53424 kB
LowTotal:       903652 kB
LowFree:        851484 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10956 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:05:09 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3700 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17809 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 |   17809    35618 |    5936       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 883   maxlim: 23   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23816    57084 |    7938       0        0     nan |  0.000 % |
c |       100 |   23798    57022 |    8731      94      790     8.4 |  0.311 % |
c |       250 |   23798    57022 |    9604     244     2447    10.0 |  0.313 % |
c |       475 |   23747    56847 |   10565     458     4254     9.3 |  0.758 % |
c |       813 |   23702    56694 |   11622     789     8242    10.4 |  1.212 % |
c |      1319 |   23675    56601 |   12784    1287    15431    12.0 |  1.439 % |
c |      2078 |   23527    56091 |   14062    2008    27476    13.7 |  2.879 % |
c |      3217 |   23270    55206 |   15468    3062    51315    16.8 |  5.462 % |
c |      4925 |   22979    54201 |   17015    4667    93293    20.0 |  8.712 % |
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 |      5740 |   22880    53862 |    7626    5420   123126    22.7 |  8.712 % |
c |      5841 |   22834    53706 |    8388    5507   125167    22.7 | 10.650 % |
c |      5992 |   22742    53388 |    9227    5629   127152    22.6 | 11.783 % |
c |      6218 |   22651    53077 |   10150    5828   131895    22.6 | 12.840 % |
c |      6555 |   22336    51986 |   11165    6036   139183    23.1 | 16.843 % |
c |      7061 |   22040    50958 |   12281    6413   152522    23.8 | 21.148 % |
c |      7821 |   21992    50792 |   13509    7164   194127    27.1 | 21.828 % |
c |      8960 |   21858    50332 |   14860    8186   229756    28.1 | 23.641 % |
c |     10672 |   21663    49655 |   16347    9524   293315    30.8 | 25.914 % |
c |     13234 |   21645    49593 |   17981   12034   419905    34.9 | 26.067 % |
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 |     14302 |   21627    49532 |    7209   13098   462824    35.3 | 26.067 % |
c |     14403 |   21591    49402 |    7929    6643   221927    33.4 | 27.094 % |
c |     14553 |   21576    49351 |    8722    6786   225240    33.2 | 27.245 % |
c |     14779 |   21563    49304 |    9595    7009   232477    33.2 | 27.472 % |
c |     15116 |   21539    49218 |   10554    7337   243517    33.2 | 27.849 % |
c |     15622 |   21539    49218 |   11610    7843   268650    34.3 | 27.849 % |
c |     16382 |   21533    49198 |   12771    8592   291153    33.9 | 27.925 % |
c |     17521 |   21516    49139 |   14048    9706   381529    39.3 | 28.151 % |
c |     19229 |   21516    49139 |   15453   11414   463189    40.6 | 28.151 % |
c |     21791 |   21443    48894 |   16998   13956   558184    40.0 | 29.283 % |
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 |     24341 |   21352    48579 |    7117   16456   633129    38.5 | 29.283 % |
c |     24441 |   21325    48484 |    7828    4209    86075    20.5 | 31.379 % |
c |     24591 |   21325    48484 |    8611    4359    93456    21.4 | 31.379 % |
c |     24816 |   21325    48484 |    9472    4584   100465    21.9 | 31.373 % |
c |     25153 |   21325    48484 |   10419    4921   117557    23.9 | 31.373 % |
c |     25659 |   21325    48484 |   11461    5427   134400    24.8 | 31.379 % |
c |     26418 |   21316    48453 |   12608    6178   155861    25.2 | 31.448 % |
c |     27557 |   21316    48453 |   13869    7317   193996    26.5 | 31.454 % |
c |     29265 |   21224    48129 |   15255    8985   250338    27.9 | 32.963 % |
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 |     31394 |   21225    48134 |    7075   11114   361580    32.5 | 32.963 % |
c |     31494 |   21225    48134 |    7782    5657   179182    31.7 | 33.007 % |
c |     31644 |   21216    48101 |    8560    5806   181144    31.2 | 33.158 % |
c |     31869 |   21216    48101 |    9416    6031   192203    31.9 | 33.164 % |
c |     32208 |   21216    48101 |   10358    6370   202320    31.8 | 33.158 % |
c |     32714 |   21199    48042 |   11394    6860   219784    32.0 | 33.384 % |
c |     33473 |   21199    48042 |   12533    7619   236324    31.0 | 33.384 % |
c |     34612 |   21199    48042 |   13787    8758   271429    31.0 | 33.384 % |
c |     36323 |   21153    47880 |   15165   10450   346001    33.1 | 34.137 % |
c |     38885 |   21153    47880 |   16682   13012   443552    34.1 | 34.137 % |
c |     42729 |   21153    47880 |   18350   16856   588135    34.9 | 34.144 % |
c |     48496 |   21153    47880 |   20185   13049   425720    32.6 | 34.138 % |
c |     57145 |   21153    47880 |   22204   11270   339071    30.1 | 34.138 % |
c |     70120 |   21153    47880 |   24424   12769   347512    27.2 | 34.144 % |
c |     89581 |   21153    47880 |   26867   19652   498919    25.4 | 34.144 % |
c |    118773 |   21153    47880 |   29554   21202   689838    32.5 | 34.144 % |
c |    162563 |   21153    47880 |   32509   18928   611434    32.3 | 34.137 % |
c |    228247 |   21153    47880 |   35760   32604  1109003    34.0 | 34.137 % |
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 |    286799 |   21132    47809 |    7044   27626  1460911    52.9 | 34.137 % |
c |    286899 |   21132    47809 |    7748    7007   331431    47.3 | 34.639 % |
c |    287050 |   21132    47809 |    8523    7158   334651    46.8 | 34.639 % |
c |    287275 |   21132    47809 |    9375    7383   343142    46.5 | 34.639 % |
c |    287612 |   21132    47809 |   10313    7720   355190    46.0 | 34.639 % |
c |    288118 |   21132    47809 |   11344    8226   375878    45.7 | 34.646 % |
c |    288877 |   21132    47809 |   12478    8985   391380    43.6 | 34.639 % |
c |    290016 |   21132    47809 |   13726   10124   423511    41.8 | 34.639 % |
c |    291724 |   21132    47809 |   15099   11832   491205    41.5 | 34.643 % |
c |    294286 |   21132    47809 |   16609   14394   541555    37.6 | 34.639 % |
c |    298132 |   21132    47809 |   18270    9544   212391    22.3 | 34.639 % |
c |    303898 |   21132    47809 |   20097   15310   343080    22.4 | 34.643 % |
c |    312548 |   21132    47809 |   22107   13469   381543    28.3 | 34.643 % |
c |    325522 |   21132    47809 |   24317   14995   277350    18.5 | 34.639 % |
c |    344984 |   21132    47809 |   26749   21932   474071    21.6 | 34.643 % |
c |    374176 |   21132    47809 |   29424   23620   488497    20.7 | 34.645 % |
c |    417966 |   21132    47809 |   32366   22264   442673    19.9 | 34.643 % |
c |    483652 |   21132    47809 |   35603   18556   462328    24.9 | 34.644 % |
c |    582180 |   21132    47809 |   39164   19884   410528    20.6 | 34.643 % |
c |    729969 |   21132    47809 |   43080   20121   391208    19.4 | 34.643 % |
c |    951652 |   21132    47809 |   47388   37227   820170    22.0 | 34.639 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 25918
Raw data (stat): 25918 (runsolver) R 25917 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421435217 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+9.99993 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 1235 0 0 0 993 4 0 0 25 0 1 0 421435217 6635520 1213 4294967295 134512640 134672761 3221224560 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1620 1213 603 41 0 1579 0
vsize: 6480
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 1460 0 0 0 1992 5 0 0 25 0 1 0 421435217 7692288 1438 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1878 1438 603 41 0 1837 0
vsize: 7512
[startup+30.0013 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 1561 0 0 0 2992 5 0 0 25 0 1 0 421435217 8097792 1539 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1977 1539 603 41 0 1936 0
vsize: 7908
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 1648 0 0 0 3992 5 0 0 25 0 1 0 421435217 8368128 1626 4294967295 134512640 134672761 3221224560 3221223744 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2043 1626 603 41 0 2002 0
vsize: 8172
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 1685 0 0 0 4992 5 0 0 25 0 1 0 421435217 8507392 1663 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2077 1663 603 41 0 2036 0
vsize: 8308
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 1727 0 0 0 5992 6 0 0 25 0 1 0 421435217 8642560 1705 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2110 1705 603 41 0 2069 0
vsize: 8440
[startup+70.0016 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 1864 0 0 0 6992 6 0 0 25 0 1 0 421435217 9236480 1842 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2255 1842 603 41 0 2214 0
vsize: 9020
[startup+80.0015 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2007 0 0 0 7991 6 0 0 25 0 1 0 421435217 9912320 1985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2420 1985 603 41 0 2379 0
vsize: 9680
[startup+90.0011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2028 0 0 0 8991 7 0 0 25 0 1 0 421435217 10047488 2006 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2453 2006 603 41 0 2412 0
vsize: 9812
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2308 0 0 0 9990 8 0 0 25 0 1 0 421435217 11116544 2286 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2714 2286 603 41 0 2673 0
vsize: 10856
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2331 0 0 0 10990 8 0 0 25 0 1 0 421435217 11259904 2309 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2749 2309 603 41 0 2708 0
vsize: 10996
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2387 0 0 0 11990 8 0 0 25 0 1 0 421435217 11526144 2365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2365 603 41 0 2773 0
vsize: 11256
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2395 0 0 0 12991 8 0 0 25 0 1 0 421435217 11526144 2373 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2373 603 41 0 2773 0
vsize: 11256
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2403 0 0 0 13990 8 0 0 25 0 1 0 421435217 11526144 2381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2814 2381 603 41 0 2773 0
vsize: 11256
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2441 0 0 0 14990 9 0 0 25 0 1 0 421435217 11788288 2419 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2878 2419 603 41 0 2837 0
vsize: 11512
[startup+160.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2442 0 0 0 15990 9 0 0 25 0 1 0 421435217 11788288 2420 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2878 2420 603 41 0 2837 0
vsize: 11512
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2483 0 0 0 16990 9 0 0 25 0 1 0 421435217 12054528 2461 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2943 2461 603 41 0 2902 0
vsize: 11772
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2496 0 0 0 17990 9 0 0 25 0 1 0 421435217 12054528 2474 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2943 2474 603 41 0 2902 0
vsize: 11772
[startup+190 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2500 0 0 0 18991 9 0 0 25 0 1 0 421435217 12054528 2478 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2943 2478 603 41 0 2902 0
vsize: 11772
[startup+200 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2503 0 0 0 19991 9 0 0 25 0 1 0 421435217 12054528 2481 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2943 2481 603 41 0 2902 0
vsize: 11772
[startup+210 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2662 0 0 0 20990 9 0 0 25 0 1 0 421435217 12726272 2640 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3107 2640 603 41 0 3066 0
vsize: 12428
[startup+220 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 2662 0 0 0 21991 9 0 0 25 0 1 0 421435217 12726272 2640 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3107 2640 603 41 0 3066 0
vsize: 12428
[startup+230 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3054 0 0 0 22989 10 0 0 25 0 1 0 421435217 14352384 3032 4294967295 134512640 134672761 3221224560 3221223744 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3504 3032 603 41 0 3463 0
vsize: 14016
[startup+240 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3142 0 0 0 23989 11 0 0 25 0 1 0 421435217 14753792 3120 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3602 3120 603 41 0 3561 0
vsize: 14408
[startup+250 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3158 0 0 0 24990 11 0 0 25 0 1 0 421435217 14913536 3136 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3641 3136 603 41 0 3600 0
vsize: 14564
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3506 0 0 0 25989 11 0 0 25 0 1 0 421435217 16277504 3484 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3484 603 41 0 3933 0
vsize: 15896
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3512 0 0 0 26989 11 0 0 25 0 1 0 421435217 16277504 3490 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3490 603 41 0 3933 0
vsize: 15896
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3512 0 0 0 27989 11 0 0 25 0 1 0 421435217 16277504 3490 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3490 603 41 0 3933 0
vsize: 15896
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3512 0 0 0 28990 11 0 0 25 0 1 0 421435217 16277504 3490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3490 603 41 0 3933 0
vsize: 15896
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3512 0 0 0 29990 11 0 0 25 0 1 0 421435217 16277504 3490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3490 603 41 0 3933 0
vsize: 15896
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3512 0 0 0 30990 11 0 0 25 0 1 0 421435217 16277504 3490 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3490 603 41 0 3933 0
vsize: 15896
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3513 0 0 0 31990 11 0 0 25 0 1 0 421435217 16277504 3491 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3491 603 41 0 3933 0
vsize: 15896
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3513 0 0 0 32990 11 0 0 25 0 1 0 421435217 16277504 3491 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3491 603 41 0 3933 0
vsize: 15896
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3513 0 0 0 33990 11 0 0 25 0 1 0 421435217 16277504 3491 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3491 603 41 0 3933 0
vsize: 15896
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3514 0 0 0 34991 11 0 0 25 0 1 0 421435217 16277504 3492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3492 603 41 0 3933 0
vsize: 15896
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3514 0 0 0 35991 11 0 0 25 0 1 0 421435217 16277504 3492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3492 603 41 0 3933 0
vsize: 15896
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3514 0 0 0 36991 11 0 0 25 0 1 0 421435217 16277504 3492 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3492 603 41 0 3933 0
vsize: 15896
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3514 0 0 0 37991 12 0 0 25 0 1 0 421435217 16277504 3492 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3492 603 41 0 3933 0
vsize: 15896
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3514 0 0 0 38991 12 0 0 25 0 1 0 421435217 16277504 3492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3492 603 41 0 3933 0
vsize: 15896
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3514 0 0 0 39992 12 0 0 25 0 1 0 421435217 16277504 3492 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3492 603 41 0 3933 0
vsize: 15896
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3515 0 0 0 40992 12 0 0 25 0 1 0 421435217 16277504 3493 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3493 603 41 0 3933 0
vsize: 15896
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 41992 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 42992 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 43992 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 44992 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 45993 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 46993 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223232 134565856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 47993 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+490 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 48993 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+500 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 49993 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+510 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3518 0 0 0 50993 12 0 0 25 0 1 0 421435217 16277504 3496 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3496 603 41 0 3933 0
vsize: 15896
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3519 0 0 0 51994 12 0 0 25 0 1 0 421435217 16277504 3497 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3497 603 41 0 3933 0
vsize: 15896
[startup+530 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3519 0 0 0 52994 12 0 0 25 0 1 0 421435217 16277504 3497 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3497 603 41 0 3933 0
vsize: 15896
[startup+540 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3521 0 0 0 53994 12 0 0 25 0 1 0 421435217 16277504 3499 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3499 603 41 0 3933 0
vsize: 15896
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 54994 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 55995 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 56996 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 57996 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 58996 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 59996 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 60996 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 61997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 62997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 63997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 64997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 65997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 66997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223744 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 67997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223576 1075352644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3522 0 0 0 68997 12 0 0 25 0 1 0 421435217 16277504 3500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3500 603 41 0 3933 0
vsize: 15896
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3524 0 0 0 69998 12 0 0 25 0 1 0 421435217 16277504 3502 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3502 603 41 0 3933 0
vsize: 15896
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3529 0 0 0 70998 12 0 0 25 0 1 0 421435217 16277504 3507 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3507 603 41 0 3933 0
vsize: 15896
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3529 0 0 0 71998 12 0 0 25 0 1 0 421435217 16277504 3507 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3507 603 41 0 3933 0
vsize: 15896
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3529 0 0 0 72998 12 0 0 25 0 1 0 421435217 16277504 3507 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3507 603 41 0 3933 0
vsize: 15896
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3529 0 0 0 73998 12 0 0 25 0 1 0 421435217 16277504 3507 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3507 603 41 0 3933 0
vsize: 15896
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3529 0 0 0 74998 12 0 0 25 0 1 0 421435217 16277504 3507 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3507 603 41 0 3933 0
vsize: 15896
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 75999 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 76999 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 77999 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 78999 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 79999 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221221852 134566369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 80999 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 82000 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 83000 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 84000 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 85000 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 86000 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3530 0 0 0 87001 12 0 0 25 0 1 0 421435217 16277504 3508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3508 603 41 0 3933 0
vsize: 15896
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 88001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25918
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 89001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 25955
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 90001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+910.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25971
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 91001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25971
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 92001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25971
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 93001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+940.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25971
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 94001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223664 134559814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25971
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3531 0 0 0 95001 12 0 0 25 0 1 0 421435217 16277504 3509 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3509 603 41 0 3933 0
vsize: 15896
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25971
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3535 0 0 0 96001 12 0 0 25 0 1 0 421435217 16277504 3513 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3513 603 41 0 3933 0
vsize: 15896
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3535 0 0 0 97001 12 0 0 25 0 1 0 421435217 16277504 3513 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3513 603 41 0 3933 0
vsize: 15896
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3535 0 0 0 98002 12 0 0 25 0 1 0 421435217 16277504 3513 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3513 603 41 0 3933 0
vsize: 15896
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3535 0 0 0 99002 12 0 0 25 0 1 0 421435217 16277504 3513 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3513 603 41 0 3933 0
vsize: 15896
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3535 0 0 0 100002 12 0 0 25 0 1 0 421435217 16277504 3513 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3513 603 41 0 3933 0
vsize: 15896
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3647 0 0 0 101002 12 0 0 25 0 1 0 421435217 16822272 3625 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3625 603 41 0 4066 0
vsize: 16428
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3655 0 0 0 102002 12 0 0 25 0 1 0 421435217 16822272 3633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3633 603 41 0 4066 0
vsize: 16428
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3665 0 0 0 103002 12 0 0 25 0 1 0 421435217 16965632 3643 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3643 603 41 0 4101 0
vsize: 16568
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3668 0 0 0 104002 12 0 0 25 0 1 0 421435217 16965632 3646 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3646 603 41 0 4101 0
vsize: 16568
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3678 0 0 0 105003 12 0 0 25 0 1 0 421435217 16965632 3656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3656 603 41 0 4101 0
vsize: 16568
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 106003 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 107003 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 108003 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 109004 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 110004 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 111004 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 112004 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 113004 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 114004 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3683 0 0 0 115005 12 0 0 25 0 1 0 421435217 16965632 3661 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4142 3661 603 41 0 4101 0
vsize: 16568
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3692 0 0 0 116005 12 0 0 25 0 1 0 421435217 17113088 3670 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3670 603 41 0 4137 0
vsize: 16712
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3703 0 0 0 117005 12 0 0 25 0 1 0 421435217 17113088 3681 4294967295 134512640 134672761 3221224560 3221223696 134565054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3681 603 41 0 4137 0
vsize: 16712
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3703 0 0 0 118005 12 0 0 25 0 1 0 421435217 17113088 3681 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3681 603 41 0 4137 0
vsize: 16712
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3703 0 0 0 119006 12 0 0 25 0 1 0 421435217 17113088 3681 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3681 603 41 0 4137 0
vsize: 16712
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25973
Raw data (stat): 25918 (minisat+) R 25917 22932 22931 0 -1 0 3703 0 0 0 120006 12 0 0 25 0 1 0 421435217 17113088 3681 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3681 603 41 0 4137 0
vsize: 16712
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25973
Raw data (stat): 25918 (minisat+) Z 25917 22932 22931 0 -1 12 3706 0 0 0 120006 13 0 0 25 0 1 0 421435217 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.2
CPU user time (s): 1200.06
CPU system time (s): 0.133979
CPU usage (%): 100.014
Max. virtual memory (Kb): 16712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####