%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HAL007+1 : TPTP v9.2.1. Released v6.4.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:27 PM UTC 2026
% Result : Satisfiable 1.27s 1.73s
% Output : Saturation 1.27s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% 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(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(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(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(properties_for_commute,axiom,
! [X13,X14,X15,X16,X2,X17,X18,X3] :
( ( 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)) ) )
=> commute(X13,X14,X15,X16) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',properties_for_commute) ).
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(properties_for_exact,axiom,
! [X9,X10,X2,X11,X3] :
( ( 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 ) ) )
=> exact(X9,X10) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',properties_for_exact) ).
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(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(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(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(properties_for_surjection,axiom,
! [X1,X2,X3] :
( ( morphism(X1,X2,X3)
& ! [X7] :
( element(X7,X3)
=> ? [X8] :
( element(X8,X2)
& apply(X1,X8) = X7 ) ) )
=> surjection(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',properties_for_surjection) ).
fof(c_0_13,plain,
! [X147,X148,X149] :
( ~ element(X148,X147)
| ~ element(X149,X147)
| element(subtract(X147,X148,X149),X147) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_in_domain])]) ).
fof(c_0_14,plain,
! [X150,X151] :
( ~ element(X151,X150)
| subtract(X150,X151,X151) = zero(X150) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_to_0])]) ).
cnf(c_0_15,plain,
( element(subtract(X2,X1,X3),X2)
| ~ element(X1,X2)
| ~ element(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_13]),
[final] ).
cnf(c_0_16,plain,
( subtract(X2,X1,X1) = zero(X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_14]),
[final] ).
fof(c_0_17,plain,
! [X112,X113,X114,X115,X116,X117,X119,X120] :
( ( element(esk5_6(X112,X113,X114,X115,X116,X117),X114)
| ~ element(X117,X115)
| apply(X113,X117) != zero(X116)
| ~ exact(X112,X113)
| ~ morphism(X112,X114,X115)
| ~ morphism(X113,X115,X116) )
& ( apply(X112,esk5_6(X112,X113,X114,X115,X116,X117)) = X117
| ~ element(X117,X115)
| apply(X113,X117) != zero(X116)
| ~ exact(X112,X113)
| ~ morphism(X112,X114,X115)
| ~ morphism(X113,X115,X116) )
& ( element(X119,X115)
| ~ element(X120,X114)
| apply(X112,X120) != X119
| ~ exact(X112,X113)
| ~ morphism(X112,X114,X115)
| ~ morphism(X113,X115,X116) )
& ( apply(X113,X119) = zero(X116)
| ~ element(X120,X114)
| apply(X112,X120) != X119
| ~ exact(X112,X113)
| ~ morphism(X112,X114,X115)
| ~ morphism(X113,X115,X116) ) ),
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])])])])])]) ).
fof(c_0_18,plain,
! [X102,X103,X104,X105] :
( ( element(esk3_4(X102,X103,X104,X105),X103)
| ~ element(X105,X104)
| ~ surjection(X102)
| ~ morphism(X102,X103,X104) )
& ( apply(X102,esk3_4(X102,X103,X104,X105)) = X105
| ~ element(X105,X104)
| ~ surjection(X102)
| ~ morphism(X102,X103,X104) ) ),
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])])])])]) ).
fof(c_0_19,plain,
! [X152,X153,X154] :
( ~ element(X153,X152)
| ~ element(X154,X152)
| subtract(X152,X153,subtract(X152,X153,X154)) = X154 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_cancellation])]) ).
fof(c_0_20,plain,
! [X138,X139,X140,X141,X142,X143,X144,X145] :
( ( element(esk8_5(X138,X139,X140,X141,X142),X142)
| ~ morphism(X138,X142,X143)
| ~ morphism(X139,X143,X145)
| ~ morphism(X140,X142,X144)
| ~ morphism(X141,X144,X145)
| commute(X138,X139,X140,X141) )
& ( apply(X139,apply(X138,esk8_5(X138,X139,X140,X141,X142))) != apply(X141,apply(X140,esk8_5(X138,X139,X140,X141,X142)))
| ~ morphism(X138,X142,X143)
| ~ morphism(X139,X143,X145)
| ~ morphism(X140,X142,X144)
| ~ morphism(X141,X144,X145)
| commute(X138,X139,X140,X141) ) ),
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_commute])])])])])]) ).
fof(c_0_21,plain,
! [X129,X130,X131,X132,X133,X134,X135,X136,X137] :
( ~ commute(X129,X130,X131,X132)
| ~ morphism(X129,X133,X134)
| ~ morphism(X130,X134,X136)
| ~ morphism(X131,X133,X135)
| ~ morphism(X132,X135,X136)
| ~ element(X137,X133)
| apply(X130,apply(X129,X137)) = apply(X132,apply(X131,X137)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[commute_properties])])]) ).
fof(c_0_22,plain,
! [X121,X122,X123,X124,X125,X127] :
( ( ~ element(esk6_5(X121,X122,X123,X124,X125),X124)
| apply(X122,esk6_5(X121,X122,X123,X124,X125)) != zero(X125)
| ~ element(X127,X123)
| apply(X121,X127) != esk6_5(X121,X122,X123,X124,X125)
| ~ morphism(X121,X123,X124)
| ~ morphism(X122,X124,X125)
| exact(X121,X122) )
& ( element(esk7_5(X121,X122,X123,X124,X125),X123)
| element(esk6_5(X121,X122,X123,X124,X125),X124)
| ~ morphism(X121,X123,X124)
| ~ morphism(X122,X124,X125)
| exact(X121,X122) )
& ( apply(X121,esk7_5(X121,X122,X123,X124,X125)) = esk6_5(X121,X122,X123,X124,X125)
| element(esk6_5(X121,X122,X123,X124,X125),X124)
| ~ morphism(X121,X123,X124)
| ~ morphism(X122,X124,X125)
| exact(X121,X122) )
& ( element(esk7_5(X121,X122,X123,X124,X125),X123)
| apply(X122,esk6_5(X121,X122,X123,X124,X125)) = zero(X125)
| ~ morphism(X121,X123,X124)
| ~ morphism(X122,X124,X125)
| exact(X121,X122) )
& ( apply(X121,esk7_5(X121,X122,X123,X124,X125)) = esk6_5(X121,X122,X123,X124,X125)
| apply(X122,esk6_5(X121,X122,X123,X124,X125)) = zero(X125)
| ~ morphism(X121,X123,X124)
| ~ morphism(X122,X124,X125)
| exact(X121,X122) ) ),
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_exact])])])])])]) ).
fof(c_0_23,plain,
! [X155,X156,X157,X158,X159] :
( ~ morphism(X155,X156,X157)
| ~ element(X158,X156)
| ~ element(X159,X156)
| apply(X155,subtract(X156,X158,X159)) = subtract(X157,apply(X155,X158),apply(X155,X159)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subtract_distribution])])]) ).
cnf(c_0_24,plain,
( element(zero(X1),X1)
| ~ element(X2,X1) ),
inference(spm,[status(thm)],[c_0_15,c_0_16]),
[final] ).
cnf(c_0_25,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_17]),
[final] ).
cnf(c_0_26,plain,
( apply(X1,X2) = zero(X3)
| ~ element(X4,X5)
| apply(X6,X4) != X2
| ~ exact(X6,X1)
| ~ morphism(X6,X5,X7)
| ~ morphism(X1,X7,X3) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_27,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_18]),
[final] ).
cnf(c_0_28,plain,
( subtract(X2,X1,subtract(X2,X1,X3)) = X3
| ~ element(X1,X2)
| ~ element(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_19]),
[final] ).
fof(c_0_29,plain,
! [X97,X98,X99] :
( ( element(esk1_2(X97,X98),X98)
| ~ morphism(X97,X98,X99)
| injection(X97) )
& ( element(esk2_2(X97,X98),X98)
| ~ morphism(X97,X98,X99)
| injection(X97) )
& ( apply(X97,esk1_2(X97,X98)) = apply(X97,esk2_2(X97,X98))
| ~ morphism(X97,X98,X99)
| injection(X97) )
& ( esk1_2(X97,X98) != esk2_2(X97,X98)
| ~ morphism(X97,X98,X99)
| injection(X97) ) ),
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_30,plain,
! [X92,X93,X94,X95,X96] :
( ~ injection(X92)
| ~ morphism(X92,X93,X94)
| ~ element(X95,X93)
| ~ element(X96,X93)
| apply(X92,X95) != apply(X92,X96)
| X95 = X96 ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[injection_properties])])]) ).
fof(c_0_31,plain,
! [X88,X89,X90,X91] :
( ( ~ element(X91,X89)
| element(apply(X88,X91),X90)
| ~ morphism(X88,X89,X90) )
& ( apply(X88,zero(X89)) = zero(X90)
| ~ morphism(X88,X89,X90) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[morphism])])])]) ).
fof(c_0_32,plain,
! [X107,X108,X109,X111] :
( ( element(esk4_3(X107,X108,X109),X109)
| ~ morphism(X107,X108,X109)
| surjection(X107) )
& ( ~ element(X111,X108)
| apply(X107,X111) != esk4_3(X107,X108,X109)
| ~ morphism(X107,X108,X109)
| surjection(X107) ) ),
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_surjection])])])])])]) ).
cnf(c_0_33,plain,
( commute(X2,X1,X3,X4)
| apply(X1,apply(X2,esk8_5(X2,X1,X3,X4,X5))) != apply(X4,apply(X3,esk8_5(X2,X1,X3,X4,X5)))
| ~ morphism(X2,X5,X6)
| ~ morphism(X1,X6,X7)
| ~ morphism(X3,X5,X8)
| ~ morphism(X4,X8,X7) ),
inference(split_conjunct,[status(thm)],[c_0_20]),
[final] ).
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_21]),
[final] ).
cnf(c_0_35,plain,
( apply(X1,esk7_5(X1,X2,X3,X4,X5)) = esk6_5(X1,X2,X3,X4,X5)
| apply(X2,esk6_5(X1,X2,X3,X4,X5)) = zero(X5)
| exact(X1,X2)
| ~ morphism(X1,X3,X4)
| ~ morphism(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_22]),
[final] ).
cnf(c_0_36,plain,
( apply(X1,esk7_5(X1,X2,X3,X4,X5)) = esk6_5(X1,X2,X3,X4,X5)
| element(esk6_5(X1,X2,X3,X4,X5),X4)
| exact(X1,X2)
| ~ morphism(X1,X3,X4)
| ~ morphism(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_22]),
[final] ).
cnf(c_0_37,plain,
( element(esk7_5(X1,X2,X3,X4,X5),X3)
| apply(X2,esk6_5(X1,X2,X3,X4,X5)) = zero(X5)
| exact(X1,X2)
| ~ morphism(X1,X3,X4)
| ~ morphism(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_22]),
[final] ).
cnf(c_0_38,plain,
( element(esk7_5(X1,X2,X3,X4,X5),X3)
| element(esk6_5(X1,X2,X3,X4,X5),X4)
| exact(X1,X2)
| ~ morphism(X1,X3,X4)
| ~ morphism(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_22]),
[final] ).
cnf(c_0_39,plain,
( exact(X1,X2)
| ~ element(esk6_5(X1,X2,X3,X4,X5),X4)
| apply(X2,esk6_5(X1,X2,X3,X4,X5)) != zero(X5)
| ~ element(X6,X3)
| apply(X1,X6) != esk6_5(X1,X2,X3,X4,X5)
| ~ morphism(X1,X3,X4)
| ~ morphism(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_22]),
[final] ).
cnf(c_0_40,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_23]),
[final] ).
cnf(c_0_41,plain,
( element(esk8_5(X1,X2,X3,X4,X5),X5)
| commute(X1,X2,X3,X4)
| ~ morphism(X1,X5,X6)
| ~ morphism(X2,X6,X7)
| ~ morphism(X3,X5,X8)
| ~ morphism(X4,X8,X7) ),
inference(split_conjunct,[status(thm)],[c_0_20]),
[final] ).
cnf(c_0_42,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_17]),
[final] ).
cnf(c_0_43,plain,
( element(zero(X1),X1)
| apply(X2,X3) != zero(X4)
| ~ exact(X5,X2)
| ~ element(X3,X6)
| ~ morphism(X2,X6,X4)
| ~ morphism(X5,X1,X6) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]),
[final] ).
cnf(c_0_44,plain,
( apply(X1,apply(X2,X3)) = zero(X4)
| ~ exact(X2,X1)
| ~ element(X3,X5)
| ~ morphism(X2,X5,X6)
| ~ morphism(X1,X6,X4) ),
inference(er,[status(thm)],[c_0_26]),
[final] ).
cnf(c_0_45,plain,
( element(zero(X1),X1)
| ~ surjection(X2)
| ~ element(X3,X4)
| ~ morphism(X2,X1,X4) ),
inference(spm,[status(thm)],[c_0_24,c_0_27]),
[final] ).
cnf(c_0_46,plain,
( subtract(X1,X2,zero(X1)) = X2
| ~ element(X2,X1) ),
inference(spm,[status(thm)],[c_0_28,c_0_16]),
[final] ).
cnf(c_0_47,plain,
( apply(X1,esk1_2(X1,X2)) = apply(X1,esk2_2(X1,X2))
| injection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_29]),
[final] ).
cnf(c_0_48,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_18]),
[final] ).
cnf(c_0_49,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_30]),
[final] ).
cnf(c_0_50,plain,
( element(apply(X3,X1),X4)
| ~ element(X1,X2)
| ~ morphism(X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_31]),
[final] ).
cnf(c_0_51,plain,
( element(esk2_2(X1,X2),X2)
| injection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_29]),
[final] ).
cnf(c_0_52,plain,
( element(esk1_2(X1,X2),X2)
| injection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_29]),
[final] ).
cnf(c_0_53,plain,
( element(esk4_3(X1,X2,X3),X3)
| surjection(X1)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_32]),
[final] ).
cnf(c_0_54,plain,
( apply(X1,zero(X2)) = zero(X3)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_31]),
[final] ).
cnf(c_0_55,plain,
( surjection(X3)
| ~ element(X1,X2)
| apply(X3,X1) != esk4_3(X3,X2,X4)
| ~ morphism(X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_32]),
[final] ).
cnf(c_0_56,plain,
( injection(X1)
| esk1_2(X1,X2) != esk2_2(X1,X2)
| ~ morphism(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_29]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HAL007+1 : TPTP v9.2.1. Released v6.4.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.17/0.33 % Computer : n020.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Mon May 4 19:08:20 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.35 % start to proof: theBenchmark
% 1.27/1.73 % Version : CSE_E---1.7
% 1.27/1.73 % Problem : theBenchmark.p
% 1.27/1.73 % SZS status Satisfiable for theBenchmark.p
% 1.27/1.73 % SZS output start Saturation
% See solution above
% 1.27/1.73 % Total time : 1.372s
%------------------------------------------------------------------------------