%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SYN845-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 12:03:55 EDT 2022
% Result : Unsatisfiable 1.07s 1.31s
% Output : Refutation 1.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 61
% Syntax : Number of clauses : 172 ( 50 unt; 33 nHn; 57 RR)
% Number of literals : 924 ( 0 equ; 722 neg)
% Maximal clause size : 19 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 55 ( 54 usr; 2 prp; 0-15 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 1679 ( 725 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssNder1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
( ~ ssNder1_0
| ssNder1_1r1(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(3,plain,
ssNder1_1r1(X),
inference('REWRITE',[status(thm)],[clause2,clause1]) ).
cnf(clause3,negated_conjecture,
( ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_2r1r1(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(5,plain,
ssNder1_2r1r1(X,Y),
inference('REWRITE',[status(thm)],[clause3,clause1,3]) ).
cnf(clause10,negated_conjecture,
( ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_3r1r1r1(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(11,plain,
ssNder1_3r1r1r1(X,Y,Z),
inference('REWRITE',[status(thm)],[clause10,clause1,3,5]) ).
cnf(clause18,negated_conjecture,
( ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(X,Y,Z,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(21,plain,
ssNder1_4r1r1r1r1(X,Y,Z,U),
inference('REWRITE',[status(thm)],[clause18,clause1,3,5,11]) ).
cnf(clause22,negated_conjecture,
( ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X,Y,Z,U,skc30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(23,plain,
ssPv16_5r1r1r1r1r1(X,Y,Z,U,skc30),
inference('REWRITE',[status(thm)],[clause22,clause1,3,5,11]) ).
cnf(clause31,negated_conjecture,
( ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X,Y,Z,U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(39,plain,
ssNder1_5r1r1r1r1r1(X,Y,Z,U,V),
inference('REWRITE',[status(thm)],[clause31,clause1,3,5,11,21]) ).
cnf(clause32,negated_conjecture,
( ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,skc28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(41,plain,
ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,skc28),
inference('REWRITE',[status(thm)],[clause32,clause1,3,5,11,21]) ).
cnf(clause37,negated_conjecture,
( ~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,skc29)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(43,plain,
~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,skc29),
inference('REWRITE',[status(thm)],[clause37,clause1,3,5,11,21]) ).
cnf(clause49,negated_conjecture,
( ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(61,plain,
ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W),
inference('REWRITE',[status(thm)],[clause49,clause1,3,5,11,21,39]) ).
cnf(clause59,negated_conjecture,
( ~ ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc27)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
cnf(65,plain,
~ ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc27),
inference('REWRITE',[status(thm)],[clause59,clause1,3,5,11,21,39]) ).
cnf(clause73,negated_conjecture,
( ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
cnf(87,plain,
ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1),
inference('REWRITE',[status(thm)],[clause73,clause1,3,5,11,21,39,61]) ).
cnf(clause74,negated_conjecture,
( ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
cnf(89,plain,
ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24),
inference('REWRITE',[status(thm)],[clause74,clause1,3,5,11,21,39,61]) ).
cnf(clause77,negated_conjecture,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc25)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
cnf(91,plain,
~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc25),
inference('REWRITE',[status(thm)],[clause77,clause1,3,5,11,21,39,61]) ).
cnf(clause86,negated_conjecture,
( ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssPv19_2r1r1(X,Y)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv19_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
cnf(103,plain,
( ~ ssPv19_2r1r1(X,Y)
| ssPv19_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
inference('REWRITE',[status(thm)],[clause86,clause1,3,5,11,21,39,61]) ).
cnf(clause94,negated_conjecture,
( ~ ssPv17_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv17_4r1r1r1r1(X,Y,Z,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
cnf(111,plain,
( ~ ssPv17_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv17_4r1r1r1r1(X,Y,Z,U) ),
inference('REWRITE',[status(thm)],[clause94,clause1,3,5,11,21,39,61]) ).
cnf(clause98,negated_conjecture,
( ~ ssPv15_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
cnf(119,plain,
( ~ ssPv15_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W) ),
inference('REWRITE',[status(thm)],[clause98,clause1,3,5,11,21,39,61]) ).
cnf(clause100,negated_conjecture,
( ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
cnf(123,plain,
ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1),
inference('REWRITE',[status(thm)],[clause100,clause1,3,5,11,21,39,61,87]) ).
cnf(clause115,negated_conjecture,
( ~ ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv18_3r1r1r1(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
cnf(133,plain,
( ~ ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_3r1r1r1(X,Y,Z) ),
inference('REWRITE',[status(thm)],[clause115,clause1,3,5,11,21,39,61,87]) ).
cnf(clause119,negated_conjecture,
( ~ ssPv17_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv17_4r1r1r1r1(X,Y,Z,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
cnf(139,plain,
( ~ ssPv17_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv17_4r1r1r1r1(X,Y,Z,U) ),
inference('REWRITE',[status(thm)],[clause119,clause1,3,5,11,21,39,61,87]) ).
cnf(clause126,negated_conjecture,
( ~ ssPv14_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
cnf(151,plain,
( ~ ssPv14_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
inference('REWRITE',[status(thm)],[clause126,clause1,3,5,11,21,39,61,87]) ).
cnf(clause127,negated_conjecture,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
cnf(153,plain,
ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1),
inference('REWRITE',[status(thm)],[clause127,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause133,negated_conjecture,
( ~ ssPv19_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv15_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv17_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
cnf(161,plain,
( ~ ssPv19_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv15_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv17_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
inference('REWRITE',[status(thm)],[clause133,clause1,3,5,11,21,39,61]) ).
cnf(clause134,negated_conjecture,
( ~ ssPv19_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv19_2r1r1(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause134) ).
cnf(163,plain,
( ~ ssPv19_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv19_2r1r1(X,Y) ),
inference('REWRITE',[status(thm)],[clause134,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause141,negated_conjecture,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssPv18_3r1r1r1(X,Y,Z)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv18_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause141) ).
cnf(167,plain,
( ~ ssPv18_3r1r1r1(X,Y,Z)
| ssPv18_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[clause141,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause148,negated_conjecture,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssPv16_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv16_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause148) ).
cnf(175,plain,
( ~ ssPv16_5r1r1r1r1r1(X,Y,Z,U,V)
| ssPv16_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[clause148,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause149,negated_conjecture,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv15_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
cnf(177,plain,
( ~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ssPv15_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[clause149,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause153,negated_conjecture,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause153) ).
cnf(185,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[clause153,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause155,negated_conjecture,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause155) ).
cnf(189,plain,
ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1),
inference('REWRITE',[status(thm)],[clause155,clause1,3,5,11,21,39,61,87,123,153]) ).
cnf(clause160,negated_conjecture,
( ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv14_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv17_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause160) ).
cnf(199,plain,
( ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv14_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv17_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
inference('REWRITE',[status(thm)],[clause160,clause1,3,5,11,21,39,61,87]) ).
cnf(clause185,negated_conjecture,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause185) ).
cnf(229,plain,
ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1),
inference('REWRITE',[status(thm)],[clause185,clause1,3,5,11,21,39,61,87,123,153,189]) ).
cnf(clause200,negated_conjecture,
( ~ ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv16_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv19_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause200) ).
cnf(251,plain,
( ~ ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv16_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv19_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[clause200,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause208,negated_conjecture,
( ~ ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv15_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv18_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause208) ).
cnf(263,plain,
( ~ ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv15_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv18_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[clause208,clause1,3,5,11,21,39,61,87,123]) ).
cnf(clause209,negated_conjecture,
( ~ ssPv14_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause209) ).
cnf(265,plain,
( ~ ssPv14_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
inference('REWRITE',[status(thm)],[clause209,clause1,3,5,11,21,39,61,87,123,153,189]) ).
cnf(clause211,negated_conjecture,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv13_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause211) ).
cnf(269,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv13_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1) ),
inference('REWRITE',[status(thm)],[clause211,clause1,3,5,11,21,39,61,87,123,153,189]) ).
cnf(clause215,negated_conjecture,
( ~ ssPv11_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv11_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause215) ).
cnf(277,plain,
( ~ ssPv11_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ssPv11_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1) ),
inference('REWRITE',[status(thm)],[clause215,clause1,3,5,11,21,39,61,87,123,153,189]) ).
cnf(clause217,negated_conjecture,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause217) ).
cnf(281,plain,
ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1),
inference('REWRITE',[status(thm)],[clause217,clause1,3,5,11,21,39,61,87,123,153,189,229]) ).
cnf(clause218,negated_conjecture,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
cnf(283,plain,
ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,skc22),
inference('REWRITE',[status(thm)],[clause218,clause1,3,5,11,21,39,61,87,123,153,189,229]) ).
cnf(clause247,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause247) ).
cnf(335,plain,
ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2),
inference('REWRITE',[status(thm)],[clause247,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause254,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssPv18_3r1r1r1(X,Y,Z)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv18_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause254) ).
cnf(349,plain,
( ~ ssPv18_3r1r1r1(X,Y,Z)
| ssPv18_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause254,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause258,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssPv16_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause258) ).
cnf(357,plain,
( ~ ssPv16_5r1r1r1r1r1(X,Y,Z,U,V)
| ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause258,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause263,negated_conjecture,
( ~ ssPv11_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssPv13_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ssPv14_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause263) ).
cnf(365,plain,
( ~ ssPv11_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssPv13_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ssPv14_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1) ),
inference('REWRITE',[status(thm)],[clause263,clause1,3,5,11,21,39,61,87,123,153,189]) ).
cnf(clause272,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause272) ).
cnf(383,plain,
( ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause272,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause278,negated_conjecture,
( ~ ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause278) ).
cnf(395,plain,
( ~ ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1) ),
inference('REWRITE',[status(thm)],[clause278,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause279,negated_conjecture,
( ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause279) ).
cnf(397,plain,
( ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause279,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause280,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause280) ).
cnf(399,plain,
ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2),
inference('REWRITE',[status(thm)],[clause280,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335]) ).
cnf(clause281,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause281) ).
cnf(401,plain,
ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,skc18),
inference('REWRITE',[status(thm)],[clause281,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335]) ).
cnf(clause282,negated_conjecture,
( ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,skc19)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause282) ).
cnf(403,plain,
~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,skc19),
inference('REWRITE',[status(thm)],[clause282,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335]) ).
cnf(clause323,negated_conjecture,
( ~ ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv18_3r1r1r1(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause323) ).
cnf(473,plain,
( ~ ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv18_3r1r1r1(X,Y,Z) ),
inference('REWRITE',[status(thm)],[clause323,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause325,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssPv17_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause325) ).
cnf(477,plain,
( ~ ssPv17_4r1r1r1r1(X,Y,Z,U)
| ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause325,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause328,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssPv16_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv16_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause328) ).
cnf(483,plain,
( ~ ssPv16_5r1r1r1r1r1(X,Y,Z,U,V)
| ssPv16_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause328,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause329,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv15_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause329) ).
cnf(485,plain,
( ~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ssPv15_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause329,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause337,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv13_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause337) ).
cnf(499,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv13_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause337,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause339,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv12_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause339) ).
cnf(501,plain,
( ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv12_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause339,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause344,negated_conjecture,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause344) ).
cnf(505,plain,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause344,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause346,negated_conjecture,
( ~ ssPv11_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause346) ).
cnf(509,plain,
( ~ ssPv11_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1) ),
inference('REWRITE',[status(thm)],[clause346,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause347,negated_conjecture,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv18_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause347) ).
cnf(511,plain,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv18_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause347,clause1,3,5,11,21,39,61,87,123,153,189,229,281]) ).
cnf(clause350,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv10_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause350) ).
cnf(515,plain,
( ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ssPv10_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause350,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause422,negated_conjecture,
( ~ ssPv15_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause422) ).
cnf(651,plain,
( ~ ssPv15_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause422,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause425,negated_conjecture,
( ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv12_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv13_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv11_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause425) ).
cnf(657,plain,
( ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv12_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv13_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv11_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause425,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(clause427,negated_conjecture,
( ~ ssPv10_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv16_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ~ ssNder1_5r1r1r1r1r1(X,Y,Z,U,V)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause427) ).
cnf(661,plain,
( ~ ssPv10_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv16_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause427,clause1,3,5,11,21,39,61,87,123,153,189,229,281,335,399]) ).
cnf(946,plain,
~ ssPv15_7r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W),
inference('UR-RESOLVE',[status(thm)],[119,43]) ).
cnf(953,plain,
ssPv16_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,X1,Y1),
inference('HYPERRESOLVE',[status(thm)],[175,23]) ).
cnf(955,plain,
~ ssPv14_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc27,X1),
inference('UR-RESOLVE',[status(thm)],[151,65]) ).
cnf(956,plain,
ssPv15_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1,Y1),
inference('HYPERRESOLVE',[status(thm)],[177,41]) ).
cnf(966,plain,
ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24,Y1),
inference('HYPERRESOLVE',[status(thm)],[185,89]) ).
cnf(976,plain,
~ ssPv14_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc27,X1,Y1,Z1,U1),
inference('UR-RESOLVE',[status(thm)],[265,65]) ).
cnf(980,plain,
ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,X1,Y1,Z1,U1,V1,W1),
inference('HYPERRESOLVE',[status(thm)],[357,23]) ).
cnf(982,plain,
ssPv13_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24,Y1,Z1,U1),
inference('HYPERRESOLVE',[status(thm)],[269,89]) ).
cnf(997,plain,
ssPv16_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2),
inference('HYPERRESOLVE',[status(thm)],[483,23]) ).
cnf(1002,plain,
ssPv15_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1,Y1,Z1,U1,V1,W1,X2,Y2),
inference('HYPERRESOLVE',[status(thm)],[485,41]) ).
cnf(1015,plain,
ssPv13_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24,Y1,Z1,U1,V1,W1,X2,Y2),
inference('HYPERRESOLVE',[status(thm)],[499,89]) ).
cnf(1092,plain,
( ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv14_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv17_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_3r1r1r1(X,Y,Z) ),
inference('HYPERRESOLVE',[status(thm)],[133,199]) ).
cnf(1112,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1)
| ssPv19_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1) ),
inference('HYPERRESOLVE',[status(thm)],[251,966,953]) ).
cnf(1118,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1)
| ssPv19_2r1r1(X,Y) ),
inference('HYPERRESOLVE',[status(thm)],[163,1112]) ).
cnf(1122,plain,
( ssPv19_2r1r1(X,Y)
| ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1,U1,V1) ),
inference('HYPERRESOLVE',[status(thm)],[383,1118]) ).
cnf(1124,plain,
( ssPv19_2r1r1(X,Y)
| ssPv12_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('HYPERRESOLVE',[status(thm)],[501,1118]) ).
cnf(1130,plain,
( ssPv19_2r1r1(X,Y)
| ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1,U1,skc22) ),
inference('HYPERRESOLVE',[status(thm)],[505,1122,283,980]) ).
cnf(1131,plain,
( ssPv19_2r1r1(X,Y)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1,U1) ),
inference('HYPERRESOLVE',[status(thm)],[395,1130]) ).
cnf(1132,plain,
( ssPv19_2r1r1(X,Y)
| ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1,U1,V1) ),
inference('HYPERRESOLVE',[status(thm)],[397,1131]) ).
cnf(1140,plain,
( ssPv19_2r1r1(X,Y)
| ssPv11_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1,U1,V1,W1,skc18) ),
inference('HYPERRESOLVE',[status(thm)],[657,1124,401,1015]) ).
cnf(1142,plain,
( ssPv19_2r1r1(X,Y)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1) ),
inference('HYPERRESOLVE',[status(thm)],[509,1140]) ).
cnf(1143,plain,
( ssPv19_2r1r1(X,Y)
| ssPv11_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1) ),
inference('HYPERRESOLVE',[status(thm)],[277,1142]) ).
cnf(1154,plain,
( ssPv19_2r1r1(X,Y)
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1)
| ssPv14_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,skc24,X1,Y1,Z1) ),
inference('HYPERRESOLVE',[status(thm)],[365,1143,982]) ).
cnf(1158,plain,
( ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv14_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_3r1r1r1(X,Y,Z)
| ssPv17_4r1r1r1r1(X,Y,Z,U) ),
inference('HYPERRESOLVE',[status(thm)],[139,1092]) ).
cnf(1159,plain,
( ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc27,X1)
| ssPv18_3r1r1r1(X,Y,Z)
| ssPv17_4r1r1r1r1(X,Y,Z,U) ),
inference('HYPERRESOLVE',[status(thm)],[955,1158]) ).
cnf(1161,plain,
( ssPv18_3r1r1r1(X,Y,Z)
| ssPv17_4r1r1r1r1(X,Y,Z,U) ),
inference('HYPERRESOLVE',[status(thm)],[91,1159]) ).
cnf(1172,plain,
( ssPv18_3r1r1r1(X,Y,Z)
| ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('HYPERRESOLVE',[status(thm)],[477,1161]) ).
cnf(1190,plain,
( ssPv19_2r1r1(X,Y)
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,skc27,skc24,W,X1,Y1) ),
inference('HYPERRESOLVE',[status(thm)],[976,1154]) ).
cnf(1195,plain,
( ssPv19_2r1r1(X,Y)
| ssPv10_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,skc27,skc24,W,X1,Y1,Z1,U1,V1,W1) ),
inference('HYPERRESOLVE',[status(thm)],[515,1190]) ).
cnf(1202,plain,
( ssPv19_2r1r1(X,Y)
| ssPv18_3r1r1r1(X,Y,Z)
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,skc27,skc24,W,X1,Y1,Z1,U1,V1,W1) ),
inference('HYPERRESOLVE',[status(thm)],[661,1195,997,1172]) ).
cnf(1213,plain,
( ssPv19_2r1r1(X,Y)
| ssPv18_3r1r1r1(X,Y,Z) ),
inference('HYPERRESOLVE',[status(thm)],[403,1202]) ).
cnf(1223,plain,
( ssPv19_2r1r1(X,Y)
| ssPv18_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('HYPERRESOLVE',[status(thm)],[349,1213]) ).
cnf(1243,plain,
ssPv19_2r1r1(X,Y),
inference('HYPERRESOLVE',[status(thm)],[511,1223,283,1132,980]) ).
cnf(1248,plain,
ssPv19_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1),
inference('REWRITE',[status(thm)],[103,1243]) ).
cnf(1249,plain,
( ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv15_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv17_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1) ),
inference('REWRITE',[status(thm)],[161,1248]) ).
cnf(1266,plain,
ssPv17_7r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,skc27),
inference('UR-RESOLVE',[status(thm)],[1249,65,946]) ).
cnf(1273,plain,
ssPv17_4r1r1r1r1(X,Y,Z,U),
inference('HYPERRESOLVE',[status(thm)],[111,1266]) ).
cnf(1286,plain,
ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2),
inference('REWRITE',[status(thm)],[477,1273]) ).
cnf(1287,plain,
( ~ ssPv15_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[651,1286]) ).
cnf(1294,plain,
ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1,Y1,Z1,U1,V1,W1,X2,skc19),
inference('UR-RESOLVE',[status(thm)],[1287,1002,403]) ).
cnf(1306,plain,
ssPv18_3r1r1r1(X,Y,Z),
inference('HYPERRESOLVE',[status(thm)],[473,1294]) ).
cnf(1312,plain,
ssPv18_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1),
inference('REWRITE',[status(thm)],[167,1306]) ).
cnf(1313,plain,
( ~ ssPv13_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ~ ssPv15_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1)
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[263,1312]) ).
cnf(1317,plain,
ssPv18_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2),
inference('REWRITE',[status(thm)],[349,1306]) ).
cnf(1318,plain,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[511,1317]) ).
cnf(1330,plain,
ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,skc24,X1),
inference('HYPERRESOLVE',[status(thm)],[1313,966,956]) ).
cnf(1331,plain,
~ ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,X1,Y1,Z1,U1,V1,skc22),
inference('UR-RESOLVE',[status(thm)],[1318,283,980]) ).
cnf(1339,plain,
ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,skc24,X1,Y1,Z1,U1,V1),
inference('HYPERRESOLVE',[status(thm)],[383,1330]) ).
cnf(1347,plain,
~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,X1,Y1,Z1,U1,V1),
inference('UR-RESOLVE',[status(thm)],[397,1331]) ).
cnf(1349,plain,
~ ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,skc30,V,W,X1,Y1,Z1,U1,V1,W1),
inference('UR-RESOLVE',[status(thm)],[395,1347]) ).
cnf(1357,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[505,1339,283,980]),1349]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN845-1 : TPTP v8.1.0. Released v2.5.0.
% 0.12/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue Jul 12 04:20:34 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.20/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.46 *
% 0.20/0.46 *
% 0.20/0.47 #<PACKAGE "SNARK-USER">
% 0.20/0.47 *
% 0.20/0.47 SNARK-TPTP-OPTIONS
% 0.20/0.47 *
% 0.20/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.47 (USE-FACTORING :POS)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.47 *
% 0.20/0.47 "."
% 0.20/0.47 *
% 0.20/0.47 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-12T04:20:35
% 0.20/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n027.cluster.edu at 2022-07-12T04:20:35
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 17-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv3_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 17-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv2_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 16-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 14-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv7_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv2_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv8_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv8_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv2_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv6_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv1_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv1_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv9_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv7_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv2_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv9_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv8_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv1_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv11_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv13_6r1r1r1r1r1r1| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv3_6r1r1r1r1r1r1| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv2_6r1r1r1r1r1r1| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv7_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv8_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv13_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv15_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv3_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv1_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv16_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv7_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv2_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv12_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv7_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv4_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv16_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv9_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv1_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv8_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv15_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv5_2r1r1| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv9_2r1r1| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv16_2r1r1| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.13 WARNING:
% 0.91/1.13 |ssPv13_1r1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv1_1r1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv16_1r1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv14_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv15_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv10_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv5_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv3_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv8_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv12_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv15_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv14_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv17_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv4_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv14_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv12_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv14_4r1r1r1r1| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv9_4r1r1r1r1| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv5_4r1r1r1r1| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv5_5r1r1r1r1r1| is a 5-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv2_5r1r1r1r1r1| is a 5-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv4_5r1r1r1r1r1| is a 5-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv14_5r1r1r1r1r1| is a 5-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv14_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv1_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv7_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv4_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv3_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv2_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv3_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv10_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv5_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv7_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv3_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv11_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv5_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv2_11r1r1r1r1r1r1r1r1r1r1r1| is a 11-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv7_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv1_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv1_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv5_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv4_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv3_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv2_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 14-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv3_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 14-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv2_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 15-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv2_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 18-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 19-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 16-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv4_6r1r1r1r1r1r1| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv5_6r1r1r1r1r1r1| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv15_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_4r1r1r1r1| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv12_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv9_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv13_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv11_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv6_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.14 WARNING:
% 0.91/1.14 |ssPv12_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 1.07/1.31
% 1.07/1.31
% 1.07/1.31 #||
% 1.07/1.31 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.07/1.31 % SZS output start Refutation
% See solution above
% 1.16/1.37 ||#
% 1.16/1.37
% 1.16/1.37 ; Summary of computation:
% 1.16/1.37 ; 1904 formulas have been input or derived (from 800 formulas).
% 1.16/1.37 ; 1357 (71%) were retained. Of these,
% 1.16/1.37 ; 750 (55%) were simplified or subsumed later,
% 1.16/1.37 ; 607 (45%) are still being kept.
% 1.16/1.37 ;
% 1.16/1.37 ; Run time in seconds excluding printing time:
% 1.16/1.37 ; 0.557 66% Read assertion file (1 call)
% 1.16/1.37 ; 0.089 11% Assert (576 calls)
% 1.16/1.37 ; 0.043 5% Process new row (1,263 calls)
% 1.16/1.37 ; 0.014 2% Resolution (1,598 calls)
% 1.16/1.37 ; 0.001 0% Paramodulation (799 calls)
% 1.16/1.37 ; 0.001 0% Factoring (102 calls)
% 1.16/1.37 ; 0.010 1% Condensing (683 calls)
% 1.16/1.37 ; 0.002 0% Forward subsumption (683 calls)
% 1.16/1.37 ; 0.008 1% Backward subsumption (602 calls)
% 1.16/1.37 ; 0.001 0% Clause clause subsumption (92 calls)
% 1.16/1.37 ; 0.064 8% Forward simplification (1,137 calls)
% 1.16/1.37 ; 0.011 1% Backward simplification (887 calls)
% 1.16/1.37 ; 0.000 0% Ordering (336 calls)
% 1.16/1.37 ; 0.000 0% Sortal reasoning (32 calls)
% 1.16/1.37 ; 0.013 2% Purity testing (1 call)
% 1.16/1.37 ; 0.027 3% Other
% 1.16/1.37 ; 0.841 Total
% 1.16/1.37 ; 0.896 Real time
% 1.16/1.37 ;
% 1.16/1.37 ; Term-hash-array has 558 terms in all.
% 1.16/1.37 ; Feature-vector-row-index has 326 entries (574 at peak, 602 added, 276 deleted).
% 1.16/1.37 ; Feature-vector-row-index has 210 nodes (434 at peak, 484 added, 274 deleted).
% 1.16/1.37 ; Retrieved 1,720 possibly forward subsuming rows in 683 calls.
% 1.16/1.37 ; Retrieved 1,263 possibly backward subsumed rows in 602 calls.
% 1.16/1.37 ; Path-index has 471 entries (535 at peak, 612 added, 141 deleted).
% 1.16/1.37 ; Path-index has 6,753 nodes (6,854 at peak, 7,172 added, 419 deleted).
% 1.16/1.37 ; Trie-index has 471 entries (535 at peak, 612 added, 141 deleted).
% 1.16/1.37 ; Trie-index has 4,931 nodes (5,481 at peak, 6,210 added, 1,279 deleted).
% 1.16/1.37 ; Retrieved 6,140 generalization terms in 6,525 calls.
% 1.16/1.37 ; Retrieved 296 instance terms in 284 calls.
% 1.16/1.37 ; Retrieved 3,624 unifiable terms in 3,396 calls.
% 1.16/1.37 ;
% 1.16/1.37 ; The agenda of rows to give has 41 entries:
% 1.16/1.37 ; 1 with value (4 18) 3 with value (4 25) 1 with value (4 65)
% 1.16/1.37 ; 4 with value (4 19) 2 with value (4 26) 1 with value (4 70)
% 1.16/1.37 ; 5 with value (4 20) 1 with value (4 37) 1 with value (4 71)
% 1.16/1.37 ; 5 with value (4 21) 1 with value (4 40) 1 with value (4 72)
% 1.16/1.37 ; 3 with value (4 22) 1 with value (4 42) 1 with value (4 73)
% 1.16/1.37 ; 3 with value (4 23) 1 with value (4 52) 1 with value (4 74)
% 1.16/1.37 ; 5 with value (4 24)
% 1.16/1.37 Evaluation took:
% 1.16/1.37 0.896 seconds of real time
% 1.16/1.37 0.866657 seconds of user run time
% 1.16/1.37 0.029808 seconds of system run time
% 1.16/1.37 [Run times include 0.053 seconds GC run time.]
% 1.16/1.37 0 calls to %EVAL
% 1.16/1.37 0 page faults and
% 1.16/1.37 95,997,528 bytes consed.
% 1.16/1.37 :PROOF-FOUND
% 1.16/1.37 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-12T04:20:35
% 1.16/1.37 :PROOF-FOUND
% 1.16/1.37 *
%------------------------------------------------------------------------------