%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWB020+2 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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:49 EDT 2022
% Result : Theorem 178.94s 172.93s
% Output : Proof 178.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWB020+2 : TPTP v8.1.0. Released v5.2.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 1 07:40:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 178.94/172.93 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 178.94/172.93 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 178.94/172.94
% 178.94/172.94 %-----------------------------------------------------
% 178.94/172.94 fof(owl_eqdis_disjointwith, axiom, ! [_52493, _52496] : (iext(uri_owl_disjointWith, _52493, _52496) <=> ic(_52493) & ic(_52496) & ! [_52531] : ~ (icext(_52493, _52531) & icext(_52496, _52531))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_eqdis_disjointwith)).
% 178.94/172.94 fof(owl_rdfsext_subclassof, axiom, ! [_52765, _52768] : (iext(uri_rdfs_subClassOf, _52765, _52768) <=> ic(_52765) & ic(_52768) & ! [_52803] : (icext(_52765, _52803) => icext(_52768, _52803))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_rdfsext_subclassof)).
% 178.94/172.94 fof(owl_bool_unionof_class_003, axiom, ! [_53053, _53056, _53059, _53062, _53065, _53068, _53071] : (iext(uri_rdf_first, _53056, _53059) & iext(uri_rdf_rest, _53056, _53062) & iext(uri_rdf_first, _53062, _53065) & iext(uri_rdf_rest, _53062, _53068) & iext(uri_rdf_first, _53068, _53071) & iext(uri_rdf_rest, _53068, uri_rdf_nil) => (iext(uri_owl_unionOf, _53053, _53056) <=> ic(_53053) & ic(_53059) & ic(_53065) & ic(_53071) & ! [_53198] : (icext(_53053, _53198) <=> icext(_53059, _53198) | icext(_53065, _53198) | icext(_53071, _53198)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_bool_unionof_class_003)).
% 178.94/172.94 fof(owl_bool_intersectionof_class_002, axiom, ! [_53703, _53706, _53709, _53712, _53715] : (iext(uri_rdf_first, _53706, _53709) & iext(uri_rdf_rest, _53706, _53712) & iext(uri_rdf_first, _53712, _53715) & iext(uri_rdf_rest, _53712, uri_rdf_nil) => (iext(uri_owl_intersectionOf, _53703, _53706) <=> ic(_53703) & ic(_53709) & ic(_53715) & ! [_53809] : (icext(_53703, _53809) <=> icext(_53709, _53809) & icext(_53715, _53809)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_bool_intersectionof_class_002)).
% 178.94/172.94 fof(owl_bool_complementof_class, axiom, ! [_54220, _54223] : (iext(uri_owl_complementOf, _54220, _54223) => ic(_54220) & ic(_54223) & ! [_54258] : (icext(_54220, _54258) <=> ~ icext(_54223, _54258))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_bool_complementof_class)).
% 178.94/172.94 fof(testcase_conclusion_fullish_020_Logical_Complications, conjecture, iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_c3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_020_Logical_Complications)).
% 178.94/172.94 fof(testcase_premise_fullish_020_Logical_Complications, axiom, ? [_54598, _54601, _54604, _54607, _54610, _54613, _54616] : (iext(uri_owl_unionOf, uri_ex_c, _54604) & iext(uri_rdf_first, _54604, uri_ex_c1) & iext(uri_rdf_rest, _54604, _54607) & iext(uri_rdf_first, _54607, uri_ex_c2) & iext(uri_rdf_rest, _54607, _54610) & iext(uri_rdf_first, _54610, uri_ex_c3) & iext(uri_rdf_rest, _54610, uri_rdf_nil) & iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1) & iext(uri_rdfs_subClassOf, uri_ex_d, _54598) & iext(uri_owl_intersectionOf, _54598, _54613) & iext(uri_rdf_first, _54613, uri_ex_c) & iext(uri_rdf_rest, _54613, _54616) & iext(uri_rdf_first, _54616, _54601) & iext(uri_rdf_rest, _54616, uri_rdf_nil) & iext(uri_owl_complementOf, _54601, uri_ex_c2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94
% 178.94/172.94 cnf(1, plain, [-(18 ^ [_12376, _12307]), icext(_12307, _12619), icext(_12376, _12619)], clausify(owl_eqdis_disjointwith)).
% 178.94/172.94 cnf(2, plain, [-(18 ^ [_12376, _12307]), -(ic(_12307))], clausify(owl_eqdis_disjointwith)).
% 178.94/172.94 cnf(3, plain, [-(17 ^ [_11745, _11678]), icext(_11745, 16 ^ [_11745, _11678])], clausify(owl_rdfsext_subclassof)).
% 178.94/172.94 cnf(4, plain, [-(17 ^ [_11745, _11678]), -(icext(_11678, 16 ^ [_11745, _11678]))], clausify(owl_rdfsext_subclassof)).
% 178.94/172.94 cnf(5, plain, [-(15 ^ [_11745, _11678]), icext(_11678, _11986), -(icext(_11745, _11986))], clausify(owl_rdfsext_subclassof)).
% 178.94/172.94 cnf(6, plain, [-(10 ^ [_10027, _9876, _9724, _9571, _9417, _9262, _9106]), icext(_9106, _11097), -(icext(_9417, _11097)), -(icext(_9724, _11097)), -(icext(_10027, _11097))], clausify(owl_bool_unionof_class_003)).
% 178.94/172.94 cnf(7, plain, [-(10 ^ [_10027, _9876, _9724, _9571, _9417, _9262, _9106]), -(ic(_10027))], clausify(owl_bool_unionof_class_003)).
% 178.94/172.94 cnf(8, plain, [-(14 ^ [_10027, _9876, _9724, _9571, _9417, _9262, _9106]), iext(uri_owl_unionOf, _9106, _9262), 10 ^ [_10027, _9876, _9724, _9571, _9417, _9262, _9106]], clausify(owl_bool_unionof_class_003)).
% 178.94/172.94 cnf(9, plain, [-(3 ^ [_8642, _7871, _7753, _7634, _7514, _7393]), -(icext(_7871, _8642))], clausify(owl_bool_intersectionof_class_002)).
% 178.94/172.94 cnf(10, plain, [-(3 ^ [_8642, _7871, _7753, _7634, _7514, _7393]), -(icext(_7634, _8642))], clausify(owl_bool_intersectionof_class_002)).
% 178.94/172.94 cnf(11, plain, [-(4 ^ [_7871, _7753, _7634, _7514, _7393]), icext(_7393, _8642), 3 ^ [_8642, _7871, _7753, _7634, _7514, _7393]], clausify(owl_bool_intersectionof_class_002)).
% 178.94/172.94 cnf(12, plain, [-(8 ^ [_7871, _7753, _7634, _7514, _7393]), iext(uri_owl_intersectionOf, _7393, _7514), 4 ^ [_7871, _7753, _7634, _7514, _7393]], clausify(owl_bool_intersectionof_class_002)).
% 178.94/172.94 cnf(13, plain, [-(2 ^ [_6811, _6742]), icext(_6742, _7054), icext(_6811, _7054)], clausify(owl_bool_complementof_class)).
% 178.94/172.94 cnf(14, plain, [iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_c3)], clausify(testcase_conclusion_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(15, plain, [iext(uri_owl_complementOf, _6742, _6811), 2 ^ [_6811, _6742]], clausify(owl_bool_complementof_class)).
% 178.94/172.94 cnf(16, plain, [iext(uri_rdf_rest, _7753, uri_rdf_nil), iext(uri_rdf_first, _7753, _7871), iext(uri_rdf_rest, _7514, _7753), iext(uri_rdf_first, _7514, _7634), 8 ^ [_7871, _7753, _7634, _7514, _7393]], clausify(owl_bool_intersectionof_class_002)).
% 178.94/172.94 cnf(17, plain, [iext(uri_rdf_rest, _9876, uri_rdf_nil), iext(uri_rdf_first, _9876, _10027), iext(uri_rdf_rest, _9571, _9876), iext(uri_rdf_first, _9571, _9724), iext(uri_rdf_rest, _9262, _9571), iext(uri_rdf_first, _9262, _9417), 14 ^ [_10027, _9876, _9724, _9571, _9417, _9262, _9106]], clausify(owl_bool_unionof_class_003)).
% 178.94/172.94 cnf(18, plain, [iext(uri_rdfs_subClassOf, _11678, _11745), 15 ^ [_11745, _11678]], clausify(owl_rdfsext_subclassof)).
% 178.94/172.94 cnf(19, plain, [-(iext(uri_rdfs_subClassOf, _11678, _11745)), ic(_11678), ic(_11745), 17 ^ [_11745, _11678]], clausify(owl_rdfsext_subclassof)).
% 178.94/172.94 cnf(20, plain, [-(iext(uri_owl_unionOf, uri_ex_c, 23 ^ []))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(21, plain, [-(iext(uri_rdf_first, 23 ^ [], uri_ex_c1))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(22, plain, [-(iext(uri_rdf_rest, 23 ^ [], 24 ^ []))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(23, plain, [-(iext(uri_rdf_first, 24 ^ [], uri_ex_c2))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(24, plain, [-(iext(uri_rdf_rest, 24 ^ [], 25 ^ []))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(25, plain, [-(iext(uri_rdf_first, 25 ^ [], uri_ex_c3))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(26, plain, [-(iext(uri_rdf_rest, 25 ^ [], uri_rdf_nil))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(27, plain, [-(iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(28, plain, [-(iext(uri_rdfs_subClassOf, uri_ex_d, 21 ^ []))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(29, plain, [-(iext(uri_owl_intersectionOf, 21 ^ [], 26 ^ []))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(30, plain, [-(iext(uri_rdf_first, 26 ^ [], uri_ex_c))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(31, plain, [-(iext(uri_rdf_rest, 26 ^ [], 27 ^ []))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(32, plain, [-(iext(uri_rdf_first, 27 ^ [], 22 ^ []))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(33, plain, [-(iext(uri_rdf_rest, 27 ^ [], uri_rdf_nil))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(34, plain, [-(iext(uri_owl_complementOf, 22 ^ [], uri_ex_c2))], clausify(testcase_premise_fullish_020_Logical_Complications)).
% 178.94/172.94 cnf(35, plain, [iext(uri_owl_disjointWith, _12307, _12376), 18 ^ [_12376, _12307]], clausify(owl_eqdis_disjointwith)).
% 178.94/172.94
% 178.94/172.94 cnf('1',plain,[iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_c3)],start(14)).
% 178.94/172.94 cnf('1.1',plain,[-(iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_c3)), ic(uri_ex_d), ic(uri_ex_c3), 17 ^ [uri_ex_c3, uri_ex_d]],extension(19,bind([[_11745, _11678], [uri_ex_c3, uri_ex_d]]))).
% 178.94/172.94 cnf('1.1.1',plain,[-(ic(uri_ex_d)), -(18 ^ [uri_ex_c1, uri_ex_d])],extension(2,bind([[_12376, _12307], [uri_ex_c1, uri_ex_d]]))).
% 178.94/172.94 cnf('1.1.1.1',plain,[18 ^ [uri_ex_c1, uri_ex_d], iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1)],extension(35,bind([[_12307, _12376], [uri_ex_d, uri_ex_c1]]))).
% 178.94/172.94 cnf('1.1.1.1.1',plain,[-(iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1))],extension(27)).
% 178.94/172.94 cnf('1.1.2',plain,[-(ic(uri_ex_c3)), -(10 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c])],extension(7,bind([[_10027, _9876, _9724, _9571, _9417, _9262, _9106], [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c]]))).
% 178.94/172.94 cnf('1.1.2.1',plain,[10 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c], -(14 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c]), iext(uri_owl_unionOf, uri_ex_c, 23 ^ [])],extension(8,bind([[_10027, _9876, _9724, _9571, _9417, _9106, _9262], [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, uri_ex_c, 23 ^ []]]))).
% 178.94/172.94 cnf('1.1.2.1.1',plain,[14 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c], iext(uri_rdf_rest, 25 ^ [], uri_rdf_nil), iext(uri_rdf_first, 25 ^ [], uri_ex_c3), iext(uri_rdf_rest, 24 ^ [], 25 ^ []), iext(uri_rdf_first, 24 ^ [], uri_ex_c2), iext(uri_rdf_rest, 23 ^ [], 24 ^ []), iext(uri_rdf_first, 23 ^ [], uri_ex_c1)],extension(17,bind([[_9106, _10027, _9876, _9724, _9571, _9262, _9417], [uri_ex_c, uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], 23 ^ [], uri_ex_c1]]))).
% 178.94/172.94 cnf('1.1.2.1.1.1',plain,[-(iext(uri_rdf_rest, 25 ^ [], uri_rdf_nil))],extension(26)).
% 178.94/172.94 cnf('1.1.2.1.1.2',plain,[-(iext(uri_rdf_first, 25 ^ [], uri_ex_c3))],extension(25)).
% 178.94/172.94 cnf('1.1.2.1.1.3',plain,[-(iext(uri_rdf_rest, 24 ^ [], 25 ^ []))],extension(24)).
% 178.94/172.94 cnf('1.1.2.1.1.4',plain,[-(iext(uri_rdf_first, 24 ^ [], uri_ex_c2))],extension(23)).
% 178.94/172.94 cnf('1.1.2.1.1.5',plain,[-(iext(uri_rdf_rest, 23 ^ [], 24 ^ []))],extension(22)).
% 178.94/172.94 cnf('1.1.2.1.1.6',plain,[-(iext(uri_rdf_first, 23 ^ [], uri_ex_c1))],extension(21)).
% 178.94/172.94 cnf('1.1.2.1.2',plain,[-(iext(uri_owl_unionOf, uri_ex_c, 23 ^ []))],extension(20)).
% 178.94/172.94 cnf('1.1.3',plain,[-(17 ^ [uri_ex_c3, uri_ex_d]), icext(uri_ex_c3, 16 ^ [uri_ex_c3, uri_ex_d])],extension(3,bind([[_11745, _11678], [uri_ex_c3, uri_ex_d]]))).
% 178.94/172.94 cnf('1.1.3.1',plain,[-(icext(uri_ex_c3, 16 ^ [uri_ex_c3, uri_ex_d])), -(10 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c]), icext(uri_ex_c, 16 ^ [uri_ex_c3, uri_ex_d]), -(icext(uri_ex_c1, 16 ^ [uri_ex_c3, uri_ex_d])), -(icext(uri_ex_c2, 16 ^ [uri_ex_c3, uri_ex_d]))],extension(6,bind([[_10027, _9876, _9571, _9262, _9106, _9417, _9724, _11097], [uri_ex_c3, 25 ^ [], 24 ^ [], 23 ^ [], uri_ex_c, uri_ex_c1, uri_ex_c2, 16 ^ [uri_ex_c3, uri_ex_d]]]))).
% 178.94/172.94 cnf('1.1.3.1.1',plain,[10 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c], -(14 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c]), iext(uri_owl_unionOf, uri_ex_c, 23 ^ [])],extension(8,bind([[_10027, _9876, _9724, _9571, _9417, _9106, _9262], [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, uri_ex_c, 23 ^ []]]))).
% 178.94/172.94 cnf('1.1.3.1.1.1',plain,[14 ^ [uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], uri_ex_c1, 23 ^ [], uri_ex_c], iext(uri_rdf_rest, 25 ^ [], uri_rdf_nil), iext(uri_rdf_first, 25 ^ [], uri_ex_c3), iext(uri_rdf_rest, 24 ^ [], 25 ^ []), iext(uri_rdf_first, 24 ^ [], uri_ex_c2), iext(uri_rdf_rest, 23 ^ [], 24 ^ []), iext(uri_rdf_first, 23 ^ [], uri_ex_c1)],extension(17,bind([[_9106, _10027, _9876, _9724, _9571, _9262, _9417], [uri_ex_c, uri_ex_c3, 25 ^ [], uri_ex_c2, 24 ^ [], 23 ^ [], uri_ex_c1]]))).
% 178.94/172.94 cnf('1.1.3.1.1.1.1',plain,[-(iext(uri_rdf_rest, 25 ^ [], uri_rdf_nil))],extension(26)).
% 178.94/172.94 cnf('1.1.3.1.1.1.2',plain,[-(iext(uri_rdf_first, 25 ^ [], uri_ex_c3))],extension(25)).
% 178.94/172.94 cnf('1.1.3.1.1.1.3',plain,[-(iext(uri_rdf_rest, 24 ^ [], 25 ^ []))],extension(24)).
% 178.94/172.94 cnf('1.1.3.1.1.1.4',plain,[-(iext(uri_rdf_first, 24 ^ [], uri_ex_c2))],extension(23)).
% 178.94/172.94 cnf('1.1.3.1.1.1.5',plain,[-(iext(uri_rdf_rest, 23 ^ [], 24 ^ []))],extension(22)).
% 178.94/172.94 cnf('1.1.3.1.1.1.6',plain,[-(iext(uri_rdf_first, 23 ^ [], uri_ex_c1))],extension(21)).
% 178.94/172.94 cnf('1.1.3.1.1.2',plain,[-(iext(uri_owl_unionOf, uri_ex_c, 23 ^ []))],extension(20)).
% 178.94/172.94 cnf('1.1.3.1.2',plain,[-(icext(uri_ex_c, 16 ^ [uri_ex_c3, uri_ex_d])), -(3 ^ [16 ^ [uri_ex_c3, uri_ex_d], 22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []])],extension(10,bind([[_8642, _7871, _7753, _7634, _7514, _7393], [16 ^ [uri_ex_c3, uri_ex_d], 22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []]]))).
% 178.94/172.94 cnf('1.1.3.1.2.1',plain,[3 ^ [16 ^ [uri_ex_c3, uri_ex_d], 22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []], -(4 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []]), icext(21 ^ [], 16 ^ [uri_ex_c3, uri_ex_d])],extension(11,bind([[_7871, _7753, _7634, _7514, _7393, _8642], [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ [], 16 ^ [uri_ex_c3, uri_ex_d]]]))).
% 178.94/172.94 cnf('1.1.3.1.2.1.1',plain,[4 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []], -(8 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []]), iext(uri_owl_intersectionOf, 21 ^ [], 26 ^ [])],extension(12,bind([[_7871, _7753, _7634, _7393, _7514], [22 ^ [], 27 ^ [], uri_ex_c, 21 ^ [], 26 ^ []]]))).
% 178.94/172.94 cnf('1.1.3.1.2.1.1.1',plain,[8 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []], iext(uri_rdf_rest, 27 ^ [], uri_rdf_nil), iext(uri_rdf_first, 27 ^ [], 22 ^ []), iext(uri_rdf_rest, 26 ^ [], 27 ^ []), iext(uri_rdf_first, 26 ^ [], uri_ex_c)],extension(16,bind([[_7393, _7871, _7753, _7514, _7634], [21 ^ [], 22 ^ [], 27 ^ [], 26 ^ [], uri_ex_c]]))).
% 178.94/172.94 cnf('1.1.3.1.2.1.1.1.1',plain,[-(iext(uri_rdf_rest, 27 ^ [], uri_rdf_nil))],extension(33)).
% 178.94/172.94 cnf('1.1.3.1.2.1.1.1.2',plain,[-(iext(uri_rdf_first, 27 ^ [], 22 ^ []))],extension(32)).
% 178.94/172.94 cnf('1.1.3.1.2.1.1.1.3',plain,[-(iext(uri_rdf_rest, 26 ^ [], 27 ^ []))],extension(31)).
% 178.94/172.94 cnf('1.1.3.1.2.1.1.1.4',plain,[-(iext(uri_rdf_first, 26 ^ [], uri_ex_c))],extension(30)).
% 178.94/172.94 cnf('1.1.3.1.2.1.1.2',plain,[-(iext(uri_owl_intersectionOf, 21 ^ [], 26 ^ []))],extension(29)).
% 178.94/172.94 cnf('1.1.3.1.2.1.2',plain,[-(icext(21 ^ [], 16 ^ [uri_ex_c3, uri_ex_d])), -(15 ^ [21 ^ [], uri_ex_d]), icext(uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d])],extension(5,bind([[_11745, _11678, _11986], [21 ^ [], uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d]]]))).
% 178.94/172.94 cnf('1.1.3.1.2.1.2.1',plain,[15 ^ [21 ^ [], uri_ex_d], iext(uri_rdfs_subClassOf, uri_ex_d, 21 ^ [])],extension(18,bind([[_11678, _11745], [uri_ex_d, 21 ^ []]]))).
% 178.94/172.94 cnf('1.1.3.1.2.1.2.1.1',plain,[-(iext(uri_rdfs_subClassOf, uri_ex_d, 21 ^ []))],extension(28)).
% 178.94/172.94 cnf('1.1.3.1.2.1.2.2',plain,[-(icext(uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d])), -(17 ^ [uri_ex_c3, uri_ex_d])],extension(4,bind([[_11745, _11678], [uri_ex_c3, uri_ex_d]]))).
% 178.94/172.94 cnf('1.1.3.1.2.1.2.2.1',plain,[17 ^ [uri_ex_c3, uri_ex_d]],reduction('1.1')).
% 178.94/172.94 cnf('1.1.3.1.3',plain,[icext(uri_ex_c1, 16 ^ [uri_ex_c3, uri_ex_d]), -(18 ^ [uri_ex_c1, uri_ex_d]), icext(uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d])],extension(1,bind([[_12376, _12307, _12619], [uri_ex_c1, uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d]]]))).
% 178.94/172.94 cnf('1.1.3.1.3.1',plain,[18 ^ [uri_ex_c1, uri_ex_d], iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1)],extension(35,bind([[_12307, _12376], [uri_ex_d, uri_ex_c1]]))).
% 178.94/172.94 cnf('1.1.3.1.3.1.1',plain,[-(iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1))],extension(27)).
% 178.94/172.94 cnf('1.1.3.1.3.2',plain,[-(icext(uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d])), -(17 ^ [uri_ex_c3, uri_ex_d])],extension(4,bind([[_11745, _11678], [uri_ex_c3, uri_ex_d]]))).
% 178.94/172.94 cnf('1.1.3.1.3.2.1',plain,[17 ^ [uri_ex_c3, uri_ex_d]],reduction('1.1')).
% 178.94/172.94 cnf('1.1.3.1.4',plain,[icext(uri_ex_c2, 16 ^ [uri_ex_c3, uri_ex_d]), -(2 ^ [uri_ex_c2, 22 ^ []]), icext(22 ^ [], 16 ^ [uri_ex_c3, uri_ex_d])],extension(13,bind([[_6811, _6742, _7054], [uri_ex_c2, 22 ^ [], 16 ^ [uri_ex_c3, uri_ex_d]]]))).
% 178.94/172.94 cnf('1.1.3.1.4.1',plain,[2 ^ [uri_ex_c2, 22 ^ []], iext(uri_owl_complementOf, 22 ^ [], uri_ex_c2)],extension(15,bind([[_6742, _6811], [22 ^ [], uri_ex_c2]]))).
% 178.94/172.94 cnf('1.1.3.1.4.1.1',plain,[-(iext(uri_owl_complementOf, 22 ^ [], uri_ex_c2))],extension(34)).
% 178.94/172.94 cnf('1.1.3.1.4.2',plain,[-(icext(22 ^ [], 16 ^ [uri_ex_c3, uri_ex_d])), -(3 ^ [16 ^ [uri_ex_c3, uri_ex_d], 22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []])],extension(9,bind([[_8642, _7871, _7753, _7634, _7514, _7393], [16 ^ [uri_ex_c3, uri_ex_d], 22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []]]))).
% 178.94/172.94 cnf('1.1.3.1.4.2.1',plain,[3 ^ [16 ^ [uri_ex_c3, uri_ex_d], 22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []], -(4 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []]), icext(21 ^ [], 16 ^ [uri_ex_c3, uri_ex_d])],extension(11,bind([[_7871, _7753, _7634, _7514, _7393, _8642], [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ [], 16 ^ [uri_ex_c3, uri_ex_d]]]))).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.1',plain,[4 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []], -(8 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []]), iext(uri_owl_intersectionOf, 21 ^ [], 26 ^ [])],extension(12,bind([[_7871, _7753, _7634, _7393, _7514], [22 ^ [], 27 ^ [], uri_ex_c, 21 ^ [], 26 ^ []]]))).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.1.1',plain,[8 ^ [22 ^ [], 27 ^ [], uri_ex_c, 26 ^ [], 21 ^ []], iext(uri_rdf_rest, 27 ^ [], uri_rdf_nil), iext(uri_rdf_first, 27 ^ [], 22 ^ []), iext(uri_rdf_rest, 26 ^ [], 27 ^ []), iext(uri_rdf_first, 26 ^ [], uri_ex_c)],extension(16,bind([[_7393, _7871, _7753, _7514, _7634], [21 ^ [], 22 ^ [], 27 ^ [], 26 ^ [], uri_ex_c]]))).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.1.1.1',plain,[-(iext(uri_rdf_rest, 27 ^ [], uri_rdf_nil))],extension(33)).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.1.1.2',plain,[-(iext(uri_rdf_first, 27 ^ [], 22 ^ []))],extension(32)).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.1.1.3',plain,[-(iext(uri_rdf_rest, 26 ^ [], 27 ^ []))],extension(31)).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.1.1.4',plain,[-(iext(uri_rdf_first, 26 ^ [], uri_ex_c))],extension(30)).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.1.2',plain,[-(iext(uri_owl_intersectionOf, 21 ^ [], 26 ^ []))],extension(29)).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.2',plain,[-(icext(21 ^ [], 16 ^ [uri_ex_c3, uri_ex_d])), -(15 ^ [21 ^ [], uri_ex_d]), icext(uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d])],extension(5,bind([[_11745, _11678, _11986], [21 ^ [], uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d]]]))).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.2.1',plain,[15 ^ [21 ^ [], uri_ex_d], iext(uri_rdfs_subClassOf, uri_ex_d, 21 ^ [])],extension(18,bind([[_11678, _11745], [uri_ex_d, 21 ^ []]]))).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.2.1.1',plain,[-(iext(uri_rdfs_subClassOf, uri_ex_d, 21 ^ []))],extension(28)).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.2.2',plain,[-(icext(uri_ex_d, 16 ^ [uri_ex_c3, uri_ex_d])), -(17 ^ [uri_ex_c3, uri_ex_d])],extension(4,bind([[_11745, _11678], [uri_ex_c3, uri_ex_d]]))).
% 178.94/172.94 cnf('1.1.3.1.4.2.1.2.2.1',plain,[17 ^ [uri_ex_c3, uri_ex_d]],reduction('1.1')).
% 178.94/172.94 %-----------------------------------------------------
% 178.94/172.94
% 178.94/172.94 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------