PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-e64.b.opb
MD5SUM	bf7f8537c6faa135d25c67c53576abb5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	49
Optimality of the best value was proved	NO
Number of terms in the objective function	608
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	608
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	608
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	607
Total number of constraints	1053
Number of constraints which are clauses	1022
Number of constraints which are cardinality constraints (but not clauses)	31
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	32
Trace number 4659

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-13 19:43:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3450 boxname=wulflinc23 idbench=66 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf7f8537c6faa135d25c67c53576abb5  /oldhome/oroussel/tmp/wulflinc23/normalized-e64.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-e64.b.opb /oldhome/oroussel/tmp/wulflinc23/normalized-e64.b.opb
IDLAUNCH: 3450
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        912444 kB
Buffers:         33880 kB
Cached:          45760 kB
SwapCached:        192 kB
Active:          44392 kB
Inactive:        38300 kB
HighTotal:      131008 kB
HighFree:        81368 kB
LowTotal:       903652 kB
LowFree:        831076 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            33896 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:03:04 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3450 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1022 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1022     8200 |     340       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1210   maxlim: 526   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |    9411    38155 |    3137       1       16    16.0 |  0.000 % |
c |       101 |    9411    38155 |    3450     101      442     4.4 |  0.604 % |
c |       251 |    9411    38155 |    3795     251     1124     4.5 |  0.604 % |
c |       476 |    9411    38155 |    4175     476     2099     4.4 |  0.604 % |
c |       813 |    9395    38103 |    4592     810     4022     5.0 |  0.768 % |
c |      1320 |    9395    38103 |    5052    1317     9177     7.0 |  0.768 % |
c |      2081 |    9395    38103 |    5557    2078    63712    30.7 |  0.768 % |
c |      3222 |    9395    38103 |    6113    3219   114041    35.4 |  0.768 % |
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 528   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3937 |    9399    38121 |    3133    3934   132020    33.6 |  0.768 % |
c |      4037 |    9399    38121 |    3446    2067    40884    19.8 |  0.877 % |
c |      4187 |    9399    38121 |    3790    2217    43496    19.6 |  0.877 % |
c |      4412 |    9399    38121 |    4170    2442    48550    19.9 |  0.877 % |
c |      4751 |    9399    38121 |    4587    2781    56122    20.2 |  0.877 % |
c |      5257 |    9399    38121 |    5045    3287    90194    27.4 |  0.877 % |
c |      6016 |    9399    38121 |    5550    4046   110167    27.2 |  0.877 % |
c |      7156 |    9399    38121 |    6105    5186   204655    39.5 |  0.877 % |
c ==============================================================================
c [1mFound solution: 79[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 529   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7604 |    9400    38128 |    3133    5634   219009    38.9 |  0.877 % |
c |      7704 |    9400    38128 |    3446    2917    94937    32.5 |  0.932 % |
c |      7855 |    9400    38128 |    3790    3068    98949    32.3 |  0.932 % |
c |      8081 |    9400    38128 |    4170    3294   106549    32.3 |  0.932 % |
c |      8418 |    9400    38128 |    4587    3631   132514    36.5 |  0.932 % |
c |      8924 |    9400    38128 |    5045    4137   161119    38.9 |  0.932 % |
c |      9683 |    9400    38128 |    5550    4896   233782    47.7 |  0.932 % |
c |     10823 |    9400    38128 |    6105    3113   161863    52.0 |  0.932 % |
c |     12531 |    9400    38128 |    6715    4821   270889    56.2 |  0.932 % |
c |     15093 |    9400    38128 |    7387    3790   188014    49.6 |  0.932 % |
c ==============================================================================
c [1mFound solution: 78[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 530   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17758 |    9401    38136 |    3133    6455   329691    51.1 |  0.932 % |
c |     17858 |    9401    38136 |    3446    1714    24243    14.1 |  0.986 % |
c |     18008 |    9401    38136 |    3790    1864    25401    13.6 |  0.986 % |
c |     18233 |    9401    38136 |    4170    2089    29380    14.1 |  0.986 % |
c |     18571 |    9401    38136 |    4587    2427    50665    20.9 |  0.986 % |
c |     19077 |    9401    38136 |    5045    2933    64336    21.9 |  0.986 % |
c |     19837 |    9401    38136 |    5550    3693   101278    27.4 |  0.986 % |
c |     20979 |    9401    38136 |    6105    4835   240887    49.8 |  0.986 % |
c |     22687 |    9401    38136 |    6715    6543   403193    61.6 |  0.986 % |
c |     25252 |    9401    38136 |    7387    5323   439924    82.6 |  0.986 % |
c |     29097 |    9401    38136 |    8126    5415   391208    72.2 |  0.986 % |
c |     34863 |    9401    38136 |    8938    7021   559707    79.7 |  0.986 % |
c |     43513 |    9401    38136 |    9832    6482   591363    91.2 |  0.986 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 536   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47463 |    9404    38151 |    3134   10432   768617    73.7 |  0.986 % |
c |     47563 |    9404    38151 |    3447    2708    62538    23.1 |  1.094 % |
c |     47715 |    9404    38151 |    3792    2860    68391    23.9 |  1.094 % |
c |     47940 |    9404    38151 |    4171    3085    75466    24.5 |  1.094 % |
c |     48281 |    9404    38151 |    4588    3426    90116    26.3 |  1.094 % |
c |     48789 |    9404    38151 |    5047    3934   111517    28.3 |  1.094 % |
c |     49552 |    9404    38151 |    5552    4697   132583    28.2 |  1.094 % |
c |     50694 |    9404    38151 |    6107    5839   223876    38.3 |  1.094 % |
c |     52402 |    9404    38151 |    6718    4263   171799    40.3 |  1.094 % |
c |     54966 |    9404    38151 |    7389    6827   416683    61.0 |  1.094 % |
c |     58811 |    9404    38151 |    8128    6680   556831    83.4 |  1.094 % |
c |     64577 |    9404    38151 |    8941    8016   552242    68.9 |  1.094 % |
c |     73227 |    9404    38151 |    9835    7129   602754    84.5 |  1.094 % |
c |     86201 |    9404    38151 |   10819    9945  1114895   112.1 |  1.094 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 538   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91259 |    9407    38168 |    3135    9122   731010    80.1 |  1.094 % |
c |     91359 |    9407    38168 |    3448    2381   156758    65.8 |  1.201 % |
c |     91509 |    9407    38168 |    3793    2531   157955    62.4 |  1.201 % |
c |     91734 |    9407    38168 |    4172    2756   160926    58.4 |  1.201 % |
c |     92072 |    9407    38168 |    4589    3094   165238    53.4 |  1.201 % |
c |     92578 |    9407    38168 |    5048    3600   179522    49.9 |  1.201 % |
c |     93337 |    9407    38168 |    5553    4359   208989    47.9 |  1.201 % |
c |     94477 |    9407    38168 |    6109    5499   289266    52.6 |  1.201 % |
c |     96185 |    9407    38168 |    6720    3710   149164    40.2 |  1.201 % |
c |     98747 |    9407    38168 |    7392    6272   304515    48.6 |  1.201 % |
c |    102591 |    9407    38168 |    8131    6094   479853    78.7 |  1.201 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 544   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103651 |    9414    38196 |    3138    7154   574820    80.3 |  1.201 % |
c |    103752 |    9414    38196 |    3451    1890    35093    18.6 |  1.308 % |
c |    103902 |    9414    38196 |    3796    2040    36642    18.0 |  1.308 % |
c |    104127 |    9414    38196 |    4176    2265    42160    18.6 |  1.308 % |
c |    104466 |    9414    38196 |    4594    2604    52863    20.3 |  1.308 % |
c |    104975 |    9414    38196 |    5053    3113    69155    22.2 |  1.308 % |
c |    105734 |    9414    38196 |    5559    3872   124989    32.3 |  1.308 % |
c |    106873 |    9414    38196 |    6115    5011   233763    46.6 |  1.308 % |
c |    108581 |    9414    38196 |    6726    6719   431438    64.2 |  1.308 % |
c |    111143 |    9414    38196 |    7399    5592   385479    68.9 |  1.308 % |
c |    114988 |    9414    38196 |    8139    5494   377851    68.8 |  1.308 % |
c |    120754 |    9414    38196 |    8953    6928   693458   100.1 |  1.308 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 545   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127556 |    9416    38205 |    3138    8831  1069963   121.2 |  1.308 % |
c |    127656 |    9416    38205 |    3451    2308   163694    70.9 |  1.361 % |
c |    127806 |    9416    38205 |    3796    2458   164639    67.0 |  1.361 % |
c |    128031 |    9416    38205 |    4176    2683   166857    62.2 |  1.361 % |
c |    128368 |    9416    38205 |    4594    3020   173608    57.5 |  1.361 % |
c |    128875 |    9416    38205 |    5053    3527   192692    54.6 |  1.361 % |
c |    129634 |    9416    38205 |    5559    4286   231220    53.9 |  1.361 % |
c |    130775 |    9416    38205 |    6115    5427   339378    62.5 |  1.361 % |
c |    132483 |    9416    38205 |    6726    3738   253185    67.7 |  1.361 % |
c |    135045 |    9416    38205 |    7399    6300   554481    88.0 |  1.361 % |
c |    138889 |    9416    38205 |    8139    6039   479915    79.5 |  1.361 % |
c |    144655 |    9416    38205 |    8953    7504   874482   116.5 |  1.361 % |
c |    153305 |    9416    38205 |    9848    6760   817355   120.9 |  1.361 % |
c |    166281 |    9416    38205 |   10833    9273  1138630   122.8 |  1.361 % |
c |    185744 |    9416    38205 |   11916   11738  1630700   138.9 |  1.361 % |
c |    214939 |    9416    38205 |   13108    9755  1300834   133.4 |  1.361 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 546   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    232712 |    9418    38214 |    3139    7356   865878   117.7 |  1.361 % |
c |    232812 |    9418    38214 |    3452    1939    62656    32.3 |  1.414 % |
c |    232963 |    9418    38214 |    3798    2090    63821    30.5 |  1.414 % |
c |    233188 |    9418    38214 |    4178    2315    65448    28.3 |  1.414 % |
c |    233526 |    9418    38214 |    4595    2653    70536    26.6 |  1.414 % |
c |    234032 |    9418    38214 |    5055    3159    95277    30.2 |  1.414 % |
c |    234791 |    9418    38214 |    5560    3918   132740    33.9 |  1.414 % |
c |    235930 |    9418    38214 |    6117    5057   203750    40.3 |  1.414 % |
c |    237639 |    9418    38214 |    6728    6766   367311    54.3 |  1.414 % |
c |    240202 |    9418    38214 |    7401    5946   321572    54.1 |  1.414 % |
c |    244046 |    9418    38214 |    8141    5829   481075    82.5 |  1.414 % |
c |    249814 |    9418    38214 |    8955    7233   328140    45.4 |  1.414 % |
c |    258465 |    9418    38214 |    9851    6333   619241    97.8 |  1.414 % |
c |    271439 |    9418    38214 |   10836    8906   777237    87.3 |  1.414 % |
c |    290901 |    9418    38214 |   11920   11367  1588541   139.8 |  1.414 % |
c |    320097 |    9418    38214 |   13112    9787  1014716   103.7 |  1.414 % |
c |    363891 |    9418    38214 |   14423   12868  1589759   123.5 |  1.414 % |
c |    429576 |    9418    38214 |   15865   12007  1855678   154.5 |  1.414 % |
c |    528103 |    9418    38214 |   17452   12817  1004864    78.4 |  1.414 % |
c |    675892 |    9418    38214 |   19197   16876  3121436   185.0 |  1.414 % |
c |    897575 |    9418    38214 |   21117   11273  1899807   168.5 |  1.414 % |
#### 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.84 0.94 0.70 2/54 4633
Raw data (stat): 4633 (runsolver) R 4632 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478558471 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0011 s]
Raw data (loadavg): 0.87 0.94 0.70 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 1151 0 0 0 994 4 0 0 25 0 1 0 478558471 6242304 1129 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1524 1129 603 41 0 1483 0
vsize: 6096
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.70 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 1506 0 0 0 1992 5 0 0 25 0 1 0 478558471 7733248 1484 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1888 1484 603 41 0 1847 0
vsize: 7552
[startup+30.0008 s]
Raw data (loadavg): 0.90 0.94 0.70 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 1607 0 0 0 2992 5 0 0 25 0 1 0 478558471 8138752 1585 4294967295 134512640 134672761 3221224576 3221223760 134558934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1585 603 41 0 1946 0
vsize: 7948
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.94 0.71 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 1716 0 0 0 3991 5 0 0 25 0 1 0 478558471 8540160 1694 4294967295 134512640 134672761 3221224576 3221223576 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2085 1694 603 41 0 2044 0
vsize: 8340
[startup+50 s]
Raw data (loadavg): 0.93 0.94 0.71 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 1936 0 0 0 4991 6 0 0 25 0 1 0 478558471 9478144 1914 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2314 1914 603 41 0 2273 0
vsize: 9256
[startup+59.9996 s]
Raw data (loadavg): 0.94 0.94 0.71 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2131 0 0 0 5991 6 0 0 25 0 1 0 478558471 10297344 2109 4294967295 134512640 134672761 3221224576 3221223700 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2514 2109 603 41 0 2473 0
vsize: 10056
[startup+69.9996 s]
Raw data (loadavg): 0.95 0.95 0.72 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2131 0 0 0 6991 6 0 0 25 0 1 0 478558471 10297344 2109 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2514 2109 603 41 0 2473 0
vsize: 10056
[startup+79.9989 s]
Raw data (loadavg): 0.96 0.95 0.72 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2131 0 0 0 7991 6 0 0 25 0 1 0 478558471 10297344 2109 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2514 2109 603 41 0 2473 0
vsize: 10056
[startup+89.9986 s]
Raw data (loadavg): 0.96 0.95 0.72 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2158 0 0 0 8991 6 0 0 25 0 1 0 478558471 10428416 2136 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2546 2136 603 41 0 2505 0
vsize: 10184
[startup+99.9984 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2337 0 0 0 9990 7 0 0 25 0 1 0 478558471 11096064 2315 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2709 2315 603 41 0 2668 0
vsize: 10836
[startup+109.999 s]
Raw data (loadavg): 0.97 0.95 0.73 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2463 0 0 0 10990 7 0 0 25 0 1 0 478558471 11636736 2441 4294967295 134512640 134672761 3221224576 3221223816 134558237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2841 2441 603 41 0 2800 0
vsize: 11364
[startup+119.998 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2478 0 0 0 11990 7 0 0 25 0 1 0 478558471 11636736 2456 4294967295 134512640 134672761 3221224576 3221223680 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2841 2456 603 41 0 2800 0
vsize: 11364
[startup+129.998 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2826 0 0 0 12989 8 0 0 25 0 1 0 478558471 13123584 2804 4294967295 134512640 134672761 3221224576 3221223760 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3204 2804 603 41 0 3163 0
vsize: 12816
[startup+139.999 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 2963 0 0 0 13989 9 0 0 25 0 1 0 478558471 13664256 2941 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3336 2941 603 41 0 3295 0
vsize: 13344
[startup+149.998 s]
Raw data (loadavg): 0.98 0.95 0.74 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3099 0 0 0 14989 9 0 0 25 0 1 0 478558471 14200832 3077 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3077 603 41 0 3426 0
vsize: 13868
[startup+159.999 s]
Raw data (loadavg): 0.99 0.95 0.74 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3099 0 0 0 15989 9 0 0 25 0 1 0 478558471 14200832 3077 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3077 603 41 0 3426 0
vsize: 13868
[startup+169.999 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3100 0 0 0 16989 9 0 0 25 0 1 0 478558471 14200832 3078 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3078 603 41 0 3426 0
vsize: 13868
[startup+179.998 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3100 0 0 0 17989 9 0 0 25 0 1 0 478558471 14200832 3078 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3078 603 41 0 3426 0
vsize: 13868
[startup+189.999 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3100 0 0 0 18990 9 0 0 25 0 1 0 478558471 14200832 3078 4294967295 134512640 134672761 3221224576 3221223760 134559356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3078 603 41 0 3426 0
vsize: 13868
[startup+199.999 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3100 0 0 0 19990 9 0 0 25 0 1 0 478558471 14200832 3078 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3078 603 41 0 3426 0
vsize: 13868
[startup+209.998 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3100 0 0 0 20990 10 0 0 25 0 1 0 478558471 14200832 3078 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3078 603 41 0 3426 0
vsize: 13868
[startup+219.999 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3100 0 0 0 21990 10 0 0 25 0 1 0 478558471 14200832 3078 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3467 3078 603 41 0 3426 0
vsize: 13868
[startup+229.998 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3256 0 0 0 22990 10 0 0 25 0 1 0 478558471 14872576 3234 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3631 3234 603 41 0 3590 0
vsize: 14524
[startup+239.998 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3275 0 0 0 23990 10 0 0 25 0 1 0 478558471 15007744 3253 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3664 3253 603 41 0 3623 0
vsize: 14656
[startup+249.998 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3275 0 0 0 24990 10 0 0 25 0 1 0 478558471 15007744 3253 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3664 3253 603 41 0 3623 0
vsize: 14656
[startup+259.998 s]
Raw data (loadavg): 0.99 0.96 0.76 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3275 0 0 0 25990 10 0 0 25 0 1 0 478558471 15007744 3253 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3664 3253 603 41 0 3623 0
vsize: 14656
[startup+269.998 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3391 0 0 0 26990 10 0 0 25 0 1 0 478558471 15409152 3369 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3762 3369 603 41 0 3721 0
vsize: 15048
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3412 0 0 0 27990 10 0 0 25 0 1 0 478558471 15540224 3390 4294967295 134512640 134672761 3221224576 3221223760 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3794 3390 603 41 0 3753 0
vsize: 15176
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3440 0 0 0 28990 10 0 0 25 0 1 0 478558471 15671296 3418 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3826 3418 603 41 0 3785 0
vsize: 15304
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3653 0 0 0 29990 11 0 0 25 0 1 0 478558471 16474112 3631 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4022 3631 603 41 0 3981 0
vsize: 16088
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 3907 0 0 0 30989 12 0 0 25 0 1 0 478558471 17543168 3885 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4283 3885 603 41 0 4242 0
vsize: 17132
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4146 0 0 0 31989 13 0 0 25 0 1 0 478558471 18485248 4124 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4124 603 41 0 4472 0
vsize: 18052
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4146 0 0 0 32989 13 0 0 25 0 1 0 478558471 18485248 4124 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4124 603 41 0 4472 0
vsize: 18052
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4147 0 0 0 33989 13 0 0 25 0 1 0 478558471 18485248 4125 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4125 603 41 0 4472 0
vsize: 18052
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4147 0 0 0 34989 13 0 0 25 0 1 0 478558471 18485248 4125 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4125 603 41 0 4472 0
vsize: 18052
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4147 0 0 0 35989 13 0 0 25 0 1 0 478558471 18485248 4125 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4125 603 41 0 4472 0
vsize: 18052
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4147 0 0 0 36989 13 0 0 25 0 1 0 478558471 18485248 4125 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4125 603 41 0 4472 0
vsize: 18052
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4147 0 0 0 37990 13 0 0 25 0 1 0 478558471 18485248 4125 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4125 603 41 0 4472 0
vsize: 18052
[startup+390 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4165 0 0 0 38990 13 0 0 25 0 1 0 478558471 18735104 4143 4294967295 134512640 134672761 3221224576 3221223760 134558768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4574 4143 603 41 0 4533 0
vsize: 18296
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4165 0 0 0 39990 13 0 0 25 0 1 0 478558471 18735104 4143 4294967295 134512640 134672761 3221224576 3221223760 134559509 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4574 4143 603 41 0 4533 0
vsize: 18296
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4165 0 0 0 40990 13 0 0 25 0 1 0 478558471 18735104 4143 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4574 4143 603 41 0 4533 0
vsize: 18296
[startup+420 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4165 0 0 0 41990 13 0 0 25 0 1 0 478558471 18735104 4143 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4574 4143 603 41 0 4533 0
vsize: 18296
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4165 0 0 0 42990 13 0 0 25 0 1 0 478558471 18735104 4143 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4574 4143 603 41 0 4533 0
vsize: 18296
[startup+440 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4165 0 0 0 43991 13 0 0 25 0 1 0 478558471 18735104 4143 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4574 4143 603 41 0 4533 0
vsize: 18296
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4313 0 0 0 44990 14 0 0 25 0 1 0 478558471 19267584 4291 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4704 4291 603 41 0 4663 0
vsize: 18816
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4355 0 0 0 45990 14 0 0 25 0 1 0 478558471 19398656 4333 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4333 603 41 0 4695 0
vsize: 18944
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4355 0 0 0 46990 14 0 0 25 0 1 0 478558471 19398656 4333 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4333 603 41 0 4695 0
vsize: 18944
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4355 0 0 0 47990 14 0 0 25 0 1 0 478558471 19398656 4333 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4333 603 41 0 4695 0
vsize: 18944
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4356 0 0 0 48990 14 0 0 25 0 1 0 478558471 19398656 4334 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4334 603 41 0 4695 0
vsize: 18944
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4356 0 0 0 49991 14 0 0 25 0 1 0 478558471 19398656 4334 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4334 603 41 0 4695 0
vsize: 18944
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4356 0 0 0 50991 14 0 0 25 0 1 0 478558471 19398656 4334 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4334 603 41 0 4695 0
vsize: 18944
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4356 0 0 0 51991 14 0 0 25 0 1 0 478558471 19398656 4334 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4334 603 41 0 4695 0
vsize: 18944
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4356 0 0 0 52991 14 0 0 25 0 1 0 478558471 19398656 4334 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4334 603 41 0 4695 0
vsize: 18944
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4356 0 0 0 53991 14 0 0 25 0 1 0 478558471 19398656 4334 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4736 4334 603 41 0 4695 0
vsize: 18944
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 4834 0 0 0 54990 16 0 0 25 0 1 0 478558471 21413888 4812 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5228 4812 603 41 0 5187 0
vsize: 20912
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5004 0 0 0 55990 16 0 0 25 0 1 0 478558471 22102016 4982 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4982 603 41 0 5355 0
vsize: 21584
[startup+570.002 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5385 0 0 0 56989 18 0 0 25 0 1 0 478558471 23728128 5363 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5363 603 41 0 5752 0
vsize: 23172
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5385 0 0 0 57989 18 0 0 25 0 1 0 478558471 23728128 5363 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5363 603 41 0 5752 0
vsize: 23172
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5385 0 0 0 58989 18 0 0 25 0 1 0 478558471 23728128 5363 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5363 603 41 0 5752 0
vsize: 23172
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5385 0 0 0 59989 18 0 0 25 0 1 0 478558471 23728128 5363 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5363 603 41 0 5752 0
vsize: 23172
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5533 0 0 0 60989 18 0 0 25 0 1 0 478558471 24268800 5511 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5925 5511 603 41 0 5884 0
vsize: 23700
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5533 0 0 0 61989 18 0 0 25 0 1 0 478558471 24268800 5511 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5925 5511 603 41 0 5884 0
vsize: 23700
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5539 0 0 0 62989 18 0 0 25 0 1 0 478558471 24424448 5517 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5963 5517 603 41 0 5922 0
vsize: 23852
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5539 0 0 0 63989 18 0 0 25 0 1 0 478558471 24424448 5517 4294967295 134512640 134672761 3221224576 3221223680 134554673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5963 5517 603 41 0 5922 0
vsize: 23852
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5539 0 0 0 64989 18 0 0 25 0 1 0 478558471 24424448 5517 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5963 5517 603 41 0 5922 0
vsize: 23852
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5539 0 0 0 65990 18 0 0 25 0 1 0 478558471 24424448 5517 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5963 5517 603 41 0 5922 0
vsize: 23852
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5539 0 0 0 66990 18 0 0 25 0 1 0 478558471 24424448 5517 4294967295 134512640 134672761 3221224576 3221223744 134561554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5963 5517 603 41 0 5922 0
vsize: 23852
[startup+680.004 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5539 0 0 0 67990 18 0 0 25 0 1 0 478558471 24424448 5517 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5963 5517 603 41 0 5922 0
vsize: 23852
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5638 0 0 0 68990 19 0 0 25 0 1 0 478558471 24825856 5616 4294967295 134512640 134672761 3221224576 3221223760 134559379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6061 5616 603 41 0 6020 0
vsize: 24244
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5655 0 0 0 69990 19 0 0 25 0 1 0 478558471 24825856 5633 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6061 5633 603 41 0 6020 0
vsize: 24244
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5693 0 0 0 70990 19 0 0 25 0 1 0 478558471 24961024 5671 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5671 603 41 0 6053 0
vsize: 24376
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5693 0 0 0 71990 19 0 0 25 0 1 0 478558471 24961024 5671 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5671 603 41 0 6053 0
vsize: 24376
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5693 0 0 0 72990 19 0 0 25 0 1 0 478558471 24961024 5671 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5671 603 41 0 6053 0
vsize: 24376
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5693 0 0 0 73990 19 0 0 25 0 1 0 478558471 24961024 5671 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5671 603 41 0 6053 0
vsize: 24376
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5803 0 0 0 74990 20 0 0 25 0 1 0 478558471 25501696 5781 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5781 603 41 0 6185 0
vsize: 24904
[startup+760.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5803 0 0 0 75990 20 0 0 25 0 1 0 478558471 25501696 5781 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5781 603 41 0 6185 0
vsize: 24904
[startup+770.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5809 0 0 0 76990 20 0 0 25 0 1 0 478558471 25501696 5787 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5787 603 41 0 6185 0
vsize: 24904
[startup+780.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5809 0 0 0 77991 20 0 0 25 0 1 0 478558471 25501696 5787 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5787 603 41 0 6185 0
vsize: 24904
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5809 0 0 0 78991 20 0 0 25 0 1 0 478558471 25501696 5787 4294967295 134512640 134672761 3221224576 3221223752 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5787 603 41 0 6185 0
vsize: 24904
[startup+800.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5809 0 0 0 79991 20 0 0 25 0 1 0 478558471 25501696 5787 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5787 603 41 0 6185 0
vsize: 24904
[startup+810.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5809 0 0 0 80991 20 0 0 25 0 1 0 478558471 25501696 5787 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5787 603 41 0 6185 0
vsize: 24904
[startup+820.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5809 0 0 0 81991 20 0 0 25 0 1 0 478558471 25501696 5787 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5787 603 41 0 6185 0
vsize: 24904
[startup+830.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 5809 0 0 0 82991 20 0 0 25 0 1 0 478558471 25501696 5787 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5787 603 41 0 6185 0
vsize: 24904
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6054 0 0 0 83991 20 0 0 25 0 1 0 478558471 26566656 6032 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 6032 603 41 0 6445 0
vsize: 25944
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6054 0 0 0 84991 20 0 0 25 0 1 0 478558471 26566656 6032 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6486 6032 603 41 0 6445 0
vsize: 25944
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6108 0 0 0 85991 21 0 0 25 0 1 0 478558471 26697728 6086 4294967295 134512640 134672761 3221224576 3221223760 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6086 603 41 0 6477 0
vsize: 26072
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6108 0 0 0 86992 21 0 0 25 0 1 0 478558471 26697728 6086 4294967295 134512640 134672761 3221224576 3221223760 134558836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6086 603 41 0 6477 0
vsize: 26072
[startup+880.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6108 0 0 0 87992 21 0 0 25 0 1 0 478558471 26697728 6086 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6086 603 41 0 6477 0
vsize: 26072
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6108 0 0 0 88992 21 0 0 25 0 1 0 478558471 26697728 6086 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6086 603 41 0 6477 0
vsize: 26072
[startup+900.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 89992 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+910.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 90992 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+920.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 91993 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+930.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 92993 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 93993 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+950.009 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 94993 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 95993 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6114 0 0 0 96994 21 0 0 25 0 1 0 478558471 26697728 6092 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6518 6092 603 41 0 6477 0
vsize: 26072
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6163 0 0 0 97994 21 0 0 25 0 1 0 478558471 26968064 6141 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6141 603 41 0 6543 0
vsize: 26336
[startup+990.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6489 0 0 0 98993 22 0 0 25 0 1 0 478558471 28311552 6467 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6912 6467 603 41 0 6871 0
vsize: 27648
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6489 0 0 0 99993 22 0 0 25 0 1 0 478558471 28311552 6467 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6912 6467 603 41 0 6871 0
vsize: 27648
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6711 0 0 0 100993 23 0 0 25 0 1 0 478558471 29257728 6689 4294967295 134512640 134672761 3221224576 3221223680 134559814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6689 603 41 0 7102 0
vsize: 28572
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 4633
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6716 0 0 0 101993 23 0 0 25 0 1 0 478558471 29257728 6694 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6694 603 41 0 7102 0
vsize: 28572
[startup+1030.01 s]
Raw data (loadavg): 1.07 0.99 0.87 2/54 4686
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6792 0 0 0 102989 26 0 0 25 0 1 0 478558471 29528064 6770 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6770 603 41 0 7168 0
vsize: 28836
[startup+1040.01 s]
Raw data (loadavg): 1.06 0.99 0.87 2/54 4686
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6792 0 0 0 103989 26 0 0 25 0 1 0 478558471 29528064 6770 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6770 603 41 0 7168 0
vsize: 28836
[startup+1050.01 s]
Raw data (loadavg): 1.05 0.99 0.87 2/54 4686
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6792 0 0 0 104990 26 0 0 25 0 1 0 478558471 29528064 6770 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6770 603 41 0 7168 0
vsize: 28836
[startup+1060.01 s]
Raw data (loadavg): 1.04 0.99 0.87 2/54 4686
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6792 0 0 0 105990 26 0 0 25 0 1 0 478558471 29528064 6770 4294967295 134512640 134672761 3221224576 3221223744 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7209 6770 603 41 0 7168 0
vsize: 28836
[startup+1070.01 s]
Raw data (loadavg): 1.03 0.99 0.87 2/54 4686
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6793 0 0 0 106990 26 0 0 25 0 1 0 478558471 29528064 6771 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6771 603 41 0 7168 0
vsize: 28836
[startup+1080.01 s]
Raw data (loadavg): 1.03 0.99 0.87 2/54 4686
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6794 0 0 0 107990 26 0 0 25 0 1 0 478558471 29528064 6772 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6772 603 41 0 7168 0
vsize: 28836
[startup+1090.01 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 4686
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6794 0 0 0 108990 26 0 0 25 0 1 0 478558471 29528064 6772 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6772 603 41 0 7168 0
vsize: 28836
[startup+1100.01 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6794 0 0 0 109990 26 0 0 25 0 1 0 478558471 29528064 6772 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6772 603 41 0 7168 0
vsize: 28836
[startup+1110.01 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6794 0 0 0 110990 26 0 0 25 0 1 0 478558471 29528064 6772 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6772 603 41 0 7168 0
vsize: 28836
[startup+1120.01 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6794 0 0 0 111991 26 0 0 25 0 1 0 478558471 29528064 6772 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7209 6772 603 41 0 7168 0
vsize: 28836
[startup+1130.01 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6828 0 0 0 112991 26 0 0 25 0 1 0 478558471 29675520 6806 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7245 6806 603 41 0 7204 0
vsize: 28980
[startup+1140.01 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6837 0 0 0 113991 26 0 0 25 0 1 0 478558471 29810688 6815 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7278 6815 603 41 0 7237 0
vsize: 29112
[startup+1150.01 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6885 0 0 0 114991 26 0 0 25 0 1 0 478558471 29945856 6863 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7311 6863 603 41 0 7270 0
vsize: 29244
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6885 0 0 0 115991 26 0 0 25 0 1 0 478558471 29945856 6863 4294967295 134512640 134672761 3221224576 3221223728 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7311 6863 603 41 0 7270 0
vsize: 29244
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6885 0 0 0 116991 26 0 0 25 0 1 0 478558471 29945856 6863 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7311 6863 603 41 0 7270 0
vsize: 29244
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6885 0 0 0 117992 26 0 0 25 0 1 0 478558471 29945856 6863 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7311 6863 603 41 0 7270 0
vsize: 29244
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6885 0 0 0 118992 26 0 0 25 0 1 0 478558471 29945856 6863 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7311 6863 603 41 0 7270 0
vsize: 29244
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 4688
Raw data (stat): 4633 (minisat+) R 4632 3260 3259 0 -1 0 6885 0 0 0 119992 26 0 0 25 0 1 0 478558471 29945856 6863 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7311 6863 603 41 0 7270 0
vsize: 29244
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.88 1/54 4688
Raw data (stat): 4633 (minisat+) Z 4632 3260 3259 0 -1 12 6888 0 0 0 119992 27 0 0 25 0 1 0 478558471 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.03
CPU time (s): 1200.2
CPU user time (s): 1199.93
CPU system time (s): 0.277957
CPU usage (%): 100.015
Max. virtual memory (Kb): 29244
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####