%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO440+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 12:25:03 PM UTC 2026
% Result : Theorem 10.97s 3.38s
% Output : CNFRefutation 6.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 103
% Syntax : Number of formulae : 398 ( 39 unt; 68 def)
% Number of atoms : 1175 ( 220 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1295 ( 518 ~; 521 |; 135 &)
% ( 95 <=>; 25 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 71 ( 69 usr; 69 prp; 0-2 aty)
% Number of functors : 45 ( 45 usr; 32 con; 0-3 aty)
% Number of variables : 440 ( 415 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
( p(s(bool,f0))
<=> ! [P0] : p(s(bool,P0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] :
( ~ p(s(bool,X))
<=> ( p(s(bool,X))
=> p(s(bool,f0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
p(s(bool,t)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
s(bool,u_falsityu_) = s(bool,f0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,X] :
( s(A,X) = s(A,X)
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,X,Y,Z0] :
( ( s(A,Y) = s(A,Z0)
& s(A,X) = s(A,Y) )
=> s(A,X) = s(A,Z0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
( s(bool,a0) = s(bool,b0)
=> ( p(s(bool,a0))
=> p(s(bool,b0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [T0] :
( ( s(bool,T0) = s(bool,f0)
<=> ~ p(s(bool,T0)) )
& ( s(bool,f0) = s(bool,T0)
<=> ~ p(s(bool,T0)) )
& ( s(bool,T0) = s(bool,t)
<=> p(s(bool,T0)) )
& ( s(bool,t) = s(bool,T0)
<=> p(s(bool,T0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
~ p(s(bool,f0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
( ~ p(s(bool,f0))
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A,P0,Q0] :
( ( p(s(bool,Q0))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ! [X] :
( p(s(bool,Q0))
& p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) )
<=> ! [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A,P0,Q0] :
( ( p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ? [X] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
( s(bool,a0) = s(bool,b0)
<=> ( ( p(s(bool,b0))
=> p(s(bool,a0)) )
& ( p(s(bool,a0))
=> p(s(bool,b0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
( ( ( p(s(bool,c0))
=> p(s(bool,d0)) )
& ( p(s(bool,a))
=> p(s(bool,b)) ) )
=> ( ( p(s(bool,c0))
& p(s(bool,a)) )
=> ( p(s(bool,d0))
& p(s(bool,b)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
( ( ( p(s(bool,c0))
=> p(s(bool,d0)) )
& ( p(s(bool,a))
=> p(s(bool,b)) ) )
=> ( ( p(s(bool,c0))
| p(s(bool,a)) )
=> ( p(s(bool,d0))
| p(s(bool,b)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
( ( ( p(s(bool,c0))
=> p(s(bool,d0)) )
& ( p(s(bool,b))
=> p(s(bool,a)) ) )
=> ( ( p(s(bool,a))
=> p(s(bool,c0)) )
=> ( p(s(bool,b))
=> p(s(bool,d0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
( ( ( p(s(bool,c0))
=> p(s(bool,d0)) )
& ( p(s(bool,a))
=> p(s(bool,b)) ) )
=> ( p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,a))),s(bool,c0))))
=> p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,b))),s(bool,d0)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,axiom,
? [B0] : p(s(bool,B0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [V] : s(n10,V) = s(n10,one),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,axiom,
( s(num,u_0) = s(num,u_0)
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,axiom,
! [N0] : s(num,i(s(fun(num,num),numeral),s(num,N0))) = s(num,N0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f568,axiom,
! [N0] :
( s(num,i(s(fun(num,num),bit1),s(num,N0))) = s(num,u_0)
<=> p(s(bool,f0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f572,axiom,
! [M0,N0] :
( s(num,i(s(fun(num,num),bit0),s(num,M0))) = s(num,i(s(fun(num,num),bit1),s(num,N0)))
<=> p(s(bool,f0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f982,axiom,
! [Y,X] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y))))
<=> ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,Y))),s(real,X)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1028,axiom,
! [X,Y] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y))))
<=> ( s(real,X) = s(real,Y)
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1032,axiom,
! [X,Y] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y))))
<=> ( s(real,X) != s(real,Y)
& p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1033,axiom,
! [X] : ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,X)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2041,axiom,
! [Q58981,P0] :
( ! [X] :
( p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty))))
=> p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X)))) )
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2043,axiom,
! [Q59041,P0] :
( ? [X] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) )
<=> p(s(bool,f0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2377,axiom,
! [B,A,R0] :
( p(s(bool,t))
<=> s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) = s(fun(finite_image(B),A),R0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2845,axiom,
! [Q102146] : s(real,i(s(fun(cart(real,Q102146),real),vectoru_norm),s(cart(real,Q102146),i(s(fun(num,cart(real,Q102146)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2846,axiom,
! [Q102162,X] : p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,Q102162),real),vectoru_norm),s(cart(real,Q102162),X)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2851,axiom,
! [Q102285,X] :
( s(real,i(s(fun(cart(real,Q102285),real),vectoru_norm),s(cart(real,Q102285),X))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
<=> s(cart(real,Q102285),X) = s(cart(real,Q102285),i(s(fun(num,cart(real,Q102285)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2852,conjecture,
! [Q102307,X] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,Q102307),real),vectoru_norm),s(cart(real,Q102307),X))))))
<=> s(cart(real,Q102307),X) != s(cart(real,Q102307),i(s(fun(num,cart(real,Q102307)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2853,negated_conjecture,
~ ! [Q102307,X] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,Q102307),real),vectoru_norm),s(cart(real,Q102307),X))))))
<=> s(cart(real,Q102307),X) != s(cart(real,Q102307),i(s(fun(num,cart(real,Q102307)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
inference(negated_conjecture,[status(cth)],[f2852]) ).
fof(f2893,plain,
( ( ? [P0] : ~ p(s(bool,P0))
| p(s(bool,f0)) )
& ( ! [P0] : p(s(bool,P0))
| ~ p(s(bool,f0)) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f2894,plain,
( ( ~ p(s(bool,sK5_skl))
| p(s(bool,f0)) )
& ( ! [P0] : p(s(bool,P0))
| ~ p(s(bool,f0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(P0,sK5_skl)],[f2893]) ).
fof(f2896,plain,
( ~ p(s(bool,sK5_skl))
| p(s(bool,f0)) ),
inference(cnf_transformation,[status(thm)],[f2894]) ).
fof(f2897,plain,
! [X] :
( ~ p(s(bool,X))
<=> ( p(s(bool,f0))
| ~ p(s(bool,X)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f2898,plain,
! [X] :
( ( ( ~ p(s(bool,f0))
& p(s(bool,X)) )
| ~ p(s(bool,X)) )
& ( p(s(bool,f0))
| ~ p(s(bool,X))
| p(s(bool,X)) ) ),
inference(NNF_transformation,[status(thm)],[f2897]) ).
fof(f2899,plain,
( ! [X] :
( ( ~ p(s(bool,f0))
& p(s(bool,X)) )
| ~ p(s(bool,X)) )
& ! [X] :
( p(s(bool,f0))
| ~ p(s(bool,X))
| p(s(bool,X)) ) ),
inference(miniscoping,[status(thm)],[f2898]) ).
fof(f2900,plain,
! [X0] :
( p(s(bool,f0))
| ~ p(s(bool,X0))
| p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f2899]) ).
fof(f2903,plain,
p(s(bool,t)),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f2904,plain,
s(bool,u_falsityu_) = s(bool,f0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f2914,plain,
! [A,X] :
( ( ~ p(s(bool,t))
| s(A,X) = s(A,X) )
& ( p(s(bool,t))
| s(A,X) != s(A,X) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f2915,plain,
( ( ~ p(s(bool,t))
| ! [A,X] : s(A,X) = s(A,X) )
& ( p(s(bool,t))
| ! [A,X] : s(A,X) != s(A,X) ) ),
inference(miniscoping,[status(thm)],[f2914]) ).
fof(f2916,plain,
! [X0,X1] :
( p(s(bool,t))
| s(X0,X1) != s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2915]) ).
fof(f2917,plain,
! [X0,X1] :
( ~ p(s(bool,t))
| s(X0,X1) = s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2915]) ).
fof(f2924,plain,
! [A,X,Y,Z0] :
( s(A,X) = s(A,Z0)
| s(A,Y) != s(A,Z0)
| s(A,X) != s(A,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f2925,plain,
! [A,X,Z0] :
( s(A,X) = s(A,Z0)
| ! [Y] :
( s(A,Y) != s(A,Z0)
| s(A,X) != s(A,Y) ) ),
inference(miniscoping,[status(thm)],[f2924]) ).
fof(f2926,plain,
! [X0,X1,X2,X3] :
( s(X0,X1) = s(X0,X3)
| s(X0,X2) != s(X0,X3)
| s(X0,X1) != s(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f2925]) ).
fof(f3060,plain,
( p(s(bool,b0))
| ~ p(s(bool,a0))
| s(bool,a0) != s(bool,b0) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f3061,plain,
( p(s(bool,b0))
| ~ p(s(bool,a0))
| s(bool,a0) != s(bool,b0) ),
inference(cnf_transformation,[status(thm)],[f3060]) ).
fof(f3062,plain,
! [T0] :
( ( p(s(bool,T0))
| s(bool,T0) = s(bool,f0) )
& ( ~ p(s(bool,T0))
| s(bool,T0) != s(bool,f0) )
& ( p(s(bool,T0))
| s(bool,f0) = s(bool,T0) )
& ( ~ p(s(bool,T0))
| s(bool,f0) != s(bool,T0) )
& ( ~ p(s(bool,T0))
| s(bool,T0) = s(bool,t) )
& ( p(s(bool,T0))
| s(bool,T0) != s(bool,t) )
& ( ~ p(s(bool,T0))
| s(bool,t) = s(bool,T0) )
& ( p(s(bool,T0))
| s(bool,t) != s(bool,T0) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f3063,plain,
( ! [T0] :
( p(s(bool,T0))
| s(bool,T0) = s(bool,f0) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,T0) != s(bool,f0) )
& ! [T0] :
( p(s(bool,T0))
| s(bool,f0) = s(bool,T0) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,f0) != s(bool,T0) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,T0) = s(bool,t) )
& ! [T0] :
( p(s(bool,T0))
| s(bool,T0) != s(bool,t) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,t) = s(bool,T0) )
& ! [T0] :
( p(s(bool,T0))
| s(bool,t) != s(bool,T0) ) ),
inference(miniscoping,[status(thm)],[f3062]) ).
fof(f3064,plain,
! [X0] :
( p(s(bool,X0))
| s(bool,t) != s(bool,X0) ),
inference(cnf_transformation,[status(thm)],[f3063]) ).
fof(f3065,plain,
! [X0] :
( ~ p(s(bool,X0))
| s(bool,t) = s(bool,X0) ),
inference(cnf_transformation,[status(thm)],[f3063]) ).
fof(f3069,plain,
! [X0] :
( p(s(bool,X0))
| s(bool,f0) = s(bool,X0) ),
inference(cnf_transformation,[status(thm)],[f3063]) ).
fof(f3072,plain,
~ p(s(bool,f0)),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f3073,plain,
( ( ~ p(s(bool,t))
| ~ p(s(bool,f0)) )
& ( p(s(bool,t))
| p(s(bool,f0)) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f3075,plain,
( ~ p(s(bool,t))
| ~ p(s(bool,f0)) ),
inference(cnf_transformation,[status(thm)],[f3073]) ).
fof(f3199,plain,
! [A,P0,Q0] :
( ( ? [X] :
( ~ p(s(bool,Q0))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ( p(s(bool,Q0))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ( ! [X] :
( p(s(bool,Q0))
& p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ~ p(s(bool,Q0))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
inference(NNF_transformation,[status(thm)],[f60]) ).
fof(f3200,plain,
( ! [A,P0,Q0] :
( ~ p(s(bool,Q0))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( p(s(bool,Q0))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ! [A,P0,Q0] :
( ( p(s(bool,Q0))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ~ p(s(bool,Q0))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
inference(miniscoping,[status(thm)],[f3199]) ).
fof(f3201,plain,
( ! [A,P0,Q0] :
( ~ p(s(bool,Q0))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK35_skl(Q0,P0,A)))))
| ( p(s(bool,Q0))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ! [A,P0,Q0] :
( ( p(s(bool,Q0))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ~ p(s(bool,Q0))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK34_skl(Q0,P0,A))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl,sK35_skl]),skolemize(X,sK34_skl(Q0,P0,A)),skolemize(X,sK35_skl(Q0,P0,A))],[f3200]) ).
fof(f3202,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X3))))
| ~ p(s(bool,X2))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK34_skl(X2,X1,X0))))) ),
inference(cnf_transformation,[status(thm)],[f3201]) ).
fof(f3204,plain,
! [X0,X1,X2,X3] :
( ~ p(s(bool,X3))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK35_skl(X3,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(cnf_transformation,[status(thm)],[f3201]) ).
fof(f3206,plain,
! [A,P0,Q0] :
( ( ? [X] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0)) )
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) ) )
& ( ! [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) )
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0)) ) ),
inference(NNF_transformation,[status(thm)],[f61]) ).
fof(f3207,plain,
( ! [A,P0,Q0] :
( ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0))
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) ) )
& ! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) )
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0)) ) ),
inference(miniscoping,[status(thm)],[f3206]) ).
fof(f3208,plain,
( ! [A,P0,Q0] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,sK37_skl(Q0,P0,A)))))
| ~ p(s(bool,P0))
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) ) )
& ! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) )
| ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,sK36_skl(Q0,P0,A)))))
| ~ p(s(bool,P0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl]),skolemize(X,sK36_skl(Q0,P0,A)),skolemize(X,sK37_skl(Q0,P0,A))],[f3207]) ).
fof(f3210,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X1,bool),X2),s(X1,X3))))
| ~ p(s(bool,i(s(fun(X1,bool),X2),s(X1,sK36_skl(X2,X0,X1)))))
| ~ p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3208]) ).
fof(f3212,plain,
! [X0,X1,X2,X3] :
( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK37_skl(X1,X3,X0)))))
| ~ p(s(bool,X3))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(cnf_transformation,[status(thm)],[f3208]) ).
fof(f3227,plain,
! [A,P0,Q0] :
( ( ! [X] :
( ~ p(s(bool,Q0))
& ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ( ? [X] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f64]) ).
fof(f3228,plain,
( ! [A,P0,Q0] :
( ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ! [A,P0,Q0] :
( p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(miniscoping,[status(thm)],[f3227]) ).
fof(f3229,plain,
( ! [A,P0,Q0] :
( ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK47_skl(Q0,P0,A))))) )
& ! [A,P0,Q0] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK46_skl(Q0,P0,A)))))
| ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46_skl,sK47_skl]),skolemize(X,sK46_skl(Q0,P0,A)),skolemize(X,sK47_skl(Q0,P0,A))],[f3228]) ).
fof(f3230,plain,
! [X0,X1,X2,X3] :
( p(s(bool,X3))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK46_skl(X3,X1,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(cnf_transformation,[status(thm)],[f3229]) ).
fof(f3349,plain,
( s(bool,a0) = s(bool,b0)
<=> ( ( p(s(bool,a0))
| ~ p(s(bool,b0)) )
& ( p(s(bool,b0))
| ~ p(s(bool,a0)) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f3350,plain,
( ( ( ~ p(s(bool,a0))
& p(s(bool,b0)) )
| ( ~ p(s(bool,b0))
& p(s(bool,a0)) )
| s(bool,a0) = s(bool,b0) )
& ( ( ( p(s(bool,a0))
| ~ p(s(bool,b0)) )
& ( p(s(bool,b0))
| ~ p(s(bool,a0)) ) )
| s(bool,a0) != s(bool,b0) ) ),
inference(NNF_transformation,[status(thm)],[f3349]) ).
fof(f3352,plain,
( p(s(bool,a0))
| ~ p(s(bool,b0))
| s(bool,a0) != s(bool,b0) ),
inference(cnf_transformation,[status(thm)],[f3350]) ).
fof(f3353,plain,
( p(s(bool,b0))
| p(s(bool,a0))
| s(bool,a0) = s(bool,b0) ),
inference(cnf_transformation,[status(thm)],[f3350]) ).
fof(f3356,plain,
( ~ p(s(bool,a0))
| ~ p(s(bool,b0))
| s(bool,a0) = s(bool,b0) ),
inference(cnf_transformation,[status(thm)],[f3350]) ).
fof(f3369,plain,
( ( p(s(bool,d0))
& p(s(bool,b)) )
| ~ p(s(bool,c0))
| ~ p(s(bool,a))
| ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,b))
& p(s(bool,a)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f3370,definition,
( sP8_prd
<=> ( ~ p(s(bool,b))
& p(s(bool,a)) ) ),
introduced(definition,[new_symbols(definition,[sP8_prd])],[]) ).
fof(f3376,plain,
( p(s(bool,d0))
| p(s(bool,b))
| ( ~ p(s(bool,c0))
& ~ p(s(bool,a)) )
| ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,b))
& p(s(bool,a)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f3377,definition,
( sP9_prd
<=> ( ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,b))
& p(s(bool,a)) ) ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f3381,plain,
( p(s(bool,d0))
| ~ p(s(bool,b))
| ( ~ p(s(bool,c0))
& p(s(bool,a)) )
| ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,a))
& p(s(bool,b)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f3382,definition,
( sP10_prd
<=> ( ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,a))
& p(s(bool,b)) ) ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f3569,plain,
( p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,b))),s(bool,d0))))
| ~ p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,a))),s(bool,c0))))
| ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,b))
& p(s(bool,a)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f123]) ).
fof(f3570,definition,
( sP11_prd
<=> ( ~ p(s(bool,b))
& p(s(bool,a)) ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f3571,plain,
( p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,b))),s(bool,d0))))
| ~ p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,a))),s(bool,c0))))
| ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| sP11_prd ),
inference(formula_renaming,[status(thm)],[f3569,f3570]) ).
fof(f3572,plain,
( p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,b))),s(bool,d0))))
| ~ p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,a))),s(bool,c0))))
| p(s(bool,c0))
| sP11_prd ),
inference(cnf_transformation,[status(thm)],[f3571]) ).
fof(f3573,plain,
( p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,b))),s(bool,d0))))
| ~ p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,a))),s(bool,c0))))
| ~ p(s(bool,d0))
| sP11_prd ),
inference(cnf_transformation,[status(thm)],[f3571]) ).
fof(f3624,plain,
p(s(bool,sK134_skl)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK134_skl]),skolemize(B0,sK134_skl)],[f136]) ).
fof(f3625,plain,
p(s(bool,sK134_skl)),
inference(cnf_transformation,[status(thm)],[f3624]) ).
fof(f3634,plain,
! [X0] : s(n10,X0) = s(n10,one),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f3867,plain,
( ( ~ p(s(bool,t))
| s(num,u_0) = s(num,u_0) )
& ( p(s(bool,t))
| s(num,u_0) != s(num,u_0) ) ),
inference(NNF_transformation,[status(thm)],[f199]) ).
fof(f3869,plain,
( ~ p(s(bool,t))
| s(num,u_0) = s(num,u_0) ),
inference(cnf_transformation,[status(thm)],[f3867]) ).
fof(f3870,plain,
! [X0] : s(num,i(s(fun(num,num),numeral),s(num,X0))) = s(num,X0),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f4862,plain,
! [N0] :
( ( ~ p(s(bool,f0))
| s(num,i(s(fun(num,num),bit1),s(num,N0))) = s(num,u_0) )
& ( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit1),s(num,N0))) != s(num,u_0) ) ),
inference(NNF_transformation,[status(thm)],[f568]) ).
fof(f4863,plain,
( ( ~ p(s(bool,f0))
| ! [N0] : s(num,i(s(fun(num,num),bit1),s(num,N0))) = s(num,u_0) )
& ( p(s(bool,f0))
| ! [N0] : s(num,i(s(fun(num,num),bit1),s(num,N0))) != s(num,u_0) ) ),
inference(miniscoping,[status(thm)],[f4862]) ).
fof(f4864,plain,
! [X0] :
( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit1),s(num,X0))) != s(num,u_0) ),
inference(cnf_transformation,[status(thm)],[f4863]) ).
fof(f4878,plain,
! [M0,N0] :
( ( ~ p(s(bool,f0))
| s(num,i(s(fun(num,num),bit0),s(num,M0))) = s(num,i(s(fun(num,num),bit1),s(num,N0))) )
& ( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit0),s(num,M0))) != s(num,i(s(fun(num,num),bit1),s(num,N0))) ) ),
inference(NNF_transformation,[status(thm)],[f572]) ).
fof(f4879,plain,
( ( ~ p(s(bool,f0))
| ! [M0,N0] : s(num,i(s(fun(num,num),bit0),s(num,M0))) = s(num,i(s(fun(num,num),bit1),s(num,N0))) )
& ( p(s(bool,f0))
| ! [M0,N0] : s(num,i(s(fun(num,num),bit0),s(num,M0))) != s(num,i(s(fun(num,num),bit1),s(num,N0))) ) ),
inference(miniscoping,[status(thm)],[f4878]) ).
fof(f4880,plain,
! [X0,X1] :
( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit0),s(num,X0))) != s(num,i(s(fun(num,num),bit1),s(num,X1))) ),
inference(cnf_transformation,[status(thm)],[f4879]) ).
fof(f5943,plain,
! [Y,X] :
( ( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,Y))),s(real,X))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) )
& ( ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,Y))),s(real,X))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) ) ),
inference(NNF_transformation,[status(thm)],[f982]) ).
fof(f5944,plain,
( ! [Y,X] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,Y))),s(real,X))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) )
& ! [Y,X] :
( ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,Y))),s(real,X))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) ) ),
inference(miniscoping,[status(thm)],[f5943]) ).
fof(f5946,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X1))),s(real,X0))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X1)))) ),
inference(cnf_transformation,[status(thm)],[f5944]) ).
fof(f6030,plain,
! [X,Y] :
( ( ( s(real,X) != s(real,Y)
& ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) )
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y)))) )
& ( s(real,X) = s(real,Y)
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y)))) ) ),
inference(NNF_transformation,[status(thm)],[f1028]) ).
fof(f6031,plain,
( ! [X,Y] :
( ( s(real,X) != s(real,Y)
& ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) )
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y)))) )
& ! [X,Y] :
( s(real,X) = s(real,Y)
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y)))) ) ),
inference(miniscoping,[status(thm)],[f6030]) ).
fof(f6032,plain,
! [X0,X1] :
( s(real,X0) = s(real,X1)
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X1))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X0))),s(real,X1)))) ),
inference(cnf_transformation,[status(thm)],[f6031]) ).
fof(f6044,plain,
! [X,Y] :
( ( s(real,X) = s(real,Y)
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) )
& ( ( s(real,X) != s(real,Y)
& p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y)))) )
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) ) ),
inference(NNF_transformation,[status(thm)],[f1032]) ).
fof(f6045,plain,
( ! [X,Y] :
( s(real,X) = s(real,Y)
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) )
& ! [X,Y] :
( ( s(real,X) != s(real,Y)
& p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X))),s(real,Y)))) )
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X))),s(real,Y)))) ) ),
inference(miniscoping,[status(thm)],[f6044]) ).
fof(f6047,plain,
! [X0,X1] :
( s(real,X0) != s(real,X1)
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X1)))) ),
inference(cnf_transformation,[status(thm)],[f6045]) ).
fof(f6049,plain,
! [X0] : ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X0)))),
inference(cnf_transformation,[status(thm)],[f1033]) ).
fof(f9178,plain,
! [Q58981,P0] :
( ! [X] :
( p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) )
<=> p(s(bool,t)) ),
inference(pre_NNF_transformation,[status(thm)],[f2041]) ).
fof(f9179,plain,
! [Q58981,P0] :
( ( ~ p(s(bool,t))
| ! [X] :
( p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) )
& ( p(s(bool,t))
| ? [X] :
( ~ p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
& p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f9178]) ).
fof(f9180,plain,
( ( ~ p(s(bool,t))
| ! [Q58981,X] :
( ! [P0] : p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) )
& ( p(s(bool,t))
| ! [Q58981,P0] :
? [X] :
( ~ p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
& p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) ) ),
inference(miniscoping,[status(thm)],[f9179]) ).
fof(f9181,plain,
( ( ~ p(s(bool,t))
| ! [Q58981,X] :
( ! [P0] : p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) )
& ( p(s(bool,t))
| ! [Q58981,P0] :
( ~ p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,sK1408_skl(P0,Q58981)))))
& p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,sK1408_skl(P0,Q58981)))),s(fun(Q58981,bool),empty)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1408_skl]),skolemize(X,sK1408_skl(P0,Q58981))],[f9180]) ).
fof(f9184,plain,
! [X0,X1,X2] :
( ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ),
inference(cnf_transformation,[status(thm)],[f9181]) ).
fof(f9194,plain,
! [Q59041,P0] :
( ( ~ p(s(bool,f0))
| ? [X] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) )
& ( p(s(bool,f0))
| ! [X] :
( ~ p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
| ~ p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f2043]) ).
fof(f9195,plain,
( ( ~ p(s(bool,f0))
| ! [Q59041,P0] :
? [X] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) )
& ( p(s(bool,f0))
| ! [Q59041,X] :
( ! [P0] : ~ p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
| ~ p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) ) ),
inference(miniscoping,[status(thm)],[f9194]) ).
fof(f9196,plain,
( ( ~ p(s(bool,f0))
| ! [Q59041,P0] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,sK1410_skl(P0,Q59041)))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,sK1410_skl(P0,Q59041)))),s(fun(Q59041,bool),empty)))) ) )
& ( p(s(bool,f0))
| ! [Q59041,X] :
( ! [P0] : ~ p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
| ~ p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1410_skl]),skolemize(X,sK1410_skl(P0,Q59041))],[f9195]) ).
fof(f9197,plain,
! [X0,X1,X2] :
( p(s(bool,f0))
| ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ),
inference(cnf_transformation,[status(thm)],[f9196]) ).
fof(f10828,plain,
! [B,A,R0] :
( ( s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) != s(fun(finite_image(B),A),R0)
| p(s(bool,t)) )
& ( s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) = s(fun(finite_image(B),A),R0)
| ~ p(s(bool,t)) ) ),
inference(NNF_transformation,[status(thm)],[f2377]) ).
fof(f10829,plain,
( ( ! [B,A,R0] : s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) != s(fun(finite_image(B),A),R0)
| p(s(bool,t)) )
& ( ! [B,A,R0] : s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) = s(fun(finite_image(B),A),R0)
| ~ p(s(bool,t)) ) ),
inference(miniscoping,[status(thm)],[f10828]) ).
fof(f10830,plain,
! [X0,X1,X2] :
( s(fun(finite_image(X0),X1),i(s(fun(cart(X1,X0),fun(finite_image(X0),X1)),destu_cart),s(cart(X1,X0),i(s(fun(fun(finite_image(X0),X1),cart(X1,X0)),mku_cart),s(fun(finite_image(X0),X1),X2))))) = s(fun(finite_image(X0),X1),X2)
| ~ p(s(bool,t)) ),
inference(cnf_transformation,[status(thm)],[f10829]) ).
fof(f12650,plain,
! [X0] : s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))),
inference(cnf_transformation,[status(thm)],[f2845]) ).
fof(f12651,plain,
! [X0,X1] : p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1)))))),
inference(cnf_transformation,[status(thm)],[f2846]) ).
fof(f12659,plain,
! [Q102285,X] :
( ( s(cart(real,Q102285),X) != s(cart(real,Q102285),i(s(fun(num,cart(real,Q102285)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,Q102285),real),vectoru_norm),s(cart(real,Q102285),X))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) )
& ( s(cart(real,Q102285),X) = s(cart(real,Q102285),i(s(fun(num,cart(real,Q102285)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,Q102285),real),vectoru_norm),s(cart(real,Q102285),X))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ) ),
inference(NNF_transformation,[status(thm)],[f2851]) ).
fof(f12660,plain,
( ! [Q102285,X] :
( s(cart(real,Q102285),X) != s(cart(real,Q102285),i(s(fun(num,cart(real,Q102285)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,Q102285),real),vectoru_norm),s(cart(real,Q102285),X))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) )
& ! [Q102285,X] :
( s(cart(real,Q102285),X) = s(cart(real,Q102285),i(s(fun(num,cart(real,Q102285)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,Q102285),real),vectoru_norm),s(cart(real,Q102285),X))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ) ),
inference(miniscoping,[status(thm)],[f12659]) ).
fof(f12661,plain,
! [X0,X1] :
( s(cart(real,X0),X1) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
inference(cnf_transformation,[status(thm)],[f12660]) ).
fof(f12662,plain,
! [X0,X1] :
( s(cart(real,X0),X1) != s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
inference(cnf_transformation,[status(thm)],[f12660]) ).
fof(f12663,plain,
? [Q102307,X] :
( p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,Q102307),real),vectoru_norm),s(cart(real,Q102307),X))))))
<~> s(cart(real,Q102307),X) != s(cart(real,Q102307),i(s(fun(num,cart(real,Q102307)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
inference(pre_NNF_transformation,[status(thm)],[f2853]) ).
fof(f12664,plain,
? [Q102307,X] :
( ( s(cart(real,Q102307),X) = s(cart(real,Q102307),i(s(fun(num,cart(real,Q102307)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,Q102307),real),vectoru_norm),s(cart(real,Q102307),X)))))) )
& ( s(cart(real,Q102307),X) != s(cart(real,Q102307),i(s(fun(num,cart(real,Q102307)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,Q102307),real),vectoru_norm),s(cart(real,Q102307),X)))))) ) ),
inference(NNF_transformation,[status(thm)],[f12663]) ).
fof(f12665,plain,
( ( s(cart(real,sK2954_skl),sK2955_skl) = s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) )
& ( s(cart(real,sK2954_skl),sK2955_skl) != s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2954_skl,sK2955_skl]),skolemize(Q102307,sK2954_skl),skolemize(X,sK2955_skl)],[f12664]) ).
fof(f12666,plain,
( s(cart(real,sK2954_skl),sK2955_skl) != s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(cnf_transformation,[status(thm)],[f12665]) ).
fof(f12667,plain,
( s(cart(real,sK2954_skl),sK2955_skl) = s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(cnf_transformation,[status(thm)],[f12665]) ).
fof(f12723,plain,
( ( p(s(bool,b))
| ~ p(s(bool,a))
| sP8_prd )
& ( ( ~ p(s(bool,b))
& p(s(bool,a)) )
| ~ sP8_prd ) ),
inference(NNF_transformation,[status(thm)],[f3370]) ).
fof(f12724,plain,
( p(s(bool,a))
| ~ sP8_prd ),
inference(cnf_transformation,[status(thm)],[f12723]) ).
fof(f12725,plain,
( ~ p(s(bool,b))
| ~ sP8_prd ),
inference(cnf_transformation,[status(thm)],[f12723]) ).
fof(f12726,plain,
( p(s(bool,b))
| ~ p(s(bool,a))
| sP8_prd ),
inference(cnf_transformation,[status(thm)],[f12723]) ).
fof(f12727,plain,
( ( ( ( p(s(bool,d0))
| ~ p(s(bool,c0)) )
& ( p(s(bool,b))
| ~ p(s(bool,a)) ) )
| sP9_prd )
& ( ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,b))
& p(s(bool,a)) )
| ~ sP9_prd ) ),
inference(NNF_transformation,[status(thm)],[f3377]) ).
fof(f12728,plain,
( p(s(bool,c0))
| p(s(bool,a))
| ~ sP9_prd ),
inference(cnf_transformation,[status(thm)],[f12727]) ).
fof(f12729,plain,
( ~ p(s(bool,d0))
| p(s(bool,a))
| ~ sP9_prd ),
inference(cnf_transformation,[status(thm)],[f12727]) ).
fof(f12730,plain,
( p(s(bool,c0))
| ~ p(s(bool,b))
| ~ sP9_prd ),
inference(cnf_transformation,[status(thm)],[f12727]) ).
fof(f12731,plain,
( ~ p(s(bool,d0))
| ~ p(s(bool,b))
| ~ sP9_prd ),
inference(cnf_transformation,[status(thm)],[f12727]) ).
fof(f12732,plain,
( p(s(bool,b))
| ~ p(s(bool,a))
| sP9_prd ),
inference(cnf_transformation,[status(thm)],[f12727]) ).
fof(f12733,plain,
( p(s(bool,d0))
| ~ p(s(bool,c0))
| sP9_prd ),
inference(cnf_transformation,[status(thm)],[f12727]) ).
fof(f12734,plain,
( ( ( ( p(s(bool,d0))
| ~ p(s(bool,c0)) )
& ( p(s(bool,a))
| ~ p(s(bool,b)) ) )
| sP10_prd )
& ( ( ~ p(s(bool,d0))
& p(s(bool,c0)) )
| ( ~ p(s(bool,a))
& p(s(bool,b)) )
| ~ sP10_prd ) ),
inference(NNF_transformation,[status(thm)],[f3382]) ).
fof(f12735,plain,
( p(s(bool,c0))
| p(s(bool,b))
| ~ sP10_prd ),
inference(cnf_transformation,[status(thm)],[f12734]) ).
fof(f12736,plain,
( ~ p(s(bool,d0))
| p(s(bool,b))
| ~ sP10_prd ),
inference(cnf_transformation,[status(thm)],[f12734]) ).
fof(f12737,plain,
( p(s(bool,c0))
| ~ p(s(bool,a))
| ~ sP10_prd ),
inference(cnf_transformation,[status(thm)],[f12734]) ).
fof(f12738,plain,
( ~ p(s(bool,d0))
| ~ p(s(bool,a))
| ~ sP10_prd ),
inference(cnf_transformation,[status(thm)],[f12734]) ).
fof(f12739,plain,
( p(s(bool,a))
| ~ p(s(bool,b))
| sP10_prd ),
inference(cnf_transformation,[status(thm)],[f12734]) ).
fof(f12740,plain,
( p(s(bool,d0))
| ~ p(s(bool,c0))
| sP10_prd ),
inference(cnf_transformation,[status(thm)],[f12734]) ).
fof(f12741,plain,
( ( p(s(bool,b))
| ~ p(s(bool,a))
| sP11_prd )
& ( ( ~ p(s(bool,b))
& p(s(bool,a)) )
| ~ sP11_prd ) ),
inference(NNF_transformation,[status(thm)],[f3570]) ).
fof(f12742,plain,
( p(s(bool,a))
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f12741]) ).
fof(f12743,plain,
( ~ p(s(bool,b))
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f12741]) ).
fof(f12744,plain,
( p(s(bool,b))
| ~ p(s(bool,a))
| sP11_prd ),
inference(cnf_transformation,[status(thm)],[f12741]) ).
fof(f15139,definition,
! [X2] :
( sQ1_spl
<=> ( p(s(bool,X2))
| ~ p(s(bool,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f15143,definition,
( sQ2_spl
<=> p(s(bool,f0)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f15146,definition,
! [X0] :
( sQ3_spl
<=> p(s(bool,X0)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f15147,plain,
! [X0] :
( ~ sQ3_spl
| p(s(bool,X0)) ),
inference(component_clause,[status(thm)],[f15146]) ).
fof(f15150,definition,
( sQ4_spl
<=> p(s(bool,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f15152,plain,
( sQ4_spl
| ~ p(s(bool,sK5_skl)) ),
inference(component_clause,[status(thm)],[f15150]) ).
fof(f15153,plain,
( ~ sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2896,f15143,f15150]) ).
fof(f15154,plain,
( sQ2_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f2900,f15139,f15143]) ).
fof(f15155,definition,
! [X0] :
( sQ5_spl
<=> ~ p(s(bool,X0)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f15156,plain,
! [X0] :
( ~ sQ5_spl
| ~ p(s(bool,X0)) ),
inference(component_clause,[status(thm)],[f15155]) ).
fof(f15174,definition,
! [X0,X1] :
( sQ9_spl
<=> s(X0,X1) != s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f15175,plain,
! [X0,X1] :
( ~ sQ9_spl
| s(X0,X1) != s(X0,X1) ),
inference(component_clause,[status(thm)],[f15174]) ).
fof(f15177,definition,
( sQ10_spl
<=> p(s(bool,t)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f15180,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f2916,f15174,f15177]) ).
fof(f15181,definition,
! [X0,X1] :
( sQ11_spl
<=> s(X0,X1) = s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f15184,plain,
( ~ sQ10_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2917,f15181,f15177]) ).
fof(f15265,definition,
( sQ12_spl
<=> s(bool,a0) = s(bool,b0) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f15267,plain,
( sQ12_spl
| s(bool,a0) != s(bool,b0) ),
inference(component_clause,[status(thm)],[f15265]) ).
fof(f15268,definition,
( sQ13_spl
<=> p(s(bool,a0)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f15269,plain,
( ~ sQ13_spl
| p(s(bool,a0)) ),
inference(component_clause,[status(thm)],[f15268]) ).
fof(f15271,definition,
( sQ14_spl
<=> p(s(bool,b0)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f15274,plain,
( sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f3061,f15265,f15268,f15271]) ).
fof(f15276,plain,
( ~ sQ10_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f3075,f15143,f15177]) ).
fof(f15359,plain,
( sQ13_spl
| ~ sQ14_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f3352,f15265,f15271,f15268]) ).
fof(f15360,plain,
( sQ14_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f3353,f15265,f15268,f15271]) ).
fof(f15363,plain,
( ~ sQ13_spl
| ~ sQ14_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f3356,f15265,f15271,f15268]) ).
fof(f15364,definition,
( sQ17_spl
<=> sP8_prd ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f15367,definition,
( sQ18_spl
<=> p(s(bool,c0)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f15369,plain,
( sQ18_spl
| ~ p(s(bool,c0)) ),
inference(component_clause,[status(thm)],[f15367]) ).
fof(f15370,definition,
( sQ19_spl
<=> p(s(bool,a)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f15372,plain,
( sQ19_spl
| ~ p(s(bool,a)) ),
inference(component_clause,[status(thm)],[f15370]) ).
fof(f15373,definition,
( sQ20_spl
<=> p(s(bool,b)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f15374,plain,
( ~ sQ20_spl
| p(s(bool,b)) ),
inference(component_clause,[status(thm)],[f15373]) ).
fof(f15377,definition,
( sQ21_spl
<=> p(s(bool,d0)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f15383,definition,
( sQ22_spl
<=> sP9_prd ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f15388,definition,
( sQ23_spl
<=> sP10_prd ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f15443,definition,
( sQ30_spl
<=> sP11_prd ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f15446,definition,
( sQ31_spl
<=> p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,a))),s(bool,c0)))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f15449,definition,
( sQ32_spl
<=> p(s(bool,i(s(fun(bool,bool),i(s(fun(bool,fun(bool,bool)),i(s(fun(bool,fun(bool,fun(bool,bool))),cond),s(bool,b0))),s(bool,b))),s(bool,d0)))) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f15452,plain,
( sQ32_spl
| ~ sQ31_spl
| sQ18_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f3572,f15443,f15367,f15446,f15449]) ).
fof(f15453,plain,
( sQ32_spl
| ~ sQ31_spl
| ~ sQ21_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f3573,f15443,f15377,f15446,f15449]) ).
fof(f15477,definition,
( sQ39_spl
<=> s(num,u_0) = s(num,u_0) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f15481,plain,
( ~ sQ10_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f3869,f15477,f15177]) ).
fof(f15655,definition,
! [X0] :
( sQ86_spl
<=> s(num,i(s(fun(num,num),bit1),s(num,X0))) != s(num,u_0) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f15658,plain,
( sQ2_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f4864,f15655,f15143]) ).
fof(f15665,definition,
! [X0,X1] :
( sQ88_spl
<=> s(num,i(s(fun(num,num),bit0),s(num,X0))) != s(num,i(s(fun(num,num),bit1),s(num,X1))) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f15668,plain,
( sQ2_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f4880,f15665,f15143]) ).
fof(f15831,definition,
! [X0,X1,X2] :
( sQ132_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f15834,plain,
( ~ sQ10_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f9184,f15831,f15177]) ).
fof(f15835,definition,
! [X0,X1,X2] :
( sQ133_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f15838,plain,
( sQ2_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f9197,f15835,f15143]) ).
fof(f15866,definition,
! [X0,X1,X2] :
( sQ141_spl
<=> s(fun(finite_image(X0),X1),i(s(fun(cart(X1,X0),fun(finite_image(X0),X1)),destu_cart),s(cart(X1,X0),i(s(fun(fun(finite_image(X0),X1),cart(X1,X0)),mku_cart),s(fun(finite_image(X0),X1),X2))))) = s(fun(finite_image(X0),X1),X2) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f15869,plain,
( sQ141_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f10830,f15177,f15866]) ).
fof(f15934,definition,
( sQ159_spl
<=> p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f15935,plain,
( ~ sQ159_spl
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(component_clause,[status(thm)],[f15934]) ).
fof(f15936,plain,
( sQ159_spl
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(component_clause,[status(thm)],[f15934]) ).
fof(f15937,definition,
( sQ160_spl
<=> s(cart(real,sK2954_skl),sK2955_skl) = s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f15938,plain,
( ~ sQ160_spl
| s(cart(real,sK2954_skl),sK2955_skl) = s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
inference(component_clause,[status(thm)],[f15937]) ).
fof(f15939,plain,
( sQ160_spl
| s(cart(real,sK2954_skl),sK2955_skl) != s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
inference(component_clause,[status(thm)],[f15937]) ).
fof(f15940,plain,
( ~ sQ160_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f12666,f15934,f15937]) ).
fof(f15941,plain,
( sQ160_spl
| ~ sQ159_spl ),
inference(split_clause,[status(thm)],[f12667,f15934,f15937]) ).
fof(f15942,plain,
( sQ19_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f12724,f15364,f15370]) ).
fof(f15943,plain,
( ~ sQ20_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f12725,f15364,f15373]) ).
fof(f15944,plain,
( sQ20_spl
| ~ sQ19_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f12726,f15364,f15370,f15373]) ).
fof(f15945,plain,
( sQ18_spl
| sQ19_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f12728,f15383,f15370,f15367]) ).
fof(f15946,plain,
( ~ sQ21_spl
| sQ19_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f12729,f15383,f15370,f15377]) ).
fof(f15947,plain,
( sQ18_spl
| ~ sQ20_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f12730,f15383,f15373,f15367]) ).
fof(f15948,plain,
( ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f12731,f15383,f15373,f15377]) ).
fof(f15949,plain,
( sQ20_spl
| ~ sQ19_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f12732,f15383,f15370,f15373]) ).
fof(f15950,plain,
( sQ21_spl
| ~ sQ18_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f12733,f15383,f15367,f15377]) ).
fof(f15951,plain,
( sQ18_spl
| sQ20_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f12735,f15388,f15373,f15367]) ).
fof(f15952,plain,
( ~ sQ21_spl
| sQ20_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f12736,f15388,f15373,f15377]) ).
fof(f15953,plain,
( sQ18_spl
| ~ sQ19_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f12737,f15388,f15370,f15367]) ).
fof(f15954,plain,
( ~ sQ21_spl
| ~ sQ19_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f12738,f15388,f15370,f15377]) ).
fof(f15955,plain,
( sQ19_spl
| ~ sQ20_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f12739,f15388,f15373,f15370]) ).
fof(f15956,plain,
( sQ21_spl
| ~ sQ18_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f12740,f15388,f15367,f15377]) ).
fof(f15957,plain,
( sQ19_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f12742,f15443,f15370]) ).
fof(f15958,plain,
( ~ sQ20_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f12743,f15443,f15373]) ).
fof(f15959,plain,
( sQ20_spl
| ~ sQ19_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f12744,f15443,f15370,f15373]) ).
fof(f15981,plain,
( ~ sQ9_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f15175]) ).
fof(f15982,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f15981]) ).
fof(f16021,plain,
( ~ sQ160_spl
| s(cart(real,sK2954_skl),sK2955_skl) = s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,u_0))) ),
inference(backward_demodulation,[status(thm)],[f3870,f15938]) ).
fof(f16079,plain,
( ~ sQ159_spl
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(forward_demodulation,[status(thm)],[f3870,f15935]) ).
fof(f16087,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6049,f15147]) ).
fof(f16088,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f16087]) ).
fof(f16123,plain,
( sQ159_spl
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(forward_demodulation,[status(thm)],[f3870,f15936]) ).
fof(f16124,plain,
( sQ160_spl
| s(cart(real,sK2954_skl),sK2955_skl) != s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,u_0))) ),
inference(forward_demodulation,[status(thm)],[f3870,f15939]) ).
fof(f16142,plain,
( ~ sQ159_spl
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) ),
inference(resolution,[status(thm)],[f6047,f16079]) ).
fof(f16187,plain,
( sQ19_spl
| s(bool,t) != s(bool,a) ),
inference(resolution,[status(thm)],[f3064,f15372]) ).
fof(f16188,plain,
( sQ4_spl
| s(bool,t) != s(bool,sK5_skl) ),
inference(resolution,[status(thm)],[f3064,f15152]) ).
fof(f16196,plain,
! [X0] : s(bool,t) != s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X0))),
inference(resolution,[status(thm)],[f3064,f6049]) ).
fof(f16199,plain,
( p(s(bool,f0))
| s(bool,t) != s(bool,u_falsityu_) ),
inference(paramodulation,[status(thm)],[f2904,f3064]) ).
fof(f16200,definition,
( sQ166_spl
<=> s(bool,t) = s(bool,u_falsityu_) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f16203,plain,
( sQ2_spl
| ~ sQ166_spl ),
inference(split_clause,[status(thm)],[f16199,f16200,f15143]) ).
fof(f16205,plain,
( ~ sQ13_spl
| s(bool,t) = s(bool,a0) ),
inference(resolution,[status(thm)],[f3065,f15269]) ).
fof(f16208,plain,
( ~ sQ20_spl
| s(bool,t) = s(bool,b) ),
inference(resolution,[status(thm)],[f3065,f15374]) ).
fof(f16212,plain,
s(bool,t) = s(bool,sK134_skl),
inference(resolution,[status(thm)],[f3065,f3625]) ).
fof(f16219,plain,
! [X0,X1] :
( s(bool,X0) != s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X1))),s(real,X1)))
| s(bool,t) != s(bool,X0) ),
inference(resolution,[status(thm)],[f16196,f2926]) ).
fof(f16253,definition,
( sQ167_spl
<=> s(bool,f0) = s(bool,u_falsityu_) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f16255,plain,
( sQ167_spl
| s(bool,f0) != s(bool,u_falsityu_) ),
inference(component_clause,[status(thm)],[f16253]) ).
fof(f16257,plain,
( sQ167_spl
| s(bool,f0) != s(bool,f0) ),
inference(forward_demodulation,[status(thm)],[f2904,f16255]) ).
fof(f16258,plain,
( sQ167_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16257]) ).
fof(f16259,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f16258]) ).
fof(f16269,definition,
( sQ168_spl
<=> s(bool,t) = s(bool,f0) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f16270,plain,
( ~ sQ168_spl
| s(bool,t) = s(bool,f0) ),
inference(component_clause,[status(thm)],[f16269]) ).
fof(f16271,plain,
( sQ168_spl
| s(bool,t) != s(bool,f0) ),
inference(component_clause,[status(thm)],[f16269]) ).
fof(f16382,plain,
( sQ18_spl
| s(bool,f0) = s(bool,c0) ),
inference(resolution,[status(thm)],[f3069,f15369]) ).
fof(f16412,definition,
( sQ171_spl
<=> s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) = s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f16413,plain,
( ~ sQ171_spl
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) = s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) ),
inference(component_clause,[status(thm)],[f16412]) ).
fof(f16414,plain,
( sQ171_spl
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) ),
inference(component_clause,[status(thm)],[f16412]) ).
fof(f16416,plain,
( ~ sQ171_spl
| ~ sQ159_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16413,f16142]) ).
fof(f16417,plain,
( ~ sQ171_spl
| ~ sQ159_spl ),
inference(contradiction_clause,[status(thm)],[f16416]) ).
fof(f16418,plain,
! [X0] :
( sQ168_spl
| s(bool,X0) != s(bool,f0)
| s(bool,t) != s(bool,X0) ),
inference(resolution,[status(thm)],[f16271,f2926]) ).
fof(f16420,plain,
! [X0,X1] :
( sQ168_spl
| s(bool,X1) != s(bool,X0)
| s(bool,t) != s(bool,X1)
| s(bool,X0) != s(bool,f0) ),
inference(resolution,[status(thm)],[f16418,f2926]) ).
fof(f16529,plain,
! [X0,X1] : s(n10,X0) = s(n10,X1),
inference(paramodulation,[status(thm)],[f3634,f3634]) ).
fof(f16658,plain,
! [X0] :
( sQ168_spl
| s(bool,X0) != s(bool,u_falsityu_)
| s(bool,t) != s(bool,X0)
| s(bool,f0) != s(bool,f0) ),
inference(paramodulation,[status(thm)],[f2904,f16420]) ).
fof(f16665,definition,
( sQ172_spl
<=> s(bool,f0) = s(bool,f0) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f16667,plain,
( sQ172_spl
| s(bool,f0) != s(bool,f0) ),
inference(component_clause,[status(thm)],[f16665]) ).
fof(f16668,definition,
! [X0] :
( sQ173_spl
<=> ( s(bool,X0) != s(bool,u_falsityu_)
| s(bool,t) != s(bool,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f16671,plain,
( sQ168_spl
| sQ173_spl
| ~ sQ172_spl ),
inference(split_clause,[status(thm)],[f16658,f16665,f16668,f16269]) ).
fof(f16675,plain,
( sQ172_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16667]) ).
fof(f16676,plain,
sQ172_spl,
inference(contradiction_clause,[status(thm)],[f16675]) ).
fof(f16786,plain,
( ~ sQ168_spl
| ~ p(s(bool,t)) ),
inference(backward_demodulation,[status(thm)],[f16270,f3072]) ).
fof(f16801,plain,
( ~ sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16786,f2903]) ).
fof(f16802,plain,
~ sQ168_spl,
inference(contradiction_clause,[status(thm)],[f16801]) ).
fof(f17042,plain,
! [X0] :
( sQ12_spl
| s(bool,X0) != s(bool,b0)
| s(bool,a0) != s(bool,X0) ),
inference(resolution,[status(thm)],[f15267,f2926]) ).
fof(f17127,definition,
! [X1] :
( sQ203_spl
<=> p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f17128,plain,
! [X0] :
( ~ sQ203_spl
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,X0)))) ),
inference(component_clause,[status(thm)],[f17127]) ).
fof(f17140,plain,
( ~ sQ203_spl
| $false ),
inference(resolution,[status(thm)],[f17128,f6049]) ).
fof(f17152,plain,
~ sQ203_spl,
inference(contradiction_clause,[status(thm)],[f17140]) ).
fof(f17255,plain,
! [X0,X1] :
( ~ sQ5_spl
| p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,X0))),s(real,X1)))) ),
inference(backward_subsumption_resolution,[status(thm)],[f5946,f15156]) ).
fof(f17276,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17255,f15156]) ).
fof(f17277,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f17276]) ).
fof(f17469,plain,
! [X0] : s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0))))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))),
inference(forward_demodulation,[status(thm)],[f3870,f12650]) ).
fof(f17470,plain,
! [X0] : s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0))))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))),
inference(forward_demodulation,[status(thm)],[f3870,f17469]) ).
fof(f17483,plain,
! [X0,X1] : p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1)))))),
inference(forward_demodulation,[status(thm)],[f3870,f12651]) ).
fof(f17722,plain,
! [X0] :
( sQ19_spl
| s(bool,X0) != s(bool,a)
| s(bool,t) != s(bool,X0) ),
inference(resolution,[status(thm)],[f16187,f2926]) ).
fof(f17785,definition,
( sQ205_spl
<=> s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f17787,plain,
( sQ205_spl
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
inference(component_clause,[status(thm)],[f17785]) ).
fof(f17800,plain,
! [X0,X1] :
( s(cart(real,X0),X1) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
inference(forward_demodulation,[status(thm)],[f3870,f12661]) ).
fof(f17801,plain,
! [X0,X1] :
( s(cart(real,X0),X1) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0)))
| s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
inference(forward_demodulation,[status(thm)],[f3870,f17800]) ).
fof(f17805,plain,
( ~ sQ171_spl
| s(cart(real,sK2954_skl),sK2955_skl) = s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,u_0))) ),
inference(resolution,[status(thm)],[f17801,f16413]) ).
fof(f17812,plain,
! [X0] :
( s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0))) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0)))
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
inference(paramodulation,[status(thm)],[f17470,f17801]) ).
fof(f17815,plain,
( ~ sQ171_spl
| sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17805,f16124]) ).
fof(f17816,plain,
( ~ sQ171_spl
| sQ160_spl ),
inference(contradiction_clause,[status(thm)],[f17815]) ).
fof(f17817,definition,
! [X0] :
( sQ208_spl
<=> s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0))) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0))) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f17820,plain,
( sQ208_spl
| ~ sQ205_spl ),
inference(split_clause,[status(thm)],[f17812,f17785,f17817]) ).
fof(f17823,plain,
( sQ205_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17787]) ).
fof(f17824,plain,
sQ205_spl,
inference(contradiction_clause,[status(thm)],[f17823]) ).
fof(f17825,plain,
! [X0] :
( sQ4_spl
| s(bool,X0) != s(bool,sK5_skl)
| s(bool,t) != s(bool,X0) ),
inference(resolution,[status(thm)],[f16188,f2926]) ).
fof(f17833,plain,
! [X0,X1,X2,X3] :
( p(s(bool,X3))
| p(s(bool,i(s(fun(n10,bool),X0),s(n10,X2))))
| ~ p(s(bool,i(s(fun(n10,bool),X0),s(n10,X1)))) ),
inference(paramodulation,[status(thm)],[f16529,f3230]) ).
fof(f17837,definition,
! [X0,X1,X2] :
( sQ209_spl
<=> ( p(s(bool,i(s(fun(n10,bool),X0),s(n10,X2))))
| ~ p(s(bool,i(s(fun(n10,bool),X0),s(n10,X1)))) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f17840,plain,
( sQ3_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f17833,f17837,f15146]) ).
fof(f17866,plain,
! [X0] :
( sQ171_spl
| s(real,X0) != s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,X0) ),
inference(resolution,[status(thm)],[f16414,f2926]) ).
fof(f17880,plain,
! [X0,X1] :
( s(cart(real,X0),X1) != s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))
| s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
inference(forward_demodulation,[status(thm)],[f3870,f12662]) ).
fof(f17881,plain,
! [X0,X1] :
( s(cart(real,X0),X1) != s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,u_0)))
| s(real,i(s(fun(cart(real,X0),real),vectoru_norm),s(cart(real,X0),X1))) = s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
inference(forward_demodulation,[status(thm)],[f3870,f17880]) ).
fof(f17906,plain,
! [X0,X1,X2] :
( ~ sQ13_spl
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK37_skl(X1,a0,X0)))))
| ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f16205,f3212]) ).
fof(f17907,plain,
! [X0,X1,X2] :
( ~ sQ13_spl
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK36_skl(X1,a0,X0)))))
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f16205,f3210]) ).
fof(f17908,plain,
! [X0,X1,X2] :
( ~ sQ13_spl
| ~ p(s(bool,t))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK35_skl(a0,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f16205,f3204]) ).
fof(f17909,plain,
! [X0,X1,X2] :
( ~ sQ13_spl
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,t))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK34_skl(a0,X1,X0))))) ),
inference(paramodulation,[status(thm)],[f16205,f3202]) ).
fof(f17911,plain,
! [X0] :
( ~ sQ13_spl
| s(bool,a0) != s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X0)))
| s(bool,t) != s(bool,t) ),
inference(paramodulation,[status(thm)],[f16205,f16219]) ).
fof(f17916,definition,
! [X0,X1,X2] :
( sQ211_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK37_skl(X1,a0,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f17919,plain,
( ~ sQ13_spl
| ~ sQ10_spl
| sQ211_spl ),
inference(split_clause,[status(thm)],[f17906,f17916,f15177,f15268]) ).
fof(f17920,definition,
! [X0,X1,X2] :
( sQ212_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK36_skl(X1,a0,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f17923,plain,
( ~ sQ13_spl
| sQ212_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f17907,f15177,f17920,f15268]) ).
fof(f17924,definition,
! [X0,X1,X2] :
( sQ213_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK35_skl(a0,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f17927,plain,
( ~ sQ13_spl
| ~ sQ10_spl
| sQ213_spl ),
inference(split_clause,[status(thm)],[f17908,f17924,f15177,f15268]) ).
fof(f17928,definition,
! [X0,X1,X2] :
( sQ214_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK34_skl(a0,X1,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f17931,plain,
( ~ sQ13_spl
| ~ sQ10_spl
| sQ214_spl ),
inference(split_clause,[status(thm)],[f17909,f17928,f15177,f15268]) ).
fof(f17932,definition,
( sQ215_spl
<=> s(bool,t) = s(bool,t) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f17934,plain,
( sQ215_spl
| s(bool,t) != s(bool,t) ),
inference(component_clause,[status(thm)],[f17932]) ).
fof(f17936,definition,
! [X0] :
( sQ216_spl
<=> s(bool,a0) != s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X0))) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f17939,plain,
( ~ sQ13_spl
| sQ216_spl
| ~ sQ215_spl ),
inference(split_clause,[status(thm)],[f17911,f17932,f17936,f15268]) ).
fof(f17942,plain,
( sQ215_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17934]) ).
fof(f17943,plain,
sQ215_spl,
inference(contradiction_clause,[status(thm)],[f17942]) ).
fof(f17988,plain,
( sQ171_spl
| s(cart(real,sK2954_skl),sK2955_skl) != s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,u_0)))
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) ),
inference(resolution,[status(thm)],[f17866,f17881]) ).
fof(f18006,definition,
( sQ217_spl
<=> s(cart(real,sK2954_skl),sK2955_skl) = s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,u_0))) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f18008,plain,
( sQ217_spl
| s(cart(real,sK2954_skl),sK2955_skl) != s(cart(real,sK2954_skl),i(s(fun(num,cart(real,sK2954_skl)),vec),s(num,u_0))) ),
inference(component_clause,[status(thm)],[f18006]) ).
fof(f18009,plain,
( sQ171_spl
| ~ sQ217_spl
| ~ sQ205_spl ),
inference(split_clause,[status(thm)],[f17988,f17785,f18006,f16412]) ).
fof(f18172,plain,
( ~ sQ20_spl
| sQ4_spl
| s(bool,t) != s(bool,sK5_skl)
| s(bool,t) != s(bool,b) ),
inference(paramodulation,[status(thm)],[f16208,f17825]) ).
fof(f18173,plain,
( ~ sQ20_spl
| sQ19_spl
| s(bool,t) != s(bool,a)
| s(bool,t) != s(bool,b) ),
inference(paramodulation,[status(thm)],[f16208,f17722]) ).
fof(f18175,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK37_skl(X1,b,X0)))))
| ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f16208,f3212]) ).
fof(f18176,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK36_skl(X1,b,X0)))))
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f16208,f3210]) ).
fof(f18177,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ p(s(bool,t))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK35_skl(b,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f16208,f3204]) ).
fof(f18178,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,t))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK34_skl(b,X1,X0))))) ),
inference(paramodulation,[status(thm)],[f16208,f3202]) ).
fof(f18180,plain,
! [X0] :
( ~ sQ20_spl
| s(bool,b) != s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X0)))
| s(bool,t) != s(bool,t) ),
inference(paramodulation,[status(thm)],[f16208,f16219]) ).
fof(f18184,definition,
( sQ219_spl
<=> s(bool,t) = s(bool,b) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f18187,definition,
( sQ220_spl
<=> s(bool,t) = s(bool,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f18190,plain,
( ~ sQ20_spl
| sQ4_spl
| ~ sQ220_spl
| ~ sQ219_spl ),
inference(split_clause,[status(thm)],[f18172,f18184,f18187,f15150,f15373]) ).
fof(f18191,definition,
( sQ221_spl
<=> s(bool,t) = s(bool,a) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f18194,plain,
( ~ sQ20_spl
| sQ19_spl
| ~ sQ221_spl
| ~ sQ219_spl ),
inference(split_clause,[status(thm)],[f18173,f18184,f18191,f15370,f15373]) ).
fof(f18199,definition,
! [X0,X1,X2] :
( sQ223_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK37_skl(X1,b,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f18202,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f18175,f18199,f15177,f15373]) ).
fof(f18203,definition,
! [X0,X1,X2] :
( sQ224_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK36_skl(X1,b,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f18206,plain,
( ~ sQ20_spl
| sQ224_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f18176,f15177,f18203,f15373]) ).
fof(f18207,definition,
! [X0,X1,X2] :
( sQ225_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK35_skl(b,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f18210,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| sQ225_spl ),
inference(split_clause,[status(thm)],[f18177,f18207,f15177,f15373]) ).
fof(f18211,definition,
! [X0,X1,X2] :
( sQ226_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK34_skl(b,X1,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f18214,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| sQ226_spl ),
inference(split_clause,[status(thm)],[f18178,f18211,f15177,f15373]) ).
fof(f18216,definition,
! [X0] :
( sQ227_spl
<=> s(bool,b) != s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_lt),s(real,X0))),s(real,X0))) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f18219,plain,
( ~ sQ20_spl
| sQ227_spl
| ~ sQ215_spl ),
inference(split_clause,[status(thm)],[f18180,f17932,f18216,f15373]) ).
fof(f18456,definition,
! [X0] :
( sQ228_spl
<=> ( s(real,X0) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0)))
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f18457,plain,
! [X0] :
( ~ sQ228_spl
| s(real,X0) != s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0)))
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,X0) ),
inference(component_clause,[status(thm)],[f18456]) ).
fof(f18473,plain,
! [X0] :
( ~ sQ228_spl
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) != s(real,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f18457]) ).
fof(f18498,definition,
( sQ231_spl
<=> s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) = s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f18500,plain,
( sQ231_spl
| s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) != s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl))) ),
inference(component_clause,[status(thm)],[f18498]) ).
fof(f18521,plain,
( sQ231_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18500]) ).
fof(f18522,plain,
sQ231_spl,
inference(contradiction_clause,[status(thm)],[f18521]) ).
fof(f18615,plain,
( sQ159_spl
| s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))) = s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(resolution,[status(thm)],[f6032,f16123]) ).
fof(f18657,definition,
( sQ233_spl
<=> p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f18659,plain,
( sQ233_spl
| ~ p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(real,i(s(fun(cart(real,sK2954_skl),real),vectoru_norm),s(cart(real,sK2954_skl),sK2955_skl)))))) ),
inference(component_clause,[status(thm)],[f18657]) ).
fof(f18660,plain,
( sQ159_spl
| sQ171_spl
| ~ sQ233_spl ),
inference(split_clause,[status(thm)],[f18615,f18657,f16412,f15934]) ).
fof(f18713,plain,
( sQ233_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18659,f17483]) ).
fof(f18714,plain,
sQ233_spl,
inference(contradiction_clause,[status(thm)],[f18713]) ).
fof(f18734,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK37_skl(X1,t,X0)))))
| ~ p(s(bool,sK134_skl))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f16212,f3212]) ).
fof(f18735,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK36_skl(X1,t,X0)))))
| ~ p(s(bool,sK134_skl)) ),
inference(paramodulation,[status(thm)],[f16212,f3210]) ).
fof(f18736,plain,
! [X0,X1,X2] :
( ~ p(s(bool,sK134_skl))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK35_skl(t,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f16212,f3204]) ).
fof(f18737,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,sK134_skl))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK34_skl(t,X1,X0))))) ),
inference(paramodulation,[status(thm)],[f16212,f3202]) ).
fof(f18740,definition,
! [X0,X1,X2] :
( sQ234_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK37_skl(X1,t,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f18743,definition,
( sQ235_spl
<=> p(s(bool,sK134_skl)) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f18745,plain,
( sQ235_spl
| ~ p(s(bool,sK134_skl)) ),
inference(component_clause,[status(thm)],[f18743]) ).
fof(f18746,plain,
( ~ sQ235_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f18734,f18740,f18743]) ).
fof(f18747,definition,
! [X0,X1,X2] :
( sQ236_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK36_skl(X1,t,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f18750,plain,
( sQ236_spl
| ~ sQ235_spl ),
inference(split_clause,[status(thm)],[f18735,f18743,f18747]) ).
fof(f18751,definition,
! [X0,X1,X2] :
( sQ237_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK35_skl(t,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f18754,plain,
( ~ sQ235_spl
| sQ237_spl ),
inference(split_clause,[status(thm)],[f18736,f18751,f18743]) ).
fof(f18755,definition,
! [X0,X1,X2] :
( sQ238_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK34_skl(t,X1,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f18758,plain,
( ~ sQ235_spl
| sQ238_spl ),
inference(split_clause,[status(thm)],[f18737,f18755,f18743]) ).
fof(f18761,plain,
( sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18745,f3625]) ).
fof(f18762,plain,
sQ235_spl,
inference(contradiction_clause,[status(thm)],[f18761]) ).
fof(f18801,plain,
( ~ sQ228_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f17470,f18473]) ).
fof(f18820,plain,
~ sQ228_spl,
inference(contradiction_clause,[status(thm)],[f18801]) ).
fof(f18964,plain,
( sQ18_spl
| sQ12_spl
| s(bool,f0) != s(bool,b0)
| s(bool,a0) != s(bool,c0) ),
inference(paramodulation,[status(thm)],[f16382,f17042]) ).
fof(f18971,definition,
( sQ239_spl
<=> s(bool,a0) = s(bool,c0) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f18974,definition,
( sQ240_spl
<=> s(bool,f0) = s(bool,b0) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f18977,plain,
( sQ18_spl
| sQ12_spl
| ~ sQ240_spl
| ~ sQ239_spl ),
inference(split_clause,[status(thm)],[f18964,f18971,f18974,f15265,f15367]) ).
fof(f19045,plain,
( ~ sQ160_spl
| sQ217_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16021,f18008]) ).
fof(f19046,plain,
( ~ sQ160_spl
| sQ217_spl ),
inference(contradiction_clause,[status(thm)],[f19045]) ).
fof(f19047,plain,
$false,
inference(sat_refutation,[status(thm)],[f15153,f15154,f15180,f15184,f15274,f15276,f15359,f15360,f15363,f15452,f15453,f15481,f15658,f15668,f15834,f15838,f15869,f15940,f15941,f15942,f15943,f15944,f15945,f15946,f15947,f15948,f15949,f15950,f15951,f15952,f15953,f15954,f15955,f15956,f15957,f15958,f15959,f15982,f16088,f16203,f16259,f16417,f16671,f16676,f16802,f17152,f17277,f17816,f17820,f17824,f17840,f17919,f17923,f17927,f17931,f17939,f17943,f18009,f18190,f18194,f18202,f18206,f18210,f18214,f18219,f18522,f18660,f18714,f18746,f18750,f18754,f18758,f18762,f18820,f18977,f19046]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO440+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 16:19:07 UTC 2026
% 0.09/0.37 % CPUTime :
% 1.78/2.11 % Drodi V4.1.1
% 10.97/3.38 % Refutation found
% 10.97/3.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.97/3.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.58/3.56 % Elapsed time: 3.174510 seconds
% 6.58/3.56 % CPU time: 12.026604 seconds
% 6.58/3.56 % Total memory used: 1.405 GB
% 6.58/3.56 % Net memory used: 1.400 GB
%------------------------------------------------------------------------------