%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB024+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:42:54 EDT 2024
% Result : Theorem 0.40s 0.62s
% Output : Refutation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB024+2 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n024.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 : Wed May 8 22:01:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.40/0.62 % Version: 1.5
% 0.40/0.62 % SZS status Theorem
% 0.40/0.62 % SZS output start CNFRefutation
% 0.40/0.62 fof(testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties,axiom,(?[BNODE_z]:(((((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,BNODE_z))&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,BNODE_z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties)).
% 0.40/0.62 fof(c0,plain,((((?[BNODE_z]:((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,BNODE_z))&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,BNODE_z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties])).
% 0.40/0.62 fof(c1,plain,((((?[X2]:((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,X2))&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,X2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),inference(variable_rename,[status(thm)],[c0])).
% 0.40/0.62 fof(c2,plain,(((((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,skolem0001,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),inference(skolemize,[status(esa)],[c1])).
% 0.40/0.62 cnf(c9,plain,iext(uri_rdf_type,uri_ex_bob,uri_ex_Person),inference(split_conjunct,[status(thm)],[c2])).
% 0.40/0.62 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.40/0.62 fof(c45,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 0.40/0.62 fof(c46,plain,((![X]:(![C]:(~iext(uri_rdf_type,X,C)|icext(C,X))))&(![X]:(![C]:(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(shift_quantors,[status(thm)],[c45])).
% 0.40/0.62 fof(c48,plain,(![X24]:(![X25]:(![X26]:(![X27]:((~iext(uri_rdf_type,X24,X25)|icext(X25,X24))&(~icext(X27,X26)|iext(uri_rdf_type,X26,X27))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X24]:(![X25]:(~iext(uri_rdf_type,X24,X25)|icext(X25,X24))))&(![X26]:(![X27]:(~icext(X27,X26)|iext(uri_rdf_type,X26,X27))))),inference(variable_rename,[status(thm)],[c46])).])).
% 0.40/0.62 cnf(c49,plain,~iext(uri_rdf_type,X34,X35)|icext(X35,X34),inference(split_conjunct,[status(thm)],[c48])).
% 0.40/0.62 cnf(c56,plain,icext(uri_ex_Person,uri_ex_bob),inference(resolution,[status(thm)],[c49, c9])).
% 0.40/0.62 cnf(c4,plain,iext(uri_rdfs_subClassOf,uri_ex_Person,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 0.40/0.62 fof(owl_rdfsext_subclassof,axiom,(![C1]:(![C2]:(iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]:(icext(C1,X)=>icext(C2,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_rdfsext_subclassof)).
% 0.40/0.62 fof(c26,plain,(![C1]:(![C2]:((~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|icext(C2,X)))))&(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&~icext(C2,X))))|iext(uri_rdfs_subClassOf,C1,C2))))),inference(fof_nnf,[status(thm)],[owl_rdfsext_subclassof])).
% 0.40/0.62 fof(c27,plain,((![C1]:(![C2]:(~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|icext(C2,X)))))))&(![C1]:(![C2]:(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&~icext(C2,X))))|iext(uri_rdfs_subClassOf,C1,C2))))),inference(shift_quantors,[status(thm)],[c26])).
% 0.40/0.62 fof(c28,plain,((![X12]:(![X13]:(~iext(uri_rdfs_subClassOf,X12,X13)|((ic(X12)&ic(X13))&(![X14]:(~icext(X12,X14)|icext(X13,X14)))))))&(![X15]:(![X16]:(((~ic(X15)|~ic(X16))|(?[X17]:(icext(X15,X17)&~icext(X16,X17))))|iext(uri_rdfs_subClassOf,X15,X16))))),inference(variable_rename,[status(thm)],[c27])).
% 0.40/0.62 fof(c30,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((~iext(uri_rdfs_subClassOf,X12,X13)|((ic(X12)&ic(X13))&(~icext(X12,X14)|icext(X13,X14))))&(((~ic(X15)|~ic(X16))|(icext(X15,skolem0005(X15,X16))&~icext(X16,skolem0005(X15,X16))))|iext(uri_rdfs_subClassOf,X15,X16)))))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X12]:(![X13]:(~iext(uri_rdfs_subClassOf,X12,X13)|((ic(X12)&ic(X13))&(![X14]:(~icext(X12,X14)|icext(X13,X14)))))))&(![X15]:(![X16]:(((~ic(X15)|~ic(X16))|(icext(X15,skolem0005(X15,X16))&~icext(X16,skolem0005(X15,X16))))|iext(uri_rdfs_subClassOf,X15,X16))))),inference(skolemize,[status(esa)],[c28])).])).
% 0.40/0.62 fof(c31,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((((~iext(uri_rdfs_subClassOf,X12,X13)|ic(X12))&(~iext(uri_rdfs_subClassOf,X12,X13)|ic(X13)))&(~iext(uri_rdfs_subClassOf,X12,X13)|(~icext(X12,X14)|icext(X13,X14))))&((((~ic(X15)|~ic(X16))|icext(X15,skolem0005(X15,X16)))|iext(uri_rdfs_subClassOf,X15,X16))&(((~ic(X15)|~ic(X16))|~icext(X16,skolem0005(X15,X16)))|iext(uri_rdfs_subClassOf,X15,X16))))))))),inference(distribute,[status(thm)],[c30])).
% 0.40/0.62 cnf(c34,plain,~iext(uri_rdfs_subClassOf,X44,X45)|~icext(X44,X43)|icext(X45,X43),inference(split_conjunct,[status(thm)],[c31])).
% 0.40/0.62 cnf(c73,plain,~icext(uri_ex_Person,X47)|icext(skolem0001,X47),inference(resolution,[status(thm)],[c34, c4])).
% 0.40/0.62 cnf(c76,plain,icext(skolem0001,uri_ex_bob),inference(resolution,[status(thm)],[c73, c56])).
% 0.40/0.62 cnf(c6,plain,iext(uri_owl_onProperty,skolem0001,uri_ex_hasAncestor),inference(split_conjunct,[status(thm)],[c2])).
% 0.40/0.62 cnf(c7,plain,iext(uri_owl_minCardinality,skolem0001,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)),inference(split_conjunct,[status(thm)],[c2])).
% 0.40/0.62 fof(owl_restrict_mincard_001,axiom,(![Z]:(![P]:((iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))&iext(uri_owl_onProperty,Z,P))=>(![X]:(icext(Z,X)<=>(?[Y]:iext(P,X,Y))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_restrict_mincard_001)).
% 0.40/0.62 fof(c37,plain,(![Z]:(![P]:((~iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|(![X]:((~icext(Z,X)|(?[Y]:iext(P,X,Y)))&((![Y]:~iext(P,X,Y))|icext(Z,X))))))),inference(fof_nnf,[status(thm)],[owl_restrict_mincard_001])).
% 0.40/0.62 fof(c38,plain,(![Z]:(![P]:((~iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|((![X]:(~icext(Z,X)|(?[Y]:iext(P,X,Y))))&(![X]:((![Y]:~iext(P,X,Y))|icext(Z,X))))))),inference(shift_quantors,[status(thm)],[c37])).
% 0.40/0.62 fof(c39,plain,(![X18]:(![X19]:((~iext(uri_owl_minCardinality,X18,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X18,X19))|((![X20]:(~icext(X18,X20)|(?[X21]:iext(X19,X20,X21))))&(![X22]:((![X23]:~iext(X19,X22,X23))|icext(X18,X22))))))),inference(variable_rename,[status(thm)],[c38])).
% 0.40/0.62 fof(c41,plain,(![X18]:(![X19]:(![X20]:(![X22]:(![X23]:((~iext(uri_owl_minCardinality,X18,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X18,X19))|((~icext(X18,X20)|iext(X19,X20,skolem0006(X18,X19,X20)))&(~iext(X19,X22,X23)|icext(X18,X22))))))))),inference(shift_quantors,[status(thm)],[fof(c40,plain,(![X18]:(![X19]:((~iext(uri_owl_minCardinality,X18,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X18,X19))|((![X20]:(~icext(X18,X20)|iext(X19,X20,skolem0006(X18,X19,X20))))&(![X22]:((![X23]:~iext(X19,X22,X23))|icext(X18,X22))))))),inference(skolemize,[status(esa)],[c39])).])).
% 0.40/0.62 fof(c42,plain,(![X18]:(![X19]:(![X20]:(![X22]:(![X23]:(((~iext(uri_owl_minCardinality,X18,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X18,X19))|(~icext(X18,X20)|iext(X19,X20,skolem0006(X18,X19,X20))))&((~iext(uri_owl_minCardinality,X18,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X18,X19))|(~iext(X19,X22,X23)|icext(X18,X22))))))))),inference(distribute,[status(thm)],[c41])).
% 0.40/0.62 cnf(c43,plain,~iext(uri_owl_minCardinality,X61,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X61,X59)|~icext(X61,X60)|iext(X59,X60,skolem0006(X61,X59,X60)),inference(split_conjunct,[status(thm)],[c42])).
% 0.40/0.62 cnf(c104,plain,~iext(uri_owl_onProperty,skolem0001,X85)|~icext(skolem0001,X86)|iext(X85,X86,skolem0006(skolem0001,X85,X86)),inference(resolution,[status(thm)],[c43, c7])).
% 0.40/0.62 cnf(c151,plain,~icext(skolem0001,X87)|iext(uri_ex_hasAncestor,X87,skolem0006(skolem0001,uri_ex_hasAncestor,X87)),inference(resolution,[status(thm)],[c104, c6])).
% 0.40/0.62 cnf(c152,plain,iext(uri_ex_hasAncestor,uri_ex_bob,skolem0006(skolem0001,uri_ex_hasAncestor,uri_ex_bob)),inference(resolution,[status(thm)],[c151, c76])).
% 0.40/0.62 fof(testcase_conclusion_fullish_024_Cardinality_Restrictions_on_Complex_Properties,conjecture,(?[BNODE_x]:(iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)&iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_024_Cardinality_Restrictions_on_Complex_Properties)).
% 0.40/0.62 fof(c11,negated_conjecture,(~(?[BNODE_x]:(iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)&iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x)))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_024_Cardinality_Restrictions_on_Complex_Properties])).
% 0.40/0.62 fof(c12,negated_conjecture,(![BNODE_x]:(~iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)|~iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x))),inference(fof_nnf,[status(thm)],[c11])).
% 0.40/0.62 fof(c13,negated_conjecture,(![X3]:(~iext(uri_ex_hasAncestor,uri_ex_bob,X3)|~iext(uri_ex_hasAncestor,uri_ex_alice,X3))),inference(variable_rename,[status(thm)],[c12])).
% 0.40/0.62 cnf(c14,negated_conjecture,~iext(uri_ex_hasAncestor,uri_ex_bob,X31)|~iext(uri_ex_hasAncestor,uri_ex_alice,X31),inference(split_conjunct,[status(thm)],[c13])).
% 0.40/0.62 cnf(c3,plain,iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty),inference(split_conjunct,[status(thm)],[c2])).
% 0.40/0.62 cnf(c54,plain,icext(uri_owl_TransitiveProperty,uri_ex_hasAncestor),inference(resolution,[status(thm)],[c49, c3])).
% 0.40/0.62 cnf(c10,plain,iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob),inference(split_conjunct,[status(thm)],[c2])).
% 0.40/0.62 fof(owl_char_transitive,axiom,(![P]:(icext(uri_owl_TransitiveProperty,P)<=>(ip(P)&(![X]:(![Y]:(![Z]:((iext(P,X,Y)&iext(P,Y,Z))=>iext(P,X,Z)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_char_transitive)).
% 0.40/0.62 fof(c15,plain,(![P]:((~icext(uri_owl_TransitiveProperty,P)|(ip(P)&(![X]:(![Y]:(![Z]:((~iext(P,X,Y)|~iext(P,Y,Z))|iext(P,X,Z)))))))&((~ip(P)|(?[X]:(?[Y]:(?[Z]:((iext(P,X,Y)&iext(P,Y,Z))&~iext(P,X,Z))))))|icext(uri_owl_TransitiveProperty,P)))),inference(fof_nnf,[status(thm)],[owl_char_transitive])).
% 0.40/0.62 fof(c16,plain,((![P]:(~icext(uri_owl_TransitiveProperty,P)|(ip(P)&(![X]:(![Y]:(![Z]:((~iext(P,X,Y)|~iext(P,Y,Z))|iext(P,X,Z))))))))&(![P]:((~ip(P)|(?[X]:(?[Y]:(?[Z]:((iext(P,X,Y)&iext(P,Y,Z))&~iext(P,X,Z))))))|icext(uri_owl_TransitiveProperty,P)))),inference(shift_quantors,[status(thm)],[c15])).
% 0.40/0.62 fof(c17,plain,((![X4]:(~icext(uri_owl_TransitiveProperty,X4)|(ip(X4)&(![X5]:(![X6]:(![X7]:((~iext(X4,X5,X6)|~iext(X4,X6,X7))|iext(X4,X5,X7))))))))&(![X8]:((~ip(X8)|(?[X9]:(?[X10]:(?[X11]:((iext(X8,X9,X10)&iext(X8,X10,X11))&~iext(X8,X9,X11))))))|icext(uri_owl_TransitiveProperty,X8)))),inference(variable_rename,[status(thm)],[c16])).
% 0.40/0.62 fof(c19,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:((~icext(uri_owl_TransitiveProperty,X4)|(ip(X4)&((~iext(X4,X5,X6)|~iext(X4,X6,X7))|iext(X4,X5,X7))))&((~ip(X8)|((iext(X8,skolem0002(X8),skolem0003(X8))&iext(X8,skolem0003(X8),skolem0004(X8)))&~iext(X8,skolem0002(X8),skolem0004(X8))))|icext(uri_owl_TransitiveProperty,X8)))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X4]:(~icext(uri_owl_TransitiveProperty,X4)|(ip(X4)&(![X5]:(![X6]:(![X7]:((~iext(X4,X5,X6)|~iext(X4,X6,X7))|iext(X4,X5,X7))))))))&(![X8]:((~ip(X8)|((iext(X8,skolem0002(X8),skolem0003(X8))&iext(X8,skolem0003(X8),skolem0004(X8)))&~iext(X8,skolem0002(X8),skolem0004(X8))))|icext(uri_owl_TransitiveProperty,X8)))),inference(skolemize,[status(esa)],[c17])).])).
% 0.40/0.62 fof(c20,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(((~icext(uri_owl_TransitiveProperty,X4)|ip(X4))&(~icext(uri_owl_TransitiveProperty,X4)|((~iext(X4,X5,X6)|~iext(X4,X6,X7))|iext(X4,X5,X7))))&((((~ip(X8)|iext(X8,skolem0002(X8),skolem0003(X8)))|icext(uri_owl_TransitiveProperty,X8))&((~ip(X8)|iext(X8,skolem0003(X8),skolem0004(X8)))|icext(uri_owl_TransitiveProperty,X8)))&((~ip(X8)|~iext(X8,skolem0002(X8),skolem0004(X8)))|icext(uri_owl_TransitiveProperty,X8))))))))),inference(distribute,[status(thm)],[c19])).
% 0.40/0.62 cnf(c22,plain,~icext(uri_owl_TransitiveProperty,X39)|~iext(X39,X36,X38)|~iext(X39,X38,X37)|iext(X39,X36,X37),inference(split_conjunct,[status(thm)],[c20])).
% 0.40/0.62 cnf(c155,plain,~icext(uri_owl_TransitiveProperty,uri_ex_hasAncestor)|~iext(uri_ex_hasAncestor,X94,uri_ex_bob)|iext(uri_ex_hasAncestor,X94,skolem0006(skolem0001,uri_ex_hasAncestor,uri_ex_bob)),inference(resolution,[status(thm)],[c152, c22])).
% 0.40/0.62 cnf(c171,plain,~icext(uri_owl_TransitiveProperty,uri_ex_hasAncestor)|iext(uri_ex_hasAncestor,uri_ex_alice,skolem0006(skolem0001,uri_ex_hasAncestor,uri_ex_bob)),inference(resolution,[status(thm)],[c155, c10])).
% 0.40/0.62 cnf(c172,plain,iext(uri_ex_hasAncestor,uri_ex_alice,skolem0006(skolem0001,uri_ex_hasAncestor,uri_ex_bob)),inference(resolution,[status(thm)],[c171, c54])).
% 0.40/0.62 cnf(c175,plain,~iext(uri_ex_hasAncestor,uri_ex_bob,skolem0006(skolem0001,uri_ex_hasAncestor,uri_ex_bob)),inference(resolution,[status(thm)],[c172, c14])).
% 0.40/0.62 cnf(c176,plain,$false,inference(resolution,[status(thm)],[c175, c152])).
% 0.40/0.62 % SZS output end CNFRefutation
% 0.40/0.62
% 0.40/0.62 % Initial clauses : 23
% 0.40/0.62 % Processed clauses : 82
% 0.40/0.62 % Factors computed : 4
% 0.40/0.62 % Resolvents computed: 122
% 0.40/0.62 % Tautologies deleted: 9
% 0.40/0.62 % Forward subsumed : 50
% 0.40/0.62 % Backward subsumed : 5
% 0.40/0.62 % -------- CPU Time ---------
% 0.40/0.62 % User time : 0.265 s
% 0.40/0.62 % System time : 0.014 s
% 0.40/0.62 % Total time : 0.279 s
%------------------------------------------------------------------------------