PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-5.opb
MD5SUM	00a81d808a7a59d6e11f17e19e68d826
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04884
Number of variables	450
Total number of constraints	17794
Number of constraints which are clauses	17794
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 5234

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        903816 kB
Buffers:         33528 kB
Cached:          75720 kB
SwapCached:       2272 kB
Active:          53700 kB
Inactive:        60720 kB
HighTotal:      131008 kB
HighFree:        51380 kB
LowTotal:       903652 kB
LowFree:        852436 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10876 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:06:11 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3702 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17794 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 |   17794    35588 |    5931       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 883   maxlim: 22   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23817    57118 |    7939       0        0     nan |  0.000 % |
c |       100 |   23781    56994 |    8732      93      965    10.4 |  0.604 % |
c |       250 |   23772    56963 |    9606     241     2070     8.6 |  0.684 % |
c |       475 |   23763    56932 |   10566     463     5086    11.0 |  0.830 % |
c |       812 |   23718    56777 |   11623     790     8740    11.1 |  1.132 % |
c |      1319 |   23559    56232 |   12785    1257    15363    12.2 |  2.566 % |
c |      2079 |   23232    55111 |   14064    1910    24710    12.9 |  5.969 % |
c |      3218 |   22785    53566 |   15470    2898    49664    17.1 | 11.094 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4163 |   22500    52590 |    7500    3672    71630    19.5 | 11.094 % |
c |      4264 |   22473    52497 |    8250    3694    74176    20.1 | 14.996 % |
c |      4415 |   22473    52497 |    9075    3845    77558    20.2 | 14.996 % |
c |      4640 |   22473    52497 |    9982    4070    87035    21.4 | 14.996 % |
c |      4977 |   22347    52063 |   10980    4359   101352    23.3 | 16.730 % |
c |      5483 |   22276    51816 |   12078    4816   114543    23.8 | 17.634 % |
c |      6242 |   21928    50614 |   13286    5424   139325    25.7 | 22.464 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7220 |   21856    50369 |    7285    6383   187524    29.4 | 22.464 % |
c |      7321 |   21845    50330 |    8013    6479   189175    29.2 | 23.720 % |
c |      7471 |   21835    50294 |    8814    6626   194734    29.4 | 23.946 % |
c |      7696 |   21816    50227 |    9696    6843   201731    29.5 | 24.247 % |
c |      8033 |   21792    50141 |   10665    7170   223992    31.2 | 24.633 % |
c |      8539 |   21774    50079 |   11732    7624   238322    31.3 | 24.774 % |
c |      9298 |   21757    50020 |   12905    8377   280301    33.5 | 25.000 % |
c |     10438 |   21727    49914 |   14196    9468   332289    35.1 | 25.459 % |
c |     12146 |   21703    49832 |   15616   11100   401252    36.1 | 25.678 % |
c |     14709 |   21580    49403 |   17177   13543   514820    38.0 | 27.636 % |
c |     18553 |   21449    48952 |   18895   17118   690683    40.3 | 29.378 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 26   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19560 |   21450    48959 |    7150   18125   751381    41.5 | 29.378 % |
c |     19661 |   21450    48959 |    7865    4633   166337    35.9 | 29.421 % |
c |     19811 |   21441    48928 |    8651    4775   169533    35.5 | 29.496 % |
c |     20037 |   21441    48928 |    9516    5001   176692    35.3 | 29.496 % |
c |     20374 |   21441    48928 |   10468    5338   192170    36.0 | 29.503 % |
c |     20881 |   21441    48928 |   11515    5845   214513    36.7 | 29.496 % |
c |     21642 |   21441    48928 |   12666    6606   238968    36.2 | 29.503 % |
c |     22781 |   21340    48571 |   13933    7710   279342    36.2 | 31.157 % |
c |     24489 |   21271    48326 |   15326    9405   372287    39.6 | 32.355 % |
c |     27052 |   21262    48295 |   16859   11964   487092    40.7 | 32.436 % |
c |     30896 |   21202    48083 |   18545   15777   658745    41.8 | 33.333 % |
c |     36662 |   21202    48083 |   20399   11903   363668    30.6 | 33.333 % |
c |     45311 |   21202    48083 |   22439   20552   668813    32.5 | 33.341 % |
c |     58285 |   21202    48083 |   24683   21979   535227    24.4 | 33.333 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 27   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73612 |   21203    48088 |    7067   24639   557119    22.6 | 33.333 % |
c |     73713 |   21203    48088 |    7773    6261   171914    27.5 | 33.390 % |
c |     73863 |   21203    48088 |    8551    6411   173382    27.0 | 33.384 % |
c |     74089 |   21203    48088 |    9406    6637   179223    27.0 | 33.390 % |
c |     74426 |   21203    48088 |   10346    6974   184379    26.4 | 33.384 % |
c |     74932 |   21203    48088 |   11381    7480   208185    27.8 | 33.388 % |
c |     75693 |   21203    48088 |   12519    8241   241636    29.3 | 33.384 % |
c |     76832 |   21203    48088 |   13771    9380   298007    31.8 | 33.384 % |
c |     78540 |   21203    48088 |   15148   11088   389706    35.1 | 33.388 % |
c |     81102 |   21203    48088 |   16663   13650   514351    37.7 | 33.384 % |
c |     84946 |   21203    48088 |   18329    8755   334315    38.2 | 33.384 % |
c |     90713 |   21203    48088 |   20162   14522   578181    39.8 | 33.384 % |
c |     99363 |   21188    48037 |   22179   12702   451997    35.6 | 33.534 % |
c |    112338 |   21136    47855 |   24397   14126   504412    35.7 | 34.368 % |
c |    131800 |   21136    47855 |   26836   20983   771221    36.8 | 34.361 % |
c |    160992 |   21136    47855 |   29520   22568   672847    29.8 | 34.368 % |
c |    204782 |   21136    47855 |   32472   20869   448929    21.5 | 34.368 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 28   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    238646 |   21137    47862 |    7045   21519   493542    22.9 | 34.368 % |
c |    238746 |   21137    47862 |    7749    5480    94978    17.3 | 34.417 % |
c |    238896 |   21137    47862 |    8524    5630    97795    17.4 | 34.410 % |
c |    239124 |   21137    47862 |    9376    5858   102085    17.4 | 34.410 % |
c |    239462 |   21118    47795 |   10314    6193   107592    17.4 | 34.711 % |
c |    239970 |   21118    47795 |   11346    6701   126872    18.9 | 34.711 % |
c |    240729 |   21118    47795 |   12480    7460   147823    19.8 | 34.711 % |
c |    241869 |   21118    47795 |   13728    8600   188500    21.9 | 34.711 % |
c |    243578 |   21118    47795 |   15101   10309   250586    24.3 | 34.718 % |
c |    246140 |   21118    47795 |   16611   12871   316160    24.6 | 34.711 % |
c |    249984 |   21118    47795 |   18272   16715   406188    24.3 | 34.711 % |
c |    255751 |   21091    47698 |   20100   12983   266679    20.5 | 35.237 % |
c |    264401 |   21091    47698 |   22110   11152   315178    28.3 | 35.237 % |
c |    277376 |   21091    47698 |   24321   12748   314521    24.7 | 35.237 % |
c |    296839 |   21091    47698 |   26753   19687   612921    31.1 | 35.237 % |
c |    326031 |   21091    47698 |   29428   21469   423632    19.7 | 35.237 % |
c |    369820 |   21091    47698 |   32371   20189   359468    17.8 | 35.237 % |
c |    435504 |   21091    47698 |   35608   19647   351905    17.9 | 35.237 % |
c |    534030 |   21091    47698 |   39169   18630   563786    30.3 | 35.242 % |
c |    681820 |   21091    47698 |   43086   23982  1109987    46.3 | 35.237 % |
c |    903504 |   21091    47698 |   47395   41814  1596904    38.2 | 35.237 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 27005
Raw data (stat): 27005 (runsolver) R 27004 24215 24214 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 421437367 1052672 97 4294967295 134512640 135381576 3221224464 3221219904 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99984 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1453 0 0 0 994 4 0 0 25 0 1 0 421437367 7581696 1431 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1851 1432 603 41 0 1810 0
vsize: 7404
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1576 0 0 0 1993 5 0 0 25 0 1 0 421437367 8130560 1554 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1985 1554 603 41 0 1944 0
vsize: 7940
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1633 0 0 0 2992 5 0 0 25 0 1 0 421437367 8261632 1611 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2017 1611 603 41 0 1976 0
vsize: 8068
[startup+40.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1696 0 0 0 3992 5 0 0 25 0 1 0 421437367 8527872 1674 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2082 1674 603 41 0 2041 0
vsize: 8328
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1749 0 0 0 4992 5 0 0 25 0 1 0 421437367 8839168 1727 4294967295 134512640 134672761 3221224560 3221223656 1075347133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2158 1727 603 41 0 2117 0
vsize: 8632
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1750 0 0 0 5992 6 0 0 25 0 1 0 421437367 8839168 1728 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2158 1728 603 41 0 2117 0
vsize: 8632
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1899 0 0 0 6992 6 0 0 25 0 1 0 421437367 9515008 1877 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2323 1877 603 41 0 2282 0
vsize: 9292
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1934 0 0 0 7992 6 0 0 25 0 1 0 421437367 9650176 1912 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2356 1912 603 41 0 2315 0
vsize: 9424
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 1966 0 0 0 8993 6 0 0 25 0 1 0 421437367 9789440 1944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2390 1944 603 41 0 2349 0
vsize: 9560
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2161 0 0 0 9992 7 0 0 25 0 1 0 421437367 10600448 2139 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2588 2139 603 41 0 2547 0
vsize: 10352
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2174 0 0 0 10991 7 0 0 25 0 1 0 421437367 10600448 2152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2588 2152 603 41 0 2547 0
vsize: 10352
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2241 0 0 0 11991 7 0 0 25 0 1 0 421437367 10870784 2219 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2654 2219 603 41 0 2613 0
vsize: 10616
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2254 0 0 0 12992 7 0 0 25 0 1 0 421437367 11014144 2232 4294967295 134512640 134672761 3221224560 3221223744 134559618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2689 2232 603 41 0 2648 0
vsize: 10756
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2254 0 0 0 13992 7 0 0 25 0 1 0 421437367 11014144 2232 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2689 2232 603 41 0 2648 0
vsize: 10756
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2257 0 0 0 14992 7 0 0 25 0 1 0 421437367 11014144 2235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2689 2235 603 41 0 2648 0
vsize: 10756
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2283 0 0 0 15992 7 0 0 25 0 1 0 421437367 11014144 2261 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2689 2261 603 41 0 2648 0
vsize: 10756
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2287 0 0 0 16992 8 0 0 25 0 1 0 421437367 11157504 2265 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2724 2265 603 41 0 2683 0
vsize: 10896
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2301 0 0 0 17992 8 0 0 25 0 1 0 421437367 11157504 2279 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2724 2279 603 41 0 2683 0
vsize: 10896
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2309 0 0 0 18992 8 0 0 25 0 1 0 421437367 11157504 2287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2724 2287 603 41 0 2683 0
vsize: 10896
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 19992 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 20993 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 21993 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 22993 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 23993 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 24993 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 25994 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 26994 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 27994 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2359 0 0 0 28994 8 0 0 25 0 1 0 421437367 11616256 2337 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2337 603 41 0 2795 0
vsize: 11344
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2366 0 0 0 29994 8 0 0 25 0 1 0 421437367 11616256 2344 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2344 603 41 0 2795 0
vsize: 11344
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2376 0 0 0 30994 8 0 0 25 0 1 0 421437367 11616256 2354 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2354 603 41 0 2795 0
vsize: 11344
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2376 0 0 0 31995 8 0 0 25 0 1 0 421437367 11616256 2354 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2354 603 41 0 2795 0
vsize: 11344
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2382 0 0 0 32995 8 0 0 25 0 1 0 421437367 11616256 2360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2360 603 41 0 2795 0
vsize: 11344
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2396 0 0 0 33995 8 0 0 25 0 1 0 421437367 11763712 2374 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2872 2374 603 41 0 2831 0
vsize: 11488
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2396 0 0 0 34995 8 0 0 25 0 1 0 421437367 11763712 2374 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2872 2374 603 41 0 2831 0
vsize: 11488
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2397 0 0 0 35995 8 0 0 25 0 1 0 421437367 11763712 2375 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2872 2375 603 41 0 2831 0
vsize: 11488
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2404 0 0 0 36996 8 0 0 25 0 1 0 421437367 11763712 2382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2872 2382 603 41 0 2831 0
vsize: 11488
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2515 0 0 0 37995 8 0 0 25 0 1 0 421437367 12177408 2493 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2973 2493 603 41 0 2932 0
vsize: 11892
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2532 0 0 0 38996 8 0 0 25 0 1 0 421437367 12328960 2510 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3010 2510 603 41 0 2969 0
vsize: 12040
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2714 0 0 0 39995 9 0 0 25 0 1 0 421437367 13037568 2692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3216 2692 603 41 0 3175 0
vsize: 12732
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2848 0 0 0 40995 9 0 0 25 0 1 0 421437367 13574144 2826 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3314 2826 603 41 0 3273 0
vsize: 13256
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2851 0 0 0 41995 10 0 0 25 0 1 0 421437367 13721600 2829 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3350 2829 603 41 0 3309 0
vsize: 13400
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2862 0 0 0 42995 10 0 0 25 0 1 0 421437367 13721600 2840 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3350 2840 603 41 0 3309 0
vsize: 13400
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2880 0 0 0 43996 10 0 0 25 0 1 0 421437367 13869056 2858 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3386 2858 603 41 0 3345 0
vsize: 13544
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2891 0 0 0 44996 10 0 0 25 0 1 0 421437367 13869056 2869 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3386 2869 603 41 0 3345 0
vsize: 13544
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2910 0 0 0 45996 10 0 0 25 0 1 0 421437367 13869056 2888 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3386 2888 603 41 0 3345 0
vsize: 13544
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 2914 0 0 0 46996 10 0 0 25 0 1 0 421437367 14008320 2892 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3420 2892 603 41 0 3379 0
vsize: 13680
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3000 0 0 0 47996 10 0 0 25 0 1 0 421437367 14282752 2978 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3487 2978 603 41 0 3446 0
vsize: 13948
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3007 0 0 0 48996 10 0 0 25 0 1 0 421437367 14282752 2985 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3487 2985 603 41 0 3446 0
vsize: 13948
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3050 0 0 0 49996 10 0 0 25 0 1 0 421437367 14553088 3028 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3553 3028 603 41 0 3512 0
vsize: 14212
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3369 0 0 0 50995 11 0 0 25 0 1 0 421437367 15757312 3347 4294967295 134512640 134672761 3221224560 3221222592 134565831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3847 3347 603 41 0 3806 0
vsize: 15388
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3370 0 0 0 51995 11 0 0 25 0 1 0 421437367 15757312 3348 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3847 3348 603 41 0 3806 0
vsize: 15388
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3380 0 0 0 52996 11 0 0 25 0 1 0 421437367 15912960 3358 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3358 603 41 0 3844 0
vsize: 15540
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3642 0 0 0 53995 12 0 0 25 0 1 0 421437367 17006592 3620 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4152 3620 603 41 0 4111 0
vsize: 16608
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3798 0 0 0 54993 14 0 0 25 0 1 0 421437367 17539072 3776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4282 3776 603 41 0 4241 0
vsize: 17128
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3804 0 0 0 55993 14 0 0 25 0 1 0 421437367 17674240 3782 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4315 3782 603 41 0 4274 0
vsize: 17260
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 3811 0 0 0 56994 14 0 0 25 0 1 0 421437367 17674240 3789 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4315 3789 603 41 0 4274 0
vsize: 17260
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4063 0 0 0 57993 14 0 0 25 0 1 0 421437367 18747392 4041 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4577 4041 603 41 0 4536 0
vsize: 18308
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4064 0 0 0 58993 14 0 0 25 0 1 0 421437367 18747392 4042 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4577 4042 603 41 0 4536 0
vsize: 18308
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4064 0 0 0 59994 14 0 0 25 0 1 0 421437367 18747392 4042 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4577 4042 603 41 0 4536 0
vsize: 18308
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4160 0 0 0 60993 15 0 0 25 0 1 0 421437367 19152896 4138 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4138 603 41 0 4635 0
vsize: 18704
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4412 0 0 0 61992 16 0 0 25 0 1 0 421437367 20090880 4390 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4390 603 41 0 4864 0
vsize: 19620
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4414 0 0 0 62993 16 0 0 25 0 1 0 421437367 20090880 4392 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4392 603 41 0 4864 0
vsize: 19620
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4414 0 0 0 63993 16 0 0 25 0 1 0 421437367 20090880 4392 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4392 603 41 0 4864 0
vsize: 19620
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4415 0 0 0 64993 16 0 0 25 0 1 0 421437367 20090880 4393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4393 603 41 0 4864 0
vsize: 19620
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4415 0 0 0 65993 16 0 0 25 0 1 0 421437367 20090880 4393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4393 603 41 0 4864 0
vsize: 19620
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4415 0 0 0 66994 16 0 0 25 0 1 0 421437367 20090880 4393 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4393 603 41 0 4864 0
vsize: 19620
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4415 0 0 0 67994 16 0 0 25 0 1 0 421437367 20090880 4393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4393 603 41 0 4864 0
vsize: 19620
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4415 0 0 0 68994 16 0 0 25 0 1 0 421437367 20090880 4393 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4393 603 41 0 4864 0
vsize: 19620
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4415 0 0 0 69993 16 0 0 25 0 1 0 421437367 20090880 4393 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4393 603 41 0 4864 0
vsize: 19620
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4415 0 0 0 70993 17 0 0 25 0 1 0 421437367 20090880 4393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4393 603 41 0 4864 0
vsize: 19620
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 71992 17 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 72992 17 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 73991 18 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 74991 18 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 75991 18 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 76990 19 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 77990 19 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 78990 19 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 79989 20 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 80989 20 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4418 0 0 0 81989 20 0 0 25 0 1 0 421437367 20090880 4396 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4396 603 41 0 4864 0
vsize: 19620
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27005
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 82988 20 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 27048
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 83977 33 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+850.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27058
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 84976 33 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+860.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27058
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 85977 33 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+870.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27058
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 86977 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+880.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27058
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 87977 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27058
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 88977 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+900.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27058
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 89977 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+910.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27058
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 90977 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+920.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 91978 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+930.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 92978 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+940.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 93978 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+950.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 94978 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+960.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 95978 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+970.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 96978 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+980.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4419 0 0 0 97979 34 0 0 25 0 1 0 421437367 20090880 4397 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4397 603 41 0 4864 0
vsize: 19620
[startup+990.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4421 0 0 0 98979 34 0 0 25 0 1 0 421437367 20090880 4399 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4399 603 41 0 4864 0
vsize: 19620
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4426 0 0 0 99978 34 0 0 25 0 1 0 421437367 20090880 4404 4294967295 134512640 134672761 3221224560 3221222864 134565764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4404 603 41 0 4864 0
vsize: 19620
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4426 0 0 0 100979 34 0 0 25 0 1 0 421437367 20090880 4404 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4404 603 41 0 4864 0
vsize: 19620
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4426 0 0 0 101979 34 0 0 25 0 1 0 421437367 20090880 4404 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4404 603 41 0 4864 0
vsize: 19620
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4426 0 0 0 102979 34 0 0 25 0 1 0 421437367 20090880 4404 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4404 603 41 0 4864 0
vsize: 19620
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4427 0 0 0 103979 34 0 0 25 0 1 0 421437367 20090880 4405 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4405 603 41 0 4864 0
vsize: 19620
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4427 0 0 0 104979 34 0 0 25 0 1 0 421437367 20090880 4405 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4405 603 41 0 4864 0
vsize: 19620
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4428 0 0 0 105979 34 0 0 25 0 1 0 421437367 20090880 4406 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4406 603 41 0 4864 0
vsize: 19620
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4429 0 0 0 106980 34 0 0 25 0 1 0 421437367 20090880 4407 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4407 603 41 0 4864 0
vsize: 19620
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4439 0 0 0 107980 34 0 0 25 0 1 0 421437367 20250624 4417 4294967295 134512640 134672761 3221224560 3221223744 134559254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4417 603 41 0 4903 0
vsize: 19776
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4441 0 0 0 108980 34 0 0 25 0 1 0 421437367 20250624 4419 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4419 603 41 0 4903 0
vsize: 19776
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4442 0 0 0 109980 34 0 0 25 0 1 0 421437367 20250624 4420 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4420 603 41 0 4903 0
vsize: 19776
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4452 0 0 0 110980 34 0 0 25 0 1 0 421437367 20250624 4430 4294967295 134512640 134672761 3221224560 3221223664 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4430 603 41 0 4903 0
vsize: 19776
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4452 0 0 0 111980 34 0 0 25 0 1 0 421437367 20250624 4430 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4430 603 41 0 4903 0
vsize: 19776
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4453 0 0 0 112981 34 0 0 25 0 1 0 421437367 20250624 4431 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4431 603 41 0 4903 0
vsize: 19776
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4454 0 0 0 113981 34 0 0 25 0 1 0 421437367 20250624 4432 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4432 603 41 0 4903 0
vsize: 19776
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4454 0 0 0 114981 34 0 0 25 0 1 0 421437367 20250624 4432 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4432 603 41 0 4903 0
vsize: 19776
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4454 0 0 0 115981 34 0 0 25 0 1 0 421437367 20250624 4432 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4432 603 41 0 4903 0
vsize: 19776
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27060
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4454 0 0 0 116981 34 0 0 25 0 1 0 421437367 20250624 4432 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4432 603 41 0 4903 0
vsize: 19776
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4455 0 0 0 117982 34 0 0 25 0 1 0 421437367 20250624 4433 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4433 603 41 0 4903 0
vsize: 19776
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4468 0 0 0 118982 34 0 0 25 0 1 0 421437367 20250624 4446 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4446 603 41 0 4903 0
vsize: 19776
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27005 (minisat+) R 27004 24215 24214 0 -1 0 4505 0 0 0 119982 34 0 0 25 0 1 0 421437367 20447232 4483 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4992 4483 603 41 0 4951 0
vsize: 19968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27062
Raw data (stat): 27005 (minisat+) Z 27004 24215 24214 0 -1 12 4508 0 0 0 119982 35 0 0 25 0 1 0 421437367 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.18
CPU user time (s): 1199.83
CPU system time (s): 0.352946
CPU usage (%): 100.01
Max. virtual memory (Kb): 19968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####