PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.01784
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 21982

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-22 01:42:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12272 boxname=wulflinc13 idbench=944 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-sentoy.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-sentoy.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-sentoy.opb
IDLAUNCH: 12272
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        361680 kB
Buffers:         21664 kB
Cached:         630200 kB
SwapCached:        392 kB
Active:          94480 kB
Inactive:       559460 kB
HighTotal:      131008 kB
HighFree:          476 kB
LowTotal:       903652 kB
LowFree:        361204 kB
SwapTotal:     2097136 kB
SwapFree:      2095968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13352 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:03:00 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 12272 7 1200.22 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.92 0.98 0.99 2/54 367
Raw data (stat): 367 (runsolver) R 366 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491631726 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 2148 0 0 0 993 5 0 0 25 0 1 0 491631726 10514432 2074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2567 2074 603 41 0 2526 0
vsize: 10268
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 2716 0 0 0 1991 6 0 0 25 0 1 0 491631726 13389824 2640 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2640 603 41 0 3228 0
vsize: 13076
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 2850 0 0 0 2990 7 0 0 25 0 1 0 491631726 13955072 2774 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3407 2774 603 41 0 3366 0
vsize: 13628
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 2989 0 0 0 3989 8 0 0 25 0 1 0 491631726 14495744 2913 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3539 2913 603 41 0 3498 0
vsize: 14156
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3097 0 0 0 4989 8 0 0 25 0 1 0 491631726 14893056 3021 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3636 3021 603 41 0 3595 0
vsize: 14544
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3200 0 0 0 5989 8 0 0 25 0 1 0 491631726 15298560 3124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3735 3124 603 41 0 3694 0
vsize: 14940
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3293 0 0 0 6989 8 0 0 25 0 1 0 491631726 15699968 3217 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3833 3217 603 41 0 3792 0
vsize: 15332
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3393 0 0 0 7989 8 0 0 25 0 1 0 491631726 16207872 3317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3957 3317 603 41 0 3916 0
vsize: 15828
[startup+90.0099 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3498 0 0 0 8989 9 0 0 25 0 1 0 491631726 16613376 3422 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4056 3422 603 41 0 4015 0
vsize: 16224
[startup+100.009 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3623 0 0 0 9989 9 0 0 25 0 1 0 491631726 17014784 3547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3547 603 41 0 4113 0
vsize: 16616
[startup+110.01 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3812 0 0 0 10987 10 0 0 25 0 1 0 491631726 17825792 3736 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4352 3736 603 41 0 4311 0
vsize: 17408
[startup+120.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3906 0 0 0 11987 11 0 0 25 0 1 0 491631726 18223104 3830 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4449 3830 603 41 0 4408 0
vsize: 17796
[startup+130.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 3975 0 0 0 12987 11 0 0 25 0 1 0 491631726 18493440 3899 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4515 3899 603 41 0 4474 0
vsize: 18060
[startup+140.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4081 0 0 0 13987 11 0 0 25 0 1 0 491631726 18898944 4005 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4614 4005 603 41 0 4573 0
vsize: 18456
[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4201 0 0 0 14987 12 0 0 25 0 1 0 491631726 19562496 4125 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4776 4125 603 41 0 4735 0
vsize: 19104
[startup+160.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4299 0 0 0 15987 12 0 0 25 0 1 0 491631726 19959808 4223 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4873 4223 603 41 0 4832 0
vsize: 19492
[startup+170.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4416 0 0 0 16987 12 0 0 25 0 1 0 491631726 20357120 4340 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4970 4340 603 41 0 4929 0
vsize: 19880
[startup+180.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4524 0 0 0 17987 13 0 0 25 0 1 0 491631726 20889600 4448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5100 4448 603 41 0 5059 0
vsize: 20400
[startup+190.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4646 0 0 0 18987 13 0 0 25 0 1 0 491631726 21291008 4570 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5198 4570 603 41 0 5157 0
vsize: 20792
[startup+200.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4734 0 0 0 19986 13 0 0 25 0 1 0 491631726 21688320 4658 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5295 4658 603 41 0 5254 0
vsize: 21180
[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4834 0 0 0 20986 14 0 0 25 0 1 0 491631726 22085632 4758 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5392 4758 603 41 0 5351 0
vsize: 21568
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 4930 0 0 0 21986 14 0 0 25 0 1 0 491631726 22482944 4854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5489 4854 603 41 0 5448 0
vsize: 21956
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5020 0 0 0 22985 15 0 0 25 0 1 0 491631726 22884352 4944 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5587 4944 603 41 0 5546 0
vsize: 22348
[startup+240.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5123 0 0 0 23985 15 0 0 25 0 1 0 491631726 23285760 5047 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5047 603 41 0 5644 0
vsize: 22740
[startup+250.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5243 0 0 0 24985 16 0 0 25 0 1 0 491631726 23707648 5167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5167 603 41 0 5747 0
vsize: 23152
[startup+260.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5352 0 0 0 25985 16 0 0 25 0 1 0 491631726 24113152 5276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5887 5276 603 41 0 5846 0
vsize: 23548
[startup+270.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5469 0 0 0 26985 16 0 0 25 0 1 0 491631726 24641536 5393 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6016 5393 603 41 0 5975 0
vsize: 24064
[startup+280.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5578 0 0 0 27985 17 0 0 25 0 1 0 491631726 25038848 5502 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6113 5502 603 41 0 6072 0
vsize: 24452
[startup+290.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5737 0 0 0 28985 17 0 0 25 0 1 0 491631726 25702400 5661 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6275 5661 603 41 0 6234 0
vsize: 25100
[startup+300.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 5923 0 0 0 29984 18 0 0 25 0 1 0 491631726 26505216 5847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6471 5847 603 41 0 6430 0
vsize: 25884
[startup+310.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6011 0 0 0 30984 19 0 0 25 0 1 0 491631726 26910720 5935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6570 5935 603 41 0 6529 0
vsize: 26280
[startup+320.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6094 0 0 0 31984 19 0 0 25 0 1 0 491631726 27181056 6018 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6636 6018 603 41 0 6595 0
vsize: 26544
[startup+330.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6185 0 0 0 32983 19 0 0 25 0 1 0 491631726 27582464 6109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 6109 603 41 0 6693 0
vsize: 26936
[startup+340.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6266 0 0 0 33984 20 0 0 25 0 1 0 491631726 27844608 6190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6798 6190 603 41 0 6757 0
vsize: 27192
[startup+350.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6352 0 0 0 34984 20 0 0 25 0 1 0 491631726 28508160 6276 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6960 6276 603 41 0 6919 0
vsize: 27840
[startup+360.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 35984 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+370.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 36984 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+380.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 37984 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+390.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 38984 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+400.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 39985 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+410.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 40985 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+420.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 41985 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+430.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 42986 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+440.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 43986 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+450.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 44986 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+460.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 45986 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+470.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 46986 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+480.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 47987 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+490.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 48987 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+500.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 49987 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+510.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 50987 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+520.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 51987 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+530.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 52987 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+540.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 53987 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+550.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 54988 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+560.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 55988 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+570.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 56988 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+580.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 57988 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+590.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 58988 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+600.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 59988 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+610.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 60989 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+620.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 61989 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+630.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 62989 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+640.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 63989 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+650.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 64989 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+660.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 65989 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+670.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 66989 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+680.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 67990 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+690.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6374 0 0 0 68990 20 0 0 25 0 1 0 491631726 28614656 6298 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6298 603 41 0 6945 0
vsize: 27944
[startup+700.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6428 0 0 0 69990 20 0 0 25 0 1 0 491631726 28762112 6352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7022 6352 603 41 0 6981 0
vsize: 28088
[startup+710.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6600 0 0 0 70990 21 0 0 25 0 1 0 491631726 29564928 6524 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7218 6524 603 41 0 7177 0
vsize: 28872
[startup+720.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6722 0 0 0 71989 21 0 0 25 0 1 0 491631726 29966336 6646 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7316 6646 603 41 0 7275 0
vsize: 29264
[startup+730.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 6926 0 0 0 72989 22 0 0 25 0 1 0 491631726 30904320 6850 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7545 6850 603 41 0 7504 0
vsize: 30180
[startup+740.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7044 0 0 0 73988 22 0 0 25 0 1 0 491631726 31305728 6968 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7643 6968 603 41 0 7602 0
vsize: 30572
[startup+750.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7180 0 0 0 74987 24 0 0 25 0 1 0 491631726 31838208 7104 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7773 7104 603 41 0 7732 0
vsize: 31092
[startup+760.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7296 0 0 0 75987 24 0 0 25 0 1 0 491631726 32370688 7220 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7903 7220 603 41 0 7862 0
vsize: 31612
[startup+770.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7430 0 0 0 76987 25 0 0 25 0 1 0 491631726 32899072 7354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7354 603 41 0 7991 0
vsize: 32128
[startup+780.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7553 0 0 0 77987 25 0 0 25 0 1 0 491631726 33435648 7477 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8163 7477 603 41 0 8122 0
vsize: 32652
[startup+790.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7665 0 0 0 78986 25 0 0 25 0 1 0 491631726 33828864 7589 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8259 7589 603 41 0 8218 0
vsize: 33036
[startup+800.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7769 0 0 0 79986 26 0 0 25 0 1 0 491631726 34234368 7693 4294967295 134512640 134672761 3221224544 3221223728 134558371 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8358 7693 603 41 0 8317 0
vsize: 33432
[startup+810.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7874 0 0 0 80986 27 0 0 25 0 1 0 491631726 34631680 7798 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8455 7798 603 41 0 8414 0
vsize: 33820
[startup+820.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 7970 0 0 0 81985 27 0 0 25 0 1 0 491631726 35033088 7894 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8553 7894 603 41 0 8512 0
vsize: 34212
[startup+830.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8064 0 0 0 82985 27 0 0 25 0 1 0 491631726 35434496 7988 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8651 7988 603 41 0 8610 0
vsize: 34604
[startup+840.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8203 0 0 0 83985 27 0 0 25 0 1 0 491631726 35971072 8127 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8782 8127 603 41 0 8741 0
vsize: 35128
[startup+850.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8343 0 0 0 84985 28 0 0 25 0 1 0 491631726 36638720 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8945 8267 603 41 0 8904 0
vsize: 35780
[startup+860.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8508 0 0 0 85985 28 0 0 25 0 1 0 491631726 37302272 8432 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9107 8432 603 41 0 9066 0
vsize: 36428
[startup+870.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8635 0 0 0 86984 29 0 0 25 0 1 0 491631726 37699584 8559 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9204 8559 603 41 0 9163 0
vsize: 36816
[startup+880.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8765 0 0 0 87985 29 0 0 25 0 1 0 491631726 38236160 8689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9335 8689 603 41 0 9294 0
vsize: 37340
[startup+890.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8873 0 0 0 88984 30 0 0 25 0 1 0 491631726 38768640 8797 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9465 8797 603 41 0 9424 0
vsize: 37860
[startup+900.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 8989 0 0 0 89984 30 0 0 25 0 1 0 491631726 39161856 8913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9561 8913 603 41 0 9520 0
vsize: 38244
[startup+910.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9107 0 0 0 90984 30 0 0 25 0 1 0 491631726 39694336 9031 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9031 603 41 0 9650 0
vsize: 38764
[startup+920.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9233 0 0 0 91984 31 0 0 25 0 1 0 491631726 40226816 9157 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9821 9157 603 41 0 9780 0
vsize: 39284
[startup+930.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9348 0 0 0 92984 31 0 0 25 0 1 0 491631726 40624128 9272 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9918 9272 603 41 0 9877 0
vsize: 39672
[startup+940.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9467 0 0 0 93983 31 0 0 25 0 1 0 491631726 41160704 9391 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10049 9391 603 41 0 10008 0
vsize: 40196
[startup+950.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9554 0 0 0 94983 32 0 0 25 0 1 0 491631726 41426944 9478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10114 9478 603 41 0 10073 0
vsize: 40456
[startup+960.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9647 0 0 0 95983 32 0 0 25 0 1 0 491631726 41824256 9571 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10211 9571 603 41 0 10170 0
vsize: 40844
[startup+970.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9740 0 0 0 96983 32 0 0 25 0 1 0 491631726 42229760 9664 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9664 603 41 0 10269 0
vsize: 41240
[startup+980.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9840 0 0 0 97983 33 0 0 25 0 1 0 491631726 42627072 9764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10407 9764 603 41 0 10366 0
vsize: 41628
[startup+990.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 9919 0 0 0 98983 33 0 0 25 0 1 0 491631726 43024384 9843 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10504 9843 603 41 0 10463 0
vsize: 42016
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10014 0 0 0 99982 34 0 0 25 0 1 0 491631726 43286528 9938 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10568 9938 603 41 0 10527 0
vsize: 42272
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10125 0 0 0 100981 34 0 0 25 0 1 0 491631726 43823104 10049 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10699 10049 603 41 0 10658 0
vsize: 42796
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 367
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10253 0 0 0 101982 35 0 0 25 0 1 0 491631726 44376064 10177 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10834 10177 603 41 0 10793 0
vsize: 43336
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 420
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10358 0 0 0 102981 35 0 0 25 0 1 0 491631726 44781568 10282 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10282 603 41 0 10892 0
vsize: 43732
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 420
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10460 0 0 0 103980 36 0 0 25 0 1 0 491631726 45187072 10384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11032 10384 603 41 0 10991 0
vsize: 44128
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 420
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10554 0 0 0 104980 37 0 0 25 0 1 0 491631726 45588480 10478 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10478 603 41 0 11089 0
vsize: 44520
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 420
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 105980 37 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 420
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 106979 38 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 420
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 107979 38 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 420
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 108979 38 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 109979 39 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 110979 39 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 111978 40 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 112978 40 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 113978 40 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 114978 40 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 115978 41 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 116978 41 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 117978 41 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 118978 41 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 422
Raw data (stat): 367 (minisat+) R 366 30701 30700 0 -1 0 10577 0 0 0 119978 41 0 0 25 0 1 0 491631726 45588480 10501 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10501 603 41 0 11089 0
vsize: 44520
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.99 1/54 422
Raw data (stat): 367 (minisat+) Z 366 30701 30700 0 -1 12 10580 0 0 0 119978 43 0 0 25 0 1 0 491631726 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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