%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWB057+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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:55 EDT 2022
% Result : Theorem 67.19s 65.68s
% Output : Proof 67.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB057+1 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n027.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 09:55:33 EDT 2022
% 0.12/0.33 % CPUTime :
% 67.19/65.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.26/65.69 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.26/65.69
% 67.26/65.69 %-----------------------------------------------------
% 67.26/65.69 fof(owl_bool_complementof_class, axiom, ! [_243805, _243808] : (iext(uri_owl_complementOf, _243805, _243808) => ic(_243805) & ic(_243808) & ! [_243843] : (icext(_243805, _243843) <=> ~ icext(_243808, _243843))), file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_bool_complementof_class)).
% 67.26/65.69 fof(conclusion_rdfbased_sem_eqdis_different_ext, conjecture, iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conclusion_rdfbased_sem_eqdis_different_ext)).
% 67.26/65.69 fof(premise_rdfbased_sem_eqdis_different_ext, axiom, ? [_244286] : (iext(uri_rdf_type, uri_ex_u, _244286) & iext(uri_owl_complementOf, _244286, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', premise_rdfbased_sem_eqdis_different_ext)).
% 67.26/65.69 fof(rdfs_cext_def, axiom, ! [_244519, _244522] : (iext(uri_rdf_type, _244519, _244522) <=> icext(_244522, _244519)), file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', rdfs_cext_def)).
% 67.26/65.69 fof(owl_eqdis_differentfrom, axiom, ! [_245037, _245040] : (iext(uri_owl_differentFrom, _245037, _245040) <=> (! _245037) = _245040), file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_eqdis_differentfrom)).
% 67.26/65.69
% 67.26/65.69 cnf(1, plain, [-(60 ^ [_26524, _26523]), icext(_26523, _26533), icext(_26524, _26533)], clausify(owl_bool_complementof_class)).
% 67.26/65.69 cnf(2, plain, [iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)], clausify(conclusion_rdfbased_sem_eqdis_different_ext)).
% 67.26/65.69 cnf(3, plain, [-(_21129 = _21129)], theory(equality)).
% 67.26/65.69 cnf(4, plain, [_21143 = _21144, -(_21144 = _21143)], theory(equality)).
% 67.26/65.69 cnf(5, plain, [-(icext(_21244, _21246)), icext(_21243, _21245), _21243 = _21244, _21245 = _21246], theory(equality)).
% 67.26/65.69 cnf(6, plain, [-(iext(uri_rdf_type, uri_ex_u, 504 ^ []))], clausify(premise_rdfbased_sem_eqdis_different_ext)).
% 67.26/65.69 cnf(7, plain, [-(iext(uri_owl_complementOf, 504 ^ [], uri_ex_c))], clausify(premise_rdfbased_sem_eqdis_different_ext)).
% 67.26/65.69 cnf(8, plain, [-(iext(uri_rdf_type, uri_ex_w, uri_ex_c))], clausify(premise_rdfbased_sem_eqdis_different_ext)).
% 67.26/65.69 cnf(9, plain, [iext(uri_rdf_type, _21977, _21978), -(icext(_21978, _21977))], clausify(rdfs_cext_def)).
% 67.26/65.69 cnf(10, plain, [iext(uri_owl_complementOf, _26523, _26524), 60 ^ [_26524, _26523]], clausify(owl_bool_complementof_class)).
% 67.26/65.69 cnf(11, plain, [-(iext(uri_owl_differentFrom, _33040, _33041)), -(_33040 = _33041)], clausify(owl_eqdis_differentfrom)).
% 67.26/65.69
% 67.26/65.69 cnf('1',plain,[iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)],start(2)).
% 67.26/65.69 cnf('1.1',plain,[-(iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)), -(uri_ex_w = uri_ex_u)],extension(11,bind([[_33040, _33041], [uri_ex_w, uri_ex_u]]))).
% 67.26/65.69 cnf('1.1.1',plain,[uri_ex_w = uri_ex_u, -(uri_ex_u = uri_ex_w)],extension(4,bind([[_21144, _21143], [uri_ex_u, uri_ex_w]]))).
% 67.26/65.69 cnf('1.1.1.1',plain,[uri_ex_u = uri_ex_w, -(icext(504 ^ [], uri_ex_w)), icext(504 ^ [], uri_ex_u), 504 ^ [] = 504 ^ []],extension(5,bind([[_21246, _21245, _21243, _21244], [uri_ex_w, uri_ex_u, 504 ^ [], 504 ^ []]]))).
% 67.26/65.69 cnf('1.1.1.1.1',plain,[icext(504 ^ [], uri_ex_w), -(60 ^ [uri_ex_c, 504 ^ []]), icext(uri_ex_c, uri_ex_w)],extension(1,bind([[_26523, _26524, _26533], [504 ^ [], uri_ex_c, uri_ex_w]]))).
% 67.26/65.69 cnf('1.1.1.1.1.1',plain,[60 ^ [uri_ex_c, 504 ^ []], iext(uri_owl_complementOf, 504 ^ [], uri_ex_c)],extension(10,bind([[_26523, _26524], [504 ^ [], uri_ex_c]]))).
% 67.26/65.69 cnf('1.1.1.1.1.1.1',plain,[-(iext(uri_owl_complementOf, 504 ^ [], uri_ex_c))],extension(7)).
% 67.26/65.69 cnf('1.1.1.1.1.2',plain,[-(icext(uri_ex_c, uri_ex_w)), iext(uri_rdf_type, uri_ex_w, uri_ex_c)],extension(9,bind([[_21977, _21978], [uri_ex_w, uri_ex_c]]))).
% 67.26/65.69 cnf('1.1.1.1.1.2.1',plain,[-(iext(uri_rdf_type, uri_ex_w, uri_ex_c))],extension(8)).
% 67.26/65.69 cnf('1.1.1.1.2',plain,[-(icext(504 ^ [], uri_ex_u)), icext(504 ^ [], uri_ex_u), 504 ^ [] = 504 ^ [], uri_ex_u = uri_ex_u],extension(5,bind([[_21243, _21244, _21245, _21246], [504 ^ [], 504 ^ [], uri_ex_u, uri_ex_u]]))).
% 67.26/65.69 cnf('1.1.1.1.2.1',plain,[-(icext(504 ^ [], uri_ex_u)), iext(uri_rdf_type, uri_ex_u, 504 ^ [])],extension(9,bind([[_21977, _21978], [uri_ex_u, 504 ^ []]]))).
% 67.26/65.69 cnf('1.1.1.1.2.1.1',plain,[-(iext(uri_rdf_type, uri_ex_u, 504 ^ []))],extension(6)).
% 67.26/65.69 cnf('1.1.1.1.2.2',plain,[-(504 ^ [] = 504 ^ [])],extension(3,bind([[_21129], [504 ^ []]]))).
% 67.26/65.69 cnf('1.1.1.1.2.3',plain,[-(uri_ex_u = uri_ex_u)],extension(3,bind([[_21129], [uri_ex_u]]))).
% 67.26/65.69 cnf('1.1.1.1.3',plain,[-(504 ^ [] = 504 ^ [])],extension(3,bind([[_21129], [504 ^ []]]))).
% 67.26/65.69 %-----------------------------------------------------
% 67.26/65.70
% 67.26/65.70 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------