now we satlib! and verification! and testing!

.gitignore

@@ -0,0 +1,5 @@
+
+bin/
+
+.build-all.db
+

README.md

@@ -7,3 +7,12 @@ Still needs to be stress-tested. The biggest test I've given it is 20 variables,
 7 clauses.
 
 Requires C++23. Sorry guys.
+
+I'm testing it using `https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html`. If you'd
+like to do that yourself, pick your favorite test suite and extract into the
+`test/` directory, and run `make test`. The `test.py` will automatically detect
+them and test against them.
+
+
+
+

automata.cpp

@@ -56,7 +56,7 @@ struct automata* automata::new_variable(
     
     if (verbose)
     {
-        printf("%*s" "returned automata with %lu states.\n",
+        printf("%*s" "returned automata with %'lu states.\n",
             depth, "", total_number_of_states);
     }
     
@@ -95,7 +95,7 @@ void automata::dump(struct automata* start, const char* fmt, ...)
     
     set<automata*> queued;
     
-    if (queued.add(start))
+    if (start && queued.add(start))
     {
         todo.append(start);
     }
@@ -251,7 +251,7 @@ struct automata* automata::union_(
     
     if (verbose)
     {
-        printf("%*s" "returned automata with %lu states" "\n",
+        printf("%*s" "returned automata with %'lu states" "\n",
             depth, "", total_number_of_states);
     }
     
@@ -319,13 +319,156 @@ struct automata* automata::intersect(
     
     if (verbose)
     {
-        printf("%*s" "returned automata with %lu states" "\n",
+        printf("%*s" "returned automata with %'lu states" "\n",
             depth, "", total_number_of_states);
     }
     
     return start;
 }
 
+struct automata* automata::eliminate_dead_code(
+    int depth,
+    bool verbose,
+    const struct automata* original_start)
+{
+    if (verbose)
+    {
+        printf("%*s" "eliminate_dead_code():\n", depth++, "");
+    }
+    
+    set<const automata*> can_reach;
+    {
+        set<const automata*> queued;
+        
+        dict<const automata*, set<const automata*>> dep_on;
+        
+        quack<const automata*> explore_todo;
+        
+        quack<const automata*> percolate_todo;
+        
+        queued.add(original_start);
+        
+        explore_todo.append(original_start);
+        
+        if (verbose)
+        {
+            printf("%*s" "exploring ...\n", depth, "");
+        }
+        
+        while (explore_todo.n)
+        {
+            auto state = explore_todo.pop();
+            
+            if (state->is_accepting)
+            {
+                can_reach.add(state);
+                
+                percolate_todo.append(state);
+            }
+            else for (int val = 0; val < 2; val++)
+            {
+                if (auto to = state->on[val])
+                {
+                    if (!dep_on.has(to))
+                    {
+                        dep_on.add(to, set<const automata*>());
+                    }
+                    
+                    dep_on[to].add(state);
+                    
+                    if (queued.add(to))
+                    {
+                        explore_todo.append(to);
+                    }
+                }
+            }
+        }
+        
+        if (verbose)
+        {
+            printf("%*s" "percolating ...\n", depth, "");
+        }
+        
+        while (percolate_todo.n)
+        {
+            auto state = percolate_todo.pop();
+            
+            if (dep_on.has(state))
+            {
+                for (auto substate: dep_on[state])
+                {
+                    if (can_reach.add(substate))
+                    {
+                        percolate_todo.append(substate);
+                    }
+                }
+            }
+        }
+    }
+    
+    if (verbose)
+    {
+        printf("%*s" "cloning ...\n", depth, "");
+    }
+    
+	size_t total_number_of_states = 0;
+	
+	struct automata* new_start = NULL;
+	{
+        dict<const automata*, automata*> mapping;
+        
+        quack<decltype(mapping)::keyvalue_pair*> todo;
+        
+        // initial state:
+        if (can_reach.has(original_start))
+        {
+            new_start = new automata();
+            
+            total_number_of_states++;
+            
+            todo.append(mapping.add(original_start, new_start));
+        }
+        
+        while (todo.n)
+        {
+            auto [old, state] = *todo.pop();
+            
+	        state->is_accepting = old->is_accepting;
+	        
+	        for (int val = 0; val < 2; val++)
+	        {
+	            const automata* to = old->on[val];
+	            
+		        if (to && can_reach.has(to))
+		        {
+			        if (mapping.has(to))
+			        {
+			            state->on[val] = mapping[to];
+			        }
+			        else
+			        {
+                        automata* substate = new automata();
+				        
+				        total_number_of_states++;
+				        
+				        state->on[val] = substate;
+				        
+				        todo.append(mapping.add(to, substate));
+			        }
+		        }
+	        }
+        }
+	}
+	
+    if (verbose)
+    {
+        printf("%*s" "returned automata with %'lu states" "\n",
+            depth, "", total_number_of_states);
+    }
+    
+	return new_start;
+}
+
 struct automata* automata::simplify(
     int depth,
     bool verbose,
@@ -485,7 +628,7 @@ struct automata* automata::simplify(
 	
     if (verbose)
     {
-        printf("%*s" "returned automata with %lu states" "\n",
+        printf("%*s" "returned automata with %'lu states" "\n",
             depth, "", total_number_of_states);
     }
     
@@ -498,9 +641,12 @@ void automata::free(struct automata* start)
     
     quack<automata*> todo;
     
-    queued.add(start);
-    
-    todo.append(start);
+    if (start)
+    {
+        queued.add(start);
+        
+        todo.append(start);
+    }
     
     while (todo.n)
     {

automata.hpp

@@ -34,6 +34,11 @@ struct automata
             const struct automata* left,
             const struct automata* right);
         
+        static struct automata* eliminate_dead_code(
+            int depth,
+            bool verbose,
+            const struct automata* original);
+        
         static struct automata* simplify(
             int depth,
             bool verbose,

avl.hpp

@@ -556,7 +556,7 @@ template <
             ;
         }
         
-        struct avl_node_t* search(I& item) const
+        struct avl_node_t* search(const I& item) const
         {
             avl_node_t *node;
             

build_automata.cpp

@@ -17,12 +17,13 @@ automata* build_automata(
     {
         struct automata* clause_start = NULL;
         
-        depth++;
+        if (flags.verbose)
+        {
+            printf("%*s" "building clause:\n", depth++, "");
+        }
         
         for (const auto& bundle: clause->bundles)
         {
-            depth++;
-            
             unsigned index = bundle.variable - 1;
             
             struct automata* variable_start = automata::new_variable(
@@ -70,8 +71,6 @@ automata* build_automata(
             {
                 clause_start = variable_start;
             }
-            
-            depth--;
         }
         
         if (automata_start)
@@ -86,12 +85,12 @@ automata* build_automata(
                 automata::dump(intersected, "label = \"intersect\"");
             }
             
-            struct automata* simped = automata::simplify(
+            struct automata* simped = automata::eliminate_dead_code(
                 depth, flags.verbose, intersected);
             
             if (flags.dump_automata)
             {
-                automata::dump(simped, "label = \"simped\"");
+                automata::dump(simped, "label = \"eliminate_dead_code\"");
             }
             
             automata_start = simped;
@@ -111,6 +110,8 @@ automata* build_automata(
         // to fix it.
         if (!automata_start)
         {
+            automata::dump(automata_start, "label = \"abort early\"");
+            
             break;
         }
         

buildtypes/debug.txt

@@ -1,7 +1,4 @@
 
--fsanitize=undefined
--fsanitize=address
-
 -std=c++20
 
 -I .
@@ -11,3 +8,5 @@
 -g
 
 -Wall -Werror -Wextra -Wfatal-errors
+
+-Wno-unused

buildtypes/release.txt

@@ -5,8 +5,8 @@
 
 -I .
 
--D TEST_BUILD
-
--g
+-D RELEASE_BUILD
 
 -Wall -Werror -Wextra -Wfatal-errors
+
+

cmdln_flags.cpp

@@ -12,10 +12,11 @@ cmdln_flags::cmdln_flags(int argc, char* const* argv)
         {"input-file",      required_argument, 0, 'i'},
         {"dump-automata",         no_argument, 0, 'd'},
         {"verbose",               no_argument, 0, 'v'},
+        {"verify",                no_argument, 0, 'V'},
         {0, 0, 0, 0}
     };
     
-    for (int c; (c = getopt_long(argc, argv, "i:dv", long_options, NULL)) >= 0; )
+    for (int c; (c = getopt_long(argc, argv, "i:dvV", long_options, NULL)) >= 0; )
     {
         switch (c)
         {
@@ -31,6 +32,10 @@ cmdln_flags::cmdln_flags(int argc, char* const* argv)
                 verbose = true;
                 break;
             
+            case 'V':
+                verify = true;
+                break;
+            
             default:
                 exit(1);
                 break;

cmdln_flags.hpp

@@ -12,7 +12,9 @@ class cmdln_flags
         bool dump_automata = false;
         
         bool verbose = false;
-    
+        
+        bool verify = false;
+        
     public:
         cmdln_flags(int argc, char* const* argv);
 };

find_solution.cpp

@@ -4,7 +4,9 @@
 
 #include <automata.hpp>
 
-#include "find_solutions.hpp"
+#include <print.hpp>
+
+#include "find_solution.hpp"
 
 static bool is_empty_solution_space(
     unsigned number_of_variables,
@@ -20,11 +22,13 @@ static bool is_empty_solution_space(
     return !moving || !moving->is_accepting;
 }
 
-void find_solutions(
-    unsigned number_of_variables,
+refcounted<class solution> find_solution(
+    refcounted<problem> problem,
     const struct automata* start)
 {
-    bool found_solution = false;
+    refcounted<solution> found_solution = NULL;
+    
+    auto number_of_variables = problem->number_of_variables;
     
     // there are three cases:
         // 1. solutions for no inputs
@@ -36,9 +40,7 @@ void find_solutions(
     {
         if (is_empty_solution_space(number_of_variables, start))
         {
-            puts("no solutions.");
-            
-            found_solution = true;
+            found_solution = new solution(solution::none);
         }
     }
     
@@ -52,9 +54,7 @@ void find_solutions(
         
         if (is_empty_solution_space(number_of_variables, complement))
         {
-            puts("all solutions.");
-            
-            found_solution = true;
+            found_solution = new solution(solution::all);
         }
         
         automata::free(complement);
@@ -63,7 +63,7 @@ void find_solutions(
     // consider case 3: (solutions for some inputs)
     if (!found_solution)
     {
-        int solution[number_of_variables];
+        int* input = new int[number_of_variables];
         
         const struct automata* moving = start;
         
@@ -71,23 +71,20 @@ void find_solutions(
         {
             if (moving->on[0])
             {
-                solution[i] = 0, moving = moving->on[0];
+                input[i] = 0, moving = moving->on[0];
             }
             else
             {
-                solution[i] = 1, moving = moving->on[1];
+                input[i] = 1, moving = moving->on[1];
             }
         }
         
         assert(moving && moving->is_accepting);
         
-        for (unsigned i = 0; i < number_of_variables; i++)
-        {
-            printf("variable %u = %i\n", i + 1, solution[i]);
-        }
-        
-        found_solution = true;
+        found_solution = new solution(number_of_variables, input);
     }
+    
+    return found_solution;
 }
 
 

find_solution.hpp

@@ -0,0 +1,13 @@
+
+#include <refcounted.hpp>
+
+#include <solution.hpp>
+
+#include <problem.hpp>
+
+struct automata;
+
+refcounted<class solution> find_solution(
+    refcounted<problem> problem,
+    const struct automata* start);
+

find_solutions.hpp

@@ -1,7 +0,0 @@
-
-struct automata;
-
-void find_solutions(
-    unsigned number_of_variables,
-    const struct automata* start);
-

main.cpp

@@ -1,4 +1,6 @@
 
+#include <locale.h>
+
 #include <cmdln_flags.hpp>
 
 #include <parse.hpp>
@@ -7,12 +9,17 @@
 
 #include <automata.hpp>
 
-#include <find_solutions.hpp>
+#include <find_solution.hpp>
+
+#include <verify_solution.hpp>
 
 int main(
     int argc,
     char* const* argv)
 {
+    // to get printf to print numbers with commas:
+    setlocale(LC_ALL,"");
+    
     cmdln_flags flags(argc, argv);
     
     auto problems = parse(flags.input_path);
@@ -21,7 +28,14 @@ int main(
     {
         automata* start = build_automata(flags, problem);
         
-        find_solutions(problem->number_of_variables, start);
+        auto solution = find_solution(problem, start);
+        
+        solution->print();
+        
+        if (flags.verify)
+        {
+            verify_solution(problem, solution);
+        }
         
         automata::free(start);
     }

makefile

@@ -29,19 +29,25 @@ ${prefix}/%.o ${prefix}/%.d: %.cpp ${buildtype_options} | ${prefix}/%/
 	@echo "${buildtype}: compiling ${*}.cpp ..."
 	@gcc -c @${buildtype_options} $< -MD -MF ${prefix}/${*}.d -o ${prefix}/${*}.o
 
-#args += -d
+args += -d
 args += -v
+args += -V
 
 #args += -i ./inputs/0.txt
 #args += -i ./inputs/1.txt
 #args += -i ./inputs/2.txt
-args += -i ./inputs/3.txt
+#args += -i ./inputs/3.txt
 #args += -i ./inputs/all.txt
 #args += -i ./inputs/none.txt
 
+args += -i ./satlib/uf20-91/uf20-01.cnf
+
 run: ${prefix}/sat-solver
 	${env} $< ${args}
 
+time-run: ${prefix}/sat-solver
+	bash -c "time ${env} $< ${args}"
+
 gdbrun: ${prefix}/sat-solver
 	gdb --args $< ${args}
 
@@ -51,6 +57,9 @@ valrun: ${prefix}/sat-solver
 valrun-leak: ${prefix}/sat-solver
 	valgrind --leak-check=full --gen-suppressions=yes -- $< ${args}
 
+test: ${prefix}/sat-solver
+	./test.py ${<} ${targs}
+
 include $(patsubst %.cpp,${prefix}/%.d,$(srcs))
 
 
@@ -61,6 +70,17 @@ include $(patsubst %.cpp,${prefix}/%.d,$(srcs))
 
 
 
+
+
+
+
+
+
+
+
+
+
+
 
 
 

parse.cpp

@@ -14,6 +14,12 @@ refcounted<list<refcounted<problem>>> parse(const char* path)
     
     FILE* stream = fopen(path, "r");
     
+    if (!stream)
+    {
+        printf("sat-solver: fopen(): %m\n");
+        exit(1);
+    }
+    
     char *line = NULL;
     size_t len = 0;
     ssize_t nread;
@@ -22,9 +28,15 @@ refcounted<list<refcounted<problem>>> parse(const char* path)
     {
         line[--nread] = 0;
         
+//        println("line = ", line);
+        
         if (line[0] == '\0') continue;
         if (line[0] == 'c') continue;
         
+        // why do the satlib tests have the percent symbol at the end of the
+        // file?
+        if (line[0] == '%') break;
+        
         if (line[0] != 'p')
         {
             assert(!"TODO");
@@ -34,7 +46,7 @@ refcounted<list<refcounted<problem>>> parse(const char* path)
         unsigned number_of_variables;
         unsigned number_of_clauses;
         
-        int r = sscanf(line, " p %u %u ", &number_of_variables, &number_of_clauses);
+        int r = sscanf(line, " p cnf %u %u ", &number_of_variables, &number_of_clauses);
         
         if (r < 2)
         {
@@ -56,6 +68,8 @@ refcounted<list<refcounted<problem>>> parse(const char* path)
             
             line[--nread] = 0;
             
+//            println("clause line = ", line);
+            
             refcounted<clause> c = new clause();
             
             char *moving = line;
@@ -74,6 +88,11 @@ refcounted<list<refcounted<problem>>> parse(const char* path)
                     exit(1);
                 }
                 
+                if (variable == 0)
+                {
+                    continue;
+                }
+                
                 bool value = true;
                 
                 if (variable < 0)

print.cpp

@@ -11,6 +11,11 @@ template <> void print<char*>(char* x)
     printf("%s", x);
 }
 
+template <> void print<void*>(void* x)
+{
+    printf("%p", x);
+}
+
 template <> void print<const char*>(const char* x)
 {
     printf("%s", x);

print.hpp

@@ -34,12 +34,23 @@ template <> void print<double>(const double x);
 
 template <typename F, typename ...R> void print(const F& f, const R&... r)
 {
-    print(f), print(r ...), puts("");
+    print(f), print(r ...);
 }
 
 template <typename ...T> void println(const T&... t)
 {
-    print(t ...);
+    print(t ...), puts("");
 }
 
 
+
+
+
+
+
+
+
+
+
+
+

refcounted.hpp

@@ -1,8 +1,11 @@
 
-
 #ifndef CLASS_REFCOUNT
 #define CLASS_REFCOUNT
 
+#include <valgrind/memcheck.h>
+
+#include <utility>
+
 template<typename T> class refcounted
 {
     T* ptr;
@@ -18,7 +21,10 @@ template<typename T> class refcounted
         {
             ptr = _ptr;
             
-            refcount = new size_t(1);
+            if (ptr)
+            {
+                refcount = new size_t(1);
+            }
         }
         
         refcounted(const refcounted& other):
@@ -71,6 +77,11 @@ template<typename T> class refcounted
             return *ptr;
         }
         
+        const T* get() const
+        {
+            return ptr;
+        }
+        
         T* operator->()
         {
             return ptr;

set.hpp

@@ -78,6 +78,11 @@ template<typename T> class set
             return are_any_new;
         }
         
+        bool has(const T& element) const
+        {
+            return !!tree.search(element);
+        }
+        
         operator bool() const
         {
             return !!tree.head;

solution.cpp

@@ -0,0 +1,36 @@
+
+#include <stdio.h>
+#include <assert.h>
+
+#include <solution.hpp>
+
+void solution::print()
+{
+    switch (kind)
+    {
+        case all:
+        {
+            puts("all solutions.");
+            break;
+        }
+        
+        case none:
+        {
+            puts("no solutions.");
+            break;
+        }
+        
+        case specific:
+        {
+            puts("solution:");
+            
+            for (unsigned i = 0; i < n; i++)
+            {
+                printf("variable %u = %i\n", i + 1, input[i]);
+            }
+        
+            break;
+        }
+    }
+}
+

solution.hpp

@@ -0,0 +1,45 @@
+
+#ifndef STRUCT_SOLUTION
+#define STRUCT_SOLUTION
+
+#include <stddef.h>
+#include <stdlib.h>
+
+class solution
+{
+    public:
+        enum kind_e {
+            all,
+            none,
+            specific,
+        } kind;
+        
+        unsigned n;
+        
+        int* input = NULL;
+    
+    public:
+        solution(kind_e k): kind(k)
+        {
+            ;
+        }
+        
+        solution(unsigned n_, int* input_):
+            kind(solution::specific),
+            n(n_),
+            input(input_)
+        {
+            ;
+        }
+        
+        void print();
+        
+        ~solution()
+        {
+            delete[] input;
+        }
+};
+
+#endif
+
+

srclist.mk

@@ -1,8 +1,10 @@
 srcs += ./automata.cpp
 srcs += ./build_automata.cpp
 srcs += ./cmdln_flags.cpp
-srcs += ./find_solutions.cpp
+srcs += ./find_solution.cpp
 srcs += ./main.cpp
 srcs += ./parse.cpp
 srcs += ./print.cpp
 srcs += ./problem.cpp
+srcs += ./solution.cpp
+srcs += ./verify_solution.cpp

test.py

@@ -0,0 +1,77 @@
+#!/usr/bin/env python3
+
+import os;
+import sys, glob, subprocess, shlex, pickle, atexit, time, argparse;
+
+parser = argparse.ArgumentParser(
+    prog='test',
+    description='What the program does',
+    epilog='Text at the bottom of help')
+
+parser.add_argument('executable')
+parser.add_argument('-v', '--verbose', action='store_true')
+parser.add_argument('-c', '--color', action='store_true', default=os.isatty(0));
+parser.add_argument('--no-color', action='store_const', dest='color', const=False);
+
+args = parser.parse_args(sys.argv[1:]);
+
+try:
+    with open(".test.db", "rb") as stream:
+        ftimes = pickle.load(stream);
+except:
+    ftimes = dict();
+
+def write_ftimes():
+    with open(".test.db", "wb") as stream:
+        pickle.dump(ftimes, stream);
+
+atexit.register(write_ftimes);
+
+all_tests = list(glob.glob("tests/**/*.cnf", recursive = True));
+
+for test in all_tests:
+    if test not in ftimes:
+        ftimes[test] = time.time();
+
+def printgreen(text):
+    if args.color:
+        print("\033[38;2;0;200;0m" + text + "\033[0m");
+    else:
+        print(text);
+
+n = len(all_tests);
+
+for i, test in enumerate(sorted(all_tests, key = lambda x: -ftimes[x])):
+    command = [args.executable, "-i", test, "-vV"];
+    
+    prettycommand = f"[{i}/{n}]: {test} ...";
+    
+    printgreen(prettycommand);
+    
+    res = subprocess.run(command);
+    
+    if res.returncode:
+        ftimes[test] = time.time();
+        exit(1);
+
+printgreen("All tests pass!");
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

tests/0.cnf

@@ -7,7 +7,7 @@ c possibly negative, meaning complement, ending in 0?
 c '0' is the "sentinel", so "1" is the first variable index.
 c like this:
 
-p 3 3
+p cnf 3 3
   +1 +2
   -1 +3
   +2 +3

tests/1.cnf

@@ -1,5 +1,5 @@
 
-p 5 8
+p cnf 5 8
   +1 +5
   -1 +5
   +2 +5

tests/2.cnf

@@ -1,5 +1,5 @@
 
-p 6 2
+p cnf 6 2
   +1 +2 +3 +4 +5 +6
   -1 -2 -3 -4 -5 -6
 
@@ -7,3 +7,4 @@ p 6 2
 c a correct solution is: 0 0 0 0 0 1
 
 
+

tests/3.cnf

@@ -1,5 +1,5 @@
 
-p 20 7
+p cnf 20 7
   1 3 5 7 9 11 13 15 17 19
   1 4 7 10 13 16 19
   1 6 11 16
@@ -11,3 +11,4 @@ p 20 7
 c a correct solution is: 0 0 0 0 0 0 0 0 0 0 0 1 0 1 1 1 0 1 0 0
 
 
+

tests/all.cnf

@@ -1,7 +1,7 @@
 
 c 'c' means comment
 
-p 3 3
+p cnf 3 3
   +1 -1
   +2 -2
   +3 -3

tests/none.cnf

@@ -1,7 +1,7 @@
 
 c 'c' means comment
 
-p 3 6
+p cnf 3 6
   +1
   +2
   +3
@@ -11,3 +11,5 @@ p 3 6
 
 c no inputs satisfy the constraints.
 
+
+

tests/satlib/.gitignore

@@ -0,0 +1,3 @@
+
+uf100-430/
+

tests/satlib/uf20-91/uf20-01.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91
+ 4 -18 19 0
+3 18 -5 0
+-5 -8 -15 0
+-20 7 -16 0
+10 -13 -7 0
+-12 -9 17 0
+17 19 5 0
+-16 9 15 0
+11 -5 -14 0
+18 -10 13 0
+-3 11 12 0
+-6 -17 -8 0
+-18 14 1 0
+-19 -15 10 0
+12 18 -19 0
+-8 4 7 0
+-8 -9 4 0
+7 17 -15 0
+12 -7 -14 0
+-10 -11 8 0
+2 -15 -11 0
+9 6 1 0
+-11 20 -17 0
+9 -15 13 0
+12 -7 -17 0
+-18 -2 20 0
+20 12 4 0
+19 11 14 0
+-16 18 -4 0
+-1 -17 -19 0
+-13 15 10 0
+-12 -14 -13 0
+12 -14 -7 0
+-7 16 10 0
+6 10 7 0
+20 14 -16 0
+-19 17 11 0
+-7 1 -20 0
+-5 12 15 0
+-4 -9 -13 0
+12 -11 -7 0
+-5 19 -8 0
+1 16 17 0
+20 -14 -15 0
+13 -4 10 0
+14 7 10 0
+-5 9 20 0
+10 1 -19 0
+-16 -15 -1 0
+16 3 -11 0
+-15 -10 4 0
+4 -15 -3 0
+-10 -16 11 0
+-8 12 -5 0
+14 -6 12 0
+1 6 11 0
+-13 -5 -1 0
+-7 -2 12 0
+1 -20 19 0
+-2 -13 -8 0
+15 18 4 0
+-11 14 9 0
+-6 -15 -2 0
+5 -12 -15 0
+-6 17 5 0
+-13 5 -19 0
+20 -1 14 0
+9 -17 15 0
+-5 19 -18 0
+-12 8 -10 0
+-18 14 -4 0
+15 -9 13 0
+9 -5 -1 0
+10 -19 -14 0
+20 9 4 0
+-9 -2 19 0
+-5 13 -17 0
+2 -10 -18 0
+-18 3 11 0
+7 -9 17 0
+-15 -6 -3 0
+-2 3 -13 0
+12 3 -2 0
+-2 -3 17 0
+20 -15 -16 0
+-5 -17 -19 0
+-20 -18 11 0
+-9 1 -5 0
+-19 9 17 0
+12 -2 17 0
+4 -16 -5 0
+%
+0
+

tests/satlib/uf20-91/uf20-010.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -11 9 12 0
+-7 -17 -18 0
+-13 -17 20 0
+-4 -16 12 0
+8 2 14 0
+-9 -19 14 0
+7 4 18 0
+-19 -16 5 0
+-1 -16 17 0
+-2 20 -11 0
+-20 9 -17 0
+-14 -15 -17 0
+19 -18 15 0
+6 15 -2 0
+12 8 -14 0
+-1 -2 -3 0
+11 -8 5 0
+6 18 -1 0
+7 -11 8 0
+1 5 15 0
+4 10 12 0
+11 6 18 0
+7 10 3 0
+14 -16 -17 0
+4 18 13 0
+-11 -15 -13 0
+-2 -9 20 0
+2 -5 19 0
+14 6 -19 0
+-8 -13 20 0
+-9 8 13 0
+2 -14 -7 0
+3 16 -15 0
+-2 13 17 0
+-18 -13 16 0
+-18 1 -16 0
+18 2 14 0
+-20 6 -14 0
+15 -19 -8 0
+4 12 -11 0
+19 3 -14 0
+6 5 -7 0
+10 13 -11 0
+15 -1 -3 0
+9 6 10 0
+-11 -1 16 0
+18 -1 12 0
+18 -2 -4 0
+5 13 -20 0
+19 -12 -6 0
+15 11 13 0
+12 2 -7 0
+3 5 -19 0
+3 13 -10 0
+1 8 -6 0
+-2 18 -11 0
+-3 6 -9 0
+-18 -14 -3 0
+-4 -19 -17 0
+7 5 -14 0
+13 19 -12 0
+-12 -7 -3 0
+9 7 -19 0
+6 2 10 0
+11 6 -12 0
+15 1 -17 0
+20 -1 -4 0
+-18 1 5 0
+9 18 14 0
+15 -17 9 0
+-3 11 9 0
+14 12 9 0
+5 14 2 0
+17 -10 -8 0
+14 -15 9 0
+-6 -20 13 0
+1 6 13 0
+-16 15 -17 0
+-8 19 7 0
+-7 3 -1 0
+-18 10 17 0
+12 -4 14 0
+7 10 19 0
+20 15 19 0
+-13 -17 -9 0
+10 -9 3 0
+15 -11 10 0
+12 1 -13 0
+11 3 15 0
+16 -2 -1 0
+-17 -5 -1 0
+%
+0
+

tests/satlib/uf20-91/uf20-0100.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -6 -7 -3 0
+-16 12 18 0
+12 -7 -19 0
+14 1 11 0
+4 5 -20 0
+-17 -9 -1 0
+-17 -16 -2 0
+-15 -5 -18 0
+-7 8 -15 0
+4 -13 3 0
+-17 10 -15 0
+7 -6 10 0
+-20 14 8 0
+11 13 -10 0
+3 -14 12 0
+11 13 14 0
+20 16 10 0
+-12 3 20 0
+-10 -2 -12 0
+17 5 3 0
+-12 13 1 0
+16 17 13 0
+-17 3 -5 0
+18 13 15 0
+1 3 -11 0
+9 -16 5 0
+13 -8 2 0
+-7 8 5 0
+-5 -2 20 0
+-6 -12 -9 0
+-8 -4 9 0
+-18 5 -8 0
+2 17 -7 0
+-14 -12 13 0
+-19 -17 8 0
+-1 14 9 0
+-11 -17 -10 0
+16 -3 -18 0
+16 -6 5 0
+-3 -7 -11 0
+16 -12 1 0
+18 8 6 0
+-19 3 -4 0
+-8 2 -3 0
+15 10 -20 0
+-17 20 8 0
+-7 -6 -13 0
+-15 12 2 0
+15 -9 17 0
+1 5 9 0
+3 -9 -14 0
+8 -1 11 0
+-15 -5 -11 0
+6 -8 7 0
+12 -14 -7 0
+-7 3 -4 0
+18 -11 -20 0
+17 -6 18 0
+-6 3 17 0
+14 -18 4 0
+-16 4 -7 0
+-18 1 9 0
+-18 -7 -13 0
+17 13 10 0
+-20 7 -4 0
+1 17 -18 0
+-5 -8 13 0
+-19 -17 9 0
+-9 8 -18 0
+2 9 -6 0
+4 -7 -13 0
+17 15 7 0
+-11 -7 -3 0
+4 6 1 0
+20 6 19 0
+-1 -14 -10 0
+-13 -10 15 0
+5 9 -7 0
+-11 -12 20 0
+-12 -1 -7 0
+-18 -4 -20 0
+3 8 -15 0
+-6 15 5 0
+-11 13 -1 0
+19 -15 18 0
+-16 -9 12 0
+15 2 17 0
+6 -8 -17 0
+20 -11 -1 0
+20 -9 15 0
+-1 8 14 0
+%
+0
+

tests/satlib/uf20-91/uf20-01000.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 8 -9 7 0
+-7 9 -15 0
+9 8 1 0
+5 -19 2 0
+-1 -9 -8 0
+4 19 16 0
+9 -2 -12 0
+1 20 5 0
+-15 -6 8 0
+-20 -16 -15 0
+-11 7 18 0
+-20 11 -18 0
+1 2 11 0
+10 -13 -16 0
+-1 15 10 0
+3 -12 -5 0
+-20 -10 9 0
+20 -11 -8 0
+15 5 4 0
+-5 -7 19 0
+1 3 -15 0
+17 3 -4 0
+-11 -1 -5 0
+-10 -5 -14 0
+-19 -18 -15 0
+-14 20 12 0
+16 5 10 0
+12 -8 9 0
+-19 -3 13 0
+9 16 -20 0
+-1 2 -16 0
+19 -17 3 0
+-12 -9 -17 0
+7 -17 20 0
+-17 -8 -2 0
+-1 -18 -14 0
+-11 -15 14 0
+10 -2 -20 0
+17 11 -16 0
+2 11 -19 0
+-2 4 10 0
+5 18 -14 0
+13 -11 16 0
+-18 -7 19 0
+10 -14 -13 0
+-4 16 3 0
+14 -15 -2 0
+-3 -10 19 0
+9 19 6 0
+-12 -3 -20 0
+-3 14 1 0
+-10 -17 -7 0
+-19 -4 -1 0
+4 12 -10 0
+-18 4 -17 0
+-20 -15 16 0
+14 7 -1 0
+12 -6 -17 0
+-10 -16 6 0
+9 15 -17 0
+4 -6 -11 0
+9 -8 3 0
+-4 -6 -16 0
+-5 19 -4 0
+14 17 1 0
+9 -18 -12 0
+-16 17 -8 0
+-1 11 16 0
+7 10 9 0
+4 -2 11 0
+-17 -20 -3 0
+-4 -11 -5 0
+-11 -7 20 0
+-5 2 -18 0
+16 5 -3 0
+14 7 -17 0
+8 19 -1 0
+13 16 -12 0
+-10 3 8 0
+18 -5 9 0
+-14 12 -19 0
+5 19 -16 0
+-20 -5 -7 0
+-7 -2 -15 0
+17 -12 -1 0
+7 13 10 0
+-20 14 -9 0
+-6 -20 -2 0
+-5 -18 15 0
+-16 -8 -20 0
+14 19 -10 0
+%
+0
+

tests/satlib/uf20-91/uf20-0101.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 13 -16 -5 0
+11 8 10 0
+-10 -8 16 0
+-9 -17 -7 0
+6 -15 20 0
+4 -11 6 0
+-5 4 -8 0
+-3 -15 -19 0
+-6 -20 8 0
+5 18 -2 0
+-14 -7 11 0
+-19 -7 -6 0
+-15 -6 17 0
+-20 16 15 0
+17 6 3 0
+-14 15 -13 0
+-10 -7 -3 0
+14 13 -20 0
+-18 -6 -12 0
+-13 -15 -5 0
+-18 -8 11 0
+10 -2 8 0
+19 -13 -1 0
+5 8 17 0
+-18 11 5 0
+-20 11 -12 0
+9 5 -13 0
+-1 7 19 0
+5 -11 20 0
+-5 -8 -13 0
+-17 1 7 0
+-4 16 -9 0
+8 4 2 0
+10 -9 -15 0
+-19 1 12 0
+14 -10 -13 0
+13 -12 -5 0
+18 1 -4 0
+10 -20 4 0
+6 -9 -13 0
+17 6 11 0
+19 14 11 0
+6 -10 9 0
+16 13 6 0
+6 12 -19 0
+-5 -14 -8 0
+-9 -10 -4 0
+3 -2 -12 0
+4 -8 19 0
+-10 2 4 0
+-3 -4 8 0
+-2 9 -5 0
+-1 -7 -18 0
+5 19 -1 0
+-8 12 14 0
+-13 12 7 0
+1 5 -15 0
+-1 -3 6 0
+12 19 13 0
+10 13 18 0
+-13 -8 17 0
+8 -18 4 0
+-12 18 -1 0
+-11 2 6 0
+12 -5 -4 0
+17 -15 -4 0
+8 20 18 0
+-4 8 -1 0
+-14 -9 2 0
+-1 10 -5 0
+-11 -3 19 0
+7 -18 -13 0
+-11 17 8 0
+6 -9 20 0
+14 3 -5 0
+-18 13 19 0
+-4 -7 -15 0
+-13 -1 -7 0
+-1 3 -7 0
+16 6 8 0
+-18 3 -8 0
+-6 -3 5 0
+-2 -15 3 0
+15 -17 -11 0
+5 3 19 0
+-8 11 -7 0
+-11 7 -16 0
+1 -3 6 0
+-8 -12 -18 0
+10 -4 18 0
+-12 -2 -16 0
+%
+0
+

tests/satlib/uf20-91/uf20-0102.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 1 6 -8 0
+5 10 17 0
+-15 -10 -20 0
+-3 11 -18 0
+10 -14 8 0
+19 -15 -8 0
+-19 -4 2 0
+3 -6 13 0
+-2 -20 16 0
+16 2 15 0
+-5 -7 3 0
+5 12 -6 0
+-10 -3 2 0
+-13 -19 4 0
+7 -12 19 0
+14 -7 -10 0
+-10 -11 -17 0
+5 -7 -16 0
+-15 10 14 0
+3 -8 -16 0
+-9 -11 3 0
+8 6 12 0
+-18 -6 -15 0
+9 8 2 0
+7 -9 11 0
+-19 -18 2 0
+4 -19 15 0
+-5 -6 18 0
+7 -6 -11 0
+-16 -1 -4 0
+17 9 18 0
+-8 1 -15 0
+-20 6 15 0
+-5 10 14 0
+10 -1 -9 0
+4 20 -9 0
+-3 12 -11 0
+14 7 17 0
+11 9 -10 0
+-10 12 -19 0
+3 2 -6 0
+7 -17 -3 0
+-9 -15 -5 0
+2 -5 19 0
+-16 7 6 0
+17 -10 9 0
+-8 12 11 0
+-3 -4 11 0
+-17 -4 -1 0
+-5 17 10 0
+-3 -9 -8 0
+-10 -5 4 0
+-18 2 -3 0
+20 -11 18 0
+-19 -6 -16 0
+8 -19 17 0
+7 18 -11 0
+-18 -11 -20 0
+-14 -10 -18 0
+14 11 -19 0
+8 -18 9 0
+12 5 20 0
+-20 -3 -19 0
+10 -7 15 0
+14 -9 -7 0
+-11 -15 6 0
+7 19 -8 0
+7 6 -16 0
+-2 -12 -20 0
+-4 7 6 0
+-7 -20 -19 0
+20 2 -10 0
+-4 16 19 0
+-11 -3 13 0
+-8 -2 12 0
+-17 -19 -1 0
+-7 -11 17 0
+-9 2 7 0
+11 5 1 0
+9 -5 -17 0
+-20 15 -18 0
+-1 -17 -11 0
+-4 -16 -18 0
+-18 6 4 0
+-3 -15 11 0
+-17 16 2 0
+-9 10 -5 0
+-15 10 -12 0
+18 -15 -16 0
+-15 -11 -18 0
+-8 19 -9 0
+%
+0
+

tests/satlib/uf20-91/uf20-0103.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -1 4 13 0
+19 -9 -16 0
+9 4 19 0
+14 -1 7 0
+13 -17 2 0
+17 13 -9 0
+9 11 18 0
+-11 -1 16 0
+12 18 14 0
+-4 -3 11 0
+16 4 -15 0
+-14 15 2 0
+-17 12 -4 0
+-1 14 -12 0
+19 5 17 0
+-17 19 -12 0
+2 17 -11 0
+-6 4 9 0
+-15 19 9 0
+-4 -17 7 0
+-3 4 10 0
+10 -8 -14 0
+5 2 12 0
+8 19 15 0
+-10 11 18 0
+-3 5 -14 0
+-18 -13 -7 0
+-8 18 2 0
+5 -15 -19 0
+11 2 17 0
+-9 -20 12 0
+5 -9 -18 0
+-5 -14 -2 0
+15 -16 17 0
+-7 -12 14 0
+19 -17 -2 0
+-14 20 8 0
+7 -9 -17 0
+5 -14 10 0
+8 -6 -17 0
+4 15 10 0
+-5 18 4 0
+16 -15 12 0
+9 7 -15 0
+-18 11 16 0
+2 1 19 0
+12 -2 -7 0
+-20 -7 8 0
+-16 19 -8 0
+11 6 3 0
+-15 -6 -10 0
+17 5 15 0
+17 -8 13 0
+-6 14 2 0
+6 -14 -15 0
+18 15 -4 0
+-20 5 1 0
+-20 5 -17 0
+-16 15 -8 0
+6 12 -1 0
+18 20 -3 0
+-3 13 20 0
+17 -6 -5 0
+-4 -9 -8 0
+6 7 4 0
+5 4 -9 0
+6 -10 -5 0
+2 -17 -18 0
+-14 -19 4 0
+20 1 -7 0
+-11 5 18 0
+8 -12 -13 0
+19 -18 -4 0
+7 -18 11 0
+1 6 15 0
+-19 6 3 0
+-4 19 -13 0
+-11 19 10 0
+11 -14 -20 0
+11 14 6 0
+-11 -20 -13 0
+-19 -20 -18 0
+-3 -6 17 0
+-15 -11 -17 0
+-14 2 5 0
+-6 -18 5 0
+-19 -9 -20 0
+-15 -2 -20 0
+-14 8 10 0
+1 -16 3 0
+-10 -1 -8 0
+%
+0
+

tests/satlib/uf20-91/uf20-0104.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 7 6 -8 0
+-11 -8 16 0
+8 3 1 0
+14 -15 18 0
+-8 -16 -10 0
+18 -6 2 0
+-19 -5 13 0
+-17 -3 -10 0
+-6 -4 14 0
+-13 -3 12 0
+-18 20 -14 0
+-16 18 6 0
+13 14 1 0
+10 11 4 0
+-19 4 16 0
+-9 2 17 0
+16 3 -15 0
+18 1 19 0
+-13 16 -14 0
+-19 -2 -14 0
+1 -15 7 0
+-18 -2 -17 0
+-14 -2 -3 0
+11 9 2 0
+4 -2 -15 0
+4 -14 -16 0
+-19 15 -13 0
+-12 4 13 0
+-14 -12 15 0
+-18 1 3 0
+8 -7 -16 0
+15 14 -7 0
+-19 1 -11 0
+9 13 -11 0
+-1 -10 -15 0
+20 -19 12 0
+18 -9 11 0
+-3 -18 7 0
+10 1 -20 0
+-4 -20 6 0
+-17 12 -14 0
+17 -14 -7 0
+-3 9 1 0
+5 1 -9 0
+15 8 18 0
+-2 1 -16 0
+-16 -1 -19 0
+-19 -20 -12 0
+19 20 8 0
+-18 -12 -4 0
+-20 -16 14 0
+6 11 -1 0
+16 -6 11 0
+-7 19 -10 0
+20 -18 -5 0
+16 15 10 0
+-16 20 11 0
+15 -12 13 0
+8 9 12 0
+2 7 9 0
+20 17 -3 0
+-20 -1 -12 0
+12 -15 -10 0
+-6 4 -9 0
+1 -7 5 0
+18 11 3 0
+13 20 9 0
+3 -2 -12 0
+11 2 -20 0
+-9 13 2 0
+-15 -14 -10 0
+-8 14 -6 0
+-16 -6 -7 0
+2 15 -19 0
+-17 -14 18 0
+9 11 -15 0
+12 18 -19 0
+19 -7 8 0
+5 18 -15 0
+-19 -3 9 0
+-1 5 -16 0
+9 20 -18 0
+20 3 5 0
+8 -13 20 0
+19 14 9 0
+13 11 -10 0
+9 15 18 0
+5 1 -4 0
+-11 -15 -4 0
+16 12 5 0
+15 -11 -19 0
+%
+0
+

tests/satlib/uf20-91/uf20-0105.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 12 -15 -19 0
+-4 -12 20 0
+11 19 -5 0
+12 -5 4 0
+-10 -20 -4 0
+6 7 -14 0
+10 12 -13 0
+20 -6 -11 0
+18 -8 17 0
+-7 -20 9 0
+-6 20 7 0
+12 16 19 0
+-5 4 13 0
+7 6 16 0
+-11 15 -6 0
+20 10 -6 0
+20 1 -12 0
+-9 -11 4 0
+-3 -14 13 0
+5 6 3 0
+19 5 -8 0
+-7 -11 12 0
+20 -5 -3 0
+-4 -11 5 0
+20 16 -10 0
+-8 -5 -19 0
+-1 -5 -10 0
+-12 4 -18 0
+6 9 -7 0
+18 -3 -12 0
+-19 -17 -13 0
+15 -5 -14 0
+-2 10 17 0
+5 -13 -19 0
+10 6 -3 0
+-5 17 9 0
+4 -15 -16 0
+8 -20 15 0
+7 20 -17 0
+-16 -12 18 0
+17 3 18 0
+7 -6 -2 0
+16 20 13 0
+14 -10 7 0
+-2 10 -1 0
+-1 4 2 0
+6 -15 9 0
+-1 13 20 0
+20 16 12 0
+-16 7 17 0
+-15 6 -8 0
+20 -10 11 0
+9 18 1 0
+11 -10 18 0
+9 12 -10 0
+-9 -2 20 0
+12 18 -13 0
+10 15 -8 0
+13 -14 8 0
+13 4 15 0
+-16 -18 4 0
+19 6 12 0
+17 20 10 0
+19 -16 -14 0
+1 15 -12 0
+-18 -20 -16 0
+12 19 16 0
+-5 2 20 0
+-20 -6 17 0
+11 -14 2 0
+-15 13 -4 0
+8 -17 -15 0
+3 -4 2 0
+5 16 15 0
+9 20 -3 0
+-14 16 -12 0
+-14 -13 9 0
+19 -16 -10 0
+6 -8 14 0
+15 -17 5 0
+-18 -13 -15 0
+-9 12 -4 0
+-5 6 12 0
+14 -13 11 0
+-10 -14 4 0
+-18 16 -14 0
+-3 18 6 0
+-20 16 -14 0
+-7 -15 -8 0
+-3 8 -19 0
+14 -1 13 0
+%
+0
+

tests/satlib/uf20-91/uf20-0106.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 19 -17 11 0
+1 19 18 0
+4 -5 11 0
+16 -9 14 0
+-18 10 6 0
+-7 -14 20 0
+-14 18 20 0
+-2 12 -13 0
+-6 -19 11 0
+-7 20 -4 0
+6 -4 -20 0
+2 19 -11 0
+20 13 2 0
+8 11 19 0
+12 5 10 0
+10 -12 6 0
+-2 17 4 0
+4 -5 18 0
+14 -1 -12 0
+18 -4 8 0
+-10 -3 -14 0
+-20 -15 3 0
+16 -4 5 0
+15 18 2 0
+-5 2 -4 0
+-1 -12 -18 0
+-14 10 -11 0
+4 -17 -15 0
+-16 -13 -10 0
+18 -4 -15 0
+-17 16 -9 0
+11 -3 8 0
+12 2 6 0
+18 6 -16 0
+1 -18 -15 0
+-18 -9 -19 0
+3 -1 -5 0
+15 -2 20 0
+19 -17 -18 0
+6 19 9 0
+-12 -19 10 0
+-8 -13 9 0
+6 -11 10 0
+7 -11 -17 0
+16 2 -15 0
+-6 14 13 0
+-4 11 -16 0
+-1 -8 -10 0
+20 -3 7 0
+20 -16 4 0
+-16 4 6 0
+-10 -1 2 0
+-20 13 12 0
+-12 8 9 0
+-15 5 -6 0
+-9 -2 20 0
+4 10 -6 0
+-7 -1 -10 0
+20 -5 2 0
+18 -15 -11 0
+-20 -2 -19 0
+4 20 8 0
+-7 10 9 0
+-11 -7 6 0
+18 -12 -20 0
+-7 -15 5 0
+-17 -11 -6 0
+-4 7 -8 0
+-18 -14 10 0
+-5 18 17 0
+14 -5 7 0
+3 -6 -1 0
+20 -3 -6 0
+-5 12 7 0
+2 -9 18 0
+2 -17 -8 0
+-12 -17 -18 0
+-19 -2 -6 0
+5 3 -9 0
+9 4 5 0
+17 11 15 0
+6 -1 2 0
+10 -12 19 0
+-6 4 -8 0
+-16 -5 -17 0
+-11 -6 3 0
+4 17 8 0
+8 -11 -19 0
+-7 16 -18 0
+11 -3 8 0
+12 -20 -4 0
+%
+0
+

tests/satlib/uf20-91/uf20-0107.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 8 7 14 0
+17 16 1 0
+19 11 17 0
+14 17 10 0
+16 20 -2 0
+18 2 -11 0
+20 2 13 0
+4 16 19 0
+20 -10 6 0
+-6 -20 5 0
+13 17 -16 0
+4 -18 1 0
+5 -18 -11 0
+8 -16 -14 0
+6 2 15 0
+-18 17 -2 0
+-4 -19 17 0
+18 -15 12 0
+13 20 -18 0
+-6 -12 17 0
+6 10 -17 0
+5 14 -16 0
+-2 4 -8 0
+-15 2 20 0
+7 -14 17 0
+3 19 -20 0
+-11 1 13 0
+14 -10 -13 0
+1 -12 -14 0
+-2 14 3 0
+-14 20 5 0
+10 -8 15 0
+15 4 14 0
+2 -18 -15 0
+12 8 17 0
+-20 -9 7 0
+-9 3 10 0
+20 18 4 0
+-4 -1 -20 0
+-5 -2 -10 0
+11 -19 17 0
+18 -17 -8 0
+-11 -13 -9 0
+-20 -18 13 0
+12 16 -9 0
+12 17 -18 0
+-13 -4 9 0
+-11 -1 14 0
+11 -15 -5 0
+-10 6 -11 0
+18 -14 16 0
+-17 -3 -16 0
+8 14 -11 0
+-17 -5 -4 0
+9 4 10 0
+-4 -6 -20 0
+7 8 -1 0
+20 -12 -8 0
+-9 -14 -2 0
+-11 1 -2 0
+6 -12 17 0
+3 -17 -15 0
+18 10 6 0
+16 -1 4 0
+-19 15 -4 0
+4 13 -12 0
+-11 -20 -15 0
+-13 16 3 0
+20 19 11 0
+5 -18 9 0
+-6 -13 -16 0
+-5 -15 9 0
+12 -8 -5 0
+-9 6 -11 0
+20 7 4 0
+9 -19 -3 0
+7 9 6 0
+18 -9 12 0
+15 8 -11 0
+1 3 -7 0
+-11 -13 12 0
+-10 2 -15 0
+-2 -5 4 0
+19 -6 -11 0
+-10 -11 16 0
+10 -6 13 0
+7 9 -10 0
+17 -6 -2 0
+-3 18 19 0
+7 -17 -1 0
+2 -1 15 0
+%
+0
+

tests/satlib/uf20-91/uf20-0108.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -14 -9 1 0
+6 11 -15 0
+13 12 -4 0
+-17 16 -3 0
+2 17 7 0
+5 -1 11 0
+9 20 19 0
+-17 13 16 0
+-12 -19 -18 0
+-6 19 14 0
+14 -12 -2 0
+-13 5 -16 0
+-16 4 9 0
+-13 15 9 0
+8 16 -5 0
+3 1 4 0
+-20 17 -6 0
+-12 -3 -16 0
+-10 -6 14 0
+4 18 -8 0
+-8 6 3 0
+12 -7 9 0
+-19 -18 -16 0
+-8 -17 5 0
+-16 -9 1 0
+18 -20 -8 0
+10 -19 9 0
+-5 15 -17 0
+-7 -6 5 0
+-5 10 2 0
+16 2 10 0
+17 12 -20 0
+11 -6 -7 0
+11 -18 5 0
+12 1 -7 0
+5 7 9 0
+-9 2 -5 0
+7 12 8 0
+-11 17 -2 0
+2 1 15 0
+-17 15 -6 0
+19 8 15 0
+18 -11 -8 0
+11 -15 13 0
+-10 18 19 0
+-14 20 6 0
+-9 -10 -16 0
+13 4 19 0
+-16 17 -14 0
+-17 -3 -15 0
+3 -7 17 0
+-18 11 20 0
+-18 -15 1 0
+15 -13 -7 0
+-19 8 -15 0
+8 7 -18 0
+10 8 4 0
+-12 -19 -1 0
+1 13 11 0
+-19 -20 -10 0
+4 2 1 0
+15 -17 18 0
+15 -17 4 0
+-7 8 -13 0
+12 9 -4 0
+9 4 18 0
+5 3 2 0
+1 -20 9 0
+13 2 -3 0
+18 19 -1 0
+12 -4 16 0
+6 -14 7 0
+12 20 9 0
+-10 19 -4 0
+9 3 -12 0
+7 -17 15 0
+-5 3 -20 0
+1 20 -9 0
+12 4 15 0
+-12 -11 -19 0
+6 -12 -7 0
+-11 -12 3 0
+1 -10 12 0
+-13 18 17 0
+8 -16 -3 0
+-12 -2 -19 0
+-11 1 -2 0
+17 -2 -8 0
+-17 -14 -7 0
+20 15 14 0
+-18 -8 -6 0
+%
+0
+

tests/satlib/uf20-91/uf20-0109.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 17 19 -12 0
+18 -15 20 0
+-17 -6 12 0
+11 10 12 0
+5 9 -8 0
+-5 20 -8 0
+-12 -7 -6 0
+-2 10 -3 0
+-2 16 7 0
+19 -6 -18 0
+-18 19 -6 0
+-6 12 -2 0
+-19 -15 -2 0
+14 -15 -6 0
+-5 -20 12 0
+-9 13 -8 0
+-11 13 5 0
+-12 -9 4 0
+-12 -14 -18 0
+11 -5 13 0
+-13 -4 18 0
+-13 9 18 0
+-7 13 -16 0
+-14 -17 8 0
+-3 5 12 0
+-1 -20 10 0
+-3 12 -16 0
+7 17 -9 0
+17 -20 11 0
+12 13 -8 0
+11 7 -15 0
+8 -6 -4 0
+-14 -12 8 0
+-12 18 -11 0
+-9 1 -3 0
+2 -15 12 0
+-10 -7 11 0
+-12 8 -17 0
+-20 -15 13 0
+5 -19 1 0
+-4 -12 3 0
+-20 -4 8 0
+-16 9 -10 0
+-6 -8 -19 0
+3 15 20 0
+13 -17 -10 0
+-8 -15 19 0
+13 19 10 0
+10 -14 7 0
+7 13 18 0
+14 19 -3 0
+9 -4 -12 0
+19 -14 2 0
+-12 13 -9 0
+-7 -17 -10 0
+6 -13 -11 0
+-2 3 -4 0
+6 8 -12 0
+-9 2 4 0
+-9 -8 5 0
+-9 -6 15 0
+20 16 -10 0
+-2 15 -6 0
+4 10 -17 0
+-16 6 20 0
+2 11 16 0
+1 20 -14 0
+-5 4 -18 0
+1 15 10 0
+4 17 -13 0
+-5 -12 -9 0
+-3 13 17 0
+-1 5 -6 0
+19 4 -8 0
+-11 -2 7 0
+-18 -4 14 0
+-1 9 19 0
+5 -6 10 0
+1 17 15 0
+-18 -4 16 0
+9 -18 15 0
+6 3 -20 0
+-7 -13 -4 0
+-4 17 -15 0
+7 -2 -20 0
+-3 1 12 0
+-17 -13 -8 0
+-16 -1 8 0
+-18 20 12 0
+4 -5 7 0
+8 19 -12 0
+%
+0
+

tests/satlib/uf20-91/uf20-011.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 1 -20 5 0
+8 -1 2 0
+3 -15 19 0
+-15 6 -13 0
+9 -19 -13 0
+3 20 17 0
+-2 -11 8 0
+16 13 -9 0
+-17 15 6 0
+3 -19 16 0
+5 14 -7 0
+-8 -14 19 0
+-16 -6 17 0
+15 -8 -9 0
+7 -14 -9 0
+2 -3 20 0
+18 12 7 0
+16 17 -20 0
+17 -1 -2 0
+-11 -10 -20 0
+-14 19 -20 0
+20 -1 5 0
+9 -6 2 0
+2 -11 9 0
+-16 6 13 0
+-13 -20 -9 0
+-5 12 -9 0
+7 16 -14 0
+-12 -18 -6 0
+9 -17 19 0
+-13 9 18 0
+-6 19 -10 0
+-15 18 -19 0
+10 16 -6 0
+-12 -4 -13 0
+5 8 16 0
+6 -7 -14 0
+-20 8 -9 0
+-8 -11 -13 0
+-8 -5 4 0
+-18 2 -11 0
+-18 -8 -5 0
+-3 12 4 0
+9 17 14 0
+2 -17 11 0
+-8 14 -9 0
+18 -5 -19 0
+18 19 -3 0
+-5 -18 -8 0
+-4 20 14 0
+-3 13 12 0
+-9 15 -1 0
+9 -8 15 0
+-14 -15 -11 0
+-13 -5 -10 0
+-10 16 3 0
+-9 19 -6 0
+-9 -17 -13 0
+11 -8 13 0
+17 13 8 0
+-18 16 1 0
+7 19 11 0
+-14 -5 -20 0
+3 5 -11 0
+2 17 1 0
+5 4 -17 0
+-10 -8 16 0
+8 19 5 0
+16 6 -15 0
+-10 -14 17 0
+-7 3 -4 0
+-12 -4 2 0
+-7 -10 14 0
+-7 17 18 0
+-5 -17 6 0
+2 17 -8 0
+4 1 -2 0
+14 -7 -2 0
+-10 -5 -7 0
+-5 8 1 0
+2 19 -14 0
+-11 9 12 0
+-9 -16 -6 0
+-6 -19 -8 0
+-8 3 10 0
+-7 11 17 0
+-9 16 15 0
+-18 1 4 0
+4 19 1 0
+-11 14 5 0
+8 14 -19 0
+%
+0
+

tests/satlib/uf20-91/uf20-0110.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 12 -3 17 0
+1 -5 16 0
+-10 9 -1 0
+7 8 -2 0
+11 5 -3 0
+9 19 -16 0
+12 4 1 0
+13 15 11 0
+-10 11 12 0
+4 -6 -10 0
+-8 13 -4 0
+-19 -9 6 0
+-9 15 -4 0
+5 -16 -7 0
+12 -2 -20 0
+8 13 -1 0
+1 10 15 0
+7 -16 1 0
+-4 16 -2 0
+-1 -14 -20 0
+1 -12 -17 0
+4 2 -8 0
+17 -4 -15 0
+-10 -1 -20 0
+-5 -20 -18 0
+12 13 2 0
+-5 13 -15 0
+-18 20 13 0
+-20 7 -13 0
+-19 6 -15 0
+-9 -15 -12 0
+-12 15 11 0
+-17 3 1 0
+15 -16 -13 0
+8 -7 -9 0
+4 -15 9 0
+-15 -8 16 0
+9 16 5 0
+-18 1 -2 0
+2 11 -20 0
+-7 4 14 0
+-20 -3 15 0
+20 3 4 0
+-10 -4 -9 0
+5 16 2 0
+-4 11 -6 0
+6 15 1 0
+1 -11 -12 0
+15 -20 -8 0
+-10 -8 20 0
+-18 4 -7 0
+1 -14 15 0
+-9 -16 14 0
+19 -14 9 0
+5 9 10 0
+-5 -20 -12 0
+-17 8 5 0
+6 -18 1 0
+-5 11 -18 0
+-16 19 8 0
+-4 -1 15 0
+-6 13 -15 0
+-18 16 -14 0
+8 -6 -2 0
+-4 -12 -11 0
+-2 14 12 0
+-4 15 20 0
+15 3 5 0
+20 -8 11 0
+13 17 19 0
+15 10 -2 0
+-15 9 -6 0
+4 1 -13 0
+13 -9 -1 0
+10 3 -11 0
+-17 1 -9 0
+-9 -2 3 0
+-5 19 -10 0
+-10 19 -8 0
+-5 -12 1 0
+14 -16 -8 0
+-16 -3 18 0
+-1 -10 -16 0
+-8 -14 -2 0
+-3 6 20 0
+-12 -20 14 0
+9 -16 -3 0
+13 -3 9 0
+-17 11 4 0
+-18 -12 2 0
+-7 17 1 0
+%
+0
+

tests/satlib/uf20-91/uf20-0111.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 15 -19 10 0
+15 -7 20 0
+-19 -11 -8 0
+-15 8 -14 0
+2 14 19 0
+-8 3 -4 0
+3 2 5 0
+11 -16 15 0
+18 7 -3 0
+20 13 5 0
+9 18 -16 0
+6 -3 11 0
+20 7 19 0
+15 6 -2 0
+-6 -10 -15 0
+9 2 -13 0
+-10 13 -6 0
+15 -16 -10 0
+-17 5 20 0
+14 12 -15 0
+-20 -14 13 0
+10 12 13 0
+18 -16 12 0
+-18 19 -6 0
+-10 -16 -6 0
+17 -13 -11 0
+17 2 -9 0
+3 -19 -13 0
+15 16 14 0
+11 -2 9 0
+19 8 -14 0
+-11 13 1 0
+-12 6 -4 0
+-9 2 -8 0
+5 9 -14 0
+-15 -20 -2 0
+-11 -16 -6 0
+-19 4 -1 0
+-2 -11 16 0
+-5 2 14 0
+6 -8 -4 0
+-18 6 8 0
+-20 3 -9 0
+-18 -16 -15 0
+-17 -10 -5 0
+3 -20 -15 0
+8 2 9 0
+12 8 -16 0
+-6 -4 9 0
+17 10 -18 0
+14 8 12 0
+1 17 -7 0
+-17 18 3 0
+-7 -11 -14 0
+3 8 -1 0
+2 14 -5 0
+-10 20 -18 0
+15 4 14 0
+14 -1 17 0
+-12 19 7 0
+-13 -10 18 0
+16 17 6 0
+-5 3 8 0
+15 -3 10 0
+-4 5 -12 0
+-18 -15 6 0
+2 6 -3 0
+-9 12 -13 0
+17 -1 6 0
+-10 -18 -19 0
+-18 15 1 0
+15 -11 -9 0
+11 -9 12 0
+3 15 11 0
+-16 10 2 0
+9 -7 16 0
+15 -14 11 0
+-2 -6 -17 0
+-3 15 6 0
+-18 -19 16 0
+20 -13 -15 0
+4 5 -6 0
+-9 -7 3 0
+-13 -6 -19 0
+14 -7 -15 0
+-6 -4 9 0
+18 1 9 0
+-14 7 -11 0
+-2 -17 16 0
+-17 5 14 0
+-5 15 9 0
+%
+0
+

tests/satlib/uf20-91/uf20-0112.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 17 4 8 0
+-19 13 -12 0
+3 17 1 0
+6 -19 12 0
+2 -5 1 0
+-3 16 17 0
+10 -17 15 0
+5 16 -10 0
+13 -9 -16 0
+-12 -13 16 0
+-1 2 18 0
+1 2 16 0
+-7 -16 13 0
+5 -9 -6 0
+-20 11 -12 0
+12 -9 1 0
+11 20 8 0
+9 -8 4 0
+-10 -4 11 0
+12 11 1 0
+3 13 -18 0
+-9 -13 -16 0
+4 7 5 0
+10 -17 -7 0
+-11 4 8 0
+-19 -10 2 0
+13 -2 -18 0
+6 2 3 0
+-13 -18 -5 0
+18 -9 20 0
+-14 -18 17 0
+-20 -7 11 0
+-13 -1 -10 0
+4 -16 8 0
+1 3 -5 0
+-19 -8 -15 0
+-20 -8 11 0
+16 5 18 0
+-9 -17 -12 0
+13 -17 -14 0
+-16 10 6 0
+-19 -14 -20 0
+19 -14 1 0
+18 -3 -1 0
+-1 13 10 0
+-7 16 -14 0
+-17 7 11 0
+-11 -20 -1 0
+20 17 -18 0
+14 -5 6 0
+-7 -6 3 0
+17 -14 -7 0
+19 -16 15 0
+-10 -12 8 0
+4 -1 -8 0
+-12 5 16 0
+-9 16 -2 0
+9 -3 14 0
+13 -2 -1 0
+2 16 -17 0
+2 13 18 0
+13 19 4 0
+-17 -5 16 0
+-13 -19 5 0
+15 7 -19 0
+5 20 -16 0
+5 17 -18 0
+10 -1 5 0
+-9 12 -1 0
+-15 19 18 0
+8 6 4 0
+-3 -12 5 0
+-20 8 4 0
+-1 20 -6 0
+10 2 -15 0
+-11 -9 -4 0
+16 -7 -6 0
+-11 18 6 0
+18 9 -1 0
+3 2 13 0
+14 -4 -17 0
+15 -10 8 0
+-14 4 20 0
+6 -20 -12 0
+17 3 -19 0
+13 1 -3 0
+2 4 8 0
+11 -18 5 0
+13 3 6 0
+2 -7 -8 0
+20 -10 15 0
+%
+0
+

tests/satlib/uf20-91/uf20-0113.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -13 -6 -14 0
+-8 10 18 0
+14 -16 -9 0
+-12 -10 -7 0
+3 14 -4 0
+-13 17 -12 0
+1 5 -17 0
+-20 17 -10 0
+3 11 -16 0
+8 -6 10 0
+-15 9 -13 0
+11 -13 5 0
+17 -2 5 0
+-11 -15 -12 0
+2 -18 -8 0
+-1 -4 7 0
+4 -6 8 0
+1 -19 6 0
+13 10 -1 0
+2 -6 11 0
+3 12 10 0
+13 -9 8 0
+-9 -14 3 0
+-20 -11 -1 0
+16 -1 -5 0
+-9 4 1 0
+-11 17 -10 0
+-20 3 -17 0
+-15 12 9 0
+-8 2 -4 0
+2 -16 19 0
+-5 -4 -3 0
+9 14 -15 0
+-4 -2 -7 0
+-15 3 -18 0
+17 -11 19 0
+13 -20 18 0
+20 7 -12 0
+8 3 -20 0
+-20 -1 -16 0
+-3 -16 -2 0
+20 -17 -12 0
+15 -5 19 0
+-17 16 7 0
+-19 -2 16 0
+-13 -14 9 0
+12 -9 -2 0
+2 -7 -5 0
+-7 -14 -12 0
+14 -10 -15 0
+17 13 -6 0
+7 17 -8 0
+-7 2 6 0
+9 15 -1 0
+15 -16 -8 0
+1 -9 6 0
+-11 -12 18 0
+-13 -16 17 0
+2 -12 -5 0
+18 14 6 0
+3 -18 -11 0
+-18 -2 -7 0
+-1 -5 12 0
+1 -20 6 0
+1 12 -10 0
+-5 19 -6 0
+9 12 7 0
+5 8 14 0
+2 6 3 0
+-12 -9 -1 0
+17 12 -20 0
+17 -13 6 0
+6 4 2 0
+-8 15 7 0
+7 12 -19 0
+2 20 8 0
+-15 -7 5 0
+15 17 16 0
+20 -8 19 0
+15 -13 -18 0
+-5 16 7 0
+3 13 -17 0
+18 -12 14 0
+20 14 15 0
+-17 6 -10 0
+6 -7 20 0
+5 8 14 0
+15 8 13 0
+10 -8 17 0
+11 -10 -9 0
+-14 6 -18 0
+%
+0
+

tests/satlib/uf20-91/uf20-0114.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 6 7 -16 0
+11 9 15 0
+20 12 19 0
+-7 3 -6 0
+-10 -4 15 0
+5 17 -11 0
+-19 15 2 0
+-19 20 -14 0
+2 14 -1 0
+-3 15 14 0
+-2 15 12 0
+15 2 6 0
+6 2 3 0
+3 -2 -11 0
+-2 -6 -12 0
+7 -13 5 0
+17 20 16 0
+-10 -2 5 0
+17 -13 -7 0
+-2 -5 13 0
+20 8 -11 0
+18 6 -16 0
+11 -9 3 0
+20 -12 -15 0
+9 13 -18 0
+-7 5 1 0
+-18 4 -12 0
+-11 -15 6 0
+-2 18 16 0
+11 -13 19 0
+-1 10 -18 0
+19 -18 -7 0
+-18 2 -11 0
+-14 1 -10 0
+11 6 7 0
+4 -20 -8 0
+16 -14 12 0
+-1 15 -8 0
+4 14 -13 0
+-11 -6 19 0
+-19 15 13 0
+-15 -3 18 0
+18 13 -9 0
+6 -20 -5 0
+-18 6 15 0
+11 16 -14 0
+5 7 18 0
+20 19 15 0
+20 -7 -1 0
+-20 12 6 0
+15 14 2 0
+8 -13 5 0
+-9 -17 3 0
+-16 4 -19 0
+-9 14 12 0
+16 -8 -1 0
+-8 -5 12 0
+-17 9 5 0
+-3 -6 -1 0
+5 8 -2 0
+-18 -4 19 0
+17 -8 -1 0
+18 20 -17 0
+3 14 -5 0
+-18 11 5 0
+-16 18 11 0
+1 -7 15 0
+-19 -13 -10 0
+-14 -17 -11 0
+16 -17 8 0
+-8 11 -5 0
+-5 6 -1 0
+-9 -5 10 0
+16 13 -19 0
+-4 6 -16 0
+19 -13 2 0
+-18 -15 -11 0
+15 3 -2 0
+7 18 13 0
+-4 -7 -8 0
+-10 -16 -5 0
+-17 11 8 0
+-11 7 6 0
+1 6 -18 0
+11 -17 -7 0
+19 10 -5 0
+6 -10 -13 0
+12 20 3 0
+-7 14 6 0
+-3 -20 -12 0
+-11 -4 -15 0
+%
+0
+

tests/satlib/uf20-91/uf20-0115.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 12 14 16 0
+-13 11 -17 0
+-20 10 13 0
+-15 7 16 0
+4 10 -11 0
+-3 1 14 0
+-19 -20 14 0
+7 -13 19 0
+4 1 -16 0
+17 -19 3 0
+-7 -12 3 0
+12 -9 18 0
+18 4 2 0
+10 -5 -7 0
+4 -8 -14 0
+-12 -19 -4 0
+-16 4 -7 0
+-17 -7 2 0
+-5 2 -7 0
+-6 -11 -5 0
+-12 8 16 0
+15 17 -10 0
+-19 6 -5 0
+2 -8 19 0
+5 -16 9 0
+16 1 12 0
+20 -17 7 0
+-15 -19 5 0
+7 -15 -14 0
+-10 16 -7 0
+-8 -9 -13 0
+-5 -11 16 0
+16 -15 9 0
+8 20 -19 0
+20 14 -7 0
+15 11 -14 0
+-13 -5 9 0
+-7 3 -5 0
+20 7 -13 0
+-18 -19 -5 0
+-10 -8 12 0
+-5 -2 18 0
+4 19 -7 0
+-4 12 8 0
+-14 -2 10 0
+-4 6 20 0
+-20 -4 7 0
+1 18 -16 0
+-8 -16 6 0
+-2 -6 12 0
+-19 -2 -16 0
+-8 -17 -1 0
+-3 -14 17 0
+-13 6 16 0
+-7 -3 -13 0
+8 -12 13 0
+20 -18 -6 0
+-20 -14 11 0
+-17 5 -15 0
+-20 9 -18 0
+-4 -15 -3 0
+-6 -18 11 0
+-8 -18 16 0
+8 -12 -2 0
+-4 2 16 0
+-1 3 9 0
+-2 -18 -12 0
+-20 13 -9 0
+7 -19 8 0
+6 2 1 0
+-3 -13 -15 0
+-20 11 9 0
+12 20 10 0
+16 5 -12 0
+9 -12 14 0
+-16 17 11 0
+15 -20 -6 0
+-6 7 -12 0
+-3 -6 15 0
+-4 9 11 0
+-10 -19 -16 0
+11 -19 2 0
+12 1 -19 0
+-5 9 -17 0
+-6 7 20 0
+-3 -15 -2 0
+13 2 15 0
+-20 -8 2 0
+19 11 -5 0
+-9 1 7 0
+-10 7 -6 0
+%
+0
+

tests/satlib/uf20-91/uf20-0116.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -20 6 17 0
+-16 -11 -19 0
+18 -4 -5 0
+-20 11 1 0
+-19 13 -17 0
+-16 -13 12 0
+6 16 -19 0
+6 15 -1 0
+9 -6 3 0
+-2 11 -18 0
+7 -20 -4 0
+7 13 9 0
+-13 16 -9 0
+4 15 -20 0
+8 -5 -4 0
+19 2 11 0
+13 -10 20 0
+-4 11 17 0
+8 -7 -17 0
+20 2 -5 0
+14 5 2 0
+-12 -20 -14 0
+13 -4 2 0
+12 4 11 0
+-8 -10 -7 0
+-12 -7 18 0
+-19 -3 4 0
+-4 7 5 0
+-8 -6 20 0
+-4 -5 11 0
+8 -4 1 0
+-19 -17 -10 0
+-15 -17 19 0
+-7 20 6 0
+-19 7 20 0
+2 8 4 0
+1 -19 12 0
+-6 -10 -5 0
+-18 19 17 0
+12 -8 6 0
+7 20 12 0
+10 1 -20 0
+-8 -15 -1 0
+3 -10 19 0
+-14 18 -11 0
+-6 9 -11 0
+5 -10 11 0
+14 -2 5 0
+-15 -3 6 0
+10 -11 -20 0
+-15 -9 -10 0
+8 -10 -20 0
+20 13 17 0
+19 -9 16 0
+-13 -18 15 0
+-1 4 -19 0
+6 13 -12 0
+16 -2 1 0
+-14 -10 12 0
+-10 -17 5 0
+-18 15 11 0
+3 12 6 0
+-10 -17 -3 0
+9 -1 3 0
+-10 5 -3 0
+-3 -2 -14 0
+16 6 2 0
+12 -5 -6 0
+-15 -16 20 0
+-5 -17 9 0
+-1 -2 14 0
+-9 2 -11 0
+4 13 -20 0
+-5 -4 16 0
+-5 -11 3 0
+13 -1 18 0
+15 -18 7 0
+19 11 20 0
+11 3 4 0
+17 -16 -11 0
+20 -15 -11 0
+1 -10 15 0
+16 -15 -1 0
+5 -3 -18 0
+-5 -1 2 0
+14 5 7 0
+15 17 13 0
+4 19 3 0
+-16 -6 -5 0
+7 -19 15 0
+-10 -11 -14 0
+%
+0
+

tests/satlib/uf20-91/uf20-0117.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 13 -2 -1 0
+-15 -9 8 0
+-8 14 -2 0
+4 -3 18 0
+1 -9 -11 0
+17 -16 15 0
+17 -4 20 0
+5 2 4 0
+-2 5 10 0
+19 -10 13 0
+-5 -10 -3 0
+4 -8 -2 0
+-13 16 -18 0
+4 -3 -14 0
+20 -2 -12 0
+-15 -5 -1 0
+-17 -3 -1 0
+13 9 -14 0
+12 -13 15 0
+-3 14 8 0
+-13 -18 7 0
+-12 7 -4 0
+8 19 -6 0
+14 18 8 0
+-15 -6 2 0
+12 16 -11 0
+17 -13 -16 0
+-17 -19 -3 0
+-3 1 -4 0
+18 -8 -17 0
+12 5 18 0
+-20 11 8 0
+12 -7 6 0
+-9 -20 -13 0
+-12 4 -8 0
+5 8 17 0
+8 20 -14 0
+-12 -13 4 0
+-7 11 -18 0
+-10 18 -17 0
+16 -9 -13 0
+-12 17 13 0
+4 16 14 0
+8 18 -20 0
+-16 -1 -11 0
+9 -7 -20 0
+-20 -3 -13 0
+-2 19 -11 0
+-18 -9 -15 0
+11 19 -2 0
+-12 17 13 0
+13 10 -2 0
+6 4 7 0
+-19 12 -18 0
+6 -17 14 0
+-1 11 19 0
+-2 16 -3 0
+6 4 7 0
+20 7 6 0
+-16 -13 -2 0
+18 6 -16 0
+-19 10 -11 0
+-3 14 2 0
+-10 -6 -16 0
+8 -4 -20 0
+3 2 -9 0
+5 17 10 0
+-6 19 -7 0
+6 11 18 0
+-19 -10 12 0
+-11 17 -10 0
+19 7 -14 0
+-14 -16 -17 0
+-13 -17 8 0
+-19 -17 -20 0
+19 6 -11 0
+-5 -3 20 0
+-16 4 -5 0
+-9 16 -13 0
+6 -5 7 0
+-20 15 -8 0
+4 7 15 0
+-13 -19 -9 0
+14 -19 -8 0
+18 -1 5 0
+-5 8 14 0
+-19 16 -2 0
+19 12 9 0
+11 12 2 0
+-2 -14 -7 0
+-2 -13 6 0
+%
+0
+

tests/satlib/uf20-91/uf20-0118.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 12 -3 -7 0
+-9 18 14 0
+-15 3 -2 0
+-16 17 -5 0
+-19 13 1 0
+-1 -10 -20 0
+-14 13 15 0
+-19 -15 10 0
+-9 13 8 0
+-18 19 -7 0
+12 -13 10 0
+-1 4 -2 0
+16 -19 1 0
+18 7 20 0
+-12 -3 4 0
+-9 -5 19 0
+5 13 -14 0
+-17 -6 15 0
+5 -13 17 0
+10 -4 -13 0
+-16 -3 18 0
+19 -7 -1 0
+-2 13 18 0
+10 -18 -7 0
+17 3 10 0
+-20 -3 -6 0
+-12 -4 -14 0
+-18 -2 3 0
+17 -8 2 0
+20 -12 3 0
+17 15 6 0
+16 -20 6 0
+20 13 7 0
+7 5 12 0
+-9 -7 -18 0
+-15 -12 -8 0
+2 -9 -15 0
+-11 18 -3 0
+-2 -8 15 0
+-19 -5 10 0
+-9 11 16 0
+-11 -18 -6 0
+8 -14 19 0
+-7 -2 4 0
+-17 -2 -16 0
+-2 -7 16 0
+8 -2 14 0
+-13 11 -8 0
+4 6 20 0
+-19 4 2 0
+13 7 -16 0
+17 -11 -2 0
+19 7 -11 0
+3 7 1 0
+-9 7 -10 0
+-11 -14 7 0
+17 7 8 0
+-6 -8 -18 0
+14 -19 16 0
+14 4 12 0
+-4 -10 -2 0
+7 -3 -6 0
+16 8 -2 0
+-6 -14 -11 0
+-5 14 -8 0
+19 7 -20 0
+19 14 18 0
+-15 18 -16 0
+11 10 -2 0
+6 -15 -3 0
+1 -5 13 0
+20 5 -6 0
+-18 3 10 0
+4 -17 -16 0
+1 4 12 0
+17 6 14 0
+17 6 -9 0
+15 -6 17 0
+10 3 -20 0
+-2 -8 20 0
+-3 -8 -11 0
+1 -13 2 0
+-3 -9 -15 0
+2 1 16 0
+-17 8 11 0
+-1 -3 9 0
+7 19 -17 0
+-18 9 -19 0
+6 9 -12 0
+-4 7 6 0
+15 -3 9 0
+%
+0
+

tests/satlib/uf20-91/uf20-0119.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -19 -8 2 0
+7 15 -1 0
+-2 11 3 0
+-4 2 7 0
+-16 7 -14 0
+-16 -9 -20 0
+4 -6 -10 0
+-17 16 -3 0
+3 10 -14 0
+15 5 1 0
+-1 -20 -19 0
+16 1 -3 0
+19 2 -12 0
+12 -4 -8 0
+-20 -6 2 0
+10 -15 5 0
+5 -11 2 0
+-4 -14 9 0
+13 -7 14 0
+-18 -11 12 0
+5 -20 9 0
+-12 -4 20 0
+13 -6 -19 0
+14 -9 12 0
+16 5 -9 0
+-6 9 -2 0
+5 -3 4 0
+17 6 -5 0
+18 10 -9 0
+19 -8 -6 0
+10 5 -1 0
+6 -12 -15 0
+16 -12 20 0
+17 -13 -10 0
+3 -14 -20 0
+8 7 1 0
+-20 14 -19 0
+9 -18 6 0
+-10 16 14 0
+-12 -3 -2 0
+7 18 -5 0
+-16 6 14 0
+-9 6 -13 0
+7 -19 -6 0
+17 -2 -15 0
+14 -10 18 0
+-17 2 16 0
+18 10 -9 0
+2 -13 11 0
+-2 14 11 0
+10 -15 12 0
+-17 14 9 0
+15 -2 19 0
+15 13 -19 0
+14 -2 -10 0
+-7 6 19 0
+10 -16 14 0
+-16 -1 3 0
+-13 5 6 0
+11 6 15 0
+10 7 20 0
+-13 4 19 0
+10 -4 -5 0
+-20 19 -18 0
+-7 -10 2 0
+2 17 3 0
+-18 -9 7 0
+1 16 13 0
+8 -9 -2 0
+-11 -2 -9 0
+-15 16 17 0
+18 -10 9 0
+-17 11 -7 0
+-17 -9 8 0
+6 11 -3 0
+1 2 -18 0
+-11 -16 -3 0
+-9 -5 15 0
+-16 2 18 0
+17 -12 9 0
+2 19 -4 0
+13 -20 -1 0
+14 -18 -2 0
+-18 13 -17 0
+1 -9 2 0
+4 -17 -6 0
+-7 16 -4 0
+-18 10 5 0
+6 -1 -16 0
+-11 -6 -5 0
+16 14 -2 0
+%
+0
+

tests/satlib/uf20-91/uf20-012.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -17 -12 -5 0
+-14 -10 6 0
+6 20 9 0
+-12 -5 -9 0
+-2 -3 -16 0
+-10 -16 7 0
+-9 -5 12 0
+-3 2 -4 0
+-20 18 9 0
+14 -12 -17 0
+14 -8 19 0
+16 -3 -12 0
+12 -20 3 0
+-3 -11 15 0
+12 9 3 0
+-20 13 -8 0
+12 17 9 0
+-7 -10 -13 0
+-11 -2 -10 0
+2 -9 -4 0
+-2 -7 -1 0
+11 20 19 0
+-20 7 15 0
+8 -16 1 0
+13 19 -4 0
+-8 -1 -5 0
+19 14 15 0
+6 7 3 0
+5 -11 -19 0
+-15 -12 19 0
+5 16 14 0
+2 4 -7 0
+-9 -14 13 0
+-11 -3 6 0
+17 -11 15 0
+-19 -18 -9 0
+-7 -2 19 0
+13 3 19 0
+-13 9 -16 0
+-7 13 -10 0
+-11 6 -17 0
+11 12 19 0
+-16 -2 -12 0
+-4 -5 6 0
+14 -2 1 0
+-3 4 -15 0
+-16 12 -11 0
+-3 -17 -2 0
+-11 -14 -18 0
+4 -7 14 0
+-13 -10 8 0
+8 4 -17 0
+-3 -20 -18 0
+7 -5 10 0
+-7 -4 16 0
+-4 -7 12 0
+-17 5 6 0
+10 -8 -7 0
+-11 5 8 0
+-20 5 -11 0
+5 19 3 0
+-8 15 13 0
+7 11 -5 0
+-12 17 8 0
+-18 -10 17 0
+-15 -16 -4 0
+4 -12 3 0
+-8 -5 7 0
+-6 -10 -9 0
+-15 5 14 0
+-12 -16 -1 0
+6 -16 9 0
+-10 -4 9 0
+18 -3 12 0
+-2 15 -11 0
+-20 -18 -7 0
+17 18 13 0
+-9 -16 12 0
+-19 -10 -11 0
+17 -18 -5 0
+19 -12 8 0
+-3 -8 19 0
+-5 -2 -19 0
+-5 18 -20 0
+-6 13 11 0
+-11 17 9 0
+-19 17 -8 0
+-19 -12 -10 0
+-19 -8 -20 0
+19 -2 -7 0
+-11 5 -10 0
+%
+0
+

tests/satlib/uf20-91/uf20-0120.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 4 -8 -2 0
+14 -16 12 0
+11 19 4 0
+3 13 -12 0
+-13 -4 -16 0
+-19 20 -3 0
+13 18 -12 0
+-14 -11 -10 0
+-3 17 -5 0
+11 15 -16 0
+1 6 -12 0
+-20 18 -12 0
+-2 -16 -3 0
+3 -16 -15 0
+-20 1 -11 0
+7 4 -18 0
+10 7 -4 0
+-3 -5 -19 0
+16 14 12 0
+-2 4 -19 0
+3 16 1 0
+-13 -15 16 0
+-13 -18 8 0
+-8 6 19 0
+7 10 -6 0
+3 9 -12 0
+12 -1 11 0
+-11 -9 -3 0
+4 8 19 0
+-5 -13 17 0
+-6 1 -11 0
+14 15 -20 0
+-10 -13 6 0
+5 -15 -13 0
+11 -2 12 0
+-10 -18 -20 0
+8 -18 12 0
+-1 20 -13 0
+6 -18 -2 0
+-3 -8 20 0
+12 8 -7 0
+-8 -4 7 0
+18 17 -1 0
+-14 -18 -19 0
+-19 -2 -11 0
+6 -7 12 0
+-16 -13 12 0
+9 -20 -18 0
+7 17 20 0
+-18 19 1 0
+-3 16 -15 0
+10 -15 -2 0
+-11 -14 -8 0
+7 -8 -6 0
+8 12 -11 0
+16 -10 11 0
+-14 -6 -3 0
+7 13 -1 0
+-13 11 -6 0
+-6 17 8 0
+10 -14 12 0
+1 12 9 0
+-17 15 1 0
+17 -14 -15 0
+1 -19 -16 0
+10 3 -14 0
+-5 4 -3 0
+1 -3 5 0
+-6 -17 -20 0
+20 11 -16 0
+-17 5 -9 0
+-3 -11 -2 0
+-17 20 18 0
+-17 -3 4 0
+16 5 -18 0
+-1 -13 2 0
+-1 11 -3 0
+-13 8 -12 0
+-15 -4 16 0
+-1 -16 15 0
+-12 -19 -15 0
+-14 -19 -5 0
+11 -8 20 0
+-16 -13 11 0
+-1 11 6 0
+-18 -1 4 0
+-7 6 -19 0
+3 -12 -2 0
+-9 -8 13 0
+-8 -20 13 0
+18 13 -3 0
+%
+0
+

tests/satlib/uf20-91/uf20-0121.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 5 -9 15 0
+13 11 -5 0
+3 1 -8 0
+20 -5 4 0
+-19 2 3 0
+19 9 1 0
+15 -18 -5 0
+4 1 7 0
+5 7 10 0
+-1 8 -11 0
+-13 18 -16 0
+-11 3 -1 0
+-15 2 7 0
+-5 -12 -11 0
+-1 13 -5 0
+7 -20 -10 0
+-19 -5 -17 0
+19 -12 1 0
+11 16 -2 0
+10 20 -3 0
+7 -6 -5 0
+7 5 -16 0
+4 12 -14 0
+20 19 14 0
+20 -18 1 0
+18 -5 -13 0
+-2 1 -17 0
+-11 -10 4 0
+-17 -11 -15 0
+-18 -15 17 0
+-17 18 20 0
+-12 5 18 0
+6 -12 -4 0
+-14 8 -18 0
+-7 1 -14 0
+17 1 -11 0
+-19 -14 -9 0
+-1 8 5 0
+-4 -9 -2 0
+-2 -14 11 0
+17 19 12 0
+-3 -2 11 0
+18 -6 -16 0
+7 -20 -5 0
+-5 -17 11 0
+16 -13 -8 0
+-9 -19 -18 0
+8 -14 -1 0
+18 2 -17 0
+-20 14 8 0
+20 3 -16 0
+3 -19 10 0
+-16 6 -19 0
+-14 6 15 0
+2 -9 18 0
+13 19 -8 0
+-1 9 -16 0
+-16 6 20 0
+7 16 13 0
+6 -8 9 0
+-7 -10 -6 0
+12 19 1 0
+2 -4 -15 0
+9 4 -13 0
+1 -11 5 0
+17 -20 10 0
+-14 -7 -6 0
+-5 -16 -19 0
+16 5 19 0
+-6 15 -10 0
+-12 8 1 0
+7 9 14 0
+6 -18 7 0
+20 18 1 0
+13 9 20 0
+-13 15 -16 0
+-2 -15 6 0
+4 1 -5 0
+-11 -5 -17 0
+-16 6 -8 0
+-3 -1 -5 0
+15 -16 6 0
+-8 15 2 0
+11 15 12 0
+-6 -2 -10 0
+4 -20 -19 0
+20 -12 -9 0
+7 -1 -13 0
+16 -4 -12 0
+11 17 -20 0
+-18 13 -16 0
+%
+0
+

tests/satlib/uf20-91/uf20-0122.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 20 -8 -11 0
+-15 17 -19 0
+19 5 12 0
+-6 14 16 0
+19 20 5 0
+-7 8 -16 0
+11 5 -13 0
+-3 2 -19 0
+-18 -14 -13 0
+-9 18 1 0
+5 14 6 0
+12 -8 14 0
+-3 -13 7 0
+15 14 -1 0
+4 -13 17 0
+-15 -16 20 0
+10 -5 14 0
+13 8 -9 0
+3 1 -16 0
+-14 17 -11 0
+-12 -3 7 0
+-12 9 6 0
+-10 -12 -16 0
+-2 20 7 0
+5 20 11 0
+14 -9 -5 0
+-17 2 3 0
+5 -18 -6 0
+-5 -15 3 0
+1 18 -14 0
+16 14 -4 0
+-17 19 20 0
+18 -3 -15 0
+6 -13 -14 0
+2 -9 10 0
+-20 6 9 0
+-17 -6 5 0
+-5 -16 12 0
+9 -2 -3 0
+6 -1 -8 0
+9 20 1 0
+6 12 -11 0
+5 -11 -4 0
+3 -1 -15 0
+12 15 -1 0
+-11 -8 14 0
+4 -5 11 0
+-10 -18 -20 0
+-5 2 -1 0
+-13 20 -9 0
+7 -12 -4 0
+-1 -15 -2 0
+1 8 -13 0
+-20 6 13 0
+14 17 20 0
+18 -17 12 0
+18 -17 -20 0
+9 3 -7 0
+9 -8 10 0
+2 -9 10 0
+-2 15 3 0
+-9 -20 17 0
+-18 -20 14 0
+-8 -7 -11 0
+9 -7 -16 0
+-3 18 20 0
+-2 -20 18 0
+-14 -13 -16 0
+2 -17 -8 0
+-10 -20 -16 0
+-20 -15 -13 0
+-15 -18 13 0
+-15 8 19 0
+-9 3 -6 0
+-16 -14 -20 0
+-4 11 10 0
+9 -18 -4 0
+-8 5 -6 0
+-4 -9 1 0
+15 -5 -20 0
+10 6 5 0
+-15 -8 -13 0
+-3 16 9 0
+-1 10 5 0
+15 6 -5 0
+-11 -8 -4 0
+12 4 -7 0
+-10 3 -12 0
+3 1 2 0
+-11 -16 9 0
+-15 7 -18 0
+%
+0
+

tests/satlib/uf20-91/uf20-0123.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 10 8 -14 0
+15 -9 19 0
+-10 -18 -6 0
+11 8 -20 0
+12 -3 5 0
+-20 -3 -16 0
+-8 7 -6 0
+4 -1 17 0
+13 -6 -8 0
+-13 -19 -4 0
+-19 13 8 0
+19 12 -14 0
+-15 8 -17 0
+20 2 -1 0
+-6 15 10 0
+13 19 -9 0
+3 -15 9 0
+-1 -7 -12 0
+-18 17 -1 0
+-8 -13 9 0
+-11 -3 6 0
+8 6 -15 0
+13 10 -8 0
+7 -2 -16 0
+2 -11 14 0
+7 18 5 0
+-1 12 19 0
+4 -13 -14 0
+-17 7 -10 0
+-6 -20 4 0
+17 -10 -6 0
+11 -17 2 0
+-18 -17 -19 0
+-7 14 -6 0
+-7 15 13 0
+18 1 14 0
+-14 13 -5 0
+2 -20 -14 0
+19 -18 -5 0
+-19 -1 -8 0
+15 -9 -13 0
+17 6 7 0
+-19 3 -8 0
+3 2 16 0
+1 -4 -10 0
+-19 -10 -8 0
+-5 15 -11 0
+14 8 6 0
+-9 -11 20 0
+-16 -20 3 0
+4 8 -12 0
+-16 -11 7 0
+-5 -4 -11 0
+-19 -4 15 0
+-11 -20 4 0
+14 -17 -10 0
+1 13 8 0
+12 -9 -7 0
+-17 -18 3 0
+-15 -2 18 0
+-9 12 11 0
+15 3 -14 0
+-13 -14 4 0
+12 10 5 0
+-17 -4 9 0
+15 7 16 0
+11 -15 -7 0
+1 9 -7 0
+-7 -15 -10 0
+19 14 -15 0
+11 2 20 0
+-11 18 -15 0
+-11 2 20 0
+17 12 -18 0
+-17 1 -8 0
+5 19 17 0
+-5 -16 1 0
+10 4 -9 0
+17 1 10 0
+-20 -5 12 0
+-16 -12 3 0
+4 11 6 0
+13 7 -11 0
+13 4 20 0
+-6 8 17 0
+-12 -6 -7 0
+17 -19 2 0
+-14 13 -16 0
+-13 -8 -6 0
+4 -11 9 0
+15 19 12 0
+%
+0
+

tests/satlib/uf20-91/uf20-0124.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 10 -7 2 0
+-19 7 15 0
+-20 -16 -7 0
+17 -11 1 0
+-4 -10 13 0
+20 5 10 0
+-4 7 -12 0
+2 -1 14 0
+-20 12 -15 0
+-4 2 -16 0
+-3 -15 -16 0
+-17 11 -18 0
+-19 -2 7 0
+-4 11 -5 0
+17 9 12 0
+-10 -16 -2 0
+-17 -7 -15 0
+17 2 -7 0
+18 12 9 0
+-12 2 17 0
+8 -19 4 0
+-4 -1 -18 0
+12 18 -19 0
+16 17 -20 0
+4 19 -9 0
+-6 5 3 0
+-1 10 -3 0
+8 4 12 0
+3 4 -17 0
+12 -9 -17 0
+-16 -20 -3 0
+4 -20 1 0
+-1 3 -10 0
+13 -10 1 0
+8 3 14 0
+2 -19 9 0
+-16 1 8 0
+-3 -8 -5 0
+10 13 -3 0
+16 -10 -17 0
+-18 -15 -6 0
+14 16 2 0
+12 10 -4 0
+2 -5 -3 0
+13 -15 7 0
+-1 12 10 0
+14 2 6 0
+-15 13 20 0
+-12 3 6 0
+13 -18 19 0
+4 3 -13 0
+-16 -10 -2 0
+-14 5 -11 0
+-5 -8 19 0
+-12 -10 -20 0
+-13 16 6 0
+-15 11 -4 0
+-7 -8 -6 0
+4 -1 -17 0
+14 -3 19 0
+17 12 2 0
+-4 -14 7 0
+-4 8 3 0
+-18 3 8 0
+14 19 5 0
+1 -10 3 0
+13 -6 -10 0
+6 2 15 0
+-20 -10 9 0
+-5 -10 -15 0
+14 -7 19 0
+16 5 -17 0
+-18 -13 14 0
+14 15 11 0
+11 10 5 0
+-16 -15 19 0
+-14 19 -20 0
+17 -18 4 0
+3 -8 -16 0
+-15 2 -8 0
+-20 11 19 0
+-12 3 -20 0
+-8 -6 -15 0
+20 -6 -16 0
+-18 20 -1 0
+-17 3 7 0
+-16 12 13 0
+7 10 1 0
+6 11 16 0
+7 -8 9 0
+-1 -14 11 0
+%
+0
+

tests/satlib/uf20-91/uf20-0125.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -16 19 -2 0
+3 -16 8 0
+3 -18 10 0
+-12 -14 19 0
+-19 -15 -6 0
+6 11 17 0
+-5 -1 13 0
+-15 10 -12 0
+7 -2 -14 0
+-1 7 4 0
+2 -14 18 0
+14 -20 -4 0
+7 -6 -18 0
+7 15 8 0
+-9 14 5 0
+11 -8 15 0
+-5 15 14 0
+3 16 -19 0
+-10 -4 20 0
+-7 5 13 0
+-18 -11 -10 0
+1 -15 -17 0
+19 13 -2 0
+11 4 -9 0
+5 1 8 0
+-16 -13 -17 0
+-12 7 9 0
+10 19 17 0
+7 -9 -14 0
+-12 17 9 0
+11 16 -9 0
+9 12 8 0
+-11 2 -10 0
+10 15 8 0
+20 -3 -17 0
+-11 7 -15 0
+17 18 -11 0
+-8 -15 13 0
+15 1 17 0
+7 -4 6 0
+-3 2 -8 0
+16 17 -14 0
+18 9 13 0
+13 1 4 0
+-13 -10 11 0
+19 -15 5 0
+-3 -6 2 0
+14 -9 -12 0
+-10 -11 19 0
+-1 12 11 0
+-14 -9 17 0
+3 -18 14 0
+-8 -14 -20 0
+-3 -16 -2 0
+8 -3 11 0
+20 5 15 0
+-7 16 13 0
+-13 -16 19 0
+6 -15 -3 0
+11 -19 18 0
+9 20 -13 0
+11 9 -10 0
+10 16 8 0
+-9 -11 -1 0
+7 5 10 0
+12 -14 -9 0
+-19 8 -9 0
+20 16 -8 0
+17 12 14 0
+-15 -10 14 0
+10 12 -14 0
+13 1 4 0
+-17 8 12 0
+-9 -14 -16 0
+-4 -12 -9 0
+-9 7 13 0
+-7 -10 5 0
+14 7 -13 0
+13 12 8 0
+19 9 -17 0
+-6 16 19 0
+3 17 -8 0
+20 -14 -6 0
+18 -8 -6 0
+-5 2 -8 0
+-18 4 -16 0
+-10 2 -6 0
+-15 -2 4 0
+17 -6 -8 0
+-7 20 6 0
+-17 13 2 0
+%
+0
+

tests/satlib/uf20-91/uf20-0126.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 9 -12 19 0
+-2 -9 14 0
+-13 19 -3 0
+5 -18 -17 0
+12 8 14 0
+12 9 -15 0
+15 11 -1 0
+-9 -17 15 0
+4 19 -2 0
+16 -12 6 0
+12 -6 15 0
+-19 -10 -14 0
+-16 -6 14 0
+-15 1 7 0
+-14 17 -18 0
+6 -18 20 0
+3 -2 -16 0
+18 5 -6 0
+-3 2 20 0
+-13 19 -4 0
+-18 1 13 0
+-20 8 7 0
+-8 -11 14 0
+-19 -13 -6 0
+10 -13 15 0
+-19 17 2 0
+-16 -9 -13 0
+-19 6 9 0
+-19 14 -5 0
+6 -1 -11 0
+7 -14 2 0
+17 4 -1 0
+-6 7 8 0
+17 6 1 0
+17 -8 10 0
+7 -1 -8 0
+20 -19 -17 0
+-13 -7 -3 0
+7 20 12 0
+4 9 -11 0
+17 -4 -5 0
+-6 11 -16 0
+-5 17 14 0
+1 -10 -17 0
+11 19 8 0
+17 4 -1 0
+-1 15 -2 0
+8 -11 2 0
+-6 -7 -3 0
+3 -15 -7 0
+1 20 11 0
+-2 3 -4 0
+5 20 4 0
+-12 9 8 0
+15 5 -20 0
+12 8 14 0
+5 -10 8 0
+-12 -13 7 0
+10 6 -15 0
+-19 -12 -18 0
+-12 -7 6 0
+18 -6 12 0
+-9 5 -19 0
+-1 -13 2 0
+-14 -15 -20 0
+-3 6 -9 0
+16 -7 -8 0
+9 4 12 0
+-4 -19 -8 0
+13 10 -16 0
+-7 9 1 0
+-10 2 8 0
+10 -12 -11 0
+-8 -18 -16 0
+12 -10 20 0
+2 -19 -11 0
+-3 19 -11 0
+9 13 8 0
+-17 4 20 0
+3 10 -9 0
+-12 -2 -13 0
+-18 6 17 0
+-11 -10 14 0
+20 14 1 0
+-10 12 13 0
+14 5 -17 0
+6 -1 18 0
+-6 9 10 0
+9 5 18 0
+14 15 -12 0
+11 1 20 0
+%
+0
+

tests/satlib/uf20-91/uf20-0127.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -7 -9 -8 0
+3 7 -8 0
+6 19 11 0
+11 10 1 0
+1 -17 -18 0
+-12 -18 5 0
+-11 15 7 0
+16 -9 -7 0
+-14 3 7 0
+-8 -18 17 0
+16 -19 -7 0
+1 -6 -16 0
+13 -20 -18 0
+-7 16 5 0
+-1 -15 -4 0
+-5 -7 -16 0
+10 -15 -1 0
+-17 -12 13 0
+5 -3 1 0
+-16 -17 -2 0
+-16 -19 -1 0
+7 20 9 0
+-1 -2 -18 0
+-19 1 -16 0
+7 5 9 0
+-1 -19 -11 0
+-11 3 4 0
+18 -7 -13 0
+17 16 3 0
+-17 9 11 0
+-20 11 5 0
+1 -18 17 0
+-3 8 -4 0
+-14 -4 8 0
+-4 -1 3 0
+3 10 -14 0
+-15 -7 14 0
+-14 -16 -17 0
+-5 20 4 0
+2 -11 -15 0
+-11 7 -4 0
+-4 15 8 0
+-8 19 -16 0
+18 3 -5 0
+15 -19 16 0
+-14 -19 3 0
+-10 4 20 0
+11 -3 6 0
+1 -14 -11 0
+-19 14 13 0
+1 14 6 0
+9 18 5 0
+15 1 13 0
+-9 -7 3 0
+14 10 -15 0
+-14 5 -8 0
+2 16 13 0
+16 -19 3 0
+16 7 -19 0
+20 17 14 0
+-19 -5 -16 0
+20 -8 4 0
+1 10 -9 0
+4 -15 14 0
+-3 20 -17 0
+-5 4 -2 0
+12 -2 16 0
+-8 2 11 0
+20 4 2 0
+-4 3 -19 0
+4 -10 -18 0
+-15 13 -11 0
+7 -6 2 0
+2 18 -12 0
+6 4 13 0
+-9 -19 -5 0
+-8 3 -9 0
+-9 -19 11 0
+-12 13 15 0
+16 19 -6 0
+-5 11 -7 0
+-17 15 12 0
+-8 -7 -12 0
+11 12 -5 0
+5 20 -9 0
+-4 9 -5 0
+-5 -20 -6 0
+18 7 -19 0
+1 -15 -10 0
+16 -4 -13 0
+19 18 6 0
+%
+0
+

tests/satlib/uf20-91/uf20-0128.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -16 10 -17 0
+-5 3 19 0
+-9 -10 -20 0
+-4 -16 12 0
+16 14 9 0
+20 -16 19 0
+-6 -10 14 0
+-4 -19 -14 0
+-20 10 -9 0
+6 17 7 0
+10 19 -8 0
+11 9 5 0
+7 -1 3 0
+-10 7 -12 0
+-9 -11 -8 0
+-10 8 -5 0
+1 15 3 0
+9 8 -12 0
+-19 -12 4 0
+-20 7 9 0
+-1 -13 10 0
+-14 -13 -5 0
+-6 -3 20 0
+10 -17 -14 0
+-20 18 3 0
+12 -16 17 0
+-18 8 -7 0
+-19 -6 18 0
+-5 6 -19 0
+-13 -6 -9 0
+-3 8 20 0
+9 -10 7 0
+-2 -17 3 0
+-2 19 -4 0
+12 11 -3 0
+9 15 2 0
+-9 -15 14 0
+1 -19 -2 0
+-8 -17 -14 0
+6 -8 -9 0
+2 -11 3 0
+-18 11 1 0
+-13 6 7 0
+-3 -18 -15 0
+-19 -2 7 0
+18 8 -11 0
+-4 15 18 0
+9 8 -10 0
+6 -7 -20 0
+-2 -1 -5 0
+15 7 -3 0
+6 5 -17 0
+-10 14 -9 0
+-19 9 6 0
+18 11 6 0
+-15 3 11 0
+-17 -10 -5 0
+13 -20 4 0
+2 12 15 0
+-12 8 15 0
+-2 4 5 0
+-13 -17 18 0
+-7 4 8 0
+-17 -7 12 0
+16 7 -9 0
+-12 -5 2 0
+6 9 18 0
+-11 13 -12 0
+-20 -1 -3 0
+13 -7 3 0
+20 8 12 0
+-2 -9 17 0
+-8 3 -15 0
+-15 -1 19 0
+-15 5 -17 0
+-4 6 20 0
+-3 7 13 0
+-2 -14 8 0
+-14 6 10 0
+-2 -18 -6 0
+11 -18 17 0
+14 -15 -9 0
+-11 -16 -8 0
+-7 -5 6 0
+18 -17 -5 0
+-16 -5 17 0
+15 -8 -5 0
+19 5 14 0
+-6 9 8 0
+19 3 -20 0
+-3 -2 -19 0
+%
+0
+

tests/satlib/uf20-91/uf20-0129.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -14 3 -9 0
+16 -9 8 0
+3 -11 -16 0
+18 -9 -13 0
+-15 18 5 0
+-7 15 6 0
+-20 -17 4 0
+-5 14 -16 0
+-15 -18 5 0
+13 -12 -6 0
+-13 -3 -6 0
+19 14 11 0
+8 12 -2 0
+-15 -2 8 0
+-2 13 -7 0
+11 -4 9 0
+-18 -8 -5 0
+-18 4 -8 0
+-13 -5 16 0
+-1 17 16 0
+-2 15 11 0
+7 9 14 0
+-2 -13 10 0
+7 3 20 0
+-1 17 4 0
+-1 19 20 0
+-9 -2 -10 0
+14 4 20 0
+-15 -4 -12 0
+-14 4 5 0
+14 1 -13 0
+10 -1 5 0
+1 -3 -9 0
+-9 12 -16 0
+-15 -1 -19 0
+-3 8 1 0
+-10 -18 9 0
+-3 19 6 0
+-4 -12 -13 0
+-16 7 -20 0
+-15 8 2 0
+-3 14 8 0
+-15 11 5 0
+-2 7 -1 0
+-14 -1 19 0
+8 9 -11 0
+19 -7 -8 0
+-12 -13 6 0
+5 14 -15 0
+-17 -2 -1 0
+18 -3 5 0
+3 -10 -14 0
+-6 8 -4 0
+-20 -8 -11 0
+-14 10 -1 0
+-10 -2 18 0
+-2 13 -18 0
+-7 -8 20 0
+-7 -19 12 0
+-15 -5 -14 0
+10 8 20 0
+-16 3 13 0
+-3 -14 6 0
+-20 11 1 0
+11 8 -18 0
+-15 14 -3 0
+-17 -8 -11 0
+16 -7 -2 0
+-8 -11 -4 0
+20 12 -19 0
+-19 1 -16 0
+9 12 -3 0
+17 -12 -1 0
+-13 -1 -2 0
+10 -14 -9 0
+-1 17 16 0
+-9 -18 -13 0
+-11 16 -9 0
+3 14 -20 0
+1 19 7 0
+3 -7 -19 0
+12 10 11 0
+15 5 -16 0
+-8 20 15 0
+13 -8 -15 0
+4 1 -2 0
+-1 -16 -3 0
+-18 -14 16 0
+8 -7 1 0
+10 -12 -17 0
+4 -16 -12 0
+%
+0
+

tests/satlib/uf20-91/uf20-013.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -19 2 16 0
+10 -4 -19 0
+7 -20 15 0
+16 11 -9 0
+15 5 6 0
+10 8 3 0
+-13 10 11 0
+-18 -4 2 0
+-15 7 -4 0
+18 -11 20 0
+-13 16 15 0
+-4 -11 18 0
+11 -18 -6 0
+4 -1 -7 0
+6 -11 -3 0
+14 9 -11 0
+-16 -5 -3 0
+18 -10 15 0
+17 -4 9 0
+-15 17 13 0
+13 16 -17 0
+-15 -20 3 0
+-14 -11 -9 0
+-11 14 6 0
+8 1 20 0
+18 4 -2 0
+-1 5 14 0
+-4 17 -16 0
+8 1 18 0
+9 -6 -14 0
+5 -17 14 0
+7 3 20 0
+-6 1 -13 0
+16 -10 19 0
+7 -12 -20 0
+17 3 -14 0
+-9 -6 19 0
+-12 -4 -3 0
+9 -16 20 0
+18 12 6 0
+19 12 -15 0
+-14 10 17 0
+-17 -12 11 0
+-18 20 3 0
+4 14 -10 0
+4 -15 -6 0
+-2 5 14 0
+-11 17 8 0
+1 6 -13 0
+-18 19 1 0
+15 -16 -13 0
+-14 6 -8 0
+15 -18 -9 0
+10 17 -2 0
+-18 -10 19 0
+12 15 -1 0
+-13 -17 12 0
+-17 5 -10 0
+9 -3 -1 0
+7 4 -17 0
+-15 17 14 0
+9 -17 -19 0
+-7 13 -19 0
+-15 14 -3 0
+-14 -10 20 0
+10 8 19 0
+7 -12 -19 0
+-20 -19 -8 0
+-18 10 7 0
+-16 18 -19 0
+-17 19 20 0
+-17 -9 14 0
+-11 -13 -5 0
+-11 8 -9 0
+7 -4 -11 0
+-16 14 -17 0
+-17 5 7 0
+17 12 13 0
+-20 -11 8 0
+3 -1 11 0
+-3 13 7 0
+14 6 -13 0
+1 18 5 0
+1 6 -18 0
+-9 -4 -16 0
+-9 13 7 0
+-20 4 -13 0
+5 9 16 0
+-16 -10 7 0
+9 7 13 0
+19 14 16 0
+%
+0
+

tests/satlib/uf20-91/uf20-0130.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 4 -11 14 0
+-9 -8 -6 0
+9 -12 -14 0
+-10 -14 -20 0
+-7 -12 3 0
+6 -9 13 0
+-13 -18 20 0
+-3 10 15 0
+13 -2 15 0
+-18 10 7 0
+-6 10 -19 0
+-7 20 18 0
+7 2 -19 0
+11 1 -17 0
+19 8 -13 0
+13 19 -17 0
+-13 -1 17 0
+11 -3 -6 0
+-20 -3 -12 0
+-10 20 3 0
+-6 7 -18 0
+-5 8 -11 0
+-6 -7 -20 0
+14 -1 -2 0
+19 -3 13 0
+-2 -1 -8 0
+14 -17 2 0
+-18 -17 -13 0
+7 -4 13 0
+-3 -13 7 0
+17 -15 -2 0
+-18 -9 10 0
+-6 10 17 0
+10 14 11 0
+-7 -4 16 0
+-15 -4 17 0
+-16 -7 -20 0
+-1 -8 17 0
+-9 8 -15 0
+-17 -13 14 0
+5 7 1 0
+-1 12 10 0
+-17 -18 6 0
+4 19 -14 0
+-20 -16 1 0
+-18 -6 3 0
+-2 -5 -19 0
+10 20 -11 0
+1 -13 -8 0
+-8 10 19 0
+-17 14 11 0
+-2 -6 12 0
+15 7 -5 0
+19 -9 -6 0
+4 5 -9 0
+-7 -1 -11 0
+-4 -20 -15 0
+-14 -5 -4 0
+17 2 18 0
+10 -8 7 0
+-17 -12 5 0
+11 10 -4 0
+12 13 -16 0
+6 -11 -14 0
+-7 1 6 0
+19 -4 12 0
+-8 -5 17 0
+8 4 18 0
+15 -14 17 0
+-6 -4 -9 0
+12 -14 -19 0
+11 -4 18 0
+12 2 14 0
+-16 20 -15 0
+1 13 -16 0
+5 17 -3 0
+-11 -5 13 0
+-10 1 -15 0
+14 -5 12 0
+-7 5 19 0
+20 5 -14 0
+-19 -15 -11 0
+-2 17 8 0
+-14 -7 -15 0
+6 -3 17 0
+1 -15 -20 0
+-2 15 12 0
+-6 9 5 0
+-17 2 -14 0
+10 7 15 0
+-12 -9 -20 0
+%
+0
+

tests/satlib/uf20-91/uf20-0131.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -20 -2 16 0
+-6 5 -14 0
+12 16 -14 0
+-20 -6 4 0
+14 -20 -15 0
+-8 -20 -6 0
+5 19 -6 0
+12 19 -6 0
+-2 -7 20 0
+-6 -17 18 0
+2 14 8 0
+11 -6 10 0
+19 -4 -11 0
+7 19 5 0
+-20 19 4 0
+-8 20 -7 0
+-2 15 -19 0
+20 -2 11 0
+-8 -18 -7 0
+12 17 1 0
+12 2 14 0
+-9 2 5 0
+20 5 -1 0
+-12 14 -17 0
+-15 17 -13 0
+-1 -14 17 0
+20 9 5 0
+5 -8 -13 0
+4 9 -12 0
+17 -1 -14 0
+-3 16 8 0
+3 -10 16 0
+15 18 12 0
+-5 6 17 0
+13 2 -4 0
+1 -13 15 0
+-16 15 13 0
+15 3 -6 0
+6 -10 -11 0
+14 -17 -20 0
+-19 -10 8 0
+5 -6 14 0
+-1 14 2 0
+-8 18 -2 0
+8 2 5 0
+12 -10 -15 0
+11 -6 5 0
+-16 -7 14 0
+11 2 3 0
+9 5 12 0
+15 3 -8 0
+12 -7 -20 0
+12 -19 9 0
+-16 -13 -11 0
+-7 20 16 0
+1 20 7 0
+7 18 16 0
+1 -14 -6 0
+17 -15 10 0
+-18 -6 -14 0
+16 -11 -5 0
+-10 -16 -8 0
+16 12 -20 0
+2 -4 -7 0
+-7 13 18 0
+18 3 -20 0
+15 -17 12 0
+-17 -8 -1 0
+14 13 15 0
+13 8 2 0
+-19 4 -12 0
+14 20 15 0
+-14 18 15 0
+8 -19 20 0
+-11 10 -14 0
+12 -5 3 0
+-4 3 10 0
+-11 15 9 0
+15 9 -7 0
+-13 18 7 0
+-4 10 6 0
+17 11 10 0
+-10 -19 4 0
+-6 -8 14 0
+-5 -4 20 0
+15 -19 14 0
+-8 -12 18 0
+4 -18 -12 0
+-8 19 -11 0
+4 -13 15 0
+-6 -10 -11 0
+%
+0
+

tests/satlib/uf20-91/uf20-0132.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 14 6 17 0
+-20 18 -4 0
+15 -13 5 0
+7 18 20 0
+17 11 -20 0
+-1 15 3 0
+2 -1 5 0
+20 6 1 0
+7 16 19 0
+-12 18 -15 0
+8 5 9 0
+17 3 10 0
+-10 -7 -11 0
+-12 -9 -2 0
+-11 8 -4 0
+-19 -11 -20 0
+2 -10 17 0
+-16 17 6 0
+4 -15 17 0
+-15 20 -1 0
+7 10 -18 0
+16 2 8 0
+3 -9 -16 0
+3 14 15 0
+-4 -10 2 0
+-6 -9 -18 0
+-8 15 5 0
+-18 -5 17 0
+11 15 -1 0
+7 8 -20 0
+8 14 -7 0
+3 13 -15 0
+-16 -5 -1 0
+-20 -7 -8 0
+11 19 20 0
+-8 -14 20 0
+14 2 18 0
+4 -5 9 0
+17 -16 12 0
+-16 -6 3 0
+-3 -1 2 0
+-11 1 5 0
+2 -15 18 0
+4 7 -15 0
+-4 8 1 0
+1 6 9 0
+-10 -13 -9 0
+-3 13 1 0
+2 -10 -19 0
+-12 20 18 0
+-11 8 16 0
+-3 -13 -17 0
+5 4 1 0
+-5 17 -2 0
+-5 -9 17 0
+-7 19 18 0
+-3 11 14 0
+-18 -8 -7 0
+2 15 -10 0
+-3 12 -6 0
+-2 -13 15 0
+-20 -15 -14 0
+17 11 -4 0
+17 -10 -9 0
+3 -15 -7 0
+-5 -16 -6 0
+-3 15 12 0
+-13 4 14 0
+-11 4 12 0
+14 -12 -20 0
+-13 4 9 0
+16 6 17 0
+11 -15 -8 0
+-6 3 19 0
+2 -16 -18 0
+14 9 2 0
+5 2 -11 0
+-5 19 -7 0
+8 9 1 0
+13 8 -18 0
+7 2 1 0
+13 8 -9 0
+15 -13 -2 0
+-14 -6 1 0
+12 18 -20 0
+-8 7 -13 0
+-9 17 8 0
+6 18 -20 0
+6 -17 -2 0
+8 7 -10 0
+-19 -16 -1 0
+%
+0
+

tests/satlib/uf20-91/uf20-0133.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -19 -5 15 0
+8 1 11 0
+9 -16 1 0
+-12 -14 20 0
+20 8 -12 0
+12 5 -10 0
+-9 -13 -7 0
+3 10 17 0
+-20 -18 4 0
+19 -12 16 0
+20 -9 -10 0
+-6 9 13 0
+2 -13 5 0
+10 14 13 0
+-7 17 -16 0
+-3 12 -5 0
+6 -16 -3 0
+-7 11 16 0
+-7 1 -17 0
+-1 -2 -14 0
+-13 -18 -7 0
+-8 3 9 0
+-2 -15 17 0
+-2 -19 3 0
+16 14 9 0
+-5 -3 -2 0
+-5 -8 2 0
+-19 -20 -4 0
+-18 14 1 0
+-11 20 17 0
+-5 -12 -2 0
+-20 -19 -2 0
+12 -17 14 0
+5 10 3 0
+13 -16 -8 0
+-11 -1 -8 0
+-12 16 -19 0
+-4 20 12 0
+6 -11 -14 0
+17 -9 15 0
+20 -9 11 0
+7 12 2 0
+-20 9 -10 0
+14 -12 6 0
+6 -16 9 0
+11 18 -15 0
+6 -11 -7 0
+17 14 20 0
+2 19 -16 0
+-8 -12 11 0
+-4 2 -7 0
+-13 -8 -3 0
+-11 -12 -18 0
+-14 12 -6 0
+11 17 -10 0
+5 13 11 0
+15 6 -3 0
+-2 14 -4 0
+18 3 -11 0
+16 -13 -14 0
+18 20 -11 0
+-11 -2 20 0
+-8 -13 17 0
+11 -9 8 0
+-18 -7 -2 0
+10 -9 17 0
+-15 7 -6 0
+-18 -8 9 0
+19 9 -7 0
+7 18 -15 0
+8 2 16 0
+-18 -10 17 0
+9 16 -6 0
+14 15 10 0
+19 -2 -7 0
+-6 9 -17 0
+4 5 -10 0
+17 16 -6 0
+-15 4 -9 0
+15 3 17 0
+-15 13 19 0
+-6 -11 12 0
+-13 8 17 0
+17 -4 -10 0
+-1 -15 16 0
+7 11 15 0
+12 8 13 0
+6 -16 -12 0
+-9 -10 3 0
+12 -15 -16 0
+10 19 1 0
+%
+0
+

tests/satlib/uf20-91/uf20-0134.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 11 17 -9 0
+-15 -16 1 0
+-7 -12 14 0
+8 -19 -1 0
+20 -3 -5 0
+20 7 -4 0
+-19 4 15 0
+4 -15 -18 0
+-11 12 -1 0
+-14 -9 -3 0
+-13 -16 20 0
+10 -19 -12 0
+10 20 7 0
+13 15 7 0
+-20 12 9 0
+11 5 2 0
+-16 -3 -1 0
+-9 -17 5 0
+2 -12 3 0
+-14 18 3 0
+-6 -10 11 0
+-16 15 -6 0
+11 15 -10 0
+-1 -5 -19 0
+-17 -8 -15 0
+17 -3 -4 0
+-13 11 12 0
+12 15 -16 0
+11 5 -3 0
+-1 -20 -16 0
+-7 -16 -19 0
+7 2 9 0
+-15 20 6 0
+-6 -8 -15 0
+10 -19 11 0
+-8 -4 1 0
+20 -8 11 0
+5 3 1 0
+16 11 -20 0
+-16 -9 -6 0
+3 7 -15 0
+11 4 -3 0
+7 14 3 0
+-12 17 19 0
+-7 -18 -16 0
+-3 16 -18 0
+-10 -11 -15 0
+-17 13 -4 0
+-11 -3 -7 0
+10 7 4 0
+-20 -5 -4 0
+-9 3 11 0
+-17 16 2 0
+15 -20 -8 0
+-13 2 5 0
+3 4 12 0
+-3 -12 6 0
+-18 8 -4 0
+-4 2 12 0
+-10 -15 5 0
+-1 -13 -14 0
+-15 -2 -8 0
+-8 12 -6 0
+-3 13 -14 0
+18 14 -10 0
+12 9 -13 0
+1 -15 14 0
+-7 -3 19 0
+-5 -17 20 0
+13 -9 18 0
+2 -15 14 0
+-8 10 19 0
+-3 -7 -4 0
+-19 17 -11 0
+-9 16 -13 0
+13 -7 12 0
+11 -1 -16 0
+-15 -20 6 0
+-9 12 3 0
+15 17 5 0
+-6 20 17 0
+-4 16 11 0
+18 -20 7 0
+-10 7 13 0
+2 18 -6 0
+-14 5 12 0
+-14 -6 -12 0
+-10 11 7 0
+-4 15 -20 0
+17 2 -3 0
+-4 -7 9 0
+%
+0
+

tests/satlib/uf20-91/uf20-0135.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 3 -1 -15 0
+3 -2 1 0
+14 -2 -15 0
+7 18 16 0
+-12 -8 -10 0
+18 -1 12 0
+-9 17 -5 0
+-4 -11 8 0
+20 9 3 0
+-18 -17 -16 0
+15 16 11 0
+-11 -9 -2 0
+-8 -3 16 0
+15 -1 5 0
+-18 7 -6 0
+-9 -17 15 0
+6 16 20 0
+7 9 3 0
+-17 -3 -9 0
+14 20 4 0
+-17 -18 10 0
+-18 20 19 0
+4 -12 -15 0
+-11 10 -18 0
+18 1 -10 0
+-3 -6 8 0
+-16 -15 2 0
+-19 15 17 0
+9 11 20 0
+17 6 -7 0
+17 10 -1 0
+6 -17 12 0
+12 10 -17 0
+-19 -11 -8 0
+4 -13 2 0
+5 -16 -18 0
+-3 -5 16 0
+-16 -3 -15 0
+-10 9 7 0
+-13 11 -17 0
+3 5 11 0
+-20 12 15 0
+-1 -8 -15 0
+-3 -7 18 0
+12 4 -17 0
+9 -8 -3 0
+-9 -8 3 0
+15 -20 18 0
+-11 -5 6 0
+2 1 -4 0
+17 12 -19 0
+-14 -17 18 0
+-20 -5 10 0
+-6 -4 12 0
+18 16 -10 0
+-17 19 -4 0
+6 -18 -9 0
+13 -14 -4 0
+10 16 -20 0
+-10 6 -8 0
+-12 -4 -9 0
+-8 4 11 0
+-16 19 18 0
+-16 -11 -5 0
+-7 2 17 0
+-5 12 6 0
+-6 -15 -7 0
+-20 7 -12 0
+6 -2 -4 0
+-1 -3 -17 0
+20 -1 -9 0
+-10 -20 11 0
+-9 -16 -1 0
+19 -16 -17 0
+9 13 6 0
+11 14 12 0
+-5 19 17 0
+16 9 -6 0
+-7 19 16 0
+-3 -15 -9 0
+3 13 6 0
+-11 20 3 0
+-6 -10 -14 0
+-1 12 -8 0
+18 -4 9 0
+20 19 1 0
+-11 16 2 0
+-1 11 12 0
+-7 -5 -16 0
+-8 18 -1 0
+5 3 -15 0
+%
+0
+

tests/satlib/uf20-91/uf20-0136.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 14 2 -12 0
+10 5 17 0
+-20 -12 -6 0
+-7 -10 11 0
+-18 -7 -4 0
+-13 7 19 0
+-9 6 -17 0
+-5 13 -10 0
+-6 19 7 0
+-3 11 -4 0
+5 -13 15 0
+13 -6 -9 0
+-6 -4 -8 0
+-11 -4 14 0
+3 -2 -11 0
+-2 20 9 0
+19 16 11 0
+2 10 -12 0
+-4 -16 -14 0
+17 16 15 0
+-4 -3 -9 0
+17 18 -8 0
+16 -7 3 0
+-18 -19 -4 0
+-5 13 -12 0
+-10 -4 -16 0
+-11 -13 -12 0
+-11 16 -3 0
+20 -1 -17 0
+-20 -17 6 0
+-4 6 10 0
+14 -15 -18 0
+1 -3 -13 0
+-1 -15 16 0
+-10 16 5 0
+1 11 -7 0
+-15 3 -6 0
+10 -9 -20 0
+-18 12 8 0
+2 -19 1 0
+-7 14 17 0
+5 -18 -10 0
+7 1 -6 0
+20 -1 -8 0
+12 -15 1 0
+1 15 2 0
+-2 11 16 0
+13 8 -15 0
+-17 14 9 0
+-8 -16 -4 0
+-15 9 -13 0
+-19 1 -14 0
+-3 1 -5 0
+13 -7 5 0
+4 7 -6 0
+-19 -16 -8 0
+10 12 18 0
+19 5 -7 0
+-15 3 20 0
+19 8 -15 0
+-6 -4 -2 0
+6 8 17 0
+7 -15 9 0
+5 12 7 0
+12 -5 15 0
+1 -17 7 0
+-2 18 -10 0
+1 13 -15 0
+-13 7 2 0
+7 2 13 0
+-4 -9 -20 0
+-13 -9 3 0
+12 7 16 0
+-13 16 -9 0
+-18 -6 -9 0
+-3 -2 12 0
+5 -6 13 0
+9 8 13 0
+-11 -1 17 0
+15 10 7 0
+16 11 -3 0
+10 -8 -1 0
+9 3 -5 0
+4 -17 13 0
+2 -10 15 0
+-9 -13 11 0
+5 -4 6 0
+-16 1 -8 0
+1 -4 -13 0
+2 9 -12 0
+18 11 7 0
+%
+0
+

tests/satlib/uf20-91/uf20-0137.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -15 14 16 0
+4 -17 -9 0
+-19 -7 -11 0
+9 -1 -12 0
+-14 -12 -2 0
+14 -10 -8 0
+-11 15 -4 0
+18 -15 -4 0
+-20 2 15 0
+-2 -17 -3 0
+-9 3 -2 0
+8 15 -20 0
+-3 17 -1 0
+-10 -11 1 0
+11 12 -5 0
+-15 8 -1 0
+19 2 -16 0
+-7 20 14 0
+7 -20 -19 0
+-9 4 5 0
+-11 -5 18 0
+8 -15 -7 0
+16 5 -11 0
+-18 -7 -19 0
+-9 -2 16 0
+4 -6 10 0
+-6 4 -1 0
+3 -13 11 0
+10 11 -4 0
+6 18 20 0
+-13 -10 2 0
+-19 8 -12 0
+19 -3 -5 0
+-11 5 17 0
+-20 4 14 0
+4 -19 13 0
+-10 16 -1 0
+-11 7 -19 0
+-3 -6 -8 0
+16 -10 -14 0
+-1 -6 -2 0
+14 -9 12 0
+16 1 -5 0
+9 -7 -4 0
+-1 -14 10 0
+-12 -17 8 0
+-4 -8 10 0
+1 -8 4 0
+2 4 12 0
+-6 9 -4 0
+17 16 4 0
+12 18 -15 0
+-8 -18 1 0
+-15 16 17 0
+-6 -13 9 0
+-16 -12 -3 0
+-4 -11 -10 0
+-15 -5 17 0
+-1 -12 4 0
+-3 -17 -20 0
+19 -12 8 0
+-14 -18 3 0
+-6 19 2 0
+-7 -11 20 0
+-15 -19 -14 0
+2 14 13 0
+-5 -10 18 0
+-19 -10 5 0
+-1 8 6 0
+13 -4 -1 0
+-5 20 -6 0
+4 -12 -2 0
+5 10 -3 0
+16 4 -6 0
+-9 -15 10 0
+-3 -12 8 0
+3 -10 4 0
+-11 -17 -14 0
+-2 13 -20 0
+-7 -11 -13 0
+11 1 -15 0
+-19 -3 20 0
+10 -15 -4 0
+-1 12 8 0
+14 11 -20 0
+-1 20 -13 0
+-12 8 -17 0
+19 -17 -10 0
+18 -20 -11 0
+-14 -13 -5 0
+-5 -20 14 0
+%
+0
+

tests/satlib/uf20-91/uf20-0138.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 11 -19 -17 0
+-5 -16 -7 0
+-8 10 -18 0
+1 -4 10 0
+20 10 17 0
+16 -19 -18 0
+9 13 -20 0
+15 17 9 0
+10 19 -17 0
+-12 1 -13 0
+-12 -1 11 0
+-5 -10 -2 0
+-7 13 15 0
+9 -1 11 0
+4 9 -20 0
+5 -12 -8 0
+12 -17 4 0
+-1 8 5 0
+-9 -11 10 0
+2 17 -14 0
+-13 6 8 0
+12 -19 15 0
+-8 -1 11 0
+-6 14 12 0
+17 -11 1 0
+-9 3 10 0
+-15 -9 1 0
+7 -3 -12 0
+-9 12 -7 0
+-5 7 -6 0
+3 5 2 0
+-17 15 -10 0
+2 13 -3 0
+-13 2 -1 0
+17 13 4 0
+-15 -9 -11 0
+-6 8 12 0
+6 4 14 0
+3 -19 -5 0
+1 7 -6 0
+10 -3 -1 0
+-18 -4 -10 0
+-4 3 5 0
+-14 -9 13 0
+18 -6 12 0
+-12 -17 -3 0
+-10 -19 -12 0
+-10 -1 14 0
+-2 6 -12 0
+-20 1 -17 0
+14 9 17 0
+-15 -2 14 0
+-20 6 -16 0
+-17 -2 -11 0
+19 9 -1 0
+-14 -9 11 0
+-14 -3 7 0
+11 1 4 0
+-18 11 12 0
+-16 -12 -3 0
+10 -1 9 0
+1 -6 12 0
+-15 8 -7 0
+-20 8 7 0
+-14 -19 -2 0
+14 -4 15 0
+-11 12 3 0
+-14 17 15 0
+12 -13 17 0
+-17 15 9 0
+6 13 17 0
+19 -15 14 0
+9 -7 19 0
+13 -11 -17 0
+16 10 -8 0
+7 -8 -9 0
+-5 -14 -7 0
+-1 3 7 0
+-3 19 15 0
+-12 5 -18 0
+16 -15 8 0
+16 2 -17 0
+3 2 -14 0
+13 4 19 0
+-16 -14 -11 0
+-14 -8 1 0
+-8 -12 -20 0
+13 -14 4 0
+15 -18 2 0
+-18 14 -19 0
+5 14 11 0
+%
+0
+

tests/satlib/uf20-91/uf20-0139.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 12 -6 -4 0
+10 -15 -11 0
+7 18 13 0
+-12 20 8 0
+-1 -7 -10 0
+-16 -12 -1 0
+11 -8 10 0
+14 2 5 0
+-9 -20 -8 0
+1 18 -20 0
+5 12 6 0
+-14 -18 -10 0
+-8 14 1 0
+-2 -1 -18 0
+18 15 -11 0
+-12 -9 -2 0
+18 6 9 0
+4 8 -14 0
+-15 4 -16 0
+-2 19 -7 0
+3 -17 -20 0
+16 -11 -18 0
+6 3 -20 0
+-2 -10 9 0
+15 -9 -8 0
+-10 11 18 0
+-10 -16 7 0
+-20 16 -9 0
+13 -4 -5 0
+-3 -10 -4 0
+9 -5 -8 0
+16 9 7 0
+-5 -2 -16 0
+-9 -12 -2 0
+-8 16 7 0
+-8 15 7 0
+-8 -16 -14 0
+-15 -2 -17 0
+-8 4 9 0
+-5 17 -12 0
+-4 -16 1 0
+7 12 -20 0
+16 10 13 0
+14 8 -17 0
+-8 9 -14 0
+-13 7 11 0
+-20 -12 17 0
+15 -8 -14 0
+15 6 12 0
+-16 18 -2 0
+-7 -6 -1 0
+-3 -9 -19 0
+-3 7 -20 0
+1 -10 -6 0
+-4 -17 -16 0
+5 18 -16 0
+-18 -4 -14 0
+18 -17 -11 0
+-13 -18 20 0
+9 -8 20 0
+10 -17 6 0
+-4 -17 -19 0
+-13 11 -6 0
+-8 -19 -16 0
+-8 18 14 0
+-14 11 -10 0
+-4 -2 13 0
+11 6 13 0
+-14 -6 4 0
+-1 -15 19 0
+18 5 -12 0
+-1 7 -18 0
+-2 16 18 0
+2 15 10 0
+7 8 -1 0
+-5 18 -16 0
+12 -5 -7 0
+-1 -20 7 0
+2 16 -12 0
+-7 -16 18 0
+-17 -14 5 0
+4 12 -13 0
+-2 -9 -11 0
+-11 18 5 0
+18 -2 20 0
+-6 12 -14 0
+-2 -13 -10 0
+-8 -16 -1 0
+-11 -1 -14 0
+-17 -10 -1 0
+-4 5 -10 0
+%
+0
+

tests/satlib/uf20-91/uf20-014.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 14 -20 -11 0
+-9 4 -14 0
+-6 -7 -20 0
+-13 12 -9 0
+-9 -14 5 0
+13 -9 -2 0
+-1 -20 19 0
+-14 -17 13 0
+-9 6 1 0
+-10 11 -18 0
+-16 20 -2 0
+-12 -4 13 0
+17 11 -1 0
+-19 12 1 0
+3 -17 -12 0
+-14 6 -17 0
+-8 15 -3 0
+4 -1 -10 0
+-19 10 -4 0
+-1 -11 -9 0
+10 -5 4 0
+5 6 1 0
+-7 -9 -6 0
+-9 11 -6 0
+-4 10 -5 0
+-10 -20 -14 0
+1 5 -8 0
+18 12 -11 0
+1 14 -12 0
+-19 12 -6 0
+10 7 9 0
+-6 -9 -10 0
+-7 16 -6 0
+17 -6 -7 0
+2 -14 -5 0
+-3 2 18 0
+20 12 11 0
+4 11 10 0
+-5 14 10 0
+15 -2 -8 0
+-5 -16 -2 0
+-8 5 17 0
+20 18 -15 0
+-3 -11 12 0
+12 -2 -8 0
+20 -16 7 0
+14 -2 -7 0
+-17 18 -13 0
+11 -8 -4 0
+-8 -10 -19 0
+7 -14 15 0
+8 -2 -17 0
+3 9 -4 0
+-17 5 16 0
+-4 -1 18 0
+11 -12 -18 0
+13 -7 14 0
+3 15 -18 0
+-1 -20 4 0
+-19 -18 6 0
+-20 -6 -15 0
+10 -4 -20 0
+13 16 6 0
+-9 2 -13 0
+-16 -20 4 0
+12 -20 -2 0
+18 14 -1 0
+2 -10 -3 0
+5 7 4 0
+18 9 -5 0
+1 -3 12 0
+8 -7 20 0
+20 -13 -15 0
+-14 1 20 0
+20 18 -4 0
+-10 -3 -7 0
+-7 -2 -13 0
+-14 7 11 0
+10 -3 8 0
+-5 8 11 0
+4 11 13 0
+10 9 -18 0
+-17 -10 5 0
+-3 -15 11 0
+18 -4 -10 0
+15 2 -9 0
+12 -14 5 0
+3 14 16 0
+16 10 2 0
+-7 18 5 0
+14 1 4 0
+%
+0
+

tests/satlib/uf20-91/uf20-0140.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -5 -11 15 0
+-12 11 -15 0
+13 2 -18 0
+17 18 -7 0
+-14 -15 18 0
+7 -5 -19 0
+-2 11 -6 0
+-14 1 -13 0
+-7 5 -13 0
+8 -2 -12 0
+-14 1 -16 0
+-9 -4 -5 0
+5 14 -17 0
+10 -7 5 0
+-10 -16 13 0
+9 -11 -20 0
+10 -16 -19 0
+8 -9 6 0
+17 1 15 0
+-3 13 -5 0
+-20 -17 -5 0
+-13 9 11 0
+20 16 -8 0
+20 8 -10 0
+-4 -3 -2 0
+-18 8 -2 0
+-9 14 -10 0
+1 5 -13 0
+-4 8 -7 0
+-11 -12 19 0
+9 8 17 0
+-8 -13 17 0
+15 12 -7 0
+-6 -4 -3 0
+9 -8 -3 0
+-17 -9 1 0
+-16 6 17 0
+-14 18 -20 0
+-15 11 -4 0
+8 -11 7 0
+3 14 -15 0
+7 -2 19 0
+10 7 20 0
+-9 -1 -14 0
+-12 -6 7 0
+-6 17 -20 0
+6 -4 -12 0
+18 3 -13 0
+16 10 11 0
+-20 12 -13 0
+-4 -13 3 0
+-19 9 -16 0
+18 -15 -1 0
+15 3 5 0
+-13 -2 3 0
+3 11 10 0
+13 -4 -14 0
+2 16 11 0
+18 -16 -4 0
+6 10 -15 0
+14 -13 3 0
+9 -10 11 0
+19 20 5 0
+-11 -18 -2 0
+8 -5 -9 0
+-14 7 11 0
+3 -18 14 0
+20 -15 -8 0
+-19 -14 -16 0
+20 18 3 0
+15 16 -11 0
+13 3 -16 0
+-10 -3 6 0
+11 9 14 0
+1 2 -4 0
+-4 17 -9 0
+12 20 -17 0
+18 -16 -2 0
+-5 1 19 0
+-11 4 8 0
+16 3 10 0
+2 -10 -20 0
+7 11 -1 0
+-14 -8 -12 0
+9 19 4 0
+18 -8 -15 0
+-9 7 -19 0
+-3 -13 18 0
+-6 4 -3 0
+-13 -11 17 0
+-2 -10 9 0
+%
+0
+

tests/satlib/uf20-91/uf20-0141.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 15 12 -6 0
+-13 14 -15 0
+16 -12 14 0
+8 14 11 0
+14 9 13 0
+7 -14 -3 0
+-1 14 -6 0
+-8 5 -11 0
+3 17 4 0
+4 -10 1 0
+-12 -8 -15 0
+14 -4 -17 0
+17 -5 -13 0
+-18 2 5 0
+8 -10 12 0
+9 -6 18 0
+16 -19 -5 0
+-2 9 3 0
+-8 7 -2 0
+-20 -13 -12 0
+2 -19 13 0
+19 14 6 0
+-5 13 8 0
+-6 -8 -9 0
+18 -4 -19 0
+-5 20 12 0
+18 2 19 0
+-8 9 -17 0
+-2 -13 -6 0
+10 -8 -1 0
+-20 -2 -18 0
+-17 -16 1 0
+-19 6 -14 0
+-13 -3 12 0
+-15 -3 10 0
+-14 11 9 0
+-10 -18 -2 0
+16 12 6 0
+-8 -19 9 0
+-2 11 -4 0
+19 5 -8 0
+19 -4 -15 0
+-5 -8 20 0
+1 12 -14 0
+-3 18 -19 0
+14 -2 17 0
+14 -10 5 0
+3 -4 9 0
+8 -18 15 0
+-17 -2 20 0
+7 9 -4 0
+-5 3 -10 0
+-13 8 20 0
+3 -17 -4 0
+-3 18 15 0
+-7 4 -17 0
+3 19 10 0
+-14 -10 -18 0
+1 9 4 0
+4 6 -17 0
+9 10 -2 0
+-4 -11 -9 0
+-16 11 -7 0
+-13 -10 -7 0
+-19 -15 20 0
+-13 4 14 0
+-5 12 13 0
+-11 -19 1 0
+15 -4 19 0
+-16 -17 -4 0
+-19 -5 -3 0
+15 -4 2 0
+-17 7 -5 0
+6 -18 -20 0
+14 16 -18 0
+-8 -12 19 0
+14 -15 -11 0
+-17 -18 -1 0
+19 -18 -16 0
+-18 -11 -9 0
+11 6 -8 0
+18 -20 14 0
+5 16 2 0
+-1 -8 -19 0
+-10 9 5 0
+14 -9 -1 0
+-1 -14 -9 0
+-9 20 -18 0
+-6 -20 15 0
+6 20 -2 0
+3 12 -16 0
+%
+0
+

tests/satlib/uf20-91/uf20-0142.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -11 -6 -15 0
+-2 16 8 0
+19 8 4 0
+-6 5 17 0
+3 9 15 0
+-20 13 9 0
+-10 6 -4 0
+1 2 4 0
+12 -9 4 0
+-9 7 3 0
+11 2 14 0
+14 -12 -5 0
+-10 17 18 0
+1 15 10 0
+-13 -9 14 0
+-20 -10 4 0
+-15 -6 -2 0
+-16 -6 -14 0
+15 1 -11 0
+12 -17 -20 0
+9 12 -5 0
+7 -3 -18 0
+8 13 7 0
+-8 19 -5 0
+9 -3 -1 0
+-16 3 -17 0
+3 7 13 0
+13 18 -12 0
+-8 -4 -17 0
+9 2 16 0
+-1 -3 -9 0
+13 2 19 0
+12 -19 2 0
+-16 7 11 0
+7 15 -5 0
+-8 4 -16 0
+8 -14 16 0
+-10 -11 -1 0
+18 11 -6 0
+-12 -9 6 0
+8 -18 -12 0
+-17 1 6 0
+-14 16 15 0
+-14 -4 19 0
+-12 -4 11 0
+-6 7 -19 0
+-10 -6 -13 0
+-20 12 15 0
+3 -20 -5 0
+-3 12 -20 0
+-14 -15 -5 0
+-5 -2 -19 0
+16 -9 -10 0
+-13 -15 -16 0
+16 -6 -13 0
+-3 9 15 0
+-20 -3 7 0
+11 15 13 0
+11 17 -2 0
+-19 -6 -1 0
+-1 -18 3 0
+-4 12 5 0
+-15 19 -7 0
+-10 20 15 0
+15 10 5 0
+-7 6 1 0
+-10 -14 15 0
+16 15 -18 0
+-4 -1 -6 0
+3 20 -9 0
+13 6 -2 0
+-5 -1 11 0
+-10 -11 -3 0
+-3 15 5 0
+19 -8 13 0
+-19 18 1 0
+14 13 -4 0
+-10 17 -12 0
+19 16 -14 0
+16 14 -19 0
+-6 1 16 0
+-6 8 13 0
+9 17 14 0
+-3 20 1 0
+9 2 -14 0
+-3 15 -16 0
+7 -14 20 0
+-15 -11 19 0
+-11 1 17 0
+20 15 -12 0
+4 -13 12 0
+%
+0
+

tests/satlib/uf20-91/uf20-0143.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -1 -2 -20 0
+-6 18 -9 0
+-17 -11 6 0
+-4 1 2 0
+12 16 8 0
+-18 -7 3 0
+14 5 19 0
+19 17 12 0
+5 11 6 0
+15 -18 3 0
+3 -18 -15 0
+7 9 -18 0
+-6 -9 15 0
+2 17 -12 0
+-15 17 19 0
+13 -20 -7 0
+17 12 -7 0
+4 19 8 0
+-18 8 7 0
+10 20 2 0
+17 -5 10 0
+1 -9 19 0
+1 2 20 0
+-13 -5 -9 0
+-3 -10 5 0
+-11 -19 -17 0
+15 6 -18 0
+-3 -5 -18 0
+3 -16 -7 0
+-4 7 -8 0
+8 -20 -12 0
+-17 1 8 0
+-20 -9 4 0
+-13 16 9 0
+18 -14 -13 0
+-1 -18 13 0
+-4 -16 -9 0
+17 14 1 0
+3 16 -12 0
+-7 19 11 0
+13 7 18 0
+-9 -2 15 0
+-16 -9 8 0
+-20 -9 4 0
+-9 -5 -8 0
+4 -10 3 0
+7 3 11 0
+-9 -18 15 0
+4 14 -15 0
+17 -14 -18 0
+20 -17 -4 0
+11 5 2 0
+7 -15 -2 0
+8 14 -9 0
+-15 19 -6 0
+6 2 -15 0
+8 -16 18 0
+-13 4 18 0
+-10 -12 2 0
+-11 -7 2 0
+15 -4 5 0
+3 1 5 0
+4 -3 5 0
+9 7 -20 0
+-13 -15 -20 0
+17 -7 -1 0
+-11 -20 14 0
+17 3 5 0
+10 11 -8 0
+2 13 -7 0
+-19 3 5 0
+13 14 -1 0
+-8 6 2 0
+14 17 -16 0
+14 7 -9 0
+19 7 -17 0
+5 18 14 0
+5 10 -9 0
+-11 -17 6 0
+-12 -3 11 0
+-11 18 2 0
+19 20 -15 0
+-7 -12 6 0
+3 11 -9 0
+-20 10 1 0
+-1 18 6 0
+-13 1 -2 0
+-3 15 5 0
+18 19 16 0
+-17 -7 -13 0
+2 -18 -11 0
+%
+0
+

tests/satlib/uf20-91/uf20-0144.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -17 -8 -1 0
+-14 -18 -10 0
+12 16 1 0
+-14 17 -5 0
+-19 20 8 0
+15 14 -4 0
+-2 8 9 0
+-4 -18 5 0
+-8 13 4 0
+2 4 -7 0
+-12 16 -7 0
+15 -5 4 0
+-7 -1 4 0
+18 -1 -15 0
+-8 14 3 0
+-6 14 20 0
+-9 3 8 0
+18 12 -5 0
+-4 20 -19 0
+-18 9 5 0
+3 -8 20 0
+-5 9 -12 0
+16 -19 9 0
+-19 4 -10 0
+-8 -19 -12 0
+1 7 18 0
+-8 -16 -18 0
+-16 -15 -3 0
+-14 -18 -3 0
+-18 11 9 0
+-16 17 -5 0
+6 -19 10 0
+-1 9 -7 0
+-9 -20 -1 0
+17 15 -4 0
+-13 5 -10 0
+-9 12 18 0
+-14 8 -9 0
+-15 8 -17 0
+-8 -4 -19 0
+2 -5 -8 0
+-14 -9 7 0
+8 2 9 0
+-19 -15 -4 0
+-18 16 -15 0
+-19 -15 -1 0
+-4 1 18 0
+20 -10 8 0
+-2 -20 -17 0
+15 -12 9 0
+7 13 -6 0
+6 8 -19 0
+-8 5 16 0
+14 -4 -19 0
+-4 -12 3 0
+-19 4 -12 0
+6 -14 10 0
+-18 -4 -16 0
+-15 -9 4 0
+7 -2 15 0
+16 -12 -8 0
+18 17 8 0
+-15 -4 11 0
+-11 -14 -5 0
+13 -11 -20 0
+-17 3 8 0
+-5 7 -11 0
+3 12 10 0
+-2 -15 -5 0
+-6 -2 -16 0
+-8 -20 -14 0
+20 -2 1 0
+-4 16 -14 0
+-14 -5 11 0
+-15 -2 -3 0
+-2 -1 -18 0
+10 -15 5 0
+3 5 -2 0
+10 -11 13 0
+9 -15 -18 0
+-2 11 16 0
+-11 20 14 0
+4 -10 -11 0
+-20 -5 -1 0
+20 -7 -18 0
+-2 -11 -13 0
+9 14 -11 0
+-8 11 -6 0
+12 17 4 0
+2 -16 -1 0
+4 -6 10 0
+%
+0
+

tests/satlib/uf20-91/uf20-0145.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -1 17 11 0
+19 11 1 0
+-11 15 -16 0
+-19 6 -1 0
+-20 16 -9 0
+10 -9 16 0
+3 -19 -16 0
+7 -11 -2 0
+-2 -3 -20 0
+-19 7 18 0
+3 1 8 0
+1 -20 -12 0
+-11 7 -20 0
+-16 -7 -18 0
+-13 -4 3 0
+18 2 -8 0
+15 5 12 0
+4 16 -15 0
+-2 5 -20 0
+12 7 18 0
+19 -7 13 0
+18 -15 17 0
+-7 16 -19 0
+-12 9 3 0
+6 20 -11 0
+9 20 -2 0
+5 1 7 0
+6 12 2 0
+3 13 14 0
+-10 1 -20 0
+2 17 5 0
+15 -8 10 0
+2 19 -3 0
+1 -6 20 0
+3 15 2 0
+-6 -7 -5 0
+16 9 -19 0
+7 -11 -12 0
+-5 -18 -4 0
+3 -8 -15 0
+13 -4 -2 0
+19 -7 11 0
+11 7 15 0
+5 -2 9 0
+-4 5 -16 0
+3 5 15 0
+4 9 17 0
+-19 -11 15 0
+-4 -16 5 0
+14 -20 6 0
+-3 -14 -12 0
+3 -20 10 0
+-19 -15 -8 0
+8 20 -4 0
+-5 8 15 0
+7 6 1 0
+9 18 11 0
+-3 14 2 0
+-17 9 -14 0
+6 15 -12 0
+7 -11 -5 0
+-10 -8 -11 0
+9 -19 -12 0
+-19 -13 -6 0
+10 -17 -7 0
+-1 4 -6 0
+-20 8 10 0
+-9 -3 -18 0
+17 11 -19 0
+-19 17 -20 0
+17 8 6 0
+8 -16 -13 0
+-16 3 17 0
+-10 -11 -9 0
+16 8 -15 0
+18 -11 20 0
+-13 -14 -16 0
+15 -16 11 0
+-17 -7 9 0
+10 5 3 0
+-19 4 -15 0
+-3 2 -7 0
+13 15 -16 0
+-4 -18 -12 0
+1 20 5 0
+-9 -1 3 0
+-19 -20 -3 0
+-13 15 18 0
+11 -4 -12 0
+2 18 -12 0
+-10 12 -18 0
+%
+0
+

tests/satlib/uf20-91/uf20-0146.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 5 7 -12 0
+18 3 14 0
+4 -8 -10 0
+-9 -16 1 0
+-9 7 -5 0
+1 -17 -5 0
+-19 2 20 0
+1 6 -13 0
+3 -16 6 0
+4 13 9 0
+2 -18 6 0
+-2 -18 4 0
+14 -4 -1 0
+6 7 17 0
+13 6 -15 0
+3 7 -14 0
+-12 11 8 0
+3 19 10 0
+-15 -8 7 0
+-14 9 -10 0
+-6 19 -20 0
+6 16 11 0
+-12 -11 -7 0
+15 7 -12 0
+13 20 4 0
+-3 1 11 0
+19 16 -9 0
+20 -15 12 0
+-4 -8 -17 0
+-14 4 17 0
+-1 10 2 0
+18 3 6 0
+-9 -3 17 0
+-17 -4 -2 0
+6 18 -15 0
+-3 -15 18 0
+-11 1 -8 0
+-2 18 12 0
+16 6 20 0
+-8 -19 13 0
+-13 -4 6 0
+6 -11 -15 0
+18 -11 -4 0
+-5 20 -12 0
+-2 -3 15 0
+9 -17 -7 0
+-12 -2 8 0
+-9 -5 -4 0
+-4 18 8 0
+-20 -3 -6 0
+16 -8 15 0
+15 -6 8 0
+3 6 7 0
+2 8 4 0
+-12 -4 7 0
+-16 -13 14 0
+16 -10 13 0
+-5 -14 -16 0
+-17 1 -7 0
+-5 -2 -15 0
+17 15 -5 0
+17 20 -9 0
+-20 -8 -13 0
+15 -16 13 0
+12 -20 5 0
+19 -7 17 0
+-3 14 1 0
+10 -3 11 0
+14 -12 6 0
+-9 -5 -1 0
+-16 -11 -18 0
+-14 17 7 0
+18 -17 13 0
+18 -14 -2 0
+5 9 19 0
+-17 -18 -20 0
+-8 -4 -10 0
+-4 16 -14 0
+6 2 -7 0
+-10 -14 18 0
+11 13 8 0
+12 7 10 0
+9 -20 5 0
+5 18 -16 0
+-19 -17 14 0
+4 5 8 0
+-19 15 -4 0
+20 -5 17 0
+-8 -14 -2 0
+16 13 -11 0
+-12 -9 19 0
+%
+0
+

tests/satlib/uf20-91/uf20-0147.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -4 -7 2 0
+14 1 19 0
+-10 12 -6 0
+17 -12 15 0
+3 -20 13 0
+2 -3 12 0
+11 -9 17 0
+1 4 -20 0
+-15 17 18 0
+-14 18 2 0
+-15 14 -6 0
+-3 -9 5 0
+5 19 7 0
+-20 16 6 0
+-18 -4 8 0
+2 11 8 0
+5 11 -9 0
+-8 7 17 0
+12 -4 11 0
+7 -17 -8 0
+-8 3 19 0
+19 -10 -12 0
+-18 -1 -6 0
+20 -4 16 0
+-10 19 -6 0
+-13 12 1 0
+12 -6 15 0
+2 11 -8 0
+-20 -4 -3 0
+5 -3 -14 0
+8 12 -10 0
+-14 -2 -9 0
+18 5 3 0
+-4 13 5 0
+-4 9 -15 0
+2 20 -3 0
+-4 -16 -1 0
+8 -10 20 0
+-12 -18 2 0
+-17 -2 16 0
+4 16 2 0
+4 9 -20 0
+-19 -8 -1 0
+7 10 12 0
+-16 -3 10 0
+-14 17 1 0
+-19 6 -15 0
+-9 3 -7 0
+-9 15 -2 0
+-18 -12 -7 0
+8 17 -15 0
+16 -17 -11 0
+-14 -8 -20 0
+-3 5 -15 0
+14 -19 -18 0
+12 -1 13 0
+-15 -2 -20 0
+-2 15 7 0
+17 -3 -6 0
+-3 10 -4 0
+9 19 -17 0
+-11 -18 14 0
+-4 14 -3 0
+20 3 13 0
+4 9 16 0
+-3 -15 1 0
+12 -6 -2 0
+-14 20 -6 0
+-8 -9 -14 0
+6 18 -9 0
+3 8 9 0
+7 19 10 0
+1 -17 -6 0
+-18 1 -4 0
+-12 6 -14 0
+15 -10 -7 0
+-7 19 -12 0
+3 -8 12 0
+3 12 5 0
+-3 -15 -11 0
+15 -9 -7 0
+14 -19 18 0
+-20 18 12 0
+-15 -9 -16 0
+-5 -17 14 0
+-14 8 17 0
+-19 2 6 0
+-1 -6 19 0
+-18 -12 13 0
+13 -16 -3 0
+14 5 -4 0
+%
+0
+

tests/satlib/uf20-91/uf20-0148.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 16 -13 10 0
+-19 -10 -14 0
+12 2 8 0
+-14 -15 3 0
+8 -14 -18 0
+19 12 -13 0
+17 -19 -20 0
+-7 -10 17 0
+-17 11 15 0
+-19 -17 -4 0
+17 18 -12 0
+-20 -3 11 0
+-14 -19 -11 0
+8 -7 -5 0
+5 -14 -18 0
+17 -11 10 0
+5 -19 13 0
+17 10 -1 0
+18 -10 -3 0
+-17 20 14 0
+12 18 -16 0
+-4 -8 11 0
+-18 -8 -12 0
+-14 -12 -2 0
+16 10 -18 0
+-15 -16 11 0
+-1 -6 -14 0
+-14 -4 -7 0
+4 9 -2 0
+17 -12 -16 0
+-1 12 10 0
+14 9 8 0
+18 -13 10 0
+-12 20 10 0
+-9 14 -5 0
+14 20 -8 0
+19 17 -9 0
+-10 19 11 0
+-8 -19 1 0
+5 -19 15 0
+-7 -6 -3 0
+-10 -9 8 0
+17 5 -7 0
+9 10 12 0
+10 -12 -20 0
+8 7 17 0
+1 11 -16 0
+17 -6 -15 0
+17 1 -7 0
+10 19 5 0
+2 -11 19 0
+-1 -3 10 0
+17 6 9 0
+10 14 -19 0
+-7 -14 -1 0
+-2 -13 -11 0
+16 19 1 0
+-3 -16 15 0
+-1 -9 -15 0
+-16 19 12 0
+-7 11 -19 0
+8 20 15 0
+14 -9 -19 0
+9 -20 -6 0
+-1 15 -12 0
+-17 -15 -16 0
+2 19 7 0
+-3 -13 9 0
+20 11 12 0
+-2 4 -14 0
+11 2 -6 0
+5 -19 -14 0
+15 3 7 0
+17 20 8 0
+9 -12 -3 0
+-13 1 -19 0
+1 -19 -15 0
+16 17 -2 0
+-6 -10 -4 0
+5 -2 14 0
+4 13 3 0
+3 10 17 0
+20 1 4 0
+19 12 -17 0
+15 -10 -17 0
+-15 -16 -4 0
+-19 2 3 0
+3 6 -7 0
+13 6 5 0
+4 2 18 0
+-12 5 6 0
+%
+0
+

tests/satlib/uf20-91/uf20-0149.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 10 16 4 0
+-6 9 -11 0
+4 20 -14 0
+-1 13 17 0
+-18 -3 17 0
+-14 1 -5 0
+19 8 20 0
+-5 -7 -6 0
+-16 13 4 0
+-18 3 -7 0
+4 -14 -18 0
+-20 -10 6 0
+-7 -3 17 0
+3 16 1 0
+-10 -4 9 0
+-14 1 -4 0
+-10 9 3 0
+5 16 3 0
+9 -10 19 0
+16 6 9 0
+-14 16 -8 0
+-11 -16 -6 0
+-15 -10 18 0
+-5 6 19 0
+-10 -8 -13 0
+-8 6 -5 0
+8 10 -18 0
+11 1 -8 0
+-13 20 -6 0
+-3 -15 -9 0
+19 -1 -11 0
+8 6 17 0
+20 -10 16 0
+-19 -10 13 0
+-16 -7 9 0
+-18 14 -19 0
+-7 15 13 0
+16 14 18 0
+-1 14 18 0
+-10 -12 -1 0
+6 -10 4 0
+-14 -11 9 0
+-8 -12 6 0
+4 -14 20 0
+-1 -19 -8 0
+1 -18 -17 0
+-2 -3 11 0
+15 -5 -18 0
+6 19 8 0
+14 9 -5 0
+-14 1 13 0
+-8 11 9 0
+4 -16 10 0
+16 2 -4 0
+-10 1 20 0
+10 16 -1 0
+-7 -14 1 0
+20 -16 -18 0
+-14 -13 16 0
+9 -5 3 0
+9 7 20 0
+20 -16 19 0
+-3 -11 6 0
+14 -9 -11 0
+-14 -8 -11 0
+17 5 6 0
+-1 5 12 0
+-16 -7 -1 0
+12 -9 5 0
+-14 11 5 0
+-8 12 -10 0
+20 -1 -7 0
+-2 14 12 0
+-1 -5 18 0
+-4 -2 12 0
+9 -20 -11 0
+15 1 8 0
+-20 -19 5 0
+-20 -4 7 0
+17 -1 12 0
+-9 3 -20 0
+-7 4 -19 0
+-13 6 -5 0
+13 9 20 0
+-3 8 1 0
+-20 -5 6 0
+11 -2 -12 0
+9 3 13 0
+-13 16 -6 0
+-1 -11 -14 0
+10 -17 -3 0
+%
+0
+

tests/satlib/uf20-91/uf20-015.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -1 -10 -16 0
+-12 -20 6 0
+-2 -12 -17 0
+-19 12 -20 0
+8 18 -16 0
+4 13 20 0
+-19 -5 -16 0
+13 -7 -15 0
+-7 -9 11 0
+5 -16 -2 0
+11 -12 -6 0
+-20 17 15 0
+13 1 -17 0
+19 -15 -2 0
+-15 -17 -4 0
+5 17 -3 0
+-3 -19 7 0
+9 -20 -16 0
+3 -7 -2 0
+19 -3 -10 0
+-6 1 -17 0
+15 -4 3 0
+-15 -5 -17 0
+19 -18 -1 0
+19 -8 -15 0
+-19 -5 1 0
+17 6 -20 0
+11 -17 7 0
+-4 -17 6 0
+-18 1 11 0
+9 -1 8 0
+-13 -12 -14 0
+-6 -8 11 0
+18 -17 -3 0
+-7 15 -17 0
+20 15 -1 0
+15 16 7 0
+-2 13 11 0
+19 3 -1 0
+-17 11 -12 0
+-13 -8 -14 0
+-9 -11 13 0
+18 -20 -14 0
+-12 -10 1 0
+10 -7 17 0
+-1 13 12 0
+12 14 -18 0
+-5 -6 16 0
+-17 -6 18 0
+-3 8 -15 0
+-3 11 -7 0
+-1 17 -6 0
+14 7 -20 0
+-16 -1 -18 0
+-1 -20 -4 0
+-9 -20 3 0
+-7 -15 5 0
+-7 -12 -6 0
+-11 -17 4 0
+13 15 18 0
+10 -11 1 0
+-19 3 1 0
+-18 -20 -13 0
+3 11 -8 0
+9 17 15 0
+-13 -16 14 0
+18 14 1 0
+-6 -20 -1 0
+-20 -6 10 0
+-14 -1 13 0
+-9 7 8 0
+-12 -9 15 0
+13 17 -19 0
+13 7 -3 0
+9 -19 -18 0
+-10 3 18 0
+3 13 -18 0
+18 -5 -17 0
+18 19 -17 0
+-10 -3 11 0
+-1 -19 18 0
+-1 -12 16 0
+-16 -15 9 0
+7 -18 19 0
+16 -8 5 0
+8 -19 -20 0
+8 -17 11 0
+-6 11 2 0
+-15 -9 -20 0
+-15 -7 6 0
+-1 20 -3 0
+%
+0
+

tests/satlib/uf20-91/uf20-0150.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -14 -10 5 0
+3 -5 -10 0
+14 -15 13 0
+1 4 -17 0
+6 12 -20 0
+-8 16 9 0
+17 -9 6 0
+-4 -9 -19 0
+4 14 17 0
+-20 -9 -13 0
+19 -2 -10 0
+-8 -10 6 0
+-18 -20 10 0
+9 -20 17 0
+-7 -20 10 0
+13 17 -6 0
+19 12 7 0
+-5 -3 -2 0
+-18 -7 -15 0
+-19 -17 5 0
+-11 -13 15 0
+-18 -15 -11 0
+-1 -14 -11 0
+-16 -5 10 0
+9 -4 -6 0
+14 -4 9 0
+14 -12 -15 0
+16 12 -8 0
+-4 -5 3 0
+2 -5 8 0
+1 -20 -13 0
+2 -6 8 0
+1 -7 9 0
+11 -1 -10 0
+-5 1 -16 0
+16 -9 12 0
+20 19 11 0
+-8 -5 14 0
+-4 2 10 0
+5 11 -7 0
+12 18 4 0
+-9 -5 20 0
+-7 -19 -8 0
+-9 -20 1 0
+3 -17 -16 0
+4 -9 16 0
+8 1 -5 0
+-11 7 -15 0
+-17 -14 10 0
+-4 14 -19 0
+-17 -6 -4 0
+-13 1 -16 0
+14 -18 3 0
+19 12 -2 0
+11 -13 6 0
+4 8 14 0
+-2 -14 -7 0
+-14 -5 11 0
+4 -11 18 0
+18 -10 19 0
+11 2 -17 0
+-12 10 11 0
+12 -1 -6 0
+8 20 9 0
+11 2 -17 0
+-18 16 17 0
+13 12 15 0
+4 1 -3 0
+-7 -11 18 0
+-2 -6 4 0
+14 13 4 0
+15 20 16 0
+-12 -6 5 0
+-13 -2 -18 0
+-13 -18 -19 0
+-5 -10 -9 0
+14 -11 -8 0
+16 -18 17 0
+-3 14 -2 0
+7 13 3 0
+-12 10 16 0
+4 13 16 0
+3 -13 16 0
+-9 18 -4 0
+18 -7 -1 0
+2 -9 13 0
+-5 20 -10 0
+14 15 -8 0
+-9 -19 -14 0
+8 -11 5 0
+-20 17 11 0
+%
+0
+

tests/satlib/uf20-91/uf20-0151.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 17 -6 -12 0
+17 -10 -19 0
+-1 -9 7 0
+-16 13 -15 0
+2 -12 6 0
+-1 13 -9 0
+-10 -17 -5 0
+-2 7 -10 0
+16 4 9 0
+9 10 18 0
+11 15 -19 0
+5 13 10 0
+-10 -16 6 0
+15 2 -3 0
+-15 -4 13 0
+-11 13 -12 0
+-8 20 -6 0
+-6 13 8 0
+-13 19 2 0
+-6 -17 12 0
+-1 -4 18 0
+-8 5 6 0
+-6 1 -13 0
+9 3 15 0
+9 -2 -15 0
+7 18 -16 0
+-8 19 1 0
+-17 16 -3 0
+2 15 7 0
+-19 -10 -2 0
+-17 -14 -15 0
+8 18 15 0
+-20 17 -3 0
+2 -7 -8 0
+-16 10 -20 0
+-17 5 10 0
+6 -11 7 0
+1 -13 4 0
+17 14 16 0
+-15 -17 16 0
+11 -10 20 0
+8 -4 15 0
+-9 11 -6 0
+-9 -16 13 0
+13 -11 -3 0
+-17 -5 -12 0
+-6 -1 -14 0
+-4 8 -1 0
+-4 6 -3 0
+5 -14 8 0
+19 -16 8 0
+10 -20 6 0
+-19 -17 11 0
+-12 -16 6 0
+-12 16 1 0
+-3 20 16 0
+-15 20 9 0
+-3 -1 -19 0
+-14 11 -6 0
+6 -17 -13 0
+7 18 14 0
+12 3 1 0
+-5 7 -1 0
+11 16 -17 0
+16 -17 -5 0
+-9 -10 -12 0
+4 1 18 0
+6 7 -10 0
+-18 15 -11 0
+-7 19 8 0
+10 11 -2 0
+4 -9 -15 0
+-13 18 8 0
+-18 -17 13 0
+18 -19 -12 0
+-19 9 2 0
+-17 -13 18 0
+-9 -13 7 0
+18 -9 4 0
+13 18 3 0
+-16 4 -11 0
+7 20 -13 0
+-14 -19 -5 0
+-8 11 6 0
+-15 -13 2 0
+19 13 -12 0
+9 17 14 0
+-13 -14 -2 0
+-13 -1 7 0
+3 7 -20 0
+12 -3 -9 0
+%
+0
+

tests/satlib/uf20-91/uf20-0152.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 7 10 -6 0
+-20 14 17 0
+16 -19 -11 0
+12 6 -11 0
+6 -18 1 0
+19 -18 9 0
+17 8 -4 0
+-20 -2 12 0
+19 14 -9 0
+-3 5 -14 0
+20 -4 2 0
+-13 2 -19 0
+-13 -12 6 0
+-9 -19 -10 0
+18 -15 -6 0
+9 -18 7 0
+-2 -1 -3 0
+20 -9 4 0
+14 11 15 0
+10 17 4 0
+-4 -3 -20 0
+-16 14 -19 0
+-12 -7 -20 0
+-17 5 -7 0
+20 -11 4 0
+-9 18 4 0
+-14 3 -20 0
+-3 17 11 0
+14 13 5 0
+1 -19 -8 0
+-14 12 -17 0
+-7 -4 18 0
+-1 -10 20 0
+-11 -10 20 0
+19 -11 7 0
+-19 10 -14 0
+-13 8 -19 0
+-20 6 -1 0
+5 14 -8 0
+-13 -8 9 0
+-1 13 -15 0
+9 -20 -5 0
+-18 10 -16 0
+17 -14 12 0
+-3 -11 9 0
+-17 12 15 0
+-8 -13 -1 0
+-3 -17 2 0
+17 -12 4 0
+-9 19 13 0
+-19 -6 -14 0
+-15 -5 -12 0
+7 -20 8 0
+18 14 -15 0
+-3 11 -9 0
+-18 -7 4 0
+11 14 5 0
+13 16 -1 0
+-4 1 -12 0
+-9 -5 -18 0
+-18 -19 -9 0
+12 5 -2 0
+-16 7 -15 0
+19 17 16 0
+5 14 -2 0
+-2 5 -16 0
+-10 -14 19 0
+6 9 -11 0
+-19 6 13 0
+-19 -11 17 0
+17 7 12 0
+17 -1 4 0
+-14 3 -19 0
+13 -15 7 0
+6 11 -8 0
+-13 9 1 0
+2 13 -16 0
+9 -1 8 0
+-10 1 -2 0
+-4 -13 -17 0
+5 8 -7 0
+7 -8 -4 0
+1 5 11 0
+-10 -18 -6 0
+-3 -20 -5 0
+17 -15 -7 0
+-14 7 -19 0
+-8 -10 1 0
+3 -8 6 0
+-20 -2 5 0
+-16 8 10 0
+%
+0
+

tests/satlib/uf20-91/uf20-0153.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -11 3 10 0
+-4 5 -8 0
+-17 -4 -20 0
+-12 -20 4 0
+8 5 -16 0
+-16 1 -5 0
+14 -5 -20 0
+-4 -16 11 0
+-5 10 -11 0
+-4 8 12 0
+-8 6 11 0
+-12 11 -3 0
+-1 18 3 0
+18 -20 -15 0
+9 19 -10 0
+8 -9 7 0
+-16 5 12 0
+14 -5 -8 0
+-5 10 17 0
+17 -18 7 0
+1 5 -18 0
+17 -5 16 0
+13 -11 -7 0
+-18 2 -9 0
+3 18 -16 0
+-18 -4 19 0
+8 -7 12 0
+-7 8 -20 0
+13 -6 -19 0
+-19 2 -17 0
+7 8 -3 0
+12 -11 -20 0
+-13 -1 -3 0
+9 6 -16 0
+7 -4 16 0
+2 4 -14 0
+-17 1 8 0
+-11 17 -3 0
+-3 18 2 0
+-12 11 -8 0
+-14 13 7 0
+14 2 -12 0
+-20 -4 -17 0
+-14 -10 15 0
+-4 14 12 0
+11 -15 -12 0
+-2 18 8 0
+10 -8 -19 0
+15 9 7 0
+10 6 3 0
+-6 14 -19 0
+13 -3 -12 0
+2 3 -1 0
+18 -11 19 0
+-14 18 -11 0
+-20 14 17 0
+17 -1 -11 0
+-11 19 13 0
+-11 12 -5 0
+7 2 -3 0
+-1 16 -12 0
+-8 -7 -20 0
+10 -7 -15 0
+-8 10 -7 0
+4 -11 -12 0
+-4 12 -9 0
+-15 -16 5 0
+9 4 7 0
+19 14 -16 0
+15 -9 10 0
+20 -19 12 0
+-7 8 17 0
+-12 -11 -13 0
+-5 -12 -20 0
+-12 6 8 0
+-18 -20 -6 0
+2 16 -4 0
+13 -18 -14 0
+17 -8 13 0
+-11 -4 -2 0
+-11 -4 5 0
+-7 -20 8 0
+10 7 6 0
+-14 -1 -16 0
+-9 -19 -1 0
+-11 -1 -3 0
+20 -18 8 0
+19 18 -14 0
+-17 -3 -12 0
+3 18 11 0
+-12 9 7 0
+%
+0
+

tests/satlib/uf20-91/uf20-0154.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 19 5 8 0
+-3 -2 -12 0
+7 14 16 0
+13 -5 -10 0
+-12 2 18 0
+1 -6 -9 0
+14 16 -17 0
+-3 -13 -11 0
+-1 -10 17 0
+8 7 -10 0
+-9 -3 -2 0
+13 -5 -10 0
+-6 -14 9 0
+8 13 15 0
+12 -11 -16 0
+-18 6 -20 0
+14 15 -4 0
+10 18 -8 0
+-13 3 -8 0
+8 -17 -14 0
+7 -18 -10 0
+-19 -15 2 0
+-8 17 9 0
+-4 9 20 0
+11 20 17 0
+-20 -9 8 0
+13 -11 -20 0
+17 1 -16 0
+20 -16 -3 0
+-12 5 -3 0
+12 -4 18 0
+-19 -10 -17 0
+9 16 17 0
+19 20 -2 0
+1 -3 13 0
+7 -12 10 0
+-14 -15 -5 0
+9 -7 -18 0
+-9 14 -18 0
+-19 -11 -1 0
+14 1 5 0
+-11 18 16 0
+19 15 6 0
+-16 -1 -19 0
+12 -1 -17 0
+-16 19 -20 0
+16 -5 8 0
+17 20 14 0
+-5 -20 -3 0
+-17 13 -16 0
+7 -19 -10 0
+-4 -12 -14 0
+-17 -11 -15 0
+-18 -2 -15 0
+6 10 3 0
+8 10 -16 0
+16 12 11 0
+-1 6 -18 0
+14 -20 -18 0
+20 3 -2 0
+17 13 6 0
+16 13 15 0
+6 7 -19 0
+15 9 14 0
+3 1 -8 0
+-14 6 3 0
+-4 1 -15 0
+-19 -12 -2 0
+13 7 20 0
+-12 -2 19 0
+10 16 -12 0
+12 2 9 0
+8 -20 -7 0
+18 -16 -3 0
+18 13 9 0
+13 10 5 0
+16 -11 -14 0
+7 -3 5 0
+-20 -3 8 0
+14 -9 -18 0
+-6 3 -10 0
+17 6 -1 0
+3 -13 2 0
+-9 -16 -4 0
+-2 5 -8 0
+19 12 -1 0
+19 17 -20 0
+-11 -16 20 0
+6 -7 4 0
+4 3 10 0
+2 1 -9 0
+%
+0
+

tests/satlib/uf20-91/uf20-0155.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -18 5 -13 0
+20 8 17 0
+15 14 9 0
+-16 20 -12 0
+14 -6 11 0
+5 17 -13 0
+-3 20 18 0
+-2 4 16 0
+18 -3 1 0
+-4 -11 -7 0
+15 2 -16 0
+-18 7 16 0
+-19 -7 -9 0
+-15 16 -19 0
+16 8 6 0
+-1 15 5 0
+13 -20 16 0
+14 8 -2 0
+-2 1 -17 0
+-11 18 -13 0
+7 -5 9 0
+9 10 -4 0
+17 5 4 0
+2 -19 -1 0
+17 8 -4 0
+15 12 6 0
+-12 14 -17 0
+-12 19 5 0
+1 2 -7 0
+-13 -4 -17 0
+6 3 19 0
+-1 2 3 0
+7 3 -8 0
+3 -5 -1 0
+-18 15 -1 0
+8 12 15 0
+-13 -1 4 0
+18 3 -10 0
+-19 -8 17 0
+-17 9 3 0
+9 -10 1 0
+5 8 -2 0
+16 20 -5 0
+3 13 -2 0
+-13 -3 15 0
+-5 -12 -6 0
+8 -15 -19 0
+-10 -13 -19 0
+-15 9 -17 0
+-5 13 -8 0
+5 -16 9 0
+-4 -2 16 0
+-17 -4 -5 0
+-2 15 -6 0
+3 17 -11 0
+1 2 -19 0
+13 10 -8 0
+-5 7 -19 0
+18 1 17 0
+-10 -5 -17 0
+17 -13 11 0
+18 -9 -14 0
+-20 -1 4 0
+10 -15 -6 0
+12 -3 10 0
+4 7 -12 0
+-7 14 6 0
+11 -7 -9 0
+2 5 -4 0
+-15 6 3 0
+-6 -18 15 0
+-4 -17 14 0
+-4 -5 -13 0
+-12 4 14 0
+-10 -12 15 0
+-17 16 20 0
+14 10 6 0
+11 -7 10 0
+14 8 -13 0
+-17 12 -10 0
+-14 -20 16 0
+3 -5 -10 0
+13 3 -19 0
+11 20 4 0
+-2 -3 -17 0
+11 -8 19 0
+-7 -3 15 0
+9 -3 8 0
+-15 -14 -7 0
+19 -3 9 0
+1 4 -6 0
+%
+0
+

tests/satlib/uf20-91/uf20-0156.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 2 20 5 0
+-16 15 -19 0
+-12 20 1 0
+-11 -5 17 0
+16 -20 7 0
+-10 12 -6 0
+-15 16 -8 0
+5 19 -14 0
+12 -1 2 0
+-11 -15 -1 0
+4 -6 3 0
+-3 15 20 0
+-4 -13 -6 0
+-14 -10 -16 0
+-16 9 10 0
+8 -10 -13 0
+-14 -1 -7 0
+19 -15 7 0
+-19 6 -15 0
+-9 -16 1 0
+-5 20 -16 0
+-9 -3 15 0
+-10 -14 -1 0
+-1 -17 -18 0
+7 -19 14 0
+-15 -2 -5 0
+-5 6 -16 0
+5 10 4 0
+-17 7 18 0
+12 -9 7 0
+-10 11 5 0
+8 6 -3 0
+-9 19 -17 0
+10 -12 16 0
+-15 -2 -11 0
+9 20 -3 0
+-15 -10 13 0
+-7 17 3 0
+-9 12 -16 0
+6 10 -5 0
+12 3 16 0
+-15 -14 19 0
+-19 8 7 0
+-6 20 3 0
+-3 -10 -7 0
+4 -16 -14 0
+-19 13 18 0
+10 -11 -9 0
+13 -18 -10 0
+12 9 -18 0
+-8 -18 10 0
+11 -10 7 0
+-11 3 -18 0
+-10 -19 11 0
+11 -12 -18 0
+-4 -3 -17 0
+2 6 -3 0
+-17 -18 14 0
+-6 18 -5 0
+9 4 2 0
+6 -20 -18 0
+-7 -16 8 0
+11 9 18 0
+-12 5 2 0
+-11 -10 -12 0
+-18 -19 14 0
+14 -6 -2 0
+5 -10 1 0
+7 8 -12 0
+17 15 -3 0
+-2 -4 -14 0
+1 -13 -18 0
+-15 19 6 0
+-2 -8 -10 0
+6 -13 -7 0
+-4 -1 -18 0
+10 -17 9 0
+4 13 2 0
+12 9 11 0
+-14 -8 -20 0
+-14 -19 -20 0
+-7 -5 -12 0
+-18 15 3 0
+-2 -16 -19 0
+-19 9 8 0
+-17 -3 -2 0
+12 -20 -1 0
+-13 -8 16 0
+13 7 5 0
+-3 -11 -12 0
+-16 -2 12 0
+%
+0
+

tests/satlib/uf20-91/uf20-0157.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ -8 17 7 0
+-6 11 14 0
+13 -15 -5 0
+9 8 -17 0
+15 2 4 0
+17 16 5 0
+14 -15 19 0
+-15 3 -2 0
+11 18 -6 0
+2 13 -5 0
+5 18 9 0
+-2 -5 9 0
+15 -13 -2 0
+2 16 -19 0
+-10 20 -5 0
+2 18 15 0
+-12 -7 -5 0
+2 -13 -9 0
+15 18 -13 0
+-15 1 -18 0
+14 19 10 0
+-14 10 -15 0
+-15 -20 -18 0
+-14 -12 -5 0
+14 -13 15 0
+-19 12 -2 0
+-5 -3 9 0
+12 -13 -2 0
+-2 -18 -20 0
+8 -9 -19 0
+13 16 -20 0
+12 -7 4 0
+15 12 9 0
+5 -4 -19 0
+-18 5 -2 0
+-15 18 -14 0
+-9 -16 4 0
+19 -14 -15 0
+8 1 -20 0
+-20 3 -1 0
+14 5 -13 0
+15 -5 7 0
+17 -12 -13 0
+7 -18 4 0
+6 -19 -14 0
+-18 -7 9 0
+20 14 -1 0
+-17 -2 20 0
+3 -12 -11 0
+14 10 -19 0
+-18 14 5 0
+-10 18 -8 0
+12 9 19 0
+10 -16 -18 0
+-16 2 9 0
+14 3 -11 0
+15 -5 6 0
+20 1 4 0
+-17 19 -5 0
+-4 -1 19 0
+-18 -10 9 0
+-8 -1 -11 0
+16 -12 20 0
+-19 -14 13 0
+16 -19 -8 0
+-7 -4 5 0
+-20 -4 -1 0
+7 -15 -4 0
+14 16 -13 0
+16 -4 10 0
+19 -18 7 0
+3 13 7 0
+-16 -10 -1 0
+-19 -9 15 0
+-2 -12 -5 0
+-15 14 2 0
+19 -11 -3 0
+-11 -18 -6 0
+-11 7 10 0
+-17 -20 16 0
+-8 16 5 0
+-13 12 6 0
+-5 7 -1 0
+-5 13 -3 0
+15 -1 10 0
+19 -2 -20 0
+-7 9 -12 0
+-15 -7 6 0
+-11 -2 20 0
+-4 11 -5 0
+-18 19 -2 0
+%
+0
+

tests/satlib/uf20-91/uf20-0158.cnf

@@ -0,0 +1,102 @@
+c This Formular is generated by mcnf
+c
+c    horn? no 
+c    forced? no 
+c    mixed sat? no 
+c    clause length = 3 
+c
+p cnf 20  91 
+ 9 -11 -6 0
+-4 10 16 0
+12 16 -11 0
+-10 -18 -9 0
+-7 -16 10 0
+-7 3 -16 0
+-19 -10 7 0
+-10 15 -18 0
+1 18 -6 0
+-9 -15 14 0
+-9 19 -4 0
+12 -18 1 0
+19 -11 6 0
+-10 -9 8 0
+8 12 20 0
+-15 -3 14 0
+-13 -8 -20 0
+2 15 -7 0
+-9 -14 6 0
+3 20 -14 0
+-8 -20 1 0
+11 -3 -2 0
+-6 -14 5 0
+-1 11 8 0
+1 4 -3 0
+6 -20 -11 0
+-15 -18 -16 0
+-3 11 -18 0
+-16 -19 -7 0
+-15 1 -20 0
+-7 -13 -20 0
+12 11 13 0
+20 12 -17 0
+-3 6 -2 0
+11 -7 -18 0
+-15 7 -17 0
+4 -14 10 0
+15 13 5 0
+4 -6 2 0
+-11 -18 -12 0
+13 5 -2 0
+8 17 -18 0
+-14 -11 -17 0
+12 -13 8 0
+-1 -6 18 0
+-20 2 9 0
+13 10 11 0
+-18 12 -14 0
+-9 17 19 0
+-18 13 1 0
+-16 12 -11 0
+3 -11 7 0
+-4 12 1 0
+9 -17 1 0
+-10 12 20 0
+13 -4 2 0
+19 16 13 0
+-14 6 19 0
+-18 -11 -4 0
+6 -7 -10 0
+-15 -10 -1 0
+-18 -12 -11 0
+18 11 17 0
+3 12 8 0
+-7 -15 -14 0
+7 -2 12 0
+-1 7 16 0
+9 -15 6 0
+-9 2 17 0
+-1 10 -20 0
+-5 -8 14 0
+-2 11 -15 0
+4 -10 -13 0
+-15 -4 -14 0
+-16 -19 5 0
+8 -18 14 0
+-10 -15 4 0
+16 6 15 0
+-19 4 -20 0
+6 -1 20 0
+9 12 19 0
+19 -1 -17 0
+-6 -7 -18 0
+7 -10 1 0
+1 6 -4 0
+6 16 -9 0
+6 5 15 0
+-14 13 12 0
+19 -13 -9 0
+6 19 -15 0
+-11 2 -1 0
+%
+0
+