Vampire---5.0.1.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWB029-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n014.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 01:00:14 PM UTC 2026

% Result   : Satisfiable 5.99s 1.94s
% Output   : Saturation 0.15s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u661,negated_conjecture,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u1021,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,icext(uri_rdf_Property,X1),true) ).

cnf(u1415,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource) ).

cnf(u778,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u550,negated_conjecture,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,true,true) ).

cnf(u1788,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u1019,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

cnf(u5646,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_owl_Class,X1),true,true,true),true) ).

cnf(u784,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u151,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,ic(X0),true) ).

cnf(u1938,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2) ).

cnf(u289,negated_conjecture,
    true = sF28 ).

cnf(u556,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u406,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource) ).

cnf(u805,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_B,uri_owl_Class),true) ).

cnf(u4007,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label) ).

cnf(u906,negated_conjecture,
    true = ifeq(sF52,true,true,true) ).

cnf(u2203,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u678,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,uri_rdf_nil),true,true,true),true) ).

cnf(u149,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,ic(X1),true) ).

cnf(u1057,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0),true) ).

cnf(u295,negated_conjecture,
    true = sF30 ).

cnf(u2458,negated_conjecture,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,iext(uri_rdfs_seeAlso,X0,X1),true) ).

cnf(u417,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,ifeq(sF52,true,icext(X0,uri_ex_w),true),true) ).

cnf(u649,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u404,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource) ).

cnf(u1694,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_first,uri_rdf_first),true) ).

cnf(u933,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u3953,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdf_Property),true,true,true),true) ).

cnf(u2873,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Resource),true) ).

cnf(u538,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

cnf(u2579,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u931,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Container),true) ).

cnf(u1334,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u61,axiom,
    true = iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource) ).

cnf(u5688,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_owl_Class,uri_owl_Class),true,true,true),true) ).

cnf(u5692,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Class),true) ).

cnf(u1715,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u1169,negated_conjecture,
    true = ic(uri_rdfs_Datatype) ).

cnf(u1947,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__1,uri_rdf__1),true,true,true),true) ).

cnf(u2350,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class) ).

cnf(u634,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_value,uri_rdf_Property),true) ).

cnf(u2472,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class) ).

cnf(u1338,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X1),true,icext(X1,X0),true) ).

cnf(u1058,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true) ).

cnf(u1953,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdf__1),true) ).

cnf(u1332,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u3989,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_label,uri_rdf_Property),true,true,true),true) ).

cnf(u1967,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__3,X1),true,true,true),true) ).

cnf(u2218,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u1081,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X1,X2),true,true,true),true) ).

cnf(u2780,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

cnf(u1336,negated_conjecture,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u2867,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1186,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),true) ).

cnf(u785,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_intersectionOf),true,ifeq(iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1),true,true,true),true) ).

cnf(u3268,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),true) ).

cnf(u335,negated_conjecture,
    true = sF43 ).

cnf(u2984,negated_conjecture,
    true = icext(uri_rdf_List,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) ).

cnf(u1734,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u2645,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Class,uri_rdfs_Class),true,true,true),true) ).

cnf(u1034,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_type,uri_rdf_Property),true,true,true),true) ).

cnf(u578,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_predicate,uri_rdfs_Resource),true) ).

cnf(u1624,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdfs_domain),true,true,true),true) ).

cnf(u3922,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_label) ).

cnf(u432,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_value,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2756,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u1987,negated_conjecture,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,iext(uri_rdf_object,X0,X1),true) ).

cnf(u706,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_predicate,uri_rdfs_Statement),true) ).

cnf(u4052,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdfs_comment),true,true,true),true) ).

cnf(u3976,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_label),true,true,true),true) ).

cnf(u323,negated_conjecture,
    true = sF39 ).

cnf(u1222,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_subject) ).

cnf(u2133,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u2128,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdf_Alt),true,true,true),true) ).

cnf(u961,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true) ).

cnf(u862,negated_conjecture,
    true = ip(uri_rdfs_range) ).

cnf(u1245,negated_conjecture,
    true = ip(uri_rdf_subject) ).

cnf(u1376,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Seq) ).

cnf(u586,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u3917,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_predicate) ).

cnf(u1096,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_range,uri_rdf_Property),true,true,true),true) ).

cnf(u975,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u1226,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__3) ).

cnf(u2926,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true) ).

cnf(u3137,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_type,X1),true,true,true),true) ).

cnf(u1220,negated_conjecture,
    true = icext(uri_owl_Class,uri_ex_A) ).

cnf(u2134,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdf_Alt),true) ).

cnf(u344,negated_conjecture,
    true = sF46 ).

cnf(u1127,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdf_Property),true,true,true),true) ).

cnf(u1692,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u3807,negated_conjecture,
    true = ic(uri_rdf_List) ).

cnf(u2634,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Class),true,true,true),true) ).

cnf(u5675,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_owl_Class,uri_rdfs_Class),true) ).

cnf(u1884,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type) ).

cnf(u1235,axiom,
    true = icext(uri_rdf_Property,uri_rdf_type) ).

cnf(u3806,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class) ).

cnf(u1224,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_object) ).

cnf(u1044,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_first,uri_rdfs_Resource),true,true,true),true) ).

cnf(u217,negated_conjecture,
    true = sF4 ).

cnf(u996,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u363,negated_conjecture,
    true = icext(uri_rdfs_Resource,X0) ).

cnf(u4043,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate) ).

cnf(u350,negated_conjecture,
    true = sF48 ).

cnf(u472,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2671,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true) ).

cnf(u624,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u1487,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Class,X0),true,icext(X0,uri_ex_A),true) ).

cnf(u2470,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Seq),true,true,true),true) ).

cnf(u2890,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Datatype,X1),true,true,true),true) ).

cnf(u1517,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_owl_complementOf),true,true,true),true) ).

cnf(u3816,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource) ).

cnf(u223,negated_conjecture,
    true = sF6 ).

cnf(u2010,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Datatype) ).

cnf(u361,axiom,
    iext(uri_rdf_type,uri_ex_w,uri_ex_B) = sF52 ).

cnf(u628,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_value,uri_rdf_Property),true,true,true),true) ).

cnf(u3845,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdfs_Resource),true) ).

cnf(u256,negated_conjecture,
    true = sF17 ).

cnf(u478,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

cnf(u2533,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

cnf(u2892,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u3843,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u2062,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__1),true,true,true),true) ).

cnf(u658,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u1507,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_owl_complementOf,uri_rdf_Property),true) ).

cnf(u750,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y),true,true,true),true) ).

cnf(u1661,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_domain,X1),true,true,true),true) ).

cnf(u4102,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u2559,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u3047,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty) ).

cnf(u756,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y),true) ).

cnf(u262,negated_conjecture,
    true = sF19 ).

cnf(u645,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_List),true,true,true),true) ).

cnf(u3863,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_List,uri_rdf_List),true,true,true),true) ).

cnf(u2088,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdf__3),true) ).

cnf(u232,negated_conjecture,
    true = sF9 ).

cnf(u7295,negated_conjecture,
    true = ifeq(sF52,true,sF52,true) ).

cnf(u890,negated_conjecture,
    true = ip(uri_rdf_first) ).

cnf(u1106,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_Property,uri_rdfs_Class),true,true,true),true) ).

cnf(u3971,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment) ).

cnf(u5912,axiom,
    true = ifeq(sF52,true,icext(uri_rdfs_Class,uri_ex_B),true) ).

cnf(u1789,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u1551,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u1922,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_owl_intersectionOf,uri_owl_intersectionOf),true) ).

cnf(u3089,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,icext(uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u2527,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true,true,true),true) ).

cnf(u3057,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource) ).

cnf(u5636,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_owl_Class) ).

cnf(u2307,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_seeAlso) ).

cnf(u390,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource) ).

cnf(u789,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_intersectionOf,X0),true,icext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true) ).

cnf(u2696,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u5663,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource) ).

cnf(u1018,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u2299,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdf_Property),true,true,true),true) ).

cnf(u73,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property) ).

cnf(u5662,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Class) ).

cnf(u1573,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_range) ).

cnf(u2803,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1534,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_complementOf),true) ).

cnf(u1679,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first) ).

cnf(u2073,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3) ).

cnf(u2852,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true) ).

cnf(u1571,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_range,uri_rdf_Property),true) ).

cnf(u3118,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_rest),true,true,true),true) ).

cnf(u388,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource) ).

cnf(u2435,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Class),true) ).

cnf(u917,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Literal),true) ).

cnf(u1439,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u4608,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u2063,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__1,X1),true,true,true),true) ).

cnf(u2178,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property) ).

cnf(u915,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u2974,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).

cnf(u2290,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,X1),true,true,true),true) ).

cnf(u277,negated_conjecture,
    true = sF24 ).

cnf(u528,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

cnf(u407,negated_conjecture,
    true = iext(uri_owl_complementOf,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y,uri_ex_A) ).

cnf(u2201,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_subClassOf,X1),true,true,true),true) ).

cnf(u1061,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true,true,true),true) ).

cnf(u1688,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_first,uri_rdf_first),true,true,true),true) ).

cnf(u2496,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Container,X1),true,true,true),true) ).

cnf(u930,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u2985,negated_conjecture,
    true = icext(uri_rdf_List,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) ).

cnf(u2191,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdf_Property),true) ).

cnf(u650,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u2555,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),true,true,true),true) ).

cnf(u173,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource) ).

cnf(u319,negated_conjecture,
    true = sF38 ).

cnf(u405,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource) ).

cnf(u1951,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u1065,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u428,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

cnf(u1843,negated_conjecture,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,true,true) ).

cnf(u1718,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u3731,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement) ).

cnf(u806,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_w,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true,true,true),true) ).

cnf(u1189,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u1320,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,X1,uri_rdfs_Resource),true) ).

cnf(u2274,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdf_Property),true,true,true),true) ).

cnf(u562,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1170,negated_conjecture,
    true = ic(uri_rdf_XMLLiteral) ).

cnf(u812,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_w,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true) ).

cnf(u163,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ip(X0),true) ).

cnf(u1078,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_domain,uri_rdfs_Class),true) ).

cnf(u568,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

cnf(u2973,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member) ).

cnf(u418,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,ifeq(sF52,true,icext(X0,uri_ex_B),true),true) ).

cnf(u2851,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u934,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u1333,negated_conjecture,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u690,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_owl_complementOf,X0),true,icext(X0,uri_ex_A),true) ).

cnf(u3738,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Statement,uri_rdfs_Class),true,true,true),true) ).

cnf(u161,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ip(X1),true) ).

cnf(u307,negated_conjecture,
    true = sF34 ).

cnf(u2486,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Class),true) ).

cnf(u2119,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Container,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u3744,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Class),true) ).

cnf(u548,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

cnf(u945,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Container),true) ).

cnf(u1080,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u959,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

cnf(u2636,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u4034,negated_conjecture,
    true = ip(uri_rdf_predicate) ).

cnf(u369,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

cnf(u1465,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_value,uri_rdf_value),true,true,true),true) ).

cnf(u1091,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true) ).

cnf(u1229,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1) ).

cnf(u2497,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class) ).

cnf(u1484,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_Class),true,ifeq(iext(X0,X1,uri_ex_A),true,true,true),true) ).

cnf(u375,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ).

cnf(u1862,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdf_Bag),true,true,true),true) ).

cnf(u2245,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u1111,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u458,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Resource),true) ).

cnf(u3822,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_List,uri_rdfs_Class),true,true,true),true) ).

cnf(u1868,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdf_Bag),true) ).

cnf(u1219,negated_conjecture,
    true = icext(uri_owl_Class,uri_ex_B) ).

cnf(u3029,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,uri_rdf_List),true) ).

cnf(u2940,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Literal,X1),true,true,true),true) ).

cnf(u1116,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true,true,true),true) ).

cnf(u347,negated_conjecture,
    true = sF47 ).

cnf(u1246,negated_conjecture,
    true = ip(uri_rdf_value) ).

cnf(u3868,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u4103,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u456,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u2519,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,true,true) ).

cnf(u985,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_type,uri_rdfs_Resource),true) ).

cnf(u1131,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u1363,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt) ).

cnf(u606,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u1501,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_owl_complementOf,uri_rdf_Property),true,true,true),true) ).

cnf(u1120,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u999,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u3154,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u1902,negated_conjecture,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,iext(uri_rdf_type,X0,X1),true) ).

cnf(u368,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).

cnf(u462,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true,true,true),true) ).

cnf(u861,negated_conjecture,
    true = ip(uri_owl_complementOf) ).

cnf(u2000,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u3177,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_member,uri_rdf_Property),true,true,true),true) ).

cnf(u627,negated_conjecture,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,icext(uri_rdf_List,X0),true) ).

cnf(u2260,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

cnf(u734,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u1248,negated_conjecture,
    true = ip(uri_rdf__3) ).

cnf(u2710,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Resource,uri_rdfs_Class),true) ).

cnf(u1028,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u374,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

cnf(u757,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u3847,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u874,negated_conjecture,
    true = ip(uri_rdfs_domain) ).

cnf(u1767,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_owl_intersectionOf),true) ).

cnf(u4083,negated_conjecture,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,iext(uri_rdfs_label,X0,X1),true) ).

cnf(u518,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

cnf(u1756,negated_conjecture,
    true = icext(uri_rdf_Property,uri_owl_intersectionOf) ).

cnf(u247,negated_conjecture,
    true = sF14 ).

cnf(u2034,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,icext(uri_rdfs_Seq,X0),true) ).

cnf(u3295,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true) ).

cnf(u1754,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_owl_intersectionOf,uri_rdf_Property),true) ).

cnf(u617,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_Literal),true) ).

cnf(u372,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

cnf(u2419,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Bag),true,true,true),true) ).

cnf(u502,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1803,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__1),true,true,true),true) ).

cnf(u3975,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_label,X1),true,true,true),true) ).

cnf(u1002,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),true,true,true),true) ).

cnf(u771,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__3,uri_rdf_Property),true,true,true),true) ).

cnf(u1557,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,true,true) ).

cnf(u916,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u1008,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),true) ).

cnf(u1538,negated_conjecture,
    true = ifeq(iext(uri_owl_complementOf,X0,X1),true,iext(uri_owl_complementOf,X0,X1),true) ).

cnf(u385,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u5652,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_owl_Class),true) ).

cnf(u1137,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_first,uri_rdf_Property),true,true,true),true) ).

cnf(u5669,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_owl_Class,uri_rdfs_Class),true,true,true),true) ).

cnf(u3211,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__2,uri_rdfs_member),true) ).

cnf(u1790,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_subject,uri_rdf_subject),true) ).

cnf(u2268,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Class,X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u1423,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,true,true) ).

cnf(u3962,negated_conjecture,
    true = ip(uri_rdfs_comment) ).

cnf(u1793,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,iext(uri_rdf_subject,X0,X1),true) ).

cnf(u1668,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_Class),true,ifeq(iext(X0,X1,uri_ex_B),true,true,true),true) ).

cnf(u2315,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_seeAlso,X1),true,true,true),true) ).

cnf(u29,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdf_Property),true,ip(X0),true) ).

cnf(u792,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2),true,true,true),true) ).

cnf(u512,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true,true,true),true) ).

cnf(u391,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource) ).

cnf(u2185,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdf_Property),true,true,true),true) ).

cnf(u3099,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Property,uri_rdf_Property),true,true,true),true) ).

cnf(u2043,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__2,uri_rdf__2),true,true,true),true) ).

cnf(u1520,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_owl_complementOf),true) ).

cnf(u1921,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_intersectionOf),true) ).

cnf(u157,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,ifeq(iext(uri_rdfs_subClassOf,X2,X0),true,iext(uri_rdfs_subClassOf,X2,X1),true),true) ).

cnf(u389,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u640,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u274,negated_conjecture,
    true = sF23 ).

cnf(u412,negated_conjecture,
    true = iext(uri_rdf_first,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,uri_ex_A) ).

cnf(u3227,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_member),true,true,true),true) ).

cnf(u2827,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u790,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_owl_intersectionOf,X0),true,icext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1),true) ).

cnf(u1173,negated_conjecture,
    true = ic(uri_rdf_Alt) ).

cnf(u508,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

cnf(u546,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u3721,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u796,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_rest,X0),true,icext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1),true) ).

cnf(u147,axiom,
    true = ifeq(icext(X0,X1),true,ifeq(iext(uri_rdfs_subClassOf,X0,X2),true,icext(X2,X1),true),true) ).

cnf(u301,negated_conjecture,
    true = sF32 ).

cnf(u552,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_member,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2364,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Class),true) ).

cnf(u3236,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u402,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement) ).

cnf(u1085,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true,true,true),true) ).

cnf(u918,negated_conjecture,
    true = ip(uri_rdfs_subClassOf) ).

cnf(u2200,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_subClassOf),true,true,true),true) ).

cnf(u674,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u3722,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class) ).

cnf(u145,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class) ).

cnf(u5542,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true) ).

cnf(u1190,axiom,
    true = ic(uri_rdf_Property) ).

cnf(u4018,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property) ).

cnf(u400,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement) ).

cnf(u929,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u1213,axiom,
    true = ifeq(sF52,true,icext(uri_ex_B,uri_ex_w),true) ).

cnf(u1812,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_object,X1),true,true,true),true) ).

cnf(u313,negated_conjecture,
    true = sF36 ).

cnf(u943,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u57,axiom,
    true = ifeq(ic(X0),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u2576,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Alt),true,true,true),true) ).

cnf(u2453,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u1188,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true) ).

cnf(u419,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,ifeq(sF52,true,iext(X0,uri_ex_w,uri_ex_B),true),true) ).

cnf(u1565,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_range,uri_rdf_Property),true,true,true),true) ).

cnf(u442,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_subject,uri_rdfs_Resource),true,true,true),true) ).

cnf(u958,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u5544,negated_conjecture,
    true = ic(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) ).

cnf(u2545,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u1102,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_range,uri_rdf_Property),true) ).

cnf(u684,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,uri_rdf_nil),true) ).

cnf(u4011,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_predicate,X1),true,true,true),true) ).

cnf(u2375,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdfs_subClassOf),true,true,true),true) ).

cnf(u4017,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u3755,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Statement,uri_rdfs_Resource),true,true,true),true) ).

cnf(u4031,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_Property),true) ).

cnf(u1978,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_object,uri_rdf_object),true,true,true),true) ).

cnf(u2380,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u1230,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__1) ).

cnf(u446,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u1223,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_value) ).

cnf(u1845,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object) ).

cnf(u1347,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy) ).

cnf(u590,negated_conjecture,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,true,true) ).

cnf(u3157,negated_conjecture,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u1104,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u2635,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Class,X1),true,true,true),true) ).

cnf(u329,negated_conjecture,
    true = sF41 ).

cnf(u596,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u5653,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class) ).

cnf(u1984,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_object,uri_rdf_object),true) ).

cnf(u370,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).

cnf(u3161,negated_conjecture,
    true = ip(uri_rdfs_member) ).

cnf(u611,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_label,uri_rdfs_Literal),true,true,true),true) ).

cnf(u2158,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,true,true) ).

cnf(u2244,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

cnf(u3158,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u1629,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u1232,negated_conjecture,
    true = icext(uri_rdf_List,uri_rdf_nil) ).

cnf(u103,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true) ).

cnf(u3945,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u3015,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,X1),true,true,true),true) ).

cnf(u3959,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_comment,uri_rdf_Property),true) ).

cnf(u973,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Container),true) ).

cnf(u200,negated_conjecture,
    true = ifeq(lv(X0),true,true,true) ).

cnf(u1495,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,uri_owl_complementOf) ).

cnf(u1633,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,iext(uri_rdfs_domain,X0,X1),true) ).

cnf(u2020,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Seq),true,true,true),true) ).

cnf(u1387,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_XMLLiteral) ).

cnf(u1740,negated_conjecture,
    true = ifeq(iext(uri_owl_intersectionOf,X0,X1),true,true,true) ).

cnf(u971,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u1374,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq) ).

cnf(u2471,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Seq,X1),true,true,true),true) ).

cnf(u3185,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_member) ).

cnf(u636,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_subject,uri_rdfs_Statement),true,true,true),true) ).

cnf(u356,negated_conjecture,
    true = sF50 ).

cnf(u2403,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u486,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u1731,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__2),true,true,true),true) ).

cnf(u1407,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u3779,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Statement,uri_rdfs_Statement),true,true,true),true) ).

cnf(u615,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u1652,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_domain) ).

cnf(u2942,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u2771,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1829,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),true) ).

cnf(u229,negated_conjecture,
    true = sF8 ).

cnf(u1775,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject) ).

cnf(u1650,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_domain,uri_rdf_Property),true) ).

cnf(u729,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u2667,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u1013,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true,true,true),true) ).

cnf(u1535,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_owl_complementOf,uri_owl_complementOf),true) ).

cnf(u770,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_A,uri_owl_Class),true) ).

cnf(u2825,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Resource),true) ).

cnf(u743,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,uri_ex_A),true,true,true),true) ).

cnf(u618,negated_conjecture,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

cnf(u13,axiom,
    true = iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).

cnf(u373,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

cnf(u2087,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u2170,negated_conjecture,
    true = ifeq(icext(X0,X1),true,true,true) ).

cnf(u268,negated_conjecture,
    true = sF21 ).

cnf(u1558,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property) ).

cnf(u2795,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Resource),true,true,true),true) ).

cnf(u4056,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u1290,axiom,
    true = ifeq(icext(uri_ex_B,uri_ex_w),true,sF52,true) ).

cnf(u2065,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u3705,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_List) ).

cnf(u4604,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_member,uri_rdfs_member),true,true,true),true) ).

cnf(u3,axiom,
    true = ifeq(iext(X0,X1,X2),true,ip(X0),true) ).

cnf(u1414,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container) ).

cnf(u3205,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_member),true,true,true),true) ).

cnf(u2941,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class) ).

cnf(u4080,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u2047,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u641,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u396,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container) ).

cnf(u2258,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u244,negated_conjecture,
    true = sF13 ).

cnf(u2939,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Literal),true,true,true),true) ).

cnf(u530,negated_conjecture,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,true,true) ).

cnf(u3876,negated_conjecture,
    true = ifeq(icext(uri_rdf_List,X0),true,icext(uri_rdf_List,X0),true) ).

cnf(u5715,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_owl_Class,uri_rdfs_Resource),true,true,true),true) ).

cnf(ifeq_axiom,axiom,
    ifeq(X0,X0,X1,X2) = X1 ).

cnf(u131,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class) ).

cnf(u536,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u415,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_w,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) ).

cnf(u386,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u1161,negated_conjecture,
    true = ic(uri_rdfs_Container) ).

cnf(u3998,negated_conjecture,
    true = ip(uri_rdfs_label) ).

cnf(u1069,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u3939,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_comment,X1),true,true,true),true) ).

cnf(u3183,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_member,uri_rdf_Property),true) ).

cnf(u1416,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Container) ).

cnf(u799,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_B,uri_owl_Class),true,true,true),true) ).

cnf(u1050,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_first,uri_rdfs_Resource),true) ).

cnf(u129,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,ifeq(iext(X0,X2,X3),true,icext(X1,X3),true),true) ).

cnf(u3247,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Property),true,true,true),true) ).

cnf(u3723,negated_conjecture,
    true = ic(uri_rdfs_Statement) ).

cnf(u1404,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_value),true,true,true),true) ).

cnf(u413,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_A,uri_owl_Class) ).

cnf(u298,negated_conjecture,
    true = sF31 ).

cnf(u384,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container) ).

cnf(u2726,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u962,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

cnf(u3869,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdf_List),true) ).

cnf(u1048,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u171,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(uri_rdfs_subPropertyOf,X2,X0),true,iext(uri_rdfs_subPropertyOf,X2,X1),true),true) ).

cnf(u3248,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Property,X1),true,true,true),true) ).

cnf(u1172,negated_conjecture,
    true = ic(uri_rdf_Bag) ).

cnf(u403,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement) ).

cnf(u2086,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u2213,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u777,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdf_Property),true) ).

cnf(u426,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u2586,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdfs_Class),true,true,true),true) ).

cnf(u5647,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_owl_Class),true,true,true),true) ).

cnf(u2109,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u1456,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value) ).

cnf(u2592,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Class),true) ).

cnf(u169,axiom,
    true = ifeq(ip(X0),true,iext(uri_rdfs_subPropertyOf,X0,X0),true) ).

cnf(u948,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u668,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Datatype),true) ).

cnf(u3995,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_label,uri_rdf_Property),true) ).

cnf(u685,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_complementOf),true,ifeq(iext(X0,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y,uri_ex_A),true,true,true),true) ).

cnf(u3946,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property) ).

cnf(u953,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true,true,true),true) ).

cnf(u683,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,uri_rdf_nil),true) ).

cnf(u1469,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u1823,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u175,axiom,
    true = iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class) ).

cnf(u3715,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Statement,X1),true,true,true),true) ).

cnf(u5553,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,uri_rdfs_Resource) ).

cnf(u430,negated_conjecture,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,true,true) ).

cnf(u3759,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u3105,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Property,uri_rdf_Property),true) ).

cnf(u2505,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Container,uri_rdfs_Class),true,true,true),true) ).

cnf(u2876,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

cnf(u5559,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,uri_rdfs_Class),true,true,true),true) ).

cnf(u3250,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u3127,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_first),true,true,true),true) ).

cnf(u580,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,true,true) ).

cnf(u2398,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),true,true,true),true) ).

cnf(u3925,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_comment) ).

cnf(u957,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u5703,negated_conjecture,
    true = ifeq(icext(uri_owl_Class,X0),true,icext(uri_owl_Class,X0),true) ).

cnf(u1876,negated_conjecture,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdf_Bag,X0),true) ).

cnf(u2142,negated_conjecture,
    true = ifeq(icext(uri_rdf_Alt,X0),true,icext(uri_rdf_Alt,X0),true) ).

cnf(u1724,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true,ifeq(iext(X0,uri_ex_w,X1),true,true,true),true) ).

cnf(u643,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u2381,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_subClassOf),true) ).

cnf(u2511,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Class),true) ).

cnf(u1124,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u708,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_object,uri_rdf_Property),true,true,true),true) ).

cnf(u2243,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u1998,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__2,X1),true,true,true),true) ).

cnf(u3784,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u3761,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Resource),true) ).

cnf(u3800,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_List),true,true,true),true) ).

cnf(u2498,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u1318,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,X1),true) ).

cnf(u3270,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1741,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_intersectionOf,uri_rdf_Property) ).

cnf(u353,negated_conjecture,
    true = sF49 ).

cnf(u620,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_first,uri_rdf_List),true,true,true),true) ).

cnf(u470,negated_conjecture,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,true,true) ).

cnf(u3023,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,uri_rdf_List),true,true,true),true) ).

cnf(u742,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__2,uri_rdf_Property),true) ).

cnf(u2755,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u4057,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u976,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

cnf(u359,negated_conjecture,
    true = sF51 ).

cnf(u1518,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_owl_complementOf,X1),true,true,true),true) ).

cnf(u5611,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,uri_rdfs_Resource),true) ).

cnf(u468,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true) ).

cnf(u2651,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

cnf(u997,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_type,uri_rdfs_Class),true) ).

cnf(u2254,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Class,uri_rdfs_Class),true,true,true),true) ).

cnf(u2052,negated_conjecture,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdf__2,X0,X1),true) ).

cnf(u602,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdfs_Literal),true,true,true),true) ).

cnf(u1764,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_owl_intersectionOf),true,true,true),true) ).

cnf(u995,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u1398,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_Bag) ).

cnf(u125,axiom,
    true = iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).

cnf(u888,negated_conjecture,
    true = ip(uri_rdf_rest) ).

cnf(u608,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Literal),true) ).

cnf(u625,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u380,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List) ).

cnf(u1899,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_type,uri_rdf_type),true) ).

cnf(u1337,negated_conjecture,
    true = ifeq(icext(uri_rdf_Alt,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u4060,negated_conjecture,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,iext(uri_rdfs_comment,X0,X1),true) ).

cnf(u2779,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u438,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

cnf(u1010,negated_conjecture,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,iext(uri_rdfs_seeAlso,X0,X1),true) ).

cnf(u2049,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__2,uri_rdf__2),true) ).

cnf(u1548,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_subject),true,true,true),true) ).

cnf(u1122,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true) ).

cnf(u5654,negated_conjecture,
    true = ic(uri_owl_Class) ).

cnf(u1396,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag) ).

cnf(u115,axiom,
    true = ifeq(icext(uri_rdfs_Class,X0),true,ic(X0),true) ).

cnf(u2686,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Resource) ).

cnf(u253,negated_conjecture,
    true = sF16 ).

cnf(u271,negated_conjecture,
    true = sF22 ).

cnf(u2925,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u736,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__2,uri_rdf_Property),true,true,true),true) ).

cnf(u2282,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_isDefinedBy) ).

cnf(u3193,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_member,X1),true,true,true),true) ).

cnf(u2564,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,iext(uri_rdfs_subPropertyOf,X0,X1),true) ).

cnf(u2923,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Resource),true) ).

cnf(u2542,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_subPropertyOf),true,true,true),true) ).

cnf(u4058,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_comment),true) ).

cnf(u3170,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member) ).

cnf(u1582,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_range,X1),true,true,true),true) ).

cnf(u1250,negated_conjecture,
    true = ip(uri_rdf__1) ).

cnf(u113,axiom,
    true = ifeq(ic(X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u892,negated_conjecture,
    true = ip(uri_rdf_type) ).

cnf(u1030,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_Class),true) ).

cnf(u1925,negated_conjecture,
    true = ifeq(iext(uri_owl_intersectionOf,X0,X1),true,iext(uri_owl_intersectionOf,X0,X1),true) ).

cnf(u399,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u3048,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource) ).

cnf(u3213,negated_conjecture,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u498,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true) ).

cnf(u769,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_owl_Class),true) ).

cnf(u3982,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property) ).

cnf(u1053,negated_conjecture,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,true,true) ).

cnf(u642,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_subject,uri_rdfs_Statement),true) ).

cnf(u27,axiom,
    true = ifeq(ip(X0),true,iext(uri_rdf_type,X0,uri_rdf_Property),true) ).

cnf(u241,negated_conjecture,
    true = sF12 ).

cnf(u1146,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_Property),true,true,true),true) ).

cnf(u259,negated_conjecture,
    true = sF18 ).

cnf(u397,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) ).

cnf(u496,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u3192,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_member),true,true,true),true) ).

cnf(u798,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2),true) ).

cnf(u1032,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u911,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Literal),true,true,true),true) ).

cnf(u2449,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdfs_seeAlso),true,true,true),true) ).

cnf(u155,axiom,
    true = ifeq(ic(X0),true,iext(uri_rdfs_subClassOf,X0,X0),true) ).

cnf(u387,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource) ).

cnf(u1814,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u280,negated_conjecture,
    true = sF25 ).

cnf(u410,negated_conjecture,
    true = iext(uri_rdf_rest,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) ).

cnf(u1171,negated_conjecture,
    true = ic(uri_rdfs_Seq) ).

cnf(u1440,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_rest,uri_rdf_rest),true) ).

cnf(u3981,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u1160,negated_conjecture,
    true = ic(uri_rdfs_Literal) ).

cnf(u153,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class) ).

cnf(u2348,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u2314,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_seeAlso),true,true,true),true) ).

cnf(u652,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,icext(uri_rdf_List,X1),true) ).

cnf(u286,negated_conjecture,
    true = sF27 ).

cnf(u2341,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u408,negated_conjecture,
    true = iext(uri_owl_intersectionOf,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) ).

cnf(u1191,axiom,
    true = ic(uri_rdfs_ContainerMembershipProperty) ).

cnf(u5536,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,X1),true,true,true),true) ).

cnf(u1193,negated_conjecture,
    true = ip(uri_rdfs_seeAlso) ).

cnf(u3763,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u667,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u558,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

cnf(u1072,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdfs_Class),true,true,true),true) ).

cnf(u2994,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2),true) ).

cnf(u2704,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Resource,uri_rdfs_Class),true,true,true),true) ).

cnf(u159,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u427,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u5565,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,uri_rdfs_Class),true) ).

cnf(u414,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_B,uri_owl_Class) ).

cnf(u749,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,uri_ex_A),true) ).

cnf(u1952,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u1335,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,icext(uri_rdf_Property,X0),true) ).

cnf(u5525,negated_conjecture,
    true = icext(uri_rdfs_Class,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) ).

cnf(u2801,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Resource),true) ).

cnf(u811,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true) ).

cnf(u1597,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u2495,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Container),true,true,true),true) ).

cnf(u920,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u3119,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_rest,X1),true,true,true),true) ).

cnf(u692,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_nil,uri_rdf_List),true,true,true),true) ).

cnf(u2227,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Datatype,X0),true) ).

cnf(u1982,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u320,negated_conjecture,
    true = sF37 ).

cnf(u3764,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true) ).

cnf(u1584,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u3130,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u1708,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,uri_rdf_nil,X1),true,true,true),true) ).

cnf(u939,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Container),true,true,true),true) ).

cnf(u71,negated_conjecture,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u3076,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u1663,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u2993,negated_conjecture,
    true = iext(uri_rdf_type,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,uri_rdf_List) ).

cnf(u1723,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true,ifeq(iext(X0,X1,uri_ex_w),true,true,true),true) ).

cnf(u326,negated_conjecture,
    true = sF40 ).

cnf(u3149,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_member),true,true,true),true) ).

cnf(u1485,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_Class),true,ifeq(iext(X0,uri_ex_A,X1),true,true,true),true) ).

cnf(u1355,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso) ).

cnf(u598,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__3,uri_rdfs_Resource),true) ).

cnf(u1470,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u1581,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_range),true,true,true),true) ).

cnf(u1615,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain) ).

cnf(u697,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u1614,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u1375,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource) ).

cnf(u1346,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property) ).

cnf(u3155,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdfs_member),true) ).

cnf(u1811,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_object),true,true,true),true) ).

cnf(u2637,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u5583,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true) ).

cnf(u2917,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Literal,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1089,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u452,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1867,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u1742,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,uri_owl_intersectionOf) ).

cnf(u208,negated_conjecture,
    true = sF1 ).

cnf(u1082,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X1,X2),true,true,true),true) ).

cnf(u1474,negated_conjecture,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,iext(uri_rdf_value,X0,X1),true) ).

cnf(u1748,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_owl_intersectionOf,uri_rdf_Property),true,true,true),true) ).

cnf(u979,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_type,uri_rdfs_Resource),true,true,true),true) ).

cnf(u109,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,ifeq(iext(X0,X2,X3),true,icext(X1,X2),true),true) ).

cnf(u341,negated_conjecture,
    true = sF45 ).

cnf(u592,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2753,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Resource),true) ).

cnf(u609,negated_conjecture,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

cnf(u364,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).

cnf(u1784,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_subject,uri_rdf_subject),true,true,true),true) ).

cnf(u2235,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u214,negated_conjecture,
    true = sF3 ).

cnf(u5616,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,X0),true) ).

cnf(u2520,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u1386,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource) ).

cnf(u3049,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1660,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_domain),true,true,true),true) ).

cnf(u714,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_object,uri_rdf_Property),true) ).

cnf(u3292,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Property,uri_rdfs_Resource),true) ).

cnf(u2670,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u383,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

cnf(u5584,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true) ).

cnf(u2349,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

cnf(u492,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1593,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_range,uri_rdfs_range),true,true,true),true) ).

cnf(u626,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_first,uri_rdf_List),true) ).

cnf(u983,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u1234,axiom,
    true = icext(uri_rdf_Property,uri_rdf_first) ).

cnf(u3691,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Statement) ).

cnf(u2422,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u381,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) ).

cnf(u4610,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_member),true) ).

cnf(u1135,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u482,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_label,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2906,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

cnf(u2804,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u2693,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3848,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true) ).

cnf(u1397,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource) ).

cnf(u2280,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdf_Property),true) ).

cnf(u754,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_first,X0),true,icext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2),true) ).

cnf(u2305,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdf_Property),true) ).

cnf(u4098,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdf_predicate),true,true,true),true) ).

cnf(u371,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource) ).

cnf(u2048,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u480,negated_conjecture,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,true,true) ).

cnf(u1009,negated_conjecture,
    true = ip(uri_rdfs_subPropertyOf) ).

cnf(u2694,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Resource,X1),true,true,true),true) ).

cnf(u5582,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true) ).

cnf(u1997,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__2),true,true,true),true) ).

cnf(u3195,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u3056,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property) ).

cnf(u3839,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_List,uri_rdfs_Resource),true,true,true),true) ).

cnf(u689,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_complementOf,X0),true,icext(X0,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y),true) ).

cnf(u9,axiom,
    true = iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).

cnf(u1613,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,true,true) ).

cnf(u2358,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Class),true,true,true),true) ).

cnf(u2327,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Literal,uri_rdfs_Literal),true,true,true),true) ).

cnf(u394,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1529,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_owl_complementOf,uri_owl_complementOf),true,true,true),true) ).

cnf(u1804,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__1,X1),true,true,true),true) ).

cnf(u1630,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_domain,uri_rdfs_domain),true) ).

cnf(u2560,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u2695,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class) ).

cnf(u4106,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,iext(uri_rdf_predicate,X0,X1),true) ).

cnf(u2577,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Alt,X1),true,true,true),true) ).

cnf(u3732,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource) ).

cnf(u283,negated_conjecture,
    true = sF26 ).

cnf(u764,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_A,uri_owl_Class),true,true,true),true) ).

cnf(u392,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u2455,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_seeAlso),true) ).

cnf(u1067,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

cnf(u651,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u542,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3215,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0),true) ).

cnf(u2351,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u4104,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_predicate),true) ).

cnf(u1559,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range) ).

cnf(u1180,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),true,true,true),true) ).

cnf(u411,negated_conjecture,
    true = iext(uri_rdf_first,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y) ).

cnf(u304,negated_conjecture,
    true = sF33 ).

cnf(u398,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).

cnf(u797,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2),true) ).

cnf(u1319,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u2429,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdfs_Class),true,true,true),true) ).

cnf(u1195,negated_conjecture,
    true = ip(uri_rdfs_isDefinedBy) ).

cnf(u670,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_List),true,true,true),true) ).

cnf(u3237,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0),true) ).

cnf(u1184,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u55,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,icext(X1,X0),true) ).

cnf(u3103,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u409,negated_conjecture,
    true = iext(uri_rdf_rest,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,uri_rdf_nil) ).

cnf(u676,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u310,negated_conjecture,
    true = sF35 ).

cnf(u5693,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Class),true) ).

cnf(u925,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdfs_Container),true,true,true),true) ).

cnf(u4180,axiom,
    true = iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class) ).

cnf(u691,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0),true,iext(X0,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y,uri_ex_A),true) ).

cnf(u2193,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_subClassOf) ).

cnf(u2972,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member) ).

cnf(u53,axiom,
    true = ifeq(icext(X0,X1),true,iext(uri_rdf_type,X1,X0),true) ).

cnf(u2543,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,X1),true,true,true),true) ).

cnf(u1599,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_range),true) ).

cnf(u4025,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdf_Property),true,true,true),true) ).

cnf(u3233,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdfs_member),true) ).

cnf(u1707,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,uri_rdf_nil),true,true,true),true) ).

cnf(u1598,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u2289,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_isDefinedBy),true,true,true),true) ).

cnf(u4193,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),true) ).

cnf(u2991,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2),true,true,true),true) ).

cnf(u1228,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__2) ).

cnf(u582,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1853,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1) ).

cnf(u3128,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_first,X1),true,true,true),true) ).

cnf(u588,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__3,uri_rdfs_Resource),true) ).

cnf(u436,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u1726,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,X0),true,icext(X0,uri_ex_w),true) ).

cnf(u1669,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_Class),true,ifeq(iext(X0,uri_ex_B,X1),true,true,true),true) ).

cnf(u2111,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Container),true) ).

cnf(u3286,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Property,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3139,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u2404,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),true) ).

cnf(u1602,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,iext(uri_rdfs_range,X0,X1),true) ).

cnf(u2843,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Container,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2900,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true,true,true),true) ).

cnf(u1966,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u2747,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Resource),true,true,true),true) ).

cnf(u4173,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,X1),true,true,true),true) ).

cnf(u3159,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0),true) ).

cnf(u698,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_nil,uri_rdf_List),true) ).

cnf(u1732,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__2,X1),true,true,true),true) ).

cnf(u2379,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u576,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u1066,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u3294,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u607,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u2992,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,X1),true,true,true),true) ).

cnf(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u1364,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource) ).

cnf(u1494,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_complementOf,uri_rdf_Property) ).

cnf(u1893,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_type,uri_rdf_type),true,true,true),true) ).

cnf(u1249,negated_conjecture,
    true = ip(uri_rdf__2) ).

cnf(u367,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).

cnf(u704,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u338,negated_conjecture,
    true = sF44 ).

cnf(u721,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_subject,uri_rdf_Property),true) ).

cnf(u476,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u2891,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u735,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u1897,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u967,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdfs_Container),true,true,true),true) ).

cnf(u1218,negated_conjecture,
    true = icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,uri_ex_w) ).

cnf(u3785,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Statement),true) ).

cnf(u860,negated_conjecture,
    true = ip(uri_owl_intersectionOf) ).

cnf(u211,negated_conjecture,
    true = sF2 ).

cnf(u365,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).

cnf(u1100,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u1076,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u3016,negated_conjecture,
    true = iext(uri_rdf_type,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1,uri_rdf_List) ).

cnf(u3799,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_List,X1),true,true,true),true) ).

cnf(u466,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u2521,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf) ).

cnf(u238,negated_conjecture,
    true = sF11 ).

cnf(u662,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u1227,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2) ).

cnf(u3805,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u2025,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u2684,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource) ).

cnf(u123,negated_conjecture,
    true = ifeq(lv(X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u988,negated_conjecture,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,true,true) ).

cnf(u633,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u378,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

cnf(u3792,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Statement,X0),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u1247,negated_conjecture,
    true = ip(uri_rdf_object) ).

cnf(u1385,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral) ).

cnf(u2420,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Bag,X1),true,true,true),true) ).

cnf(u1509,negated_conjecture,
    true = icext(uri_rdf_Property,uri_owl_complementOf) ).

cnf(u1007,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u121,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,lv(X0),true) ).

cnf(u3262,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2819,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5593,negated_conjecture,
    true = ifeq(icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,X0),true,icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,X0),true) ).

cnf(u5727,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_owl_Class),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u3214,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u376,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource) ).

cnf(u506,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u2008,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype) ).

cnf(u226,negated_conjecture,
    true = sF7 ).

cnf(u5726,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_owl_Class,X0),true) ).

cnf(u1916,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_owl_intersectionOf,uri_owl_intersectionOf),true,true,true),true) ).

cnf(u791,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,X0),true,iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1),true) ).

cnf(u127,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property) ).

cnf(u2082,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__3,uri_rdf__3),true,true,true),true) ).

cnf(u2561,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),true) ).

cnf(u3716,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Statement),true,true,true),true) ).

cnf(u5721,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_owl_Class,uri_rdfs_Resource),true) ).

cnf(u748,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_A),true) ).

cnf(u4075,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_label,uri_rdfs_label),true,true,true),true) ).

cnf(u382,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u1159,negated_conjecture,
    true = ic(uri_rdfs_Class) ).

cnf(u1121,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u4081,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_label),true) ).

cnf(u4612,negated_conjecture,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u763,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u526,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u3235,negated_conjecture,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u1040,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_type,uri_rdf_Property),true) ).

cnf(u919,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true) ).

cnf(u33,axiom,
    true = iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).

cnf(u265,negated_conjecture,
    true = sF20 ).

cnf(u532,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u395,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).

cnf(u2535,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_subPropertyOf) ).

cnf(u5578,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true,true,true),true) ).

cnf(u510,negated_conjecture,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,true,true) ).

cnf(u1920,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_intersectionOf),true) ).

cnf(u1425,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest) ).

cnf(u1828,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u2828,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u654,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_object,uri_rdfs_Statement),true,true,true),true) ).

cnf(u2333,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Literal),true) ).

cnf(u2331,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u5537,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true,true,true),true) ).

cnf(u1671,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Class,X0),true,icext(X0,uri_ex_B),true) ).

cnf(u393,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).

cnf(u660,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_object,uri_rdfs_Statement),true) ).

cnf(u677,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,icext(uri_rdf_List,X0),true) ).

cnf(u2950,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Literal,uri_rdfs_Class),true,true,true),true) ).

cnf(u1956,negated_conjecture,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,iext(uri_rdf__1,X0,X1),true) ).

cnf(u2091,negated_conjecture,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,iext(uri_rdf__3,X0,X1),true) ).

cnf(u566,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u2956,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Class),true) ).

cnf(u1310,negated_conjecture,
    true = iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

cnf(u1693,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u5543,negated_conjecture,
    true = iext(uri_rdf_type,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,uri_rdfs_Class) ).

cnf(u2722,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Resource,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3121,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u572,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdfs_Resource),true,true,true),true) ).

cnf(u715,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_subject,uri_rdf_Property),true,true,true),true) ).

cnf(u292,negated_conjecture,
    true = sF29 ).

cnf(u422,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_value,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2728,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Resource,uri_rdfs_Resource),true) ).

cnf(u755,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y),true) ).

cnf(u1314,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,X1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1697,negated_conjecture,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,iext(uri_rdf_first,X0,X1),true) ).

cnf(u2219,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Datatype),true) ).

cnf(u5694,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_owl_Class,uri_owl_Class),true) ).

cnf(u1438,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u165,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(X0,X2,X3),true,iext(X1,X2,X3),true),true) ).

cnf(u3112,axiom,
    true = ifeq(icext(uri_rdf_Property,X0),true,icext(uri_rdf_Property,X0),true) ).

cnf(u2105,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Container,uri_rdfs_Container),true,true,true),true) ).

cnf(u700,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdfs_Statement),true,true,true),true) ).

cnf(u420,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_w,uri_ex_B),true,sF52,true),true) ).

cnf(u1434,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_rest),true,true,true),true) ).

cnf(u1710,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,uri_rdf_nil),true) ).

cnf(u522,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_member,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1471,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_value,uri_rdf_value),true) ).

cnf(u1716,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__3,X1),true,true,true),true) ).

cnf(u947,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u3006,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,uri_rdf_List),true) ).

cnf(u1443,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,iext(uri_rdf_rest,X0,X1),true) ).

cnf(u2233,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

cnf(u1185,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u4012,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_predicate),true,true,true),true) ).

cnf(u2407,negated_conjecture,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,iext(uri_rdfs_isDefinedBy,X0,X1),true) ).

cnf(u2889,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u682,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_rest,X0),true,icext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2),true) ).

cnf(u1969,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u437,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u5552,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) ).

cnf(u1983,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u332,negated_conjecture,
    true = sF42 ).

cnf(u2875,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1093,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u3136,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_type),true,true,true),true) ).

cnf(u3271,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u1354,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property) ).

cnf(u3017,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1),true) ).

cnf(u1628,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u4174,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u205,negated_conjecture,
    true = sF0 ).

cnf(u2384,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,iext(uri_rdfs_subClassOf,X0,X1),true) ).

cnf(u3000,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2,uri_rdf_List),true,true,true),true) ).

cnf(u1765,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_owl_intersectionOf,X1),true,true,true),true) ).

cnf(u460,negated_conjecture,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,true,true) ).

cnf(u4179,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u1221,negated_conjecture,
    true = icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).

cnf(u1233,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_Property) ).

cnf(u3940,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_comment),true,true,true),true) ).

cnf(u2151,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Literal) ).

cnf(u450,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,true,true) ).

cnf(u1225,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).

cnf(u4187,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),true,true,true),true) ).

cnf(u2662,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Class,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1133,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_domain,uri_rdf_Property),true) ).

cnf(u3014,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1),true,true,true),true) ).

cnf(u1365,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_Alt) ).

cnf(u3815,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List) ).

cnf(u722,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__1,uri_rdf_Property),true,true,true),true) ).

cnf(u2009,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource) ).

cnf(u2668,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Resource),true) ).

cnf(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u2849,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Resource),true) ).

cnf(u401,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) ).

cnf(u2149,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal) ).

cnf(u728,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdf_Property),true) ).

cnf(u362,negated_conjecture,
    true != sF52 ).

cnf(u448,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_subject,uri_rdfs_Resource),true) ).

cnf(u1231,axiom,
    true = icext(uri_rdf_Property,uri_rdf_rest) ).

cnf(u1549,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_subject,X1),true,true,true),true) ).

cnf(u220,negated_conjecture,
    true = sF5 ).

cnf(u707,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u1493,negated_conjecture,
    true = ifeq(iext(uri_owl_complementOf,X0,X1),true,true,true) ).

cnf(u1112,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Property,uri_rdfs_Class),true) ).

cnf(u991,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_type,uri_rdfs_Class),true,true,true),true) ).

cnf(u3169,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property) ).

cnf(u235,negated_conjecture,
    true = sF10 ).

cnf(u2150,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource) ).

cnf(u5605,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2480,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Class),true,true,true),true) ).

cnf(u1143,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_first,uri_rdf_Property),true) ).

cnf(u490,negated_conjecture,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,true,true) ).

cnf(u5617,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u2232,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u2777,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Resource),true) ).

cnf(u1006,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u1405,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_value,X1),true,true,true),true) ).

cnf(u2473,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u111,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class) ).

cnf(u1898,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u2673,negated_conjecture,
    true = ic(uri_rdfs_Resource) ).

cnf(u3828,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_List,uri_rdfs_Class),true) ).

cnf(u379,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

cnf(u366,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).

cnf(u2421,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class) ).

cnf(u488,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_Resource),true) ).

cnf(u1017,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u3082,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u747,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_first,X0),true,icext(X0,sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1),true) ).

cnf(u1533,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_complementOf),true) ).

cnf(u1024,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_range,uri_rdfs_Class),true,true,true),true) ).

cnf(u4079,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u2026,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Seq),true) ).

cnf(u377,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) ).

cnf(u516,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u1806,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u250,negated_conjecture,
    true = sF15 ).

cnf(u3081,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u1837,negated_conjecture,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,icext(uri_rdf_XMLLiteral,X0),true) ).

cnf(u1644,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdf_Property),true,true,true),true) ).

cnf(u2292,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u2317,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u1152,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_rest,uri_rdf_Property),true) ).

cnf(u2578,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class) ).

cnf(u2179,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWB029-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36  % Computer : n014.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.37  % CPULimit : 300
% 0.09/0.37  % WCLimit  : 300
% 0.09/0.37  % DateTime : Mon Sep 28 07:06:31 UTC 2026
% 0.09/0.37  % CPUTime  : 
% 0.09/0.37  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40  Running first-order theorem proving
% 0.09/0.40  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.99/1.94  % (1597782)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.99/1.94  % (1597789)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=4210967716:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.99/1.94  % (1597791)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2204481703:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.99/1.94  % (1597788)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2308531209:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.99/1.94  % (1597793)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1866756134:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.99/1.94  % (1597790)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1415942265:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.99/1.94  % (1597787)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=901855809:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.99/1.94  % (1597792)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3617554065:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.99/1.94  % (1597790)Instruction limit reached! 
% 5.99/1.94  % (1597790)------------------------------
% 5.99/1.94  % (1597790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.94  % (1597790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.94  % (1597790)CaDiCaL version: 2.1.3
% 5.99/1.94  % (1597790)Termination reason: Instruction limit
% 5.99/1.94  % (1597790)Termination phase: Saturation
% 5.99/1.94  % (1597790)Time elapsed: 0.067 s
% 5.99/1.94  % (1597790)Peak memory usage: 88 MB
% 5.99/1.94  % (1597790)Instructions burned: 137 (million)
% 5.99/1.94  % (1597791)Refutation not found, incomplete strategy
% 5.99/1.94  % (1597791)------------------------------
% 5.99/1.94  % (1597791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.94  % (1597791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.94  % (1597791)CaDiCaL version: 2.1.3
% 5.99/1.94  % (1597791)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.94  % (1597791)Time elapsed: 0.074 s
% 5.99/1.94  % (1597791)Peak memory usage: 89 MB
% 5.99/1.94  % (1597791)Instructions burned: 135 (million)
% 5.99/1.94  % (1597792)Instruction limit reached! 
% 5.99/1.94  % (1597792)------------------------------
% 5.99/1.94  % (1597792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.94  % (1597792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.94  % (1597792)CaDiCaL version: 2.1.3
% 5.99/1.94  % (1597792)Termination reason: Instruction limit
% 5.99/1.94  % (1597792)Termination phase: Saturation
% 5.99/1.94  % (1597792)Time elapsed: 0.152 s
% 5.99/1.94  % (1597792)Peak memory usage: 92 MB
% 5.99/1.94  % (1597792)Instructions burned: 257 (million)
% 5.99/1.94  % (1597801)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=570944565:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 5.99/1.94  % (1597793)Refutation not found, incomplete strategy
% 5.99/1.94  % (1597793)------------------------------
% 5.99/1.94  % (1597793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.94  % (1597793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.94  % (1597793)CaDiCaL version: 2.1.3
% 5.99/1.94  % (1597793)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.94  % (1597793)Time elapsed: 0.287 s
% 5.99/1.94  % (1597793)Peak memory usage: 93 MB
% 5.99/1.94  % (1597793)Instructions burned: 568 (million)
% 5.99/1.94  % (1597802)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3383566606:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 5.99/1.94  % (1597791)------------------------------
% 5.99/1.94  % (1597791)------------------------------
% 5.99/1.94  % (1597805)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=778873646:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.99/1.94  % (1597793)------------------------------
% 5.99/1.94  % (1597793)------------------------------
% 5.99/1.94  % (1597805)Instruction limit reached! 
% 5.99/1.94  % (1597805)------------------------------
% 5.99/1.94  % (1597805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.94  % (1597805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.94  % (1597805)CaDiCaL version: 2.1.3
% 5.99/1.94  % (1597805)Termination reason: Instruction limit
% 5.99/1.94  % (1597805)Termination phase: Saturation
% 5.99/1.94  % (1597805)Time elapsed: 0.094 s
% 5.99/1.94  % (1597805)Peak memory usage: 91 MB
% 5.99/1.94  % (1597805)Instructions burned: 215 (million)
% 5.99/1.94  [W928 07:06:32.349933069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 5.99/1.94  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.99/1.94  [W928 07:06:32.349976486 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 5.99/1.94  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.99/1.94  [W928 07:06:32.350023463 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 5.99/1.94  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.99/1.94  [W928 07:06:32.350035806 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 5.99/1.94  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.99/1.94  [W928 07:06:32.350062156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 5.99/1.94  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.99/1.94  [W928 07:06:32.350072919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 5.99/1.94  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.99/1.94  % (1597807)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=85510143:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 5.99/1.94  % (1597808)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=521413144:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 5.99/1.94  % (1597789)First to succeed.
% 5.99/1.94  % (1597789)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1597782"
% 5.99/1.94  % (1597807)Instruction limit reached! 
% 5.99/1.94  % (1597807)------------------------------
% 5.99/1.94  % (1597807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.94  % (1597807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.94  % (1597807)CaDiCaL version: 2.1.3
% 5.99/1.94  % (1597807)Termination reason: Instruction limit
% 5.99/1.94  % (1597807)Termination phase: Saturation
% 5.99/1.94  % (1597807)Time elapsed: 0.176 s
% 5.99/1.94  % (1597807)Peak memory usage: 95 MB
% 5.99/1.94  % (1597807)Instructions burned: 317 (million)
% 5.99/1.94  % (1597802)Refutation not found, incomplete strategy
% 5.99/1.94  % (1597802)------------------------------
% 5.99/1.94  % (1597802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.94  % (1597802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.94  % (1597802)CaDiCaL version: 2.1.3
% 5.99/1.94  % (1597802)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.94  % (1597802)Time elapsed: 0.571 s
% 5.99/1.94  % (1597802)Peak memory usage: 127 MB
% 5.99/1.94  % (1597802)Instructions burned: 860 (million)
% 5.99/1.94  % SZS status Satisfiable for theBenchmark
% 5.99/1.94  % SZS output start Saturation.
% See solution above
% 0.15/2.13  % SZS output start Definitions and Model Updates.
% 0.15/2.13  for all inputs,
% 0.15/2.13      define ir(X0) := true
% 0.15/2.13  % SZS output end Definitions and Model Updates.
% 0.15/2.13  % (1597789)------------------------------
% 0.15/2.13  % (1597789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/2.13  % (1597789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/2.13  % (1597789)CaDiCaL version: 2.1.3
% 0.15/2.13  % (1597789)Termination reason: Satisfiable
% 0.15/2.13  % (1597789)Time elapsed: 0.805 s
% 0.15/2.13  % (1597789)Peak memory usage: 140 MB
% 0.15/2.13  % (1597789)Instructions burned: 2224 (million)
% 0.15/2.13  % (1597789)------------------------------
% 0.15/2.13  % (1597789)------------------------------
% 0.15/2.13  % (1597782)Success in time 1.092 s
% 0.15/2.13  % Vampire exiting
%------------------------------------------------------------------------------