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 30497

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        622528 kB
Buffers:         35104 kB
Cached:         355360 kB
SwapCached:        672 kB
Active:          74016 kB
Inactive:       318592 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        622276 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5080 kB
Slab:            13912 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 17:28:30 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 21901 7 1229.84 152
#### 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 % |
c |    631992 |   30983    63957 |   29492   38173  1062628    27.8 | 84.385 % |
c |    640641 |   30838    63649 |   32441   21452   580040    27.0 | 84.513 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10835 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.93 0.93 2/54 10831
Raw data (stat): 10831 (runsolver) R 10830 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782330611 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 0 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.93 0.94 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.94 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.94 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0027 s]
Raw data (loadavg): 0.95 0.94 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0041 s]
Raw data (loadavg): 0.96 0.94 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0048 s]
Raw data (loadavg): 0.97 0.94 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0052 s]
Raw data (loadavg): 0.97 0.94 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.005 s]
Raw data (loadavg): 0.97 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.98 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.98 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.006 s]
Raw data (loadavg): 0.99 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.99 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.006 s]
Raw data (loadavg): 0.99 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 10835
Raw data (stat): 10831 (minisat+_script) S 10830 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782330611 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.84
CPU user time (s): 1229.48
CPU system time (s): 0.368943
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####