%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV109+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 : n020.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 53.18s 7.28s
% Output : CNFRefutation 53.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 38
% Syntax : Number of formulae : 225 ( 76 unt; 21 def)
% Number of atoms : 836 ( 130 equ)
% Maximal formula atoms : 56 ( 3 avg)
% Number of connectives : 965 ( 354 ~; 368 |; 195 &)
% ( 21 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 18 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 23 con; 0-3 aty)
% Number of variables : 303 ( 283 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
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(f30,axiom,
! [X] : plus(n1,X) = succ(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X] : plus(X,n3) = succ(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(f35,axiom,
! [X] : plus(X,n4) = succ(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(f37,axiom,
! [X] : plus(X,n5) = succ(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(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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& leq(n0,pv5) )
=> ( ! [S] :
( ( leq(S,minus(n6,n1))
& leq(n0,S) )
=> ! [T] :
( ( leq(T,minus(n6,n1))
& leq(n0,T) )
=> a_select3(id_ds1_filter,S,T) = a_select3(id_ds1_filter,T,S) ) )
& ! [Q,R] :
( ( leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
=> a_select3(pminus_ds1_filter,Q,R) = a_select3(pminus_ds1_filter,R,Q) )
& ! [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) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
file('/export/starexec/sandbox2/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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& leq(n0,pv5) )
=> ( ! [S] :
( ( leq(S,minus(n6,n1))
& leq(n0,S) )
=> ! [T] :
( ( leq(T,minus(n6,n1))
& leq(n0,T) )
=> a_select3(id_ds1_filter,S,T) = a_select3(id_ds1_filter,T,S) ) )
& ! [Q,R] :
( ( leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
=> a_select3(pminus_ds1_filter,Q,R) = a_select3(pminus_ds1_filter,R,Q) )
& ! [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) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f70,axiom,
gt(n5,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
gt(n3,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,axiom,
gt(n5,n1),
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(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(f218,plain,
! [X0] : plus(n1,X0) = succ(X0),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f221,plain,
! [X0] : plus(X0,n3) = succ(succ(succ(X0))),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f222,plain,
! [X0] : plus(n3,X0) = succ(succ(succ(X0))),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f223,plain,
! [X0] : plus(X0,n4) = succ(succ(succ(succ(X0)))),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f224,plain,
! [X0] : plus(n4,X0) = succ(succ(succ(succ(X0)))),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f225,plain,
! [X0] : plus(X0,n5) = succ(succ(succ(succ(succ(X0))))),
inference(cnf_transformation,[status(thm)],[f37]) ).
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(f261,plain,
( ( ? [S] :
( ? [T] :
( a_select3(id_ds1_filter,S,T) != a_select3(id_ds1_filter,T,S)
& leq(T,minus(n6,n1))
& leq(n0,T) )
& leq(S,minus(n6,n1))
& leq(n0,S) )
| ? [Q,R] :
( a_select3(pminus_ds1_filter,Q,R) != a_select3(pminus_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
| ? [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) )
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ! [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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& leq(n0,pv5) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f262,definition,
! [K,L] :
( sP3_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,[sP3_prd])],[]) ).
fof(f263,definition,
! [M,N] :
( sP4_prd(N,M)
<=> ( 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) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f264,definition,
! [O,P] :
( sP5_prd(P,O)
<=> ( 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) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f265,definition,
! [Q,R] :
( sP6_prd(R,Q)
<=> ( a_select3(pminus_ds1_filter,Q,R) != a_select3(pminus_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f266,plain,
( ( ? [S] :
( ? [T] :
( a_select3(id_ds1_filter,S,T) != a_select3(id_ds1_filter,T,S)
& leq(T,minus(n6,n1))
& leq(n0,T) )
& leq(S,minus(n6,n1))
& leq(n0,S) )
| ? [Q,R] : sP6_prd(R,Q)
| ? [O,P] : sP5_prd(P,O)
| ? [M,N] : sP4_prd(N,M)
| ? [K,L] : sP3_prd(L,K)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ! [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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& leq(n0,pv5) ),
inference(formula_renaming,[status(thm)],[f261,f265,f264,f263,f262]) ).
fof(f267,plain,
( ( ( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
& leq(sK32_skl,minus(n6,n1))
& leq(n0,sK32_skl)
& leq(sK31_skl,minus(n6,n1))
& leq(n0,sK31_skl) )
| sP6_prd(sK30_skl,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) )
& ! [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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& 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,sK31_skl,sK32_skl]),skolemize(K,sK23_skl),skolemize(L,sK24_skl),skolemize(M,sK25_skl),skolemize(N,sK26_skl),skolemize(O,sK27_skl),skolemize(P,sK28_skl),skolemize(Q,sK29_skl),skolemize(R,sK30_skl),skolemize(S,sK31_skl),skolemize(T,sK32_skl)],[f266]) ).
fof(f268,plain,
leq(n0,pv5),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f270,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f272,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)],[f267]) ).
fof(f273,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)],[f267]) ).
fof(f274,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)],[f267]) ).
fof(f276,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)],[f267]) ).
fof(f277,plain,
( leq(n0,sK31_skl)
| sP6_prd(sK30_skl,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)],[f267]) ).
fof(f278,plain,
( leq(sK31_skl,minus(n6,n1))
| sP6_prd(sK30_skl,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)],[f267]) ).
fof(f279,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,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)],[f267]) ).
fof(f280,plain,
( leq(sK32_skl,minus(n6,n1))
| sP6_prd(sK30_skl,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)],[f267]) ).
fof(f281,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,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)],[f267]) ).
fof(f297,plain,
gt(n5,n0),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f302,plain,
gt(n3,n0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f304,plain,
gt(n5,n1),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f334,plain,
succ(succ(succ(succ(succ(succ(n0)))))) = n6,
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f335,plain,
succ(n0) = n1,
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f366,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)
| sP3_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) )
| ~ sP3_prd(L,K) ) ),
inference(NNF_transformation,[status(thm)],[f262]) ).
fof(f367,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)
| sP3_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) )
| ~ sP3_prd(L,K) ) ),
inference(miniscoping,[status(thm)],[f366]) ).
fof(f368,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f369,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f370,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f371,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f372,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)],[f367]) ).
fof(f374,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)
| sP4_prd(N,M) )
& ( ( 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) )
| ~ sP4_prd(N,M) ) ),
inference(NNF_transformation,[status(thm)],[f263]) ).
fof(f375,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)
| sP4_prd(N,M) )
& ! [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) )
| ~ sP4_prd(N,M) ) ),
inference(miniscoping,[status(thm)],[f374]) ).
fof(f376,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f377,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f378,plain,
! [X0,X1] :
( leq(X1,minus(n3,n1))
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f379,plain,
! [X0,X1] :
( leq(X0,minus(n3,n1))
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f380,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)],[f375]) ).
fof(f382,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)
| sP5_prd(P,O) )
& ( ( 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) )
| ~ sP5_prd(P,O) ) ),
inference(NNF_transformation,[status(thm)],[f264]) ).
fof(f383,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)
| sP5_prd(P,O) )
& ! [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) )
| ~ sP5_prd(P,O) ) ),
inference(miniscoping,[status(thm)],[f382]) ).
fof(f384,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f385,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f386,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f387,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f388,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)],[f383]) ).
fof(f390,plain,
! [Q,R] :
( ( a_select3(pminus_ds1_filter,Q,R) = a_select3(pminus_ds1_filter,R,Q)
| ~ leq(R,minus(n6,n1))
| ~ leq(Q,minus(n6,n1))
| ~ leq(n0,R)
| ~ leq(n0,Q)
| sP6_prd(R,Q) )
& ( ( a_select3(pminus_ds1_filter,Q,R) != a_select3(pminus_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
| ~ sP6_prd(R,Q) ) ),
inference(NNF_transformation,[status(thm)],[f265]) ).
fof(f391,plain,
( ! [Q,R] :
( a_select3(pminus_ds1_filter,Q,R) = a_select3(pminus_ds1_filter,R,Q)
| ~ leq(R,minus(n6,n1))
| ~ leq(Q,minus(n6,n1))
| ~ leq(n0,R)
| ~ leq(n0,Q)
| sP6_prd(R,Q) )
& ! [Q,R] :
( ( a_select3(pminus_ds1_filter,Q,R) != a_select3(pminus_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
| ~ sP6_prd(R,Q) ) ),
inference(miniscoping,[status(thm)],[f390]) ).
fof(f392,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f393,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f394,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f395,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f396,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X1,X0) != a_select3(pminus_ds1_filter,X0,X1)
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f406,definition,
( sQ0_spl
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( sQ0_spl
| ~ leq(n0,pv5) ),
inference(component_clause,[status(thm)],[f406]) ).
fof(f409,definition,
( sQ1_spl
<=> leq(pv5,minus(n999,n1)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( sQ1_spl
| ~ leq(pv5,minus(n999,n1)) ),
inference(component_clause,[status(thm)],[f409]) ).
fof(f412,definition,
( sQ2_spl
<=> sP3_prd(sK24_skl,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( ~ sQ2_spl
| sP3_prd(sK24_skl,sK23_skl) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,definition,
( sQ3_spl
<=> sP4_prd(sK26_skl,sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f416,plain,
( ~ sQ3_spl
| sP4_prd(sK26_skl,sK25_skl) ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f418,definition,
( sQ4_spl
<=> sP5_prd(sK28_skl,sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( ~ sQ4_spl
| sP5_prd(sK28_skl,sK27_skl) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,definition,
( sQ5_spl
<=> sP6_prd(sK30_skl,sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( ~ sQ5_spl
| sP6_prd(sK30_skl,sK29_skl) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,definition,
( sQ6_spl
<=> leq(n0,sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f427,plain,
( sQ6_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f277,f406,f409,f412,f415,f418,f421,f424]) ).
fof(f428,definition,
( sQ7_spl
<=> leq(sK31_skl,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( ~ sQ7_spl
| leq(sK31_skl,minus(n6,n1)) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,plain,
( sQ7_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f278,f406,f409,f412,f415,f418,f421,f428]) ).
fof(f432,definition,
( sQ8_spl
<=> leq(n0,sK32_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( sQ8_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f279,f406,f409,f412,f415,f418,f421,f432]) ).
fof(f436,definition,
( sQ9_spl
<=> leq(sK32_skl,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f437,plain,
( ~ sQ9_spl
| leq(sK32_skl,minus(n6,n1)) ),
inference(component_clause,[status(thm)],[f436]) ).
fof(f439,plain,
( sQ9_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f280,f406,f409,f412,f415,f418,f421,f436]) ).
fof(f440,definition,
( sQ10_spl
<=> a_select3(id_ds1_filter,sK31_skl,sK32_skl) = a_select3(id_ds1_filter,sK32_skl,sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( sQ10_spl
| a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,plain,
( ~ sQ10_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f281,f406,f409,f412,f415,f418,f421,f440]) ).
fof(f445,plain,
! [X0] : plus(n3,X0) = plus(X0,n3),
inference(forward_demodulation,[status(thm)],[f221,f222]) ).
fof(f446,plain,
! [X0] : plus(X0,n4) = plus(succ(X0),n3),
inference(forward_demodulation,[status(thm)],[f221,f223]) ).
fof(f447,plain,
! [X0] : plus(X0,n4) = plus(n3,succ(X0)),
inference(forward_demodulation,[status(thm)],[f445,f446]) ).
fof(f448,plain,
! [X0] : plus(n4,X0) = plus(succ(X0),n3),
inference(forward_demodulation,[status(thm)],[f221,f224]) ).
fof(f449,plain,
! [X0] : plus(n4,X0) = plus(n3,succ(X0)),
inference(forward_demodulation,[status(thm)],[f445,f448]) ).
fof(f450,plain,
! [X0] : plus(n4,X0) = plus(X0,n4),
inference(forward_demodulation,[status(thm)],[f447,f449]) ).
fof(f451,plain,
! [X0] : plus(X0,n5) = plus(succ(succ(X0)),n3),
inference(forward_demodulation,[status(thm)],[f221,f225]) ).
fof(f452,plain,
! [X0] : plus(X0,n5) = plus(n3,succ(succ(X0))),
inference(forward_demodulation,[status(thm)],[f445,f451]) ).
fof(f453,plain,
! [X0] : plus(X0,n5) = plus(succ(X0),n4),
inference(forward_demodulation,[status(thm)],[f447,f452]) ).
fof(f454,plain,
! [X0] : plus(X0,n5) = plus(n4,succ(X0)),
inference(forward_demodulation,[status(thm)],[f450,f453]) ).
fof(f455,plain,
! [X0] : plus(n5,X0) = plus(succ(succ(X0)),n3),
inference(forward_demodulation,[status(thm)],[f221,f226]) ).
fof(f456,plain,
! [X0] : plus(n5,X0) = plus(n3,succ(succ(X0))),
inference(forward_demodulation,[status(thm)],[f445,f455]) ).
fof(f457,plain,
! [X0] : plus(n5,X0) = plus(succ(X0),n4),
inference(forward_demodulation,[status(thm)],[f447,f456]) ).
fof(f458,plain,
! [X0] : plus(n5,X0) = plus(n4,succ(X0)),
inference(forward_demodulation,[status(thm)],[f450,f457]) ).
fof(f459,plain,
! [X0] : plus(n5,X0) = plus(X0,n5),
inference(forward_demodulation,[status(thm)],[f454,f458]) ).
fof(f462,plain,
leq(pv5,pred(n999)),
inference(forward_demodulation,[status(thm)],[f227,f270]) ).
fof(f464,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,f272]) ).
fof(f465,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,f464]) ).
fof(f466,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,f273]) ).
fof(f467,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,f466]) ).
fof(f468,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,f274]) ).
fof(f469,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,f468]) ).
fof(f472,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,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f276]) ).
fof(f473,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,f472]) ).
fof(f482,plain,
plus(succ(succ(succ(n0))),n3) = n6,
inference(forward_demodulation,[status(thm)],[f221,f334]) ).
fof(f483,plain,
plus(n3,succ(succ(succ(n0)))) = n6,
inference(forward_demodulation,[status(thm)],[f445,f482]) ).
fof(f484,plain,
plus(succ(succ(n0)),n4) = n6,
inference(forward_demodulation,[status(thm)],[f447,f483]) ).
fof(f485,plain,
plus(n4,succ(succ(n0))) = n6,
inference(forward_demodulation,[status(thm)],[f450,f484]) ).
fof(f486,plain,
plus(succ(n0),n5) = n6,
inference(forward_demodulation,[status(thm)],[f454,f485]) ).
fof(f487,plain,
plus(n5,succ(n0)) = n6,
inference(forward_demodulation,[status(thm)],[f459,f486]) ).
fof(f488,plain,
plus(n5,n1) = n6,
inference(backward_demodulation,[status(thm)],[f335,f487]) ).
fof(f491,plain,
! [X0,X1] :
( leq(X1,pred(n6))
| ~ sP3_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f370]) ).
fof(f492,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP3_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f371]) ).
fof(f495,plain,
! [X0,X1] :
( leq(X1,pred(n3))
| ~ sP4_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f378]) ).
fof(f496,plain,
! [X0,X1] :
( leq(X0,pred(n3))
| ~ sP4_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f379]) ).
fof(f499,plain,
! [X0,X1] :
( leq(X1,pred(n6))
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f386]) ).
fof(f500,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f387]) ).
fof(f503,plain,
! [X0,X1] :
( leq(X1,pred(n6))
| ~ sP6_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f394]) ).
fof(f504,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP6_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f395]) ).
fof(f507,plain,
plus(n1,n5) = n6,
inference(forward_demodulation,[status(thm)],[f459,f488]) ).
fof(f508,plain,
succ(n5) = n6,
inference(forward_demodulation,[status(thm)],[f218,f507]) ).
fof(f569,plain,
leq(n1,n5),
inference(resolution,[status(thm)],[f122,f304]) ).
fof(f570,plain,
leq(n0,n5),
inference(resolution,[status(thm)],[f122,f297]) ).
fof(f575,plain,
leq(n0,n3),
inference(resolution,[status(thm)],[f122,f302]) ).
fof(f693,plain,
( sQ1_spl
| ~ leq(pv5,pred(n999)) ),
inference(forward_demodulation,[status(thm)],[f227,f411]) ).
fof(f694,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f693,f462]) ).
fof(f695,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f694]) ).
fof(f696,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f268]) ).
fof(f697,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f696]) ).
fof(f1899,plain,
( ~ sQ7_spl
| leq(sK31_skl,pred(n6)) ),
inference(forward_demodulation,[status(thm)],[f227,f429]) ).
fof(f1901,plain,
( ~ sQ9_spl
| leq(sK32_skl,pred(n6)) ),
inference(forward_demodulation,[status(thm)],[f227,f437]) ).
fof(f1969,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,pred(n3))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f467,f380]) ).
fof(f1971,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,pred(n3))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1969,f377]) ).
fof(f2344,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,pred(n3)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1971,f376]) ).
fof(f2345,plain,
! [X0,X1] :
( ~ sP4_prd(X0,X1)
| ~ leq(X0,pred(n3)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2344,f495]) ).
fof(f2346,plain,
! [X0,X1] : ~ sP4_prd(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f2345,f496]) ).
fof(f3032,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f465,f372]) ).
fof(f3038,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3032,f369]) ).
fof(f3387,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3038,f491]) ).
fof(f3508,plain,
! [X0,X1] :
( ~ sP3_prd(X0,X1)
| ~ leq(X0,pred(n6)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3387,f368]) ).
fof(f3509,plain,
! [X0,X1] : ~ sP3_prd(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f492,f3508]) ).
fof(f4501,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f469,f396]) ).
fof(f4502,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f469,f388]) ).
fof(f4513,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4501,f393]) ).
fof(f4514,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4502,f385]) ).
fof(f4610,definition,
( sQ164_spl
<=> leq(n0,n3) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f4612,plain,
( sQ164_spl
| ~ leq(n0,n3) ),
inference(component_clause,[status(thm)],[f4610]) ).
fof(f4792,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f3509]) ).
fof(f4793,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f4792]) ).
fof(f4802,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4514,f384]) ).
fof(f4803,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4513,f392]) ).
fof(f4806,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f416,f2346]) ).
fof(f4807,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f4806]) ).
fof(f4858,plain,
pred(n6) = n5,
inference(paramodulation,[status(thm)],[f508,f228]) ).
fof(f4866,plain,
! [X0,X1] :
( leq(X0,n5)
| ~ sP5_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4858,f500]) ).
fof(f4883,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,pred(n6)) ),
inference(backward_demodulation,[status(thm)],[f4858,f4803]) ).
fof(f4884,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,pred(n6)) ),
inference(backward_demodulation,[status(thm)],[f4858,f4802]) ).
fof(f4904,plain,
! [X0,X1] :
( leq(X1,n5)
| ~ sP6_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4858,f503]) ).
fof(f4905,plain,
! [X0,X1] :
( leq(X0,n5)
| ~ sP6_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4858,f504]) ).
fof(f4908,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(n0,X1)
| ~ leq(X0,pred(n6))
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f4858,f473]) ).
fof(f4909,plain,
! [X0,X1] :
( leq(X1,n5)
| ~ sP5_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4858,f499]) ).
fof(f4916,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5) ),
inference(forward_demodulation,[status(thm)],[f4858,f4883]) ).
fof(f4917,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5) ),
inference(forward_demodulation,[status(thm)],[f4858,f4884]) ).
fof(f4918,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f4917,f4866]) ).
fof(f4929,plain,
! [X0,X1] :
( ~ sP6_prd(X0,X1)
| ~ leq(X0,n5) ),
inference(backward_subsumption_resolution,[status(thm)],[f4916,f4904]) ).
fof(f4932,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(n0,X1)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f4858,f4908]) ).
fof(f4934,plain,
! [X0,X1] : ~ sP5_prd(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f4909,f4918]) ).
fof(f4935,plain,
! [X0,X1] : ~ sP6_prd(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f4929,f4905]) ).
fof(f4946,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f419,f4934]) ).
fof(f4947,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f4946]) ).
fof(f4958,plain,
( ~ sQ7_spl
| leq(sK31_skl,n5) ),
inference(forward_demodulation,[status(thm)],[f4858,f1899]) ).
fof(f5039,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f422,f4935]) ).
fof(f5040,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f5039]) ).
fof(f5043,plain,
( ~ sQ9_spl
| leq(sK32_skl,n5) ),
inference(forward_demodulation,[status(thm)],[f4858,f1901]) ).
fof(f5376,definition,
( sQ175_spl
<=> leq(n0,n5) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f5378,plain,
( sQ175_spl
| ~ leq(n0,n5) ),
inference(component_clause,[status(thm)],[f5376]) ).
fof(f5379,definition,
( sQ176_spl
<=> leq(n5,n5) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f5381,plain,
( sQ176_spl
| ~ leq(n5,n5) ),
inference(component_clause,[status(thm)],[f5379]) ).
fof(f5384,plain,
( sQ176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5381,f109]) ).
fof(f5385,plain,
sQ176_spl,
inference(contradiction_clause,[status(thm)],[f5384]) ).
fof(f5386,plain,
( sQ175_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5378,f570]) ).
fof(f5387,plain,
sQ175_spl,
inference(contradiction_clause,[status(thm)],[f5386]) ).
fof(f5482,plain,
( sQ164_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4612,f575]) ).
fof(f5483,plain,
sQ164_spl,
inference(contradiction_clause,[status(thm)],[f5482]) ).
fof(f5538,definition,
( sQ183_spl
<=> leq(n1,n5) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f5540,plain,
( sQ183_spl
| ~ leq(n1,n5) ),
inference(component_clause,[status(thm)],[f5538]) ).
fof(f5543,plain,
( sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5540,f569]) ).
fof(f5544,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f5543]) ).
fof(f5572,definition,
( sQ185_spl
<=> leq(sK32_skl,n5) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f5574,plain,
( sQ185_spl
| ~ leq(sK32_skl,n5) ),
inference(component_clause,[status(thm)],[f5572]) ).
fof(f5577,plain,
( sQ10_spl
| ~ leq(sK32_skl,n5)
| ~ leq(n0,sK32_skl)
| ~ leq(sK31_skl,n5)
| ~ leq(n0,sK31_skl) ),
inference(resolution,[status(thm)],[f442,f4932]) ).
fof(f5579,definition,
( sQ186_spl
<=> leq(sK31_skl,n5) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f5581,plain,
( sQ186_spl
| ~ leq(sK31_skl,n5) ),
inference(component_clause,[status(thm)],[f5579]) ).
fof(f5582,plain,
( sQ10_spl
| ~ sQ185_spl
| ~ sQ8_spl
| ~ sQ186_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f5577,f424,f5579,f432,f5572,f440]) ).
fof(f5584,plain,
( sQ185_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5574,f5043]) ).
fof(f5585,plain,
( sQ185_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f5584]) ).
fof(f5586,plain,
( sQ186_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5581,f4958]) ).
fof(f5587,plain,
( sQ186_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f5586]) ).
fof(f5588,plain,
$false,
inference(sat_refutation,[status(thm)],[f427,f431,f435,f439,f443,f695,f697,f4793,f4807,f4947,f5040,f5385,f5387,f5483,f5544,f5582,f5585,f5587]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV109+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n020.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 08:32:33 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 53.18/7.28 % Refutation found
% 53.18/7.28 % SZS status Theorem for theBenchmark: Theorem is valid
% 53.18/7.28 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.59/7.34 % Elapsed time: 6.900653 seconds
% 1.59/7.34 % CPU time: 53.718060 seconds
% 1.59/7.34 % Total memory used: 269.293 MB
% 1.59/7.34 % Net memory used: 239.367 MB
%------------------------------------------------------------------------------