PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cm42a.opb
MD5SUM	62b75258091a8b1382fa8b1c633d9511
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	694
Optimality of the best value was proved	NO
Number of terms in the objective function	99
Biggest coefficient in the objective function	60
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	4087
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	60
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	4087
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.168973
Number of variables	99
Total number of constraints	185
Number of constraints which are clauses	185
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	20
Trace number 5002

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 21:12:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2264 boxname=wulflinc20 idbench=252 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  62b75258091a8b1382fa8b1c633d9511  /oldhome/oroussel/tmp/wulflinc20/normalized-cm42a.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc20/normalized-cm42a.opb
IDLAUNCH: 2264
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        895528 kB
Buffers:         33516 kB
Cached:          70336 kB
SwapCached:       2636 kB
Active:          44612 kB
Inactive:        64712 kB
HighTotal:      131008 kB
HighFree:        56924 kB
LowTotal:       903652 kB
LowFree:        838604 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24224 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:32:26 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 2264 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 185 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 |     185      626 |      61       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 939[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 8480     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21020    49263 |    7006       0        0     nan |  0.000 % |
c |       100 |   20519    48138 |    7706      89     1028    11.6 |  1.713 % |
c |       250 |   20519    48138 |    8477     239     3004    12.6 |  1.713 % |
c |       475 |   20519    48138 |    9324     464     6184    13.3 |  1.713 % |
c |       812 |   20519    48138 |   10257     801    13852    17.3 |  1.713 % |
c |      1318 |   20519    48138 |   11283    1307    26131    20.0 |  1.713 % |
c |      2077 |   20519    48138 |   12411    2066    36951    17.9 |  1.713 % |
c |      3218 |   20519    48138 |   13652    3207    50232    15.7 |  1.713 % |
c ==============================================================================
c [1mFound solution: 930[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6779     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4515 |   36935    86465 |   12311    4239   125935    29.7 |  1.713 % |
c |      4615 |   36935    86465 |   13542    4339   127931    29.5 |  1.049 % |
c ==============================================================================
c [1mFound solution: 871[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4625 |   37031    86764 |   12343    4349   128034    29.4 |  1.049 % |
c ==============================================================================
c [1mFound solution: 868[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4628 |   37041    86807 |   12347    4352   128611    29.6 |  1.049 % |
c ==============================================================================
c [1mFound solution: 848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4714 |   37044    86814 |   12348    4438   131852    29.7 |  1.049 % |
c |      4815 |   37044    86814 |   13582    4539   137459    30.3 |  1.066 % |
c |      4965 |   37044    86814 |   14941    4689   139947    29.8 |  1.066 % |
c ==============================================================================
c [1mFound solution: 843[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4995 |   37052    86848 |   12350    4719   141269    29.9 |  1.066 % |
c |      5095 |   37052    86848 |   13585    4819   146504    30.4 |  1.073 % |
c |      5245 |   37052    86848 |   14943    4969   148441    29.9 |  1.073 % |
c ==============================================================================
c [1mFound solution: 760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5423 |   37074    86904 |   12358    5147   151537    29.4 |  1.073 % |
c |      5525 |   36992    86727 |   13593    5248   152666    29.1 |  1.269 % |
c |      5677 |   36992    86727 |   14953    5400   154353    28.6 |  1.269 % |
c |      5902 |   36845    86396 |   16448    5570   159179    28.6 |  1.560 % |
c |      6239 |   36845    86396 |   18093    5907   171397    29.0 |  1.560 % |
c |      6747 |   36845    86396 |   19902    6415   186197    29.0 |  1.560 % |
c ==============================================================================
c [1mFound solution: 750[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6801 |   36853    86417 |   12284    6469   186718    28.9 |  1.560 % |
c |      6903 |   36853    86417 |   13512    6571   189822    28.9 |  1.567 % |
c |      7053 |   36853    86417 |   14863    6721   194339    28.9 |  1.567 % |
c ==============================================================================
c [1mFound solution: 727[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7081 |   36859    86432 |   12286    6749   194737    28.9 |  1.567 % |
c |      7185 |   36859    86432 |   13514    6853   196190    28.6 |  1.574 % |
c ==============================================================================
c [1mFound solution: 725[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7267 |   36863    86444 |   12287    6935   197305    28.5 |  1.574 % |
c |      7368 |   36863    86444 |   13515    7036   199384    28.3 |  1.581 % |
c |      7519 |   36863    86444 |   14867    7187   204956    28.5 |  1.581 % |
c |      7745 |   36863    86444 |   16353    7413   209249    28.2 |  1.581 % |
c |      8082 |   36863    86444 |   17989    7750   217404    28.1 |  1.581 % |
c |      8588 |   36863    86444 |   19788    8256   232248    28.1 |  1.581 % |
c |      9350 |   36863    86444 |   21767    9018   254804    28.3 |  1.581 % |
c |     10490 |   36863    86444 |   23943   10158   295961    29.1 |  1.581 % |
c |     12198 |   36863    86444 |   26338   11866   348800    29.4 |  1.581 % |
c |     14760 |   36863    86444 |   28972   14428   430582    29.8 |  1.581 % |
c |     18605 |   36863    86444 |   31869   18273   554507    30.3 |  1.581 % |
c |     24371 |   36863    86444 |   35056   24039   742719    30.9 |  1.581 % |
c ==============================================================================
c [1mFound solution: 721[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32325 |   36870    86462 |   12290   31993  1001266    31.3 |  1.581 % |
c |     32425 |   36870    86462 |   13519    7193   181885    25.3 |  1.587 % |
c |     32575 |   36870    86462 |   14870    7343   187243    25.5 |  1.587 % |
c |     32800 |   36870    86462 |   16357    7568   193785    25.6 |  1.587 % |
c |     33137 |   36870    86462 |   17993    7905   204955    25.9 |  1.587 % |
c |     33643 |   36870    86462 |   19793    8411   222819    26.5 |  1.587 % |
c |     34402 |   36870    86462 |   21772    9170   247919    27.0 |  1.587 % |
c |     35541 |   36870    86462 |   23949   10309   281263    27.3 |  1.587 % |
c |     37251 |   36673    86016 |   26344   11354   308391    27.2 |  2.010 % |
c |     39814 |   36673    86016 |   28979   13917   414447    29.8 |  2.010 % |
c |     43658 |   36673    86016 |   31877   17761   606961    34.2 |  2.010 % |
c |     49424 |   36673    86016 |   35064   23527   847619    36.0 |  2.010 % |
c ==============================================================================
c [1mFound solution: 696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54796 |   36681    86035 |   12227   28899  1065079    36.9 |  2.010 % |
c |     54897 |   36681    86035 |   13449    7326   204774    28.0 |  2.016 % |
c |     55050 |   36681    86035 |   14794    7479   209137    28.0 |  2.016 % |
c |     55279 |   36681    86035 |   16274    7708   217316    28.2 |  2.016 % |
c |     55616 |   36681    86035 |   17901    8045   227927    28.3 |  2.016 % |
c |     56123 |   36681    86035 |   19691    8552   242511    28.4 |  2.016 % |
c |     56882 |   36681    86035 |   21660    9311   267475    28.7 |  2.016 % |
c |     58021 |   36681    86035 |   23826   10450   303809    29.1 |  2.016 % |
c |     59730 |   36681    86035 |   26209   12159   371468    30.6 |  2.016 % |
c |     62293 |   36681    86035 |   28830   14722   458406    31.1 |  2.016 % |
c |     66138 |   36596    85839 |   31713   18566   616592    33.2 |  2.220 % |
c |     71905 |   36596    85839 |   34885   24333   831643    34.2 |  2.220 % |
c |     80554 |   36596    85839 |   38373   32982  1166482    35.4 |  2.220 % |
c |     93528 |   36596    85839 |   42210   22811   854263    37.4 |  2.220 % |
c |    112990 |   36596    85839 |   46432   42273  1684549    39.8 |  2.220 % |
c |    142185 |   36596    85839 |   51075   42418  1729647    40.8 |  2.220 % |
c |    185974 |   36596    85839 |   56182   51791  2490585    48.1 |  2.220 % |
c ==============================================================================
c [1mFound solution: 694[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225026 |   36603    85855 |   12201   53073  2198951    41.4 |  2.220 % |
c |    225126 |   36603    85855 |   13421    9803   290594    29.6 |  2.227 % |
c |    225276 |   36603    85855 |   14763    9953   297699    29.9 |  2.227 % |
c |    225504 |   36603    85855 |   16239   10181   308736    30.3 |  2.227 % |
c |    225843 |   36603    85855 |   17863   10520   324699    30.9 |  2.227 % |
c |    226349 |   36603    85855 |   19649   11026   350759    31.8 |  2.227 % |
c |    227109 |   36603    85855 |   21614   11786   380901    32.3 |  2.227 % |
c |    228248 |   36603    85855 |   23776   12925   435314    33.7 |  2.227 % |
c |    229958 |   36603    85855 |   26153   14635   527195    36.0 |  2.227 % |
c |    232522 |   36603    85855 |   28769   17199   660247    38.4 |  2.227 % |
c |    236366 |   36603    85855 |   31646   21043   843540    40.1 |  2.227 % |
c |    242132 |   36603    85855 |   34810   26809  1110921    41.4 |  2.227 % |
c |    250782 |   36603    85855 |   38291   35459  1600907    45.1 |  2.227 % |
c |    263756 |   36603    85855 |   42121   26184  1173309    44.8 |  2.227 % |
c |    283217 |   36603    85855 |   46333   18155   718766    39.6 |  2.227 % |
#### 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.85 0.95 0.90 2/54 30786
Raw data (stat): 30786 (runsolver) R 30785 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479095066 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 1641 0 0 0 994 3 0 0 25 0 1 0 479095066 8589312 1618 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2097 1618 603 41 0 2056 0
vsize: 8388
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 1796 0 0 0 1993 4 0 0 25 0 1 0 479095066 9199616 1773 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2246 1773 603 41 0 2205 0
vsize: 8984
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 1940 0 0 0 2993 4 0 0 25 0 1 0 479095066 9728000 1917 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2375 1917 603 41 0 2334 0
vsize: 9500
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2092 0 0 0 3992 5 0 0 25 0 1 0 479095066 10506240 2069 4294967295 134512640 134672761 3221224640 3221223744 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2565 2069 603 41 0 2524 0
vsize: 10260
[startup+50.0009 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2205 0 0 0 4992 5 0 0 25 0 1 0 479095066 10903552 2182 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2662 2182 603 41 0 2621 0
vsize: 10648
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2318 0 0 0 5992 6 0 0 25 0 1 0 479095066 11321344 2295 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2764 2295 603 41 0 2723 0
vsize: 11056
[startup+70.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2452 0 0 0 6990 7 0 0 25 0 1 0 479095066 11853824 2429 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2894 2429 603 41 0 2853 0
vsize: 11576
[startup+80.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2578 0 0 0 7990 8 0 0 25 0 1 0 479095066 12402688 2555 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3028 2555 603 41 0 2987 0
vsize: 12112
[startup+90.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2706 0 0 0 8989 8 0 0 25 0 1 0 479095066 12935168 2683 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2683 603 41 0 3117 0
vsize: 12632
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2763 0 0 0 9989 9 0 0 25 0 1 0 479095066 13160448 2740 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3213 2740 603 41 0 3172 0
vsize: 12852
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2771 0 0 0 10989 9 0 0 25 0 1 0 479095066 13160448 2748 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3213 2748 603 41 0 3172 0
vsize: 12852
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2781 0 0 0 11989 9 0 0 25 0 1 0 479095066 13307904 2758 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3249 2758 603 41 0 3208 0
vsize: 12996
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2785 0 0 0 12989 9 0 0 25 0 1 0 479095066 13307904 2762 4294967295 134512640 134672761 3221224640 3221223700 1075346562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3249 2762 603 41 0 3208 0
vsize: 12996
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2793 0 0 0 13989 9 0 0 25 0 1 0 479095066 13307904 2770 4294967295 134512640 134672761 3221224640 3221223744 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3249 2770 603 41 0 3208 0
vsize: 12996
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2806 0 0 0 14990 9 0 0 25 0 1 0 479095066 13307904 2783 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3249 2783 603 41 0 3208 0
vsize: 12996
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2816 0 0 0 15990 9 0 0 25 0 1 0 479095066 13471744 2793 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3289 2793 603 41 0 3248 0
vsize: 13156
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2864 0 0 0 16990 9 0 0 25 0 1 0 479095066 13602816 2841 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3321 2841 603 41 0 3280 0
vsize: 13284
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2940 0 0 0 17990 9 0 0 25 0 1 0 479095066 13877248 2917 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3388 2917 603 41 0 3347 0
vsize: 13552
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2940 0 0 0 18990 9 0 0 25 0 1 0 479095066 13877248 2917 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3388 2917 603 41 0 3347 0
vsize: 13552
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2950 0 0 0 19990 10 0 0 25 0 1 0 479095066 14041088 2927 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2927 603 41 0 3387 0
vsize: 13712
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2963 0 0 0 20990 10 0 0 25 0 1 0 479095066 14041088 2940 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2940 603 41 0 3387 0
vsize: 13712
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2967 0 0 0 21990 10 0 0 25 0 1 0 479095066 14041088 2944 4294967295 134512640 134672761 3221224640 3221223776 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2944 603 41 0 3387 0
vsize: 13712
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 2986 0 0 0 22990 10 0 0 25 0 1 0 479095066 14237696 2963 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3476 2963 603 41 0 3435 0
vsize: 13904
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3000 0 0 0 23991 10 0 0 25 0 1 0 479095066 14237696 2977 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3476 2977 603 41 0 3435 0
vsize: 13904
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3000 0 0 0 24991 10 0 0 25 0 1 0 479095066 14237696 2977 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3476 2977 603 41 0 3435 0
vsize: 13904
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3025 0 0 0 25991 10 0 0 25 0 1 0 479095066 14368768 3002 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3508 3002 603 41 0 3467 0
vsize: 14032
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3122 0 0 0 26990 11 0 0 25 0 1 0 479095066 14770176 3099 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3606 3099 603 41 0 3565 0
vsize: 14424
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3239 0 0 0 27990 12 0 0 25 0 1 0 479095066 15474688 3216 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3778 3216 603 41 0 3737 0
vsize: 15112
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3354 0 0 0 28989 12 0 0 25 0 1 0 479095066 15876096 3331 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3876 3331 603 41 0 3835 0
vsize: 15504
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3470 0 0 0 29989 12 0 0 25 0 1 0 479095066 16355328 3447 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3993 3447 603 41 0 3952 0
vsize: 15972
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3470 0 0 0 30989 12 0 0 25 0 1 0 479095066 16355328 3447 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3993 3447 603 41 0 3952 0
vsize: 15972
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3473 0 0 0 31989 12 0 0 25 0 1 0 479095066 16355328 3450 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3993 3450 603 41 0 3952 0
vsize: 15972
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3474 0 0 0 32990 12 0 0 25 0 1 0 479095066 16355328 3451 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3993 3451 603 41 0 3952 0
vsize: 15972
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3483 0 0 0 33990 12 0 0 25 0 1 0 479095066 16539648 3460 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4038 3460 603 41 0 3997 0
vsize: 16152
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3484 0 0 0 34989 13 0 0 25 0 1 0 479095066 16539648 3461 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4038 3461 603 41 0 3997 0
vsize: 16152
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3494 0 0 0 35989 13 0 0 25 0 1 0 479095066 16539648 3471 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4038 3471 603 41 0 3997 0
vsize: 16152
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3494 0 0 0 36989 13 0 0 25 0 1 0 479095066 16539648 3471 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4038 3471 603 41 0 3997 0
vsize: 16152
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3554 0 0 0 37989 13 0 0 25 0 1 0 479095066 16826368 3531 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4108 3531 603 41 0 4067 0
vsize: 16432
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3658 0 0 0 38989 13 0 0 25 0 1 0 479095066 17227776 3635 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4206 3635 603 41 0 4165 0
vsize: 16824
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3748 0 0 0 39989 14 0 0 25 0 1 0 479095066 17645568 3725 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4308 3725 603 41 0 4267 0
vsize: 17232
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3833 0 0 0 40989 14 0 0 25 0 1 0 479095066 17907712 3810 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3810 603 41 0 4331 0
vsize: 17488
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 3935 0 0 0 41989 14 0 0 25 0 1 0 479095066 18345984 3912 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4479 3912 603 41 0 4438 0
vsize: 17916
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4044 0 0 0 42989 15 0 0 25 0 1 0 479095066 18788352 4021 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4021 603 41 0 4546 0
vsize: 18348
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4116 0 0 0 43988 15 0 0 25 0 1 0 479095066 19050496 4093 4294967295 134512640 134672761 3221224640 3221223744 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4093 603 41 0 4610 0
vsize: 18604
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4116 0 0 0 44988 15 0 0 25 0 1 0 479095066 19050496 4093 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4093 603 41 0 4610 0
vsize: 18604
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4116 0 0 0 45989 15 0 0 25 0 1 0 479095066 19050496 4093 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4093 603 41 0 4610 0
vsize: 18604
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4116 0 0 0 46989 15 0 0 25 0 1 0 479095066 19050496 4093 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4093 603 41 0 4610 0
vsize: 18604
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4116 0 0 0 47989 15 0 0 25 0 1 0 479095066 19050496 4093 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4093 603 41 0 4610 0
vsize: 18604
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4116 0 0 0 48989 15 0 0 25 0 1 0 479095066 19050496 4093 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4093 603 41 0 4610 0
vsize: 18604
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4131 0 0 0 49989 16 0 0 25 0 1 0 479095066 19193856 4108 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4108 603 41 0 4645 0
vsize: 18744
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4133 0 0 0 50989 16 0 0 25 0 1 0 479095066 19193856 4110 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4110 603 41 0 4645 0
vsize: 18744
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4134 0 0 0 51989 16 0 0 25 0 1 0 479095066 19193856 4111 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4111 603 41 0 4645 0
vsize: 18744
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4134 0 0 0 52990 16 0 0 25 0 1 0 479095066 19193856 4111 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4111 603 41 0 4645 0
vsize: 18744
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4166 0 0 0 53989 16 0 0 25 0 1 0 479095066 19390464 4143 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4734 4143 603 41 0 4693 0
vsize: 18936
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4188 0 0 0 54989 16 0 0 25 0 1 0 479095066 19390464 4165 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4734 4165 603 41 0 4693 0
vsize: 18936
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4188 0 0 0 55989 16 0 0 25 0 1 0 479095066 19390464 4165 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4734 4165 603 41 0 4693 0
vsize: 18936
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4258 0 0 0 56989 17 0 0 25 0 1 0 479095066 19787776 4235 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4831 4235 603 41 0 4790 0
vsize: 19324
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4376 0 0 0 57989 17 0 0 25 0 1 0 479095066 20189184 4353 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4353 603 41 0 4888 0
vsize: 19716
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4497 0 0 0 58989 17 0 0 25 0 1 0 479095066 20713472 4474 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5057 4474 603 41 0 5016 0
vsize: 20228
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4522 0 0 0 59989 17 0 0 25 0 1 0 479095066 20844544 4499 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4499 603 41 0 5048 0
vsize: 20356
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4522 0 0 0 60989 17 0 0 25 0 1 0 479095066 20844544 4499 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4499 603 41 0 5048 0
vsize: 20356
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4522 0 0 0 61989 17 0 0 25 0 1 0 479095066 20844544 4499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4499 603 41 0 5048 0
vsize: 20356
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4525 0 0 0 62990 17 0 0 25 0 1 0 479095066 20844544 4502 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4502 603 41 0 5048 0
vsize: 20356
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4528 0 0 0 63990 17 0 0 25 0 1 0 479095066 20844544 4505 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4505 603 41 0 5048 0
vsize: 20356
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4528 0 0 0 64990 17 0 0 25 0 1 0 479095066 20844544 4505 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4505 603 41 0 5048 0
vsize: 20356
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4528 0 0 0 65990 17 0 0 25 0 1 0 479095066 20844544 4505 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4505 603 41 0 5048 0
vsize: 20356
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4533 0 0 0 66990 17 0 0 25 0 1 0 479095066 20844544 4510 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4510 603 41 0 5048 0
vsize: 20356
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4547 0 0 0 67991 17 0 0 25 0 1 0 479095066 20996096 4524 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5126 4524 603 41 0 5085 0
vsize: 20504
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4561 0 0 0 68992 17 0 0 25 0 1 0 479095066 20996096 4538 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5126 4538 603 41 0 5085 0
vsize: 20504
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4562 0 0 0 69992 17 0 0 25 0 1 0 479095066 20996096 4539 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5126 4539 603 41 0 5085 0
vsize: 20504
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4586 0 0 0 70992 18 0 0 25 0 1 0 479095066 21143552 4563 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5162 4563 603 41 0 5121 0
vsize: 20648
[startup+720.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4590 0 0 0 71993 18 0 0 25 0 1 0 479095066 21143552 4567 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5162 4567 603 41 0 5121 0
vsize: 20648
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4726 0 0 0 72992 18 0 0 25 0 1 0 479095066 21712896 4703 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5301 4703 603 41 0 5260 0
vsize: 21204
[startup+740.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4857 0 0 0 73992 19 0 0 25 0 1 0 479095066 22245376 4834 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4834 603 41 0 5390 0
vsize: 21724
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 4954 0 0 0 74991 19 0 0 25 0 1 0 479095066 22646784 4931 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5529 4931 603 41 0 5488 0
vsize: 22116
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5021 0 0 0 75991 19 0 0 25 0 1 0 479095066 22929408 4998 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5598 4998 603 41 0 5557 0
vsize: 22392
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5107 0 0 0 76991 20 0 0 25 0 1 0 479095066 23326720 5084 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5695 5084 603 41 0 5654 0
vsize: 22780
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5166 0 0 0 77991 20 0 0 25 0 1 0 479095066 23457792 5143 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5727 5143 603 41 0 5686 0
vsize: 22908
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5168 0 0 0 78991 20 0 0 25 0 1 0 479095066 23457792 5145 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5727 5145 603 41 0 5686 0
vsize: 22908
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5177 0 0 0 79991 20 0 0 25 0 1 0 479095066 23650304 5154 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5154 603 41 0 5733 0
vsize: 23096
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5188 0 0 0 80991 20 0 0 25 0 1 0 479095066 23650304 5165 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5165 603 41 0 5733 0
vsize: 23096
[startup+820.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5190 0 0 0 81992 20 0 0 25 0 1 0 479095066 23650304 5167 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5167 603 41 0 5733 0
vsize: 23096
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5190 0 0 0 82992 20 0 0 25 0 1 0 479095066 23650304 5167 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5167 603 41 0 5733 0
vsize: 23096
[startup+840.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5191 0 0 0 83992 20 0 0 25 0 1 0 479095066 23650304 5168 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5168 603 41 0 5733 0
vsize: 23096
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5191 0 0 0 84992 20 0 0 25 0 1 0 479095066 23650304 5168 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5168 603 41 0 5733 0
vsize: 23096
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5191 0 0 0 85992 20 0 0 25 0 1 0 479095066 23650304 5168 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5168 603 41 0 5733 0
vsize: 23096
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5191 0 0 0 86993 20 0 0 25 0 1 0 479095066 23650304 5168 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5168 603 41 0 5733 0
vsize: 23096
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5191 0 0 0 87993 20 0 0 25 0 1 0 479095066 23650304 5168 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5774 5168 603 41 0 5733 0
vsize: 23096
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5209 0 0 0 88993 20 0 0 25 0 1 0 479095066 23846912 5186 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5186 603 41 0 5781 0
vsize: 23288
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 89993 20 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 90993 20 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 91993 20 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 92992 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+940.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 93993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 94993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223744 134555098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 95993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 96993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 97993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 98993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 99993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 100993 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 101994 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223824 134558859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 102994 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 103994 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 104994 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 105994 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 106994 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 107995 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 108995 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 109995 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 110995 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223824 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 111995 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 112996 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223840 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 113996 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 114996 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 115996 21 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5210 0 0 0 116996 22 0 0 25 0 1 0 479095066 23846912 5187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5187 603 41 0 5781 0
vsize: 23288
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5211 0 0 0 117996 22 0 0 25 0 1 0 479095066 23846912 5188 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5188 603 41 0 5781 0
vsize: 23288
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5211 0 0 0 118997 22 0 0 25 0 1 0 479095066 23846912 5188 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5188 603 41 0 5781 0
vsize: 23288
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30786
Raw data (stat): 30786 (minisat+) R 30785 27565 27564 0 -1 0 5211 0 0 0 119997 22 0 0 25 0 1 0 479095066 23846912 5188 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5188 603 41 0 5781 0
vsize: 23288
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30786
Raw data (stat): 30786 (minisat+) Z 30785 27565 27564 0 -1 12 5214 0 0 0 119997 23 0 0 25 0 1 0 479095066 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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