%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWB056+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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 35.58s 34.61s
% Output : Proof 35.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWB056+1 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n017.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Wed Jun 1 02:39:56 EDT 2022
% 0.13/0.35 % CPUTime :
% 35.58/34.61 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.58/34.62 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.58/34.62
% 35.58/34.62 %-----------------------------------------------------
% 35.58/34.62 fof(owl_enum_class_002, axiom, ! [_246889, _246892, _246895, _246898, _246901] : (iext(uri_rdf_first, _246892, _246895) & iext(uri_rdf_rest, _246892, _246898) & iext(uri_rdf_first, _246898, _246901) & iext(uri_rdf_rest, _246898, uri_rdf_nil) => (iext(uri_owl_oneOf, _246889, _246892) <=> ic(_246889) & ! [_246981] : (icext(_246889, _246981) <=> _246981 = _246895 | _246981 = _246901))), file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax', owl_enum_class_002)).
% 35.58/34.62 fof(conclusion_rdfbased_sem_enum_inst_closed, conjecture, iext(uri_owl_sameAs, uri_ex_z, uri_ex_y), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conclusion_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 fof(premise_rdfbased_sem_enum_inst_closed, axiom, ? [_247657, _247660] : (iext(uri_rdf_type, uri_ex_z, uri_ex_e) & iext(uri_owl_differentFrom, uri_ex_z, uri_ex_x) & iext(uri_owl_oneOf, uri_ex_e, _247657) & iext(uri_rdf_first, _247657, uri_ex_x) & iext(uri_rdf_rest, _247657, _247660) & iext(uri_rdf_first, _247660, uri_ex_y) & iext(uri_rdf_rest, _247660, uri_rdf_nil)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 fof(rdfs_cext_def, axiom, ! [_248089, _248092] : (iext(uri_rdf_type, _248089, _248092) <=> icext(_248092, _248089)), file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax', rdfs_cext_def)).
% 35.58/34.62 fof(owl_eqdis_differentfrom, axiom, ! [_248606, _248609] : (iext(uri_owl_differentFrom, _248606, _248609) <=> (! _248606) = _248609), file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax', owl_eqdis_differentfrom)).
% 35.58/34.62 fof(owl_eqdis_sameas, axiom, ! [_248777, _248780] : (iext(uri_owl_sameAs, _248777, _248780) <=> _248777 = _248780), file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax', owl_eqdis_sameas)).
% 35.58/34.62
% 35.58/34.62 cnf(1, plain, [-(111 ^ [_27973, _27972, _27971, _27970, _27969]), icext(_27969, _28005), -(_28005 = _27971), -(_28005 = _27973)], clausify(owl_enum_class_002)).
% 35.58/34.62 cnf(2, plain, [-(115 ^ [_27973, _27972, _27971, _27970, _27969]), iext(uri_owl_oneOf, _27969, _27970), 111 ^ [_27973, _27972, _27971, _27970, _27969]], clausify(owl_enum_class_002)).
% 35.58/34.62 cnf(3, plain, [iext(uri_owl_sameAs, uri_ex_z, uri_ex_y)], clausify(conclusion_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(4, plain, [-(_21163 = _21163)], theory(equality)).
% 35.58/34.62 cnf(5, plain, [-(_21203 = _21205), _21203 = _21204, _21204 = _21205], theory(equality)).
% 35.58/34.62 cnf(6, plain, [-(icext(_21278, _21280)), icext(_21277, _21279), _21277 = _21278, _21279 = _21280], theory(equality)).
% 35.58/34.62 cnf(7, plain, [-(iext(uri_rdf_type, uri_ex_z, uri_ex_e))], clausify(premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(8, plain, [-(iext(uri_owl_differentFrom, uri_ex_z, uri_ex_x))], clausify(premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(9, plain, [-(iext(uri_owl_oneOf, uri_ex_e, 504 ^ []))], clausify(premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(10, plain, [-(iext(uri_rdf_first, 504 ^ [], uri_ex_x))], clausify(premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(11, plain, [-(iext(uri_rdf_rest, 504 ^ [], 505 ^ []))], clausify(premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(12, plain, [-(iext(uri_rdf_first, 505 ^ [], uri_ex_y))], clausify(premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(13, plain, [-(iext(uri_rdf_rest, 505 ^ [], uri_rdf_nil))], clausify(premise_rdfbased_sem_enum_inst_closed)).
% 35.58/34.62 cnf(14, plain, [iext(uri_rdf_type, _22011, _22012), -(icext(_22012, _22011))], clausify(rdfs_cext_def)).
% 35.58/34.62 cnf(15, plain, [iext(uri_rdf_rest, _27972, uri_rdf_nil), iext(uri_rdf_first, _27972, _27973), iext(uri_rdf_rest, _27970, _27972), iext(uri_rdf_first, _27970, _27971), 115 ^ [_27973, _27972, _27971, _27970, _27969]], clausify(owl_enum_class_002)).
% 35.58/34.62 cnf(16, plain, [iext(uri_owl_differentFrom, _33074, _33075), _33074 = _33075], clausify(owl_eqdis_differentfrom)).
% 35.58/34.62 cnf(17, plain, [-(iext(uri_owl_sameAs, _33736, _33737)), _33736 = _33737], clausify(owl_eqdis_sameas)).
% 35.58/34.62
% 35.58/34.62 cnf('1',plain,[iext(uri_owl_sameAs, uri_ex_z, uri_ex_y)],start(3)).
% 35.58/34.62 cnf('1.1',plain,[-(iext(uri_owl_sameAs, uri_ex_z, uri_ex_y)), uri_ex_z = uri_ex_y],extension(17,bind([[_33736, _33737], [uri_ex_z, uri_ex_y]]))).
% 35.58/34.62 cnf('1.1.1',plain,[-(uri_ex_z = uri_ex_y), -(111 ^ [uri_ex_y, 505 ^ [], uri_ex_x, 504 ^ [], uri_ex_e]), icext(uri_ex_e, uri_ex_z), -(uri_ex_z = uri_ex_x)],extension(1,bind([[_27973, _27972, _27970, _27969, _28005, _27971], [uri_ex_y, 505 ^ [], 504 ^ [], uri_ex_e, uri_ex_z, uri_ex_x]]))).
% 35.58/34.62 cnf('1.1.1.1',plain,[111 ^ [uri_ex_y, 505 ^ [], uri_ex_x, 504 ^ [], uri_ex_e], -(115 ^ [uri_ex_y, 505 ^ [], uri_ex_x, 504 ^ [], uri_ex_e]), iext(uri_owl_oneOf, uri_ex_e, 504 ^ [])],extension(2,bind([[_27973, _27972, _27971, _27969, _27970], [uri_ex_y, 505 ^ [], uri_ex_x, uri_ex_e, 504 ^ []]]))).
% 35.58/34.62 cnf('1.1.1.1.1',plain,[115 ^ [uri_ex_y, 505 ^ [], uri_ex_x, 504 ^ [], uri_ex_e], iext(uri_rdf_rest, 505 ^ [], uri_rdf_nil), iext(uri_rdf_first, 505 ^ [], uri_ex_y), iext(uri_rdf_rest, 504 ^ [], 505 ^ []), iext(uri_rdf_first, 504 ^ [], uri_ex_x)],extension(15,bind([[_27969, _27973, _27972, _27970, _27971], [uri_ex_e, uri_ex_y, 505 ^ [], 504 ^ [], uri_ex_x]]))).
% 35.58/34.62 cnf('1.1.1.1.1.1',plain,[-(iext(uri_rdf_rest, 505 ^ [], uri_rdf_nil))],extension(13)).
% 35.58/34.62 cnf('1.1.1.1.1.2',plain,[-(iext(uri_rdf_first, 505 ^ [], uri_ex_y))],extension(12)).
% 35.58/34.62 cnf('1.1.1.1.1.3',plain,[-(iext(uri_rdf_rest, 504 ^ [], 505 ^ []))],extension(11)).
% 35.58/34.62 cnf('1.1.1.1.1.4',plain,[-(iext(uri_rdf_first, 504 ^ [], uri_ex_x))],extension(10)).
% 35.58/34.62 cnf('1.1.1.1.2',plain,[-(iext(uri_owl_oneOf, uri_ex_e, 504 ^ []))],extension(9)).
% 35.58/34.62 cnf('1.1.1.2',plain,[-(icext(uri_ex_e, uri_ex_z)), icext(uri_ex_e, uri_ex_z), uri_ex_e = uri_ex_e, uri_ex_z = uri_ex_z],extension(6,bind([[_21277, _21278, _21279, _21280], [uri_ex_e, uri_ex_e, uri_ex_z, uri_ex_z]]))).
% 35.58/34.62 cnf('1.1.1.2.1',plain,[-(icext(uri_ex_e, uri_ex_z)), iext(uri_rdf_type, uri_ex_z, uri_ex_e)],extension(14,bind([[_22011, _22012], [uri_ex_z, uri_ex_e]]))).
% 35.58/34.62 cnf('1.1.1.2.1.1',plain,[-(iext(uri_rdf_type, uri_ex_z, uri_ex_e))],extension(7)).
% 35.58/34.62 cnf('1.1.1.2.2',plain,[-(uri_ex_e = uri_ex_e)],extension(4,bind([[_21163], [uri_ex_e]]))).
% 35.58/34.62 cnf('1.1.1.2.3',plain,[-(uri_ex_z = uri_ex_z)],extension(4,bind([[_21163], [uri_ex_z]]))).
% 35.58/34.62 cnf('1.1.1.3',plain,[uri_ex_z = uri_ex_x, -(uri_ex_z = uri_ex_x), uri_ex_z = uri_ex_z],extension(5,bind([[_21205, _21203, _21204], [uri_ex_x, uri_ex_z, uri_ex_z]]))).
% 35.58/34.62 cnf('1.1.1.3.1',plain,[uri_ex_z = uri_ex_x, iext(uri_owl_differentFrom, uri_ex_z, uri_ex_x)],extension(16,bind([[_33074, _33075], [uri_ex_z, uri_ex_x]]))).
% 35.58/34.62 cnf('1.1.1.3.1.1',plain,[-(iext(uri_owl_differentFrom, uri_ex_z, uri_ex_x))],extension(8)).
% 35.58/34.62 cnf('1.1.1.3.2',plain,[-(uri_ex_z = uri_ex_z)],extension(4,bind([[_21163], [uri_ex_z]]))).
% 35.58/34.62 %-----------------------------------------------------
% 35.58/34.63
% 35.58/34.63 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------