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 21989

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-22 01:43:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12264 boxname=wulflinc15 idbench=944 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-sentoy.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-sentoy.opb
IDLAUNCH: 12264
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        638244 kB
Buffers:         27284 kB
Cached:         346896 kB
SwapCached:        432 kB
Active:          38448 kB
Inactive:       337872 kB
HighTotal:      131008 kB
HighFree:        60704 kB
LowTotal:       903652 kB
LowFree:        577540 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5364 kB
Slab:            14208 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:15 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 12264 7 1200.21 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 |   89253   318894 |   29751       0        0     nan |  0.000 % |
c |       100 |   89253   318894 |   32726     100     1024    10.2 |  1.712 % |
c ==============================================================================
c [1mFound solution: -1341[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 |       191 |  106220   358591 |   35406     191     1682     8.8 |  1.712 % |
c |       291 |  106220   358591 |   38946     291     5111    17.6 |  1.192 % |
c |       443 |  106220   358591 |   42841     443     9280    20.9 |  1.192 % |
c |       669 |  106220   358591 |   47125     669    14719    22.0 |  1.192 % |
c |      1007 |  106214   358574 |   51837    1006    19436    19.3 |  1.197 % |
c ==============================================================================
c [1mFound solution: -1485[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 |      1190 |  106519   359320 |   35506    1189    21596    18.2 |  1.197 % |
c |      1293 |  106519   359320 |   39056    1292    22436    17.4 |  1.191 % |
c |      1445 |  106519   359320 |   42962    1444    24976    17.3 |  1.191 % |
c |      1670 |  106519   359320 |   47258    1669    29751    17.8 |  1.191 % |
c |      2007 |  106519   359320 |   51984    2006    35780    17.8 |  1.191 % |
c ==============================================================================
c [1mFound solution: -1703[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 |      2104 |  106596   359531 |   35532    2103    37022    17.6 |  1.191 % |
c |      2204 |  106596   359531 |   39085    2203    38425    17.4 |  1.194 % |
c |      2357 |  106596   359531 |   42993    2356    40994    17.4 |  1.194 % |
c |      2582 |  106596   359531 |   47293    2581    48161    18.7 |  1.194 % |
c |      2920 |  106596   359531 |   52022    2919    55040    18.9 |  1.194 % |
c ==============================================================================
c [1mFound solution: -2044[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 |      3041 |  106710   359836 |   35570    3040    59039    19.4 |  1.194 % |
c |      3141 |  106710   359836 |   39127    3140    59910    19.1 |  1.195 % |
c |      3291 |  106704   359819 |   43039    3289    62063    18.9 |  1.200 % |
c |      3516 |  106704   359819 |   47343    3514    64855    18.5 |  1.200 % |
c ==============================================================================
c [1mFound solution: -2051[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 |      3838 |  106709   359842 |   35569    3836    75916    19.8 |  1.200 % |
c |      3938 |  106709   359842 |   39125    3936    77693    19.7 |  1.205 % |
c |      4088 |  106709   359842 |   43038    4086    78884    19.3 |  1.205 % |
c ==============================================================================
c [1mFound solution: -2441[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4105 |  106730   359904 |   35576    4103    79182    19.3 |  1.205 % |
c |      4205 |  106730   359904 |   39133    4203    85074    20.2 |  1.209 % |
c |      4356 |  106730   359904 |   43046    4354    87121    20.0 |  1.209 % |
c ==============================================================================
c [1mFound solution: -2545[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 |      4437 |  106743   359939 |   35581    4435    91419    20.6 |  1.209 % |
c |      4537 |  106743   359939 |   39139    4535    93846    20.7 |  1.214 % |
c |      4687 |  106743   359939 |   43053    4685    97645    20.8 |  1.214 % |
c |      4912 |  106743   359939 |   47358    4910   102902    21.0 |  1.214 % |
c |      5249 |  106743   359939 |   52094    5247   110257    21.0 |  1.213 % |
c |      5755 |  106743   359939 |   57303    5753   131413    22.8 |  1.214 % |
c |      6514 |  106743   359939 |   63033    6512   170601    26.2 |  1.214 % |
c |      7653 |  106743   359939 |   69337    7651   215921    28.2 |  1.214 % |
c ==============================================================================
c [1mFound solution: -2651[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 |      7953 |  106748   359952 |   35582    7951   223593    28.1 |  1.214 % |
c |      8055 |  106748   359952 |   39140    8053   225854    28.0 |  1.218 % |
c |      8205 |  106748   359952 |   43054    8203   228739    27.9 |  1.218 % |
c ==============================================================================
c [1mFound solution: -2952[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 |      8246 |  106757   359976 |   35585    8244   230421    28.0 |  1.218 % |
c |      8346 |  106757   359976 |   39143    8344   232767    27.9 |  1.223 % |
c |      8496 |  106757   359976 |   43057    8494   236015    27.8 |  1.223 % |
c |      8721 |  106757   359976 |   47363    8719   243030    27.9 |  1.223 % |
c |      9058 |  106757   359976 |   52099    9056   255321    28.2 |  1.223 % |
c |      9566 |  106757   359976 |   57309    9564   270673    28.3 |  1.223 % |
c ==============================================================================
c [1mFound solution: -3309[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 |      9599 |  106798   360082 |   35599    9597   271200    28.3 |  1.223 % |
c |      9699 |  106798   360082 |   39158    9697   276476    28.5 |  1.227 % |
c |      9849 |  106798   360082 |   43074    9847   279294    28.4 |  1.227 % |
c |     10074 |  106798   360082 |   47382   10072   291867    29.0 |  1.227 % |
c |     10412 |  106798   360082 |   52120   10410   298988    28.7 |  1.227 % |
c |     10919 |  106798   360082 |   57332   10917   331053    30.3 |  1.227 % |
c |     11680 |  106792   360065 |   63065   11677   353489    30.3 |  1.232 % |
c |     12819 |  106792   360065 |   69372   12816   416224    32.5 |  1.232 % |
c |     14527 |  106792   360065 |   76309   14524   500281    34.4 |  1.232 % |
c |     17090 |  106786   360048 |   83940   17086   621843    36.4 |  1.237 % |
c |     20934 |  106786   360048 |   92334   20930   766604    36.6 |  1.237 % |
c |     26700 |  106786   360048 |  101568   26696   976667    36.6 |  1.237 % |
c |     35352 |  106786   360048 |  111724   35348  1373187    38.8 |  1.237 % |
c |     48326 |  106786   360048 |  122897   48322  2301426    47.6 |  1.237 % |
c ==============================================================================
c [1mFound solution: -5491[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 |     49564 |  106852   360209 |   35617   49560  2348470    47.4 |  1.237 % |
c |     49664 |  106852   360209 |   39178   13139   877063    66.8 |  1.239 % |
c |     49815 |  106852   360209 |   43096   13290   878830    66.1 |  1.239 % |
c |     50040 |  106852   360209 |   47406   13515   892196    66.0 |  1.239 % |
c |     50379 |  106852   360209 |   52146   13854   895991    64.7 |  1.239 % |
c |     50887 |  106852   360209 |   57361   14362   901416    62.8 |  1.239 % |
c |     51646 |  106852   360209 |   63097   15121   912500    60.3 |  1.239 % |
c |     52787 |  106852   360209 |   69407   16262   956151    58.8 |  1.239 % |
c |     54495 |  106852   360209 |   76348   17970  1040942    57.9 |  1.239 % |
c |     57057 |  106852   360209 |   83983   20532  1211813    59.0 |  1.239 % |
c |     60902 |  106852   360209 |   92381   24377  1475337    60.5 |  1.239 % |
c |     66669 |  106846   360192 |  101619   30143  1911942    63.4 |  1.245 % |
c |     75319 |  106846   360192 |  111781   38793  2562755    66.1 |  1.245 % |
c |     88295 |  106846   360192 |  122959   51769  3109322    60.1 |  1.245 % |
c |    107756 |  106846   360192 |  135255   71230  4469811    62.8 |  1.245 % |
c |    136950 |  106846   360192 |  148781  100424  6087573    60.6 |  1.245 % |
c |    180739 |  106840   360175 |  163659  144212  8423431    58.4 |  1.250 % |
#### 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.55 0.84 0.94 2/54 21945
Raw data (stat): 21945 (runsolver) R 21944 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491625447 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0002 s]
Raw data (loadavg): 0.62 0.85 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 2607 0 0 0 992 7 0 0 25 0 1 0 491625447 12935168 2531 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2531 603 41 0 3117 0
vsize: 12632
[startup+20.001 s]
Raw data (loadavg): 0.68 0.85 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 2714 0 0 0 1991 8 0 0 25 0 1 0 491625447 13471744 2638 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3289 2638 603 41 0 3248 0
vsize: 13156
[startup+30.0014 s]
Raw data (loadavg): 0.73 0.85 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 2842 0 0 0 2990 9 0 0 25 0 1 0 491625447 14020608 2766 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3423 2766 603 41 0 3382 0
vsize: 13692
[startup+40.0027 s]
Raw data (loadavg): 0.77 0.86 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 2951 0 0 0 3989 10 0 0 25 0 1 0 491625447 14422016 2875 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3521 2875 603 41 0 3480 0
vsize: 14084
[startup+50.0035 s]
Raw data (loadavg): 0.80 0.86 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3072 0 0 0 4989 10 0 0 25 0 1 0 491625447 14946304 2996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3649 2996 603 41 0 3608 0
vsize: 14596
[startup+60.0029 s]
Raw data (loadavg): 0.83 0.87 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3186 0 0 0 5988 11 0 0 25 0 1 0 491625447 15343616 3110 4294967295 134512640 134672761 3221224624 3221223760 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3746 3110 603 41 0 3705 0
vsize: 14984
[startup+70.0041 s]
Raw data (loadavg): 0.86 0.87 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3292 0 0 0 6988 12 0 0 25 0 1 0 491625447 15876096 3216 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3876 3216 603 41 0 3835 0
vsize: 15504
[startup+80.005 s]
Raw data (loadavg): 0.88 0.87 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3396 0 0 0 7987 13 0 0 25 0 1 0 491625447 16273408 3320 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3973 3320 603 41 0 3932 0
vsize: 15892
[startup+90.0054 s]
Raw data (loadavg): 0.90 0.88 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3520 0 0 0 8987 13 0 0 25 0 1 0 491625447 16814080 3444 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4105 3444 603 41 0 4064 0
vsize: 16420
[startup+100.006 s]
Raw data (loadavg): 0.91 0.88 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3648 0 0 0 9986 14 0 0 25 0 1 0 491625447 17350656 3572 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4236 3572 603 41 0 4195 0
vsize: 16944
[startup+110.007 s]
Raw data (loadavg): 0.93 0.89 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3768 0 0 0 10985 15 0 0 25 0 1 0 491625447 17760256 3692 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4336 3692 603 41 0 4295 0
vsize: 17344
[startup+120.007 s]
Raw data (loadavg): 0.94 0.89 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 3920 0 0 0 11985 16 0 0 25 0 1 0 491625447 18427904 3844 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4499 3844 603 41 0 4458 0
vsize: 17996
[startup+130.007 s]
Raw data (loadavg): 0.95 0.89 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4117 0 0 0 12984 16 0 0 25 0 1 0 491625447 19361792 4041 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4727 4041 603 41 0 4686 0
vsize: 18908
[startup+140.008 s]
Raw data (loadavg): 0.95 0.89 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4269 0 0 0 13983 17 0 0 25 0 1 0 491625447 19894272 4193 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4857 4193 603 41 0 4816 0
vsize: 19428
[startup+150.008 s]
Raw data (loadavg): 0.96 0.90 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4372 0 0 0 14983 18 0 0 25 0 1 0 491625447 20295680 4296 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4955 4296 603 41 0 4914 0
vsize: 19820
[startup+160.009 s]
Raw data (loadavg): 0.97 0.90 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4486 0 0 0 15983 18 0 0 25 0 1 0 491625447 20832256 4410 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5086 4410 603 41 0 5045 0
vsize: 20344
[startup+170.01 s]
Raw data (loadavg): 0.97 0.90 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4641 0 0 0 16982 19 0 0 25 0 1 0 491625447 21372928 4565 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5218 4565 603 41 0 5177 0
vsize: 20872
[startup+180.01 s]
Raw data (loadavg): 0.98 0.91 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4740 0 0 0 17982 19 0 0 25 0 1 0 491625447 21774336 4664 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5316 4664 603 41 0 5275 0
vsize: 21264
[startup+190.011 s]
Raw data (loadavg): 0.98 0.91 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4872 0 0 0 18981 20 0 0 25 0 1 0 491625447 22306816 4796 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5446 4796 603 41 0 5405 0
vsize: 21784
[startup+200.012 s]
Raw data (loadavg): 0.98 0.91 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 4998 0 0 0 19980 22 0 0 25 0 1 0 491625447 22839296 4922 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5576 4922 603 41 0 5535 0
vsize: 22304
[startup+210.012 s]
Raw data (loadavg): 0.98 0.91 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5125 0 0 0 20980 22 0 0 25 0 1 0 491625447 23379968 5049 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5708 5049 603 41 0 5667 0
vsize: 22832
[startup+220.013 s]
Raw data (loadavg): 0.99 0.92 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5252 0 0 0 21979 23 0 0 25 0 1 0 491625447 23908352 5176 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5837 5176 603 41 0 5796 0
vsize: 23348
[startup+230.013 s]
Raw data (loadavg): 0.99 0.92 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 22978 24 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+240.014 s]
Raw data (loadavg): 0.99 0.92 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 23978 24 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+250.014 s]
Raw data (loadavg): 0.99 0.92 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 24978 25 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+260.014 s]
Raw data (loadavg): 0.99 0.92 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 25977 25 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+270.014 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 26977 26 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+280.014 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 27977 26 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+290.016 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 28977 26 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223808 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+300.016 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 29977 27 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+310.016 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 30976 27 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223728 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+320.017 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5380 0 0 0 31976 27 0 0 25 0 1 0 491625447 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+330.016 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5549 0 0 0 32975 29 0 0 25 0 1 0 491625447 25108480 5473 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6130 5473 603 41 0 6089 0
vsize: 24520
[startup+340.017 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5699 0 0 0 33974 29 0 0 25 0 1 0 491625447 25767936 5623 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6291 5623 603 41 0 6250 0
vsize: 25164
[startup+350.019 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5832 0 0 0 34974 30 0 0 25 0 1 0 491625447 26300416 5756 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6421 5756 603 41 0 6380 0
vsize: 25684
[startup+360.018 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 5957 0 0 0 35973 31 0 0 25 0 1 0 491625447 26836992 5881 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6552 5881 603 41 0 6511 0
vsize: 26208
[startup+370.018 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6063 0 0 0 36972 32 0 0 25 0 1 0 491625447 27230208 5987 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6648 5987 603 41 0 6607 0
vsize: 26592
[startup+380.019 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6179 0 0 0 37971 33 0 0 25 0 1 0 491625447 27766784 6103 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6779 6103 603 41 0 6738 0
vsize: 27116
[startup+390.019 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6302 0 0 0 38970 34 0 0 25 0 1 0 491625447 28164096 6226 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6876 6226 603 41 0 6835 0
vsize: 27504
[startup+400.019 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6401 0 0 0 39970 35 0 0 25 0 1 0 491625447 28565504 6325 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6325 603 41 0 6933 0
vsize: 27896
[startup+410.021 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6483 0 0 0 40969 35 0 0 25 0 1 0 491625447 28962816 6407 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7071 6407 603 41 0 7030 0
vsize: 28284
[startup+420.021 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6571 0 0 0 41969 36 0 0 25 0 1 0 491625447 29360128 6495 4294967295 134512640 134672761 3221224624 3221223808 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7168 6495 603 41 0 7127 0
vsize: 28672
[startup+430.021 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6712 0 0 0 42968 37 0 0 25 0 1 0 491625447 29888512 6636 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7297 6636 603 41 0 7256 0
vsize: 29188
[startup+440.022 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6845 0 0 0 43968 38 0 0 25 0 1 0 491625447 30420992 6769 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7427 6769 603 41 0 7386 0
vsize: 29708
[startup+450.023 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 6968 0 0 0 44967 39 0 0 25 0 1 0 491625447 30961664 6892 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7559 6892 603 41 0 7518 0
vsize: 30236
[startup+460.022 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7078 0 0 0 45967 39 0 0 25 0 1 0 491625447 31363072 7002 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7657 7002 603 41 0 7616 0
vsize: 30628
[startup+470.023 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7206 0 0 0 46967 40 0 0 25 0 1 0 491625447 31891456 7130 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7786 7130 603 41 0 7745 0
vsize: 31144
[startup+480.023 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7320 0 0 0 47966 40 0 0 25 0 1 0 491625447 32284672 7244 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7882 7244 603 41 0 7841 0
vsize: 31528
[startup+490.024 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7463 0 0 0 48965 41 0 0 25 0 1 0 491625447 33206272 7387 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8107 7387 603 41 0 8066 0
vsize: 32428
[startup+500.024 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7592 0 0 0 49965 42 0 0 25 0 1 0 491625447 33730560 7516 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8235 7516 603 41 0 8194 0
vsize: 32940
[startup+510.024 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7688 0 0 0 50964 43 0 0 25 0 1 0 491625447 34127872 7612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8332 7612 603 41 0 8291 0
vsize: 33328
[startup+520.025 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7762 0 0 0 51964 43 0 0 25 0 1 0 491625447 34390016 7686 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8396 7686 603 41 0 8355 0
vsize: 33584
[startup+530.025 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7848 0 0 0 52963 44 0 0 25 0 1 0 491625447 34791424 7772 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8494 7772 603 41 0 8453 0
vsize: 33976
[startup+540.026 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 7992 0 0 0 53962 45 0 0 25 0 1 0 491625447 35323904 7916 4294967295 134512640 134672761 3221224624 3221223640 1075352732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8624 7916 603 41 0 8583 0
vsize: 34496
[startup+550.027 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8161 0 0 0 54962 46 0 0 25 0 1 0 491625447 35987456 8085 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8786 8085 603 41 0 8745 0
vsize: 35144
[startup+560.026 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8274 0 0 0 55962 46 0 0 25 0 1 0 491625447 36388864 8198 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8884 8198 603 41 0 8843 0
vsize: 35536
[startup+570.026 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8352 0 0 0 56961 47 0 0 25 0 1 0 491625447 36794368 8276 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8983 8276 603 41 0 8942 0
vsize: 35932
[startup+580.026 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8430 0 0 0 57960 48 0 0 25 0 1 0 491625447 37072896 8354 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9051 8354 603 41 0 9010 0
vsize: 36204
[startup+590.027 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8509 0 0 0 58960 49 0 0 25 0 1 0 491625447 37343232 8433 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9117 8433 603 41 0 9076 0
vsize: 36468
[startup+600.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8580 0 0 0 59960 49 0 0 25 0 1 0 491625447 37740544 8504 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8504 603 41 0 9173 0
vsize: 36856
[startup+610.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8682 0 0 0 60959 50 0 0 25 0 1 0 491625447 38146048 8606 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9313 8606 603 41 0 9272 0
vsize: 37252
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8782 0 0 0 61959 50 0 0 25 0 1 0 491625447 38547456 8706 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9411 8706 603 41 0 9370 0
vsize: 37644
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8870 0 0 0 62959 50 0 0 25 0 1 0 491625447 38817792 8794 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9477 8794 603 41 0 9436 0
vsize: 37908
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 8962 0 0 0 63959 51 0 0 25 0 1 0 491625447 39219200 8886 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9575 8886 603 41 0 9534 0
vsize: 38300
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9031 0 0 0 64958 51 0 0 25 0 1 0 491625447 39485440 8955 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9640 8955 603 41 0 9599 0
vsize: 38560
[startup+660.031 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9098 0 0 0 65958 52 0 0 25 0 1 0 491625447 39747584 9022 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 9022 603 41 0 9663 0
vsize: 38816
[startup+670.032 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9168 0 0 0 66958 52 0 0 25 0 1 0 491625447 40009728 9092 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9768 9092 603 41 0 9727 0
vsize: 39072
[startup+680.031 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9233 0 0 0 67957 53 0 0 25 0 1 0 491625447 40280064 9157 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9834 9157 603 41 0 9793 0
vsize: 39336
[startup+690.032 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9306 0 0 0 68957 53 0 0 25 0 1 0 491625447 40685568 9230 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9933 9230 603 41 0 9892 0
vsize: 39732
[startup+700.033 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9377 0 0 0 69957 53 0 0 25 0 1 0 491625447 40951808 9301 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9998 9301 603 41 0 9957 0
vsize: 39992
[startup+710.033 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9452 0 0 0 70956 54 0 0 25 0 1 0 491625447 41218048 9376 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10063 9376 603 41 0 10022 0
vsize: 40252
[startup+720.034 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9530 0 0 0 71956 55 0 0 25 0 1 0 491625447 41488384 9454 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10129 9454 603 41 0 10088 0
vsize: 40516
[startup+730.035 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9603 0 0 0 72956 55 0 0 25 0 1 0 491625447 41889792 9527 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10227 9527 603 41 0 10186 0
vsize: 40908
[startup+740.035 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9670 0 0 0 73955 56 0 0 25 0 1 0 491625447 42156032 9594 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10292 9594 603 41 0 10251 0
vsize: 41168
[startup+750.035 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9771 0 0 0 74955 57 0 0 25 0 1 0 491625447 42573824 9695 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10394 9695 603 41 0 10353 0
vsize: 41576
[startup+760.036 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9849 0 0 0 75954 57 0 0 25 0 1 0 491625447 42835968 9773 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10458 9773 603 41 0 10417 0
vsize: 41832
[startup+770.037 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 9942 0 0 0 76954 57 0 0 25 0 1 0 491625447 43233280 9866 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10555 9866 603 41 0 10514 0
vsize: 42220
[startup+780.037 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10028 0 0 0 77954 58 0 0 25 0 1 0 491625447 43630592 9952 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10652 9952 603 41 0 10611 0
vsize: 42608
[startup+790.037 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10132 0 0 0 78953 59 0 0 25 0 1 0 491625447 44027904 10056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10749 10056 603 41 0 10708 0
vsize: 42996
[startup+800.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10217 0 0 0 79953 59 0 0 25 0 1 0 491625447 44294144 10141 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10814 10141 603 41 0 10773 0
vsize: 43256
[startup+810.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10353 0 0 0 80953 59 0 0 25 0 1 0 491625447 44834816 10277 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10946 10278 603 41 0 10905 0
vsize: 43784
[startup+820.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10478 0 0 0 81952 60 0 0 25 0 1 0 491625447 45383680 10402 4294967295 134512640 134672761 3221224624 3221223760 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11080 10402 603 41 0 11039 0
vsize: 44320
[startup+830.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10602 0 0 0 82952 61 0 0 25 0 1 0 491625447 45916160 10526 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11210 10526 603 41 0 11169 0
vsize: 44840
[startup+840.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10738 0 0 0 83951 62 0 0 25 0 1 0 491625447 46448640 10662 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11340 10662 603 41 0 11299 0
vsize: 45360
[startup+850.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10850 0 0 0 84951 62 0 0 25 0 1 0 491625447 46985216 10774 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11471 10774 603 41 0 11430 0
vsize: 45884
[startup+860.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 10961 0 0 0 85950 63 0 0 25 0 1 0 491625447 47382528 10885 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11568 10885 603 41 0 11527 0
vsize: 46272
[startup+870.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11048 0 0 0 86950 63 0 0 25 0 1 0 491625447 47779840 10972 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11665 10972 603 41 0 11624 0
vsize: 46660
[startup+880.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11166 0 0 0 87949 64 0 0 25 0 1 0 491625447 48185344 11090 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11764 11090 603 41 0 11723 0
vsize: 47056
[startup+890.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11257 0 0 0 88949 65 0 0 25 0 1 0 491625447 48578560 11181 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11181 603 41 0 11819 0
vsize: 47440
[startup+900.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11362 0 0 0 89948 66 0 0 25 0 1 0 491625447 48979968 11286 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11958 11286 603 41 0 11917 0
vsize: 47832
[startup+910.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11435 0 0 0 90947 67 0 0 25 0 1 0 491625447 49393664 11359 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12059 11359 603 41 0 12018 0
vsize: 48236
[startup+920.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11498 0 0 0 91947 67 0 0 25 0 1 0 491625447 49528832 11422 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12092 11422 603 41 0 12051 0
vsize: 48368
[startup+930.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11580 0 0 0 92947 67 0 0 25 0 1 0 491625447 49926144 11504 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12189 11504 603 41 0 12148 0
vsize: 48756
[startup+940.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11664 0 0 0 93946 68 0 0 25 0 1 0 491625447 50855936 11588 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12416 11588 603 41 0 12375 0
vsize: 49664
[startup+950.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11755 0 0 0 94945 69 0 0 25 0 1 0 491625447 51118080 11679 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12480 11679 603 41 0 12439 0
vsize: 49920
[startup+960.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11847 0 0 0 95945 69 0 0 25 0 1 0 491625447 51515392 11771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12577 11771 603 41 0 12536 0
vsize: 50308
[startup+970.043 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11916 0 0 0 96945 70 0 0 25 0 1 0 491625447 51789824 11840 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12644 11840 603 41 0 12603 0
vsize: 50576
[startup+980.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 11985 0 0 0 97944 71 0 0 25 0 1 0 491625447 52060160 11909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12710 11909 603 41 0 12669 0
vsize: 50840
[startup+990.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12057 0 0 0 98943 72 0 0 25 0 1 0 491625447 52457472 11981 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12807 11981 603 41 0 12766 0
vsize: 51228
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 21945
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12125 0 0 0 99943 72 0 0 25 0 1 0 491625447 52723712 12049 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12872 12049 603 41 0 12831 0
vsize: 51488
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 21946
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12199 0 0 0 100943 73 0 0 25 0 1 0 491625447 52985856 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12936 12123 603 41 0 12895 0
vsize: 51744
[startup+1020.05 s]
Raw data (loadavg): 1.07 1.00 0.95 2/54 21998
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12268 0 0 0 101943 73 0 0 25 0 1 0 491625447 53252096 12192 4294967295 134512640 134672761 3221224624 3221223760 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13001 12192 603 41 0 12960 0
vsize: 52004
[startup+1030.05 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 21998
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12330 0 0 0 102943 73 0 0 25 0 1 0 491625447 53526528 12254 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13068 12254 603 41 0 13027 0
vsize: 52272
[startup+1040.05 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 21998
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12401 0 0 0 103943 73 0 0 25 0 1 0 491625447 53792768 12325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13133 12325 603 41 0 13092 0
vsize: 52532
[startup+1050.05 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 21998
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12476 0 0 0 104943 73 0 0 25 0 1 0 491625447 54063104 12400 4294967295 134512640 134672761 3221224624 3221223760 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13199 12400 603 41 0 13158 0
vsize: 52796
[startup+1060.05 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 21998
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12566 0 0 0 105942 74 0 0 25 0 1 0 491625447 54476800 12490 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12490 603 41 0 13259 0
vsize: 53200
[startup+1070.05 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 21998
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12660 0 0 0 106942 74 0 0 25 0 1 0 491625447 54874112 12584 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13397 12584 603 41 0 13356 0
vsize: 53588
[startup+1080.05 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 21998
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12754 0 0 0 107941 74 0 0 25 0 1 0 491625447 55279616 12678 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13496 12678 603 41 0 13455 0
vsize: 53984
[startup+1090.05 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12835 0 0 0 108941 75 0 0 25 0 1 0 491625447 55545856 12759 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13561 12759 603 41 0 13520 0
vsize: 54244
[startup+1100.05 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 12916 0 0 0 109941 75 0 0 25 0 1 0 491625447 55816192 12840 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13627 12840 603 41 0 13586 0
vsize: 54508
[startup+1110.05 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13005 0 0 0 110941 76 0 0 25 0 1 0 491625447 56221696 12929 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13726 12929 603 41 0 13685 0
vsize: 54904
[startup+1120.05 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13096 0 0 0 111940 76 0 0 25 0 1 0 491625447 56614912 13020 4294967295 134512640 134672761 3221224624 3221223808 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13822 13020 603 41 0 13781 0
vsize: 55288
[startup+1130.05 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13187 0 0 0 112940 77 0 0 25 0 1 0 491625447 57024512 13111 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13922 13111 603 41 0 13881 0
vsize: 55688
[startup+1140.05 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13261 0 0 0 113939 77 0 0 25 0 1 0 491625447 57294848 13185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13988 13185 603 41 0 13947 0
vsize: 55952
[startup+1150.05 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13354 0 0 0 114939 78 0 0 25 0 1 0 491625447 57561088 13278 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14053 13278 603 41 0 14012 0
vsize: 56212
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13434 0 0 0 115938 78 0 0 25 0 1 0 491625447 57962496 13358 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14151 13358 603 41 0 14110 0
vsize: 56604
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13515 0 0 0 116938 79 0 0 25 0 1 0 491625447 58228736 13439 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14216 13439 603 41 0 14175 0
vsize: 56864
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13590 0 0 0 117938 79 0 0 25 0 1 0 491625447 58630144 13514 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14314 13514 603 41 0 14273 0
vsize: 57256
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13666 0 0 0 118938 79 0 0 25 0 1 0 491625447 58896384 13590 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14379 13590 603 41 0 14338 0
vsize: 57516
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 22000
Raw data (stat): 21945 (minisat+) R 21944 29151 29150 0 -1 0 13728 0 0 0 119938 80 0 0 25 0 1 0 491625447 59162624 13652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14444 13652 603 41 0 14403 0
vsize: 57776
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 22000
Raw data (stat): 21945 (minisat+) Z 21944 29151 29150 0 -1 12 13731 0 0 0 119938 82 0 0 25 0 1 0 491625447 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.21
CPU user time (s): 1199.38
CPU system time (s): 0.828873
CPU usage (%): 100.011
Max. virtual memory (Kb): 57776
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####