%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWB057+1 : TPTP v9.0.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n005.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 : Sat Jun 21 05:29:46 AM UTC 2025
% Result : Theorem 0.49s 0.70s
% Output : Proof 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWB057+1 : TPTP v9.0.0. Released v5.2.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.13/0.33 % Computer : n005.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri Jun 20 07:54:35 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.49/0.70 % SZS status Theorem
% 0.49/0.70 % SZS output start Proof
% 0.49/0.70 tff(icext_type, type, (
% 0.49/0.70 icext: ( $i * $i ) > $o)).
% 0.49/0.70 tff(uri_ex_u_type, type, (
% 0.49/0.70 uri_ex_u: $i)).
% 0.49/0.70 tff(uri_ex_c_type, type, (
% 0.49/0.70 uri_ex_c: $i)).
% 0.49/0.70 tff(uri_ex_w_type, type, (
% 0.49/0.70 uri_ex_w: $i)).
% 0.49/0.70 tff(iext_type, type, (
% 0.49/0.70 iext: ( $i * $i * $i ) > $o)).
% 0.49/0.70 tff(uri_owl_differentFrom_type, type, (
% 0.49/0.70 uri_owl_differentFrom: $i)).
% 0.49/0.70 tff(uri_rdf_type_type, type, (
% 0.49/0.70 uri_rdf_type: $i)).
% 0.49/0.70 tff(tptp_fun_X0_140_type, type, (
% 0.49/0.70 tptp_fun_X0_140: $i)).
% 0.49/0.70 tff(uri_owl_complementOf_type, type, (
% 0.49/0.70 uri_owl_complementOf: $i)).
% 0.49/0.70 tff(ic_type, type, (
% 0.49/0.70 ic: $i > $o)).
% 0.49/0.70 tff(1,plain,
% 0.49/0.70 (^[X: $i, Y: $i] : refl((~((X = Y) <=> iext(uri_owl_differentFrom, X, Y))) <=> (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y))))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(2,plain,
% 0.49/0.70 (![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y))) <=> ![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[1])).
% 0.49/0.70 tff(3,plain,
% 0.49/0.70 (![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y))) <=> ![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))),
% 0.49/0.70 inference(rewrite,[status(thm)],[])).
% 0.49/0.70 tff(4,plain,
% 0.49/0.70 (^[X: $i, Y: $i] : trans(rewrite((iext(uri_owl_differentFrom, X, Y) <=> (~(X = Y))) <=> (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))), rewrite((~((X = Y) <=> iext(uri_owl_differentFrom, X, Y))) <=> (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))), ((iext(uri_owl_differentFrom, X, Y) <=> (~(X = Y))) <=> (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(5,plain,
% 0.49/0.70 (![X: $i, Y: $i] : (iext(uri_owl_differentFrom, X, Y) <=> (~(X = Y))) <=> ![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[4])).
% 0.49/0.70 tff(6,axiom,(![X: $i, Y: $i] : (iext(uri_owl_differentFrom, X, Y) <=> (~(X = Y)))), file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax','owl_eqdis_differentfrom')).
% 0.49/0.70 tff(7,plain,
% 0.49/0.70 (![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.49/0.70 tff(8,plain,
% 0.49/0.70 (![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.49/0.70 tff(9,plain,(
% 0.49/0.70 ![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))),
% 0.49/0.70 inference(skolemize,[status(sab)],[8])).
% 0.49/0.70 tff(10,plain,
% 0.49/0.70 (![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.49/0.70 tff(11,plain,
% 0.49/0.70 ((~![X: $i, Y: $i] : (~((X = Y) <=> iext(uri_owl_differentFrom, X, Y)))) | (~((uri_ex_w = uri_ex_u) <=> iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)))),
% 0.49/0.70 inference(quant_inst,[status(thm)],[])).
% 0.49/0.70 tff(12,plain,
% 0.49/0.70 (~((uri_ex_w = uri_ex_u) <=> iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u))),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[11, 10])).
% 0.49/0.70 tff(13,plain,
% 0.49/0.70 ((~iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)) <=> (~iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u))),
% 0.49/0.70 inference(rewrite,[status(thm)],[])).
% 0.49/0.70 tff(14,axiom,(~iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conclusion_rdfbased_sem_eqdis_different_ext')).
% 0.49/0.70 tff(15,plain,
% 0.49/0.70 (~iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[14, 13])).
% 0.49/0.70 tff(16,plain,
% 0.49/0.70 (((uri_ex_w = uri_ex_u) <=> iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)) | (uri_ex_w = uri_ex_u) | iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)),
% 0.49/0.70 inference(tautology,[status(thm)],[])).
% 0.49/0.70 tff(17,plain,
% 0.49/0.70 (((uri_ex_w = uri_ex_u) <=> iext(uri_owl_differentFrom, uri_ex_w, uri_ex_u)) | (uri_ex_w = uri_ex_u)),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[16, 15])).
% 0.49/0.70 tff(18,plain,
% 0.49/0.70 (uri_ex_w = uri_ex_u),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[17, 12])).
% 0.49/0.70 tff(19,plain,
% 0.49/0.70 (uri_ex_u = uri_ex_w),
% 0.49/0.70 inference(symmetry,[status(thm)],[18])).
% 0.49/0.70 tff(20,plain,
% 0.49/0.70 (icext(uri_ex_c, uri_ex_u) <=> icext(uri_ex_c, uri_ex_w)),
% 0.49/0.70 inference(monotonicity,[status(thm)],[19])).
% 0.49/0.70 tff(21,plain,
% 0.49/0.70 (icext(uri_ex_c, uri_ex_w) <=> icext(uri_ex_c, uri_ex_u)),
% 0.49/0.70 inference(symmetry,[status(thm)],[20])).
% 0.49/0.70 tff(22,plain,
% 0.49/0.70 (^[X: $i, C: $i] : refl((iext(uri_rdf_type, X, C) <=> icext(C, X)) <=> (iext(uri_rdf_type, X, C) <=> icext(C, X)))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(23,plain,
% 0.49/0.70 (![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X)) <=> ![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[22])).
% 0.49/0.70 tff(24,plain,
% 0.49/0.70 (![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X)) <=> ![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))),
% 0.49/0.70 inference(rewrite,[status(thm)],[])).
% 0.49/0.70 tff(25,axiom,(![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))), file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax','rdfs_cext_def')).
% 0.49/0.70 tff(26,plain,
% 0.49/0.70 (![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.49/0.70 tff(27,plain,(
% 0.49/0.70 ![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))),
% 0.49/0.70 inference(skolemize,[status(sab)],[26])).
% 0.49/0.70 tff(28,plain,
% 0.49/0.70 (![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[27, 23])).
% 0.49/0.70 tff(29,plain,
% 0.49/0.70 ((~![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))) | (iext(uri_rdf_type, uri_ex_w, uri_ex_c) <=> icext(uri_ex_c, uri_ex_w))),
% 0.49/0.70 inference(quant_inst,[status(thm)],[])).
% 0.49/0.70 tff(30,plain,
% 0.49/0.70 (iext(uri_rdf_type, uri_ex_w, uri_ex_c) <=> icext(uri_ex_c, uri_ex_w)),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[29, 28])).
% 0.49/0.70 tff(31,plain,
% 0.49/0.70 (?[X0: $i] : (iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c)) <=> ?[X0: $i] : (iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c))),
% 0.49/0.70 inference(rewrite,[status(thm)],[])).
% 0.49/0.70 tff(32,plain,
% 0.49/0.70 (^[X0: $i] : rewrite(((iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c)) & iext(uri_rdf_type, uri_ex_w, uri_ex_c)) <=> (iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c)))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(33,plain,
% 0.49/0.70 (?[X0: $i] : ((iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c)) & iext(uri_rdf_type, uri_ex_w, uri_ex_c)) <=> ?[X0: $i] : (iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[32])).
% 0.49/0.70 tff(34,axiom,(?[X0: $i] : ((iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c)) & iext(uri_rdf_type, uri_ex_w, uri_ex_c))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','premise_rdfbased_sem_eqdis_different_ext')).
% 0.49/0.70 tff(35,plain,
% 0.49/0.70 (?[X0: $i] : (iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.49/0.70 tff(36,plain,
% 0.49/0.70 (?[X0: $i] : (iext(uri_rdf_type, uri_ex_u, X0) & iext(uri_owl_complementOf, X0, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[35, 31])).
% 0.49/0.70 tff(37,plain,(
% 0.49/0.70 iext(uri_rdf_type, uri_ex_u, X0!140) & iext(uri_owl_complementOf, X0!140, uri_ex_c) & iext(uri_rdf_type, uri_ex_w, uri_ex_c)),
% 0.49/0.70 inference(skolemize,[status(sab)],[36])).
% 0.49/0.70 tff(38,plain,
% 0.49/0.70 (iext(uri_rdf_type, uri_ex_w, uri_ex_c)),
% 0.49/0.70 inference(and_elim,[status(thm)],[37])).
% 0.49/0.70 tff(39,plain,
% 0.49/0.70 ((~(iext(uri_rdf_type, uri_ex_w, uri_ex_c) <=> icext(uri_ex_c, uri_ex_w))) | (~iext(uri_rdf_type, uri_ex_w, uri_ex_c)) | icext(uri_ex_c, uri_ex_w)),
% 0.49/0.70 inference(tautology,[status(thm)],[])).
% 0.49/0.70 tff(40,plain,
% 0.49/0.70 ((~(iext(uri_rdf_type, uri_ex_w, uri_ex_c) <=> icext(uri_ex_c, uri_ex_w))) | icext(uri_ex_c, uri_ex_w)),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[39, 38])).
% 0.49/0.70 tff(41,plain,
% 0.49/0.70 (icext(uri_ex_c, uri_ex_w)),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[40, 30])).
% 0.49/0.70 tff(42,plain,
% 0.49/0.70 (icext(uri_ex_c, uri_ex_u)),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[41, 21])).
% 0.49/0.70 tff(43,plain,
% 0.49/0.70 (iext(uri_owl_complementOf, X0!140, uri_ex_c)),
% 0.49/0.70 inference(and_elim,[status(thm)],[37])).
% 0.49/0.70 tff(44,plain,
% 0.49/0.70 (^[Z: $i, C: $i] : refl(((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))) <=> ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(45,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))) <=> ![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[44])).
% 0.49/0.70 tff(46,plain,
% 0.49/0.70 (^[Z: $i, C: $i] : rewrite(((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))) <=> ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(47,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))) <=> ![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[46])).
% 0.49/0.70 tff(48,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))) <=> ![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))),
% 0.49/0.70 inference(transitivity,[status(thm)],[47, 45])).
% 0.49/0.70 tff(49,plain,
% 0.49/0.70 (^[Z: $i, C: $i] : rewrite(((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X))))) <=> ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(50,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X))))) <=> ![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[49])).
% 0.49/0.70 tff(51,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X))))) <=> ![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))),
% 0.49/0.70 inference(rewrite,[status(thm)],[])).
% 0.49/0.70 tff(52,plain,
% 0.49/0.70 (^[Z: $i, C: $i] : trans(monotonicity(trans(monotonicity(quant_intro(proof_bind(^[X: $i] : trans(rewrite((icext(Z, X) <=> (~icext(C, X))) <=> (~(icext(C, X) <=> icext(Z, X)))), rewrite((~(icext(C, X) <=> icext(Z, X))) <=> (~(icext(C, X) <=> icext(Z, X)))), ((icext(Z, X) <=> (~icext(C, X))) <=> (~(icext(C, X) <=> icext(Z, X)))))), (![X: $i] : (icext(Z, X) <=> (~icext(C, X))) <=> ![X: $i] : (~(icext(C, X) <=> icext(Z, X))))), (((ic(Z) & ic(C)) & ![X: $i] : (icext(Z, X) <=> (~icext(C, X)))) <=> ((ic(Z) & ic(C)) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))), rewrite(((ic(Z) & ic(C)) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))) <=> (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X))))), (((ic(Z) & ic(C)) & ![X: $i] : (icext(Z, X) <=> (~icext(C, X)))) <=> (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))), ((iext(uri_owl_complementOf, Z, C) => ((ic(Z) & ic(C)) & ![X: $i] : (icext(Z, X) <=> (~icext(C, X))))) <=> (iext(uri_owl_complementOf, Z, C) => (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X))))))), rewrite((iext(uri_owl_complementOf, Z, C) => (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X))))) <=> ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))), ((iext(uri_owl_complementOf, Z, C) => ((ic(Z) & ic(C)) & ![X: $i] : (icext(Z, X) <=> (~icext(C, X))))) <=> ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))),
% 0.49/0.70 inference(bind,[status(th)],[])).
% 0.49/0.70 tff(53,plain,
% 0.49/0.70 (![Z: $i, C: $i] : (iext(uri_owl_complementOf, Z, C) => ((ic(Z) & ic(C)) & ![X: $i] : (icext(Z, X) <=> (~icext(C, X))))) <=> ![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))),
% 0.49/0.70 inference(quant_intro,[status(thm)],[52])).
% 0.49/0.70 tff(54,axiom,(![Z: $i, C: $i] : (iext(uri_owl_complementOf, Z, C) => ((ic(Z) & ic(C)) & ![X: $i] : (icext(Z, X) <=> (~icext(C, X)))))), file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax','owl_bool_complementof_class')).
% 0.49/0.70 tff(55,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[54, 53])).
% 0.49/0.70 tff(56,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[55, 51])).
% 0.49/0.70 tff(57,plain,(
% 0.49/0.70 ![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (ic(Z) & ic(C) & ![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))),
% 0.49/0.70 inference(skolemize,[status(sab)],[56])).
% 0.49/0.70 tff(58,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[57, 50])).
% 0.49/0.70 tff(59,plain,
% 0.49/0.70 (![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[58, 48])).
% 0.49/0.70 tff(60,plain,
% 0.49/0.70 (((~![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))) | ((~iext(uri_owl_complementOf, X0!140, uri_ex_c)) | (~((~ic(uri_ex_c)) | (~ic(X0!140)) | (~![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X)))))))) <=> ((~![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))) | (~iext(uri_owl_complementOf, X0!140, uri_ex_c)) | (~((~ic(uri_ex_c)) | (~ic(X0!140)) | (~![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X)))))))),
% 0.49/0.70 inference(rewrite,[status(thm)],[])).
% 0.49/0.70 tff(61,plain,
% 0.49/0.70 ((~![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))) | ((~iext(uri_owl_complementOf, X0!140, uri_ex_c)) | (~((~ic(uri_ex_c)) | (~ic(X0!140)) | (~![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X)))))))),
% 0.49/0.70 inference(quant_inst,[status(thm)],[])).
% 0.49/0.70 tff(62,plain,
% 0.49/0.70 ((~![Z: $i, C: $i] : ((~iext(uri_owl_complementOf, Z, C)) | (~((~ic(C)) | (~ic(Z)) | (~![X: $i] : (~(icext(C, X) <=> icext(Z, X)))))))) | (~iext(uri_owl_complementOf, X0!140, uri_ex_c)) | (~((~ic(uri_ex_c)) | (~ic(X0!140)) | (~![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X))))))),
% 0.49/0.70 inference(modus_ponens,[status(thm)],[61, 60])).
% 0.49/0.70 tff(63,plain,
% 0.49/0.70 (~((~ic(uri_ex_c)) | (~ic(X0!140)) | (~![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X)))))),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[62, 59, 43])).
% 0.49/0.70 tff(64,plain,
% 0.49/0.70 (((~ic(uri_ex_c)) | (~ic(X0!140)) | (~![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X))))) | ![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X)))),
% 0.49/0.70 inference(tautology,[status(thm)],[])).
% 0.49/0.70 tff(65,plain,
% 0.49/0.70 (![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X)))),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[64, 63])).
% 0.49/0.70 tff(66,plain,
% 0.49/0.70 ((~![X: $i] : (~(icext(uri_ex_c, X) <=> icext(X0!140, X)))) | (~(icext(uri_ex_c, uri_ex_u) <=> icext(X0!140, uri_ex_u)))),
% 0.49/0.70 inference(quant_inst,[status(thm)],[])).
% 0.49/0.70 tff(67,plain,
% 0.49/0.70 (~(icext(uri_ex_c, uri_ex_u) <=> icext(X0!140, uri_ex_u))),
% 0.49/0.70 inference(unit_resolution,[status(thm)],[66, 65])).
% 0.49/0.70 tff(68,plain,
% 0.49/0.70 ((~![X: $i, C: $i] : (iext(uri_rdf_type, X, C) <=> icext(C, X))) | (iext(uri_rdf_type, uri_ex_u, X0!140) <=> icext(X0!140, uri_ex_u))),
% 0.49/0.70 inference(quant_inst,[status(thm)],[])).
% 0.49/0.70 tff(69,plain,
% 0.57/0.72 (iext(uri_rdf_type, uri_ex_u, X0!140) <=> icext(X0!140, uri_ex_u)),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[68, 28])).
% 0.57/0.72 tff(70,plain,
% 0.57/0.72 (iext(uri_rdf_type, uri_ex_u, X0!140)),
% 0.57/0.72 inference(and_elim,[status(thm)],[37])).
% 0.57/0.72 tff(71,plain,
% 0.57/0.72 ((~(iext(uri_rdf_type, uri_ex_u, X0!140) <=> icext(X0!140, uri_ex_u))) | (~iext(uri_rdf_type, uri_ex_u, X0!140)) | icext(X0!140, uri_ex_u)),
% 0.57/0.72 inference(tautology,[status(thm)],[])).
% 0.57/0.72 tff(72,plain,
% 0.57/0.72 ((~(iext(uri_rdf_type, uri_ex_u, X0!140) <=> icext(X0!140, uri_ex_u))) | icext(X0!140, uri_ex_u)),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[71, 70])).
% 0.57/0.72 tff(73,plain,
% 0.57/0.72 (icext(X0!140, uri_ex_u)),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[72, 69])).
% 0.57/0.72 tff(74,plain,
% 0.57/0.72 ((icext(uri_ex_c, uri_ex_u) <=> icext(X0!140, uri_ex_u)) | (~icext(uri_ex_c, uri_ex_u)) | (~icext(X0!140, uri_ex_u))),
% 0.57/0.72 inference(tautology,[status(thm)],[])).
% 0.57/0.72 tff(75,plain,
% 0.57/0.72 ((icext(uri_ex_c, uri_ex_u) <=> icext(X0!140, uri_ex_u)) | (~icext(uri_ex_c, uri_ex_u))),
% 0.57/0.72 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.57/0.73 tff(76,plain,
% 0.57/0.73 (~icext(uri_ex_c, uri_ex_u)),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[75, 67])).
% 0.57/0.73 tff(77,plain,
% 0.57/0.73 ($false),
% 0.57/0.73 inference(unit_resolution,[status(thm)],[76, 42])).
% 0.57/0.73 % SZS output end Proof
% 0.57/0.73 % E exiting
%------------------------------------------------------------------------------