PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-1.opb
MD5SUM	16a8eb66aae2bcfd534a482dd0a3948e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	27856
Number of constraints which are clauses	27856
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 5987

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-14 02:44:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4455 boxname=wulflinc26 idbench=319 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  16a8eb66aae2bcfd534a482dd0a3948e  /oldhome/oroussel/tmp/wulflinc26/normalized-frb35-17-1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-frb35-17-1.opb /oldhome/oroussel/tmp/wulflinc26/normalized-frb35-17-1.opb
IDLAUNCH: 4455
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        826840 kB
Buffers:         35496 kB
Cached:         131824 kB
SwapCached:       2476 kB
Active:          56500 kB
Inactive:       116164 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        826560 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29552 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:04:45 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 4455 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27856 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 |   27856    55712 |    9285       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56151   122167 |   18717       0        0     nan |  0.000 % |
c |       100 |   55641   121103 |   20588      80     1297    16.2 |  1.436 % |
c |       250 |   54951   119605 |   22647     189     2268    12.0 |  3.524 % |
c |       476 |   54022   117586 |   24912     364     4235    11.6 |  6.330 % |
c |       813 |   52202   113569 |   27403     615     7046    11.5 | 11.983 % |
c |      1319 |   50454   109647 |   30143    1040    11817    11.4 | 17.600 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1402 |   50068   108787 |   16689    1107    12820    11.6 | 17.600 % |
c |      1502 |   49454   107371 |   18357    1174    13840    11.8 | 21.069 % |
c |      1652 |   48818   105945 |   20193    1300    15532    11.9 | 22.940 % |
c |      1877 |   48058   104211 |   22213    1452    17303    11.9 | 25.446 % |
c |      2214 |   47050   101919 |   24434    1732    20313    11.7 | 28.742 % |
c |      2720 |   45617    98616 |   26877    2151    25789    12.0 | 33.547 % |
c |      3479 |   43899    94657 |   29565    2788    35155    12.6 | 39.272 % |
c |      4618 |   40020    85547 |   32522    3583    49056    13.7 | 52.286 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4643 |   40055    85703 |   13351    3591    49288    13.7 | 52.286 % |
c |      4745 |   39723    84935 |   14686    3575    49232    13.8 | 53.493 % |
c |      4895 |   39621    84699 |   16154    3698    51856    14.0 | 53.838 % |
c |      5120 |   39179    83659 |   17770    3874    56863    14.7 | 55.355 % |
c |      5457 |   37944    80743 |   19547    4038    60606    15.0 | 59.650 % |
c |      5963 |   37234    79072 |   21501    4463    73988    16.6 | 62.099 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6315 |   37042    78587 |   12347    4760    82824    17.4 | 62.099 % |
c |      6415 |   36898    78246 |   13581    4847    84510    17.4 | 63.317 % |
c |      6566 |   36429    77135 |   14939    4926    88695    18.0 | 64.927 % |
c |      6791 |   36313    76855 |   16433    5126    95703    18.7 | 65.343 % |
c |      7128 |   35730    75480 |   18077    5353   100982    18.9 | 67.308 % |
c |      7634 |   35222    74253 |   19884    5765   125403    21.8 | 69.093 % |
c |      8393 |   34627    72820 |   21873    6399   144024    22.5 | 71.186 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9306 |   34209    71811 |   11403    7189   178763    24.9 | 71.186 % |
c |      9407 |   34209    71811 |   12543    7290   180868    24.8 | 72.783 % |
c |      9557 |   34129    71619 |   13797    7379   182136    24.7 | 73.065 % |
c |      9783 |   34089    71525 |   15177    7572   191361    25.3 | 73.204 % |
c |     10120 |   34089    71525 |   16695    7909   209404    26.5 | 73.204 % |
c |     10626 |   34043    71415 |   18364    8361   232830    27.8 | 73.363 % |
c |     11385 |   33962    71214 |   20201    9085   269116    29.6 | 73.666 % |
c |     12525 |   33255    69528 |   22221    9902   298057    30.1 | 76.137 % |
c |     14233 |   32889    68642 |   24443   11283   385731    34.2 | 77.457 % |
c |     16795 |   32768    68345 |   26887   13632   659300    48.4 | 77.888 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17157 |   32647    68009 |   10882   13954   681985    48.9 | 77.888 % |
c |     17258 |   32641    67993 |   11970   14049   684582    48.7 | 78.347 % |
c |     17408 |   32641    67993 |   13167   14199   690091    48.6 | 78.347 % |
c |     17634 |   32588    67867 |   14483   14349   701963    48.9 | 78.532 % |
c |     17971 |   32555    67786 |   15932   14650   714775    48.8 | 78.655 % |
c |     18477 |   32411    67425 |   17525   15034   729230    48.5 | 79.195 % |
c |     19237 |   32367    67321 |   19278   15759   758129    48.1 | 79.349 % |
c |     20376 |   32301    67168 |   21205   16840   848616    50.4 | 79.544 % |
c |     22085 |   32218    66973 |   23326   18501   944250    51.0 | 79.832 % |
c |     24647 |   32151    66816 |   25659   21011  1154613    55.0 | 80.063 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27056 |   32115    66734 |   10705   23335  1321535    56.6 | 80.063 % |
c |     27157 |   32113    66730 |   11775   23435  1326791    56.6 | 80.316 % |
c |     27308 |   32113    66730 |   12953   23586  1331776    56.5 | 80.316 % |
c |     27533 |   32071    66627 |   14248   23711  1346197    56.8 | 80.470 % |
c |     27871 |   32034    66544 |   15673   23983  1360153    56.7 | 80.587 % |
c |     28377 |   31959    66360 |   17240   24473  1380446    56.4 | 80.868 % |
c |     29136 |   31866    66137 |   18964   25210  1423417    56.5 | 81.191 % |
c |     30275 |   31832    66053 |   20861   26274  1496718    57.0 | 81.313 % |
c |     31983 |   31832    66053 |   22947   27982  1622123    58.0 | 81.313 % |
c |     34545 |   31805    65984 |   25241   30493  1805024    59.2 | 81.416 % |
c |     38389 |   31766    65891 |   27766   34166  2010912    58.9 | 81.554 % |
c |     44157 |   31719    65774 |   30542   39804  2430835    61.1 | 81.733 % |
c |     52806 |   31615    65520 |   33596   18059   877920    48.6 | 82.106 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62973 |   31532    65307 |   10510   28208  1448576    51.4 | 82.106 % |
c |     63076 |   31532    65307 |   11561   14207   578195    40.7 | 82.410 % |
c |     63226 |   31532    65307 |   12717   14357   585145    40.8 | 82.410 % |
c |     63451 |   31532    65307 |   13988   14582   598581    41.0 | 82.410 % |
c |     63788 |   31532    65307 |   15387   14919   620951    41.6 | 82.410 % |
c |     64294 |   31532    65307 |   16926   15425   653206    42.3 | 82.410 % |
c |     65053 |   31464    65147 |   18619   16165   701648    43.4 | 82.634 % |
c |     66192 |   31419    65036 |   20481   17286   776803    44.9 | 82.803 % |
c |     67901 |   31419    65036 |   22529   18995   879887    46.3 | 82.803 % |
c |     70463 |   31402    64997 |   24782   21553   994708    46.2 | 82.860 % |
c |     74308 |   31402    64997 |   27260   25398  1201104    47.3 | 82.859 % |
c |     80074 |   31402    64997 |   29986   31164  1386011    44.5 | 82.860 % |
c |     88723 |   31378    64935 |   32984   39808  1664419    41.8 | 82.957 % |
c |    101698 |   31329    64818 |   36283   20738   615428    29.7 | 83.131 % |
c |    121159 |   31329    64818 |   39911   40199  1368273    34.0 | 83.131 % |
c |    150352 |   31266    64657 |   43902   30887   952875    30.9 | 83.376 % |
c |    194141 |   31229    64565 |   48293   31138  1004370    32.3 | 83.514 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217392 |   31241    64598 |   10413   54386  1860959    34.2 | 83.514 % |
c |    217494 |   31241    64598 |   11454   17566   456371    26.0 | 83.495 % |
c |    217644 |   31241    64598 |   12599   17716   463136    26.1 | 83.495 % |
c |    217869 |   31241    64598 |   13859   17941   471453    26.3 | 83.495 % |
c |    218206 |   31241    64598 |   15245   18278   487008    26.6 | 83.495 % |
c |    218712 |   31241    64598 |   16770   18784   502493    26.8 | 83.495 % |
c |    219471 |   31241    64598 |   18447   19543   525927    26.9 | 83.495 % |
c |    220610 |   31241    64598 |   20291   20682   558029    27.0 | 83.495 % |
c |    222318 |   31241    64598 |   22321   22390   603953    27.0 | 83.495 % |
c |    224880 |   31241    64598 |   24553   24952   673524    27.0 | 83.495 % |
c |    228724 |   31227    64566 |   27008   28790   773486    26.9 | 83.541 % |
c |    234490 |   31207    64514 |   29709   34403   940104    27.3 | 83.623 % |
c |    243140 |   31207    64514 |   32680   43053  1183495    27.5 | 83.623 % |
c |    256114 |   31207    64514 |   35948   24367   575570    23.6 | 83.623 % |
c |    275576 |   31168    64425 |   39543   43805  1874953    42.8 | 83.750 % |
c |    304768 |   31161    64408 |   43497   33136  1335594    40.3 | 83.776 % |
c |    348558 |   31153    64388 |   47847   36328   955951    26.3 | 83.807 % |
c |    414243 |   31122    64317 |   52632   58263  1623043    27.9 | 83.904 % |
c |    512769 |   31083    64216 |   57895   59889  2165270    36.2 | 84.047 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    614887 |   31011    64017 |   10337   52804  1656316    31.4 | 84.047 % |
c |    614988 |   31011    64017 |   11370   21171   575638    27.2 | 84.304 % |
c |    615139 |   31011    64017 |   12507   21322   578882    27.1 | 84.304 % |
c |    615365 |   31011    64017 |   13758   21548   583379    27.1 | 84.304 % |
c |    615703 |   31011    64017 |   15134   21886   590624    27.0 | 84.304 % |
c |    616209 |   31011    64017 |   16647   22392   603214    26.9 | 84.304 % |
c |    616969 |   31011    64017 |   18312   23152   624588    27.0 | 84.304 % |
c |    618110 |   31011    64017 |   20143   24293   653811    26.9 | 84.304 % |
c |    619819 |   31011    64017 |   22158   26002   714382    27.5 | 84.304 % |
c |    622381 |   30983    63957 |   24374   28562   777468    27.2 | 84.385 % |
c |    626226 |   30983    63957 |   26811   32407   890463    27.5 | 84.385 % |
#### 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.94 0.90 2/54 30347
Raw data (stat): 30347 (runsolver) R 30346 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481094746 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 2266 0 0 0 993 5 0 0 25 0 1 0 481094746 11476992 2237 4294967295 134512640 134672761 3221224560 3221223756 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2802 2237 603 41 0 2761 0
vsize: 11208
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 2358 0 0 0 1992 6 0 0 25 0 1 0 481094746 11874304 2329 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2899 2329 603 41 0 2858 0
vsize: 11596
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 2923 0 0 0 2990 8 0 0 25 0 1 0 481094746 14299136 2894 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3491 2894 603 41 0 3450 0
vsize: 13964
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 3461 0 0 0 3989 9 0 0 25 0 1 0 481094746 16502784 3432 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4029 3432 603 41 0 3988 0
vsize: 16116
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 3940 0 0 0 4987 12 0 0 25 0 1 0 481094746 18374656 3911 4294967295 134512640 134672761 3221224560 3221223744 134558403 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4486 3911 603 41 0 4445 0
vsize: 17944
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 4382 0 0 0 5986 13 0 0 25 0 1 0 481094746 20234240 4353 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4353 603 41 0 4899 0
vsize: 19760
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 4775 0 0 0 6985 14 0 0 25 0 1 0 481094746 21975040 4746 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4746 603 41 0 5324 0
vsize: 21460
[startup+80.0034 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5178 0 0 0 7984 15 0 0 25 0 1 0 481094746 23564288 5149 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5753 5149 603 41 0 5712 0
vsize: 23012
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5494 0 0 0 8982 17 0 0 25 0 1 0 481094746 24895488 5465 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6078 5465 603 41 0 6037 0
vsize: 24312
[startup+100.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5620 0 0 0 9981 18 0 0 25 0 1 0 481094746 25292800 5591 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6175 5591 603 41 0 6134 0
vsize: 24700
[startup+110.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5620 0 0 0 10981 18 0 0 25 0 1 0 481094746 25292800 5591 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6175 5591 603 41 0 6134 0
vsize: 24700
[startup+120.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5640 0 0 0 11980 19 0 0 25 0 1 0 481094746 25452544 5611 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5611 603 41 0 6173 0
vsize: 24856
[startup+130.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5640 0 0 0 12980 20 0 0 25 0 1 0 481094746 25452544 5611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5611 603 41 0 6173 0
vsize: 24856
[startup+140.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5640 0 0 0 13980 20 0 0 25 0 1 0 481094746 25452544 5611 4294967295 134512640 134672761 3221224560 3221223744 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5611 603 41 0 6173 0
vsize: 24856
[startup+150.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5640 0 0 0 14980 20 0 0 25 0 1 0 481094746 25452544 5611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5611 603 41 0 6173 0
vsize: 24856
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5640 0 0 0 15979 21 0 0 25 0 1 0 481094746 25452544 5611 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5611 603 41 0 6173 0
vsize: 24856
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5640 0 0 0 16979 21 0 0 25 0 1 0 481094746 25452544 5611 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5611 603 41 0 6173 0
vsize: 24856
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5641 0 0 0 17979 21 0 0 25 0 1 0 481094746 25452544 5612 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5612 603 41 0 6173 0
vsize: 24856
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5641 0 0 0 18979 21 0 0 25 0 1 0 481094746 25452544 5612 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5612 603 41 0 6173 0
vsize: 24856
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5641 0 0 0 19979 21 0 0 25 0 1 0 481094746 25452544 5612 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5612 603 41 0 6173 0
vsize: 24856
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5641 0 0 0 20979 22 0 0 25 0 1 0 481094746 25452544 5612 4294967295 134512640 134672761 3221224560 3221223664 134559905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5612 603 41 0 6173 0
vsize: 24856
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5641 0 0 0 21979 22 0 0 25 0 1 0 481094746 25452544 5612 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5612 603 41 0 6173 0
vsize: 24856
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5641 0 0 0 22979 22 0 0 25 0 1 0 481094746 25452544 5612 4294967295 134512640 134672761 3221224560 3221223712 134541802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5612 603 41 0 6173 0
vsize: 24856
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5642 0 0 0 23979 23 0 0 25 0 1 0 481094746 25452544 5613 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5613 603 41 0 6173 0
vsize: 24856
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5647 0 0 0 24978 23 0 0 25 0 1 0 481094746 25452544 5618 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5618 603 41 0 6173 0
vsize: 24856
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5648 0 0 0 25978 24 0 0 25 0 1 0 481094746 25452544 5619 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5619 603 41 0 6173 0
vsize: 24856
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5648 0 0 0 26978 24 0 0 25 0 1 0 481094746 25452544 5619 4294967295 134512640 134672761 3221224560 3221223744 134558941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5619 603 41 0 6173 0
vsize: 24856
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5648 0 0 0 27978 24 0 0 25 0 1 0 481094746 25452544 5619 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5619 603 41 0 6173 0
vsize: 24856
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5648 0 0 0 28978 25 0 0 25 0 1 0 481094746 25452544 5619 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6214 5619 603 41 0 6173 0
vsize: 24856
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5648 0 0 0 29978 25 0 0 25 0 1 0 481094746 25452544 5619 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6214 5619 603 41 0 6173 0
vsize: 24856
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5648 0 0 0 30978 25 0 0 25 0 1 0 481094746 25452544 5619 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6214 5619 603 41 0 6173 0
vsize: 24856
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5671 0 0 0 31978 25 0 0 25 0 1 0 481094746 25624576 5642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6256 5642 603 41 0 6215 0
vsize: 25024
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5674 0 0 0 32978 25 0 0 25 0 1 0 481094746 25624576 5645 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6256 5645 603 41 0 6215 0
vsize: 25024
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 33978 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 34978 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 35979 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 36979 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 37979 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 38979 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 39979 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 40979 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 41980 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 42980 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 43980 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 44980 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 45980 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 46980 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5688 0 0 0 47980 25 0 0 25 0 1 0 481094746 25821184 5659 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5659 603 41 0 6263 0
vsize: 25216
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5697 0 0 0 48980 25 0 0 25 0 1 0 481094746 25821184 5668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5668 603 41 0 6263 0
vsize: 25216
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5698 0 0 0 49981 25 0 0 25 0 1 0 481094746 25821184 5669 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5669 603 41 0 6263 0
vsize: 25216
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5699 0 0 0 50981 25 0 0 25 0 1 0 481094746 25821184 5670 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6304 5670 603 41 0 6263 0
vsize: 25216
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5725 0 0 0 51981 26 0 0 25 0 1 0 481094746 25952256 5696 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6336 5696 603 41 0 6295 0
vsize: 25344
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5781 0 0 0 52980 26 0 0 25 0 1 0 481094746 26218496 5752 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6401 5752 603 41 0 6360 0
vsize: 25604
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5785 0 0 0 53981 26 0 0 25 0 1 0 481094746 26218496 5756 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6401 5756 603 41 0 6360 0
vsize: 25604
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5785 0 0 0 54980 26 0 0 25 0 1 0 481094746 26218496 5756 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6401 5756 603 41 0 6360 0
vsize: 25604
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5792 0 0 0 55980 26 0 0 25 0 1 0 481094746 26218496 5763 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6401 5763 603 41 0 6360 0
vsize: 25604
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5802 0 0 0 56981 26 0 0 25 0 1 0 481094746 26218496 5773 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6401 5773 603 41 0 6360 0
vsize: 25604
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5803 0 0 0 57981 26 0 0 25 0 1 0 481094746 26218496 5774 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6401 5774 603 41 0 6360 0
vsize: 25604
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5816 0 0 0 58981 26 0 0 25 0 1 0 481094746 26353664 5787 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6434 5787 603 41 0 6393 0
vsize: 25736
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5830 0 0 0 59981 26 0 0 25 0 1 0 481094746 26353664 5801 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6434 5801 603 41 0 6393 0
vsize: 25736
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5841 0 0 0 60981 26 0 0 25 0 1 0 481094746 26517504 5812 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5812 603 41 0 6433 0
vsize: 25896
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5841 0 0 0 61981 26 0 0 25 0 1 0 481094746 26517504 5812 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5812 603 41 0 6433 0
vsize: 25896
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5846 0 0 0 62982 26 0 0 25 0 1 0 481094746 26517504 5817 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5817 603 41 0 6433 0
vsize: 25896
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5846 0 0 0 63982 26 0 0 25 0 1 0 481094746 26517504 5817 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5817 603 41 0 6433 0
vsize: 25896
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5846 0 0 0 64982 26 0 0 25 0 1 0 481094746 26517504 5817 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5817 603 41 0 6433 0
vsize: 25896
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5847 0 0 0 65982 26 0 0 25 0 1 0 481094746 26517504 5818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5818 603 41 0 6433 0
vsize: 25896
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5855 0 0 0 66982 26 0 0 25 0 1 0 481094746 26517504 5826 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5826 603 41 0 6433 0
vsize: 25896
[startup+680.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5858 0 0 0 67982 27 0 0 25 0 1 0 481094746 26517504 5829 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6474 5829 603 41 0 6433 0
vsize: 25896
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5883 0 0 0 68983 27 0 0 25 0 1 0 481094746 26714112 5854 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6522 5854 603 41 0 6481 0
vsize: 26088
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5890 0 0 0 69983 27 0 0 25 0 1 0 481094746 26714112 5861 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6522 5861 603 41 0 6481 0
vsize: 26088
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5890 0 0 0 70983 27 0 0 25 0 1 0 481094746 26714112 5861 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6522 5861 603 41 0 6481 0
vsize: 26088
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5895 0 0 0 71983 27 0 0 25 0 1 0 481094746 26714112 5866 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6522 5866 603 41 0 6481 0
vsize: 26088
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5896 0 0 0 72983 27 0 0 25 0 1 0 481094746 26714112 5867 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6522 5867 603 41 0 6481 0
vsize: 26088
[startup+740.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5912 0 0 0 73983 27 0 0 25 0 1 0 481094746 26861568 5883 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6558 5883 603 41 0 6517 0
vsize: 26232
[startup+750.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5916 0 0 0 74983 27 0 0 25 0 1 0 481094746 26861568 5887 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6558 5887 603 41 0 6517 0
vsize: 26232
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5917 0 0 0 75983 27 0 0 25 0 1 0 481094746 26861568 5888 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6558 5888 603 41 0 6517 0
vsize: 26232
[startup+770.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5924 0 0 0 76983 27 0 0 25 0 1 0 481094746 26861568 5895 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6558 5895 603 41 0 6517 0
vsize: 26232
[startup+780.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5925 0 0 0 77983 27 0 0 25 0 1 0 481094746 26861568 5896 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6558 5896 603 41 0 6517 0
vsize: 26232
[startup+790.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5952 0 0 0 78983 27 0 0 25 0 1 0 481094746 27287552 5923 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5923 603 41 0 6621 0
vsize: 26648
[startup+800.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5953 0 0 0 79983 27 0 0 25 0 1 0 481094746 27287552 5924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5924 603 41 0 6621 0
vsize: 26648
[startup+810.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5953 0 0 0 80983 27 0 0 25 0 1 0 481094746 27287552 5924 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5924 603 41 0 6621 0
vsize: 26648
[startup+820.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5953 0 0 0 81983 28 0 0 25 0 1 0 481094746 27287552 5924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5924 603 41 0 6621 0
vsize: 26648
[startup+830.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5953 0 0 0 82983 28 0 0 25 0 1 0 481094746 27287552 5924 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5924 603 41 0 6621 0
vsize: 26648
[startup+840.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5953 0 0 0 83984 28 0 0 25 0 1 0 481094746 27287552 5924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5924 603 41 0 6621 0
vsize: 26648
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5962 0 0 0 84984 28 0 0 25 0 1 0 481094746 27287552 5933 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5933 603 41 0 6621 0
vsize: 26648
[startup+860.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5963 0 0 0 85984 28 0 0 25 0 1 0 481094746 27287552 5934 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5934 603 41 0 6621 0
vsize: 26648
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 86984 28 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+880.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 87984 28 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+890.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 88984 28 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 89984 28 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 90984 28 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30347
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 91984 28 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+930.003 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 30400
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 92984 29 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+940.003 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 30400
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 93985 29 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+950.004 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 30400
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 94985 29 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+960.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30400
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 95985 29 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+970.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30400
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 5964 0 0 0 96984 29 0 0 25 0 1 0 481094746 27287552 5935 4294967295 134512640 134672761 3221224560 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 5935 603 41 0 6621 0
vsize: 26648
[startup+980.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30400
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6070 0 0 0 97984 29 0 0 25 0 1 0 481094746 27680768 6041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6758 6041 603 41 0 6717 0
vsize: 27032
[startup+990.002 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6235 0 0 0 98984 30 0 0 25 0 1 0 481094746 28344320 6206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6920 6206 603 41 0 6879 0
vsize: 27680
[startup+1000 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6367 0 0 0 99984 30 0 0 25 0 1 0 481094746 28868608 6338 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7048 6338 603 41 0 7007 0
vsize: 28192
[startup+1010 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6371 0 0 0 100984 30 0 0 25 0 1 0 481094746 28999680 6342 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6342 603 41 0 7039 0
vsize: 28320
[startup+1020 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6371 0 0 0 101984 30 0 0 25 0 1 0 481094746 28999680 6342 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6342 603 41 0 7039 0
vsize: 28320
[startup+1030 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6371 0 0 0 102984 30 0 0 25 0 1 0 481094746 28999680 6342 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6342 603 41 0 7039 0
vsize: 28320
[startup+1040 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6371 0 0 0 103984 30 0 0 25 0 1 0 481094746 28999680 6342 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6342 603 41 0 7039 0
vsize: 28320
[startup+1050 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6371 0 0 0 104984 30 0 0 25 0 1 0 481094746 28999680 6342 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6342 603 41 0 7039 0
vsize: 28320
[startup+1060 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6382 0 0 0 105984 30 0 0 25 0 1 0 481094746 28999680 6353 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6353 603 41 0 7039 0
vsize: 28320
[startup+1070 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6382 0 0 0 106984 31 0 0 25 0 1 0 481094746 28999680 6353 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6353 603 41 0 7039 0
vsize: 28320
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6384 0 0 0 107985 31 0 0 25 0 1 0 481094746 28999680 6355 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6355 603 41 0 7039 0
vsize: 28320
[startup+1090 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6384 0 0 0 108985 31 0 0 25 0 1 0 481094746 28999680 6355 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7080 6355 603 41 0 7039 0
vsize: 28320
[startup+1100 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6397 0 0 0 109985 31 0 0 25 0 1 0 481094746 29147136 6368 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7116 6368 603 41 0 7075 0
vsize: 28464
[startup+1110 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6526 0 0 0 110985 31 0 0 25 0 1 0 481094746 29548544 6497 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7214 6497 603 41 0 7173 0
vsize: 28856
[startup+1120 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6640 0 0 0 111985 31 0 0 25 0 1 0 481094746 30076928 6611 4294967295 134512640 134672761 3221224560 3221223696 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7343 6611 603 41 0 7302 0
vsize: 29372
[startup+1130 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6640 0 0 0 112985 31 0 0 25 0 1 0 481094746 30076928 6611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7343 6611 603 41 0 7302 0
vsize: 29372
[startup+1140 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6645 0 0 0 113985 31 0 0 25 0 1 0 481094746 30076928 6616 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7343 6616 603 41 0 7302 0
vsize: 29372
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6652 0 0 0 114985 31 0 0 25 0 1 0 481094746 30076928 6623 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7343 6623 603 41 0 7302 0
vsize: 29372
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6653 0 0 0 115985 31 0 0 25 0 1 0 481094746 30076928 6624 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7343 6624 603 41 0 7302 0
vsize: 29372
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6653 0 0 0 116985 31 0 0 25 0 1 0 481094746 30076928 6624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7343 6624 603 41 0 7302 0
vsize: 29372
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6653 0 0 0 117985 32 0 0 25 0 1 0 481094746 30076928 6624 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7343 6624 603 41 0 7302 0
vsize: 29372
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6653 0 0 0 118985 32 0 0 25 0 1 0 481094746 30076928 6624 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7343 6624 603 41 0 7302 0
vsize: 29372
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30402
Raw data (stat): 30347 (minisat+) R 30346 22612 22611 0 -1 0 6653 0 0 0 119984 32 0 0 25 0 1 0 481094746 30076928 6624 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7343 6624 603 41 0 7302 0
vsize: 29372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 30402
Raw data (stat): 30347 (minisat+) Z 30346 22612 22611 0 -1 12 6656 0 0 0 119984 33 0 0 25 0 1 0 481094746 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.02
CPU time (s): 1200.18
CPU user time (s): 1199.85
CPU system time (s): 0.334949
CPU usage (%): 100.014
Max. virtual memory (Kb): 29372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####