%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HAL004+1 : TPTP v9.2.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.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 : Tue May 5 04:28:27 PM UTC 2026
% Result : Theorem 86.86s 52.96s
% Output : CNFRefutation 87.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 15
% Syntax : Number of formulae : 97 ( 24 unt; 0 def)
% Number of atoms : 265 ( 69 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 319 ( 151 ~; 134 |; 21 &)
% ( 0 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-4 aty)
% Number of variables : 178 ( 5 sgn 64 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(subtract_in_domain,axiom,
! [X2,X5,X6] :
( ( element(X5,X2)
& element(X6,X2) )
=> element(subtract(X2,X5,X6),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',subtract_in_domain) ).
fof(subtract_to_0,axiom,
! [X2,X4] :
( element(X4,X2)
=> subtract(X2,X4,X4) = zero(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',subtract_to_0) ).
fof(morphism,axiom,
! [X1,X2,X3] :
( morphism(X1,X2,X3)
=> ( ! [X4] :
( element(X4,X2)
=> element(apply(X1,X4),X3) )
& apply(X1,zero(X2)) = zero(X3) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',morphism) ).
fof(surjection_properties,axiom,
! [X1,X2,X3] :
( ( surjection(X1)
& morphism(X1,X2,X3) )
=> ! [X7] :
( element(X7,X3)
=> ? [X8] :
( element(X8,X2)
& apply(X1,X8) = X7 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',surjection_properties) ).
fof(delta_morphism,axiom,
morphism(delta,e,r),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',delta_morphism) ).
fof(lemma3,conjecture,
! [X19] :
( element(X19,e)
=> ? [X20,X21] :
( element(X20,r)
& apply(delta,X19) = X20
& element(X21,b)
& apply(h,apply(beta,X21)) = X20
& apply(delta,apply(g,X21)) = X20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lemma3) ).
fof(commute_properties,axiom,
! [X13,X14,X15,X16,X2,X17,X18,X3] :
( ( commute(X13,X14,X15,X16)
& morphism(X13,X2,X17)
& morphism(X14,X17,X3)
& morphism(X15,X2,X18)
& morphism(X16,X18,X3) )
=> ! [X8] :
( element(X8,X2)
=> apply(X14,apply(X13,X8)) = apply(X16,apply(X15,X8)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',commute_properties) ).
fof(h_morphism,axiom,
morphism(h,c,r),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_morphism) ).
fof(h_surjection,hypothesis,
surjection(h),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_surjection) ).
fof(beta_h_g_delta_commute,axiom,
commute(beta,h,g,delta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',beta_h_g_delta_commute) ).
fof(subtract_distribution,axiom,
! [X1,X2,X3] :
( morphism(X1,X2,X3)
=> ! [X5,X6] :
( ( element(X5,X2)
& element(X6,X2) )
=> apply(X1,subtract(X2,X5,X6)) = subtract(X3,apply(X1,X5),apply(X1,X6)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',subtract_distribution) ).
fof(beta_morphism,axiom,
morphism(beta,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',beta_morphism) ).
fof(beta_surjection,axiom,
surjection(beta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',beta_surjection) ).
fof(subtract_cancellation,axiom,
! [X2,X5,X6] :
( ( element(X5,X2)
& element(X6,X2) )
=> subtract(X2,X5,subtract(X2,X5,X6)) = X6 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',subtract_cancellation) ).
fof(g_morphism,axiom,
morphism(g,b,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',g_morphism) ).
fof(c_0_15,plain,
! [X153,X154,X155] :
( ~ element(X154,X153)
| ~ element(X155,X153)
| element(subtract(X153,X154,X155),X153) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_in_domain])]) ).
fof(c_0_16,plain,
! [X156,X157] :
( ~ element(X157,X156)
| subtract(X156,X157,X157) = zero(X156) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_to_0])]) ).
fof(c_0_17,plain,
! [X94,X95,X96,X97] :
( ( ~ element(X97,X95)
| element(apply(X94,X97),X96)
| ~ morphism(X94,X95,X96) )
& ( apply(X94,zero(X95)) = zero(X96)
| ~ morphism(X94,X95,X96) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[morphism])])])]) ).
cnf(c_0_18,plain,
( element(subtract(X2,X1,X3),X2)
| ~ element(X1,X2)
| ~ element(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_19,plain,
( subtract(X2,X1,X1) = zero(X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_20,plain,
! [X108,X109,X110,X111] :
( ( element(esk3_4(X108,X109,X110,X111),X109)
| ~ element(X111,X110)
| ~ surjection(X108)
| ~ morphism(X108,X109,X110) )
& ( apply(X108,esk3_4(X108,X109,X110,X111)) = X111
| ~ element(X111,X110)
| ~ surjection(X108)
| ~ morphism(X108,X109,X110) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[surjection_properties])])])])]) ).
cnf(c_0_21,plain,
( element(apply(X3,X1),X4)
| ~ element(X1,X2)
| ~ morphism(X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_22,plain,
morphism(delta,e,r),
inference(split_conjunct,[status(thm)],[delta_morphism]) ).
fof(c_0_23,negated_conjecture,
~ ! [X19] :
( element(X19,e)
=> ? [X20,X21] :
( element(X20,r)
& apply(delta,X19) = X20
& element(X21,b)
& apply(h,apply(beta,X21)) = X20
& apply(delta,apply(g,X21)) = X20 ) ),
inference(assume_negation,[status(cth)],[lemma3]) ).
cnf(c_0_24,plain,
( element(zero(X1),X1)
| ~ element(X2,X1) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_25,plain,
( element(esk3_4(X1,X2,X3,X4),X2)
| ~ element(X4,X3)
| ~ surjection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_26,plain,
( element(apply(delta,X1),r)
| ~ element(X1,e) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
fof(c_0_27,negated_conjecture,
! [X167,X168] :
( element(esk9_0,e)
& ( ~ element(X167,r)
| apply(delta,esk9_0) != X167
| ~ element(X168,b)
| apply(h,apply(beta,X168)) != X167
| apply(delta,apply(g,X168)) != X167 ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_23])])])]) ).
fof(c_0_28,plain,
! [X135,X136,X137,X138,X139,X140,X141,X142,X143] :
( ~ commute(X135,X136,X137,X138)
| ~ morphism(X135,X139,X140)
| ~ morphism(X136,X140,X142)
| ~ morphism(X137,X139,X141)
| ~ morphism(X138,X141,X142)
| ~ element(X143,X139)
| apply(X136,apply(X135,X143)) = apply(X138,apply(X137,X143)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[commute_properties])])]) ).
cnf(c_0_29,plain,
( element(zero(X1),X1)
| ~ surjection(X2)
| ~ element(X3,X4)
| ~ morphism(X2,X1,X4) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_30,plain,
morphism(h,c,r),
inference(split_conjunct,[status(thm)],[h_morphism]) ).
cnf(c_0_31,hypothesis,
surjection(h),
inference(split_conjunct,[status(thm)],[h_surjection]) ).
cnf(c_0_32,plain,
( element(zero(r),r)
| ~ element(X1,e) ),
inference(spm,[status(thm)],[c_0_24,c_0_26]) ).
cnf(c_0_33,negated_conjecture,
element(esk9_0,e),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_34,plain,
( apply(X2,apply(X1,X9)) = apply(X4,apply(X3,X9))
| ~ commute(X1,X2,X3,X4)
| ~ morphism(X1,X5,X6)
| ~ morphism(X2,X6,X7)
| ~ morphism(X3,X5,X8)
| ~ morphism(X4,X8,X7)
| ~ element(X9,X5) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_35,plain,
commute(beta,h,g,delta),
inference(split_conjunct,[status(thm)],[beta_h_g_delta_commute]) ).
fof(c_0_36,plain,
! [X161,X162,X163,X164,X165] :
( ~ morphism(X161,X162,X163)
| ~ element(X164,X162)
| ~ element(X165,X162)
| apply(X161,subtract(X162,X164,X165)) = subtract(X163,apply(X161,X164),apply(X161,X165)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_distribution])])]) ).
cnf(c_0_37,plain,
morphism(beta,b,c),
inference(split_conjunct,[status(thm)],[beta_morphism]) ).
cnf(c_0_38,plain,
surjection(beta),
inference(split_conjunct,[status(thm)],[beta_surjection]) ).
cnf(c_0_39,plain,
( element(zero(c),c)
| ~ element(X1,r) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31])]) ).
cnf(c_0_40,negated_conjecture,
element(zero(r),r),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_41,plain,
( apply(h,apply(beta,X1)) = apply(delta,apply(g,X1))
| ~ element(X1,X2)
| ~ morphism(delta,X3,X4)
| ~ morphism(g,X2,X3)
| ~ morphism(h,X5,X4)
| ~ morphism(beta,X2,X5) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
fof(c_0_42,plain,
! [X158,X159,X160] :
( ~ element(X159,X158)
| ~ element(X160,X158)
| subtract(X158,X159,subtract(X158,X159,X160)) = X160 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_cancellation])]) ).
cnf(c_0_43,plain,
( apply(X1,subtract(X2,X4,X5)) = subtract(X3,apply(X1,X4),apply(X1,X5))
| ~ morphism(X1,X2,X3)
| ~ element(X4,X2)
| ~ element(X5,X2) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_44,plain,
morphism(g,b,e),
inference(split_conjunct,[status(thm)],[g_morphism]) ).
cnf(c_0_45,plain,
( apply(X1,zero(X2)) = zero(X3)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_46,plain,
( element(zero(b),b)
| ~ element(X1,c) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_37]),c_0_38])]) ).
cnf(c_0_47,negated_conjecture,
element(zero(c),c),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
cnf(c_0_48,negated_conjecture,
( ~ element(X1,r)
| apply(delta,esk9_0) != X1
| ~ element(X2,b)
| apply(h,apply(beta,X2)) != X1
| apply(delta,apply(g,X2)) != X1 ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_49,plain,
( apply(h,apply(beta,X1)) = apply(delta,apply(g,X1))
| ~ element(X1,X2)
| ~ morphism(g,X2,e)
| ~ morphism(h,X3,r)
| ~ morphism(beta,X2,X3) ),
inference(spm,[status(thm)],[c_0_41,c_0_22]) ).
cnf(c_0_50,plain,
( subtract(X2,X1,subtract(X2,X1,X3)) = X3
| ~ element(X1,X2)
| ~ element(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
cnf(c_0_51,plain,
( subtract(e,apply(g,X1),apply(g,X2)) = apply(g,subtract(b,X1,X2))
| ~ element(X2,b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_52,plain,
apply(g,zero(b)) = zero(e),
inference(spm,[status(thm)],[c_0_45,c_0_44]) ).
cnf(c_0_53,negated_conjecture,
element(zero(b),b),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_54,negated_conjecture,
( apply(h,apply(beta,X1)) != apply(delta,apply(g,X1))
| apply(delta,apply(g,X1)) != apply(delta,esk9_0)
| ~ element(apply(delta,apply(g,X1)),r)
| ~ element(X1,b) ),
inference(er,[status(thm)],[c_0_48]) ).
cnf(c_0_55,plain,
( element(apply(g,X1),e)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_21,c_0_44]) ).
cnf(c_0_56,plain,
( apply(h,apply(beta,X1)) = apply(delta,apply(g,X1))
| ~ element(X1,b)
| ~ morphism(h,X2,r)
| ~ morphism(beta,b,X2) ),
inference(spm,[status(thm)],[c_0_49,c_0_44]) ).
cnf(c_0_57,plain,
( subtract(X1,X2,zero(X1)) = X2
| ~ element(X2,X1) ),
inference(spm,[status(thm)],[c_0_50,c_0_19]) ).
cnf(c_0_58,plain,
( subtract(e,apply(g,X1),zero(e)) = apply(g,subtract(b,X1,zero(b)))
| ~ element(X1,b) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_52]),c_0_53])]) ).
cnf(c_0_59,plain,
( subtract(r,apply(delta,X1),apply(delta,X2)) = apply(delta,subtract(e,X1,X2))
| ~ element(X2,e)
| ~ element(X1,e) ),
inference(spm,[status(thm)],[c_0_43,c_0_22]) ).
cnf(c_0_60,plain,
apply(delta,zero(e)) = zero(r),
inference(spm,[status(thm)],[c_0_45,c_0_22]) ).
cnf(c_0_61,negated_conjecture,
element(zero(e),e),
inference(spm,[status(thm)],[c_0_24,c_0_33]) ).
cnf(c_0_62,negated_conjecture,
( apply(h,apply(beta,X1)) != apply(delta,apply(g,X1))
| apply(delta,apply(g,X1)) != apply(delta,esk9_0)
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_26]),c_0_55]) ).
cnf(c_0_63,plain,
( apply(h,apply(beta,X1)) = apply(delta,apply(g,X1))
| ~ element(X1,b) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_30]),c_0_37])]) ).
cnf(c_0_64,plain,
( apply(g,subtract(b,X1,zero(b))) = apply(g,X1)
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_55]) ).
cnf(c_0_65,plain,
( subtract(r,apply(delta,X1),zero(r)) = apply(delta,subtract(e,X1,zero(e)))
| ~ element(X1,e) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_60]),c_0_61])]) ).
cnf(c_0_66,negated_conjecture,
( apply(delta,apply(g,X1)) != apply(delta,esk9_0)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_62,c_0_63]) ).
cnf(c_0_67,plain,
( apply(g,subtract(b,subtract(b,X1,zero(b)),zero(b))) = subtract(e,apply(g,X1),zero(e))
| ~ element(subtract(b,X1,zero(b)),b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_58,c_0_64]) ).
cnf(c_0_68,plain,
( apply(delta,subtract(e,X1,zero(e))) = apply(delta,X1)
| ~ element(X1,e) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_65]),c_0_26]) ).
cnf(c_0_69,plain,
( subtract(r,apply(h,X1),apply(h,X2)) = apply(h,subtract(c,X1,X2))
| ~ element(X2,c)
| ~ element(X1,c) ),
inference(spm,[status(thm)],[c_0_43,c_0_30]) ).
cnf(c_0_70,plain,
( element(apply(h,X1),r)
| ~ element(X1,c) ),
inference(spm,[status(thm)],[c_0_21,c_0_30]) ).
cnf(c_0_71,plain,
( subtract(c,apply(beta,X1),apply(beta,X2)) = apply(beta,subtract(b,X1,X2))
| ~ element(X2,b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_43,c_0_37]) ).
cnf(c_0_72,plain,
( element(apply(beta,X1),c)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_21,c_0_37]) ).
cnf(c_0_73,negated_conjecture,
( apply(delta,subtract(e,apply(g,X1),zero(e))) != apply(delta,esk9_0)
| ~ element(subtract(b,subtract(b,X1,zero(b)),zero(b)),b)
| ~ element(subtract(b,X1,zero(b)),b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_66,c_0_67]) ).
cnf(c_0_74,plain,
( apply(delta,apply(g,subtract(b,X1,zero(b)))) = apply(delta,apply(g,X1))
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_58]),c_0_55]) ).
cnf(c_0_75,plain,
( element(apply(g,subtract(b,X1,zero(b))),e)
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18,c_0_58]),c_0_61])]),c_0_55]) ).
cnf(c_0_76,plain,
( subtract(r,apply(h,X1),apply(h,subtract(c,X1,X2))) = apply(h,X2)
| ~ element(X2,c)
| ~ element(X1,c) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_69]),c_0_70]),c_0_70]) ).
cnf(c_0_77,plain,
( subtract(c,apply(beta,X1),apply(beta,subtract(b,X1,X2))) = apply(beta,X2)
| ~ element(X2,b)
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_71]),c_0_72]),c_0_72]) ).
cnf(c_0_78,plain,
( element(apply(beta,subtract(b,X1,X2)),c)
| ~ element(X2,b)
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_18,c_0_71]),c_0_72]),c_0_72]) ).
cnf(c_0_79,negated_conjecture,
( apply(delta,subtract(e,apply(g,X1),zero(e))) != apply(delta,esk9_0)
| ~ element(subtract(b,X1,zero(b)),b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_73,c_0_57]) ).
cnf(c_0_80,plain,
( apply(delta,subtract(e,apply(g,subtract(b,X1,zero(b))),zero(e))) = subtract(r,apply(delta,apply(g,X1)),zero(r))
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_74]),c_0_75]) ).
cnf(c_0_81,plain,
( subtract(r,apply(h,apply(beta,X1)),apply(h,apply(beta,X2))) = apply(h,apply(beta,subtract(b,X1,X2)))
| ~ element(X2,b)
| ~ element(X1,b) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_77]),c_0_72]),c_0_78]) ).
cnf(c_0_82,plain,
apply(beta,zero(b)) = zero(c),
inference(spm,[status(thm)],[c_0_45,c_0_37]) ).
cnf(c_0_83,plain,
apply(h,zero(c)) = zero(r),
inference(spm,[status(thm)],[c_0_45,c_0_30]) ).
cnf(c_0_84,negated_conjecture,
( subtract(r,apply(delta,apply(g,X1)),zero(r)) != apply(delta,esk9_0)
| ~ element(subtract(b,subtract(b,X1,zero(b)),zero(b)),b)
| ~ element(subtract(b,X1,zero(b)),b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_79,c_0_80]) ).
cnf(c_0_85,plain,
( subtract(r,apply(h,apply(beta,X1)),zero(r)) = apply(h,apply(beta,subtract(b,X1,zero(b))))
| ~ element(X1,b) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_82]),c_0_83]),c_0_53])]) ).
cnf(c_0_86,negated_conjecture,
( subtract(r,apply(delta,apply(g,X1)),zero(r)) != apply(delta,esk9_0)
| ~ element(subtract(b,X1,zero(b)),b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_84,c_0_57]) ).
cnf(c_0_87,plain,
( subtract(r,apply(delta,apply(g,X1)),zero(r)) = apply(h,apply(beta,subtract(b,X1,zero(b))))
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_85,c_0_63]) ).
cnf(c_0_88,negated_conjecture,
( apply(h,apply(beta,subtract(b,X1,zero(b)))) != apply(delta,esk9_0)
| ~ element(subtract(b,X1,zero(b)),b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_86,c_0_87]) ).
cnf(c_0_89,negated_conjecture,
( apply(h,apply(beta,X1)) != apply(delta,esk9_0)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_88,c_0_57]) ).
cnf(c_0_90,plain,
( apply(X1,esk3_4(X1,X2,X3,X4)) = X4
| ~ element(X4,X3)
| ~ surjection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_91,negated_conjecture,
( apply(h,X1) != apply(delta,esk9_0)
| ~ element(esk3_4(beta,X2,X3,X1),b)
| ~ element(X1,X3)
| ~ morphism(beta,X2,X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_90]),c_0_38])]) ).
cnf(c_0_92,negated_conjecture,
( apply(h,X1) != apply(delta,esk9_0)
| ~ element(X1,X2)
| ~ morphism(beta,b,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_25]),c_0_38])]) ).
cnf(c_0_93,negated_conjecture,
( apply(h,X1) != apply(delta,esk9_0)
| ~ element(X1,c) ),
inference(spm,[status(thm)],[c_0_92,c_0_37]) ).
cnf(c_0_94,negated_conjecture,
( ~ element(esk3_4(h,X1,X2,apply(delta,esk9_0)),c)
| ~ element(apply(delta,esk9_0),X2)
| ~ morphism(h,X1,X2) ),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93,c_0_90]),c_0_31])])]) ).
cnf(c_0_95,negated_conjecture,
( ~ element(apply(delta,esk9_0),X1)
| ~ morphism(h,c,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94,c_0_25]),c_0_31])]) ).
cnf(c_0_96,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95,c_0_26]),c_0_30]),c_0_33])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HAL004+1 : TPTP v9.2.1. Released v2.6.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.12/0.32 % Computer : n022.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Mon May 4 19:08:06 EDT 2026
% 0.12/0.32 % CPUTime :
% 0.12/0.33 % start to proof: theBenchmark
% 86.86/52.96 % Version : CSE_E---1.7
% 86.86/52.96 % Problem : theBenchmark.p
% 86.86/52.96 % SZS status Theorem for theBenchmark.p
% 86.86/52.96 % SZS output start CNFRefutation
% See solution above
% 87.16/53.29 % Total time : 40.565s
%------------------------------------------------------------------------------