%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : SWB005+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:59:41 PM UTC 2026
% Result : Theorem 0.12s 0.44s
% Output : Proof 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB005+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 28 06:58:31 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.44 Command-line arguments: --no-flatten-goal
% 0.12/0.44
% 0.12/0.44 % SZS status Theorem
% 0.12/0.44
% 0.12/0.47 % SZS output start Proof
% 0.12/0.47 Axiom 1 (simple_ir): ir(X) = true.
% 0.12/0.47 Axiom 2 (testcase_premise_fullish_005_Everything_is_a_Resource): iext(uri_ex_p, uri_ex_s, uri_ex_o) = true.
% 0.12/0.47 Axiom 3 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 0.12/0.47 Axiom 4 (owl_class_objectproperty_ext): ifeq(ip(X), true, icext(uri_owl_ObjectProperty, X), true) = true.
% 0.12/0.47 Axiom 5 (rdf_type_ip_1): ifeq(ip(X), true, iext(uri_rdf_type, X, uri_rdf_Property), true) = true.
% 0.12/0.47 Axiom 6 (rdfs_ir_def): ifeq(ir(X), true, icext(uri_rdfs_Resource, X), true) = true.
% 0.12/0.47 Axiom 7 (owl_class_thing_ext): ifeq(ir(X), true, icext(uri_owl_Thing, X), true) = true.
% 0.12/0.47 Axiom 8 (simple_iext_property): ifeq(iext(X, Y, Z), true, ip(X), true) = true.
% 0.12/0.47 Axiom 9 (rdfs_cext_def_1): ifeq(icext(X, Y), true, iext(uri_rdf_type, Y, X), true) = true.
% 0.12/0.47
% 0.12/0.47 Goal 1 (testcase_conclusion_fullish_005_Everything_is_a_Resource): tuple(iext(uri_rdf_type, uri_ex_s, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing)) = tuple(true, true, true, true, true, true, true, true).
% 0.12/0.47 Proof:
% 0.12/0.47 tuple(iext(uri_rdf_type, uri_ex_s, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.47 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.47 tuple(ifeq(true, true, iext(uri_rdf_type, uri_ex_s, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.47 = { by axiom 6 (rdfs_ir_def) R->L }
% 0.12/0.47 tuple(ifeq(ifeq(ir(uri_ex_s), true, icext(uri_rdfs_Resource, uri_ex_s), true), true, iext(uri_rdf_type, uri_ex_s, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.47 = { by axiom 1 (simple_ir) }
% 0.12/0.47 tuple(ifeq(ifeq(true, true, icext(uri_rdfs_Resource, uri_ex_s), true), true, iext(uri_rdf_type, uri_ex_s, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.47 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.47 tuple(ifeq(icext(uri_rdfs_Resource, uri_ex_s), true, iext(uri_rdf_type, uri_ex_s, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.47 = { by axiom 9 (rdfs_cext_def_1) }
% 0.12/0.47 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.47 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.47 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), ifeq(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 6 (rdfs_ir_def) R->L }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), ifeq(ifeq(ir(uri_ex_p), true, icext(uri_rdfs_Resource, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 1 (simple_ir) }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), ifeq(ifeq(true, true, icext(uri_rdfs_Resource, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), ifeq(icext(uri_rdfs_Resource, uri_ex_p), true, iext(uri_rdf_type, uri_ex_p, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 9 (rdfs_cext_def_1) }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), ifeq(true, true, iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 6 (rdfs_ir_def) R->L }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), ifeq(ifeq(ir(uri_ex_o), true, icext(uri_rdfs_Resource, uri_ex_o), true), true, iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 1 (simple_ir) }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), ifeq(ifeq(true, true, icext(uri_rdfs_Resource, uri_ex_o), true), true, iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), ifeq(icext(uri_rdfs_Resource, uri_ex_o), true, iext(uri_rdf_type, uri_ex_o, uri_rdfs_Resource), true), iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 9 (rdfs_cext_def_1) }
% 0.12/0.48 tuple(true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.48 tuple(true, ifeq(true, true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 7 (owl_class_thing_ext) R->L }
% 0.12/0.48 tuple(true, ifeq(ifeq(ir(uri_ex_s), true, icext(uri_owl_Thing, uri_ex_s), true), true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 1 (simple_ir) }
% 0.12/0.48 tuple(true, ifeq(ifeq(true, true, icext(uri_owl_Thing, uri_ex_s), true), true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.48 tuple(true, ifeq(icext(uri_owl_Thing, uri_ex_s), true, iext(uri_rdf_type, uri_ex_s, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 9 (rdfs_cext_def_1) }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, ifeq(true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 7 (owl_class_thing_ext) R->L }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, ifeq(ifeq(ir(uri_ex_p), true, icext(uri_owl_Thing, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 1 (simple_ir) }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, ifeq(ifeq(true, true, icext(uri_owl_Thing, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, ifeq(icext(uri_owl_Thing, uri_ex_p), true, iext(uri_rdf_type, uri_ex_p, uri_owl_Thing), true), iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 9 (rdfs_cext_def_1) }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, ifeq(true, true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing), true))
% 0.12/0.48 = { by axiom 7 (owl_class_thing_ext) R->L }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, ifeq(ifeq(ir(uri_ex_o), true, icext(uri_owl_Thing, uri_ex_o), true), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing), true))
% 0.12/0.48 = { by axiom 1 (simple_ir) }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, ifeq(ifeq(true, true, icext(uri_owl_Thing, uri_ex_o), true), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing), true))
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, ifeq(icext(uri_owl_Thing, uri_ex_o), true, iext(uri_rdf_type, uri_ex_o, uri_owl_Thing), true))
% 0.12/0.48 = { by axiom 9 (rdfs_cext_def_1) }
% 0.12/0.48 tuple(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, true)
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.48 tuple(true, true, ifeq(true, true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, true)
% 0.12/0.48 = { by axiom 8 (simple_iext_property) R->L }
% 0.12/0.48 tuple(true, true, ifeq(ifeq(iext(uri_ex_p, uri_ex_s, uri_ex_o), true, ip(uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, true)
% 0.12/0.48 = { by axiom 2 (testcase_premise_fullish_005_Everything_is_a_Resource) }
% 0.12/0.48 tuple(true, true, ifeq(ifeq(true, true, ip(uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, true)
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.48 tuple(true, true, ifeq(ip(uri_ex_p), true, iext(uri_rdf_type, uri_ex_p, uri_rdf_Property), true), true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, true)
% 0.12/0.48 = { by axiom 5 (rdf_type_ip_1) }
% 0.12/0.48 tuple(true, true, true, true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true, true)
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.48 tuple(true, true, true, true, true, ifeq(true, true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true), true, true)
% 0.12/0.48 = { by axiom 4 (owl_class_objectproperty_ext) R->L }
% 0.12/0.48 tuple(true, true, true, true, true, ifeq(ifeq(ip(uri_ex_p), true, icext(uri_owl_ObjectProperty, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true), true, true)
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) R->L }
% 0.12/0.48 tuple(true, true, true, true, true, ifeq(ifeq(ifeq(true, true, ip(uri_ex_p), true), true, icext(uri_owl_ObjectProperty, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true), true, true)
% 0.12/0.48 = { by axiom 2 (testcase_premise_fullish_005_Everything_is_a_Resource) R->L }
% 0.12/0.48 tuple(true, true, true, true, true, ifeq(ifeq(ifeq(iext(uri_ex_p, uri_ex_s, uri_ex_o), true, ip(uri_ex_p), true), true, icext(uri_owl_ObjectProperty, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true), true, true)
% 0.12/0.48 = { by axiom 8 (simple_iext_property) }
% 0.12/0.48 tuple(true, true, true, true, true, ifeq(ifeq(true, true, icext(uri_owl_ObjectProperty, uri_ex_p), true), true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true), true, true)
% 0.12/0.48 = { by axiom 3 (ifeq_axiom) }
% 0.12/0.48 tuple(true, true, true, true, true, ifeq(icext(uri_owl_ObjectProperty, uri_ex_p), true, iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty), true), true, true)
% 0.12/0.48 = { by axiom 9 (rdfs_cext_def_1) }
% 0.12/0.48 tuple(true, true, true, true, true, true, true, true)
% 0.12/0.48 % SZS output end Proof
% 0.12/0.48
% 0.12/0.48 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------