%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN784-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:29 PM UTC 2026
% Result : Unsatisfiable 7.78s 1.39s
% Output : CNFRefutation 6.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 115
% Number of leaves : 34
% Syntax : Number of formulae : 444 ( 10 unt; 0 def)
% Number of atoms : 2035 ( 0 equ)
% Maximal formula atoms : 7 ( 4 avg)
% Number of connectives : 2635 (1044 ~;1591 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 0 con; 1-1 aty)
% Number of variables : 753 ( 753 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [U] : ssRr(skf3(U),U),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
! [U] : ssRr(U,skf2(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
! [U,V] :
( ssPv4(V)
| ssPv3(V)
| ssPv2(V)
| ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
! [U,V] :
( ssPv3(V)
| ssPv2(V)
| ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
! [U,V] :
( ssPv2(V)
| ssPv2(U)
| ~ ssPv4(V)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
! [U,V] :
( ssPv1(U)
| ssPv1(V)
| ~ ssPv4(U)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
! [U,V] :
( ssPv1(V)
| ssPv1(U)
| ~ ssPv3(V)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
! [U,V,W] :
( ssPv4(U)
| ssPv3(U)
| ssPv3(W)
| ssPv4(V)
| ~ ssRr(U,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
! [U,V,W] :
( ssPv4(V)
| ssPv4(W)
| ssPv2(U)
| ~ ssPv3(V)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
! [U,V,W] :
( ssPv3(V)
| ssPv2(W)
| ssPv3(U)
| ~ ssPv2(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
! [U,V,W] :
( ssPv2(W)
| ssPv4(U)
| ~ ssPv4(V)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
! [U,V,W] :
( ssPv4(U)
| ssPv4(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
! [U,V,W] :
( ssPv3(V)
| ssPv4(W)
| ~ ssPv4(V)
| ~ ssRr(W,V)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
! [U,V,W] :
( ssPv3(U)
| ssPv1(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
! [U,V,W] :
( ssPv3(U)
| ssPv4(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
! [U,V,W] :
( ssPv2(V)
| ssPv3(W)
| ~ ssPv4(V)
| ~ ssRr(W,V)
| ~ ssPv1(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
! [U,V,W] :
( ssPv4(V)
| ssPv2(V)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
! [U,V,W] :
( ssPv3(U)
| ~ ssPv4(V)
| ~ ssPv3(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [U,V,W] :
( ssPv4(W)
| ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [U,V,W] :
( ssPv2(W)
| ~ ssPv3(V)
| ~ ssPv2(V)
| ~ ssRr(V,W)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv4(V)
| ~ ssPv1(V)
| ~ ssRr(V,W)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [U,V,W] :
( ssPv4(U)
| ~ ssPv3(U)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
! [U,V,W] :
( ssPv1(V)
| ~ ssPv3(V)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
! [U,V,W] :
( ssPv1(V)
| ~ ssPv3(V)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
! [U,V,W,X] :
( ssPv3(V)
| ssPv2(X)
| ssPv4(W)
| ssPv1(U)
| ~ ssRr(V,X)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
! [U,V,W,X] :
( ssPv4(V)
| ssPv4(X)
| ~ ssRr(V,X)
| ~ ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
! [U,V,W,X] :
( ssPv3(X)
| ssPv4(W)
| ~ ssPv4(V)
| ~ ssRr(V,X)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
! [U,V,W,X] :
( ssPv2(V)
| ssPv1(X)
| ~ ssRr(X,V)
| ~ ssPv2(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
! [U,V,W,X] :
( ssPv2(V)
| ssPv4(U)
| ~ ssPv3(X)
| ~ ssRr(V,X)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
! [U,V,W,X] :
( ssPv2(V)
| ssPv3(X)
| ~ ssRr(V,X)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
! [U,V,W,X] :
( ssPv2(X)
| ~ ssPv1(V)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssPv1(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
! [U,V,W,X] :
( ssPv4(U)
| ~ ssPv1(V)
| ~ ssPv2(X)
| ~ ssRr(V,X)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
! [U,V,W,X] :
( ~ ssPv1(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
! [U,V,W,X] :
( ~ ssPv1(V)
| ~ ssPv3(X)
| ~ ssRr(V,X)
| ~ ssPv2(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,plain,
! [X0] : ssRr(skf3(X0),X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f44,plain,
! [X0] : ssRr(X0,skf2(X0)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
! [V] :
( ssPv4(V)
| ssPv3(V)
| ssPv2(V)
| ! [U] :
( ssPv4(U)
| ~ ssRr(U,V) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f46,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv3(X1)
| ssPv2(X1)
| ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
! [V] :
( ssPv3(V)
| ssPv2(V)
| ! [U] :
( ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f48,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv2(X1)
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [V] :
( ssPv2(V)
| ! [U] :
( ssPv2(U)
| ~ ssPv4(V)
| ~ ssPv1(V)
| ~ ssRr(U,V) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f50,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [U] :
( ssPv1(U)
| ! [V] :
( ssPv1(V)
| ~ ssPv4(U)
| ~ ssPv3(U)
| ~ ssRr(U,V) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f52,plain,
! [X0,X1] :
( ssPv1(X0)
| ssPv1(X1)
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
! [V] :
( ssPv1(V)
| ! [U] :
( ssPv1(U)
| ~ ssPv3(V)
| ~ ssPv2(V)
| ~ ssRr(U,V) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f54,plain,
! [X0,X1] :
( ssPv1(X1)
| ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
! [U] :
( ssPv4(U)
| ssPv3(U)
| ! [W] :
( ssPv3(W)
| ! [V] :
( ssPv4(V)
| ~ ssRr(U,W)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(X2)
| ssPv4(X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [V] :
( ssPv4(V)
| ! [W] :
( ssPv4(W)
| ! [U] :
( ssPv2(U)
| ~ ssPv3(V)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f58,plain,
! [X0,X1,X2] :
( ssPv4(X1)
| ssPv4(X2)
| ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [V] :
( ssPv3(V)
| ! [W] :
( ssPv2(W)
| ! [U] :
( ssPv3(U)
| ~ ssPv2(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ssPv3(X1)
| ssPv2(X2)
| ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssRr(X2,X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f63,plain,
! [W] :
( ssPv2(W)
| ! [U] :
( ssPv4(U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ssPv2(X2)
| ssPv4(X0)
| ~ ssPv4(X1)
| ~ ssPv1(X1)
| ~ ssRr(X2,X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f67,plain,
! [U] :
( ssPv4(U)
| ! [W] :
( ssPv4(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f68,plain,
! [X0,X1,X2] :
( ssPv4(X0)
| ssPv4(X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [V] :
( ssPv3(V)
| ! [W] :
( ssPv4(W)
| ~ ssPv4(V)
| ~ ssRr(W,V)
| ! [U] :
( ~ ssPv3(U)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ssPv3(X1)
| ssPv4(X2)
| ~ ssPv4(X1)
| ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [U] :
( ssPv3(U)
| ! [W] :
( ssPv1(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f72,plain,
! [X0,X1,X2] :
( ssPv3(X0)
| ssPv1(X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [U] :
( ssPv3(U)
| ! [W] :
( ssPv4(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ssPv3(X0)
| ssPv4(X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
! [V] :
( ssPv2(V)
| ! [W] :
( ssPv3(W)
| ~ ssPv4(V)
| ~ ssRr(W,V)
| ! [U] :
( ~ ssPv1(U)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ssPv2(X1)
| ssPv3(X2)
| ~ ssPv4(X1)
| ~ ssRr(X2,X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [V] :
( ssPv4(V)
| ssPv2(V)
| ! [W] :
( ~ ssPv3(W)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv4(U)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ssPv4(X1)
| ssPv2(X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [U] :
( ssPv3(U)
| ! [V] :
( ~ ssPv4(V)
| ~ ssPv3(V)
| ! [W] :
( ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssPv3(X1)
| ~ ssPv4(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [W] :
( ssPv4(W)
| ! [U] :
( ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ! [V] :
( ~ ssPv2(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ssPv4(X2)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [W] :
( ssPv2(W)
| ! [V] :
( ~ ssPv3(V)
| ~ ssPv2(V)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv3(U)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ssPv2(X2)
| ~ ssPv3(X1)
| ~ ssPv2(X1)
| ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [W] :
( ssPv1(W)
| ! [V] :
( ~ ssPv4(V)
| ~ ssPv1(V)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv4(U)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ssPv1(X2)
| ~ ssPv4(X1)
| ~ ssPv1(X1)
| ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
! [U] :
( ssPv4(U)
| ~ ssPv3(U)
| ! [W] :
( ~ ssPv2(W)
| ~ ssRr(U,W)
| ! [V] :
( ~ ssPv3(V)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f88,plain,
! [X0,X1,X2] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
! [V] :
( ssPv1(V)
| ~ ssPv3(V)
| ! [W] :
( ~ ssPv3(W)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv4(U)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ssPv1(X1)
| ~ ssPv3(X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [V] :
( ssPv1(V)
| ~ ssPv3(V)
| ! [W] :
( ~ ssPv3(W)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv2(U)
| ~ ssRr(U,V) ) ) ),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f92,plain,
! [X0,X1,X2] :
( ssPv1(X1)
| ~ ssPv3(X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [V] :
( ssPv3(V)
| ! [X] :
( ssPv2(X)
| ! [W] :
( ssPv4(W)
| ! [U] :
( ssPv1(U)
| ~ ssRr(V,X)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f27]) ).
fof(f94,plain,
! [X0,X1,X2,X3] :
( ssPv3(X1)
| ssPv2(X3)
| ssPv4(X2)
| ssPv1(X0)
| ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f101,plain,
! [V] :
( ssPv4(V)
| ! [X] :
( ssPv4(X)
| ~ ssRr(V,X)
| ! [W] :
( ~ ssPv2(W)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv3(U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( ssPv4(X1)
| ssPv4(X3)
| ~ ssRr(X1,X3)
| ~ ssPv2(X2)
| ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f107,plain,
! [X] :
( ssPv3(X)
| ! [W] :
( ssPv4(W)
| ! [V] :
( ~ ssPv4(V)
| ~ ssRr(V,X)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv2(U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f108,plain,
! [X0,X1,X2,X3] :
( ssPv3(X3)
| ssPv4(X2)
| ~ ssPv4(X1)
| ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [V] :
( ssPv2(V)
| ! [X] :
( ssPv1(X)
| ~ ssRr(X,V)
| ! [W] :
( ~ ssPv2(W)
| ~ ssRr(W,V)
| ! [U] :
( ~ ssPv4(U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f110,plain,
! [X0,X1,X2,X3] :
( ssPv2(X1)
| ssPv1(X3)
| ~ ssRr(X3,X1)
| ~ ssPv2(X2)
| ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [V] :
( ssPv2(V)
| ! [U] :
( ssPv4(U)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(V,X)
| ! [W] :
( ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( ssPv2(X1)
| ssPv4(X0)
| ~ ssPv3(X3)
| ~ ssRr(X1,X3)
| ~ ssPv4(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [V] :
( ssPv2(V)
| ! [X] :
( ssPv3(X)
| ~ ssRr(V,X)
| ! [W] :
( ~ ssPv4(W)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv2(U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( ssPv2(X1)
| ssPv3(X3)
| ~ ssRr(X1,X3)
| ~ ssPv4(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [X] :
( ssPv2(X)
| ! [V] :
( ~ ssPv1(V)
| ~ ssRr(V,X)
| ! [W] :
( ~ ssPv3(W)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv1(U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f116,plain,
! [X0,X1,X2,X3] :
( ssPv2(X3)
| ~ ssPv1(X1)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [U] :
( ssPv4(U)
| ! [V] :
( ~ ssPv1(V)
| ! [X] :
( ~ ssPv2(X)
| ~ ssRr(V,X)
| ! [W] :
( ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f39]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X3)
| ~ ssRr(X1,X3)
| ~ ssPv4(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f121,plain,
! [V] :
( ~ ssPv1(V)
| ! [X] :
( ~ ssPv1(X)
| ~ ssRr(V,X)
| ! [W] :
( ~ ssPv2(W)
| ~ ssRr(V,W)
| ! [U] :
( ~ ssPv2(U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f122,plain,
! [X0,X1,X2,X3] :
( ~ ssPv1(X1)
| ~ ssPv1(X3)
| ~ ssRr(X1,X3)
| ~ ssPv2(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [V] :
( ~ ssPv1(V)
| ! [X] :
( ~ ssPv3(X)
| ~ ssRr(V,X)
| ! [W] :
( ~ ssPv2(W)
| ~ ssRr(W,V)
| ! [U] :
( ~ ssPv4(U)
| ~ ssRr(U,V) ) ) ) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( ~ ssPv1(X1)
| ~ ssPv3(X3)
| ~ ssRr(X1,X3)
| ~ ssPv2(X2)
| ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f126,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f46,f44]) ).
fof(f127,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf3(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f48,f43]) ).
fof(f128,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f48,f44]) ).
fof(f129,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f50,f43]) ).
fof(f130,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[f50,f44]) ).
fof(f131,plain,
! [X0] :
( ssPv1(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[f52,f43]) ).
fof(f132,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f52,f44]) ).
fof(f133,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f54,f43]) ).
fof(f137,plain,
! [X0,X1] :
( ssPv4(skf3(X0))
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv4(X1)
| ~ ssRr(skf3(X0),X1) ),
inference(resolution,[status(thm)],[f56,f43]) ).
fof(f138,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f56,f44]) ).
fof(f140,plain,
! [X0] :
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f138,f44]) ).
fof(f142,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv4(skf2(X1))
| ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f58,f44]) ).
fof(f143,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv2(skf3(X1))
| ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f60,f43]) ).
fof(f144,plain,
! [X0,X1] :
( ssPv3(skf2(X1))
| ssPv2(X1)
| ssPv3(X0)
| ~ ssPv2(skf2(X1))
| ~ ssRr(X0,skf2(X1)) ),
inference(resolution,[status(thm)],[f60,f44]) ).
fof(f145,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv2(skf3(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f142,f43]) ).
fof(f146,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ~ ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[f142,f44]) ).
fof(f147,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf3(X0))
| ssPv3(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f143,f43]) ).
fof(f148,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf3(skf2(X0)))
| ssPv3(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[f143,f44]) ).
fof(f154,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv4(X0)
| ~ ssPv4(skf2(X1))
| ~ ssPv1(skf2(X1))
| ~ ssRr(X0,skf2(X1)) ),
inference(resolution,[status(thm)],[f64,f44]) ).
fof(f161,plain,
! [X0,X1] :
( ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv2(X1)
| ~ ssRr(skf3(X0),X1) ),
inference(resolution,[status(thm)],[f68,f43]) ).
fof(f162,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f68,f44]) ).
fof(f164,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[f162,f44]) ).
fof(f165,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv4(X0)
| ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f164,f126]) ).
fof(f166,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f165]) ).
fof(f167,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv4(skf3(X1))
| ~ ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f70,f43]) ).
fof(f168,plain,
! [X0,X1] :
( ssPv3(skf2(X1))
| ssPv4(X1)
| ~ ssPv4(skf2(X1))
| ~ ssPv3(X0)
| ~ ssRr(X0,skf2(X1)) ),
inference(resolution,[status(thm)],[f70,f44]) ).
fof(f169,plain,
! [X0,X1] :
( ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv4(X1)
| ~ ssRr(skf3(X0),X1) ),
inference(resolution,[status(thm)],[f72,f43]) ).
fof(f170,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f72,f44]) ).
fof(f171,plain,
! [X0,X1] :
( ssPv3(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv2(X1)
| ~ ssRr(skf3(X0),X1) ),
inference(resolution,[status(thm)],[f74,f43]) ).
fof(f172,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f74,f44]) ).
fof(f173,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv3(skf3(X1))
| ~ ssPv4(X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f76,f43]) ).
fof(f174,plain,
! [X0,X1] :
( ssPv2(skf2(X1))
| ssPv3(X1)
| ~ ssPv4(skf2(X1))
| ~ ssPv1(X0)
| ~ ssRr(X0,skf2(X1)) ),
inference(resolution,[status(thm)],[f76,f44]) ).
fof(f175,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[f167,f43]) ).
fof(f178,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f170,f44]) ).
fof(f180,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[f172,f44]) ).
fof(f183,plain,
! [X0,X1] :
( ssPv4(skf3(X1))
| ssPv2(skf3(X1))
| ~ ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f78,f43]) ).
fof(f184,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv2(X1)
| ~ ssPv3(skf2(X1))
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f78,f44]) ).
fof(f185,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[status(thm)],[f173,f43]) ).
fof(f191,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv3(X1)
| ssPv4(skf2(X1))
| ssPv4(X1)
| ssPv2(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f184,f140]) ).
fof(f193,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv4(skf2(X1))
| ssPv4(X1)
| ssPv2(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f191]) ).
fof(f194,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv4(skf2(X1))
| ssPv4(X1)
| ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f193,f46]) ).
fof(f195,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f194,f43]) ).
fof(f198,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f195,f128]) ).
fof(f199,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f198]) ).
fof(f209,plain,
! [X0,X1] :
( ssPv3(X0)
| ~ ssPv4(skf3(X1))
| ~ ssPv3(skf3(X1))
| ~ ssPv4(X1)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f80,f43]) ).
fof(f210,plain,
! [X0,X1] :
( ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssPv3(X1)
| ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f80,f44]) ).
fof(f212,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv2(X1)
| ~ ssRr(skf3(X0),X1) ),
inference(resolution,[status(thm)],[f82,f43]) ).
fof(f213,plain,
! [X0,X1] :
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f82,f44]) ).
fof(f215,plain,
! [X0] :
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[f213,f44]) ).
fof(f220,plain,
! [X0,X1] :
( ssPv2(skf2(X1))
| ~ ssPv3(X1)
| ~ ssPv2(X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f84,f44]) ).
fof(f221,plain,
! [X0,X1] :
( ssPv1(X1)
| ~ ssPv4(skf3(X1))
| ~ ssPv1(skf3(X1))
| ~ ssPv4(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f86,f43]) ).
fof(f222,plain,
! [X0,X1] :
( ssPv1(skf2(X1))
| ~ ssPv4(X1)
| ~ ssPv1(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f86,f44]) ).
fof(f223,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[f220,f43]) ).
fof(f225,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[f222,f43]) ).
fof(f228,plain,
! [X0,X1] :
( ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(skf3(X0),X1) ),
inference(resolution,[status(thm)],[f88,f43]) ).
fof(f229,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f88,f44]) ).
fof(f236,plain,
! [X0,X1] :
( ssPv1(X1)
| ~ ssPv3(X1)
| ~ ssPv3(skf2(X1))
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f90,f44]) ).
fof(f240,plain,
! [X0,X1] :
( ssPv1(X1)
| ~ ssPv3(X1)
| ~ ssPv3(skf2(X1))
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f92,f44]) ).
fof(f265,plain,
! [X0,X1] :
( ssPv3(skf3(X1))
| ssPv2(X1)
| ssPv4(X1)
| ssPv1(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f94,f43]) ).
fof(f267,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv2(skf2(X1))
| ssPv4(skf2(X1))
| ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f94,f44]) ).
fof(f312,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f265,f43]) ).
fof(f314,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ssPv1(skf3(X0)) ),
inference(resolution,[status(thm)],[f267,f43]) ).
fof(f316,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f314,f185]) ).
fof(f317,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f316,f195]) ).
fof(f339,plain,
! [X0,X1] :
( ssPv4(skf3(X1))
| ssPv4(X1)
| ~ ssPv2(X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f102,f43]) ).
fof(f341,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv4(skf2(X1))
| ~ ssPv2(skf2(X1))
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f102,f44]) ).
fof(f349,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv3(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f339,f43]) ).
fof(f354,plain,
! [X0,X1] :
( ssPv4(skf2(X1))
| ssPv3(skf2(X1))
| ssPv4(X1)
| ssPv4(X1)
| ssPv4(skf2(X1))
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f341,f126]) ).
fof(f356,plain,
! [X0,X1] :
( ssPv3(skf2(X1))
| ssPv4(X1)
| ssPv4(skf2(X1))
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f354]) ).
fof(f357,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[f356,f43]) ).
fof(f371,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f317,f180]) ).
fof(f380,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f371]) ).
fof(f388,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f380,f175]) ).
fof(f391,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f388]) ).
fof(f392,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f391,f195]) ).
fof(f413,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f137,f43]) ).
fof(f429,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[f144,f44]) ).
fof(f436,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv4(X1)
| ~ ssPv4(skf3(X1))
| ~ ssPv2(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f108,f43]) ).
fof(f438,plain,
! [X0,X1] :
( ssPv3(skf2(X1))
| ssPv4(skf2(X1))
| ~ ssPv4(X1)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f108,f44]) ).
fof(f442,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv1(skf3(X1))
| ~ ssPv2(skf3(X1))
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f110,f43]) ).
fof(f444,plain,
! [X0,X1] :
( ssPv2(skf2(X1))
| ssPv1(X1)
| ~ ssPv2(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,skf2(X1)) ),
inference(resolution,[status(thm)],[f110,f44]) ).
fof(f448,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f199,f429]) ).
fof(f462,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f448,f184]) ).
fof(f463,plain,
! [X0,X1] :
( ~ ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f462]) ).
fof(f464,plain,
! [X0,X1] :
( ~ ssRr(X1,X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f46]) ).
fof(f466,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f464,f43]) ).
fof(f468,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f127,f466]) ).
fof(f469,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f128,f466]) ).
fof(f474,plain,
! [X0] :
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f466,f215]) ).
fof(f480,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f474]) ).
fof(f483,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(skf3(skf2(X0)))
| ssPv3(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f148,f468]) ).
fof(f484,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf3(X0))
| ssPv3(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f147,f468]) ).
fof(f490,plain,
! [X0,X1] :
( ssPv2(skf3(X1))
| ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f112,f43]) ).
fof(f492,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv4(X0)
| ~ ssPv3(skf2(X1))
| ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f112,f44]) ).
fof(f497,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f429,f469]) ).
fof(f527,plain,
! [X0,X1] :
( ssPv2(skf3(X1))
| ssPv3(X1)
| ~ ssPv4(X1)
| ~ ssPv2(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f114,f43]) ).
fof(f533,plain,
! [X0,X1] :
( ssPv2(X1)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f116,f43]) ).
fof(f535,plain,
! [X0,X1] :
( ssPv2(skf2(X1))
| ~ ssPv1(X1)
| ~ ssPv3(skf2(X1))
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f116,f44]) ).
fof(f548,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f436,f43]) ).
fof(f570,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[f438,f43]) ).
fof(f579,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f570,f129]) ).
fof(f587,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f579]) ).
fof(f588,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f587,f166]) ).
fof(f621,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv2(X1)
| ssPv2(X1)
| ssPv1(skf3(X1))
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f442,f468]) ).
fof(f627,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv2(X1)
| ssPv1(skf3(X1))
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f621]) ).
fof(f630,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[f627,f43]) ).
fof(f634,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv2(skf2(X1))
| ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f118,f44]) ).
fof(f644,plain,
! [X0,X1] :
( ~ ssPv1(X1)
| ~ ssPv1(skf2(X1))
| ~ ssPv2(skf2(X1))
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f122,f44]) ).
fof(f657,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f444,f44]) ).
fof(f662,plain,
! [X0] :
( ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f657,f215]) ).
fof(f666,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f662]) ).
fof(f668,plain,
! [X0,X1] :
( ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f666,f210]) ).
fof(f669,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f666,f178]) ).
fof(f670,plain,
! [X0,X1] :
( ssPv3(X1)
| ~ ssPv3(X0)
| ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f668]) ).
fof(f671,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f669]) ).
fof(f672,plain,
! [X0] :
( ssPv1(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f132]) ).
fof(f699,plain,
! [X0] :
( ssPv3(skf3(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f670,f43]) ).
fof(f708,plain,
! [X0] :
( ssPv2(skf3(X0))
| ssPv4(skf3(skf3(X0)))
| ~ ssPv3(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f490,f43]) ).
fof(f729,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv3(X1)
| ssPv2(X1)
| ssPv4(X0)
| ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f492,f497]) ).
fof(f737,plain,
! [X0,X1] :
( ssPv3(X1)
| ssPv2(X1)
| ssPv4(X0)
| ~ ssPv4(skf2(X1))
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f729]) ).
fof(f748,plain,
! [X0] :
( ssPv2(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv2(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f527,f43]) ).
fof(f771,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[f154,f44]) ).
fof(f776,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv1(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f533,f43]) ).
fof(f777,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f776,f312]) ).
fof(f781,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f777]) ).
fof(f782,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv1(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f781,f466]) ).
fof(f785,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv2(X0)
| ~ ssPv1(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f185]) ).
fof(f807,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv4(skf2(X1))
| ~ ssPv1(X1)
| ssPv2(skf2(X1))
| ~ ssPv1(X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f535,f166]) ).
fof(f816,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv4(skf2(X1))
| ssPv2(skf2(X1))
| ~ ssPv1(X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f807]) ).
fof(f817,plain,
! [X0,X1] :
( ssPv4(X1)
| ssPv4(skf2(X1))
| ~ ssPv1(X1)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f816,f164]) ).
fof(f819,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[status(thm)],[f817,f43]) ).
fof(f822,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f819,f314]) ).
fof(f825,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f822]) ).
fof(f826,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f180]) ).
fof(f832,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f826,f178]) ).
fof(f834,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f832]) ).
fof(f835,plain,
! [X0] :
( ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv4(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f834,f466]) ).
fof(f902,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f161,f43]) ).
fof(f904,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv3(skf3(skf2(X0))) ),
inference(resolution,[status(thm)],[f168,f43]) ).
fof(f905,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f168,f44]) ).
fof(f942,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f169,f43]) ).
fof(f947,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f942,f484]) ).
fof(f948,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f942,f468]) ).
fof(f952,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv4(skf3(X0))
| ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f942,f466]) ).
fof(f953,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f947]) ).
fof(f954,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f948,f466]) ).
fof(f955,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f952]) ).
fof(f956,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f699,f953]) ).
fof(f960,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f953,f175]) ).
fof(f962,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f960]) ).
fof(f968,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f954,f175]) ).
fof(f970,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f968]) ).
fof(f971,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f970,f466]) ).
fof(f988,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f392,f971]) ).
fof(f1018,plain,
! [X0,X1] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f988,f737]) ).
fof(f1025,plain,
! [X0,X1] :
( ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv4(skf3(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1018]) ).
fof(f1028,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f171,f43]) ).
fof(f1030,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv4(X0)
| ~ ssPv1(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1028,f785]) ).
fof(f1032,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv3(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f174,f44]) ).
fof(f1038,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f1030,f133]) ).
fof(f1039,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1038,f956]) ).
fof(f1042,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1039,f223]) ).
fof(f1047,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1042]) ).
fof(f1051,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1047,f229]) ).
fof(f1057,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1051]) ).
fof(f1124,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv4(skf3(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f1025,f43]) ).
fof(f1126,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1124]) ).
fof(f1127,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f630,f1126]) ).
fof(f1130,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f1126,f225]) ).
fof(f1134,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1130,f835]) ).
fof(f1140,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f1127,f785]) ).
fof(f1141,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1140]) ).
fof(f1159,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv4(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f183,f43]) ).
fof(f1160,plain,
! [X0] :
( ssPv3(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f209,f43]) ).
fof(f1161,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f212,f43]) ).
fof(f1166,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1161,f484]) ).
fof(f1174,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv4(X0)
| ~ ssPv4(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1166,f1141]) ).
fof(f1176,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f953,f1177]) ).
fof(f1177,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1174,f413]) ).
fof(f1185,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1039,f1176]) ).
fof(f1190,plain,
! [X0] :
( ssPv1(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f1176,f131]) ).
fof(f1193,plain,
! [X0] :
( ssPv1(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1190]) ).
fof(f1194,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ~ ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[f1185,f349]) ).
fof(f1195,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1185,f357]) ).
fof(f1199,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1194,f902]) ).
fof(f1200,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1195,f166]) ).
fof(f1234,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1199,f1161]) ).
fof(f1236,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv4(skf2(X0))
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[f1234,f483]) ).
fof(f1241,plain,
! [X0] :
( ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1234,f145]) ).
fof(f1245,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1236,f466]) ).
fof(f1246,plain,
! [X0] :
( ssPv4(skf2(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1241]) ).
fof(f1248,plain,
! [X0,X1] :
( ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X0)
| ssPv3(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f1245,f535]) ).
fof(f1253,plain,
! [X0,X1] :
( ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1248,f1032]) ).
fof(f1255,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1246,f905]) ).
fof(f1263,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv3(X0)
| ssPv4(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1255]) ).
fof(f1274,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f588,f1275]) ).
fof(f1275,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1200,f480]) ).
fof(f1309,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv4(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f221,f43]) ).
fof(f1310,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f228,f43]) ).
fof(f1311,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(skf2(skf3(X0))) ),
inference(resolution,[status(thm)],[f228,f44]) ).
fof(f1315,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ssPv4(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1310,f1185]) ).
fof(f1321,plain,
! [X0] :
( ssPv1(X0)
| ssPv4(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1315]) ).
fof(f1360,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv1(skf3(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f1253,f43]) ).
fof(f1366,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f1360,f314]) ).
fof(f1371,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv2(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1366]) ).
fof(f1372,plain,
! [X0] :
( ssPv4(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1371,f180]) ).
fof(f1373,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1032,f1372]) ).
fof(f1381,plain,
! [X0] :
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f1372,f178]) ).
fof(f1385,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1381]) ).
fof(f1386,plain,
! [X0] :
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1385,f1134]) ).
fof(f1387,plain,
! [X0,X1] :
( ssPv4(X1)
| ~ ssPv1(X0)
| ~ ssPv4(skf2(X0))
| ~ ssRr(X1,X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1373,f634]) ).
fof(f1393,plain,
! [X0,X1] :
( ssPv4(X1)
| ~ ssPv4(skf2(X0))
| ~ ssRr(X1,X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1387]) ).
fof(f1394,plain,
! [X0,X1] :
( ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1393,f1372]) ).
fof(f1399,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1394,f43]) ).
fof(f1401,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f962,f1399]) ).
fof(f1450,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1057,f44]) ).
fof(f1451,plain,
! [X0] :
( ssPv4(X0)
| ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1450,f1263]) ).
fof(f1506,plain,
! [X0,X1] :
( ssPv3(X1)
| ~ ssPv1(X1)
| ~ ssPv1(X1)
| ~ ssPv1(skf2(X1))
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f644,f1373]) ).
fof(f1519,plain,
! [X0,X1] :
( ssPv3(X1)
| ~ ssPv1(X1)
| ~ ssPv1(skf2(X1))
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1506]) ).
fof(f1520,plain,
! [X0,X1] :
( ssPv3(X1)
| ~ ssPv1(X1)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1519,f1386]) ).
fof(f1525,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[f1520,f43]) ).
fof(f1526,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv1(skf2(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1520,f44]) ).
fof(f1528,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv3(skf2(X0))
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[f1525,f483]) ).
fof(f1530,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1525,f484]) ).
fof(f1531,plain,
! [X0] :
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[f1525,f468]) ).
fof(f1536,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf2(X0))
| ~ ssPv1(skf2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1528]) ).
fof(f1538,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1530]) ).
fof(f1539,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1538,f1176]) ).
fof(f1540,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1531]) ).
fof(f1567,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1526,f1386]) ).
fof(f1568,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv3(skf2(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1526,f672]) ).
fof(f1573,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1567,f1540]) ).
fof(f1574,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ssPv3(skf2(X0))
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1568]) ).
fof(f1588,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[f1536,f672]) ).
fof(f1593,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1588,f497]) ).
fof(f1599,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1574,f236]) ).
fof(f1605,plain,
! [X0,X1] :
( ~ ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1599]) ).
fof(f1606,plain,
! [X0,X1] :
( ~ ssPv3(X0)
| ~ ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1605,f1451]) ).
fof(f1618,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1593,f1573]) ).
fof(f1665,plain,
! [X0] :
( ~ ssPv3(X0)
| ~ ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1606,f43]) ).
fof(f1667,plain,
! [X0] :
( ~ ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1665,f1321]) ).
fof(f1772,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv3(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f357,f1775]) ).
fof(f1775,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv4(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f904,f1539]) ).
fof(f1789,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[f1772,f1539]) ).
fof(f1793,plain,
! [X0] :
( ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1789,f1618]) ).
fof(f1796,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(X0)
| ~ ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1263,f1793]) ).
fof(f1939,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f1159,f708]) ).
fof(f1946,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv2(skf3(X0))
| ~ ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1939]) ).
fof(f1947,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv2(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1946,f1401]) ).
fof(f1951,plain,
! [X0] :
( ssPv2(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f1947,f748]) ).
fof(f1952,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f1947,f548]) ).
fof(f1961,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ssPv1(skf3(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[f1947,f1667]) ).
fof(f1962,plain,
! [X0] :
( ssPv2(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv4(skf3(skf3(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1951,f1947]) ).
fof(f1963,plain,
! [X0] :
( ssPv3(X0)
| ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f1952]) ).
fof(f1982,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(skf3(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1962,f708]) ).
fof(f2025,plain,
! [X0] :
( ssPv4(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(skf3(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[f1961,f955]) ).
fof(f2027,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv4(X0)
| ssPv4(skf3(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2025]) ).
fof(f2039,plain,
! [X0] :
( ssPv3(skf3(skf3(X0)))
| ~ ssPv4(skf3(X0))
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1160,f1539]) ).
fof(f2090,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[status(thm)],[f1309,f1982]) ).
fof(f2099,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv1(X0)
| ~ ssPv1(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2090,f1947]) ).
fof(f2286,plain,
! [X0] :
( ssPv4(skf3(X0))
| ~ ssPv2(skf3(X0))
| ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f1311,f1796]) ).
fof(f2293,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2286]) ).
fof(f2299,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[f2293,f1947]) ).
fof(f2306,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2299]) ).
fof(f2307,plain,
! [X0] :
( ~ ssPv4(skf3(X0))
| ~ ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[f2306,f2039]) ).
fof(f2313,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0)))
| ~ ssPv2(skf3(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2307]) ).
fof(f2314,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2313,f1982]) ).
fof(f2317,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(skf3(X0))
| ssPv4(skf3(skf3(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1963,f2314]) ).
fof(f2330,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[f2317,f1309]) ).
fof(f2338,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv1(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(skf3(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2330]) ).
fof(f2339,plain,
! [X0] :
( ssPv1(X0)
| ssPv3(X0)
| ~ ssPv4(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2338,f1193]) ).
fof(f2349,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f2339,f1401]) ).
fof(f2352,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[f2339,f1126]) ).
fof(f2354,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv1(X0)
| ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2349]) ).
fof(f2355,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2352]) ).
fof(f2356,plain,
! [X0] :
( ssPv2(X0)
| ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2355,f1540]) ).
fof(f2374,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[f2356,f1234]) ).
fof(f2403,plain,
! [X0] :
( ssPv1(skf3(X0))
| ssPv1(X0)
| ~ ssPv4(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f131,f2354]) ).
fof(f2495,plain,
! [X0] :
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2027,f2403]) ).
fof(f2509,plain,
! [X0] :
( ssPv2(skf3(X0))
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2099,f2495]) ).
fof(f2522,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf3(X0))
| ~ ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f129,f2509]) ).
fof(f2532,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[f2509,f570]) ).
fof(f2537,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2532]) ).
fof(f2538,plain,
! [X0] :
( ssPv3(skf2(X0))
| ssPv4(skf2(X0))
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2537,f1274]) ).
fof(f2540,plain,
! [X0] :
( ssPv2(skf3(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[f2522,f748]) ).
fof(f2551,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv2(skf3(X0))
| ~ ssPv4(skf3(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2540]) ).
fof(f2552,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv2(skf3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2551,f1947]) ).
fof(f2562,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f2552,f1525]) ).
fof(f2571,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(X0)
| ~ ssPv4(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2562]) ).
fof(f2572,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2571,f2354]) ).
fof(f2577,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv3(skf2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1274,f2572]) ).
fof(f2636,plain,
! [X0] :
( ssPv3(skf2(X0))
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2538,f2572]) ).
fof(f2638,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssRr(X1,X0)
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f2636,f240]) ).
fof(f2641,plain,
! [X0,X1] :
( ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(X1,X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2638,f2572]) ).
fof(f2670,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[f2641,f43]) ).
fof(f2672,plain,
! [X0] :
( ssPv1(X0)
| ~ ssPv4(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2670,f2509]) ).
fof(f2683,plain,
! [X0] :
( ssPv2(X0)
| ssPv4(X0)
| ~ ssPv4(skf2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f771,f2672]) ).
fof(f2684,plain,
! [X0] :
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv4(skf2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f130,f2672]) ).
fof(f2706,plain,
! [X0] :
( ssPv4(skf2(X0))
| ssPv2(X0)
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[f2683,f146]) ).
fof(f2711,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2706]) ).
fof(f2712,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2711,f2356]) ).
fof(f2746,plain,
! [X0] :
( ssPv2(skf2(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f223,f2748]) ).
fof(f2748,plain,
! [X0] :
( ssPv2(X0)
| ssPv2(skf2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2712,f2684]) ).
fof(f2756,plain,
! [X0,X1] :
( ssPv4(X0)
| ssPv4(skf2(X0))
| ~ ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f2748,f341]) ).
fof(f2760,plain,
! [X0] :
( ~ ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f2748,f1667]) ).
fof(f2763,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2756,f2683]) ).
fof(f2787,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv2(X0)
| ssPv2(skf2(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f2746,f2374]) ).
fof(f2791,plain,
! [X0] :
( ssPv4(X0)
| ssPv2(skf2(X0))
| ~ ssPv3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2787,f2748]) ).
fof(f2792,plain,
! [X0,X1] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f229,f2791]) ).
fof(f2838,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(skf3(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f2763,f43]) ).
fof(f2852,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv1(skf2(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f2760,f2577]) ).
fof(f2856,plain,
! [X0,X1] :
( ~ ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv2(X1)
| ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f2852,f644]) ).
fof(f2858,plain,
! [X0,X1] :
( ~ ssPv2(skf2(X0))
| ~ ssPv2(X1)
| ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2856]) ).
fof(f2859,plain,
! [X0,X1] :
( ~ ssPv2(X1)
| ~ ssRr(X1,X0)
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2858,f2748]) ).
fof(f2921,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[f2792,f44]) ).
fof(f2926,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[f2921,f2577]) ).
fof(f2980,plain,
! [X0] :
( ~ ssPv2(skf3(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f2859,f43]) ).
fof(f3011,plain,
! [X0] :
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f2980,f2522]) ).
fof(f3015,plain,
! [X0] :
( ~ ssPv4(X0)
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3011]) ).
fof(f3016,plain,
! [X0] :
( ~ ssPv4(X0)
| ssPv2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3015,f2672]) ).
fof(f3028,plain,
! [X0] :
( ~ ssPv3(skf3(X0))
| ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2838,f3016]) ).
fof(f3029,plain,
! [X0,X1] :
( ~ ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2763,f3016]) ).
fof(f3041,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0)
| ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[f3016,f1399]) ).
fof(f3042,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3041,f1525]) ).
fof(f3050,plain,
! [X0] :
( ssPv3(X0)
| ~ ssPv4(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2339,f3042]) ).
fof(f3051,plain,
! [X0] :
( ~ ssPv1(X0)
| ssPv4(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2926,f3042]) ).
fof(f3120,plain,
! [X0,X1,X2,X3] :
( ssPv2(X3)
| ssPv4(X2)
| ssPv1(X0)
| ~ ssRr(X1,X3)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f94,f3029]) ).
fof(f3212,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv4(X1)
| ssPv1(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(resolution,[status(thm)],[f3120,f43]) ).
fof(f3218,plain,
! [X0,X1] :
( ssPv2(X1)
| ssPv1(X0)
| ~ ssRr(X0,skf3(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3212,f3016]) ).
fof(f3220,plain,
! [X0] :
( ssPv2(X0)
| ssPv1(skf3(skf3(X0))) ),
inference(resolution,[status(thm)],[f3218,f43]) ).
fof(f3221,plain,
! [X0] :
( ssPv4(skf3(skf3(X0)))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f3220,f3051]) ).
fof(f3225,plain,
! [X0] :
( ssPv3(skf3(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[f3221,f3050]) ).
fof(f3229,plain,
! [X0] : ssPv2(X0),
inference(forward_subsumption_resolution,[status(thm)],[f3225,f3028]) ).
fof(f3237,plain,
! [X0] :
( ssPv4(X0)
| ~ ssPv2(skf3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1234,f3229]) ).
fof(f3239,plain,
! [X0,X1,X2,X3] :
( ~ ssPv1(X1)
| ~ ssPv3(X3)
| ~ ssRr(X1,X3)
| ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f124,f3229]) ).
fof(f3247,plain,
! [X0] : ssPv4(X0),
inference(forward_subsumption_resolution,[status(thm)],[f3237,f3229]) ).
fof(f3260,plain,
! [X0] : ssPv3(X0),
inference(backward_subsumption_resolution,[status(thm)],[f3050,f3247]) ).
fof(f3261,plain,
! [X0] : ssPv1(X0),
inference(backward_subsumption_resolution,[status(thm)],[f2672,f3247]) ).
fof(f3273,plain,
! [X0,X1,X2,X3] :
( ~ ssPv1(X1)
| ~ ssPv3(X3)
| ~ ssRr(X1,X3)
| ~ ssRr(X2,X1)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f3239,f3247]) ).
fof(f3274,plain,
! [X0,X1,X2] :
( ~ ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[f3273,f43]) ).
fof(f3278,plain,
! [X0,X1,X2] :
( ~ ssPv1(X1)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f3274,f3260]) ).
fof(f3282,plain,
! [X0,X1,X2] :
( ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f3278,f3261]) ).
fof(f3284,plain,
! [X0,X1] : ~ ssRr(X0,X1),
inference(resolution,[status(thm)],[f3282,f44]) ).
fof(f3286,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f43,f3284]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN784-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 11:16:05 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 7.78/1.39 % Refutation found
% 7.78/1.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 7.78/1.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.38/1.42 % Elapsed time: 1.046756 seconds
% 6.38/1.42 % CPU time: 8.008449 seconds
% 6.38/1.42 % Total memory used: 50.330 MB
% 6.38/1.42 % Net memory used: 39.535 MB
%------------------------------------------------------------------------------