%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HAL001+2 : 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 : n020.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:26 PM UTC 2026
% Result : Theorem 36.92s 21.79s
% Output : CNFRefutation 37.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 26
% Syntax : Number of formulae : 132 ( 69 unt; 0 def)
% Number of atoms : 346 ( 108 equ)
% Maximal formula atoms : 24 ( 2 avg)
% Number of connectives : 374 ( 160 ~; 164 |; 31 &)
% ( 1 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 20 ( 20 usr; 13 con; 0-6 aty)
% Number of variables : 208 ( 2 sgn 99 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
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(g_morphism,axiom,
morphism(g,b,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',g_morphism) ).
fof(f_morphism,axiom,
morphism(f,a,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f_morphism) ).
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(alpha_morphism,axiom,
morphism(alpha,a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alpha_morphism) ).
fof(h_morphism,axiom,
morphism(h,c,r),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_morphism) ).
fof(gamma_morphism,axiom,
morphism(gamma,d,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gamma_morphism) ).
fof(delta_morphism,axiom,
morphism(delta,e,r),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',delta_morphism) ).
fof(injection_properties_2,axiom,
! [X1,X2,X3] :
( ( injection(X1)
& morphism(X1,X2,X3) )
=> ! [X4] :
( ( element(X4,X2)
& apply(X1,X4) = zero(X3) )
=> X4 = zero(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',injection_properties_2) ).
fof(beta_morphism,axiom,
morphism(beta,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',beta_morphism) ).
fof(properties_for_injection_2,axiom,
! [X1,X2,X3] :
( ( morphism(X1,X2,X3)
& ! [X4] :
( ( element(X4,X2)
& apply(X1,X4) = zero(X3) )
=> X4 = zero(X2) ) )
=> injection(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',properties_for_injection_2) ).
fof(g_injection,conjecture,
injection(g),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',g_injection) ).
fof(h_injection,hypothesis,
injection(h),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_injection) ).
fof(properties_for_injection,axiom,
! [X1,X2,X3] :
( ( morphism(X1,X2,X3)
& ! [X5,X6] :
( ( element(X5,X2)
& element(X6,X2)
& apply(X1,X5) = apply(X1,X6) )
=> X5 = X6 ) )
=> injection(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',properties_for_injection) ).
fof(exact_properties,axiom,
! [X9,X10,X2,X11,X3] :
( ( exact(X9,X10)
& morphism(X9,X2,X11)
& morphism(X10,X11,X3) )
=> ! [X12] :
( ( element(X12,X11)
& apply(X10,X12) = zero(X3) )
<=> ? [X8] :
( element(X8,X2)
& apply(X9,X8) = X12 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',exact_properties) ).
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_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(alpha_beta_exact,axiom,
exact(alpha,beta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alpha_beta_exact) ).
fof(alpha_g_f_gamma_commute,axiom,
commute(alpha,g,f,gamma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alpha_g_f_gamma_commute) ).
fof(alpha_injection,axiom,
injection(alpha),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',alpha_injection) ).
fof(injection_properties,axiom,
! [X1,X2,X3] :
( ( injection(X1)
& morphism(X1,X2,X3) )
=> ! [X5,X6] :
( ( element(X5,X2)
& element(X6,X2)
& apply(X1,X5) = apply(X1,X6) )
=> X5 = X6 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',injection_properties) ).
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(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(gamma_injection,axiom,
injection(gamma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gamma_injection) ).
fof(f_injection,hypothesis,
injection(f),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f_injection) ).
fof(c_0_26,plain,
! [X96,X97,X98,X99] :
( ( ~ element(X99,X97)
| element(apply(X96,X99),X98)
| ~ morphism(X96,X97,X98) )
& ( apply(X96,zero(X97)) = zero(X98)
| ~ morphism(X96,X97,X98) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[morphism])])])]) ).
cnf(c_0_27,plain,
( apply(X1,zero(X2)) = zero(X3)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_28,plain,
morphism(g,b,e),
inference(split_conjunct,[status(thm)],[g_morphism]) ).
cnf(c_0_29,plain,
morphism(f,a,d),
inference(split_conjunct,[status(thm)],[f_morphism]) ).
fof(c_0_30,plain,
! [X137,X138,X139,X140,X141,X142,X143,X144,X145] :
( ~ commute(X137,X138,X139,X140)
| ~ morphism(X137,X141,X142)
| ~ morphism(X138,X142,X144)
| ~ morphism(X139,X141,X143)
| ~ morphism(X140,X143,X144)
| ~ element(X145,X141)
| apply(X138,apply(X137,X145)) = apply(X140,apply(X139,X145)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[commute_properties])])]) ).
cnf(c_0_31,plain,
morphism(alpha,a,b),
inference(split_conjunct,[status(thm)],[alpha_morphism]) ).
cnf(c_0_32,plain,
morphism(h,c,r),
inference(split_conjunct,[status(thm)],[h_morphism]) ).
cnf(c_0_33,plain,
morphism(gamma,d,e),
inference(split_conjunct,[status(thm)],[gamma_morphism]) ).
cnf(c_0_34,plain,
zero(e) = apply(g,zero(b)),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_35,plain,
zero(d) = apply(f,zero(a)),
inference(spm,[status(thm)],[c_0_27,c_0_29]) ).
cnf(c_0_36,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_30]) ).
cnf(c_0_37,plain,
morphism(delta,e,r),
inference(split_conjunct,[status(thm)],[delta_morphism]) ).
fof(c_0_38,plain,
! [X168,X169,X170,X171] :
( ~ injection(X168)
| ~ morphism(X168,X169,X170)
| ~ element(X171,X169)
| apply(X168,X171) != zero(X170)
| X171 = zero(X169) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[injection_properties_2])])]) ).
cnf(c_0_39,plain,
morphism(beta,b,c),
inference(split_conjunct,[status(thm)],[beta_morphism]) ).
cnf(c_0_40,plain,
zero(b) = apply(alpha,zero(a)),
inference(spm,[status(thm)],[c_0_27,c_0_31]) ).
cnf(c_0_41,plain,
zero(r) = apply(h,zero(c)),
inference(spm,[status(thm)],[c_0_27,c_0_32]) ).
cnf(c_0_42,plain,
apply(g,zero(b)) = apply(gamma,apply(f,zero(a))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_33]),c_0_34]),c_0_35]) ).
fof(c_0_43,plain,
! [X172,X173,X174] :
( ( element(esk9_3(X172,X173,X174),X173)
| ~ morphism(X172,X173,X174)
| injection(X172) )
& ( apply(X172,esk9_3(X172,X173,X174)) = zero(X174)
| ~ morphism(X172,X173,X174)
| injection(X172) )
& ( esk9_3(X172,X173,X174) != zero(X173)
| ~ morphism(X172,X173,X174)
| injection(X172) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[properties_for_injection_2])])])])])]) ).
fof(c_0_44,negated_conjecture,
~ injection(g),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[g_injection])]) ).
cnf(c_0_45,plain,
( apply(X1,apply(X2,X3)) = apply(delta,apply(X4,X3))
| ~ commute(X2,X1,X4,delta)
| ~ element(X3,X5)
| ~ morphism(X4,X5,e)
| ~ morphism(X1,X6,r)
| ~ morphism(X2,X5,X6) ),
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
cnf(c_0_46,plain,
( X4 = zero(X2)
| ~ injection(X1)
| ~ morphism(X1,X2,X3)
| ~ element(X4,X2)
| apply(X1,X4) != zero(X3) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_47,hypothesis,
injection(h),
inference(split_conjunct,[status(thm)],[h_injection]) ).
cnf(c_0_48,plain,
zero(c) = apply(beta,apply(alpha,zero(a))),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_39]),c_0_40]) ).
cnf(c_0_49,plain,
apply(h,zero(c)) = apply(delta,apply(g,apply(alpha,zero(a)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_37]),c_0_34]),c_0_40]),c_0_41]) ).
cnf(c_0_50,plain,
apply(g,apply(alpha,zero(a))) = apply(gamma,apply(f,zero(a))),
inference(rw,[status(thm)],[c_0_42,c_0_40]) ).
cnf(c_0_51,plain,
( element(apply(X3,X1),X4)
| ~ element(X1,X2)
| ~ morphism(X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_52,plain,
( element(esk9_3(X1,X2,X3),X2)
| injection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_53,negated_conjecture,
~ injection(g),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_54,plain,
( apply(X1,apply(beta,X2)) = apply(delta,apply(X3,X2))
| ~ commute(beta,X1,X3,delta)
| ~ element(X2,b)
| ~ morphism(X3,b,e)
| ~ morphism(X1,c,r) ),
inference(spm,[status(thm)],[c_0_45,c_0_39]) ).
cnf(c_0_55,plain,
( apply(X1,esk9_3(X1,X2,X3)) = zero(X3)
| injection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
fof(c_0_56,plain,
! [X105,X106,X107] :
( ( element(esk1_2(X105,X106),X106)
| ~ morphism(X105,X106,X107)
| injection(X105) )
& ( element(esk2_2(X105,X106),X106)
| ~ morphism(X105,X106,X107)
| injection(X105) )
& ( apply(X105,esk1_2(X105,X106)) = apply(X105,esk2_2(X105,X106))
| ~ morphism(X105,X106,X107)
| injection(X105) )
& ( esk1_2(X105,X106) != esk2_2(X105,X106)
| ~ morphism(X105,X106,X107)
| injection(X105) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[properties_for_injection])])])])])]) ).
fof(c_0_57,plain,
! [X120,X121,X122,X123,X124,X125,X127,X128] :
( ( element(esk5_6(X120,X121,X122,X123,X124,X125),X122)
| ~ element(X125,X123)
| apply(X121,X125) != zero(X124)
| ~ exact(X120,X121)
| ~ morphism(X120,X122,X123)
| ~ morphism(X121,X123,X124) )
& ( apply(X120,esk5_6(X120,X121,X122,X123,X124,X125)) = X125
| ~ element(X125,X123)
| apply(X121,X125) != zero(X124)
| ~ exact(X120,X121)
| ~ morphism(X120,X122,X123)
| ~ morphism(X121,X123,X124) )
& ( element(X127,X123)
| ~ element(X128,X122)
| apply(X120,X128) != X127
| ~ exact(X120,X121)
| ~ morphism(X120,X122,X123)
| ~ morphism(X121,X123,X124) )
& ( apply(X121,X127) = zero(X124)
| ~ element(X128,X122)
| apply(X120,X128) != X127
| ~ exact(X120,X121)
| ~ morphism(X120,X122,X123)
| ~ morphism(X121,X123,X124) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[exact_properties])])])])])]) ).
cnf(c_0_58,plain,
( X1 = apply(beta,apply(alpha,zero(a)))
| apply(h,X1) != apply(h,apply(beta,apply(alpha,zero(a))))
| ~ element(X1,c) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_32]),c_0_47])]),c_0_48]),c_0_41]),c_0_48]) ).
cnf(c_0_59,plain,
apply(h,apply(beta,apply(alpha,zero(a)))) = apply(delta,apply(gamma,apply(f,zero(a)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_49,c_0_48]),c_0_50]) ).
cnf(c_0_60,plain,
( element(apply(beta,X1),c)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_51,c_0_39]) ).
cnf(c_0_61,plain,
element(esk9_3(g,b,e),b),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_28]),c_0_53]) ).
cnf(c_0_62,plain,
( apply(X1,apply(beta,X2)) = apply(delta,apply(g,X2))
| ~ commute(beta,X1,g,delta)
| ~ element(X2,b)
| ~ morphism(X1,c,r) ),
inference(spm,[status(thm)],[c_0_54,c_0_28]) ).
cnf(c_0_63,plain,
commute(beta,h,g,delta),
inference(split_conjunct,[status(thm)],[beta_h_g_delta_commute]) ).
cnf(c_0_64,plain,
apply(g,esk9_3(g,b,e)) = apply(g,apply(alpha,zero(a))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_28]),c_0_53]),c_0_34]),c_0_40]) ).
fof(c_0_65,plain,
! [X155,X156,X157] :
( ~ element(X156,X155)
| ~ element(X157,X155)
| element(subtract(X155,X156,X157),X155) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_in_domain])]) ).
cnf(c_0_66,plain,
( element(esk1_2(X1,X2),X2)
| injection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
fof(c_0_67,plain,
! [X158,X159] :
( ~ element(X159,X158)
| subtract(X158,X159,X159) = zero(X158) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_to_0])]) ).
cnf(c_0_68,plain,
( apply(X1,apply(X2,X3)) = apply(gamma,apply(X4,X3))
| ~ commute(X2,X1,X4,gamma)
| ~ element(X3,X5)
| ~ morphism(X4,X5,d)
| ~ morphism(X1,X6,e)
| ~ morphism(X2,X5,X6) ),
inference(spm,[status(thm)],[c_0_36,c_0_33]) ).
cnf(c_0_69,plain,
( element(esk5_6(X1,X2,X3,X4,X5,X6),X3)
| ~ element(X6,X4)
| apply(X2,X6) != zero(X5)
| ~ exact(X1,X2)
| ~ morphism(X1,X3,X4)
| ~ morphism(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
cnf(c_0_70,plain,
( X1 = apply(beta,apply(alpha,zero(a)))
| apply(h,X1) != apply(delta,apply(gamma,apply(f,zero(a))))
| ~ element(X1,c) ),
inference(rw,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_71,plain,
element(apply(beta,esk9_3(g,b,e)),c),
inference(spm,[status(thm)],[c_0_60,c_0_61]) ).
cnf(c_0_72,plain,
( apply(delta,apply(g,X1)) = apply(h,apply(beta,X1))
| ~ element(X1,b) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_32]),c_0_63])]) ).
cnf(c_0_73,plain,
apply(g,esk9_3(g,b,e)) = apply(gamma,apply(f,zero(a))),
inference(rw,[status(thm)],[c_0_64,c_0_50]) ).
cnf(c_0_74,plain,
( element(subtract(X2,X1,X3),X2)
| ~ element(X1,X2)
| ~ element(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_75,plain,
element(esk1_2(g,b),b),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_28]),c_0_53]) ).
cnf(c_0_76,plain,
( subtract(X2,X1,X1) = zero(X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_77,plain,
( apply(X1,esk5_6(X1,X2,X3,X4,X5,X6)) = X6
| ~ element(X6,X4)
| apply(X2,X6) != zero(X5)
| ~ exact(X1,X2)
| ~ morphism(X1,X3,X4)
| ~ morphism(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
cnf(c_0_78,plain,
( apply(X1,apply(alpha,X2)) = apply(gamma,apply(X3,X2))
| ~ commute(alpha,X1,X3,gamma)
| ~ element(X2,a)
| ~ morphism(X3,a,d)
| ~ morphism(X1,b,e) ),
inference(spm,[status(thm)],[c_0_68,c_0_31]) ).
cnf(c_0_79,plain,
( element(esk5_6(X1,beta,X2,b,c,X3),X2)
| apply(beta,X3) != apply(beta,apply(alpha,zero(a)))
| ~ exact(X1,beta)
| ~ element(X3,b)
| ~ morphism(X1,X2,b) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_39]),c_0_48]) ).
cnf(c_0_80,plain,
exact(alpha,beta),
inference(split_conjunct,[status(thm)],[alpha_beta_exact]) ).
cnf(c_0_81,plain,
( apply(beta,esk9_3(g,b,e)) = apply(beta,apply(alpha,zero(a)))
| apply(h,apply(beta,esk9_3(g,b,e))) != apply(delta,apply(gamma,apply(f,zero(a)))) ),
inference(spm,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_82,plain,
apply(h,apply(beta,esk9_3(g,b,e))) = apply(delta,apply(gamma,apply(f,zero(a)))),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_61]),c_0_73]) ).
cnf(c_0_83,plain,
( element(subtract(b,X1,esk1_2(g,b)),b)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_84,plain,
subtract(b,esk1_2(g,b),esk1_2(g,b)) = apply(alpha,zero(a)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_75]),c_0_40]) ).
cnf(c_0_85,plain,
( apply(X1,esk5_6(X1,beta,X2,b,c,X3)) = X3
| apply(beta,X3) != apply(beta,apply(alpha,zero(a)))
| ~ exact(X1,beta)
| ~ element(X3,b)
| ~ morphism(X1,X2,b) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_39]),c_0_48]) ).
cnf(c_0_86,plain,
( apply(X1,apply(alpha,X2)) = apply(gamma,apply(f,X2))
| ~ commute(alpha,X1,f,gamma)
| ~ element(X2,a)
| ~ morphism(X1,b,e) ),
inference(spm,[status(thm)],[c_0_78,c_0_29]) ).
cnf(c_0_87,plain,
commute(alpha,g,f,gamma),
inference(split_conjunct,[status(thm)],[alpha_g_f_gamma_commute]) ).
cnf(c_0_88,plain,
( element(esk5_6(alpha,beta,a,b,c,X1),a)
| apply(beta,X1) != apply(beta,apply(alpha,zero(a)))
| ~ element(X1,b) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79,c_0_31]),c_0_80])]) ).
cnf(c_0_89,plain,
apply(beta,esk9_3(g,b,e)) = apply(beta,apply(alpha,zero(a))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_81,c_0_82])]) ).
cnf(c_0_90,plain,
injection(alpha),
inference(split_conjunct,[status(thm)],[alpha_injection]) ).
cnf(c_0_91,plain,
element(apply(alpha,zero(a)),b),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_83,c_0_75]),c_0_84]) ).
cnf(c_0_92,plain,
( apply(alpha,esk5_6(alpha,beta,a,b,c,X1)) = X1
| apply(beta,X1) != apply(beta,apply(alpha,zero(a)))
| ~ element(X1,b) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85,c_0_31]),c_0_80])]) ).
fof(c_0_93,plain,
! [X100,X101,X102,X103,X104] :
( ~ injection(X100)
| ~ morphism(X100,X101,X102)
| ~ element(X103,X101)
| ~ element(X104,X101)
| apply(X100,X103) != apply(X100,X104)
| X103 = X104 ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[injection_properties])])]) ).
cnf(c_0_94,plain,
( apply(g,apply(alpha,X1)) = apply(gamma,apply(f,X1))
| ~ element(X1,a) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_28]),c_0_87])]) ).
cnf(c_0_95,plain,
element(esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)),a),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88,c_0_61]),c_0_89])]) ).
fof(c_0_96,plain,
! [X163,X164,X165,X166,X167] :
( ~ morphism(X163,X164,X165)
| ~ element(X166,X164)
| ~ element(X167,X164)
| apply(X163,subtract(X164,X166,X167)) = subtract(X165,apply(X163,X166),apply(X163,X167)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_distribution])])]) ).
cnf(c_0_97,plain,
( X1 = zero(a)
| apply(alpha,X1) != apply(alpha,zero(a))
| ~ element(X1,a) ),
inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_31]),c_0_90])]),c_0_40]) ).
cnf(c_0_98,plain,
element(esk5_6(alpha,beta,a,b,c,apply(alpha,zero(a))),a),
inference(spm,[status(thm)],[c_0_88,c_0_91]) ).
cnf(c_0_99,plain,
apply(alpha,esk5_6(alpha,beta,a,b,c,apply(alpha,zero(a)))) = apply(alpha,zero(a)),
inference(spm,[status(thm)],[c_0_92,c_0_91]) ).
fof(c_0_100,plain,
! [X160,X161,X162] :
( ~ element(X161,X160)
| ~ element(X162,X160)
| subtract(X160,X161,subtract(X160,X161,X162)) = X162 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_cancellation])]) ).
cnf(c_0_101,plain,
( X4 = X5
| ~ injection(X1)
| ~ morphism(X1,X2,X3)
| ~ element(X4,X2)
| ~ element(X5,X2)
| apply(X1,X4) != apply(X1,X5) ),
inference(split_conjunct,[status(thm)],[c_0_93]) ).
cnf(c_0_102,plain,
injection(gamma),
inference(split_conjunct,[status(thm)],[gamma_injection]) ).
cnf(c_0_103,plain,
( element(apply(f,X1),d)
| ~ element(X1,a) ),
inference(spm,[status(thm)],[c_0_51,c_0_29]) ).
cnf(c_0_104,plain,
apply(g,apply(alpha,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)))) = apply(gamma,apply(f,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)))),
inference(spm,[status(thm)],[c_0_94,c_0_95]) ).
cnf(c_0_105,plain,
apply(alpha,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e))) = esk9_3(g,b,e),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_61]),c_0_89])]) ).
cnf(c_0_106,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_96]) ).
cnf(c_0_107,plain,
esk5_6(alpha,beta,a,b,c,apply(alpha,zero(a))) = zero(a),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_98]),c_0_99])]) ).
cnf(c_0_108,plain,
( subtract(X2,X1,subtract(X2,X1,X3)) = X3
| ~ element(X1,X2)
| ~ element(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_100]) ).
cnf(c_0_109,hypothesis,
injection(f),
inference(split_conjunct,[status(thm)],[f_injection]) ).
cnf(c_0_110,plain,
( X1 = X2
| apply(gamma,X1) != apply(gamma,X2)
| ~ element(X2,d)
| ~ element(X1,d) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101,c_0_33]),c_0_102])]) ).
cnf(c_0_111,plain,
element(apply(f,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e))),d),
inference(spm,[status(thm)],[c_0_103,c_0_95]) ).
cnf(c_0_112,plain,
apply(gamma,apply(f,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)))) = apply(gamma,apply(f,zero(a))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_104,c_0_105]),c_0_73]) ).
cnf(c_0_113,plain,
element(apply(f,esk5_6(alpha,beta,a,b,c,apply(alpha,zero(a)))),d),
inference(spm,[status(thm)],[c_0_103,c_0_98]) ).
cnf(c_0_114,plain,
( subtract(b,apply(alpha,X1),apply(alpha,X2)) = apply(alpha,subtract(a,X1,X2))
| ~ element(X2,a)
| ~ element(X1,a) ),
inference(spm,[status(thm)],[c_0_106,c_0_31]) ).
cnf(c_0_115,plain,
element(zero(a),a),
inference(rw,[status(thm)],[c_0_98,c_0_107]) ).
cnf(c_0_116,plain,
( subtract(b,X1,subtract(b,X1,esk9_3(g,b,e))) = esk9_3(g,b,e)
| ~ element(X1,b) ),
inference(spm,[status(thm)],[c_0_108,c_0_61]) ).
cnf(c_0_117,plain,
subtract(b,esk9_3(g,b,e),esk9_3(g,b,e)) = apply(alpha,zero(a)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_61]),c_0_40]) ).
cnf(c_0_118,plain,
( X1 = zero(a)
| apply(f,X1) != apply(f,zero(a))
| ~ element(X1,a) ),
inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_29]),c_0_109])]),c_0_35]) ).
cnf(c_0_119,plain,
( X1 = apply(f,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)))
| apply(gamma,X1) != apply(gamma,apply(f,zero(a)))
| ~ element(X1,d) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110,c_0_111]),c_0_112]) ).
cnf(c_0_120,plain,
element(apply(f,zero(a)),d),
inference(rw,[status(thm)],[c_0_113,c_0_107]) ).
cnf(c_0_121,plain,
( injection(X1)
| esk9_3(X1,X2,X3) != zero(X2)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_122,plain,
( subtract(b,apply(alpha,X1),apply(alpha,zero(a))) = apply(alpha,subtract(a,X1,zero(a)))
| ~ element(X1,a) ),
inference(spm,[status(thm)],[c_0_114,c_0_115]) ).
cnf(c_0_123,plain,
subtract(b,esk9_3(g,b,e),apply(alpha,zero(a))) = esk9_3(g,b,e),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116,c_0_61]),c_0_117]) ).
cnf(c_0_124,plain,
( esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)) = zero(a)
| apply(f,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e))) != apply(f,zero(a)) ),
inference(spm,[status(thm)],[c_0_118,c_0_95]) ).
cnf(c_0_125,plain,
apply(f,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e))) = apply(f,zero(a)),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_126,plain,
esk9_3(g,b,e) != zero(b),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_28]),c_0_53]) ).
cnf(c_0_127,plain,
apply(alpha,subtract(a,esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)),zero(a))) = esk9_3(g,b,e),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122,c_0_95]),c_0_105]),c_0_123]) ).
cnf(c_0_128,plain,
esk5_6(alpha,beta,a,b,c,esk9_3(g,b,e)) = zero(a),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_124,c_0_125])]) ).
cnf(c_0_129,plain,
subtract(a,zero(a),zero(a)) = zero(a),
inference(spm,[status(thm)],[c_0_76,c_0_115]) ).
cnf(c_0_130,plain,
esk9_3(g,b,e) != apply(alpha,zero(a)),
inference(rw,[status(thm)],[c_0_126,c_0_40]) ).
cnf(c_0_131,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_127,c_0_128]),c_0_129]),c_0_130]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HAL001+2 : 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.14/0.32 % Computer : n020.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Mon May 4 19:08:35 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 36.92/21.79 % Version : CSE_E---1.7
% 36.92/21.79 % Problem : theBenchmark.p
% 36.92/21.79 % SZS status Theorem for theBenchmark.p
% 36.92/21.79 % SZS output start CNFRefutation
% See solution above
% 37.12/21.92 % Total time : 16.403s
%------------------------------------------------------------------------------