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 5989

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 02:45:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4457 boxname=wulflinc25 idbench=321 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  25457db86ce3cc3b7604dfa37c8096b4  /oldhome/oroussel/tmp/wulflinc25/normalized-frb35-17-3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-frb35-17-3.opb /oldhome/oroussel/tmp/wulflinc25/normalized-frb35-17-3.opb
IDLAUNCH: 4457
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        873232 kB
Buffers:         34956 kB
Cached:          91352 kB
SwapCached:         36 kB
Active:          50584 kB
Inactive:        78592 kB
HighTotal:      131008 kB
HighFree:        35980 kB
LowTotal:       903652 kB
LowFree:        837252 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26516 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:06:02 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4457 7 1200.22 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]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56226   122317 |   18742       0        0     nan |  0.000 % |
c |       100 |   56017   121884 |   20616      93     1165    12.5 |  0.585 % |
c |       250 |   55219   120180 |   22677     215     2505    11.7 |  2.925 % |
c |       475 |   54050   117632 |   24945     366     4294    11.7 |  6.485 % |
c |       813 |   52427   114064 |   27440     604     7515    12.4 | 11.657 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1312 |   49748   108075 |   16582     973    13038    13.4 | 11.657 % |
c |      1412 |   49314   107081 |   18240    1047    14480    13.8 | 21.494 % |
c |      1562 |   48109   104346 |   20064    1117    15274    13.7 | 25.435 % |
c |      1787 |   46873   101501 |   22070    1273    17136    13.5 | 29.543 % |
c |      2124 |   45440    98214 |   24277    1530    19819    13.0 | 34.301 % |
c |      2630 |   43350    93367 |   26705    1845    25665    13.9 | 41.215 % |
c |      3389 |   41978    90084 |   29376    2483    31539    12.7 | 45.869 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3553 |   41830    89810 |   13943    2628    34703    13.2 | 45.869 % |
c |      3653 |   41490    88994 |   15337    2682    35918    13.4 | 47.845 % |
c |      3803 |   41155    88218 |   16871    2808    38474    13.7 | 48.966 % |
c |      4028 |   40908    87625 |   18558    2975    42154    14.2 | 49.830 % |
c |      4365 |   40256    86118 |   20413    3168    49450    15.6 | 52.022 % |
c |      4871 |   39264    83777 |   22455    3528    61471    17.4 | 55.427 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5253 |   38681    82397 |   12893    3832    66544    17.4 | 55.427 % |
c |      5354 |   38557    82103 |   14182    3922    71658    18.3 | 57.906 % |
c |      5504 |   38289    81462 |   15600    4018    73309    18.2 | 58.842 % |
c |      5730 |   38127    81078 |   17160    4185    78516    18.8 | 59.413 % |
c |      6067 |   37939    80622 |   18876    4417    84596    19.2 | 60.102 % |
c |      6574 |   37077    78579 |   20764    4679    91036    19.5 | 63.065 % |
c |      7334 |   36460    77108 |   22840    5284   107904    20.4 | 65.312 % |
c |      8474 |   35325    74406 |   25124    6063   138814    22.9 | 69.098 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9550 |   35051    73788 |   11683    7007   181532    25.9 | 69.098 % |
c |      9650 |   35051    73788 |   12851    7107   185723    26.1 | 70.086 % |
c |      9800 |   35044    73773 |   14136    7237   189597    26.2 | 70.106 % |
c |     10025 |   35044    73773 |   15550    7462   206968    27.7 | 70.106 % |
c |     10362 |   34754    73089 |   17105    7671   217020    28.3 | 71.113 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10418 |   34746    73026 |   11582    7715   217249    28.2 | 71.113 % |
c |     10519 |   34708    72936 |   12740    7766   220611    28.4 | 71.286 % |
c |     10669 |   34561    72582 |   14014    7879   225784    28.7 | 71.809 % |
c |     10895 |   34561    72582 |   15415    8105   234073    28.9 | 71.809 % |
c |     11232 |   34503    72446 |   16957    8415   250564    29.8 | 72.010 % |
c |     11738 |   34040    71355 |   18652    8744   269440    30.8 | 73.746 % |
c |     12497 |   33540    70146 |   20518    9112   292045    32.1 | 75.384 % |
c |     13637 |   33245    69430 |   22570   10095   339815    33.7 | 76.437 % |
c |     15346 |   33103    69093 |   24827   11789   430037    36.5 | 76.935 % |
c |     17908 |   32838    68436 |   27309   14169   571943    40.4 | 77.900 % |
c |     21752 |   32406    67389 |   30040   17744   810159    45.7 | 79.467 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25513 |   32400    67391 |   10800   21435  1132948    52.9 | 79.467 % |
c |     25613 |   32400    67391 |   11880   21535  1137302    52.8 | 79.580 % |
c |     25763 |   32297    67128 |   13068   21449  1138247    53.1 | 79.974 % |
c |     25988 |   32297    67128 |   14374   21674  1153380    53.2 | 79.973 % |
c |     26325 |   32226    66949 |   15812   21871  1164442    53.2 | 80.245 % |
c |     26832 |   32226    66949 |   17393   22378  1189285    53.1 | 80.245 % |
c |     27591 |   32203    66890 |   19132   23072  1220699    52.9 | 80.337 % |
c |     28731 |   32203    66890 |   21046   24212  1292326    53.4 | 80.337 % |
c |     30439 |   32177    66823 |   23150   25888  1432498    55.3 | 80.439 % |
c |     33002 |   32174    66816 |   25465   28443  1544015    54.3 | 80.449 % |
c |     36846 |   32165    66795 |   28012   32086  1770438    55.2 | 80.480 % |
c |     42612 |   32165    66795 |   30813   37852  2233106    59.0 | 80.480 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49852 |   32020    66434 |   10673   44908  2776824    61.8 | 80.480 % |
c |     49952 |   32020    66434 |   11740   16606   965248    58.1 | 81.008 % |
c |     50103 |   32020    66434 |   12914   16757   968861    57.8 | 81.008 % |
c |     50328 |   32020    66434 |   14205   16982   978993    57.6 | 81.008 % |
c |     50665 |   32020    66434 |   15626   17319  1003362    57.9 | 81.008 % |
c |     51172 |   32020    66434 |   17188   17826  1036082    58.1 | 81.008 % |
c |     51931 |   31991    66359 |   18907   18574  1086045    58.5 | 81.121 % |
c |     53070 |   31649    65547 |   20798   19664  1187670    60.4 | 82.297 % |
c |     54779 |   31649    65547 |   22878   21373  1349706    63.2 | 82.297 % |
c |     57343 |   31614    65464 |   25166   23929  1562175    65.3 | 82.420 % |
c |     61188 |   31576    65372 |   27683   27752  1803243    65.0 | 82.553 % |
c |     66954 |   31574    65368 |   30451   33497  2289530    68.4 | 82.558 % |
c |     75604 |   31532    65264 |   33496   42137  3056028    72.5 | 82.716 % |
c |     88578 |   31532    65264 |   36846   21336  1265506    59.3 | 82.716 % |
c |    108040 |   31529    65257 |   40530   40797  2591421    63.5 | 82.727 % |
c |    137232 |   31529    65257 |   44583   29377  1221521    41.6 | 82.727 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    148357 |   31547    65303 |   10515   40502  1622760    40.1 | 82.727 % |
c |    148458 |   31547    65303 |   11566   17946   543672    30.3 | 82.688 % |
c |    148609 |   31547    65303 |   12723   18097   548810    30.3 | 82.688 % |
c |    148834 |   31547    65303 |   13995   18322   556443    30.4 | 82.688 % |
c |    149172 |   31547    65303 |   15395   18660   571214    30.6 | 82.688 % |
c |    149678 |   31547    65303 |   16934   19166   590946    30.8 | 82.688 % |
c |    150437 |   31509    65208 |   18627   19917   627694    31.5 | 82.826 % |
c |    151576 |   31503    65192 |   20490   21053   676051    32.1 | 82.852 % |
c |    153284 |   31462    65089 |   22539   22760   774749    34.0 | 83.010 % |
c |    155846 |   31462    65089 |   24793   25322   914275    36.1 | 83.010 % |
c |    159690 |   31462    65089 |   27273   29166  1077698    37.0 | 83.010 % |
c |    165456 |   31450    65059 |   30000   34929  1306380    37.4 | 83.056 % |
c |    174105 |   31447    65052 |   33000   43576  1753198    40.2 | 83.066 % |
c |    187079 |   31420    64985 |   36300   24815   994131    40.1 | 83.168 % |
c |    206540 |   31420    64985 |   39930   44276  1745057    39.4 | 83.168 % |
c |    235733 |   31410    64963 |   43923   34580  1120114    32.4 | 83.199 % |
c |    279522 |   31398    64933 |   48316   36368  1076415    29.6 | 83.245 % |
c |    345206 |   31387    64906 |   53147   56897  1731001    30.4 | 83.286 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    407607 |   31371    64837 |   10457   69202  2220207    32.1 | 83.286 % |
c |    407708 |   31371    64837 |   11502   21207   509732    24.0 | 83.349 % |
c |    407858 |   31371    64837 |   12652   21357   514760    24.1 | 83.349 % |
c |    408084 |   31371    64837 |   13918   21583   523197    24.2 | 83.349 % |
c |    408421 |   31371    64837 |   15310   21920   537769    24.5 | 83.349 % |
c |    408927 |   31371    64837 |   16841   22426   560502    25.0 | 83.349 % |
c |    409687 |   31341    64767 |   18525   23178   592062    25.5 | 83.446 % |
c |    410826 |   31341    64767 |   20377   24317   636022    26.2 | 83.446 % |
c |    412534 |   31341    64767 |   22415   26025   707984    27.2 | 83.446 % |
c |    415097 |   31341    64767 |   24657   28588   779097    27.3 | 83.446 % |
c |    418942 |   31341    64767 |   27122   32433   897343    27.7 | 83.446 % |
c |    424708 |   31341    64767 |   29835   38199  1050979    27.5 | 83.446 % |
c |    433357 |   31341    64767 |   32818   46848  1391591    29.7 | 83.446 % |
c |    446331 |   31332    64746 |   36100   27082   843797    31.2 | 83.476 % |
c |    465792 |   31329    64739 |   39710   46542  1633843    35.1 | 83.487 % |
c |    494985 |   31256    64553 |   43681   39503  1039816    26.3 | 83.767 % |
c |    538775 |   31101    64220 |   48049   32061   824480    25.7 | 83.982 % |
c |    604460 |   30912    63770 |   52854   25803   577004    22.4 | 84.630 % |
#### 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.91 0.90 2/54 1313
Raw data (stat): 1313 (runsolver) R 1311 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481107367 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.87 0.91 0.90 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 2266 0 0 0 991 7 0 0 25 0 1 0 481107367 11571200 2237 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2825 2237 603 41 0 2784 0
vsize: 11300
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.91 0.90 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 2357 0 0 0 1990 8 0 0 25 0 1 0 481107367 11927552 2328 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2328 603 41 0 2871 0
vsize: 11648
[startup+30.0023 s]
Raw data (loadavg): 0.90 0.91 0.90 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 2796 0 0 0 2989 10 0 0 25 0 1 0 481107367 13664256 2767 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3336 2767 603 41 0 3295 0
vsize: 13344
[startup+40.0029 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 3401 0 0 0 3985 13 0 0 25 0 1 0 481107367 16171008 3372 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3948 3372 603 41 0 3907 0
vsize: 15792
[startup+50.0035 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 3893 0 0 0 4983 15 0 0 25 0 1 0 481107367 18173952 3864 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4437 3864 603 41 0 4396 0
vsize: 17748
[startup+60.0037 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 4258 0 0 0 5982 16 0 0 25 0 1 0 481107367 19648512 4229 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4797 4229 603 41 0 4756 0
vsize: 19188
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 4688 0 0 0 6980 18 0 0 25 0 1 0 481107367 21499904 4659 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5249 4659 603 41 0 5208 0
vsize: 20996
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.92 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5055 0 0 0 7979 20 0 0 25 0 1 0 481107367 23097344 5026 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5639 5026 603 41 0 5598 0
vsize: 22556
[startup+90.0049 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 8977 21 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6005 5371 603 41 0 5964 0
vsize: 24020
[startup+100.004 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 9977 21 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6005 5371 603 41 0 5964 0
vsize: 24020
[startup+110.005 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 10977 22 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6005 5371 603 41 0 5964 0
vsize: 24020
[startup+120.004 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 11976 22 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6005 5371 603 41 0 5964 0
vsize: 24020
[startup+130.005 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5476 0 0 0 12976 23 0 0 25 0 1 0 481107367 24866816 5447 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6071 5447 603 41 0 6030 0
vsize: 24284
[startup+140.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5869 0 0 0 13974 25 0 0 25 0 1 0 481107367 26468352 5840 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6462 5840 603 41 0 6421 0
vsize: 25848
[startup+150.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6191 0 0 0 14973 26 0 0 25 0 1 0 481107367 27787264 6162 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6784 6162 603 41 0 6743 0
vsize: 27136
[startup+160.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 15971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223516 1075350660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7043 6414 603 41 0 7002 0
vsize: 28172
[startup+170.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 16971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7043 6414 603 41 0 7002 0
vsize: 28172
[startup+180.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 17971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6414 603 41 0 7002 0
vsize: 28172
[startup+190.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 18971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6414 603 41 0 7002 0
vsize: 28172
[startup+200.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 19971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6414 603 41 0 7002 0
vsize: 28172
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 20972 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6414 603 41 0 7002 0
vsize: 28172
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 21972 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6414 603 41 0 7002 0
vsize: 28172
[startup+230.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6447 0 0 0 22972 28 0 0 25 0 1 0 481107367 28848128 6418 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6418 603 41 0 7002 0
vsize: 28172
[startup+240.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6450 0 0 0 23972 28 0 0 25 0 1 0 481107367 28848128 6421 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6421 603 41 0 7002 0
vsize: 28172
[startup+250.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 24972 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+260.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 25973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+270.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 26973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+280.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 27973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+290.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 28973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+300.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 29973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+310.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 30973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+320.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 31974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+330.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 32974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+340.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 33974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+350.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 34974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+360.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 35975 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+370.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 36975 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+380.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 37975 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6430 603 41 0 7002 0
vsize: 28172
[startup+390.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 38975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+400.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 39975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 40975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 41975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 42976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 43976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223744 134559599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 44976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 45976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 46976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 47977 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 48977 29 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6433 603 41 0 7002 0
vsize: 28172
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6463 0 0 0 49977 29 0 0 25 0 1 0 481107367 28848128 6434 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6434 603 41 0 7002 0
vsize: 28172
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 50977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 51977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 52977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 53977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 54978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 55978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 56978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 57978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6436 603 41 0 7002 0
vsize: 28172
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6466 0 0 0 58979 29 0 0 25 0 1 0 481107367 28848128 6437 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7043 6437 603 41 0 7002 0
vsize: 28172
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 59979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 60979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 61979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 62979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223744 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 63979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 64980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 65980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 66980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 67980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 68980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6440 603 41 0 7066 0
vsize: 28428
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6470 0 0 0 69980 29 0 0 25 0 1 0 481107367 29110272 6441 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6441 603 41 0 7066 0
vsize: 28428
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6473 0 0 0 70980 29 0 0 25 0 1 0 481107367 29110272 6444 4294967295 134512640 134672761 3221224560 3221223656 1075347344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6444 603 41 0 7066 0
vsize: 28428
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 71981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 72981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 73981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 74981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 75981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 76981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 77982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 78982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 79982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 80982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 81982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223712 134565212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 82981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1313
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 83981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+850.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 1361
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 84981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+860.031 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1367
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 85984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+870.031 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1367
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 86984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+880.031 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1367
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 87984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+890.032 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1367
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 88984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+900.031 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1367
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 89985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+910.031 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1367
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 90985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223744 134559514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+920.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 91985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+930.031 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 92985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+940.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 93985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+950.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 94985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+960.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 95985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+970.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 96986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+980.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 97986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+990.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 98986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 99986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 100986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 101987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 102987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 103987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 104987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 105987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 106988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 107988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 108988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 109988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 110988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 111989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 112989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 113989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 114989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 115989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 116990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 117990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1369
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 118990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1371
Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 119990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6445 603 41 0 7066 0
vsize: 28428
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1371
Raw data (stat): 1313 (minisat+) Z 1311 28099 28098 0 -1 12 6477 0 0 0 119990 31 0 0 25 0 1 0 481107367 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.05
CPU time (s): 1200.22
CPU user time (s): 1199.91
CPU system time (s): 0.310952
CPU usage (%): 100.014
Max. virtual memory (Kb): 28428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####