%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO462+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:05 PM UTC 2026
% Result : Theorem 2.23s 2.94s
% Output : CNFRefutation 2.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 20
% Syntax : Number of formulae : 95 ( 24 unt; 12 def)
% Number of atoms : 259 ( 69 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 270 ( 106 ~; 91 |; 48 &)
% ( 21 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 12 prp; 0-4 aty)
% Number of functors : 28 ( 28 usr; 18 con; 0-3 aty)
% Number of variables : 137 ( 121 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
s(bool,u_falsityu_) = s(bool,f0),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A,P0,A5] :
( ? [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) )
<=> p(s(bool,i(s(fun(A,bool),P0),s(A,A5)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1700,axiom,
! [A,S0] :
( ? [X] : p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,X))),s(fun(A,bool),S0))))
<=> s(fun(A,bool),S0) != s(fun(A,bool),empty) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1708,axiom,
! [A,S0] : p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(fun(A,bool),fun(fun(A,bool),bool)),subset),s(fun(A,bool),empty))),s(fun(A,bool),S0)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1887,axiom,
! [Q50725] : p(s(bool,i(s(fun(fun(Q50725,bool),bool),finite),s(fun(Q50725,bool),empty)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3294,axiom,
! [Q121390,S0] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))
<=> ( ! [C0,X] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0))))
=> p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [X,Y] :
( ( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),Y))),s(fun(cart(real,Q121390),bool),S0))))
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
=> p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(cart(real,Q121390),fun(cart(real,Q121390),cart(real,Q121390))),vectoru_add),s(cart(real,Q121390),X))),s(cart(real,Q121390),Y))))),s(fun(cart(real,Q121390),bool),S0)))) )
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3299,conjecture,
! [Q121443,S0] :
( p(s(bool,i(s(fun(fun(cart(real,Q121443),bool),bool),subspace),s(fun(cart(real,Q121443),bool),S0))))
=> s(fun(cart(real,Q121443),bool),S0) != s(fun(cart(real,Q121443),bool),empty) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3300,negated_conjecture,
~ ! [Q121443,S0] :
( p(s(bool,i(s(fun(fun(cart(real,Q121443),bool),bool),subspace),s(fun(cart(real,Q121443),bool),S0))))
=> s(fun(cart(real,Q121443),bool),S0) != s(fun(cart(real,Q121443),bool),empty) ),
inference(negated_conjecture,[status(cth)],[f3299]) ).
fof(f3351,plain,
s(bool,u_falsityu_) = s(bool,f0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f3509,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(f3510,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)],[f3509]) ).
fof(f3512,plain,
! [X0] :
( ~ p(s(bool,X0))
| s(bool,t) = s(bool,X0) ),
inference(cnf_transformation,[status(thm)],[f3510]) ).
fof(f3515,plain,
! [X0] :
( ~ p(s(bool,X0))
| s(bool,f0) != s(bool,X0) ),
inference(cnf_transformation,[status(thm)],[f3510]) ).
fof(f3602,plain,
! [A,P0,A5] :
( ( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ? [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) ) )
& ( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) ) ),
inference(NNF_transformation,[status(thm)],[f53]) ).
fof(f3603,plain,
( ! [A,P0,A5] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ? [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) ) )
& ! [A,P0,A5] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) ) ),
inference(miniscoping,[status(thm)],[f3602]) ).
fof(f3604,plain,
( ! [A,P0,A5] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ( p(s(bool,i(s(fun(A,bool),P0),s(A,sK15_skl(A5,P0,A)))))
& s(A,sK15_skl(A5,P0,A)) = s(A,A5) ) )
& ! [A,P0,A5] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X,sK15_skl(A5,P0,A))],[f3603]) ).
fof(f3606,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| s(X0,sK15_skl(X1,X2,X0)) = s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3604]) ).
fof(f8135,plain,
! [A,S0] :
( ( s(fun(A,bool),S0) = s(fun(A,bool),empty)
| ? [X] : p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,X))),s(fun(A,bool),S0)))) )
& ( s(fun(A,bool),S0) != s(fun(A,bool),empty)
| ! [X] : ~ p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,X))),s(fun(A,bool),S0)))) ) ),
inference(NNF_transformation,[status(thm)],[f1700]) ).
fof(f8136,plain,
( ! [A,S0] :
( s(fun(A,bool),S0) = s(fun(A,bool),empty)
| ? [X] : p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,X))),s(fun(A,bool),S0)))) )
& ! [A,S0] :
( s(fun(A,bool),S0) != s(fun(A,bool),empty)
| ! [X] : ~ p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,X))),s(fun(A,bool),S0)))) ) ),
inference(miniscoping,[status(thm)],[f8135]) ).
fof(f8137,plain,
( ! [A,S0] :
( s(fun(A,bool),S0) = s(fun(A,bool),empty)
| p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,sK832_skl(S0,A)))),s(fun(A,bool),S0)))) )
& ! [A,S0] :
( s(fun(A,bool),S0) != s(fun(A,bool),empty)
| ! [X] : ~ p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(A,fun(fun(A,bool),bool)),in),s(A,X))),s(fun(A,bool),S0)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK832_skl]),skolemize(X,sK832_skl(S0,A))],[f8136]) ).
fof(f8138,plain,
! [X0,X1,X2] :
( s(fun(X0,bool),X2) != s(fun(X0,bool),empty)
| ~ 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),X2)))) ),
inference(cnf_transformation,[status(thm)],[f8137]) ).
fof(f8158,plain,
! [X0,X1] : p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),empty))),s(fun(X0,bool),X1)))),
inference(cnf_transformation,[status(thm)],[f1708]) ).
fof(f8857,plain,
! [X0] : p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),empty)))),
inference(cnf_transformation,[status(thm)],[f1887]) ).
fof(f14382,plain,
! [Q121390,S0] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))
<=> ( ! [C0,X] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [X,Y] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(cart(real,Q121390),fun(cart(real,Q121390),cart(real,Q121390))),vectoru_add),s(cart(real,Q121390),X))),s(cart(real,Q121390),Y))))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),Y))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0)))) ) ),
inference(pre_NNF_transformation,[status(thm)],[f3294]) ).
fof(f14383,definition,
! [Q121390,S0,X,Y] :
( sP256_prd(Y,X,S0,Q121390)
<=> ( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(cart(real,Q121390),fun(cart(real,Q121390),cart(real,Q121390))),vectoru_add),s(cart(real,Q121390),X))),s(cart(real,Q121390),Y))))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),Y))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) ) ),
introduced(definition,[new_symbols(definition,[sP256_prd])],[]) ).
fof(f14384,plain,
! [Q121390,S0] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0))))
<=> ( ! [C0,X] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [X,Y] : sP256_prd(Y,X,S0,Q121390)
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0)))) ) ),
inference(formula_renaming,[status(thm)],[f14382,f14383]) ).
fof(f14385,plain,
! [Q121390,S0] :
( ( ? [C0,X] :
( ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
| ? [X,Y] : ~ sP256_prd(Y,X,S0,Q121390)
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))
| p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0)))) )
& ( ( ! [C0,X] :
( p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [X,Y] : sP256_prd(Y,X,S0,Q121390)
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0)))) )
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0)))) ) ),
inference(NNF_transformation,[status(thm)],[f14384]) ).
fof(f14386,plain,
( ! [Q121390,S0] :
( ? [X] :
( ? [C0] : ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
| ? [X,Y] : ~ sP256_prd(Y,X,S0,Q121390)
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))
| p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [Q121390,S0] :
( ( ! [X] :
( ! [C0] : p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [X,Y] : sP256_prd(Y,X,S0,Q121390)
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0)))) )
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0)))) ) ),
inference(miniscoping,[status(thm)],[f14385]) ).
fof(f14387,plain,
( ! [Q121390,S0] :
( ( ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,sK3452_skl(S0,Q121390)))),s(cart(real,Q121390),sK3451_skl(S0,Q121390)))))),s(fun(cart(real,Q121390),bool),S0))))
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),sK3451_skl(S0,Q121390)))),s(fun(cart(real,Q121390),bool),S0)))) )
| ~ sP256_prd(sK3450_skl(S0,Q121390),sK3449_skl(S0,Q121390),S0,Q121390)
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0))))
| p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [Q121390,S0] :
( ( ! [X] :
( ! [C0] : p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(cart(real,Q121390),cart(real,Q121390)),i(s(fun(real,fun(cart(real,Q121390),cart(real,Q121390))),r_),s(real,C0))),s(cart(real,Q121390),X))))),s(fun(cart(real,Q121390),bool),S0))))
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),X))),s(fun(cart(real,Q121390),bool),S0)))) )
& ! [X,Y] : sP256_prd(Y,X,S0,Q121390)
& p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),i(s(fun(cart(real,Q121390),fun(fun(cart(real,Q121390),bool),bool)),in),s(cart(real,Q121390),i(s(fun(num,cart(real,Q121390)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,Q121390),bool),S0)))) )
| ~ p(s(bool,i(s(fun(fun(cart(real,Q121390),bool),bool),subspace),s(fun(cart(real,Q121390),bool),S0)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3449_skl,sK3450_skl,sK3451_skl,sK3452_skl]),skolemize(X,sK3449_skl(S0,Q121390)),skolemize(Y,sK3450_skl(S0,Q121390)),skolemize(X,sK3451_skl(S0,Q121390)),skolemize(C0,sK3452_skl(S0,Q121390))],[f14386]) ).
fof(f14388,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),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(fun(cart(real,X0),bool),X1))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),X1)))) ),
inference(cnf_transformation,[status(thm)],[f14387]) ).
fof(f14405,plain,
? [Q121443,S0] :
( s(fun(cart(real,Q121443),bool),S0) = s(fun(cart(real,Q121443),bool),empty)
& p(s(bool,i(s(fun(fun(cart(real,Q121443),bool),bool),subspace),s(fun(cart(real,Q121443),bool),S0)))) ),
inference(pre_NNF_transformation,[status(thm)],[f3300]) ).
fof(f14406,plain,
( s(fun(cart(real,sK3454_skl),bool),sK3455_skl) = s(fun(cart(real,sK3454_skl),bool),empty)
& p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),subspace),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3454_skl,sK3455_skl]),skolemize(Q121443,sK3454_skl),skolemize(S0,sK3455_skl)],[f14405]) ).
fof(f14407,plain,
p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),subspace),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))),
inference(cnf_transformation,[status(thm)],[f14406]) ).
fof(f14408,plain,
s(fun(cart(real,sK3454_skl),bool),sK3455_skl) = s(fun(cart(real,sK3454_skl),bool),empty),
inference(cnf_transformation,[status(thm)],[f14406]) ).
fof(f18005,plain,
p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),finite),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))),
inference(paramodulation,[status(thm)],[f14408,f8857]) ).
fof(f18010,plain,
! [X0] :
( s(fun(cart(real,sK3454_skl),bool),empty) != s(fun(cart(real,sK3454_skl),bool),empty)
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),X0))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
inference(paramodulation,[status(thm)],[f14408,f8138]) ).
fof(f18011,definition,
! [X0] :
( sQ204_spl
<=> ~ p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),X0))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f18012,plain,
! [X0] :
( ~ sQ204_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),X0))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
inference(component_clause,[status(thm)],[f18011]) ).
fof(f18014,definition,
( sQ205_spl
<=> s(fun(cart(real,sK3454_skl),bool),empty) = s(fun(cart(real,sK3454_skl),bool),empty) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f18016,plain,
( sQ205_spl
| s(fun(cart(real,sK3454_skl),bool),empty) != s(fun(cart(real,sK3454_skl),bool),empty) ),
inference(component_clause,[status(thm)],[f18014]) ).
fof(f18017,plain,
( ~ sQ205_spl
| sQ204_spl ),
inference(split_clause,[status(thm)],[f18010,f18011,f18014]) ).
fof(f18018,plain,
( sQ205_spl
| s(fun(cart(real,sK3454_skl),bool),sK3455_skl) != s(fun(cart(real,sK3454_skl),bool),empty) ),
inference(forward_demodulation,[status(thm)],[f14408,f18016]) ).
fof(f18019,plain,
( sQ205_spl
| s(fun(cart(real,sK3454_skl),bool),sK3455_skl) != s(fun(cart(real,sK3454_skl),bool),sK3455_skl) ),
inference(forward_demodulation,[status(thm)],[f14408,f18018]) ).
fof(f18020,plain,
( sQ205_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18019]) ).
fof(f18021,plain,
sQ205_spl,
inference(contradiction_clause,[status(thm)],[f18020]) ).
fof(f18024,plain,
! [X0] : p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(fun(cart(real,sK3454_skl),bool),fun(fun(cart(real,sK3454_skl),bool),bool)),subset),s(fun(cart(real,sK3454_skl),bool),sK3455_skl))),s(fun(cart(real,sK3454_skl),bool),X0)))),
inference(paramodulation,[status(thm)],[f14408,f8158]) ).
fof(f18136,definition,
( sQ215_spl
<=> s(fun(cart(real,sK3454_skl),bool),sK3455_skl) = s(fun(cart(real,sK3454_skl),bool),empty) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f18138,plain,
( sQ215_spl
| s(fun(cart(real,sK3454_skl),bool),sK3455_skl) != s(fun(cart(real,sK3454_skl),bool),empty) ),
inference(component_clause,[status(thm)],[f18136]) ).
fof(f18198,definition,
( sQ218_spl
<=> p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),subspace),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f18200,plain,
( sQ218_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),subspace),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
inference(component_clause,[status(thm)],[f18198]) ).
fof(f18205,plain,
( sQ218_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18200,f14407]) ).
fof(f18206,plain,
sQ218_spl,
inference(contradiction_clause,[status(thm)],[f18205]) ).
fof(f18208,plain,
( sQ215_spl
| s(fun(cart(real,sK3454_skl),bool),sK3455_skl) != s(fun(cart(real,sK3454_skl),bool),sK3455_skl) ),
inference(forward_demodulation,[status(thm)],[f14408,f18138]) ).
fof(f18209,plain,
( sQ215_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18208]) ).
fof(f18210,plain,
sQ215_spl,
inference(contradiction_clause,[status(thm)],[f18209]) ).
fof(f18231,plain,
! [X0] : s(bool,t) = s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),empty))),
inference(resolution,[status(thm)],[f3512,f8857]) ).
fof(f18240,definition,
( sQ221_spl
<=> p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(fun(cart(real,sK3454_skl),bool),fun(fun(cart(real,sK3454_skl),bool),bool)),subset),s(fun(cart(real,sK3454_skl),bool),sK3455_skl))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f18242,plain,
( sQ221_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(fun(cart(real,sK3454_skl),bool),fun(fun(cart(real,sK3454_skl),bool),bool)),subset),s(fun(cart(real,sK3454_skl),bool),sK3455_skl))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
inference(component_clause,[status(thm)],[f18240]) ).
fof(f18244,plain,
( sQ221_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18242,f18024]) ).
fof(f18245,plain,
sQ221_spl,
inference(contradiction_clause,[status(thm)],[f18244]) ).
fof(f18246,plain,
p(s(bool,t)),
inference(backward_demodulation,[status(thm)],[f18231,f8857]) ).
fof(f18261,definition,
! [X0] :
( sQ224_spl
<=> s(bool,t) != s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),empty))) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f18262,plain,
! [X0] :
( ~ sQ224_spl
| s(bool,t) != s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),empty))) ),
inference(component_clause,[status(thm)],[f18261]) ).
fof(f18267,plain,
( ~ sQ224_spl
| s(bool,t) != s(bool,t) ),
inference(forward_demodulation,[status(thm)],[f18231,f18262]) ).
fof(f18268,plain,
( ~ sQ224_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18267]) ).
fof(f18269,plain,
~ sQ224_spl,
inference(contradiction_clause,[status(thm)],[f18268]) ).
fof(f18309,plain,
s(bool,f0) != s(bool,t),
inference(resolution,[status(thm)],[f3515,f18246]) ).
fof(f18322,definition,
( sQ228_spl
<=> s(bool,f0) = s(bool,u_falsityu_) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f18324,plain,
( sQ228_spl
| s(bool,f0) != s(bool,u_falsityu_) ),
inference(component_clause,[status(thm)],[f18322]) ).
fof(f18327,plain,
( sQ228_spl
| s(bool,f0) != s(bool,f0) ),
inference(forward_demodulation,[status(thm)],[f3351,f18324]) ).
fof(f18328,plain,
( sQ228_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18327]) ).
fof(f18329,plain,
sQ228_spl,
inference(contradiction_clause,[status(thm)],[f18328]) ).
fof(f18340,definition,
! [X0] :
( sQ229_spl
<=> s(bool,f0) = s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),empty))) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f18341,plain,
! [X0] :
( ~ sQ229_spl
| s(bool,f0) = s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),empty))) ),
inference(component_clause,[status(thm)],[f18340]) ).
fof(f18345,plain,
( ~ sQ229_spl
| s(bool,f0) = s(bool,t) ),
inference(forward_demodulation,[status(thm)],[f18231,f18341]) ).
fof(f18407,definition,
! [X0] :
( sQ235_spl
<=> s(fun(X0,bool),empty) != s(fun(X0,bool),empty) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f18408,plain,
! [X0] :
( ~ sQ235_spl
| s(fun(X0,bool),empty) != s(fun(X0,bool),empty) ),
inference(component_clause,[status(thm)],[f18407]) ).
fof(f18412,plain,
( ~ sQ235_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18408]) ).
fof(f18413,plain,
~ sQ235_spl,
inference(contradiction_clause,[status(thm)],[f18412]) ).
fof(f18485,plain,
( ~ sQ229_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18345,f18309]) ).
fof(f18486,plain,
~ sQ229_spl,
inference(contradiction_clause,[status(thm)],[f18485]) ).
fof(f18503,definition,
( sQ238_spl
<=> s(bool,f0) = s(bool,f0) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f18505,plain,
( sQ238_spl
| s(bool,f0) != s(bool,f0) ),
inference(component_clause,[status(thm)],[f18503]) ).
fof(f18508,plain,
( sQ238_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18505]) ).
fof(f18509,plain,
sQ238_spl,
inference(contradiction_clause,[status(thm)],[f18508]) ).
fof(f18675,plain,
s(fun(cart(real,sK3454_skl),bool),sK15_skl(sK3455_skl,finite,fun(cart(real,sK3454_skl),bool))) = s(fun(cart(real,sK3454_skl),bool),sK3455_skl),
inference(resolution,[status(thm)],[f3606,f18005]) ).
fof(f20449,plain,
( p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),i(s(fun(num,cart(real,sK3454_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,sK3454_skl),bool),sK15_skl(sK3455_skl,finite,fun(cart(real,sK3454_skl),bool))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),subspace),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
inference(paramodulation,[status(thm)],[f18675,f14388]) ).
fof(f20511,definition,
( sQ318_spl
<=> p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),i(s(fun(num,cart(real,sK3454_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,sK3454_skl),bool),sK15_skl(sK3455_skl,finite,fun(cart(real,sK3454_skl),bool)))))) ),
introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition]) ).
fof(f20512,plain,
( ~ sQ318_spl
| p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),i(s(fun(num,cart(real,sK3454_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,sK3454_skl),bool),sK15_skl(sK3455_skl,finite,fun(cart(real,sK3454_skl),bool)))))) ),
inference(component_clause,[status(thm)],[f20511]) ).
fof(f20514,plain,
( sQ318_spl
| ~ sQ218_spl ),
inference(split_clause,[status(thm)],[f20449,f18198,f20511]) ).
fof(f20599,plain,
( ~ sQ318_spl
| p(s(bool,i(s(fun(fun(cart(real,sK3454_skl),bool),bool),i(s(fun(cart(real,sK3454_skl),fun(fun(cart(real,sK3454_skl),bool),bool)),in),s(cart(real,sK3454_skl),i(s(fun(num,cart(real,sK3454_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,sK3454_skl),bool),sK3455_skl)))) ),
inference(forward_demodulation,[status(thm)],[f18675,f20512]) ).
fof(f20600,plain,
( ~ sQ318_spl
| ~ sQ204_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20599,f18012]) ).
fof(f20601,plain,
( ~ sQ318_spl
| ~ sQ204_spl ),
inference(contradiction_clause,[status(thm)],[f20600]) ).
fof(f20602,plain,
$false,
inference(sat_refutation,[status(thm)],[f18017,f18021,f18206,f18210,f18245,f18269,f18329,f18413,f18486,f18509,f20514,f20601]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO462+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n011.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 20 16:29:26 UTC 2026
% 0.10/0.38 % CPUTime :
% 2.06/2.35 % Drodi V4.1.1
% 2.23/2.94 % Refutation found
% 2.23/2.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.23/2.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.25/3.13 % Elapsed time: 2.727236 seconds
% 2.25/3.13 % CPU time: 6.755077 seconds
% 2.25/3.13 % Total memory used: 1.465 GB
% 2.25/3.13 % Net memory used: 1.461 GB
%------------------------------------------------------------------------------