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/primes-dimacs-cnf/normalized-ii8a3.opb
MD5SUM	a430664a9b4f203a5896b33ca2b0e0e5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	528
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	528
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	528
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02384
Number of variables	528
Total number of constraints	1816
Number of constraints which are clauses	1816
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	8
Trace number 4736

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 20:07:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3549 boxname=wulflinc17 idbench=165 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a430664a9b4f203a5896b33ca2b0e0e5  /oldhome/oroussel/tmp/wulflinc17/normalized-ii8a3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc17/normalized-ii8a3.opb /oldhome/oroussel/tmp/wulflinc17/normalized-ii8a3.opb
IDLAUNCH: 3549
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        850300 kB
Buffers:         34204 kB
Cached:         115400 kB
SwapCached:       2376 kB
Active:          50996 kB
Inactive:       103916 kB
HighTotal:      131008 kB
HighFree:        12096 kB
LowTotal:       903652 kB
LowFree:        838204 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23740 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:27:22 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 3549 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1816 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 |    1816     4536 |     605       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1052   maxlim: 296   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |    9113    30567 |    3037       3       16     5.3 |  0.000 % |
c |       103 |    9113    30567 |    3340     103      653     6.3 |  0.253 % |
c |       253 |    9113    30567 |    3674     253     1660     6.6 |  0.253 % |
c |       478 |    9113    30567 |    4042     478     3621     7.6 |  0.253 % |
c |       815 |    9113    30567 |    4446     815    10257    12.6 |  0.253 % |
c |      1321 |    9113    30567 |    4891    1321    20707    15.7 |  0.253 % |
c |      2083 |    9113    30567 |    5380    2083    37828    18.2 |  0.253 % |
c |      3223 |    9113    30567 |    5918    3223    90386    28.0 |  0.253 % |
c |      4931 |    9113    30567 |    6510    4931   171398    34.8 |  0.253 % |
c |      7493 |    9113    30567 |    7161    7493   329551    44.0 |  0.253 % |
c ==============================================================================
c [1mFound solution: 221[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 307   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8548 |    9119    30599 |    3039    4802   191571    39.9 |  0.253 % |
c |      8649 |    9119    30599 |    3342    2502    54510    21.8 |  0.378 % |
c |      8799 |    9119    30599 |    3677    2652    57317    21.6 |  0.378 % |
c |      9026 |    9119    30599 |    4044    2879    62334    21.7 |  0.378 % |
c |      9363 |    9119    30599 |    4449    3216    68355    21.3 |  0.378 % |
c |      9869 |    9119    30599 |    4894    3722    97942    26.3 |  0.378 % |
c |     10628 |    9119    30599 |    5383    4481   114195    25.5 |  0.378 % |
c |     11768 |    9119    30599 |    5922    5621   147648    26.3 |  0.378 % |
c |     13478 |    9119    30599 |    6514    4218    91517    21.7 |  0.378 % |
c |     16045 |    9119    30599 |    7165    3419    86043    25.2 |  0.378 % |
c |     19892 |    9119    30599 |    7882    7266   339680    46.7 |  0.378 % |
c |     25658 |    9119    30599 |    8670    4788   163922    34.2 |  0.378 % |
c |     34309 |    9119    30599 |    9537    8681   634352    73.1 |  0.380 % |
c |     47285 |    9119    30599 |   10491    6075   380667    62.7 |  0.378 % |
c |     66747 |    9119    30599 |   11540    8339   805639    96.6 |  0.378 % |
c |     95939 |    9119    30599 |   12694   12499  1317776   105.4 |  0.378 % |
c |    139729 |    9119    30599 |   13964    8137   659977    81.1 |  0.378 % |
c |    205415 |    9119    30599 |   15360   13944  1167963    83.8 |  0.378 % |
c |    303941 |    9119    30599 |   16896   13860  1423615   102.7 |  0.378 % |
c ==============================================================================
c [1mFound solution: 220[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 308   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    305964 |    9122    30616 |    3040   15883  1513954    95.3 |  0.378 % |
c |    306064 |    9122    30616 |    3344    2086    57067    27.4 |  0.442 % |
c |    306214 |    9122    30616 |    3678    2236    58873    26.3 |  0.441 % |
c |    306439 |    9122    30616 |    4046    2461    72758    29.6 |  0.441 % |
c |    306776 |    9122    30616 |    4450    2798    77294    27.6 |  0.441 % |
c |    307282 |    9122    30616 |    4895    3304    94588    28.6 |  0.441 % |
c |    308043 |    9122    30616 |    5385    4065   111431    27.4 |  0.441 % |
c |    309183 |    9122    30616 |    5924    5205   189505    36.4 |  0.441 % |
c |    310891 |    9122    30616 |    6516    6913   273916    39.6 |  0.441 % |
c |    313453 |    9122    30616 |    7168    6019   253038    42.0 |  0.441 % |
c |    317297 |    9122    30616 |    7884    5714   250988    43.9 |  0.441 % |
c |    323065 |    9122    30616 |    8673    7054   512807    72.7 |  0.441 % |
c |    331716 |    9122    30616 |    9540    6110   465028    76.1 |  0.441 % |
c |    344690 |    9122    30616 |   10494    8521   714648    83.9 |  0.441 % |
c ==============================================================================
c [1mFound solution: 219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 309   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    345870 |    9123    30626 |    3041    9701   766771    79.0 |  0.441 % |
c |    345970 |    9123    30626 |    3345    2526    68431    27.1 |  0.504 % |
c |    346120 |    9123    30626 |    3679    2676    73443    27.4 |  0.504 % |
c |    346346 |    9123    30626 |    4047    2902    78592    27.1 |  0.504 % |
c |    346683 |    9123    30626 |    4452    3239    84579    26.1 |  0.504 % |
c |    347189 |    9123    30626 |    4897    3745   101151    27.0 |  0.504 % |
c |    347949 |    9123    30626 |    5387    4505   129815    28.8 |  0.504 % |
c |    349089 |    9123    30626 |    5926    5645   185115    32.8 |  0.505 % |
c |    350799 |    9123    30626 |    6518    3892   156710    40.3 |  0.504 % |
c |    353362 |    9123    30626 |    7170    6455   298671    46.3 |  0.504 % |
c |    357207 |    9123    30626 |    7887    6419   335766    52.3 |  0.504 % |
c ==============================================================================
c [1mFound solution: 216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 312   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    360273 |    9126    30647 |    3042    5045   247238    49.0 |  0.504 % |
c |    360373 |    9126    30647 |    3346    2623   117103    44.6 |  0.629 % |
c |    360523 |    9126    30647 |    3680    2773   118580    42.8 |  0.629 % |
c |    360748 |    9126    30647 |    4048    2998   122725    40.9 |  0.629 % |
c |    361088 |    9126    30647 |    4453    3338   134307    40.2 |  0.629 % |
c |    361595 |    9126    30647 |    4899    3845   149787    39.0 |  0.629 % |
c |    362354 |    9126    30647 |    5389    4604   173693    37.7 |  0.629 % |
c |    363493 |    9126    30647 |    5927    5743   237669    41.4 |  0.629 % |
c |    365201 |    9126    30647 |    6520    4367   156419    35.8 |  0.629 % |
c |    367763 |    9126    30647 |    7172    6929   294612    42.5 |  0.629 % |
c |    371608 |    9126    30647 |    7890    6811   357117    52.4 |  0.629 % |
c |    377374 |    9126    30647 |    8679    8095   536314    66.3 |  0.629 % |
c |    386025 |    9126    30647 |    9547    7057   433609    61.4 |  0.629 % |
c |    398999 |    9126    30647 |   10501    9683   812575    83.9 |  0.629 % |
c |    418461 |    9126    30647 |   11551    6111   484350    79.3 |  0.629 % |
c |    447653 |    9126    30647 |   12707   10392   820895    79.0 |  0.629 % |
c |    491445 |    9126    30647 |   13977   13467  1193079    88.6 |  0.629 % |
c |    557131 |    9126    30647 |   15375   11978  1113398    93.0 |  0.629 % |
c |    655659 |    9126    30647 |   16913   12274  1398312   113.9 |  0.629 % |
c ==============================================================================
c [1mFound solution: 210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 318   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    673862 |    9131    30683 |    3043   12451   901240    72.4 |  0.629 % |
c |    673962 |    9131    30683 |    3347    1658    14441     8.7 |  0.817 % |
c |    674114 |    9131    30683 |    3682    1810    17468     9.7 |  0.816 % |
c |    674340 |    9131    30683 |    4050    2036    21920    10.8 |  0.816 % |
c |    674678 |    9131    30683 |    4455    2374    33078    13.9 |  0.816 % |
c |    675184 |    9131    30683 |    4900    2880    49725    17.3 |  0.816 % |
c |    675944 |    9131    30683 |    5390    3640    67327    18.5 |  0.816 % |
c |    677084 |    9131    30683 |    5929    4780   135254    28.3 |  0.816 % |
c |    678792 |    9131    30683 |    6522    6488   254965    39.3 |  0.816 % |
c |    681356 |    9131    30683 |    7175    5274   258731    49.1 |  0.816 % |
c |    685201 |    9131    30683 |    7892    5448   274870    50.5 |  0.816 % |
c ==============================================================================
c [1mFound solution: 209[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 319   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    686469 |    9132    30688 |    3044    6716   340937    50.8 |  0.816 % |
c |    686569 |    9132    30688 |    3348    1779    23656    13.3 |  0.878 % |
c |    686719 |    9132    30688 |    3683    1929    27328    14.2 |  0.878 % |
c |    686944 |    9132    30688 |    4051    2154    31619    14.7 |  0.878 % |
c |    687283 |    9132    30688 |    4456    2493    41726    16.7 |  0.878 % |
c |    687789 |    9132    30688 |    4902    2999    54900    18.3 |  0.878 % |
c |    688548 |    9132    30688 |    5392    3758    83816    22.3 |  0.878 % |
c |    689688 |    9132    30688 |    5931    4898   133414    27.2 |  0.878 % |
c |    691398 |    9132    30688 |    6525    6608   220056    33.3 |  0.878 % |
c |    693963 |    9132    30688 |    7177    5869   247992    42.3 |  0.878 % |
c |    697809 |    9132    30688 |    7895    5682   320393    56.4 |  0.878 % |
c |    703575 |    9132    30688 |    8684    6976   374540    53.7 |  0.878 % |
c |    712224 |    9132    30688 |    9553    6042   466862    77.3 |  0.878 % |
c |    725199 |    9132    30688 |   10508    8517   754241    88.6 |  0.878 % |
c |    744660 |    9132    30688 |   11559   10854   864859    79.7 |  0.878 % |
c |    773852 |    9126    30671 |   12715    8954   608471    68.0 |  0.940 % |
c |    817642 |    9126    30671 |   13987   11695  1050111    89.8 |  0.940 % |
c |    883327 |    9126    30671 |   15385   10063   908950    90.3 |  0.940 % |
c |    981854 |    9126    30671 |   16924   11138  1187317   106.6 |  0.940 % |
c |   1129643 |    9126    30671 |   18616   15480  1449843    93.7 |  0.940 % |
#### 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.93 0.97 0.86 2/55 24872
Raw data (stat): 24872 (runsolver) R 24871 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478712763 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.94 0.97 0.86 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 960 0 0 0 996 2 0 0 25 0 1 0 478712763 5554176 938 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1356 938 603 41 0 1315 0
vsize: 5424
[startup+20.0008 s]
Raw data (loadavg): 0.95 0.97 0.86 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 1388 0 0 0 1994 3 0 0 25 0 1 0 478712763 7172096 1366 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1751 1366 603 41 0 1710 0
vsize: 7004
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.97 0.86 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 1487 0 0 0 2994 3 0 0 25 0 1 0 478712763 7577600 1465 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1850 1465 603 41 0 1809 0
vsize: 7400
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.86 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 1669 0 0 0 3993 4 0 0 25 0 1 0 478712763 8384512 1647 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2047 1647 603 41 0 2006 0
vsize: 8188
[startup+50.0016 s]
Raw data (loadavg): 0.97 0.97 0.86 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 1893 0 0 0 4992 5 0 0 25 0 1 0 478712763 9326592 1871 4294967295 134512640 134672761 3221224576 3221223680 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2277 1871 603 41 0 2236 0
vsize: 9108
[startup+60.0014 s]
Raw data (loadavg): 0.97 0.97 0.86 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2061 0 0 0 5992 5 0 0 25 0 1 0 478712763 9998336 2039 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2441 2039 603 41 0 2400 0
vsize: 9764
[startup+70.0008 s]
Raw data (loadavg): 0.97 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2093 0 0 0 6992 5 0 0 25 0 1 0 478712763 10129408 2071 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2473 2071 603 41 0 2432 0
vsize: 9892
[startup+80.0014 s]
Raw data (loadavg): 0.98 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2257 0 0 0 7992 6 0 0 25 0 1 0 478712763 10801152 2235 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2637 2235 603 41 0 2596 0
vsize: 10548
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2258 0 0 0 8992 6 0 0 25 0 1 0 478712763 10801152 2236 4294967295 134512640 134672761 3221224576 3221223776 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2637 2236 603 41 0 2596 0
vsize: 10548
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2301 0 0 0 9992 6 0 0 25 0 1 0 478712763 10932224 2279 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2279 603 41 0 2628 0
vsize: 10676
[startup+110.001 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2301 0 0 0 10992 6 0 0 25 0 1 0 478712763 10932224 2279 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2279 603 41 0 2628 0
vsize: 10676
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2305 0 0 0 11992 6 0 0 25 0 1 0 478712763 10932224 2283 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2283 603 41 0 2628 0
vsize: 10676
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2306 0 0 0 12993 6 0 0 25 0 1 0 478712763 10932224 2284 4294967295 134512640 134672761 3221224576 3221223680 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2284 603 41 0 2628 0
vsize: 10676
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2306 0 0 0 13993 6 0 0 25 0 1 0 478712763 10932224 2284 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2284 603 41 0 2628 0
vsize: 10676
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2306 0 0 0 14993 6 0 0 25 0 1 0 478712763 10932224 2284 4294967295 134512640 134672761 3221224576 3221223744 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2284 603 41 0 2628 0
vsize: 10676
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2306 0 0 0 15993 6 0 0 25 0 1 0 478712763 10932224 2284 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2284 603 41 0 2628 0
vsize: 10676
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2347 0 0 0 16993 6 0 0 25 0 1 0 478712763 11202560 2325 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2735 2325 603 41 0 2694 0
vsize: 10940
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2394 0 0 0 17993 6 0 0 25 0 1 0 478712763 11337728 2372 4294967295 134512640 134672761 3221224576 3221223680 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2372 603 41 0 2727 0
vsize: 11072
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24872
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2411 0 0 0 18993 6 0 0 25 0 1 0 478712763 11530240 2389 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2389 603 41 0 2774 0
vsize: 11260
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2411 0 0 0 19993 6 0 0 25 0 1 0 478712763 11530240 2389 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2389 603 41 0 2774 0
vsize: 11260
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2428 0 0 0 20994 6 0 0 25 0 1 0 478712763 11530240 2406 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2406 603 41 0 2774 0
vsize: 11260
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2587 0 0 0 21993 7 0 0 25 0 1 0 478712763 12214272 2565 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2565 603 41 0 2941 0
vsize: 11928
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2690 0 0 0 22993 7 0 0 25 0 1 0 478712763 12619776 2668 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3081 2668 603 41 0 3040 0
vsize: 12324
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2690 0 0 0 23993 7 0 0 25 0 1 0 478712763 12619776 2668 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3081 2668 603 41 0 3040 0
vsize: 12324
[startup+250 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2690 0 0 0 24993 7 0 0 25 0 1 0 478712763 12619776 2668 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3081 2668 603 41 0 3040 0
vsize: 12324
[startup+259.999 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2904 0 0 0 25993 8 0 0 25 0 1 0 478712763 13430784 2882 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3279 2882 603 41 0 3238 0
vsize: 13116
[startup+269.999 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2904 0 0 0 26993 8 0 0 25 0 1 0 478712763 13430784 2882 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3279 2882 603 41 0 3238 0
vsize: 13116
[startup+279.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2973 0 0 0 27993 8 0 0 25 0 1 0 478712763 13832192 2951 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2951 603 41 0 3336 0
vsize: 13508
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 28993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+299.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 29994 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223752 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 30993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 31993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 32993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 33993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 34993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+359.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 35993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+369.999 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 36993 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 37994 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 38994 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 39994 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+409.997 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 40994 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+419.997 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 41994 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+429.997 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 42994 8 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+439.997 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 43994 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+449.997 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 44995 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+459.997 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 45995 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223760 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+469.997 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 46995 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+479.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 47995 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+489.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 48995 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+499.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 49995 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+509.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 50996 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+519.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 51996 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223792 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+529.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 52996 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+539.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 2977 0 0 0 53996 9 0 0 25 0 1 0 478712763 13832192 2955 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3377 2955 603 41 0 3336 0
vsize: 13508
[startup+549.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3024 0 0 0 54996 9 0 0 25 0 1 0 478712763 13967360 3002 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 3002 603 41 0 3369 0
vsize: 13640
[startup+559.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3225 0 0 0 55996 9 0 0 25 0 1 0 478712763 14774272 3203 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3607 3203 603 41 0 3566 0
vsize: 14428
[startup+569.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3262 0 0 0 56996 9 0 0 25 0 1 0 478712763 15040512 3240 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3672 3240 603 41 0 3631 0
vsize: 14688
[startup+579.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3370 0 0 0 57996 10 0 0 25 0 1 0 478712763 15441920 3348 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3348 603 41 0 3729 0
vsize: 15080
[startup+589.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3376 0 0 0 58996 10 0 0 25 0 1 0 478712763 15441920 3354 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3354 603 41 0 3729 0
vsize: 15080
[startup+599.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3410 0 0 0 59996 10 0 0 25 0 1 0 478712763 15577088 3388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3803 3388 603 41 0 3762 0
vsize: 15212
[startup+609.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3436 0 0 0 60996 10 0 0 25 0 1 0 478712763 15712256 3414 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3836 3414 603 41 0 3795 0
vsize: 15344
[startup+619.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3436 0 0 0 61996 10 0 0 25 0 1 0 478712763 15712256 3414 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3836 3414 603 41 0 3795 0
vsize: 15344
[startup+629.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3509 0 0 0 62996 10 0 0 25 0 1 0 478712763 15978496 3487 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3901 3487 603 41 0 3860 0
vsize: 15604
[startup+639.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 63995 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+649.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 64995 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223760 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+659.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 65996 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+669.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 66996 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+679.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 67996 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+689.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 68996 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223760 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+699.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 69996 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+709.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 70996 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+719.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 71997 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+729.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 72997 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+739.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 73997 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+749.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 74997 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+759.991 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 75997 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+769.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 76997 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+779.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 77998 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+789.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 78998 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+799.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 79998 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+809.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 80998 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+819.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 81998 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+829.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 82998 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+839.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 83999 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+849.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 84999 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+859.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 85999 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+869.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3510 0 0 0 86999 10 0 0 25 0 1 0 478712763 15978496 3488 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3901 3488 603 41 0 3860 0
vsize: 15604
[startup+879.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3693 0 0 0 87999 11 0 0 25 0 1 0 478712763 16781312 3671 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4097 3671 603 41 0 4056 0
vsize: 16388
[startup+889.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3693 0 0 0 88999 11 0 0 25 0 1 0 478712763 16781312 3671 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4097 3671 603 41 0 4056 0
vsize: 16388
[startup+899.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3693 0 0 0 89999 11 0 0 25 0 1 0 478712763 16781312 3671 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4097 3671 603 41 0 4056 0
vsize: 16388
[startup+909.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3693 0 0 0 90999 11 0 0 25 0 1 0 478712763 16781312 3671 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4097 3671 603 41 0 4056 0
vsize: 16388
[startup+919.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3693 0 0 0 91999 11 0 0 25 0 1 0 478712763 16781312 3671 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4097 3671 603 41 0 4056 0
vsize: 16388
[startup+929.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3694 0 0 0 93000 11 0 0 25 0 1 0 478712763 16781312 3672 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4097 3672 603 41 0 4056 0
vsize: 16388
[startup+939.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3694 0 0 0 94000 11 0 0 25 0 1 0 478712763 16781312 3672 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4097 3672 603 41 0 4056 0
vsize: 16388
[startup+949.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 95000 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223680 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+959.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 96000 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+969.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 97000 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+979.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 98000 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+989.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 99001 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+999.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 100001 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 101001 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223712 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 102001 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 103001 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 104001 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3725 0 0 0 105002 11 0 0 25 0 1 0 478712763 16916480 3703 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3703 603 41 0 4089 0
vsize: 16520
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3739 0 0 0 106002 11 0 0 25 0 1 0 478712763 16916480 3717 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3717 603 41 0 4089 0
vsize: 16520
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3739 0 0 0 107002 11 0 0 25 0 1 0 478712763 16916480 3717 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3717 603 41 0 4089 0
vsize: 16520
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3739 0 0 0 108002 11 0 0 25 0 1 0 478712763 16916480 3717 4294967295 134512640 134672761 3221224576 3221223592 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3717 603 41 0 4089 0
vsize: 16520
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3739 0 0 0 109002 11 0 0 25 0 1 0 478712763 16916480 3717 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3717 603 41 0 4089 0
vsize: 16520
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3745 0 0 0 110002 11 0 0 25 0 1 0 478712763 17051648 3723 4294967295 134512640 134672761 3221224576 3221223680 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4163 3723 603 41 0 4122 0
vsize: 16652
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3745 0 0 0 111003 11 0 0 25 0 1 0 478712763 17051648 3723 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4163 3723 603 41 0 4122 0
vsize: 16652
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3745 0 0 0 112003 11 0 0 25 0 1 0 478712763 17051648 3723 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4163 3723 603 41 0 4122 0
vsize: 16652
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3747 0 0 0 113003 11 0 0 25 0 1 0 478712763 17051648 3725 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4163 3725 603 41 0 4122 0
vsize: 16652
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3747 0 0 0 114002 12 0 0 25 0 1 0 478712763 17051648 3725 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4163 3725 603 41 0 4122 0
vsize: 16652
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3747 0 0 0 115002 12 0 0 25 0 1 0 478712763 17051648 3725 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4163 3725 603 41 0 4122 0
vsize: 16652
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 3804 0 0 0 116002 12 0 0 25 0 1 0 478712763 17186816 3782 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3782 603 41 0 4155 0
vsize: 16784
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 4026 0 0 0 117001 12 0 0 25 0 1 0 478712763 18120704 4004 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4424 4004 603 41 0 4383 0
vsize: 17696
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 4076 0 0 0 118001 12 0 0 25 0 1 0 478712763 18391040 4054 4294967295 134512640 134672761 3221224576 3221223680 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 4054 603 41 0 4449 0
vsize: 17960
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 4172 0 0 0 119001 13 0 0 25 0 1 0 478712763 18792448 4150 4294967295 134512640 134672761 3221224576 3221223680 134555333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4150 603 41 0 4547 0
vsize: 18352
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24880
Raw data (stat): 24872 (minisat+) R 24871 20838 20837 0 -1 0 4172 0 0 0 120002 13 0 0 25 0 1 0 478712763 18792448 4150 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4150 603 41 0 4547 0
vsize: 18352
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 24880
Raw data (stat): 24872 (minisat+) Z 24871 20838 20837 0 -1 12 4175 0 0 0 120002 13 0 0 25 0 1 0 478712763 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
CPU time (s): 1200.16
CPU user time (s): 1200.02
CPU system time (s): 0.139978
CPU usage (%): 100.014
Max. virtual memory (Kb): 18352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####