%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ITP021+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:50:20 PM UTC 2026
% Result : Theorem 62.44s 44.28s
% Output : CNFRefutation 41.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 10
% Syntax : Number of formulae : 105 ( 15 unt; 0 def)
% Number of atoms : 372 ( 39 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 455 ( 188 ~; 213 |; 23 &)
% ( 6 <=>; 24 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 103 ( 97 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B,F] :
( mem(F,arr(A,B))
=> ! [X] :
( mem(X,A)
=> mem(ap(F,X),B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18639,axiom,
mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18725,axiom,
! [V0x] :
( mem(V0x,ty_2Eextreal_2Eextreal)
=> p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V0x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18731,axiom,
! [V0x] :
( mem(V0x,ty_2Eextreal_2Eextreal)
=> ! [V1y] :
( mem(V1y,ty_2Eextreal_2Eextreal)
=> ! [V2z] :
( mem(V2z,ty_2Eextreal_2Eextreal)
=> ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) )
=> p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V2z)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18734,axiom,
! [V0x] :
( mem(V0x,ty_2Eextreal_2Eextreal)
=> ! [V1y] :
( mem(V1y,ty_2Eextreal_2Eextreal)
=> ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) )
<=> V0x = V1y ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18737,axiom,
! [V0x] :
( mem(V0x,ty_2Eextreal_2Eextreal)
=> ! [V1y] :
( mem(V1y,ty_2Eextreal_2Eextreal)
=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x))
| p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19036,axiom,
! [V0z] :
( mem(V0z,ty_2Eextreal_2Eextreal)
=> ! [V1x] :
( mem(V1x,ty_2Eextreal_2Eextreal)
=> ! [V2y] :
( mem(V2y,ty_2Eextreal_2Eextreal)
=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y)))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V2y))
| p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V1x)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19037,axiom,
! [V0x] :
( mem(V0x,ty_2Eextreal_2Eextreal)
=> ! [V1y] :
( mem(V1y,ty_2Eextreal_2Eextreal)
=> p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),ap(ap(c_2Eextreal_2Eextreal__max,V0x),V1y))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19038,axiom,
! [V0x] :
( mem(V0x,ty_2Eextreal_2Eextreal)
=> ! [V1y] :
( mem(V1y,ty_2Eextreal_2Eextreal)
=> p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__max,V0x),V1y))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19039,conjecture,
! [V0z] :
( mem(V0z,ty_2Eextreal_2Eextreal)
=> ! [V1x] :
( mem(V1x,ty_2Eextreal_2Eextreal)
=> ! [V2y] :
( mem(V2y,ty_2Eextreal_2Eextreal)
=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y)),V0z))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V2y),V0z))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),V0z)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19040,negated_conjecture,
~ ! [V0z] :
( mem(V0z,ty_2Eextreal_2Eextreal)
=> ! [V1x] :
( mem(V1x,ty_2Eextreal_2Eextreal)
=> ! [V2y] :
( mem(V2y,ty_2Eextreal_2Eextreal)
=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y)),V0z))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V2y),V0z))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),V0z)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f19039]) ).
fof(f19045,plain,
! [A,B,F] :
( ! [X] :
( mem(ap(F,X),B)
| ~ mem(X,A) )
| ~ mem(F,arr(A,B)) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f19046,plain,
! [X0,X1,X2,X3] :
( mem(ap(X0,X3),X2)
| ~ mem(X3,X1)
| ~ mem(X0,arr(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f19045]) ).
fof(f95845,plain,
mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))),
inference(cnf_transformation,[status(thm)],[f18639]) ).
fof(f96134,plain,
! [V0x] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V0x))
| ~ mem(V0x,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f18725]) ).
fof(f96135,plain,
! [X0] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[status(thm)],[f96134]) ).
fof(f96161,plain,
! [V0x] :
( ! [V1y] :
( ! [V2z] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V2z))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y))
| ~ mem(V2z,ty_2Eextreal_2Eextreal) )
| ~ mem(V1y,ty_2Eextreal_2Eextreal) )
| ~ mem(V0x,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f18731]) ).
fof(f96162,plain,
! [X0,X1,X2] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X2))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X2))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ~ mem(X2,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[status(thm)],[f96161]) ).
fof(f96167,plain,
! [V0x] :
( ! [V1y] :
( ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) )
<=> V0x = V1y )
| ~ mem(V1y,ty_2Eextreal_2Eextreal) )
| ~ mem(V0x,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f18734]) ).
fof(f96168,plain,
! [V0x] :
( ! [V1y] :
( ( ( V0x != V1y
| ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) )
& ( V0x = V1y
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) )
| ~ mem(V1y,ty_2Eextreal_2Eextreal) )
| ~ mem(V0x,ty_2Eextreal_2Eextreal) ),
inference(NNF_transformation,[status(thm)],[f96167]) ).
fof(f96169,plain,
! [X0,X1] :
( X0 = X1
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[status(thm)],[f96168]) ).
fof(f96176,plain,
! [V0x] :
( ! [V1y] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x))
| p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y))
| ~ mem(V1y,ty_2Eextreal_2Eextreal) )
| ~ mem(V0x,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f18737]) ).
fof(f96177,plain,
! [X0,X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[status(thm)],[f96176]) ).
fof(f97118,plain,
! [V0z] :
( ! [V1x] :
( ! [V2y] :
( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y)))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V2y))
| p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V1x)) ) )
| ~ mem(V2y,ty_2Eextreal_2Eextreal) )
| ~ mem(V1x,ty_2Eextreal_2Eextreal) )
| ~ mem(V0z,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f19036]) ).
fof(f97119,plain,
! [V0z] :
( ! [V1x] :
( ! [V2y] :
( ( ( ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V2y))
& ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V1x)) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y))) )
& ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V2y))
| p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),V1x))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V0z),ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y))) ) )
| ~ mem(V2y,ty_2Eextreal_2Eextreal) )
| ~ mem(V1x,ty_2Eextreal_2Eextreal) )
| ~ mem(V0z,ty_2Eextreal_2Eextreal) ),
inference(NNF_transformation,[status(thm)],[f97118]) ).
fof(f97120,plain,
! [X0,X1,X2] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X2))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)))
| ~ mem(X2,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[status(thm)],[f97119]) ).
fof(f97123,plain,
! [V0x] :
( ! [V1y] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),ap(ap(c_2Eextreal_2Eextreal__max,V0x),V1y)))
| ~ mem(V1y,ty_2Eextreal_2Eextreal) )
| ~ mem(V0x,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f19037]) ).
fof(f97124,plain,
! [X0,X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[status(thm)],[f97123]) ).
fof(f97125,plain,
! [V0x] :
( ! [V1y] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__max,V0x),V1y)))
| ~ mem(V1y,ty_2Eextreal_2Eextreal) )
| ~ mem(V0x,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f19038]) ).
fof(f97126,plain,
! [X0,X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[status(thm)],[f97125]) ).
fof(f97127,plain,
? [V0z] :
( ? [V1x] :
( ? [V2y] :
( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y)),V0z))
<~> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V2y),V0z))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),V0z)) ) )
& mem(V2y,ty_2Eextreal_2Eextreal) )
& mem(V1x,ty_2Eextreal_2Eextreal) )
& mem(V0z,ty_2Eextreal_2Eextreal) ),
inference(pre_NNF_transformation,[status(thm)],[f19040]) ).
fof(f97128,plain,
? [V0z] :
( ? [V1x] :
( ? [V2y] :
( ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V2y),V0z))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),V0z))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y)),V0z)) )
& ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V2y),V0z))
& p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),V0z)) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,V1x),V2y)),V0z)) )
& mem(V2y,ty_2Eextreal_2Eextreal) )
& mem(V1x,ty_2Eextreal_2Eextreal) )
& mem(V0z,ty_2Eextreal_2Eextreal) ),
inference(NNF_transformation,[status(thm)],[f97127]) ).
fof(f97129,plain,
( ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16595_skl)) )
& ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
& p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl)) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16595_skl)) )
& mem(sK16597_skl,ty_2Eextreal_2Eextreal)
& mem(sK16596_skl,ty_2Eextreal_2Eextreal)
& mem(sK16595_skl,ty_2Eextreal_2Eextreal) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16595_skl,sK16596_skl,sK16597_skl]),skolemize(V0z,sK16595_skl),skolemize(V1x,sK16596_skl),skolemize(V2y,sK16597_skl)],[f97128]) ).
fof(f97130,plain,
mem(sK16595_skl,ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[status(thm)],[f97129]) ).
fof(f97131,plain,
mem(sK16596_skl,ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[status(thm)],[f97129]) ).
fof(f97132,plain,
mem(sK16597_skl,ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[status(thm)],[f97129]) ).
fof(f97133,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16595_skl)) ),
inference(cnf_transformation,[status(thm)],[f97129]) ).
fof(f97134,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16595_skl)) ),
inference(cnf_transformation,[status(thm)],[f97129]) ).
fof(f97135,plain,
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16595_skl)) ),
inference(cnf_transformation,[status(thm)],[f97129]) ).
fof(f110378,plain,
! [X0] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)))
| ~ mem(sK16595_skl,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f96162,f97134]) ).
fof(f110379,plain,
! [X0] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)))
| ~ mem(sK16595_skl,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f96162,f97133]) ).
fof(f110382,plain,
! [X0] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110378,f97130]) ).
fof(f110383,plain,
! [X0] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110379,f97130]) ).
fof(f110387,plain,
! [X0,X1] :
( ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X0
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f96169,f97124]) ).
fof(f110391,plain,
! [X0,X1] :
( ~ mem(X1,ty_2Eextreal_2Eextreal)
| ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X0
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal) ),
inference(duplicate_literals_removal,[status(thm)],[f110387]) ).
fof(f110392,plain,
! [X0] :
( mem(ap(c_2Eextreal_2Eextreal__max,X0),arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f19046,f95845]) ).
fof(f110401,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110383,f97124]) ).
fof(f110403,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(duplicate_literals_removal,[status(thm)],[f110401]) ).
fof(f110404,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110403,f97131]) ).
fof(f110406,plain,
! [X0,X1] :
( mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110392,f19046]) ).
fof(f110410,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f97126,f110382]) ).
fof(f110411,plain,
! [X0,X1] :
( ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X1
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X1))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f97126,f96169]) ).
fof(f110415,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(duplicate_literals_removal,[status(thm)],[f110410]) ).
fof(f110416,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110415,f97131]) ).
fof(f110417,plain,
! [X0,X1] :
( ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X1
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X1))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(duplicate_literals_removal,[status(thm)],[f110411]) ).
fof(f110418,plain,
! [X0,X1] :
( ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X1
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X1))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110417,f110406]) ).
fof(f110434,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110404,f97132]) ).
fof(f110435,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl)) ),
inference(resolution,[status(thm)],[f110434,f110406]) ).
fof(f110436,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f110435,f97131]) ).
fof(f110437,plain,
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16595_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f97135,f110438]) ).
fof(f110438,plain,
p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16595_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f110436,f97132]) ).
fof(f110439,plain,
( sK16595_skl = sK16596_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16596_skl))
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16595_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110438,f96169]) ).
fof(f110441,plain,
( sK16595_skl = sK16596_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16596_skl))
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110439,f97130]) ).
fof(f110446,plain,
! [X0,X1] :
( ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X1))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f97120,f96135]) ).
fof(f110451,plain,
! [X0,X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X1))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal) ),
inference(duplicate_literals_removal,[status(thm)],[f110446]) ).
fof(f110452,plain,
! [X0,X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X1))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110451,f110406]) ).
fof(f110458,plain,
( sK16595_skl = sK16596_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16596_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f110441,f97131]) ).
fof(f110460,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110416,f97132]) ).
fof(f110461,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl)) ),
inference(resolution,[status(thm)],[f110460,f110406]) ).
fof(f110462,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f110461,f97131]) ).
fof(f110463,plain,
p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16595_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f110462,f97132]) ).
fof(f110464,plain,
( sK16595_skl = sK16597_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16595_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110463,f96169]) ).
fof(f110466,plain,
( sK16595_skl = sK16597_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110464,f97130]) ).
fof(f110468,plain,
( sK16595_skl = sK16597_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f110466,f97132]) ).
fof(f110470,plain,
~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16595_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f110437,f110463]) ).
fof(f110471,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal)
| ~ mem(sK16595_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110470,f96177]) ).
fof(f110472,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)))
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110471,f97130]) ).
fof(f110505,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16596_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16595_skl,ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl),ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110472,f97120]) ).
fof(f110508,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16596_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16595_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110505,f110406]) ).
fof(f110588,plain,
! [X0,X1] :
( ~ mem(X1,ty_2Eextreal_2Eextreal)
| ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X0
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110391,f110406]) ).
fof(f110597,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl))
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16596_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110508,f97130]) ).
fof(f110598,plain,
( sK16595_skl = sK16596_skl
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110597,f110458]) ).
fof(f110604,plain,
( sK16595_skl = sK16596_skl
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110598,f97131]) ).
fof(f110611,plain,
( sK16595_skl = sK16596_skl
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16595_skl),sK16597_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f110604,f97132]) ).
fof(f110612,plain,
( sK16595_skl = sK16597_skl
| sK16595_skl = sK16596_skl ),
inference(resolution,[status(thm)],[f110611,f110468]) ).
fof(f110627,plain,
( sK16595_skl = sK16597_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16596_skl)) ),
inference(paramodulation,[status(thm)],[f110612,f110470]) ).
fof(f110629,plain,
( sK16595_skl = sK16597_skl
| p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16596_skl)) ),
inference(paramodulation,[status(thm)],[f110612,f110463]) ).
fof(f110838,plain,
! [X0,X1] :
( ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X1
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110452,f110418]) ).
fof(f110851,plain,
! [X0,X1] :
( ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = X1
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X0),X1)),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(duplicate_literals_removal,[status(thm)],[f110838]) ).
fof(f110965,plain,
( sK16595_skl = sK16597_skl
| ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl) = sK16597_skl
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f110851,f110627]) ).
fof(f110981,plain,
( sK16595_skl = sK16597_skl
| ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl) = sK16597_skl
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f110965,f97131]) ).
fof(f111002,plain,
( sK16595_skl = sK16597_skl
| ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl) = sK16597_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f110981,f97132]) ).
fof(f111004,plain,
( sK16595_skl = sK16597_skl
| sK16595_skl = sK16597_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16596_skl)) ),
inference(paramodulation,[status(thm)],[f111002,f110627]) ).
fof(f111024,plain,
( sK16595_skl = sK16597_skl
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16597_skl),sK16596_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f111004]) ).
fof(f111025,plain,
sK16595_skl = sK16597_skl,
inference(forward_subsumption_resolution,[status(thm)],[f111024,f110629]) ).
fof(f111067,plain,
~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16597_skl)),
inference(backward_demodulation,[status(thm)],[f111025,f110470]) ).
fof(f111071,plain,
p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16597_skl)),
inference(backward_demodulation,[status(thm)],[f111025,f110438]) ).
fof(f111079,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16596_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f111067,f110452]) ).
fof(f111082,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16596_skl))
| ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f111079,f97131]) ).
fof(f111194,plain,
p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl)),sK16596_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f111082,f97132]) ).
fof(f111197,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl) = sK16596_skl
| ~ mem(sK16596_skl,ty_2Eextreal_2Eextreal) ),
inference(resolution,[status(thm)],[f111194,f110588]) ).
fof(f111206,plain,
( ~ mem(sK16597_skl,ty_2Eextreal_2Eextreal)
| ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl) = sK16596_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f111197,f97131]) ).
fof(f111213,plain,
~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK16596_skl),sK16597_skl)),
inference(backward_demodulation,[status(thm)],[f111214,f111067]) ).
fof(f111214,plain,
ap(ap(c_2Eextreal_2Eextreal__max,sK16596_skl),sK16597_skl) = sK16596_skl,
inference(forward_subsumption_resolution,[status(thm)],[f111206,f97132]) ).
fof(f111234,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f111213,f111071]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP021+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 21:58:32 UTC 2026
% 0.12/0.36 % CPUTime :
% 41.06/41.36 % Drodi V4.1.1
% 62.44/44.28 % Refutation found
% 62.44/44.28 % SZS status Theorem for theBenchmark: Theorem is valid
% 62.44/44.28 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 41.95/44.94 % Elapsed time: 44.477923 seconds
% 41.95/44.94 % CPU time: 64.696681 seconds
% 41.95/44.94 % Total memory used: 5.262 GB
% 41.95/44.94 % Net memory used: 5.212 GB
%------------------------------------------------------------------------------