From 2bc4c351bbf89103577fa9f33ebb395f5d61826a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 12 Oct 2010 20:20:24 +0000 Subject: Merge from cc-memout branch. Here are the main points * Add ContextMemoryAllocator allocator type, conforming to STL allocator requirements. * Extend the CDList<> template to take an allocator (defaults to std::allocator). * Add a specialized version of the CDList<> template (in src/context/cdlist_context_memory.h) that allocates a list in segments, in context memory. * Add "forward" headers -- cdlist_forward.h, cdmap_forward.h, and cdset_forward.h. Use these in public headers, and other places where you don't need the full header (just the forward-declaration). These types justify their own header (instead of just forward-declaring yourself), because they are complex templated types, with default template parameters, specializations, etc. * theory_engine.h no longer depends on individual theory headers. (Instead it forward-declares Theory implementations.) This is especially important now that theory .cpp files depend on TheoryEngine (to implement Theory::getValue()). Previously, any modification to any theory header file required *all* theories, and the engine, to be completely rebuilt. * Support memory cleanup for nontrivial CONSTANT kinds. This resolves an issue with arithmetic where memory leaked for each distinct Rational or Integer that was wrapped in a Node. --- test/regress/regress0/uf/NEQ016_size5.smt | 27 --------------------------- test/regress/regress3/Makefile.am | 3 ++- test/regress/regress3/NEQ016_size5.smt | 27 +++++++++++++++++++++++++++ 3 files changed, 29 insertions(+), 28 deletions(-) delete mode 100644 test/regress/regress0/uf/NEQ016_size5.smt create mode 100644 test/regress/regress3/NEQ016_size5.smt (limited to 'test/regress') diff --git a/test/regress/regress0/uf/NEQ016_size5.smt b/test/regress/regress0/uf/NEQ016_size5.smt deleted file mode 100644 index ec56385f6..000000000 --- a/test/regress/regress0/uf/NEQ016_size5.smt +++ /dev/null @@ -1,27 +0,0 @@ -(benchmark NEQ016_size5.smt -:source { -CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC - for more information. - -This benchmark was obtained by trying to find a finite model of a first-order -formula (Albert Oliveras). -} -:status unsat -:category { crafted } -:difficulty { 0 } -:logic QF_UF -:extrapreds ((p2 U)) -:extrafuns ((f1 U U U)) -:extrapreds ((p4 U)) -:extrapreds ((p3 U)) -:extrafuns ((c6 U)) -:extrafuns ((c5 U)) -:extrafuns ((c7 U)) -:extrafuns ((c_0 U)) -:extrafuns ((c_1 U)) -:extrafuns ((c_2 U)) -:extrafuns ((c_3 U)) -:extrafuns ((c_4 U)) -:formula -( and -( distinct c_0 c_1 c_2 c_3 c_4 )(or (not (p2 c_0)) (not (p2 c_0)) (p4 (f1 c_0 c_0)) (p3 (f1 c_0 c_0)) )(or (not (p2 c_0)) (not (p2 c_1)) (p4 (f1 c_1 c_0)) (p3 (f1 c_1 c_0)) )(or (not (p2 c_0)) (not (p2 c_2)) (p4 (f1 c_2 c_0)) (p3 (f1 c_2 c_0)) )(or (not (p2 c_0)) (not (p2 c_3)) (p4 (f1 c_3 c_0)) (p3 (f1 c_3 c_0)) )(or (not (p2 c_0)) (not (p2 c_4)) (p4 (f1 c_4 c_0)) (p3 (f1 c_4 c_0)) )(or (not (p2 c_1)) (not (p2 c_0)) (p4 (f1 c_0 c_1)) (p3 (f1 c_0 c_1)) )(or (not (p2 c_1)) (not (p2 c_1)) (p4 (f1 c_1 c_1)) (p3 (f1 c_1 c_1)) )(or (not (p2 c_1)) (not (p2 c_2)) (p4 (f1 c_2 c_1)) (p3 (f1 c_2 c_1)) )(or (not (p2 c_1)) (not (p2 c_3)) (p4 (f1 c_3 c_1)) (p3 (f1 c_3 c_1)) )(or (not (p2 c_1)) (not (p2 c_4)) (p4 (f1 c_4 c_1)) (p3 (f1 c_4 c_1)) )(or (not (p2 c_2)) (not (p2 c_0)) (p4 (f1 c_0 c_2)) (p3 (f1 c_0 c_2)) )(or (not (p2 c_2)) (not (p2 c_1)) (p4 (f1 c_1 c_2)) (p3 (f1 c_1 c_2)) )(or (not (p2 c_2)) (not (p2 c_2)) (p4 (f1 c_2 c_2)) (p3 (f1 c_2 c_2)) )(or (not (p2 c_2)) (not (p2 c_3)) (p4 (f1 c_3 c_2)) (p3 (f1 c_3 c_2)) )(or (not (p2 c_2)) (not (p2 c_4)) (p4 (f1 c_4 c_2)) (p3 (f1 c_4 c_2)) )(or (not (p2 c_3)) (not (p2 c_0)) (p4 (f1 c_0 c_3)) (p3 (f1 c_0 c_3)) )(or (not (p2 c_3)) (not (p2 c_1)) (p4 (f1 c_1 c_3)) (p3 (f1 c_1 c_3)) )(or (not (p2 c_3)) (not (p2 c_2)) (p4 (f1 c_2 c_3)) (p3 (f1 c_2 c_3)) )(or (not (p2 c_3)) (not (p2 c_3)) (p4 (f1 c_3 c_3)) (p3 (f1 c_3 c_3)) )(or (not (p2 c_3)) (not (p2 c_4)) (p4 (f1 c_4 c_3)) (p3 (f1 c_4 c_3)) )(or (not (p2 c_4)) (not (p2 c_0)) (p4 (f1 c_0 c_4)) (p3 (f1 c_0 c_4)) )(or (not (p2 c_4)) (not (p2 c_1)) (p4 (f1 c_1 c_4)) (p3 (f1 c_1 c_4)) )(or (not (p2 c_4)) (not (p2 c_2)) (p4 (f1 c_2 c_4)) (p3 (f1 c_2 c_4)) )(or (not (p2 c_4)) (not (p2 c_3)) (p4 (f1 c_3 c_4)) (p3 (f1 c_3 c_4)) )(or (not (p2 c_4)) (not (p2 c_4)) (p4 (f1 c_4 c_4)) (p3 (f1 c_4 c_4)) )(or (not (p2 c_0)) (not (p3 c_0)) )(or (not (p2 c_1)) (not (p3 c_1)) )(or (not (p2 c_2)) (not (p3 c_2)) )(or (not (p2 c_3)) (not (p3 c_3)) )(or (not (p2 c_4)) (not (p3 c_4)) )(or (p4 c_0) (p3 c_0) (p2 c_0) )(or (p4 c_1) (p3 c_1) (p2 c_1) )(or (p4 c_2) (p3 c_2) (p2 c_2) )(or (p4 c_3) (p3 c_3) (p2 c_3) )(or (p4 c_4) (p3 c_4) (p2 c_4) )(p3 c6) (p2 c5) (or (not (p4 c_0)) (not (p4 c_0)) (p2 (f1 c_0 c_0)) )(or (not (p4 c_0)) (not (p4 c_1)) (p2 (f1 c_1 c_0)) )(or (not (p4 c_0)) (not (p4 c_2)) (p2 (f1 c_2 c_0)) )(or (not (p4 c_0)) (not (p4 c_3)) (p2 (f1 c_3 c_0)) )(or (not (p4 c_0)) (not (p4 c_4)) (p2 (f1 c_4 c_0)) )(or (not (p4 c_1)) (not (p4 c_0)) (p2 (f1 c_0 c_1)) )(or (not (p4 c_1)) (not (p4 c_1)) (p2 (f1 c_1 c_1)) )(or (not (p4 c_1)) (not (p4 c_2)) (p2 (f1 c_2 c_1)) )(or (not (p4 c_1)) (not (p4 c_3)) (p2 (f1 c_3 c_1)) )(or (not (p4 c_1)) (not (p4 c_4)) (p2 (f1 c_4 c_1)) )(or (not (p4 c_2)) (not (p4 c_0)) (p2 (f1 c_0 c_2)) )(or (not (p4 c_2)) (not (p4 c_1)) (p2 (f1 c_1 c_2)) )(or (not (p4 c_2)) (not (p4 c_2)) (p2 (f1 c_2 c_2)) )(or (not (p4 c_2)) (not (p4 c_3)) (p2 (f1 c_3 c_2)) )(or (not (p4 c_2)) (not (p4 c_4)) (p2 (f1 c_4 c_2)) )(or (not (p4 c_3)) (not (p4 c_0)) (p2 (f1 c_0 c_3)) )(or (not (p4 c_3)) (not (p4 c_1)) (p2 (f1 c_1 c_3)) )(or (not (p4 c_3)) (not (p4 c_2)) (p2 (f1 c_2 c_3)) )(or (not (p4 c_3)) (not (p4 c_3)) (p2 (f1 c_3 c_3)) )(or (not (p4 c_3)) (not (p4 c_4)) (p2 (f1 c_4 c_3)) )(or (not (p4 c_4)) (not (p4 c_0)) (p2 (f1 c_0 c_4)) )(or (not (p4 c_4)) (not (p4 c_1)) (p2 (f1 c_1 c_4)) )(or (not (p4 c_4)) (not (p4 c_2)) (p2 (f1 c_2 c_4)) )(or (not (p4 c_4)) (not (p4 c_3)) (p2 (f1 c_3 c_4)) )(or (not (p4 c_4)) (not (p4 c_4)) (p2 (f1 c_4 c_4)) )(= (f1 c_0 (f1 c_0 c_0)) (f1 (f1 c_0 c_0) c_0)) (= (f1 c_0 (f1 c_0 c_1)) (f1 (f1 c_0 c_0) c_1)) (= (f1 c_0 (f1 c_0 c_2)) (f1 (f1 c_0 c_0) c_2)) (= (f1 c_0 (f1 c_0 c_3)) (f1 (f1 c_0 c_0) c_3)) (= (f1 c_0 (f1 c_0 c_4)) (f1 (f1 c_0 c_0) c_4)) (= (f1 c_0 (f1 c_1 c_0)) (f1 (f1 c_0 c_1) c_0)) (= (f1 c_0 (f1 c_1 c_1)) (f1 (f1 c_0 c_1) c_1)) (= (f1 c_0 (f1 c_1 c_2)) (f1 (f1 c_0 c_1) c_2)) (= (f1 c_0 (f1 c_1 c_3)) (f1 (f1 c_0 c_1) c_3)) (= (f1 c_0 (f1 c_1 c_4)) (f1 (f1 c_0 c_1) c_4)) (= (f1 c_0 (f1 c_2 c_0)) (f1 (f1 c_0 c_2) c_0)) (= (f1 c_0 (f1 c_2 c_1)) (f1 (f1 c_0 c_2) c_1)) (= (f1 c_0 (f1 c_2 c_2)) (f1 (f1 c_0 c_2) c_2)) (= (f1 c_0 (f1 c_2 c_3)) (f1 (f1 c_0 c_2) c_3)) (= (f1 c_0 (f1 c_2 c_4)) (f1 (f1 c_0 c_2) c_4)) (= (f1 c_0 (f1 c_3 c_0)) (f1 (f1 c_0 c_3) c_0)) (= (f1 c_0 (f1 c_3 c_1)) (f1 (f1 c_0 c_3) c_1)) (= (f1 c_0 (f1 c_3 c_2)) (f1 (f1 c_0 c_3) c_2)) (= (f1 c_0 (f1 c_3 c_3)) (f1 (f1 c_0 c_3) c_3)) (= (f1 c_0 (f1 c_3 c_4)) (f1 (f1 c_0 c_3) c_4)) (= (f1 c_0 (f1 c_4 c_0)) (f1 (f1 c_0 c_4) c_0)) (= (f1 c_0 (f1 c_4 c_1)) (f1 (f1 c_0 c_4) c_1)) (= (f1 c_0 (f1 c_4 c_2)) (f1 (f1 c_0 c_4) c_2)) (= (f1 c_0 (f1 c_4 c_3)) (f1 (f1 c_0 c_4) c_3)) (= (f1 c_0 (f1 c_4 c_4)) (f1 (f1 c_0 c_4) c_4)) (= (f1 c_1 (f1 c_0 c_0)) (f1 (f1 c_1 c_0) c_0)) (= (f1 c_1 (f1 c_0 c_1)) (f1 (f1 c_1 c_0) c_1)) (= (f1 c_1 (f1 c_0 c_2)) (f1 (f1 c_1 c_0) c_2)) (= (f1 c_1 (f1 c_0 c_3)) (f1 (f1 c_1 c_0) c_3)) (= (f1 c_1 (f1 c_0 c_4)) (f1 (f1 c_1 c_0) c_4)) (= (f1 c_1 (f1 c_1 c_0)) (f1 (f1 c_1 c_1) c_0)) (= (f1 c_1 (f1 c_1 c_1)) (f1 (f1 c_1 c_1) c_1)) (= (f1 c_1 (f1 c_1 c_2)) (f1 (f1 c_1 c_1) c_2)) (= (f1 c_1 (f1 c_1 c_3)) (f1 (f1 c_1 c_1) c_3)) (= (f1 c_1 (f1 c_1 c_4)) (f1 (f1 c_1 c_1) c_4)) (= (f1 c_1 (f1 c_2 c_0)) (f1 (f1 c_1 c_2) c_0)) (= (f1 c_1 (f1 c_2 c_1)) (f1 (f1 c_1 c_2) c_1)) (= (f1 c_1 (f1 c_2 c_2)) (f1 (f1 c_1 c_2) c_2)) (= (f1 c_1 (f1 c_2 c_3)) (f1 (f1 c_1 c_2) c_3)) (= (f1 c_1 (f1 c_2 c_4)) (f1 (f1 c_1 c_2) c_4)) (= (f1 c_1 (f1 c_3 c_0)) (f1 (f1 c_1 c_3) c_0)) (= (f1 c_1 (f1 c_3 c_1)) (f1 (f1 c_1 c_3) c_1)) (= (f1 c_1 (f1 c_3 c_2)) (f1 (f1 c_1 c_3) c_2)) (= (f1 c_1 (f1 c_3 c_3)) (f1 (f1 c_1 c_3) c_3)) (= (f1 c_1 (f1 c_3 c_4)) (f1 (f1 c_1 c_3) c_4)) (= (f1 c_1 (f1 c_4 c_0)) (f1 (f1 c_1 c_4) c_0)) (= (f1 c_1 (f1 c_4 c_1)) (f1 (f1 c_1 c_4) c_1)) (= (f1 c_1 (f1 c_4 c_2)) (f1 (f1 c_1 c_4) c_2)) (= (f1 c_1 (f1 c_4 c_3)) (f1 (f1 c_1 c_4) c_3)) (= (f1 c_1 (f1 c_4 c_4)) (f1 (f1 c_1 c_4) c_4)) (= (f1 c_2 (f1 c_0 c_0)) (f1 (f1 c_2 c_0) c_0)) (= (f1 c_2 (f1 c_0 c_1)) (f1 (f1 c_2 c_0) c_1)) (= (f1 c_2 (f1 c_0 c_2)) (f1 (f1 c_2 c_0) c_2)) (= (f1 c_2 (f1 c_0 c_3)) (f1 (f1 c_2 c_0) c_3)) (= (f1 c_2 (f1 c_0 c_4)) (f1 (f1 c_2 c_0) c_4)) (= (f1 c_2 (f1 c_1 c_0)) (f1 (f1 c_2 c_1) c_0)) (= (f1 c_2 (f1 c_1 c_1)) (f1 (f1 c_2 c_1) c_1)) (= (f1 c_2 (f1 c_1 c_2)) (f1 (f1 c_2 c_1) c_2)) (= (f1 c_2 (f1 c_1 c_3)) (f1 (f1 c_2 c_1) c_3)) (= (f1 c_2 (f1 c_1 c_4)) (f1 (f1 c_2 c_1) c_4)) (= (f1 c_2 (f1 c_2 c_0)) (f1 (f1 c_2 c_2) c_0)) (= (f1 c_2 (f1 c_2 c_1)) (f1 (f1 c_2 c_2) c_1)) (= (f1 c_2 (f1 c_2 c_2)) (f1 (f1 c_2 c_2) c_2)) (= (f1 c_2 (f1 c_2 c_3)) (f1 (f1 c_2 c_2) c_3)) (= (f1 c_2 (f1 c_2 c_4)) (f1 (f1 c_2 c_2) c_4)) (= (f1 c_2 (f1 c_3 c_0)) (f1 (f1 c_2 c_3) c_0)) (= (f1 c_2 (f1 c_3 c_1)) (f1 (f1 c_2 c_3) c_1)) (= (f1 c_2 (f1 c_3 c_2)) (f1 (f1 c_2 c_3) c_2)) (= (f1 c_2 (f1 c_3 c_3)) (f1 (f1 c_2 c_3) c_3)) (= (f1 c_2 (f1 c_3 c_4)) (f1 (f1 c_2 c_3) c_4)) (= (f1 c_2 (f1 c_4 c_0)) (f1 (f1 c_2 c_4) c_0)) (= (f1 c_2 (f1 c_4 c_1)) (f1 (f1 c_2 c_4) c_1)) (= (f1 c_2 (f1 c_4 c_2)) (f1 (f1 c_2 c_4) c_2)) (= (f1 c_2 (f1 c_4 c_3)) (f1 (f1 c_2 c_4) c_3)) (= (f1 c_2 (f1 c_4 c_4)) (f1 (f1 c_2 c_4) c_4)) (= (f1 c_3 (f1 c_0 c_0)) (f1 (f1 c_3 c_0) c_0)) (= (f1 c_3 (f1 c_0 c_1)) (f1 (f1 c_3 c_0) c_1)) (= (f1 c_3 (f1 c_0 c_2)) (f1 (f1 c_3 c_0) c_2)) (= (f1 c_3 (f1 c_0 c_3)) (f1 (f1 c_3 c_0) c_3)) (= (f1 c_3 (f1 c_0 c_4)) (f1 (f1 c_3 c_0) c_4)) (= (f1 c_3 (f1 c_1 c_0)) (f1 (f1 c_3 c_1) c_0)) (= (f1 c_3 (f1 c_1 c_1)) (f1 (f1 c_3 c_1) c_1)) (= (f1 c_3 (f1 c_1 c_2)) (f1 (f1 c_3 c_1) c_2)) (= (f1 c_3 (f1 c_1 c_3)) (f1 (f1 c_3 c_1) c_3)) (= (f1 c_3 (f1 c_1 c_4)) (f1 (f1 c_3 c_1) c_4)) (= (f1 c_3 (f1 c_2 c_0)) (f1 (f1 c_3 c_2) c_0)) (= (f1 c_3 (f1 c_2 c_1)) (f1 (f1 c_3 c_2) c_1)) (= (f1 c_3 (f1 c_2 c_2)) (f1 (f1 c_3 c_2) c_2)) (= (f1 c_3 (f1 c_2 c_3)) (f1 (f1 c_3 c_2) c_3)) (= (f1 c_3 (f1 c_2 c_4)) (f1 (f1 c_3 c_2) c_4)) (= (f1 c_3 (f1 c_3 c_0)) (f1 (f1 c_3 c_3) c_0)) (= (f1 c_3 (f1 c_3 c_1)) (f1 (f1 c_3 c_3) c_1)) (= (f1 c_3 (f1 c_3 c_2)) (f1 (f1 c_3 c_3) c_2)) (= (f1 c_3 (f1 c_3 c_3)) (f1 (f1 c_3 c_3) c_3)) (= (f1 c_3 (f1 c_3 c_4)) (f1 (f1 c_3 c_3) c_4)) (= (f1 c_3 (f1 c_4 c_0)) (f1 (f1 c_3 c_4) c_0)) (= (f1 c_3 (f1 c_4 c_1)) (f1 (f1 c_3 c_4) c_1)) (= (f1 c_3 (f1 c_4 c_2)) (f1 (f1 c_3 c_4) c_2)) (= (f1 c_3 (f1 c_4 c_3)) (f1 (f1 c_3 c_4) c_3)) (= (f1 c_3 (f1 c_4 c_4)) (f1 (f1 c_3 c_4) c_4)) (= (f1 c_4 (f1 c_0 c_0)) (f1 (f1 c_4 c_0) c_0)) (= (f1 c_4 (f1 c_0 c_1)) (f1 (f1 c_4 c_0) c_1)) (= (f1 c_4 (f1 c_0 c_2)) (f1 (f1 c_4 c_0) c_2)) (= (f1 c_4 (f1 c_0 c_3)) (f1 (f1 c_4 c_0) c_3)) (= (f1 c_4 (f1 c_0 c_4)) (f1 (f1 c_4 c_0) c_4)) (= (f1 c_4 (f1 c_1 c_0)) (f1 (f1 c_4 c_1) c_0)) (= (f1 c_4 (f1 c_1 c_1)) (f1 (f1 c_4 c_1) c_1)) (= (f1 c_4 (f1 c_1 c_2)) (f1 (f1 c_4 c_1) c_2)) (= (f1 c_4 (f1 c_1 c_3)) (f1 (f1 c_4 c_1) c_3)) (= (f1 c_4 (f1 c_1 c_4)) (f1 (f1 c_4 c_1) c_4)) (= (f1 c_4 (f1 c_2 c_0)) (f1 (f1 c_4 c_2) c_0)) (= (f1 c_4 (f1 c_2 c_1)) (f1 (f1 c_4 c_2) c_1)) (= (f1 c_4 (f1 c_2 c_2)) (f1 (f1 c_4 c_2) c_2)) (= (f1 c_4 (f1 c_2 c_3)) (f1 (f1 c_4 c_2) c_3)) (= (f1 c_4 (f1 c_2 c_4)) (f1 (f1 c_4 c_2) c_4)) (= (f1 c_4 (f1 c_3 c_0)) (f1 (f1 c_4 c_3) c_0)) (= (f1 c_4 (f1 c_3 c_1)) (f1 (f1 c_4 c_3) c_1)) (= (f1 c_4 (f1 c_3 c_2)) (f1 (f1 c_4 c_3) c_2)) (= (f1 c_4 (f1 c_3 c_3)) (f1 (f1 c_4 c_3) c_3)) (= (f1 c_4 (f1 c_3 c_4)) (f1 (f1 c_4 c_3) c_4)) (= (f1 c_4 (f1 c_4 c_0)) (f1 (f1 c_4 c_4) c_0)) (= (f1 c_4 (f1 c_4 c_1)) (f1 (f1 c_4 c_4) c_1)) (= (f1 c_4 (f1 c_4 c_2)) (f1 (f1 c_4 c_4) c_2)) (= (f1 c_4 (f1 c_4 c_3)) (f1 (f1 c_4 c_4) c_3)) (= (f1 c_4 (f1 c_4 c_4)) (f1 (f1 c_4 c_4) c_4)) (or (p2 (f1 c_0 c_0)) (not (p3 c_0)) (not (p3 c_0)) )(or (p2 (f1 c_0 c_1)) (not (p3 c_0)) (not (p3 c_1)) )(or (p2 (f1 c_0 c_2)) (not (p3 c_0)) (not (p3 c_2)) )(or (p2 (f1 c_0 c_3)) (not (p3 c_0)) (not (p3 c_3)) )(or (p2 (f1 c_0 c_4)) (not (p3 c_0)) (not (p3 c_4)) )(or (p2 (f1 c_1 c_0)) (not (p3 c_1)) (not (p3 c_0)) )(or (p2 (f1 c_1 c_1)) (not (p3 c_1)) (not (p3 c_1)) )(or (p2 (f1 c_1 c_2)) (not (p3 c_1)) (not (p3 c_2)) )(or (p2 (f1 c_1 c_3)) (not (p3 c_1)) (not (p3 c_3)) )(or (p2 (f1 c_1 c_4)) (not (p3 c_1)) (not (p3 c_4)) )(or (p2 (f1 c_2 c_0)) (not (p3 c_2)) (not (p3 c_0)) )(or (p2 (f1 c_2 c_1)) (not (p3 c_2)) (not (p3 c_1)) )(or (p2 (f1 c_2 c_2)) (not (p3 c_2)) (not (p3 c_2)) )(or (p2 (f1 c_2 c_3)) (not (p3 c_2)) (not (p3 c_3)) )(or (p2 (f1 c_2 c_4)) (not (p3 c_2)) (not (p3 c_4)) )(or (p2 (f1 c_3 c_0)) (not (p3 c_3)) (not (p3 c_0)) )(or (p2 (f1 c_3 c_1)) (not (p3 c_3)) (not (p3 c_1)) )(or (p2 (f1 c_3 c_2)) (not (p3 c_3)) (not (p3 c_2)) )(or (p2 (f1 c_3 c_3)) (not (p3 c_3)) (not (p3 c_3)) )(or (p2 (f1 c_3 c_4)) (not (p3 c_3)) (not (p3 c_4)) )(or (p2 (f1 c_4 c_0)) (not (p3 c_4)) (not (p3 c_0)) )(or (p2 (f1 c_4 c_1)) (not (p3 c_4)) (not (p3 c_1)) )(or (p2 (f1 c_4 c_2)) (not (p3 c_4)) (not (p3 c_2)) )(or (p2 (f1 c_4 c_3)) (not (p3 c_4)) (not (p3 c_3)) )(or (p2 (f1 c_4 c_4)) (not (p3 c_4)) (not (p3 c_4)) )(p4 c7) (or (not (p4 c_0)) (not (p2 c_0)) )(or (not (p4 c_1)) (not (p2 c_1)) )(or (not (p4 c_2)) (not (p2 c_2)) )(or (not (p4 c_3)) (not (p2 c_3)) )(or (not (p4 c_4)) (not (p2 c_4)) )(or (not (p3 c_0)) (not (p4 c_0)) )(or (not (p3 c_1)) (not (p4 c_1)) )(or (not (p3 c_2)) (not (p4 c_2)) )(or (not (p3 c_3)) (not (p4 c_3)) )(or (not (p3 c_4)) (not (p4 c_4)) )(or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2)(= (f1 c_0 c_0) c_3)(= (f1 c_0 c_0) c_4))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2)(= (f1 c_0 c_1) c_3)(= (f1 c_0 c_1) c_4))(or (= (f1 c_0 c_2) c_0)(= (f1 c_0 c_2) c_1)(= (f1 c_0 c_2) c_2)(= (f1 c_0 c_2) c_3)(= (f1 c_0 c_2) c_4))(or (= (f1 c_0 c_3) c_0)(= (f1 c_0 c_3) c_1)(= (f1 c_0 c_3) c_2)(= (f1 c_0 c_3) c_3)(= (f1 c_0 c_3) c_4))(or (= (f1 c_0 c_4) c_0)(= (f1 c_0 c_4) c_1)(= (f1 c_0 c_4) c_2)(= (f1 c_0 c_4) c_3)(= (f1 c_0 c_4) c_4))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2)(= (f1 c_1 c_0) c_3)(= (f1 c_1 c_0) c_4))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2)(= (f1 c_1 c_1) c_3)(= (f1 c_1 c_1) c_4))(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2)(= (f1 c_1 c_2) c_3)(= (f1 c_1 c_2) c_4))(or (= (f1 c_1 c_3) c_0)(= (f1 c_1 c_3) c_1)(= (f1 c_1 c_3) c_2)(= (f1 c_1 c_3) c_3)(= (f1 c_1 c_3) c_4))(or (= (f1 c_1 c_4) c_0)(= (f1 c_1 c_4) c_1)(= (f1 c_1 c_4) c_2)(= (f1 c_1 c_4) c_3)(= (f1 c_1 c_4) c_4))(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2)(= (f1 c_2 c_0) c_3)(= (f1 c_2 c_0) c_4))(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2)(= (f1 c_2 c_1) c_3)(= (f1 c_2 c_1) c_4))(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2)(= (f1 c_2 c_2) c_3)(= (f1 c_2 c_2) c_4))(or (= (f1 c_2 c_3) c_0)(= (f1 c_2 c_3) c_1)(= (f1 c_2 c_3) c_2)(= (f1 c_2 c_3) c_3)(= (f1 c_2 c_3) c_4))(or (= (f1 c_2 c_4) c_0)(= (f1 c_2 c_4) c_1)(= (f1 c_2 c_4) c_2)(= (f1 c_2 c_4) c_3)(= (f1 c_2 c_4) c_4))(or (= (f1 c_3 c_0) c_0)(= (f1 c_3 c_0) c_1)(= (f1 c_3 c_0) c_2)(= (f1 c_3 c_0) c_3)(= (f1 c_3 c_0) c_4))(or (= (f1 c_3 c_1) c_0)(= (f1 c_3 c_1) c_1)(= (f1 c_3 c_1) c_2)(= (f1 c_3 c_1) c_3)(= (f1 c_3 c_1) c_4))(or (= (f1 c_3 c_2) c_0)(= (f1 c_3 c_2) c_1)(= (f1 c_3 c_2) c_2)(= (f1 c_3 c_2) c_3)(= (f1 c_3 c_2) c_4))(or (= (f1 c_3 c_3) c_0)(= (f1 c_3 c_3) c_1)(= (f1 c_3 c_3) c_2)(= (f1 c_3 c_3) c_3)(= (f1 c_3 c_3) c_4))(or (= (f1 c_3 c_4) c_0)(= (f1 c_3 c_4) c_1)(= (f1 c_3 c_4) c_2)(= (f1 c_3 c_4) c_3)(= (f1 c_3 c_4) c_4))(or (= (f1 c_4 c_0) c_0)(= (f1 c_4 c_0) c_1)(= (f1 c_4 c_0) c_2)(= (f1 c_4 c_0) c_3)(= (f1 c_4 c_0) c_4))(or (= (f1 c_4 c_1) c_0)(= (f1 c_4 c_1) c_1)(= (f1 c_4 c_1) c_2)(= (f1 c_4 c_1) c_3)(= (f1 c_4 c_1) c_4))(or (= (f1 c_4 c_2) c_0)(= (f1 c_4 c_2) c_1)(= (f1 c_4 c_2) c_2)(= (f1 c_4 c_2) c_3)(= (f1 c_4 c_2) c_4))(or (= (f1 c_4 c_3) c_0)(= (f1 c_4 c_3) c_1)(= (f1 c_4 c_3) c_2)(= (f1 c_4 c_3) c_3)(= (f1 c_4 c_3) c_4))(or (= (f1 c_4 c_4) c_0)(= (f1 c_4 c_4) c_1)(= (f1 c_4 c_4) c_2)(= (f1 c_4 c_4) c_3)(= (f1 c_4 c_4) c_4))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3)(= c6 c_4))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3)(= c5 c_4))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3)(= c7 c_4)))) diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 744ec5775..fca3c4ef8 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -10,7 +10,8 @@ TESTS = bug143.smt \ C880mul.miter.shuffled-as.sat03-348.smt \ comb2.shuffled-as.sat03-420.smt \ hole10.cvc \ - instance_1151.smt + instance_1151.smt \ + NEQ016_size5.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress3/NEQ016_size5.smt b/test/regress/regress3/NEQ016_size5.smt new file mode 100644 index 000000000..ec56385f6 --- /dev/null +++ b/test/regress/regress3/NEQ016_size5.smt @@ -0,0 +1,27 @@ +(benchmark NEQ016_size5.smt +:source { +CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC + for more information. + +This benchmark was obtained by trying to find a finite model of a first-order +formula (Albert Oliveras). +} +:status unsat +:category { crafted } +:difficulty { 0 } +:logic QF_UF +:extrapreds ((p2 U)) +:extrafuns ((f1 U U U)) +:extrapreds ((p4 U)) +:extrapreds ((p3 U)) +:extrafuns ((c6 U)) +:extrafuns ((c5 U)) +:extrafuns ((c7 U)) +:extrafuns ((c_0 U)) +:extrafuns ((c_1 U)) +:extrafuns ((c_2 U)) +:extrafuns ((c_3 U)) +:extrafuns ((c_4 U)) +:formula +( and +( distinct c_0 c_1 c_2 c_3 c_4 )(or (not (p2 c_0)) (not (p2 c_0)) (p4 (f1 c_0 c_0)) (p3 (f1 c_0 c_0)) )(or (not (p2 c_0)) (not (p2 c_1)) (p4 (f1 c_1 c_0)) (p3 (f1 c_1 c_0)) )(or (not (p2 c_0)) (not (p2 c_2)) (p4 (f1 c_2 c_0)) (p3 (f1 c_2 c_0)) )(or (not (p2 c_0)) (not (p2 c_3)) (p4 (f1 c_3 c_0)) (p3 (f1 c_3 c_0)) )(or (not (p2 c_0)) (not (p2 c_4)) (p4 (f1 c_4 c_0)) (p3 (f1 c_4 c_0)) )(or (not (p2 c_1)) (not (p2 c_0)) (p4 (f1 c_0 c_1)) (p3 (f1 c_0 c_1)) )(or (not (p2 c_1)) (not (p2 c_1)) (p4 (f1 c_1 c_1)) (p3 (f1 c_1 c_1)) )(or (not (p2 c_1)) (not (p2 c_2)) (p4 (f1 c_2 c_1)) (p3 (f1 c_2 c_1)) )(or (not (p2 c_1)) (not (p2 c_3)) (p4 (f1 c_3 c_1)) (p3 (f1 c_3 c_1)) )(or (not (p2 c_1)) (not (p2 c_4)) (p4 (f1 c_4 c_1)) (p3 (f1 c_4 c_1)) )(or (not (p2 c_2)) (not (p2 c_0)) (p4 (f1 c_0 c_2)) (p3 (f1 c_0 c_2)) )(or (not (p2 c_2)) (not (p2 c_1)) (p4 (f1 c_1 c_2)) (p3 (f1 c_1 c_2)) )(or (not (p2 c_2)) (not (p2 c_2)) (p4 (f1 c_2 c_2)) (p3 (f1 c_2 c_2)) )(or (not (p2 c_2)) (not (p2 c_3)) (p4 (f1 c_3 c_2)) (p3 (f1 c_3 c_2)) )(or (not (p2 c_2)) (not (p2 c_4)) (p4 (f1 c_4 c_2)) (p3 (f1 c_4 c_2)) )(or (not (p2 c_3)) (not (p2 c_0)) (p4 (f1 c_0 c_3)) (p3 (f1 c_0 c_3)) )(or (not (p2 c_3)) (not (p2 c_1)) (p4 (f1 c_1 c_3)) (p3 (f1 c_1 c_3)) )(or (not (p2 c_3)) (not (p2 c_2)) (p4 (f1 c_2 c_3)) (p3 (f1 c_2 c_3)) )(or (not (p2 c_3)) (not (p2 c_3)) (p4 (f1 c_3 c_3)) (p3 (f1 c_3 c_3)) )(or (not (p2 c_3)) (not (p2 c_4)) (p4 (f1 c_4 c_3)) (p3 (f1 c_4 c_3)) )(or (not (p2 c_4)) (not (p2 c_0)) (p4 (f1 c_0 c_4)) (p3 (f1 c_0 c_4)) )(or (not (p2 c_4)) (not (p2 c_1)) (p4 (f1 c_1 c_4)) (p3 (f1 c_1 c_4)) )(or (not (p2 c_4)) (not (p2 c_2)) (p4 (f1 c_2 c_4)) (p3 (f1 c_2 c_4)) )(or (not (p2 c_4)) (not (p2 c_3)) (p4 (f1 c_3 c_4)) (p3 (f1 c_3 c_4)) )(or (not (p2 c_4)) (not (p2 c_4)) (p4 (f1 c_4 c_4)) (p3 (f1 c_4 c_4)) )(or (not (p2 c_0)) (not (p3 c_0)) )(or (not (p2 c_1)) (not (p3 c_1)) )(or (not (p2 c_2)) (not (p3 c_2)) )(or (not (p2 c_3)) (not (p3 c_3)) )(or (not (p2 c_4)) (not (p3 c_4)) )(or (p4 c_0) (p3 c_0) (p2 c_0) )(or (p4 c_1) (p3 c_1) (p2 c_1) )(or (p4 c_2) (p3 c_2) (p2 c_2) )(or (p4 c_3) (p3 c_3) (p2 c_3) )(or (p4 c_4) (p3 c_4) (p2 c_4) )(p3 c6) (p2 c5) (or (not (p4 c_0)) (not (p4 c_0)) (p2 (f1 c_0 c_0)) )(or (not (p4 c_0)) (not (p4 c_1)) (p2 (f1 c_1 c_0)) )(or (not (p4 c_0)) (not (p4 c_2)) (p2 (f1 c_2 c_0)) )(or (not (p4 c_0)) (not (p4 c_3)) (p2 (f1 c_3 c_0)) )(or (not (p4 c_0)) (not (p4 c_4)) (p2 (f1 c_4 c_0)) )(or (not (p4 c_1)) (not (p4 c_0)) (p2 (f1 c_0 c_1)) )(or (not (p4 c_1)) (not (p4 c_1)) (p2 (f1 c_1 c_1)) )(or (not (p4 c_1)) (not (p4 c_2)) (p2 (f1 c_2 c_1)) )(or (not (p4 c_1)) (not (p4 c_3)) (p2 (f1 c_3 c_1)) )(or (not (p4 c_1)) (not (p4 c_4)) (p2 (f1 c_4 c_1)) )(or (not (p4 c_2)) (not (p4 c_0)) (p2 (f1 c_0 c_2)) )(or (not (p4 c_2)) (not (p4 c_1)) (p2 (f1 c_1 c_2)) )(or (not (p4 c_2)) (not (p4 c_2)) (p2 (f1 c_2 c_2)) )(or (not (p4 c_2)) (not (p4 c_3)) (p2 (f1 c_3 c_2)) )(or (not (p4 c_2)) (not (p4 c_4)) (p2 (f1 c_4 c_2)) )(or (not (p4 c_3)) (not (p4 c_0)) (p2 (f1 c_0 c_3)) )(or (not (p4 c_3)) (not (p4 c_1)) (p2 (f1 c_1 c_3)) )(or (not (p4 c_3)) (not (p4 c_2)) (p2 (f1 c_2 c_3)) )(or (not (p4 c_3)) (not (p4 c_3)) (p2 (f1 c_3 c_3)) )(or (not (p4 c_3)) (not (p4 c_4)) (p2 (f1 c_4 c_3)) )(or (not (p4 c_4)) (not (p4 c_0)) (p2 (f1 c_0 c_4)) )(or (not (p4 c_4)) (not (p4 c_1)) (p2 (f1 c_1 c_4)) )(or (not (p4 c_4)) (not (p4 c_2)) (p2 (f1 c_2 c_4)) )(or (not (p4 c_4)) (not (p4 c_3)) (p2 (f1 c_3 c_4)) )(or (not (p4 c_4)) (not (p4 c_4)) (p2 (f1 c_4 c_4)) )(= (f1 c_0 (f1 c_0 c_0)) (f1 (f1 c_0 c_0) c_0)) (= (f1 c_0 (f1 c_0 c_1)) (f1 (f1 c_0 c_0) c_1)) (= (f1 c_0 (f1 c_0 c_2)) (f1 (f1 c_0 c_0) c_2)) (= (f1 c_0 (f1 c_0 c_3)) (f1 (f1 c_0 c_0) c_3)) (= (f1 c_0 (f1 c_0 c_4)) (f1 (f1 c_0 c_0) c_4)) (= (f1 c_0 (f1 c_1 c_0)) (f1 (f1 c_0 c_1) c_0)) (= (f1 c_0 (f1 c_1 c_1)) (f1 (f1 c_0 c_1) c_1)) (= (f1 c_0 (f1 c_1 c_2)) (f1 (f1 c_0 c_1) c_2)) (= (f1 c_0 (f1 c_1 c_3)) (f1 (f1 c_0 c_1) c_3)) (= (f1 c_0 (f1 c_1 c_4)) (f1 (f1 c_0 c_1) c_4)) (= (f1 c_0 (f1 c_2 c_0)) (f1 (f1 c_0 c_2) c_0)) (= (f1 c_0 (f1 c_2 c_1)) (f1 (f1 c_0 c_2) c_1)) (= (f1 c_0 (f1 c_2 c_2)) (f1 (f1 c_0 c_2) c_2)) (= (f1 c_0 (f1 c_2 c_3)) (f1 (f1 c_0 c_2) c_3)) (= (f1 c_0 (f1 c_2 c_4)) (f1 (f1 c_0 c_2) c_4)) (= (f1 c_0 (f1 c_3 c_0)) (f1 (f1 c_0 c_3) c_0)) (= (f1 c_0 (f1 c_3 c_1)) (f1 (f1 c_0 c_3) c_1)) (= (f1 c_0 (f1 c_3 c_2)) (f1 (f1 c_0 c_3) c_2)) (= (f1 c_0 (f1 c_3 c_3)) (f1 (f1 c_0 c_3) c_3)) (= (f1 c_0 (f1 c_3 c_4)) (f1 (f1 c_0 c_3) c_4)) (= (f1 c_0 (f1 c_4 c_0)) (f1 (f1 c_0 c_4) c_0)) (= (f1 c_0 (f1 c_4 c_1)) (f1 (f1 c_0 c_4) c_1)) (= (f1 c_0 (f1 c_4 c_2)) (f1 (f1 c_0 c_4) c_2)) (= (f1 c_0 (f1 c_4 c_3)) (f1 (f1 c_0 c_4) c_3)) (= (f1 c_0 (f1 c_4 c_4)) (f1 (f1 c_0 c_4) c_4)) (= (f1 c_1 (f1 c_0 c_0)) (f1 (f1 c_1 c_0) c_0)) (= (f1 c_1 (f1 c_0 c_1)) (f1 (f1 c_1 c_0) c_1)) (= (f1 c_1 (f1 c_0 c_2)) (f1 (f1 c_1 c_0) c_2)) (= (f1 c_1 (f1 c_0 c_3)) (f1 (f1 c_1 c_0) c_3)) (= (f1 c_1 (f1 c_0 c_4)) (f1 (f1 c_1 c_0) c_4)) (= (f1 c_1 (f1 c_1 c_0)) (f1 (f1 c_1 c_1) c_0)) (= (f1 c_1 (f1 c_1 c_1)) (f1 (f1 c_1 c_1) c_1)) (= (f1 c_1 (f1 c_1 c_2)) (f1 (f1 c_1 c_1) c_2)) (= (f1 c_1 (f1 c_1 c_3)) (f1 (f1 c_1 c_1) c_3)) (= (f1 c_1 (f1 c_1 c_4)) (f1 (f1 c_1 c_1) c_4)) (= (f1 c_1 (f1 c_2 c_0)) (f1 (f1 c_1 c_2) c_0)) (= (f1 c_1 (f1 c_2 c_1)) (f1 (f1 c_1 c_2) c_1)) (= (f1 c_1 (f1 c_2 c_2)) (f1 (f1 c_1 c_2) c_2)) (= (f1 c_1 (f1 c_2 c_3)) (f1 (f1 c_1 c_2) c_3)) (= (f1 c_1 (f1 c_2 c_4)) (f1 (f1 c_1 c_2) c_4)) (= (f1 c_1 (f1 c_3 c_0)) (f1 (f1 c_1 c_3) c_0)) (= (f1 c_1 (f1 c_3 c_1)) (f1 (f1 c_1 c_3) c_1)) (= (f1 c_1 (f1 c_3 c_2)) (f1 (f1 c_1 c_3) c_2)) (= (f1 c_1 (f1 c_3 c_3)) (f1 (f1 c_1 c_3) c_3)) (= (f1 c_1 (f1 c_3 c_4)) (f1 (f1 c_1 c_3) c_4)) (= (f1 c_1 (f1 c_4 c_0)) (f1 (f1 c_1 c_4) c_0)) (= (f1 c_1 (f1 c_4 c_1)) (f1 (f1 c_1 c_4) c_1)) (= (f1 c_1 (f1 c_4 c_2)) (f1 (f1 c_1 c_4) c_2)) (= (f1 c_1 (f1 c_4 c_3)) (f1 (f1 c_1 c_4) c_3)) (= (f1 c_1 (f1 c_4 c_4)) (f1 (f1 c_1 c_4) c_4)) (= (f1 c_2 (f1 c_0 c_0)) (f1 (f1 c_2 c_0) c_0)) (= (f1 c_2 (f1 c_0 c_1)) (f1 (f1 c_2 c_0) c_1)) (= (f1 c_2 (f1 c_0 c_2)) (f1 (f1 c_2 c_0) c_2)) (= (f1 c_2 (f1 c_0 c_3)) (f1 (f1 c_2 c_0) c_3)) (= (f1 c_2 (f1 c_0 c_4)) (f1 (f1 c_2 c_0) c_4)) (= (f1 c_2 (f1 c_1 c_0)) (f1 (f1 c_2 c_1) c_0)) (= (f1 c_2 (f1 c_1 c_1)) (f1 (f1 c_2 c_1) c_1)) (= (f1 c_2 (f1 c_1 c_2)) (f1 (f1 c_2 c_1) c_2)) (= (f1 c_2 (f1 c_1 c_3)) (f1 (f1 c_2 c_1) c_3)) (= (f1 c_2 (f1 c_1 c_4)) (f1 (f1 c_2 c_1) c_4)) (= (f1 c_2 (f1 c_2 c_0)) (f1 (f1 c_2 c_2) c_0)) (= (f1 c_2 (f1 c_2 c_1)) (f1 (f1 c_2 c_2) c_1)) (= (f1 c_2 (f1 c_2 c_2)) (f1 (f1 c_2 c_2) c_2)) (= (f1 c_2 (f1 c_2 c_3)) (f1 (f1 c_2 c_2) c_3)) (= (f1 c_2 (f1 c_2 c_4)) (f1 (f1 c_2 c_2) c_4)) (= (f1 c_2 (f1 c_3 c_0)) (f1 (f1 c_2 c_3) c_0)) (= (f1 c_2 (f1 c_3 c_1)) (f1 (f1 c_2 c_3) c_1)) (= (f1 c_2 (f1 c_3 c_2)) (f1 (f1 c_2 c_3) c_2)) (= (f1 c_2 (f1 c_3 c_3)) (f1 (f1 c_2 c_3) c_3)) (= (f1 c_2 (f1 c_3 c_4)) (f1 (f1 c_2 c_3) c_4)) (= (f1 c_2 (f1 c_4 c_0)) (f1 (f1 c_2 c_4) c_0)) (= (f1 c_2 (f1 c_4 c_1)) (f1 (f1 c_2 c_4) c_1)) (= (f1 c_2 (f1 c_4 c_2)) (f1 (f1 c_2 c_4) c_2)) (= (f1 c_2 (f1 c_4 c_3)) (f1 (f1 c_2 c_4) c_3)) (= (f1 c_2 (f1 c_4 c_4)) (f1 (f1 c_2 c_4) c_4)) (= (f1 c_3 (f1 c_0 c_0)) (f1 (f1 c_3 c_0) c_0)) (= (f1 c_3 (f1 c_0 c_1)) (f1 (f1 c_3 c_0) c_1)) (= (f1 c_3 (f1 c_0 c_2)) (f1 (f1 c_3 c_0) c_2)) (= (f1 c_3 (f1 c_0 c_3)) (f1 (f1 c_3 c_0) c_3)) (= (f1 c_3 (f1 c_0 c_4)) (f1 (f1 c_3 c_0) c_4)) (= (f1 c_3 (f1 c_1 c_0)) (f1 (f1 c_3 c_1) c_0)) (= (f1 c_3 (f1 c_1 c_1)) (f1 (f1 c_3 c_1) c_1)) (= (f1 c_3 (f1 c_1 c_2)) (f1 (f1 c_3 c_1) c_2)) (= (f1 c_3 (f1 c_1 c_3)) (f1 (f1 c_3 c_1) c_3)) (= (f1 c_3 (f1 c_1 c_4)) (f1 (f1 c_3 c_1) c_4)) (= (f1 c_3 (f1 c_2 c_0)) (f1 (f1 c_3 c_2) c_0)) (= (f1 c_3 (f1 c_2 c_1)) (f1 (f1 c_3 c_2) c_1)) (= (f1 c_3 (f1 c_2 c_2)) (f1 (f1 c_3 c_2) c_2)) (= (f1 c_3 (f1 c_2 c_3)) (f1 (f1 c_3 c_2) c_3)) (= (f1 c_3 (f1 c_2 c_4)) (f1 (f1 c_3 c_2) c_4)) (= (f1 c_3 (f1 c_3 c_0)) (f1 (f1 c_3 c_3) c_0)) (= (f1 c_3 (f1 c_3 c_1)) (f1 (f1 c_3 c_3) c_1)) (= (f1 c_3 (f1 c_3 c_2)) (f1 (f1 c_3 c_3) c_2)) (= (f1 c_3 (f1 c_3 c_3)) (f1 (f1 c_3 c_3) c_3)) (= (f1 c_3 (f1 c_3 c_4)) (f1 (f1 c_3 c_3) c_4)) (= (f1 c_3 (f1 c_4 c_0)) (f1 (f1 c_3 c_4) c_0)) (= (f1 c_3 (f1 c_4 c_1)) (f1 (f1 c_3 c_4) c_1)) (= (f1 c_3 (f1 c_4 c_2)) (f1 (f1 c_3 c_4) c_2)) (= (f1 c_3 (f1 c_4 c_3)) (f1 (f1 c_3 c_4) c_3)) (= (f1 c_3 (f1 c_4 c_4)) (f1 (f1 c_3 c_4) c_4)) (= (f1 c_4 (f1 c_0 c_0)) (f1 (f1 c_4 c_0) c_0)) (= (f1 c_4 (f1 c_0 c_1)) (f1 (f1 c_4 c_0) c_1)) (= (f1 c_4 (f1 c_0 c_2)) (f1 (f1 c_4 c_0) c_2)) (= (f1 c_4 (f1 c_0 c_3)) (f1 (f1 c_4 c_0) c_3)) (= (f1 c_4 (f1 c_0 c_4)) (f1 (f1 c_4 c_0) c_4)) (= (f1 c_4 (f1 c_1 c_0)) (f1 (f1 c_4 c_1) c_0)) (= (f1 c_4 (f1 c_1 c_1)) (f1 (f1 c_4 c_1) c_1)) (= (f1 c_4 (f1 c_1 c_2)) (f1 (f1 c_4 c_1) c_2)) (= (f1 c_4 (f1 c_1 c_3)) (f1 (f1 c_4 c_1) c_3)) (= (f1 c_4 (f1 c_1 c_4)) (f1 (f1 c_4 c_1) c_4)) (= (f1 c_4 (f1 c_2 c_0)) (f1 (f1 c_4 c_2) c_0)) (= (f1 c_4 (f1 c_2 c_1)) (f1 (f1 c_4 c_2) c_1)) (= (f1 c_4 (f1 c_2 c_2)) (f1 (f1 c_4 c_2) c_2)) (= (f1 c_4 (f1 c_2 c_3)) (f1 (f1 c_4 c_2) c_3)) (= (f1 c_4 (f1 c_2 c_4)) (f1 (f1 c_4 c_2) c_4)) (= (f1 c_4 (f1 c_3 c_0)) (f1 (f1 c_4 c_3) c_0)) (= (f1 c_4 (f1 c_3 c_1)) (f1 (f1 c_4 c_3) c_1)) (= (f1 c_4 (f1 c_3 c_2)) (f1 (f1 c_4 c_3) c_2)) (= (f1 c_4 (f1 c_3 c_3)) (f1 (f1 c_4 c_3) c_3)) (= (f1 c_4 (f1 c_3 c_4)) (f1 (f1 c_4 c_3) c_4)) (= (f1 c_4 (f1 c_4 c_0)) (f1 (f1 c_4 c_4) c_0)) (= (f1 c_4 (f1 c_4 c_1)) (f1 (f1 c_4 c_4) c_1)) (= (f1 c_4 (f1 c_4 c_2)) (f1 (f1 c_4 c_4) c_2)) (= (f1 c_4 (f1 c_4 c_3)) (f1 (f1 c_4 c_4) c_3)) (= (f1 c_4 (f1 c_4 c_4)) (f1 (f1 c_4 c_4) c_4)) (or (p2 (f1 c_0 c_0)) (not (p3 c_0)) (not (p3 c_0)) )(or (p2 (f1 c_0 c_1)) (not (p3 c_0)) (not (p3 c_1)) )(or (p2 (f1 c_0 c_2)) (not (p3 c_0)) (not (p3 c_2)) )(or (p2 (f1 c_0 c_3)) (not (p3 c_0)) (not (p3 c_3)) )(or (p2 (f1 c_0 c_4)) (not (p3 c_0)) (not (p3 c_4)) )(or (p2 (f1 c_1 c_0)) (not (p3 c_1)) (not (p3 c_0)) )(or (p2 (f1 c_1 c_1)) (not (p3 c_1)) (not (p3 c_1)) )(or (p2 (f1 c_1 c_2)) (not (p3 c_1)) (not (p3 c_2)) )(or (p2 (f1 c_1 c_3)) (not (p3 c_1)) (not (p3 c_3)) )(or (p2 (f1 c_1 c_4)) (not (p3 c_1)) (not (p3 c_4)) )(or (p2 (f1 c_2 c_0)) (not (p3 c_2)) (not (p3 c_0)) )(or (p2 (f1 c_2 c_1)) (not (p3 c_2)) (not (p3 c_1)) )(or (p2 (f1 c_2 c_2)) (not (p3 c_2)) (not (p3 c_2)) )(or (p2 (f1 c_2 c_3)) (not (p3 c_2)) (not (p3 c_3)) )(or (p2 (f1 c_2 c_4)) (not (p3 c_2)) (not (p3 c_4)) )(or (p2 (f1 c_3 c_0)) (not (p3 c_3)) (not (p3 c_0)) )(or (p2 (f1 c_3 c_1)) (not (p3 c_3)) (not (p3 c_1)) )(or (p2 (f1 c_3 c_2)) (not (p3 c_3)) (not (p3 c_2)) )(or (p2 (f1 c_3 c_3)) (not (p3 c_3)) (not (p3 c_3)) )(or (p2 (f1 c_3 c_4)) (not (p3 c_3)) (not (p3 c_4)) )(or (p2 (f1 c_4 c_0)) (not (p3 c_4)) (not (p3 c_0)) )(or (p2 (f1 c_4 c_1)) (not (p3 c_4)) (not (p3 c_1)) )(or (p2 (f1 c_4 c_2)) (not (p3 c_4)) (not (p3 c_2)) )(or (p2 (f1 c_4 c_3)) (not (p3 c_4)) (not (p3 c_3)) )(or (p2 (f1 c_4 c_4)) (not (p3 c_4)) (not (p3 c_4)) )(p4 c7) (or (not (p4 c_0)) (not (p2 c_0)) )(or (not (p4 c_1)) (not (p2 c_1)) )(or (not (p4 c_2)) (not (p2 c_2)) )(or (not (p4 c_3)) (not (p2 c_3)) )(or (not (p4 c_4)) (not (p2 c_4)) )(or (not (p3 c_0)) (not (p4 c_0)) )(or (not (p3 c_1)) (not (p4 c_1)) )(or (not (p3 c_2)) (not (p4 c_2)) )(or (not (p3 c_3)) (not (p4 c_3)) )(or (not (p3 c_4)) (not (p4 c_4)) )(or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2)(= (f1 c_0 c_0) c_3)(= (f1 c_0 c_0) c_4))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2)(= (f1 c_0 c_1) c_3)(= (f1 c_0 c_1) c_4))(or (= (f1 c_0 c_2) c_0)(= (f1 c_0 c_2) c_1)(= (f1 c_0 c_2) c_2)(= (f1 c_0 c_2) c_3)(= (f1 c_0 c_2) c_4))(or (= (f1 c_0 c_3) c_0)(= (f1 c_0 c_3) c_1)(= (f1 c_0 c_3) c_2)(= (f1 c_0 c_3) c_3)(= (f1 c_0 c_3) c_4))(or (= (f1 c_0 c_4) c_0)(= (f1 c_0 c_4) c_1)(= (f1 c_0 c_4) c_2)(= (f1 c_0 c_4) c_3)(= (f1 c_0 c_4) c_4))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2)(= (f1 c_1 c_0) c_3)(= (f1 c_1 c_0) c_4))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2)(= (f1 c_1 c_1) c_3)(= (f1 c_1 c_1) c_4))(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2)(= (f1 c_1 c_2) c_3)(= (f1 c_1 c_2) c_4))(or (= (f1 c_1 c_3) c_0)(= (f1 c_1 c_3) c_1)(= (f1 c_1 c_3) c_2)(= (f1 c_1 c_3) c_3)(= (f1 c_1 c_3) c_4))(or (= (f1 c_1 c_4) c_0)(= (f1 c_1 c_4) c_1)(= (f1 c_1 c_4) c_2)(= (f1 c_1 c_4) c_3)(= (f1 c_1 c_4) c_4))(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2)(= (f1 c_2 c_0) c_3)(= (f1 c_2 c_0) c_4))(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2)(= (f1 c_2 c_1) c_3)(= (f1 c_2 c_1) c_4))(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2)(= (f1 c_2 c_2) c_3)(= (f1 c_2 c_2) c_4))(or (= (f1 c_2 c_3) c_0)(= (f1 c_2 c_3) c_1)(= (f1 c_2 c_3) c_2)(= (f1 c_2 c_3) c_3)(= (f1 c_2 c_3) c_4))(or (= (f1 c_2 c_4) c_0)(= (f1 c_2 c_4) c_1)(= (f1 c_2 c_4) c_2)(= (f1 c_2 c_4) c_3)(= (f1 c_2 c_4) c_4))(or (= (f1 c_3 c_0) c_0)(= (f1 c_3 c_0) c_1)(= (f1 c_3 c_0) c_2)(= (f1 c_3 c_0) c_3)(= (f1 c_3 c_0) c_4))(or (= (f1 c_3 c_1) c_0)(= (f1 c_3 c_1) c_1)(= (f1 c_3 c_1) c_2)(= (f1 c_3 c_1) c_3)(= (f1 c_3 c_1) c_4))(or (= (f1 c_3 c_2) c_0)(= (f1 c_3 c_2) c_1)(= (f1 c_3 c_2) c_2)(= (f1 c_3 c_2) c_3)(= (f1 c_3 c_2) c_4))(or (= (f1 c_3 c_3) c_0)(= (f1 c_3 c_3) c_1)(= (f1 c_3 c_3) c_2)(= (f1 c_3 c_3) c_3)(= (f1 c_3 c_3) c_4))(or (= (f1 c_3 c_4) c_0)(= (f1 c_3 c_4) c_1)(= (f1 c_3 c_4) c_2)(= (f1 c_3 c_4) c_3)(= (f1 c_3 c_4) c_4))(or (= (f1 c_4 c_0) c_0)(= (f1 c_4 c_0) c_1)(= (f1 c_4 c_0) c_2)(= (f1 c_4 c_0) c_3)(= (f1 c_4 c_0) c_4))(or (= (f1 c_4 c_1) c_0)(= (f1 c_4 c_1) c_1)(= (f1 c_4 c_1) c_2)(= (f1 c_4 c_1) c_3)(= (f1 c_4 c_1) c_4))(or (= (f1 c_4 c_2) c_0)(= (f1 c_4 c_2) c_1)(= (f1 c_4 c_2) c_2)(= (f1 c_4 c_2) c_3)(= (f1 c_4 c_2) c_4))(or (= (f1 c_4 c_3) c_0)(= (f1 c_4 c_3) c_1)(= (f1 c_4 c_3) c_2)(= (f1 c_4 c_3) c_3)(= (f1 c_4 c_3) c_4))(or (= (f1 c_4 c_4) c_0)(= (f1 c_4 c_4) c_1)(= (f1 c_4 c_4) c_2)(= (f1 c_4 c_4) c_3)(= (f1 c_4 c_4) c_4))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3)(= c6 c_4))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3)(= c5 c_4))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3)(= c7 c_4)))) -- cgit v1.2.3