CNF Benchmark Suite: PIPE-OOO-UNSAT.1.1
==========================================

Description:    Bigger variants of the pipe_ooo benchmarks, generated in a new way [1]

# of instances: 14

Author:         Miroslav N. Velev (mvelev@ece.cmu.edu)
                http://www.ece.cmu.edu/~mvelev

Date:           August 23, 2003



CNF Formula      Size [Bytes]    Variables    Clauses    Literals    Avg. Literals/Clause
--------------------------------------------------------------------------------------------
2pipe_2_ooo_q0_T0         93711          895       6561       18491                2.818320
3pipe_3_ooo_q0_T0        411784         2566      25625       73531                2.869502
4pipe_4_ooo_q0_T0       1206307         5605      70042      202998                2.898232
5pipe_5_ooo_q0_T0       2770297        10482     156027      455065                2.916579
6pipe_6_ooo_q0_T0       5695394        17710     304026      890580                2.929289
7pipe_7_ooo_q0_T0      10420768        27846     538853     1583475                2.938603
8pipe_8_ooo_q0_T0      17907224        41491     889823     2621165                2.945715
9pipe_9_ooo_q0_T0      28848720        59024    1430330     4221778                2.951611
10pipe_10_ooo_q0_T0    43122443        81932    2080755     6150399                2.955850
11pipe_11_ooo_q0_T0    63121765       110150    3003049     8887779                2.959585
12pipe_12_ooo_q0_T0    90564549       144721    4206416    12462424                2.962718
13pipe_13_ooo_q0_T0   128475571       185924    5911016    17529176                2.965510
14pipe_14_ooo_q0_T0   171037169       236250    7676928    22782646                2.967677
15pipe_15_ooo_q0_T0   228709743       294982   10067733    29897883                2.969674



References:

[1] M.N. Velev, "Automatic Abstraction of Equations in a Logic of Equality,"
    TABLEAUX'03, LNAI, Springer-Verlag, September 2003.






output of md5sum:
--------------------------------------------------------------------------------------------
8a741ba3d4e5bb1cd57831eceb8365ea  2pipe_2_ooo_q0_T0.cnf
a57f8007abe06a08f2a7139b020b9f65  3pipe_3_ooo_q0_T0.cnf
c9e49521f0d3fae830778cf85de8960a  4pipe_4_ooo_q0_T0.cnf
f931d259683b0bd4f0c2b56f40247977  5pipe_5_ooo_q0_T0.cnf
a6b972b212c8d2781429eb814afabd26  6pipe_6_ooo_q0_T0.cnf
2315b6e1f0ae9836b35aabd68badac91  7pipe_7_ooo_q0_T0.cnf
a6cafd006aee21c30f878e0ee41bc74d  8pipe_8_ooo_q0_T0.cnf
1147fbebfb310863a64249f49a21aed7  9pipe_9_ooo_q0_T0.cnf
9559726a8731d0a26437f04155894b4f  10pipe_10_ooo_q0_T0.cnf
a330365682519d6419522b5c26f9db68  11pipe_11_ooo_q0_T0.cnf
246cc0842a0e162463bb31a866943b82  12pipe_12_ooo_q0_T0.cnf
a146c014da57cadc28fac9470ba87dcb  13pipe_13_ooo_q0_T0.cnf
01bf43748804783331a3b6128637bfa2  14pipe_14_ooo_q0_T0.cnf
5f7c3652ab952feb5c739bf599a0efe4  15pipe_15_ooo_q0_T0.cnf