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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-3.opb
MD5SUM	25457db86ce3cc3b7604dfa37c8096b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
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	595
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	595
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	1175.05
Number of variables	595
Total number of constraints	27931
Number of constraints which are clauses	27931
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5237

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-13 22:49:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3705 boxname=wulflinc23 idbench=321 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  25457db86ce3cc3b7604dfa37c8096b4  /oldhome/oroussel/tmp/wulflinc23/normalized-frb35-17-3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-frb35-17-3.opb /oldhome/oroussel/tmp/wulflinc23/normalized-frb35-17-3.opb
IDLAUNCH: 3705
/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:        898200 kB
Buffers:         34240 kB
Cached:          59272 kB
SwapCached:        192 kB
Active:          48924 kB
Inactive:        47652 kB
HighTotal:      131008 kB
HighFree:        67900 kB
LowTotal:       903652 kB
LowFree:        830300 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34360 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:09:50 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3705 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27931 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 |   27931    55862 |    9310       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1165   maxlim: 25   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35889    84316 |   11963       0        0     nan |  0.000 % |
c |       100 |   35880    84285 |   13159      98      856     8.7 |  0.229 % |
c |       253 |   35862    84223 |   14475     246     2423     9.8 |  0.348 % |
c |       478 |   35853    84192 |   15922     468     4370     9.3 |  0.401 % |
c |       815 |   35835    84130 |   17515     800     7430     9.3 |  0.516 % |
c |      1322 |   35790    83975 |   19266    1290    13334    10.3 |  0.802 % |
c |      2081 |   35610    83359 |   21193    2009    24035    12.0 |  2.062 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 28   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2701 |   35489    82950 |   11829    2599    32999    12.7 |  2.062 % |
c |      2801 |   35451    82820 |   13011    2690    35004    13.0 |  3.488 % |
c |      2951 |   35436    82769 |   14313    2833    37843    13.4 |  3.602 % |
c |      3177 |   35436    82769 |   15744    3059    41455    13.6 |  3.602 % |
c |      3514 |   35361    82512 |   17318    3371    47553    14.1 |  4.122 % |
c |      4020 |   35104    81629 |   19050    3809    54345    14.3 |  6.118 % |
c |      4779 |   34897    80918 |   20955    4477    82201    18.4 |  7.833 % |
c |      5918 |   34677    80160 |   23051    5559   123121    22.1 |  9.834 % |
c |      7626 |   34484    79495 |   25356    7155   199296    27.9 | 11.607 % |
c |     10188 |   34475    79464 |   27892    9714   483408    49.8 | 11.670 % |
c |     14033 |   34211    78550 |   30681   13404   697502    52.0 | 14.180 % |
c |     19799 |   33992    77795 |   33749   19037  1089787    57.2 | 16.295 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22447 |   33961    77689 |   11320   21667  1271371    58.7 | 16.295 % |
c |     22547 |   33834    77252 |   12452   10909   570946    52.3 | 17.778 % |
c |     22697 |   33834    77252 |   13697   11059   577769    52.2 | 17.778 % |
c |     22922 |   33793    77111 |   15066   11236   584668    52.0 | 18.122 % |
c |     23260 |   33793    77111 |   16573   11574   606256    52.4 | 18.120 % |
c |     23766 |   33793    77111 |   18230   12080   636696    52.7 | 18.120 % |
c |     24525 |   33678    76716 |   20054   12822   684056    53.4 | 19.319 % |
c |     25665 |   33678    76716 |   22059   13962   793589    56.8 | 19.314 % |
c |     27373 |   33672    76696 |   24265   15666   942202    60.1 | 19.371 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27445 |   33677    76719 |   11225   15738   946417    60.1 | 19.371 % |
c |     27545 |   33660    76660 |   12347    7965   429713    54.0 | 19.589 % |
c |     27696 |   33635    76573 |   13582    8113   436323    53.8 | 19.874 % |
c |     27922 |   33635    76573 |   14940    8339   450996    54.1 | 19.883 % |
c |     28259 |   33635    76573 |   16434    8676   476725    54.9 | 19.874 % |
c |     28765 |   33610    76486 |   18077    9178   509236    55.5 | 20.160 % |
c |     29524 |   33595    76435 |   19885    9930   548104    55.2 | 20.279 % |
c |     30664 |   33584    76396 |   21874   11067   674186    60.9 | 20.394 % |
c |     32372 |   33552    76282 |   24061   12768   798976    62.6 | 20.788 % |
c |     34936 |   33398    75746 |   26467   15283   959337    62.8 | 22.330 % |
c |     38780 |   33398    75746 |   29114   19127  1284909    67.2 | 22.330 % |
c |     44546 |   33366    75636 |   32026   24890  1990973    80.0 | 22.730 % |
c |     53195 |   33279    75333 |   35228   15282  1138599    74.5 | 23.644 % |
c |     66170 |   33235    75181 |   38751   28245  2635238    93.3 | 24.101 % |
c |     85631 |   33235    75181 |   42626   21653  2678060   123.7 | 24.104 % |
c |    114823 |   33235    75181 |   46889   21257  2080744    97.9 | 24.104 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    142132 |   33163    74924 |   11054   15607  1028071    65.9 | 24.104 % |
c |    142232 |   33163    74924 |   12159    7904   328845    41.6 | 24.905 % |
c |    142382 |   33163    74924 |   13375    8054   335305    41.6 | 24.900 % |
c |    142607 |   33163    74924 |   14712    8279   342341    41.4 | 24.903 % |
c |    142944 |   33132    74819 |   16184    8610   352785    41.0 | 25.585 % |
c |    143450 |   33094    74687 |   17802    9108   378978    41.6 | 25.643 % |
c |    144209 |   33094    74687 |   19582    9867   424898    43.1 | 25.643 % |
c |    145348 |   33079    74636 |   21541   11003   482271    43.8 | 25.757 % |
c |    147056 |   33059    74566 |   23695   12703   610879    48.1 | 25.928 % |
c |    149621 |   33059    74566 |   26064   15268   855623    56.0 | 25.928 % |
c |    153465 |   33059    74566 |   28671   19112  1241442    65.0 | 25.932 % |
c |    159231 |   33044    74515 |   31538   24873  1562551    62.8 | 26.042 % |
c |    167880 |   33044    74515 |   34692   14680  1039164    70.8 | 26.047 % |
c |    180856 |   33014    74413 |   38161   27640  1976060    71.5 | 26.275 % |
c |    200318 |   32955    74208 |   41977   22393  1767719    78.9 | 26.899 % |
c |    229510 |   32955    74208 |   46175   23121  1156171    50.0 | 26.899 % |
c |    273299 |   32946    74177 |   50792   34601  3330214    96.2 | 26.961 % |
c |    338984 |   32946    74177 |   55872   27689  1966812    71.0 | 26.959 % |
c |    437511 |   32946    74177 |   61459   43636  3027699    69.4 | 26.961 % |
c |    585300 |   32925    74106 |   67605   53905  2040837    37.9 | 27.132 % |
#### 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.94 0.98 0.91 2/54 6342
Raw data (stat): 6342 (runsolver) R 6341 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479679207 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99983 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 1696 0 0 0 994 4 0 0 25 0 1 0 479679207 8495104 1674 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2074 1674 603 41 0 2033 0
vsize: 8296
[startup+19.9999 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 2348 0 0 0 1991 7 0 0 25 0 1 0 479679207 11190272 2326 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2732 2326 603 41 0 2691 0
vsize: 10928
[startup+30.0005 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 2348 0 0 0 2990 7 0 0 25 0 1 0 479679207 11190272 2326 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2732 2326 603 41 0 2691 0
vsize: 10928
[startup+39.9996 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 3216 0 0 0 3987 10 0 0 25 0 1 0 479679207 14671872 3194 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3194 603 41 0 3541 0
vsize: 14328
[startup+50.0005 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 3797 0 0 0 4985 12 0 0 25 0 1 0 479679207 17084416 3775 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4171 3775 603 41 0 4130 0
vsize: 16684
[startup+60.0001 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 3872 0 0 0 5985 12 0 0 25 0 1 0 479679207 17481728 3850 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4268 3850 603 41 0 4227 0
vsize: 17072
[startup+69.9995 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 3872 0 0 0 6986 12 0 0 25 0 1 0 479679207 17481728 3850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4268 3850 603 41 0 4227 0
vsize: 17072
[startup+80.0004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 4481 0 0 0 7984 14 0 0 25 0 1 0 479679207 20029440 4459 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4890 4459 603 41 0 4849 0
vsize: 19560
[startup+90 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 5159 0 0 0 8981 17 0 0 25 0 1 0 479679207 22716416 5137 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5546 5137 603 41 0 5505 0
vsize: 22184
[startup+100 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 5473 0 0 0 9980 18 0 0 25 0 1 0 479679207 24064000 5451 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5875 5451 603 41 0 5834 0
vsize: 23500
[startup+110 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 5473 0 0 0 10981 18 0 0 25 0 1 0 479679207 24064000 5451 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5875 5451 603 41 0 5834 0
vsize: 23500
[startup+120 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 5473 0 0 0 11981 18 0 0 25 0 1 0 479679207 24064000 5451 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5875 5451 603 41 0 5834 0
vsize: 23500
[startup+130 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 5474 0 0 0 12981 18 0 0 25 0 1 0 479679207 24064000 5452 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5875 5452 603 41 0 5834 0
vsize: 23500
[startup+140 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 5834 0 0 0 13980 19 0 0 25 0 1 0 479679207 25526272 5812 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6232 5812 603 41 0 6191 0
vsize: 24928
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6331 0 0 0 14979 21 0 0 25 0 1 0 479679207 27537408 6309 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6309 603 41 0 6682 0
vsize: 26892
[startup+160 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6337 0 0 0 15979 21 0 0 25 0 1 0 479679207 27537408 6315 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6315 603 41 0 6682 0
vsize: 26892
[startup+170 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6337 0 0 0 16979 21 0 0 25 0 1 0 479679207 27537408 6315 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6315 603 41 0 6682 0
vsize: 26892
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6337 0 0 0 17979 21 0 0 25 0 1 0 479679207 27537408 6315 4294967295 134512640 134672761 3221224560 3221223744 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6315 603 41 0 6682 0
vsize: 26892
[startup+190.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6337 0 0 0 18979 21 0 0 25 0 1 0 479679207 27537408 6315 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6315 603 41 0 6682 0
vsize: 26892
[startup+200.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6340 0 0 0 19979 21 0 0 25 0 1 0 479679207 27537408 6318 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6318 603 41 0 6682 0
vsize: 26892
[startup+210.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 20979 21 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+220.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 21977 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+230.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 22977 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+240.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 23977 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+250.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 24977 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+260.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 25977 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+270.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 26977 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223664 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+280.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 27978 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+290.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 28978 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+300.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 29978 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+310.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 30978 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+320.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 31979 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+330.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 32979 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+340.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 33979 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+350.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 34979 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+360.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 35979 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+370.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 36980 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+380.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 37980 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223516 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+390.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 38980 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+400.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 39980 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+410.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 40980 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+420.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 41980 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+430.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 42981 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223744 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+440.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6341 0 0 0 43981 22 0 0 25 0 1 0 479679207 27537408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6723 6319 603 41 0 6682 0
vsize: 26892
[startup+450.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6456 0 0 0 44981 22 0 0 25 0 1 0 479679207 28065792 6434 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6852 6434 603 41 0 6811 0
vsize: 27408
[startup+460.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6586 0 0 0 45980 23 0 0 25 0 1 0 479679207 28598272 6564 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6564 603 41 0 6941 0
vsize: 27928
[startup+470.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6586 0 0 0 46980 23 0 0 25 0 1 0 479679207 28598272 6564 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6564 603 41 0 6941 0
vsize: 27928
[startup+480.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6586 0 0 0 47981 23 0 0 25 0 1 0 479679207 28598272 6564 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6564 603 41 0 6941 0
vsize: 27928
[startup+490.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6586 0 0 0 48981 23 0 0 25 0 1 0 479679207 28598272 6564 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6564 603 41 0 6941 0
vsize: 27928
[startup+500.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6586 0 0 0 49981 23 0 0 25 0 1 0 479679207 28598272 6564 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6564 603 41 0 6941 0
vsize: 27928
[startup+510.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6595 0 0 0 50981 23 0 0 25 0 1 0 479679207 28598272 6573 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6573 603 41 0 6941 0
vsize: 27928
[startup+520.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6595 0 0 0 51981 23 0 0 25 0 1 0 479679207 28598272 6573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6573 603 41 0 6941 0
vsize: 27928
[startup+530.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 52982 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+540.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 53982 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+550.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 54982 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+560.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 55982 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+570.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 56982 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+580.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 57981 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+590.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 58981 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+600.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6596 0 0 0 59982 23 0 0 25 0 1 0 479679207 28598272 6574 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6574 603 41 0 6941 0
vsize: 27928
[startup+610.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6342
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6598 0 0 0 60982 23 0 0 25 0 1 0 479679207 28598272 6576 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6576 603 41 0 6941 0
vsize: 27928
[startup+620.007 s]
Raw data (loadavg): 1.07 1.00 0.92 3/58 6385
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 61982 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+630.008 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 6395
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 62982 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+640.007 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 6395
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 63982 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+650.008 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 6395
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 64983 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+660.007 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 6395
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 65983 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+670.007 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6395
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 66983 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+680.007 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6395
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 67983 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+690.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 68983 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+700.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 69983 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+710.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 70984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+720.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 71984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+730.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 72984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+740.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 73984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+750.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 74984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+760.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 75984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+770.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 76984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+780.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 77984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+790.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6601 0 0 0 78984 23 0 0 25 0 1 0 479679207 28598272 6579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6579 603 41 0 6941 0
vsize: 27928
[startup+800.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6604 0 0 0 79985 23 0 0 25 0 1 0 479679207 28598272 6582 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6582 603 41 0 6941 0
vsize: 27928
[startup+810.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6606 0 0 0 80985 23 0 0 25 0 1 0 479679207 28598272 6584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6584 603 41 0 6941 0
vsize: 27928
[startup+820.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6606 0 0 0 81985 23 0 0 25 0 1 0 479679207 28598272 6584 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6584 603 41 0 6941 0
vsize: 27928
[startup+830.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6606 0 0 0 82985 23 0 0 25 0 1 0 479679207 28598272 6584 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6584 603 41 0 6941 0
vsize: 27928
[startup+840.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6606 0 0 0 83985 23 0 0 25 0 1 0 479679207 28598272 6584 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6584 603 41 0 6941 0
vsize: 27928
[startup+850.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6606 0 0 0 84986 23 0 0 25 0 1 0 479679207 28598272 6584 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6982 6584 603 41 0 6941 0
vsize: 27928
[startup+860.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6615 0 0 0 85986 23 0 0 25 0 1 0 479679207 28758016 6593 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6593 603 41 0 6980 0
vsize: 28084
[startup+870.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6626 0 0 0 86986 23 0 0 25 0 1 0 479679207 28758016 6604 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6604 603 41 0 6980 0
vsize: 28084
[startup+880.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6630 0 0 0 87986 23 0 0 25 0 1 0 479679207 28758016 6608 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6608 603 41 0 6980 0
vsize: 28084
[startup+890.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6631 0 0 0 88986 23 0 0 25 0 1 0 479679207 28758016 6609 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6609 603 41 0 6980 0
vsize: 28084
[startup+900.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6631 0 0 0 89986 23 0 0 25 0 1 0 479679207 28758016 6609 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6609 603 41 0 6980 0
vsize: 28084
[startup+910.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6633 0 0 0 90987 23 0 0 25 0 1 0 479679207 28758016 6611 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6611 603 41 0 6980 0
vsize: 28084
[startup+920.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6633 0 0 0 91987 23 0 0 25 0 1 0 479679207 28758016 6611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6611 603 41 0 6980 0
vsize: 28084
[startup+930.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6397
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6633 0 0 0 92987 23 0 0 25 0 1 0 479679207 28758016 6611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6611 603 41 0 6980 0
vsize: 28084
[startup+940.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6643 0 0 0 93987 23 0 0 25 0 1 0 479679207 28758016 6621 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6621 603 41 0 6980 0
vsize: 28084
[startup+950.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6644 0 0 0 94987 23 0 0 25 0 1 0 479679207 28758016 6622 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6622 603 41 0 6980 0
vsize: 28084
[startup+960.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6646 0 0 0 95988 23 0 0 25 0 1 0 479679207 28758016 6624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6624 603 41 0 6980 0
vsize: 28084
[startup+970.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 96988 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+980.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 97988 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+990.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 98988 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 99988 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 100988 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 101988 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 102989 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 103989 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 104989 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223664 134559769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 105989 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6647 0 0 0 106989 23 0 0 25 0 1 0 479679207 28758016 6625 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7021 6625 603 41 0 6980 0
vsize: 28084
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6659 0 0 0 107990 23 0 0 25 0 1 0 479679207 28954624 6637 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7069 6637 603 41 0 7028 0
vsize: 28276
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6661 0 0 0 108990 24 0 0 25 0 1 0 479679207 28954624 6639 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7069 6639 603 41 0 7028 0
vsize: 28276
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6672 0 0 0 109990 24 0 0 25 0 1 0 479679207 28954624 6650 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7069 6650 603 41 0 7028 0
vsize: 28276
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6682 0 0 0 110990 24 0 0 25 0 1 0 479679207 28954624 6660 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7069 6660 603 41 0 7028 0
vsize: 28276
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6682 0 0 0 111990 24 0 0 25 0 1 0 479679207 28954624 6660 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7117 6666 603 41 0 7076 0
vsize: 28276
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6695 0 0 0 112990 24 0 0 25 0 1 0 479679207 29413376 6673 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6673 603 41 0 7140 0
vsize: 28724
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6707 0 0 0 113990 24 0 0 25 0 1 0 479679207 29413376 6685 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6685 603 41 0 7140 0
vsize: 28724
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6707 0 0 0 114991 24 0 0 25 0 1 0 479679207 29413376 6685 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6685 603 41 0 7140 0
vsize: 28724
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6707 0 0 0 115991 24 0 0 25 0 1 0 479679207 29413376 6685 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6685 603 41 0 7140 0
vsize: 28724
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6719 0 0 0 116991 24 0 0 25 0 1 0 479679207 29413376 6697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6697 603 41 0 7140 0
vsize: 28724
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6720 0 0 0 117991 24 0 0 25 0 1 0 479679207 29413376 6698 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6698 603 41 0 7140 0
vsize: 28724
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6743 0 0 0 118991 24 0 0 25 0 1 0 479679207 29609984 6721 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7229 6721 603 41 0 7188 0
vsize: 28916
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6399
Raw data (stat): 6342 (minisat+) R 6341 3260 3259 0 -1 0 6746 0 0 0 119991 24 0 0 25 0 1 0 479679207 29609984 6724 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7229 6724 603 41 0 7188 0
vsize: 28916
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 6399
Raw data (stat): 6342 (minisat+) Z 6341 3260 3259 0 -1 12 6749 0 0 0 119992 25 0 0 25 0 1 0 479679207 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.03
CPU time (s): 1200.18
CPU user time (s): 1199.92
CPU system time (s): 0.254961
CPU usage (%): 100.012
Max. virtual memory (Kb): 28916
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####