%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SYN836-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n007.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:41 EDT 2022
% Result : Unsatisfiable 1.08s 1.29s
% Output : Refutation 1.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 47
% Syntax : Number of clauses : 122 ( 39 unt; 25 nHn; 47 RR)
% Number of literals : 684 ( 0 equ; 544 neg)
% Maximal clause size : 20 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 40 ( 39 usr; 2 prp; 0-16 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 1222 ( 543 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssNder1_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
( ~ ssNder1_0
| ssNder1_1r1(X) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(5,plain,
ssNder1_2r1r1(X,Y),
inference('REWRITE',[status(thm)],[clause3,clause1,3]) ).
cnf(clause12,negated_conjecture,
( ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_3r1r1r1(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(11,plain,
ssNder1_3r1r1r1(X,Y,Z),
inference('REWRITE',[status(thm)],[clause12,clause1,3,5]) ).
cnf(clause20,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/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(21,plain,
ssNder1_4r1r1r1r1(X,Y,Z,U),
inference('REWRITE',[status(thm)],[clause20,clause1,3,5,11]) ).
cnf(clause32,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/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(39,plain,
ssNder1_5r1r1r1r1r1(X,Y,Z,U,V),
inference('REWRITE',[status(thm)],[clause32,clause1,3,5,11,21]) ).
cnf(clause38,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/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(41,plain,
ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,skc28),
inference('REWRITE',[status(thm)],[clause38,clause1,3,5,11,21]) ).
cnf(clause41,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/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(43,plain,
~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,skc29),
inference('REWRITE',[status(thm)],[clause41,clause1,3,5,11,21]) ).
cnf(clause50,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/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(61,plain,
ssNder1_6r1r1r1r1r1r1(X,Y,Z,U,V,W),
inference('REWRITE',[status(thm)],[clause50,clause1,3,5,11,21,39]) ).
cnf(clause53,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
| ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
cnf(63,plain,
ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc26),
inference('REWRITE',[status(thm)],[clause53,clause1,3,5,11,21,39]) ).
cnf(clause68,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/sandbox2/benchmark/theBenchmark.p',clause68) ).
cnf(87,plain,
ssNder1_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1),
inference('REWRITE',[status(thm)],[clause68,clause1,3,5,11,21,39,61]) ).
cnf(clause69,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/sandbox2/benchmark/theBenchmark.p',clause69) ).
cnf(89,plain,
ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24),
inference('REWRITE',[status(thm)],[clause69,clause1,3,5,11,21,39,61]) ).
cnf(clause71,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/sandbox2/benchmark/theBenchmark.p',clause71) ).
cnf(91,plain,
~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc25),
inference('REWRITE',[status(thm)],[clause71,clause1,3,5,11,21,39,61]) ).
cnf(clause88,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/sandbox2/benchmark/theBenchmark.p',clause88) ).
cnf(117,plain,
ssNder1_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1),
inference('REWRITE',[status(thm)],[clause88,clause1,3,5,11,21,39,61,87]) ).
cnf(clause89,negated_conjecture,
( ~ ssPv20_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
| ssPv20_1r1(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
cnf(119,plain,
( ~ ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv20_1r1(X) ),
inference('REWRITE',[status(thm)],[clause89,clause1,3,5,11,21,39,61,87]) ).
cnf(clause90,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)
| ~ ssPv20_1r1(X)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
cnf(121,plain,
( ~ ssPv20_1r1(X)
| ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
inference('REWRITE',[status(thm)],[clause90,clause1,3,5,11,21,39,61,87]) ).
cnf(clause98,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)
| ~ ssPv18_3r1r1r1(X,Y,Z)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
cnf(127,plain,
( ~ ssPv18_3r1r1r1(X,Y,Z)
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
inference('REWRITE',[status(thm)],[clause98,clause1,3,5,11,21,39,61,87]) ).
cnf(clause99,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/sandbox2/benchmark/theBenchmark.p',clause99) ).
cnf(129,plain,
( ~ ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_3r1r1r1(X,Y,Z) ),
inference('REWRITE',[status(thm)],[clause99,clause1,3,5,11,21,39,61,87]) ).
cnf(clause104,negated_conjecture,
( ~ ssPv15_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
| ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
cnf(139,plain,
( ~ ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W) ),
inference('REWRITE',[status(thm)],[clause104,clause1,3,5,11,21,39,61,87]) ).
cnf(clause105,negated_conjecture,
( ~ 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_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
cnf(141,plain,
( ~ ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W)
| ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
inference('REWRITE',[status(thm)],[clause105,clause1,3,5,11,21,39,61,87]) ).
cnf(clause108,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/sandbox2/benchmark/theBenchmark.p',clause108) ).
cnf(147,plain,
ssNder1_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1),
inference('REWRITE',[status(thm)],[clause108,clause1,3,5,11,21,39,61,87,117]) ).
cnf(clause136,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/sandbox2/benchmark/theBenchmark.p',clause136) ).
cnf(181,plain,
ssNder1_10r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1),
inference('REWRITE',[status(thm)],[clause136,clause1,3,5,11,21,39,61,87,117,147]) ).
cnf(clause143,negated_conjecture,
( ~ ssPv15_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_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
cnf(195,plain,
( ~ ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
inference('REWRITE',[status(thm)],[clause143,clause1,3,5,11,21,39,61,87]) ).
cnf(clause146,negated_conjecture,
( ~ ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssPv20_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_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
cnf(199,plain,
( ~ ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ~ ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
inference('REWRITE',[status(thm)],[clause146,clause1,3,5,11,21,39,61,87]) ).
cnf(clause162,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/sandbox2/benchmark/theBenchmark.p',clause162) ).
cnf(223,plain,
ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1),
inference('REWRITE',[status(thm)],[clause162,clause1,3,5,11,21,39,61,87,117,147,181]) ).
cnf(clause189,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/sandbox2/benchmark/theBenchmark.p',clause189) ).
cnf(265,plain,
ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1),
inference('REWRITE',[status(thm)],[clause189,clause1,3,5,11,21,39,61,87,117,147,181,223]) ).
cnf(clause191,negated_conjecture,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,skc23)
| ~ 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/sandbox2/benchmark/theBenchmark.p',clause191) ).
cnf(269,plain,
~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,skc23),
inference('REWRITE',[status(thm)],[clause191,clause1,3,5,11,21,39,61,87,117,147,181,223]) ).
cnf(clause218,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/sandbox2/benchmark/theBenchmark.p',clause218) ).
cnf(315,plain,
ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2),
inference('REWRITE',[status(thm)],[clause218,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause221,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)
| ~ ssPv20_1r1(X)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause221) ).
cnf(321,plain,
( ~ ssPv20_1r1(X)
| ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause221,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause222,negated_conjecture,
( ~ ssPv20_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
| ssPv20_1r1(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause222) ).
cnf(323,plain,
( ~ ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ssPv20_1r1(X) ),
inference('REWRITE',[status(thm)],[clause222,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause238,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)
| ~ 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_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause238) ).
cnf(351,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv13_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause238,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause241,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/sandbox2/benchmark/theBenchmark.p',clause241) ).
cnf(357,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)],[clause241,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause247,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/sandbox2/benchmark/theBenchmark.p',clause247) ).
cnf(369,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)],[clause247,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause248,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/sandbox2/benchmark/theBenchmark.p',clause248) ).
cnf(371,plain,
ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2),
inference('REWRITE',[status(thm)],[clause248,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315]) ).
cnf(clause250,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/sandbox2/benchmark/theBenchmark.p',clause250) ).
cnf(375,plain,
~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,skc19),
inference('REWRITE',[status(thm)],[clause250,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315]) ).
cnf(clause286,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)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause286) ).
cnf(441,plain,
ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2),
inference('REWRITE',[status(thm)],[clause286,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371]) ).
cnf(clause287,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)
| ~ ssNder1_4r1r1r1r1(X,Y,Z,U)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,skc16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause287) ).
cnf(443,plain,
ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,skc16),
inference('REWRITE',[status(thm)],[clause287,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371]) ).
cnf(clause294,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/sandbox2/benchmark/theBenchmark.p',clause294) ).
cnf(457,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)],[clause294,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371]) ).
cnf(clause301,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)
| ~ ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ~ 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_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause301) ).
cnf(471,plain,
( ~ ssPv14_7r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1)
| ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause301,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371]) ).
cnf(clause309,negated_conjecture,
( ~ ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv13_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
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause309) ).
cnf(483,plain,
( ~ ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv13_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2) ),
inference('REWRITE',[status(thm)],[clause309,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause312,negated_conjecture,
( ~ ssPv13_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv20_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
| 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause312) ).
cnf(487,plain,
( ~ ssPv13_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| ~ ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| 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) ),
inference('REWRITE',[status(thm)],[clause312,clause1,3,5,11,21,39,61,87,117,147,181,223,265]) ).
cnf(clause320,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)
| ~ 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_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause320) ).
cnf(503,plain,
( ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1)
| ssPv9_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2) ),
inference('REWRITE',[status(thm)],[clause320,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371]) ).
cnf(clause332,negated_conjecture,
( ~ ssNder1_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)
| ~ ssPv18_3r1r1r1(X,Y,Z)
| ~ ssNder1_3r1r1r1(X,Y,Z)
| ~ ssNder1_2r1r1(X,Y)
| ~ ssNder1_1r1(X)
| ~ ssNder1_0
| ssPv18_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause332) ).
cnf(527,plain,
( ~ ssPv18_3r1r1r1(X,Y,Z)
| ssPv18_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2) ),
inference('REWRITE',[status(thm)],[clause332,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371,441]) ).
cnf(clause338,negated_conjecture,
( ~ ssPv15_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ~ ssNder1_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
| ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause338) ).
cnf(539,plain,
( ~ ssPv15_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ssPv15_6r1r1r1r1r1r1(X,Y,Z,U,V,W) ),
inference('REWRITE',[status(thm)],[clause338,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371,441]) ).
cnf(clause346,negated_conjecture,
( ~ ssPv12_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ~ ssNder1_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
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause346) ).
cnf(551,plain,
( ~ ssPv12_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1) ),
inference('REWRITE',[status(thm)],[clause346,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371,441]) ).
cnf(clause391,negated_conjecture,
( ~ ssPv9_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv14_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/sandbox2/benchmark/theBenchmark.p',clause391) ).
cnf(629,plain,
( ~ ssPv9_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv14_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)],[clause391,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371]) ).
cnf(clause433,negated_conjecture,
( ~ ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ~ ssPv18_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ~ ssNder1_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
| ssPv12_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ssPv15_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause433) ).
cnf(707,plain,
( ~ ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ~ ssPv18_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ssPv12_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2)
| ssPv15_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2) ),
inference('REWRITE',[status(thm)],[clause433,clause1,3,5,11,21,39,61,87,117,147,181,223,265,315,371,441]) ).
cnf(912,plain,
~ ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,X1),
inference('UR-RESOLVE',[status(thm)],[139,43]) ).
cnf(913,plain,
ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1),
inference('HYPERRESOLVE',[status(thm)],[141,41]) ).
cnf(960,plain,
ssPv13_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24,Y1,Z1,U1,V1,W1),
inference('HYPERRESOLVE',[status(thm)],[351,89]) ).
cnf(970,plain,
ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc26,X1,Y1,Z1,U1,V1,W1,X2,Y2),
inference('HYPERRESOLVE',[status(thm)],[471,63]) ).
cnf(973,plain,
~ ssPv15_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2),
inference('UR-RESOLVE',[status(thm)],[539,43]) ).
cnf(1067,plain,
( ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1)
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1)
| ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1) ),
inference('HYPERRESOLVE',[status(thm)],[195,913]) ).
cnf(1077,plain,
( ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1)
| ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1)
| ssPv20_1r1(X) ),
inference('HYPERRESOLVE',[status(thm)],[119,1067]) ).
cnf(1078,plain,
( ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc28,W,X1)
| ssPv20_1r1(X)
| ssPv18_3r1r1r1(X,Y,Z) ),
inference('HYPERRESOLVE',[status(thm)],[129,1077]) ).
cnf(1079,plain,
( ssPv20_1r1(X)
| ssPv18_3r1r1r1(X,Y,Z) ),
inference('HYPERRESOLVE',[status(thm)],[91,1078]) ).
cnf(1092,plain,
( ssPv20_1r1(X)
| ssPv18_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,U2) ),
inference('HYPERRESOLVE',[status(thm)],[527,1079]) ).
cnf(1100,plain,
( ssPv20_1r1(X)
| ssPv12_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,skc16)
| ssPv15_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2,skc16) ),
inference('HYPERRESOLVE',[status(thm)],[707,1092,443]) ).
cnf(1173,plain,
( ssPv20_1r1(X)
| ssPv12_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,skc16) ),
inference('HYPERRESOLVE',[status(thm)],[973,1100]) ).
cnf(1175,plain,
( ssPv20_1r1(X)
| ssPv12_9r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,X1,Y1) ),
inference('HYPERRESOLVE',[status(thm)],[551,1173]) ).
cnf(1179,plain,
( ssPv20_1r1(X)
| ssPv12_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,X1,Y1,Z1,U1,V1,W1) ),
inference('HYPERRESOLVE',[status(thm)],[357,1175]) ).
cnf(1188,plain,
( ssPv20_1r1(X)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,skc24,X1,Y1,Z1,U1,V1)
| ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,skc24,X1,Y1,Z1,U1,V1) ),
inference('HYPERRESOLVE',[status(thm)],[483,1179,960]) ).
cnf(1248,plain,
( ssPv20_1r1(X)
| ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,skc24,X1,Y1,Z1,U1,skc23) ),
inference('HYPERRESOLVE',[status(thm)],[269,1188]) ).
cnf(1257,plain,
ssPv20_1r1(X),
inference('HYPERRESOLVE',[status(thm)],[323,1248]) ).
cnf(1264,plain,
ssPv20_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1),
inference('REWRITE',[status(thm)],[121,1257]) ).
cnf(1265,plain,
( ~ ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv13_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1)
| ssPv15_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1) ),
inference('REWRITE',[status(thm)],[199,1264]) ).
cnf(1272,plain,
ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2),
inference('REWRITE',[status(thm)],[321,1257]) ).
cnf(1273,plain,
( ~ ssPv13_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2)
| 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) ),
inference('REWRITE',[status(thm)],[487,1272]) ).
cnf(1282,plain,
~ ssPv18_8r1r1r1r1r1r1r1r1(X,Y,Z,U,V,skc29,W,skc25),
inference('UR-RESOLVE',[status(thm)],[1265,91,912]) ).
cnf(1286,plain,
ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24,Y1,Z1,U1,V1,skc23),
inference('UR-RESOLVE',[status(thm)],[1273,960,269]) ).
cnf(1289,plain,
~ ssPv18_3r1r1r1(X,Y,Z),
inference('UR-RESOLVE',[status(thm)],[127,1282]) ).
cnf(1302,plain,
~ ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2),
inference('REWRITE',[status(thm)],[457,1289]) ).
cnf(1303,plain,
( ~ ssPv9_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,Y1,Z1,U1,V1,W1,X2,Y2,Z2)
| ~ ssPv14_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)],[629,1302]) ).
cnf(1312,plain,
~ ssPv9_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,skc26,X1,Y1,Z1,U1,V1,W1,X2,skc19),
inference('UR-RESOLVE',[status(thm)],[1303,970,375]) ).
cnf(1324,plain,
ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X,Y,Z,U,V,W,X1,skc24,Y1,Z1,U1,V1),
inference('HYPERRESOLVE',[status(thm)],[369,1286]) ).
cnf(1334,plain,
$false,
inference('UR-RESOLVE',[status(thm)],[503,1312,1324]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SYN836-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n007.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jul 12 02:43:48 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.18/0.45 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.46 *
% 0.18/0.46 *
% 0.18/0.46 #<PACKAGE "SNARK-USER">
% 0.18/0.46 *
% 0.18/0.46 SNARK-TPTP-OPTIONS
% 0.18/0.46 *
% 0.18/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.18/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.18/0.46 (USE-FACTORING :POS)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.18/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.18/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.18/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.18/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.18/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.18/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.18/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.18/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.18/0.46 *
% 0.18/0.46 "."
% 0.18/0.46 *
% 0.18/0.47 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-07-12T02:43:48
% 0.18/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n007.cluster.edu at 2022-07-12T02:43:48
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 20-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv2_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 14-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv6_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 14-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 14-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv1_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv5_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv1_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv4_11r1r1r1r1r1r1r1r1r1r1r1| is a 11-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv8_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv7_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv5_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv3_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv11_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv12_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv3_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv5_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv12_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv8_6r1r1r1r1r1r1| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv1_6r1r1r1r1r1r1| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv8_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv16_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv6_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv9_4r1r1r1r1| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv2_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv14_3r1r1r1| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv14_2r1r1| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv16_2r1r1| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv1_2r1r1| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv3_1r1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv12_1r1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv16_1r1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv5_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv7_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv10_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv8_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv9_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv7_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv8_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv6_2r1r1| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv11_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv13_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv16_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv17_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv6_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv12_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv8_4r1r1r1r1| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv10_4r1r1r1r1| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv12_4r1r1r1r1| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv10_5r1r1r1r1r1| is a 5-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv13_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv11_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv12_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv9_6r1r1r1r1r1r1| is a 6-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv7_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv11_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv10_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv6_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv4_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv9_8r1r1r1r1r1r1r1r1| is a 8-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv3_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv4_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv9_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv4_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv5_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv9_10r1r1r1r1r1r1r1r1r1r1| is a 10-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.09 WARNING:
% 0.91/1.09 |ssPv8_11r1r1r1r1r1r1r1r1r1r1r1| is a 11-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv7_11r1r1r1r1r1r1r1r1r1r1r1| is a 11-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv7_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv4_12r1r1r1r1r1r1r1r1r1r1r1r1| is a 12-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv5_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 14-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv2_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 15-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv4_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 15-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv3_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 15-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv4_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 16-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv3_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 16-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.10 WARNING:
% 0.91/1.10 |ssPv2_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 17-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv2_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 16-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv7_13r1r1r1r1r1r1r1r1r1r1r1r1r1| is a 13-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv4_7r1r1r1r1r1r1r1| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv9_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv14_5r1r1r1r1r1| is a 5-ary relation that occurs only negatively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv13_1r1| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv5_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv7_3r1r1r1| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv8_9r1r1r1r1r1r1r1r1r1| is a 9-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv4_5r1r1r1r1r1| is a 5-ary relation that occurs only positively; disabling rows that contain it.
% 0.91/1.11 WARNING:
% 0.91/1.11 |ssPv6_5r1r1r1r1r1| is a 5-ary relation that occurs only positively; disabling rows that contain it.
% 1.08/1.29
% 1.08/1.29
% 1.08/1.29 #||
% 1.08/1.29 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.08/1.29 % SZS output start Refutation
% See solution above
% 1.15/1.32 ||#
% 1.15/1.32
% 1.15/1.32 ; Summary of computation:
% 1.15/1.32 ; 1887 formulas have been input or derived (from 816 formulas).
% 1.15/1.32 ; 1334 (71%) were retained. Of these,
% 1.15/1.32 ; 750 (56%) were simplified or subsumed later,
% 1.15/1.32 ; 584 (44%) are still being kept.
% 1.15/1.32 ;
% 1.15/1.32 ; Run time in seconds excluding printing time:
% 1.15/1.32 ; 0.533 65% Read assertion file (1 call)
% 1.15/1.32 ; 0.080 10% Assert (536 calls)
% 1.15/1.32 ; 0.048 6% Process new row (1,262 calls)
% 1.15/1.32 ; 0.028 3% Resolution (1,630 calls)
% 1.15/1.32 ; 0.001 0% Paramodulation (815 calls)
% 1.15/1.32 ; 0.001 0% Factoring (143 calls)
% 1.15/1.32 ; 0.010 1% Condensing (733 calls)
% 1.15/1.32 ; 0.001 0% Forward subsumption (733 calls)
% 1.15/1.32 ; 0.005 1% Backward subsumption (613 calls)
% 1.15/1.32 ; 0.002 0% Clause clause subsumption (129 calls)
% 1.15/1.32 ; 0.061 7% Forward simplification (1,165 calls)
% 1.15/1.32 ; 0.009 1% Backward simplification (883 calls)
% 1.15/1.32 ; 0.001 0% Ordering (441 calls)
% 1.15/1.32 ; 0.000 0% Sortal reasoning (32 calls)
% 1.15/1.32 ; 0.020 2% Purity testing (1 call)
% 1.15/1.32 ; 0.025 3% Other
% 1.15/1.32 ; 0.825 Total
% 1.15/1.32 ; 0.858 Real time
% 1.15/1.32 ;
% 1.15/1.32 ; Term-hash-array has 543 terms in all.
% 1.15/1.32 ; Feature-vector-row-index has 316 entries (523 at peak, 613 added, 297 deleted).
% 1.15/1.32 ; Feature-vector-row-index has 181 nodes (341 at peak, 441 added, 260 deleted).
% 1.15/1.32 ; Retrieved 2,133 possibly forward subsuming rows in 733 calls.
% 1.15/1.32 ; Retrieved 1,362 possibly backward subsumed rows in 613 calls.
% 1.15/1.32 ; Path-index has 462 entries (515 at peak, 612 added, 150 deleted).
% 1.15/1.32 ; Path-index has 6,630 nodes (6,681 at peak, 7,170 added, 540 deleted).
% 1.15/1.32 ; Trie-index has 462 entries (515 at peak, 612 added, 150 deleted).
% 1.15/1.32 ; Trie-index has 4,785 nodes (5,312 at peak, 6,253 added, 1,468 deleted).
% 1.15/1.32 ; Retrieved 5,893 generalization terms in 6,310 calls.
% 1.15/1.32 ; Retrieved 277 instance terms in 269 calls.
% 1.15/1.32 ; Retrieved 3,448 unifiable terms in 3,289 calls.
% 1.15/1.32 ;
% 1.15/1.32 ; The agenda of rows to process has 1 entry:
% 1.15/1.32 ; 1 with value 17
% 1.15/1.32 ; The agenda of rows to give has 35 entries:
% 1.15/1.32 ; 2 with value (4 19) 1 with value (4 28) 1 with value (4 68)
% 1.15/1.32 ; 3 with value (4 20) 1 with value (4 38) 1 with value (4 69)
% 1.15/1.32 ; 2 with value (4 21) 1 with value (4 49) 1 with value (4 70)
% 1.15/1.32 ; 3 with value (4 22) 3 with value (4 59) 1 with value (4 71)
% 1.15/1.32 ; 3 with value (4 23) 1 with value (4 62) 1 with value (4 74)
% 1.15/1.32 ; 2 with value (4 24) 1 with value (4 65) 1 with value (4 77)
% 1.15/1.32 ; 2 with value (4 25) 1 with value (4 66) 1 with value (4 81)
% 1.15/1.32 ; 1 with value (4 26) 1 with value (4 67)
% 1.15/1.32 Evaluation took:
% 1.15/1.32 0.858 seconds of real time
% 1.15/1.32 0.821615 seconds of user run time
% 1.15/1.32 0.036062 seconds of system run time
% 1.15/1.32 [Run times include 0.041 seconds GC run time.]
% 1.15/1.32 0 calls to %EVAL
% 1.15/1.32 0 page faults and
% 1.15/1.32 83,212,784 bytes consed.
% 1.15/1.32 :PROOF-FOUND
% 1.15/1.32 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-07-12T02:43:49
% 1.15/1.32 :PROOF-FOUND
% 1.15/1.32 *
%------------------------------------------------------------------------------