%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN762-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:17 PM UTC 2026
% Result : Unsatisfiable 64.93s 8.62s
% Output : CNFRefutation 64.93s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [U] : ssRr(U,skf1(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
! [U,V,W] :
( ssPv4(W)
| ssPv3(W)
| ssPv2(W)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
! [U,V,W] :
( ssPv3(W)
| ssPv2(W)
| ssPv1(W)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
! [U,V,W] :
( ssPv4(W)
| ssPv2(W)
| ~ ssPv3(W)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
! [U,V,W] :
( ssPv2(W)
| ssPv1(W)
| ~ ssPv3(W)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
! [U,V,W] :
( ssPv2(W)
| ssPv1(W)
| ~ ssPv3(W)
| ~ ssRr(W,U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv4(W)
| ~ ssPv2(W)
| ~ ssRr(W,U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv3(W)
| ssPv2(X)
| ssPv1(V)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv1(X)
| ssPv2(V)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv2(W)
| ssPv2(V)
| ~ ssPv2(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
! [U,V,W,X] :
( ssPv2(W)
| ssPv1(W)
| ssPv1(V)
| ~ ssPv3(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv1(X)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
! [U,V,W,X] :
( ssPv1(W)
| ssPv4(X)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
! [U,V,W,X] :
( ssPv1(W)
| ssPv3(V)
| ~ ssPv2(W)
| ~ ssPv3(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] :
( ssPv4(W)
| ssPv1(W)
| ~ ssPv1(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
! [U,V,W,X] :
( ssPv4(W)
| ssPv3(V)
| ~ ssPv1(W)
| ~ ssPv1(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
! [U,V,W,X] :
( ssPv4(V)
| ~ ssPv4(W)
| ~ ssPv3(W)
| ~ ssPv4(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
! [U,V,W,X] :
( ssPv1(W)
| ~ ssPv3(W)
| ~ ssPv1(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
! [U,V,W,X] :
( ssPv3(V)
| ~ ssPv4(W)
| ~ ssPv2(W)
| ~ ssPv2(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
! [U,V,W,X] :
( ssPv4(V)
| ~ ssPv3(W)
| ~ ssPv1(W)
| ~ ssPv3(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [U,V,W,X] :
( ssPv3(X)
| ~ ssPv2(W)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [U,V,W,X] :
( ssPv2(W)
| ~ ssPv3(W)
| ~ ssPv1(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [U,V,W,X] :
( ~ ssPv2(W)
| ~ ssPv1(W)
| ~ ssPv4(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(W)
| ssPv1(W)
| ssPv3(Y)
| ssPv4(V)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv4(W)
| ssPv3(W)
| ssPv2(Y)
| ssPv4(V)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(W)
| ssPv1(Y)
| ssPv2(V)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,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(f28,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv4(W)
| ssPv3(W)
| ssPv1(Y)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(Y)
| ssPv3(V)
| ~ ssPv3(W)
| ~ ssRr(W,Y)
| ~ ssPv4(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv3(W)
| ssPv3(Y)
| ~ ssPv4(W)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv1(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(f33,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv2(W)
| ssPv4(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(f34,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv4(Y)
| ssPv1(V)
| ~ ssPv4(W)
| ~ ssRr(W,Y)
| ~ ssPv1(X)
| ~ ssRr(W,X)
| ~ ssRr(W,U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
! [U,V,W,X,Y] :
( ssPv1(W)
| ~ ssPv4(W)
| ~ ssRr(W,X)
| ~ ssPv3(Y)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
! [U,V,W,X,Y] :
( ~ ssPv3(W)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ~ ssPv1(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] :
( ssPv1(Z)
| ssPv3(Y)
| ssPv4(V)
| ~ ssPv4(W)
| ~ ssRr(W,Z)
| ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ~ ssRr(W,U)
| ~ 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] :
( ssPv4(W)
| ssPv3(W)
| ssPv2(W)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ssPv3(X2)
| ssPv2(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
! [W] :
( ssPv3(W)
| ssPv2(W)
| ssPv1(W)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ssPv3(X2)
| ssPv2(X2)
| ssPv1(X2)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [W] :
( ssPv4(W)
| ssPv2(W)
| ~ ssPv3(W)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f58,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ssPv2(X2)
| ~ ssPv3(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [W] :
( ssPv2(W)
| ssPv1(W)
| ~ ssPv3(W)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ssPv2(X2)
| ssPv1(X2)
| ~ ssPv3(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [W] :
( ssPv2(W)
| ssPv1(W)
| ~ ssPv3(W)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f62,plain,
! [X0,X1,X2] :
( ssPv2(X2)
| ssPv1(X2)
| ~ ssPv3(X2)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [W] :
( ssPv1(W)
| ~ ssPv4(W)
| ~ ssPv2(W)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ssPv1(X2)
| ~ ssPv4(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [W] :
( ssPv4(W)
| ssPv3(W)
| ! [X] :
( ssPv2(X)
| ! [V] :
( ssPv1(V)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv3(X2)
| ssPv2(X3)
| ssPv1(X1)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [W] :
( ssPv4(W)
| ! [X] :
( ssPv1(X)
| ! [V] :
( ssPv2(V)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv1(X3)
| ssPv2(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [W] :
( ssPv4(W)
| ssPv2(W)
| ! [V] :
( ssPv2(V)
| ! [X] :
( ~ ssPv2(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f70,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv2(X2)
| ssPv2(X1)
| ~ ssPv2(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [W] :
( ssPv2(W)
| ssPv1(W)
| ! [V] :
( ssPv1(V)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ssPv2(X2)
| ssPv1(X2)
| ssPv1(X1)
| ~ ssPv3(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [W] :
( ssPv4(W)
| ! [X] :
( ssPv1(X)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f74,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv1(X3)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
! [W] :
( ssPv1(W)
| ! [X] :
( ssPv4(X)
| ~ ssPv3(W)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f76,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ssPv4(X3)
| ~ ssPv3(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [W] :
( ssPv1(W)
| ! [V] :
( ssPv3(V)
| ~ ssPv2(W)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f78,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ssPv3(X1)
| ~ ssPv2(X2)
| ~ ssPv3(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [W] :
( ssPv4(W)
| ssPv1(W)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f80,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv1(X2)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [W] :
( ssPv4(W)
| ! [V] :
( ssPv3(V)
| ~ ssPv1(W)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv3(X1)
| ~ ssPv1(X2)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [V] :
( ssPv4(V)
| ! [W] :
( ~ ssPv4(W)
| ~ ssPv3(W)
| ! [X] :
( ~ ssPv4(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f84,plain,
! [X0,X1,X2,X3] :
( ssPv4(X1)
| ~ ssPv4(X2)
| ~ ssPv3(X2)
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [W] :
( ssPv1(W)
| ~ ssPv3(W)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f86,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ~ ssPv3(X2)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
! [V] :
( ssPv3(V)
| ! [W] :
( ~ ssPv4(W)
| ~ ssPv2(W)
| ! [X] :
( ~ ssPv2(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( ssPv3(X1)
| ~ ssPv4(X2)
| ~ ssPv2(X2)
| ~ ssPv2(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
! [V] :
( ssPv4(V)
| ! [W] :
( ~ ssPv3(W)
| ~ ssPv1(W)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( ssPv4(X1)
| ~ ssPv3(X2)
| ~ ssPv1(X2)
| ~ ssPv3(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [X] :
( ssPv3(X)
| ! [W] :
( ~ ssPv2(W)
| ~ ssPv1(W)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( ssPv3(X3)
| ~ ssPv2(X2)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [W] :
( ssPv2(W)
| ~ ssPv3(W)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f94,plain,
! [X0,X1,X2,X3] :
( ssPv2(X2)
| ~ ssPv3(X2)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
! [W] :
( ~ ssPv2(W)
| ~ ssPv1(W)
| ! [X] :
( ~ ssPv4(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f96,plain,
! [X0,X1,X2,X3] :
( ~ ssPv2(X2)
| ~ ssPv1(X2)
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [W] :
( ssPv3(W)
| ssPv1(W)
| ! [Y] :
( ssPv3(Y)
| ! [V] :
( ssPv4(V)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f98,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X2)
| ssPv1(X2)
| ssPv3(X4)
| ssPv4(X1)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
! [W] :
( ssPv4(W)
| ssPv3(W)
| ! [Y] :
( ssPv2(Y)
| ! [V] :
( ssPv4(V)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f100,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv3(X2)
| ssPv2(X4)
| ssPv4(X1)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
! [W] :
( ssPv3(W)
| ! [Y] :
( ssPv1(Y)
| ! [V] :
( ssPv2(V)
| ~ ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f102,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X2)
| ssPv1(X4)
| ssPv2(X1)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,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)],[f27]) ).
fof(f104,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)],[f103]) ).
fof(f105,plain,
! [W] :
( ssPv4(W)
| ssPv3(W)
| ! [Y] :
( ssPv1(Y)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f106,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X2)
| ssPv3(X2)
| ssPv1(X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f109,plain,
! [Y] :
( ssPv3(Y)
| ! [V] :
( ssPv3(V)
| ! [W] :
( ~ ssPv3(W)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv4(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X4)
| ssPv3(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X4)
| ~ ssPv4(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [W] :
( ssPv3(W)
| ! [Y] :
( ssPv3(Y)
| ~ ssPv4(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f112,plain,
! [X0,X1,X2,X3,X4] :
( ssPv3(X2)
| ssPv3(X4)
| ~ ssPv4(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [Y] :
( ssPv1(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)],[f32]) ).
fof(f114,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X4)
| ssPv4(X1)
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [W] :
( ssPv2(W)
| ! [Y] :
( ssPv4(Y)
| ~ ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f33]) ).
fof(f116,plain,
! [X0,X1,X2,X3,X4] :
( ssPv2(X2)
| ssPv4(X4)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [Y] :
( ssPv4(Y)
| ! [V] :
( ssPv1(V)
| ! [W] :
( ~ ssPv4(W)
| ~ ssRr(W,Y)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(W,X)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f118,plain,
! [X0,X1,X2,X3,X4] :
( ssPv4(X4)
| ssPv1(X1)
| ~ ssPv4(X2)
| ~ ssRr(X2,X4)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f121,plain,
! [W] :
( ssPv1(W)
| ~ ssPv4(W)
| ! [X] :
( ~ ssRr(W,X)
| ! [Y] :
( ~ ssPv3(Y)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f122,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X2)
| ~ ssPv4(X2)
| ~ ssRr(X2,X3)
| ~ ssPv3(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f125,plain,
! [W] :
( ~ ssPv3(W)
| ~ ssPv1(W)
| ! [X] :
( ~ ssRr(W,X)
| ! [Y] :
( ~ ssPv1(Y)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f126,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssPv3(X2)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssPv1(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [Z] :
( ssPv1(Z)
| ! [Y] :
( ssPv3(Y)
| ! [V] :
( ssPv4(V)
| ! [W] :
( ~ ssPv4(W)
| ~ ssRr(W,Z)
| ! [X] :
( ~ ssRr(W,X)
| ~ ssRr(X,Y)
| ! [U] :
( ~ ssRr(W,U)
| ~ ssRr(U,V) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f39]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4,X5] :
( ssPv1(X5)
| ssPv3(X4)
| ssPv4(X1)
| ~ ssPv4(X2)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f155,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f56,f52]) ).
fof(f156,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f155,f52]) ).
fof(f157,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ssPv2(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f58,f54]) ).
fof(f158,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f157,f52]) ).
fof(f159,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f158,f52]) ).
fof(f160,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f60,f52]) ).
fof(f161,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f62,f52]) ).
fof(f162,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f160,f52]) ).
fof(f163,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f161,f52]) ).
fof(f164,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f64,f52]) ).
fof(f165,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f164,f52]) ).
fof(f166,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f66,f52]) ).
fof(f169,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f166,f52]) ).
fof(f170,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(X1)
| ~ ssPv3(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f68,f52]) ).
fof(f173,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv2(X1)
| ~ ssPv2(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f70,f52]) ).
fof(f176,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv1(X1)
| ~ ssPv3(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f72,f52]) ).
fof(f179,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f169,f156]) ).
fof(f180,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f179]) ).
fof(f182,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f170,f52]) ).
fof(f183,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f74,f52]) ).
fof(f187,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f173,f52]) ).
fof(f189,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f176,f52]) ).
fof(f190,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f189,f156]) ).
fof(f191,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f190]) ).
fof(f192,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f76,f52]) ).
fof(f195,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv3(X1)
| ~ ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f78,f52]) ).
fof(f196,plain,
! [X0,X1,X2] :
( ssPv1(X0)
| ssPv3(X1)
| ~ ssPv2(X0)
| ~ ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f78,f52]) ).
fof(f198,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f183,f52]) ).
fof(f200,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f198,f182]) ).
fof(f203,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f200]) ).
fof(f209,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f192,f52]) ).
fof(f210,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f195,f52]) ).
fof(f214,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f80,f52]) ).
fof(f217,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(X1)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f82,f52]) ).
fof(f220,plain,
! [X0,X1] :
( ssPv4(X1)
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f84,f52]) ).
fof(f226,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f214,f52]) ).
fof(f227,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f86,f52]) ).
fof(f232,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f226,f169]) ).
fof(f233,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f226,f203]) ).
fof(f236,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f232]) ).
fof(f237,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f233]) ).
fof(f249,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f217,f52]) ).
fof(f252,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f220,f52]) ).
fof(f253,plain,
! [X0,X1] :
( ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f88,f52]) ).
fof(f256,plain,
! [X0,X1] :
( ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f90,f52]) ).
fof(f265,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f227,f52]) ).
fof(f267,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f265,f189]) ).
fof(f270,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f267]) ).
fof(f271,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f270,f191]) ).
fof(f275,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f271,f169]) ).
fof(f278,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f275]) ).
fof(f279,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f253,f52]) ).
fof(f282,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f256,f52]) ).
fof(f285,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f282,f159]) ).
fof(f288,plain,
! [X0,X1] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f92,f52]) ).
fof(f291,plain,
! [X0,X1] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f94,f52]) ).
fof(f294,plain,
! [X0,X1] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f96,f52]) ).
fof(f303,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f288,f52]) ).
fof(f306,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f303,f169]) ).
fof(f309,plain,
! [X0,X1,X2,X3] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(X3)
| ssPv4(X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X2,X3)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f98,f52]) ).
fof(f310,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ssPv1(X2)
| ssPv3(skf1(X3))
| ssPv4(X1)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f98,f52]) ).
fof(f312,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f291,f52]) ).
fof(f319,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f294,f52]) ).
fof(f322,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f319,f169]) ).
fof(f332,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv3(X2)
| ssPv2(skf1(X3))
| ssPv4(X1)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f100,f52]) ).
fof(f336,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ssPv1(skf1(X3))
| ssPv2(X1)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f102,f52]) ).
fof(f367,plain,
! [X0,X1,X2,X3] :
( ssPv4(X0)
| ssPv1(X3)
| ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X2)
| ~ ssRr(X2,X3)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f104,f52]) ).
fof(f368,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)],[f104,f52]) ).
fof(f372,plain,
! [X0,X1,X2,X3] :
( ssPv4(X2)
| ssPv3(X2)
| ssPv1(skf1(X3))
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f106,f52]) ).
fof(f397,plain,
! [X0,X1] :
( ssPv3(skf1(X0))
| ssPv3(X1)
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f110,f52]) ).
fof(f409,plain,
! [X0,X1,X2,X3] :
( ssPv3(X2)
| ssPv3(skf1(X3))
| ~ ssPv4(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f112,f52]) ).
fof(f412,plain,
! [X0,X1,X2,X3] :
( ssPv1(X3)
| ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssRr(X0,X2)
| ~ ssRr(X2,X3)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f114,f52]) ).
fof(f413,plain,
! [X0,X1,X2,X3] :
( ssPv1(skf1(X3))
| ssPv4(X1)
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f114,f52]) ).
fof(f432,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f196,f52]) ).
fof(f439,plain,
! [X0,X1,X2,X3] :
( ssPv2(X2)
| ssPv4(skf1(X3))
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f116,f52]) ).
fof(f441,plain,
! [X0,X1] :
( ssPv4(skf1(X0))
| ssPv1(X1)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f118,f52]) ).
fof(f464,plain,
! [X0,X1,X2,X3] :
( ssPv1(X2)
| ~ ssPv4(X2)
| ~ ssRr(X2,X3)
| ~ ssPv3(skf1(X3))
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f122,f52]) ).
fof(f483,plain,
! [X0,X1,X2,X3] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv1(X3)
| ~ ssRr(X2,X3)
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f126,f52]) ).
fof(f484,plain,
! [X0,X1,X2,X3] :
( ~ ssPv3(X2)
| ~ ssPv1(X2)
| ~ ssRr(X2,X3)
| ~ ssPv1(skf1(X3))
| ~ ssRr(X2,X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f126,f52]) ).
fof(f513,plain,
! [X0,X1,X2,X3,X4] :
( ssPv1(X4)
| ssPv3(skf1(X3))
| ssPv4(X1)
| ~ ssPv4(X2)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f128,f52]) ).
fof(f618,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f397,f52]) ).
fof(f619,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f618,f163]) ).
fof(f621,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f618,f191]) ).
fof(f622,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f619]) ).
fof(f623,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f621]) ).
fof(f637,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f441,f52]) ).
fof(f644,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f637,f312]) ).
fof(f646,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f637,f265]) ).
fof(f648,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f637,f156]) ).
fof(f654,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f644]) ).
fof(f655,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f646]) ).
fof(f667,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f655,f189]) ).
fof(f671,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f667]) ).
fof(f672,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f271]) ).
fof(f674,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f648,f655]) ).
fof(f716,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f278,f210]) ).
fof(f721,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f716,f236]) ).
fof(f722,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f721,f191]) ).
fof(f757,plain,
! [X0,X1,X2] :
( ssPv3(X2)
| ssPv1(X2)
| ssPv3(X1)
| ssPv4(skf1(skf1(X2)))
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f309,f52]) ).
fof(f774,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f310,f52]) ).
fof(f777,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f774,f52]) ).
fof(f800,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f672,f162]) ).
fof(f808,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f800]) ).
fof(f809,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f808,f622]) ).
fof(f821,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f809,f282]) ).
fof(f826,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f821]) ).
fof(f885,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f332,f52]) ).
fof(f889,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f885,f52]) ).
fof(f891,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f889,f198]) ).
fof(f895,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f891]) ).
fof(f896,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f895,f203]) ).
fof(f900,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f896,f159]) ).
fof(f905,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f900]) ).
fof(f1008,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv2(X1)
| ~ ssPv1(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f336,f52]) ).
fof(f1022,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1008,f52]) ).
fof(f1028,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1022,f319]) ).
fof(f1030,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1022,f303]) ).
fof(f1048,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1028]) ).
fof(f1049,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv2(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1030]) ).
fof(f1062,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1048,f198]) ).
fof(f1065,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1062]) ).
fof(f1066,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1065,f203]) ).
fof(f1067,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1066,f905]) ).
fof(f1080,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ssPv1(X1)
| ssPv4(skf1(skf1(X2)))
| ~ ssPv3(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f367,f52]) ).
fof(f1082,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1049,f198]) ).
fof(f1085,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1082]) ).
fof(f1086,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1085,f203]) ).
fof(f1087,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1086,f905]) ).
fof(f1097,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f1087,f226]) ).
fof(f1114,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1097]) ).
fof(f1115,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f249]) ).
fof(f1118,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f1115,f163]) ).
fof(f1125,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1118,f674]) ).
fof(f1128,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f368,f52]) ).
fof(f1131,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1125,f809]) ).
fof(f1193,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1128,f52]) ).
fof(f1200,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1193,f312]) ).
fof(f1201,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1193,f303]) ).
fof(f1202,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1193,f265]) ).
fof(f1225,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1200]) ).
fof(f1226,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1225,f159]) ).
fof(f1227,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1201,f282]) ).
fof(f1228,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1202]) ).
fof(f1246,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f654,f1226]) ).
fof(f1253,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv2(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f1226,f169]) ).
fof(f1254,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(skf1(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1226,f1087]) ).
fof(f1260,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1253]) ).
fof(f1261,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1254]) ).
fof(f1262,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1261,f285]) ).
fof(f1284,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f372,f52]) ).
fof(f1305,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1227,f1262]) ).
fof(f1334,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1228,f1305]) ).
fof(f1336,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1334,f209]) ).
fof(f1339,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1334,f1067]) ).
fof(f1345,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1336]) ).
fof(f1346,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1345,f655]) ).
fof(f1349,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1339]) ).
fof(f1350,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1349,f637]) ).
fof(f1355,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f1346,f1193]) ).
fof(f1360,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f1346,f189]) ).
fof(f1366,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1355]) ).
fof(f1367,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1366,f1334]) ).
fof(f1370,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1360]) ).
fof(f1371,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1370,f271]) ).
fof(f1398,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f1367,f209]) ).
fof(f1407,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1398]) ).
fof(f1442,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f1371,f162]) ).
fof(f1453,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1442]) ).
fof(f1454,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1453,f191]) ).
fof(f1460,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f210,f1454]) ).
fof(f1472,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f1460,f1454]) ).
fof(f1514,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f826,f1472]) ).
fof(f1528,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f623,f1514]) ).
fof(f1529,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1514,f1460]) ).
fof(f1539,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f1529]) ).
fof(f1552,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f1528,f282]) ).
fof(f1560,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1552]) ).
fof(f1561,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv2(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1560,f1022]) ).
fof(f1595,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1350,f303]) ).
fof(f1613,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1595,f1346]) ).
fof(f1628,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f1260,f306]) ).
fof(f1632,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1628]) ).
fof(f1633,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1632,f322]) ).
fof(f1652,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f409,f52]) ).
fof(f1654,plain,
! [X0,X1,X2] :
( ssPv3(X2)
| ssPv3(skf1(skf1(X2)))
| ~ ssPv4(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f409,f52]) ).
fof(f1659,plain,
! [X0,X1,X2] :
( ssPv1(X1)
| ssPv4(skf1(skf1(X2)))
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f412,f52]) ).
fof(f1660,plain,
! [X0] :
( ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1613,f1246]) ).
fof(f1701,plain,
! [X0,X1] :
( ssPv1(skf1(skf1(X0)))
| ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f413,f52]) ).
fof(f1724,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1284,f52]) ).
fof(f1731,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1724,f896]) ).
fof(f1739,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f1731]) ).
fof(f1740,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1739,f203]) ).
fof(f1779,plain,
! [X0,X1] :
( ssPv2(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f439,f52]) ).
fof(f1819,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1561,f1539]) ).
fof(f1864,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1652,f52]) ).
fof(f1896,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1701,f52]) ).
fof(f1904,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1896,f303]) ).
fof(f1905,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1896,f265]) ).
fof(f1924,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1904]) ).
fof(f1925,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1924,f282]) ).
fof(f1926,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1905]) ).
fof(f1927,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1926,f1131]) ).
fof(f1989,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f1779,f52]) ).
fof(f1998,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1989,f249]) ).
fof(f2004,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1998]) ).
fof(f2005,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv2(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2004,f159]) ).
fof(f2013,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f180,f2016]) ).
fof(f2014,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1633,f2016]) ).
fof(f2016,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2005,f905]) ).
fof(f2017,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2016,f1896]) ).
fof(f2018,plain,
! [X0] :
( ssPv2(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2016,f1819]) ).
fof(f2021,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2016,f1193]) ).
fof(f2030,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2017]) ).
fof(f2031,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2018]) ).
fof(f2032,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2021]) ).
fof(f2033,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2032,f889]) ).
fof(f2044,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f722,f2014]) ).
fof(f2049,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f2014,f165]) ).
fof(f2051,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2049,f674]) ).
fof(f2117,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f464,f52]) ).
fof(f2123,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2031,f165]) ).
fof(f2124,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2123,f1454]) ).
fof(f2130,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f2124,f209]) ).
fof(f2139,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2130]) ).
fof(f2140,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2139,f1407]) ).
fof(f2145,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2140,f1460]) ).
fof(f2155,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2145]) ).
fof(f2165,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2030,f165]) ).
fof(f2166,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2165]) ).
fof(f2167,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2166,f1925]) ).
fof(f2312,plain,
! [X0,X1,X2] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1)
| ~ ssPv1(X2)
| ~ ssRr(X1,X2)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f483,f52]) ).
fof(f2313,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(skf1(X0)))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2117,f52]) ).
fof(f2314,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2313,f1460]) ).
fof(f2317,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2313,f618]) ).
fof(f2324,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2314]) ).
fof(f2325,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2324,f2124]) ).
fof(f2326,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2317,f209]) ).
fof(f2330,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f237,f2325]) ).
fof(f2331,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2051,f2325]) ).
fof(f2332,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f2325,f1460]) ).
fof(f2335,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f2325,f618]) ).
fof(f2342,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2335]) ).
fof(f2347,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2331,f1193]) ).
fof(f2358,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2347]) ).
fof(f2359,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2358,f252]) ).
fof(f2365,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2330,f1193]) ).
fof(f2376,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2365]) ).
fof(f2377,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2376,f1334]) ).
fof(f2379,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2332,f1460]) ).
fof(f2389,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2379,f2155]) ).
fof(f2451,plain,
! [X0,X1] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(skf1(X0)))
| ~ ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f484,f52]) ).
fof(f2463,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f2359,f159]) ).
fof(f2471,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2463,f1226]) ).
fof(f2492,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f2471,f282]) ).
fof(f2503,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2492]) ).
fof(f2504,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2503,f2140]) ).
fof(f2524,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2377,f618]) ).
fof(f2532,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2524]) ).
fof(f2533,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2532,f252]) ).
fof(f2585,plain,
! [X0,X1] :
( ssPv1(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ssPv4(X1)
| ~ ssPv4(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f513,f52]) ).
fof(f2590,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2326,f2325]) ).
fof(f2591,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f2590,f2533]) ).
fof(f2598,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f2590,f1927]) ).
fof(f2613,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2591]) ).
fof(f2614,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2613,f2325]) ).
fof(f2618,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2598]) ).
fof(f2660,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f2614,f2359]) ).
fof(f2680,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2660]) ).
fof(f2681,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2680,f2342]) ).
fof(f2705,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2681,f1927]) ).
fof(f2720,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2705,f265]) ).
fof(f2751,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2720,f2389]) ).
fof(f2765,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2751]) ).
fof(f2766,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2765,f1460]) ).
fof(f2770,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2720,f2766]) ).
fof(f2771,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2330,f2766]) ).
fof(f2784,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f282,f2770]) ).
fof(f2800,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0)))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2771,f777]) ).
fof(f2808,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2800]) ).
fof(f2809,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f2533,f2784]) ).
fof(f2818,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f2784,f2681]) ).
fof(f2827,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2818]) ).
fof(f2855,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f2827,f319]) ).
fof(f2856,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f2827,f312]) ).
fof(f2874,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2855,f2770]) ).
fof(f2875,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2856]) ).
fof(f2936,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2808,f1864]) ).
fof(f2938,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2808,f1724]) ).
fof(f2942,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2808,f159]) ).
fof(f2948,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2936]) ).
fof(f2950,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2938]) ).
fof(f2951,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2950,f1740]) ).
fof(f2952,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2942,f2016]) ).
fof(f2962,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f2952,f303]) ).
fof(f2979,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2962]) ).
fof(f3005,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2951,f1346]) ).
fof(f3019,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3005]) ).
fof(f3020,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3019,f2784]) ).
fof(f3142,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3020,f2681]) ).
fof(f3150,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3142]) ).
fof(f3384,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2948,f2313]) ).
fof(f3394,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f2948,f2766]) ).
fof(f3404,plain,
! [X0] :
( ~ ssPv4(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3384]) ).
fof(f3405,plain,
! [X0] :
( ~ ssPv4(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3404,f2590]) ).
fof(f3410,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3394]) ).
fof(f3411,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3410,f2951]) ).
fof(f3487,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3405,f2808]) ).
fof(f3507,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3487]) ).
fof(f3522,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f3507,f156]) ).
fof(f3525,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f3507,f2331]) ).
fof(f3536,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3522,f2681]) ).
fof(f3537,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3525]) ).
fof(f3751,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f2979,f2504]) ).
fof(f3762,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3751]) ).
fof(f4002,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3536,f2766]) ).
fof(f4068,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f2451,f52]) ).
fof(f4074,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4068,f2827]) ).
fof(f4078,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4068,f1350]) ).
fof(f4094,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4074]) ).
fof(f4095,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4094,f2770]) ).
fof(f4099,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4078]) ).
fof(f4100,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4099,f1346]) ).
fof(f4107,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f4095,f1115]) ).
fof(f4113,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f4095,f279]) ).
fof(f4114,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f4095,f249]) ).
fof(f4118,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4107,f1660]) ).
fof(f4120,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4114,f2770]) ).
fof(f4151,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f4118,f203]) ).
fof(f4163,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f4151]) ).
fof(f4217,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f4120,f203]) ).
fof(f4229,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f4217]) ).
fof(f4230,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4229,f2770]) ).
fof(f4231,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv2(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2044,f4230]) ).
fof(f4233,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f4230,f1115]) ).
fof(f4243,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4233]) ).
fof(f4280,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4243,f1896]) ).
fof(f4283,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4243,f1350]) ).
fof(f4299,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4280]) ).
fof(f4300,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4299,f2809]) ).
fof(f4301,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4283]) ).
fof(f4302,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4301,f2809]) ).
fof(f4318,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4113,f4230]) ).
fof(f4319,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv2(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f4318,f1460]) ).
fof(f4329,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv2(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4319]) ).
fof(f4342,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f4100,f279]) ).
fof(f4347,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4342,f2016]) ).
fof(f4350,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f4118,f4351]) ).
fof(f4351,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4347,f1246]) ).
fof(f4432,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4300,f432]) ).
fof(f4438,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4432]) ).
fof(f4439,plain,
! [X0,X1] :
( ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4438,f1925]) ).
fof(f4451,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f4329,f2033]) ).
fof(f4466,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4451,f4231]) ).
fof(f4481,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4466,f2325]) ).
fof(f4496,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f4481,f2681]) ).
fof(f4508,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4496]) ).
fof(f4551,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f4508,f226]) ).
fof(f4566,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4551]) ).
fof(f4567,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4566,f2766]) ).
fof(f4577,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4567,f2325]) ).
fof(f4584,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f4577,f279]) ).
fof(f4616,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4584,f1048]) ).
fof(f4622,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f4584,f3762]) ).
fof(f4630,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4616]) ).
fof(f4631,plain,
! [X0] :
( ~ ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4630,f319]) ).
fof(f4633,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4622]) ).
fof(f4634,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4633,f4350]) ).
fof(f4676,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4634,f4163]) ).
fof(f4769,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f4631,f2014]) ).
fof(f4778,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4769]) ).
fof(f4779,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4778,f2016]) ).
fof(f4823,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f4439,f209]) ).
fof(f4839,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f4823]) ).
fof(f4840,plain,
! [X0,X1] :
( ssPv4(skf1(X0))
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4839,f4676]) ).
fof(f4841,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f4840,f52]) ).
fof(f4842,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4841,f2874]) ).
fof(f4844,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2875,f4842]) ).
fof(f4852,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f4842,f249]) ).
fof(f4856,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4852,f4231]) ).
fof(f4926,plain,
! [X0] :
( ssPv1(skf1(skf1(X0)))
| ~ ssPv3(skf1(X0))
| ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3150,f4929]) ).
fof(f4929,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4856,f4577]) ).
fof(f4941,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f4929,f637]) ).
fof(f4954,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f4941]) ).
fof(f4955,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4954,f4577]) ).
fof(f5041,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f4955,f279]) ).
fof(f5045,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5041]) ).
fof(f5067,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f5045,f2033]) ).
fof(f5073,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f5045,f187]) ).
fof(f5083,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f5067]) ).
fof(f5086,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f5073]) ).
fof(f5087,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5086,f159]) ).
fof(f5107,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f5087,f2013]) ).
fof(f5117,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5107]) ).
fof(f5118,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5117,f2471]) ).
fof(f5129,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[f5118,f2167]) ).
fof(f5145,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5129,f5045]) ).
fof(f5164,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f5145,f2681]) ).
fof(f5172,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5164]) ).
fof(f5388,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f5083,f1724]) ).
fof(f5402,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5388]) ).
fof(f5403,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5402,f169]) ).
fof(f5420,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f5403,f226]) ).
fof(f5435,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5420]) ).
fof(f5436,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5435,f4779]) ).
fof(f5455,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f5436,f3411]) ).
fof(f5477,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5455,f2808]) ).
fof(f5492,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5477,f4577]) ).
fof(f5604,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0)))
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4302,f4577]) ).
fof(f5863,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ssPv2(X2)
| ssPv3(X2)
| ssPv1(X2)
| ssPv3(X1)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f757,f159]) ).
fof(f5879,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ssPv2(X2)
| ssPv3(X2)
| ssPv3(X1)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f5863,f2016]) ).
fof(f5906,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f5879,f52]) ).
fof(f5907,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f5906,f52]) ).
fof(f6207,plain,
! [X0,X1,X2] :
( ssPv1(X2)
| ssPv4(skf1(X2))
| ~ ssPv3(X2)
| ssPv4(X2)
| ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f1080,f209]) ).
fof(f6221,plain,
! [X0,X1,X2] :
( ssPv1(X2)
| ssPv4(skf1(X2))
| ssPv4(X2)
| ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f6207]) ).
fof(f6222,plain,
! [X0,X1,X2] :
( ssPv4(skf1(X2))
| ssPv4(X2)
| ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6221,f4163]) ).
fof(f6320,plain,
! [X0,X1] :
( ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv1(X1)
| ~ ssPv3(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f6222,f52]) ).
fof(f6321,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f6320,f52]) ).
fof(f6876,plain,
! [X0,X1,X2] :
( ~ ssPv4(X2)
| ssPv4(skf1(X2))
| ssPv3(X2)
| ~ ssPv4(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f1654,f4955]) ).
fof(f6889,plain,
! [X0,X1,X2] :
( ssPv1(skf1(X2))
| ssPv3(X2)
| ~ ssPv4(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f1654,f4577]) ).
fof(f6893,plain,
! [X0,X1,X2] :
( ssPv4(skf1(X2))
| ssPv3(X2)
| ~ ssPv4(X2)
| ~ ssRr(X2,X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f6876]) ).
fof(f6993,plain,
! [X0,X1,X2] :
( ssPv1(X2)
| ssPv4(skf1(X2))
| ~ ssPv3(X2)
| ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f1659,f209]) ).
fof(f7010,plain,
! [X0,X1,X2] :
( ssPv1(X2)
| ssPv4(skf1(X2))
| ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f6993]) ).
fof(f7011,plain,
! [X0,X1,X2] :
( ssPv4(skf1(X2))
| ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssPv2(X2)
| ~ ssRr(X2,X0)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f7010,f4676]) ).
fof(f7301,plain,
! [X0,X1] :
( ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f6893,f52]) ).
fof(f7302,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f7301,f52]) ).
fof(f7339,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f7302,f4163]) ).
fof(f7352,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f7339]) ).
fof(f7353,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7352,f4929]) ).
fof(f7356,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7353,f4844]) ).
fof(f7368,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f7356,f5403]) ).
fof(f7399,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(skf1(X0)))
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f7368,f5604]) ).
fof(f7407,plain,
! [X0,X1] :
( ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv4(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f6889,f52]) ).
fof(f7408,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f7407,f52]) ).
fof(f7498,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f7408,f3537]) ).
fof(f7511,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f7498]) ).
fof(f7512,plain,
! [X0] :
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7511,f2681]) ).
fof(f7538,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f7512,f2809]) ).
fof(f7564,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f7538]) ).
fof(f7758,plain,
! [X0,X1] :
( ssPv4(skf1(X0))
| ssPv1(X1)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f7011,f52]) ).
fof(f7759,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f7758,f52]) ).
fof(f7997,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f7399,f777]) ).
fof(f8008,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f7997]) ).
fof(f8009,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8008,f4779]) ).
fof(f8017,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv4(skf1(X0))
| ssPv4(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8009,f2809]) ).
fof(f8040,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f8017,f7512]) ).
fof(f8055,plain,
! [X0] :
( ssPv3(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8040]) ).
fof(f8208,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f7564,f319]) ).
fof(f8209,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f7564,f312]) ).
fof(f8229,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8208]) ).
fof(f8230,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8229,f4676]) ).
fof(f8231,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8209]) ).
fof(f8232,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8231,f4350]) ).
fof(f8284,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv4(skf1(skf1(X0)))
| ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f8232,f5604]) ).
fof(f8309,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8284]) ).
fof(f8704,plain,
! [X0,X1,X2] :
( ~ ssPv2(X2)
| ~ ssPv1(X2)
| ~ ssPv3(X2)
| ~ ssPv3(X2)
| ~ ssPv1(X2)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f2312,f8230]) ).
fof(f8722,plain,
! [X0,X1,X2] :
( ~ ssPv2(X2)
| ~ ssPv3(X2)
| ~ ssPv1(X2)
| ~ ssRr(X2,X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f8704]) ).
fof(f8734,plain,
! [X0,X1] :
( ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssRr(skf1(X0),X1) ),
inference(resolution,[status(thm)],[f8722,f52]) ).
fof(f8735,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[f8734,f52]) ).
fof(f8828,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f8055,f226]) ).
fof(f8851,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8828]) ).
fof(f8852,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8851,f1115]) ).
fof(f8890,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv3(skf1(skf1(X0)))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8852,f249]) ).
fof(f9108,plain,
! [X0,X1] :
( ssPv1(skf1(X0))
| ssPv4(X1)
| ~ ssPv4(X0)
| ~ ssRr(skf1(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2585,f4577]) ).
fof(f9109,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv4(skf1(skf1(X0)))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f9108,f52]) ).
fof(f9112,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f7408,f9109]) ).
fof(f9129,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f9109,f2590]) ).
fof(f9155,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0))
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f9129]) ).
fof(f9156,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9155,f2618]) ).
fof(f9172,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f7512,f9156]) ).
fof(f9175,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3537,f9156]) ).
fof(f9210,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2952,f9112]) ).
fof(f9211,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5172,f9112]) ).
fof(f9401,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f9211,f2016]) ).
fof(f9411,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9401,f5045]) ).
fof(f9502,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1067,f9172]) ).
fof(f9579,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f4002,f9502]) ).
fof(f9582,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f9502,f8309]) ).
fof(f9608,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f9502,f1927]) ).
fof(f9617,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9582]) ).
fof(f9618,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9617,f312]) ).
fof(f9627,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(skf1(skf1(X0)))
| ~ ssPv1(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9608]) ).
fof(f9628,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9627,f265]) ).
fof(f9700,plain,
! [X0] :
( ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f9628,f4926]) ).
fof(f9703,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f9628,f2827]) ).
fof(f9706,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[f9628,f1740]) ).
fof(f9730,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9700]) ).
fof(f9731,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9730,f4929]) ).
fof(f9733,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9703]) ).
fof(f9734,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9733,f4844]) ).
fof(f9736,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9706]) ).
fof(f9737,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9736,f1087]) ).
fof(f9746,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9731,f8890]) ).
fof(f9754,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9731,f5907]) ).
fof(f9762,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9754,f5118]) ).
fof(f9933,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5436,f9746]) ).
fof(f9960,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9746,f9737]) ).
fof(f9965,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9746,f5492]) ).
fof(f9984,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9960]) ).
fof(f9985,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9965]) ).
fof(f9986,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9985,f9175]) ).
fof(f9992,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9933,f7759]) ).
fof(f9997,plain,
! [X0] :
( ssPv4(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f9933,f6321]) ).
fof(f10012,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f9933,f9737]) ).
fof(f10022,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9992]) ).
fof(f10023,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f10022,f9734]) ).
fof(f10027,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9997]) ).
fof(f10028,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ssPv4(skf1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f10027,f9734]) ).
fof(f10037,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10012]) ).
fof(f10041,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f7356,f10037]) ).
fof(f10138,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[f10041,f9112]) ).
fof(f10234,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f10023,f2681]) ).
fof(f10241,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10234]) ).
fof(f10261,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f10028,f5118]) ).
fof(f10262,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f10028,f2681]) ).
fof(f10270,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10261]) ).
fof(f10271,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10270,f9762]) ).
fof(f10272,plain,
! [X0] :
( ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10262]) ).
fof(f10356,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f10241,f9628]) ).
fof(f10359,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10356]) ).
fof(f10370,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f8735,f10359]) ).
fof(f10416,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f10272,f9628]) ).
fof(f10422,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f10416]) ).
fof(f10423,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10422,f9156]) ).
fof(f10436,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f9986,f10423]) ).
fof(f10448,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f156,f10423]) ).
fof(f10454,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f4068,f10423]) ).
fof(f10469,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f10454,f10423]) ).
fof(f10473,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f9984,f10436]) ).
fof(f10485,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f10436,f9579]) ).
fof(f10492,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f8017,f10473]) ).
fof(f10499,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f10138,f10473]) ).
fof(f10500,plain,
! [X0] :
( ssPv4(skf1(X0))
| ~ ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f9411,f10473]) ).
fof(f10540,plain,
! [X0] :
( ssPv1(skf1(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f10499,f9502]) ).
fof(f10581,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f10469,f8890]) ).
fof(f10588,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10581,f9933]) ).
fof(f10606,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f10272,f10588]) ).
fof(f10661,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f2313,f10606]) ).
fof(f10825,plain,
! [X0] :
( ~ ssPv4(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f10370,f9211]) ).
fof(f10826,plain,
! [X0] :
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f10370,f9210]) ).
fof(f10831,plain,
! [X0] :
( ~ ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10825,f10500]) ).
fof(f10832,plain,
! [X0] :
( ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10826,f9734]) ).
fof(f10848,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv1(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f9618,f10851]) ).
fof(f10851,plain,
! [X0] :
( ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10832,f10831]) ).
fof(f10859,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv4(skf1(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2681,f10848]) ).
fof(f10898,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f10448,f10540]) ).
fof(f10906,plain,
! [X0] :
( ~ ssPv1(skf1(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10898,f4577]) ).
fof(f10924,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f165,f10927]) ).
fof(f10927,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10906,f10485]) ).
fof(f11027,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f10924,f10271]) ).
fof(f11028,plain,
! [X0] :
( ssPv4(skf1(skf1(X0)))
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11027,f10492]) ).
fof(f11033,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f11028,f1864]) ).
fof(f11040,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11033,f10661]) ).
fof(f11042,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11040,f10423]) ).
fof(f11048,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[f11042,f10473]) ).
fof(f11050,plain,
! [X0] : ssPv4(X0),
inference(forward_subsumption_resolution,[status(thm)],[f11048,f10588]) ).
fof(f11076,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf1(skf1(X0)))
| ~ ssPv4(skf1(skf1(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1864,f11050]) ).
fof(f11089,plain,
! [X0] : ~ ssPv3(X0),
inference(backward_subsumption_resolution,[status(thm)],[f10859,f11050]) ).
fof(f11101,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf1(skf1(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f11076,f11050]) ).
fof(f11160,plain,
! [X0] : ssPv3(X0),
inference(forward_subsumption_resolution,[status(thm)],[f11101,f11089]) ).
fof(f11161,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f11089,f11160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN762-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.36 % Computer : n004.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Mon Sep 21 11:15:05 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 64.93/8.62 % Refutation found
% 64.93/8.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 64.93/8.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 64.93/8.66 % Elapsed time: 8.274626 seconds
% 64.93/8.66 % CPU time: 65.294538 seconds
% 64.93/8.66 % Total memory used: 95.031 MB
% 64.93/8.66 % Net memory used: 66.275 MB
%------------------------------------------------------------------------------