%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV116+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 02:46:41 PM UTC 2026
% Result : Theorem 3.52s 0.90s
% Output : CNFRefutation 2.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 113
% Syntax : Number of formulae : 500 ( 93 unt; 85 def)
% Number of atoms : 1346 ( 220 equ)
% Maximal formula atoms : 42 ( 2 avg)
% Number of connectives : 1409 ( 563 ~; 580 |; 151 &)
% ( 88 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 89 ( 87 usr; 85 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 19 con; 0-3 aty)
% Number of variables : 297 ( 277 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( X = Y
| gt(Y,X)
| gt(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( gt(Y,X)
=> leq(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( ( X != Y
& leq(X,Y) )
=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] :
( leq(X,pred(Y))
<=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] : gt(succ(X),X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y] :
( leq(X,Y)
=> leq(X,succ(Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,C] :
( leq(n0,X)
=> leq(uniform_int_rnd(C,X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [I,L1,U1,J,L2,U2,Val] :
( ( leq(J,U2)
& leq(L2,J)
& leq(I,U1)
& leq(L1,I) )
=> a_select3(tptp_const_array2(dim(L1,U1),dim(L2,U2),Val),I,J) = Val ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [Body] : sum(n0,tptp_minus_1,Body) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
succ(tptp_minus_1) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] : pred(succ(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] : succ(pred(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ! [I] :
( ( leq(I,minus(n6,n1))
& leq(n0,I) )
=> ! [J] :
( ( leq(J,minus(n6,n1))
& leq(n0,J) )
=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
=> a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_ds1_filter,H,G) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) )
=> ( ! [O,P] :
( ( leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
=> a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O) )
& ! [M,N] :
( ( leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ! [I] :
( ( leq(I,minus(n6,n1))
& leq(n0,I) )
=> ! [J] :
( ( leq(J,minus(n6,n1))
& leq(n0,J) )
=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
=> a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_ds1_filter,H,G) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) )
=> ( ! [O,P] :
( ( leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
=> a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O) )
& ! [M,N] :
( ( leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f65,axiom,
gt(n0,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
gt(n6,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
gt(n1,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
gt(n2,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
gt(n3,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [X] :
( ( leq(X,n0)
& leq(n0,X) )
=> X = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [X] :
( ( leq(X,n1)
& leq(n0,X) )
=> ( X = n1
| X = n0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,plain,
! [X0,X1] :
( X0 = X1
| gt(X1,X0)
| gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f108,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f109,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f121,plain,
! [X,Y] :
( leq(X,Y)
| ~ gt(Y,X) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f122,plain,
! [X0,X1] :
( leq(X1,X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [X,Y] :
( gt(Y,X)
| X = Y
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f124,plain,
! [X0,X1] :
( gt(X1,X0)
| X0 = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [X,Y] :
( ( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f126,plain,
( ! [X,Y] :
( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ! [X,Y] :
( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(miniscoping,[status(thm)],[f125]) ).
fof(f127,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,pred(X1)) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f128,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,pred(X1)) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f129,plain,
! [X0] : gt(succ(X0),X0),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f130,plain,
! [X,Y] :
( leq(X,succ(Y))
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f131,plain,
! [X0,X1] :
( leq(X0,succ(X1))
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
! [X,Y] :
( ( ~ gt(succ(Y),X)
| leq(X,Y) )
& ( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f133,plain,
( ! [X,Y] :
( ~ gt(succ(Y),X)
| leq(X,Y) )
& ! [X,Y] :
( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f132]) ).
fof(f135,plain,
! [X0,X1] :
( ~ gt(succ(X1),X0)
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f136,plain,
! [X,C] :
( leq(uniform_int_rnd(C,X),X)
| ~ leq(n0,X) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f137,plain,
! [X] :
( ! [C] : leq(uniform_int_rnd(C,X),X)
| ~ leq(n0,X) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( leq(uniform_int_rnd(X1,X0),X0)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f145,plain,
! [I,L1,U1,J,L2,U2,Val] :
( a_select3(tptp_const_array2(dim(L1,U1),dim(L2,U2),Val),I,J) = Val
| ~ leq(J,U2)
| ~ leq(L2,J)
| ~ leq(I,U1)
| ~ leq(L1,I) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f146,plain,
! [I,L1,U1,J,L2,U2] :
( ! [Val] : a_select3(tptp_const_array2(dim(L1,U1),dim(L2,U2),Val),I,J) = Val
| ~ leq(J,U2)
| ~ leq(L2,J)
| ~ leq(I,U1)
| ~ leq(L1,I) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( a_select3(tptp_const_array2(dim(X0,X2),dim(X3,X5),X6),X1,X4) = X6
| ~ leq(X4,X5)
| ~ leq(X3,X4)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f214,plain,
! [X0] : sum(n0,tptp_minus_1,X0) = n0,
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f215,plain,
! [X0] : tptp_float_0_0 = sum(n0,tptp_minus_1,X0),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f216,plain,
succ(tptp_minus_1) = n0,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f227,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f228,plain,
! [X0] : pred(succ(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f229,plain,
! [X0] : succ(pred(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f261,plain,
( ( ? [O,P] :
( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
| ? [M,N] :
( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] :
( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) ) )
& ! [I] :
( ! [J] :
( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J) )
| ~ leq(I,minus(n6,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ! [E,F] :
( a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E)
| ~ leq(F,minus(n6,n1))
| ~ leq(E,minus(n6,n1))
| ~ leq(n0,F)
| ~ leq(n0,E) )
& ! [C,D] :
( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C)
| ~ leq(D,minus(n3,n1))
| ~ leq(C,minus(n3,n1))
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A)
| ~ leq(B,minus(n6,n1))
| ~ leq(A,minus(n6,n1))
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f262,definition,
( sP3_prd
<=> ( ? [M,N] :
( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] :
( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) ) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f263,plain,
( ( ? [O,P] :
( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
| sP3_prd )
& ! [I] :
( ! [J] :
( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J) )
| ~ leq(I,minus(n6,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ! [E,F] :
( a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E)
| ~ leq(F,minus(n6,n1))
| ~ leq(E,minus(n6,n1))
| ~ leq(n0,F)
| ~ leq(n0,E) )
& ! [C,D] :
( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C)
| ~ leq(D,minus(n3,n1))
| ~ leq(C,minus(n3,n1))
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A)
| ~ leq(B,minus(n6,n1))
| ~ leq(A,minus(n6,n1))
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ),
inference(formula_renaming,[status(thm)],[f261,f262]) ).
fof(f264,plain,
( ( ( a_select3(pminus_ds1_filter,sK23_skl,sK24_skl) != a_select3(pminus_ds1_filter,sK24_skl,sK23_skl)
& leq(sK24_skl,minus(n6,n1))
& leq(sK23_skl,minus(n6,n1))
& leq(n0,sK24_skl)
& leq(n0,sK23_skl) )
| sP3_prd )
& ! [I] :
( ! [J] :
( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J) )
| ~ leq(I,minus(n6,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ! [E,F] :
( a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E)
| ~ leq(F,minus(n6,n1))
| ~ leq(E,minus(n6,n1))
| ~ leq(n0,F)
| ~ leq(n0,E) )
& ! [C,D] :
( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C)
| ~ leq(D,minus(n3,n1))
| ~ leq(C,minus(n3,n1))
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A)
| ~ leq(B,minus(n6,n1))
| ~ leq(A,minus(n6,n1))
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(O,sK23_skl),skolemize(P,sK24_skl)],[f263]) ).
fof(f267,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f268,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,minus(n3,n1))
| ~ leq(X0,minus(n3,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f269,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f271,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f272,plain,
( leq(n0,sK23_skl)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f273,plain,
( leq(n0,sK24_skl)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f274,plain,
( leq(sK23_skl,minus(n6,n1))
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f275,plain,
( leq(sK24_skl,minus(n6,n1))
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f276,plain,
( a_select3(pminus_ds1_filter,sK23_skl,sK24_skl) != a_select3(pminus_ds1_filter,sK24_skl,sK23_skl)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f287,plain,
gt(n0,tptp_minus_1),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f293,plain,
gt(n6,n0),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f295,plain,
gt(n1,n0),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f302,plain,
gt(n2,n1),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f303,plain,
gt(n3,n1),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f319,plain,
! [X] :
( X = n0
| ~ leq(X,n0)
| ~ leq(n0,X) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f320,plain,
! [X0] :
( X0 = n0
| ~ leq(X0,n0)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f321,plain,
! [X] :
( X = n1
| X = n0
| ~ leq(X,n1)
| ~ leq(n0,X) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f322,plain,
! [X0] :
( X0 = n1
| X0 = n0
| ~ leq(X0,n1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f330,plain,
succ(n0) = n1,
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f331,plain,
succ(succ(n0)) = n2,
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f332,plain,
succ(succ(succ(n0))) = n3,
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f361,definition,
! [K,L] :
( sP5_prd(L,K)
<=> ( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f362,plain,
( sP3_prd
<=> ( ? [M,N] :
( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] : sP5_prd(L,K) ) ),
inference(formula_renaming,[status(thm)],[f262,f361]) ).
fof(f363,plain,
( ( ( ! [M,N] :
( a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M)
| ~ leq(N,minus(n3,n1))
| ~ leq(M,minus(n3,n1))
| ~ leq(n0,N)
| ~ leq(n0,M) )
& ! [K,L] : ~ sP5_prd(L,K) )
| sP3_prd )
& ( ? [M,N] :
( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] : sP5_prd(L,K)
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f362]) ).
fof(f364,plain,
( ( ( ! [M,N] :
( a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M)
| ~ leq(N,minus(n3,n1))
| ~ leq(M,minus(n3,n1))
| ~ leq(n0,N)
| ~ leq(n0,M) )
& ! [K,L] : ~ sP5_prd(L,K) )
| sP3_prd )
& ( ( a_select3(r_ds1_filter,sK31_skl,sK32_skl) != a_select3(r_ds1_filter,sK32_skl,sK31_skl)
& leq(sK32_skl,minus(n3,n1))
& leq(sK31_skl,minus(n3,n1))
& leq(n0,sK32_skl)
& leq(n0,sK31_skl) )
| sP5_prd(sK30_skl,sK29_skl)
| ~ sP3_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl,sK30_skl,sK31_skl,sK32_skl]),skolemize(K,sK29_skl),skolemize(L,sK30_skl),skolemize(M,sK31_skl),skolemize(N,sK32_skl)],[f363]) ).
fof(f365,plain,
( leq(n0,sK31_skl)
| sP5_prd(sK30_skl,sK29_skl)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f366,plain,
( leq(n0,sK32_skl)
| sP5_prd(sK30_skl,sK29_skl)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f367,plain,
( leq(sK31_skl,minus(n3,n1))
| sP5_prd(sK30_skl,sK29_skl)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f368,plain,
( leq(sK32_skl,minus(n3,n1))
| sP5_prd(sK30_skl,sK29_skl)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f369,plain,
( a_select3(r_ds1_filter,sK31_skl,sK32_skl) != a_select3(r_ds1_filter,sK32_skl,sK31_skl)
| sP5_prd(sK30_skl,sK29_skl)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f380,plain,
! [K,L] :
( ( a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K)
| ~ leq(L,minus(n6,n1))
| ~ leq(K,minus(n6,n1))
| ~ leq(n0,L)
| ~ leq(n0,K)
| sP5_prd(L,K) )
& ( ( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ~ sP5_prd(L,K) ) ),
inference(NNF_transformation,[status(thm)],[f361]) ).
fof(f381,plain,
( ! [K,L] :
( a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K)
| ~ leq(L,minus(n6,n1))
| ~ leq(K,minus(n6,n1))
| ~ leq(n0,L)
| ~ leq(n0,K)
| sP5_prd(L,K) )
& ! [K,L] :
( ( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ~ sP5_prd(L,K) ) ),
inference(miniscoping,[status(thm)],[f380]) ).
fof(f382,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f383,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f384,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f385,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f386,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X1,X0) != a_select3(q_ds1_filter,X0,X1)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f388,definition,
( sQ0_spl
<=> sP3_prd ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f391,definition,
( sQ1_spl
<=> leq(n0,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f394,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f272,f388,f391]) ).
fof(f395,definition,
( sQ2_spl
<=> leq(n0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f398,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f273,f388,f395]) ).
fof(f399,definition,
( sQ3_spl
<=> leq(sK23_skl,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( ~ sQ3_spl
| leq(sK23_skl,minus(n6,n1)) ),
inference(component_clause,[status(thm)],[f399]) ).
fof(f402,plain,
( sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f274,f388,f399]) ).
fof(f403,definition,
( sQ4_spl
<=> leq(sK24_skl,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( ~ sQ4_spl
| leq(sK24_skl,minus(n6,n1)) ),
inference(component_clause,[status(thm)],[f403]) ).
fof(f406,plain,
( sQ4_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f275,f388,f403]) ).
fof(f407,definition,
( sQ5_spl
<=> a_select3(pminus_ds1_filter,sK23_skl,sK24_skl) = a_select3(pminus_ds1_filter,sK24_skl,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( sQ5_spl
| a_select3(pminus_ds1_filter,sK23_skl,sK24_skl) != a_select3(pminus_ds1_filter,sK24_skl,sK23_skl) ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f410,plain,
( ~ sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f276,f388,f407]) ).
fof(f411,definition,
( sQ6_spl
<=> sP5_prd(sK30_skl,sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f412,plain,
( ~ sQ6_spl
| sP5_prd(sK30_skl,sK29_skl) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f414,definition,
( sQ7_spl
<=> leq(n0,sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( ~ sQ7_spl
| leq(n0,sK31_skl) ),
inference(component_clause,[status(thm)],[f414]) ).
fof(f417,plain,
( sQ7_spl
| sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f365,f388,f411,f414]) ).
fof(f418,definition,
( sQ8_spl
<=> leq(n0,sK32_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( ~ sQ8_spl
| leq(n0,sK32_skl) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,plain,
( sQ8_spl
| sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f366,f388,f411,f418]) ).
fof(f422,definition,
( sQ9_spl
<=> leq(sK31_skl,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f423,plain,
( ~ sQ9_spl
| leq(sK31_skl,minus(n3,n1)) ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f425,plain,
( sQ9_spl
| sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f367,f388,f411,f422]) ).
fof(f426,definition,
( sQ10_spl
<=> leq(sK32_skl,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f427,plain,
( ~ sQ10_spl
| leq(sK32_skl,minus(n3,n1)) ),
inference(component_clause,[status(thm)],[f426]) ).
fof(f429,plain,
( sQ10_spl
| sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f368,f388,f411,f426]) ).
fof(f430,definition,
( sQ11_spl
<=> a_select3(r_ds1_filter,sK31_skl,sK32_skl) = a_select3(r_ds1_filter,sK32_skl,sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( sQ11_spl
| a_select3(r_ds1_filter,sK31_skl,sK32_skl) != a_select3(r_ds1_filter,sK32_skl,sK31_skl) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f433,plain,
( ~ sQ11_spl
| sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f369,f388,f411,f430]) ).
fof(f445,plain,
pred(n0) = tptp_minus_1,
inference(paramodulation,[status(thm)],[f216,f228]) ).
fof(f448,plain,
! [X0] : gt(X0,pred(X0)),
inference(paramodulation,[status(thm)],[f229,f129]) ).
fof(f452,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f267,f386]) ).
fof(f454,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f452,f383]) ).
fof(f457,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f454,f382]) ).
fof(f458,plain,
( ~ sQ6_spl
| ~ leq(sK30_skl,minus(n6,n1))
| ~ leq(sK29_skl,minus(n6,n1)) ),
inference(resolution,[status(thm)],[f457,f412]) ).
fof(f459,definition,
( sQ14_spl
<=> leq(sK29_skl,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ14_spl
| ~ leq(sK29_skl,minus(n6,n1)) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
( sQ15_spl
<=> leq(sK30_skl,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( sQ15_spl
| ~ leq(sK30_skl,minus(n6,n1)) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( ~ sQ6_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f458,f459,f462,f411]) ).
fof(f467,plain,
! [X0] :
( sQ14_spl
| ~ sP5_prd(X0,sK29_skl) ),
inference(resolution,[status(thm)],[f461,f384]) ).
fof(f470,plain,
( ~ sQ6_spl
| sQ14_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f412,f467]) ).
fof(f471,plain,
( ~ sQ6_spl
| sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f470]) ).
fof(f472,plain,
pred(n1) = n0,
inference(paramodulation,[status(thm)],[f330,f228]) ).
fof(f475,plain,
succ(succ(n1)) = n3,
inference(forward_demodulation,[status(thm)],[f330,f332]) ).
fof(f476,plain,
pred(n3) = succ(n1),
inference(paramodulation,[status(thm)],[f475,f228]) ).
fof(f477,plain,
gt(n3,succ(n1)),
inference(paramodulation,[status(thm)],[f475,f129]) ).
fof(f481,plain,
( n0 = n0
| ~ leq(n0,n0) ),
inference(resolution,[status(thm)],[f320,f109]) ).
fof(f482,definition,
( sQ16_spl
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( sQ16_spl
| ~ leq(n0,n0) ),
inference(component_clause,[status(thm)],[f482]) ).
fof(f485,definition,
( sQ17_spl
<=> n0 = n0 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f481,f482,f485]) ).
fof(f493,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f484,f109]) ).
fof(f494,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f493]) ).
fof(f499,plain,
! [X0] :
( X0 = n0
| ~ leq(n0,X0)
| ~ gt(n0,X0) ),
inference(resolution,[status(thm)],[f122,f320]) ).
fof(f502,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,minus(n3,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f268]) ).
fof(f503,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(n0,X1)
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f271]) ).
fof(f504,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f269]) ).
fof(f505,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f267]) ).
fof(f507,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,pred(n3))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f502]) ).
fof(f508,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(n0,X1)
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f503]) ).
fof(f509,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f504]) ).
fof(f510,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f505]) ).
fof(f512,plain,
! [X0] : ~ leq(X0,pred(X0)),
inference(resolution,[status(thm)],[f127,f108]) ).
fof(f516,plain,
( ~ sQ3_spl
| leq(sK23_skl,pred(n6)) ),
inference(forward_demodulation,[status(thm)],[f227,f400]) ).
fof(f517,plain,
( ~ sQ4_spl
| leq(sK24_skl,pred(n6)) ),
inference(forward_demodulation,[status(thm)],[f227,f404]) ).
fof(f521,plain,
! [X0] :
( ~ gt(n3,X0)
| leq(X0,succ(n1)) ),
inference(paramodulation,[status(thm)],[f476,f128]) ).
fof(f526,plain,
( tptp_minus_1 = n0
| ~ leq(n0,tptp_minus_1) ),
inference(resolution,[status(thm)],[f499,f287]) ).
fof(f527,plain,
( pred(n0) = n0
| ~ leq(n0,pred(n0)) ),
inference(resolution,[status(thm)],[f499,f448]) ).
fof(f532,definition,
( sQ19_spl
<=> leq(n0,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f535,definition,
( sQ20_spl
<=> tptp_minus_1 = n0 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f536,plain,
( ~ sQ20_spl
| tptp_minus_1 = n0 ),
inference(component_clause,[status(thm)],[f535]) ).
fof(f537,plain,
( sQ20_spl
| tptp_minus_1 != n0 ),
inference(component_clause,[status(thm)],[f535]) ).
fof(f538,plain,
( sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f526,f532,f535]) ).
fof(f539,definition,
( sQ21_spl
<=> leq(n0,pred(n0)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f541,plain,
( sQ21_spl
| ~ leq(n0,pred(n0)) ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,definition,
( sQ22_spl
<=> pred(n0) = n0 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( ~ sQ22_spl
| pred(n0) = n0 ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,plain,
( sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f527,f539,f542]) ).
fof(f549,plain,
( sQ21_spl
| ~ leq(n0,tptp_minus_1) ),
inference(forward_demodulation,[status(thm)],[f445,f541]) ).
fof(f551,plain,
( sQ21_spl
| ~ gt(tptp_minus_1,n0) ),
inference(resolution,[status(thm)],[f549,f122]) ).
fof(f555,plain,
! [X0] :
( ~ gt(n1,X0)
| X0 = n1
| X0 = n0
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f322,f122]) ).
fof(f558,plain,
( n1 = n1
| n1 = n0
| ~ leq(n0,n1) ),
inference(resolution,[status(thm)],[f322,f109]) ).
fof(f559,definition,
( sQ23_spl
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( ~ sQ23_spl
| n0 = n1 ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f561,plain,
( sQ23_spl
| n0 != n1 ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,definition,
! [X0] :
( sQ24_spl
<=> ~ leq(minus(X0,n1),X0) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f563,plain,
! [X0] :
( ~ sQ24_spl
| ~ leq(minus(X0,n1),X0) ),
inference(component_clause,[status(thm)],[f562]) ).
fof(f566,definition,
( sQ25_spl
<=> leq(n0,n1) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f568,plain,
( sQ25_spl
| ~ leq(n0,n1) ),
inference(component_clause,[status(thm)],[f566]) ).
fof(f569,definition,
( sQ26_spl
<=> n1 = n1 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f572,plain,
( sQ26_spl
| sQ23_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f558,f566,f559,f569]) ).
fof(f579,plain,
! [X0] : ~ gt(pred(X0),X0),
inference(resolution,[status(thm)],[f512,f122]) ).
fof(f582,plain,
~ leq(n3,succ(n1)),
inference(paramodulation,[status(thm)],[f476,f512]) ).
fof(f584,plain,
~ leq(n1,n0),
inference(paramodulation,[status(thm)],[f472,f512]) ).
fof(f585,plain,
! [X0] : ~ leq(succ(X0),X0),
inference(paramodulation,[status(thm)],[f228,f512]) ).
fof(f590,plain,
( sQ21_spl
| n0 = tptp_minus_1
| gt(n0,tptp_minus_1) ),
inference(resolution,[status(thm)],[f551,f104]) ).
fof(f592,definition,
( sQ27_spl
<=> gt(n0,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f595,plain,
( sQ21_spl
| sQ20_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f590,f592,f535,f539]) ).
fof(f596,plain,
( ~ sQ22_spl
| tptp_minus_1 = n0 ),
inference(forward_demodulation,[status(thm)],[f445,f543]) ).
fof(f611,plain,
( ~ sQ20_spl
| gt(tptp_minus_1,tptp_minus_1) ),
inference(backward_demodulation,[status(thm)],[f536,f287]) ).
fof(f627,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f611,f108]) ).
fof(f628,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f627]) ).
fof(f629,plain,
( sQ20_spl
| ~ sQ22_spl
| tptp_minus_1 != tptp_minus_1 ),
inference(forward_demodulation,[status(thm)],[f596,f537]) ).
fof(f630,plain,
( sQ20_spl
| ~ sQ22_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f629]) ).
fof(f631,plain,
( sQ20_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f630]) ).
fof(f636,plain,
~ gt(succ(n1),n3),
inference(paramodulation,[status(thm)],[f476,f579]) ).
fof(f637,plain,
! [X0] : ~ gt(X0,succ(X0)),
inference(paramodulation,[status(thm)],[f228,f579]) ).
fof(f641,plain,
~ gt(n0,n1),
inference(resolution,[status(thm)],[f584,f122]) ).
fof(f650,plain,
~ leq(n3,succ(n1)),
inference(paramodulation,[status(thm)],[f475,f585]) ).
fof(f672,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,succ(n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f476,f507]) ).
fof(f673,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,succ(n1))
| ~ leq(X0,succ(n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f476,f672]) ).
fof(f678,plain,
gt(n1,n0),
inference(paramodulation,[status(thm)],[f472,f448]) ).
fof(f685,plain,
( sQ5_spl
| ~ leq(sK24_skl,pred(n6))
| ~ leq(sK23_skl,pred(n6))
| ~ leq(n0,sK24_skl)
| ~ leq(n0,sK23_skl) ),
inference(resolution,[status(thm)],[f509,f409]) ).
fof(f687,definition,
( sQ28_spl
<=> leq(sK23_skl,pred(n6)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f689,plain,
( sQ28_spl
| ~ leq(sK23_skl,pred(n6)) ),
inference(component_clause,[status(thm)],[f687]) ).
fof(f690,definition,
( sQ29_spl
<=> leq(sK24_skl,pred(n6)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( sQ29_spl
| ~ leq(sK24_skl,pred(n6)) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f693,plain,
( sQ5_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f685,f391,f395,f687,f690,f407]) ).
fof(f695,plain,
( sQ28_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f689,f516]) ).
fof(f696,plain,
( sQ28_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f695]) ).
fof(f697,plain,
( sQ29_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f692,f517]) ).
fof(f698,plain,
( sQ29_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f697]) ).
fof(f699,plain,
( sQ15_spl
| ~ leq(sK30_skl,pred(n6)) ),
inference(forward_demodulation,[status(thm)],[f227,f464]) ).
fof(f703,plain,
( ~ sQ10_spl
| leq(sK32_skl,pred(n3)) ),
inference(forward_demodulation,[status(thm)],[f227,f427]) ).
fof(f704,plain,
( ~ sQ10_spl
| leq(sK32_skl,succ(n1)) ),
inference(forward_demodulation,[status(thm)],[f476,f703]) ).
fof(f705,plain,
( ~ sQ9_spl
| leq(sK31_skl,pred(n3)) ),
inference(forward_demodulation,[status(thm)],[f227,f423]) ).
fof(f706,plain,
( ~ sQ9_spl
| leq(sK31_skl,succ(n1)) ),
inference(forward_demodulation,[status(thm)],[f476,f705]) ).
fof(f708,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f385]) ).
fof(f717,plain,
( ~ sQ23_spl
| gt(n1,n1) ),
inference(backward_demodulation,[status(thm)],[f560,f295]) ).
fof(f729,plain,
( ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f108]) ).
fof(f730,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f729]) ).
fof(f768,plain,
~ leq(n1,pred(n0)),
inference(resolution,[status(thm)],[f641,f127]) ).
fof(f769,plain,
( n1 = n0
| ~ leq(n1,n0) ),
inference(resolution,[status(thm)],[f641,f124]) ).
fof(f771,plain,
( n1 = n0
| gt(n1,n0) ),
inference(resolution,[status(thm)],[f641,f104]) ).
fof(f772,plain,
~ leq(n1,tptp_minus_1),
inference(forward_demodulation,[status(thm)],[f445,f768]) ).
fof(f773,definition,
( sQ30_spl
<=> leq(n1,n0) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( sQ23_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f769,f773,f559]) ).
fof(f777,definition,
( sQ31_spl
<=> gt(n1,n0) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( sQ23_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f771,f777,f559]) ).
fof(f782,plain,
! [X0] :
( ~ leq(n0,n1)
| uniform_int_rnd(X0,n1) = n1
| uniform_int_rnd(X0,n1) = n0
| ~ leq(n0,uniform_int_rnd(X0,n1)) ),
inference(resolution,[status(thm)],[f322,f138]) ).
fof(f788,definition,
! [X0] :
( sQ32_spl
<=> ( uniform_int_rnd(X0,n1) = n1
| uniform_int_rnd(X0,n1) = n0
| ~ leq(n0,uniform_int_rnd(X0,n1)) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f791,plain,
( ~ sQ25_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f782,f788,f566]) ).
fof(f793,plain,
! [X0] :
( ~ leq(n0,n0)
| uniform_int_rnd(X0,n0) = n0
| ~ leq(n0,uniform_int_rnd(X0,n0)) ),
inference(resolution,[status(thm)],[f320,f138]) ).
fof(f799,definition,
! [X0] :
( sQ33_spl
<=> ( uniform_int_rnd(X0,n0) = n0
| ~ leq(n0,uniform_int_rnd(X0,n0)) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f802,plain,
( ~ sQ16_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f793,f799,f482]) ).
fof(f826,plain,
( sQ25_spl
| ~ gt(n1,n0) ),
inference(resolution,[status(thm)],[f568,f122]) ).
fof(f829,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f826,f678]) ).
fof(f830,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f829]) ).
fof(f846,plain,
! [X0,X1] :
( ~ gt(n3,succ(n1))
| a_select3(tptp_const_array2(dim(X0,succ(n1)),dim(succ(n1),succ(n1)),X1),succ(n1),succ(n1)) = X1
| ~ leq(X0,succ(n1)) ),
inference(resolution,[status(thm)],[f147,f521]) ).
fof(f869,plain,
! [X0,X1,X2,X3] :
( ~ gt(n3,succ(n1))
| a_select3(tptp_const_array2(dim(X0,X2),dim(succ(n1),succ(n1)),X3),X1,succ(n1)) = X3
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(resolution,[status(thm)],[f147,f521]) ).
fof(f900,definition,
! [X0,X1] :
( sQ34_spl
<=> ( a_select3(tptp_const_array2(dim(X0,succ(n1)),dim(succ(n1),succ(n1)),X1),succ(n1),succ(n1)) = X1
| ~ leq(X0,succ(n1)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f903,definition,
( sQ35_spl
<=> gt(n3,succ(n1)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f905,plain,
( sQ35_spl
| ~ gt(n3,succ(n1)) ),
inference(component_clause,[status(thm)],[f903]) ).
fof(f906,plain,
( ~ sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f846,f900,f903]) ).
fof(f909,definition,
! [X0,X1,X2,X3] :
( sQ36_spl
<=> ( a_select3(tptp_const_array2(dim(X0,X2),dim(succ(n1),succ(n1)),X3),X1,succ(n1)) = X3
| ~ leq(X1,X2)
| ~ leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f912,plain,
( ~ sQ35_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f869,f909,f903]) ).
fof(f915,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f905,f477]) ).
fof(f916,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f915]) ).
fof(f935,plain,
( sQ15_spl
| ~ gt(n6,sK30_skl) ),
inference(resolution,[status(thm)],[f699,f128]) ).
fof(f942,plain,
( sQ15_spl
| sK30_skl = n6
| ~ leq(sK30_skl,n6) ),
inference(resolution,[status(thm)],[f935,f124]) ).
fof(f945,definition,
( sQ37_spl
<=> leq(sK30_skl,n6) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f947,plain,
( sQ37_spl
| ~ leq(sK30_skl,n6) ),
inference(component_clause,[status(thm)],[f945]) ).
fof(f948,definition,
( sQ38_spl
<=> sK30_skl = n6 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f949,plain,
( ~ sQ38_spl
| sK30_skl = n6 ),
inference(component_clause,[status(thm)],[f948]) ).
fof(f951,plain,
( sQ15_spl
| sQ38_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f942,f945,f948,f462]) ).
fof(f976,plain,
~ gt(tptp_minus_1,n1),
inference(resolution,[status(thm)],[f772,f122]) ).
fof(f1000,plain,
! [X0] :
( ~ sQ24_spl
| ~ leq(pred(X0),X0) ),
inference(forward_demodulation,[status(thm)],[f227,f563]) ).
fof(f1032,plain,
( sQ37_spl
| ~ gt(n6,sK30_skl) ),
inference(resolution,[status(thm)],[f947,f122]) ).
fof(f1060,plain,
( n1 = tptp_minus_1
| ~ leq(n1,tptp_minus_1) ),
inference(resolution,[status(thm)],[f976,f124]) ).
fof(f1062,plain,
( n1 = tptp_minus_1
| gt(n1,tptp_minus_1) ),
inference(resolution,[status(thm)],[f976,f104]) ).
fof(f1063,definition,
( sQ44_spl
<=> leq(n1,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1066,definition,
( sQ45_spl
<=> n1 = tptp_minus_1 ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1067,plain,
( ~ sQ45_spl
| n1 = tptp_minus_1 ),
inference(component_clause,[status(thm)],[f1066]) ).
fof(f1069,plain,
( sQ45_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f1060,f1063,f1066]) ).
fof(f1070,definition,
( sQ46_spl
<=> gt(n1,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1073,plain,
( sQ45_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f1062,f1070,f1066]) ).
fof(f1075,plain,
( ~ sQ45_spl
| ~ leq(n1,n1) ),
inference(backward_demodulation,[status(thm)],[f1067,f772]) ).
fof(f1090,plain,
( ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1075,f109]) ).
fof(f1091,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f1090]) ).
fof(f1093,plain,
( ~ sQ24_spl
| ~ gt(n3,pred(succ(n1))) ),
inference(resolution,[status(thm)],[f1000,f521]) ).
fof(f1103,plain,
( ~ sQ24_spl
| ~ gt(n3,n1) ),
inference(forward_demodulation,[status(thm)],[f228,f1093]) ).
fof(f1104,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1103,f303]) ).
fof(f1105,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1104]) ).
fof(f1119,plain,
( sQ37_spl
| ~ leq(sK30_skl,pred(n6)) ),
inference(resolution,[status(thm)],[f1032,f127]) ).
fof(f1222,plain,
( ~ sQ6_spl
| ~ sQ38_spl
| sP5_prd(n6,sK29_skl) ),
inference(forward_demodulation,[status(thm)],[f949,f412]) ).
fof(f1223,plain,
( ~ sQ6_spl
| ~ sQ38_spl
| leq(n6,pred(n6)) ),
inference(resolution,[status(thm)],[f1222,f708]) ).
fof(f1225,plain,
( ~ sQ6_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1223,f512]) ).
fof(f1226,plain,
( ~ sQ6_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1225]) ).
fof(f1261,plain,
~ leq(n3,n1),
inference(resolution,[status(thm)],[f582,f131]) ).
fof(f1268,plain,
~ gt(n1,n3),
inference(resolution,[status(thm)],[f1261,f122]) ).
fof(f1271,plain,
~ leq(n3,pred(n1)),
inference(resolution,[status(thm)],[f1268,f127]) ).
fof(f1272,plain,
( n3 = n1
| ~ leq(n3,n1) ),
inference(resolution,[status(thm)],[f1268,f124]) ).
fof(f1274,plain,
( n3 = n1
| gt(n3,n1) ),
inference(resolution,[status(thm)],[f1268,f104]) ).
fof(f1275,plain,
~ leq(n3,n0),
inference(forward_demodulation,[status(thm)],[f472,f1271]) ).
fof(f1276,definition,
( sQ50_spl
<=> leq(n3,n1) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1279,definition,
( sQ51_spl
<=> n3 = n1 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1280,plain,
( ~ sQ51_spl
| n3 = n1 ),
inference(component_clause,[status(thm)],[f1279]) ).
fof(f1282,plain,
( sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1272,f1276,f1279]) ).
fof(f1283,definition,
( sQ52_spl
<=> gt(n3,n1) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1284,plain,
( ~ sQ52_spl
| gt(n3,n1) ),
inference(component_clause,[status(thm)],[f1283]) ).
fof(f1286,plain,
( sQ51_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1274,f1283,f1279]) ).
fof(f1288,plain,
( ~ sQ51_spl
| ~ leq(n3,n3) ),
inference(backward_demodulation,[status(thm)],[f1280,f1261]) ).
fof(f1317,plain,
( ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1288,f109]) ).
fof(f1318,plain,
~ sQ51_spl,
inference(contradiction_clause,[status(thm)],[f1317]) ).
fof(f1321,plain,
~ gt(n0,n3),
inference(resolution,[status(thm)],[f1275,f122]) ).
fof(f1334,plain,
~ gt(succ(tptp_minus_1),n1),
inference(resolution,[status(thm)],[f772,f135]) ).
fof(f1338,plain,
~ gt(n0,n1),
inference(forward_demodulation,[status(thm)],[f216,f1334]) ).
fof(f1391,plain,
succ(n0) = n1,
inference(paramodulation,[status(thm)],[f472,f229]) ).
fof(f1407,plain,
~ leq(n3,pred(n0)),
inference(resolution,[status(thm)],[f1321,f127]) ).
fof(f1408,plain,
( n3 = n0
| ~ leq(n3,n0) ),
inference(resolution,[status(thm)],[f1321,f124]) ).
fof(f1410,plain,
( n3 = n0
| gt(n3,n0) ),
inference(resolution,[status(thm)],[f1321,f104]) ).
fof(f1411,plain,
~ leq(n3,tptp_minus_1),
inference(forward_demodulation,[status(thm)],[f445,f1407]) ).
fof(f1412,definition,
( sQ53_spl
<=> leq(n3,n0) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1415,definition,
( sQ54_spl
<=> n3 = n0 ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1416,plain,
( ~ sQ54_spl
| n3 = n0 ),
inference(component_clause,[status(thm)],[f1415]) ).
fof(f1417,plain,
( sQ54_spl
| n3 != n0 ),
inference(component_clause,[status(thm)],[f1415]) ).
fof(f1418,plain,
( sQ54_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f1408,f1412,f1415]) ).
fof(f1419,definition,
( sQ55_spl
<=> gt(n3,n0) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1420,plain,
( ~ sQ55_spl
| gt(n3,n0) ),
inference(component_clause,[status(thm)],[f1419]) ).
fof(f1422,plain,
( sQ54_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1410,f1419,f1415]) ).
fof(f1426,plain,
( ~ sQ54_spl
| ~ gt(n3,n1) ),
inference(backward_demodulation,[status(thm)],[f1416,f641]) ).
fof(f1475,plain,
( ~ sQ54_spl
| ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1426,f1284]) ).
fof(f1476,plain,
( ~ sQ54_spl
| ~ sQ52_spl ),
inference(contradiction_clause,[status(thm)],[f1475]) ).
fof(f1529,plain,
~ gt(tptp_minus_1,n3),
inference(resolution,[status(thm)],[f1411,f122]) ).
fof(f1551,plain,
! [X0] :
( ~ sQ10_spl
| a_select3(r_ds1_filter,X0,sK32_skl) = a_select3(r_ds1_filter,sK32_skl,X0)
| ~ leq(X0,succ(n1))
| ~ leq(n0,sK32_skl)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f673,f704]) ).
fof(f1559,definition,
! [X0] :
( sQ56_spl
<=> ( a_select3(r_ds1_filter,X0,sK32_skl) = a_select3(r_ds1_filter,sK32_skl,X0)
| ~ leq(X0,succ(n1))
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1562,plain,
( ~ sQ10_spl
| ~ sQ8_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1551,f1559,f418,f426]) ).
fof(f1655,plain,
! [X0] :
( a_select3(id_ds1_filter,X0,pred(n6)) = a_select3(id_ds1_filter,pred(n6),X0)
| ~ leq(n0,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f508,f109]) ).
fof(f1657,definition,
! [X0] :
( sQ60_spl
<=> ( a_select3(id_ds1_filter,X0,pred(n6)) = a_select3(id_ds1_filter,pred(n6),X0)
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1660,definition,
( sQ61_spl
<=> leq(n0,pred(n6)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1662,plain,
( sQ61_spl
| ~ leq(n0,pred(n6)) ),
inference(component_clause,[status(thm)],[f1660]) ).
fof(f1663,plain,
( ~ sQ61_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1655,f1657,f1660]) ).
fof(f1665,plain,
( n3 = tptp_minus_1
| ~ leq(n3,tptp_minus_1) ),
inference(resolution,[status(thm)],[f1529,f124]) ).
fof(f1667,plain,
( n3 = tptp_minus_1
| gt(n3,tptp_minus_1) ),
inference(resolution,[status(thm)],[f1529,f104]) ).
fof(f1668,definition,
( sQ62_spl
<=> leq(n3,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1671,definition,
( sQ63_spl
<=> n3 = tptp_minus_1 ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1672,plain,
( ~ sQ63_spl
| n3 = tptp_minus_1 ),
inference(component_clause,[status(thm)],[f1671]) ).
fof(f1674,plain,
( sQ63_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f1665,f1668,f1671]) ).
fof(f1675,definition,
( sQ64_spl
<=> gt(n3,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1678,plain,
( sQ63_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1667,f1675,f1671]) ).
fof(f1681,plain,
( ~ sQ63_spl
| gt(n0,n3) ),
inference(backward_demodulation,[status(thm)],[f1672,f287]) ).
fof(f1700,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1681,f1321]) ).
fof(f1701,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f1700]) ).
fof(f1708,plain,
! [X0] :
( a_select3(pminus_ds1_filter,X0,pred(n6)) = a_select3(pminus_ds1_filter,pred(n6),X0)
| ~ leq(X0,pred(n6))
| ~ leq(n0,pred(n6))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f509,f109]) ).
fof(f1710,definition,
! [X0] :
( sQ65_spl
<=> ( a_select3(pminus_ds1_filter,X0,pred(n6)) = a_select3(pminus_ds1_filter,pred(n6),X0)
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1713,plain,
( ~ sQ61_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1708,f1710,f1660]) ).
fof(f1774,plain,
! [X0] :
( a_select3(q_ds1_filter,X0,pred(n6)) = a_select3(q_ds1_filter,pred(n6),X0)
| ~ leq(X0,pred(n6))
| ~ leq(n0,pred(n6))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f510,f109]) ).
fof(f1776,definition,
! [X0] :
( sQ68_spl
<=> ( a_select3(q_ds1_filter,X0,pred(n6)) = a_select3(q_ds1_filter,pred(n6),X0)
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1779,plain,
( ~ sQ61_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1774,f1776,f1660]) ).
fof(f2099,plain,
( ~ sQ6_spl
| leq(sK30_skl,pred(n6)) ),
inference(resolution,[status(thm)],[f708,f412]) ).
fof(f2188,plain,
( pred(n1) = n1
| pred(n1) = n0
| ~ leq(n0,pred(n1)) ),
inference(resolution,[status(thm)],[f555,f448]) ).
fof(f2195,definition,
( sQ81_spl
<=> leq(n0,pred(n1)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f2197,plain,
( sQ81_spl
| ~ leq(n0,pred(n1)) ),
inference(component_clause,[status(thm)],[f2195]) ).
fof(f2198,definition,
( sQ82_spl
<=> pred(n1) = n0 ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f2201,definition,
( sQ83_spl
<=> pred(n1) = n1 ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f2202,plain,
( ~ sQ83_spl
| pred(n1) = n1 ),
inference(component_clause,[status(thm)],[f2201]) ).
fof(f2204,plain,
( sQ83_spl
| sQ82_spl
| ~ sQ81_spl ),
inference(split_clause,[status(thm)],[f2188,f2195,f2198,f2201]) ).
fof(f2208,plain,
( ~ sQ83_spl
| n0 = n1 ),
inference(forward_demodulation,[status(thm)],[f472,f2202]) ).
fof(f2209,plain,
( ~ sQ83_spl
| sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2208,f561]) ).
fof(f2210,plain,
( ~ sQ83_spl
| sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f2209]) ).
fof(f2211,plain,
( sQ81_spl
| ~ leq(n0,n0) ),
inference(forward_demodulation,[status(thm)],[f472,f2197]) ).
fof(f2212,plain,
( sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2211,f109]) ).
fof(f2213,plain,
sQ81_spl,
inference(contradiction_clause,[status(thm)],[f2212]) ).
fof(f2216,plain,
~ leq(n3,n2),
inference(backward_demodulation,[status(thm)],[f2221,f650]) ).
fof(f2218,plain,
~ gt(n2,n3),
inference(backward_demodulation,[status(thm)],[f2221,f636]) ).
fof(f2219,plain,
succ(n2) = n3,
inference(backward_demodulation,[status(thm)],[f2221,f475]) ).
fof(f2220,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,n2)
| ~ leq(X0,succ(n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f2221,f673]) ).
fof(f2221,plain,
succ(n1) = n2,
inference(forward_demodulation,[status(thm)],[f1391,f331]) ).
fof(f2223,plain,
~ gt(n1,n2),
inference(paramodulation,[status(thm)],[f2221,f637]) ).
fof(f2226,plain,
~ leq(n2,n1),
inference(paramodulation,[status(thm)],[f2221,f585]) ).
fof(f2229,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,n2)
| ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f2221,f2220]) ).
fof(f2236,plain,
( n3 = n2
| ~ leq(n3,n2) ),
inference(resolution,[status(thm)],[f2218,f124]) ).
fof(f2238,plain,
( n3 = n2
| gt(n3,n2) ),
inference(resolution,[status(thm)],[f2218,f104]) ).
fof(f2239,definition,
( sQ84_spl
<=> leq(n3,n2) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f2242,definition,
( sQ85_spl
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2243,plain,
( ~ sQ85_spl
| n3 = n2 ),
inference(component_clause,[status(thm)],[f2242]) ).
fof(f2245,plain,
( sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f2236,f2239,f2242]) ).
fof(f2246,definition,
( sQ86_spl
<=> gt(n3,n2) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2249,plain,
( sQ85_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f2238,f2246,f2242]) ).
fof(f2252,plain,
( ~ sQ85_spl
| ~ leq(n3,n3) ),
inference(backward_demodulation,[status(thm)],[f2243,f2216]) ).
fof(f2262,plain,
( ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2252,f109]) ).
fof(f2263,plain,
~ sQ85_spl,
inference(contradiction_clause,[status(thm)],[f2262]) ).
fof(f2272,plain,
~ leq(n2,pred(n1)),
inference(resolution,[status(thm)],[f2223,f127]) ).
fof(f2273,plain,
( n2 = n1
| ~ leq(n2,n1) ),
inference(resolution,[status(thm)],[f2223,f124]) ).
fof(f2275,plain,
( n2 = n1
| gt(n2,n1) ),
inference(resolution,[status(thm)],[f2223,f104]) ).
fof(f2276,plain,
~ leq(n2,n0),
inference(forward_demodulation,[status(thm)],[f472,f2272]) ).
fof(f2277,definition,
( sQ87_spl
<=> leq(n2,n1) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f2280,definition,
( sQ88_spl
<=> n2 = n1 ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2281,plain,
( ~ sQ88_spl
| n2 = n1 ),
inference(component_clause,[status(thm)],[f2280]) ).
fof(f2283,plain,
( sQ88_spl
| ~ sQ87_spl ),
inference(split_clause,[status(thm)],[f2273,f2277,f2280]) ).
fof(f2284,definition,
( sQ89_spl
<=> gt(n2,n1) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2287,plain,
( sQ88_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f2275,f2284,f2280]) ).
fof(f2322,plain,
( sQ61_spl
| ~ gt(n6,n0) ),
inference(resolution,[status(thm)],[f1662,f128]) ).
fof(f2327,plain,
( sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2322,f293]) ).
fof(f2328,plain,
sQ61_spl,
inference(contradiction_clause,[status(thm)],[f2327]) ).
fof(f2345,plain,
! [X0] :
( a_select3(r_ds1_filter,X0,n2) = a_select3(r_ds1_filter,n2,X0)
| ~ leq(X0,n2)
| ~ leq(n0,n2)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f2229,f109]) ).
fof(f2351,definition,
! [X0] :
( sQ90_spl
<=> ( a_select3(r_ds1_filter,X0,n2) = a_select3(r_ds1_filter,n2,X0)
| ~ leq(X0,n2)
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2354,definition,
( sQ91_spl
<=> leq(n0,n2) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2355,plain,
( ~ sQ91_spl
| leq(n0,n2) ),
inference(component_clause,[status(thm)],[f2354]) ).
fof(f2356,plain,
( sQ91_spl
| ~ leq(n0,n2) ),
inference(component_clause,[status(thm)],[f2354]) ).
fof(f2357,plain,
( ~ sQ91_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2345,f2351,f2354]) ).
fof(f2358,plain,
( ~ sQ88_spl
| ~ leq(n2,n2) ),
inference(forward_demodulation,[status(thm)],[f2281,f2226]) ).
fof(f2359,plain,
( ~ sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2358,f109]) ).
fof(f2360,plain,
~ sQ88_spl,
inference(contradiction_clause,[status(thm)],[f2359]) ).
fof(f2387,plain,
( sQ91_spl
| ~ gt(succ(n2),n0) ),
inference(resolution,[status(thm)],[f2356,f135]) ).
fof(f2391,plain,
( sQ91_spl
| ~ gt(n3,n0) ),
inference(forward_demodulation,[status(thm)],[f2219,f2387]) ).
fof(f2392,plain,
( sQ91_spl
| ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2391,f1420]) ).
fof(f2393,plain,
( sQ91_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f2392]) ).
fof(f2394,plain,
! [X0] :
( ~ sQ91_spl
| a_select3(r_ds1_filter,X0,n0) = a_select3(r_ds1_filter,n0,X0)
| ~ leq(X0,n2)
| ~ leq(n0,n0)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f2355,f2229]) ).
fof(f2402,definition,
! [X0] :
( sQ92_spl
<=> ( a_select3(r_ds1_filter,X0,n0) = a_select3(r_ds1_filter,n0,X0)
| ~ leq(X0,n2)
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2405,plain,
( ~ sQ91_spl
| ~ sQ16_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f2394,f2402,f482,f2354]) ).
fof(f2446,plain,
( ~ sQ9_spl
| leq(sK31_skl,n2) ),
inference(forward_demodulation,[status(thm)],[f2221,f706]) ).
fof(f2473,plain,
( ~ sQ10_spl
| leq(sK32_skl,n2) ),
inference(forward_demodulation,[status(thm)],[f2221,f704]) ).
fof(f2499,plain,
~ gt(n0,n2),
inference(resolution,[status(thm)],[f2276,f122]) ).
fof(f2573,plain,
( sQ23_spl
| tptp_float_0_0 != n1 ),
inference(backward_demodulation,[status(thm)],[f2628,f561]) ).
fof(f2574,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,n2)
| ~ leq(X0,n2)
| ~ leq(tptp_float_0_0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f2628,f2229]) ).
fof(f2596,plain,
! [X0] :
( X0 = tptp_float_0_0
| ~ leq(X0,n0)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f2628,f320]) ).
fof(f2598,plain,
( sQ21_spl
| ~ gt(tptp_minus_1,tptp_float_0_0) ),
inference(backward_demodulation,[status(thm)],[f2628,f551]) ).
fof(f2606,plain,
( sQ20_spl
| tptp_minus_1 != tptp_float_0_0 ),
inference(backward_demodulation,[status(thm)],[f2628,f537]) ).
fof(f2619,plain,
~ gt(tptp_float_0_0,n3),
inference(backward_demodulation,[status(thm)],[f2628,f1321]) ).
fof(f2627,plain,
( sQ54_spl
| n3 != tptp_float_0_0 ),
inference(backward_demodulation,[status(thm)],[f2628,f1417]) ).
fof(f2628,plain,
tptp_float_0_0 = n0,
inference(forward_demodulation,[status(thm)],[f214,f215]) ).
fof(f2633,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,n2)
| ~ leq(X0,n2)
| ~ leq(tptp_float_0_0,X1)
| ~ leq(tptp_float_0_0,X0) ),
inference(forward_demodulation,[status(thm)],[f2628,f2574]) ).
fof(f2656,plain,
! [X0] :
( X0 = tptp_float_0_0
| ~ leq(X0,n0)
| ~ leq(tptp_float_0_0,X0) ),
inference(forward_demodulation,[status(thm)],[f2628,f2596]) ).
fof(f2657,plain,
! [X0] :
( X0 = tptp_float_0_0
| ~ leq(X0,tptp_float_0_0)
| ~ leq(tptp_float_0_0,X0) ),
inference(forward_demodulation,[status(thm)],[f2628,f2656]) ).
fof(f2700,plain,
( ~ sQ7_spl
| leq(tptp_float_0_0,sK31_skl) ),
inference(forward_demodulation,[status(thm)],[f2628,f415]) ).
fof(f2708,plain,
( ~ sQ8_spl
| leq(tptp_float_0_0,sK32_skl) ),
inference(forward_demodulation,[status(thm)],[f2628,f419]) ).
fof(f2719,plain,
~ gt(tptp_float_0_0,n1),
inference(forward_demodulation,[status(thm)],[f2628,f1338]) ).
fof(f2721,plain,
( n1 = tptp_float_0_0
| ~ leq(n1,tptp_float_0_0) ),
inference(resolution,[status(thm)],[f2719,f124]) ).
fof(f2723,plain,
( n1 = tptp_float_0_0
| gt(n1,tptp_float_0_0) ),
inference(resolution,[status(thm)],[f2719,f104]) ).
fof(f2724,definition,
( sQ97_spl
<=> leq(n1,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f2727,definition,
( sQ98_spl
<=> n1 = tptp_float_0_0 ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2728,plain,
( ~ sQ98_spl
| n1 = tptp_float_0_0 ),
inference(component_clause,[status(thm)],[f2727]) ).
fof(f2730,plain,
( sQ98_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f2721,f2724,f2727]) ).
fof(f2731,definition,
( sQ99_spl
<=> gt(n1,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2734,plain,
( sQ98_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f2723,f2731,f2727]) ).
fof(f2735,plain,
( ~ sQ98_spl
| sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2728,f2573]) ).
fof(f2736,plain,
( ~ sQ98_spl
| sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f2735]) ).
fof(f2805,plain,
( sQ11_spl
| ~ leq(sK32_skl,n2)
| ~ leq(sK31_skl,n2)
| ~ leq(tptp_float_0_0,sK32_skl)
| ~ leq(tptp_float_0_0,sK31_skl) ),
inference(resolution,[status(thm)],[f2633,f432]) ).
fof(f2807,definition,
( sQ100_spl
<=> leq(tptp_float_0_0,sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f2809,plain,
( sQ100_spl
| ~ leq(tptp_float_0_0,sK31_skl) ),
inference(component_clause,[status(thm)],[f2807]) ).
fof(f2810,definition,
( sQ101_spl
<=> leq(tptp_float_0_0,sK32_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2812,plain,
( sQ101_spl
| ~ leq(tptp_float_0_0,sK32_skl) ),
inference(component_clause,[status(thm)],[f2810]) ).
fof(f2813,definition,
( sQ102_spl
<=> leq(sK31_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2815,plain,
( sQ102_spl
| ~ leq(sK31_skl,n2) ),
inference(component_clause,[status(thm)],[f2813]) ).
fof(f2816,definition,
( sQ103_spl
<=> leq(sK32_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f2818,plain,
( sQ103_spl
| ~ leq(sK32_skl,n2) ),
inference(component_clause,[status(thm)],[f2816]) ).
fof(f2819,plain,
( sQ11_spl
| ~ sQ103_spl
| ~ sQ102_spl
| ~ sQ101_spl
| ~ sQ100_spl ),
inference(split_clause,[status(thm)],[f2805,f2807,f2810,f2813,f2816,f430]) ).
fof(f2821,plain,
( sQ103_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2818,f2473]) ).
fof(f2822,plain,
( sQ103_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f2821]) ).
fof(f2862,plain,
( ~ sQ6_spl
| sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2099,f1119]) ).
fof(f2863,plain,
( ~ sQ6_spl
| sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f2862]) ).
fof(f2967,plain,
~ gt(tptp_float_0_0,n2),
inference(forward_demodulation,[status(thm)],[f2628,f2499]) ).
fof(f2969,plain,
( n2 = tptp_float_0_0
| ~ leq(n2,tptp_float_0_0) ),
inference(resolution,[status(thm)],[f2967,f124]) ).
fof(f2971,plain,
( n2 = tptp_float_0_0
| gt(n2,tptp_float_0_0) ),
inference(resolution,[status(thm)],[f2967,f104]) ).
fof(f2972,definition,
( sQ105_spl
<=> leq(n2,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f2975,definition,
( sQ106_spl
<=> n2 = tptp_float_0_0 ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f2976,plain,
( ~ sQ106_spl
| n2 = tptp_float_0_0 ),
inference(component_clause,[status(thm)],[f2975]) ).
fof(f2978,plain,
( sQ106_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f2969,f2972,f2975]) ).
fof(f2979,definition,
( sQ107_spl
<=> gt(n2,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f2982,plain,
( sQ106_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f2971,f2979,f2975]) ).
fof(f2990,plain,
( ~ sQ106_spl
| ~ gt(n2,n1) ),
inference(backward_demodulation,[status(thm)],[f2976,f2719]) ).
fof(f3001,plain,
( ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2990,f302]) ).
fof(f3002,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f3001]) ).
fof(f3074,plain,
( tptp_float_0_0 = tptp_float_0_0
| ~ leq(tptp_float_0_0,tptp_float_0_0) ),
inference(resolution,[status(thm)],[f2657,f109]) ).
fof(f3076,definition,
( sQ108_spl
<=> leq(tptp_float_0_0,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f3078,plain,
( sQ108_spl
| ~ leq(tptp_float_0_0,tptp_float_0_0) ),
inference(component_clause,[status(thm)],[f3076]) ).
fof(f3079,definition,
( sQ109_spl
<=> tptp_float_0_0 = tptp_float_0_0 ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f3082,plain,
( sQ109_spl
| ~ sQ108_spl ),
inference(split_clause,[status(thm)],[f3074,f3076,f3079]) ).
fof(f3083,plain,
( sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3078,f109]) ).
fof(f3084,plain,
sQ108_spl,
inference(contradiction_clause,[status(thm)],[f3083]) ).
fof(f3117,plain,
( sQ21_spl
| tptp_float_0_0 = tptp_minus_1
| ~ leq(tptp_float_0_0,tptp_minus_1) ),
inference(resolution,[status(thm)],[f2598,f124]) ).
fof(f3119,plain,
( sQ21_spl
| tptp_float_0_0 = tptp_minus_1
| gt(tptp_float_0_0,tptp_minus_1) ),
inference(resolution,[status(thm)],[f2598,f104]) ).
fof(f3120,definition,
( sQ110_spl
<=> leq(tptp_float_0_0,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f3123,definition,
( sQ111_spl
<=> tptp_float_0_0 = tptp_minus_1 ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f3124,plain,
( ~ sQ111_spl
| tptp_float_0_0 = tptp_minus_1 ),
inference(component_clause,[status(thm)],[f3123]) ).
fof(f3126,plain,
( sQ21_spl
| sQ111_spl
| ~ sQ110_spl ),
inference(split_clause,[status(thm)],[f3117,f3120,f3123,f539]) ).
fof(f3127,definition,
( sQ112_spl
<=> gt(tptp_float_0_0,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f3130,plain,
( sQ21_spl
| sQ111_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f3119,f3127,f3123,f539]) ).
fof(f3131,plain,
( ~ sQ111_spl
| sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3124,f2606]) ).
fof(f3132,plain,
( ~ sQ111_spl
| sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f3131]) ).
fof(f3229,plain,
( n3 = tptp_float_0_0
| ~ leq(n3,tptp_float_0_0) ),
inference(resolution,[status(thm)],[f2619,f124]) ).
fof(f3231,plain,
( n3 = tptp_float_0_0
| gt(n3,tptp_float_0_0) ),
inference(resolution,[status(thm)],[f2619,f104]) ).
fof(f3233,definition,
( sQ113_spl
<=> leq(n3,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f3236,definition,
( sQ114_spl
<=> n3 = tptp_float_0_0 ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f3237,plain,
( ~ sQ114_spl
| n3 = tptp_float_0_0 ),
inference(component_clause,[status(thm)],[f3236]) ).
fof(f3239,plain,
( sQ114_spl
| ~ sQ113_spl ),
inference(split_clause,[status(thm)],[f3229,f3233,f3236]) ).
fof(f3240,definition,
( sQ115_spl
<=> gt(n3,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f3243,plain,
( sQ114_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f3231,f3240,f3236]) ).
fof(f3244,plain,
( ~ sQ114_spl
| sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3237,f2627]) ).
fof(f3245,plain,
( ~ sQ114_spl
| sQ54_spl ),
inference(contradiction_clause,[status(thm)],[f3244]) ).
fof(f3258,plain,
( ~ sQ9_spl
| sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2446,f2815]) ).
fof(f3259,plain,
( ~ sQ9_spl
| sQ102_spl ),
inference(contradiction_clause,[status(thm)],[f3258]) ).
fof(f3260,plain,
( sQ100_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2809,f2700]) ).
fof(f3261,plain,
( sQ100_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f3260]) ).
fof(f3262,plain,
( sQ101_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2812,f2708]) ).
fof(f3263,plain,
( sQ101_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f3262]) ).
fof(f3264,plain,
$false,
inference(sat_refutation,[status(thm)],[f394,f398,f402,f406,f410,f417,f421,f425,f429,f433,f465,f471,f492,f494,f538,f545,f572,f595,f628,f631,f693,f696,f698,f730,f776,f780,f791,f802,f830,f906,f912,f916,f951,f1069,f1073,f1091,f1105,f1226,f1282,f1286,f1318,f1418,f1422,f1476,f1562,f1663,f1674,f1678,f1701,f1713,f1779,f2204,f2210,f2213,f2245,f2249,f2263,f2283,f2287,f2328,f2357,f2360,f2393,f2405,f2730,f2734,f2736,f2819,f2822,f2863,f2978,f2982,f3002,f3082,f3084,f3126,f3130,f3132,f3239,f3243,f3245,f3259,f3261,f3263]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV116+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 08:33:01 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 3.52/0.90 % Refutation found
% 3.52/0.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.52/0.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.95/0.93 % Elapsed time: 0.558723 seconds
% 2.95/0.93 % CPU time: 4.112388 seconds
% 2.95/0.93 % Total memory used: 148.787 MB
% 2.95/0.93 % Net memory used: 141.780 MB
%------------------------------------------------------------------------------