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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sentoy.opb
MD5SUM	4df3e7eb358d27d446e34b975724a6c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-7772
Optimality of the best value was proved	NO
Number of terms in the objective function	60
Biggest coefficient in the objective function	974
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	9460
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	6000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	26162
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	60
Total number of constraints	90
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	30
Minimum length of a constraint	1
Maximum length of a constraint	60
Trace number 18944

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 17:09:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17264 boxname=wulflinc30 idbench=1328 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-sentoy.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-sentoy.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-sentoy.opb
IDLAUNCH: 17264
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        847620 kB
Buffers:          7200 kB
Cached:         152572 kB
SwapCached:         28 kB
Active:          49760 kB
Inactive:       112772 kB
HighTotal:      131008 kB
HighFree:        15092 kB
LowTotal:       903652 kB
LowFree:        832528 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18860 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:29:17 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 17264 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> Adder-cost: 448   maxlim: 11620   bits: 15/14
c ---[  28]---> Adder-cost: 408   maxlim: 6087   bits: 14/13
c ---[  27]---> Adder-cost: 432   maxlim: 9310   bits: 14/14
c ---[  26]---> Adder-cost: 468   maxlim: 11096   bits: 15/14
c ---[  25]---> Adder-cost: 444   maxlim: 10275   bits: 14/14
c ---[  24]---> Adder-cost: 458   maxlim: 10302   bits: 14/14
c ---[  23]---> Adder-cost: 436   maxlim: 13436   bits: 15/14
c ---[  22]---> Adder-cost: 428   maxlim: 9755   bits: 14/14
c ---[  21]---> Adder-cost: 412   maxlim: 6448   bits: 14/13
c ---[  20]---> Adder-cost: 464   maxlim: 10002   bits: 14/14
c ---[  19]---> Adder-cost: 426   maxlim: 9583   bits: 14/14
c ---[  18]---> Adder-cost: 424   maxlim: 9848   bits: 14/14
c ---[  17]---> Adder-cost: 364   maxlim: 5722   bits: 14/13
c ---[  16]---> Adder-cost: 452   maxlim: 10594   bits: 15/14
c ---[  15]---> Adder-cost: 434   maxlim: 10081   bits: 14/14
c ---[  14]---> Adder-cost: 442   maxlim: 9196   bits: 14/14
c ---[  13]---> Adder-cost: 456   maxlim: 12391   bits: 15/14
c ---[  12]---> Adder-cost: 450   maxlim: 14161   bits: 15/14
c ---[  11]---> Adder-cost: 418   maxlim: 12220   bits: 15/14
c ---[  10]---> Adder-cost: 420   maxlim: 12782   bits: 15/14
c ---[   9]---> Adder-cost: 460   maxlim: 11486   bits: 15/14
c ---[   8]---> Adder-cost: 436   maxlim: 8903   bits: 14/14
c ---[   7]---> Adder-cost: 456   maxlim: 10103   bits: 14/14
c ---[   6]---> Adder-cost: 380   maxlim: 6238   bits: 14/13
c ---[   5]---> Adder-cost: 430   maxlim: 10469   bits: 15/14
c ---[   4]---> Adder-cost: 438   maxlim: 9149   bits: 14/14
c ---[   3]---> Adder-cost: 420   maxlim: 13773   bits: 15/14
c ---[   2]---> Adder-cost: 448   maxlim: 9436   bits: 14/14
c ---[   1]---> Adder-cost: 456   maxlim: 8907   bits: 14/14
c ---[   0]---> Adder-cost: 408   maxlim: 13608   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   89887   321260 |   29962       0        0     nan |  0.000 % |
c |       100 |   89881   321243 |   32958      98      375     3.8 |  1.719 % |
c |       250 |   89881   321243 |   36254     248     6817    27.5 |  1.719 % |
c |       478 |   89881   321243 |   39879     476    12453    26.2 |  1.719 % |
c |       815 |   89881   321243 |   43867     813    19283    23.7 |  1.719 % |
c |      1321 |   89881   321243 |   48254    1319    34926    26.5 |  1.719 % |
c |      2081 |   89881   321243 |   53079    2079    62220    29.9 |  1.719 % |
c |      3221 |   89881   321243 |   58387    3219   110152    34.2 |  1.719 % |
c ==============================================================================
c [1mFound solution: -2805[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6599     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3809 |  107810   363266 |   35936    3807   142479    37.4 |  1.719 % |
c |      3909 |  107810   363266 |   39529    3907   145347    37.2 |  1.196 % |
c |      4061 |  107810   363266 |   43482    4059   147402    36.3 |  1.196 % |
c |      4286 |  107810   363266 |   47830    4284   155456    36.3 |  1.196 % |
c |      4623 |  107810   363266 |   52613    4621   160509    34.7 |  1.196 % |
c ==============================================================================
c [1mFound solution: -3139[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4738 |  108736   365525 |   36245    4736   162547    34.3 |  1.196 % |
c |      4838 |  108736   365525 |   39869    4836   163678    33.8 |  1.185 % |
c |      4988 |  108736   365525 |   43856    4986   169606    34.0 |  1.185 % |
c |      5216 |  108736   365525 |   48242    5214   177174    34.0 |  1.185 % |
c |      5553 |  108736   365525 |   53066    5551   181565    32.7 |  1.185 % |
c ==============================================================================
c [1mFound solution: -4552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5758 |  108892   365929 |   36297    5756   188668    32.8 |  1.185 % |
c |      5859 |  108892   365929 |   39926    5857   189912    32.4 |  1.188 % |
c |      6009 |  108892   365929 |   43919    6007   191748    31.9 |  1.188 % |
c |      6234 |  108892   365929 |   48311    6232   195100    31.3 |  1.188 % |
c |      6572 |  108892   365929 |   53142    6570   202187    30.8 |  1.188 % |
c |      7079 |  108892   365929 |   58456    7077   208357    29.4 |  1.188 % |
c |      7838 |  108892   365929 |   64302    7836   241831    30.9 |  1.188 % |
c |      8977 |  108892   365929 |   70732    8975   283161    31.5 |  1.188 % |
c |     10687 |  108880   365895 |   77805   10683   345666    32.4 |  1.198 % |
c |     13249 |  108880   365895 |   85586   13245   541921    40.9 |  1.198 % |
c |     17093 |  108880   365895 |   94145   17089   674244    39.5 |  1.198 % |
c ==============================================================================
c [1mFound solution: -4901[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17469 |  108932   366021 |   36310   17465   688275    39.4 |  1.198 % |
c |     17569 |  108932   366021 |   39941   17565   695956    39.6 |  1.203 % |
c |     17721 |  108932   366021 |   43935   17717   698585    39.4 |  1.203 % |
c |     17946 |  108932   366021 |   48328   17942   705102    39.3 |  1.203 % |
c |     18283 |  108932   366021 |   53161   18279   717123    39.2 |  1.203 % |
c |     18790 |  108926   366004 |   58477   18785   728777    38.8 |  1.208 % |
c |     19550 |  108926   366004 |   64325   19545   768406    39.3 |  1.208 % |
c |     20690 |  108926   366004 |   70757   20685   809530    39.1 |  1.208 % |
c ==============================================================================
c [1mFound solution: -4916[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21479 |  108955   366081 |   36318   21474   859230    40.0 |  1.208 % |
c |     21579 |  108955   366081 |   39949   21574   860128    39.9 |  1.212 % |
c |     21729 |  108955   366081 |   43944   21724   867169    39.9 |  1.212 % |
c |     21954 |  108955   366081 |   48339   21949   875343    39.9 |  1.212 % |
c |     22291 |  108955   366081 |   53173   22286   887342    39.8 |  1.212 % |
c |     22798 |  108955   366081 |   58490   22793   896559    39.3 |  1.212 % |
c |     23558 |  108955   366081 |   64339   23553   928568    39.4 |  1.212 % |
c |     24697 |  108955   366081 |   70773   24692   973304    39.4 |  1.212 % |
c |     26406 |  108955   366081 |   77850   26401  1037270    39.3 |  1.212 % |
c |     28968 |  108955   366081 |   85635   28963  1142553    39.4 |  1.212 % |
c |     32814 |  108949   366064 |   94199   32808  1280274    39.0 |  1.218 % |
c |     38580 |  108949   366064 |  103619   38574  1657414    43.0 |  1.218 % |
c |     47230 |  108949   366064 |  113981   47224  2148043    45.5 |  1.218 % |
c |     60204 |  108949   366064 |  125379   60198  2815717    46.8 |  1.218 % |
c ==============================================================================
c [1mFound solution: -4952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65682 |  108963   366098 |   36321   65676  3226282    49.1 |  1.218 % |
c |     65782 |  108963   366098 |   39953   14953   778783    52.1 |  1.222 % |
c |     65934 |  108963   366098 |   43948   15105   790171    52.3 |  1.222 % |
c |     66160 |  108963   366098 |   48343   15331   795346    51.9 |  1.222 % |
c |     66497 |  108963   366098 |   53177   15668   810254    51.7 |  1.222 % |
c |     67003 |  108963   366098 |   58495   16174   815242    50.4 |  1.222 % |
c |     67762 |  108963   366098 |   64344   16933   855550    50.5 |  1.222 % |
c |     68901 |  108963   366098 |   70779   18072   883689    48.9 |  1.222 % |
c |     70611 |  108963   366098 |   77857   19782   947484    47.9 |  1.222 % |
c |     73173 |  108963   366098 |   85643   22344  1024533    45.9 |  1.222 % |
c ==============================================================================
c [1mFound solution: -5237[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75127 |  109012   366221 |   36337   24298  1170928    48.2 |  1.222 % |
c |     75227 |  109012   366221 |   39970   24398  1172650    48.1 |  1.227 % |
c |     75378 |  109012   366221 |   43967   24549  1177146    48.0 |  1.227 % |
c ==============================================================================
c [1mFound solution: -5381[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75575 |  109025   366256 |   36341   24746  1180432    47.7 |  1.227 % |
c ==============================================================================
c [1mFound solution: -5741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75668 |  109068   366363 |   36356   24839  1181650    47.6 |  1.227 % |
c |     75769 |  109068   366363 |   39991   24940  1186128    47.6 |  1.236 % |
c |     75919 |  109068   366363 |   43990   25090  1188430    47.4 |  1.236 % |
c |     76144 |  109068   366363 |   48389   25315  1197760    47.3 |  1.236 % |
c |     76481 |  109068   366363 |   53228   25652  1208336    47.1 |  1.236 % |
c |     76987 |  109068   366363 |   58551   26158  1225547    46.9 |  1.236 % |
c |     77747 |  109068   366363 |   64406   26918  1261049    46.8 |  1.236 % |
c |     78886 |  109068   366363 |   70847   28057  1299844    46.3 |  1.236 % |
c |     80594 |  109068   366363 |   77932   29765  1412864    47.5 |  1.236 % |
c |     83156 |  109068   366363 |   85725   32327  1540852    47.7 |  1.236 % |
c |     87000 |  109068   366363 |   94298   36171  1734898    48.0 |  1.236 % |
c |     92766 |  109068   366363 |  103727   41937  1973278    47.1 |  1.236 % |
c ==============================================================================
c [1mFound solution: -5831[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95631 |  109084   366403 |   36361   44802  2200136    49.1 |  1.236 % |
c |     95731 |  109084   366403 |   39997   14978   623798    41.6 |  1.241 % |
c |     95882 |  109084   366403 |   43996   15129   627325    41.5 |  1.241 % |
c |     96108 |  109084   366403 |   48396   15355   637107    41.5 |  1.241 % |
c |     96445 |  109084   366403 |   53236   15692   656181    41.8 |  1.241 % |
c |     96952 |  109084   366403 |   58559   16199   672865    41.5 |  1.241 % |
c |     97711 |  109084   366403 |   64415   16958   712904    42.0 |  1.241 % |
c |     98850 |  109084   366403 |   70857   18097   731145    40.4 |  1.241 % |
c |    100558 |  109084   366403 |   77943   19805   753762    38.1 |  1.241 % |
c |    103120 |  109084   366403 |   85737   22367   891180    39.8 |  1.241 % |
c |    106964 |  109084   366403 |   94311   26211  1228122    46.9 |  1.241 % |
c |    112731 |  109084   366403 |  103742   31978  1634045    51.1 |  1.241 % |
c |    121381 |  109084   366403 |  114116   40628  2039159    50.2 |  1.241 % |
c |    134357 |  109084   366403 |  125528   53604  2822241    52.6 |  1.241 % |
c |    153820 |  109078   366386 |  138080   73066  3936065    53.9 |  1.246 % |
c |    183012 |  109078   366386 |  151888  102258  6352473    62.1 |  1.246 % |
c ==============================================================================
c [1mFound solution: -6489[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    189797 |  109143   366543 |   36381  109043  6764950    62.0 |  1.246 % |
c |    189899 |  109143   366543 |   40019   18632   990957    53.2 |  1.249 % |
c |    190051 |  109143   366543 |   44021   18784   994505    52.9 |  1.249 % |
c |    190280 |  109143   366543 |   48423   19013  1003162    52.8 |  1.249 % |
c |    190619 |  109143   366543 |   53265   19352  1014750    52.4 |  1.249 % |
c |    191125 |  109143   366543 |   58591   19858  1026113    51.7 |  1.249 % |
c |    191884 |  109143   366543 |   64451   20617  1040046    50.4 |  1.249 % |
c |    193023 |  109143   366543 |   70896   21756  1060561    48.7 |  1.249 % |
c |    194732 |  109143   366543 |   77985   23465  1113039    47.4 |  1.250 % |
c |    197294 |  109143   366543 |   85784   26027  1259614    48.4 |  1.250 % |
c |    201138 |  109143   366543 |   94362   29871  1482985    49.6 |  1.249 % |
c |    206904 |  109143   366543 |  103799   35637  1761450    49.4 |  1.249 % |
c |    215554 |  109143   366543 |  114179   44287  2119266    47.9 |  1.249 % |
#### 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.80 0.94 0.91 2/54 22858
Raw data (stat): 22858 (runsolver) R 22857 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546763198 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.83 0.94 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 2147 0 0 0 994 5 0 0 25 0 1 0 546763198 10514432 2073 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2567 2073 603 41 0 2526 0
vsize: 10268
[startup+20.002 s]
Raw data (loadavg): 0.86 0.94 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 2685 0 0 0 1992 7 0 0 25 0 1 0 546763198 13205504 2609 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3224 2609 603 41 0 3183 0
vsize: 12896
[startup+30.003 s]
Raw data (loadavg): 0.88 0.94 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 2848 0 0 0 2990 8 0 0 25 0 1 0 546763198 13955072 2772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3407 2772 603 41 0 3366 0
vsize: 13628
[startup+40.0036 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 2982 0 0 0 3990 9 0 0 25 0 1 0 546763198 14495744 2906 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3539 2906 603 41 0 3498 0
vsize: 14156
[startup+50.0043 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3090 0 0 0 4989 10 0 0 25 0 1 0 546763198 14893056 3014 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3636 3014 603 41 0 3595 0
vsize: 14544
[startup+60.0051 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3194 0 0 0 5988 11 0 0 25 0 1 0 546763198 15298560 3118 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3118 603 41 0 3694 0
vsize: 14940
[startup+70.0059 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3287 0 0 0 6987 12 0 0 25 0 1 0 546763198 15699968 3211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3833 3211 603 41 0 3792 0
vsize: 15332
[startup+80.0066 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3379 0 0 0 7987 12 0 0 25 0 1 0 546763198 16072704 3303 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3924 3303 603 41 0 3883 0
vsize: 15696
[startup+90.0077 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3478 0 0 0 8987 13 0 0 25 0 1 0 546763198 16478208 3402 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4023 3402 603 41 0 3982 0
vsize: 16092
[startup+100.008 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3609 0 0 0 9986 14 0 0 25 0 1 0 546763198 17014784 3533 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3533 603 41 0 4113 0
vsize: 16616
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3797 0 0 0 10985 15 0 0 25 0 1 0 546763198 17825792 3721 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4352 3721 603 41 0 4311 0
vsize: 17408
[startup+120.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3893 0 0 0 11984 16 0 0 25 0 1 0 546763198 18092032 3817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4417 3817 603 41 0 4376 0
vsize: 17668
[startup+130.01 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 3966 0 0 0 12984 16 0 0 25 0 1 0 546763198 18493440 3890 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4515 3890 603 41 0 4474 0
vsize: 18060
[startup+140.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4043 0 0 0 13984 17 0 0 25 0 1 0 546763198 18763776 3967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4581 3967 603 41 0 4540 0
vsize: 18324
[startup+150.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4183 0 0 0 14983 17 0 0 25 0 1 0 546763198 19427328 4107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4743 4107 603 41 0 4702 0
vsize: 18972
[startup+160.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4279 0 0 0 15983 18 0 0 25 0 1 0 546763198 19828736 4203 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4841 4203 603 41 0 4800 0
vsize: 19364
[startup+170.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4393 0 0 0 16982 18 0 0 25 0 1 0 546763198 20357120 4317 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4970 4317 603 41 0 4929 0
vsize: 19880
[startup+180.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4495 0 0 0 17982 19 0 0 25 0 1 0 546763198 20758528 4419 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5068 4419 603 41 0 5027 0
vsize: 20272
[startup+190.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4622 0 0 0 18981 20 0 0 25 0 1 0 546763198 21155840 4546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5165 4546 603 41 0 5124 0
vsize: 20660
[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4714 0 0 0 19981 20 0 0 25 0 1 0 546763198 21557248 4638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5263 4638 603 41 0 5222 0
vsize: 21052
[startup+210.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4801 0 0 0 20981 20 0 0 25 0 1 0 546763198 21954560 4725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5360 4725 603 41 0 5319 0
vsize: 21440
[startup+220.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4900 0 0 0 21981 20 0 0 25 0 1 0 546763198 22347776 4824 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5456 4824 603 41 0 5415 0
vsize: 21824
[startup+230.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 4998 0 0 0 22981 21 0 0 25 0 1 0 546763198 22749184 4922 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5554 4922 603 41 0 5513 0
vsize: 22216
[startup+240.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5077 0 0 0 23981 21 0 0 25 0 1 0 546763198 23015424 5001 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5619 5001 603 41 0 5578 0
vsize: 22476
[startup+250.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5204 0 0 0 24981 21 0 0 25 0 1 0 546763198 23572480 5128 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5755 5128 603 41 0 5714 0
vsize: 23020
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5312 0 0 0 25980 22 0 0 25 0 1 0 546763198 23977984 5236 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5854 5236 603 41 0 5813 0
vsize: 23416
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5426 0 0 0 26980 22 0 0 25 0 1 0 546763198 24506368 5350 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5983 5350 603 41 0 5942 0
vsize: 23932
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5534 0 0 0 27980 22 0 0 25 0 1 0 546763198 24907776 5458 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5458 603 41 0 6040 0
vsize: 24324
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5667 0 0 0 28980 23 0 0 25 0 1 0 546763198 25436160 5591 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6210 5591 603 41 0 6169 0
vsize: 24840
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5836 0 0 0 29979 24 0 0 25 0 1 0 546763198 26095616 5760 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5760 603 41 0 6330 0
vsize: 25484
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 5979 0 0 0 30979 24 0 0 25 0 1 0 546763198 26775552 5903 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6537 5903 603 41 0 6496 0
vsize: 26148
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6050 0 0 0 31979 24 0 0 25 0 1 0 546763198 27045888 5974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6603 5974 603 41 0 6562 0
vsize: 26412
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6143 0 0 0 32979 25 0 0 25 0 1 0 546763198 27447296 6067 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6701 6067 603 41 0 6660 0
vsize: 26804
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6228 0 0 0 33979 25 0 0 25 0 1 0 546763198 27713536 6152 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6766 6152 603 41 0 6725 0
vsize: 27064
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6305 0 0 0 34979 25 0 0 25 0 1 0 546763198 27979776 6229 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6831 6229 603 41 0 6790 0
vsize: 27324
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 35979 25 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 36979 25 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 37979 25 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 38979 25 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 39979 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 40980 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 41980 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223728 134559492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 42980 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 43980 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 44980 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 45981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 46981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 47981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 48981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 49981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 50981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 51981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+530.021 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 52981 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+540.022 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 53982 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+550.022 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 54982 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+560.023 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 55982 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+570.023 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 56982 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+580.022 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 57982 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+590.023 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 58983 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+600.034 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 59983 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+610.035 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 60983 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+620.035 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 61983 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+630.036 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 62984 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+640.036 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 63984 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223680 134560720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+650.036 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 64984 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+660.037 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 65984 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+670.037 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 66984 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+680.043 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 67985 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223728 134558341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+690.044 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 68985 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+700.045 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6374 0 0 0 69986 26 0 0 25 0 1 0 546763198 28614656 6298 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+710.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6413 0 0 0 70986 26 0 0 25 0 1 0 546763198 28762112 6337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7022 6337 603 41 0 6981 0
vsize: 28088
[startup+720.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6588 0 0 0 71985 27 0 0 25 0 1 0 546763198 29429760 6512 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7185 6512 603 41 0 7144 0
vsize: 28740
[startup+730.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6701 0 0 0 72985 27 0 0 25 0 1 0 546763198 29966336 6625 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7316 6625 603 41 0 7275 0
vsize: 29264
[startup+740.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 6905 0 0 0 73984 28 0 0 25 0 1 0 546763198 30769152 6829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7512 6829 603 41 0 7471 0
vsize: 30048
[startup+750.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7030 0 0 0 74984 29 0 0 25 0 1 0 546763198 31305728 6954 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7643 6954 603 41 0 7602 0
vsize: 30572
[startup+760.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7156 0 0 0 75984 29 0 0 25 0 1 0 546763198 31703040 7080 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7740 7080 603 41 0 7699 0
vsize: 30960
[startup+770.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7278 0 0 0 76984 29 0 0 25 0 1 0 546763198 32239616 7202 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7202 603 41 0 7830 0
vsize: 31484
[startup+780.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7392 0 0 0 77983 30 0 0 25 0 1 0 546763198 32768000 7316 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8000 7316 603 41 0 7959 0
vsize: 32000
[startup+790.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7530 0 0 0 78983 30 0 0 25 0 1 0 546763198 33304576 7454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8131 7454 603 41 0 8090 0
vsize: 32524
[startup+800.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7642 0 0 0 79983 31 0 0 25 0 1 0 546763198 33697792 7566 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8227 7566 603 41 0 8186 0
vsize: 32908
[startup+810.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7747 0 0 0 80983 31 0 0 25 0 1 0 546763198 34234368 7671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8358 7671 603 41 0 8317 0
vsize: 33432
[startup+820.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7847 0 0 0 81983 31 0 0 25 0 1 0 546763198 34631680 7771 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8455 7771 603 41 0 8414 0
vsize: 33820
[startup+830.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 7946 0 0 0 82983 31 0 0 25 0 1 0 546763198 35033088 7870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8553 7870 603 41 0 8512 0
vsize: 34212
[startup+840.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8038 0 0 0 83983 32 0 0 25 0 1 0 546763198 35299328 7962 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8618 7962 603 41 0 8577 0
vsize: 34472
[startup+850.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8162 0 0 0 84983 32 0 0 25 0 1 0 546763198 35840000 8086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8750 8086 603 41 0 8709 0
vsize: 35000
[startup+860.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8290 0 0 0 85983 32 0 0 25 0 1 0 546763198 36372480 8214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8880 8214 603 41 0 8839 0
vsize: 35520
[startup+870.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8449 0 0 0 86982 33 0 0 25 0 1 0 546763198 37036032 8373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9042 8373 603 41 0 9001 0
vsize: 36168
[startup+880.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8598 0 0 0 87982 34 0 0 25 0 1 0 546763198 37568512 8522 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9172 8522 603 41 0 9131 0
vsize: 36688
[startup+890.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8722 0 0 0 88981 34 0 0 25 0 1 0 546763198 38100992 8646 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9302 8646 603 41 0 9261 0
vsize: 37208
[startup+900.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8828 0 0 0 89981 35 0 0 25 0 1 0 546763198 38502400 8752 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9400 8752 603 41 0 9359 0
vsize: 37600
[startup+910.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 8946 0 0 0 90981 35 0 0 25 0 1 0 546763198 39030784 8870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9529 8870 603 41 0 9488 0
vsize: 38116
[startup+920.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9060 0 0 0 91981 35 0 0 25 0 1 0 546763198 39432192 8984 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9627 8984 603 41 0 9586 0
vsize: 38508
[startup+930.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9179 0 0 0 92981 36 0 0 25 0 1 0 546763198 39956480 9103 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9755 9103 603 41 0 9714 0
vsize: 39020
[startup+940.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9310 0 0 0 93980 36 0 0 25 0 1 0 546763198 40488960 9234 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9885 9234 603 41 0 9844 0
vsize: 39540
[startup+950.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9418 0 0 0 94980 37 0 0 25 0 1 0 546763198 40894464 9342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9984 9342 603 41 0 9943 0
vsize: 39936
[startup+960.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9514 0 0 0 95980 37 0 0 25 0 1 0 546763198 41295872 9438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10082 9438 603 41 0 10041 0
vsize: 40328
[startup+970.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9604 0 0 0 96980 37 0 0 25 0 1 0 546763198 41693184 9528 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10179 9528 603 41 0 10138 0
vsize: 40716
[startup+980.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9695 0 0 0 97980 37 0 0 25 0 1 0 546763198 42094592 9619 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10277 9619 603 41 0 10236 0
vsize: 41108
[startup+990.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9793 0 0 0 98980 38 0 0 25 0 1 0 546763198 42496000 9717 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10375 9717 603 41 0 10334 0
vsize: 41500
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9878 0 0 0 99980 38 0 0 25 0 1 0 546763198 42762240 9802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10440 9802 603 41 0 10399 0
vsize: 41760
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 9965 0 0 0 100980 39 0 0 25 0 1 0 546763198 43155456 9889 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10536 9889 603 41 0 10495 0
vsize: 42144
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10055 0 0 0 101979 39 0 0 25 0 1 0 546763198 43548672 9979 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10632 9979 603 41 0 10591 0
vsize: 42528
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10198 0 0 0 102978 40 0 0 25 0 1 0 546763198 44093440 10122 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10765 10122 603 41 0 10724 0
vsize: 43060
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10307 0 0 0 103979 40 0 0 25 0 1 0 546763198 44511232 10231 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10867 10231 603 41 0 10826 0
vsize: 43468
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10405 0 0 0 104978 40 0 0 25 0 1 0 546763198 44916736 10329 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10966 10329 603 41 0 10925 0
vsize: 43864
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10495 0 0 0 105978 40 0 0 25 0 1 0 546763198 45322240 10419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11065 10419 603 41 0 11024 0
vsize: 44260
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 106979 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 107979 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 108979 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 109979 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 110979 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 111979 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 112980 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 113980 40 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 114980 41 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 115980 41 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 116980 41 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 117980 41 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 118981 41 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22858
Raw data (stat): 22858 (minisat+) R 22857 11931 11930 0 -1 0 10577 0 0 0 119981 41 0 0 25 0 1 0 546763198 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 22858
Raw data (stat): 22858 (minisat+) Z 22857 11931 11930 0 -1 12 10580 0 0 0 119981 43 0 0 25 0 1 0 546763198 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.24
CPU user time (s): 1199.81
CPU system time (s): 0.431934
CPU usage (%): 100.013
Max. virtual memory (Kb): 44520
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####