%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : ITP018+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:38:09 AM UTC 2026
% Result : Theorem 22.79s 4.13s
% Output : CNFRefutation 22.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 32 ( 8 unt; 0 def)
% Number of atoms : 79 ( 13 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 93 ( 46 ~; 31 |; 0 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-2 aty)
% Number of variables : 35 ( 0 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ne_ty_2Epair_2Eprod,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ne('ty$u2Epair$u2Eprod'(X0,X1)) ) ) ).
fof(mem_c_2Ebinary__ieee_2Efloat__plus__min,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> mem('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(X0,X1),arr('ty$u2Ebool$u2Eitself'('ty$u2Epair$u2Eprod'(X0,X1)),'ty$u2Ebinary$u$uieee$u2Efloat'(X0,X1))) ) ) ).
fof(mem_c_2Ebool_2Ethe__value,axiom,
! [X0] :
( ne(X0)
=> mem('c$u2Ebool$u2Ethe$u$uvalue'(X0),'ty$u2Ebool$u2Eitself'(X0)) ) ).
fof(conj_thm_2Ebinary__ieee_2Efloat__to__real__negate,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,'ty$u2Ebinary$u$uieee$u2Efloat'(X0,X1))
=> ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$unegate'(X0,X1),X2)) = ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),X2)) ) ) ) ).
fof(conj_thm_2Ebinary__ieee_2Eulp,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ap('c$u2Ebinary$u$uieee$u2Eulp'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1))) = ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1)))) ) ) ).
fof(ap_tp,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ) ).
fof(conj_thm_2Ebinary__ieee_2Eneg__ulp,conjecture,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1)))) = ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$unegate'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1))))) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1)))) = ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$unegate'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1))))) ) ),
inference(negate_conjecture,[status(cth)],[conj_thm_2Ebinary__ieee_2Eneg__ulp]) ).
cnf(c4,plain,
( ne('ty$u2Epair$u2Eprod'(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(clausification,[status(esa)],[ne_ty_2Epair_2Eprod]) ).
cnf(c6,plain,
( mem('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(X0,X1),arr('ty$u2Ebool$u2Eitself'('ty$u2Epair$u2Eprod'(X0,X1)),'ty$u2Ebinary$u$uieee$u2Efloat'(X0,X1)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(clausification,[status(esa)],[mem_c_2Ebinary__ieee_2Efloat__plus__min]) ).
cnf(c8,plain,
( mem('c$u2Ebool$u2Ethe$u$uvalue'(X0),'ty$u2Ebool$u2Eitself'(X0))
| ~ ne(X0) ),
inference(clausification,[status(esa)],[mem_c_2Ebool_2Ethe__value]) ).
cnf(c19,plain,
( ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$unegate'(X0,X1),X2)) = ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),X2))
| ~ mem(X2,'ty$u2Ebinary$u$uieee$u2Efloat'(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(clausification,[status(esa)],[conj_thm_2Ebinary__ieee_2Efloat__to__real__negate]) ).
cnf(c20,plain,
( ap('c$u2Ebinary$u$uieee$u2Eulp'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1))) = ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(X0,X1),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(X0,X1),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(X0,X1))))
| ~ ne(X1)
| ~ ne(X0) ),
inference(clausification,[status(esa)],[conj_thm_2Ebinary__ieee_2Eulp]) ).
cnf(c25,plain,
( mem(ap(X0,X3),X2)
| ~ mem(X3,X1)
| ~ mem(X0,arr(X1,X2)) ),
inference(clausification,[status(esa)],[ap_tp]) ).
cnf(c34,plain,
ne(sK48),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c35,plain,
ne(sK49),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c36,plain,
ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) != ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(sK48,sK49),ap('c$u2Ebinary$u$uieee$u2Efloat$u$unegate'(sK48,sK49),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(X1,X0),X2),'ty$u2Ebinary$u$uieee$u2Efloat'(X1,X0))
| ~ mem(X2,'ty$u2Ebool$u2Eitself'('ty$u2Epair$u2Eprod'(X1,X0)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(resolution,[status(thm)],[c6,c25]) ).
cnf(d1,plain,
( ~ mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))),'ty$u2Ebinary$u$uieee$u2Efloat'(sK48,sK49))
| ~ ne(sK49)
| ~ ne(sK48)
| ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) != ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(sK48,sK49),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))))) ),
inference(superposition,[status(thm)],[c19,c36]) ).
cnf(d2,plain,
( ~ mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))),'ty$u2Ebinary$u$uieee$u2Efloat'(sK48,sK49))
| ~ ne(sK49)
| ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) != ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(sK48,sK49),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))))) ),
inference(resolution,[status(thm)],[c34,d1]) ).
cnf(d3,plain,
( ~ mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))),'ty$u2Ebinary$u$uieee$u2Efloat'(sK48,sK49))
| ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) != ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Efloat$u$uto$u$ureal'(sK48,sK49),ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))))) ),
inference(resolution,[status(thm)],[c35,d2]) ).
cnf(d4,plain,
( ~ ne(sK48)
| ~ ne(sK49)
| ~ mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))),'ty$u2Ebinary$u$uieee$u2Efloat'(sK48,sK49))
| ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) != ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) ),
inference(superposition,[status(thm)],[c20,d3]) ).
cnf(d5,plain,
( ~ mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))),'ty$u2Ebinary$u$uieee$u2Efloat'(sK48,sK49))
| ~ ne(sK49)
| ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) != ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) ),
inference(resolution,[status(thm)],[c34,d4]) ).
cnf(d6,plain,
( ~ mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))),'ty$u2Ebinary$u$uieee$u2Efloat'(sK48,sK49))
| ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) != ap('c$u2Erealax$u2Ereal$u$uneg',ap('c$u2Ebinary$u$uieee$u2Eulp'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)))) ),
inference(resolution,[status(thm)],[c35,d5]) ).
cnf(d7,plain,
~ mem(ap('c$u2Ebinary$u$uieee$u2Efloat$u$uplus$u$umin'(sK48,sK49),'c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49))),'ty$u2Ebinary$u$uieee$u2Efloat'(sK48,sK49)),
inference(equality_resolution,[status(thm)],[d6]) ).
cnf(d8,plain,
( ~ mem('c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)),'ty$u2Ebool$u2Eitself'('ty$u2Epair$u2Eprod'(sK48,sK49)))
| ~ ne(sK49)
| ~ ne(sK48) ),
inference(resolution,[status(thm)],[d7,d0]) ).
cnf(d9,plain,
( ~ mem('c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)),'ty$u2Ebool$u2Eitself'('ty$u2Epair$u2Eprod'(sK48,sK49)))
| ~ ne(sK49) ),
inference(resolution,[status(thm)],[c34,d8]) ).
cnf(d10,plain,
~ mem('c$u2Ebool$u2Ethe$u$uvalue'('ty$u2Epair$u2Eprod'(sK48,sK49)),'ty$u2Ebool$u2Eitself'('ty$u2Epair$u2Eprod'(sK48,sK49))),
inference(resolution,[status(thm)],[c35,d9]) ).
cnf(d11,plain,
~ ne('ty$u2Epair$u2Eprod'(sK48,sK49)),
inference(resolution,[status(thm)],[d10,c8]) ).
cnf(d12,plain,
( ~ ne(sK49)
| ~ ne(sK48) ),
inference(resolution,[status(thm)],[d11,c4]) ).
cnf(d13,plain,
~ ne(sK49),
inference(resolution,[status(thm)],[c34,d12]) ).
cnf(d14,plain,
$false,
inference(resolution,[status(thm)],[c35,d13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP018+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n016.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 : Fri Sep 25 17:31:15 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.79/4.13 % SZS status Theorem for theBenchmark.p
% 22.79/4.13 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------