%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV114+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:40 PM UTC 2026
% Result : Theorem 19.79s 3.20s
% Output : CNFRefutation 2.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 80
% Syntax : Number of formulae : 379 ( 105 unt; 49 def)
% Number of atoms : 1006 ( 178 equ)
% Maximal formula atoms : 39 ( 2 avg)
% Number of connectives : 1032 ( 405 ~; 402 |; 148 &)
% ( 52 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 47 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 22 con; 0-3 aty)
% Number of variables : 287 ( 271 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( X = Y
| gt(Y,X)
| gt(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( gt(Y,X)
=> leq(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( ( X != Y
& leq(X,Y) )
=> gt(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] :
( leq(X,pred(Y))
<=> gt(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y] :
( leq(X,Y)
=> leq(X,succ(Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,C] :
( leq(n0,X)
=> leq(uniform_int_rnd(C,X),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
succ(tptp_minus_1) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X] : plus(X,n1) = succ(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X] : plus(n2,X) = succ(succ(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X] : plus(n3,X) = succ(succ(succ(X))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X] : plus(n4,X) = succ(succ(succ(succ(X)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [X] : plus(n5,X) = succ(succ(succ(succ(succ(X))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] : pred(succ(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [X,Y] :
( leq(succ(X),succ(Y))
<=> leq(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X,Y] :
( leq(succ(X),Y)
=> gt(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ! [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) )
=> ( ! [M] :
( ( leq(M,minus(n0,n1))
& leq(n0,M) )
=> ! [N] :
( ( leq(N,minus(n6,n1))
& leq(n0,N) )
=> a_select3(id_ds1_filter,M,N) = a_select3(id_ds1_filter,N,M) ) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(pminus_ds1_filter,K,L) = a_select3(pminus_ds1_filter,L,K) )
& ! [I,J] :
( ( leq(J,minus(n3,n1))
& leq(I,minus(n3,n1))
& leq(n0,J)
& leq(n0,I) )
=> a_select3(r_ds1_filter,I,J) = a_select3(r_ds1_filter,J,I) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
=> a_select3(q_ds1_filter,G,H) = a_select3(q_ds1_filter,H,G) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ! [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) )
=> ( ! [M] :
( ( leq(M,minus(n0,n1))
& leq(n0,M) )
=> ! [N] :
( ( leq(N,minus(n6,n1))
& leq(n0,N) )
=> a_select3(id_ds1_filter,M,N) = a_select3(id_ds1_filter,N,M) ) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(pminus_ds1_filter,K,L) = a_select3(pminus_ds1_filter,L,K) )
& ! [I,J] :
( ( leq(J,minus(n3,n1))
& leq(I,minus(n3,n1))
& leq(n0,J)
& leq(n0,I) )
=> a_select3(r_ds1_filter,I,J) = a_select3(r_ds1_filter,J,I) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
=> a_select3(q_ds1_filter,G,H) = a_select3(q_ds1_filter,H,G) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f65,axiom,
gt(n0,tptp_minus_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
gt(n1,tptp_minus_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
gt(n1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
gt(n2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
gt(n2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [X] :
( ( leq(X,n0)
& leq(n0,X) )
=> X = n0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [X] :
( ( leq(X,n1)
& leq(n0,X) )
=> ( X = n1
| X = n0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
succ(succ(succ(succ(succ(n0))))) = n5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
succ(succ(succ(succ(succ(succ(n0)))))) = n6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox2/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(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(f216,plain,
succ(tptp_minus_1) = n0,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f217,plain,
! [X0] : plus(X0,n1) = succ(X0),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f220,plain,
! [X0] : plus(n2,X0) = succ(succ(X0)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f222,plain,
! [X0] : plus(n3,X0) = succ(succ(succ(X0))),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f224,plain,
! [X0] : plus(n4,X0) = succ(succ(succ(succ(X0)))),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f226,plain,
! [X0] : plus(n5,X0) = succ(succ(succ(succ(succ(X0))))),
inference(cnf_transformation,[status(thm)],[f38]) ).
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(f230,plain,
! [X,Y] :
( ( ~ leq(X,Y)
| leq(succ(X),succ(Y)) )
& ( leq(X,Y)
| ~ leq(succ(X),succ(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f231,plain,
( ! [X,Y] :
( ~ leq(X,Y)
| leq(succ(X),succ(Y)) )
& ! [X,Y] :
( leq(X,Y)
| ~ leq(succ(X),succ(Y)) ) ),
inference(miniscoping,[status(thm)],[f230]) ).
fof(f233,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| leq(succ(X0),succ(X1)) ),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f234,plain,
! [X,Y] :
( gt(Y,X)
| ~ leq(succ(X),Y) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f235,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(succ(X0),X1) ),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f261,plain,
( ( ? [M] :
( ? [N] :
( a_select3(id_ds1_filter,M,N) != a_select3(id_ds1_filter,N,M)
& leq(N,minus(n6,n1))
& leq(n0,N) )
& leq(M,minus(n0,n1))
& leq(n0,M) )
| ? [K,L] :
( a_select3(pminus_ds1_filter,K,L) != a_select3(pminus_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ? [I,J] :
( a_select3(r_ds1_filter,I,J) != a_select3(r_ds1_filter,J,I)
& leq(J,minus(n3,n1))
& leq(I,minus(n3,n1))
& leq(n0,J)
& leq(n0,I) )
| ? [G,H] :
( a_select3(q_ds1_filter,G,H) != a_select3(q_ds1_filter,H,G)
& leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ! [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,
! [G,H] :
( sP3_prd(H,G)
<=> ( a_select3(q_ds1_filter,G,H) != a_select3(q_ds1_filter,H,G)
& leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f263,definition,
! [I,J] :
( sP4_prd(J,I)
<=> ( a_select3(r_ds1_filter,I,J) != a_select3(r_ds1_filter,J,I)
& leq(J,minus(n3,n1))
& leq(I,minus(n3,n1))
& leq(n0,J)
& leq(n0,I) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f264,definition,
! [K,L] :
( sP5_prd(L,K)
<=> ( a_select3(pminus_ds1_filter,K,L) != a_select3(pminus_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(f265,plain,
( ( ? [M] :
( ? [N] :
( a_select3(id_ds1_filter,M,N) != a_select3(id_ds1_filter,N,M)
& leq(N,minus(n6,n1))
& leq(n0,N) )
& leq(M,minus(n0,n1))
& leq(n0,M) )
| ? [K,L] : sP5_prd(L,K)
| ? [I,J] : sP4_prd(J,I)
| ? [G,H] : sP3_prd(H,G)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ! [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,f264,f263,f262]) ).
fof(f266,plain,
( ( ( a_select3(id_ds1_filter,sK29_skl,sK30_skl) != a_select3(id_ds1_filter,sK30_skl,sK29_skl)
& leq(sK30_skl,minus(n6,n1))
& leq(n0,sK30_skl)
& leq(sK29_skl,minus(n0,n1))
& leq(n0,sK29_skl) )
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ! [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,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl]),skolemize(G,sK23_skl),skolemize(H,sK24_skl),skolemize(I,sK25_skl),skolemize(J,sK26_skl),skolemize(K,sK27_skl),skolemize(L,sK28_skl),skolemize(M,sK29_skl),skolemize(N,sK30_skl)],[f265]) ).
fof(f267,plain,
leq(n0,pv5),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f268,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f269,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)],[f266]) ).
fof(f270,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)],[f266]) ).
fof(f271,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)],[f266]) ).
fof(f272,plain,
( leq(n0,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f273,plain,
( leq(sK29_skl,minus(n0,n1))
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f287,plain,
gt(n0,tptp_minus_1),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f288,plain,
gt(n1,tptp_minus_1),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f295,plain,
gt(n1,n0),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f296,plain,
gt(n2,n0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f302,plain,
gt(n2,n1),
inference(cnf_transformation,[status(thm)],[f80]) ).
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(f328,plain,
succ(succ(succ(succ(succ(n0))))) = n5,
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f329,plain,
succ(succ(succ(succ(succ(succ(n0)))))) = n6,
inference(cnf_transformation,[status(thm)],[f100]) ).
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(f361,plain,
! [G,H] :
( ( a_select3(q_ds1_filter,G,H) = a_select3(q_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G)
| sP3_prd(H,G) )
& ( ( a_select3(q_ds1_filter,G,H) != a_select3(q_ds1_filter,H,G)
& leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
| ~ sP3_prd(H,G) ) ),
inference(NNF_transformation,[status(thm)],[f262]) ).
fof(f362,plain,
( ! [G,H] :
( a_select3(q_ds1_filter,G,H) = a_select3(q_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G)
| sP3_prd(H,G) )
& ! [G,H] :
( ( a_select3(q_ds1_filter,G,H) != a_select3(q_ds1_filter,H,G)
& leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
| ~ sP3_prd(H,G) ) ),
inference(miniscoping,[status(thm)],[f361]) ).
fof(f363,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f364,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f365,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f366,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f367,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X1,X0) != a_select3(q_ds1_filter,X0,X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f369,plain,
! [I,J] :
( ( a_select3(r_ds1_filter,I,J) = a_select3(r_ds1_filter,J,I)
| ~ leq(J,minus(n3,n1))
| ~ leq(I,minus(n3,n1))
| ~ leq(n0,J)
| ~ leq(n0,I)
| sP4_prd(J,I) )
& ( ( a_select3(r_ds1_filter,I,J) != a_select3(r_ds1_filter,J,I)
& leq(J,minus(n3,n1))
& leq(I,minus(n3,n1))
& leq(n0,J)
& leq(n0,I) )
| ~ sP4_prd(J,I) ) ),
inference(NNF_transformation,[status(thm)],[f263]) ).
fof(f370,plain,
( ! [I,J] :
( a_select3(r_ds1_filter,I,J) = a_select3(r_ds1_filter,J,I)
| ~ leq(J,minus(n3,n1))
| ~ leq(I,minus(n3,n1))
| ~ leq(n0,J)
| ~ leq(n0,I)
| sP4_prd(J,I) )
& ! [I,J] :
( ( a_select3(r_ds1_filter,I,J) != a_select3(r_ds1_filter,J,I)
& leq(J,minus(n3,n1))
& leq(I,minus(n3,n1))
& leq(n0,J)
& leq(n0,I) )
| ~ sP4_prd(J,I) ) ),
inference(miniscoping,[status(thm)],[f369]) ).
fof(f371,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f372,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f373,plain,
! [X0,X1] :
( leq(X1,minus(n3,n1))
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f374,plain,
! [X0,X1] :
( leq(X0,minus(n3,n1))
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f375,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X1,X0) != a_select3(r_ds1_filter,X0,X1)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f377,plain,
! [K,L] :
( ( a_select3(pminus_ds1_filter,K,L) = a_select3(pminus_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(pminus_ds1_filter,K,L) != a_select3(pminus_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)],[f264]) ).
fof(f378,plain,
( ! [K,L] :
( a_select3(pminus_ds1_filter,K,L) = a_select3(pminus_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(pminus_ds1_filter,K,L) != a_select3(pminus_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)],[f377]) ).
fof(f379,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f380,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f381,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f382,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f383,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X1,X0) != a_select3(pminus_ds1_filter,X0,X1)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f393,definition,
( sQ0_spl
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f395,plain,
( sQ0_spl
| ~ leq(n0,pv5) ),
inference(component_clause,[status(thm)],[f393]) ).
fof(f396,definition,
( sQ1_spl
<=> leq(pv5,minus(n999,n1)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f398,plain,
( sQ1_spl
| ~ leq(pv5,minus(n999,n1)) ),
inference(component_clause,[status(thm)],[f396]) ).
fof(f399,definition,
( sQ2_spl
<=> sP3_prd(sK24_skl,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( ~ sQ2_spl
| sP3_prd(sK24_skl,sK23_skl) ),
inference(component_clause,[status(thm)],[f399]) ).
fof(f402,definition,
( sQ3_spl
<=> sP4_prd(sK26_skl,sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( ~ sQ3_spl
| sP4_prd(sK26_skl,sK25_skl) ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f405,definition,
( sQ4_spl
<=> sP5_prd(sK28_skl,sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( ~ sQ4_spl
| sP5_prd(sK28_skl,sK27_skl) ),
inference(component_clause,[status(thm)],[f405]) ).
fof(f408,definition,
( sQ5_spl
<=> leq(n0,sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( ~ sQ5_spl
| leq(n0,sK29_skl) ),
inference(component_clause,[status(thm)],[f408]) ).
fof(f411,plain,
( sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f272,f393,f396,f399,f402,f405,f408]) ).
fof(f412,definition,
( sQ6_spl
<=> leq(sK29_skl,minus(n0,n1)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( ~ sQ6_spl
| leq(sK29_skl,minus(n0,n1)) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,plain,
( sQ6_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f273,f393,f396,f399,f402,f405,f412]) ).
fof(f430,plain,
! [X0] : plus(n3,X0) = plus(n2,succ(X0)),
inference(forward_demodulation,[status(thm)],[f220,f222]) ).
fof(f433,plain,
! [X0] : plus(n4,X0) = plus(n2,succ(succ(X0))),
inference(forward_demodulation,[status(thm)],[f220,f224]) ).
fof(f434,plain,
! [X0] : plus(n4,X0) = plus(n3,succ(X0)),
inference(forward_demodulation,[status(thm)],[f430,f433]) ).
fof(f438,plain,
! [X0] : plus(n5,X0) = plus(n2,succ(succ(succ(X0)))),
inference(forward_demodulation,[status(thm)],[f220,f226]) ).
fof(f439,plain,
! [X0] : plus(n5,X0) = plus(n3,succ(succ(X0))),
inference(forward_demodulation,[status(thm)],[f430,f438]) ).
fof(f440,plain,
! [X0] : plus(n5,X0) = plus(n4,succ(X0)),
inference(forward_demodulation,[status(thm)],[f434,f439]) ).
fof(f443,plain,
leq(pv5,pred(n999)),
inference(forward_demodulation,[status(thm)],[f227,f268]) ).
fof(f444,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f269]) ).
fof(f445,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,f444]) ).
fof(f446,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,minus(n3,n1))
| ~ leq(X0,pred(n3))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f270]) ).
fof(f447,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,f446]) ).
fof(f448,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f271]) ).
fof(f449,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,f448]) ).
fof(f453,plain,
plus(n2,succ(succ(succ(n0)))) = n5,
inference(forward_demodulation,[status(thm)],[f220,f328]) ).
fof(f454,plain,
plus(n3,succ(succ(n0))) = n5,
inference(forward_demodulation,[status(thm)],[f430,f453]) ).
fof(f455,plain,
plus(n4,succ(n0)) = n5,
inference(forward_demodulation,[status(thm)],[f434,f454]) ).
fof(f456,plain,
plus(n5,n0) = n5,
inference(forward_demodulation,[status(thm)],[f440,f455]) ).
fof(f457,plain,
plus(n2,succ(succ(succ(succ(n0))))) = n6,
inference(forward_demodulation,[status(thm)],[f220,f329]) ).
fof(f458,plain,
plus(n3,succ(succ(succ(n0)))) = n6,
inference(forward_demodulation,[status(thm)],[f430,f457]) ).
fof(f459,plain,
plus(n4,succ(succ(n0))) = n6,
inference(forward_demodulation,[status(thm)],[f434,f458]) ).
fof(f460,plain,
plus(n5,succ(n0)) = n6,
inference(forward_demodulation,[status(thm)],[f440,f459]) ).
fof(f461,plain,
plus(n5,n1) = n6,
inference(backward_demodulation,[status(thm)],[f330,f460]) ).
fof(f462,plain,
plus(n2,n0) = n2,
inference(forward_demodulation,[status(thm)],[f220,f331]) ).
fof(f465,plain,
! [X0,X1] :
( leq(X1,pred(n6))
| ~ sP3_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f365]) ).
fof(f466,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP3_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f366]) ).
fof(f469,plain,
! [X0,X1] :
( leq(X1,pred(n3))
| ~ sP4_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f373]) ).
fof(f470,plain,
! [X0,X1] :
( leq(X0,pred(n3))
| ~ sP4_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f374]) ).
fof(f473,plain,
! [X0,X1] :
( leq(X1,pred(n6))
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f381]) ).
fof(f474,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f382]) ).
fof(f477,plain,
succ(n5) = n6,
inference(forward_demodulation,[status(thm)],[f217,f461]) ).
fof(f479,plain,
pred(n0) = tptp_minus_1,
inference(paramodulation,[status(thm)],[f216,f228]) ).
fof(f485,plain,
pred(n1) = n0,
inference(paramodulation,[status(thm)],[f330,f228]) ).
fof(f487,plain,
pred(n6) = n5,
inference(paramodulation,[status(thm)],[f477,f228]) ).
fof(f489,plain,
! [X0,X1] :
( leq(X1,n5)
| ~ sP3_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f487,f465]) ).
fof(f490,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f487,f445]) ).
fof(f491,plain,
! [X0,X1] :
( leq(X0,n5)
| ~ sP5_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f487,f474]) ).
fof(f492,plain,
! [X0,X1] :
( leq(X1,n5)
| ~ sP5_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f487,f473]) ).
fof(f493,plain,
! [X0,X1] :
( leq(X0,n5)
| ~ sP3_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f487,f466]) ).
fof(f494,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f487,f449]) ).
fof(f495,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f487,f490]) ).
fof(f496,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f487,f494]) ).
fof(f507,plain,
( n0 = n0
| ~ leq(n0,n0) ),
inference(resolution,[status(thm)],[f320,f109]) ).
fof(f508,definition,
( sQ10_spl
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( sQ10_spl
| ~ leq(n0,n0) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,definition,
( sQ11_spl
<=> n0 = n0 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f507,f508,f511]) ).
fof(f543,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f510,f109]) ).
fof(f544,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f543]) ).
fof(f553,plain,
( n1 = n1
| n1 = n0
| ~ leq(n0,n1) ),
inference(resolution,[status(thm)],[f322,f109]) ).
fof(f554,definition,
( sQ19_spl
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( ~ sQ19_spl
| n0 = n1 ),
inference(component_clause,[status(thm)],[f554]) ).
fof(f585,definition,
( sQ27_spl
<=> leq(n0,n1) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f587,plain,
( sQ27_spl
| ~ leq(n0,n1) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f588,definition,
( sQ28_spl
<=> n1 = n1 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f591,plain,
( sQ28_spl
| sQ19_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f553,f585,f554,f588]) ).
fof(f592,plain,
( sQ1_spl
| ~ leq(pv5,pred(n999)) ),
inference(forward_demodulation,[status(thm)],[f227,f398]) ).
fof(f593,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f592,f443]) ).
fof(f594,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f593]) ).
fof(f595,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f395,f267]) ).
fof(f596,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f595]) ).
fof(f601,plain,
( ~ sQ3_spl
| a_select3(r_ds1_filter,sK25_skl,sK26_skl) != a_select3(r_ds1_filter,sK26_skl,sK25_skl) ),
inference(resolution,[status(thm)],[f375,f403]) ).
fof(f603,plain,
( ~ sQ3_spl
| ~ leq(sK26_skl,pred(n3))
| ~ leq(sK25_skl,pred(n3))
| ~ leq(n0,sK26_skl)
| ~ leq(n0,sK25_skl) ),
inference(resolution,[status(thm)],[f601,f447]) ).
fof(f605,definition,
( sQ29_spl
<=> leq(n0,sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f607,plain,
( sQ29_spl
| ~ leq(n0,sK25_skl) ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f608,definition,
( sQ30_spl
<=> leq(n0,sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f610,plain,
( sQ30_spl
| ~ leq(n0,sK26_skl) ),
inference(component_clause,[status(thm)],[f608]) ).
fof(f611,definition,
( sQ31_spl
<=> leq(sK25_skl,pred(n3)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f614,definition,
( sQ32_spl
<=> leq(sK26_skl,pred(n3)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f616,plain,
( sQ32_spl
| ~ leq(sK26_skl,pred(n3)) ),
inference(component_clause,[status(thm)],[f614]) ).
fof(f617,plain,
( ~ sQ3_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f603,f605,f608,f611,f614,f402]) ).
fof(f627,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f495,f367]) ).
fof(f629,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f627,f364]) ).
fof(f630,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f496,f383]) ).
fof(f632,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f630,f380]) ).
fof(f651,plain,
! [X0] : ~ leq(X0,pred(X0)),
inference(resolution,[status(thm)],[f127,f108]) ).
fof(f780,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f632,f379]) ).
fof(f781,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f629,f363]) ).
fof(f915,plain,
! [X0] : ~ gt(pred(X0),X0),
inference(resolution,[status(thm)],[f651,f122]) ).
fof(f918,plain,
~ leq(n6,n5),
inference(paramodulation,[status(thm)],[f487,f651]) ).
fof(f919,plain,
! [X0] : ~ leq(succ(X0),X0),
inference(paramodulation,[status(thm)],[f228,f651]) ).
fof(f932,plain,
~ gt(tptp_minus_1,n0),
inference(paramodulation,[status(thm)],[f479,f915]) ).
fof(f933,plain,
~ gt(n0,n1),
inference(paramodulation,[status(thm)],[f485,f915]) ).
fof(f934,plain,
~ gt(n5,n6),
inference(paramodulation,[status(thm)],[f487,f915]) ).
fof(f935,plain,
! [X0] : ~ gt(X0,succ(X0)),
inference(paramodulation,[status(thm)],[f228,f915]) ).
fof(f959,plain,
! [X0] :
( sQ32_spl
| ~ sP4_prd(sK26_skl,X0) ),
inference(resolution,[status(thm)],[f616,f470]) ).
fof(f966,plain,
~ leq(n1,pred(n0)),
inference(resolution,[status(thm)],[f933,f127]) ).
fof(f967,plain,
( n1 = n0
| ~ leq(n1,n0) ),
inference(resolution,[status(thm)],[f933,f124]) ).
fof(f969,plain,
( n1 = n0
| gt(n1,n0) ),
inference(resolution,[status(thm)],[f933,f104]) ).
fof(f970,plain,
~ leq(n1,tptp_minus_1),
inference(forward_demodulation,[status(thm)],[f479,f966]) ).
fof(f971,definition,
( sQ37_spl
<=> leq(n1,n0) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f973,plain,
( sQ37_spl
| ~ leq(n1,n0) ),
inference(component_clause,[status(thm)],[f971]) ).
fof(f974,plain,
( sQ19_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f967,f971,f554]) ).
fof(f975,definition,
( sQ38_spl
<=> gt(n1,n0) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f978,plain,
( sQ19_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f969,f975,f554]) ).
fof(f983,plain,
( ~ sQ19_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f555,f295]) ).
fof(f1011,plain,
~ leq(n6,pred(n5)),
inference(resolution,[status(thm)],[f934,f127]) ).
fof(f1012,plain,
( n6 = n5
| ~ leq(n6,n5) ),
inference(resolution,[status(thm)],[f934,f124]) ).
fof(f1014,plain,
( n6 = n5
| gt(n6,n5) ),
inference(resolution,[status(thm)],[f934,f104]) ).
fof(f1015,definition,
( sQ39_spl
<=> leq(n6,n5) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1017,plain,
( sQ39_spl
| ~ leq(n6,n5) ),
inference(component_clause,[status(thm)],[f1015]) ).
fof(f1018,definition,
( sQ40_spl
<=> n6 = n5 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1019,plain,
( ~ sQ40_spl
| n6 = n5 ),
inference(component_clause,[status(thm)],[f1018]) ).
fof(f1021,plain,
( sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1012,f1015,f1018]) ).
fof(f1022,definition,
( sQ41_spl
<=> gt(n6,n5) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1025,plain,
( sQ40_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1014,f1022,f1018]) ).
fof(f1031,plain,
( ~ sQ40_spl
| ~ leq(n5,n5) ),
inference(backward_demodulation,[status(thm)],[f1019,f918]) ).
fof(f1055,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f983,f108]) ).
fof(f1056,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1055]) ).
fof(f1057,plain,
( ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1031,f109]) ).
fof(f1058,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f1057]) ).
fof(f1090,plain,
( n0 = tptp_minus_1
| ~ leq(n0,tptp_minus_1) ),
inference(resolution,[status(thm)],[f932,f124]) ).
fof(f1092,plain,
( n0 = tptp_minus_1
| gt(n0,tptp_minus_1) ),
inference(resolution,[status(thm)],[f932,f104]) ).
fof(f1093,definition,
( sQ42_spl
<=> leq(n0,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1096,definition,
( sQ43_spl
<=> n0 = tptp_minus_1 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1097,plain,
( ~ sQ43_spl
| n0 = tptp_minus_1 ),
inference(component_clause,[status(thm)],[f1096]) ).
fof(f1099,plain,
( sQ43_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1090,f1093,f1096]) ).
fof(f1100,definition,
( sQ44_spl
<=> gt(n0,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1103,plain,
( sQ43_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1092,f1100,f1096]) ).
fof(f1106,plain,
( ~ sQ43_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f1097,f287]) ).
fof(f1178,plain,
( ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1106,f108]) ).
fof(f1179,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f1178]) ).
fof(f1188,plain,
( sQ27_spl
| ~ gt(n1,n0) ),
inference(resolution,[status(thm)],[f587,f122]) ).
fof(f1191,plain,
( sQ27_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f1188,f975,f585]) ).
fof(f1412,plain,
plus(n2,n0) = succ(n1),
inference(paramodulation,[status(thm)],[f330,f220]) ).
fof(f1427,plain,
n2 = succ(n1),
inference(forward_demodulation,[status(thm)],[f462,f1412]) ).
fof(f1442,plain,
plus(n5,n0) = plus(n4,n1),
inference(paramodulation,[status(thm)],[f330,f440]) ).
fof(f1449,plain,
n5 = plus(n4,n1),
inference(forward_demodulation,[status(thm)],[f456,f1442]) ).
fof(f1451,plain,
n5 = succ(n4),
inference(forward_demodulation,[status(thm)],[f217,f1449]) ).
fof(f1514,plain,
~ gt(tptp_minus_1,n1),
inference(resolution,[status(thm)],[f970,f122]) ).
fof(f1528,plain,
~ gt(n1,n2),
inference(paramodulation,[status(thm)],[f1427,f935]) ).
fof(f1529,plain,
~ leq(n2,n1),
inference(paramodulation,[status(thm)],[f1427,f919]) ).
fof(f1542,plain,
~ gt(n4,n5),
inference(paramodulation,[status(thm)],[f1451,f935]) ).
fof(f1546,plain,
pred(n5) = n4,
inference(paramodulation,[status(thm)],[f1451,f228]) ).
fof(f1550,plain,
~ leq(n6,n4),
inference(backward_demodulation,[status(thm)],[f1546,f1011]) ).
fof(f1573,plain,
( n1 = tptp_minus_1
| ~ leq(n1,tptp_minus_1) ),
inference(resolution,[status(thm)],[f1514,f124]) ).
fof(f1575,plain,
( n1 = tptp_minus_1
| gt(n1,tptp_minus_1) ),
inference(resolution,[status(thm)],[f1514,f104]) ).
fof(f1576,definition,
( sQ56_spl
<=> leq(n1,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1579,definition,
( sQ57_spl
<=> n1 = tptp_minus_1 ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1580,plain,
( ~ sQ57_spl
| n1 = tptp_minus_1 ),
inference(component_clause,[status(thm)],[f1579]) ).
fof(f1582,plain,
( sQ57_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1573,f1576,f1579]) ).
fof(f1583,definition,
( sQ58_spl
<=> gt(n1,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1586,plain,
( sQ57_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1575,f1583,f1579]) ).
fof(f1589,plain,
( ~ sQ57_spl
| gt(tptp_minus_1,tptp_minus_1) ),
inference(backward_demodulation,[status(thm)],[f1580,f288]) ).
fof(f1641,plain,
( n5 = n4
| ~ leq(n5,n4) ),
inference(resolution,[status(thm)],[f1542,f124]) ).
fof(f1643,plain,
( n5 = n4
| gt(n5,n4) ),
inference(resolution,[status(thm)],[f1542,f104]) ).
fof(f1644,definition,
( sQ59_spl
<=> leq(n5,n4) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1647,definition,
( sQ60_spl
<=> n5 = n4 ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1648,plain,
( ~ sQ60_spl
| n5 = n4 ),
inference(component_clause,[status(thm)],[f1647]) ).
fof(f1650,plain,
( sQ60_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f1641,f1644,f1647]) ).
fof(f1651,definition,
( sQ61_spl
<=> gt(n5,n4) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1654,plain,
( sQ60_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1643,f1651,f1647]) ).
fof(f1659,plain,
( ~ sQ60_spl
| n4 = succ(n4) ),
inference(backward_demodulation,[status(thm)],[f1648,f1451]) ).
fof(f1664,plain,
( ~ sQ60_spl
| succ(n4) = n6 ),
inference(backward_demodulation,[status(thm)],[f1648,f477]) ).
fof(f1667,plain,
( sQ39_spl
| ~ sQ60_spl
| ~ leq(n6,n4) ),
inference(backward_demodulation,[status(thm)],[f1648,f1017]) ).
fof(f1728,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1589,f108]) ).
fof(f1729,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f1728]) ).
fof(f1730,plain,
! [X0,X1] : ~ sP3_prd(X0,X1),
inference(backward_subsumption_resolution,[status(thm)],[f493,f1731]) ).
fof(f1731,plain,
! [X0,X1] :
( ~ sP3_prd(X0,X1)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f781,f489]) ).
fof(f1732,plain,
! [X0,X1] : ~ sP5_prd(X0,X1),
inference(backward_subsumption_resolution,[status(thm)],[f492,f1733]) ).
fof(f1733,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f780,f491]) ).
fof(f1766,plain,
( ~ sQ60_spl
| n4 = n6 ),
inference(forward_demodulation,[status(thm)],[f1659,f1664]) ).
fof(f1770,plain,
( sQ39_spl
| ~ sQ60_spl
| ~ leq(n4,n4) ),
inference(forward_demodulation,[status(thm)],[f1766,f1667]) ).
fof(f1771,plain,
( sQ39_spl
| ~ sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1770,f109]) ).
fof(f1772,plain,
( sQ39_spl
| ~ sQ60_spl ),
inference(contradiction_clause,[status(thm)],[f1771]) ).
fof(f1773,plain,
( ~ sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f400,f1730]) ).
fof(f1774,plain,
( ~ sQ4_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f406,f1732]) ).
fof(f1775,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1773]) ).
fof(f1776,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1774]) ).
fof(f1779,plain,
( ~ sQ3_spl
| sQ32_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f403,f959]) ).
fof(f1780,plain,
( ~ sQ3_spl
| sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f1779]) ).
fof(f1818,plain,
( ~ sQ3_spl
| leq(n0,sK26_skl) ),
inference(resolution,[status(thm)],[f403,f372]) ).
fof(f1819,plain,
( ~ sQ3_spl
| leq(n0,sK25_skl) ),
inference(resolution,[status(thm)],[f403,f371]) ).
fof(f1828,plain,
~ leq(succ(n1),tptp_minus_1),
inference(resolution,[status(thm)],[f1514,f235]) ).
fof(f1833,plain,
~ leq(n2,tptp_minus_1),
inference(forward_demodulation,[status(thm)],[f1427,f1828]) ).
fof(f1910,plain,
( n2 = n1
| ~ leq(n2,n1) ),
inference(resolution,[status(thm)],[f1528,f124]) ).
fof(f1912,plain,
( n2 = n1
| gt(n2,n1) ),
inference(resolution,[status(thm)],[f1528,f104]) ).
fof(f1914,definition,
( sQ62_spl
<=> leq(n2,n1) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1917,definition,
( sQ63_spl
<=> n2 = n1 ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1918,plain,
( ~ sQ63_spl
| n2 = n1 ),
inference(component_clause,[status(thm)],[f1917]) ).
fof(f1920,plain,
( sQ63_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f1910,f1914,f1917]) ).
fof(f1921,definition,
( sQ64_spl
<=> gt(n2,n1) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1924,plain,
( sQ63_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1912,f1921,f1917]) ).
fof(f1926,plain,
( ~ sQ63_spl
| ~ leq(n1,n1) ),
inference(backward_demodulation,[status(thm)],[f1918,f1529]) ).
fof(f2005,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1926,f109]) ).
fof(f2006,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f2005]) ).
fof(f2096,plain,
( sQ29_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f607,f1819]) ).
fof(f2097,plain,
( sQ29_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f2096]) ).
fof(f2149,plain,
( ~ sQ6_spl
| leq(sK29_skl,pred(n0)) ),
inference(forward_demodulation,[status(thm)],[f227,f413]) ).
fof(f2150,plain,
( ~ sQ6_spl
| leq(sK29_skl,tptp_minus_1) ),
inference(forward_demodulation,[status(thm)],[f479,f2149]) ).
fof(f2153,plain,
( ~ sQ5_spl
| leq(succ(n0),succ(sK29_skl)) ),
inference(resolution,[status(thm)],[f409,f233]) ).
fof(f2161,plain,
( ~ sQ5_spl
| leq(n1,succ(sK29_skl)) ),
inference(forward_demodulation,[status(thm)],[f330,f2153]) ).
fof(f2200,plain,
~ gt(n4,n6),
inference(resolution,[status(thm)],[f1550,f122]) ).
fof(f2231,plain,
( ~ sQ6_spl
| leq(succ(sK29_skl),succ(tptp_minus_1)) ),
inference(resolution,[status(thm)],[f2150,f233]) ).
fof(f2239,plain,
( ~ sQ6_spl
| leq(succ(sK29_skl),n0) ),
inference(forward_demodulation,[status(thm)],[f216,f2231]) ).
fof(f2279,plain,
~ gt(succ(tptp_minus_1),n2),
inference(resolution,[status(thm)],[f1833,f135]) ).
fof(f2280,plain,
~ gt(tptp_minus_1,n2),
inference(resolution,[status(thm)],[f1833,f122]) ).
fof(f2283,plain,
~ gt(n0,n2),
inference(forward_demodulation,[status(thm)],[f216,f2279]) ).
fof(f2305,plain,
( n6 = n4
| ~ leq(n6,n4) ),
inference(resolution,[status(thm)],[f2200,f124]) ).
fof(f2307,plain,
( n6 = n4
| gt(n6,n4) ),
inference(resolution,[status(thm)],[f2200,f104]) ).
fof(f2308,definition,
( sQ68_spl
<=> leq(n6,n4) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f2311,definition,
( sQ69_spl
<=> n6 = n4 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f2312,plain,
( ~ sQ69_spl
| n6 = n4 ),
inference(component_clause,[status(thm)],[f2311]) ).
fof(f2314,plain,
( sQ69_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f2305,f2308,f2311]) ).
fof(f2315,definition,
( sQ70_spl
<=> gt(n6,n4) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f2318,plain,
( sQ69_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f2307,f2315,f2311]) ).
fof(f2322,plain,
( ~ sQ69_spl
| ~ leq(n4,n4) ),
inference(backward_demodulation,[status(thm)],[f2312,f1550]) ).
fof(f2351,plain,
( ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2322,f109]) ).
fof(f2352,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f2351]) ).
fof(f2355,plain,
( n2 = n0
| ~ leq(n2,n0) ),
inference(resolution,[status(thm)],[f2283,f124]) ).
fof(f2357,plain,
( n2 = n0
| gt(n2,n0) ),
inference(resolution,[status(thm)],[f2283,f104]) ).
fof(f2359,definition,
( sQ71_spl
<=> leq(n2,n0) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f2362,definition,
( sQ72_spl
<=> n2 = n0 ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f2363,plain,
( ~ sQ72_spl
| n2 = n0 ),
inference(component_clause,[status(thm)],[f2362]) ).
fof(f2365,plain,
( sQ72_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f2355,f2359,f2362]) ).
fof(f2366,definition,
( sQ73_spl
<=> gt(n2,n0) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f2369,plain,
( sQ72_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f2357,f2366,f2362]) ).
fof(f2374,plain,
( ~ sQ72_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f2363,f296]) ).
fof(f2446,plain,
( ~ sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2374,f108]) ).
fof(f2447,plain,
~ sQ72_spl,
inference(contradiction_clause,[status(thm)],[f2446]) ).
fof(f2687,plain,
( n2 = tptp_minus_1
| ~ leq(n2,tptp_minus_1) ),
inference(resolution,[status(thm)],[f2280,f124]) ).
fof(f2689,plain,
( n2 = tptp_minus_1
| gt(n2,tptp_minus_1) ),
inference(resolution,[status(thm)],[f2280,f104]) ).
fof(f2690,definition,
( sQ88_spl
<=> leq(n2,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2693,definition,
( sQ89_spl
<=> n2 = tptp_minus_1 ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2694,plain,
( ~ sQ89_spl
| n2 = tptp_minus_1 ),
inference(component_clause,[status(thm)],[f2693]) ).
fof(f2696,plain,
( sQ89_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f2687,f2690,f2693]) ).
fof(f2697,definition,
( sQ90_spl
<=> gt(n2,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2700,plain,
( sQ89_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2689,f2697,f2693]) ).
fof(f2705,plain,
( ~ sQ89_spl
| gt(tptp_minus_1,n1) ),
inference(backward_demodulation,[status(thm)],[f2694,f302]) ).
fof(f2784,plain,
( ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2705,f1514]) ).
fof(f2785,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f2784]) ).
fof(f2868,plain,
( ~ sQ6_spl
| succ(sK29_skl) = n0
| ~ leq(n0,succ(sK29_skl)) ),
inference(resolution,[status(thm)],[f2239,f320]) ).
fof(f2877,definition,
( sQ91_spl
<=> leq(n0,succ(sK29_skl)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2879,plain,
( sQ91_spl
| ~ leq(n0,succ(sK29_skl)) ),
inference(component_clause,[status(thm)],[f2877]) ).
fof(f2880,definition,
( sQ92_spl
<=> succ(sK29_skl) = n0 ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2881,plain,
( ~ sQ92_spl
| succ(sK29_skl) = n0 ),
inference(component_clause,[status(thm)],[f2880]) ).
fof(f2883,plain,
( ~ sQ6_spl
| sQ92_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f2868,f2877,f2880,f412]) ).
fof(f2886,plain,
( ~ sQ5_spl
| ~ sQ92_spl
| leq(n1,n0) ),
inference(backward_demodulation,[status(thm)],[f2881,f2161]) ).
fof(f2893,plain,
( ~ sQ5_spl
| ~ sQ92_spl
| sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2886,f973]) ).
fof(f2894,plain,
( ~ sQ5_spl
| ~ sQ92_spl
| sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f2893]) ).
fof(f2944,plain,
( ~ sQ3_spl
| leq(sK25_skl,pred(n3)) ),
inference(resolution,[status(thm)],[f469,f403]) ).
fof(f2945,plain,
( ~ sQ3_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f2944,f611,f402]) ).
fof(f2947,plain,
( sQ30_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f610,f1818]) ).
fof(f2948,plain,
( sQ30_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f2947]) ).
fof(f2995,plain,
! [X0] :
( uniform_int_rnd(X0,n1) = n1
| uniform_int_rnd(X0,n1) = n0
| ~ leq(n0,uniform_int_rnd(X0,n1))
| ~ leq(n0,n1) ),
inference(resolution,[status(thm)],[f138,f322]) ).
fof(f2996,plain,
! [X0] :
( uniform_int_rnd(X0,n0) = n0
| ~ leq(n0,uniform_int_rnd(X0,n0))
| ~ leq(n0,n0) ),
inference(resolution,[status(thm)],[f138,f320]) ).
fof(f3005,definition,
! [X0] :
( sQ93_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,[sQ93_spl])],[split_symbol_definition]) ).
fof(f3008,plain,
( sQ93_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f2995,f585,f3005]) ).
fof(f3009,definition,
! [X0] :
( sQ94_spl
<=> ( uniform_int_rnd(X0,n0) = n0
| ~ leq(n0,uniform_int_rnd(X0,n0)) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f3012,plain,
( sQ94_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f2996,f508,f3009]) ).
fof(f3051,plain,
( sQ91_spl
| ~ leq(n0,sK29_skl) ),
inference(resolution,[status(thm)],[f2879,f131]) ).
fof(f3056,plain,
( sQ91_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3051,f409]) ).
fof(f3057,plain,
( sQ91_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f3056]) ).
fof(f3058,plain,
$false,
inference(sat_refutation,[status(thm)],[f411,f415,f542,f544,f591,f594,f596,f617,f974,f978,f1021,f1025,f1056,f1058,f1099,f1103,f1179,f1191,f1582,f1586,f1650,f1654,f1729,f1772,f1775,f1776,f1780,f1920,f1924,f2006,f2097,f2314,f2318,f2352,f2365,f2369,f2447,f2696,f2700,f2785,f2883,f2894,f2945,f2948,f3008,f3012,f3057]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV114+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n005.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 21 08:31:18 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.09/0.58 % Drodi V4.1.1
% 19.79/3.20 % Refutation found
% 19.79/3.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.79/3.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.02/3.24 % Elapsed time: 2.660255 seconds
% 2.02/3.24 % CPU time: 20.715325 seconds
% 2.02/3.24 % Total memory used: 198.407 MB
% 2.02/3.24 % Net memory used: 182.953 MB
%------------------------------------------------------------------------------