%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HAL007+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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 : Thu May 9 17:24:44 EDT 2024
% Result : Satisfiable 0.46s 0.64s
% Output : Saturation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : HAL007+1 : TPTP v8.1.2. Released v6.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 00:18:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.46/0.64 % Version: 1.5
% 0.46/0.64 % SZS status Satisfiable
% 0.46/0.64 % SZS output start Saturation
% 0.46/0.64 fof(properties_for_exact,axiom,(![Morphism1]:(![Morphism2]:(![Dom]:(![CodDom]:(![Cod]:(((morphism(Morphism1,Dom,CodDom)&morphism(Morphism2,CodDom,Cod))&(![ElCodDom]:((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))<=>(?[ElDom]:(element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom)))))=>exact(Morphism1,Morphism2))))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', properties_for_exact)).
% 0.46/0.64 fof(c35,plain,(![Morphism1]:(![Morphism2]:(![Dom]:(![CodDom]:(![Cod]:(((~morphism(Morphism1,Dom,CodDom)|~morphism(Morphism2,CodDom,Cod))|(?[ElCodDom]:(((~element(ElCodDom,CodDom)|apply(Morphism2,ElCodDom)!=zero(Cod))|(![ElDom]:(~element(ElDom,Dom)|apply(Morphism1,ElDom)!=ElCodDom)))&((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))|(?[ElDom]:(element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom))))))|exact(Morphism1,Morphism2))))))),inference(fof_nnf,[status(thm)],[properties_for_exact])).
% 0.46/0.64 fof(c36,plain,(![Morphism1]:(![Morphism2]:((![Dom]:(![CodDom]:(![Cod]:((~morphism(Morphism1,Dom,CodDom)|~morphism(Morphism2,CodDom,Cod))|(?[ElCodDom]:(((~element(ElCodDom,CodDom)|apply(Morphism2,ElCodDom)!=zero(Cod))|(![ElDom]:(~element(ElDom,Dom)|apply(Morphism1,ElDom)!=ElCodDom)))&((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))|(?[ElDom]:(element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom)))))))))|exact(Morphism1,Morphism2)))),inference(shift_quantors,[status(thm)],[c35])).
% 0.46/0.64 fof(c37,plain,(![X33]:(![X34]:((![X35]:(![X36]:(![X37]:((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|(?[X38]:(((~element(X38,X36)|apply(X34,X38)!=zero(X37))|(![X39]:(~element(X39,X35)|apply(X33,X39)!=X38)))&((element(X38,X36)&apply(X34,X38)=zero(X37))|(?[X40]:(element(X40,X35)&apply(X33,X40)=X38)))))))))|exact(X33,X34)))),inference(variable_rename,[status(thm)],[c36])).
% 0.46/0.64 fof(c39,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X39]:(((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|(((~element(skolem0002(X33,X34,X35,X36,X37),X36)|apply(X34,skolem0002(X33,X34,X35,X36,X37))!=zero(X37))|(~element(X39,X35)|apply(X33,X39)!=skolem0002(X33,X34,X35,X36,X37)))&((element(skolem0002(X33,X34,X35,X36,X37),X36)&apply(X34,skolem0002(X33,X34,X35,X36,X37))=zero(X37))|(element(skolem0003(X33,X34,X35,X36,X37),X35)&apply(X33,skolem0003(X33,X34,X35,X36,X37))=skolem0002(X33,X34,X35,X36,X37)))))|exact(X33,X34)))))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,(![X33]:(![X34]:((![X35]:(![X36]:(![X37]:((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|(((~element(skolem0002(X33,X34,X35,X36,X37),X36)|apply(X34,skolem0002(X33,X34,X35,X36,X37))!=zero(X37))|(![X39]:(~element(X39,X35)|apply(X33,X39)!=skolem0002(X33,X34,X35,X36,X37))))&((element(skolem0002(X33,X34,X35,X36,X37),X36)&apply(X34,skolem0002(X33,X34,X35,X36,X37))=zero(X37))|(element(skolem0003(X33,X34,X35,X36,X37),X35)&apply(X33,skolem0003(X33,X34,X35,X36,X37))=skolem0002(X33,X34,X35,X36,X37))))))))|exact(X33,X34)))),inference(skolemize,[status(esa)],[c37])).])).
% 0.46/0.64 fof(c40,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X39]:((((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|((~element(skolem0002(X33,X34,X35,X36,X37),X36)|apply(X34,skolem0002(X33,X34,X35,X36,X37))!=zero(X37))|(~element(X39,X35)|apply(X33,X39)!=skolem0002(X33,X34,X35,X36,X37))))|exact(X33,X34))&(((((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|(element(skolem0002(X33,X34,X35,X36,X37),X36)|element(skolem0003(X33,X34,X35,X36,X37),X35)))|exact(X33,X34))&(((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|(element(skolem0002(X33,X34,X35,X36,X37),X36)|apply(X33,skolem0003(X33,X34,X35,X36,X37))=skolem0002(X33,X34,X35,X36,X37)))|exact(X33,X34)))&((((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|(apply(X34,skolem0002(X33,X34,X35,X36,X37))=zero(X37)|element(skolem0003(X33,X34,X35,X36,X37),X35)))|exact(X33,X34))&(((~morphism(X33,X35,X36)|~morphism(X34,X36,X37))|(apply(X34,skolem0002(X33,X34,X35,X36,X37))=zero(X37)|apply(X33,skolem0003(X33,X34,X35,X36,X37))=skolem0002(X33,X34,X35,X36,X37)))|exact(X33,X34))))))))))),inference(distribute,[status(thm)],[c39])).
% 0.46/0.64 cnf(c45,plain,~morphism(X371,X370,X368)|~morphism(X369,X368,X372)|apply(X369,skolem0002(X371,X369,X370,X368,X372))=zero(X372)|apply(X371,skolem0003(X371,X369,X370,X368,X372))=skolem0002(X371,X369,X370,X368,X372)|exact(X371,X369),inference(split_conjunct,[status(thm)],[c40])).
% 0.46/0.64 cnf(c142,plain,~morphism(X392,X393,X393)|apply(X392,skolem0002(X392,X392,X393,X393,X393))=zero(X393)|apply(X392,skolem0003(X392,X392,X393,X393,X393))=skolem0002(X392,X392,X393,X393,X393)|exact(X392,X392),inference(factor,[status(thm)],[c45])).
% 0.46/0.64 fof(exact_properties,axiom,(![Morphism1]:(![Morphism2]:(![Dom]:(![CodDom]:(![Cod]:(((exact(Morphism1,Morphism2)&morphism(Morphism1,Dom,CodDom))&morphism(Morphism2,CodDom,Cod))=>(![ElCodDom]:((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))<=>(?[ElDom]:(element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', exact_properties)).
% 0.46/0.64 fof(c46,plain,(![Morphism1]:(![Morphism2]:(![Dom]:(![CodDom]:(![Cod]:(((~exact(Morphism1,Morphism2)|~morphism(Morphism1,Dom,CodDom))|~morphism(Morphism2,CodDom,Cod))|(![ElCodDom]:(((~element(ElCodDom,CodDom)|apply(Morphism2,ElCodDom)!=zero(Cod))|(?[ElDom]:(element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom)))&((![ElDom]:(~element(ElDom,Dom)|apply(Morphism1,ElDom)!=ElCodDom))|(element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))))))))))),inference(fof_nnf,[status(thm)],[exact_properties])).
% 0.46/0.64 fof(c47,plain,(![Morphism1]:(![Morphism2]:(![Dom]:(![CodDom]:(![Cod]:(((~exact(Morphism1,Morphism2)|~morphism(Morphism1,Dom,CodDom))|~morphism(Morphism2,CodDom,Cod))|((![ElCodDom]:((~element(ElCodDom,CodDom)|apply(Morphism2,ElCodDom)!=zero(Cod))|(?[ElDom]:(element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom))))&(![ElCodDom]:((![ElDom]:(~element(ElDom,Dom)|apply(Morphism1,ElDom)!=ElCodDom))|(element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))))))))))),inference(shift_quantors,[status(thm)],[c46])).
% 0.46/0.64 fof(c48,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(((~exact(X41,X42)|~morphism(X41,X43,X44))|~morphism(X42,X44,X45))|((![X46]:((~element(X46,X44)|apply(X42,X46)!=zero(X45))|(?[X47]:(element(X47,X43)&apply(X41,X47)=X46))))&(![X48]:((![X49]:(~element(X49,X43)|apply(X41,X49)!=X48))|(element(X48,X44)&apply(X42,X48)=zero(X45))))))))))),inference(variable_rename,[status(thm)],[c47])).
% 0.46/0.64 fof(c50,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X48]:(![X49]:(((~exact(X41,X42)|~morphism(X41,X43,X44))|~morphism(X42,X44,X45))|(((~element(X46,X44)|apply(X42,X46)!=zero(X45))|(element(skolem0004(X41,X42,X43,X44,X45,X46),X43)&apply(X41,skolem0004(X41,X42,X43,X44,X45,X46))=X46))&((~element(X49,X43)|apply(X41,X49)!=X48)|(element(X48,X44)&apply(X42,X48)=zero(X45))))))))))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(((~exact(X41,X42)|~morphism(X41,X43,X44))|~morphism(X42,X44,X45))|((![X46]:((~element(X46,X44)|apply(X42,X46)!=zero(X45))|(element(skolem0004(X41,X42,X43,X44,X45,X46),X43)&apply(X41,skolem0004(X41,X42,X43,X44,X45,X46))=X46)))&(![X48]:((![X49]:(~element(X49,X43)|apply(X41,X49)!=X48))|(element(X48,X44)&apply(X42,X48)=zero(X45))))))))))),inference(skolemize,[status(esa)],[c48])).])).
% 0.46/0.64 fof(c51,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X48]:(![X49]:(((((~exact(X41,X42)|~morphism(X41,X43,X44))|~morphism(X42,X44,X45))|((~element(X46,X44)|apply(X42,X46)!=zero(X45))|element(skolem0004(X41,X42,X43,X44,X45,X46),X43)))&(((~exact(X41,X42)|~morphism(X41,X43,X44))|~morphism(X42,X44,X45))|((~element(X46,X44)|apply(X42,X46)!=zero(X45))|apply(X41,skolem0004(X41,X42,X43,X44,X45,X46))=X46)))&((((~exact(X41,X42)|~morphism(X41,X43,X44))|~morphism(X42,X44,X45))|((~element(X49,X43)|apply(X41,X49)!=X48)|element(X48,X44)))&(((~exact(X41,X42)|~morphism(X41,X43,X44))|~morphism(X42,X44,X45))|((~element(X49,X43)|apply(X41,X49)!=X48)|apply(X42,X48)=zero(X45))))))))))))),inference(distribute,[status(thm)],[c50])).
% 0.46/0.64 cnf(c53,plain,~exact(X390,X387)|~morphism(X390,X389,X391)|~morphism(X387,X391,X388)|~element(X386,X391)|apply(X387,X386)!=zero(X388)|apply(X390,skolem0004(X390,X387,X389,X391,X388,X386))=X386,inference(split_conjunct,[status(thm)],[c51])).
% 0.46/0.64 cnf(c43,plain,~morphism(X319,X318,X316)|~morphism(X317,X316,X320)|element(skolem0002(X319,X317,X318,X316,X320),X316)|apply(X319,skolem0003(X319,X317,X318,X316,X320))=skolem0002(X319,X317,X318,X316,X320)|exact(X319,X317),inference(split_conjunct,[status(thm)],[c40])).
% 0.46/0.64 cnf(c133,plain,~morphism(X385,X384,X384)|element(skolem0002(X385,X385,X384,X384,X384),X384)|apply(X385,skolem0003(X385,X385,X384,X384,X384))=skolem0002(X385,X385,X384,X384,X384)|exact(X385,X385),inference(factor,[status(thm)],[c43])).
% 0.46/0.64 cnf(c52,plain,~exact(X382,X379)|~morphism(X382,X381,X383)|~morphism(X379,X383,X380)|~element(X378,X383)|apply(X379,X378)!=zero(X380)|element(skolem0004(X382,X379,X381,X383,X380,X378),X381),inference(split_conjunct,[status(thm)],[c51])).
% 0.46/0.64 cnf(c44,plain,~morphism(X342,X341,X339)|~morphism(X340,X339,X343)|apply(X340,skolem0002(X342,X340,X341,X339,X343))=zero(X343)|element(skolem0003(X342,X340,X341,X339,X343),X341)|exact(X342,X340),inference(split_conjunct,[status(thm)],[c40])).
% 0.46/0.64 cnf(c137,plain,~morphism(X377,X376,X376)|apply(X377,skolem0002(X377,X377,X376,X376,X376))=zero(X376)|element(skolem0003(X377,X377,X376,X376,X376),X376)|exact(X377,X377),inference(factor,[status(thm)],[c44])).
% 0.46/0.64 cnf(reflexivity,axiom,X74=X74,theory(equality)).
% 0.46/0.64 cnf(c55,plain,~exact(X358,X355)|~morphism(X358,X357,X361)|~morphism(X355,X361,X356)|~element(X359,X357)|apply(X358,X359)!=X360|apply(X355,X360)=zero(X356),inference(split_conjunct,[status(thm)],[c51])).
% 0.46/0.64 cnf(c140,plain,~exact(X364,X367)|~morphism(X364,X365,X363)|~morphism(X367,X363,X362)|~element(X366,X365)|apply(X367,apply(X364,X366))=zero(X362),inference(resolution,[status(thm)],[c55, reflexivity])).
% 0.46/0.64 cnf(c141,plain,~exact(X373,X373)|~morphism(X373,X375,X375)|~element(X374,X375)|apply(X373,apply(X373,X374))=zero(X375),inference(factor,[status(thm)],[c140])).
% 0.46/0.64 fof(properties_for_commute,axiom,(![M1]:(![M2]:(![M3]:(![M4]:(![Dom]:(![DomCod1]:(![DomCod2]:(![Cod]:(((((morphism(M1,Dom,DomCod1)&morphism(M2,DomCod1,Cod))&morphism(M3,Dom,DomCod2))&morphism(M4,DomCod2,Cod))&(![ElDom]:(element(ElDom,Dom)=>apply(M2,apply(M1,ElDom))=apply(M4,apply(M3,ElDom)))))=>commute(M1,M2,M3,M4)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', properties_for_commute)).
% 0.46/0.64 fof(c22,plain,(![M1]:(![M2]:(![M3]:(![M4]:(![Dom]:(![DomCod1]:(![DomCod2]:(![Cod]:(((((~morphism(M1,Dom,DomCod1)|~morphism(M2,DomCod1,Cod))|~morphism(M3,Dom,DomCod2))|~morphism(M4,DomCod2,Cod))|(?[ElDom]:(element(ElDom,Dom)&apply(M2,apply(M1,ElDom))!=apply(M4,apply(M3,ElDom)))))|commute(M1,M2,M3,M4)))))))))),inference(fof_nnf,[status(thm)],[properties_for_commute])).
% 0.46/0.64 fof(c23,plain,(![M1]:(![M2]:(![M3]:(![M4]:((![Dom]:((![DomCod1]:(![DomCod2]:(![Cod]:(((~morphism(M1,Dom,DomCod1)|~morphism(M2,DomCod1,Cod))|~morphism(M3,Dom,DomCod2))|~morphism(M4,DomCod2,Cod)))))|(?[ElDom]:(element(ElDom,Dom)&apply(M2,apply(M1,ElDom))!=apply(M4,apply(M3,ElDom))))))|commute(M1,M2,M3,M4)))))),inference(shift_quantors,[status(thm)],[c22])).
% 0.46/0.64 fof(c24,plain,(![X15]:(![X16]:(![X17]:(![X18]:((![X19]:((![X20]:(![X21]:(![X22]:(((~morphism(X15,X19,X20)|~morphism(X16,X20,X22))|~morphism(X17,X19,X21))|~morphism(X18,X21,X22)))))|(?[X23]:(element(X23,X19)&apply(X16,apply(X15,X23))!=apply(X18,apply(X17,X23))))))|commute(X15,X16,X17,X18)))))),inference(variable_rename,[status(thm)],[c23])).
% 0.46/0.64 fof(c26,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(((((~morphism(X15,X19,X20)|~morphism(X16,X20,X22))|~morphism(X17,X19,X21))|~morphism(X18,X21,X22))|(element(skolem0001(X15,X16,X17,X18,X19),X19)&apply(X16,apply(X15,skolem0001(X15,X16,X17,X18,X19)))!=apply(X18,apply(X17,skolem0001(X15,X16,X17,X18,X19)))))|commute(X15,X16,X17,X18)))))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,(![X15]:(![X16]:(![X17]:(![X18]:((![X19]:((![X20]:(![X21]:(![X22]:(((~morphism(X15,X19,X20)|~morphism(X16,X20,X22))|~morphism(X17,X19,X21))|~morphism(X18,X21,X22)))))|(element(skolem0001(X15,X16,X17,X18,X19),X19)&apply(X16,apply(X15,skolem0001(X15,X16,X17,X18,X19)))!=apply(X18,apply(X17,skolem0001(X15,X16,X17,X18,X19))))))|commute(X15,X16,X17,X18)))))),inference(skolemize,[status(esa)],[c24])).])).
% 0.46/0.64 fof(c27,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:((((((~morphism(X15,X19,X20)|~morphism(X16,X20,X22))|~morphism(X17,X19,X21))|~morphism(X18,X21,X22))|element(skolem0001(X15,X16,X17,X18,X19),X19))|commute(X15,X16,X17,X18))&(((((~morphism(X15,X19,X20)|~morphism(X16,X20,X22))|~morphism(X17,X19,X21))|~morphism(X18,X21,X22))|apply(X16,apply(X15,skolem0001(X15,X16,X17,X18,X19)))!=apply(X18,apply(X17,skolem0001(X15,X16,X17,X18,X19))))|commute(X15,X16,X17,X18))))))))))),inference(distribute,[status(thm)],[c26])).
% 0.46/0.64 cnf(c28,plain,~morphism(X193,X188,X192)|~morphism(X187,X192,X190)|~morphism(X191,X188,X189)|~morphism(X194,X189,X190)|element(skolem0001(X193,X187,X191,X194,X188),X188)|commute(X193,X187,X191,X194),inference(split_conjunct,[status(thm)],[c27])).
% 0.46/0.64 cnf(c115,plain,~morphism(X346,X348,X344)|~morphism(X345,X344,X348)|~morphism(X347,X348,X348)|element(skolem0001(X346,X345,X347,X347,X348),X348)|commute(X346,X345,X347,X347),inference(factor,[status(thm)],[c28])).
% 0.46/0.64 cnf(c114,plain,~morphism(X324,X323,X327)|~morphism(X325,X327,X328)|~morphism(X326,X323,X327)|element(skolem0001(X324,X325,X326,X325,X323),X323)|commute(X324,X325,X326,X325),inference(factor,[status(thm)],[c28])).
% 0.46/0.64 cnf(c135,plain,~morphism(X334,X335,X335)|~morphism(X336,X335,X335)|element(skolem0001(X334,X336,X336,X336,X335),X335)|commute(X334,X336,X336,X336),inference(factor,[status(thm)],[c114])).
% 0.46/0.64 cnf(c113,plain,~morphism(X304,X306,X307)|~morphism(X303,X307,X307)|~morphism(X305,X306,X306)|element(skolem0001(X304,X303,X305,X304,X306),X306)|commute(X304,X303,X305,X304),inference(factor,[status(thm)],[c28])).
% 0.46/0.64 cnf(c130,plain,~morphism(X315,X313,X313)|~morphism(X314,X313,X313)|element(skolem0001(X315,X314,X314,X315,X313),X313)|commute(X315,X314,X314,X315),inference(factor,[status(thm)],[c113])).
% 0.46/0.64 cnf(c129,plain,~morphism(X308,X309,X309)|~morphism(X310,X309,X309)|element(skolem0001(X308,X310,X308,X308,X309),X309)|commute(X308,X310,X308,X308),inference(factor,[status(thm)],[c113])).
% 0.46/0.64 cnf(c42,plain,~morphism(X299,X298,X296)|~morphism(X297,X296,X300)|element(skolem0002(X299,X297,X298,X296,X300),X296)|element(skolem0003(X299,X297,X298,X296,X300),X298)|exact(X299,X297),inference(split_conjunct,[status(thm)],[c40])).
% 0.46/0.64 cnf(c128,plain,~morphism(X302,X301,X301)|element(skolem0002(X302,X302,X301,X301,X301),X301)|element(skolem0003(X302,X302,X301,X301,X301),X301)|exact(X302,X302),inference(factor,[status(thm)],[c42])).
% 0.46/0.64 fof(injection_properties,axiom,(![Morphism]:(![Dom]:(![Cod]:((injection(Morphism)&morphism(Morphism,Dom,Cod))=>(![El1]:(![El2]:(((element(El1,Dom)&element(El2,Dom))&apply(Morphism,El1)=apply(Morphism,El2))=>El1=El2))))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', injection_properties)).
% 0.46/0.64 fof(c81,plain,(![Morphism]:(![Dom]:(![Cod]:((~injection(Morphism)|~morphism(Morphism,Dom,Cod))|(![El1]:(![El2]:(((~element(El1,Dom)|~element(El2,Dom))|apply(Morphism,El1)!=apply(Morphism,El2))|El1=El2))))))),inference(fof_nnf,[status(thm)],[injection_properties])).
% 0.46/0.64 fof(c82,plain,(![Morphism]:(![Dom]:((~injection(Morphism)|(![Cod]:~morphism(Morphism,Dom,Cod)))|(![El1]:(![El2]:(((~element(El1,Dom)|~element(El2,Dom))|apply(Morphism,El1)!=apply(Morphism,El2))|El1=El2)))))),inference(shift_quantors,[status(thm)],[c81])).
% 0.46/0.64 fof(c84,plain,(![X65]:(![X66]:(![X67]:(![X68]:(![X69]:((~injection(X65)|~morphism(X65,X66,X67))|(((~element(X68,X66)|~element(X69,X66))|apply(X65,X68)!=apply(X65,X69))|X68=X69))))))),inference(shift_quantors,[status(thm)],[fof(c83,plain,(![X65]:(![X66]:((~injection(X65)|(![X67]:~morphism(X65,X66,X67)))|(![X68]:(![X69]:(((~element(X68,X66)|~element(X69,X66))|apply(X65,X68)!=apply(X65,X69))|X68=X69)))))),inference(variable_rename,[status(thm)],[c82])).])).
% 0.46/0.64 cnf(c85,plain,~injection(X291)|~morphism(X291,X289,X290)|~element(X288,X289)|~element(X287,X289)|apply(X291,X288)!=apply(X291,X287)|X288=X287,inference(split_conjunct,[status(thm)],[c84])).
% 0.46/0.64 cnf(c54,plain,~exact(X277,X274)|~morphism(X277,X276,X280)|~morphism(X274,X280,X275)|~element(X278,X276)|apply(X277,X278)!=X279|element(X279,X280),inference(split_conjunct,[status(thm)],[c51])).
% 0.46/0.65 cnf(c41,plain,~morphism(X269,X267,X265)|~morphism(X266,X265,X270)|~element(skolem0002(X269,X266,X267,X265,X270),X265)|apply(X266,skolem0002(X269,X266,X267,X265,X270))!=zero(X270)|~element(X268,X267)|apply(X269,X268)!=skolem0002(X269,X266,X267,X265,X270)|exact(X269,X266),inference(split_conjunct,[status(thm)],[c40])).
% 0.46/0.65 cnf(c29,plain,~morphism(X216,X211,X215)|~morphism(X210,X215,X213)|~morphism(X214,X211,X212)|~morphism(X217,X212,X213)|apply(X210,apply(X216,skolem0001(X216,X210,X214,X217,X211)))!=apply(X217,apply(X214,skolem0001(X216,X210,X214,X217,X211)))|commute(X216,X210,X214,X217),inference(split_conjunct,[status(thm)],[c27])).
% 0.46/0.65 cnf(c120,plain,~morphism(X251,X252,X250)|~morphism(X253,X250,X254)|~morphism(X251,X252,X249)|~morphism(X253,X249,X254)|commute(X251,X253,X251,X253),inference(resolution,[status(thm)],[c29, reflexivity])).
% 0.46/0.65 cnf(c123,plain,~morphism(X258,X259,X256)|~morphism(X255,X256,X257)|commute(X258,X255,X258,X255),inference(factor,[status(thm)],[c120])).
% 0.46/0.65 cnf(c125,plain,~morphism(X260,X261,X261)|commute(X260,X260,X260,X260),inference(factor,[status(thm)],[c123])).
% 0.46/0.65 fof(properties_for_injection,axiom,(![Morphism]:(![Dom]:(![Cod]:((morphism(Morphism,Dom,Cod)&(![El1]:(![El2]:(((element(El1,Dom)&element(El2,Dom))&apply(Morphism,El1)=apply(Morphism,El2))=>El1=El2))))=>injection(Morphism))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', properties_for_injection)).
% 0.46/0.65 fof(c71,plain,(![Morphism]:(![Dom]:(![Cod]:((~morphism(Morphism,Dom,Cod)|(?[El1]:(?[El2]:(((element(El1,Dom)&element(El2,Dom))&apply(Morphism,El1)=apply(Morphism,El2))&El1!=El2))))|injection(Morphism))))),inference(fof_nnf,[status(thm)],[properties_for_injection])).
% 0.46/0.65 fof(c72,plain,(![Morphism]:((![Dom]:((![Cod]:~morphism(Morphism,Dom,Cod))|(?[El1]:(?[El2]:(((element(El1,Dom)&element(El2,Dom))&apply(Morphism,El1)=apply(Morphism,El2))&El1!=El2)))))|injection(Morphism))),inference(shift_quantors,[status(thm)],[c71])).
% 0.46/0.65 fof(c73,plain,(![X60]:((![X61]:((![X62]:~morphism(X60,X61,X62))|(?[X63]:(?[X64]:(((element(X63,X61)&element(X64,X61))&apply(X60,X63)=apply(X60,X64))&X63!=X64)))))|injection(X60))),inference(variable_rename,[status(thm)],[c72])).
% 0.46/0.65 fof(c75,plain,(![X60]:(![X61]:(![X62]:((~morphism(X60,X61,X62)|(((element(skolem0007(X60,X61),X61)&element(skolem0008(X60,X61),X61))&apply(X60,skolem0007(X60,X61))=apply(X60,skolem0008(X60,X61)))&skolem0007(X60,X61)!=skolem0008(X60,X61)))|injection(X60))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,(![X60]:((![X61]:((![X62]:~morphism(X60,X61,X62))|(((element(skolem0007(X60,X61),X61)&element(skolem0008(X60,X61),X61))&apply(X60,skolem0007(X60,X61))=apply(X60,skolem0008(X60,X61)))&skolem0007(X60,X61)!=skolem0008(X60,X61))))|injection(X60))),inference(skolemize,[status(esa)],[c73])).])).
% 0.46/0.65 fof(c76,plain,(![X60]:(![X61]:(![X62]:(((((~morphism(X60,X61,X62)|element(skolem0007(X60,X61),X61))|injection(X60))&((~morphism(X60,X61,X62)|element(skolem0008(X60,X61),X61))|injection(X60)))&((~morphism(X60,X61,X62)|apply(X60,skolem0007(X60,X61))=apply(X60,skolem0008(X60,X61)))|injection(X60)))&((~morphism(X60,X61,X62)|skolem0007(X60,X61)!=skolem0008(X60,X61))|injection(X60)))))),inference(distribute,[status(thm)],[c75])).
% 0.46/0.65 cnf(c79,plain,~morphism(X247,X248,X246)|apply(X247,skolem0007(X247,X248))=apply(X247,skolem0008(X247,X248))|injection(X247),inference(split_conjunct,[status(thm)],[c76])).
% 0.46/0.65 fof(commute_properties,axiom,(![M1]:(![M2]:(![M3]:(![M4]:(![Dom]:(![DomCod1]:(![DomCod2]:(![Cod]:(((((commute(M1,M2,M3,M4)&morphism(M1,Dom,DomCod1))&morphism(M2,DomCod1,Cod))&morphism(M3,Dom,DomCod2))&morphism(M4,DomCod2,Cod))=>(![ElDom]:(element(ElDom,Dom)=>apply(M2,apply(M1,ElDom))=apply(M4,apply(M3,ElDom))))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', commute_properties)).
% 0.46/0.65 fof(c30,plain,(![M1]:(![M2]:(![M3]:(![M4]:(![Dom]:(![DomCod1]:(![DomCod2]:(![Cod]:(((((~commute(M1,M2,M3,M4)|~morphism(M1,Dom,DomCod1))|~morphism(M2,DomCod1,Cod))|~morphism(M3,Dom,DomCod2))|~morphism(M4,DomCod2,Cod))|(![ElDom]:(~element(ElDom,Dom)|apply(M2,apply(M1,ElDom))=apply(M4,apply(M3,ElDom))))))))))))),inference(fof_nnf,[status(thm)],[commute_properties])).
% 0.46/0.65 fof(c31,plain,(![M1]:(![M2]:(![M3]:(![M4]:(![Dom]:((![DomCod1]:(![DomCod2]:(![Cod]:((((~commute(M1,M2,M3,M4)|~morphism(M1,Dom,DomCod1))|~morphism(M2,DomCod1,Cod))|~morphism(M3,Dom,DomCod2))|~morphism(M4,DomCod2,Cod)))))|(![ElDom]:(~element(ElDom,Dom)|apply(M2,apply(M1,ElDom))=apply(M4,apply(M3,ElDom)))))))))),inference(shift_quantors,[status(thm)],[c30])).
% 0.46/0.65 fof(c33,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(((((~commute(X24,X25,X26,X27)|~morphism(X24,X28,X29))|~morphism(X25,X29,X31))|~morphism(X26,X28,X30))|~morphism(X27,X30,X31))|(~element(X32,X28)|apply(X25,apply(X24,X32))=apply(X27,apply(X26,X32))))))))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:((![X29]:(![X30]:(![X31]:((((~commute(X24,X25,X26,X27)|~morphism(X24,X28,X29))|~morphism(X25,X29,X31))|~morphism(X26,X28,X30))|~morphism(X27,X30,X31)))))|(![X32]:(~element(X32,X28)|apply(X25,apply(X24,X32))=apply(X27,apply(X26,X32)))))))))),inference(variable_rename,[status(thm)],[c31])).])).
% 0.46/0.65 cnf(c34,plain,~commute(X241,X245,X239,X240)|~morphism(X241,X242,X237)|~morphism(X245,X237,X238)|~morphism(X239,X242,X243)|~morphism(X240,X243,X238)|~element(X244,X242)|apply(X245,apply(X241,X244))=apply(X240,apply(X239,X244)),inference(split_conjunct,[status(thm)],[c33])).
% 0.46/0.65 fof(surjection_properties,axiom,(![Morphism]:(![Dom]:(![Cod]:((surjection(Morphism)&morphism(Morphism,Dom,Cod))=>(![ElCod]:(element(ElCod,Cod)=>(?[ElDom]:(element(ElDom,Dom)&apply(Morphism,ElDom)=ElCod)))))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', surjection_properties)).
% 0.46/0.65 fof(c64,plain,(![Morphism]:(![Dom]:(![Cod]:((~surjection(Morphism)|~morphism(Morphism,Dom,Cod))|(![ElCod]:(~element(ElCod,Cod)|(?[ElDom]:(element(ElDom,Dom)&apply(Morphism,ElDom)=ElCod)))))))),inference(fof_nnf,[status(thm)],[surjection_properties])).
% 0.46/0.65 fof(c65,plain,(![X55]:(![X56]:(![X57]:((~surjection(X55)|~morphism(X55,X56,X57))|(![X58]:(~element(X58,X57)|(?[X59]:(element(X59,X56)&apply(X55,X59)=X58)))))))),inference(variable_rename,[status(thm)],[c64])).
% 0.46/0.65 fof(c67,plain,(![X55]:(![X56]:(![X57]:(![X58]:((~surjection(X55)|~morphism(X55,X56,X57))|(~element(X58,X57)|(element(skolem0006(X55,X56,X57,X58),X56)&apply(X55,skolem0006(X55,X56,X57,X58))=X58))))))),inference(shift_quantors,[status(thm)],[fof(c66,plain,(![X55]:(![X56]:(![X57]:((~surjection(X55)|~morphism(X55,X56,X57))|(![X58]:(~element(X58,X57)|(element(skolem0006(X55,X56,X57,X58),X56)&apply(X55,skolem0006(X55,X56,X57,X58))=X58))))))),inference(skolemize,[status(esa)],[c65])).])).
% 0.46/0.65 fof(c68,plain,(![X55]:(![X56]:(![X57]:(![X58]:(((~surjection(X55)|~morphism(X55,X56,X57))|(~element(X58,X57)|element(skolem0006(X55,X56,X57,X58),X56)))&((~surjection(X55)|~morphism(X55,X56,X57))|(~element(X58,X57)|apply(X55,skolem0006(X55,X56,X57,X58))=X58))))))),inference(distribute,[status(thm)],[c67])).
% 0.46/0.65 cnf(c70,plain,~surjection(X233)|~morphism(X233,X234,X235)|~element(X236,X235)|apply(X233,skolem0006(X233,X234,X235,X236))=X236,inference(split_conjunct,[status(thm)],[c68])).
% 0.46/0.65 fof(properties_for_surjection,axiom,(![Morphism]:(![Dom]:(![Cod]:((morphism(Morphism,Dom,Cod)&(![ElCod]:(element(ElCod,Cod)=>(?[ElDom]:(element(ElDom,Dom)&apply(Morphism,ElDom)=ElCod)))))=>surjection(Morphism))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', properties_for_surjection)).
% 0.46/0.65 fof(c56,plain,(![Morphism]:(![Dom]:(![Cod]:((~morphism(Morphism,Dom,Cod)|(?[ElCod]:(element(ElCod,Cod)&(![ElDom]:(~element(ElDom,Dom)|apply(Morphism,ElDom)!=ElCod)))))|surjection(Morphism))))),inference(fof_nnf,[status(thm)],[properties_for_surjection])).
% 0.46/0.65 fof(c57,plain,(![Morphism]:((![Dom]:(![Cod]:(~morphism(Morphism,Dom,Cod)|(?[ElCod]:(element(ElCod,Cod)&(![ElDom]:(~element(ElDom,Dom)|apply(Morphism,ElDom)!=ElCod)))))))|surjection(Morphism))),inference(shift_quantors,[status(thm)],[c56])).
% 0.46/0.65 fof(c58,plain,(![X50]:((![X51]:(![X52]:(~morphism(X50,X51,X52)|(?[X53]:(element(X53,X52)&(![X54]:(~element(X54,X51)|apply(X50,X54)!=X53)))))))|surjection(X50))),inference(variable_rename,[status(thm)],[c57])).
% 0.46/0.65 fof(c60,plain,(![X50]:(![X51]:(![X52]:(![X54]:((~morphism(X50,X51,X52)|(element(skolem0005(X50,X51,X52),X52)&(~element(X54,X51)|apply(X50,X54)!=skolem0005(X50,X51,X52))))|surjection(X50)))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,(![X50]:((![X51]:(![X52]:(~morphism(X50,X51,X52)|(element(skolem0005(X50,X51,X52),X52)&(![X54]:(~element(X54,X51)|apply(X50,X54)!=skolem0005(X50,X51,X52)))))))|surjection(X50))),inference(skolemize,[status(esa)],[c58])).])).
% 0.46/0.65 fof(c61,plain,(![X50]:(![X51]:(![X52]:(![X54]:(((~morphism(X50,X51,X52)|element(skolem0005(X50,X51,X52),X52))|surjection(X50))&((~morphism(X50,X51,X52)|(~element(X54,X51)|apply(X50,X54)!=skolem0005(X50,X51,X52)))|surjection(X50))))))),inference(distribute,[status(thm)],[c60])).
% 0.46/0.65 cnf(c63,plain,~morphism(X231,X230,X232)|~element(X229,X230)|apply(X231,X229)!=skolem0005(X231,X230,X232)|surjection(X231),inference(split_conjunct,[status(thm)],[c61])).
% 0.46/0.65 cnf(c69,plain,~surjection(X225)|~morphism(X225,X226,X227)|~element(X228,X227)|element(skolem0006(X225,X226,X227,X228),X226),inference(split_conjunct,[status(thm)],[c68])).
% 0.46/0.65 cnf(c2,axiom,X107!=X109|X108!=X106|X110!=X105|subtract(X107,X108,X110)=subtract(X109,X106,X105),theory(equality)).
% 0.46/0.65 cnf(c104,plain,X202!=X204|X200!=X201|subtract(X202,X200,X203)=subtract(X204,X201,X203),inference(resolution,[status(thm)],[c2, reflexivity])).
% 0.46/0.65 cnf(c118,plain,X218!=X221|subtract(X218,X219,X220)=subtract(X221,X219,X220),inference(resolution,[status(thm)],[c104, reflexivity])).
% 0.46/0.65 cnf(c117,plain,X206!=X207|subtract(X206,X206,X205)=subtract(X207,X207,X205),inference(factor,[status(thm)],[c104])).
% 0.46/0.65 cnf(c103,plain,X184!=X183|X182!=X181|subtract(X184,X182,X182)=subtract(X183,X181,X181),inference(factor,[status(thm)],[c2])).
% 0.46/0.65 cnf(c102,plain,X167!=X164|X165!=X166|subtract(X167,X165,X167)=subtract(X164,X166,X164),inference(factor,[status(thm)],[c2])).
% 0.46/0.65 cnf(c108,plain,X178!=X176|subtract(X178,X177,X178)=subtract(X176,X177,X176),inference(resolution,[status(thm)],[c102, reflexivity])).
% 0.46/0.65 fof(subtract_distribution,axiom,(![Morphism]:(![Dom]:(![Cod]:(morphism(Morphism,Dom,Cod)=>(![El1]:(![El2]:((element(El1,Dom)&element(El2,Dom))=>apply(Morphism,subtract(Dom,El1,El2))=subtract(Cod,apply(Morphism,El1),apply(Morphism,El2))))))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', subtract_distribution)).
% 0.46/0.65 fof(c9,plain,(![Morphism]:(![Dom]:(![Cod]:(~morphism(Morphism,Dom,Cod)|(![El1]:(![El2]:((~element(El1,Dom)|~element(El2,Dom))|apply(Morphism,subtract(Dom,El1,El2))=subtract(Cod,apply(Morphism,El1),apply(Morphism,El2))))))))),inference(fof_nnf,[status(thm)],[subtract_distribution])).
% 0.46/0.65 fof(c11,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(~morphism(X2,X3,X4)|((~element(X5,X3)|~element(X6,X3))|apply(X2,subtract(X3,X5,X6))=subtract(X4,apply(X2,X5),apply(X2,X6))))))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,(![X2]:(![X3]:(![X4]:(~morphism(X2,X3,X4)|(![X5]:(![X6]:((~element(X5,X3)|~element(X6,X3))|apply(X2,subtract(X3,X5,X6))=subtract(X4,apply(X2,X5),apply(X2,X6))))))))),inference(variable_rename,[status(thm)],[c9])).])).
% 0.46/0.65 cnf(c12,plain,~morphism(X173,X174,X172)|~element(X171,X174)|~element(X170,X174)|apply(X173,subtract(X174,X171,X170))=subtract(X172,apply(X173,X171),apply(X173,X170)),inference(split_conjunct,[status(thm)],[c11])).
% 0.46/0.65 cnf(c107,plain,X169!=X168|subtract(X169,X169,X169)=subtract(X168,X168,X168),inference(factor,[status(thm)],[c102])).
% 0.46/0.65 fof(subtract_cancellation,axiom,(![Dom]:(![El1]:(![El2]:((element(El1,Dom)&element(El2,Dom))=>subtract(Dom,El1,subtract(Dom,El1,El2))=El2)))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', subtract_cancellation)).
% 0.46/0.65 fof(c13,plain,(![Dom]:(![El1]:(![El2]:((~element(El1,Dom)|~element(El2,Dom))|subtract(Dom,El1,subtract(Dom,El1,El2))=El2)))),inference(fof_nnf,[status(thm)],[subtract_cancellation])).
% 0.46/0.65 fof(c14,plain,(![X7]:(![X8]:(![X9]:((~element(X8,X7)|~element(X9,X7))|subtract(X7,X8,subtract(X7,X8,X9))=X9)))),inference(variable_rename,[status(thm)],[c13])).
% 0.46/0.65 cnf(c15,plain,~element(X160,X159)|~element(X161,X159)|subtract(X159,X160,subtract(X159,X160,X161))=X161,inference(split_conjunct,[status(thm)],[c14])).
% 0.46/0.65 cnf(c106,plain,~element(X163,X162)|subtract(X162,X163,subtract(X162,X163,X163))=X163,inference(factor,[status(thm)],[c15])).
% 0.46/0.65 cnf(c80,plain,~morphism(X157,X158,X156)|skolem0007(X157,X158)!=skolem0008(X157,X158)|injection(X157),inference(split_conjunct,[status(thm)],[c76])).
% 0.46/0.65 cnf(c8,axiom,X151!=X154|X153!=X150|X155!=X148|X152!=X149|~commute(X151,X153,X155,X152)|commute(X154,X150,X148,X149),theory(equality)).
% 0.46/0.65 fof(morphism,axiom,(![Morphism]:(![Dom]:(![Cod]:(morphism(Morphism,Dom,Cod)=>((![El]:(element(El,Dom)=>element(apply(Morphism,El),Cod)))&apply(Morphism,zero(Dom))=zero(Cod)))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', morphism)).
% 0.46/0.65 fof(c86,plain,(![Morphism]:(![Dom]:(![Cod]:(~morphism(Morphism,Dom,Cod)|((![El]:(~element(El,Dom)|element(apply(Morphism,El),Cod)))&apply(Morphism,zero(Dom))=zero(Cod)))))),inference(fof_nnf,[status(thm)],[morphism])).
% 0.46/0.65 fof(c88,plain,(![X70]:(![X71]:(![X72]:(![X73]:(~morphism(X70,X71,X72)|((~element(X73,X71)|element(apply(X70,X73),X72))&apply(X70,zero(X71))=zero(X72))))))),inference(shift_quantors,[status(thm)],[fof(c87,plain,(![X70]:(![X71]:(![X72]:(~morphism(X70,X71,X72)|((![X73]:(~element(X73,X71)|element(apply(X70,X73),X72)))&apply(X70,zero(X71))=zero(X72)))))),inference(variable_rename,[status(thm)],[c86])).])).
% 0.46/0.65 fof(c89,plain,(![X70]:(![X71]:(![X72]:(![X73]:((~morphism(X70,X71,X72)|(~element(X73,X71)|element(apply(X70,X73),X72)))&(~morphism(X70,X71,X72)|apply(X70,zero(X71))=zero(X72))))))),inference(distribute,[status(thm)],[c88])).
% 0.46/0.65 cnf(c91,plain,~morphism(X147,X145,X146)|apply(X147,zero(X145))=zero(X146),inference(split_conjunct,[status(thm)],[c89])).
% 0.46/0.65 cnf(c90,plain,~morphism(X144,X142,X143)|~element(X141,X142)|element(apply(X144,X141),X143),inference(split_conjunct,[status(thm)],[c89])).
% 0.46/0.65 cnf(c62,plain,~morphism(X139,X138,X140)|element(skolem0005(X139,X138,X140),X140)|surjection(X139),inference(split_conjunct,[status(thm)],[c61])).
% 0.46/0.65 fof(subtract_in_domain,axiom,(![Dom]:(![El1]:(![El2]:((element(El1,Dom)&element(El2,Dom))=>element(subtract(Dom,El1,El2),Dom))))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', subtract_in_domain)).
% 0.46/0.65 fof(c19,plain,(![Dom]:(![El1]:(![El2]:((~element(El1,Dom)|~element(El2,Dom))|element(subtract(Dom,El1,El2),Dom))))),inference(fof_nnf,[status(thm)],[subtract_in_domain])).
% 0.46/0.65 fof(c20,plain,(![X12]:(![X13]:(![X14]:((~element(X13,X12)|~element(X14,X12))|element(subtract(X12,X13,X14),X12))))),inference(variable_rename,[status(thm)],[c19])).
% 0.46/0.65 cnf(c21,plain,~element(X134,X135)|~element(X133,X135)|element(subtract(X135,X134,X133),X135),inference(split_conjunct,[status(thm)],[c20])).
% 0.46/0.65 cnf(c105,plain,~element(X137,X136)|element(subtract(X136,X137,X137),X136),inference(factor,[status(thm)],[c21])).
% 0.46/0.65 cnf(c3,axiom,X129!=X131|X130!=X128|X132!=X127|~morphism(X129,X130,X132)|morphism(X131,X128,X127),theory(equality)).
% 0.46/0.65 cnf(c7,axiom,X126!=X124|X123!=X125|~exact(X126,X123)|exact(X124,X125),theory(equality)).
% 0.46/0.65 cnf(c4,axiom,X122!=X120|X119!=X121|~element(X122,X119)|element(X120,X121),theory(equality)).
% 0.46/0.65 cnf(c78,plain,~morphism(X117,X118,X116)|element(skolem0008(X117,X118),X118)|injection(X117),inference(split_conjunct,[status(thm)],[c76])).
% 0.46/0.65 cnf(c77,plain,~morphism(X114,X115,X113)|element(skolem0007(X114,X115),X115)|injection(X114),inference(split_conjunct,[status(thm)],[c76])).
% 0.46/0.65 cnf(c0,axiom,X95!=X93|X92!=X94|apply(X95,X92)=apply(X93,X94),theory(equality)).
% 0.46/0.65 cnf(c99,plain,X102!=X104|apply(X102,X103)=apply(X104,X103),inference(resolution,[status(thm)],[c0, reflexivity])).
% 0.46/0.65 cnf(c98,plain,X99!=X100|apply(X99,X99)=apply(X100,X100),inference(factor,[status(thm)],[c0])).
% 0.46/0.65 fof(subtract_to_0,axiom,(![Dom]:(![El]:(element(El,Dom)=>subtract(Dom,El,El)=zero(Dom)))),file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax', subtract_to_0)).
% 0.46/0.65 fof(c16,plain,(![Dom]:(![El]:(~element(El,Dom)|subtract(Dom,El,El)=zero(Dom)))),inference(fof_nnf,[status(thm)],[subtract_to_0])).
% 0.46/0.65 fof(c17,plain,(![X10]:(![X11]:(~element(X11,X10)|subtract(X10,X11,X11)=zero(X10)))),inference(variable_rename,[status(thm)],[c16])).
% 0.46/0.65 cnf(c18,plain,~element(X98,X97)|subtract(X97,X98,X98)=zero(X97),inference(split_conjunct,[status(thm)],[c17])).
% 0.46/0.65 cnf(c1,axiom,X91!=X90|zero(X91)=zero(X90),theory(equality)).
% 0.46/0.65 cnf(c6,axiom,X88!=X87|~surjection(X88)|surjection(X87),theory(equality)).
% 0.46/0.65 cnf(transitivity,axiom,X82!=X81|X81!=X83|X82=X83,theory(equality)).
% 0.46/0.65 cnf(c5,axiom,X79!=X78|~injection(X79)|injection(X78),theory(equality)).
% 0.46/0.65 cnf(symmetry,axiom,X76!=X75|X75=X76,theory(equality)).
% 0.46/0.65 % SZS output end Saturation
% 0.46/0.65
% 0.46/0.65 % Initial clauses : 39
% 0.46/0.65 % Processed clauses : 66
% 0.46/0.65 % Factors computed : 30
% 0.46/0.65 % Resolvents computed: 21
% 0.46/0.65 % Tautologies deleted: 4
% 0.46/0.65 % Forward subsumed : 20
% 0.46/0.65 % Backward subsumed : 2
% 0.46/0.65 % -------- CPU Time ---------
% 0.46/0.65 % User time : 0.276 s
% 0.46/0.65 % System time : 0.016 s
% 0.46/0.65 % Total time : 0.292 s
%------------------------------------------------------------------------------