%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO445+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 : n008.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 2.10s 2.87s
% Output : CNFRefutation 2.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 35
% Syntax : Number of formulae : 121 ( 14 unt; 19 def)
% Number of atoms : 315 ( 91 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 325 ( 131 ~; 121 |; 36 &)
% ( 34 <=>; 2 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 20 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 23 con; 0-2 aty)
% Number of variables : 167 ( 154 !; 13 ?)
% 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(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(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(f199,axiom,
( s(num,u_0) = s(num,u_0)
<=> p(s(bool,t)) ),
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(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(f2796,axiom,
! [Q100205,X,Y] : s(real,i(s(fun(cart(real,Q100205),real),i(s(fun(cart(real,Q100205),fun(cart(real,Q100205),real)),dot),s(cart(real,Q100205),X))),s(cart(real,Q100205),Y))) = s(real,i(s(fun(cart(real,Q100205),real),i(s(fun(cart(real,Q100205),fun(cart(real,Q100205),real)),dot),s(cart(real,Q100205),Y))),s(cart(real,Q100205),X))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2807,axiom,
! [Q100487,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,Q100487),real),i(s(fun(cart(real,Q100487),fun(cart(real,Q100487),real)),dot),s(cart(real,Q100487),X))),s(cart(real,Q100487),X)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2889,axiom,
! [Q104636,X,Y] :
( s(cart(real,Q104636),X) = s(cart(real,Q104636),Y)
<=> ( s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))
& s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3003,conjecture,
! [Q110616,X,Y] :
( ! [Z0] : s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0))) = s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0)))
<=> s(cart(real,Q110616),X) = s(cart(real,Q110616),Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3004,negated_conjecture,
~ ! [Q110616,X,Y] :
( ! [Z0] : s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0))) = s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0)))
<=> s(cart(real,Q110616),X) = s(cart(real,Q110616),Y) ),
inference(negated_conjecture,[status(cth)],[f3003]) ).
fof(f3044,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(f3045,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)],[f3044]) ).
fof(f3047,plain,
( ~ p(s(bool,sK5_skl))
| p(s(bool,f0)) ),
inference(cnf_transformation,[status(thm)],[f3045]) ).
fof(f3048,plain,
! [X] :
( ~ p(s(bool,X))
<=> ( p(s(bool,f0))
| ~ p(s(bool,X)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f3049,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)],[f3048]) ).
fof(f3050,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)],[f3049]) ).
fof(f3051,plain,
! [X0] :
( p(s(bool,f0))
| ~ p(s(bool,X0))
| p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3050]) ).
fof(f3055,plain,
s(bool,u_falsityu_) = s(bool,f0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f3065,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(f3066,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)],[f3065]) ).
fof(f3067,plain,
! [X0,X1] :
( p(s(bool,t))
| s(X0,X1) != s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3066]) ).
fof(f3068,plain,
! [X0,X1] :
( ~ p(s(bool,t))
| s(X0,X1) = s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3066]) ).
fof(f3223,plain,
~ p(s(bool,f0)),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f3224,plain,
( ( ~ p(s(bool,t))
| ~ p(s(bool,f0)) )
& ( p(s(bool,t))
| p(s(bool,f0)) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f3226,plain,
( ~ p(s(bool,t))
| ~ p(s(bool,f0)) ),
inference(cnf_transformation,[status(thm)],[f3224]) ).
fof(f4018,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(f4020,plain,
( ~ p(s(bool,t))
| s(num,u_0) = s(num,u_0) ),
inference(cnf_transformation,[status(thm)],[f4018]) ).
fof(f5013,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(f5014,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)],[f5013]) ).
fof(f5015,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)],[f5014]) ).
fof(f5029,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(f5030,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)],[f5029]) ).
fof(f5031,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)],[f5030]) ).
fof(f9329,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(f9330,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)],[f9329]) ).
fof(f9331,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)],[f9330]) ).
fof(f9332,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))],[f9331]) ).
fof(f9335,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)],[f9332]) ).
fof(f9345,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(f9346,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)],[f9345]) ).
fof(f9347,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))],[f9346]) ).
fof(f9348,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)],[f9347]) ).
fof(f10979,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(f10980,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)],[f10979]) ).
fof(f10981,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)],[f10980]) ).
fof(f12682,plain,
! [X0,X1,X2] : s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X2))) = s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X2))),s(cart(real,X0),X1))),
inference(cnf_transformation,[status(thm)],[f2796]) ).
fof(f12693,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),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X1)))))),
inference(cnf_transformation,[status(thm)],[f2807]) ).
fof(f12916,plain,
! [Q104636,X,Y] :
( ( s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y))) != s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))
| s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))) != s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y)))
| s(cart(real,Q104636),X) = s(cart(real,Q104636),Y) )
& ( ( s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))
& s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y))) )
| s(cart(real,Q104636),X) != s(cart(real,Q104636),Y) ) ),
inference(NNF_transformation,[status(thm)],[f2889]) ).
fof(f12917,plain,
( ! [Q104636,X,Y] :
( s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y))) != s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))
| s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))) != s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y)))
| s(cart(real,Q104636),X) = s(cart(real,Q104636),Y) )
& ! [Q104636,X,Y] :
( ( s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))
& s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y))) )
| s(cart(real,Q104636),X) != s(cart(real,Q104636),Y) ) ),
inference(miniscoping,[status(thm)],[f12916]) ).
fof(f12920,plain,
! [X0,X1,X2] :
( s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X2))),s(cart(real,X0),X2))) != s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X1)))
| s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X1))) != s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X2)))
| s(cart(real,X0),X1) = s(cart(real,X0),X2) ),
inference(cnf_transformation,[status(thm)],[f12917]) ).
fof(f13369,plain,
? [Q110616,X,Y] :
( ! [Z0] : s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0))) = s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0)))
<~> s(cart(real,Q110616),X) = s(cart(real,Q110616),Y) ),
inference(pre_NNF_transformation,[status(thm)],[f3004]) ).
fof(f13370,plain,
? [Q110616,X,Y] :
( ( s(cart(real,Q110616),X) != s(cart(real,Q110616),Y)
| ? [Z0] : s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0))) != s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0))) )
& ( s(cart(real,Q110616),X) = s(cart(real,Q110616),Y)
| ! [Z0] : s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0))) = s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0))) ) ),
inference(NNF_transformation,[status(thm)],[f13369]) ).
fof(f13371,plain,
( ( s(cart(real,sK3163_skl),sK3164_skl) != s(cart(real,sK3163_skl),sK3165_skl)
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl))) )
& ( s(cart(real,sK3163_skl),sK3164_skl) = s(cart(real,sK3163_skl),sK3165_skl)
| ! [Z0] : s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),Z0))) = s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),Z0))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3163_skl,sK3164_skl,sK3165_skl,sK3166_skl]),skolemize(Q110616,sK3163_skl),skolemize(X,sK3164_skl),skolemize(Y,sK3165_skl),skolemize(Z0,sK3166_skl)],[f13370]) ).
fof(f13372,plain,
! [X0] :
( s(cart(real,sK3163_skl),sK3164_skl) = s(cart(real,sK3163_skl),sK3165_skl)
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0))) = s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),X0))) ),
inference(cnf_transformation,[status(thm)],[f13371]) ).
fof(f13373,plain,
( s(cart(real,sK3163_skl),sK3164_skl) != s(cart(real,sK3163_skl),sK3165_skl)
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl))) ),
inference(cnf_transformation,[status(thm)],[f13371]) ).
fof(f15901,definition,
! [X2] :
( sQ1_spl
<=> ( p(s(bool,X2))
| ~ p(s(bool,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f15905,definition,
( sQ2_spl
<=> p(s(bool,f0)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f15908,definition,
! [X0] :
( sQ3_spl
<=> p(s(bool,X0)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f15909,plain,
! [X0] :
( ~ sQ3_spl
| p(s(bool,X0)) ),
inference(component_clause,[status(thm)],[f15908]) ).
fof(f15912,definition,
( sQ4_spl
<=> p(s(bool,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f15915,plain,
( ~ sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f3047,f15905,f15912]) ).
fof(f15916,plain,
( sQ2_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f3051,f15901,f15905]) ).
fof(f15917,definition,
! [X0] :
( sQ5_spl
<=> ~ p(s(bool,X0)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f15918,plain,
! [X0] :
( ~ sQ5_spl
| ~ p(s(bool,X0)) ),
inference(component_clause,[status(thm)],[f15917]) ).
fof(f15936,definition,
! [X0,X1] :
( sQ9_spl
<=> s(X0,X1) != s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f15937,plain,
! [X0,X1] :
( ~ sQ9_spl
| s(X0,X1) != s(X0,X1) ),
inference(component_clause,[status(thm)],[f15936]) ).
fof(f15939,definition,
( sQ10_spl
<=> p(s(bool,t)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f15942,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f3067,f15936,f15939]) ).
fof(f15943,definition,
! [X0,X1] :
( sQ11_spl
<=> s(X0,X1) = s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f15946,plain,
( ~ sQ10_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f3068,f15943,f15939]) ).
fof(f16038,plain,
( ~ sQ10_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f3226,f15905,f15939]) ).
fof(f16239,definition,
( sQ39_spl
<=> s(num,u_0) = s(num,u_0) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f16243,plain,
( ~ sQ10_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f4020,f16239,f15939]) ).
fof(f16417,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(f16420,plain,
( sQ2_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f5015,f16417,f15905]) ).
fof(f16427,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(f16430,plain,
( sQ2_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f5031,f16427,f15905]) ).
fof(f16593,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(f16596,plain,
( ~ sQ10_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f9335,f16593,f15939]) ).
fof(f16597,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(f16600,plain,
( sQ2_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f9348,f16597,f15905]) ).
fof(f16628,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(f16631,plain,
( sQ141_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f10981,f15939,f16628]) ).
fof(f16750,definition,
! [X0] :
( sQ173_spl
<=> s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0))) = s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),X0))) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f16751,plain,
! [X0] :
( ~ sQ173_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0))) = s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),X0))) ),
inference(component_clause,[status(thm)],[f16750]) ).
fof(f16753,definition,
( sQ174_spl
<=> s(cart(real,sK3163_skl),sK3164_skl) = s(cart(real,sK3163_skl),sK3165_skl) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f16754,plain,
( ~ sQ174_spl
| s(cart(real,sK3163_skl),sK3164_skl) = s(cart(real,sK3163_skl),sK3165_skl) ),
inference(component_clause,[status(thm)],[f16753]) ).
fof(f16756,plain,
( sQ174_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f13372,f16750,f16753]) ).
fof(f16757,definition,
( sQ175_spl
<=> s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl))) = s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl))) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f16759,plain,
( sQ175_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl))) ),
inference(component_clause,[status(thm)],[f16757]) ).
fof(f16760,plain,
( ~ sQ174_spl
| ~ sQ175_spl ),
inference(split_clause,[status(thm)],[f13373,f16757,f16753]) ).
fof(f16800,plain,
( ~ sQ9_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f15937]) ).
fof(f16801,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f16800]) ).
fof(f16802,plain,
( sQ175_spl
| ~ sQ174_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl))) ),
inference(forward_demodulation,[status(thm)],[f16754,f16759]) ).
fof(f16803,plain,
( sQ175_spl
| ~ sQ174_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16802]) ).
fof(f16804,plain,
( sQ175_spl
| ~ sQ174_spl ),
inference(contradiction_clause,[status(thm)],[f16803]) ).
fof(f16817,plain,
! [X0] :
( ~ sQ173_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0))) = s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),X0))),s(cart(real,sK3163_skl),sK3165_skl))) ),
inference(paramodulation,[status(thm)],[f16751,f12682]) ).
fof(f17013,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12693,f15918]) ).
fof(f17014,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f17013]) ).
fof(f17118,plain,
~ p(s(bool,u_falsityu_)),
inference(forward_demodulation,[status(thm)],[f3055,f3223]) ).
fof(f17119,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17118,f15909]) ).
fof(f17120,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f17119]) ).
fof(f17144,definition,
( sQ189_spl
<=> s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl))) = s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl))) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f17146,plain,
( sQ189_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl))) ),
inference(component_clause,[status(thm)],[f17144]) ).
fof(f17151,plain,
( sQ189_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17146]) ).
fof(f17152,plain,
sQ189_spl,
inference(contradiction_clause,[status(thm)],[f17151]) ).
fof(f17306,plain,
( ~ sQ173_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3165_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl)))
| s(cart(real,sK3163_skl),sK3164_skl) = s(cart(real,sK3163_skl),sK3165_skl) ),
inference(resolution,[status(thm)],[f12920,f16817]) ).
fof(f17320,definition,
( sQ202_spl
<=> s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3165_skl))) = s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl))) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f17322,plain,
( sQ202_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3165_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl))) ),
inference(component_clause,[status(thm)],[f17320]) ).
fof(f17323,plain,
( ~ sQ173_spl
| ~ sQ202_spl
| sQ174_spl ),
inference(split_clause,[status(thm)],[f17306,f16753,f17320,f16750]) ).
fof(f17345,plain,
( sQ202_spl
| ~ sQ173_spl
| s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3165_skl))) != s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl))) ),
inference(forward_demodulation,[status(thm)],[f16751,f17322]) ).
fof(f17350,plain,
( sQ202_spl
| ~ sQ173_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17345,f16817]) ).
fof(f17351,plain,
( sQ202_spl
| ~ sQ173_spl ),
inference(contradiction_clause,[status(thm)],[f17350]) ).
fof(f17352,plain,
$false,
inference(sat_refutation,[status(thm)],[f15915,f15916,f15942,f15946,f16038,f16243,f16420,f16430,f16596,f16600,f16631,f16756,f16760,f16801,f16804,f17014,f17120,f17152,f17323,f17351]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO445+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.34 % Computer : n008.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Sun Sep 20 16:16:23 UTC 2026
% 0.10/0.34 % CPUTime :
% 1.96/2.20 % Drodi V4.1.1
% 2.10/2.87 % Refutation found
% 2.10/2.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.10/2.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.12/3.04 % Elapsed time: 2.670688 seconds
% 2.12/3.04 % CPU time: 7.213476 seconds
% 2.12/3.04 % Total memory used: 1.404 GB
% 2.12/3.04 % Net memory used: 1.401 GB
%------------------------------------------------------------------------------