%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN892-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.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:30:45 EDT 2022
% Result : Unsatisfiable 0.21s 0.54s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 34
% Syntax : Number of clauses : 91 ( 32 unt; 24 nHn; 91 RR)
% Number of literals : 468 ( 0 equ; 353 neg)
% Maximal clause size : 19 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 2 prp; 0-15 aty)
% Number of functors : 26 ( 26 usr; 26 con; 0-0 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
ssNder1_0,
file('SYN892-1.p',unknown),
[] ).
cnf(2,axiom,
( ~ ssNder1_0
| ssNder1_1r1(u) ),
file('SYN892-1.p',unknown),
[] ).
cnf(3,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_0
| ssNder1_2r1r1(u,v) ),
file('SYN892-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_0
| ssNder1_3r1r1r1(u,v,w) ),
file('SYN892-1.p',unknown),
[] ).
cnf(5,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(u,v,w,x) ),
file('SYN892-1.p',unknown),
[] ).
cnf(6,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(u,v,w,x,skc30) ),
file('SYN892-1.p',unknown),
[] ).
cnf(7,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssPv16_5r1r1r1r1r1(u,v,w,x,skc31)
| ~ ssNder1_0 ),
file('SYN892-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(u,v,w,x,y) ),
file('SYN892-1.p',unknown),
[] ).
cnf(9,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_0
| ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,skc28) ),
file('SYN892-1.p',unknown),
[] ).
cnf(10,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,skc29)
| ~ ssNder1_0 ),
file('SYN892-1.p',unknown),
[] ).
cnf(11,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z) ),
file('SYN892-1.p',unknown),
[] ).
cnf(12,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,skc26) ),
file('SYN892-1.p',unknown),
[] ).
cnf(13,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,skc27)
| ~ ssNder1_0 ),
file('SYN892-1.p',unknown),
[] ).
cnf(14,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1) ),
file('SYN892-1.p',unknown),
[] ).
cnf(17,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2) ),
file('SYN892-1.p',unknown),
[] ).
cnf(18,axiom,
( ~ ssPv20_1r1(u)
| ~ ssNder1_1r1(u)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_0
| ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ssPv19_2r1r1(u,v) ),
file('SYN892-1.p',unknown),
[] ).
cnf(19,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3) ),
file('SYN892-1.p',unknown),
[] ).
cnf(20,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4) ),
file('SYN892-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5) ),
file('SYN892-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6) ),
file('SYN892-1.p',unknown),
[] ).
cnf(25,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc22) ),
file('SYN892-1.p',unknown),
[] ).
cnf(26,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc23)
| ~ ssNder1_0 ),
file('SYN892-1.p',unknown),
[] ).
cnf(28,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7) ),
file('SYN892-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc20) ),
file('SYN892-1.p',unknown),
[] ).
cnf(30,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc21)
| ~ ssNder1_0 ),
file('SYN892-1.p',unknown),
[] ).
cnf(32,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
file('SYN892-1.p',unknown),
[] ).
cnf(34,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc18) ),
file('SYN892-1.p',unknown),
[] ).
cnf(36,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssPv19_2r1r1(u,v)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4) ),
file('SYN892-1.p',unknown),
[] ).
cnf(37,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssPv16_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_0
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ssPv17_4r1r1r1r1(u,v,w,x) ),
file('SYN892-1.p',unknown),
[] ).
cnf(39,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssPv19_2r1r1(u,v)
| ~ ssNder1_2r1r1(u,v)
| ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_0 ),
file('SYN892-1.p',unknown),
[] ).
cnf(40,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv20_1r1(u) ),
file('SYN892-1.p',unknown),
[] ).
cnf(41,axiom,
( ~ ssNder1_1r1(u)
| ~ ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssPv17_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(u,v,w,x,y)
| ssPv19_2r1r1(u,v) ),
file('SYN892-1.p',unknown),
[] ).
cnf(46,axiom,
( ~ ssNder1_1r1(u)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssPv11_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y)
| ssPv18_3r1r1r1(u,v,w) ),
file('SYN892-1.p',unknown),
[] ).
cnf(53,axiom,
( ~ ssNder1_1r1(u)
| ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssNder1_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssPv17_4r1r1r1r1(u,v,w,x)
| ~ ssNder1_4r1r1r1r1(u,v,w,x)
| ~ ssPv18_3r1r1r1(u,v,w)
| ~ ssNder1_3r1r1r1(u,v,w)
| ~ ssNder1_2r1r1(u,v)
| ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
file('SYN892-1.p',unknown),
[] ).
cnf(87,plain,
ssNder1_1r1(u),
inference(mrr,[status(thm)],[2,1]),
[iquote('0:MRR:2.0,1.0')] ).
cnf(88,plain,
ssNder1_2r1r1(u,v),
inference(mrr,[status(thm)],[3,87,1]),
[iquote('0:MRR:3.0,3.1,87.0,1.0')] ).
cnf(89,plain,
ssNder1_3r1r1r1(u,v,w),
inference(mrr,[status(thm)],[4,87,88,1]),
[iquote('0:MRR:4.0,4.1,4.2,87.0,88.0,1.0')] ).
cnf(90,plain,
ssNder1_4r1r1r1r1(u,v,w,x),
inference(mrr,[status(thm)],[5,87,88,89,1]),
[iquote('0:MRR:5.0,5.1,5.2,5.3,87.0,88.0,89.0,1.0')] ).
cnf(91,plain,
ssPv16_5r1r1r1r1r1(u,v,w,x,skc30),
inference(mrr,[status(thm)],[6,87,88,89,1]),
[iquote('0:MRR:6.0,6.1,6.2,6.3,87.0,88.0,89.0,1.0')] ).
cnf(92,plain,
~ ssPv16_5r1r1r1r1r1(u,v,w,x,skc31),
inference(mrr,[status(thm)],[7,87,89,88,1]),
[iquote('0:MRR:7.0,7.1,7.2,7.4,87.0,89.0,88.0,1.0')] ).
cnf(93,plain,
ssNder1_5r1r1r1r1r1(u,v,w,x,y),
inference(mrr,[status(thm)],[8,87,89,88,90,1]),
[iquote('0:MRR:8.0,8.1,8.2,8.3,8.4,87.0,89.0,88.0,90.0,1.0')] ).
cnf(94,plain,
ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,skc28),
inference(mrr,[status(thm)],[9,87,89,88,90,1]),
[iquote('0:MRR:9.0,9.1,9.2,9.3,9.4,87.0,89.0,88.0,90.0,1.0')] ).
cnf(95,plain,
~ ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,skc29),
inference(mrr,[status(thm)],[10,87,90,89,88,1]),
[iquote('0:MRR:10.0,10.1,10.2,10.3,10.5,87.0,90.0,89.0,88.0,1.0')] ).
cnf(96,plain,
ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z),
inference(mrr,[status(thm)],[11,87,90,89,88,93,1]),
[iquote('0:MRR:11.0,11.1,11.2,11.3,11.4,11.5,87.0,90.0,89.0,88.0,93.0,1.0')] ).
cnf(97,plain,
ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,skc26),
inference(mrr,[status(thm)],[12,87,90,89,88,93,1]),
[iquote('0:MRR:12.0,12.1,12.2,12.3,12.4,12.5,87.0,90.0,89.0,88.0,93.0,1.0')] ).
cnf(98,plain,
~ ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,skc27),
inference(mrr,[status(thm)],[13,87,93,90,89,88,1]),
[iquote('0:MRR:13.0,13.1,13.2,13.3,13.4,13.6,87.0,93.0,90.0,89.0,88.0,1.0')] ).
cnf(99,plain,
ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1),
inference(mrr,[status(thm)],[14,87,93,90,89,88,96,1]),
[iquote('0:MRR:14.0,14.1,14.2,14.3,14.4,14.5,14.6,87.0,93.0,90.0,89.0,88.0,96.0,1.0')] ).
cnf(102,plain,
ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2),
inference(mrr,[status(thm)],[17,87,96,93,90,89,88,99,1]),
[iquote('0:MRR:17.0,17.1,17.2,17.3,17.4,17.5,17.6,17.7,87.0,96.0,93.0,90.0,89.0,88.0,99.0,1.0')] ).
cnf(103,plain,
( ~ ssPv20_1r1(u)
| ssPv19_2r1r1(u,v)
| ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1) ),
inference(mrr,[status(thm)],[18,87,90,89,88,96,93,1]),
[iquote('0:MRR:18.1,18.2,18.3,18.4,18.5,18.6,18.7,87.0,90.0,89.0,88.0,96.0,93.0,1.0')] ).
cnf(104,plain,
ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3),
inference(mrr,[status(thm)],[19,87,99,96,93,90,89,88,102,1]),
[iquote('0:MRR:19.0,19.1,19.2,19.3,19.4,19.5,19.6,19.7,19.8,87.0,99.0,96.0,93.0,90.0,89.0,88.0,102.0,1.0')] ).
cnf(105,plain,
ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4),
inference(mrr,[status(thm)],[20,87,102,99,96,93,90,89,88,104,1]),
[iquote('0:MRR:20.0,20.1,20.2,20.3,20.4,20.5,20.6,20.7,20.8,20.9,87.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,104.0,1.0')] ).
cnf(107,plain,
ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5),
inference(mrr,[status(thm)],[22,87,104,102,99,96,93,90,89,88,105,1]),
[iquote('0:MRR:22.0,22.1,22.2,22.3,22.4,22.5,22.6,22.7,22.8,22.9,22.10,87.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,105.0,1.0')] ).
cnf(109,plain,
ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6),
inference(mrr,[status(thm)],[24,87,105,104,102,99,96,93,90,89,88,107,1]),
[iquote('0:MRR:24.0,24.1,24.2,24.3,24.4,24.5,24.6,24.7,24.8,24.9,24.10,24.11,87.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,107.0,1.0')] ).
cnf(110,plain,
ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc22),
inference(mrr,[status(thm)],[25,87,105,104,102,99,96,93,90,89,88,107,1]),
[iquote('0:MRR:25.0,25.1,25.2,25.3,25.4,25.5,25.6,25.7,25.8,25.9,25.10,25.11,87.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,107.0,1.0')] ).
cnf(111,plain,
~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc23),
inference(mrr,[status(thm)],[26,87,107,105,104,102,99,96,93,90,89,88,1]),
[iquote('0:MRR:26.0,26.1,26.2,26.3,26.4,26.5,26.6,26.7,26.8,26.9,26.10,26.12,87.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,1.0')] ).
cnf(113,plain,
ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7),
inference(mrr,[status(thm)],[28,87,107,105,104,102,99,96,93,90,89,88,109,1]),
[iquote('0:MRR:28.0,28.1,28.2,28.3,28.4,28.5,28.6,28.7,28.8,28.9,28.10,28.11,28.12,87.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,109.0,1.0')] ).
cnf(114,plain,
ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc20),
inference(mrr,[status(thm)],[29,87,107,105,104,102,99,96,93,90,89,88,109,1]),
[iquote('0:MRR:29.0,29.1,29.2,29.3,29.4,29.5,29.6,29.7,29.8,29.9,29.10,29.11,29.12,87.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,109.0,1.0')] ).
cnf(115,plain,
~ ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc21),
inference(mrr,[status(thm)],[30,87,109,107,105,104,102,99,96,93,90,89,88,1]),
[iquote('0:MRR:30.0,30.1,30.2,30.3,30.4,30.5,30.6,30.7,30.8,30.9,30.10,30.11,30.13,87.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,1.0')] ).
cnf(117,plain,
ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8),
inference(mrr,[status(thm)],[32,87,109,107,105,104,102,99,96,93,90,89,88,113,1]),
[iquote('0:MRR:32.0,32.1,32.2,32.3,32.4,32.5,32.6,32.7,32.8,32.9,32.10,32.11,32.12,32.13,87.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,113.0,1.0')] ).
cnf(119,plain,
ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc18),
inference(mrr,[status(thm)],[34,87,109,107,105,104,102,99,96,93,90,89,88,113,1]),
[iquote('0:MRR:34.0,34.1,34.2,34.3,34.4,34.5,34.6,34.7,34.8,34.9,34.10,34.11,34.12,34.13,87.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,113.0,1.0')] ).
cnf(121,plain,
( ~ ssPv19_2r1r1(u,v)
| ~ ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7) ),
inference(mrr,[status(thm)],[36,87,107,105,104,102,99,96,93,90,89,88,109,1]),
[iquote('0:MRR:36.0,36.1,36.2,36.3,36.4,36.5,36.7,36.8,36.9,36.10,36.12,36.13,36.14,87.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,109.0,1.0')] ).
cnf(122,plain,
( ~ ssPv16_5r1r1r1r1r1(u,v,w,x,y)
| ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7) ),
inference(mrr,[status(thm)],[37,87,107,105,104,102,99,96,93,90,89,88,109,1]),
[iquote('0:MRR:37.0,37.1,37.2,37.3,37.4,37.5,37.6,37.8,37.9,37.10,37.11,37.12,37.13,87.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,109.0,1.0')] ).
cnf(124,plain,
( ~ ssPv19_2r1r1(u,v)
| ~ ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7) ),
inference(mrr,[status(thm)],[39,87,109,107,105,104,102,99,96,93,90,89,88,1]),
[iquote('0:MRR:39.0,39.1,39.3,39.4,39.5,39.6,39.8,39.9,39.10,39.11,39.12,39.14,39.16,87.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,1.0')] ).
cnf(125,plain,
( ssPv20_1r1(u)
| ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
inference(mrr,[status(thm)],[40,87,109,107,105,104,102,99,96,93,90,89,88,113,1]),
[iquote('0:MRR:40.0,40.1,40.2,40.3,40.4,40.5,40.6,40.7,40.8,40.9,40.10,40.11,40.12,40.13,87.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,113.0,1.0')] ).
cnf(126,plain,
( ~ ssPv17_4r1r1r1r1(u,v,w,x)
| ~ ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv19_2r1r1(u,v)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y) ),
inference(mrr,[status(thm)],[41,87,109,107,105,104,102,99,96,93,90,89,88,113,1]),
[iquote('0:MRR:41.0,41.2,41.3,41.4,41.5,41.6,41.7,41.8,41.9,41.11,41.12,41.13,41.14,41.15,87.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,113.0,1.0')] ).
cnf(131,plain,
( ~ ssPv11_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv18_3r1r1r1(u,v,w)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y)
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
inference(mrr,[status(thm)],[46,87,109,107,105,104,102,99,96,93,90,89,88,113,1]),
[iquote('0:MRR:46.0,46.1,46.2,46.4,46.5,46.6,46.7,46.8,46.9,46.10,46.11,46.12,46.13,46.14,87.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,113.0,1.0')] ).
cnf(138,plain,
( ~ ssPv18_3r1r1r1(u,v,w)
| ~ ssPv17_4r1r1r1r1(u,v,w,x)
| ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9)
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
inference(mrr,[status(thm)],[53,87,113,109,107,105,104,102,99,96,93,90,89,88,117,1]),
[iquote('0:MRR:53.0,53.2,53.3,53.4,53.5,53.6,53.7,53.8,53.9,53.10,53.12,53.14,53.15,53.16,53.17,87.0,113.0,109.0,107.0,105.0,104.0,102.0,99.0,96.0,93.0,90.0,89.0,88.0,117.0,1.0')] ).
cnf(178,plain,
( ~ ssPv20_1r1(u)
| ssPv19_2r1r1(u,v)
| ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z) ),
inference(res,[status(thm),theory(equality)],[103,98]),
[iquote('0:Res:103.3,98.0')] ).
cnf(179,plain,
( ~ ssPv20_1r1(u)
| ssPv19_2r1r1(u,v) ),
inference(res,[status(thm),theory(equality)],[178,95]),
[iquote('0:Res:178.2,95.0')] ).
cnf(182,plain,
( ssPv20_1r1(u)
| ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z) ),
inference(res,[status(thm),theory(equality)],[125,115]),
[iquote('0:Res:125.3,115.0')] ).
cnf(183,plain,
( ~ ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv19_2r1r1(u,v)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y) ),
inference(res,[status(thm),theory(equality)],[114,126]),
[iquote('0:Res:114.0,126.1')] ).
cnf(184,plain,
( ssPv20_1r1(u)
| ssPv17_4r1r1r1r1(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[182,95]),
[iquote('0:Res:182.2,95.0')] ).
cnf(186,plain,
( ssPv20_1r1(u)
| ssPv19_2r1r1(u,v)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y) ),
inference(res,[status(thm),theory(equality)],[184,183]),
[iquote('0:Res:184.1,183.0')] ).
cnf(187,plain,
( ssPv19_2r1r1(u,v)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y) ),
inference(mrr,[status(thm)],[186,179]),
[iquote('0:MRR:186.0,179.0')] ).
cnf(188,plain,
ssPv19_2r1r1(u,v),
inference(res,[status(thm),theory(equality)],[187,92]),
[iquote('0:Res:187.1,92.0')] ).
cnf(190,plain,
( ~ ssPv15_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7) ),
inference(mrr,[status(thm)],[121,188]),
[iquote('0:MRR:121.0,188.0')] ).
cnf(192,plain,
( ~ ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7) ),
inference(mrr,[status(thm)],[124,188]),
[iquote('0:MRR:124.0,188.0')] ).
cnf(197,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc28,z,x1,x2,x3)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc28,z,x1,x2,x3,x4,x5,x6) ),
inference(res,[status(thm),theory(equality)],[94,190]),
[iquote('0:Res:94.0,190.0')] ).
cnf(198,plain,
ssPv11_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc28,z,x1,x2,x3),
inference(res,[status(thm),theory(equality)],[197,111]),
[iquote('0:Res:197.1,111.0')] ).
cnf(208,plain,
( ssPv18_3r1r1r1(u,v,w)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y)
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc28,z,x1,x2,x3,x4,x5,x6,x7) ),
inference(res,[status(thm),theory(equality)],[198,131]),
[iquote('0:Res:198.0,131.0')] ).
cnf(210,plain,
( ssPv18_3r1r1r1(u,v,w)
| ssPv16_5r1r1r1r1r1(u,v,w,x,y) ),
inference(res,[status(thm),theory(equality)],[208,115]),
[iquote('0:Res:208.2,115.0')] ).
cnf(212,plain,
ssPv18_3r1r1r1(u,v,w),
inference(res,[status(thm),theory(equality)],[210,92]),
[iquote('0:Res:210.1,92.0')] ).
cnf(216,plain,
( ~ ssPv17_4r1r1r1r1(u,v,w,x)
| ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9)
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
inference(mrr,[status(thm)],[138,212]),
[iquote('0:MRR:138.0,212.0')] ).
cnf(222,plain,
( ~ ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6) ),
inference(res,[status(thm),theory(equality)],[110,192]),
[iquote('0:Res:110.0,192.2')] ).
cnf(227,plain,
( ~ ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
inference(res,[status(thm),theory(equality)],[119,216]),
[iquote('0:Res:119.0,216.1')] ).
cnf(231,plain,
( ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,skc30,y,z,x1,x2,x3,x4,x5)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,skc30,y,z,x1,x2,x3,x4,x5,x6) ),
inference(res,[status(thm),theory(equality)],[91,122]),
[iquote('0:Res:91.0,122.0')] ).
cnf(234,plain,
( ssPv17_4r1r1r1r1(u,v,w,x)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,skc30,y,z,x1,x2,x3,x4,x5) ),
inference(res,[status(thm),theory(equality)],[231,111]),
[iquote('0:Res:231.2,111.0')] ).
cnf(236,plain,
( ~ ssPv14_7r1r1r1r1r1r1r1(u,v,w,x,skc30,y,z)
| ssPv17_4r1r1r1r1(u,v,w,x) ),
inference(res,[status(thm),theory(equality)],[234,222]),
[iquote('0:Res:234.1,222.1')] ).
cnf(237,plain,
ssPv17_4r1r1r1r1(u,v,w,x),
inference(res,[status(thm),theory(equality)],[97,236]),
[iquote('0:Res:97.0,236.0')] ).
cnf(239,plain,
ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8),
inference(mrr,[status(thm)],[227,237]),
[iquote('0:MRR:227.0,237.0')] ).
cnf(242,plain,
$false,
inference(unc,[status(thm)],[239,115]),
[iquote('0:UnC:239.0,115.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYN892-1 : TPTP v8.1.0. Released v2.5.0.
% 0.08/0.14 % Command : run_spass %d %s
% 0.14/0.36 % Computer : n021.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Tue Jul 12 03:22:24 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.21/0.54
% 0.21/0.54 SPASS V 3.9
% 0.21/0.54 SPASS beiseite: Proof found.
% 0.21/0.54 % SZS status Theorem
% 0.21/0.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.54 SPASS derived 63 clauses, backtracked 0 clauses, performed 0 splits and kept 143 clauses.
% 0.21/0.54 SPASS allocated 76470 KBytes.
% 0.21/0.54 SPASS spent 0:00:00.18 on the problem.
% 0.21/0.54 0:00:00.06 for the input.
% 0.21/0.54 0:00:00.00 for the FLOTTER CNF translation.
% 0.21/0.54 0:00:00.00 for inferences.
% 0.21/0.54 0:00:00.00 for the backtracking.
% 0.21/0.54 0:00:00.08 for the reduction.
% 0.21/0.54
% 0.21/0.54
% 0.21/0.54 Here is a proof with depth 5, length 91 :
% 0.21/0.54 % SZS output start Refutation
% See solution above
% 0.21/0.55 Formulae used in the proof : clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause9 clause10 clause11 clause12 clause13 clause14 clause17 clause18 clause19 clause20 clause22 clause24 clause25 clause26 clause28 clause29 clause30 clause32 clause34 clause36 clause37 clause39 clause40 clause41 clause46 clause53
% 0.21/0.55
%------------------------------------------------------------------------------