%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO451+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 : n006.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:04 PM UTC 2026
% Result : Theorem 15.24s 9.25s
% Output : CNFRefutation 16.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 56 ( 11 unt; 6 def)
% Number of atoms : 157 ( 62 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 165 ( 64 ~; 55 |; 30 &)
% ( 12 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 7 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 18 con; 0-2 aty)
% Number of variables : 86 ( 78 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [A,X] :
( s(A,X) = s(A,X)
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox/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/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(f44,axiom,
( ~ p(s(bool,f0))
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,axiom,
! [N0] : s(num,i(s(fun(num,num),numeral),s(num,N0))) = s(num,N0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3155,axiom,
! [N,M,A5] : s(cart(cart(real,N),M),i(s(fun(cart(cart(real,M),N),cart(cart(real,N),M)),transp),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) = s(cart(cart(real,N),M),A5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3157,axiom,
! [N,M,A5,I0] :
( ( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,I0))),s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ))))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,I0)))) )
=> s(cart(real,M),i(s(fun(cart(cart(real,M),N),cart(real,M)),i(s(fun(num,fun(cart(cart(real,M),N),cart(real,M))),row),s(num,I0))),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) = s(cart(real,M),i(s(fun(cart(cart(real,N),M),cart(real,M)),i(s(fun(num,fun(cart(cart(real,N),M),cart(real,M))),column),s(num,I0))),s(cart(cart(real,N),M),A5))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3158,conjecture,
! [N,M,A5,I0] :
( ( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,I0))),s(num,i(s(fun(fun(M,bool),num),dimindex),s(fun(M,bool),univ))))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,I0)))) )
=> s(cart(real,N),i(s(fun(cart(cart(real,M),N),cart(real,N)),i(s(fun(num,fun(cart(cart(real,M),N),cart(real,N))),column),s(num,I0))),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) = s(cart(real,N),i(s(fun(cart(cart(real,N),M),cart(real,N)),i(s(fun(num,fun(cart(cart(real,N),M),cart(real,N))),row),s(num,I0))),s(cart(cart(real,N),M),A5))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3159,negated_conjecture,
~ ! [N,M,A5,I0] :
( ( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,I0))),s(num,i(s(fun(fun(M,bool),num),dimindex),s(fun(M,bool),univ))))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,I0)))) )
=> s(cart(real,N),i(s(fun(cart(cart(real,M),N),cart(real,N)),i(s(fun(num,fun(cart(cart(real,M),N),cart(real,N))),column),s(num,I0))),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) = s(cart(real,N),i(s(fun(cart(cart(real,N),M),cart(real,N)),i(s(fun(num,fun(cart(cart(real,N),M),cart(real,N))),row),s(num,I0))),s(cart(cart(real,N),M),A5))) ),
inference(negated_conjecture,[status(cth)],[f3158]) ).
fof(f3220,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(f3221,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)],[f3220]) ).
fof(f3222,plain,
! [X0,X1] :
( p(s(bool,t))
| s(X0,X1) != s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3221]) ).
fof(f3230,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(f3231,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)],[f3230]) ).
fof(f3232,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)],[f3231]) ).
fof(f3368,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(f3369,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)],[f3368]) ).
fof(f3375,plain,
! [X0] :
( p(s(bool,X0))
| s(bool,f0) = s(bool,X0) ),
inference(cnf_transformation,[status(thm)],[f3369]) ).
fof(f3379,plain,
( ( ~ p(s(bool,t))
| ~ p(s(bool,f0)) )
& ( p(s(bool,t))
| p(s(bool,f0)) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f3381,plain,
( ~ p(s(bool,t))
| ~ p(s(bool,f0)) ),
inference(cnf_transformation,[status(thm)],[f3379]) ).
fof(f4176,plain,
! [X0] : s(num,i(s(fun(num,num),numeral),s(num,X0))) = s(num,X0),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f13898,plain,
! [X0,X1,X2] : s(cart(cart(real,X0),X1),i(s(fun(cart(cart(real,X1),X0),cart(cart(real,X0),X1)),transp),s(cart(cart(real,X1),X0),i(s(fun(cart(cart(real,X0),X1),cart(cart(real,X1),X0)),transp),s(cart(cart(real,X0),X1),X2))))) = s(cart(cart(real,X0),X1),X2),
inference(cnf_transformation,[status(thm)],[f3155]) ).
fof(f13903,plain,
! [N,M,A5,I0] :
( s(cart(real,M),i(s(fun(cart(cart(real,M),N),cart(real,M)),i(s(fun(num,fun(cart(cart(real,M),N),cart(real,M))),row),s(num,I0))),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) = s(cart(real,M),i(s(fun(cart(cart(real,N),M),cart(real,M)),i(s(fun(num,fun(cart(cart(real,N),M),cart(real,M))),column),s(num,I0))),s(cart(cart(real,N),M),A5)))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,I0))),s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ))))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,I0)))) ),
inference(pre_NNF_transformation,[status(thm)],[f3157]) ).
fof(f13904,plain,
! [N,I0] :
( ! [M,A5] : s(cart(real,M),i(s(fun(cart(cart(real,M),N),cart(real,M)),i(s(fun(num,fun(cart(cart(real,M),N),cart(real,M))),row),s(num,I0))),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) = s(cart(real,M),i(s(fun(cart(cart(real,N),M),cart(real,M)),i(s(fun(num,fun(cart(cart(real,N),M),cart(real,M))),column),s(num,I0))),s(cart(cart(real,N),M),A5)))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,I0))),s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ))))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,I0)))) ),
inference(miniscoping,[status(thm)],[f13903]) ).
fof(f13905,plain,
! [X0,X1,X2,X3] :
( s(cart(real,X2),i(s(fun(cart(cart(real,X2),X1),cart(real,X2)),i(s(fun(num,fun(cart(cart(real,X2),X1),cart(real,X2))),row),s(num,X0))),s(cart(cart(real,X2),X1),i(s(fun(cart(cart(real,X1),X2),cart(cart(real,X2),X1)),transp),s(cart(cart(real,X1),X2),X3))))) = s(cart(real,X2),i(s(fun(cart(cart(real,X1),X2),cart(real,X2)),i(s(fun(num,fun(cart(cart(real,X1),X2),cart(real,X2))),column),s(num,X0))),s(cart(cart(real,X1),X2),X3)))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,X0))),s(num,i(s(fun(fun(X1,bool),num),dimindex),s(fun(X1,bool),univ))))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,X0)))) ),
inference(cnf_transformation,[status(thm)],[f13904]) ).
fof(f13906,plain,
? [N,M,A5,I0] :
( s(cart(real,N),i(s(fun(cart(cart(real,M),N),cart(real,N)),i(s(fun(num,fun(cart(cart(real,M),N),cart(real,N))),column),s(num,I0))),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) != s(cart(real,N),i(s(fun(cart(cart(real,N),M),cart(real,N)),i(s(fun(num,fun(cart(cart(real,N),M),cart(real,N))),row),s(num,I0))),s(cart(cart(real,N),M),A5)))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,I0))),s(num,i(s(fun(fun(M,bool),num),dimindex),s(fun(M,bool),univ))))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,I0)))) ),
inference(pre_NNF_transformation,[status(thm)],[f3159]) ).
fof(f13907,plain,
? [M,I0] :
( ? [N,A5] : s(cart(real,N),i(s(fun(cart(cart(real,M),N),cart(real,N)),i(s(fun(num,fun(cart(cart(real,M),N),cart(real,N))),column),s(num,I0))),s(cart(cart(real,M),N),i(s(fun(cart(cart(real,N),M),cart(cart(real,M),N)),transp),s(cart(cart(real,N),M),A5))))) != s(cart(real,N),i(s(fun(cart(cart(real,N),M),cart(real,N)),i(s(fun(num,fun(cart(cart(real,N),M),cart(real,N))),row),s(num,I0))),s(cart(cart(real,N),M),A5)))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,I0))),s(num,i(s(fun(fun(M,bool),num),dimindex),s(fun(M,bool),univ))))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,I0)))) ),
inference(miniscoping,[status(thm)],[f13906]) ).
fof(f13908,plain,
( s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(real,sK3341_skl))),column),s(num,sK3340_skl))),s(cart(cart(real,sK3339_skl),sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(cart(real,sK3339_skl),sK3341_skl)),transp),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))))) != s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl)))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,sK3340_skl))),s(num,i(s(fun(fun(sK3339_skl,bool),num),dimindex),s(fun(sK3339_skl,bool),univ))))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,sK3340_skl)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3339_skl,sK3340_skl,sK3341_skl,sK3342_skl]),skolemize(M,sK3339_skl),skolemize(I0,sK3340_skl),skolemize(N,sK3341_skl),skolemize(A5,sK3342_skl)],[f13907]) ).
fof(f13909,plain,
p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,sK3340_skl)))),
inference(cnf_transformation,[status(thm)],[f13908]) ).
fof(f13910,plain,
p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,sK3340_skl))),s(num,i(s(fun(fun(sK3339_skl,bool),num),dimindex),s(fun(sK3339_skl,bool),univ)))))),
inference(cnf_transformation,[status(thm)],[f13908]) ).
fof(f13911,plain,
s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(real,sK3341_skl))),column),s(num,sK3340_skl))),s(cart(cart(real,sK3339_skl),sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(cart(real,sK3339_skl),sK3341_skl)),transp),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))))) != s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))),
inference(cnf_transformation,[status(thm)],[f13908]) ).
fof(f16443,definition,
( sQ2_spl
<=> p(s(bool,f0)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f16474,definition,
! [X0,X1] :
( sQ9_spl
<=> s(X0,X1) != s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f16475,plain,
! [X0,X1] :
( ~ sQ9_spl
| s(X0,X1) != s(X0,X1) ),
inference(component_clause,[status(thm)],[f16474]) ).
fof(f16477,definition,
( sQ10_spl
<=> p(s(bool,t)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f16480,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f3222,f16474,f16477]) ).
fof(f16576,plain,
( ~ sQ10_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f3381,f16443,f16477]) ).
fof(f17327,plain,
( ~ sQ9_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16475]) ).
fof(f17328,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f17327]) ).
fof(f17345,plain,
! [X0] :
( s(cart(real,sK3341_skl),X0) != s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl)))
| s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(real,sK3341_skl))),column),s(num,sK3340_skl))),s(cart(cart(real,sK3339_skl),sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(cart(real,sK3339_skl),sK3341_skl)),transp),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))))) != s(cart(real,sK3341_skl),X0) ),
inference(resolution,[status(thm)],[f13911,f3232]) ).
fof(f17411,plain,
p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),bit1),s(num,u_0))))),s(num,sK3340_skl)))),
inference(backward_demodulation,[status(thm)],[f4176,f13909]) ).
fof(f17882,plain,
( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,sK3340_skl))),s(num,i(s(fun(fun(sK3339_skl,bool),num),dimindex),s(fun(sK3339_skl,bool),univ))))))
| p(s(bool,f0)) ),
inference(paramodulation,[status(thm)],[f3375,f13910]) ).
fof(f17883,plain,
( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),bit1),s(num,u_0))))),s(num,sK3340_skl))))
| p(s(bool,f0)) ),
inference(paramodulation,[status(thm)],[f3375,f17411]) ).
fof(f17946,definition,
( sQ198_spl
<=> p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,sK3340_skl))),s(num,i(s(fun(fun(sK3339_skl,bool),num),dimindex),s(fun(sK3339_skl,bool),univ)))))) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f17949,plain,
( sQ198_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f17882,f16443,f17946]) ).
fof(f17950,definition,
( sQ199_spl
<=> p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),bit1),s(num,u_0))))),s(num,sK3340_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f17953,plain,
( sQ199_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f17883,f16443,f17950]) ).
fof(f21229,plain,
! [X0,X1,X2,X3] :
( s(cart(real,X2),i(s(fun(cart(cart(real,X2),X1),cart(real,X2)),i(s(fun(num,fun(cart(cart(real,X2),X1),cart(real,X2))),row),s(num,X0))),s(cart(cart(real,X2),X1),i(s(fun(cart(cart(real,X1),X2),cart(cart(real,X2),X1)),transp),s(cart(cart(real,X1),X2),X3))))) = s(cart(real,X2),i(s(fun(cart(cart(real,X1),X2),cart(real,X2)),i(s(fun(num,fun(cart(cart(real,X1),X2),cart(real,X2))),column),s(num,X0))),s(cart(cart(real,X1),X2),X3)))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,X0))),s(num,i(s(fun(fun(X1,bool),num),dimindex),s(fun(X1,bool),univ))))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),bit1),s(num,u_0))))),s(num,X0)))) ),
inference(forward_demodulation,[status(thm)],[f4176,f13905]) ).
fof(f21235,plain,
( s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),i(s(fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(cart(real,sK3341_skl),sK3339_skl)),transp),s(cart(cart(real,sK3339_skl),sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(cart(real,sK3339_skl),sK3341_skl)),transp),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))))))) != s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl)))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,sK3340_skl))),s(num,i(s(fun(fun(sK3339_skl,bool),num),dimindex),s(fun(sK3339_skl,bool),univ))))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),bit1),s(num,u_0))))),s(num,sK3340_skl)))) ),
inference(resolution,[status(thm)],[f21229,f17345]) ).
fof(f21263,definition,
( sQ279_spl
<=> s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),i(s(fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(cart(real,sK3341_skl),sK3339_skl)),transp),s(cart(cart(real,sK3339_skl),sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(cart(real,sK3339_skl),sK3341_skl)),transp),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))))))) = s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f21265,plain,
( sQ279_spl
| s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),i(s(fun(cart(cart(real,sK3339_skl),sK3341_skl),cart(cart(real,sK3341_skl),sK3339_skl)),transp),s(cart(cart(real,sK3339_skl),sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(cart(real,sK3339_skl),sK3341_skl)),transp),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))))))) != s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))) ),
inference(component_clause,[status(thm)],[f21263]) ).
fof(f21266,plain,
( ~ sQ279_spl
| ~ sQ198_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f21235,f17950,f17946,f21263]) ).
fof(f21304,plain,
( sQ279_spl
| s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))) != s(cart(real,sK3341_skl),i(s(fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl)),i(s(fun(num,fun(cart(cart(real,sK3341_skl),sK3339_skl),cart(real,sK3341_skl))),row),s(num,sK3340_skl))),s(cart(cart(real,sK3341_skl),sK3339_skl),sK3342_skl))) ),
inference(forward_demodulation,[status(thm)],[f13898,f21265]) ).
fof(f21305,plain,
( sQ279_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21304]) ).
fof(f21306,plain,
sQ279_spl,
inference(contradiction_clause,[status(thm)],[f21305]) ).
fof(f21307,plain,
$false,
inference(sat_refutation,[status(thm)],[f16480,f16576,f17328,f17949,f17953,f21266,f21306]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO451+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n006.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sun Sep 20 16:21:51 UTC 2026
% 0.09/5.37 % CPUTime :
% 2.05/7.30 % Drodi V4.1.1
% 15.24/9.25 % Refutation found
% 15.24/9.25 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.24/9.25 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.18/9.45 % Elapsed time: 4.051489 seconds
% 7.18/9.45 % CPU time: 17.680926 seconds
% 7.18/9.45 % Total memory used: 1.641 GB
% 7.18/9.45 % Net memory used: 1.635 GB
%------------------------------------------------------------------------------