%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWB010+2 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 : 600s
% DateTime : Tue Jul 19 19:12:46 EDT 2022
% Result : Theorem 0.36s 1.32s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SWB010+2 : TPTP v8.1.0. Released v5.2.0.
% 0.00/0.08 % Command : leancop_casc.sh %s %d
% 0.07/0.26 % Computer : n032.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 600
% 0.07/0.26 % DateTime : Wed Jun 1 14:25:59 EDT 2022
% 0.07/0.27 % CPUTime :
% 0.36/1.32 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.33 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.33
% 0.36/1.33 %-----------------------------------------------------
% 0.36/1.33 fof(testcase_conclusion_fullish_010_Negative_Property_Assertions, conjecture, ? [_42225] : (iext(uri_rdf_type, _42225, uri_owl_NegativePropertyAssertion) & iext(uri_owl_sourceIndividual, _42225, uri_ex_s) & iext(uri_owl_assertionProperty, _42225, uri_ex_p) & iext(uri_owl_targetIndividual, _42225, uri_ex_o)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 fof(simple_ir, axiom, ! [_42474] : ir(_42474), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', simple_ir)).
% 0.36/1.33 fof(rdfs_cext_def, axiom, ! [_42574, _42577] : (iext(uri_rdf_type, _42574, _42577) <=> icext(_42577, _42574)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.36/1.33 fof(owl_prop_sourceindividual_ext, axiom, ! [_42739, _42742] : (iext(uri_owl_sourceIndividual, _42739, _42742) => icext(uri_owl_NegativePropertyAssertion, _42739) & ir(_42742)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_prop_sourceindividual_ext)).
% 0.36/1.33 fof(owl_prop_onproperty_ext, axiom, ! [_42915, _42918] : (iext(uri_owl_onProperty, _42915, _42918) => icext(uri_owl_Restriction, _42915) & ip(_42918)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_prop_onproperty_ext)).
% 0.36/1.33 fof(owl_bool_complementof_class, axiom, ! [_43090, _43093] : (iext(uri_owl_complementOf, _43090, _43093) => ic(_43090) & ic(_43093) & ! [_43128] : (icext(_43090, _43128) <=> ~ icext(_43093, _43128))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_bool_complementof_class)).
% 0.36/1.33 fof(owl_enum_class_001, axiom, ! [_43364, _43367, _43370] : (iext(uri_rdf_first, _43367, _43370) & iext(uri_rdf_rest, _43367, uri_rdf_nil) => (iext(uri_owl_oneOf, _43364, _43367) <=> ic(_43364) & ! [_43424] : (icext(_43364, _43424) <=> _43424 = _43370))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_enum_class_001)).
% 0.36/1.33 fof(testcase_premise_fullish_010_Negative_Property_Assertions, axiom, ? [_43710, _43713, _43716, _43719] : (iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty) & iext(uri_rdf_type, uri_ex_s, _43710) & iext(uri_owl_onProperty, _43710, uri_ex_p) & iext(uri_owl_allValuesFrom, _43710, _43713) & iext(uri_owl_complementOf, _43713, _43716) & iext(uri_owl_oneOf, _43716, _43719) & iext(uri_rdf_first, _43719, uri_ex_o) & iext(uri_rdf_rest, _43719, uri_rdf_nil)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 fof(owl_npa_object_fi, axiom, ! [_44174, _44177, _44180] : (ir(_44177) & ip(_44174) & ir(_44180) & ~ iext(_44174, _44177, _44180) => ? [_44224] : (iext(uri_owl_sourceIndividual, _44224, _44177) & iext(uri_owl_assertionProperty, _44224, _44174) & iext(uri_owl_targetIndividual, _44224, _44180))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_npa_object_fi)).
% 0.36/1.33 fof(owl_restrict_allvaluesfrom, axiom, ! [_44541, _44544, _44547] : (iext(uri_owl_allValuesFrom, _44541, _44547) & iext(uri_owl_onProperty, _44541, _44544) => ! [_44581] : (icext(_44541, _44581) <=> ! [_44599] : (iext(_44544, _44581, _44599) => icext(_44547, _44599)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_restrict_allvaluesfrom)).
% 0.36/1.33
% 0.36/1.33 cnf(1, plain, [iext(uri_rdf_type, _18272, uri_owl_NegativePropertyAssertion), iext(uri_owl_sourceIndividual, _18272, uri_ex_s), iext(uri_owl_assertionProperty, _18272, uri_ex_p), iext(uri_owl_targetIndividual, _18272, uri_ex_o)], clausify(testcase_conclusion_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(2, plain, [-(_8256 = _8256)], theory(equality)).
% 0.36/1.33 cnf(3, plain, [-(_8688 = _8799), _8688 = _8744, _8744 = _8799], theory(equality)).
% 0.36/1.33 cnf(4, plain, [-(ir(_11886))], clausify(simple_ir)).
% 0.36/1.33 cnf(5, plain, [iext(uri_rdf_type, _12038, _12084), -(icext(_12084, _12038))], clausify(rdfs_cext_def)).
% 0.36/1.33 cnf(6, plain, [-(iext(uri_rdf_type, _12038, _12084)), icext(_12084, _12038)], clausify(rdfs_cext_def)).
% 0.36/1.33 cnf(7, plain, [iext(uri_owl_sourceIndividual, _12390, _12441), -(icext(uri_owl_NegativePropertyAssertion, _12390))], clausify(owl_prop_sourceindividual_ext)).
% 0.36/1.33 cnf(8, plain, [iext(uri_owl_onProperty, _12805, _12856), -(ip(_12856))], clausify(owl_prop_onproperty_ext)).
% 0.36/1.33 cnf(9, plain, [iext(uri_owl_complementOf, _13220, _13289), -(ic(_13289))], clausify(owl_bool_complementof_class)).
% 0.36/1.33 cnf(10, plain, [iext(uri_owl_complementOf, _13220, _13289), icext(_13220, _13532), icext(_13289, _13532)], clausify(owl_bool_complementof_class)).
% 0.36/1.33 cnf(11, plain, [iext(uri_rdf_rest, _13952, uri_rdf_nil), iext(uri_rdf_first, _13952, _14032), iext(uri_owl_oneOf, _13871, _13952), icext(_13871, _14461), -(_14461 = _14032)], clausify(owl_enum_class_001)).
% 0.36/1.33 cnf(12, plain, [iext(uri_rdf_rest, _13952, uri_rdf_nil), iext(uri_rdf_first, _13952, _14032), iext(uri_owl_oneOf, _13871, _13952), -(icext(_13871, _14461)), _14461 = _14032], clausify(owl_enum_class_001)).
% 0.36/1.33 cnf(13, plain, [iext(uri_rdf_rest, _13952, uri_rdf_nil), iext(uri_rdf_first, _13952, _14032), -(iext(uri_owl_oneOf, _13871, _13952)), ic(_13871), icext(_13871, 1 ^ [_14032, _13952, _13871]), 1 ^ [_14032, _13952, _13871] = _14032], clausify(owl_enum_class_001)).
% 0.36/1.33 cnf(14, plain, [iext(uri_rdf_rest, _13952, uri_rdf_nil), iext(uri_rdf_first, _13952, _14032), -(iext(uri_owl_oneOf, _13871, _13952)), ic(_13871), -(icext(_13871, 1 ^ [_14032, _13952, _13871])), -(1 ^ [_14032, _13952, _13871] = _14032)], clausify(owl_enum_class_001)).
% 0.36/1.33 cnf(15, plain, [-(iext(uri_rdf_type, uri_ex_s, 4 ^ []))], clausify(testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(16, plain, [-(iext(uri_owl_onProperty, 4 ^ [], uri_ex_p))], clausify(testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(17, plain, [-(iext(uri_owl_allValuesFrom, 4 ^ [], 5 ^ []))], clausify(testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(18, plain, [-(iext(uri_owl_complementOf, 5 ^ [], 6 ^ []))], clausify(testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(19, plain, [-(iext(uri_owl_oneOf, 6 ^ [], 7 ^ []))], clausify(testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(20, plain, [-(iext(uri_rdf_first, 7 ^ [], uri_ex_o))], clausify(testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(21, plain, [-(iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil))], clausify(testcase_premise_fullish_010_Negative_Property_Assertions)).
% 0.36/1.33 cnf(22, plain, [-(iext(uri_owl_sourceIndividual, 3 ^ [_15913, _15826, _15738], _15826)), ir(_15826), ip(_15738), ir(_15913), -(iext(_15738, _15826, _15913))], clausify(owl_npa_object_fi)).
% 0.36/1.33 cnf(23, plain, [-(iext(uri_owl_assertionProperty, 3 ^ [_15913, _15826, _15738], _15738)), ir(_15826), ip(_15738), ir(_15913), -(iext(_15738, _15826, _15913))], clausify(owl_npa_object_fi)).
% 0.36/1.33 cnf(24, plain, [-(iext(uri_owl_targetIndividual, 3 ^ [_15913, _15826, _15738], _15913)), ir(_15826), ip(_15738), ir(_15913), -(iext(_15738, _15826, _15913))], clausify(owl_npa_object_fi)).
% 0.36/1.33 cnf(25, plain, [iext(uri_owl_onProperty, _14793, _14874), iext(uri_owl_allValuesFrom, _14793, _14954), icext(_14793, _15246), iext(_14874, _15246, _15369), -(icext(_14954, _15369))], clausify(owl_restrict_allvaluesfrom)).
% 0.36/1.33
% 0.36/1.33 cnf('1',plain,[iext(uri_owl_complementOf, 5 ^ [], 6 ^ []), icext(5 ^ [], uri_ex_o), icext(6 ^ [], uri_ex_o)],start(10,bind([[_13220, _13289, _13532], [5 ^ [], 6 ^ [], uri_ex_o]]))).
% 0.36/1.33 cnf('1.1',plain,[-(iext(uri_owl_complementOf, 5 ^ [], 6 ^ []))],extension(18)).
% 0.36/1.33 cnf('1.2',plain,[-(icext(5 ^ [], uri_ex_o)), iext(uri_owl_onProperty, 4 ^ [], uri_ex_p), iext(uri_owl_allValuesFrom, 4 ^ [], 5 ^ []), icext(4 ^ [], uri_ex_s), iext(uri_ex_p, uri_ex_s, uri_ex_o)],extension(25,bind([[_14954, _14793, _14874, _15246, _15369], [5 ^ [], 4 ^ [], uri_ex_p, uri_ex_s, uri_ex_o]]))).
% 0.36/1.33 cnf('1.2.1',plain,[-(iext(uri_owl_onProperty, 4 ^ [], uri_ex_p))],extension(16)).
% 0.36/1.33 cnf('1.2.2',plain,[-(iext(uri_owl_allValuesFrom, 4 ^ [], 5 ^ []))],extension(17)).
% 0.36/1.33 cnf('1.2.3',plain,[-(icext(4 ^ [], uri_ex_s)), iext(uri_rdf_type, uri_ex_s, 4 ^ [])],extension(5,bind([[_12038, _12084], [uri_ex_s, 4 ^ []]]))).
% 0.36/1.33 cnf('1.2.3.1',plain,[-(iext(uri_rdf_type, uri_ex_s, 4 ^ []))],extension(15)).
% 0.36/1.33 cnf('1.2.4',plain,[-(iext(uri_ex_p, uri_ex_s, uri_ex_o)), -(iext(uri_owl_sourceIndividual, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_s)), ir(uri_ex_s), ip(uri_ex_p), ir(uri_ex_o)],extension(22,bind([[_15826, _15738, _15913], [uri_ex_s, uri_ex_p, uri_ex_o]]))).
% 0.36/1.33 cnf('1.2.4.1',plain,[iext(uri_owl_sourceIndividual, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_s), iext(uri_rdf_type, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_owl_NegativePropertyAssertion), iext(uri_owl_assertionProperty, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_p), iext(uri_owl_targetIndividual, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_o)],extension(1,bind([[_18272], [3 ^ [uri_ex_o, uri_ex_s, uri_ex_p]]]))).
% 0.36/1.33 cnf('1.2.4.1.1',plain,[-(iext(uri_rdf_type, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_owl_NegativePropertyAssertion)), icext(uri_owl_NegativePropertyAssertion, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p])],extension(6,bind([[_12084, _12038], [uri_owl_NegativePropertyAssertion, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p]]]))).
% 0.36/1.33 cnf('1.2.4.1.1.1',plain,[-(icext(uri_owl_NegativePropertyAssertion, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p])), iext(uri_owl_sourceIndividual, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_s)],extension(7,bind([[_12390, _12441], [3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_s]]))).
% 0.36/1.33 cnf('1.2.4.1.1.1.1',plain,[-(iext(uri_owl_sourceIndividual, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_s))],reduction('1.2.4')).
% 0.36/1.33 cnf('1.2.4.1.2',plain,[-(iext(uri_owl_assertionProperty, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_p)), ir(uri_ex_s), ip(uri_ex_p), ir(uri_ex_o), -(iext(uri_ex_p, uri_ex_s, uri_ex_o))],extension(23,bind([[_15738, _15826, _15913], [uri_ex_p, uri_ex_s, uri_ex_o]]))).
% 0.36/1.33 cnf('1.2.4.1.2.1',plain,[-(ir(uri_ex_s))],extension(4,bind([[_11886], [uri_ex_s]]))).
% 0.36/1.33 cnf('1.2.4.1.2.2',plain,[-(ip(uri_ex_p)), iext(uri_owl_onProperty, 4 ^ [], uri_ex_p)],extension(8,bind([[_12805, _12856], [4 ^ [], uri_ex_p]]))).
% 0.36/1.33 cnf('1.2.4.1.2.2.1',plain,[-(iext(uri_owl_onProperty, 4 ^ [], uri_ex_p))],extension(16)).
% 0.36/1.33 cnf('1.2.4.1.2.3',plain,[-(ir(uri_ex_o))],extension(4,bind([[_11886], [uri_ex_o]]))).
% 0.36/1.33 cnf('1.2.4.1.2.4',plain,[iext(uri_ex_p, uri_ex_s, uri_ex_o)],reduction('1.2')).
% 0.36/1.33 cnf('1.2.4.1.3',plain,[-(iext(uri_owl_targetIndividual, 3 ^ [uri_ex_o, uri_ex_s, uri_ex_p], uri_ex_o)), ir(uri_ex_s), ip(uri_ex_p), ir(uri_ex_o), -(iext(uri_ex_p, uri_ex_s, uri_ex_o))],extension(24,bind([[_15738, _15826, _15913], [uri_ex_p, uri_ex_s, uri_ex_o]]))).
% 0.36/1.33 cnf('1.2.4.1.3.1',plain,[-(ir(uri_ex_s))],extension(4,bind([[_11886], [uri_ex_s]]))).
% 0.36/1.33 cnf('1.2.4.1.3.2',plain,[-(ip(uri_ex_p)), iext(uri_owl_onProperty, 4 ^ [], uri_ex_p)],extension(8,bind([[_12805, _12856], [4 ^ [], uri_ex_p]]))).
% 0.36/1.33 cnf('1.2.4.1.3.2.1',plain,[-(iext(uri_owl_onProperty, 4 ^ [], uri_ex_p))],extension(16)).
% 0.36/1.33 cnf('1.2.4.1.3.3',plain,[-(ir(uri_ex_o))],extension(4,bind([[_11886], [uri_ex_o]]))).
% 0.36/1.33 cnf('1.2.4.1.3.4',plain,[iext(uri_ex_p, uri_ex_s, uri_ex_o)],reduction('1.2')).
% 0.36/1.33 cnf('1.2.4.2',plain,[-(ir(uri_ex_s))],extension(4,bind([[_11886], [uri_ex_s]]))).
% 0.36/1.33 cnf('1.2.4.3',plain,[-(ip(uri_ex_p)), iext(uri_owl_onProperty, 4 ^ [], uri_ex_p)],extension(8,bind([[_12805, _12856], [4 ^ [], uri_ex_p]]))).
% 0.36/1.33 cnf('1.2.4.3.1',plain,[-(iext(uri_owl_onProperty, 4 ^ [], uri_ex_p))],extension(16)).
% 0.36/1.33 cnf('1.2.4.4',plain,[-(ir(uri_ex_o))],extension(4,bind([[_11886], [uri_ex_o]]))).
% 0.36/1.33 cnf('1.3',plain,[-(icext(6 ^ [], uri_ex_o)), iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil), iext(uri_rdf_first, 7 ^ [], uri_ex_o), iext(uri_owl_oneOf, 6 ^ [], 7 ^ []), uri_ex_o = uri_ex_o],extension(12,bind([[_13871, _13952, _14461, _14032], [6 ^ [], 7 ^ [], uri_ex_o, uri_ex_o]]))).
% 0.36/1.33 cnf('1.3.1',plain,[-(iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil))],extension(21)).
% 0.36/1.33 cnf('1.3.2',plain,[-(iext(uri_rdf_first, 7 ^ [], uri_ex_o))],extension(20)).
% 0.36/1.33 cnf('1.3.3',plain,[-(iext(uri_owl_oneOf, 6 ^ [], 7 ^ [])), iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil), iext(uri_rdf_first, 7 ^ [], uri_ex_o), ic(6 ^ []), icext(6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []]), 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []] = uri_ex_o],extension(13,bind([[_13952, _13871, _14032], [7 ^ [], 6 ^ [], uri_ex_o]]))).
% 0.36/1.33 cnf('1.3.3.1',plain,[-(iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil))],extension(21)).
% 0.36/1.33 cnf('1.3.3.2',plain,[-(iext(uri_rdf_first, 7 ^ [], uri_ex_o))],extension(20)).
% 0.36/1.33 cnf('1.3.3.3',plain,[-(ic(6 ^ [])), iext(uri_owl_complementOf, 5 ^ [], 6 ^ [])],extension(9,bind([[_13220, _13289], [5 ^ [], 6 ^ []]]))).
% 0.36/1.33 cnf('1.3.3.3.1',plain,[-(iext(uri_owl_complementOf, 5 ^ [], 6 ^ []))],extension(18)).
% 0.36/1.33 cnf('1.3.3.4',plain,[-(icext(6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []])), iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil), iext(uri_rdf_first, 7 ^ [], uri_ex_o), -(iext(uri_owl_oneOf, 6 ^ [], 7 ^ [])), ic(6 ^ []), -(1 ^ [uri_ex_o, 7 ^ [], 6 ^ []] = uri_ex_o)],extension(14,bind([[_13952, _13871, _14032], [7 ^ [], 6 ^ [], uri_ex_o]]))).
% 0.36/1.33 cnf('1.3.3.4.1',plain,[-(iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil))],extension(21)).
% 0.36/1.33 cnf('1.3.3.4.2',plain,[-(iext(uri_rdf_first, 7 ^ [], uri_ex_o))],extension(20)).
% 0.36/1.33 cnf('1.3.3.4.3',plain,[iext(uri_owl_oneOf, 6 ^ [], 7 ^ [])],reduction('1.3')).
% 0.36/1.33 cnf('1.3.3.4.4',plain,[-(ic(6 ^ []))],lemmata('1.3.3')).
% 0.36/1.33 cnf('1.3.3.4.5',plain,[1 ^ [uri_ex_o, 7 ^ [], 6 ^ []] = uri_ex_o, -(1 ^ [uri_ex_o, 7 ^ [], 6 ^ []] = uri_ex_o), uri_ex_o = uri_ex_o],extension(3,bind([[_8688, _8744, _8799], [1 ^ [uri_ex_o, 7 ^ [], 6 ^ []], uri_ex_o, uri_ex_o]]))).
% 0.36/1.33 cnf('1.3.3.4.5.1',plain,[1 ^ [uri_ex_o, 7 ^ [], 6 ^ []] = uri_ex_o, iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil), iext(uri_rdf_first, 7 ^ [], uri_ex_o), iext(uri_owl_oneOf, 6 ^ [], 7 ^ []), -(icext(6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []]))],extension(12,bind([[_14032, _13952, _13871, _14461], [uri_ex_o, 7 ^ [], 6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []]]]))).
% 0.36/1.33 cnf('1.3.3.4.5.1.1',plain,[-(iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil))],extension(21)).
% 0.36/1.33 cnf('1.3.3.4.5.1.2',plain,[-(iext(uri_rdf_first, 7 ^ [], uri_ex_o))],extension(20)).
% 0.36/1.33 cnf('1.3.3.4.5.1.3',plain,[-(iext(uri_owl_oneOf, 6 ^ [], 7 ^ []))],extension(19)).
% 0.36/1.33 cnf('1.3.3.4.5.1.4',plain,[icext(6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []])],reduction('1.3.3')).
% 0.36/1.33 cnf('1.3.3.4.5.2',plain,[-(uri_ex_o = uri_ex_o)],extension(2,bind([[_8256], [uri_ex_o]]))).
% 0.36/1.33 cnf('1.3.3.5',plain,[-(1 ^ [uri_ex_o, 7 ^ [], 6 ^ []] = uri_ex_o), iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil), iext(uri_rdf_first, 7 ^ [], uri_ex_o), iext(uri_owl_oneOf, 6 ^ [], 7 ^ []), icext(6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []])],extension(11,bind([[_14032, _13952, _13871, _14461], [uri_ex_o, 7 ^ [], 6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []]]]))).
% 0.36/1.33 cnf('1.3.3.5.1',plain,[-(iext(uri_rdf_rest, 7 ^ [], uri_rdf_nil))],extension(21)).
% 0.36/1.33 cnf('1.3.3.5.2',plain,[-(iext(uri_rdf_first, 7 ^ [], uri_ex_o))],extension(20)).
% 0.36/1.33 cnf('1.3.3.5.3',plain,[-(iext(uri_owl_oneOf, 6 ^ [], 7 ^ []))],extension(19)).
% 0.36/1.33 cnf('1.3.3.5.4',plain,[-(icext(6 ^ [], 1 ^ [uri_ex_o, 7 ^ [], 6 ^ []]))],lemmata('1.3.3')).
% 0.36/1.33 cnf('1.3.4',plain,[-(uri_ex_o = uri_ex_o)],extension(2,bind([[_8256], [uri_ex_o]]))).
% 0.36/1.33 %-----------------------------------------------------
% 0.36/1.33
% 0.36/1.34 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------