%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP012+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 : n007.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:02 PM UTC 2025
% Result : Theorem 182.39s 119.40s
% Output : CNFRefutation 182.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 17
% Syntax : Number of formulae : 140 ( 49 unt; 0 typ; 0 def)
% Number of atoms : 359 ( 48 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 401 ( 182 ~; 189 |; 1 &)
% ( 7 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 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 : 31 ( 31 usr; 16 con; 0-4 aty)
% Number of variables : 121 ( 121 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ mem > p > ne > k > arr > ap > #nlpp > i > c_2Emin_2E_3D > c_2Ebool_2E_3F > c_2Ebool_2E_21 > ty_2Einteger_2Eint > ind > c_2Emin_2E_3D_3D_3E > c_2Einteger_2Eint__sub > c_2Einteger_2Eint__neg > c_2Einteger_2Eint__divides > c_2Einteger_2Eint__add > c_2Ebool_2E_7E > c_2Ebool_2E_5C_2F > c_2Ebool_2E_2F_5C > c_2Ebool_2ET > c_2Ebool_2EF > bool > #skF_11 > #skF_6 > #skF_3 > #skF_10 > #skF_9 > #skF_7 > #skF_2 > #skF_8 > #skF_1 > #skF_5 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(arr,type,
arr: ( $i * $i ) > $i ).
tff(ne,type,
ne: $i > $o ).
tff(c_2Ebool_2EF,type,
c_2Ebool_2EF: $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i ) > $i ).
tff(i,type,
i: $i > $i ).
tff(c_2Ebool_2E_21,type,
c_2Ebool_2E_21: $i > $i ).
tff(bool,type,
bool: $i ).
tff(mem,type,
mem: ( $i * $i ) > $o ).
tff(ap,type,
ap: ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(p,type,
p: $i > $o ).
tff(ind,type,
ind: $i ).
tff(c_2Ebool_2E_3F,type,
c_2Ebool_2E_3F: $i > $i ).
tff(c_2Emin_2E_3D_3D_3E,type,
c_2Emin_2E_3D_3D_3E: $i ).
tff(c_2Einteger_2Eint__add,type,
c_2Einteger_2Eint__add: $i ).
tff(c_2Einteger_2Eint__divides,type,
c_2Einteger_2Eint__divides: $i ).
tff(c_2Ebool_2E_5C_2F,type,
c_2Ebool_2E_5C_2F: $i ).
tff('#skF_9',type,
'#skF_9': $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i ) > $i ).
tff(c_2Ebool_2E_7E,type,
c_2Ebool_2E_7E: $i ).
tff(c_2Ebool_2ET,type,
c_2Ebool_2ET: $i ).
tff(k,type,
k: ( $i * $i ) > $i ).
tff(ty_2Einteger_2Eint,type,
ty_2Einteger_2Eint: $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(c_2Einteger_2Eint__sub,type,
c_2Einteger_2Eint__sub: $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $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(c_2Ebool_2E_2F_5C,type,
c_2Ebool_2E_2F_5C: $i ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff(c_2Einteger_2Eint__neg,type,
c_2Einteger_2Eint__neg: $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(f_672,negated_conjecture,
~ ! [V0p] :
( mem(V0p,ty_2Einteger_2Eint)
=> ! [V1q] :
( mem(V1q,ty_2Einteger_2Eint)
=> ! [V2r] :
( mem(V2r,ty_2Einteger_2Eint)
=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))
=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__sub,V2r),V1q)))
<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__DIVIDES__RSUB) ).
tff(f_102,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_true_p) ).
tff(f_123,axiom,
mem(c_2Einteger_2Eint__divides,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__divides) ).
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_101,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
tff(f_78,axiom,
! [Q] :
( mem(Q,bool)
=> ! [R] :
( mem(R,bool)
=> ( ( p(Q)
<=> p(R) )
=> ( Q = R ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',boolext) ).
tff(f_437,axiom,
! [V0p] :
( mem(V0p,ty_2Einteger_2Eint)
=> ! [V1q] :
( mem(V1q,ty_2Einteger_2Eint)
=> ( ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(c_2Einteger_2Eint__neg,V1q)))
<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)) )
& ( p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,V0p)),V1q))
<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__DIVIDES__NEG) ).
tff(f_122,axiom,
mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__neg) ).
tff(f_126,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
tff(f_52,axiom,
ne(bool),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',bool_ne) ).
tff(f_163,axiom,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2E_7E) ).
tff(f_124,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
tff(f_170,axiom,
! [Q] :
( mem(Q,bool)
=> ( p(ap(c_2Ebool_2E_7E,Q))
<=> ~ p(Q) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_neg_p) ).
tff(f_174,axiom,
! [A_27a] :
( ne(A_27a)
=> mem(c_2Emin_2E_3D(A_27a),arr(A_27a,arr(A_27a,bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D) ).
tff(f_202,axiom,
! [A] :
( ne(A)
=> ! [Q] :
( mem(Q,arr(A,bool))
=> ( p(ap(c_2Ebool_2E_21(A),Q))
<=> ! [X] :
( mem(X,A)
=> p(ap(Q,X)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_all_p) ).
tff(f_410,axiom,
! [V0x] :
( mem(V0x,ty_2Einteger_2Eint)
=> ! [V1y] :
( mem(V1y,ty_2Einteger_2Eint)
=> ( ap(ap(c_2Einteger_2Eint__sub,V0x),V1y) = ap(ap(c_2Einteger_2Eint__add,V0x),ap(c_2Einteger_2Eint__neg,V1y)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Einteger_2Eint__sub) ).
tff(f_424,axiom,
! [V0p] :
( mem(V0p,ty_2Einteger_2Eint)
=> ! [V1q] :
( mem(V1q,ty_2Einteger_2Eint)
=> ! [V2r] :
( mem(V2r,ty_2Einteger_2Eint)
=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))
=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__add,V2r),V1q)))
<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__DIVIDES__RADD) ).
tff(c_1666,plain,
mem('#skF_9',ty_2Einteger_2Eint),
inference(cnfTransformation,[status(thm)],[f_672]) ).
tff(c_1664,plain,
mem('#skF_10',ty_2Einteger_2Eint),
inference(cnfTransformation,[status(thm)],[f_672]) ).
tff(c_28,plain,
p(c_2Ebool_2ET),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_1660,plain,
p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10')),
inference(cnfTransformation,[status(thm)],[f_672]) ).
tff(c_46,plain,
mem(c_2Einteger_2Eint__divides,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_293765,plain,
! [F_3159,X_3160,B_3161,A_3162] :
( mem(ap(F_3159,X_3160),B_3161)
| ~ mem(X_3160,A_3162)
| ~ mem(F_3159,arr(A_3162,B_3161)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_293812,plain,
! [F_3159,B_3161] :
( mem(ap(F_3159,'#skF_9'),B_3161)
| ~ mem(F_3159,arr(ty_2Einteger_2Eint,B_3161)) ),
inference(resolution,[status(thm)],[c_1666,c_293765]) ).
tff(c_293874,plain,
! [F_3167,B_3168] :
( mem(ap(F_3167,'#skF_10'),B_3168)
| ~ mem(F_3167,arr(ty_2Einteger_2Eint,B_3168)) ),
inference(resolution,[status(thm)],[c_1664,c_293765]) ).
tff(c_26,plain,
mem(c_2Ebool_2ET,bool),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_293744,plain,
! [R_3156,Q_3157] :
( ~ p(R_3156)
| ~ p(Q_3157)
| ( R_3156 = Q_3157 )
| ~ mem(R_3156,bool)
| ~ mem(Q_3157,bool) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_293746,plain,
! [Q_3157] :
( ~ p(c_2Ebool_2ET)
| ~ p(Q_3157)
| ( c_2Ebool_2ET = Q_3157 )
| ~ mem(Q_3157,bool) ),
inference(resolution,[status(thm)],[c_26,c_293744]) ).
tff(c_293751,plain,
! [Q_3157] :
( ~ p(Q_3157)
| ( c_2Ebool_2ET = Q_3157 )
| ~ mem(Q_3157,bool) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_293746]) ).
tff(c_297970,plain,
! [F_3419] :
( ~ p(ap(F_3419,'#skF_10'))
| ( ap(F_3419,'#skF_10') = c_2Ebool_2ET )
| ~ mem(F_3419,arr(ty_2Einteger_2Eint,bool)) ),
inference(resolution,[status(thm)],[c_293874,c_293751]) ).
tff(c_411856,plain,
! [F_5059] :
( ~ p(ap(ap(F_5059,'#skF_9'),'#skF_10'))
| ( ap(ap(F_5059,'#skF_9'),'#skF_10') = c_2Ebool_2ET )
| ~ mem(F_5059,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))) ),
inference(resolution,[status(thm)],[c_293812,c_297970]) ).
tff(c_411943,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10'))
| ( ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10') = c_2Ebool_2ET ) ),
inference(resolution,[status(thm)],[c_46,c_411856]) ).
tff(c_411970,plain,
ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10') = c_2Ebool_2ET,
inference(demodulation,[status(thm),theory(equality)],[c_1660,c_411943]) ).
tff(c_194,plain,
! [V0p_165,V1q_167] :
( p(ap(ap(c_2Einteger_2Eint__divides,V0p_165),ap(c_2Einteger_2Eint__neg,V1q_167)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_165),V1q_167))
| ~ mem(V1q_167,ty_2Einteger_2Eint)
| ~ mem(V0p_165,ty_2Einteger_2Eint) ),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_44,plain,
mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_293813,plain,
! [F_3159,B_3161] :
( mem(ap(F_3159,'#skF_10'),B_3161)
| ~ mem(F_3159,arr(ty_2Einteger_2Eint,B_3161)) ),
inference(resolution,[status(thm)],[c_1664,c_293765]) ).
tff(c_50,plain,
~ p(c_2Ebool_2EF),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_1662,plain,
mem('#skF_11',ty_2Einteger_2Eint),
inference(cnfTransformation,[status(thm)],[f_672]) ).
tff(c_1751,plain,
! [F_232,X_233,B_234,A_235] :
( mem(ap(F_232,X_233),B_234)
| ~ mem(X_233,A_235)
| ~ mem(F_232,arr(A_235,B_234)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_1798,plain,
! [F_232,B_234] :
( mem(ap(F_232,'#skF_9'),B_234)
| ~ mem(F_232,arr(ty_2Einteger_2Eint,B_234)) ),
inference(resolution,[status(thm)],[c_1666,c_1751]) ).
tff(c_2,plain,
ne(bool),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_76,plain,
mem(c_2Ebool_2E_7E,arr(bool,bool)),
inference(cnfTransformation,[status(thm)],[f_163]) ).
tff(c_48,plain,
mem(c_2Ebool_2EF,bool),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_78,plain,
! [Q_45] :
( p(ap(c_2Ebool_2E_7E,Q_45))
| p(Q_45)
| ~ mem(Q_45,bool) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_1860,plain,
! [F_240,B_241] :
( mem(ap(F_240,c_2Ebool_2EF),B_241)
| ~ mem(F_240,arr(bool,B_241)) ),
inference(resolution,[status(thm)],[c_48,c_1751]) ).
tff(c_1706,plain,
! [R_224,Q_225] :
( ~ p(R_224)
| ~ p(Q_225)
| ( R_224 = Q_225 )
| ~ mem(R_224,bool)
| ~ mem(Q_225,bool) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_1708,plain,
! [Q_225] :
( ~ p(c_2Ebool_2ET)
| ~ p(Q_225)
| ( c_2Ebool_2ET = Q_225 )
| ~ mem(Q_225,bool) ),
inference(resolution,[status(thm)],[c_26,c_1706]) ).
tff(c_1713,plain,
! [Q_225] :
( ~ p(Q_225)
| ( c_2Ebool_2ET = Q_225 )
| ~ mem(Q_225,bool) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_1708]) ).
tff(c_5359,plain,
! [F_478] :
( ~ p(ap(F_478,c_2Ebool_2EF))
| ( ap(F_478,c_2Ebool_2EF) = c_2Ebool_2ET )
| ~ mem(F_478,arr(bool,bool)) ),
inference(resolution,[status(thm)],[c_1860,c_1713]) ).
tff(c_5388,plain,
( ~ p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))
| ( ap(c_2Ebool_2E_7E,c_2Ebool_2EF) = c_2Ebool_2ET ) ),
inference(resolution,[status(thm)],[c_76,c_5359]) ).
tff(c_5389,plain,
~ p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF)),
inference(splitLeft,[status(thm)],[c_5388]) ).
tff(c_5392,plain,
( p(c_2Ebool_2EF)
| ~ mem(c_2Ebool_2EF,bool) ),
inference(resolution,[status(thm)],[c_78,c_5389]) ).
tff(c_5395,plain,
p(c_2Ebool_2EF),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_5392]) ).
tff(c_5397,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_50,c_5395]) ).
tff(c_5398,plain,
ap(c_2Ebool_2E_7E,c_2Ebool_2EF) = c_2Ebool_2ET,
inference(splitRight,[status(thm)],[c_5388]) ).
tff(c_82,plain,
! [A_27a_46] :
( mem(c_2Emin_2E_3D(A_27a_46),arr(A_27a_46,arr(A_27a_46,bool)))
| ~ ne(A_27a_46) ),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_8,plain,
! [F_6,X_8,B_5,A_4] :
( mem(ap(F_6,X_8),B_5)
| ~ mem(X_8,A_4)
| ~ mem(F_6,arr(A_4,B_5)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_28178,plain,
! [F_1003,F_1004,B_1005,B_1006] :
( mem(ap(F_1003,ap(F_1004,c_2Ebool_2EF)),B_1005)
| ~ mem(F_1003,arr(B_1006,B_1005))
| ~ mem(F_1004,arr(bool,B_1006)) ),
inference(resolution,[status(thm)],[c_1860,c_8]) ).
tff(c_35075,plain,
! [A_27a_1076,F_1077] :
( mem(ap(c_2Emin_2E_3D(A_27a_1076),ap(F_1077,c_2Ebool_2EF)),arr(A_27a_1076,bool))
| ~ mem(F_1077,arr(bool,A_27a_1076))
| ~ ne(A_27a_1076) ),
inference(resolution,[status(thm)],[c_82,c_28178]) ).
tff(c_35348,plain,
! [A_27a_1078] :
( mem(ap(c_2Emin_2E_3D(A_27a_1078),c_2Ebool_2ET),arr(A_27a_1078,bool))
| ~ mem(c_2Ebool_2E_7E,arr(bool,A_27a_1078))
| ~ ne(A_27a_1078) ),
inference(superposition,[status(thm),theory(equality)],[c_5398,c_35075]) ).
tff(c_1888,plain,
! [F_240] :
( ~ p(ap(F_240,c_2Ebool_2EF))
| ( ap(F_240,c_2Ebool_2EF) = c_2Ebool_2ET )
| ~ mem(F_240,arr(bool,bool)) ),
inference(resolution,[status(thm)],[c_1860,c_1713]) ).
tff(c_35484,plain,
( ~ p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF))
| ( ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF) = c_2Ebool_2ET )
| ~ mem(c_2Ebool_2E_7E,arr(bool,bool))
| ~ ne(bool) ),
inference(resolution,[status(thm)],[c_35348,c_1888]) ).
tff(c_35578,plain,
( ~ p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF))
| ( ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF) = c_2Ebool_2ET ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_76,c_35484]) ).
tff(c_36340,plain,
~ p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF)),
inference(splitLeft,[status(thm)],[c_35578]) ).
tff(c_1728,plain,
! [Q_229,R_230] :
( p(Q_229)
| p(R_230)
| ( R_230 = Q_229 )
| ~ mem(R_230,bool)
| ~ mem(Q_229,bool) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_1732,plain,
! [Q_229] :
( p(Q_229)
| p(c_2Ebool_2EF)
| ( c_2Ebool_2EF = Q_229 )
| ~ mem(Q_229,bool) ),
inference(resolution,[status(thm)],[c_48,c_1728]) ).
tff(c_1737,plain,
! [Q_229] :
( p(Q_229)
| ( c_2Ebool_2EF = Q_229 )
| ~ mem(Q_229,bool) ),
inference(negUnitSimplification,[status(thm)],[c_50,c_1732]) ).
tff(c_1886,plain,
! [F_240] :
( p(ap(F_240,c_2Ebool_2EF))
| ( ap(F_240,c_2Ebool_2EF) = c_2Ebool_2EF )
| ~ mem(F_240,arr(bool,bool)) ),
inference(resolution,[status(thm)],[c_1860,c_1737]) ).
tff(c_35464,plain,
( p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF))
| ( ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF) = c_2Ebool_2EF )
| ~ mem(c_2Ebool_2E_7E,arr(bool,bool))
| ~ ne(bool) ),
inference(resolution,[status(thm)],[c_35348,c_1886]) ).
tff(c_35563,plain,
( p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF))
| ( ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF) = c_2Ebool_2EF ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_76,c_35464]) ).
tff(c_36342,plain,
ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF) = c_2Ebool_2EF,
inference(negUnitSimplification,[status(thm)],[c_36340,c_35563]) ).
tff(c_35250,plain,
! [A_27a_1076] :
( mem(ap(c_2Emin_2E_3D(A_27a_1076),c_2Ebool_2ET),arr(A_27a_1076,bool))
| ~ mem(c_2Ebool_2E_7E,arr(bool,A_27a_1076))
| ~ ne(A_27a_1076) ),
inference(superposition,[status(thm),theory(equality)],[c_5398,c_35075]) ).
tff(c_94,plain,
! [A_55,Q_61] :
( mem('#skF_3'(A_55,Q_61),A_55)
| p(ap(c_2Ebool_2E_21(A_55),Q_61))
| ~ mem(Q_61,arr(A_55,bool))
| ~ ne(A_55) ),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_9636,plain,
! [Q_701,X_702,A_703] :
( p(ap(Q_701,X_702))
| ~ mem(X_702,A_703)
| ~ p(ap(c_2Ebool_2E_21(A_703),Q_701))
| ~ mem(Q_701,arr(A_703,bool))
| ~ ne(A_703) ),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_9756,plain,
! [Q_701] :
( p(ap(Q_701,c_2Ebool_2EF))
| ~ p(ap(c_2Ebool_2E_21(bool),Q_701))
| ~ mem(Q_701,arr(bool,bool))
| ~ ne(bool) ),
inference(resolution,[status(thm)],[c_48,c_9636]) ).
tff(c_9925,plain,
! [Q_706] :
( p(ap(Q_706,c_2Ebool_2EF))
| ~ p(ap(c_2Ebool_2E_21(bool),Q_706))
| ~ mem(Q_706,arr(bool,bool)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9756]) ).
tff(c_9929,plain,
! [Q_61] :
( p(ap(Q_61,c_2Ebool_2EF))
| mem('#skF_3'(bool,Q_61),bool)
| ~ mem(Q_61,arr(bool,bool))
| ~ ne(bool) ),
inference(resolution,[status(thm)],[c_94,c_9925]) ).
tff(c_9954,plain,
! [Q_709] :
( p(ap(Q_709,c_2Ebool_2EF))
| mem('#skF_3'(bool,Q_709),bool)
| ~ mem(Q_709,arr(bool,bool)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9929]) ).
tff(c_37644,plain,
! [Q_1101] :
( ~ p('#skF_3'(bool,Q_1101))
| ( '#skF_3'(bool,Q_1101) = c_2Ebool_2ET )
| p(ap(Q_1101,c_2Ebool_2EF))
| ~ mem(Q_1101,arr(bool,bool)) ),
inference(resolution,[status(thm)],[c_9954,c_1713]) ).
tff(c_37656,plain,
( ~ p('#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)))
| ( '#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)) = c_2Ebool_2ET )
| p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF))
| ~ mem(c_2Ebool_2E_7E,arr(bool,bool))
| ~ ne(bool) ),
inference(resolution,[status(thm)],[c_35250,c_37644]) ).
tff(c_37797,plain,
( ~ p('#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)))
| ( '#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)) = c_2Ebool_2ET )
| p(c_2Ebool_2EF) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_76,c_36342,c_37656]) ).
tff(c_37798,plain,
( ~ p('#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)))
| ( '#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)) = c_2Ebool_2ET ) ),
inference(negUnitSimplification,[status(thm)],[c_50,c_37797]) ).
tff(c_37860,plain,
~ p('#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET))),
inference(splitLeft,[status(thm)],[c_37798]) ).
tff(c_1674,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(ap(c_2Einteger_2Eint__sub,'#skF_11'),'#skF_10')))
| p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11')) ),
inference(cnfTransformation,[status(thm)],[f_672]) ).
tff(c_1675,plain,
p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11')),
inference(splitLeft,[status(thm)],[c_1674]) ).
tff(c_1830,plain,
! [F_238,B_239] :
( mem(ap(F_238,'#skF_11'),B_239)
| ~ mem(F_238,arr(ty_2Einteger_2Eint,B_239)) ),
inference(resolution,[status(thm)],[c_1662,c_1751]) ).
tff(c_5333,plain,
! [F_477] :
( ~ p(ap(F_477,'#skF_11'))
| ( ap(F_477,'#skF_11') = c_2Ebool_2ET )
| ~ mem(F_477,arr(ty_2Einteger_2Eint,bool)) ),
inference(resolution,[status(thm)],[c_1830,c_1713]) ).
tff(c_40753,plain,
! [F_1141] :
( ~ p(ap(ap(F_1141,'#skF_9'),'#skF_11'))
| ( ap(ap(F_1141,'#skF_9'),'#skF_11') = c_2Ebool_2ET )
| ~ mem(F_1141,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))) ),
inference(resolution,[status(thm)],[c_1798,c_5333]) ).
tff(c_40824,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11'))
| ( ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11') = c_2Ebool_2ET ) ),
inference(resolution,[status(thm)],[c_46,c_40753]) ).
tff(c_40846,plain,
ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11') = c_2Ebool_2ET,
inference(demodulation,[status(thm),theory(equality)],[c_1675,c_40824]) ).
tff(c_7288,plain,
! [F_600,F_601,B_602,B_603] :
( mem(ap(F_600,ap(F_601,'#skF_11')),B_602)
| ~ mem(F_600,arr(B_603,B_602))
| ~ mem(F_601,arr(ty_2Einteger_2Eint,B_603)) ),
inference(resolution,[status(thm)],[c_1830,c_8]) ).
tff(c_7338,plain,
! [A_27a_46,F_601] :
( mem(ap(c_2Emin_2E_3D(A_27a_46),ap(F_601,'#skF_11')),arr(A_27a_46,bool))
| ~ mem(F_601,arr(ty_2Einteger_2Eint,A_27a_46))
| ~ ne(A_27a_46) ),
inference(resolution,[status(thm)],[c_82,c_7288]) ).
tff(c_56322,plain,
! [A_27a_1315] :
( mem(ap(c_2Emin_2E_3D(A_27a_1315),c_2Ebool_2ET),arr(A_27a_1315,bool))
| ~ mem(ap(c_2Einteger_2Eint__divides,'#skF_9'),arr(ty_2Einteger_2Eint,A_27a_1315))
| ~ ne(A_27a_1315) ),
inference(superposition,[status(thm),theory(equality)],[c_40846,c_7338]) ).
tff(c_9989,plain,
! [Q_709] :
( p('#skF_3'(bool,Q_709))
| ( '#skF_3'(bool,Q_709) = c_2Ebool_2EF )
| p(ap(Q_709,c_2Ebool_2EF))
| ~ mem(Q_709,arr(bool,bool)) ),
inference(resolution,[status(thm)],[c_9954,c_1737]) ).
tff(c_56386,plain,
( p('#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)))
| ( '#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)) = c_2Ebool_2EF )
| p(ap(ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET),c_2Ebool_2EF))
| ~ mem(ap(c_2Einteger_2Eint__divides,'#skF_9'),arr(ty_2Einteger_2Eint,bool))
| ~ ne(bool) ),
inference(resolution,[status(thm)],[c_56322,c_9989]) ).
tff(c_56577,plain,
( p('#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)))
| ( '#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)) = c_2Ebool_2EF )
| p(c_2Ebool_2EF)
| ~ mem(ap(c_2Einteger_2Eint__divides,'#skF_9'),arr(ty_2Einteger_2Eint,bool)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36342,c_56386]) ).
tff(c_56578,plain,
( ( '#skF_3'(bool,ap(c_2Emin_2E_3D(bool),c_2Ebool_2ET)) = c_2Ebool_2EF )
| ~ mem(ap(c_2Einteger_2Eint__divides,'#skF_9'),arr(ty_2Einteger_2Eint,bool)) ),
inference(negUnitSimplification,[status(thm)],[c_50,c_37860,c_56577]) ).
tff(c_56669,plain,
~ mem(ap(c_2Einteger_2Eint__divides,'#skF_9'),arr(ty_2Einteger_2Eint,bool)),
inference(splitLeft,[status(thm)],[c_56578]) ).
tff(c_57525,plain,
~ mem(c_2Einteger_2Eint__divides,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
inference(resolution,[status(thm)],[c_1798,c_56669]) ).
tff(c_57529,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_46,c_57525]) ).
tff(c_57531,plain,
mem(ap(c_2Einteger_2Eint__divides,'#skF_9'),arr(ty_2Einteger_2Eint,bool)),
inference(splitRight,[status(thm)],[c_56578]) ).
tff(c_1920,plain,
! [F_244,B_245] :
( mem(ap(F_244,'#skF_10'),B_245)
| ~ mem(F_244,arr(ty_2Einteger_2Eint,B_245)) ),
inference(resolution,[status(thm)],[c_1664,c_1751]) ).
tff(c_1948,plain,
! [F_244] :
( ~ p(ap(F_244,'#skF_10'))
| ( ap(F_244,'#skF_10') = c_2Ebool_2ET )
| ~ mem(F_244,arr(ty_2Einteger_2Eint,bool)) ),
inference(resolution,[status(thm)],[c_1920,c_1713]) ).
tff(c_57598,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10'))
| ( ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10') = c_2Ebool_2ET ) ),
inference(resolution,[status(thm)],[c_57531,c_1948]) ).
tff(c_57651,plain,
ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10') = c_2Ebool_2ET,
inference(demodulation,[status(thm),theory(equality)],[c_1660,c_57598]) ).
tff(c_1799,plain,
! [F_232,B_234] :
( mem(ap(F_232,'#skF_10'),B_234)
| ~ mem(F_232,arr(ty_2Einteger_2Eint,B_234)) ),
inference(resolution,[status(thm)],[c_1664,c_1751]) ).
tff(c_184,plain,
! [V0x_155,V1y_157] :
( ( ap(ap(c_2Einteger_2Eint__add,V0x_155),ap(c_2Einteger_2Eint__neg,V1y_157)) = ap(ap(c_2Einteger_2Eint__sub,V0x_155),V1y_157) )
| ~ mem(V1y_157,ty_2Einteger_2Eint)
| ~ mem(V0x_155,ty_2Einteger_2Eint) ),
inference(cnfTransformation,[status(thm)],[f_410]) ).
tff(c_14821,plain,
! [V0p_819,V2r_820,V1q_821] :
( p(ap(ap(c_2Einteger_2Eint__divides,V0p_819),ap(ap(c_2Einteger_2Eint__add,V2r_820),V1q_821)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_819),V2r_820))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_819),V1q_821))
| ~ mem(V2r_820,ty_2Einteger_2Eint)
| ~ mem(V1q_821,ty_2Einteger_2Eint)
| ~ mem(V0p_819,ty_2Einteger_2Eint) ),
inference(cnfTransformation,[status(thm)],[f_424]) ).
tff(c_293403,plain,
! [V0p_3135,V0x_3136,V1y_3137] :
( p(ap(ap(c_2Einteger_2Eint__divides,V0p_3135),ap(ap(c_2Einteger_2Eint__sub,V0x_3136),V1y_3137)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_3135),V0x_3136))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_3135),ap(c_2Einteger_2Eint__neg,V1y_3137)))
| ~ mem(V0x_3136,ty_2Einteger_2Eint)
| ~ mem(ap(c_2Einteger_2Eint__neg,V1y_3137),ty_2Einteger_2Eint)
| ~ mem(V0p_3135,ty_2Einteger_2Eint)
| ~ mem(V1y_3137,ty_2Einteger_2Eint)
| ~ mem(V0x_3136,ty_2Einteger_2Eint) ),
inference(superposition,[status(thm),theory(equality)],[c_184,c_14821]) ).
tff(c_1668,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11'))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(ap(c_2Einteger_2Eint__sub,'#skF_11'),'#skF_10'))) ),
inference(cnfTransformation,[status(thm)],[f_672]) ).
tff(c_1705,plain,
~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(ap(c_2Einteger_2Eint__sub,'#skF_11'),'#skF_10'))),
inference(demodulation,[status(thm),theory(equality)],[c_1675,c_1668]) ).
tff(c_293419,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11'))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(c_2Einteger_2Eint__neg,'#skF_10')))
| ~ mem(ap(c_2Einteger_2Eint__neg,'#skF_10'),ty_2Einteger_2Eint)
| ~ mem('#skF_9',ty_2Einteger_2Eint)
| ~ mem('#skF_10',ty_2Einteger_2Eint)
| ~ mem('#skF_11',ty_2Einteger_2Eint) ),
inference(resolution,[status(thm)],[c_293403,c_1705]) ).
tff(c_293426,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(c_2Einteger_2Eint__neg,'#skF_10')))
| ~ mem(ap(c_2Einteger_2Eint__neg,'#skF_10'),ty_2Einteger_2Eint) ),
inference(demodulation,[status(thm),theory(equality)],[c_1662,c_1664,c_1666,c_28,c_40846,c_293419]) ).
tff(c_293427,plain,
~ mem(ap(c_2Einteger_2Eint__neg,'#skF_10'),ty_2Einteger_2Eint),
inference(splitLeft,[status(thm)],[c_293426]) ).
tff(c_293430,plain,
~ mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
inference(resolution,[status(thm)],[c_1799,c_293427]) ).
tff(c_293434,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_44,c_293430]) ).
tff(c_293435,plain,
~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(c_2Einteger_2Eint__neg,'#skF_10'))),
inference(splitRight,[status(thm)],[c_293426]) ).
tff(c_293683,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10'))
| ~ mem('#skF_10',ty_2Einteger_2Eint)
| ~ mem('#skF_9',ty_2Einteger_2Eint) ),
inference(resolution,[status(thm)],[c_194,c_293435]) ).
tff(c_293687,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1666,c_1664,c_28,c_57651,c_293683]) ).
tff(c_293689,plain,
~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11')),
inference(splitRight,[status(thm)],[c_1674]) ).
tff(c_293844,plain,
! [F_3165,B_3166] :
( mem(ap(F_3165,'#skF_11'),B_3166)
| ~ mem(F_3165,arr(ty_2Einteger_2Eint,B_3166)) ),
inference(resolution,[status(thm)],[c_1662,c_293765]) ).
tff(c_293721,plain,
! [Q_3153,R_3154] :
( p(Q_3153)
| p(R_3154)
| ( R_3154 = Q_3153 )
| ~ mem(R_3154,bool)
| ~ mem(Q_3153,bool) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_293725,plain,
! [Q_3153] :
( p(Q_3153)
| p(c_2Ebool_2EF)
| ( c_2Ebool_2EF = Q_3153 )
| ~ mem(Q_3153,bool) ),
inference(resolution,[status(thm)],[c_48,c_293721]) ).
tff(c_293730,plain,
! [Q_3153] :
( p(Q_3153)
| ( c_2Ebool_2EF = Q_3153 )
| ~ mem(Q_3153,bool) ),
inference(negUnitSimplification,[status(thm)],[c_50,c_293725]) ).
tff(c_298189,plain,
! [F_3434] :
( p(ap(F_3434,'#skF_11'))
| ( ap(F_3434,'#skF_11') = c_2Ebool_2EF )
| ~ mem(F_3434,arr(ty_2Einteger_2Eint,bool)) ),
inference(resolution,[status(thm)],[c_293844,c_293730]) ).
tff(c_329381,plain,
! [F_4110] :
( p(ap(ap(F_4110,'#skF_9'),'#skF_11'))
| ( ap(ap(F_4110,'#skF_9'),'#skF_11') = c_2Ebool_2EF )
| ~ mem(F_4110,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))) ),
inference(resolution,[status(thm)],[c_293812,c_298189]) ).
tff(c_329448,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11'))
| ( ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11') = c_2Ebool_2EF ) ),
inference(resolution,[status(thm)],[c_46,c_329381]) ).
tff(c_329470,plain,
ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11') = c_2Ebool_2EF,
inference(negUnitSimplification,[status(thm)],[c_293689,c_329448]) ).
tff(c_293688,plain,
p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(ap(c_2Einteger_2Eint__sub,'#skF_11'),'#skF_10'))),
inference(splitRight,[status(thm)],[c_1674]) ).
tff(c_320975,plain,
! [V0p_3975,V2r_3976,V1q_3977] :
( p(ap(ap(c_2Einteger_2Eint__divides,V0p_3975),V2r_3976))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_3975),ap(ap(c_2Einteger_2Eint__add,V2r_3976),V1q_3977)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_3975),V1q_3977))
| ~ mem(V2r_3976,ty_2Einteger_2Eint)
| ~ mem(V1q_3977,ty_2Einteger_2Eint)
| ~ mem(V0p_3975,ty_2Einteger_2Eint) ),
inference(cnfTransformation,[status(thm)],[f_424]) ).
tff(c_583485,plain,
! [V0p_6089,V0x_6090,V1y_6091] :
( p(ap(ap(c_2Einteger_2Eint__divides,V0p_6089),V0x_6090))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_6089),ap(ap(c_2Einteger_2Eint__sub,V0x_6090),V1y_6091)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,V0p_6089),ap(c_2Einteger_2Eint__neg,V1y_6091)))
| ~ mem(V0x_6090,ty_2Einteger_2Eint)
| ~ mem(ap(c_2Einteger_2Eint__neg,V1y_6091),ty_2Einteger_2Eint)
| ~ mem(V0p_6089,ty_2Einteger_2Eint)
| ~ mem(V1y_6091,ty_2Einteger_2Eint)
| ~ mem(V0x_6090,ty_2Einteger_2Eint) ),
inference(superposition,[status(thm),theory(equality)],[c_184,c_320975]) ).
tff(c_583499,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_11'))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(c_2Einteger_2Eint__neg,'#skF_10')))
| ~ mem(ap(c_2Einteger_2Eint__neg,'#skF_10'),ty_2Einteger_2Eint)
| ~ mem('#skF_9',ty_2Einteger_2Eint)
| ~ mem('#skF_10',ty_2Einteger_2Eint)
| ~ mem('#skF_11',ty_2Einteger_2Eint) ),
inference(resolution,[status(thm)],[c_293688,c_583485]) ).
tff(c_583505,plain,
( p(c_2Ebool_2EF)
| ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(c_2Einteger_2Eint__neg,'#skF_10')))
| ~ mem(ap(c_2Einteger_2Eint__neg,'#skF_10'),ty_2Einteger_2Eint) ),
inference(demodulation,[status(thm),theory(equality)],[c_1662,c_1664,c_1666,c_329470,c_583499]) ).
tff(c_583506,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(c_2Einteger_2Eint__neg,'#skF_10')))
| ~ mem(ap(c_2Einteger_2Eint__neg,'#skF_10'),ty_2Einteger_2Eint) ),
inference(negUnitSimplification,[status(thm)],[c_50,c_583505]) ).
tff(c_583507,plain,
~ mem(ap(c_2Einteger_2Eint__neg,'#skF_10'),ty_2Einteger_2Eint),
inference(splitLeft,[status(thm)],[c_583506]) ).
tff(c_583510,plain,
~ mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
inference(resolution,[status(thm)],[c_293813,c_583507]) ).
tff(c_583514,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_44,c_583510]) ).
tff(c_583515,plain,
~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),ap(c_2Einteger_2Eint__neg,'#skF_10'))),
inference(splitRight,[status(thm)],[c_583506]) ).
tff(c_583743,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,'#skF_9'),'#skF_10'))
| ~ mem('#skF_10',ty_2Einteger_2Eint)
| ~ mem('#skF_9',ty_2Einteger_2Eint) ),
inference(resolution,[status(thm)],[c_194,c_583515]) ).
tff(c_583747,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1666,c_1664,c_28,c_411970,c_583743]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ITP012+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.12/0.33 % Computer : n007.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 00:41:38 EDT 2025
% 0.12/0.34 % CPUTime :
% 182.39/119.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.39/119.42
% 182.39/119.42 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------