%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS008-1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 01:00:04 PM UTC 2026
% Result : Satisfiable 0.72s 0.52s
% Output : Saturation 0.72s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
e(exist),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ f(exist),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X1] :
( ~ c(X1)
| s2least(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X1] :
( ~ s2least(X1)
| c(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X1] :
( ~ equalish(u1r2(X1),u1r1(X1))
| ~ s2least(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X1] :
( ~ s2least(X1)
| s(X1,u1r1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X1] :
( ~ s2least(X1)
| s(X1,u1r2(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X1,X3,X2] :
( ~ s(X1,X2)
| ~ s(X1,X3)
| equalish(X3,X2)
| s2least(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X1] :
( ~ d(X1)
| s1most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X1] :
( ~ s1most(X1)
| d(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X3,X2,X1] :
( ~ s(X1,X2)
| ~ s(X1,X3)
| ~ s1most(X1)
| equalish(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X1] :
( ~ equalish(u3r2(X1),u3r1(X1))
| s1most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X1] :
( s(X1,u3r1(X1))
| s1most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X1] :
( s(X1,u3r2(X1))
| s1most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X1] :
( ~ e(X1)
| d(u4r2(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X1] :
( ~ e(X1)
| r(X1,u4r2(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X1] :
( ~ e(X1)
| c(u4r1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X1] :
( ~ e(X1)
| r(X1,u4r1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X1] :
( ~ e(X1)
| r2most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X1,X2,X3] :
( ~ d(X3)
| ~ r(X1,X3)
| ~ c(X2)
| ~ r(X1,X2)
| ~ r2most(X1)
| e(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X4,X3,X2,X1] :
( ~ r(X1,X2)
| ~ r(X1,X3)
| ~ r(X1,X4)
| ~ r2most(X1)
| equalish(X3,X2)
| equalish(X4,X2)
| equalish(X4,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X1] :
( ~ equalish(u5r2(X1),u5r1(X1))
| r2most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X1] :
( ~ equalish(u5r3(X1),u5r1(X1))
| r2most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X1] :
( ~ equalish(u5r3(X1),u5r2(X1))
| r2most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X1] :
( r(X1,u5r1(X1))
| r2most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X1] :
( r(X1,u5r2(X1))
| r2most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X1] :
( r(X1,u5r3(X1))
| r2most(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X5,X4,X1] :
( ~ d(X4)
| ~ d(X5)
| ~ r(X1,X4)
| ~ r(X1,X5)
| ~ f(X1)
| equalish(X5,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X3,X2,X1] :
( ~ c(X2)
| ~ c(X3)
| ~ r(X1,X2)
| ~ r(X1,X3)
| ~ f(X1)
| equalish(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X1] :
( ~ equalish(u6r4(X1),u6r3(X1))
| ~ equalish(u6r2(X1),u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X1] :
( ~ equalish(u6r2(X1),u6r1(X1))
| d(u6r3(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X1] :
( ~ equalish(u6r2(X1),u6r1(X1))
| d(u6r4(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X1] :
( ~ equalish(u6r2(X1),u6r1(X1))
| r(X1,u6r3(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X1] :
( ~ equalish(u6r2(X1),u6r1(X1))
| r(X1,u6r4(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X1] :
( ~ equalish(u6r4(X1),u6r3(X1))
| c(u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X1] :
( d(u6r3(X1))
| c(u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X1] :
( d(u6r4(X1))
| c(u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [X1] :
( r(X1,u6r3(X1))
| c(u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X1] :
( r(X1,u6r4(X1))
| c(u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X1] :
( ~ equalish(u6r4(X1),u6r3(X1))
| c(u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X1] :
( d(u6r3(X1))
| c(u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [X1] :
( d(u6r4(X1))
| c(u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X1] :
( r(X1,u6r3(X1))
| c(u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X1] :
( r(X1,u6r4(X1))
| c(u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X1] :
( ~ equalish(u6r4(X1),u6r3(X1))
| r(X1,u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X1] :
( d(u6r3(X1))
| r(X1,u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X1] :
( d(u6r4(X1))
| r(X1,u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X1] :
( r(X1,u6r3(X1))
| r(X1,u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X1] :
( r(X1,u6r4(X1))
| r(X1,u6r1(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X1] :
( ~ equalish(u6r4(X1),u6r3(X1))
| r(X1,u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [X1] :
( d(u6r3(X1))
| r(X1,u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X1] :
( d(u6r4(X1))
| r(X1,u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X1] :
( r(X1,u6r3(X1))
| r(X1,u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X1] :
( r(X1,u6r4(X1))
| r(X1,u6r2(X1))
| f(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,plain,
e(exist),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f56,plain,
~ f(exist),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f57,plain,
! [X0] :
( ~ c(X0)
| s2least(X0) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f58,plain,
! [X0] :
( ~ s2least(X0)
| c(X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f59,plain,
! [X0] :
( ~ equalish(u1r2(X0),u1r1(X0))
| ~ s2least(X0) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f60,plain,
! [X0] :
( ~ s2least(X0)
| s(X0,u1r1(X0)) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f61,plain,
! [X0] :
( ~ s2least(X0)
| s(X0,u1r2(X0)) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f62,plain,
! [X1,X2] :
( ~ s(X1,X2)
| ! [X3] :
( ~ s(X1,X3)
| equalish(X3,X2)
| s2least(X1) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ s(X0,X2)
| ~ s(X0,X1)
| equalish(X1,X2)
| s2least(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [X0] :
( ~ d(X0)
| s1most(X0) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f65,plain,
! [X0] :
( ~ s1most(X0)
| d(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f66,plain,
! [X2,X1] :
( ~ s(X1,X2)
| ! [X3] :
( ~ s(X1,X3)
| ~ s1most(X1)
| equalish(X3,X2) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f67,plain,
! [X0,X1,X2] :
( ~ s(X2,X1)
| ~ s(X2,X0)
| ~ s1most(X2)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [X0] :
( ~ equalish(u3r2(X0),u3r1(X0))
| s1most(X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f69,plain,
! [X0] :
( s(X0,u3r1(X0))
| s1most(X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f70,plain,
! [X0] :
( s(X0,u3r2(X0))
| s1most(X0) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f71,plain,
! [X0] :
( ~ e(X0)
| d(u4r2(X0)) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f72,plain,
! [X0] :
( ~ e(X0)
| r(X0,u4r2(X0)) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f73,plain,
! [X0] :
( ~ e(X0)
| c(u4r1(X0)) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f74,plain,
! [X0] :
( ~ e(X0)
| r(X0,u4r1(X0)) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f75,plain,
! [X0] :
( ~ e(X0)
| r2most(X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f76,plain,
! [X3] :
( ~ d(X3)
| ! [X1] :
( ~ r(X1,X3)
| ! [X2] :
( ~ c(X2)
| ~ r(X1,X2)
| ~ r2most(X1)
| e(X1) ) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ d(X2)
| ~ r(X0,X2)
| ~ c(X1)
| ~ r(X0,X1)
| ~ r2most(X0)
| e(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [X2,X1] :
( ~ r(X1,X2)
| ! [X3] :
( ~ r(X1,X3)
| ! [X4] :
( ~ r(X1,X4)
| ~ r2most(X1)
| equalish(X3,X2)
| equalish(X4,X2)
| equalish(X4,X3) ) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f79,plain,
! [X0,X1,X2,X3] :
( ~ r(X3,X2)
| ~ r(X3,X1)
| ~ r(X3,X0)
| ~ r2most(X3)
| equalish(X1,X2)
| equalish(X0,X2)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f80,plain,
! [X0] :
( ~ equalish(u5r2(X0),u5r1(X0))
| r2most(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f81,plain,
! [X0] :
( ~ equalish(u5r3(X0),u5r1(X0))
| r2most(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f82,plain,
! [X0] :
( ~ equalish(u5r3(X0),u5r2(X0))
| r2most(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f83,plain,
! [X0] :
( r(X0,u5r1(X0))
| r2most(X0) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f84,plain,
! [X0] :
( r(X0,u5r2(X0))
| r2most(X0) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f85,plain,
! [X0] :
( r(X0,u5r3(X0))
| r2most(X0) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f86,plain,
! [X4] :
( ~ d(X4)
| ! [X5] :
( ~ d(X5)
| ! [X1] :
( ~ r(X1,X4)
| ~ r(X1,X5)
| ~ f(X1)
| equalish(X5,X4) ) ) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f87,plain,
! [X0,X1,X2] :
( ~ d(X1)
| ~ d(X0)
| ~ r(X2,X1)
| ~ r(X2,X0)
| ~ f(X2)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f88,plain,
! [X2] :
( ~ c(X2)
| ! [X3] :
( ~ c(X3)
| ! [X1] :
( ~ r(X1,X2)
| ~ r(X1,X3)
| ~ f(X1)
| equalish(X3,X2) ) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f89,plain,
! [X0,X1,X2] :
( ~ c(X1)
| ~ c(X0)
| ~ r(X2,X1)
| ~ r(X2,X0)
| ~ f(X2)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [X0] :
( ~ equalish(u6r4(X0),u6r3(X0))
| ~ equalish(u6r2(X0),u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f91,plain,
! [X0] :
( ~ equalish(u6r2(X0),u6r1(X0))
| d(u6r3(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f92,plain,
! [X0] :
( ~ equalish(u6r2(X0),u6r1(X0))
| d(u6r4(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f93,plain,
! [X0] :
( ~ equalish(u6r2(X0),u6r1(X0))
| r(X0,u6r3(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f94,plain,
! [X0] :
( ~ equalish(u6r2(X0),u6r1(X0))
| r(X0,u6r4(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f95,plain,
! [X0] :
( ~ equalish(u6r4(X0),u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f96,plain,
! [X0] :
( d(u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f97,plain,
! [X0] :
( d(u6r4(X0))
| c(u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f98,plain,
! [X0] :
( r(X0,u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f99,plain,
! [X0] :
( r(X0,u6r4(X0))
| c(u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f100,plain,
! [X0] :
( ~ equalish(u6r4(X0),u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f101,plain,
! [X0] :
( d(u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f102,plain,
! [X0] :
( d(u6r4(X0))
| c(u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f103,plain,
! [X0] :
( r(X0,u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f104,plain,
! [X0] :
( r(X0,u6r4(X0))
| c(u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f105,plain,
! [X0] :
( ~ equalish(u6r4(X0),u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f106,plain,
! [X0] :
( d(u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f107,plain,
! [X0] :
( d(u6r4(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f108,plain,
! [X0] :
( r(X0,u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f109,plain,
! [X0] :
( r(X0,u6r4(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f110,plain,
! [X0] :
( ~ equalish(u6r4(X0),u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f111,plain,
! [X0] :
( d(u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f112,plain,
! [X0] :
( d(u6r4(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f113,plain,
! [X0] :
( r(X0,u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f114,plain,
! [X0] :
( r(X0,u6r4(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f115,plain,
r2most(exist),
inference(resolution,[status(thm)],[f75,f55]) ).
fof(f116,plain,
d(u4r2(exist)),
inference(resolution,[status(thm)],[f71,f55]) ).
fof(f117,plain,
r(exist,u4r2(exist)),
inference(resolution,[status(thm)],[f72,f55]) ).
fof(f118,plain,
c(u4r1(exist)),
inference(resolution,[status(thm)],[f73,f55]) ).
fof(f119,plain,
r(exist,u4r1(exist)),
inference(resolution,[status(thm)],[f74,f55]) ).
fof(f124,plain,
! [X0,X1] :
( s1most(X0)
| ~ s(X0,X1)
| equalish(u3r2(X0),X1)
| s2least(X0) ),
inference(resolution,[status(thm)],[f63,f70]) ).
fof(f130,plain,
! [X0] :
( s1most(u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f96,f64]) ).
fof(f131,plain,
! [X0] :
( s1most(u6r4(X0))
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f97,f64]) ).
fof(f132,plain,
! [X0] :
( s1most(u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f101,f64]) ).
fof(f133,plain,
! [X0] :
( s1most(u6r4(X0))
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f102,f64]) ).
fof(f138,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r3(X0),X2)
| equalish(u6r3(X0),X1)
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f98,f79]) ).
fof(f139,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r3(X0))
| ~ r2most(X0)
| e(X0)
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f98,f77]) ).
fof(f140,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r4(X0),X2)
| equalish(u6r4(X0),X1)
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f99,f79]) ).
fof(f141,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r4(X0))
| ~ r2most(X0)
| e(X0)
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f99,f77]) ).
fof(f142,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r3(X0),X2)
| equalish(u6r3(X0),X1)
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f103,f79]) ).
fof(f143,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r3(X0))
| ~ r2most(X0)
| e(X0)
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f103,f77]) ).
fof(f144,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r4(X0),X2)
| equalish(u6r4(X0),X1)
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f104,f79]) ).
fof(f145,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r4(X0))
| ~ r2most(X0)
| e(X0)
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f104,f77]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r1(X0),X2)
| equalish(u6r1(X0),X1)
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f106,f79]) ).
fof(f147,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r1(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f106,f77]) ).
fof(f148,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f147,f96]) ).
fof(f149,plain,
! [X0] :
( d(u6r3(X0))
| f(X0)
| ~ d(u6r1(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f148,f106]) ).
fof(f157,plain,
! [X0] :
( ~ d(u6r1(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f149]) ).
fof(f161,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r1(X0),X2)
| equalish(u6r1(X0),X1)
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f107,f79]) ).
fof(f162,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r1(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f107,f77]) ).
fof(f164,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f162,f97]) ).
fof(f165,plain,
! [X0] :
( d(u6r4(X0))
| f(X0)
| ~ d(u6r1(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f164,f107]) ).
fof(f174,plain,
! [X0] :
( ~ d(u6r1(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f165]) ).
fof(f179,plain,
! [X0] :
( ~ d(u6r2(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0)
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f111,f148]) ).
fof(f180,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r2(X0),X2)
| equalish(u6r2(X0),X1)
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f111,f79]) ).
fof(f183,plain,
! [X0] :
( ~ d(u6r2(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f179]) ).
fof(f184,plain,
! [X0] :
( ~ d(u6r2(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0)
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f112,f164]) ).
fof(f186,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r2(X0),X2)
| equalish(u6r2(X0),X1)
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f112,f79]) ).
fof(f188,plain,
! [X0] :
( ~ d(u6r2(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f184]) ).
fof(f192,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r3(X0),X2)
| equalish(u6r3(X0),X1)
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f108,f79]) ).
fof(f193,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r3(X0))
| ~ r2most(X0)
| e(X0)
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f108,f77]) ).
fof(f197,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r4(X0),X2)
| equalish(u6r4(X0),X1)
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f109,f79]) ).
fof(f198,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r4(X0))
| ~ r2most(X0)
| e(X0)
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f109,f77]) ).
fof(f202,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r3(X0),X2)
| equalish(u6r3(X0),X1)
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f113,f79]) ).
fof(f203,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r3(X0))
| ~ r2most(X0)
| e(X0)
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f113,f77]) ).
fof(f207,plain,
! [X0,X1,X2] :
( ~ r(X0,X2)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(X1,X2)
| equalish(u6r4(X0),X2)
| equalish(u6r4(X0),X1)
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f114,f79]) ).
fof(f208,plain,
! [X0,X1] :
( ~ d(X1)
| ~ r(X0,X1)
| ~ c(u6r4(X0))
| ~ r2most(X0)
| e(X0)
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f114,f77]) ).
fof(f211,plain,
! [X0] :
( s1most(X0)
| s1most(X0)
| equalish(u3r2(X0),u3r1(X0))
| s2least(X0) ),
inference(resolution,[status(thm)],[f124,f69]) ).
fof(f213,plain,
! [X0] :
( s1most(X0)
| equalish(u3r2(X0),u3r1(X0))
| s2least(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f211]) ).
fof(f214,plain,
! [X0] :
( s1most(X0)
| s2least(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f213,f68]) ).
fof(f215,plain,
! [X0] :
( d(X0)
| s2least(X0) ),
inference(resolution,[status(thm)],[f214,f65]) ).
fof(f216,plain,
! [X0] :
( ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0)
| s2least(u6r1(X0)) ),
inference(resolution,[status(thm)],[f215,f174]) ).
fof(f217,plain,
! [X0] :
( ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0)
| s2least(u6r1(X0)) ),
inference(resolution,[status(thm)],[f215,f157]) ).
fof(f230,plain,
! [X0,X1] :
( c(u6r1(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f138,f98]) ).
fof(f245,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f230]) ).
fof(f253,plain,
! [X0,X1] :
( c(u6r1(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f140,f99]) ).
fof(f257,plain,
! [X0,X1] :
( c(u6r1(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f140,f98]) ).
fof(f268,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| c(u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f253]) ).
fof(f275,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f257]) ).
fof(f276,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| c(u6r1(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f275,f95]) ).
fof(f287,plain,
! [X0,X1] :
( c(u6r2(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f142,f103]) ).
fof(f302,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f287]) ).
fof(f310,plain,
! [X0,X1] :
( c(u6r2(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f144,f104]) ).
fof(f314,plain,
! [X0,X1] :
( c(u6r2(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f144,f103]) ).
fof(f325,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| c(u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f310]) ).
fof(f331,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f314]) ).
fof(f332,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| c(u6r2(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f331,f100]) ).
fof(f338,plain,
! [X0,X1] :
( d(u6r3(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r1(X0),X1)
| equalish(u6r1(X0),u6r1(X0))
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f146,f106]) ).
fof(f353,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r1(X0),u6r1(X0))
| d(u6r3(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f338]) ).
fof(f364,plain,
! [X0,X1] :
( d(u6r4(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r1(X0),X1)
| equalish(u6r1(X0),u6r1(X0))
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f161,f107]) ).
fof(f379,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r1(X0),u6r1(X0))
| d(u6r4(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f364]) ).
fof(f390,plain,
! [X0,X1] :
( d(u6r3(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r2(X0))
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f180,f111]) ).
fof(f392,plain,
! [X0,X1] :
( d(u6r3(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r1(X0))
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f180,f106]) ).
fof(f405,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r2(X0))
| d(u6r3(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f390]) ).
fof(f408,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r1(X0))
| d(u6r3(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f392]) ).
fof(f409,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r2(X0),X1)
| d(u6r3(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f91]) ).
fof(f418,plain,
! [X0,X1] :
( d(u6r4(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r2(X0))
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f186,f112]) ).
fof(f420,plain,
! [X0,X1] :
( d(u6r4(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r1(X0))
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f186,f107]) ).
fof(f433,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r2(X0))
| d(u6r4(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f418]) ).
fof(f435,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r2(X0),X1)
| equalish(u6r2(X0),u6r1(X0))
| d(u6r4(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f420]) ).
fof(f436,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r1(X0),X1)
| equalish(u6r2(X0),X1)
| d(u6r4(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f435,f92]) ).
fof(f456,plain,
! [X0,X1] :
( r(X0,u6r1(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f192,f108]) ).
fof(f471,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f456]) ).
fof(f479,plain,
! [X0,X1] :
( r(X0,u6r1(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f197,f109]) ).
fof(f483,plain,
! [X0,X1] :
( r(X0,u6r1(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f197,f108]) ).
fof(f494,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f479]) ).
fof(f499,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f483]) ).
fof(f500,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| r(X0,u6r1(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f499,f105]) ).
fof(f513,plain,
! [X0,X1] :
( r(X0,u6r2(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f202,f113]) ).
fof(f528,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f513]) ).
fof(f536,plain,
! [X0,X1] :
( r(X0,u6r2(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f207,f114]) ).
fof(f540,plain,
! [X0,X1] :
( r(X0,u6r2(X0))
| f(X0)
| ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f207,f113]) ).
fof(f551,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f536]) ).
fof(f555,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| equalish(u6r4(X0),u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f540]) ).
fof(f556,plain,
! [X0,X1] :
( ~ r(X0,X1)
| ~ r2most(X0)
| equalish(u6r3(X0),X1)
| equalish(u6r4(X0),X1)
| r(X0,u6r2(X0))
| f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f110]) ).
fof(f564,plain,
! [X0] :
( s2least(u6r2(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f183,f215]) ).
fof(f565,plain,
! [X0] :
( s2least(u6r2(X0))
| ~ r2most(X0)
| e(X0)
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f188,f215]) ).
fof(f690,plain,
s1most(u4r2(exist)),
inference(resolution,[status(thm)],[f116,f64]) ).
fof(f692,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r2(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f207]) ).
fof(f693,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r2(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f202]) ).
fof(f694,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r2(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f197]) ).
fof(f695,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r2(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f192]) ).
fof(f696,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u4r2(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f186]) ).
fof(f697,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u4r2(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f180]) ).
fof(f698,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r1(exist),X0)
| equalish(u6r1(exist),u4r2(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f161]) ).
fof(f699,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r1(exist),X0)
| equalish(u6r1(exist),u4r2(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f146]) ).
fof(f700,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r2(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f144]) ).
fof(f701,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r2(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f142]) ).
fof(f702,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r2(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f140]) ).
fof(f703,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r2(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r2(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f138]) ).
fof(f704,plain,
( ~ d(u4r2(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f164]) ).
fof(f705,plain,
( ~ d(u4r2(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f117,f148]) ).
fof(f706,plain,
! [X0,X1] :
( ~ r(exist,X1)
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(X0,X1)
| equalish(u4r2(exist),X1)
| equalish(u4r2(exist),X0) ),
inference(resolution,[status(thm)],[f117,f79]) ).
fof(f707,plain,
! [X0] :
( ~ d(X0)
| ~ r(exist,X0)
| ~ c(u4r2(exist))
| ~ r2most(exist)
| e(exist) ),
inference(resolution,[status(thm)],[f117,f77]) ).
fof(f708,definition,
( sQ0_spl
<=> f(exist) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( ~ sQ0_spl
| f(exist) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,definition,
( sQ1_spl
<=> c(u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( ~ sQ1_spl
| c(u6r1(exist)) ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,definition,
( sQ2_spl
<=> equalish(u6r3(exist),u6r4(exist)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f715,plain,
( ~ sQ2_spl
| equalish(u6r3(exist),u6r4(exist)) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f717,definition,
( sQ3_spl
<=> equalish(u6r3(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f718,plain,
( ~ sQ3_spl
| equalish(u6r3(exist),u4r2(exist)) ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f720,definition,
( sQ4_spl
<=> equalish(u6r4(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f721,plain,
( ~ sQ4_spl
| equalish(u6r4(exist),u4r2(exist)) ),
inference(component_clause,[status(thm)],[f720]) ).
fof(f723,definition,
( sQ5_spl
<=> r2most(exist) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f725,plain,
( sQ5_spl
| ~ r2most(exist) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f727,definition,
( sQ6_spl
<=> r(exist,u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f728,plain,
( ~ sQ6_spl
| r(exist,u6r2(exist)) ),
inference(component_clause,[status(thm)],[f727]) ).
fof(f729,plain,
( sQ6_spl
| ~ r(exist,u6r2(exist)) ),
inference(component_clause,[status(thm)],[f727]) ).
fof(f730,definition,
! [X0] :
( sQ7_spl
<=> ( ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u6r4(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f731,plain,
! [X0] :
( ~ sQ7_spl
| ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u6r4(exist),X0) ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f733,plain,
( ~ sQ5_spl
| sQ7_spl
| sQ4_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f692,f708,f727,f720,f730,f723]) ).
fof(f734,definition,
! [X0] :
( sQ8_spl
<=> ( ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u6r3(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f735,plain,
! [X0] :
( ~ sQ8_spl
| ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u6r3(exist),X0) ),
inference(component_clause,[status(thm)],[f734]) ).
fof(f737,plain,
( ~ sQ5_spl
| sQ8_spl
| sQ3_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f693,f708,f727,f717,f734,f723]) ).
fof(f738,definition,
( sQ9_spl
<=> r(exist,u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f739,plain,
( ~ sQ9_spl
| r(exist,u6r1(exist)) ),
inference(component_clause,[status(thm)],[f738]) ).
fof(f740,plain,
( sQ9_spl
| ~ r(exist,u6r1(exist)) ),
inference(component_clause,[status(thm)],[f738]) ).
fof(f741,plain,
( ~ sQ5_spl
| sQ7_spl
| sQ4_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f694,f708,f738,f720,f730,f723]) ).
fof(f742,plain,
( ~ sQ5_spl
| sQ8_spl
| sQ3_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f695,f708,f738,f717,f734,f723]) ).
fof(f743,definition,
( sQ10_spl
<=> d(u6r4(exist)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f744,plain,
( ~ sQ10_spl
| d(u6r4(exist)) ),
inference(component_clause,[status(thm)],[f743]) ).
fof(f746,definition,
( sQ11_spl
<=> equalish(u6r2(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f747,plain,
( ~ sQ11_spl
| equalish(u6r2(exist),u4r2(exist)) ),
inference(component_clause,[status(thm)],[f746]) ).
fof(f749,definition,
! [X0] :
( sQ12_spl
<=> ( ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f752,plain,
( ~ sQ5_spl
| sQ12_spl
| sQ11_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f696,f708,f743,f746,f749,f723]) ).
fof(f753,definition,
( sQ13_spl
<=> d(u6r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f754,plain,
( ~ sQ13_spl
| d(u6r3(exist)) ),
inference(component_clause,[status(thm)],[f753]) ).
fof(f756,plain,
( ~ sQ5_spl
| sQ12_spl
| sQ11_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f697,f708,f753,f746,f749,f723]) ).
fof(f757,definition,
( sQ14_spl
<=> equalish(u6r1(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( ~ sQ14_spl
| equalish(u6r1(exist),u4r2(exist)) ),
inference(component_clause,[status(thm)],[f757]) ).
fof(f760,definition,
! [X0] :
( sQ15_spl
<=> ( ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u6r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( ~ sQ5_spl
| sQ15_spl
| sQ14_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f698,f708,f743,f757,f760,f723]) ).
fof(f764,plain,
( ~ sQ5_spl
| sQ15_spl
| sQ14_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f699,f708,f753,f757,f760,f723]) ).
fof(f765,definition,
( sQ16_spl
<=> c(u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f766,plain,
( ~ sQ16_spl
| c(u6r2(exist)) ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f768,plain,
( ~ sQ5_spl
| sQ7_spl
| sQ4_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f700,f708,f765,f720,f730,f723]) ).
fof(f769,plain,
( ~ sQ5_spl
| sQ8_spl
| sQ3_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f701,f708,f765,f717,f734,f723]) ).
fof(f770,plain,
( ~ sQ5_spl
| sQ7_spl
| sQ4_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f702,f708,f711,f720,f730,f723]) ).
fof(f771,plain,
( ~ sQ5_spl
| sQ8_spl
| sQ3_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f703,f708,f711,f717,f734,f723]) ).
fof(f772,definition,
( sQ17_spl
<=> e(exist) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f775,definition,
( sQ18_spl
<=> d(u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f778,plain,
( ~ sQ18_spl
| ~ sQ5_spl
| sQ17_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f704,f708,f743,f772,f723,f775]) ).
fof(f779,plain,
( ~ sQ18_spl
| ~ sQ5_spl
| sQ17_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f705,f708,f753,f772,f723,f775]) ).
fof(f780,definition,
! [X0,X1] :
( sQ19_spl
<=> ( ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u4r2(exist),X1)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f781,plain,
! [X0,X1] :
( ~ sQ19_spl
| ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u4r2(exist),X1)
| equalish(u4r2(exist),X0) ),
inference(component_clause,[status(thm)],[f780]) ).
fof(f783,plain,
( ~ sQ5_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f706,f780,f723]) ).
fof(f784,definition,
( sQ20_spl
<=> c(u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f787,definition,
! [X0] :
( sQ21_spl
<=> ( ~ d(X0)
| ~ r(exist,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( sQ21_spl
| ~ sQ20_spl
| ~ sQ5_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f707,f772,f723,f784,f787]) ).
fof(f791,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f725,f115]) ).
fof(f792,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f791]) ).
fof(f793,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f56]) ).
fof(f794,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f793]) ).
fof(f795,plain,
s2least(u4r1(exist)),
inference(resolution,[status(thm)],[f118,f57]) ).
fof(f797,plain,
( ~ sQ13_spl
| s1most(u6r3(exist)) ),
inference(resolution,[status(thm)],[f754,f64]) ).
fof(f799,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r1(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f207]) ).
fof(f800,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r1(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f202]) ).
fof(f801,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r1(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f197]) ).
fof(f802,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r1(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f192]) ).
fof(f803,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u4r1(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f186]) ).
fof(f804,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u4r1(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f180]) ).
fof(f805,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r1(exist),X0)
| equalish(u6r1(exist),u4r1(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f161]) ).
fof(f806,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r1(exist),X0)
| equalish(u6r1(exist),u4r1(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f146]) ).
fof(f807,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r1(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f144]) ).
fof(f808,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r1(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f142]) ).
fof(f809,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u4r1(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f140]) ).
fof(f810,plain,
! [X0] :
( ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u4r1(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u4r1(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f138]) ).
fof(f811,plain,
( ~ d(u4r1(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f164]) ).
fof(f812,plain,
( ~ d(u4r1(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f119,f148]) ).
fof(f813,plain,
! [X0,X1] :
( ~ r(exist,X1)
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(X0,X1)
| equalish(u4r1(exist),X1)
| equalish(u4r1(exist),X0) ),
inference(resolution,[status(thm)],[f119,f79]) ).
fof(f814,plain,
! [X0] :
( ~ d(X0)
| ~ r(exist,X0)
| ~ c(u4r1(exist))
| ~ r2most(exist)
| e(exist) ),
inference(resolution,[status(thm)],[f119,f77]) ).
fof(f815,definition,
( sQ22_spl
<=> equalish(u6r3(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f816,plain,
( ~ sQ22_spl
| equalish(u6r3(exist),u4r1(exist)) ),
inference(component_clause,[status(thm)],[f815]) ).
fof(f818,definition,
( sQ23_spl
<=> equalish(u6r4(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f819,plain,
( ~ sQ23_spl
| equalish(u6r4(exist),u4r1(exist)) ),
inference(component_clause,[status(thm)],[f818]) ).
fof(f822,definition,
! [X0] :
( sQ24_spl
<=> ( ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u6r4(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f823,plain,
! [X0] :
( ~ sQ24_spl
| ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u6r4(exist),X0) ),
inference(component_clause,[status(thm)],[f822]) ).
fof(f825,plain,
( ~ sQ5_spl
| sQ24_spl
| sQ23_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f799,f708,f727,f818,f822,f723]) ).
fof(f826,definition,
! [X0] :
( sQ25_spl
<=> ( ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u6r3(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f827,plain,
! [X0] :
( ~ sQ25_spl
| ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u6r3(exist),X0) ),
inference(component_clause,[status(thm)],[f826]) ).
fof(f829,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ22_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f800,f708,f727,f815,f826,f723]) ).
fof(f830,plain,
( ~ sQ5_spl
| sQ24_spl
| sQ23_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f801,f708,f738,f818,f822,f723]) ).
fof(f831,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ22_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f802,f708,f738,f815,f826,f723]) ).
fof(f832,definition,
( sQ26_spl
<=> equalish(u6r2(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f833,plain,
( ~ sQ26_spl
| equalish(u6r2(exist),u4r1(exist)) ),
inference(component_clause,[status(thm)],[f832]) ).
fof(f835,definition,
! [X0] :
( sQ27_spl
<=> ( ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f838,plain,
( ~ sQ5_spl
| sQ27_spl
| sQ26_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f803,f708,f743,f832,f835,f723]) ).
fof(f839,plain,
( ~ sQ5_spl
| sQ27_spl
| sQ26_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f804,f708,f753,f832,f835,f723]) ).
fof(f840,definition,
( sQ28_spl
<=> equalish(u6r1(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f841,plain,
( ~ sQ28_spl
| equalish(u6r1(exist),u4r1(exist)) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f843,definition,
! [X0] :
( sQ29_spl
<=> ( ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u6r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f846,plain,
( ~ sQ5_spl
| sQ29_spl
| sQ28_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f805,f708,f743,f840,f843,f723]) ).
fof(f847,plain,
( ~ sQ5_spl
| sQ29_spl
| sQ28_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f806,f708,f753,f840,f843,f723]) ).
fof(f848,plain,
( ~ sQ5_spl
| sQ24_spl
| sQ23_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f807,f708,f765,f818,f822,f723]) ).
fof(f849,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ22_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f808,f708,f765,f815,f826,f723]) ).
fof(f850,plain,
( ~ sQ5_spl
| sQ24_spl
| sQ23_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f809,f708,f711,f818,f822,f723]) ).
fof(f851,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ22_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f810,f708,f711,f815,f826,f723]) ).
fof(f852,definition,
( sQ30_spl
<=> d(u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f855,plain,
( ~ sQ30_spl
| ~ sQ5_spl
| sQ17_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f811,f708,f743,f772,f723,f852]) ).
fof(f856,plain,
( ~ sQ30_spl
| ~ sQ5_spl
| sQ17_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f812,f708,f753,f772,f723,f852]) ).
fof(f857,definition,
! [X0,X1] :
( sQ31_spl
<=> ( ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u4r1(exist),X1)
| equalish(u4r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f858,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u4r1(exist),X1)
| equalish(u4r1(exist),X0) ),
inference(component_clause,[status(thm)],[f857]) ).
fof(f860,plain,
( ~ sQ5_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f813,f857,f723]) ).
fof(f861,definition,
( sQ32_spl
<=> c(u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ21_spl
| ~ sQ32_spl
| ~ sQ5_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f814,f772,f723,f861,f787]) ).
fof(f865,plain,
( ~ sQ10_spl
| s1most(u6r4(exist)) ),
inference(resolution,[status(thm)],[f744,f64]) ).
fof(f866,plain,
s(u4r1(exist),u1r2(u4r1(exist))),
inference(resolution,[status(thm)],[f795,f61]) ).
fof(f867,plain,
s(u4r1(exist),u1r1(u4r1(exist))),
inference(resolution,[status(thm)],[f795,f60]) ).
fof(f870,plain,
( ~ sQ1_spl
| s2least(u6r1(exist)) ),
inference(resolution,[status(thm)],[f712,f57]) ).
fof(f872,plain,
! [X0] :
( ~ d(X0)
| ~ d(u4r1(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u4r1(exist),X0) ),
inference(resolution,[status(thm)],[f87,f119]) ).
fof(f873,plain,
! [X0] :
( ~ d(X0)
| ~ d(u4r2(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u4r2(exist),X0) ),
inference(resolution,[status(thm)],[f87,f117]) ).
fof(f886,plain,
! [X0,X1] :
( r2most(X0)
| ~ d(X1)
| ~ d(u5r3(X0))
| ~ r(X0,X1)
| ~ f(X0)
| equalish(u5r3(X0),X1) ),
inference(resolution,[status(thm)],[f87,f85]) ).
fof(f887,plain,
! [X0,X1] :
( r2most(X0)
| ~ d(X1)
| ~ d(u5r2(X0))
| ~ r(X0,X1)
| ~ f(X0)
| equalish(u5r2(X0),X1) ),
inference(resolution,[status(thm)],[f87,f84]) ).
fof(f888,plain,
! [X0,X1] :
( r2most(X0)
| ~ d(X1)
| ~ d(u5r1(X0))
| ~ r(X0,X1)
| ~ f(X0)
| equalish(u5r1(X0),X1) ),
inference(resolution,[status(thm)],[f87,f83]) ).
fof(f889,definition,
! [X0] :
( sQ33_spl
<=> ( ~ d(X0)
| ~ r(exist,X0)
| equalish(u4r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f892,plain,
( ~ sQ30_spl
| ~ sQ0_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f872,f889,f708,f852]) ).
fof(f893,definition,
! [X0] :
( sQ34_spl
<=> ( ~ d(X0)
| ~ r(exist,X0)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f896,plain,
( ~ sQ18_spl
| ~ sQ0_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f873,f893,f708,f775]) ).
fof(f897,plain,
! [X0] :
( ~ c(X0)
| ~ c(u4r1(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u4r1(exist),X0) ),
inference(resolution,[status(thm)],[f89,f119]) ).
fof(f898,plain,
! [X0] :
( ~ c(X0)
| ~ c(u4r2(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u4r2(exist),X0) ),
inference(resolution,[status(thm)],[f89,f117]) ).
fof(f911,plain,
! [X0,X1] :
( r2most(X0)
| ~ c(X1)
| ~ c(u5r3(X0))
| ~ r(X0,X1)
| ~ f(X0)
| equalish(u5r3(X0),X1) ),
inference(resolution,[status(thm)],[f89,f85]) ).
fof(f912,plain,
! [X0,X1] :
( r2most(X0)
| ~ c(X1)
| ~ c(u5r2(X0))
| ~ r(X0,X1)
| ~ f(X0)
| equalish(u5r2(X0),X1) ),
inference(resolution,[status(thm)],[f89,f84]) ).
fof(f913,plain,
! [X0,X1] :
( r2most(X0)
| ~ c(X1)
| ~ c(u5r1(X0))
| ~ r(X0,X1)
| ~ f(X0)
| equalish(u5r1(X0),X1) ),
inference(resolution,[status(thm)],[f89,f83]) ).
fof(f914,definition,
! [X0] :
( sQ35_spl
<=> ( ~ c(X0)
| ~ r(exist,X0)
| equalish(u4r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f917,plain,
( ~ sQ32_spl
| ~ sQ0_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f897,f914,f708,f861]) ).
fof(f918,definition,
! [X0] :
( sQ36_spl
<=> ( ~ c(X0)
| ~ r(exist,X0)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f921,plain,
( ~ sQ20_spl
| ~ sQ0_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f898,f918,f708,f784]) ).
fof(f922,plain,
! [X0] :
( ~ sQ19_spl
| ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f781,f119]) ).
fof(f923,plain,
! [X0] :
( ~ sQ19_spl
| ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f781,f117]) ).
fof(f924,plain,
! [X0] :
( ~ sQ19_spl
| d(u6r4(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f781,f112]) ).
fof(f925,plain,
! [X0] :
( ~ sQ19_spl
| d(u6r3(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f781,f111]) ).
fof(f926,plain,
! [X0] :
( ~ sQ19_spl
| d(u6r4(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f781,f107]) ).
fof(f927,plain,
! [X0] :
( ~ sQ19_spl
| d(u6r3(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f781,f106]) ).
fof(f928,plain,
! [X0] :
( ~ sQ19_spl
| r(exist,u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f781,f114]) ).
fof(f929,plain,
! [X0] :
( ~ sQ19_spl
| r(exist,u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f781,f109]) ).
fof(f930,plain,
! [X0] :
( ~ sQ19_spl
| c(u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f781,f104]) ).
fof(f931,plain,
! [X0] :
( ~ sQ19_spl
| c(u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f781,f99]) ).
fof(f932,plain,
! [X0] :
( ~ sQ19_spl
| r(exist,u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f781,f113]) ).
fof(f933,plain,
! [X0] :
( ~ sQ19_spl
| r(exist,u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f781,f108]) ).
fof(f934,plain,
! [X0] :
( ~ sQ19_spl
| c(u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f781,f103]) ).
fof(f935,plain,
! [X0] :
( ~ sQ19_spl
| c(u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f781,f98]) ).
fof(f936,plain,
! [X0] :
( ~ sQ19_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r3(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f781,f85]) ).
fof(f937,plain,
! [X0] :
( ~ sQ19_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r2(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f781,f84]) ).
fof(f938,plain,
! [X0] :
( ~ sQ19_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r1(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f781,f83]) ).
fof(f939,definition,
( sQ37_spl
<=> equalish(u4r2(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f940,plain,
( ~ sQ37_spl
| equalish(u4r2(exist),u4r1(exist)) ),
inference(component_clause,[status(thm)],[f939]) ).
fof(f942,definition,
! [X0] :
( sQ38_spl
<=> ( ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f943,plain,
! [X0] :
( ~ sQ38_spl
| ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u4r2(exist),X0) ),
inference(component_clause,[status(thm)],[f942]) ).
fof(f945,plain,
( ~ sQ19_spl
| sQ38_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f922,f939,f942,f780]) ).
fof(f946,definition,
( sQ39_spl
<=> equalish(u4r2(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f947,plain,
( ~ sQ39_spl
| equalish(u4r2(exist),u4r2(exist)) ),
inference(component_clause,[status(thm)],[f946]) ).
fof(f949,definition,
! [X0] :
( sQ40_spl
<=> ( ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f952,plain,
( ~ sQ19_spl
| sQ40_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f923,f946,f949,f780]) ).
fof(f953,definition,
( sQ41_spl
<=> equalish(u4r2(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f954,plain,
( ~ sQ41_spl
| equalish(u4r2(exist),u6r2(exist)) ),
inference(component_clause,[status(thm)],[f953]) ).
fof(f956,plain,
( ~ sQ19_spl
| sQ10_spl
| sQ0_spl
| sQ12_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f924,f953,f749,f708,f743,f780]) ).
fof(f957,plain,
( ~ sQ19_spl
| sQ13_spl
| sQ0_spl
| sQ12_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f925,f953,f749,f708,f753,f780]) ).
fof(f958,definition,
( sQ42_spl
<=> equalish(u4r2(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f959,plain,
( ~ sQ42_spl
| equalish(u4r2(exist),u6r1(exist)) ),
inference(component_clause,[status(thm)],[f958]) ).
fof(f961,plain,
( ~ sQ19_spl
| sQ10_spl
| sQ0_spl
| sQ15_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f926,f958,f760,f708,f743,f780]) ).
fof(f962,plain,
( ~ sQ19_spl
| sQ13_spl
| sQ0_spl
| sQ15_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f927,f958,f760,f708,f753,f780]) ).
fof(f963,definition,
( sQ43_spl
<=> equalish(u4r2(exist),u6r4(exist)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f964,plain,
( ~ sQ43_spl
| equalish(u4r2(exist),u6r4(exist)) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,plain,
( ~ sQ19_spl
| sQ6_spl
| sQ0_spl
| sQ7_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f928,f963,f730,f708,f727,f780]) ).
fof(f967,plain,
( ~ sQ19_spl
| sQ9_spl
| sQ0_spl
| sQ7_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f929,f963,f730,f708,f738,f780]) ).
fof(f968,plain,
( ~ sQ19_spl
| sQ16_spl
| sQ0_spl
| sQ7_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f930,f963,f730,f708,f765,f780]) ).
fof(f969,plain,
( ~ sQ19_spl
| sQ1_spl
| sQ0_spl
| sQ7_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f931,f963,f730,f708,f711,f780]) ).
fof(f970,definition,
( sQ44_spl
<=> equalish(u4r2(exist),u6r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f971,plain,
( ~ sQ44_spl
| equalish(u4r2(exist),u6r3(exist)) ),
inference(component_clause,[status(thm)],[f970]) ).
fof(f973,plain,
( ~ sQ19_spl
| sQ6_spl
| sQ0_spl
| sQ8_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f932,f970,f734,f708,f727,f780]) ).
fof(f974,plain,
( ~ sQ19_spl
| sQ9_spl
| sQ0_spl
| sQ8_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f933,f970,f734,f708,f738,f780]) ).
fof(f975,plain,
( ~ sQ19_spl
| sQ16_spl
| sQ0_spl
| sQ8_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f934,f970,f734,f708,f765,f780]) ).
fof(f976,plain,
( ~ sQ19_spl
| sQ1_spl
| sQ0_spl
| sQ8_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f935,f970,f734,f708,f711,f780]) ).
fof(f977,definition,
( sQ45_spl
<=> equalish(u4r2(exist),u5r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f980,definition,
! [X0] :
( sQ46_spl
<=> ( ~ r(exist,X0)
| equalish(u5r3(exist),X0)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f983,plain,
( ~ sQ19_spl
| sQ5_spl
| sQ46_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f936,f977,f980,f723,f780]) ).
fof(f984,definition,
( sQ47_spl
<=> equalish(u4r2(exist),u5r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f987,definition,
! [X0] :
( sQ48_spl
<=> ( ~ r(exist,X0)
| equalish(u5r2(exist),X0)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f990,plain,
( ~ sQ19_spl
| sQ5_spl
| sQ48_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f937,f984,f987,f723,f780]) ).
fof(f991,definition,
( sQ49_spl
<=> equalish(u4r2(exist),u5r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f994,definition,
! [X0] :
( sQ50_spl
<=> ( ~ r(exist,X0)
| equalish(u5r1(exist),X0)
| equalish(u4r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f997,plain,
( ~ sQ19_spl
| sQ5_spl
| sQ50_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f938,f991,f994,f723,f780]) ).
fof(f998,plain,
( ~ sQ8_spl
| equalish(u4r2(exist),u4r1(exist))
| equalish(u6r3(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f735,f119]) ).
fof(f999,plain,
( ~ sQ8_spl
| equalish(u4r2(exist),u4r2(exist))
| equalish(u6r3(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f735,f117]) ).
fof(f1000,plain,
( ~ sQ8_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r2(exist),u6r2(exist))
| equalish(u6r3(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f735,f112]) ).
fof(f1001,plain,
( ~ sQ8_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r2(exist),u6r2(exist))
| equalish(u6r3(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f735,f111]) ).
fof(f1002,plain,
( ~ sQ8_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r2(exist),u6r1(exist))
| equalish(u6r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f735,f107]) ).
fof(f1003,plain,
( ~ sQ8_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r2(exist),u6r1(exist))
| equalish(u6r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f735,f106]) ).
fof(f1004,plain,
( ~ sQ8_spl
| r(exist,u6r2(exist))
| f(exist)
| equalish(u4r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f735,f114]) ).
fof(f1005,plain,
( ~ sQ8_spl
| r(exist,u6r1(exist))
| f(exist)
| equalish(u4r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f735,f109]) ).
fof(f1006,plain,
( ~ sQ8_spl
| c(u6r2(exist))
| f(exist)
| equalish(u4r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f735,f104]) ).
fof(f1007,plain,
( ~ sQ8_spl
| c(u6r1(exist))
| f(exist)
| equalish(u4r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f735,f99]) ).
fof(f1012,plain,
( ~ sQ8_spl
| r2most(exist)
| equalish(u4r2(exist),u5r3(exist))
| equalish(u6r3(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f735,f85]) ).
fof(f1013,plain,
( ~ sQ8_spl
| r2most(exist)
| equalish(u4r2(exist),u5r2(exist))
| equalish(u6r3(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f735,f84]) ).
fof(f1014,plain,
( ~ sQ8_spl
| r2most(exist)
| equalish(u4r2(exist),u5r1(exist))
| equalish(u6r3(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f735,f83]) ).
fof(f1015,plain,
( ~ sQ8_spl
| sQ37_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f998,f815,f939,f734]) ).
fof(f1016,plain,
( ~ sQ8_spl
| sQ39_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f999,f717,f946,f734]) ).
fof(f1017,definition,
( sQ51_spl
<=> equalish(u6r3(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1018,plain,
( ~ sQ51_spl
| equalish(u6r3(exist),u6r2(exist)) ),
inference(component_clause,[status(thm)],[f1017]) ).
fof(f1020,plain,
( ~ sQ8_spl
| sQ10_spl
| sQ0_spl
| sQ41_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1000,f1017,f953,f708,f743,f734]) ).
fof(f1021,plain,
( ~ sQ8_spl
| sQ13_spl
| sQ0_spl
| sQ41_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1001,f1017,f953,f708,f753,f734]) ).
fof(f1022,definition,
( sQ52_spl
<=> equalish(u6r3(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1023,plain,
( ~ sQ52_spl
| equalish(u6r3(exist),u6r1(exist)) ),
inference(component_clause,[status(thm)],[f1022]) ).
fof(f1025,plain,
( ~ sQ8_spl
| sQ10_spl
| sQ0_spl
| sQ42_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1002,f1022,f958,f708,f743,f734]) ).
fof(f1026,plain,
( ~ sQ8_spl
| sQ13_spl
| sQ0_spl
| sQ42_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1003,f1022,f958,f708,f753,f734]) ).
fof(f1027,plain,
( ~ sQ8_spl
| sQ6_spl
| sQ0_spl
| sQ43_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1004,f714,f963,f708,f727,f734]) ).
fof(f1028,plain,
( ~ sQ8_spl
| sQ9_spl
| sQ0_spl
| sQ43_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1005,f714,f963,f708,f738,f734]) ).
fof(f1029,plain,
( ~ sQ8_spl
| sQ16_spl
| sQ0_spl
| sQ43_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1006,f714,f963,f708,f765,f734]) ).
fof(f1030,plain,
( ~ sQ8_spl
| sQ1_spl
| sQ0_spl
| sQ43_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1007,f714,f963,f708,f711,f734]) ).
fof(f1031,definition,
( sQ53_spl
<=> equalish(u6r3(exist),u6r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1032,plain,
( ~ sQ53_spl
| equalish(u6r3(exist),u6r3(exist)) ),
inference(component_clause,[status(thm)],[f1031]) ).
fof(f1038,definition,
( sQ54_spl
<=> equalish(u6r3(exist),u5r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1041,plain,
( ~ sQ8_spl
| sQ5_spl
| sQ45_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1012,f1038,f977,f723,f734]) ).
fof(f1042,definition,
( sQ55_spl
<=> equalish(u6r3(exist),u5r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1045,plain,
( ~ sQ8_spl
| sQ5_spl
| sQ47_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1013,f1042,f984,f723,f734]) ).
fof(f1046,definition,
( sQ56_spl
<=> equalish(u6r3(exist),u5r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( ~ sQ8_spl
| sQ5_spl
| sQ49_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1014,f1046,f991,f723,f734]) ).
fof(f1050,plain,
( ~ sQ7_spl
| equalish(u4r2(exist),u4r1(exist))
| equalish(u6r4(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f731,f119]) ).
fof(f1051,plain,
( ~ sQ7_spl
| equalish(u4r2(exist),u4r2(exist))
| equalish(u6r4(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f731,f117]) ).
fof(f1052,plain,
( ~ sQ7_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r2(exist),u6r2(exist))
| equalish(u6r4(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f731,f112]) ).
fof(f1053,plain,
( ~ sQ7_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r2(exist),u6r2(exist))
| equalish(u6r4(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f731,f111]) ).
fof(f1054,plain,
( ~ sQ7_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r2(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f731,f107]) ).
fof(f1055,plain,
( ~ sQ7_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r2(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f731,f106]) ).
fof(f1060,plain,
( ~ sQ7_spl
| r(exist,u6r2(exist))
| f(exist)
| equalish(u4r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f731,f113]) ).
fof(f1061,plain,
( ~ sQ7_spl
| r(exist,u6r1(exist))
| f(exist)
| equalish(u4r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f731,f108]) ).
fof(f1062,plain,
( ~ sQ7_spl
| c(u6r2(exist))
| f(exist)
| equalish(u4r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f731,f103]) ).
fof(f1063,plain,
( ~ sQ7_spl
| c(u6r1(exist))
| f(exist)
| equalish(u4r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f731,f98]) ).
fof(f1064,plain,
( ~ sQ7_spl
| r2most(exist)
| equalish(u4r2(exist),u5r3(exist))
| equalish(u6r4(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f731,f85]) ).
fof(f1065,plain,
( ~ sQ7_spl
| r2most(exist)
| equalish(u4r2(exist),u5r2(exist))
| equalish(u6r4(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f731,f84]) ).
fof(f1066,plain,
( ~ sQ7_spl
| r2most(exist)
| equalish(u4r2(exist),u5r1(exist))
| equalish(u6r4(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f731,f83]) ).
fof(f1067,plain,
( ~ sQ7_spl
| sQ37_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f1050,f818,f939,f730]) ).
fof(f1068,plain,
( ~ sQ7_spl
| sQ39_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1051,f720,f946,f730]) ).
fof(f1069,definition,
( sQ57_spl
<=> equalish(u6r4(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1070,plain,
( ~ sQ57_spl
| equalish(u6r4(exist),u6r2(exist)) ),
inference(component_clause,[status(thm)],[f1069]) ).
fof(f1072,plain,
( ~ sQ7_spl
| sQ10_spl
| sQ0_spl
| sQ41_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1052,f1069,f953,f708,f743,f730]) ).
fof(f1073,plain,
( ~ sQ7_spl
| sQ13_spl
| sQ0_spl
| sQ41_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1053,f1069,f953,f708,f753,f730]) ).
fof(f1074,definition,
( sQ58_spl
<=> equalish(u6r4(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1075,plain,
( ~ sQ58_spl
| equalish(u6r4(exist),u6r1(exist)) ),
inference(component_clause,[status(thm)],[f1074]) ).
fof(f1077,plain,
( ~ sQ7_spl
| sQ10_spl
| sQ0_spl
| sQ42_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1054,f1074,f958,f708,f743,f730]) ).
fof(f1078,plain,
( ~ sQ7_spl
| sQ13_spl
| sQ0_spl
| sQ42_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1055,f1074,f958,f708,f753,f730]) ).
fof(f1079,definition,
( sQ59_spl
<=> equalish(u6r4(exist),u6r4(exist)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1080,plain,
( ~ sQ59_spl
| equalish(u6r4(exist),u6r4(exist)) ),
inference(component_clause,[status(thm)],[f1079]) ).
fof(f1086,definition,
( sQ60_spl
<=> equalish(u6r4(exist),u6r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1087,plain,
( ~ sQ60_spl
| equalish(u6r4(exist),u6r3(exist)) ),
inference(component_clause,[status(thm)],[f1086]) ).
fof(f1088,plain,
( sQ60_spl
| ~ equalish(u6r4(exist),u6r3(exist)) ),
inference(component_clause,[status(thm)],[f1086]) ).
fof(f1089,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ0_spl
| sQ44_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1060,f1086,f970,f708,f727,f730]) ).
fof(f1090,plain,
( ~ sQ7_spl
| sQ9_spl
| sQ0_spl
| sQ44_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1061,f1086,f970,f708,f738,f730]) ).
fof(f1091,plain,
( ~ sQ7_spl
| sQ16_spl
| sQ0_spl
| sQ44_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1062,f1086,f970,f708,f765,f730]) ).
fof(f1092,plain,
( ~ sQ7_spl
| sQ1_spl
| sQ0_spl
| sQ44_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1063,f1086,f970,f708,f711,f730]) ).
fof(f1093,definition,
( sQ61_spl
<=> equalish(u6r4(exist),u5r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1096,plain,
( ~ sQ7_spl
| sQ5_spl
| sQ45_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1064,f1093,f977,f723,f730]) ).
fof(f1097,definition,
( sQ62_spl
<=> equalish(u6r4(exist),u5r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1100,plain,
( ~ sQ7_spl
| sQ5_spl
| sQ47_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1065,f1097,f984,f723,f730]) ).
fof(f1101,definition,
( sQ63_spl
<=> equalish(u6r4(exist),u5r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1104,plain,
( ~ sQ7_spl
| sQ5_spl
| sQ49_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1066,f1101,f991,f723,f730]) ).
fof(f1105,plain,
! [X0] :
( ~ sQ31_spl
| ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f858,f119]) ).
fof(f1106,plain,
! [X0] :
( ~ sQ31_spl
| ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f858,f117]) ).
fof(f1107,plain,
! [X0] :
( ~ sQ31_spl
| d(u6r4(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f858,f112]) ).
fof(f1108,plain,
! [X0] :
( ~ sQ31_spl
| d(u6r3(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f858,f111]) ).
fof(f1109,plain,
! [X0] :
( ~ sQ31_spl
| d(u6r4(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f858,f107]) ).
fof(f1110,plain,
! [X0] :
( ~ sQ31_spl
| d(u6r3(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f858,f106]) ).
fof(f1111,plain,
! [X0] :
( ~ sQ31_spl
| r(exist,u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f858,f114]) ).
fof(f1112,plain,
! [X0] :
( ~ sQ31_spl
| r(exist,u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f858,f109]) ).
fof(f1113,plain,
! [X0] :
( ~ sQ31_spl
| c(u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f858,f104]) ).
fof(f1114,plain,
! [X0] :
( ~ sQ31_spl
| c(u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f858,f99]) ).
fof(f1115,plain,
! [X0] :
( ~ sQ31_spl
| r(exist,u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f858,f113]) ).
fof(f1116,plain,
! [X0] :
( ~ sQ31_spl
| r(exist,u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f858,f108]) ).
fof(f1117,plain,
! [X0] :
( ~ sQ31_spl
| c(u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f858,f103]) ).
fof(f1118,plain,
! [X0] :
( ~ sQ31_spl
| c(u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f858,f98]) ).
fof(f1119,plain,
! [X0] :
( ~ sQ31_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r3(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f858,f85]) ).
fof(f1120,plain,
! [X0] :
( ~ sQ31_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r2(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f858,f84]) ).
fof(f1121,plain,
! [X0] :
( ~ sQ31_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r1(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f858,f83]) ).
fof(f1122,definition,
( sQ64_spl
<=> equalish(u4r1(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1123,plain,
( ~ sQ64_spl
| equalish(u4r1(exist),u4r1(exist)) ),
inference(component_clause,[status(thm)],[f1122]) ).
fof(f1125,definition,
! [X0] :
( sQ65_spl
<=> ( ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1128,plain,
( ~ sQ31_spl
| sQ65_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1105,f1122,f1125,f857]) ).
fof(f1129,definition,
( sQ66_spl
<=> equalish(u4r1(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1130,plain,
( ~ sQ66_spl
| equalish(u4r1(exist),u4r2(exist)) ),
inference(component_clause,[status(thm)],[f1129]) ).
fof(f1132,plain,
( ~ sQ31_spl
| sQ38_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1106,f1129,f942,f857]) ).
fof(f1133,definition,
( sQ67_spl
<=> equalish(u4r1(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1134,plain,
( ~ sQ67_spl
| equalish(u4r1(exist),u6r2(exist)) ),
inference(component_clause,[status(thm)],[f1133]) ).
fof(f1136,plain,
( ~ sQ31_spl
| sQ10_spl
| sQ0_spl
| sQ27_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1107,f1133,f835,f708,f743,f857]) ).
fof(f1137,plain,
( ~ sQ31_spl
| sQ13_spl
| sQ0_spl
| sQ27_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1108,f1133,f835,f708,f753,f857]) ).
fof(f1138,definition,
( sQ68_spl
<=> equalish(u4r1(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1139,plain,
( ~ sQ68_spl
| equalish(u4r1(exist),u6r1(exist)) ),
inference(component_clause,[status(thm)],[f1138]) ).
fof(f1141,plain,
( ~ sQ31_spl
| sQ10_spl
| sQ0_spl
| sQ29_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1109,f1138,f843,f708,f743,f857]) ).
fof(f1142,plain,
( ~ sQ31_spl
| sQ13_spl
| sQ0_spl
| sQ29_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1110,f1138,f843,f708,f753,f857]) ).
fof(f1143,definition,
( sQ69_spl
<=> equalish(u4r1(exist),u6r4(exist)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1144,plain,
( ~ sQ69_spl
| equalish(u4r1(exist),u6r4(exist)) ),
inference(component_clause,[status(thm)],[f1143]) ).
fof(f1146,plain,
( ~ sQ31_spl
| sQ6_spl
| sQ0_spl
| sQ24_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1111,f1143,f822,f708,f727,f857]) ).
fof(f1147,plain,
( ~ sQ31_spl
| sQ9_spl
| sQ0_spl
| sQ24_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1112,f1143,f822,f708,f738,f857]) ).
fof(f1148,plain,
( ~ sQ31_spl
| sQ16_spl
| sQ0_spl
| sQ24_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1113,f1143,f822,f708,f765,f857]) ).
fof(f1149,plain,
( ~ sQ31_spl
| sQ1_spl
| sQ0_spl
| sQ24_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1114,f1143,f822,f708,f711,f857]) ).
fof(f1150,definition,
( sQ70_spl
<=> equalish(u4r1(exist),u6r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1151,plain,
( ~ sQ70_spl
| equalish(u4r1(exist),u6r3(exist)) ),
inference(component_clause,[status(thm)],[f1150]) ).
fof(f1153,plain,
( ~ sQ31_spl
| sQ6_spl
| sQ0_spl
| sQ25_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1115,f1150,f826,f708,f727,f857]) ).
fof(f1154,plain,
( ~ sQ31_spl
| sQ9_spl
| sQ0_spl
| sQ25_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1116,f1150,f826,f708,f738,f857]) ).
fof(f1155,plain,
( ~ sQ31_spl
| sQ16_spl
| sQ0_spl
| sQ25_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1117,f1150,f826,f708,f765,f857]) ).
fof(f1156,plain,
( ~ sQ31_spl
| sQ1_spl
| sQ0_spl
| sQ25_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1118,f1150,f826,f708,f711,f857]) ).
fof(f1157,definition,
( sQ71_spl
<=> equalish(u4r1(exist),u5r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1160,definition,
! [X0] :
( sQ72_spl
<=> ( ~ r(exist,X0)
| equalish(u5r3(exist),X0)
| equalish(u4r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1163,plain,
( ~ sQ31_spl
| sQ5_spl
| sQ72_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1119,f1157,f1160,f723,f857]) ).
fof(f1164,definition,
( sQ73_spl
<=> equalish(u4r1(exist),u5r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1167,definition,
! [X0] :
( sQ74_spl
<=> ( ~ r(exist,X0)
| equalish(u5r2(exist),X0)
| equalish(u4r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1170,plain,
( ~ sQ31_spl
| sQ5_spl
| sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1120,f1164,f1167,f723,f857]) ).
fof(f1171,definition,
( sQ75_spl
<=> equalish(u4r1(exist),u5r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1174,definition,
! [X0] :
( sQ76_spl
<=> ( ~ r(exist,X0)
| equalish(u5r1(exist),X0)
| equalish(u4r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
( ~ sQ31_spl
| sQ5_spl
| sQ76_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1121,f1171,f1174,f723,f857]) ).
fof(f1178,plain,
( ~ sQ25_spl
| equalish(u4r1(exist),u4r1(exist))
| equalish(u6r3(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f827,f119]) ).
fof(f1179,plain,
( ~ sQ25_spl
| equalish(u4r1(exist),u4r2(exist))
| equalish(u6r3(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f827,f117]) ).
fof(f1180,plain,
( ~ sQ25_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r1(exist),u6r2(exist))
| equalish(u6r3(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f827,f112]) ).
fof(f1181,plain,
( ~ sQ25_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r1(exist),u6r2(exist))
| equalish(u6r3(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f827,f111]) ).
fof(f1182,plain,
( ~ sQ25_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r1(exist),u6r1(exist))
| equalish(u6r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f827,f107]) ).
fof(f1183,plain,
( ~ sQ25_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r1(exist),u6r1(exist))
| equalish(u6r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f827,f106]) ).
fof(f1184,plain,
( ~ sQ25_spl
| r(exist,u6r2(exist))
| f(exist)
| equalish(u4r1(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f827,f114]) ).
fof(f1185,plain,
( ~ sQ25_spl
| r(exist,u6r1(exist))
| f(exist)
| equalish(u4r1(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f827,f109]) ).
fof(f1186,plain,
( ~ sQ25_spl
| c(u6r2(exist))
| f(exist)
| equalish(u4r1(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f827,f104]) ).
fof(f1187,plain,
( ~ sQ25_spl
| c(u6r1(exist))
| f(exist)
| equalish(u4r1(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f827,f99]) ).
fof(f1192,plain,
( ~ sQ25_spl
| r2most(exist)
| equalish(u4r1(exist),u5r3(exist))
| equalish(u6r3(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f827,f85]) ).
fof(f1193,plain,
( ~ sQ25_spl
| r2most(exist)
| equalish(u4r1(exist),u5r2(exist))
| equalish(u6r3(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f827,f84]) ).
fof(f1194,plain,
( ~ sQ25_spl
| r2most(exist)
| equalish(u4r1(exist),u5r1(exist))
| equalish(u6r3(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f827,f83]) ).
fof(f1195,plain,
( ~ sQ25_spl
| sQ64_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f1178,f815,f1122,f826]) ).
fof(f1196,plain,
( ~ sQ25_spl
| sQ66_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1179,f717,f1129,f826]) ).
fof(f1197,plain,
( ~ sQ25_spl
| sQ10_spl
| sQ0_spl
| sQ67_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1180,f1017,f1133,f708,f743,f826]) ).
fof(f1198,plain,
( ~ sQ25_spl
| sQ13_spl
| sQ0_spl
| sQ67_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1181,f1017,f1133,f708,f753,f826]) ).
fof(f1199,plain,
( ~ sQ25_spl
| sQ10_spl
| sQ0_spl
| sQ68_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1182,f1022,f1138,f708,f743,f826]) ).
fof(f1200,plain,
( ~ sQ25_spl
| sQ13_spl
| sQ0_spl
| sQ68_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1183,f1022,f1138,f708,f753,f826]) ).
fof(f1201,plain,
( ~ sQ25_spl
| sQ6_spl
| sQ0_spl
| sQ69_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1184,f714,f1143,f708,f727,f826]) ).
fof(f1202,plain,
( ~ sQ25_spl
| sQ9_spl
| sQ0_spl
| sQ69_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1185,f714,f1143,f708,f738,f826]) ).
fof(f1203,plain,
( ~ sQ25_spl
| sQ16_spl
| sQ0_spl
| sQ69_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1186,f714,f1143,f708,f765,f826]) ).
fof(f1204,plain,
( ~ sQ25_spl
| sQ1_spl
| sQ0_spl
| sQ69_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1187,f714,f1143,f708,f711,f826]) ).
fof(f1209,plain,
( ~ sQ25_spl
| sQ5_spl
| sQ71_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1192,f1038,f1157,f723,f826]) ).
fof(f1210,plain,
( ~ sQ25_spl
| sQ5_spl
| sQ73_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1193,f1042,f1164,f723,f826]) ).
fof(f1211,plain,
( ~ sQ25_spl
| sQ5_spl
| sQ75_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1194,f1046,f1171,f723,f826]) ).
fof(f1212,plain,
( ~ sQ24_spl
| equalish(u4r1(exist),u4r1(exist))
| equalish(u6r4(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f823,f119]) ).
fof(f1213,plain,
( ~ sQ24_spl
| equalish(u4r1(exist),u4r2(exist))
| equalish(u6r4(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f823,f117]) ).
fof(f1214,plain,
( ~ sQ24_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r1(exist),u6r2(exist))
| equalish(u6r4(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f823,f112]) ).
fof(f1215,plain,
( ~ sQ24_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r1(exist),u6r2(exist))
| equalish(u6r4(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f823,f111]) ).
fof(f1216,plain,
( ~ sQ24_spl
| d(u6r4(exist))
| f(exist)
| equalish(u4r1(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f823,f107]) ).
fof(f1217,plain,
( ~ sQ24_spl
| d(u6r3(exist))
| f(exist)
| equalish(u4r1(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f823,f106]) ).
fof(f1222,plain,
( ~ sQ24_spl
| r(exist,u6r2(exist))
| f(exist)
| equalish(u4r1(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f823,f113]) ).
fof(f1223,plain,
( ~ sQ24_spl
| r(exist,u6r1(exist))
| f(exist)
| equalish(u4r1(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f823,f108]) ).
fof(f1224,plain,
( ~ sQ24_spl
| c(u6r2(exist))
| f(exist)
| equalish(u4r1(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f823,f103]) ).
fof(f1225,plain,
( ~ sQ24_spl
| c(u6r1(exist))
| f(exist)
| equalish(u4r1(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f823,f98]) ).
fof(f1226,plain,
( ~ sQ24_spl
| r2most(exist)
| equalish(u4r1(exist),u5r3(exist))
| equalish(u6r4(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f823,f85]) ).
fof(f1227,plain,
( ~ sQ24_spl
| r2most(exist)
| equalish(u4r1(exist),u5r2(exist))
| equalish(u6r4(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f823,f84]) ).
fof(f1228,plain,
( ~ sQ24_spl
| r2most(exist)
| equalish(u4r1(exist),u5r1(exist))
| equalish(u6r4(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f823,f83]) ).
fof(f1229,plain,
( ~ sQ24_spl
| sQ64_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f1212,f818,f1122,f822]) ).
fof(f1230,plain,
( ~ sQ24_spl
| sQ66_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1213,f720,f1129,f822]) ).
fof(f1231,plain,
( ~ sQ24_spl
| sQ10_spl
| sQ0_spl
| sQ67_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1214,f1069,f1133,f708,f743,f822]) ).
fof(f1232,plain,
( ~ sQ24_spl
| sQ13_spl
| sQ0_spl
| sQ67_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1215,f1069,f1133,f708,f753,f822]) ).
fof(f1233,plain,
( ~ sQ24_spl
| sQ10_spl
| sQ0_spl
| sQ68_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1216,f1074,f1138,f708,f743,f822]) ).
fof(f1234,plain,
( ~ sQ24_spl
| sQ13_spl
| sQ0_spl
| sQ68_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1217,f1074,f1138,f708,f753,f822]) ).
fof(f1239,plain,
( ~ sQ24_spl
| sQ6_spl
| sQ0_spl
| sQ70_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1222,f1086,f1150,f708,f727,f822]) ).
fof(f1240,plain,
( ~ sQ24_spl
| sQ9_spl
| sQ0_spl
| sQ70_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1223,f1086,f1150,f708,f738,f822]) ).
fof(f1241,plain,
( ~ sQ24_spl
| sQ16_spl
| sQ0_spl
| sQ70_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1224,f1086,f1150,f708,f765,f822]) ).
fof(f1242,plain,
( ~ sQ24_spl
| sQ1_spl
| sQ0_spl
| sQ70_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1225,f1086,f1150,f708,f711,f822]) ).
fof(f1243,plain,
( ~ sQ24_spl
| sQ5_spl
| sQ71_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1226,f1093,f1157,f723,f822]) ).
fof(f1244,plain,
( ~ sQ24_spl
| sQ5_spl
| sQ73_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1227,f1097,f1164,f723,f822]) ).
fof(f1245,plain,
( ~ sQ24_spl
| sQ5_spl
| sQ75_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1228,f1101,f1171,f723,f822]) ).
fof(f1246,plain,
( e(exist)
| d(u6r4(exist))
| f(exist)
| s2least(u6r1(exist)) ),
inference(resolution,[status(thm)],[f216,f115]) ).
fof(f1247,definition,
( sQ77_spl
<=> s2least(u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1250,plain,
( sQ17_spl
| sQ10_spl
| sQ0_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1246,f1247,f708,f743,f772]) ).
fof(f1251,plain,
( e(exist)
| d(u6r3(exist))
| f(exist)
| s2least(u6r1(exist)) ),
inference(resolution,[status(thm)],[f217,f115]) ).
fof(f1252,plain,
( sQ17_spl
| sQ13_spl
| sQ0_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1251,f1247,f708,f753,f772]) ).
fof(f1254,definition,
( sQ78_spl
<=> s2least(u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1258,plain,
( s2least(u6r2(exist))
| e(exist)
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f564,f115]) ).
fof(f1259,plain,
( sQ78_spl
| sQ17_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1258,f708,f753,f772,f1254]) ).
fof(f1260,plain,
( s2least(u6r2(exist))
| e(exist)
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f565,f115]) ).
fof(f1261,plain,
( sQ78_spl
| sQ17_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1260,f708,f743,f772,f1254]) ).
fof(f1262,plain,
( r2most(exist)
| ~ d(u4r1(exist))
| ~ d(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f886,f119]) ).
fof(f1263,plain,
( r2most(exist)
| ~ d(u4r2(exist))
| ~ d(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f886,f117]) ).
fof(f1276,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ d(u5r3(X0))
| ~ d(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r3(X0)) ),
inference(resolution,[status(thm)],[f886,f85]) ).
fof(f1277,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ d(u5r2(X0))
| ~ d(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r2(X0)) ),
inference(resolution,[status(thm)],[f886,f84]) ).
fof(f1278,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ d(u5r1(X0))
| ~ d(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r1(X0)) ),
inference(resolution,[status(thm)],[f886,f83]) ).
fof(f1279,definition,
( sQ79_spl
<=> equalish(u5r3(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1282,definition,
( sQ80_spl
<=> d(u5r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1285,plain,
( sQ5_spl
| ~ sQ30_spl
| ~ sQ80_spl
| ~ sQ0_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1262,f1279,f708,f1282,f852,f723]) ).
fof(f1286,definition,
( sQ81_spl
<=> equalish(u5r3(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1289,plain,
( sQ5_spl
| ~ sQ18_spl
| ~ sQ80_spl
| ~ sQ0_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1263,f1286,f708,f1282,f775,f723]) ).
fof(f1290,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r3(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1276]) ).
fof(f1291,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r2(X0))
| ~ d(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1277]) ).
fof(f1292,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r2(X0))
| ~ d(u5r3(X0))
| ~ f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1291,f82]) ).
fof(f1293,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r1(X0))
| ~ d(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1278]) ).
fof(f1294,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r1(X0))
| ~ d(u5r3(X0))
| ~ f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1293,f81]) ).
fof(f1295,plain,
! [X0] :
( s2least(u5r3(X0))
| r2most(X0)
| ~ f(X0)
| equalish(u5r3(X0),u5r3(X0)) ),
inference(resolution,[status(thm)],[f1290,f215]) ).
fof(f1296,plain,
( r2most(exist)
| ~ d(u4r1(exist))
| ~ d(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f887,f119]) ).
fof(f1297,plain,
( r2most(exist)
| ~ d(u4r2(exist))
| ~ d(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f887,f117]) ).
fof(f1311,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ d(u5r2(X0))
| ~ d(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r2(X0)) ),
inference(resolution,[status(thm)],[f887,f84]) ).
fof(f1312,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ d(u5r1(X0))
| ~ d(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r1(X0)) ),
inference(resolution,[status(thm)],[f887,f83]) ).
fof(f1313,definition,
( sQ82_spl
<=> equalish(u5r2(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1316,definition,
( sQ83_spl
<=> d(u5r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1319,plain,
( sQ5_spl
| ~ sQ30_spl
| ~ sQ83_spl
| ~ sQ0_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1296,f1313,f708,f1316,f852,f723]) ).
fof(f1320,definition,
( sQ84_spl
<=> equalish(u5r2(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1323,plain,
( sQ5_spl
| ~ sQ18_spl
| ~ sQ83_spl
| ~ sQ0_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1297,f1320,f708,f1316,f775,f723]) ).
fof(f1325,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1311]) ).
fof(f1326,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r1(X0))
| ~ d(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1312]) ).
fof(f1327,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r1(X0))
| ~ d(u5r2(X0))
| ~ f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1326,f80]) ).
fof(f1328,plain,
! [X0] :
( s2least(u5r2(X0))
| r2most(X0)
| ~ f(X0)
| equalish(u5r2(X0),u5r2(X0)) ),
inference(resolution,[status(thm)],[f1325,f215]) ).
fof(f1329,plain,
( r2most(exist)
| ~ d(u4r1(exist))
| ~ d(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f888,f119]) ).
fof(f1330,plain,
( r2most(exist)
| ~ d(u4r2(exist))
| ~ d(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f888,f117]) ).
fof(f1345,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ d(u5r1(X0))
| ~ d(u5r1(X0))
| ~ f(X0)
| equalish(u5r1(X0),u5r1(X0)) ),
inference(resolution,[status(thm)],[f888,f83]) ).
fof(f1346,definition,
( sQ85_spl
<=> equalish(u5r1(exist),u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1349,definition,
( sQ86_spl
<=> d(u5r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1352,plain,
( sQ5_spl
| ~ sQ30_spl
| ~ sQ86_spl
| ~ sQ0_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f1329,f1346,f708,f1349,f852,f723]) ).
fof(f1353,definition,
( sQ87_spl
<=> equalish(u5r1(exist),u4r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1356,plain,
( sQ5_spl
| ~ sQ18_spl
| ~ sQ86_spl
| ~ sQ0_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f1330,f1353,f708,f1349,f775,f723]) ).
fof(f1359,plain,
! [X0] :
( r2most(X0)
| ~ d(u5r1(X0))
| ~ f(X0)
| equalish(u5r1(X0),u5r1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1345]) ).
fof(f1360,plain,
! [X0] :
( s2least(u5r1(X0))
| r2most(X0)
| ~ f(X0)
| equalish(u5r1(X0),u5r1(X0)) ),
inference(resolution,[status(thm)],[f1359,f215]) ).
fof(f1361,plain,
( r2most(exist)
| ~ c(u4r1(exist))
| ~ c(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f911,f119]) ).
fof(f1362,plain,
( r2most(exist)
| ~ c(u4r2(exist))
| ~ c(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f911,f117]) ).
fof(f1375,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ c(u5r3(X0))
| ~ c(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r3(X0)) ),
inference(resolution,[status(thm)],[f911,f85]) ).
fof(f1376,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ c(u5r2(X0))
| ~ c(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r2(X0)) ),
inference(resolution,[status(thm)],[f911,f84]) ).
fof(f1377,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ c(u5r1(X0))
| ~ c(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r1(X0)) ),
inference(resolution,[status(thm)],[f911,f83]) ).
fof(f1378,definition,
( sQ88_spl
<=> c(u5r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
( sQ5_spl
| ~ sQ32_spl
| ~ sQ88_spl
| ~ sQ0_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1361,f1279,f708,f1378,f861,f723]) ).
fof(f1382,plain,
( sQ5_spl
| ~ sQ20_spl
| ~ sQ88_spl
| ~ sQ0_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1362,f1286,f708,f1378,f784,f723]) ).
fof(f1383,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r3(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1375]) ).
fof(f1384,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r2(X0))
| ~ c(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1376]) ).
fof(f1385,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r2(X0))
| ~ c(u5r3(X0))
| ~ f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1384,f82]) ).
fof(f1386,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r1(X0))
| ~ c(u5r3(X0))
| ~ f(X0)
| equalish(u5r3(X0),u5r1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1377]) ).
fof(f1387,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r1(X0))
| ~ c(u5r3(X0))
| ~ f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1386,f81]) ).
fof(f1388,plain,
( r2most(exist)
| ~ c(u4r1(exist))
| ~ c(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f912,f119]) ).
fof(f1389,plain,
( r2most(exist)
| ~ c(u4r2(exist))
| ~ c(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f912,f117]) ).
fof(f1403,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ c(u5r2(X0))
| ~ c(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r2(X0)) ),
inference(resolution,[status(thm)],[f912,f84]) ).
fof(f1404,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ c(u5r1(X0))
| ~ c(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r1(X0)) ),
inference(resolution,[status(thm)],[f912,f83]) ).
fof(f1405,definition,
( sQ89_spl
<=> c(u5r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1408,plain,
( sQ5_spl
| ~ sQ32_spl
| ~ sQ89_spl
| ~ sQ0_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1388,f1313,f708,f1405,f861,f723]) ).
fof(f1409,plain,
( sQ5_spl
| ~ sQ20_spl
| ~ sQ89_spl
| ~ sQ0_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1389,f1320,f708,f1405,f784,f723]) ).
fof(f1411,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r2(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1403]) ).
fof(f1412,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r1(X0))
| ~ c(u5r2(X0))
| ~ f(X0)
| equalish(u5r2(X0),u5r1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1404]) ).
fof(f1413,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r1(X0))
| ~ c(u5r2(X0))
| ~ f(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1412,f80]) ).
fof(f1414,plain,
( r2most(exist)
| ~ c(u4r1(exist))
| ~ c(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f913,f119]) ).
fof(f1415,plain,
( r2most(exist)
| ~ c(u4r2(exist))
| ~ c(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f913,f117]) ).
fof(f1430,plain,
! [X0] :
( r2most(X0)
| r2most(X0)
| ~ c(u5r1(X0))
| ~ c(u5r1(X0))
| ~ f(X0)
| equalish(u5r1(X0),u5r1(X0)) ),
inference(resolution,[status(thm)],[f913,f83]) ).
fof(f1431,definition,
( sQ90_spl
<=> c(u5r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1434,plain,
( sQ5_spl
| ~ sQ32_spl
| ~ sQ90_spl
| ~ sQ0_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f1414,f1346,f708,f1431,f861,f723]) ).
fof(f1435,plain,
( sQ5_spl
| ~ sQ20_spl
| ~ sQ90_spl
| ~ sQ0_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f1415,f1353,f708,f1431,f784,f723]) ).
fof(f1438,plain,
! [X0] :
( r2most(X0)
| ~ c(u5r1(X0))
| ~ f(X0)
| equalish(u5r1(X0),u5r1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1430]) ).
fof(f1545,plain,
! [X0] :
( c(u6r1(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| equalish(u6r3(X0),u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f245,f98]) ).
fof(f1562,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| c(u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1545]) ).
fof(f1677,plain,
! [X0] :
( c(u6r1(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| equalish(u6r4(X0),u6r4(X0))
| c(u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f268,f99]) ).
fof(f1694,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| c(u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1677]) ).
fof(f1808,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r1(exist))
| equalish(u6r4(exist),u4r1(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f276,f119]) ).
fof(f1809,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r2(exist))
| equalish(u6r4(exist),u4r2(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f276,f117]) ).
fof(f1825,plain,
( ~ sQ5_spl
| sQ22_spl
| sQ23_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1808,f708,f711,f818,f815,f723]) ).
fof(f1826,plain,
( ~ sQ5_spl
| sQ3_spl
| sQ4_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1809,f708,f711,f720,f717,f723]) ).
fof(f1878,plain,
( equalish(u6r3(exist),u6r3(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f1562,f115]) ).
fof(f1879,plain,
( sQ53_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1878,f708,f711,f1031]) ).
fof(f1880,plain,
( equalish(u6r4(exist),u6r4(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f1694,f115]) ).
fof(f1881,plain,
( sQ59_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1880,f708,f711,f1079]) ).
fof(f2027,plain,
! [X0] :
( c(u6r2(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| equalish(u6r3(X0),u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f302,f103]) ).
fof(f2044,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| c(u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2027]) ).
fof(f2122,plain,
! [X0] :
( c(u6r2(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| equalish(u6r4(X0),u6r4(X0))
| c(u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f325,f104]) ).
fof(f2139,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| c(u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2122]) ).
fof(f2216,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r1(exist))
| equalish(u6r4(exist),u4r1(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f332,f119]) ).
fof(f2217,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r2(exist))
| equalish(u6r4(exist),u4r2(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f332,f117]) ).
fof(f2233,plain,
( ~ sQ5_spl
| sQ22_spl
| sQ23_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2216,f708,f765,f818,f815,f723]) ).
fof(f2234,plain,
( ~ sQ5_spl
| sQ3_spl
| sQ4_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2217,f708,f765,f720,f717,f723]) ).
fof(f2267,definition,
( sQ91_spl
<=> equalish(u6r1(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2268,plain,
( ~ sQ91_spl
| equalish(u6r1(exist),u6r2(exist)) ),
inference(component_clause,[status(thm)],[f2267]) ).
fof(f2336,definition,
( sQ92_spl
<=> equalish(u6r1(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2337,plain,
( ~ sQ92_spl
| equalish(u6r1(exist),u6r1(exist)) ),
inference(component_clause,[status(thm)],[f2336]) ).
fof(f2358,plain,
! [X0] :
( d(u6r3(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r1(X0),u6r1(X0))
| equalish(u6r1(X0),u6r1(X0))
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f353,f106]) ).
fof(f2375,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r1(X0),u6r1(X0))
| d(u6r3(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2358]) ).
fof(f2421,plain,
! [X0] :
( d(u6r4(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r1(X0),u6r1(X0))
| equalish(u6r1(X0),u6r1(X0))
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f379,f107]) ).
fof(f2438,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r1(X0),u6r1(X0))
| d(u6r4(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2421]) ).
fof(f2465,definition,
( sQ93_spl
<=> equalish(u6r2(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f2466,plain,
( ~ sQ93_spl
| equalish(u6r2(exist),u6r2(exist)) ),
inference(component_clause,[status(thm)],[f2465]) ).
fof(f2484,plain,
( ~ sQ1_spl
| s(u6r1(exist),u1r2(u6r1(exist))) ),
inference(resolution,[status(thm)],[f870,f61]) ).
fof(f2485,plain,
( ~ sQ1_spl
| s(u6r1(exist),u1r1(u6r1(exist))) ),
inference(resolution,[status(thm)],[f870,f60]) ).
fof(f2487,plain,
( ~ sQ16_spl
| s2least(u6r2(exist)) ),
inference(resolution,[status(thm)],[f766,f57]) ).
fof(f2488,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ9_spl
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f858]) ).
fof(f2489,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ9_spl
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f781]) ).
fof(f2495,plain,
( ~ sQ9_spl
| ~ r2most(exist)
| equalish(u6r3(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f332]) ).
fof(f2498,plain,
( ~ sQ9_spl
| ~ r2most(exist)
| equalish(u6r3(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f276]) ).
fof(f2499,plain,
( ~ sQ9_spl
| r2most(exist)
| ~ c(u6r1(exist))
| ~ c(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f913]) ).
fof(f2500,plain,
( ~ sQ9_spl
| r2most(exist)
| ~ c(u6r1(exist))
| ~ c(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f912]) ).
fof(f2501,plain,
( ~ sQ9_spl
| r2most(exist)
| ~ c(u6r1(exist))
| ~ c(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f911]) ).
fof(f2502,plain,
( ~ sQ9_spl
| r2most(exist)
| ~ d(u6r1(exist))
| ~ d(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f888]) ).
fof(f2503,plain,
( ~ sQ9_spl
| r2most(exist)
| ~ d(u6r1(exist))
| ~ d(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f887]) ).
fof(f2504,plain,
( ~ sQ9_spl
| r2most(exist)
| ~ d(u6r1(exist))
| ~ d(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f739,f886]) ).
fof(f2505,plain,
! [X0] :
( ~ sQ9_spl
| ~ c(X0)
| ~ c(u6r1(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u6r1(exist),X0) ),
inference(resolution,[status(thm)],[f739,f89]) ).
fof(f2506,plain,
! [X0] :
( ~ sQ9_spl
| ~ d(X0)
| ~ d(u6r1(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u6r1(exist),X0) ),
inference(resolution,[status(thm)],[f739,f87]) ).
fof(f2507,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u6r1(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f207]) ).
fof(f2508,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u6r1(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f202]) ).
fof(f2511,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r1(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f186]) ).
fof(f2512,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r1(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f180]) ).
fof(f2515,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u6r1(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f144]) ).
fof(f2516,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u6r1(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f142]) ).
fof(f2517,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u6r1(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f140]) ).
fof(f2518,plain,
! [X0] :
( ~ sQ9_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r1(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u6r1(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f138]) ).
fof(f2519,plain,
( ~ sQ9_spl
| ~ d(u6r1(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f164]) ).
fof(f2520,plain,
( ~ sQ9_spl
| ~ d(u6r1(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f739,f148]) ).
fof(f2521,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ r(exist,X1)
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(X0,X1)
| equalish(u6r1(exist),X1)
| equalish(u6r1(exist),X0) ),
inference(resolution,[status(thm)],[f739,f79]) ).
fof(f2522,plain,
! [X0] :
( ~ sQ9_spl
| ~ d(X0)
| ~ r(exist,X0)
| ~ c(u6r1(exist))
| ~ r2most(exist)
| e(exist) ),
inference(resolution,[status(thm)],[f739,f77]) ).
fof(f2523,plain,
( ~ sQ31_spl
| ~ sQ9_spl
| sQ29_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f2488,f1138,f843,f738,f857]) ).
fof(f2524,plain,
( ~ sQ19_spl
| ~ sQ9_spl
| sQ15_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f2489,f958,f760,f738,f780]) ).
fof(f2525,definition,
( sQ94_spl
<=> equalish(u6r2(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f2526,plain,
( ~ sQ94_spl
| equalish(u6r2(exist),u6r1(exist)) ),
inference(component_clause,[status(thm)],[f2525]) ).
fof(f2533,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ52_spl
| sQ58_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2495,f708,f765,f1074,f1022,f723,f738]) ).
fof(f2536,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ52_spl
| sQ58_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2498,f708,f711,f1074,f1022,f723,f738]) ).
fof(f2537,definition,
( sQ95_spl
<=> equalish(u5r1(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f2540,plain,
( ~ sQ9_spl
| sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ0_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2499,f2537,f708,f1431,f711,f723,f738]) ).
fof(f2541,definition,
( sQ96_spl
<=> equalish(u5r2(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f2544,plain,
( ~ sQ9_spl
| sQ5_spl
| ~ sQ1_spl
| ~ sQ89_spl
| ~ sQ0_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f2500,f2541,f708,f1405,f711,f723,f738]) ).
fof(f2545,definition,
( sQ97_spl
<=> equalish(u5r3(exist),u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f2548,plain,
( ~ sQ9_spl
| sQ5_spl
| ~ sQ1_spl
| ~ sQ88_spl
| ~ sQ0_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f2501,f2545,f708,f1378,f711,f723,f738]) ).
fof(f2549,definition,
( sQ98_spl
<=> d(u6r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2552,plain,
( ~ sQ9_spl
| sQ5_spl
| ~ sQ98_spl
| ~ sQ86_spl
| ~ sQ0_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2502,f2537,f708,f1349,f2549,f723,f738]) ).
fof(f2553,plain,
( ~ sQ9_spl
| sQ5_spl
| ~ sQ98_spl
| ~ sQ83_spl
| ~ sQ0_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f2503,f2541,f708,f1316,f2549,f723,f738]) ).
fof(f2554,plain,
( ~ sQ9_spl
| sQ5_spl
| ~ sQ98_spl
| ~ sQ80_spl
| ~ sQ0_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f2504,f2545,f708,f1282,f2549,f723,f738]) ).
fof(f2555,definition,
! [X0] :
( sQ99_spl
<=> ( ~ c(X0)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2558,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ0_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f2505,f2555,f708,f711,f738]) ).
fof(f2559,definition,
! [X0] :
( sQ100_spl
<=> ( ~ d(X0)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f2562,plain,
( ~ sQ9_spl
| ~ sQ98_spl
| ~ sQ0_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f2506,f2559,f708,f2549,f738]) ).
fof(f2563,definition,
! [X0] :
( sQ101_spl
<=> ( ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u6r4(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2566,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ101_spl
| sQ58_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2507,f708,f727,f1074,f2563,f723,f738]) ).
fof(f2567,definition,
! [X0] :
( sQ102_spl
<=> ( ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u6r3(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2570,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ102_spl
| sQ52_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2508,f708,f727,f1022,f2567,f723,f738]) ).
fof(f2573,definition,
! [X0] :
( sQ103_spl
<=> ( ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f2576,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ103_spl
| sQ94_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2511,f708,f743,f2525,f2573,f723,f738]) ).
fof(f2577,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ103_spl
| sQ94_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2512,f708,f753,f2525,f2573,f723,f738]) ).
fof(f2583,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ101_spl
| sQ58_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2515,f708,f765,f1074,f2563,f723,f738]) ).
fof(f2584,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ102_spl
| sQ52_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2516,f708,f765,f1022,f2567,f723,f738]) ).
fof(f2585,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ101_spl
| sQ58_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2517,f708,f711,f1074,f2563,f723,f738]) ).
fof(f2586,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ102_spl
| sQ52_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2518,f708,f711,f1022,f2567,f723,f738]) ).
fof(f2587,plain,
( ~ sQ9_spl
| ~ sQ98_spl
| ~ sQ5_spl
| sQ17_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2519,f708,f743,f772,f723,f2549,f738]) ).
fof(f2588,plain,
( ~ sQ9_spl
| ~ sQ98_spl
| ~ sQ5_spl
| sQ17_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2520,f708,f753,f772,f723,f2549,f738]) ).
fof(f2589,definition,
! [X0,X1] :
( sQ105_spl
<=> ( ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u6r1(exist),X1)
| equalish(u6r1(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f2590,plain,
! [X0,X1] :
( ~ sQ105_spl
| ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u6r1(exist),X1)
| equalish(u6r1(exist),X0) ),
inference(component_clause,[status(thm)],[f2589]) ).
fof(f2592,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f2521,f2589,f723,f738]) ).
fof(f2593,plain,
( ~ sQ9_spl
| sQ21_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f2522,f772,f723,f711,f787,f738]) ).
fof(f2594,plain,
( ~ sQ16_spl
| s(u6r2(exist),u1r2(u6r2(exist))) ),
inference(resolution,[status(thm)],[f2487,f61]) ).
fof(f2595,plain,
( ~ sQ16_spl
| s(u6r2(exist),u1r1(u6r2(exist))) ),
inference(resolution,[status(thm)],[f2487,f60]) ).
fof(f2597,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ6_spl
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u4r1(exist),X0)
| equalish(u4r1(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f858]) ).
fof(f2598,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ6_spl
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u4r2(exist),X0)
| equalish(u4r2(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f781]) ).
fof(f2604,plain,
( ~ sQ6_spl
| ~ r2most(exist)
| equalish(u6r3(exist),u6r2(exist))
| equalish(u6r4(exist),u6r2(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f332]) ).
fof(f2607,plain,
( ~ sQ6_spl
| ~ r2most(exist)
| equalish(u6r3(exist),u6r2(exist))
| equalish(u6r4(exist),u6r2(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f276]) ).
fof(f2608,plain,
( ~ sQ6_spl
| r2most(exist)
| ~ c(u6r2(exist))
| ~ c(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f913]) ).
fof(f2609,plain,
( ~ sQ6_spl
| r2most(exist)
| ~ c(u6r2(exist))
| ~ c(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f912]) ).
fof(f2610,plain,
( ~ sQ6_spl
| r2most(exist)
| ~ c(u6r2(exist))
| ~ c(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f911]) ).
fof(f2611,plain,
( ~ sQ6_spl
| r2most(exist)
| ~ d(u6r2(exist))
| ~ d(u5r1(exist))
| ~ f(exist)
| equalish(u5r1(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f888]) ).
fof(f2612,plain,
( ~ sQ6_spl
| r2most(exist)
| ~ d(u6r2(exist))
| ~ d(u5r2(exist))
| ~ f(exist)
| equalish(u5r2(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f887]) ).
fof(f2613,plain,
( ~ sQ6_spl
| r2most(exist)
| ~ d(u6r2(exist))
| ~ d(u5r3(exist))
| ~ f(exist)
| equalish(u5r3(exist),u6r2(exist)) ),
inference(resolution,[status(thm)],[f728,f886]) ).
fof(f2614,plain,
! [X0] :
( ~ sQ6_spl
| ~ c(X0)
| ~ c(u6r2(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u6r2(exist),X0) ),
inference(resolution,[status(thm)],[f728,f89]) ).
fof(f2615,plain,
! [X0] :
( ~ sQ6_spl
| ~ d(X0)
| ~ d(u6r2(exist))
| ~ r(exist,X0)
| ~ f(exist)
| equalish(u6r2(exist),X0) ),
inference(resolution,[status(thm)],[f728,f87]) ).
fof(f2618,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u6r2(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f197]) ).
fof(f2619,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u6r2(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f192]) ).
fof(f2622,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r1(exist),X0)
| equalish(u6r1(exist),u6r2(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f161]) ).
fof(f2623,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r1(exist),X0)
| equalish(u6r1(exist),u6r2(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f146]) ).
fof(f2624,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u6r2(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f144]) ).
fof(f2625,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u6r2(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f142]) ).
fof(f2626,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r4(exist),X0)
| equalish(u6r4(exist),u6r2(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f140]) ).
fof(f2627,plain,
! [X0] :
( ~ sQ6_spl
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(u6r2(exist),X0)
| equalish(u6r3(exist),X0)
| equalish(u6r3(exist),u6r2(exist))
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f138]) ).
fof(f2628,plain,
( ~ sQ6_spl
| ~ d(u6r2(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f164]) ).
fof(f2629,plain,
( ~ sQ6_spl
| ~ d(u6r2(exist))
| ~ r2most(exist)
| e(exist)
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f728,f148]) ).
fof(f2630,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ r(exist,X1)
| ~ r(exist,X0)
| ~ r2most(exist)
| equalish(X0,X1)
| equalish(u6r2(exist),X1)
| equalish(u6r2(exist),X0) ),
inference(resolution,[status(thm)],[f728,f79]) ).
fof(f2631,plain,
! [X0] :
( ~ sQ6_spl
| ~ d(X0)
| ~ r(exist,X0)
| ~ c(u6r2(exist))
| ~ r2most(exist)
| e(exist) ),
inference(resolution,[status(thm)],[f728,f77]) ).
fof(f2632,plain,
( ~ sQ31_spl
| ~ sQ6_spl
| sQ27_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f2597,f1133,f835,f727,f857]) ).
fof(f2633,plain,
( ~ sQ19_spl
| ~ sQ6_spl
| sQ12_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f2598,f953,f749,f727,f780]) ).
fof(f2639,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ51_spl
| sQ57_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2604,f708,f765,f1069,f1017,f723,f727]) ).
fof(f2642,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ51_spl
| sQ57_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2607,f708,f711,f1069,f1017,f723,f727]) ).
fof(f2643,definition,
( sQ106_spl
<=> equalish(u5r1(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f2646,plain,
( ~ sQ6_spl
| sQ5_spl
| ~ sQ16_spl
| ~ sQ90_spl
| ~ sQ0_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f2608,f2643,f708,f1431,f765,f723,f727]) ).
fof(f2647,definition,
( sQ107_spl
<=> equalish(u5r2(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f2650,plain,
( ~ sQ6_spl
| sQ5_spl
| ~ sQ16_spl
| ~ sQ89_spl
| ~ sQ0_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f2609,f2647,f708,f1405,f765,f723,f727]) ).
fof(f2651,definition,
( sQ108_spl
<=> equalish(u5r3(exist),u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f2654,plain,
( ~ sQ6_spl
| sQ5_spl
| ~ sQ16_spl
| ~ sQ88_spl
| ~ sQ0_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f2610,f2651,f708,f1378,f765,f723,f727]) ).
fof(f2655,definition,
( sQ109_spl
<=> d(u6r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f2658,plain,
( ~ sQ6_spl
| sQ5_spl
| ~ sQ109_spl
| ~ sQ86_spl
| ~ sQ0_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f2611,f2643,f708,f1349,f2655,f723,f727]) ).
fof(f2659,plain,
( ~ sQ6_spl
| sQ5_spl
| ~ sQ109_spl
| ~ sQ83_spl
| ~ sQ0_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f2612,f2647,f708,f1316,f2655,f723,f727]) ).
fof(f2660,plain,
( ~ sQ6_spl
| sQ5_spl
| ~ sQ109_spl
| ~ sQ80_spl
| ~ sQ0_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f2613,f2651,f708,f1282,f2655,f723,f727]) ).
fof(f2661,definition,
! [X0] :
( sQ110_spl
<=> ( ~ c(X0)
| ~ r(exist,X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f2664,plain,
( ~ sQ6_spl
| ~ sQ16_spl
| ~ sQ0_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f2614,f2661,f708,f765,f727]) ).
fof(f2665,definition,
! [X0] :
( sQ111_spl
<=> ( ~ d(X0)
| ~ r(exist,X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f2668,plain,
( ~ sQ6_spl
| ~ sQ109_spl
| ~ sQ0_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f2615,f2665,f708,f2655,f727]) ).
fof(f2669,definition,
! [X0] :
( sQ112_spl
<=> ( ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u6r4(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f2670,plain,
! [X0] :
( ~ sQ112_spl
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u6r4(exist),X0) ),
inference(component_clause,[status(thm)],[f2669]) ).
fof(f2673,definition,
! [X0] :
( sQ113_spl
<=> ( ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u6r3(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f2674,plain,
! [X0] :
( ~ sQ113_spl
| ~ r(exist,X0)
| equalish(u6r2(exist),X0)
| equalish(u6r3(exist),X0) ),
inference(component_clause,[status(thm)],[f2673]) ).
fof(f2677,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ112_spl
| sQ57_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2618,f708,f738,f1069,f2669,f723,f727]) ).
fof(f2678,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ113_spl
| sQ51_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2619,f708,f738,f1017,f2673,f723,f727]) ).
fof(f2684,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ103_spl
| sQ91_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2622,f708,f743,f2267,f2573,f723,f727]) ).
fof(f2685,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ103_spl
| sQ91_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2623,f708,f753,f2267,f2573,f723,f727]) ).
fof(f2686,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ112_spl
| sQ57_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2624,f708,f765,f1069,f2669,f723,f727]) ).
fof(f2687,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ113_spl
| sQ51_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2625,f708,f765,f1017,f2673,f723,f727]) ).
fof(f2688,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ112_spl
| sQ57_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2626,f708,f711,f1069,f2669,f723,f727]) ).
fof(f2689,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ113_spl
| sQ51_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2627,f708,f711,f1017,f2673,f723,f727]) ).
fof(f2690,plain,
( ~ sQ6_spl
| ~ sQ109_spl
| ~ sQ5_spl
| sQ17_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2628,f708,f743,f772,f723,f2655,f727]) ).
fof(f2691,plain,
( ~ sQ6_spl
| ~ sQ109_spl
| ~ sQ5_spl
| sQ17_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2629,f708,f753,f772,f723,f2655,f727]) ).
fof(f2692,definition,
! [X0,X1] :
( sQ115_spl
<=> ( ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u6r2(exist),X1)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f2693,plain,
! [X0,X1] :
( ~ sQ115_spl
| ~ r(exist,X1)
| ~ r(exist,X0)
| equalish(X0,X1)
| equalish(u6r2(exist),X1)
| equalish(u6r2(exist),X0) ),
inference(component_clause,[status(thm)],[f2692]) ).
fof(f2695,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f2630,f2692,f723,f727]) ).
fof(f2696,plain,
( ~ sQ6_spl
| sQ21_spl
| ~ sQ16_spl
| ~ sQ5_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f2631,f772,f723,f765,f787,f727]) ).
fof(f2697,plain,
( sQ9_spl
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f740,f107]) ).
fof(f2698,plain,
( sQ9_spl
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f740,f106]) ).
fof(f2699,plain,
( sQ9_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2697,f708,f743,f738]) ).
fof(f2700,plain,
( sQ9_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2698,f708,f753,f738]) ).
fof(f2701,plain,
! [X0] :
( ~ s(u4r1(exist),X0)
| equalish(u1r2(u4r1(exist)),X0)
| s2least(u4r1(exist)) ),
inference(resolution,[status(thm)],[f866,f63]) ).
fof(f2702,plain,
! [X0] :
( ~ s(u4r1(exist),X0)
| ~ s1most(u4r1(exist))
| equalish(u1r2(u4r1(exist)),X0) ),
inference(resolution,[status(thm)],[f866,f67]) ).
fof(f2703,definition,
( sQ116_spl
<=> s2least(u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f2706,definition,
! [X0] :
( sQ117_spl
<=> ( ~ s(u4r1(exist),X0)
| equalish(u1r2(u4r1(exist)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f2707,plain,
! [X0] :
( ~ sQ117_spl
| ~ s(u4r1(exist),X0)
| equalish(u1r2(u4r1(exist)),X0) ),
inference(component_clause,[status(thm)],[f2706]) ).
fof(f2709,plain,
( sQ117_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f2701,f2703,f2706]) ).
fof(f2710,definition,
( sQ118_spl
<=> s1most(u4r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f2712,plain,
( sQ118_spl
| ~ s1most(u4r1(exist)) ),
inference(component_clause,[status(thm)],[f2710]) ).
fof(f2713,plain,
( ~ sQ118_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f2702,f2706,f2710]) ).
fof(f2714,plain,
! [X0] :
( s2least(u5r3(X0))
| r2most(X0)
| ~ d(u5r2(X0))
| ~ f(X0) ),
inference(resolution,[status(thm)],[f1292,f215]) ).
fof(f2715,plain,
! [X0] :
( s2least(u5r3(X0))
| r2most(X0)
| ~ d(u5r1(X0))
| ~ f(X0) ),
inference(resolution,[status(thm)],[f1294,f215]) ).
fof(f2716,plain,
! [X0] :
( s2least(u5r1(X0))
| r2most(X0)
| ~ d(u5r2(X0))
| ~ f(X0) ),
inference(resolution,[status(thm)],[f1327,f215]) ).
fof(f2717,plain,
! [X0] :
( ~ sQ115_spl
| ~ r(exist,X0)
| equalish(u4r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f2693,f119]) ).
fof(f2718,plain,
! [X0] :
( ~ sQ115_spl
| ~ r(exist,X0)
| equalish(u4r2(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f2693,f117]) ).
fof(f2721,plain,
! [X0] :
( ~ sQ115_spl
| d(u6r4(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f2693,f107]) ).
fof(f2722,plain,
! [X0] :
( ~ sQ115_spl
| d(u6r3(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f2693,f106]) ).
fof(f2723,plain,
! [X0] :
( ~ sQ115_spl
| r(exist,u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2693,f114]) ).
fof(f2724,plain,
! [X0] :
( ~ sQ115_spl
| r(exist,u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2693,f109]) ).
fof(f2725,plain,
! [X0] :
( ~ sQ115_spl
| c(u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2693,f104]) ).
fof(f2726,plain,
! [X0] :
( ~ sQ115_spl
| c(u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r4(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2693,f99]) ).
fof(f2727,plain,
! [X0] :
( ~ sQ115_spl
| r(exist,u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2693,f113]) ).
fof(f2728,plain,
! [X0] :
( ~ sQ115_spl
| r(exist,u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2693,f108]) ).
fof(f2729,plain,
! [X0] :
( ~ sQ115_spl
| c(u6r2(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2693,f103]) ).
fof(f2730,plain,
! [X0] :
( ~ sQ115_spl
| c(u6r1(exist))
| f(exist)
| ~ r(exist,X0)
| equalish(u6r3(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2693,f98]) ).
fof(f2731,plain,
! [X0] :
( ~ sQ115_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r3(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f2693,f85]) ).
fof(f2732,plain,
! [X0] :
( ~ sQ115_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r2(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f2693,f84]) ).
fof(f2733,plain,
! [X0] :
( ~ sQ115_spl
| r2most(exist)
| ~ r(exist,X0)
| equalish(u5r1(exist),X0)
| equalish(u6r2(exist),X0)
| equalish(u6r2(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f2693,f83]) ).
fof(f2734,plain,
( ~ sQ115_spl
| sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f2717,f832,f835,f2692]) ).
fof(f2735,plain,
( ~ sQ115_spl
| sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2718,f746,f749,f2692]) ).
fof(f2738,plain,
( ~ sQ115_spl
| sQ10_spl
| sQ0_spl
| sQ103_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f2721,f2525,f2573,f708,f743,f2692]) ).
fof(f2739,plain,
( ~ sQ115_spl
| sQ13_spl
| sQ0_spl
| sQ103_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f2722,f2525,f2573,f708,f753,f2692]) ).
fof(f2740,definition,
( sQ119_spl
<=> equalish(u6r2(exist),u6r4(exist)) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f2741,plain,
( ~ sQ119_spl
| equalish(u6r2(exist),u6r4(exist)) ),
inference(component_clause,[status(thm)],[f2740]) ).
fof(f2743,plain,
( ~ sQ115_spl
| sQ6_spl
| sQ0_spl
| sQ112_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f2723,f2740,f2669,f708,f727,f2692]) ).
fof(f2744,plain,
( ~ sQ115_spl
| sQ9_spl
| sQ0_spl
| sQ112_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f2724,f2740,f2669,f708,f738,f2692]) ).
fof(f2745,plain,
( ~ sQ115_spl
| sQ16_spl
| sQ0_spl
| sQ112_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f2725,f2740,f2669,f708,f765,f2692]) ).
fof(f2746,plain,
( ~ sQ115_spl
| sQ1_spl
| sQ0_spl
| sQ112_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f2726,f2740,f2669,f708,f711,f2692]) ).
fof(f2747,definition,
( sQ120_spl
<=> equalish(u6r2(exist),u6r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f2748,plain,
( ~ sQ120_spl
| equalish(u6r2(exist),u6r3(exist)) ),
inference(component_clause,[status(thm)],[f2747]) ).
fof(f2750,plain,
( ~ sQ115_spl
| sQ6_spl
| sQ0_spl
| sQ113_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f2727,f2747,f2673,f708,f727,f2692]) ).
fof(f2751,plain,
( ~ sQ115_spl
| sQ9_spl
| sQ0_spl
| sQ113_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f2728,f2747,f2673,f708,f738,f2692]) ).
fof(f2752,plain,
( ~ sQ115_spl
| sQ16_spl
| sQ0_spl
| sQ113_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f2729,f2747,f2673,f708,f765,f2692]) ).
fof(f2753,plain,
( ~ sQ115_spl
| sQ1_spl
| sQ0_spl
| sQ113_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f2730,f2747,f2673,f708,f711,f2692]) ).
fof(f2754,definition,
( sQ121_spl
<=> equalish(u6r2(exist),u5r3(exist)) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f2757,definition,
! [X0] :
( sQ122_spl
<=> ( ~ r(exist,X0)
| equalish(u5r3(exist),X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f2760,plain,
( ~ sQ115_spl
| sQ5_spl
| sQ122_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f2731,f2754,f2757,f723,f2692]) ).
fof(f2761,definition,
( sQ123_spl
<=> equalish(u6r2(exist),u5r2(exist)) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f2764,definition,
! [X0] :
( sQ124_spl
<=> ( ~ r(exist,X0)
| equalish(u5r2(exist),X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f2767,plain,
( ~ sQ115_spl
| sQ5_spl
| sQ124_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f2732,f2761,f2764,f723,f2692]) ).
fof(f2768,definition,
( sQ125_spl
<=> equalish(u6r2(exist),u5r1(exist)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f2771,definition,
! [X0] :
( sQ126_spl
<=> ( ~ r(exist,X0)
| equalish(u5r1(exist),X0)
| equalish(u6r2(exist),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f2774,plain,
( ~ sQ115_spl
| sQ5_spl
| sQ126_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f2733,f2768,f2771,f723,f2692]) ).
fof(f2775,plain,
( ~ sQ112_spl
| equalish(u6r2(exist),u4r1(exist))
| equalish(u6r4(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f2670,f119]) ).
fof(f2776,plain,
( ~ sQ112_spl
| equalish(u6r2(exist),u4r2(exist))
| equalish(u6r4(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f2670,f117]) ).
fof(f2779,plain,
( ~ sQ112_spl
| d(u6r4(exist))
| f(exist)
| equalish(u6r2(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f2670,f107]) ).
fof(f2780,plain,
( ~ sQ112_spl
| d(u6r3(exist))
| f(exist)
| equalish(u6r2(exist),u6r1(exist))
| equalish(u6r4(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f2670,f106]) ).
fof(f2785,plain,
( ~ sQ112_spl
| r(exist,u6r2(exist))
| f(exist)
| equalish(u6r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2670,f113]) ).
fof(f2786,plain,
( ~ sQ112_spl
| r(exist,u6r1(exist))
| f(exist)
| equalish(u6r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2670,f108]) ).
fof(f2787,plain,
( ~ sQ112_spl
| c(u6r2(exist))
| f(exist)
| equalish(u6r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2670,f103]) ).
fof(f2788,plain,
( ~ sQ112_spl
| c(u6r1(exist))
| f(exist)
| equalish(u6r2(exist),u6r3(exist))
| equalish(u6r4(exist),u6r3(exist)) ),
inference(resolution,[status(thm)],[f2670,f98]) ).
fof(f2789,plain,
( ~ sQ112_spl
| r2most(exist)
| equalish(u6r2(exist),u5r3(exist))
| equalish(u6r4(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f2670,f85]) ).
fof(f2790,plain,
( ~ sQ112_spl
| r2most(exist)
| equalish(u6r2(exist),u5r2(exist))
| equalish(u6r4(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f2670,f84]) ).
fof(f2791,plain,
( ~ sQ112_spl
| r2most(exist)
| equalish(u6r2(exist),u5r1(exist))
| equalish(u6r4(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f2670,f83]) ).
fof(f2792,plain,
( ~ sQ112_spl
| sQ26_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f2775,f818,f832,f2669]) ).
fof(f2793,plain,
( ~ sQ112_spl
| sQ11_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f2776,f720,f746,f2669]) ).
fof(f2796,plain,
( ~ sQ112_spl
| sQ10_spl
| sQ0_spl
| sQ94_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f2779,f1074,f2525,f708,f743,f2669]) ).
fof(f2797,plain,
( ~ sQ112_spl
| sQ13_spl
| sQ0_spl
| sQ94_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f2780,f1074,f2525,f708,f753,f2669]) ).
fof(f2802,plain,
( ~ sQ112_spl
| sQ6_spl
| sQ0_spl
| sQ120_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2785,f1086,f2747,f708,f727,f2669]) ).
fof(f2803,plain,
( ~ sQ112_spl
| sQ9_spl
| sQ0_spl
| sQ120_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2786,f1086,f2747,f708,f738,f2669]) ).
fof(f2804,plain,
( ~ sQ112_spl
| sQ16_spl
| sQ0_spl
| sQ120_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2787,f1086,f2747,f708,f765,f2669]) ).
fof(f2805,plain,
( ~ sQ112_spl
| sQ1_spl
| sQ0_spl
| sQ120_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2788,f1086,f2747,f708,f711,f2669]) ).
fof(f2806,plain,
( ~ sQ112_spl
| sQ5_spl
| sQ121_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f2789,f1093,f2754,f723,f2669]) ).
fof(f2807,plain,
( ~ sQ112_spl
| sQ5_spl
| sQ123_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f2790,f1097,f2761,f723,f2669]) ).
fof(f2808,plain,
( ~ sQ112_spl
| sQ5_spl
| sQ125_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f2791,f1101,f2768,f723,f2669]) ).
fof(f2809,plain,
( ~ sQ113_spl
| equalish(u6r2(exist),u4r1(exist))
| equalish(u6r3(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[f2674,f119]) ).
fof(f2810,plain,
( ~ sQ113_spl
| equalish(u6r2(exist),u4r2(exist))
| equalish(u6r3(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[f2674,f117]) ).
fof(f2813,plain,
( ~ sQ113_spl
| d(u6r4(exist))
| f(exist)
| equalish(u6r2(exist),u6r1(exist))
| equalish(u6r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f2674,f107]) ).
fof(f2814,plain,
( ~ sQ113_spl
| d(u6r3(exist))
| f(exist)
| equalish(u6r2(exist),u6r1(exist))
| equalish(u6r3(exist),u6r1(exist)) ),
inference(resolution,[status(thm)],[f2674,f106]) ).
fof(f2815,plain,
( ~ sQ113_spl
| r(exist,u6r2(exist))
| f(exist)
| equalish(u6r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2674,f114]) ).
fof(f2816,plain,
( ~ sQ113_spl
| r(exist,u6r1(exist))
| f(exist)
| equalish(u6r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2674,f109]) ).
fof(f2817,plain,
( ~ sQ113_spl
| c(u6r2(exist))
| f(exist)
| equalish(u6r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2674,f104]) ).
fof(f2818,plain,
( ~ sQ113_spl
| c(u6r1(exist))
| f(exist)
| equalish(u6r2(exist),u6r4(exist))
| equalish(u6r3(exist),u6r4(exist)) ),
inference(resolution,[status(thm)],[f2674,f99]) ).
fof(f2823,plain,
( ~ sQ113_spl
| r2most(exist)
| equalish(u6r2(exist),u5r3(exist))
| equalish(u6r3(exist),u5r3(exist)) ),
inference(resolution,[status(thm)],[f2674,f85]) ).
fof(f2824,plain,
( ~ sQ113_spl
| r2most(exist)
| equalish(u6r2(exist),u5r2(exist))
| equalish(u6r3(exist),u5r2(exist)) ),
inference(resolution,[status(thm)],[f2674,f84]) ).
fof(f2825,plain,
( ~ sQ113_spl
| r2most(exist)
| equalish(u6r2(exist),u5r1(exist))
| equalish(u6r3(exist),u5r1(exist)) ),
inference(resolution,[status(thm)],[f2674,f83]) ).
fof(f2826,plain,
( ~ sQ113_spl
| sQ26_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f2809,f815,f832,f2673]) ).
fof(f2827,plain,
( ~ sQ113_spl
| sQ11_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2810,f717,f746,f2673]) ).
fof(f2830,plain,
( ~ sQ113_spl
| sQ10_spl
| sQ0_spl
| sQ94_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f2813,f1022,f2525,f708,f743,f2673]) ).
fof(f2831,plain,
( ~ sQ113_spl
| sQ13_spl
| sQ0_spl
| sQ94_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f2814,f1022,f2525,f708,f753,f2673]) ).
fof(f2832,plain,
( ~ sQ113_spl
| sQ6_spl
| sQ0_spl
| sQ119_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2815,f714,f2740,f708,f727,f2673]) ).
fof(f2833,plain,
( ~ sQ113_spl
| sQ9_spl
| sQ0_spl
| sQ119_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2816,f714,f2740,f708,f738,f2673]) ).
fof(f2834,plain,
( ~ sQ113_spl
| sQ16_spl
| sQ0_spl
| sQ119_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2817,f714,f2740,f708,f765,f2673]) ).
fof(f2835,plain,
( ~ sQ113_spl
| sQ1_spl
| sQ0_spl
| sQ119_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2818,f714,f2740,f708,f711,f2673]) ).
fof(f2840,plain,
( ~ sQ113_spl
| sQ5_spl
| sQ121_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f2823,f1038,f2754,f723,f2673]) ).
fof(f2841,plain,
( ~ sQ113_spl
| sQ5_spl
| sQ123_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f2824,f1042,f2761,f723,f2673]) ).
fof(f2842,plain,
( ~ sQ113_spl
| sQ5_spl
| sQ125_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f2825,f1046,f2768,f723,f2673]) ).
fof(f2843,plain,
! [X0] :
( s2least(u5r2(X0))
| s2least(u5r3(X0))
| r2most(X0)
| ~ f(X0) ),
inference(resolution,[status(thm)],[f2714,f215]) ).
fof(f2847,plain,
! [X0] :
( d(u6r3(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r2(X0),u6r2(X0))
| equalish(u6r2(X0),u6r2(X0))
| d(u6r3(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f405,f111]) ).
fof(f2864,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r2(X0),u6r2(X0))
| d(u6r3(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2847]) ).
fof(f2910,plain,
( ~ r2most(exist)
| equalish(u6r1(exist),u4r1(exist))
| equalish(u6r2(exist),u4r1(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f409,f119]) ).
fof(f2911,plain,
( ~ r2most(exist)
| equalish(u6r1(exist),u4r2(exist))
| equalish(u6r2(exist),u4r2(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f409,f117]) ).
fof(f2927,plain,
( ~ sQ5_spl
| sQ28_spl
| sQ26_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2910,f708,f753,f832,f840,f723]) ).
fof(f2928,plain,
( ~ sQ5_spl
| sQ14_spl
| sQ11_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2911,f708,f753,f746,f757,f723]) ).
fof(f2945,plain,
! [X0] :
( d(u6r4(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r2(X0),u6r2(X0))
| equalish(u6r2(X0),u6r2(X0))
| d(u6r4(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f433,f112]) ).
fof(f2962,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r2(X0),u6r2(X0))
| d(u6r4(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2945]) ).
fof(f2976,plain,
( ~ r2most(exist)
| equalish(u6r1(exist),u4r1(exist))
| equalish(u6r2(exist),u4r1(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f436,f119]) ).
fof(f2977,plain,
( ~ r2most(exist)
| equalish(u6r1(exist),u4r2(exist))
| equalish(u6r2(exist),u4r2(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f436,f117]) ).
fof(f2993,plain,
( ~ sQ5_spl
| sQ28_spl
| sQ26_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2976,f708,f743,f832,f840,f723]) ).
fof(f2994,plain,
( ~ sQ5_spl
| sQ14_spl
| sQ11_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2977,f708,f743,f746,f757,f723]) ).
fof(f3043,plain,
! [X0] :
( s2least(u5r1(X0))
| s2least(u5r3(X0))
| r2most(X0)
| ~ f(X0) ),
inference(resolution,[status(thm)],[f2715,f215]) ).
fof(f3044,plain,
! [X0] :
( s2least(u5r2(X0))
| s2least(u5r1(X0))
| r2most(X0)
| ~ f(X0) ),
inference(resolution,[status(thm)],[f2716,f215]) ).
fof(f3045,plain,
( equalish(u6r3(exist),u6r3(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f2044,f115]) ).
fof(f3046,plain,
( sQ53_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3045,f708,f765,f1031]) ).
fof(f3047,plain,
( equalish(u6r4(exist),u6r4(exist))
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f2139,f115]) ).
fof(f3048,plain,
( sQ59_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3047,f708,f765,f1079]) ).
fof(f3124,plain,
! [X0] :
( r(X0,u6r1(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f471,f108]) ).
fof(f3141,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3124]) ).
fof(f3184,plain,
! [X0] :
( r(X0,u6r1(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f494,f109]) ).
fof(f3201,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r1(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3184]) ).
fof(f3243,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r1(exist))
| equalish(u6r4(exist),u4r1(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f500,f119]) ).
fof(f3244,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r2(exist))
| equalish(u6r4(exist),u4r2(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f500,f117]) ).
fof(f3260,plain,
( ~ sQ5_spl
| sQ22_spl
| sQ23_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3243,f708,f738,f818,f815,f723]) ).
fof(f3261,plain,
( ~ sQ5_spl
| sQ3_spl
| sQ4_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3244,f708,f738,f720,f717,f723]) ).
fof(f3309,plain,
( equalish(u6r1(exist),u6r1(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f2375,f115]) ).
fof(f3310,plain,
( sQ92_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3309,f708,f753,f2336]) ).
fof(f3311,plain,
( equalish(u6r1(exist),u6r1(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f2438,f115]) ).
fof(f3312,plain,
( sQ92_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3311,f708,f743,f2336]) ).
fof(f3313,plain,
( equalish(u6r2(exist),u6r2(exist))
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f2864,f115]) ).
fof(f3314,plain,
( sQ93_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3313,f708,f753,f2465]) ).
fof(f3315,plain,
( equalish(u6r2(exist),u6r2(exist))
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f2962,f115]) ).
fof(f3316,plain,
( sQ93_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3315,f708,f743,f2465]) ).
fof(f3317,plain,
( equalish(u6r3(exist),u6r3(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f3141,f115]) ).
fof(f3318,plain,
( sQ53_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3317,f708,f738,f1031]) ).
fof(f3319,plain,
( equalish(u6r4(exist),u6r4(exist))
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f3201,f115]) ).
fof(f3320,plain,
( sQ59_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3319,f708,f738,f1079]) ).
fof(f3331,plain,
! [X0] :
( r(X0,u6r2(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f528,f113]) ).
fof(f3348,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r3(X0),u6r3(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3331]) ).
fof(f3358,plain,
! [X0] :
( r(X0,u6r2(X0))
| f(X0)
| ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(resolution,[status(thm)],[f551,f114]) ).
fof(f3375,plain,
! [X0] :
( ~ r2most(X0)
| equalish(u6r4(X0),u6r4(X0))
| r(X0,u6r2(X0))
| f(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3358]) ).
fof(f3384,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r1(exist))
| equalish(u6r4(exist),u4r1(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f556,f119]) ).
fof(f3385,plain,
( ~ r2most(exist)
| equalish(u6r3(exist),u4r2(exist))
| equalish(u6r4(exist),u4r2(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f556,f117]) ).
fof(f3401,plain,
( ~ sQ5_spl
| sQ22_spl
| sQ23_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3384,f708,f727,f818,f815,f723]) ).
fof(f3402,plain,
( ~ sQ5_spl
| sQ3_spl
| sQ4_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3385,f708,f727,f720,f717,f723]) ).
fof(f3416,plain,
( sQ6_spl
| d(u6r4(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f729,f112]) ).
fof(f3417,plain,
( sQ6_spl
| d(u6r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f729,f111]) ).
fof(f3418,plain,
( sQ6_spl
| sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3416,f708,f743,f727]) ).
fof(f3419,plain,
( sQ6_spl
| sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3417,f708,f753,f727]) ).
fof(f3420,plain,
! [X0] :
( ~ s(u4r1(exist),X0)
| equalish(u1r1(u4r1(exist)),X0)
| s2least(u4r1(exist)) ),
inference(resolution,[status(thm)],[f867,f63]) ).
fof(f3421,plain,
! [X0] :
( ~ s(u4r1(exist),X0)
| ~ s1most(u4r1(exist))
| equalish(u1r1(u4r1(exist)),X0) ),
inference(resolution,[status(thm)],[f867,f67]) ).
fof(f3422,definition,
! [X0] :
( sQ127_spl
<=> ( ~ s(u4r1(exist),X0)
| equalish(u1r1(u4r1(exist)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f3423,plain,
! [X0] :
( ~ sQ127_spl
| ~ s(u4r1(exist),X0)
| equalish(u1r1(u4r1(exist)),X0) ),
inference(component_clause,[status(thm)],[f3422]) ).
fof(f3425,plain,
( sQ127_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f3420,f2703,f3422]) ).
fof(f3426,plain,
( ~ sQ118_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f3421,f3422,f2710]) ).
fof(f3427,plain,
( equalish(u6r3(exist),u6r3(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f3348,f115]) ).
fof(f3428,plain,
( sQ53_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3427,f708,f727,f1031]) ).
fof(f3429,plain,
( equalish(u6r4(exist),u6r4(exist))
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f3375,f115]) ).
fof(f3430,plain,
( sQ59_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3429,f708,f727,f1079]) ).
fof(f3431,plain,
( ~ sQ60_spl
| ~ equalish(u6r2(exist),u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f1087,f90]) ).
fof(f3432,plain,
( ~ sQ60_spl
| r(exist,u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f1087,f110]) ).
fof(f3433,plain,
( ~ sQ60_spl
| r(exist,u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f1087,f105]) ).
fof(f3434,plain,
( ~ sQ60_spl
| c(u6r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f1087,f100]) ).
fof(f3435,plain,
( ~ sQ60_spl
| c(u6r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[f1087,f95]) ).
fof(f3436,plain,
( ~ sQ60_spl
| ~ sQ94_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3431,f708,f2525,f1086]) ).
fof(f3437,plain,
( ~ sQ60_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3432,f708,f727,f1086]) ).
fof(f3438,plain,
( ~ sQ60_spl
| sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3433,f708,f738,f1086]) ).
fof(f3439,plain,
( ~ sQ60_spl
| sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3434,f708,f765,f1086]) ).
fof(f3440,plain,
( ~ sQ60_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3435,f708,f711,f1086]) ).
fof(f3441,plain,
( ~ sQ117_spl
| equalish(u1r2(u4r1(exist)),u1r1(u4r1(exist))) ),
inference(resolution,[status(thm)],[f2707,f867]) ).
fof(f3442,plain,
( ~ sQ117_spl
| equalish(u1r2(u4r1(exist)),u1r2(u4r1(exist))) ),
inference(resolution,[status(thm)],[f2707,f866]) ).
fof(f3445,definition,
( sQ128_spl
<=> equalish(u1r2(u4r1(exist)),u3r2(u4r1(exist))) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f3446,plain,
( ~ sQ128_spl
| equalish(u1r2(u4r1(exist)),u3r2(u4r1(exist))) ),
inference(component_clause,[status(thm)],[f3445]) ).
fof(f3449,definition,
( sQ129_spl
<=> equalish(u1r2(u4r1(exist)),u3r1(u4r1(exist))) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f3450,plain,
( ~ sQ129_spl
| equalish(u1r2(u4r1(exist)),u3r1(u4r1(exist))) ),
inference(component_clause,[status(thm)],[f3449]) ).
fof(f3453,plain,
( ~ sQ117_spl
| ~ s2least(u4r1(exist)) ),
inference(resolution,[status(thm)],[f3441,f59]) ).
fof(f3454,plain,
( ~ sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3453,f795]) ).
fof(f3455,plain,
~ sQ117_spl,
inference(contradiction_clause,[status(thm)],[f3454]) ).
fof(model,axiom,
( ~ sQ0_spl
| sQ2_spl
| sQ3_spl
| sQ4_spl
| sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| sQ10_spl
| sQ11_spl
| sQ13_spl
| sQ17_spl
| sQ19_spl
| sQ22_spl
| sQ23_spl
| sQ26_spl
| sQ31_spl
| sQ37_spl
| sQ39_spl
| sQ43_spl
| sQ44_spl
| sQ51_spl
| sQ52_spl
| sQ53_spl
| sQ57_spl
| sQ58_spl
| sQ59_spl
| ~ sQ60_spl
| sQ64_spl
| sQ66_spl
| sQ69_spl
| sQ70_spl
| sQ91_spl
| sQ92_spl
| sQ93_spl
| sQ116_spl
| ~ sQ117_spl
| ~ sQ118_spl
| sQ119_spl
| sQ120_spl ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS008-1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 22:53:01 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.72/0.52 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.72/0.52 % SZS output start Saturation for theBenchmark
% See solution above
% 0.72/0.55 % Elapsed time: 0.161245 seconds
% 0.72/0.55 % CPU time: 1.017619 seconds
% 0.72/0.55 % Total memory used: 29.062 MB
% 0.72/0.55 % Net memory used: 28.315 MB
%------------------------------------------------------------------------------