%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP018+2 : TPTP v9.0.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:52:09 PM UTC 2025
% Result : Theorem 4.86s 2.24s
% Output : CNFRefutation 5.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 7
% Syntax : Number of formulae : 30 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 66 ( 9 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 70 ( 34 ~; 22 |; 0 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-4 aty)
% Number of variables : 33 ( 33 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ mem > p > ne > ty_2Epair_2Eprod > ty_2Ebinary__ieee_2Efloat > k > c_2Ebinary__ieee_2Eulp > c_2Ebinary__ieee_2Efloat__to__real > c_2Ebinary__ieee_2Efloat__plus__min > c_2Ebinary__ieee_2Efloat__negate > arr > ap > #nlpp > ty_2Ebool_2Eitself > i > c_2Emin_2E_3D > c_2Ebool_2Ethe__value > c_2Ebool_2E_21 > ty_2Erealax_2Ereal > ind > c_2Erealax_2Ereal__neg > c_2Ebool_2ET > bool > #skF_3 > #skF_4 > #skF_2 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(arr,type,
arr: ( $i * $i ) > $i ).
tff(ne,type,
ne: $i > $o ).
tff(i,type,
i: $i > $i ).
tff(c_2Ebool_2E_21,type,
c_2Ebool_2E_21: $i > $i ).
tff(ty_2Epair_2Eprod,type,
ty_2Epair_2Eprod: ( $i * $i ) > $i ).
tff(bool,type,
bool: $i ).
tff(mem,type,
mem: ( $i * $i ) > $o ).
tff(ap,type,
ap: ( $i * $i ) > $i ).
tff(ty_2Ebool_2Eitself,type,
ty_2Ebool_2Eitself: $i > $i ).
tff(p,type,
p: $i > $o ).
tff(ind,type,
ind: $i ).
tff(c_2Erealax_2Ereal__neg,type,
c_2Erealax_2Ereal__neg: $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff(ty_2Ebinary__ieee_2Efloat,type,
ty_2Ebinary__ieee_2Efloat: ( $i * $i ) > $i ).
tff(c_2Ebinary__ieee_2Eulp,type,
c_2Ebinary__ieee_2Eulp: ( $i * $i ) > $i ).
tff(c_2Ebool_2ET,type,
c_2Ebool_2ET: $i ).
tff(k,type,
k: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(c_2Ebinary__ieee_2Efloat__negate,type,
c_2Ebinary__ieee_2Efloat__negate: ( $i * $i ) > $i ).
tff(c_2Ebinary__ieee_2Efloat__plus__min,type,
c_2Ebinary__ieee_2Efloat__plus__min: ( $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(c_2Ebinary__ieee_2Efloat__to__real,type,
c_2Ebinary__ieee_2Efloat__to__real: ( $i * $i ) > $i ).
tff(c_2Ebool_2Ethe__value,type,
c_2Ebool_2Ethe__value: $i > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i * $i ) > $i ).
tff(c_2Emin_2E_3D,type,
c_2Emin_2E_3D: $i > $i ).
tff(ty_2Erealax_2Ereal,type,
ty_2Erealax_2Ereal: $i ).
tff(f_220,negated_conjecture,
~ ! [A_27t] :
( ne(A_27t)
=> ! [A_27w] :
( ne(A_27w)
=> ( ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Eulp(A_27t,A_27w),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t,A_27w)))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t,A_27w),ap(c_2Ebinary__ieee_2Efloat__negate(A_27t,A_27w),ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t,A_27w),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t,A_27w))))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebinary__ieee_2Eneg__ulp) ).
tff(f_203,axiom,
! [A_27t] :
( ne(A_27t)
=> ! [A_27w] :
( ne(A_27w)
=> ( ap(c_2Ebinary__ieee_2Eulp(A_27t,A_27w),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t,A_27w))) = ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t,A_27w),ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t,A_27w),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t,A_27w)))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebinary__ieee_2Eulp) ).
tff(f_134,axiom,
! [A_27t] :
( ne(A_27t)
=> ! [A_27w] :
( ne(A_27w)
=> mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t,A_27w),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t,A_27w)),ty_2Ebinary__ieee_2Efloat(A_27t,A_27w))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebinary__ieee_2Efloat__plus__min) ).
tff(f_123,axiom,
! [A0] :
( ne(A0)
=> ! [A1] :
( ne(A1)
=> ne(ty_2Epair_2Eprod(A0,A1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Epair_2Eprod) ).
tff(f_145,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Ebool_2Ethe__value(A_27a),ty_2Ebool_2Eitself(A_27a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2Ethe__value) ).
tff(f_67,axiom,
! [A,B,F] :
( mem(F,arr(A,B))
=> ! [X] :
( mem(X,A)
=> mem(ap(F,X),B) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
tff(f_196,axiom,
! [A_27a] :
( ne(A_27a)
=> ! [A_27b] :
( ne(A_27b)
=> ! [V0x] :
( mem(V0x,ty_2Ebinary__ieee_2Efloat(A_27a,A_27b))
=> ( ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a,A_27b),ap(c_2Ebinary__ieee_2Efloat__negate(A_27a,A_27b),V0x)) = ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a,A_27b),V0x)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebinary__ieee_2Efloat__to__real__negate) ).
tff(c_77,plain,
ne('#skF_3'),
inference(cnfTransformation,[status(thm)],[f_220]) ).
tff(c_75,plain,
ne('#skF_4'),
inference(cnfTransformation,[status(thm)],[f_220]) ).
tff(c_66,plain,
! [A_27t_71,A_27w_73] :
( ( ap(c_2Ebinary__ieee_2Efloat__to__real(A_27t_71,A_27w_73),ap(c_2Ebinary__ieee_2Efloat__plus__min(A_27t_71,A_27w_73),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t_71,A_27w_73)))) = ap(c_2Ebinary__ieee_2Eulp(A_27t_71,A_27w_73),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod(A_27t_71,A_27w_73))) )
| ~ ne(A_27w_73)
| ~ ne(A_27t_71) ),
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_38,plain,
! [A_27t_35,A_27w_37] :
( mem(c_2Ebinary__ieee_2Efloat__plus__min(A_27t_35,A_27w_37),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod(A_27t_35,A_27w_37)),ty_2Ebinary__ieee_2Efloat(A_27t_35,A_27w_37)))
| ~ ne(A_27w_37)
| ~ ne(A_27t_35) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_34,plain,
! [A0_31,A1_33] :
( ne(ty_2Epair_2Eprod(A0_31,A1_33))
| ~ ne(A1_33)
| ~ ne(A0_31) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_42,plain,
! [A_27a_41] :
( mem(c_2Ebool_2Ethe__value(A_27a_41),ty_2Ebool_2Eitself(A_27a_41))
| ~ ne(A_27a_41) ),
inference(cnfTransformation,[status(thm)],[f_145]) ).
tff(c_123,plain,
! [F_100,X_101,B_102,A_103] :
( mem(ap(F_100,X_101),B_102)
| ~ mem(X_101,A_103)
| ~ mem(F_100,arr(A_103,B_102)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_136,plain,
! [F_100,A_27a_41,B_102] :
( mem(ap(F_100,c_2Ebool_2Ethe__value(A_27a_41)),B_102)
| ~ mem(F_100,arr(ty_2Ebool_2Eitself(A_27a_41),B_102))
| ~ ne(A_27a_41) ),
inference(resolution,[status(thm)],[c_42,c_123]) ).
tff(c_836,plain,
! [A_27a_181,A_27b_182,V0x_183] :
( ( ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a_181,A_27b_182),ap(c_2Ebinary__ieee_2Efloat__negate(A_27a_181,A_27b_182),V0x_183)) = ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Efloat__to__real(A_27a_181,A_27b_182),V0x_183)) )
| ~ mem(V0x_183,ty_2Ebinary__ieee_2Efloat(A_27a_181,A_27b_182))
| ~ ne(A_27b_182)
| ~ ne(A_27a_181) ),
inference(cnfTransformation,[status(thm)],[f_196]) ).
tff(c_73,plain,
ap(c_2Ebinary__ieee_2Efloat__to__real('#skF_3','#skF_4'),ap(c_2Ebinary__ieee_2Efloat__negate('#skF_3','#skF_4'),ap(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4'))))) != ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Eulp('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4')))),
inference(cnfTransformation,[status(thm)],[f_220]) ).
tff(c_842,plain,
( ( ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Efloat__to__real('#skF_3','#skF_4'),ap(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4'))))) != ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Eulp('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4')))) )
| ~ mem(ap(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4'))),ty_2Ebinary__ieee_2Efloat('#skF_3','#skF_4'))
| ~ ne('#skF_4')
| ~ ne('#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_836,c_73]) ).
tff(c_848,plain,
( ( ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Efloat__to__real('#skF_3','#skF_4'),ap(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4'))))) != ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Eulp('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4')))) )
| ~ mem(ap(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4'))),ty_2Ebinary__ieee_2Efloat('#skF_3','#skF_4')) ),
inference(demodulation,[status(thm),theory(equality)],[c_77,c_75,c_842]) ).
tff(c_878,plain,
~ mem(ap(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4'))),ty_2Ebinary__ieee_2Efloat('#skF_3','#skF_4')),
inference(splitLeft,[status(thm)],[c_848]) ).
tff(c_883,plain,
( ~ mem(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod('#skF_3','#skF_4')),ty_2Ebinary__ieee_2Efloat('#skF_3','#skF_4')))
| ~ ne(ty_2Epair_2Eprod('#skF_3','#skF_4')) ),
inference(resolution,[status(thm)],[c_136,c_878]) ).
tff(c_884,plain,
~ ne(ty_2Epair_2Eprod('#skF_3','#skF_4')),
inference(splitLeft,[status(thm)],[c_883]) ).
tff(c_887,plain,
( ~ ne('#skF_4')
| ~ ne('#skF_3') ),
inference(resolution,[status(thm)],[c_34,c_884]) ).
tff(c_891,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_77,c_75,c_887]) ).
tff(c_892,plain,
~ mem(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),arr(ty_2Ebool_2Eitself(ty_2Epair_2Eprod('#skF_3','#skF_4')),ty_2Ebinary__ieee_2Efloat('#skF_3','#skF_4'))),
inference(splitRight,[status(thm)],[c_883]) ).
tff(c_913,plain,
( ~ ne('#skF_4')
| ~ ne('#skF_3') ),
inference(resolution,[status(thm)],[c_38,c_892]) ).
tff(c_917,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_77,c_75,c_913]) ).
tff(c_918,plain,
ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Efloat__to__real('#skF_3','#skF_4'),ap(c_2Ebinary__ieee_2Efloat__plus__min('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4'))))) != ap(c_2Erealax_2Ereal__neg,ap(c_2Ebinary__ieee_2Eulp('#skF_3','#skF_4'),c_2Ebool_2Ethe__value(ty_2Epair_2Eprod('#skF_3','#skF_4')))),
inference(splitRight,[status(thm)],[c_848]) ).
tff(c_929,plain,
( ~ ne('#skF_4')
| ~ ne('#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_918]) ).
tff(c_933,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_77,c_75,c_929]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ITP018+2 : TPTP v9.0.0. Bugfixed v7.5.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 00:53:18 EDT 2025
% 0.13/0.34 % CPUTime :
% 4.86/2.24 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.27/2.24
% 5.27/2.24 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------