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 5025

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        916476 kB
Buffers:         34528 kB
Cached:          61700 kB
SwapCached:       2644 kB
Active:          51272 kB
Inactive:        50512 kB
HighTotal:      131008 kB
HighFree:        65380 kB
LowTotal:       903652 kB
LowFree:        851096 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10976 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:47:10 (client local time) WITH STATUS 10 IN 1200.4 SECONDS
stats: 2867 7 1200.4 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.90 0.94 0.90 2/54 32183
Raw data (stat): 32183 (runsolver) R 32182 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420962434 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0003 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 2305 0 0 0 991 6 0 0 25 0 1 0 420962434 11665408 2276 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2848 2276 603 41 0 2807 0
vsize: 11392
[startup+20.0011 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 2387 0 0 0 1991 7 0 0 25 0 1 0 420962434 11935744 2358 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2914 2358 603 41 0 2873 0
vsize: 11656
[startup+30.0016 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 2952 0 0 0 2989 9 0 0 25 0 1 0 420962434 14319616 2923 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 2923 603 41 0 3455 0
vsize: 13984
[startup+40.0017 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 3502 0 0 0 3986 11 0 0 25 0 1 0 420962434 16580608 3473 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4048 3473 603 41 0 4007 0
vsize: 16192
[startup+50.0025 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 3981 0 0 0 4986 12 0 0 25 0 1 0 420962434 18468864 3952 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4509 3952 603 41 0 4468 0
vsize: 18036
[startup+60.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 4431 0 0 0 5984 14 0 0 25 0 1 0 420962434 20332544 4402 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4964 4402 603 41 0 4923 0
vsize: 19856
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 4828 0 0 0 6983 15 0 0 25 0 1 0 420962434 22069248 4799 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5388 4799 603 41 0 5347 0
vsize: 21552
[startup+80.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5240 0 0 0 7983 17 0 0 25 0 1 0 420962434 23793664 5211 4294967295 134512640 134672761 3221224640 3221223776 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5809 5211 603 41 0 5768 0
vsize: 23236
[startup+90.0054 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5560 0 0 0 8982 17 0 0 25 0 1 0 420962434 24997888 5531 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6103 5531 603 41 0 6062 0
vsize: 24412
[startup+100.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5653 0 0 0 9982 17 0 0 25 0 1 0 420962434 25403392 5624 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6202 5624 603 41 0 6161 0
vsize: 24808
[startup+110.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5653 0 0 0 10983 17 0 0 25 0 1 0 420962434 25403392 5624 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6202 5624 603 41 0 6161 0
vsize: 24808
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5673 0 0 0 11983 18 0 0 25 0 1 0 420962434 25563136 5644 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5644 603 41 0 6200 0
vsize: 24964
[startup+130.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5673 0 0 0 12983 18 0 0 25 0 1 0 420962434 25563136 5644 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5644 603 41 0 6200 0
vsize: 24964
[startup+140.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5673 0 0 0 13984 18 0 0 25 0 1 0 420962434 25563136 5644 4294967295 134512640 134672761 3221224640 3221223812 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5644 603 41 0 6200 0
vsize: 24964
[startup+150.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5673 0 0 0 14984 18 0 0 25 0 1 0 420962434 25563136 5644 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5644 603 41 0 6200 0
vsize: 24964
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5673 0 0 0 15984 18 0 0 25 0 1 0 420962434 25563136 5644 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5644 603 41 0 6200 0
vsize: 24964
[startup+170.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5673 0 0 0 16985 18 0 0 25 0 1 0 420962434 25563136 5644 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5644 603 41 0 6200 0
vsize: 24964
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5674 0 0 0 17985 18 0 0 25 0 1 0 420962434 25563136 5645 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5645 603 41 0 6200 0
vsize: 24964
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5674 0 0 0 18985 18 0 0 25 0 1 0 420962434 25563136 5645 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5645 603 41 0 6200 0
vsize: 24964
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5674 0 0 0 19986 18 0 0 25 0 1 0 420962434 25563136 5645 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5645 603 41 0 6200 0
vsize: 24964
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5674 0 0 0 20986 18 0 0 25 0 1 0 420962434 25563136 5645 4294967295 134512640 134672761 3221224640 3221223744 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5645 603 41 0 6200 0
vsize: 24964
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5674 0 0 0 21986 18 0 0 25 0 1 0 420962434 25563136 5645 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5645 603 41 0 6200 0
vsize: 24964
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5674 0 0 0 22987 18 0 0 25 0 1 0 420962434 25563136 5645 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5645 603 41 0 6200 0
vsize: 24964
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5676 0 0 0 23987 18 0 0 25 0 1 0 420962434 25563136 5647 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5647 603 41 0 6200 0
vsize: 24964
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5681 0 0 0 24988 18 0 0 25 0 1 0 420962434 25563136 5652 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5652 603 41 0 6200 0
vsize: 24964
[startup+260.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5681 0 0 0 25988 18 0 0 25 0 1 0 420962434 25563136 5652 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5652 603 41 0 6200 0
vsize: 24964
[startup+270.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5681 0 0 0 26988 18 0 0 25 0 1 0 420962434 25563136 5652 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5652 603 41 0 6200 0
vsize: 24964
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5681 0 0 0 27989 18 0 0 25 0 1 0 420962434 25563136 5652 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5652 603 41 0 6200 0
vsize: 24964
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5681 0 0 0 28989 18 0 0 25 0 1 0 420962434 25563136 5652 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5652 603 41 0 6200 0
vsize: 24964
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5681 0 0 0 29989 18 0 0 25 0 1 0 420962434 25563136 5652 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5652 603 41 0 6200 0
vsize: 24964
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5681 0 0 0 30990 18 0 0 25 0 1 0 420962434 25563136 5652 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5652 603 41 0 6200 0
vsize: 24964
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5696 0 0 0 31990 18 0 0 25 0 1 0 420962434 25710592 5667 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5667 603 41 0 6236 0
vsize: 25108
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5708 0 0 0 32990 18 0 0 25 0 1 0 420962434 25710592 5679 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5679 603 41 0 6236 0
vsize: 25108
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 33991 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 34991 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 35991 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 36992 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 37992 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 38992 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 39993 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 40993 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 41993 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 42994 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 43994 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 44994 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 45995 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5711 0 0 0 46995 18 0 0 25 0 1 0 420962434 25710592 5682 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5682 603 41 0 6236 0
vsize: 25108
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5720 0 0 0 47996 18 0 0 25 0 1 0 420962434 25907200 5691 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6325 5691 603 41 0 6284 0
vsize: 25300
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5721 0 0 0 48996 18 0 0 25 0 1 0 420962434 25907200 5692 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6325 5692 603 41 0 6284 0
vsize: 25300
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5722 0 0 0 49996 18 0 0 25 0 1 0 420962434 25907200 5693 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6325 5693 603 41 0 6284 0
vsize: 25300
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5722 0 0 0 50997 18 0 0 25 0 1 0 420962434 25907200 5693 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6325 5693 603 41 0 6284 0
vsize: 25300
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5821 0 0 0 51996 19 0 0 25 0 1 0 420962434 26308608 5792 4294967295 134512640 134672761 3221224640 3221223744 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5792 603 41 0 6382 0
vsize: 25692
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5824 0 0 0 52997 19 0 0 25 0 1 0 420962434 26308608 5795 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5795 603 41 0 6382 0
vsize: 25692
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5825 0 0 0 53997 19 0 0 25 0 1 0 420962434 26308608 5796 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5796 603 41 0 6382 0
vsize: 25692
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5828 0 0 0 54997 19 0 0 25 0 1 0 420962434 26308608 5799 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5799 603 41 0 6382 0
vsize: 25692
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5834 0 0 0 55998 19 0 0 25 0 1 0 420962434 26308608 5805 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5805 603 41 0 6382 0
vsize: 25692
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5838 0 0 0 56998 19 0 0 25 0 1 0 420962434 26308608 5809 4294967295 134512640 134672761 3221224640 3221223776 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5809 603 41 0 6382 0
vsize: 25692
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5848 0 0 0 57998 19 0 0 25 0 1 0 420962434 26443776 5819 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6456 5819 603 41 0 6415 0
vsize: 25824
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5857 0 0 0 58999 19 0 0 25 0 1 0 420962434 26443776 5828 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6456 5828 603 41 0 6415 0
vsize: 25824
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5867 0 0 0 59999 19 0 0 25 0 1 0 420962434 26443776 5838 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6456 5838 603 41 0 6415 0
vsize: 25824
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5872 0 0 0 60999 19 0 0 25 0 1 0 420962434 26591232 5843 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5843 603 41 0 6451 0
vsize: 25968
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5877 0 0 0 62000 19 0 0 25 0 1 0 420962434 26591232 5848 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5848 603 41 0 6451 0
vsize: 25968
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5877 0 0 0 63000 19 0 0 25 0 1 0 420962434 26591232 5848 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5848 603 41 0 6451 0
vsize: 25968
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5877 0 0 0 64000 19 0 0 25 0 1 0 420962434 26591232 5848 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5848 603 41 0 6451 0
vsize: 25968
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5877 0 0 0 65001 19 0 0 25 0 1 0 420962434 26591232 5848 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5848 603 41 0 6451 0
vsize: 25968
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5878 0 0 0 66001 19 0 0 25 0 1 0 420962434 26591232 5849 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5849 603 41 0 6451 0
vsize: 25968
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5885 0 0 0 67001 19 0 0 25 0 1 0 420962434 26591232 5856 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5856 603 41 0 6451 0
vsize: 25968
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5912 0 0 0 68002 19 0 0 25 0 1 0 420962434 26783744 5883 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6539 5883 603 41 0 6498 0
vsize: 26156
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5920 0 0 0 69002 19 0 0 25 0 1 0 420962434 26783744 5891 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6539 5891 603 41 0 6498 0
vsize: 26156
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5925 0 0 0 70002 19 0 0 25 0 1 0 420962434 26783744 5896 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6539 5896 603 41 0 6498 0
vsize: 26156
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5925 0 0 0 71003 19 0 0 25 0 1 0 420962434 26783744 5896 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6539 5896 603 41 0 6498 0
vsize: 26156
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5931 0 0 0 72003 19 0 0 25 0 1 0 420962434 26783744 5902 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6539 5902 603 41 0 6498 0
vsize: 26156
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5932 0 0 0 73003 19 0 0 25 0 1 0 420962434 26783744 5903 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6539 5903 603 41 0 6498 0
vsize: 26156
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5952 0 0 0 74004 20 0 0 25 0 1 0 420962434 26931200 5923 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5923 603 41 0 6534 0
vsize: 26300
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5954 0 0 0 75004 20 0 0 25 0 1 0 420962434 26931200 5925 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5925 603 41 0 6534 0
vsize: 26300
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5960 0 0 0 76004 20 0 0 25 0 1 0 420962434 26931200 5931 4294967295 134512640 134672761 3221224640 3221223808 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5931 603 41 0 6534 0
vsize: 26300
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5962 0 0 0 77003 20 0 0 25 0 1 0 420962434 26931200 5933 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5933 603 41 0 6534 0
vsize: 26300
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5985 0 0 0 78004 20 0 0 25 0 1 0 420962434 27357184 5956 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5956 603 41 0 6638 0
vsize: 26716
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5991 0 0 0 79004 20 0 0 25 0 1 0 420962434 27357184 5962 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5962 603 41 0 6638 0
vsize: 26716
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5991 0 0 0 80005 20 0 0 25 0 1 0 420962434 27357184 5962 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5962 603 41 0 6638 0
vsize: 26716
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5991 0 0 0 81005 20 0 0 25 0 1 0 420962434 27357184 5962 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5962 603 41 0 6638 0
vsize: 26716
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5991 0 0 0 82005 20 0 0 25 0 1 0 420962434 27357184 5962 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5962 603 41 0 6638 0
vsize: 26716
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 5991 0 0 0 83006 20 0 0 25 0 1 0 420962434 27357184 5962 4294967295 134512640 134672761 3221224640 3221223776 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5962 603 41 0 6638 0
vsize: 26716
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6000 0 0 0 84006 20 0 0 25 0 1 0 420962434 27357184 5971 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5971 603 41 0 6638 0
vsize: 26716
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 85007 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223824 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 86007 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 87007 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 88008 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 89008 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 90009 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223792 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 91009 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+920.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 92010 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+930.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 93010 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+940.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 94010 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 95011 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+960.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6001 0 0 0 96011 20 0 0 25 0 1 0 420962434 27357184 5972 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6679 5972 603 41 0 6638 0
vsize: 26716
[startup+970.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6019 0 0 0 97010 20 0 0 25 0 1 0 420962434 27488256 5990 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6711 5990 603 41 0 6670 0
vsize: 26844
[startup+980.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6168 0 0 0 98010 21 0 0 25 0 1 0 420962434 28012544 6139 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6839 6139 603 41 0 6798 0
vsize: 27356
[startup+990.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6326 0 0 0 99010 21 0 0 25 0 1 0 420962434 28680192 6297 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7002 6297 603 41 0 6961 0
vsize: 28008
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6412 0 0 0 100010 21 0 0 25 0 1 0 420962434 29077504 6383 4294967295 134512640 134672761 3221224640 3221223808 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6383 603 41 0 7058 0
vsize: 28396
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6412 0 0 0 101010 21 0 0 25 0 1 0 420962434 29077504 6383 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6383 603 41 0 7058 0
vsize: 28396
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6412 0 0 0 102010 21 0 0 25 0 1 0 420962434 29077504 6383 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6383 603 41 0 7058 0
vsize: 28396
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6412 0 0 0 103011 21 0 0 25 0 1 0 420962434 29077504 6383 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6383 603 41 0 7058 0
vsize: 28396
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6412 0 0 0 104011 21 0 0 25 0 1 0 420962434 29077504 6383 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6383 603 41 0 7058 0
vsize: 28396
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6412 0 0 0 105011 21 0 0 25 0 1 0 420962434 29077504 6383 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6383 603 41 0 7058 0
vsize: 28396
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6420 0 0 0 106012 22 0 0 25 0 1 0 420962434 29077504 6391 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6391 603 41 0 7058 0
vsize: 28396
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6420 0 0 0 107012 22 0 0 25 0 1 0 420962434 29077504 6391 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6391 603 41 0 7058 0
vsize: 28396
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6421 0 0 0 108012 22 0 0 25 0 1 0 420962434 29077504 6392 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6392 603 41 0 7058 0
vsize: 28396
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6421 0 0 0 109013 22 0 0 25 0 1 0 420962434 29077504 6392 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6392 603 41 0 7058 0
vsize: 28396
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6442 0 0 0 110013 22 0 0 25 0 1 0 420962434 29220864 6413 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7134 6413 603 41 0 7093 0
vsize: 28536
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6608 0 0 0 111012 22 0 0 25 0 1 0 420962434 29880320 6579 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7295 6579 603 41 0 7254 0
vsize: 29180
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6678 0 0 0 112013 22 0 0 25 0 1 0 420962434 30154752 6649 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6649 603 41 0 7321 0
vsize: 29448
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6678 0 0 0 113013 22 0 0 25 0 1 0 420962434 30154752 6649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6649 603 41 0 7321 0
vsize: 29448
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6683 0 0 0 114013 22 0 0 25 0 1 0 420962434 30154752 6654 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6654 603 41 0 7321 0
vsize: 29448
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6690 0 0 0 115014 23 0 0 25 0 1 0 420962434 30298112 6661 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7397 6661 603 41 0 7356 0
vsize: 29588
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6690 0 0 0 116014 23 0 0 25 0 1 0 420962434 30298112 6661 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7397 6661 603 41 0 7356 0
vsize: 29588
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6691 0 0 0 117014 23 0 0 25 0 1 0 420962434 30298112 6662 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7397 6662 603 41 0 7356 0
vsize: 29588
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6696 0 0 0 118015 23 0 0 25 0 1 0 420962434 30298112 6667 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7397 6667 603 41 0 7356 0
vsize: 29588
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6696 0 0 0 119015 23 0 0 25 0 1 0 420962434 30298112 6667 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7397 6667 603 41 0 7356 0
vsize: 29588
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32183
Raw data (stat): 32183 (minisat+) R 32182 29653 29652 0 -1 0 6696 0 0 0 120015 23 0 0 25 0 1 0 420962434 30298112 6667 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7397 6667 603 41 0 7356 0
vsize: 29588
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32183
Raw data (stat): 32183 (minisat+) Z 32182 29653 29652 0 -1 12 6699 0 0 0 120016 24 0 0 25 0 1 0 420962434 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.06
CPU time (s): 1200.4
CPU user time (s): 1200.16
CPU system time (s): 0.243962
CPU usage (%): 100.029
Max. virtual memory (Kb): 29588
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####