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/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb
MD5SUM	a84a96a9314212f3d8ecd5227c500cef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	91392
Optimality of the best value was proved	NO
Number of terms in the objective function	210
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	7516192761
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	7516192761
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1202.31
Number of variables	330
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	150
Trace number 20766

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 21:47:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14495 boxname=wulflinc10 idbench=1115 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a84a96a9314212f3d8ecd5227c500cef  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare2_1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare2_1.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare2_1.opb
IDLAUNCH: 14495
/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:        750116 kB
Buffers:         15892 kB
Cached:         247064 kB
SwapCached:          0 kB
Active:          43316 kB
Inactive:       222220 kB
HighTotal:      131008 kB
HighFree:         2800 kB
LowTotal:       903652 kB
LowFree:        747316 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13148 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 22:07:13 (client local time) WITH STATUS 10 IN 1200.54 SECONDS
stats: 14495 7 1200.54 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  12]---> Adder-cost: 708   maxlim: 3756758   bits: 23/22
c ---[  10]---> Adder-cost: 758   maxlim: 4064912   bits: 23/22
c ---[   8]---> Adder-cost: 714   maxlim: 3859164   bits: 23/22
c ---[   6]---> Adder-cost: 676   maxlim: 4153021   bits: 23/22
c ---[   4]---> Adder-cost: 812   maxlim: 3812158   bits: 23/22
c ---[   2]---> Adder-cost: 766   maxlim: 4131466   bits: 23/22
c ---[   0]---> Adder-cost: 692   maxlim: 3780388   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   34939   124245 |   11646       0        0     nan |  0.000 % |
c |       100 |   34939   124245 |   12810     100      358     3.6 |  6.830 % |
c |       252 |   34939   124245 |   14091     252     1194     4.7 |  6.830 % |
c |       478 |   34939   124245 |   15500     478     2691     5.6 |  6.830 % |
c ==============================================================================
c [1mFound solution: 3508914[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2156     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       805 |   40779   138009 |   13593     805     6248     7.8 |  6.830 % |
c |       905 |   40779   138009 |   14952     905     7124     7.9 |  5.133 % |
c |      1055 |   40779   138009 |   16447    1055    11699    11.1 |  5.133 % |
c |      1281 |   40779   138009 |   18092    1281    16390    12.8 |  5.133 % |
c ==============================================================================
c [1mFound solution: 3387574[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1472 |   40932   138410 |   13644    1472    21619    14.7 |  5.133 % |
c |      1572 |   40932   138410 |   15008    1572    23947    15.2 |  5.125 % |
c |      1722 |   40932   138410 |   16509    1722    25223    14.6 |  5.125 % |
c |      1947 |   40932   138410 |   18160    1947    36799    18.9 |  5.125 % |
c |      2284 |   40924   138384 |   19976    2283    39892    17.5 |  5.139 % |
c |      2790 |   40924   138384 |   21973    2789    55062    19.7 |  5.139 % |
c ==============================================================================
c [1mFound solution: 3139612[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2942 |   41014   138611 |   13671    2941    56665    19.3 |  5.139 % |
c |      3043 |   41014   138611 |   15038    3042    60456    19.9 |  5.136 % |
c |      3193 |   40998   138559 |   16541    3190    61741    19.4 |  5.163 % |
c |      3418 |   40998   138559 |   18196    3415    63658    18.6 |  5.163 % |
c |      3755 |   40990   138533 |   20015    3751    69345    18.5 |  5.176 % |
c |      4261 |   40990   138533 |   22017    4257    81467    19.1 |  5.176 % |
c |      5020 |   40982   138507 |   24219    5015   102519    20.4 |  5.189 % |
c |      6159 |   40968   138463 |   26640    6152   127412    20.7 |  5.216 % |
c |      7867 |   40928   138358 |   29305    7856   184719    23.5 |  5.335 % |
c |     10430 |   40928   138358 |   32235   10419   298228    28.6 |  5.335 % |
c |     14274 |   40928   138358 |   35459   14263   550460    38.6 |  5.335 % |
c |     20040 |   40928   138358 |   39004   20029   837933    41.8 |  5.335 % |
c |     28689 |   40928   138358 |   42905   28678  1392722    48.6 |  5.335 % |
c |     41663 |   40920   138332 |   47195   41651  2116748    50.8 |  5.348 % |
c ==============================================================================
c [1mFound solution: 3101571[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44256 |   40997   138521 |   13665   44244  2344456    53.0 |  5.348 % |
c |     44356 |   40997   138521 |   15031    7596   331413    43.6 |  5.346 % |
c |     44506 |   40997   138521 |   16534    7746   334276    43.2 |  5.346 % |
c |     44731 |   40997   138521 |   18188    7971   339192    42.6 |  5.346 % |
c |     45069 |   40997   138521 |   20006    8309   366442    44.1 |  5.346 % |
c |     45577 |   40989   138495 |   22007    8816   375885    42.6 |  5.359 % |
c |     46338 |   40989   138495 |   24208    9577   391386    40.9 |  5.359 % |
c |     47478 |   40989   138495 |   26629   10717   523770    48.9 |  5.359 % |
c |     49187 |   40981   138469 |   29292   12425   594590    47.9 |  5.372 % |
c |     51749 |   40973   138443 |   32221   14986   702425    46.9 |  5.385 % |
c |     55593 |   40965   138417 |   35443   18829   940085    49.9 |  5.399 % |
c |     61361 |   40965   138417 |   38987   24597  1267792    51.5 |  5.399 % |
c |     70010 |   40965   138417 |   42886   33246  1915029    57.6 |  5.399 % |
c |     82985 |   40959   138399 |   47175   14648  1405707    96.0 |  5.412 % |
c ==============================================================================
c [1mFound solution: 2768881[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83299 |   40996   138494 |   13665   14962  1432871    95.8 |  5.412 % |
c |     83399 |   40996   138494 |   15031    7581   786644   103.8 |  5.419 % |
c |     83550 |   40996   138494 |   16534    7732   787689   101.9 |  5.419 % |
c |     83776 |   40996   138494 |   18188    7958   805797   101.3 |  5.419 % |
c |     84114 |   40996   138494 |   20006    8296   816626    98.4 |  5.419 % |
c |     84620 |   40980   138442 |   22007    8800   822365    93.5 |  5.445 % |
c |     85379 |   40980   138442 |   24208    9559   852520    89.2 |  5.445 % |
c |     86519 |   40980   138442 |   26629   10699   901076    84.2 |  5.445 % |
c ==============================================================================
c [1mFound solution: 2529632[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87517 |   41024   138550 |   13674   11697   920739    78.7 |  5.445 % |
c |     87618 |   41024   138550 |   15041   11798   922865    78.2 |  5.449 % |
c |     87769 |   41024   138550 |   16545   11949   924426    77.4 |  5.449 % |
c |     87994 |   41024   138550 |   18200   12174   962535    79.1 |  5.449 % |
c |     88331 |   41024   138550 |   20020   12511   970062    77.5 |  5.449 % |
c |     88838 |   41024   138550 |   22022   13018   981649    75.4 |  5.449 % |
c |     89599 |   40980   138451 |   24224   13762  1001736    72.8 |  5.607 % |
c ==============================================================================
c [1mFound solution: 2332172[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90529 |   41018   138547 |   13672   14692  1032851    70.3 |  5.607 % |
c |     90630 |   41018   138547 |   15039    7447   221730    29.8 |  5.613 % |
c |     90780 |   41018   138547 |   16543    7597   228365    30.1 |  5.613 % |
c |     91007 |   41018   138547 |   18197    7824   236020    30.2 |  5.613 % |
c |     91344 |   41018   138547 |   20017    8161   244631    30.0 |  5.613 % |
c |     91851 |   41018   138547 |   22018    8668   262010    30.2 |  5.613 % |
c |     92610 |   41018   138547 |   24220    9427   289216    30.7 |  5.613 % |
c |     93749 |   41018   138547 |   26642   10566   324001    30.7 |  5.613 % |
c ==============================================================================
c [1mFound solution: 1268000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93788 |   41058   138645 |   13686   10605   324316    30.6 |  5.613 % |
c |     93888 |   41058   138645 |   15054   10705   325878    30.4 |  5.617 % |
c |     94038 |   41058   138645 |   16560   10855   328460    30.3 |  5.617 % |
c |     94263 |   41058   138645 |   18216   11080   336119    30.3 |  5.617 % |
c |     94600 |   41058   138645 |   20037   11417   345490    30.3 |  5.617 % |
c |     95106 |   41058   138645 |   22041   11923   355958    29.9 |  5.617 % |
c |     95866 |   41058   138645 |   24245   12683   376379    29.7 |  5.617 % |
c |     97007 |   41058   138645 |   26670   13824   415717    30.1 |  5.617 % |
c |     98715 |   41042   138609 |   29337   15530   505977    32.6 |  5.682 % |
c |    101278 |   41042   138609 |   32270   18093   641493    35.5 |  5.682 % |
c |    105122 |   41042   138609 |   35497   21937   793448    36.2 |  5.682 % |
c |    110890 |   40989   138488 |   39047   27697  1249195    45.1 |  5.892 % |
c |    119540 |   40989   138488 |   42952   36347  1678871    46.2 |  5.892 % |
c |    132515 |   40989   138488 |   47247   19686  1026731    52.2 |  5.892 % |
c |    151977 |   40989   138488 |   51972   39148  2348611    60.0 |  5.892 % |
c ==============================================================================
c [1mFound solution: 1199813[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    164215 |   41028   138586 |   13676   51385  2897923    56.4 |  5.892 % |
c |    164315 |   41028   138586 |   15043    7485   215774    28.8 |  5.922 % |
c |    164465 |   41028   138586 |   16547    7635   216877    28.4 |  5.922 % |
c |    164690 |   41028   138586 |   18202    7860   220212    28.0 |  5.922 % |
c |    165029 |   41028   138586 |   20023    8199   229772    28.0 |  5.922 % |
c |    165535 |   41028   138586 |   22025    8705   244512    28.1 |  5.922 % |
c |    166295 |   41028   138586 |   24227    9465   263220    27.8 |  5.922 % |
c |    167434 |   41028   138586 |   26650   10604   307568    29.0 |  5.922 % |
c |    169142 |   41028   138586 |   29315   12312   363472    29.5 |  5.922 % |
c |    171705 |   41028   138586 |   32247   14875   436140    29.3 |  5.922 % |
c |    175550 |   41028   138586 |   35472   18720   622601    33.3 |  5.922 % |
c |    181317 |   41028   138586 |   39019   24487   866181    35.4 |  5.922 % |
c |    189966 |   41028   138586 |   42921   33136  1276195    38.5 |  5.922 % |
c |    202940 |   41028   138586 |   47213   16461   651820    39.6 |  5.922 % |
c |    222402 |   41028   138586 |   51934   35923  1718490    47.8 |  5.922 % |
c ==============================================================================
c [1mFound solution: 1170306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225084 |   41060   138668 |   13686   38605  1988811    51.5 |  5.922 % |
c |    225184 |   41060   138668 |   15054   14124   951772    67.4 |  5.929 % |
c |    225334 |   41060   138668 |   16560   14274   953626    66.8 |  5.929 % |
c |    225559 |   41060   138668 |   18216   14499   957216    66.0 |  5.929 % |
c |    225897 |   41060   138668 |   20037   14837   972112    65.5 |  5.929 % |
c |    226406 |   41060   138668 |   22041   15346   982475    64.0 |  5.929 % |
c |    227165 |   41060   138668 |   24245   16105  1015318    63.0 |  5.929 % |
c |    228305 |   41060   138668 |   26670   17245  1064522    61.7 |  5.929 % |
c |    230013 |   41060   138668 |   29337   18953  1140695    60.2 |  5.929 % |
c |    232577 |   41060   138668 |   32270   21517  1257334    58.4 |  5.929 % |
c |    236424 |   41060   138668 |   35497   25364  1437292    56.7 |  5.929 % |
c |    242190 |   41060   138668 |   39047   31130  1699206    54.6 |  5.929 % |
c ==============================================================================
c [1mFound solution: 871372[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    248630 |   40948   138349 |   13649   37528  1996004    53.2 |  5.929 % |
c |    248730 |   40948   138349 |   15013   13652   548141    40.2 |  6.442 % |
c |    248880 |   40948   138349 |   16515   13802   550205    39.9 |  6.442 % |
c |    249107 |   40948   138349 |   18166   14029   602493    42.9 |  6.442 % |
c |    249445 |   40948   138349 |   19983   14367   626735    43.6 |  6.442 % |
c |    249952 |   40948   138349 |   21981   14874   631870    42.5 |  6.442 % |
c |    250713 |   40948   138349 |   24180   15635   650787    41.6 |  6.442 % |
c |    251852 |   40948   138349 |   26598   16774   674713    40.2 |  6.442 % |
c |    253560 |   40948   138349 |   29257   18482   750180    40.6 |  6.442 % |
c |    256122 |   40948   138349 |   32183   21044   846323    40.2 |  6.442 % |
c |    259967 |   40871   138166 |   35401   24884  1027076    41.3 |  6.756 % |
c |    265733 |   40871   138166 |   38942   30650  1296850    42.3 |  6.756 % |
c |    274383 |   40836   138088 |   42836   39296  1758673    44.8 |  6.873 % |
c |    287358 |   40836   138088 |   47120   20050   912699    45.5 |  6.873 % |
c |    306819 |   40757   137906 |   51832   39505  1790297    45.3 |  7.148 % |
c |    336012 |   40757   137906 |   57015   30361  1416755    46.7 |  7.148 % |
c |    379802 |   40757   137906 |   62716   26866  1500988    55.9 |  7.148 % |
c |    445486 |   40720   137819 |   68988   44114  2970808    67.3 |  7.304 % |
c |    544012 |   40720   137819 |   75887   27098  1718385    63.4 |  7.304 % |
c |    691801 |   40720   137819 |   83476   53511  3373796    63.0 |  7.304 % |
#### 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): 1.01 1.00 0.95 2/54 5776
Raw data (stat): 5776 (runsolver) R 5775 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490220587 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99969 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 1843 0 0 0 993 5 0 0 25 0 1 0 490220587 9166848 1819 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2238 1819 603 41 0 2197 0
vsize: 8952
[startup+20.0003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 2604 0 0 0 1991 6 0 0 25 0 1 0 490220587 12283904 2580 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2999 2580 603 41 0 2958 0
vsize: 11996
[startup+30.0012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 3342 0 0 0 2989 8 0 0 25 0 1 0 490220587 15355904 3318 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3749 3318 603 41 0 3708 0
vsize: 14996
[startup+40.0014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 4017 0 0 0 3986 10 0 0 25 0 1 0 490220587 18182144 3993 4294967295 134512640 134672761 3221224528 3221223652 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4439 3993 603 41 0 4398 0
vsize: 17756
[startup+50.0019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 4020 0 0 0 4987 10 0 0 25 0 1 0 490220587 18182144 3996 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4439 3996 603 41 0 4398 0
vsize: 17756
[startup+60.0015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 4020 0 0 0 5987 10 0 0 25 0 1 0 490220587 18182144 3996 4294967295 134512640 134672761 3221224528 3221223728 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4439 3996 603 41 0 4398 0
vsize: 17756
[startup+70.0021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 4030 0 0 0 6987 10 0 0 25 0 1 0 490220587 18182144 4006 4294967295 134512640 134672761 3221224528 3221223712 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4439 4006 603 41 0 4398 0
vsize: 17756
[startup+80.0027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 4596 0 0 0 7985 12 0 0 25 0 1 0 490220587 20459520 4572 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4995 4572 603 41 0 4954 0
vsize: 19980
[startup+90.0032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5104 0 0 0 8984 14 0 0 25 0 1 0 490220587 22597632 5080 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5517 5080 603 41 0 5476 0
vsize: 22068
[startup+100.003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 9984 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+110.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 10984 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+120.003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 11984 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+130.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 12984 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+140.003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 13984 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+150.004 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 14985 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+160.003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 15985 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+170.004 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5148 0 0 0 16985 14 0 0 25 0 1 0 490220587 22728704 5124 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5124 603 41 0 5508 0
vsize: 22196
[startup+180.003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 17985 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+190.004 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 18985 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+200.006 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 19986 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+210.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 20987 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223664 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+220.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 21988 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+230.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 22988 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+240.035 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 23989 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+250.042 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 24990 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+260.045 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 25990 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+270.044 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 26991 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+280.044 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 27991 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+290.045 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 28991 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+300.045 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 29991 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223632 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+310.045 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 30991 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+320.044 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5153 0 0 0 31991 14 0 0 25 0 1 0 490220587 22728704 5129 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5129 603 41 0 5508 0
vsize: 22196
[startup+330.049 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5154 0 0 0 32992 14 0 0 25 0 1 0 490220587 22728704 5130 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5130 603 41 0 5508 0
vsize: 22196
[startup+340.056 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5154 0 0 0 33993 14 0 0 25 0 1 0 490220587 22728704 5130 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5130 603 41 0 5508 0
vsize: 22196
[startup+350.056 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5154 0 0 0 34992 14 0 0 25 0 1 0 490220587 22728704 5130 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5130 603 41 0 5508 0
vsize: 22196
[startup+360.056 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5154 0 0 0 35992 14 0 0 25 0 1 0 490220587 22728704 5130 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 5130 603 41 0 5508 0
vsize: 22196
[startup+370.081 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5545 0 0 0 36994 15 0 0 25 0 1 0 490220587 24326144 5521 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5939 5521 603 41 0 5898 0
vsize: 23756
[startup+380.089 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5872 0 0 0 37994 17 0 0 25 0 1 0 490220587 25669632 5848 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5848 603 41 0 6226 0
vsize: 25068
[startup+390.089 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5872 0 0 0 38994 17 0 0 25 0 1 0 490220587 25669632 5848 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5848 603 41 0 6226 0
vsize: 25068
[startup+400.096 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5872 0 0 0 39995 17 0 0 25 0 1 0 490220587 25669632 5848 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5848 603 41 0 6226 0
vsize: 25068
[startup+410.095 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5872 0 0 0 40995 17 0 0 25 0 1 0 490220587 25669632 5848 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5848 603 41 0 6226 0
vsize: 25068
[startup+420.096 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5872 0 0 0 41995 17 0 0 25 0 1 0 490220587 25669632 5848 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5848 603 41 0 6226 0
vsize: 25068
[startup+430.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5872 0 0 0 42996 17 0 0 25 0 1 0 490220587 25669632 5848 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5848 603 41 0 6226 0
vsize: 25068
[startup+440.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 5985 0 0 0 43996 17 0 0 25 0 1 0 490220587 26075136 5961 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6366 5961 603 41 0 6325 0
vsize: 25464
[startup+450.103 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6390 0 0 0 44995 18 0 0 25 0 1 0 490220587 27820032 6366 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6792 6366 603 41 0 6751 0
vsize: 27168
[startup+460.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6726 0 0 0 45995 19 0 0 25 0 1 0 490220587 29159424 6702 4294967295 134512640 134672761 3221224528 3221223468 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7119 6702 603 41 0 7078 0
vsize: 28476
[startup+470.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 46995 19 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+480.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 47995 19 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+490.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 48995 19 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223712 134558702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+500.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 49995 19 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+510.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 50996 19 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+520.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 51996 19 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+530.125 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 52996 20 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+540.133 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6760 0 0 0 53996 20 0 0 25 0 1 0 490220587 29294592 6736 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6736 603 41 0 7111 0
vsize: 28608
[startup+550.133 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 6953 0 0 0 54996 20 0 0 25 0 1 0 490220587 30101504 6929 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7349 6929 603 41 0 7308 0
vsize: 29396
[startup+560.132 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7263 0 0 0 55995 21 0 0 25 0 1 0 490220587 31567872 7239 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7707 7239 603 41 0 7666 0
vsize: 30828
[startup+570.133 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 56995 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223696 134561533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+580.133 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 57995 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+590.132 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 58995 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+600.133 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 59995 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+610.132 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 60995 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+620.132 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 61995 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223712 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+630.131 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 62996 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+640.242 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7612 0 0 0 64007 22 0 0 25 0 1 0 490220587 33062912 7588 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7588 603 41 0 8031 0
vsize: 32288
[startup+650.243 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 65007 22 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+660.242 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 66007 22 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+670.251 s]
Raw data (loadavg): 1.24 1.05 0.96 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 67007 22 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+680.271 s]
Raw data (loadavg): 1.28 1.06 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 68009 23 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+690.271 s]
Raw data (loadavg): 1.23 1.06 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 69009 23 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+700.374 s]
Raw data (loadavg): 1.20 1.06 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 70020 23 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+710.374 s]
Raw data (loadavg): 1.17 1.06 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 71020 23 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+720.374 s]
Raw data (loadavg): 1.14 1.05 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7613 0 0 0 72020 23 0 0 25 0 1 0 490220587 33062912 7589 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8072 7589 603 41 0 8031 0
vsize: 32288
[startup+730.374 s]
Raw data (loadavg): 1.12 1.05 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 7878 0 0 0 73019 23 0 0 25 0 1 0 490220587 34136064 7854 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8334 7854 603 41 0 8293 0
vsize: 33336
[startup+740.374 s]
Raw data (loadavg): 1.10 1.05 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8260 0 0 0 74018 25 0 0 25 0 1 0 490220587 35618816 8236 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8696 8236 603 41 0 8655 0
vsize: 34784
[startup+750.374 s]
Raw data (loadavg): 1.08 1.05 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8304 0 0 0 75018 25 0 0 25 0 1 0 490220587 35885056 8280 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8280 603 41 0 8720 0
vsize: 35044
[startup+760.374 s]
Raw data (loadavg): 1.07 1.05 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8304 0 0 0 76019 25 0 0 25 0 1 0 490220587 35885056 8280 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8280 603 41 0 8720 0
vsize: 35044
[startup+770.374 s]
Raw data (loadavg): 1.06 1.04 0.97 2/54 5776
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8304 0 0 0 77019 25 0 0 25 0 1 0 490220587 35885056 8280 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8280 603 41 0 8720 0
vsize: 35044
[startup+780.374 s]
Raw data (loadavg): 1.12 1.06 0.97 2/54 5829
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8304 0 0 0 78018 25 0 0 25 0 1 0 490220587 35885056 8280 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8280 603 41 0 8720 0
vsize: 35044
[startup+790.375 s]
Raw data (loadavg): 1.10 1.06 0.97 2/54 5829
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8304 0 0 0 79019 25 0 0 25 0 1 0 490220587 35885056 8280 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8280 603 41 0 8720 0
vsize: 35044
[startup+800.375 s]
Raw data (loadavg): 1.09 1.05 0.97 2/54 5829
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8305 0 0 0 80019 25 0 0 25 0 1 0 490220587 35885056 8281 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8281 603 41 0 8720 0
vsize: 35044
[startup+810.374 s]
Raw data (loadavg): 1.07 1.05 0.97 2/54 5829
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8305 0 0 0 81019 25 0 0 25 0 1 0 490220587 35885056 8281 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8281 603 41 0 8720 0
vsize: 35044
[startup+820.374 s]
Raw data (loadavg): 1.06 1.05 0.97 2/54 5829
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8316 0 0 0 82019 25 0 0 25 0 1 0 490220587 35885056 8292 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8761 8292 603 41 0 8720 0
vsize: 35044
[startup+830.375 s]
Raw data (loadavg): 1.05 1.05 0.97 2/54 5829
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8335 0 0 0 83019 25 0 0 25 0 1 0 490220587 36044800 8311 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8800 8311 603 41 0 8759 0
vsize: 35200
[startup+840.375 s]
Raw data (loadavg): 1.04 1.05 0.97 2/54 5829
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8349 0 0 0 84020 25 0 0 25 0 1 0 490220587 36044800 8325 4294967295 134512640 134672761 3221224528 3221223712 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8800 8325 603 41 0 8759 0
vsize: 35200
[startup+850.375 s]
Raw data (loadavg): 1.04 1.04 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8353 0 0 0 85020 25 0 0 25 0 1 0 490220587 36044800 8329 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8800 8329 603 41 0 8759 0
vsize: 35200
[startup+860.375 s]
Raw data (loadavg): 1.03 1.04 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8366 0 0 0 86020 25 0 0 25 0 1 0 490220587 36208640 8342 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8840 8342 603 41 0 8799 0
vsize: 35360
[startup+870.375 s]
Raw data (loadavg): 1.02 1.04 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8368 0 0 0 87020 25 0 0 25 0 1 0 490220587 36208640 8344 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8840 8344 603 41 0 8799 0
vsize: 35360
[startup+880.375 s]
Raw data (loadavg): 1.02 1.04 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8384 0 0 0 88020 25 0 0 25 0 1 0 490220587 36208640 8360 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8840 8360 603 41 0 8799 0
vsize: 35360
[startup+890.375 s]
Raw data (loadavg): 1.02 1.04 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 89020 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+900.375 s]
Raw data (loadavg): 1.01 1.03 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 90020 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+910.375 s]
Raw data (loadavg): 1.01 1.03 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 91020 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223712 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+920.376 s]
Raw data (loadavg): 1.01 1.03 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 92020 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+930.375 s]
Raw data (loadavg): 1.01 1.03 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 93021 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+940.375 s]
Raw data (loadavg): 1.01 1.03 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 94021 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+950.376 s]
Raw data (loadavg): 1.00 1.03 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 95021 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+960.375 s]
Raw data (loadavg): 1.00 1.03 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8626 0 0 0 96021 26 0 0 25 0 1 0 490220587 37285888 8602 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8602 603 41 0 9062 0
vsize: 36412
[startup+970.375 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8635 0 0 0 97021 26 0 0 25 0 1 0 490220587 37285888 8611 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8611 603 41 0 9062 0
vsize: 36412
[startup+980.375 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8644 0 0 0 98021 26 0 0 25 0 1 0 490220587 37449728 8620 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9143 8620 603 41 0 9102 0
vsize: 36572
[startup+990.376 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8644 0 0 0 99021 26 0 0 25 0 1 0 490220587 37449728 8620 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9143 8620 603 41 0 9102 0
vsize: 36572
[startup+1000.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8644 0 0 0 100021 26 0 0 25 0 1 0 490220587 37449728 8620 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9143 8620 603 41 0 9102 0
vsize: 36572
[startup+1010.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 8794 0 0 0 101020 27 0 0 25 0 1 0 490220587 37978112 8770 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9272 8770 603 41 0 9231 0
vsize: 37088
[startup+1020.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9041 0 0 0 102020 28 0 0 25 0 1 0 490220587 39047168 9017 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9533 9017 603 41 0 9492 0
vsize: 38132
[startup+1030.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 103020 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223712 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1040.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 104020 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223728 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1050.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 105020 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1060.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 106020 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1070.38 s]
Raw data (loadavg): 1.00 1.02 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 107021 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223712 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1080.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 108021 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1090.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 109021 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1100.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 110021 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1110.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5831
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 111021 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1120.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9119 0 0 0 112021 28 0 0 25 0 1 0 490220587 39317504 9095 4294967295 134512640 134672761 3221224528 3221223696 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 9095 603 41 0 9558 0
vsize: 38396
[startup+1130.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9143 0 0 0 113022 28 0 0 25 0 1 0 490220587 39473152 9119 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9119 603 41 0 9596 0
vsize: 38548
[startup+1140.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9144 0 0 0 114022 28 0 0 25 0 1 0 490220587 39473152 9120 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9120 603 41 0 9596 0
vsize: 38548
[startup+1150.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9145 0 0 0 115022 28 0 0 25 0 1 0 490220587 39473152 9121 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9121 603 41 0 9596 0
vsize: 38548
[startup+1160.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9151 0 0 0 116022 28 0 0 25 0 1 0 490220587 39473152 9127 4294967295 134512640 134672761 3221224528 3221223664 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9127 603 41 0 9596 0
vsize: 38548
[startup+1170.38 s]
Raw data (loadavg): 1.00 1.01 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9151 0 0 0 117022 28 0 0 25 0 1 0 490220587 39473152 9127 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9127 603 41 0 9596 0
vsize: 38548
[startup+1180.38 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9151 0 0 0 118022 28 0 0 25 0 1 0 490220587 39473152 9127 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9127 603 41 0 9596 0
vsize: 38548
[startup+1190.38 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9151 0 0 0 119023 28 0 0 25 0 1 0 490220587 39473152 9127 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9127 603 41 0 9596 0
vsize: 38548
[startup+1200.38 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 5833
Raw data (stat): 5776 (minisat+) R 5775 25347 25346 0 -1 0 9151 0 0 0 120023 28 0 0 25 0 1 0 490220587 39473152 9127 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9127 603 41 0 9596 0
vsize: 38548
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.4 s]
Raw data (loadavg): 1.00 1.00 0.97 1/54 5833
Raw data (stat): 5776 (minisat+) Z 5775 25347 25346 0 -1 12 9154 0 0 0 120023 30 0 0 25 0 1 0 490220587 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.4
CPU time (s): 1200.54
CPU user time (s): 1200.24
CPU system time (s): 0.301954
CPU usage (%): 100.012
Max. virtual memory (Kb): 38548
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####