%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN759-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:17:14 PM UTC 2026
% Result : Unsatisfiable 220.38s 28.54s
% Output : CNFRefutation 7.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 118
% Number of leaves : 39
% Syntax : Number of formulae : 631 ( 7 unt; 0 def)
% Number of atoms : 3388 ( 0 equ)
% Maximal formula atoms : 9 ( 5 avg)
% Number of connectives : 4399 (1642 ~;2757 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 1 ( 1 usr; 0 con; 1-1 aty)
% Number of variables : 1314 (1314 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [U] : ssRr(U,skf1(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
! [U,V,W,X] :
( ssPv3(W)
| ssPv2(W)
| ssPv2(X)
| ssPv1(V)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv3(W)
| ssPv1(V)
| ~ ssPv1(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
! [U,V,W,X] :
( ssPv2(W)
| ssPv1(X)
| ssPv2(V)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv2(W)
| ssPv2(V)
| ~ ssPv3(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv3(X)
| ssPv3(V)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
! [U,V,W,X] :
( ssPv2(W)
| ssPv3(V)
| ~ ssPv1(W)
| ~ ssPv4(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
! [U,V,W,X] :
( ssPv1(W)
| ssPv4(V)
| ~ ssPv4(W)
| ~ ssPv3(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
! [U,V,W,X] :
( ssPv3(W)
| ~ ssPv4(W)
| ~ ssPv1(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
! [U,V,W,X] :
( ssPv1(W)
| ~ ssPv3(W)
| ~ ssPv2(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(W)
| ssPv2(Y)
| ssPv3(V)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv4(W)
| ssPv1(Y)
| ssPv4(V)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv1(W)
| ssPv2(Y)
| ssPv3(X)
| ~ ssRr(W,Y)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv4(W)
| ssPv3(Y)
| ssPv4(V)
| ~ ssRr(W,Y)
| ~ ssPv2(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv4(W)
| ssPv2(Y)
| ssPv2(V)
| ~ ssRr(W,Y)
| ~ ssPv3(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv2(W)
| ssPv1(W)
| ssPv3(Y)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(Y)
| ssPv3(V)
| ~ ssPv4(W)
| ~ ssRr(W,Y)
| ~ ssPv2(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(W)
| ssPv1(Y)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv1(W)
| ssPv1(Y)
| ~ ssRr(W,Y)
| ~ ssPv3(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv2(Y)
| ssPv4(V)
| ~ ssPv3(W)
| ~ ssPv2(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv2(Y)
| ssPv3(V)
| ~ ssPv4(W)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv1(W)
| ssPv3(Y)
| ~ ssPv2(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(W)
| ssPv1(W)
| ~ ssRr(W,X)
| ~ ssPv2(Y)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv4(W)
| ssPv3(Y)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv2(W)
| ~ ssPv3(Y)
| ~ ssRr(W,Y)
| ~ ssPv4(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv2(W)
| ~ ssPv3(Y)
| ~ ssRr(W,Y)
| ~ ssPv4(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
! [U,V,W,X,Y] :
( ~ ssPv1(W)
| ~ ssPv3(Y)
| ~ ssRr(W,Y)
| ~ ssPv4(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv4(W)
| ssPv1(Z)
| ssPv2(Y)
| ssPv3(V)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv1(Z)
| ssPv1(Y)
| ssPv3(V)
| ~ ssPv3(W)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv2(W)
| ssPv2(Z)
| ssPv4(Y)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv1(W)
| ssPv3(Z)
| ssPv4(Y)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv4(W)
| ssPv1(Y)
| ssPv2(V)
| ~ ssPv2(Z)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv4(W)
| ssPv1(Z)
| ssPv2(Y)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv2(W)
| ssPv4(Z)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssPv1(Y)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv4(W)
| ssPv1(Z)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssPv2(Y)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv4(W)
| ssPv4(Y)
| ~ ssPv1(Z)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv1(W)
| ssPv3(Y)
| ~ ssPv4(Z)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv2(Y)
| ~ ssPv2(W)
| ~ ssPv3(Z)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
! [U,V,W,X,Y,Z] :
( ssPv4(W)
| ~ ssPv1(Z)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssPv2(Y)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,plain,
! [X0] : ssRr(X0,skf1(X0)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f53,plain,
! [W] :
( ssPv3(W)
| ssPv2(W)
| ! [X] :
( ssPv2(X)
| ! [V] :
( ssPv1(V)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f54,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ssPv2(X2)
| ssPv2(X3)
| ssPv1(X1)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
! [W] :
( ssPv4(W)
| ssPv3(W)
| ! [V] :
( ssPv1(V)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f56,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv3(X2)
| ssPv1(X1)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [W] :
( ssPv2(W)
| ! [X] :
( ssPv1(X)
| ! [V] :
( ssPv2(V)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f58,plain,
! [X0,X1,X2,X3] :
( ssPv2(X2)
| ssPv1(X3)
| ssPv2(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [W] :
( ssPv4(W)
| ssPv2(W)
| ! [V] :
( ssPv2(V)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f60,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv2(X2)
| ssPv2(X1)
| ~ ssPv3(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [W] :
( ssPv4(W)
| ! [X] :
( ssPv3(X)
| ! [V] :
( ssPv3(V)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f62,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv3(X3)
| ssPv3(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [W] :
( ssPv2(W)
| ! [V] :
( ssPv3(V)
| ~ ssPv1(W)
| ! [X] :
( ~ ssPv4(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f64,plain,
! [X0,X1,X2,X3] :
( ssPv2(X2)
| ssPv3(X1)
| ~ ssPv1(X2)
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [W] :
( ssPv1(W)
| ! [V] :
( ssPv4(V)
| ~ ssPv4(W)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ssPv4(X1)
| ~ ssPv4(X2)
| ~ ssPv3(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [W] :
( ssPv3(W)
| ~ ssPv4(W)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ~ ssPv4(X2)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [W] :
( ssPv1(W)
| ~ ssPv3(W)
| ! [X] :
( ~ ssPv2(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f70,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ~ ssPv3(X2)
| ~ ssPv2(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [W] :
( ssPv3(W)
| ! [Y] :
( ssPv2(Y)
| ! [V] :
( ssPv3(V)
| ~ ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f72,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X2)
| ssPv2(X4)
| ssPv3(X1)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [W] :
( ssPv4(W)
| ! [Y] :
( ssPv1(Y)
| ! [V] :
( ssPv4(V)
| ~ ssPv3(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f74,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv1(X4)
| ssPv4(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
! [W] :
( ssPv1(W)
| ! [Y] :
( ssPv2(Y)
| ! [X] :
( ssPv3(X)
| ~ ssRr(W,Y)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f76,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ssPv2(X4)
| ssPv3(X3)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [W] :
( ssPv4(W)
| ! [Y] :
( ssPv3(Y)
| ! [V] :
( ssPv4(V)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv2(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f78,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv3(X4)
| ssPv4(X1)
| ~ ssRr(X2,X4)
| ~ ssPv2(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [W] :
( ssPv4(W)
| ! [Y] :
( ssPv2(Y)
| ! [V] :
( ssPv2(V)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f80,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv2(X4)
| ssPv2(X1)
| ~ ssRr(X2,X4)
| ~ ssPv3(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [W] :
( ssPv2(W)
| ssPv1(W)
| ! [Y] :
( ssPv3(Y)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f82,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X2)
| ssPv1(X2)
| ssPv3(X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [Y] :
( ssPv3(Y)
| ! [V] :
( ssPv3(V)
| ! [W] :
( ~ ssPv4(W)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv2(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f84,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X4)
| ssPv3(X1)
| ~ ssPv4(X2)
| ~ ssRr(X2,X4)
| ~ ssPv2(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f87,plain,
! [W] :
( ssPv3(W)
| ! [Y] :
( ssPv1(Y)
| ~ ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f88,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X2)
| ssPv1(X4)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
! [W] :
( ssPv1(W)
| ! [Y] :
( ssPv1(Y)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f90,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ssPv1(X4)
| ~ ssRr(X2,X4)
| ~ ssPv3(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [Y] :
( ssPv2(Y)
| ! [V] :
( ssPv4(V)
| ! [W] :
( ~ ssPv3(W)
| ~ ssPv2(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f92,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X4)
| ssPv4(X1)
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [Y] :
( ssPv2(Y)
| ! [V] :
( ssPv3(V)
| ! [W] :
( ~ ssPv4(W)
| ~ ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f94,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X4)
| ssPv3(X1)
| ~ ssPv4(X2)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
! [W] :
( ssPv1(W)
| ! [Y] :
( ssPv3(Y)
| ~ ssPv2(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f96,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ssPv3(X4)
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [W] :
( ssPv3(W)
| ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ! [Y] :
( ~ ssPv2(Y)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f98,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X2)
| ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssPv2(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
! [W] :
( ssPv4(W)
| ! [Y] :
( ssPv3(Y)
| ~ ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f100,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv3(X4)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
! [W] :
( ssPv2(W)
| ! [Y] :
( ~ ssPv3(Y)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv4(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f102,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X2)
| ~ ssPv3(X4)
| ~ ssRr(X2,X4)
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f105,plain,
! [W] :
( ssPv2(W)
| ! [Y] :
( ~ ssPv3(Y)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv4(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f106,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X2)
| ~ ssPv3(X4)
| ~ ssRr(X2,X4)
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
! [W] :
( ~ ssPv1(W)
| ! [Y] :
( ~ ssPv3(Y)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv4(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssPv1(X2)
| ~ ssPv3(X4)
| ~ ssRr(X2,X4)
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [W] :
( ssPv4(W)
| ! [Z] :
( ssPv1(Z)
| ! [Y] :
( ssPv2(Y)
| ! [V] :
( ssPv3(V)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv1(X5)
| ssPv2(X4)
| ssPv3(X1)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [Z] :
( ssPv1(Z)
| ! [Y] :
( ssPv1(Y)
| ! [V] :
( ssPv3(V)
| ! [W] :
( ~ ssPv3(W)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f112,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv1(X5)
| ssPv1(X4)
| ssPv3(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [W] :
( ssPv2(W)
| ! [Z] :
( ssPv2(Z)
| ! [Y] :
( ssPv4(Y)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f114,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv2(X2)
| ssPv2(X5)
| ssPv4(X4)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [W] :
( ssPv1(W)
| ! [Z] :
( ssPv3(Z)
| ! [Y] :
( ssPv4(Y)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f33]) ).
fof(f116,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv1(X2)
| ssPv3(X5)
| ssPv4(X4)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [W] :
( ssPv4(W)
| ! [Y] :
( ssPv1(Y)
| ! [V] :
( ssPv2(V)
| ! [Z] :
( ~ ssPv2(Z)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f118,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv1(X4)
| ssPv2(X1)
| ~ ssPv2(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
! [W] :
( ssPv4(W)
| ! [Z] :
( ssPv1(Z)
| ! [Y] :
( ssPv2(Y)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f120,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv1(X5)
| ssPv2(X4)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [W] :
( ssPv2(W)
| ! [Z] :
( ssPv4(Z)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ! [Y] :
( ~ ssPv1(Y)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f122,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv2(X2)
| ssPv4(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssPv1(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [W] :
( ssPv4(W)
| ! [Z] :
( ssPv1(Z)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ! [Y] :
( ~ ssPv2(Y)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f124,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv1(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssPv2(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f127,plain,
! [W] :
( ssPv4(W)
| ! [Y] :
( ssPv4(Y)
| ! [Z] :
( ~ ssPv1(Z)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f39]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv4(X4)
| ~ ssPv1(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f135,plain,
! [W] :
( ssPv1(W)
| ! [Y] :
( ssPv3(Y)
| ! [Z] :
( ~ ssPv4(Z)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f136,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv1(X2)
| ssPv3(X4)
| ~ ssPv4(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f139,plain,
! [Y] :
( ssPv2(Y)
| ! [W] :
( ~ ssPv2(W)
| ! [Z] :
( ~ ssPv3(Z)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f45]) ).
fof(f140,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv2(X4)
| ~ ssPv2(X2)
| ~ ssPv3(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,plain,
! [W] :
( ssPv4(W)
| ! [Z] :
( ~ ssPv1(Z)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ! [Y] :
( ~ ssPv2(Y)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f46]) ).
fof(f142,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ~ ssPv1(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssPv2(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f153,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f54,f52]) ).
fof(f156,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f153,f52]) ).
fof(f157,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(X1)
| ~ ssPv1(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f56,f52]) ).
fof(f160,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f157,f52]) ).
fof(f163,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(X1)
| ~ ssPv3(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f58,f52]) ).
fof(f167,plain,
! [X0,X1,X2] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv2(X1)
| ~ ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f60,f52]) ).
fof(f169,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f163,f52]) ).
fof(f174,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv3(X1)
| ~ ssPv3(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f62,f52]) ).
fof(f177,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv3(X1)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f64,f52]) ).
fof(f180,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv4(X1)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f66,f52]) ).
fof(f183,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f174,f52]) ).
fof(f184,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f177,f52]) ).
fof(f185,plain,
! [X0,X1] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f68,f52]) ).
fof(f188,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f180,f52]) ).
fof(f189,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f185,f52]) ).
fof(f194,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f70,f52]) ).
fof(f199,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ssPv2(skf1(X3))
| ssPv3(X1)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f72,f52]) ).
fof(f201,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f194,f52]) ).
fof(f202,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f201,f188]) ).
fof(f203,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f202]) ).
fof(f207,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f167,f52]) ).
fof(f215,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv1(skf1(X3))
| ssPv4(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f74,f52]) ).
fof(f217,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f76,f52]) ).
fof(f222,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv4(X1)
| ~ ssPv2(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f78,f52]) ).
fof(f230,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv2(skf1(X0))
| ssPv2(X1)
| ~ ssPv3(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f80,f52]) ).
fof(f247,plain,
! [X0,X1,X2,X3] :
( ssPv2(X2)
| ssPv1(X2)
| ssPv3(skf1(X3))
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f82,f52]) ).
fof(f249,plain,
! [X0,X1] :
( ssPv3(skf1(X0))
| ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssPv2(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f84,f52]) ).
fof(f262,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f217,f52]) ).
fof(f265,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f262,f160]) ).
fof(f266,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f262,f156]) ).
fof(f267,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f266]) ).
fof(f269,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f222,f52]) ).
fof(f277,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ssPv1(skf1(X3))
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f88,f52]) ).
fof(f279,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f90,f52]) ).
fof(f285,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f269,f201]) ).
fof(f286,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f285]) ).
fof(f293,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f230,f52]) ).
fof(f296,plain,
! [X0,X1,X2,X3] :
( ssPv2(skf1(X3))
| ssPv4(X1)
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f92,f52]) ).
fof(f302,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f249,f52]) ).
fof(f309,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f279,f52]) ).
fof(f312,plain,
! [X0,X1,X2,X3] :
( ssPv2(skf1(X3))
| ssPv3(X1)
| ~ ssPv4(X2)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f94,f52]) ).
fof(f316,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ssPv3(skf1(X3))
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f96,f52]) ).
fof(f337,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssPv2(skf1(X3))
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f98,f52]) ).
fof(f341,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv3(skf1(X3))
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f100,f52]) ).
fof(f343,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f102,f52]) ).
fof(f347,plain,
! [X0,X1,X2,X3] :
( ssPv2(X2)
| ~ ssPv3(skf1(X2))
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f102,f52]) ).
fof(f348,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f343,f52]) ).
fof(f351,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f348,f160]) ).
fof(f352,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f348,f156]) ).
fof(f354,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f352]) ).
fof(f375,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f106,f52]) ).
fof(f380,plain,
! [X0,X1] :
( ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f108,f52]) ).
fof(f385,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f375,f52]) ).
fof(f389,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f385,f188]) ).
fof(f390,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f389]) ).
fof(f396,plain,
! [X0] :
( ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f380,f52]) ).
fof(f401,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f396,f184]) ).
fof(f406,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f401]) ).
fof(f407,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f390,f406]) ).
fof(f411,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f406,f188]) ).
fof(f412,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f411,f309]) ).
fof(f428,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv1(X4)
| ssPv2(skf1(X3))
| ssPv3(X1)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f110,f52]) ).
fof(f435,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X4)
| ssPv1(skf1(X3))
| ssPv3(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f112,f52]) ).
fof(f444,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X2)
| ssPv2(X4)
| ssPv4(skf1(X3))
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f114,f52]) ).
fof(f459,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ssPv3(X4)
| ssPv4(skf1(X3))
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f116,f52]) ).
fof(f487,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv1(skf1(X3))
| ssPv2(X1)
| ~ ssPv2(X4)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f118,f52]) ).
fof(f491,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv1(X5)
| ssPv2(X4)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f120,f110]) ).
fof(f493,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X0)
| ssPv1(X4)
| ssPv2(X3)
| ~ ssRr(X0,X4)
| ~ ssRr(X0,X2)
| ~ ssRr(X2,X3)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f491,f52]) ).
fof(f518,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X2)
| ssPv4(X4)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssPv1(skf1(X3))
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f122,f52]) ).
fof(f522,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv1(X5)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f124,f491]) ).
fof(f526,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv1(X4)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f522,f52]) ).
fof(f551,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv4(X2)
| ssPv4(X4)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f128,f522]) ).
fof(f555,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv4(skf1(X3))
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f551,f52]) ).
fof(f556,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv4(X3)
| ~ ssRr(skf1(X2),X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f551,f52]) ).
fof(f627,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ssPv3(X4)
| ~ ssPv4(skf1(X2))
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f136,f52]) ).
fof(f636,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ssPv4(skf1(skf1(X2)))
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f556,f52]) ).
fof(f651,plain,
! [X0,X1,X2,X3] :
( ssPv2(X3)
| ~ ssPv2(X2)
| ~ ssPv3(skf1(X2))
| ~ ssRr(skf1(X2),X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f140,f52]) ).
fof(f675,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ~ ssPv1(X4)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssPv2(skf1(X3))
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f142,f52]) ).
fof(f696,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f351,f407]) ).
fof(f776,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv3(X1)
| ~ ssPv1(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f199,f52]) ).
fof(f791,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f776,f52]) ).
fof(f799,plain,
! [X0] :
( ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f791,f396]) ).
fof(f804,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f799]) ).
fof(f829,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f804,f189]) ).
fof(f832,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f829]) ).
fof(f849,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f215,f52]) ).
fof(f852,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f849,f52]) ).
fof(f855,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f852,f385]) ).
fof(f862,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f855,f348]) ).
fof(f867,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f696,f870]) ).
fof(f869,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f354,f870]) ).
fof(f870,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f862,f407]) ).
fof(f1075,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f247,f52]) ).
fof(f1078,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1075,f52]) ).
fof(f1086,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1078,f269]) ).
fof(f1088,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1078,f188]) ).
fof(f1089,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1086,f302]) ).
fof(f1091,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f1088]) ).
fof(f1098,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f1091,f412]) ).
fof(f1104,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1098]) ).
fof(f1119,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f1104,f267]) ).
fof(f1126,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(X0))
| ~ ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1119]) ).
fof(f1333,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f277,f52]) ).
fof(f1336,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1333,f52]) ).
fof(f1346,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1336,f791]) ).
fof(f1357,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1346]) ).
fof(f1366,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1357,f189]) ).
fof(f1371,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1366]) ).
fof(f1372,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1371,f160]) ).
fof(f1491,plain,
! [X0,X1] :
( ssPv2(skf1(skf1(X0)))
| ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f296,f52]) ).
fof(f1504,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1491,f52]) ).
fof(f1512,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1504,f201]) ).
fof(f1520,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1512]) ).
fof(f1549,plain,
! [X0,X1] :
( ssPv2(skf1(skf1(X0)))
| ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f312,f52]) ).
fof(f1552,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1549,f52]) ).
fof(f1636,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f316,f52]) ).
fof(f1639,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1636,f52]) ).
fof(f1642,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1639,f1520]) ).
fof(f1662,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1642]) ).
fof(f1675,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1662,f309]) ).
fof(f1681,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1675]) ).
fof(f1751,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f337,f52]) ).
fof(f1755,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1751,f52]) ).
fof(f1764,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1755,f1089]) ).
fof(f1779,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f1764]) ).
fof(f1780,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1779,f267]) ).
fof(f1843,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f341,f52]) ).
fof(f1846,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1843,f52]) ).
fof(f1855,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1846,f1357]) ).
fof(f1860,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1846,f804]) ).
fof(f1873,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1855]) ).
fof(f1874,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1873,f1336]) ).
fof(f1879,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1860]) ).
fof(f1880,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv4(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1879,f396]) ).
fof(f1894,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f832,f1880]) ).
fof(f1996,plain,
! [X0,X1,X2] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(X2)
| ~ ssRr(X0,X2)
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f347,f52]) ).
fof(f2549,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1996,f52]) ).
fof(f2575,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f428,f52]) ).
fof(f2692,plain,
! [X0,X1] :
( ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv3(X1)
| ~ ssPv3(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f435,f52]) ).
fof(f2892,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2575,f52]) ).
fof(f2911,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2892,f309]) ).
fof(f2922,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2911]) ).
fof(f2948,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f444,f52]) ).
fof(f2967,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2922,f286]) ).
fof(f2974,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2967]) ).
fof(f2975,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2974,f309]) ).
fof(f3043,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2975,f267]) ).
fof(f3056,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3043]) ).
fof(f3057,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3056,f1126]) ).
fof(f3058,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f2692,f52]) ).
fof(f3157,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2948,f52]) ).
fof(f3185,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f3157,f184]) ).
fof(f3186,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f3157,f183]) ).
fof(f3200,plain,
! [X0] :
( ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f3185]) ).
fof(f3201,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3186,f269]) ).
fof(f3217,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f3201,f1880]) ).
fof(f3234,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3217]) ).
fof(f3235,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3234,f183]) ).
fof(f3283,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f459,f52]) ).
fof(f3306,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f3200,f407]) ).
fof(f3319,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3306]) ).
fof(f3320,plain,
! [X0] :
( ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3319,f184]) ).
fof(f3327,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f3320,f1504]) ).
fof(f3340,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f3327]) ).
fof(f3357,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f3340,f1639]) ).
fof(f3366,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3357]) ).
fof(f3367,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3366,f1662]) ).
fof(f3386,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3367,f412]) ).
fof(f3398,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3386]) ).
fof(f3399,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3398,f1104]) ).
fof(f3423,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3057,f869]) ).
fof(f3446,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3423]) ).
fof(f3447,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3446,f267]) ).
fof(f3554,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f3283,f52]) ).
fof(f3575,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3399,f203]) ).
fof(f3685,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv2(X1)
| ~ ssPv2(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f487,f52]) ).
fof(f3692,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f3685,f52]) ).
fof(f3702,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f3692,f1780]) ).
fof(f3711,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3702,f267]) ).
fof(f3713,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3711,f1874]) ).
fof(f3714,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f3713,f3554]) ).
fof(f3727,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3714]) ).
fof(f3728,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3727,f3201]) ).
fof(f3747,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f3728,f1078]) ).
fof(f3768,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3747]) ).
fof(f3821,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv1(X3)
| ssPv2(X1)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f493,f52]) ).
fof(f3827,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f3821,f52]) ).
fof(f3828,plain,
! [X0,X1,X2] :
( ssPv4(X0)
| ssPv1(X2)
| ssPv2(X1)
| ~ ssRr(X0,X2)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f3821,f52]) ).
fof(f3830,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f3827,f52]) ).
fof(f3839,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3830,f1846]) ).
fof(f3840,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3830,f1780]) ).
fof(f3841,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3830,f1639]) ).
fof(f3847,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3839]) ).
fof(f3896,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(X1)
| ssPv2(skf1(skf1(X0)))
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f3828,f52]) ).
fof(f3905,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f3896,f1846]) ).
fof(f3907,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f3896,f1639]) ).
fof(f3913,plain,
! [X0,X1] :
( ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f3905]) ).
fof(f3958,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3841,f3847]) ).
fof(f3967,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3958,f1755]) ).
fof(f3991,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3967,f3830]) ).
fof(f4019,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f3991,f265]) ).
fof(f4023,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f4019]) ).
fof(f4024,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4023,f267]) ).
fof(f4113,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(skf1(X0)))
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f518,f52]) ).
fof(f4119,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3840,f3991]) ).
fof(f4195,plain,
! [X0,X1] :
( ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f3907,f3913]) ).
fof(f4259,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f526,f52]) ).
fof(f4262,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f526,f52]) ).
fof(f4265,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4259,f52]) ).
fof(f4266,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f3958,f4265]) ).
fof(f4267,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f3847,f4265]) ).
fof(f4298,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f4265,f183]) ).
fof(f4316,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4298]) ).
fof(f4334,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f4119,f4267]) ).
fof(f4335,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2975,f4267]) ).
fof(f4338,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f4267,f2549]) ).
fof(f4349,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4338,f867]) ).
fof(f4353,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3235,f4316]) ).
fof(f4427,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4334,f4316]) ).
fof(f4428,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4427,f4265]) ).
fof(f4455,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4428,f4267]) ).
fof(f4474,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f4455,f262]) ).
fof(f4497,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4335,f4427]) ).
fof(f4514,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f4497,f869]) ).
fof(f4516,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f4497,f870]) ).
fof(f4525,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4514,f4427]) ).
fof(f4526,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4516,f4427]) ).
fof(f4529,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4526,f4266]) ).
fof(f4541,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4525,f4266]) ).
fof(f4646,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f4353,f1078]) ).
fof(f4667,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4646]) ).
fof(f4668,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4667,f869]) ).
fof(f4727,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f555,f52]) ).
fof(f4732,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4727,f52]) ).
fof(f4736,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4732,f3367]) ).
fof(f4746,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4732,f1662]) ).
fof(f4757,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4732,f791]) ).
fof(f4763,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4732,f183]) ).
fof(f4771,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4736,f4529]) ).
fof(f4777,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4746,f201]) ).
fof(f4779,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4763]) ).
fof(f4808,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f4777,f169]) ).
fof(f4825,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4808]) ).
fof(f4826,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4825,f870]) ).
fof(f4839,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f4779,f3320]) ).
fof(f4846,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f4779,f407]) ).
fof(f4850,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4839,f293]) ).
fof(f4858,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4846,f183]) ).
fof(f4879,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f4771,f406]) ).
fof(f4889,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4879,f3367]) ).
fof(f4951,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f4349,f267]) ).
fof(f4961,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4951]) ).
fof(f4962,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f4961,f3447]) ).
fof(f5115,plain,
! [X0,X1,X2] :
( ssPv4(X0)
| ssPv1(X2)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f4262,f52]) ).
fof(f5117,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f5115,f52]) ).
fof(f5118,plain,
! [X0,X1] :
( ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f4195,f5117]) ).
fof(f5119,plain,
! [X0,X1] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f3913,f5117]) ).
fof(f5363,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1681,f4826]) ).
fof(f5428,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f4858,f4474]) ).
fof(f5441,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5428]) ).
fof(f5442,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5441,f4024]) ).
fof(f5445,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f286,f5442]) ).
fof(f5507,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f5445,f309]) ).
fof(f5510,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f5445,f4349]) ).
fof(f5526,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5507]) ).
fof(f5528,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5510,f4529]) ).
fof(f5531,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f5526,f3058]) ).
fof(f5563,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f5531]) ).
fof(f5580,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f5528,f52]) ).
fof(f5691,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f4962,f52]) ).
fof(f5692,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv2(X0)
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5691,f3320]) ).
fof(f5702,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f5692,f1504]) ).
fof(f5717,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5702]) ).
fof(f5956,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f4777,f5957]) ).
fof(f5957,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4889,f4541]) ).
fof(f5974,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5580,f5956]) ).
fof(f6126,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f5563,f201]) ).
fof(f6143,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f6126]) ).
fof(f6257,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f4668,f4732]) ).
fof(f6291,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6257,f3728]) ).
fof(f6322,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f6291,f1078]) ).
fof(f6339,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f6291,f406]) ).
fof(f6347,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f6322]) ).
fof(f6364,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f6339]) ).
fof(f6365,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6364,f4541]) ).
fof(f6640,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1104,f6641]) ).
fof(f6641,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6365,f6347]) ).
fof(f6742,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f6640,f1552]) ).
fof(f6767,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f6742]) ).
fof(f6768,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6767,f4541]) ).
fof(f7186,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4850,f4541]) ).
fof(f7659,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f5717,f1639]) ).
fof(f7669,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f7659]) ).
fof(f7670,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7669,f1662]) ).
fof(f7729,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f6143,f3554]) ).
fof(f7740,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f7729]) ).
fof(f7741,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7740,f201]) ).
fof(f7748,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7741,f5363]) ).
fof(f7757,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f7748,f3830]) ).
fof(f7790,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f7757]) ).
fof(f7791,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f7790,f4427]) ).
fof(f7825,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f7791,f348]) ).
fof(f7832,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7825,f867]) ).
fof(f7879,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f3157,f7882]) ).
fof(f7882,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7832,f407]) ).
fof(f7884,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f7882,f4757]) ).
fof(f7887,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f7882,f5563]) ).
fof(f7906,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f7882,f4497]) ).
fof(f7908,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7884,f791]) ).
fof(f7910,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7887,f3058]) ).
fof(f7911,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7906,f4427]) ).
fof(f7918,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7911,f4266]) ).
fof(f7919,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f7918,f3554]) ).
fof(f7926,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f7918,f262]) ).
fof(f7961,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f7879,f5445]) ).
fof(f7979,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7961,f5956]) ).
fof(f8180,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7979,f7882]) ).
fof(f8181,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f8180,f7670]) ).
fof(f8214,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8181,f262]) ).
fof(f8303,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f8214,f3575]) ).
fof(f8319,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8303]) ).
fof(f8320,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8319,f5956]) ).
fof(f8387,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f7910,f262]) ).
fof(f8395,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8387]) ).
fof(f8396,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8395,f7748]) ).
fof(f8421,plain,
! [X0] :
( ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f8396,f396]) ).
fof(f8422,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f8396,f309]) ).
fof(f8445,plain,
! [X0] :
( ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f8421]) ).
fof(f8446,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8445,f7918]) ).
fof(f8447,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f8422]) ).
fof(f8536,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f7919,f201]) ).
fof(f8551,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8536]) ).
fof(f8552,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8551,f7926]) ).
fof(f8645,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f8446,f8320]) ).
fof(f8647,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8645]) ).
fof(f8648,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8647,f6768]) ).
fof(f8649,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8447,f8446]) ).
fof(f8692,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7908,f7186]) ).
fof(f8702,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f8692,f1846]) ).
fof(f8712,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8702]) ).
fof(f8724,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f8712,f7879]) ).
fof(f8729,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f8712,f4732]) ).
fof(f8756,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8724]) ).
fof(f8757,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8756,f6641]) ).
fof(f8762,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8729]) ).
fof(f8852,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f8762,f7882]) ).
fof(f8858,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8852]) ).
fof(f8859,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8858,f8712]) ).
fof(f8866,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5442,f8859]) ).
fof(f8876,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f8859,f1846]) ).
fof(f8884,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8876,f7918]) ).
fof(f8913,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f293,f8866]) ).
fof(f8916,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f269,f8866]) ).
fof(f9032,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f8913,f1639]) ).
fof(f9043,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9032,f8757]) ).
fof(f9060,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f8916,f1880]) ).
fof(f9066,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9060]) ).
fof(f9067,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9066,f7918]) ).
fof(f9166,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f8884,f4732]) ).
fof(f9193,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9166]) ).
fof(f9254,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9043,f8859]) ).
fof(f9261,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f9254,f4732]) ).
fof(f9268,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f9254,f1755]) ).
fof(f9291,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9261]) ).
fof(f9294,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9268,f8913]) ).
fof(f9299,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9294,f8859]) ).
fof(f9310,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9299,f1780]) ).
fof(f9319,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9310]) ).
fof(f9320,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9319,f8552]) ).
fof(f9331,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f9291,f7882]) ).
fof(f9339,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9331]) ).
fof(f9340,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9339,f9254]) ).
fof(f9347,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f804,f9340]) ).
fof(f9360,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9340,f1639]) ).
fof(f9774,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f9067,f9360]) ).
fof(f9775,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f9067,f8884]) ).
fof(f9809,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9774]) ).
fof(f9810,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9809,f9320]) ).
fof(f9811,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9775]) ).
fof(f9845,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9811,f9810]) ).
fof(f9852,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f9845,f1078]) ).
fof(f9864,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f9852]) ).
fof(f9865,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f9864,f9360]) ).
fof(f9875,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9865,f4732]) ).
fof(f9881,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9865,f1755]) ).
fof(f9900,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9875,f9193]) ).
fof(f9903,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9881]) ).
fof(f9904,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9903,f9340]) ).
fof(f9921,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f9904,f7882]) ).
fof(f10052,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1780,f9921]) ).
fof(f10146,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9900,f201]) ).
fof(f10156,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10146,f5974]) ).
fof(f10163,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f203,f10164]) ).
fof(f10164,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10156,f9340]) ).
fof(f10259,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f10052,f207]) ).
fof(f10269,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10259]) ).
fof(f10270,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ssPv2(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10269,f10164]) ).
fof(f10374,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f10270,f52]) ).
fof(f10379,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3768,f10374]) ).
fof(f10382,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1091,f10374]) ).
fof(f10430,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f10379,f5117]) ).
fof(f10460,plain,
! [X0,X1] :
( ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10430]) ).
fof(f10461,plain,
! [X0,X1] :
( ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv1(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10460,f5118]) ).
fof(f10493,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssPv2(skf1(X3))
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f675,f10496]) ).
fof(f10496,plain,
! [X0,X1] :
( ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10461,f5119]) ).
fof(f10522,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f10493,f52]) ).
fof(f10629,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1089,f10382]) ).
fof(f10739,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1662,f10629]) ).
fof(f10806,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f10739,f10164]) ).
fof(f10813,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10806,f201]) ).
fof(f10815,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f10813,f3554]) ).
fof(f10827,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10815]) ).
fof(f10828,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10827,f201]) ).
fof(f10837,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f8320,f10840]) ).
fof(f10839,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f8648,f10840]) ).
fof(f10840,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10828,f10163]) ).
fof(f10887,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1894,f10839]) ).
fof(f10940,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f10837,f8649]) ).
fof(f10959,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f10940]) ).
fof(f11090,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f10887,f8916]) ).
fof(f11109,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f11090]) ).
fof(f11110,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(skf1(skf1(X0)))
| ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f11109,f7918]) ).
fof(f11121,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f11110,f10379]) ).
fof(f11138,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f11110,f791]) ).
fof(f11143,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f11110,f184]) ).
fof(f11147,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f11121]) ).
fof(f11148,plain,
! [X0] :
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11147,f10374]) ).
fof(f11152,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11138,f9347]) ).
fof(f11155,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11143,f7882]) ).
fof(f11286,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11155,f11148]) ).
fof(f11308,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f11286,f9845]) ).
fof(f11316,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11308]) ).
fof(f11325,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv2(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f11316,f7879]) ).
fof(f11351,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f11325]) ).
fof(f11416,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f3320,f11351]) ).
fof(f11445,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f11416,f189]) ).
fof(f11450,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f11445]) ).
fof(f11451,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f11450,f9340]) ).
fof(f11668,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f11152,f1846]) ).
fof(f11676,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11668]) ).
fof(f11720,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f11676,f4732]) ).
fof(f11745,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11720]) ).
fof(f11754,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f4113,f7918]) ).
fof(f11755,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f11754,f52]) ).
fof(f11756,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f11755,f9340]) ).
fof(f11770,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f184,f11756]) ).
fof(f11774,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f7882,f11756]) ).
fof(f11779,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f11756,f1078]) ).
fof(f11784,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f11779,f10629]) ).
fof(f11797,plain,
! [X0,X1,X2,X3] :
( ssPv2(X3)
| ~ ssPv3(skf1(X2))
| ~ ssRr(skf1(X2),X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f651,f11774]) ).
fof(f11896,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1639,f11898]) ).
fof(f11898,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f11784,f11770]) ).
fof(f11916,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f11898,f11774]) ).
fof(f11938,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f11916,f10840]) ).
fof(f11954,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f10959,f11938]) ).
fof(f11958,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f10837,f11938]) ).
fof(f11961,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f10052,f11938]) ).
fof(f11983,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f11938,f8396]) ).
fof(f11994,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f11983]) ).
fof(f11995,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f11994,f10840]) ).
fof(f12000,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f11954,f11898]) ).
fof(f12032,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f12000,f11451]) ).
fof(f12036,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f12032,f11774]) ).
fof(f12110,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f9904,f12121]) ).
fof(f12120,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssPv2(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f98,f12121]) ).
fof(f12121,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11995,f11958]) ).
fof(f12146,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ssPv3(X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f627,f12110]) ).
fof(f12164,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f96,f12120]) ).
fof(f12210,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f12164,f52]) ).
fof(f12221,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f11451,f12230]) ).
fof(f12230,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11961,f12036]) ).
fof(f12244,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f9347,f12221]) ).
fof(f12301,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f12244,f189]) ).
fof(f12306,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f12301]) ).
fof(f12353,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f12306,f1372]) ).
fof(f12362,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f12353]) ).
fof(f12363,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f12362,f10887]) ).
fof(f12369,plain,
! [X0,X1,X2] :
( ssPv2(skf1(skf1(X2)))
| ~ ssPv3(skf1(X2))
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f11797,f52]) ).
fof(f12370,plain,
! [X0,X1,X2] :
( ssPv2(skf1(skf1(X2)))
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f12369,f12221]) ).
fof(f12629,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ssPv1(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f11896,f12230]) ).
fof(f12631,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f12629,f12121]) ).
fof(f12735,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f12210,f12230]) ).
fof(f12736,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f12735,f52]) ).
fof(f12741,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f12736,f52]) ).
fof(f12985,plain,
! [X0,X1,X2] :
( ssPv1(X2)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f12370,f12741]) ).
fof(f12989,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f12146,f12985]) ).
fof(f12998,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f12985,f52]) ).
fof(f13018,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f12998,f52]) ).
fof(f13022,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f396,f13018]) ).
fof(f13108,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0)))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f10522,f52]) ).
fof(f13112,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f13108,f11745]) ).
fof(f13114,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f13108,f9900]) ).
fof(f13118,plain,
! [X0,X1,X2] :
( ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f13108,f636]) ).
fof(f13124,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f13112]) ).
fof(f13125,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13124,f12244]) ).
fof(f13126,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f13114]) ).
fof(f13127,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13126,f9340]) ).
fof(f13130,plain,
! [X0,X1,X2] :
( ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f13118]) ).
fof(f13131,plain,
! [X0,X1,X2] :
( ~ ssRr(X0,X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13130,f12370]) ).
fof(f13138,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f13127,f12363]) ).
fof(f13140,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f13138,f12306]) ).
fof(f13149,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f13125,f12631]) ).
fof(f13154,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f13149,f13018]) ).
fof(f13225,plain,
! [X0,X1] :
( ~ ssRr(X0,X1)
| ~ ssPv3(skf1(X1))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f13131,f52]) ).
fof(f13227,plain,
! [X0] :
( ~ ssPv3(skf1(skf1(X0)))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f13225,f52]) ).
fof(f13400,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f12989,f52]) ).
fof(f13419,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f13400,f52]) ).
fof(f13425,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f13419,f52]) ).
fof(f13426,plain,
! [X0] : ssPv1(X0),
inference(forward_subsumption_resolution,[status(thm)],[f13425,f13154]) ).
fof(f13451,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f13140,f13426]) ).
fof(f13479,plain,
! [X0] : ssPv3(X0),
inference(forward_subsumption_resolution,[status(thm)],[f13451,f13426]) ).
fof(f13483,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f13022,f13479]) ).
fof(f13519,plain,
! [X0] : ssPv4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f13227,f13479]) ).
fof(f13524,plain,
! [X0] : ~ ssPv4(skf1(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f13483,f13479]) ).
fof(f13537,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f13524,f13519]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN759-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n004.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 11:15:19 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 220.38/28.54 % Refutation found
% 220.38/28.54 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 220.38/28.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.14/28.56 % Elapsed time: 28.116155 seconds
% 7.14/28.56 % CPU time: 222.103258 seconds
% 7.14/28.56 % Total memory used: 109.163 MB
% 7.14/28.56 % Net memory used: 74.420 MB
%------------------------------------------------------------------------------