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