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/submitted/een/normalized-p0282.opb
MD5SUM	dd62132555621025f45a5a6099c90742
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	258411
Optimality of the best value was proved	NO
Number of terms in the objective function	282
Biggest coefficient in the objective function	160646
Number of bits for the biggest coefficient in the objective function	18
Sum of the numbers in the objective function	1302615
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	160646
Number of bits of the biggest number in a constraint	18
Biggest sum of numbers in a constraint	1302615
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	282
Total number of constraints	221
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	44
Minimum length of a constraint	2
Maximum length of a constraint	57
Trace number 6995

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        864980 kB
Buffers:         36732 kB
Cached:         110360 kB
SwapCached:       2644 kB
Active:          59888 kB
Inactive:        92688 kB
HighTotal:      131008 kB
HighFree:        16772 kB
LowTotal:       903652 kB
LowFree:        848208 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11508 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:11:03 (client local time) WITH STATUS 10 IN 1200.42 SECONDS
stats: 5054 7 1200.42 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................sss
c ---[  46]---> Adder-cost: 7   maxlim: 3   bits: 3/2
c ---[  45]---> Adder-cost: 15   maxlim: 7   bits: 4/3
c ---[  44]---> Adder-cost: 20   maxlim: 9   bits: 5/4
c ---[  43]---> Adder-cost: 31   maxlim: 15   bits: 5/4
c ---[  42]---> Adder-cost: 126   maxlim: 188   bits: 9/8
c ---[  41]---> Adder-cost: 94   maxlim: 168   bits: 9/8
c ---[  40]---> Adder-cost: 120   maxlim: 202   bits: 9/8
c ---[  38]---> Adder-cost: 100   maxlim: 204   bits: 9/8
c ---[  37]---> Adder-cost: 98   maxlim: 224   bits: 9/8
c ---[  36]---> Adder-cost: 100   maxlim: 167   bits: 9/8
c ---[  35]---> Adder-cost: 102   maxlim: 187   bits: 9/8
c ---[  34]---> Adder-cost: 124   maxlim: 245   bits: 9/8
c ---[  33]---> Adder-cost: 104   maxlim: 265   bits: 10/9
c ---[  32]---> Adder-cost: 112   maxlim: 442   bits: 10/9
c ---[  31]---> Adder-cost: 110   maxlim: 182   bits: 9/8
c ---[  30]---> Adder-cost: 98   maxlim: 182   bits: 9/8
c ---[  29]---> Adder-cost: 102   maxlim: 138   bits: 9/8
c ---[  28]---> Adder-cost: 102   maxlim: 118   bits: 8/7
c ---[  27]---> Adder-cost: 108   maxlim: 267   bits: 10/9
c ---[  26]---> Adder-cost: 98   maxlim: 175   bits: 9/8
c ---[  25]---> Adder-cost: 98   maxlim: 155   bits: 9/8
c ---[  24]---> Adder-cost: 104   maxlim: 218   bits: 9/8
c ---[  23]---> Adder-cost: 98   maxlim: 192   bits: 9/8
c ---[  22]---> Adder-cost: 98   maxlim: 212   bits: 9/8
c ---[  21]---> Adder-cost: 102   maxlim: 178   bits: 9/8
c ---[  20]---> Adder-cost: 98   maxlim: 198   bits: 9/8
c ---[  19]---> Adder-cost: 100   maxlim: 529   bits: 10/10
c ---[  18]---> Adder-cost: 98   maxlim: 249   bits: 9/8
c ---[  17]---> Adder-cost: 104   maxlim: 198   bits: 9/8
c ---[  16]---> Adder-cost: 108   maxlim: 254   bits: 9/8
c ---[  15]---> Adder-cost: 100   maxlim: 234   bits: 9/8
c ---[  14]---> Adder-cost: 52   maxlim: 25   bits: 6/5
c ---[  13]---> Adder-cost: 123   maxlim: 341   bits: 10/9
c ---[  11]---> Adder-cost: 119   maxlim: 401   bits: 10/9
c ---[  10]---> Adder-cost: 119   maxlim: 161   bits: 9/8
c ---[   9]---> Adder-cost: 115   maxlim: 421   bits: 10/9
c ---[   8]---> Adder-cost: 115   maxlim: 141   bits: 9/8
c ---[   7]---> Adder-cost: 115   maxlim: 321   bits: 10/9
c ---[   5]---> Adder-cost: 112   maxlim: 55   bits: 7/6
c ---[   4]---> Adder-cost: 112   maxlim: 55   bits: 7/6
c ---[   3]---> Adder-cost: 112   maxlim: 55   bits: 7/6
c ---[   2]---> Adder-cost: 21   maxlim: 7   bits: 4/3
c ---[   1]---> Adder-cost: 83   maxlim: 81   bits: 8/7
c ---[   0]---> Adder-cost: 81   maxlim: 61   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27042    96123 |    9014       0        0     nan |  0.000 % |
c |       100 |   27042    96123 |    9915     100      728     7.3 |  4.011 % |
c |       250 |   27042    96123 |   10906     250     2434     9.7 |  4.011 % |
c |       475 |   27042    96123 |   11997     475     4721     9.9 |  4.011 % |
c |       813 |   27042    96123 |   13197     813     8577    10.5 |  4.011 % |
c |      1319 |   27042    96123 |   14517    1319    15433    11.7 |  4.011 % |
c |      2078 |   27042    96123 |   15968    2078    25016    12.0 |  4.011 % |
c |      3219 |   27042    96123 |   17565    3219    40783    12.7 |  4.011 % |
c ==============================================================================
c [1mFound solution: 459651[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2436   maxlim: 842964   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4604 |   44007   156752 |   14669    4604    64105    13.9 |  4.011 % |
c |      4704 |   44007   156752 |   16135    4704    65336    13.9 |  2.777 % |
c |      4855 |   44007   156752 |   17749    4855    68482    14.1 |  2.777 % |
c |      5081 |   44007   156752 |   19524    5081    69803    13.7 |  2.777 % |
c |      5418 |   44007   156752 |   21476    5418    73396    13.5 |  2.777 % |
c |      5924 |   44007   156752 |   23624    5924    79973    13.5 |  2.777 % |
c |      6685 |   44007   156752 |   25987    6685    94282    14.1 |  2.777 % |
c |      7824 |   44007   156752 |   28585    7824   117229    15.0 |  2.777 % |
c |      9532 |   44007   156752 |   31444    9532   143360    15.0 |  2.777 % |
c |     12094 |   44007   156752 |   34588   12094   217896    18.0 |  2.777 % |
c |     15938 |   44007   156752 |   38047   15938   339356    21.3 |  2.777 % |
c |     21707 |   44007   156752 |   41852   21707   801974    36.9 |  2.777 % |
c |     30356 |   44007   156752 |   46037   30356  1137422    37.5 |  2.777 % |
c |     43330 |   44007   156752 |   50641   43330  1630269    37.6 |  2.777 % |
c ==============================================================================
c [1mFound solution: 458755[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 843860   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59880 |   44019   156859 |   14673   21477  1419466    66.1 |  2.777 % |
c |     59980 |   44019   156859 |   16140   10839   828558    76.4 |  2.846 % |
c |     60130 |   44019   156859 |   17754   10989   829403    75.5 |  2.846 % |
c |     60355 |   44019   156859 |   19529   11214   831486    74.1 |  2.846 % |
c |     60695 |   44019   156859 |   21482   11554   835689    72.3 |  2.846 % |
c |     61201 |   44019   156859 |   23631   12060   842226    69.8 |  2.846 % |
c |     61960 |   44019   156859 |   25994   12819   854125    66.6 |  2.846 % |
c |     63099 |   44019   156859 |   28593   13958   901211    64.6 |  2.846 % |
c |     64807 |   44019   156859 |   31452   15666   974351    62.2 |  2.846 % |
c |     67369 |   44019   156859 |   34598   18228  1063027    58.3 |  2.846 % |
c ==============================================================================
c [1mFound solution: 438303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 864312   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70590 |   44034   156988 |   14678   21449  1216621    56.7 |  2.846 % |
c |     70691 |   44034   156988 |   16145   10826   371441    34.3 |  2.943 % |
c |     70842 |   44034   156988 |   17760   10977   372984    34.0 |  2.943 % |
c |     71068 |   44034   156988 |   19536   11203   377133    33.7 |  2.943 % |
c |     71406 |   44034   156988 |   21490   11541   384131    33.3 |  2.943 % |
c |     71912 |   44034   156988 |   23639   12047   399189    33.1 |  2.943 % |
c |     72671 |   44034   156988 |   26002   12806   416805    32.5 |  2.943 % |
c |     73812 |   44034   156988 |   28603   13947   462826    33.2 |  2.943 % |
c |     75520 |   44034   156988 |   31463   15655   507676    32.4 |  2.943 % |
c |     78083 |   44034   156988 |   34609   18218   600193    32.9 |  2.943 % |
c |     81927 |   44034   156988 |   38070   22062   792000    35.9 |  2.943 % |
c |     87694 |   44034   156988 |   41878   27829  1063212    38.2 |  2.943 % |
c ==============================================================================
c [1mFound solution: 421893[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 880722   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89671 |   44047   157111 |   14682   29806  1157272    38.8 |  2.943 % |
c |     89772 |   44047   157111 |   16150   13976   551947    39.5 |  3.039 % |
c |     89922 |   44047   157111 |   17765   14126   553638    39.2 |  3.039 % |
c |     90147 |   44047   157111 |   19541   14351   556139    38.8 |  3.039 % |
c |     90486 |   44047   157111 |   21495   14690   563159    38.3 |  3.039 % |
c |     90992 |   44047   157111 |   23645   15196   577851    38.0 |  3.039 % |
c |     91751 |   44047   157111 |   26010   15955   596928    37.4 |  3.039 % |
c |     92890 |   44047   157111 |   28611   17094   623507    36.5 |  3.039 % |
c |     94599 |   44047   157111 |   31472   18803   687380    36.6 |  3.039 % |
c |     97163 |   44047   157111 |   34619   21367   782119    36.6 |  3.039 % |
c |    101007 |   44047   157111 |   38081   25211   932790    37.0 |  3.039 % |
c |    106773 |   44047   157111 |   41889   30977  1214694    39.2 |  3.039 % |
c |    115422 |   44047   157111 |   46078   39626  1630388    41.1 |  3.039 % |
c |    128396 |   44047   157111 |   50686   21377   792735    37.1 |  3.039 % |
c |    147857 |   44047   157111 |   55754   40838  2347305    57.5 |  3.039 % |
c |    177050 |   44047   157111 |   61330   26230  1502171    57.3 |  3.039 % |
c |    220841 |   44047   157111 |   67463   22264  1361649    61.2 |  3.039 % |
c |    286526 |   44047   157111 |   74209   33279  2388822    71.8 |  3.039 % |
c |    385053 |   44047   157111 |   81630   72489  6345999    87.5 |  3.039 % |
c ==============================================================================
c [1mFound solution: 417877[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 884738   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    472196 |   44052   157165 |   14684   19748  2073303   105.0 |  3.039 % |
c |    472296 |   44052   157165 |   16152    9974  1079794   108.3 |  3.080 % |
c |    472446 |   44052   157165 |   17767   10124  1081040   106.8 |  3.080 % |
c |    472671 |   44052   157165 |   19544   10349  1083778   104.7 |  3.080 % |
c |    473008 |   44052   157165 |   21498   10686  1086916   101.7 |  3.080 % |
c |    473515 |   44052   157165 |   23648   11193  1094577    97.8 |  3.080 % |
c |    474274 |   44052   157165 |   26013   11952  1104413    92.4 |  3.080 % |
c |    475413 |   44052   157165 |   28614   13091  1134590    86.7 |  3.080 % |
c |    477121 |   44052   157165 |   31476   14799  1174490    79.4 |  3.080 % |
c |    479683 |   44052   157165 |   34624   17361  1243169    71.6 |  3.080 % |
c |    483528 |   44052   157165 |   38086   21206  1405402    66.3 |  3.080 % |
c |    489298 |   44052   157165 |   41895   26976  1657352    61.4 |  3.080 % |
c |    497947 |   44052   157165 |   46084   35625  2163015    60.7 |  3.080 % |
c ==============================================================================
c [1mFound solution: 399576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 903039   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    509218 |   44061   157239 |   14687   46896  2804741    59.8 |  3.080 % |
c |    509319 |   44061   157239 |   16155   14424   687084    47.6 |  3.149 % |
c |    509470 |   44061   157239 |   17771   14575   688840    47.3 |  3.149 % |
c |    509695 |   44061   157239 |   19548   14800   692904    46.8 |  3.149 % |
c |    510032 |   44061   157239 |   21503   15137   697245    46.1 |  3.149 % |
c |    510539 |   44061   157239 |   23653   15644   713752    45.6 |  3.149 % |
c |    511298 |   44061   157239 |   26018   16403   727236    44.3 |  3.149 % |
c |    512438 |   44061   157239 |   28620   17543   767652    43.8 |  3.149 % |
c |    514146 |   44061   157239 |   31482   19251   849018    44.1 |  3.149 % |
c |    516708 |   44061   157239 |   34631   21813   918130    42.1 |  3.149 % |
c |    520553 |   44061   157239 |   38094   25658  1102418    43.0 |  3.149 % |
c |    526320 |   44061   157239 |   41903   31425  1485501    47.3 |  3.149 % |
c |    534969 |   44061   157239 |   46094   40074  1881218    46.9 |  3.149 % |
c |    547944 |   44061   157239 |   50703   20156  1022486    50.7 |  3.149 % |
c |    567405 |   44061   157239 |   55773   39617  2339570    59.1 |  3.149 % |
c |    596598 |   44061   157239 |   61351   25837  1463942    56.7 |  3.149 % |
c |    640387 |   44061   157239 |   67486   21957  2507793   114.2 |  3.149 % |
c |    706071 |   44061   157239 |   74235   33692  2075700    61.6 |  3.149 % |
c ==============================================================================
c [1mFound solution: 368313[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 934302   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    708539 |   44074   157397 |   14691   36160  2130179    58.9 |  3.149 % |
c |    708640 |   44074   157397 |   16160    8026   282110    35.1 |  3.273 % |
c |    708793 |   44074   157397 |   17776    8179   285268    34.9 |  3.273 % |
c |    709020 |   44074   157397 |   19553    8406   288356    34.3 |  3.273 % |
c |    709357 |   44074   157397 |   21509    8743   295269    33.8 |  3.273 % |
c |    709863 |   44074   157397 |   23660    9249   310886    33.6 |  3.273 % |
c |    710623 |   44074   157397 |   26026   10009   333890    33.4 |  3.273 % |
c |    711762 |   44074   157397 |   28628   11148   378821    34.0 |  3.273 % |
c |    713470 |   44074   157397 |   31491   12856   477496    37.1 |  3.273 % |
c |    716032 |   44074   157397 |   34640   15418   542578    35.2 |  3.273 % |
c |    719878 |   44074   157397 |   38104   19264   698326    36.3 |  3.273 % |
c |    725644 |   44074   157397 |   41915   25030   927025    37.0 |  3.273 % |
c |    734294 |   44074   157397 |   46106   33680  1324406    39.3 |  3.273 % |
c |    747269 |   44074   157397 |   50717   46655  2050549    44.0 |  3.273 % |
c |    766731 |   44074   157397 |   55789   29408  1551539    52.8 |  3.273 % |
c |    795923 |   44074   157397 |   61367   16486   751524    45.6 |  3.273 % |
c |    839713 |   44074   157397 |   67504   60276  3274329    54.3 |  3.273 % |
c |    905398 |   44074   157397 |   74255   19792  1494938    75.5 |  3.273 % |
#### 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.85 0.94 0.69 2/54 6729
Raw data (stat): 6729 (runsolver) D 6728 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429386865 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.69 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 1995 0 0 0 992 5 0 0 25 0 1 0 429386865 9846784 1972 4294967295 134512640 134672761 3221224576 3221223760 134558846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2404 1972 603 41 0 2363 0
vsize: 9616
[startup+20.001 s]
Raw data (loadavg): 0.89 0.94 0.69 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 2776 0 0 0 1991 7 0 0 25 0 1 0 429386865 13082624 2753 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3194 2753 603 41 0 3153 0
vsize: 12776
[startup+30.001 s]
Raw data (loadavg): 0.91 0.94 0.70 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3479 0 0 0 2988 9 0 0 25 0 1 0 429386865 15917056 3456 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3886 3456 603 41 0 3845 0
vsize: 15544
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.70 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3946 0 0 0 3987 10 0 0 25 0 1 0 429386865 17805312 3923 4294967295 134512640 134672761 3221224576 3221223760 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4347 3923 603 41 0 4306 0
vsize: 17388
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.94 0.70 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3998 0 0 0 4987 11 0 0 25 0 1 0 429386865 18259968 3975 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4458 3975 603 41 0 4417 0
vsize: 17832
[startup+60.0015 s]
Raw data (loadavg): 0.94 0.95 0.70 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3999 0 0 0 5987 11 0 0 25 0 1 0 429386865 18259968 3976 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4458 3976 603 41 0 4417 0
vsize: 17832
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.95 0.71 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3999 0 0 0 6987 11 0 0 25 0 1 0 429386865 18259968 3976 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4458 3976 603 41 0 4417 0
vsize: 17832
[startup+80.0019 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3999 0 0 0 7987 11 0 0 25 0 1 0 429386865 18259968 3976 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4458 3976 603 41 0 4417 0
vsize: 17832
[startup+90.0017 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3999 0 0 0 8988 11 0 0 25 0 1 0 429386865 18259968 3976 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4458 3976 603 41 0 4417 0
vsize: 17832
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 3999 0 0 0 9988 11 0 0 25 0 1 0 429386865 18259968 3976 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4458 3976 603 41 0 4417 0
vsize: 17832
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 4046 0 0 0 10989 11 0 0 25 0 1 0 429386865 18395136 4023 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4491 4023 603 41 0 4450 0
vsize: 17964
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 4651 0 0 0 11988 12 0 0 25 0 1 0 429386865 20819968 4628 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5083 4628 603 41 0 5042 0
vsize: 20332
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 5149 0 0 0 12986 14 0 0 25 0 1 0 429386865 22839296 5126 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5576 5126 603 41 0 5535 0
vsize: 22304
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 5149 0 0 0 13986 14 0 0 25 0 1 0 429386865 22839296 5126 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5576 5126 603 41 0 5535 0
vsize: 22304
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 5149 0 0 0 14987 14 0 0 25 0 1 0 429386865 22839296 5126 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5576 5126 603 41 0 5535 0
vsize: 22304
[startup+160.004 s]
Raw data (loadavg): 0.99 0.95 0.73 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 5149 0 0 0 15987 14 0 0 25 0 1 0 429386865 22839296 5126 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5576 5126 603 41 0 5535 0
vsize: 22304
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 5155 0 0 0 16987 14 0 0 25 0 1 0 429386865 22974464 5132 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5609 5132 603 41 0 5568 0
vsize: 22436
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 5641 0 0 0 17986 16 0 0 25 0 1 0 429386865 24870912 5618 4294967295 134512640 134672761 3221224576 3221223680 134560070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6072 5618 603 41 0 6031 0
vsize: 24288
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6086 0 0 0 18985 17 0 0 25 0 1 0 429386865 26763264 6063 4294967295 134512640 134672761 3221224576 3221223712 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6534 6063 603 41 0 6493 0
vsize: 26136
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6303 0 0 0 19984 18 0 0 25 0 1 0 429386865 27574272 6280 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6280 603 41 0 6691 0
vsize: 26928
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6303 0 0 0 20984 18 0 0 25 0 1 0 429386865 27574272 6280 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6280 603 41 0 6691 0
vsize: 26928
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6303 0 0 0 21984 18 0 0 25 0 1 0 429386865 27574272 6280 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6280 603 41 0 6691 0
vsize: 26928
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6303 0 0 0 22985 18 0 0 25 0 1 0 429386865 27574272 6280 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6280 603 41 0 6691 0
vsize: 26928
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6303 0 0 0 23985 18 0 0 25 0 1 0 429386865 27574272 6280 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6280 603 41 0 6691 0
vsize: 26928
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6312 0 0 0 24985 19 0 0 25 0 1 0 429386865 27746304 6289 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6289 603 41 0 6733 0
vsize: 27096
[startup+260.006 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6320 0 0 0 25986 19 0 0 25 0 1 0 429386865 28008448 6297 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6838 6297 603 41 0 6797 0
vsize: 27352
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6320 0 0 0 26986 19 0 0 25 0 1 0 429386865 28008448 6297 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6838 6297 603 41 0 6797 0
vsize: 27352
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6320 0 0 0 27986 19 0 0 25 0 1 0 429386865 28008448 6297 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6838 6297 603 41 0 6797 0
vsize: 27352
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6320 0 0 0 28987 19 0 0 25 0 1 0 429386865 28008448 6297 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6838 6297 603 41 0 6797 0
vsize: 27352
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6320 0 0 0 29987 19 0 0 25 0 1 0 429386865 28008448 6297 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6838 6297 603 41 0 6797 0
vsize: 27352
[startup+310.006 s]
Raw data (loadavg): 1.07 0.99 0.77 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6472 0 0 0 30987 19 0 0 25 0 1 0 429386865 28540928 6449 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6449 603 41 0 6927 0
vsize: 27872
[startup+320.006 s]
Raw data (loadavg): 1.06 0.99 0.77 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 6887 0 0 0 31986 20 0 0 25 0 1 0 429386865 30298112 6864 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7397 6865 603 41 0 7356 0
vsize: 29588
[startup+330.007 s]
Raw data (loadavg): 1.05 0.99 0.77 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7358 0 0 0 32985 21 0 0 25 0 1 0 429386865 32178176 7335 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7856 7335 603 41 0 7815 0
vsize: 31424
[startup+340.007 s]
Raw data (loadavg): 1.04 0.99 0.77 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 33984 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+350.008 s]
Raw data (loadavg): 1.03 0.99 0.77 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 34985 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+360.009 s]
Raw data (loadavg): 1.03 0.99 0.78 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 35985 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223760 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+370.009 s]
Raw data (loadavg): 1.02 0.99 0.78 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 36985 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+380.009 s]
Raw data (loadavg): 1.02 0.99 0.78 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 37986 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+390.009 s]
Raw data (loadavg): 1.02 0.99 0.78 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 38986 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+400.009 s]
Raw data (loadavg): 1.01 0.99 0.78 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 39986 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+410.01 s]
Raw data (loadavg): 1.01 0.99 0.79 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7755 0 0 0 40987 23 0 0 25 0 1 0 429386865 33800192 7732 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7732 603 41 0 8211 0
vsize: 33008
[startup+420.01 s]
Raw data (loadavg): 1.01 0.99 0.79 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 7876 0 0 0 41987 23 0 0 25 0 1 0 429386865 34332672 7853 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8382 7853 603 41 0 8341 0
vsize: 33528
[startup+430.011 s]
Raw data (loadavg): 1.01 0.99 0.79 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 8336 0 0 0 42986 24 0 0 25 0 1 0 429386865 36192256 8313 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8836 8313 603 41 0 8795 0
vsize: 35344
[startup+440.011 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 8704 0 0 0 43985 26 0 0 25 0 1 0 429386865 37683200 8681 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9200 8681 603 41 0 9159 0
vsize: 36800
[startup+450.011 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9040 0 0 0 44984 28 0 0 25 0 1 0 429386865 39157760 9017 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9560 9017 603 41 0 9519 0
vsize: 38240
[startup+460.011 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9483 0 0 0 45982 29 0 0 25 0 1 0 429386865 40906752 9460 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9987 9460 603 41 0 9946 0
vsize: 39948
[startup+470.012 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 46981 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+480.012 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 47981 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+490.012 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 48981 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223712 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+500.012 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 49982 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+510.012 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 50982 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+520.012 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 51982 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223760 134559592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+530.013 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 52983 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+540.014 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 6729
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 53983 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+550.014 s]
Raw data (loadavg): 1.08 1.00 0.82 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 54984 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+560.014 s]
Raw data (loadavg): 1.07 1.00 0.82 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 55984 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+570.015 s]
Raw data (loadavg): 1.06 1.00 0.82 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 56984 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+580.015 s]
Raw data (loadavg): 1.05 1.00 0.82 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 9834 0 0 0 57985 31 0 0 25 0 1 0 429386865 42389504 9811 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10349 9811 603 41 0 10308 0
vsize: 41396
[startup+590.015 s]
Raw data (loadavg): 1.04 1.00 0.82 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10326 0 0 0 58983 32 0 0 25 0 1 0 429386865 44404736 10303 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10841 10303 603 41 0 10800 0
vsize: 43364
[startup+600.016 s]
Raw data (loadavg): 1.03 1.00 0.82 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 59983 33 0 0 25 0 1 0 429386865 44539904 10337 4294967295 134512640 134672761 3221224576 3221223744 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10874 10337 603 41 0 10833 0
vsize: 43496
[startup+610.017 s]
Raw data (loadavg): 1.03 1.00 0.82 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 60983 33 0 0 25 0 1 0 429386865 44539904 10337 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10337 603 41 0 10833 0
vsize: 43496
[startup+620.017 s]
Raw data (loadavg): 1.02 1.00 0.83 2/54 6782
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 61984 33 0 0 25 0 1 0 429386865 44539904 10337 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10337 603 41 0 10833 0
vsize: 43496
[startup+630.017 s]
Raw data (loadavg): 1.02 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 62984 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223760 134559334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+640.018 s]
Raw data (loadavg): 1.02 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 63984 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223680 134560501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+650.018 s]
Raw data (loadavg): 1.01 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 64985 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+660.018 s]
Raw data (loadavg): 1.01 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 65985 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+670.019 s]
Raw data (loadavg): 1.01 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 66985 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+680.019 s]
Raw data (loadavg): 1.01 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 67986 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+690.02 s]
Raw data (loadavg): 1.00 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 68986 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+700.02 s]
Raw data (loadavg): 1.00 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 69987 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+710.021 s]
Raw data (loadavg): 1.00 1.00 0.83 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 70987 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+720.021 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 71987 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+730.021 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 72988 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223712 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+740.021 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 73988 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+750.021 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 74988 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+760.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 75989 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+770.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 76989 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+780.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 77989 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+790.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 78990 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+800.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 79990 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+810.022 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 80990 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+820.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 81992 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+830.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 82992 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223680 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+840.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 83992 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+850.032 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6784
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 84993 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+860.032 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 85993 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+870.032 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 86993 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+880.033 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 87994 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+890.034 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10360 0 0 0 88994 33 0 0 25 0 1 0 429386865 44466176 10337 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10337 603 41 0 10815 0
vsize: 43424
[startup+900.035 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 89995 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+910.036 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 90995 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+920.037 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 91996 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+930.037 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 92996 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+940.038 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 93996 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+950.039 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 94997 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+960.041 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 95997 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+970.041 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 96997 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+980.041 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 97998 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+990.042 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 98998 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 99999 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 100999 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 101999 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 103000 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 104000 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 105000 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 106001 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 107001 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 108001 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 109002 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 110002 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 111003 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 112003 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 113003 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 114004 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 115004 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 116004 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 117005 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 118005 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 119006 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 6786
Raw data (stat): 6729 (minisat+) R 6728 29653 29652 0 -1 0 10361 0 0 0 120006 33 0 0 25 0 1 0 429386865 44466176 10338 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10856 10338 603 41 0 10815 0
vsize: 43424
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.88 1/54 6786
Raw data (stat): 6729 (minisat+) Z 6728 29653 29652 0 -1 12 10364 0 0 0 120006 35 0 0 25 0 1 0 429386865 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.07
CPU time (s): 1200.42
CPU user time (s): 1200.07
CPU system time (s): 0.351946
CPU usage (%): 100.029
Max. virtual memory (Kb): 43496
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####