Vampire---5.0.1.SAT-Sat.s

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

% Computer : n018.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:03 PM UTC 2026

% Result   : Satisfiable 12.88s 3.02s
% Output   : Saturation 15.78s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u661,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_member),true) ).

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

cnf(u6879,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction) ).

cnf(u1415,negated_conjecture,
    true = icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).

cnf(u2434,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(u1553,negated_conjecture,
    true = ifeq(iext(uri_owl_sameAs,X0,X1),true,true,true) ).

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

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

cnf(u3657,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1),true) ).

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

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

cnf(u784,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2),true) ).

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

cnf(u2706,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(u521,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u276,negated_conjecture,
    true = sF17 ).

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

cnf(u406,negated_conjecture,
    true = sF60 ).

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

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

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

cnf(u2273,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(u678,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(u1422,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__2) ).

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

cnf(u912,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_JoesGang,uri_ex_Clique),true,true,true),true) ).

cnf(u2458,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(u417,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).

cnf(u2581,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(u1819,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom) ).

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

cnf(u818,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_sameCliqueAs),true) ).

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

cnf(u2427,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_ex_JoesGang),true,ifeq(iext(X0,uri_ex_alice,X1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

cnf(u3262,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(u1077,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u3120,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(u1338,negated_conjecture,
    true = ic(uri_rdfs_Seq) ).

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

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

cnf(u1427,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_Property) ).

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

cnf(u5215,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(u306,negated_conjecture,
    true = sF27 ).

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

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

cnf(u1606,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral) ).

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

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

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

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

cnf(u3283,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(u2396,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource) ).

cnf(u828,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(u2750,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(u2984,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_Clique,uri_rdfs_Class) ).

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

cnf(u7066,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_ex_JoesGang,uri_rdfs_Resource),true) ).

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

cnf(u2831,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(u7101,negated_conjecture,
    true = ic(uri_owl_Class) ).

cnf(u578,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(u7617,negated_conjecture,
    true = icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_ex_JoesGang) ).

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

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

cnf(u333,negated_conjecture,
    true = sF36 ).

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

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

cnf(u432,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u1215,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(u7639,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_JoesGang,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

cnf(u1987,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest) ).

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

cnf(u5779,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

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

cnf(u706,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_owl_onProperty,X0),true,icext(X0,uri_ex_sameCliqueAs),true) ).

cnf(u2876,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(u1092,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u461,negated_conjecture,
    true = iext(uri_rdfs_range,uri_ex_sameCliqueAs,uri_ex_Clique) ).

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

cnf(u346,negated_conjecture,
    true = sF40 ).

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

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

cnf(u3531,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(u2917,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_ex_sameCliqueAs),true) ).

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

cnf(u3008,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(u5207,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource) ).

cnf(u1226,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(u5043,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

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

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

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

cnf(u451,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) ).

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

cnf(u474,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_owl_sameAs) ).

cnf(u3882,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_type),true,true,true),true) ).

cnf(u3921,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(u7235,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_owl_ObjectProperty),true,true,true),true) ).

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

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

cnf(u2412,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

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

cnf(u716,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_propertyChainAxiom),true,ifeq(iext(X0,uri_foaf_knows,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1),true,true,true),true) ).

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

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

cnf(u733,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(u472,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_alice,uri_ex_JoesGang) ).

cnf(u1147,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(u7278,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_owl_ObjectProperty,uri_owl_ObjectProperty),true,true,true),true) ).

cnf(u5340,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(u1379,negated_conjecture,
    true = ip(uri_rdf__3) ).

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

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

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

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

cnf(u361,negated_conjecture,
    true = sF45 ).

cnf(u628,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(u7173,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_owl_Class,X0),true) ).

cnf(u478,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_foaf_knows),true,ifeq(iext(X0,uri_ex_alice,uri_ex_bob),true,sF62,true),true) ).

cnf(u877,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(u5344,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

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

cnf(u234,negated_conjecture,
    true = sF3 ).

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

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

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

cnf(u658,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(u3409,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(u2429,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_ex_JoesGang,X0),true,icext(X0,uri_ex_alice),true) ).

cnf(u6911,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Restriction),true) ).

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

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

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

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

cnf(u1800,negated_conjecture,
    true = icext(uri_rdf_Property,uri_owl_onProperty) ).

cnf(u1527,negated_conjecture,
    true = ifeq(iext(uri_ex_sameCliqueAs,X0,X1),true,true,true) ).

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

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

cnf(u768,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,uri_rdf_nil),true) ).

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

cnf(u273,negated_conjecture,
    true = sF16 ).

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

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

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

cnf(u2307,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(u3344,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true) ).

cnf(u1311,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(u683,negated_conjecture,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

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

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

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

cnf(u3337,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(u1419,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__3) ).

cnf(u2803,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(u4414,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_member),true) ).

cnf(u279,negated_conjecture,
    true = sF18 ).

cnf(u1554,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_sameAs,uri_rdf_Property) ).

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

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

cnf(u388,negated_conjecture,
    true = sF54 ).

cnf(u2435,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(u802,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3),true) ).

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

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

cnf(u1410,negated_conjecture,
    true = icext(uri_ex_JoesGang,uri_ex_bob) ).

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

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

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

cnf(u528,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(u3665,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,uri_rdf_List),true,true,true),true) ).

cnf(u3361,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(u300,negated_conjecture,
    true = sF25 ).

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

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

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

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

cnf(u5794,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(u2985,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_ex_Clique),true) ).

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

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

cnf(u3609,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,X1),true,true,true),true) ).

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

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

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

cnf(u428,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

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

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

cnf(u806,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(u1189,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u3232,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(u687,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(u1888,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_owl_someValuesFrom,uri_owl_someValuesFrom),true) ).

cnf(u3610,negated_conjecture,
    true = iext(uri_rdf_type,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,uri_rdf_List) ).

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

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

cnf(u568,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(u447,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) ).

cnf(u6944,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_owl_Restriction),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

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

cnf(u3633,negated_conjecture,
    true = iext(uri_rdf_type,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,uri_rdf_List) ).

cnf(u2740,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(u3387,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_ex_Clique,uri_rdfs_Resource),true) ).

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

cnf(u7835,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_foaf_knows,uri_rdfs_Resource),true,ifeq(sF62,true,true,true),true) ).

cnf(u2864,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(u690,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u1977,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(u161,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ip(X1),true) ).

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

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

cnf(u445,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).

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

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

cnf(u5290,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List) ).

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

cnf(u2550,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(u2397,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Literal) ).

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

cnf(u4925,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(u1080,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

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

cnf(u7118,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(u435,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource) ).

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

cnf(u2642,negated_conjecture,
    true = ifeq(iext(uri_owl_sameAs,X0,X1),true,iext(uri_owl_sameAs,X0,X1),true) ).

cnf(u330,negated_conjecture,
    true = sF35 ).

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

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

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

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

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

cnf(u2865,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(u1218,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_domain),true) ).

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

cnf(u6870,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class) ).

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

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

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

cnf(u458,negated_conjecture,
    true = iext(uri_owl_propertyChainAxiom,uri_foaf_knows,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) ).

cnf(u7001,negated_conjecture,
    true = ic(uri_ex_JoesGang) ).

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

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

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

cnf(u2759,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(u1116,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(u5086,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(u7141,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Class),true) ).

cnf(u7622,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true,ifeq(iext(X0,uri_ex_JoesGang,X1),true,true,true),true) ).

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

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

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

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

cnf(u1131,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_ex_sameCliqueAs,uri_owl_sameAs),true,true,true),true) ).

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

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

cnf(u7041,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_ex_JoesGang),true) ).

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

cnf(u4941,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(u2752,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__2),true) ).

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

cnf(u475,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_ex_Clique,sK5_testcase_premise_fullish_013_Cliques_BNODE_r) ).

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

cnf(u5232,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(u462,negated_conjecture,
    true = iext(uri_rdf_rest,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) ).

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

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

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

cnf(u2174,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_Restriction),true,ifeq(iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X1),true,true,true),true) ).

cnf(u1491,negated_conjecture,
    true = iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

cnf(u3174,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class) ).

cnf(u1645,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u1248,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(u7110,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource) ).

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

cnf(u473,negated_conjecture,
    true = iext(uri_rdf_type,uri_foaf_knows,uri_owl_ObjectProperty) ).

cnf(u2156,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_ex_Clique),true,ifeq(iext(X0,X1,uri_ex_JoesGang),true,true,true),true) ).

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

cnf(u1912,negated_conjecture,
    true = icext(uri_rdf_Property,uri_owl_someValuesFrom) ).

cnf(u870,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(u1149,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),true) ).

cnf(u7281,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_ObjectProperty),true) ).

cnf(u7291,negated_conjecture,
    true = ifeq(icext(uri_owl_ObjectProperty,X0),true,icext(uri_owl_ObjectProperty,X0),true) ).

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

cnf(u518,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(u2928,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_owl_sameAs,uri_rdf_Property),true) ).

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

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

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

cnf(u2426,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_ex_JoesGang),true,ifeq(iext(X0,X1,uri_ex_alice),true,true,true),true) ).

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

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

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

cnf(u980,negated_conjecture,
    true = ip(uri_owl_propertyChainAxiom) ).

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

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

cnf(u2963,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(u2360,negated_conjecture,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,iext(uri_rdfs_seeAlso,X0,X1),true) ).

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

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

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

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

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

cnf(u385,negated_conjecture,
    true = sF53 ).

cnf(u1555,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,uri_owl_sameAs) ).

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

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

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

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

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

cnf(u786,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2),true) ).

cnf(u759,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(u4220,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Property),true) ).

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

cnf(u1668,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_ex_Clique),true) ).

cnf(u7282,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_ObjectProperty),true) ).

cnf(u1302,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(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,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u261,negated_conjecture,
    true = sF12 ).

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

cnf(u391,negated_conjecture,
    true = sF55 ).

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

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

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

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

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

cnf(u914,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_JoesGang,uri_ex_Clique),true) ).

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

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

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

cnf(u2443,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(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(u7307,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_owl_ObjectProperty,uri_rdfs_Resource),true) ).

cnf(u303,negated_conjecture,
    true = sF26 ).

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

cnf(u5190,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(u1049,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u412,negated_conjecture,
    true != sF62 ).

cnf(u3556,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(u3202,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(u790,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(u2539,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2741,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(u2583,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__2,uri_rdf__2),true) ).

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

cnf(u2200,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,X0),true,icext(X0,uri_foaf_knows),true) ).

cnf(u3631,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3),true,true,true),true) ).

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

cnf(u2353,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(u1340,negated_conjecture,
    true = ic(uri_rdf_Alt) ).

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

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

cnf(u291,negated_conjecture,
    true = sF22 ).

cnf(u429,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

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

cnf(u1279,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(u400,negated_conjecture,
    true = sF58 ).

cnf(u1183,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(u2601,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject) ).

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

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

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

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

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

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

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

cnf(u3502,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(u7093,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(u312,negated_conjecture,
    true = sF29 ).

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

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

cnf(u2729,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(u5180,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_List) ).

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

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

cnf(u2809,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_subPropertyOf) ).

cnf(u1344,negated_conjecture,
    true = ip(uri_owl_sameAs) ).

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

cnf(u2743,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__3),true) ).

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

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

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

cnf(u1102,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_ex_Clique,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true,true,true),true) ).

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

cnf(u318,negated_conjecture,
    true = sF31 ).

cnf(u3433,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(u440,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource) ).

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

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

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

cnf(u3667,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,uri_rdf_List),true) ).

cnf(u699,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_owl_someValuesFrom,X0),true,icext(X0,uri_ex_Clique),true) ).

cnf(u1357,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(u3656,negated_conjecture,
    true = iext(uri_rdf_type,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,uri_rdf_List) ).

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

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

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

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

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

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

cnf(u7010,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_ex_JoesGang,uri_rdfs_Resource) ).

cnf(u1856,negated_conjecture,
    true = icext(uri_rdf_Property,uri_owl_propertyChainAxiom) ).

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

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

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

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

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

cnf(u1104,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_ex_Clique,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

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

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

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

cnf(u459,negated_conjecture,
    true = iext(uri_owl_someValuesFrom,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_ex_Clique) ).

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

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

cnf(u352,negated_conjecture,
    true = sF42 ).

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

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

cnf(u2184,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,uri_rdf_nil),true) ).

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

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

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

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

cnf(u718,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X0),true,iext(X0,uri_foaf_knows,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1),true) ).

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

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

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

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

cnf(u3747,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(u3147,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(u7242,negated_conjecture,
    true = ic(uri_owl_ObjectProperty) ).

cnf(u457,negated_conjecture,
    true = iext(uri_owl_inverseOf,sK3_testcase_premise_fullish_013_Cliques_BNODE_i,uri_rdf_type) ).

cnf(u724,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_ex_sameCliqueAs,uri_ex_Clique),true,true,true),true) ).

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

cnf(u358,negated_conjecture,
    true = sF44 ).

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

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

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

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

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

cnf(u7009,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_ex_JoesGang,uri_ex_JoesGang) ).

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

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

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

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

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

cnf(u231,negated_conjecture,
    true = sF2 ).

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

cnf(u3185,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(u463,negated_conjecture,
    true = iext(uri_rdf_rest,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) ).

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

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

cnf(u3172,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(u1755,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_owl_inverseOf),true) ).

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

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

cnf(u7637,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_JoesGang,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true,true,true),true) ).

cnf(u1744,negated_conjecture,
    true = icext(uri_rdf_Property,uri_owl_inverseOf) ).

cnf(u1378,negated_conjecture,
    true = ip(uri_rdf_object) ).

cnf(u1761,negated_conjecture,
    true = ifeq(iext(uri_owl_onProperty,X0,X1),true,true,true) ).

cnf(u9964,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_foaf_knows,uri_ex_JoesGang),true,ifeq(sF62,true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u729,negated_conjecture,
    true = ifeq(iext(uri_ex_sameCliqueAs,X0,X1),true,icext(uri_ex_Clique,X1),true) ).

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

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

cnf(u240,negated_conjecture,
    true = sF5 ).

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

cnf(u900,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_owl_Restriction),true) ).

cnf(u2159,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_ex_Clique,X0),true,icext(X0,uri_ex_JoesGang),true) ).

cnf(u618,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(u905,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_foaf_knows,uri_owl_ObjectProperty),true,true,true),true) ).

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

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

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

cnf(u373,negated_conjecture,
    true = sF49 ).

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

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

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

cnf(u246,negated_conjecture,
    true = sF7 ).

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

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

cnf(u2451,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(u1290,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(u1564,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_ex_Clique,uri_rdfs_Resource) ).

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

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

cnf(u7073,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_ex_JoesGang,X0),true) ).

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

cnf(u1414,negated_conjecture,
    true = icext(uri_owl_ObjectProperty,uri_foaf_knows) ).

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

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

cnf(u258,negated_conjecture,
    true = sF11 ).

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

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

cnf(u3211,negated_conjecture,
    true = ic(uri_rdfs_Resource) ).

cnf(u2080,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(u1852,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_owl_propertyChainAxiom,uri_rdf_Property),true) ).

cnf(u774,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(u909,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_owl_ObjectProperty),true) ).

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

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

cnf(u1817,negated_conjecture,
    true = ifeq(iext(uri_owl_propertyChainAxiom,X0,X1),true,true,true) ).

cnf(u3876,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_rest),true) ).

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

cnf(u1412,negated_conjecture,
    true = icext(uri_owl_Class,uri_ex_Clique) ).

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

cnf(u1046,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(u285,negated_conjecture,
    true = sF20 ).

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

cnf(u3069,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(u3081,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(u785,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_rest,X0),true,icext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1),true) ).

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

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

cnf(u5784,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u902,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_owl_Restriction),true) ).

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

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

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

cnf(u1324,negated_conjecture,
    true = ic(uri_rdfs_Class) ).

cnf(u3834,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0),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(u1174,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_type,uri_rdfs_Class),true) ).

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

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

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

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

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

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

cnf(u814,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,uri_ex_sameCliqueAs),true,true,true),true) ).

cnf(u3501,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(u7039,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_ex_JoesGang,uri_ex_JoesGang),true) ).

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

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

cnf(u1178,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,icext(uri_rdfs_Class,X1),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(u4926,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(u1172,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(u403,negated_conjecture,
    true = sF59 ).

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

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

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

cnf(u426,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource) ).

cnf(u825,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,sK3_testcase_premise_fullish_013_Cliques_BNODE_i),true) ).

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

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

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

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

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

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

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

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

cnf(u315,negated_conjecture,
    true = sF30 ).

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

cnf(u668,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(u1186,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_range),true) ).

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

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

cnf(u382,negated_conjecture,
    true = sF52 ).

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

cnf(u5191,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(u2882,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_seeAlso) ).

cnf(u2720,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(u175,axiom,
    true = iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class) ).

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

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

cnf(u443,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).

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

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

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

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

cnf(u1411,negated_conjecture,
    true = icext(uri_ex_Clique,uri_ex_JoesGang) ).

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

cnf(u3514,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(u5196,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u1705,negated_conjecture,
    true = ifeq(iext(uri_owl_inverseOf,X0,X1),true,true,true) ).

cnf(u2395,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal) ).

cnf(u702,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_onProperty),true,ifeq(iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_ex_sameCliqueAs),true,true,true),true) ).

cnf(u1088,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(u2383,negated_conjecture,
    true = ifeq(iext(uri_ex_sameCliqueAs,X0,X1),true,iext(uri_ex_sameCliqueAs,X0,X1),true) ).

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

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

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

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

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

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

cnf(u3728,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u3632,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,X1),true,true,true),true) ).

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

cnf(u6983,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_ex_JoesGang) ).

cnf(u2409,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(u3923,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Property,uri_rdfs_Resource),true) ).

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

cnf(u6936,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_owl_Restriction,uri_rdfs_Resource),true) ).

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

cnf(u3068,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(u3096,negated_conjecture,
    true = iext(uri_rdf_type,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_rdfs_Class) ).

cnf(u1874,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_someValuesFrom,uri_rdf_Property) ).

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

cnf(u3798,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(u1998,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(u2197,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_ObjectProperty),true,ifeq(iext(X0,X1,uri_foaf_knows),true,true,true),true) ).

cnf(u842,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(u1617,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource) ).

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

cnf(u2139,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(u1964,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_range,uri_rdf_Property),true) ).

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

cnf(u2783,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(u2770,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,true,true) ).

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

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

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

cnf(u340,negated_conjecture,
    true = sF37 ).

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

cnf(u470,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_Clique,uri_owl_Class) ).

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

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

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

cnf(u742,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(u1653,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,icext(uri_rdfs_Seq,X0),true) ).

cnf(u7315,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_owl_ObjectProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

cnf(u2890,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(u2522,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_object),true) ).

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

cnf(u2932,negated_conjecture,
    true = icext(uri_rdf_Property,uri_owl_sameAs) ).

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

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

cnf(u468,negated_conjecture,
    true = iext(uri_rdf_type,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_owl_Restriction) ).

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

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

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

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

cnf(u727,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_ex_sameCliqueAs),true) ).

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

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

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

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

cnf(u3611,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2),true) ).

cnf(u1781,negated_conjecture,
    true = ifeq(iext(uri_owl_onProperty,X0,X1),true,iext(uri_owl_onProperty,X0,X1),true) ).

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

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

cnf(u608,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(u487,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_owl_inverseOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u1762,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property) ).

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

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

cnf(u3600,negated_conjecture,
    true = icext(uri_rdf_List,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) ).

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

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

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

cnf(u2686,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(u2064,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u485,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,X0),true,iext(X0,sK3_testcase_premise_fullish_013_Cliques_BNODE_i,uri_rdf_type),true) ).

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

cnf(u7250,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_owl_ObjectProperty) ).

cnf(u370,negated_conjecture,
    true = sF48 ).

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

cnf(u508,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(u7305,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_owl_ObjectProperty,uri_rdfs_Resource),true,true,true),true) ).

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

cnf(u228,negated_conjecture,
    true = sF1 ).

cnf(u3811,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(u886,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_Clique,uri_owl_Class),true) ).

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

cnf(u2168,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Class,X0),true,icext(X0,uri_ex_Clique),true) ).

cnf(u1530,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,uri_ex_sameCliqueAs) ).

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

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

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

cnf(u243,negated_conjecture,
    true = sF6 ).

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

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

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

cnf(u498,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(u769,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_rest,X0),true,icext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3),true) ).

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

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

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

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

cnf(u2816,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(u3463,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1034,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_alice,uri_ex_JoesGang),true,true,true),true) ).

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

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

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

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

cnf(u397,negated_conjecture,
    true = sF57 ).

cnf(u648,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(u282,negated_conjecture,
    true = sF19 ).

cnf(u1629,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_Alt) ).

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

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

cnf(u798,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3),true,true,true),true) ).

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

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

cnf(u1413,negated_conjecture,
    true = icext(uri_owl_Restriction,sK5_testcase_premise_fullish_013_Cliques_BNODE_r) ).

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

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

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

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

cnf(u2182,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(u309,negated_conjecture,
    true = sF28 ).

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

cnf(u2192,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_ex_JoesGang,X0),true,icext(X0,uri_ex_bob),true) ).

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

cnf(u5274,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(u809,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u3159,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(u2570,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2) ).

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

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

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

cnf(u823,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,sK3_testcase_premise_fullish_013_Cliques_BNODE_i),true) ).

cnf(u1160,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(u1818,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_propertyChainAxiom,uri_rdf_Property) ).

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

cnf(u2198,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_ObjectProperty),true,ifeq(iext(X0,uri_foaf_knows,X1),true,true,true),true) ).

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

cnf(u1193,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(u3644,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,uri_rdf_List),true) ).

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

cnf(u558,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(u2221,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_type,uri_rdf_type),true) ).

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

cnf(u3642,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,uri_rdf_List),true,true,true),true) ).

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

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

cnf(u297,negated_conjecture,
    true = sF24 ).

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

cnf(u427,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) ).

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

cnf(u975,axiom,
    true = ifeq(sF62,true,ip(uri_foaf_knows),true) ).

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

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

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

cnf(u1335,negated_conjecture,
    true = ic(uri_ex_Clique) ).

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

cnf(u7314,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,X0),true) ).

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

cnf(u3481,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(u811,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u1584,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,sK5_testcase_premise_fullish_013_Cliques_BNODE_r) ).

cnf(u2219,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(u7094,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(u1725,negated_conjecture,
    true = ifeq(iext(uri_owl_inverseOf,X0,X1),true,iext(uri_owl_inverseOf,X0,X1),true) ).

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

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

cnf(u7241,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_ObjectProperty,uri_rdfs_Class) ).

cnf(u1706,negated_conjecture,
    true = iext(uri_rdf_type,uri_owl_inverseOf,uri_rdf_Property) ).

cnf(u709,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(u1864,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_owl_propertyChainAxiom),true,true,true),true) ).

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

cnf(u3007,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(u3874,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_rest,X1),true,true,true),true) ).

cnf(u598,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(u7261,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_owl_ObjectProperty,uri_rdfs_Class),true) ).

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

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

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

cnf(u697,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0),true,iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_ex_Clique),true) ).

cnf(u324,negated_conjecture,
    true = sF33 ).

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

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

cnf(u2176,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Restriction,X0),true,icext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

cnf(u2760,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(u851,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdf_Property),true) ).

cnf(u726,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_ex_sameCliqueAs,uri_ex_Clique),true) ).

cnf(u6853,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_owl_Restriction) ).

cnf(u343,negated_conjecture,
    true = sF39 ).

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

cnf(u465,negated_conjecture,
    true = iext(uri_rdf_first,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,uri_rdf_type) ).

cnf(u7641,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

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

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

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

cnf(u981,negated_conjecture,
    true = ip(uri_owl_inverseOf) ).

cnf(u3391,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_ex_Clique),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

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

cnf(u2242,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(u1873,negated_conjecture,
    true = ifeq(iext(uri_owl_someValuesFrom,X0,X1),true,true,true) ).

cnf(u979,negated_conjecture,
    true = ip(uri_owl_someValuesFrom) ).

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

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

cnf(u7629,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_JoesGang,sK5_testcase_premise_fullish_013_Cliques_BNODE_r) ).

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

cnf(u471,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_bob,uri_ex_JoesGang) ).

cnf(u6934,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_owl_Restriction,uri_rdfs_Resource),true,true,true),true) ).

cnf(u364,negated_conjecture,
    true = sF46 ).

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

cnf(u1962,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(u1752,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_owl_inverseOf),true,true,true),true) ).

cnf(u3601,negated_conjecture,
    true = icext(uri_rdf_List,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) ).

cnf(u1106,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

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

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

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

cnf(u5255,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(u237,negated_conjecture,
    true = sF4 ).

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

cnf(u469,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_JoesGang,uri_ex_Clique) ).

cnf(u720,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X0),true,icext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1),true) ).

cnf(u8671,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_foaf_knows,uri_foaf_knows),true,ifeq(sF62,true,sF62,true),true) ).

cnf(u3634,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3),true) ).

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

cnf(u492,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,uri_rdf_type),true) ).

cnf(u3173,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(u2907,negated_conjecture,
    true = icext(uri_rdf_Property,uri_ex_sameCliqueAs) ).

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

cnf(u3296,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(u751,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(u1514,negated_conjecture,
    true = ifeq(icext(uri_ex_Clique,X0),true,icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X0),true) ).

cnf(u3555,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(u511,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u3654,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1),true,true,true),true) ).

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

cnf(u2488,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(u6910,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Restriction),true) ).

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

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

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

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

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

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

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

cnf(u225,negated_conjecture,
    true = sF0 ).

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

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

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

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

cnf(u480,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_foaf_knows,X0),true,ifeq(sF62,true,icext(X0,uri_ex_bob),true),true) ).

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

cnf(u252,negated_conjecture,
    true = sF9 ).

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

cnf(u782,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2),true,true,true),true) ).

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

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

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

cnf(u1420,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).

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

cnf(u1268,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(u2181,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(u264,negated_conjecture,
    true = sF13 ).

cnf(u394,negated_conjecture,
    true = sF56 ).

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

cnf(u7074,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_ex_JoesGang),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1529,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_sameCliqueAs,uri_rdf_Property) ).

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

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

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

cnf(u3608,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2),true,true,true),true) ).

cnf(u1137,negated_conjecture,
    true = ifeq(iext(uri_ex_sameCliqueAs,X0,X1),true,iext(uri_owl_sameAs,X0,X1),true) ).

cnf(u8233,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_foaf_knows,uri_rdfs_Resource),true,ifeq(sF62,true,true,true),true) ).

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

cnf(u916,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_ex_Clique),true) ).

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

cnf(u3313,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(u3749,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Property,uri_rdf_Property),true) ).

cnf(u270,negated_conjecture,
    true = sF15 ).

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

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

cnf(u921,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_bob,uri_ex_JoesGang),true) ).

cnf(u5013,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(u1067,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

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

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

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

cnf(u3457,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_rdfs_Resource),true,true,true),true) ).

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

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

cnf(u763,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u548,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(u411,axiom,
    iext(uri_foaf_knows,uri_ex_alice,uri_ex_bob) = sF62 ).

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

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

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

cnf(u3459,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_rdfs_Resource),true) ).

cnf(u2719,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(u2111,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

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

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

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

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

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

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

cnf(u3897,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(u1687,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(u409,negated_conjecture,
    true = sF61 ).

cnf(u1203,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(u3133,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(u2616,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

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

cnf(u2466,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(u1585,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_rdfs_Resource) ).

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

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

cnf(u923,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_ex_JoesGang),true) ).

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

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

cnf(u816,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,uri_ex_sameCliqueAs),true) ).

cnf(u2459,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(u3231,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(u3233,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class) ).

cnf(u1707,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_inverseOf,uri_owl_inverseOf) ).

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

cnf(u1976,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(u2519,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(u3095,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X1),true,true,true),true) ).

cnf(u2190,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_ex_JoesGang),true,ifeq(iext(X0,uri_ex_bob,X1),true,true,true),true) ).

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

cnf(u3385,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_ex_Clique,uri_rdfs_Resource),true,true,true),true) ).

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

cnf(u538,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(u2165,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_Class),true,ifeq(iext(X0,X1,uri_ex_Clique),true,true,true),true) ).

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

cnf(u321,negated_conjecture,
    true = sF32 ).

cnf(u588,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(u349,negated_conjecture,
    true = sF41 ).

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

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

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

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

cnf(u3392,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_ex_Clique,X0),true) ).

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

cnf(u695,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_someValuesFrom),true,ifeq(iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_ex_Clique),true,true,true),true) ).

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

cnf(u835,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(u2749,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(u327,negated_conjecture,
    true = sF34 ).

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

cnf(u7628,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X0),true,icext(X0,uri_ex_JoesGang),true) ).

cnf(u7251,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_rdfs_Resource) ).

cnf(u2189,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_ex_JoesGang),true,ifeq(iext(X0,X1,uri_ex_bob),true,true,true),true) ).

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

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

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

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

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

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

cnf(u2851,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(u698,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0),true,icext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

cnf(u416,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).

cnf(u3148,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class) ).

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

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

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

cnf(u856,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(u4962,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(u3904,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true) ).

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

cnf(u479,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_foaf_knows,X0),true,ifeq(sF62,true,icext(X0,uri_ex_alice),true),true) ).

cnf(u3146,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(u4977,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(u846,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u1109,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X0),true,iext(uri_rdfs_subClassOf,uri_ex_Clique,X0),true) ).

cnf(u978,negated_conjecture,
    true = ip(uri_owl_onProperty) ).

cnf(u5275,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(u1090,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

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

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

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

cnf(u1893,negated_conjecture,
    true = ifeq(iext(uri_owl_someValuesFrom,X0,X1),true,iext(uri_owl_someValuesFrom,X0,X1),true) ).

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

cnf(u367,negated_conjecture,
    true = sF47 ).

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

cnf(u704,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0),true,iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_ex_sameCliqueAs),true) ).

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

cnf(u3848,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(u1237,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(u7000,negated_conjecture,
    true = iext(uri_rdf_type,uri_ex_JoesGang,uri_rdfs_Class) ).

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

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

cnf(u2675,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf) ).

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

cnf(u2021,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(u3021,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Class),true) ).

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

cnf(u466,negated_conjecture,
    true = iext(uri_rdf_first,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,uri_ex_sameCliqueAs) ).

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

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

cnf(u3788,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property) ).

cnf(u3019,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(u982,negated_conjecture,
    true = ip(uri_rdfs_range) ).

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

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

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

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

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

cnf(u2039,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(u355,negated_conjecture,
    true = sF43 ).

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

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

cnf(u744,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_object,uri_rdfs_Statement),true) ).

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

cnf(u464,negated_conjecture,
    true = iext(uri_rdf_rest,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,uri_rdf_nil) ).

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

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

cnf(u1139,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X0),true,iext(uri_rdfs_subPropertyOf,uri_ex_sameCliqueAs,X0),true) ).

cnf(u5243,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Statement,X0),true,icext(uri_rdfs_Statement,X0),true) ).

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

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

cnf(u3724,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(u1258,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(u121,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,lv(X0),true) ).

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

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

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

cnf(u483,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_inverseOf),true,ifeq(iext(X0,sK3_testcase_premise_fullish_013_Cliques_BNODE_i,uri_rdf_type),true,true,true),true) ).

cnf(u2166,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_Class),true,ifeq(iext(X0,uri_ex_Clique,X1),true,true,true),true) ).

cnf(u2293,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype) ).

cnf(u376,negated_conjecture,
    true = sF50 ).

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

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

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

cnf(u6920,negated_conjecture,
    true = ifeq(icext(uri_owl_Restriction,X0),true,icext(uri_owl_Restriction,X0),true) ).

cnf(u127,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property) ).

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

cnf(u249,negated_conjecture,
    true = sF8 ).

cnf(u1036,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_alice,uri_ex_JoesGang),true) ).

cnf(u267,negated_conjecture,
    true = sF14 ).

cnf(u2294,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource) ).

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

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

cnf(u2038,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(u2380,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_ex_sameCliqueAs),true) ).

cnf(u6880,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource) ).

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

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

cnf(u1421,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2) ).

cnf(u919,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_bob,uri_ex_JoesGang),true,true,true),true) ).

cnf(u4998,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(u33,axiom,
    true = iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).

cnf(u255,negated_conjecture,
    true = sF10 ).

cnf(u3244,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(u2689,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u7050,negated_conjecture,
    true = ifeq(icext(uri_ex_JoesGang,X0),true,icext(uri_ex_JoesGang,X0),true) ).

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

cnf(u1138,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_ex_sameCliqueAs),true,iext(uri_rdfs_subPropertyOf,X0,uri_owl_sameAs),true) ).

cnf(u288,negated_conjecture,
    true = sF21 ).

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

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

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

cnf(u1425,axiom,
    true = icext(uri_rdf_Property,uri_rdf_rest) ).

cnf(u2330,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(u2094,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(u779,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

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

cnf(u1565,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_ex_Clique) ).

cnf(u5299,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(u2951,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

cnf(u1546,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property) ).

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

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

cnf(u1563,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_ex_Clique,uri_ex_Clique) ).

cnf(u294,negated_conjecture,
    true = sF23 ).

cnf(u7164,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(u1832,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom),true) ).

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

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

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

cnf(u2450,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(u1260,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Property,uri_rdfs_Class),true) ).

cnf(u1323,negated_conjecture,
    true = ic(sK5_testcase_premise_fullish_013_Cliques_BNODE_r) ).

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

cnf(u1676,negated_conjecture,
    true = ifeq(icext(uri_ex_Clique,X0),true,icext(uri_ex_Clique,X0),true) ).

cnf(u907,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_foaf_knows,uri_owl_ObjectProperty),true) ).

cnf(u3222,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource) ).

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

cnf(u800,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3),true) ).

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

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

cnf(u3121,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(u3812,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(u1691,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

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

cnf(u821,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,sK3_testcase_premise_fullish_013_Cliques_BNODE_i),true,true,true),true) ).

cnf(u2728,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(u1343,negated_conjecture,
    true = ip(uri_rdfs_seeAlso) ).

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

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

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

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

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

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

cnf(u2612,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(u165,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(X0,X2,X3),true,iext(X1,X2,X3),true),true) ).

cnf(u9834,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_foaf_knows,uri_ex_JoesGang),true,ifeq(sF62,true,true,true),true) ).

cnf(u1586,negated_conjecture,
    true = icext(uri_rdfs_Class,sK5_testcase_premise_fullish_013_Cliques_BNODE_r) ).

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

cnf(u7137,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(u4418,negated_conjecture,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

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

cnf(u2467,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(u7224,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_owl_ObjectProperty) ).

cnf(u2095,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(u554,negated_conjecture,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,true,true) ).

cnf(u4412,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(u2173,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_Restriction),true,ifeq(iext(X0,X1,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true,true,true),true) ).

cnf(u3568,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(u560,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

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

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

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

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

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

cnf(u3464,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X0),true) ).

cnf(u2889,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(u2223,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u1074,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(u2491,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__1),true) ).

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

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

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

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

cnf(u3284,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(u4967,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u7064,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_ex_JoesGang,uri_rdfs_Resource),true,true,true),true) ).

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

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

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

cnf(u1348,negated_conjecture,
    true = ip(uri_ex_sameCliqueAs) ).

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

cnf(u1942,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(u3655,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,X1),true,true,true),true) ).

cnf(u705,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_onProperty,X0),true,icext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

cnf(u460,negated_conjecture,
    true = iext(uri_owl_onProperty,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_ex_sameCliqueAs) ).

cnf(u1875,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,uri_owl_someValuesFrom) ).

cnf(u3621,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,uri_rdf_List),true) ).

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

cnf(u2120,negated_conjecture,
    true = ifeq(icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X0),true,icext(sK5_testcase_premise_fullish_013_Cliques_BNODE_r,X0),true) ).

cnf(u719,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X0),true,icext(X0,uri_foaf_knows),true) ).

cnf(u2060,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(u3770,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(u844,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u3619,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK2_testcase_premise_fullish_013_Cliques_BNODE_l2,uri_rdf_List),true,true,true),true) ).

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

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

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

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

cnf(u849,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(u2772,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf) ).

cnf(u1133,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_ex_sameCliqueAs,uri_owl_sameAs),true) ).

cnf(u3602,negated_conjecture,
    true = icext(uri_rdf_List,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) ).

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

cnf(u863,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(u4961,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(u2442,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(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u1108,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_ex_Clique),true,iext(uri_rdfs_subClassOf,X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true) ).

cnf(u339,negated_conjecture,
    true = sF38 ).

cnf(u477,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_foaf_knows,X0),true,ifeq(sF62,true,iext(X0,uri_ex_alice,uri_ex_bob),true),true) ).

cnf(u728,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_ex_Clique),true) ).

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

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

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

cnf(u5040,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(u5322,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

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

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

cnf(u5316,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(u4997,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(u2023,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdf_Bag),true) ).

cnf(u884,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_Clique,uri_owl_Class),true,true,true),true) ).

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

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

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

cnf(u467,negated_conjecture,
    true = iext(uri_rdf_first,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,sK3_testcase_premise_fullish_013_Cliques_BNODE_i) ).

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

cnf(u490,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK1_testcase_premise_fullish_013_Cliques_BNODE_l1,uri_rdf_type),true,true,true),true) ).

cnf(u6871,negated_conjecture,
    true = ic(uri_owl_Restriction) ).

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

cnf(u1497,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(u5092,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,iext(uri_rdf_predicate,X0,X1),true) ).

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

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

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

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

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

cnf(u111,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class) ).

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

cnf(u379,negated_conjecture,
    true = sF51 ).

cnf(u5063,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(u2421,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u898,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r,uri_owl_Restriction),true,true,true),true) ).

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

cnf(u3826,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(u418,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).

cnf(u1641,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(u2157,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_ex_Clique),true,ifeq(iext(X0,uri_ex_JoesGang,X1),true,true,true),true) ).

cnf(u747,negated_conjecture,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u638,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(u6943,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_owl_Restriction,X0),true) ).

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

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

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

cnf(u1105,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_ex_Clique),true) ).

cnf(u1763,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty) ).

cnf(u494,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_rdf_type),true) ).

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

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

cnf(u7623,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,sK5_testcase_premise_fullish_013_Cliques_BNODE_r),true,ifeq(iext(X0,X1,uri_ex_JoesGang),true,true,true),true) ).

cnf(u1409,negated_conjecture,
    true = icext(uri_ex_JoesGang,uri_ex_alice) ).

cnf(u1837,negated_conjecture,
    true = ifeq(iext(uri_owl_propertyChainAxiom,X0,X1),true,iext(uri_owl_propertyChainAxiom,X0,X1),true) ).

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

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

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

cnf(u891,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(u766,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK4_testcase_premise_fullish_013_Cliques_BNODE_l3,uri_rdf_nil),true,true,true),true) ).

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

cnf(u7040,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_ex_JoesGang),true) ).

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

cnf(u1060,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(u2817,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(u644,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,true,true) ).

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


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWB013-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36  % Computer : n018.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.36  % CPULimit : 300
% 0.10/0.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Mon Sep 28 07:01:25 UTC 2026
% 0.10/0.36  % CPUTime  : 
% 0.10/0.37  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40  Running first-order theorem proving
% 0.10/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
% 12.88/3.02  % (3192335)Detected a unit-equality problem, will run specialized UEQ schedule.
% 12.88/3.02  % (3192357)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2084355548:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 12.88/3.02  % (3192359)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2978283230:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 12.88/3.02  % (3192355)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=448730313:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 12.88/3.02  % (3192356)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=1314494888:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 12.88/3.02  % (3192358)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2027430398:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 12.88/3.02  % (3192360)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2245484094:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 12.88/3.02  % (3192362)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3398032769:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 12.88/3.02  % (3192359)Refutation not found, incomplete strategy
% 12.88/3.02  % (3192359)------------------------------
% 12.88/3.02  % (3192359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192359)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192359)Termination reason: Refutation not found, incomplete strategy
% 12.88/3.02  % (3192359)Time elapsed: 0.137 s
% 12.88/3.02  % (3192359)Peak memory usage: 89 MB
% 12.88/3.02  % (3192359)Instructions burned: 141 (million)
% 12.88/3.02  % (3192358)Instruction limit reached! 
% 12.88/3.02  % (3192358)------------------------------
% 12.88/3.02  % (3192358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192358)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192358)Termination reason: Instruction limit
% 12.88/3.02  % (3192358)Termination phase: Saturation
% 12.88/3.02  % (3192358)Time elapsed: 0.124 s
% 12.88/3.02  % (3192358)Peak memory usage: 88 MB
% 12.88/3.02  % (3192358)Instructions burned: 136 (million)
% 12.88/3.02  % (3192360)Instruction limit reached! 
% 12.88/3.02  % (3192360)------------------------------
% 12.88/3.02  % (3192360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192360)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192360)Termination reason: Instruction limit
% 12.88/3.02  % (3192360)Termination phase: Saturation
% 12.88/3.02  % (3192360)Time elapsed: 0.241 s
% 12.88/3.02  % (3192360)Peak memory usage: 93 MB
% 12.88/3.02  % (3192360)Instructions burned: 258 (million)
% 12.88/3.02  % (3192375)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1719175984:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 12.88/3.02  % (3192376)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2658128011:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 12.88/3.02  % (3192359)------------------------------
% 12.88/3.02  % (3192359)------------------------------
% 12.88/3.02  % (3192362)Refutation not found, incomplete strategy
% 12.88/3.02  % (3192362)------------------------------
% 12.88/3.02  % (3192362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192362)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192362)Termination reason: Refutation not found, incomplete strategy
% 12.88/3.02  % (3192362)Time elapsed: 0.626 s
% 12.88/3.02  % (3192362)Peak memory usage: 95 MB
% 12.88/3.02  % (3192362)Instructions burned: 744 (million)
% 12.88/3.02  % (3192383)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=556888679:i=215:ep=RSTC_2992 on theBenchmark for (2992ds/215Mi)
% 12.88/3.02  % (3192383)Instruction limit reached! 
% 12.88/3.02  % (3192383)------------------------------
% 12.88/3.02  % (3192383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192383)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192383)Termination reason: Instruction limit
% 12.88/3.02  % (3192383)Termination phase: Saturation
% 12.88/3.02  % (3192383)Time elapsed: 0.122 s
% 12.88/3.02  % (3192383)Peak memory usage: 92 MB
% 12.88/3.02  % (3192383)Instructions burned: 217 (million)
% 12.88/3.02  % (3192362)------------------------------
% 12.88/3.02  % (3192362)------------------------------
% 12.88/3.02  % (3192389)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=4171450259:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/317Mi)
% 12.88/3.02  % (3192390)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=2556205314:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/12125Mi)
% 12.88/3.02  % (3192389)Instruction limit reached! 
% 12.88/3.02  % (3192389)------------------------------
% 12.88/3.02  % (3192389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192389)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192389)Termination reason: Instruction limit
% 12.88/3.02  % (3192389)Termination phase: Saturation
% 12.88/3.02  % (3192389)Time elapsed: 0.173 s
% 12.88/3.02  % (3192389)Peak memory usage: 96 MB
% 12.88/3.02  % (3192389)Instructions burned: 318 (million)
% 12.88/3.02  % (3192394)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2721531280:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2986 on theBenchmark for (2986ds/2836Mi)
% 12.88/3.02  % (3192355)Refutation not found, incomplete strategy
% 12.88/3.02  % (3192355)------------------------------
% 12.88/3.02  % (3192355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192355)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192355)Termination reason: Refutation not found, incomplete strategy
% 12.88/3.02  % (3192355)Time elapsed: 1.359 s
% 12.88/3.02  % (3192355)Peak memory usage: 146 MB
% 12.88/3.02  % (3192355)Instructions burned: 2716 (million)
% 12.88/3.02  % (3192355)------------------------------
% 12.88/3.02  % (3192355)------------------------------
% 12.88/3.02  % (3192501)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2569645610:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2982 on theBenchmark for (2982ds/14534Mi)
% 12.88/3.02  % (3192357)First to succeed.
% 12.88/3.02  % (3192357)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3192335"
% 12.88/3.02  % (3192390)Refutation not found, incomplete strategy
% 12.88/3.02  % (3192390)------------------------------
% 12.88/3.02  % (3192390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192390)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192390)Termination reason: Refutation not found, incomplete strategy
% 12.88/3.02  % (3192390)Time elapsed: 0.631 s
% 12.88/3.02  % (3192390)Peak memory usage: 128 MB
% 12.88/3.02  % (3192390)Instructions burned: 951 (million)
% 12.88/3.02  % (3192394)Also succeeded, but the first one will report.
% 12.88/3.02  % (3192375)Instruction limit reached! 
% 12.88/3.02  % (3192375)------------------------------
% 12.88/3.02  % (3192375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/3.02  % (3192375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/3.02  % (3192375)CaDiCaL version: 2.1.3
% 12.88/3.02  % (3192375)Termination reason: Instruction limit
% 12.88/3.02  % (3192375)Termination phase: Saturation
% 12.88/3.02  % (3192375)Time elapsed: 1.550 s
% 12.88/3.02  % (3192375)Peak memory usage: 141 MB
% 12.88/3.02  % (3192375)Instructions burned: 2052 (million)
% 12.88/3.02  % SZS status Satisfiable for theBenchmark
% 12.88/3.02  % SZS output start Saturation.
% See solution above
% 15.78/3.21  % SZS output start Definitions and Model Updates.
% 15.78/3.21  for all inputs,
% 15.78/3.21      define ir(X0) := true
% 15.78/3.21  % SZS output end Definitions and Model Updates.
% 15.78/3.21  % (3192357)------------------------------
% 15.78/3.21  % (3192357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.21  % (3192357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.21  % (3192357)CaDiCaL version: 2.1.3
% 15.78/3.21  % (3192357)Termination reason: Satisfiable
% 15.78/3.21  % (3192357)Time elapsed: 1.692 s
% 15.78/3.21  % (3192357)Peak memory usage: 143 MB
% 15.78/3.21  % (3192357)Instructions burned: 2570 (million)
% 15.78/3.21  % (3192357)------------------------------
% 15.78/3.21  % (3192357)------------------------------
% 15.78/3.21  % (3192335)Success in time 2.144 s
% 15.78/3.21  % Vampire exiting
%------------------------------------------------------------------------------