PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-5xp1.b.opb
MD5SUM	24a8f38e94b07e6ca192a34c96c24c6e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	12
Optimality of the best value was proved	NO
Number of terms in the objective function	465
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	465
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	465
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	464
Total number of constraints	859
Number of constraints which are clauses	845
Number of constraints which are cardinality constraints (but not clauses)	14
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	149
Trace number 4654

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-13 19:29:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3443 boxname=wulflinc19 idbench=59 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  24a8f38e94b07e6ca192a34c96c24c6e  /oldhome/oroussel/tmp/wulflinc19/normalized-5xp1.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-5xp1.b.opb /oldhome/oroussel/tmp/wulflinc19/normalized-5xp1.b.opb
IDLAUNCH: 3443
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        895092 kB
Buffers:         32884 kB
Cached:          73208 kB
SwapCached:         56 kB
Active:          43744 kB
Inactive:        65324 kB
HighTotal:      131008 kB
HighFree:        53704 kB
LowTotal:       903652 kB
LowFree:        841388 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25040 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:49:47 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 3443 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 843 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 |     843    29887 |     281       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 920   maxlim: 445   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7236    52708 |    2412       0        0     nan |  0.000 % |
c |       100 |    7236    52708 |    2653     100      585     5.8 |  0.648 % |
c |       250 |    7236    52708 |    2918     250     1381     5.5 |  0.648 % |
c |       475 |    7196    52574 |    3210     466     2662     5.7 |  1.151 % |
c |       813 |    7174    52499 |    3531     797     5921     7.4 |  1.439 % |
c |      1320 |    7165    52468 |    3884    1301    26683    20.5 |  1.511 % |
c |      2079 |    7165    52468 |    4273    2060    89353    43.4 |  1.511 % |
c |      3220 |    7159    52448 |    4700    3197   192675    60.3 |  1.583 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 446   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4675 |    7138    52378 |    2379    4642   339417    73.1 |  1.583 % |
c |      4775 |    7138    52378 |    2616    2421   114161    47.2 |  1.940 % |
c |      4925 |    7138    52378 |    2878    2571   125555    48.8 |  1.940 % |
c |      5151 |    7138    52378 |    3166    2797   130496    46.7 |  1.940 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 447   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5392 |    7073    52133 |    2357    2989   149101    49.9 |  1.940 % |
c |      5492 |    7073    52133 |    2592    1595    35267    22.1 |  3.015 % |
c |      5642 |    7073    52133 |    2851    1745    43859    25.1 |  3.015 % |
c |      5872 |    7057    52081 |    3137    1972    60501    30.7 |  3.230 % |
c |      6209 |    7057    52081 |    3450    2309    89749    38.9 |  3.230 % |
c |      6718 |    7057    52081 |    3795    2818   134086    47.6 |  3.230 % |
c |      7479 |    7057    52081 |    4175    3579   207354    57.9 |  3.230 % |
c |      8620 |    7057    52081 |    4593    2435   105410    43.3 |  3.230 % |
c |     10330 |    7057    52081 |    5052    4145   320058    77.2 |  3.230 % |
c |     12892 |    7057    52081 |    5557    4020   290990    72.4 |  3.230 % |
c ==============================================================================
c [1mFound solution: 16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 449   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12924 |    7058    52086 |    2352    4052   293839    72.5 |  3.230 % |
c |     13024 |    7058    52086 |    2587    2126    95888    45.1 |  3.300 % |
c |     13176 |    7058    52086 |    2845    2278   112297    49.3 |  3.300 % |
c |     13401 |    7058    52086 |    3130    2503   132662    53.0 |  3.300 % |
c |     13739 |    7058    52086 |    3443    2841   161931    57.0 |  3.300 % |
c |     14245 |    7058    52086 |    3787    3347   209965    62.7 |  3.300 % |
c |     15006 |    7058    52086 |    4166    2168   101333    46.7 |  3.300 % |
c |     16150 |    7058    52086 |    4583    3312   234142    70.7 |  3.300 % |
c |     17858 |    7058    52086 |    5041    2600   157654    60.6 |  3.300 % |
c |     20421 |    7058    52086 |    5545    5163   569584   110.3 |  3.300 % |
c |     24266 |    7058    52086 |    6100    5973   720660   120.7 |  3.300 % |
c ==============================================================================
c [1mFound solution: 15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 450   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26520 |    7059    52092 |    2353    4973   558795   112.4 |  3.300 % |
c |     26620 |    7059    52092 |    2588    1344    36105    26.9 |  3.369 % |
c |     26772 |    7059    52092 |    2847    1496    37977    25.4 |  3.369 % |
c |     26997 |    7059    52092 |    3131    1721    52181    30.3 |  3.369 % |
c |     27337 |    7059    52092 |    3445    2061    80875    39.2 |  3.369 % |
c |     27843 |    7059    52092 |    3789    2567   150618    58.7 |  3.369 % |
c |     28602 |    7059    52092 |    4168    3326   189589    57.0 |  3.369 % |
c |     29741 |    7059    52092 |    4585    4465   311880    69.8 |  3.371 % |
c |     31450 |    7059    52092 |    5043    3657   291138    79.6 |  3.369 % |
c |     34013 |    7059    52092 |    5548    3554   211281    59.4 |  3.369 % |
c |     37858 |    7059    52092 |    6103    4359   347070    79.6 |  3.369 % |
c |     43624 |    7059    52092 |    6713    3562   285428    80.1 |  3.369 % |
c |     52277 |    7059    52092 |    7384    5013   547589   109.2 |  3.369 % |
c ==============================================================================
c [1mFound solution: 14[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 451   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63788 |    7060    52096 |    2353    4806   513313   106.8 |  3.369 % |
c |     63889 |    7060    52096 |    2588    1303    37710    28.9 |  3.438 % |
c |     64039 |    7060    52096 |    2847    1453    41389    28.5 |  3.438 % |
c |     64264 |    7060    52096 |    3131    1678    45680    27.2 |  3.438 % |
c |     64602 |    7060    52096 |    3445    2016    68758    34.1 |  3.438 % |
c |     65109 |    7060    52096 |    3789    2523    88828    35.2 |  3.438 % |
c |     65871 |    7060    52096 |    4168    3285   151834    46.2 |  3.438 % |
c |     67011 |    7060    52096 |    4585    4425   285646    64.6 |  3.438 % |
c |     68719 |    7060    52096 |    5043    3598   243186    67.6 |  3.438 % |
c |     71281 |    7060    52096 |    5548    3448   251029    72.8 |  3.438 % |
c |     75127 |    7060    52096 |    6103    4280   385683    90.1 |  3.438 % |
c |     80894 |    7034    52006 |    6713    3529   237076    67.2 |  3.725 % |
c |     89543 |    7008    51916 |    7384    5227   447163    85.5 |  4.012 % |
c |    102521 |    7008    51916 |    8123    6398   579192    90.5 |  4.012 % |
c |    121987 |    7008    51916 |    8935    4758   314170    66.0 |  4.012 % |
c |    151182 |    7008    51916 |    9829    5956   614863   103.2 |  4.012 % |
c |    194972 |    6973    51795 |   10811    8775   833332    95.0 |  4.370 % |
c |    260656 |    6873    51449 |   11893    6855   782631   114.2 |  5.587 % |
c |    359182 |    6873    51449 |   13082   11951  1394074   116.6 |  5.587 % |
c |    506977 |    6873    51449 |   14390   12440  1090935    87.7 |  5.587 % |
c |    728662 |    6873    51449 |   15829   13664  1413196   103.4 |  5.587 % |
#### 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.83 0.37 0.14 2/55 25311
Raw data (stat): 25311 (runsolver) R 25310 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478475089 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.0008 s]
Raw data (loadavg): 0.86 0.39 0.14 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1031 0 0 0 996 2 0 0 25 0 1 0 478475089 5791744 1009 4294967295 134512640 134672761 3221224576 3221223532 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1414 1009 603 41 0 1373 0
vsize: 5656
[startup+20.0013 s]
Raw data (loadavg): 0.88 0.41 0.15 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1491 0 0 0 1993 4 0 0 25 0 1 0 478475089 7667712 1469 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1872 1469 603 41 0 1831 0
vsize: 7488
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.43 0.16 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1491 0 0 0 2993 4 0 0 25 0 1 0 478475089 7667712 1469 4294967295 134512640 134672761 3221224576 3221223744 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1872 1469 603 41 0 1831 0
vsize: 7488
[startup+40.0032 s]
Raw data (loadavg): 0.91 0.45 0.17 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1638 0 0 0 3992 5 0 0 25 0 1 0 478475089 8204288 1616 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2003 1616 603 41 0 1962 0
vsize: 8012
[startup+50.0039 s]
Raw data (loadavg): 0.93 0.47 0.18 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1914 0 0 0 4991 6 0 0 25 0 1 0 478475089 9273344 1892 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2264 1892 603 41 0 2223 0
vsize: 9056
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.48 0.19 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1921 0 0 0 5991 6 0 0 25 0 1 0 478475089 9404416 1899 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1899 603 41 0 2255 0
vsize: 9184
[startup+70.0041 s]
Raw data (loadavg): 0.95 0.50 0.20 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1921 0 0 0 6991 6 0 0 25 0 1 0 478475089 9404416 1899 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1899 603 41 0 2255 0
vsize: 9184
[startup+80.0053 s]
Raw data (loadavg): 0.95 0.52 0.20 2/55 25311
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1921 0 0 0 7991 7 0 0 25 0 1 0 478475089 9404416 1899 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1899 603 41 0 2255 0
vsize: 9184
[startup+90.0057 s]
Raw data (loadavg): 0.96 0.53 0.21 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1921 0 0 0 8990 7 0 0 25 0 1 0 478475089 9404416 1899 4294967295 134512640 134672761 3221224576 3221223760 134558923 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1899 603 41 0 2255 0
vsize: 9184
[startup+100.006 s]
Raw data (loadavg): 0.97 0.55 0.22 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1921 0 0 0 9990 8 0 0 25 0 1 0 478475089 9404416 1899 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1899 603 41 0 2255 0
vsize: 9184
[startup+110.006 s]
Raw data (loadavg): 0.97 0.56 0.23 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 1955 0 0 0 10989 8 0 0 25 0 1 0 478475089 9539584 1933 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2329 1933 603 41 0 2288 0
vsize: 9316
[startup+120.007 s]
Raw data (loadavg): 0.97 0.57 0.23 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2056 0 0 0 11989 9 0 0 25 0 1 0 478475089 9940992 2034 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2427 2034 603 41 0 2386 0
vsize: 9708
[startup+130.007 s]
Raw data (loadavg): 0.98 0.59 0.24 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2056 0 0 0 12989 9 0 0 25 0 1 0 478475089 9940992 2034 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2427 2034 603 41 0 2386 0
vsize: 9708
[startup+140.008 s]
Raw data (loadavg): 0.98 0.60 0.25 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2140 0 0 0 13988 10 0 0 25 0 1 0 478475089 10207232 2118 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2492 2118 603 41 0 2451 0
vsize: 9968
[startup+150.008 s]
Raw data (loadavg): 0.98 0.61 0.26 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2275 0 0 0 14988 11 0 0 25 0 1 0 478475089 10883072 2253 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2657 2253 603 41 0 2616 0
vsize: 10628
[startup+160.009 s]
Raw data (loadavg): 0.99 0.63 0.27 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2382 0 0 0 15987 11 0 0 25 0 1 0 478475089 11288576 2360 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2756 2360 603 41 0 2715 0
vsize: 11024
[startup+170.009 s]
Raw data (loadavg): 0.99 0.64 0.27 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2383 0 0 0 16987 12 0 0 25 0 1 0 478475089 11288576 2361 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2756 2361 603 41 0 2715 0
vsize: 11024
[startup+180.009 s]
Raw data (loadavg): 0.99 0.65 0.28 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2383 0 0 0 17987 12 0 0 25 0 1 0 478475089 11288576 2361 4294967295 134512640 134672761 3221224576 3221223668 1075346951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2756 2361 603 41 0 2715 0
vsize: 11024
[startup+190.01 s]
Raw data (loadavg): 0.99 0.66 0.29 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2383 0 0 0 18987 12 0 0 25 0 1 0 478475089 11288576 2361 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2756 2361 603 41 0 2715 0
vsize: 11024
[startup+200.01 s]
Raw data (loadavg): 0.99 0.67 0.29 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2383 0 0 0 19987 12 0 0 25 0 1 0 478475089 11288576 2361 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2756 2361 603 41 0 2715 0
vsize: 11024
[startup+210.01 s]
Raw data (loadavg): 1.07 0.70 0.31 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2421 0 0 0 20986 13 0 0 25 0 1 0 478475089 11419648 2399 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2788 2399 603 41 0 2747 0
vsize: 11152
[startup+220.011 s]
Raw data (loadavg): 1.06 0.71 0.31 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2565 0 0 0 21986 14 0 0 25 0 1 0 478475089 11952128 2543 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2918 2543 603 41 0 2877 0
vsize: 11672
[startup+230.012 s]
Raw data (loadavg): 1.05 0.72 0.32 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2565 0 0 0 22985 14 0 0 25 0 1 0 478475089 11952128 2543 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2918 2543 603 41 0 2877 0
vsize: 11672
[startup+240.012 s]
Raw data (loadavg): 1.04 0.72 0.33 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2669 0 0 0 23985 15 0 0 25 0 1 0 478475089 12484608 2647 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3048 2647 603 41 0 3007 0
vsize: 12192
[startup+250.013 s]
Raw data (loadavg): 1.03 0.73 0.33 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2669 0 0 0 24984 15 0 0 25 0 1 0 478475089 12484608 2647 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3048 2647 603 41 0 3007 0
vsize: 12192
[startup+260.013 s]
Raw data (loadavg): 1.03 0.74 0.34 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2669 0 0 0 25984 16 0 0 25 0 1 0 478475089 12484608 2647 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3048 2647 603 41 0 3007 0
vsize: 12192
[startup+270.014 s]
Raw data (loadavg): 1.02 0.75 0.35 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2669 0 0 0 26984 16 0 0 25 0 1 0 478475089 12484608 2647 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3048 2647 603 41 0 3007 0
vsize: 12192
[startup+280.014 s]
Raw data (loadavg): 1.02 0.76 0.35 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2799 0 0 0 27983 17 0 0 25 0 1 0 478475089 13021184 2777 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3179 2777 603 41 0 3138 0
vsize: 12716
[startup+290.016 s]
Raw data (loadavg): 1.02 0.77 0.36 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2890 0 0 0 28983 18 0 0 25 0 1 0 478475089 13418496 2868 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2868 603 41 0 3235 0
vsize: 13104
[startup+300.016 s]
Raw data (loadavg): 1.01 0.77 0.37 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2890 0 0 0 29983 18 0 0 25 0 1 0 478475089 13418496 2868 4294967295 134512640 134672761 3221224576 3221223744 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2868 603 41 0 3235 0
vsize: 13104
[startup+310.016 s]
Raw data (loadavg): 1.01 0.78 0.37 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 2890 0 0 0 30983 18 0 0 25 0 1 0 478475089 13418496 2868 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3276 2868 603 41 0 3235 0
vsize: 13104
[startup+320.017 s]
Raw data (loadavg): 1.01 0.79 0.38 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3008 0 0 0 31982 19 0 0 25 0 1 0 478475089 13815808 2986 4294967295 134512640 134672761 3221224576 3221223680 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3373 2986 603 41 0 3332 0
vsize: 13492
[startup+330.018 s]
Raw data (loadavg): 1.01 0.79 0.38 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3085 0 0 0 32981 20 0 0 25 0 1 0 478475089 14217216 3063 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3471 3063 603 41 0 3430 0
vsize: 13884
[startup+340.018 s]
Raw data (loadavg): 1.00 0.80 0.39 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3085 0 0 0 33981 20 0 0 25 0 1 0 478475089 14217216 3063 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3471 3063 603 41 0 3430 0
vsize: 13884
[startup+350.019 s]
Raw data (loadavg): 1.00 0.81 0.40 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3085 0 0 0 34981 20 0 0 25 0 1 0 478475089 14217216 3063 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3471 3063 603 41 0 3430 0
vsize: 13884
[startup+360.019 s]
Raw data (loadavg): 1.00 0.81 0.40 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3085 0 0 0 35981 20 0 0 25 0 1 0 478475089 14217216 3063 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3471 3063 603 41 0 3430 0
vsize: 13884
[startup+370.02 s]
Raw data (loadavg): 1.00 0.82 0.41 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3161 0 0 0 36981 21 0 0 25 0 1 0 478475089 14483456 3139 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3139 603 41 0 3495 0
vsize: 14144
[startup+380.02 s]
Raw data (loadavg): 1.00 0.82 0.41 2/55 25313
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3162 0 0 0 37980 21 0 0 25 0 1 0 478475089 14483456 3140 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3140 603 41 0 3495 0
vsize: 14144
[startup+390.02 s]
Raw data (loadavg): 1.00 0.83 0.42 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3162 0 0 0 38980 22 0 0 25 0 1 0 478475089 14483456 3140 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3140 603 41 0 3495 0
vsize: 14144
[startup+400.021 s]
Raw data (loadavg): 1.00 0.83 0.43 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3162 0 0 0 39980 22 0 0 25 0 1 0 478475089 14483456 3140 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3140 603 41 0 3495 0
vsize: 14144
[startup+410.021 s]
Raw data (loadavg): 1.00 0.84 0.43 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3162 0 0 0 40979 23 0 0 25 0 1 0 478475089 14483456 3140 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3140 603 41 0 3495 0
vsize: 14144
[startup+420.022 s]
Raw data (loadavg): 1.00 0.84 0.44 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3162 0 0 0 41979 23 0 0 25 0 1 0 478475089 14483456 3140 4294967295 134512640 134672761 3221224576 3221223760 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3140 603 41 0 3495 0
vsize: 14144
[startup+430.023 s]
Raw data (loadavg): 1.00 0.85 0.44 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 42979 23 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223680 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+440.022 s]
Raw data (loadavg): 1.00 0.85 0.45 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 43979 24 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+450.022 s]
Raw data (loadavg): 1.00 0.86 0.45 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 44979 24 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+460.022 s]
Raw data (loadavg): 1.00 0.86 0.46 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 45979 24 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+470.023 s]
Raw data (loadavg): 1.00 0.86 0.46 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 46979 24 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+480.023 s]
Raw data (loadavg): 1.00 0.87 0.47 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 47978 25 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223680 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+490.024 s]
Raw data (loadavg): 1.00 0.87 0.47 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 48978 25 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+500.024 s]
Raw data (loadavg): 1.00 0.88 0.48 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 49978 25 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+510.024 s]
Raw data (loadavg): 1.00 0.88 0.48 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 50978 25 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+520.025 s]
Raw data (loadavg): 1.00 0.88 0.49 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 51978 26 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+530.026 s]
Raw data (loadavg): 1.00 0.89 0.49 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3165 0 0 0 52978 26 0 0 25 0 1 0 478475089 14483456 3143 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3143 603 41 0 3495 0
vsize: 14144
[startup+540.025 s]
Raw data (loadavg): 1.00 0.89 0.50 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 53978 26 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+550.025 s]
Raw data (loadavg): 1.00 0.89 0.50 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 54978 26 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+560.026 s]
Raw data (loadavg): 1.00 0.90 0.51 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 55977 27 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+570.026 s]
Raw data (loadavg): 1.00 0.90 0.51 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 56977 27 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+580.027 s]
Raw data (loadavg): 1.00 0.90 0.52 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 57977 27 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+590.027 s]
Raw data (loadavg): 1.00 0.90 0.52 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 58977 28 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+600.028 s]
Raw data (loadavg): 1.00 0.91 0.53 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 59976 28 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+610.028 s]
Raw data (loadavg): 1.00 0.91 0.53 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3166 0 0 0 60976 28 0 0 25 0 1 0 478475089 14483456 3144 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3536 3144 603 41 0 3495 0
vsize: 14144
[startup+620.029 s]
Raw data (loadavg): 1.00 0.91 0.54 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3270 0 0 0 61976 29 0 0 25 0 1 0 478475089 14888960 3248 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3635 3248 603 41 0 3594 0
vsize: 14540
[startup+630.029 s]
Raw data (loadavg): 1.00 0.91 0.54 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3274 0 0 0 62976 29 0 0 25 0 1 0 478475089 14888960 3252 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3635 3252 603 41 0 3594 0
vsize: 14540
[startup+640.029 s]
Raw data (loadavg): 1.00 0.92 0.55 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3274 0 0 0 63976 29 0 0 25 0 1 0 478475089 14888960 3252 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3635 3252 603 41 0 3594 0
vsize: 14540
[startup+650.03 s]
Raw data (loadavg): 1.00 0.92 0.55 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3274 0 0 0 64976 29 0 0 25 0 1 0 478475089 14888960 3252 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3635 3252 603 41 0 3594 0
vsize: 14540
[startup+660.029 s]
Raw data (loadavg): 1.00 0.92 0.56 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3332 0 0 0 65976 30 0 0 25 0 1 0 478475089 15175680 3310 4294967295 134512640 134672761 3221224576 3221223532 1075350763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3310 603 41 0 3664 0
vsize: 14820
[startup+670.031 s]
Raw data (loadavg): 1.00 0.92 0.56 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3332 0 0 0 66976 30 0 0 25 0 1 0 478475089 15175680 3310 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3310 603 41 0 3664 0
vsize: 14820
[startup+680.031 s]
Raw data (loadavg): 1.00 0.92 0.56 2/55 25315
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3336 0 0 0 67975 30 0 0 25 0 1 0 478475089 15175680 3314 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3314 603 41 0 3664 0
vsize: 14820
[startup+690.031 s]
Raw data (loadavg): 1.00 0.93 0.57 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3336 0 0 0 68975 31 0 0 25 0 1 0 478475089 15175680 3314 4294967295 134512640 134672761 3221224576 3221223760 134558903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3314 603 41 0 3664 0
vsize: 14820
[startup+700.031 s]
Raw data (loadavg): 1.00 0.93 0.57 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3336 0 0 0 69975 31 0 0 25 0 1 0 478475089 15175680 3314 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3314 603 41 0 3664 0
vsize: 14820
[startup+710.031 s]
Raw data (loadavg): 1.00 0.93 0.58 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3336 0 0 0 70974 31 0 0 25 0 1 0 478475089 15175680 3314 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3314 603 41 0 3664 0
vsize: 14820
[startup+720.032 s]
Raw data (loadavg): 1.00 0.93 0.58 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3336 0 0 0 71974 31 0 0 25 0 1 0 478475089 15175680 3314 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3314 603 41 0 3664 0
vsize: 14820
[startup+730.032 s]
Raw data (loadavg): 1.00 0.93 0.58 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3336 0 0 0 72974 32 0 0 25 0 1 0 478475089 15175680 3314 4294967295 134512640 134672761 3221224576 3221223816 134560737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3314 603 41 0 3664 0
vsize: 14820
[startup+740.032 s]
Raw data (loadavg): 1.00 0.94 0.59 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3336 0 0 0 73974 32 0 0 25 0 1 0 478475089 15175680 3314 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3705 3314 603 41 0 3664 0
vsize: 14820
[startup+750.033 s]
Raw data (loadavg): 1.00 0.94 0.59 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 74974 33 0 0 25 0 1 0 478475089 16773120 3676 4294967295 134512640 134672761 3221224576 3221223680 134560070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4095 3676 603 41 0 4054 0
vsize: 16380
[startup+760.033 s]
Raw data (loadavg): 1.00 0.94 0.59 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 75973 33 0 0 25 0 1 0 478475089 16773120 3676 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4095 3676 603 41 0 4054 0
vsize: 16380
[startup+770.034 s]
Raw data (loadavg): 1.00 0.94 0.60 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 76973 34 0 0 25 0 1 0 478475089 16769024 3676 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4094 3676 603 41 0 4053 0
vsize: 16376
[startup+780.034 s]
Raw data (loadavg): 1.00 0.94 0.60 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 77972 34 0 0 25 0 1 0 478475089 16756736 3676 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4091 3676 603 41 0 4050 0
vsize: 16364
[startup+790.034 s]
Raw data (loadavg): 1.00 0.94 0.61 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 78972 34 0 0 25 0 1 0 478475089 16756736 3676 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4091 3676 603 41 0 4050 0
vsize: 16364
[startup+800.035 s]
Raw data (loadavg): 1.00 0.94 0.61 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 79972 35 0 0 25 0 1 0 478475089 16756736 3676 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4091 3676 603 41 0 4050 0
vsize: 16364
[startup+810.034 s]
Raw data (loadavg): 1.00 0.95 0.61 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 80972 35 0 0 25 0 1 0 478475089 16711680 3676 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4080 3676 603 41 0 4039 0
vsize: 16320
[startup+820.035 s]
Raw data (loadavg): 1.00 0.95 0.62 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3698 0 0 0 81972 35 0 0 25 0 1 0 478475089 16711680 3676 4294967295 134512640 134672761 3221224576 3221223680 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4080 3676 603 41 0 4039 0
vsize: 16320
[startup+830.037 s]
Raw data (loadavg): 1.00 0.95 0.62 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3699 0 0 0 82972 36 0 0 25 0 1 0 478475089 16711680 3677 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4080 3677 603 41 0 4039 0
vsize: 16320
[startup+840.036 s]
Raw data (loadavg): 1.00 0.95 0.63 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3699 0 0 0 83971 36 0 0 25 0 1 0 478475089 16711680 3677 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4080 3677 603 41 0 4039 0
vsize: 16320
[startup+850.036 s]
Raw data (loadavg): 1.00 0.95 0.63 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3700 0 0 0 84971 36 0 0 25 0 1 0 478475089 16711680 3678 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4080 3678 603 41 0 4039 0
vsize: 16320
[startup+860.037 s]
Raw data (loadavg): 1.00 0.95 0.63 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3700 0 0 0 85971 37 0 0 25 0 1 0 478475089 16629760 3675 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4060 3675 603 41 0 4019 0
vsize: 16240
[startup+870.037 s]
Raw data (loadavg): 1.00 0.95 0.64 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3700 0 0 0 86971 37 0 0 25 0 1 0 478475089 16629760 3675 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4060 3675 603 41 0 4019 0
vsize: 16240
[startup+880.037 s]
Raw data (loadavg): 1.00 0.95 0.64 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3700 0 0 0 87970 38 0 0 25 0 1 0 478475089 16629760 3675 4294967295 134512640 134672761 3221224576 3221223680 134555098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4060 3675 603 41 0 4019 0
vsize: 16240
[startup+890.037 s]
Raw data (loadavg): 1.00 0.95 0.64 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3700 0 0 0 88970 38 0 0 25 0 1 0 478475089 16629760 3675 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4060 3675 603 41 0 4019 0
vsize: 16240
[startup+900.037 s]
Raw data (loadavg): 1.00 0.95 0.65 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3700 0 0 0 89970 38 0 0 25 0 1 0 478475089 16629760 3675 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4060 3675 603 41 0 4019 0
vsize: 16240
[startup+910.037 s]
Raw data (loadavg): 1.00 0.96 0.65 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3700 0 0 0 90971 38 0 0 25 0 1 0 478475089 16629760 3675 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4060 3675 603 41 0 4019 0
vsize: 16240
[startup+920.038 s]
Raw data (loadavg): 1.00 0.96 0.65 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 91971 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223760 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+930.039 s]
Raw data (loadavg): 1.00 0.96 0.66 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 92971 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+940.039 s]
Raw data (loadavg): 1.00 0.96 0.66 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 93971 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+950.04 s]
Raw data (loadavg): 1.00 0.96 0.66 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 94971 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+960.04 s]
Raw data (loadavg): 1.00 0.96 0.66 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 95972 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223680 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+970.04 s]
Raw data (loadavg): 1.00 0.96 0.67 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 96972 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+980.04 s]
Raw data (loadavg): 1.00 0.96 0.67 2/55 25317
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 97972 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+990.039 s]
Raw data (loadavg): 1.00 0.96 0.67 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 98972 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223680 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.96 0.68 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 99972 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.97 0.68 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 100972 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.97 0.68 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3711 0 0 0 101973 38 0 0 25 0 1 0 478475089 16867328 3686 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4118 3686 603 41 0 4077 0
vsize: 16472
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.97 0.68 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 3913 0 0 0 102972 38 0 0 25 0 1 0 478475089 17670144 3888 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4314 3888 603 41 0 4273 0
vsize: 17256
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.97 0.69 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4010 0 0 0 103972 39 0 0 25 0 1 0 478475089 18075648 3985 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4413 3985 603 41 0 4372 0
vsize: 17652
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.97 0.69 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4010 0 0 0 104972 39 0 0 25 0 1 0 478475089 18075648 3985 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4413 3985 603 41 0 4372 0
vsize: 17652
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.97 0.69 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4010 0 0 0 105972 39 0 0 25 0 1 0 478475089 18075648 3985 4294967295 134512640 134672761 3221224576 3221223760 134559166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4413 3985 603 41 0 4372 0
vsize: 17652
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.97 0.70 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4010 0 0 0 106973 39 0 0 25 0 1 0 478475089 18075648 3985 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4413 3985 603 41 0 4372 0
vsize: 17652
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.97 0.70 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4010 0 0 0 107973 39 0 0 25 0 1 0 478475089 18075648 3985 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4413 3985 603 41 0 4372 0
vsize: 17652
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.97 0.70 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4010 0 0 0 108973 39 0 0 25 0 1 0 478475089 18075648 3985 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4413 3985 603 41 0 4372 0
vsize: 17652
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.97 0.70 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4038 0 0 0 109973 39 0 0 25 0 1 0 478475089 18214912 4013 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4447 4013 603 41 0 4406 0
vsize: 17788
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.97 0.71 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4038 0 0 0 110974 39 0 0 25 0 1 0 478475089 18214912 4013 4294967295 134512640 134672761 3221224576 3221223728 134564785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4447 4013 603 41 0 4406 0
vsize: 17788
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.97 0.71 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4038 0 0 0 111974 39 0 0 25 0 1 0 478475089 18214912 4013 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4447 4013 603 41 0 4406 0
vsize: 17788
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.97 0.71 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4038 0 0 0 112974 39 0 0 25 0 1 0 478475089 18214912 4013 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4447 4013 603 41 0 4406 0
vsize: 17788
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.97 0.72 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4078 0 0 0 113974 39 0 0 25 0 1 0 478475089 18345984 4053 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 4053 603 41 0 4438 0
vsize: 17916
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.97 0.72 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4081 0 0 0 114974 39 0 0 25 0 1 0 478475089 18345984 4056 4294967295 134512640 134672761 3221224576 3221223680 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 4056 603 41 0 4438 0
vsize: 17916
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.97 0.72 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4081 0 0 0 115974 39 0 0 25 0 1 0 478475089 18345984 4056 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 4056 603 41 0 4438 0
vsize: 17916
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.97 0.73 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4081 0 0 0 116975 39 0 0 25 0 1 0 478475089 18345984 4056 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 4056 603 41 0 4438 0
vsize: 17916
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.97 0.73 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4081 0 0 0 117975 39 0 0 25 0 1 0 478475089 18345984 4056 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 4056 603 41 0 4438 0
vsize: 17916
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.97 0.73 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4081 0 0 0 118975 39 0 0 25 0 1 0 478475089 18345984 4056 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 4056 603 41 0 4438 0
vsize: 17916
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.97 0.73 2/55 25319
Raw data (stat): 25311 (minisat+) R 25310 22929 22928 0 -1 0 4081 0 0 0 119975 39 0 0 25 0 1 0 478475089 18345984 4056 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 4056 603 41 0 4438 0
vsize: 17916
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.97 0.73 1/55 25319
Raw data (stat): 25311 (minisat+) Z 25310 22929 22928 0 -1 12 4084 0 0 0 119975 39 0 0 25 0 1 0 478475089 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.06
CPU time (s): 1200.16
CPU user time (s): 1199.76
CPU system time (s): 0.399939
CPU usage (%): 100.009
Max. virtual memory (Kb): 17916
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####