Drodi---4.1.1.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Drodi---4.1.1
% Problem  : COL094-1 : TPTP v9.3.1. Released v2.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n016.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 : Thu Sep 24 12:08:45 PM UTC 2026

% Result   : Unsatisfiable 35.42s 5.30s
% Output   : CNFRefutation 35.42s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    9
%            Number of leaves      :  123
% Syntax   : Number of formulae    :  479 (  63 unt;  86 def)
%            Number of atoms       : 1257 ( 183 equ)
%            Maximal formula atoms :    7 (   2 avg)
%            Number of connectives : 1273 ( 495   ~; 692   |;   0   &)
%                                         (  86 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   11 (   4 avg)
%            Maximal term depth    :    7 (   2 avg)
%            Number of predicates  :   97 (  95 usr;  87 prp; 0-3 aty)
%            Number of functors    :   17 (  17 usr;   8 con; 0-3 aty)
%            Number of variables   :  341 ( 341   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    combK != combS,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f2,axiom,
    ! [P,Q] : combK != comb_app(P,Q),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f3,axiom,
    ! [P,Q] : combS != comb_app(P,Q),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f4,axiom,
    ! [P1,Q1,P2,Q2] :
      ( P1 = P2
      | comb_app(P1,Q1) != comb_app(P2,Q2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f5,axiom,
    ! [P1,Q1,P2,Q2] :
      ( Q1 = Q2
      | comb_app(P1,Q1) != comb_app(P2,Q2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f7,axiom,
    ! [P,Q] :
      ( member(P,comb)
      | ~ member(comb_app(P,Q),comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f8,axiom,
    ! [P,Q] :
      ( member(Q,comb)
      | ~ member(comb_app(P,Q),comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f9,axiom,
    member(combK,comb),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f10,axiom,
    member(combS,comb),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f11,axiom,
    ! [P,Q] :
      ( member(comb_app(P,Q),comb)
      | ~ member(Q,comb)
      | ~ member(P,comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f13,axiom,
    ! [P,Q] :
      ( member(pair(comb_app(comb_app(combK,P),Q),P),contract)
      | ~ member(Q,comb)
      | ~ member(P,comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f14,axiom,
    ! [P,Q,R] :
      ( member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),contract)
      | ~ member(R,comb)
      | ~ member(Q,comb)
      | ~ member(P,comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f15,axiom,
    ! [P,Q,R] :
      ( ap_contractE_c4(P,Q,R)
      | ap_contractE_c3(P,Q,R)
      | ap_contractE_c2(P,Q,R)
      | ap_contractE_c1(P,Q,R)
      | ~ member(pair(comb_app(P,Q),R),contract) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f22,axiom,
    ! [P,Q,R] :
      ( R = comb_app(comb_app(ap_contractE_sk1p(P,Q,R),Q),comb_app(ap_contractE_sk1q(P,Q,R),Q))
      | ~ ap_contractE_c2(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f23,axiom,
    ! [P,Q,R] :
      ( P = comb_app(comb_app(combS,ap_contractE_sk1p(P,Q,R)),ap_contractE_sk1q(P,Q,R))
      | ~ ap_contractE_c2(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f27,axiom,
    ! [P,Q,R] :
      ( member(pair(Q,ap_contractE_sk3q(P,Q,R)),contract)
      | ~ ap_contractE_c4(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f30,axiom,
    ! [R] : ~ member(pair(combK,R),contract),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f31,axiom,
    ! [R] : ~ member(pair(combS,R),contract),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f32,axiom,
    ! [P] :
      ( member(pair(P,P),parcontract)
      | ~ member(P,comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f33,axiom,
    ! [P,Q] :
      ( member(pair(comb_app(comb_app(combK,P),Q),P),parcontract)
      | ~ member(Q,comb)
      | ~ member(P,comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f34,axiom,
    ! [P,Q,R] :
      ( member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),parcontract)
      | ~ member(R,comb)
      | ~ member(Q,comb)
      | ~ member(P,comb) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f35,axiom,
    ! [P,Q,R,S] :
      ( member(pair(comb_app(P,R),comb_app(Q,S)),parcontract)
      | ~ member(pair(R,S),parcontract)
      | ~ member(pair(P,Q),parcontract) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f36,axiom,
    ! [R] :
      ( member(combK,comb)
      | ~ member(pair(combK,R),parcontract) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f37,axiom,
    ! [R] :
      ( R = combK
      | ~ member(pair(combK,R),parcontract) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f38,axiom,
    ! [R] :
      ( member(combS,comb)
      | ~ member(pair(combS,R),parcontract) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f39,axiom,
    ! [R] :
      ( R = combS
      | ~ member(pair(combS,R),parcontract) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f40,axiom,
    ! [P,Q,R] :
      ( ap_parcontractE_c4(P,Q,R)
      | ap_parcontractE_c3(P,Q,R)
      | ap_parcontractE_c2(P,Q,R)
      | ap_parcontractE_c1(P,Q,R)
      | ~ member(pair(comb_app(P,Q),R),parcontract) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f41,axiom,
    ! [P,Q,R] :
      ( member(comb_app(P,Q),comb)
      | ~ ap_parcontractE_c1(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f42,axiom,
    ! [P,Q,R] :
      ( R = comb_app(P,Q)
      | ~ ap_parcontractE_c1(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f45,axiom,
    ! [P,Q,R] :
      ( P = comb_app(combK,R)
      | ~ ap_parcontractE_c2(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f49,axiom,
    ! [P,Q,R] :
      ( R = comb_app(comb_app(ap_parcontractE_sk1p(P,Q,R),Q),comb_app(ap_parcontractE_sk1q(P,Q,R),Q))
      | ~ ap_parcontractE_c3(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f50,axiom,
    ! [P,Q,R] :
      ( P = comb_app(comb_app(combS,ap_parcontractE_sk1p(P,Q,R)),ap_parcontractE_sk1q(P,Q,R))
      | ~ ap_parcontractE_c3(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f51,axiom,
    ! [P,Q,R] :
      ( member(pair(P,ap_parcontractE_sk2q(P,Q,R)),parcontract)
      | ~ ap_parcontractE_c4(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f52,axiom,
    ! [P,Q,R] :
      ( member(pair(Q,ap_parcontractE_sk2s(P,Q,R)),parcontract)
      | ~ ap_parcontractE_c4(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f53,axiom,
    ! [P,Q,R] :
      ( R = comb_app(ap_parcontractE_sk2q(P,Q,R),ap_parcontractE_sk2s(P,Q,R))
      | ~ ap_parcontractE_c4(P,Q,R) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f54,hypothesis,
    member(pair(comb_app(comb_app(combS,p),q),r),parcontract),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f55,negated_conjecture,
    ! [PP,QP] :
      ( ~ member(pair(q,QP),parcontract)
      | ~ member(pair(p,PP),parcontract)
      | r != comb_app(comb_app(combS,PP),QP) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f56,plain,
    combK != combS,
    inference(cnf_transformation,[status(thm)],[f1]) ).

fof(f57,plain,
    ! [X0,X1] : combK != comb_app(X0,X1),
    inference(cnf_transformation,[status(thm)],[f2]) ).

fof(f58,plain,
    ! [X0,X1] : combS != comb_app(X0,X1),
    inference(cnf_transformation,[status(thm)],[f3]) ).

fof(f59,plain,
    ! [P1,P2] :
      ( P1 = P2
      | ! [Q1,Q2] : comb_app(P1,Q1) != comb_app(P2,Q2) ),
    inference(miniscoping,[status(thm)],[f4]) ).

fof(f60,plain,
    ! [X0,X1,X2,X3] :
      ( X0 = X2
      | comb_app(X0,X1) != comb_app(X2,X3) ),
    inference(cnf_transformation,[status(thm)],[f59]) ).

fof(f61,plain,
    ! [Q1,Q2] :
      ( Q1 = Q2
      | ! [P1,P2] : comb_app(P1,Q1) != comb_app(P2,Q2) ),
    inference(miniscoping,[status(thm)],[f5]) ).

fof(f62,plain,
    ! [X0,X1,X2,X3] :
      ( X1 = X3
      | comb_app(X0,X1) != comb_app(X2,X3) ),
    inference(cnf_transformation,[status(thm)],[f61]) ).

fof(f64,plain,
    ! [P] :
      ( member(P,comb)
      | ! [Q] : ~ member(comb_app(P,Q),comb) ),
    inference(miniscoping,[status(thm)],[f7]) ).

fof(f65,plain,
    ! [X0,X1] :
      ( member(X0,comb)
      | ~ member(comb_app(X0,X1),comb) ),
    inference(cnf_transformation,[status(thm)],[f64]) ).

fof(f66,plain,
    ! [Q] :
      ( member(Q,comb)
      | ! [P] : ~ member(comb_app(P,Q),comb) ),
    inference(miniscoping,[status(thm)],[f8]) ).

fof(f67,plain,
    ! [X0,X1] :
      ( member(X1,comb)
      | ~ member(comb_app(X0,X1),comb) ),
    inference(cnf_transformation,[status(thm)],[f66]) ).

fof(f68,plain,
    member(combK,comb),
    inference(cnf_transformation,[status(thm)],[f9]) ).

fof(f69,plain,
    member(combS,comb),
    inference(cnf_transformation,[status(thm)],[f10]) ).

fof(f70,plain,
    ! [X0,X1] :
      ( member(comb_app(X0,X1),comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(cnf_transformation,[status(thm)],[f11]) ).

fof(f72,plain,
    ! [X0,X1] :
      ( member(pair(comb_app(comb_app(combK,X0),X1),X0),contract)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(cnf_transformation,[status(thm)],[f13]) ).

fof(f73,plain,
    ! [X0,X1,X2] :
      ( member(pair(comb_app(comb_app(comb_app(combS,X0),X1),X2),comb_app(comb_app(X0,X2),comb_app(X1,X2))),contract)
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(cnf_transformation,[status(thm)],[f14]) ).

fof(f74,plain,
    ! [X0,X1,X2] :
      ( ap_contractE_c4(X0,X1,X2)
      | ap_contractE_c3(X0,X1,X2)
      | ap_contractE_c2(X0,X1,X2)
      | ap_contractE_c1(X0,X1,X2)
      | ~ member(pair(comb_app(X0,X1),X2),contract) ),
    inference(cnf_transformation,[status(thm)],[f15]) ).

fof(f85,plain,
    ! [X0,X1,X2] :
      ( X2 = comb_app(comb_app(ap_contractE_sk1p(X0,X1,X2),X1),comb_app(ap_contractE_sk1q(X0,X1,X2),X1))
      | ~ ap_contractE_c2(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f22]) ).

fof(f86,plain,
    ! [X0,X1,X2] :
      ( X0 = comb_app(comb_app(combS,ap_contractE_sk1p(X0,X1,X2)),ap_contractE_sk1q(X0,X1,X2))
      | ~ ap_contractE_c2(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f23]) ).

fof(f91,plain,
    ! [X0,X1,X2] :
      ( member(pair(X1,ap_contractE_sk3q(X0,X1,X2)),contract)
      | ~ ap_contractE_c4(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f27]) ).

fof(f95,plain,
    ! [X0] : ~ member(pair(combK,X0),contract),
    inference(cnf_transformation,[status(thm)],[f30]) ).

fof(f96,plain,
    ! [X0] : ~ member(pair(combS,X0),contract),
    inference(cnf_transformation,[status(thm)],[f31]) ).

fof(f97,plain,
    ! [X0] :
      ( member(pair(X0,X0),parcontract)
      | ~ member(X0,comb) ),
    inference(cnf_transformation,[status(thm)],[f32]) ).

fof(f98,plain,
    ! [X0,X1] :
      ( member(pair(comb_app(comb_app(combK,X0),X1),X0),parcontract)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(cnf_transformation,[status(thm)],[f33]) ).

fof(f99,plain,
    ! [X0,X1,X2] :
      ( member(pair(comb_app(comb_app(comb_app(combS,X0),X1),X2),comb_app(comb_app(X0,X2),comb_app(X1,X2))),parcontract)
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(cnf_transformation,[status(thm)],[f34]) ).

fof(f100,plain,
    ! [X0,X1,X2,X3] :
      ( member(pair(comb_app(X0,X2),comb_app(X1,X3)),parcontract)
      | ~ member(pair(X2,X3),parcontract)
      | ~ member(pair(X0,X1),parcontract) ),
    inference(cnf_transformation,[status(thm)],[f35]) ).

fof(f101,plain,
    ( member(combK,comb)
    | ! [R] : ~ member(pair(combK,R),parcontract) ),
    inference(miniscoping,[status(thm)],[f36]) ).

fof(f102,plain,
    ! [X0] :
      ( member(combK,comb)
      | ~ member(pair(combK,X0),parcontract) ),
    inference(cnf_transformation,[status(thm)],[f101]) ).

fof(f103,plain,
    ! [X0] :
      ( X0 = combK
      | ~ member(pair(combK,X0),parcontract) ),
    inference(cnf_transformation,[status(thm)],[f37]) ).

fof(f104,plain,
    ( member(combS,comb)
    | ! [R] : ~ member(pair(combS,R),parcontract) ),
    inference(miniscoping,[status(thm)],[f38]) ).

fof(f105,plain,
    ! [X0] :
      ( member(combS,comb)
      | ~ member(pair(combS,X0),parcontract) ),
    inference(cnf_transformation,[status(thm)],[f104]) ).

fof(f106,plain,
    ! [X0] :
      ( X0 = combS
      | ~ member(pair(combS,X0),parcontract) ),
    inference(cnf_transformation,[status(thm)],[f39]) ).

fof(f107,plain,
    ! [X0,X1,X2] :
      ( ap_parcontractE_c4(X0,X1,X2)
      | ap_parcontractE_c3(X0,X1,X2)
      | ap_parcontractE_c2(X0,X1,X2)
      | ap_parcontractE_c1(X0,X1,X2)
      | ~ member(pair(comb_app(X0,X1),X2),parcontract) ),
    inference(cnf_transformation,[status(thm)],[f40]) ).

fof(f108,plain,
    ! [P,Q] :
      ( member(comb_app(P,Q),comb)
      | ! [R] : ~ ap_parcontractE_c1(P,Q,R) ),
    inference(miniscoping,[status(thm)],[f41]) ).

fof(f109,plain,
    ! [X0,X1,X2] :
      ( member(comb_app(X0,X1),comb)
      | ~ ap_parcontractE_c1(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f108]) ).

fof(f110,plain,
    ! [X0,X1,X2] :
      ( X2 = comb_app(X0,X1)
      | ~ ap_parcontractE_c1(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f42]) ).

fof(f115,plain,
    ! [P,R] :
      ( P = comb_app(combK,R)
      | ! [Q] : ~ ap_parcontractE_c2(P,Q,R) ),
    inference(miniscoping,[status(thm)],[f45]) ).

fof(f116,plain,
    ! [X0,X1,X2] :
      ( X0 = comb_app(combK,X2)
      | ~ ap_parcontractE_c2(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f115]) ).

fof(f121,plain,
    ! [X0,X1,X2] :
      ( X2 = comb_app(comb_app(ap_parcontractE_sk1p(X0,X1,X2),X1),comb_app(ap_parcontractE_sk1q(X0,X1,X2),X1))
      | ~ ap_parcontractE_c3(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f49]) ).

fof(f122,plain,
    ! [X0,X1,X2] :
      ( X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,X2)),ap_parcontractE_sk1q(X0,X1,X2))
      | ~ ap_parcontractE_c3(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f50]) ).

fof(f123,plain,
    ! [X0,X1,X2] :
      ( member(pair(X0,ap_parcontractE_sk2q(X0,X1,X2)),parcontract)
      | ~ ap_parcontractE_c4(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f51]) ).

fof(f124,plain,
    ! [X0,X1,X2] :
      ( member(pair(X1,ap_parcontractE_sk2s(X0,X1,X2)),parcontract)
      | ~ ap_parcontractE_c4(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f52]) ).

fof(f125,plain,
    ! [X0,X1,X2] :
      ( X2 = comb_app(ap_parcontractE_sk2q(X0,X1,X2),ap_parcontractE_sk2s(X0,X1,X2))
      | ~ ap_parcontractE_c4(X0,X1,X2) ),
    inference(cnf_transformation,[status(thm)],[f53]) ).

fof(f126,plain,
    member(pair(comb_app(comb_app(combS,p),q),r),parcontract),
    inference(cnf_transformation,[status(thm)],[f54]) ).

fof(f127,plain,
    ! [QP] :
      ( ~ member(pair(q,QP),parcontract)
      | ! [PP] :
          ( ~ member(pair(p,PP),parcontract)
          | r != comb_app(comb_app(combS,PP),QP) ) ),
    inference(miniscoping,[status(thm)],[f55]) ).

fof(f128,plain,
    ! [X0,X1] :
      ( ~ member(pair(q,X1),parcontract)
      | ~ member(pair(p,X0),parcontract)
      | r != comb_app(comb_app(combS,X0),X1) ),
    inference(cnf_transformation,[status(thm)],[f127]) ).

fof(f129,definition,
    ! [X0] :
      ( sQ0_spl
    <=> ~ member(pair(combK,X0),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).

fof(f130,plain,
    ! [X0] :
      ( ~ sQ0_spl
      | ~ member(pair(combK,X0),parcontract) ),
    inference(component_clause,[status(thm)],[f129]) ).

fof(f132,definition,
    ( sQ1_spl
  <=> member(combK,comb) ),
    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).

fof(f135,plain,
    ( sQ1_spl
    | sQ0_spl ),
    inference(split_clause,[status(thm)],[f102,f129,f132]) ).

fof(f136,definition,
    ! [X0] :
      ( sQ2_spl
    <=> ~ member(pair(combS,X0),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).

fof(f137,plain,
    ! [X0] :
      ( ~ sQ2_spl
      | ~ member(pair(combS,X0),parcontract) ),
    inference(component_clause,[status(thm)],[f136]) ).

fof(f139,definition,
    ( sQ3_spl
  <=> member(combS,comb) ),
    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).

fof(f142,plain,
    ( sQ3_spl
    | sQ2_spl ),
    inference(split_clause,[status(thm)],[f105,f136,f139]) ).

fof(f145,plain,
    member(pair(combS,combS),parcontract),
    inference(resolution,[status(thm)],[f97,f69]) ).

fof(f146,plain,
    ( ~ sQ2_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f145,f137]) ).

fof(f147,plain,
    ~ sQ2_spl,
    inference(contradiction_clause,[status(thm)],[f146]) ).

fof(f149,plain,
    member(pair(combK,combK),parcontract),
    inference(resolution,[status(thm)],[f68,f97]) ).

fof(f150,plain,
    ( ~ sQ0_spl
    | $false ),
    inference(backward_subsumption_resolution,[status(thm)],[f149,f130]) ).

fof(f151,plain,
    ~ sQ0_spl,
    inference(contradiction_clause,[status(thm)],[f150]) ).

fof(f153,plain,
    ! [X0] :
      ( member(comb_app(X0,combS),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f70,f69]) ).

fof(f154,plain,
    member(comb_app(combK,combS),comb),
    inference(resolution,[status(thm)],[f153,f68]) ).

fof(f155,plain,
    member(comb_app(combS,combS),comb),
    inference(resolution,[status(thm)],[f153,f69]) ).

fof(f158,plain,
    member(comb_app(comb_app(combK,combS),combS),comb),
    inference(resolution,[status(thm)],[f154,f153]) ).

fof(f159,plain,
    ! [X0] :
      ( member(comb_app(X0,comb_app(combK,combS)),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f154,f70]) ).

fof(f160,plain,
    member(pair(comb_app(combK,combS),comb_app(combK,combS)),parcontract),
    inference(resolution,[status(thm)],[f154,f97]) ).

fof(f163,plain,
    member(comb_app(comb_app(combS,combS),combS),comb),
    inference(resolution,[status(thm)],[f155,f153]) ).

fof(f164,plain,
    ! [X0] :
      ( member(comb_app(X0,comb_app(combS,combS)),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f155,f70]) ).

fof(f165,plain,
    member(pair(comb_app(combS,combS),comb_app(combS,combS)),parcontract),
    inference(resolution,[status(thm)],[f155,f97]) ).

fof(f168,plain,
    member(comb_app(comb_app(comb_app(combK,combS),combS),combS),comb),
    inference(resolution,[status(thm)],[f158,f153]) ).

fof(f169,plain,
    ! [X0] :
      ( member(comb_app(X0,comb_app(comb_app(combK,combS),combS)),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f158,f70]) ).

fof(f170,plain,
    member(pair(comb_app(comb_app(combK,combS),combS),comb_app(comb_app(combK,combS),combS)),parcontract),
    inference(resolution,[status(thm)],[f158,f97]) ).

fof(f173,plain,
    member(comb_app(comb_app(comb_app(combS,combS),combS),combS),comb),
    inference(resolution,[status(thm)],[f163,f153]) ).

fof(f174,plain,
    ! [X0] :
      ( member(comb_app(X0,comb_app(comb_app(combS,combS),combS)),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f163,f70]) ).

fof(f175,plain,
    member(pair(comb_app(comb_app(combS,combS),combS),comb_app(comb_app(combS,combS),combS)),parcontract),
    inference(resolution,[status(thm)],[f163,f97]) ).

fof(f176,plain,
    ! [X0] :
      ( member(comb_app(combK,combS),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f159,f67]) ).

fof(f179,plain,
    ! [X0,X1] :
      ( member(comb_app(X1,comb_app(X0,comb_app(combK,combS))),comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f159,f70]) ).

fof(f181,definition,
    ! [X0] :
      ( sQ4_spl
    <=> ~ member(X0,comb) ),
    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).

fof(f182,plain,
    ! [X0] :
      ( ~ sQ4_spl
      | ~ member(X0,comb) ),
    inference(component_clause,[status(thm)],[f181]) ).

fof(f184,definition,
    ( sQ5_spl
  <=> member(comb_app(combK,combS),comb) ),
    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).

fof(f185,plain,
    ( ~ sQ5_spl
    | member(comb_app(combK,combS),comb) ),
    inference(component_clause,[status(thm)],[f184]) ).

fof(f187,plain,
    ( sQ5_spl
    | sQ4_spl ),
    inference(split_clause,[status(thm)],[f176,f181,f184]) ).

fof(f196,plain,
    ( ~ sQ4_spl
    | $false ),
    inference(backward_subsumption_resolution,[status(thm)],[f163,f182]) ).

fof(f202,plain,
    ~ sQ4_spl,
    inference(contradiction_clause,[status(thm)],[f196]) ).

fof(f203,plain,
    ( combS = combS
    | ~ member(combS,comb) ),
    inference(resolution,[status(thm)],[f97,f106]) ).

fof(f204,plain,
    ! [X0] :
      ( ~ member(pair(p,X0),parcontract)
      | r != comb_app(comb_app(combS,X0),q)
      | ~ member(q,comb) ),
    inference(resolution,[status(thm)],[f97,f128]) ).

fof(f205,definition,
    ( sQ6_spl
  <=> combS = combS ),
    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).

fof(f208,plain,
    ( sQ6_spl
    | ~ sQ3_spl ),
    inference(split_clause,[status(thm)],[f203,f139,f205]) ).

fof(f209,definition,
    ( sQ7_spl
  <=> member(q,comb) ),
    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).

fof(f212,definition,
    ! [X0] :
      ( sQ8_spl
    <=> ( ~ member(pair(p,X0),parcontract)
        | r != comb_app(comb_app(combS,X0),q) ) ),
    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).

fof(f213,plain,
    ! [X0] :
      ( ~ sQ8_spl
      | ~ member(pair(p,X0),parcontract)
      | r != comb_app(comb_app(combS,X0),q) ),
    inference(component_clause,[status(thm)],[f212]) ).

fof(f215,plain,
    ( sQ8_spl
    | ~ sQ7_spl ),
    inference(split_clause,[status(thm)],[f204,f209,f212]) ).

fof(f217,plain,
    ( ~ member(combK,comb)
    | combK = combK ),
    inference(resolution,[status(thm)],[f103,f97]) ).

fof(f218,definition,
    ( sQ9_spl
  <=> combK = combK ),
    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).

fof(f221,plain,
    ( ~ sQ1_spl
    | sQ9_spl ),
    inference(split_clause,[status(thm)],[f217,f218,f132]) ).

fof(f227,plain,
    ! [X0,X1,X2] :
      ( ~ ap_parcontractE_c1(X1,X0,X2)
      | member(X0,comb) ),
    inference(resolution,[status(thm)],[f67,f109]) ).

fof(f235,plain,
    ! [X0,X1] :
      ( ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c4(comb_app(combK,X0),X1,X0)
      | ap_contractE_c3(comb_app(combK,X0),X1,X0)
      | ap_contractE_c2(comb_app(combK,X0),X1,X0)
      | ap_contractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f74,f72]) ).

fof(f236,plain,
    ! [X0,X1,X2] :
      ( ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c2(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f74,f73]) ).

fof(f238,plain,
    ! [X0] :
      ( member(comb_app(combS,combS),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f164,f67]) ).

fof(f239,definition,
    ( sQ10_spl
  <=> member(comb_app(combS,combS),comb) ),
    introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).

fof(f242,plain,
    ( sQ10_spl
    | sQ4_spl ),
    inference(split_clause,[status(thm)],[f238,f181,f239]) ).

fof(f251,plain,
    ! [X0] :
      ( member(comb_app(comb_app(combK,combS),combS),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f169,f67]) ).

fof(f252,definition,
    ( sQ11_spl
  <=> member(comb_app(comb_app(combK,combS),combS),comb) ),
    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).

fof(f255,plain,
    ( sQ11_spl
    | sQ4_spl ),
    inference(split_clause,[status(thm)],[f251,f181,f252]) ).

fof(f257,plain,
    ! [X0] :
      ( member(comb_app(comb_app(combS,combS),combS),comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f174,f67]) ).

fof(f258,definition,
    ( sQ12_spl
  <=> member(comb_app(comb_app(combS,combS),combS),comb) ),
    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).

fof(f261,plain,
    ( sQ12_spl
    | sQ4_spl ),
    inference(split_clause,[status(thm)],[f257,f181,f258]) ).

fof(f265,plain,
    ! [X0,X1] :
      ( member(X1,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f179,f65]) ).

fof(f266,plain,
    ! [X0,X1] :
      ( member(comb_app(X0,comb_app(combK,combS)),comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb) ),
    inference(resolution,[status(thm)],[f179,f67]) ).

fof(f267,definition,
    ! [X1] :
      ( sQ13_spl
    <=> ( member(X1,comb)
        | ~ member(X1,comb) ) ),
    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).

fof(f270,plain,
    ( sQ13_spl
    | sQ4_spl ),
    inference(split_clause,[status(thm)],[f265,f181,f267]) ).

fof(f271,definition,
    ! [X0] :
      ( sQ14_spl
    <=> ( member(comb_app(X0,comb_app(combK,combS)),comb)
        | ~ member(X0,comb) ) ),
    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).

fof(f274,plain,
    ( sQ4_spl
    | sQ14_spl ),
    inference(split_clause,[status(thm)],[f266,f271,f181]) ).

fof(f282,plain,
    ( ap_parcontractE_c4(combS,combS,comb_app(combS,combS))
    | ap_parcontractE_c3(combS,combS,comb_app(combS,combS))
    | ap_parcontractE_c2(combS,combS,comb_app(combS,combS))
    | ap_parcontractE_c1(combS,combS,comb_app(combS,combS)) ),
    inference(resolution,[status(thm)],[f107,f165]) ).

fof(f283,plain,
    ( ap_parcontractE_c4(combK,combS,comb_app(combK,combS))
    | ap_parcontractE_c3(combK,combS,comb_app(combK,combS))
    | ap_parcontractE_c2(combK,combS,comb_app(combK,combS))
    | ap_parcontractE_c1(combK,combS,comb_app(combK,combS)) ),
    inference(resolution,[status(thm)],[f107,f160]) ).

fof(f285,plain,
    ! [X0,X1] :
      ( ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c4(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c3(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c2(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f107,f98]) ).

fof(f286,plain,
    ! [X0,X1,X2] :
      ( ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f107,f99]) ).

fof(f288,plain,
    ( ap_parcontractE_c4(comb_app(combS,p),q,r)
    | ap_parcontractE_c3(comb_app(combS,p),q,r)
    | ap_parcontractE_c2(comb_app(combS,p),q,r)
    | ap_parcontractE_c1(comb_app(combS,p),q,r) ),
    inference(resolution,[status(thm)],[f107,f126]) ).

fof(f290,plain,
    ! [X0,X1,X2,X3] :
      ( ~ member(pair(X1,X3),parcontract)
      | ~ member(pair(X0,X2),parcontract)
      | ap_parcontractE_c4(X0,X1,comb_app(X2,X3))
      | ap_parcontractE_c3(X0,X1,comb_app(X2,X3))
      | ap_parcontractE_c2(X0,X1,comb_app(X2,X3))
      | ap_parcontractE_c1(X0,X1,comb_app(X2,X3)) ),
    inference(resolution,[status(thm)],[f107,f100]) ).

fof(f291,plain,
    ! [X0,X1] :
      ( ~ member(comb_app(X0,X1),comb)
      | ap_parcontractE_c4(X0,X1,comb_app(X0,X1))
      | ap_parcontractE_c3(X0,X1,comb_app(X0,X1))
      | ap_parcontractE_c2(X0,X1,comb_app(X0,X1))
      | ap_parcontractE_c1(X0,X1,comb_app(X0,X1)) ),
    inference(resolution,[status(thm)],[f107,f97]) ).

fof(f292,definition,
    ( sQ15_spl
  <=> ap_parcontractE_c1(combS,combS,comb_app(combS,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).

fof(f295,definition,
    ( sQ16_spl
  <=> ap_parcontractE_c2(combS,combS,comb_app(combS,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).

fof(f296,plain,
    ( ~ sQ16_spl
    | ap_parcontractE_c2(combS,combS,comb_app(combS,combS)) ),
    inference(component_clause,[status(thm)],[f295]) ).

fof(f297,plain,
    ( sQ16_spl
    | ~ ap_parcontractE_c2(combS,combS,comb_app(combS,combS)) ),
    inference(component_clause,[status(thm)],[f295]) ).

fof(f298,definition,
    ( sQ17_spl
  <=> ap_parcontractE_c3(combS,combS,comb_app(combS,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).

fof(f299,plain,
    ( ~ sQ17_spl
    | ap_parcontractE_c3(combS,combS,comb_app(combS,combS)) ),
    inference(component_clause,[status(thm)],[f298]) ).

fof(f301,definition,
    ( sQ18_spl
  <=> ap_parcontractE_c4(combS,combS,comb_app(combS,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).

fof(f304,plain,
    ( sQ18_spl
    | sQ17_spl
    | sQ16_spl
    | sQ15_spl ),
    inference(split_clause,[status(thm)],[f282,f292,f295,f298,f301]) ).

fof(f305,definition,
    ( sQ19_spl
  <=> ap_parcontractE_c1(combK,combS,comb_app(combK,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).

fof(f308,definition,
    ( sQ20_spl
  <=> ap_parcontractE_c2(combK,combS,comb_app(combK,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).

fof(f309,plain,
    ( ~ sQ20_spl
    | ap_parcontractE_c2(combK,combS,comb_app(combK,combS)) ),
    inference(component_clause,[status(thm)],[f308]) ).

fof(f310,plain,
    ( sQ20_spl
    | ~ ap_parcontractE_c2(combK,combS,comb_app(combK,combS)) ),
    inference(component_clause,[status(thm)],[f308]) ).

fof(f311,definition,
    ( sQ21_spl
  <=> ap_parcontractE_c3(combK,combS,comb_app(combK,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).

fof(f312,plain,
    ( ~ sQ21_spl
    | ap_parcontractE_c3(combK,combS,comb_app(combK,combS)) ),
    inference(component_clause,[status(thm)],[f311]) ).

fof(f314,definition,
    ( sQ22_spl
  <=> ap_parcontractE_c4(combK,combS,comb_app(combK,combS)) ),
    introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).

fof(f317,plain,
    ( sQ22_spl
    | sQ21_spl
    | sQ20_spl
    | sQ19_spl ),
    inference(split_clause,[status(thm)],[f283,f305,f308,f311,f314]) ).

fof(f321,definition,
    ( sQ24_spl
  <=> ap_parcontractE_c2(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS)) ),
    introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).

fof(f322,plain,
    ( ~ sQ24_spl
    | ap_parcontractE_c2(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS)) ),
    inference(component_clause,[status(thm)],[f321]) ).

fof(f334,definition,
    ( sQ28_spl
  <=> ap_parcontractE_c2(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS)) ),
    introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).

fof(f335,plain,
    ( ~ sQ28_spl
    | ap_parcontractE_c2(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS)) ),
    inference(component_clause,[status(thm)],[f334]) ).

fof(f344,definition,
    ( sQ31_spl
  <=> ap_parcontractE_c1(comb_app(combS,p),q,r) ),
    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).

fof(f345,plain,
    ( ~ sQ31_spl
    | ap_parcontractE_c1(comb_app(combS,p),q,r) ),
    inference(component_clause,[status(thm)],[f344]) ).

fof(f347,definition,
    ( sQ32_spl
  <=> ap_parcontractE_c2(comb_app(combS,p),q,r) ),
    introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).

fof(f348,plain,
    ( ~ sQ32_spl
    | ap_parcontractE_c2(comb_app(combS,p),q,r) ),
    inference(component_clause,[status(thm)],[f347]) ).

fof(f350,definition,
    ( sQ33_spl
  <=> ap_parcontractE_c3(comb_app(combS,p),q,r) ),
    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).

fof(f351,plain,
    ( ~ sQ33_spl
    | ap_parcontractE_c3(comb_app(combS,p),q,r) ),
    inference(component_clause,[status(thm)],[f350]) ).

fof(f353,definition,
    ( sQ34_spl
  <=> ap_parcontractE_c4(comb_app(combS,p),q,r) ),
    introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).

fof(f354,plain,
    ( ~ sQ34_spl
    | ap_parcontractE_c4(comb_app(combS,p),q,r) ),
    inference(component_clause,[status(thm)],[f353]) ).

fof(f356,plain,
    ( sQ34_spl
    | sQ33_spl
    | sQ32_spl
    | sQ31_spl ),
    inference(split_clause,[status(thm)],[f288,f344,f347,f350,f353]) ).

fof(f357,plain,
    ( ~ sQ34_spl
    | r = comb_app(ap_parcontractE_sk2q(comb_app(combS,p),q,r),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f354,f125]) ).

fof(f358,plain,
    ( ~ sQ34_spl
    | member(pair(q,ap_parcontractE_sk2s(comb_app(combS,p),q,r)),parcontract) ),
    inference(resolution,[status(thm)],[f354,f124]) ).

fof(f359,plain,
    ( ~ sQ34_spl
    | member(pair(comb_app(combS,p),ap_parcontractE_sk2q(comb_app(combS,p),q,r)),parcontract) ),
    inference(resolution,[status(thm)],[f354,f123]) ).

fof(f360,plain,
    ! [X0,X1] :
      ( comb_app(combK,X0) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(combK,X0),X1,X0)),ap_contractE_sk1q(comb_app(combK,X0),X1,X0))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c4(comb_app(combK,X0),X1,X0)
      | ap_contractE_c3(comb_app(combK,X0),X1,X0)
      | ap_contractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f235,f86]) ).

fof(f361,plain,
    ! [X0,X1] :
      ( X0 = comb_app(comb_app(ap_contractE_sk1p(comb_app(combK,X0),X1,X0),X1),comb_app(ap_contractE_sk1q(comb_app(combK,X0),X1,X0),X1))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c4(comb_app(combK,X0),X1,X0)
      | ap_contractE_c3(comb_app(combK,X0),X1,X0)
      | ap_contractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f235,f85]) ).

fof(f363,plain,
    ! [X0,X1,X2] :
      ( comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f236,f86]) ).

fof(f364,plain,
    ! [X0,X1,X2] :
      ( comb_app(comb_app(X0,X2),comb_app(X1,X2)) = comb_app(comb_app(ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2),comb_app(ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f236,f85]) ).

fof(f366,plain,
    ! [X0,X1] :
      ( X0 = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(combK,X0),X1,X0),X1),comb_app(ap_parcontractE_sk1q(comb_app(combK,X0),X1,X0),X1))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c4(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c2(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f285,f121]) ).

fof(f367,plain,
    ! [X0,X1] :
      ( comb_app(combK,X0) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(combK,X0),X1,X0)),ap_parcontractE_sk1q(comb_app(combK,X0),X1,X0))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c4(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c2(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f285,f122]) ).

fof(f370,plain,
    ( ~ sQ33_spl
    | comb_app(combS,p) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(combS,p),q,r)),ap_parcontractE_sk1q(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f351,f122]) ).

fof(f374,plain,
    ( ~ sQ8_spl
    | ~ member(p,comb)
    | r != comb_app(comb_app(combS,p),q) ),
    inference(resolution,[status(thm)],[f213,f97]) ).

fof(f375,definition,
    ( sQ35_spl
  <=> r = comb_app(comb_app(combS,p),q) ),
    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).

fof(f377,plain,
    ( sQ35_spl
    | r != comb_app(comb_app(combS,p),q) ),
    inference(component_clause,[status(thm)],[f375]) ).

fof(f378,definition,
    ( sQ36_spl
  <=> member(p,comb) ),
    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).

fof(f381,plain,
    ( ~ sQ8_spl
    | ~ sQ36_spl
    | ~ sQ35_spl ),
    inference(split_clause,[status(thm)],[f374,f375,f378,f212]) ).

fof(f384,plain,
    ( ~ sQ32_spl
    | comb_app(combS,p) = comb_app(combK,r) ),
    inference(resolution,[status(thm)],[f348,f116]) ).

fof(f388,plain,
    ( ~ sQ31_spl
    | r = comb_app(comb_app(combS,p),q) ),
    inference(resolution,[status(thm)],[f345,f110]) ).

fof(f389,plain,
    ( ~ sQ31_spl
    | sQ35_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f388,f377]) ).

fof(f390,plain,
    ( ~ sQ31_spl
    | sQ35_spl ),
    inference(contradiction_clause,[status(thm)],[f389]) ).

fof(f395,plain,
    ( ~ sQ21_spl
    | combK = comb_app(comb_app(combS,ap_parcontractE_sk1p(combK,combS,comb_app(combK,combS))),ap_parcontractE_sk1q(combK,combS,comb_app(combK,combS))) ),
    inference(resolution,[status(thm)],[f312,f122]) ).

fof(f397,plain,
    ( ~ sQ21_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f395,f57]) ).

fof(f398,plain,
    ~ sQ21_spl,
    inference(contradiction_clause,[status(thm)],[f397]) ).

fof(f401,plain,
    ( ~ sQ20_spl
    | combK = comb_app(combK,comb_app(combK,combS)) ),
    inference(resolution,[status(thm)],[f309,f116]) ).

fof(f402,plain,
    ( ~ sQ20_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f401,f57]) ).

fof(f403,plain,
    ~ sQ20_spl,
    inference(contradiction_clause,[status(thm)],[f402]) ).

fof(f449,definition,
    ( sQ41_spl
  <=> member(comb_app(combS,p),comb) ),
    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).

fof(f450,plain,
    ( ~ sQ41_spl
    | member(comb_app(combS,p),comb) ),
    inference(component_clause,[status(thm)],[f449]) ).

fof(f451,plain,
    ( sQ41_spl
    | ~ member(comb_app(combS,p),comb) ),
    inference(component_clause,[status(thm)],[f449]) ).

fof(f492,plain,
    ! [X0,X1,X2] :
      ( comb_app(comb_app(X0,X2),comb_app(X1,X2)) = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2),comb_app(ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f286,f121]) ).

fof(f493,plain,
    ! [X0,X1,X2] :
      ( comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f286,f122]) ).

fof(f521,definition,
    ( sQ52_spl
  <=> r = r ),
    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).

fof(f523,plain,
    ( sQ52_spl
    | r != r ),
    inference(component_clause,[status(thm)],[f521]) ).

fof(f528,plain,
    ( sQ52_spl
    | $false ),
    inference(trivial_equality_resolution,[status(thm)],[f523]) ).

fof(f529,plain,
    sQ52_spl,
    inference(contradiction_clause,[status(thm)],[f528]) ).

fof(f540,plain,
    ( ~ sQ28_spl
    | comb_app(combS,combS) = comb_app(combK,comb_app(comb_app(combS,combS),combS)) ),
    inference(resolution,[status(thm)],[f335,f116]) ).

fof(f543,plain,
    ! [X0,X1,X2,X3] :
      ( X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,comb_app(X2,X3))),ap_parcontractE_sk1q(X0,X1,comb_app(X2,X3)))
      | ~ member(pair(X1,X3),parcontract)
      | ~ member(pair(X0,X2),parcontract)
      | ap_parcontractE_c4(X0,X1,comb_app(X2,X3))
      | ap_parcontractE_c2(X0,X1,comb_app(X2,X3))
      | ap_parcontractE_c1(X0,X1,comb_app(X2,X3)) ),
    inference(resolution,[status(thm)],[f290,f122]) ).

fof(f545,definition,
    ( sQ54_spl
  <=> member(pair(combK,combK),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).

fof(f547,plain,
    ( sQ54_spl
    | ~ member(pair(combK,combK),parcontract) ),
    inference(component_clause,[status(thm)],[f545]) ).

fof(f548,definition,
    ( sQ55_spl
  <=> member(pair(combS,combS),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).

fof(f550,plain,
    ( sQ55_spl
    | ~ member(pair(combS,combS),parcontract) ),
    inference(component_clause,[status(thm)],[f548]) ).

fof(f555,plain,
    ! [X0,X1] :
      ( X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,comb_app(X0,X1))),ap_parcontractE_sk1q(X0,X1,comb_app(X0,X1)))
      | ~ member(comb_app(X0,X1),comb)
      | ap_parcontractE_c4(X0,X1,comb_app(X0,X1))
      | ap_parcontractE_c2(X0,X1,comb_app(X0,X1))
      | ap_parcontractE_c1(X0,X1,comb_app(X0,X1)) ),
    inference(resolution,[status(thm)],[f291,f122]) ).

fof(f670,plain,
    ! [X0] :
      ( ~ sQ34_spl
      | ~ member(pair(p,X0),parcontract)
      | r != comb_app(comb_app(combS,X0),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f358,f128]) ).

fof(f671,plain,
    ( ~ sQ34_spl
    | ap_parcontractE_c4(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))
    | ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))
    | ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))
    | ap_parcontractE_c1(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f359,f107]) ).

fof(f672,definition,
    ( sQ72_spl
  <=> ap_parcontractE_c1(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).

fof(f673,plain,
    ( ~ sQ72_spl
    | ap_parcontractE_c1(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    inference(component_clause,[status(thm)],[f672]) ).

fof(f675,definition,
    ( sQ73_spl
  <=> ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).

fof(f676,plain,
    ( ~ sQ73_spl
    | ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    inference(component_clause,[status(thm)],[f675]) ).

fof(f678,definition,
    ( sQ74_spl
  <=> ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).

fof(f679,plain,
    ( ~ sQ74_spl
    | ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    inference(component_clause,[status(thm)],[f678]) ).

fof(f681,definition,
    ( sQ75_spl
  <=> ap_parcontractE_c4(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).

fof(f682,plain,
    ( ~ sQ75_spl
    | ap_parcontractE_c4(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    inference(component_clause,[status(thm)],[f681]) ).

fof(f684,plain,
    ( ~ sQ34_spl
    | sQ75_spl
    | sQ74_spl
    | sQ73_spl
    | sQ72_spl ),
    inference(split_clause,[status(thm)],[f671,f672,f675,f678,f681,f353]) ).

fof(f685,plain,
    ( ~ sQ75_spl
    | ap_parcontractE_sk2q(comb_app(combS,p),q,r) = comb_app(ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)),ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))) ),
    inference(resolution,[status(thm)],[f682,f125]) ).

fof(f686,plain,
    ( ~ sQ75_spl
    | member(pair(p,ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))),parcontract) ),
    inference(resolution,[status(thm)],[f682,f124]) ).

fof(f687,plain,
    ( ~ sQ75_spl
    | member(pair(combS,ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))),parcontract) ),
    inference(resolution,[status(thm)],[f682,f123]) ).

fof(f689,plain,
    ( ~ sQ74_spl
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))),ap_parcontractE_sk1q(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))) ),
    inference(resolution,[status(thm)],[f679,f122]) ).

fof(f691,plain,
    ( ~ sQ74_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f689,f58]) ).

fof(f692,plain,
    ~ sQ74_spl,
    inference(contradiction_clause,[status(thm)],[f691]) ).

fof(f695,plain,
    ( ~ sQ73_spl
    | combS = comb_app(combK,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f676,f116]) ).

fof(f699,plain,
    ( ~ sQ72_spl
    | member(p,comb) ),
    inference(resolution,[status(thm)],[f673,f227]) ).

fof(f700,plain,
    ( ~ sQ72_spl
    | ap_parcontractE_sk2q(comb_app(combS,p),q,r) = comb_app(combS,p) ),
    inference(resolution,[status(thm)],[f673,f110]) ).

fof(f707,plain,
    ( ~ sQ34_spl
    | ~ sQ72_spl
    | r = comb_app(comb_app(combS,p),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    inference(backward_demodulation,[status(thm)],[f700,f357]) ).

fof(f715,definition,
    ( sQ77_spl
  <=> ap_parcontractE_c2(combS,p,comb_app(combS,p)) ),
    introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).

fof(f716,plain,
    ( ~ sQ77_spl
    | ap_parcontractE_c2(combS,p,comb_app(combS,p)) ),
    inference(component_clause,[status(thm)],[f715]) ).

fof(f722,definition,
    ( sQ79_spl
  <=> member(pair(p,p),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).

fof(f724,plain,
    ( sQ79_spl
    | ~ member(pair(p,p),parcontract) ),
    inference(component_clause,[status(thm)],[f722]) ).

fof(f726,plain,
    ( sQ55_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f550,f145]) ).

fof(f727,plain,
    sQ55_spl,
    inference(contradiction_clause,[status(thm)],[f726]) ).

fof(f728,plain,
    ( sQ79_spl
    | ~ member(p,comb) ),
    inference(resolution,[status(thm)],[f724,f97]) ).

fof(f729,plain,
    ( sQ79_spl
    | ~ sQ36_spl ),
    inference(split_clause,[status(thm)],[f728,f378,f722]) ).

fof(f731,plain,
    ( ~ sQ72_spl
    | sQ36_spl ),
    inference(split_clause,[status(thm)],[f699,f378,f672]) ).

fof(f737,plain,
    ( ~ sQ77_spl
    | combS = comb_app(combK,comb_app(combS,p)) ),
    inference(resolution,[status(thm)],[f716,f116]) ).

fof(f738,plain,
    ( ~ sQ77_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f737,f58]) ).

fof(f739,plain,
    ~ sQ77_spl,
    inference(contradiction_clause,[status(thm)],[f738]) ).

fof(f743,plain,
    ! [X0,X1] :
      ( member(pair(X1,ap_contractE_sk3q(comb_app(combK,X0),X1,X0)),contract)
      | comb_app(combK,X0) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(combK,X0),X1,X0)),ap_contractE_sk1q(comb_app(combK,X0),X1,X0))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(combK,X0),X1,X0)
      | ap_contractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f360,f91]) ).

fof(f746,plain,
    ! [X0,X1] :
      ( member(pair(X1,ap_contractE_sk3q(comb_app(combK,X0),X1,X0)),contract)
      | X0 = comb_app(comb_app(ap_contractE_sk1p(comb_app(combK,X0),X1,X0),X1),comb_app(ap_contractE_sk1q(comb_app(combK,X0),X1,X0),X1))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(combK,X0),X1,X0)
      | ap_contractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f361,f91]) ).

fof(f749,plain,
    ! [X0,X1,X2] :
      ( member(pair(X2,ap_contractE_sk3q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),contract)
      | comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f363,f91]) ).

fof(f753,plain,
    ( ~ sQ34_spl
    | ~ member(p,comb)
    | r != comb_app(comb_app(combS,p),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f670,f97]) ).

fof(f754,definition,
    ( sQ80_spl
  <=> r = comb_app(comb_app(combS,p),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).

fof(f756,plain,
    ( sQ80_spl
    | r != comb_app(comb_app(combS,p),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    inference(component_clause,[status(thm)],[f754]) ).

fof(f757,plain,
    ( ~ sQ34_spl
    | ~ sQ36_spl
    | ~ sQ80_spl ),
    inference(split_clause,[status(thm)],[f753,f754,f378,f353]) ).

fof(f783,plain,
    ( ~ sQ32_spl
    | combS = combK ),
    inference(resolution,[status(thm)],[f384,f60]) ).

fof(f820,plain,
    ( ~ sQ32_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f783,f56]) ).

fof(f821,plain,
    ~ sQ32_spl,
    inference(contradiction_clause,[status(thm)],[f820]) ).

fof(f834,plain,
    ! [X0,X1,X2] :
      ( member(pair(X2,ap_contractE_sk3q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),contract)
      | comb_app(comb_app(X0,X2),comb_app(X1,X2)) = comb_app(comb_app(ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2),comb_app(ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f364,f91]) ).

fof(f838,plain,
    ! [X0,X1] :
      ( member(pair(X1,ap_parcontractE_sk2s(comb_app(combK,X0),X1,X0)),parcontract)
      | X0 = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(combK,X0),X1,X0),X1),comb_app(ap_parcontractE_sk1q(comb_app(combK,X0),X1,X0),X1))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f366,f124]) ).

fof(f841,plain,
    ! [X0,X1] :
      ( member(pair(X1,ap_parcontractE_sk2s(comb_app(combK,X0),X1,X0)),parcontract)
      | comb_app(combK,X0) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(combK,X0),X1,X0)),ap_parcontractE_sk1q(comb_app(combK,X0),X1,X0))
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(combK,X0),X1,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),X1,X0) ),
    inference(resolution,[status(thm)],[f367,f124]) ).

fof(f859,plain,
    ( ~ sQ24_spl
    | comb_app(combK,combS) = comb_app(combK,comb_app(comb_app(combK,combS),combS)) ),
    inference(resolution,[status(thm)],[f322,f116]) ).

fof(f869,plain,
    ! [X0,X1,X2] :
      ( member(pair(X2,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),parcontract)
      | comb_app(comb_app(X0,X2),comb_app(X1,X2)) = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2),comb_app(ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),X2))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f492,f124]) ).

fof(f872,plain,
    ! [X0,X1,X2] :
      ( member(pair(X2,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),parcontract)
      | comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))))
      | ~ member(X2,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))) ),
    inference(resolution,[status(thm)],[f493,f124]) ).

fof(f877,plain,
    ( ~ sQ28_spl
    | combS = comb_app(comb_app(combS,combS),combS) ),
    inference(resolution,[status(thm)],[f540,f62]) ).

fof(f922,plain,
    ( ~ sQ28_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f877,f58]) ).

fof(f923,plain,
    ~ sQ28_spl,
    inference(contradiction_clause,[status(thm)],[f922]) ).

fof(f929,plain,
    ( ~ sQ24_spl
    | combS = comb_app(comb_app(combK,combS),combS) ),
    inference(resolution,[status(thm)],[f859,f62]) ).

fof(f974,plain,
    ( ~ sQ24_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f929,f58]) ).

fof(f975,plain,
    ~ sQ24_spl,
    inference(contradiction_clause,[status(thm)],[f974]) ).

fof(f981,plain,
    ! [X0,X1,X2,X3] :
      ( comb_app(X2,X3) = comb_app(ap_parcontractE_sk2q(X0,X1,comb_app(X2,X3)),ap_parcontractE_sk2s(X0,X1,comb_app(X2,X3)))
      | X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,comb_app(X2,X3))),ap_parcontractE_sk1q(X0,X1,comb_app(X2,X3)))
      | ~ member(pair(X1,X3),parcontract)
      | ~ member(pair(X0,X2),parcontract)
      | ap_parcontractE_c2(X0,X1,comb_app(X2,X3))
      | ap_parcontractE_c1(X0,X1,comb_app(X2,X3)) ),
    inference(resolution,[status(thm)],[f543,f125]) ).

fof(f1001,definition,
    ( sQ82_spl
  <=> member(comb_app(comb_app(combS,p),q),comb) ),
    introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).

fof(f1002,plain,
    ( ~ sQ82_spl
    | member(comb_app(comb_app(combS,p),q),comb) ),
    inference(component_clause,[status(thm)],[f1001]) ).

fof(f1003,plain,
    ( sQ82_spl
    | ~ member(comb_app(comb_app(combS,p),q),comb) ),
    inference(component_clause,[status(thm)],[f1001]) ).

fof(f1009,plain,
    ( ~ sQ82_spl
    | member(q,comb) ),
    inference(resolution,[status(thm)],[f1002,f67]) ).

fof(f1010,plain,
    ( ~ sQ82_spl
    | sQ7_spl ),
    inference(split_clause,[status(thm)],[f1009,f209,f1001]) ).

fof(f1017,plain,
    ( ~ sQ34_spl
    | ~ sQ75_spl
    | r != comb_app(comb_app(combS,ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f686,f670]) ).

fof(f1018,plain,
    ( ~ sQ75_spl
    | ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)) = combS ),
    inference(resolution,[status(thm)],[f687,f106]) ).

fof(f1024,plain,
    ! [X0,X1] :
      ( member(pair(X1,ap_parcontractE_sk2s(X0,X1,comb_app(X0,X1))),parcontract)
      | X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,comb_app(X0,X1))),ap_parcontractE_sk1q(X0,X1,comb_app(X0,X1)))
      | ~ member(comb_app(X0,X1),comb)
      | ap_parcontractE_c2(X0,X1,comb_app(X0,X1))
      | ap_parcontractE_c1(X0,X1,comb_app(X0,X1)) ),
    inference(resolution,[status(thm)],[f555,f124]) ).

fof(f1025,plain,
    ! [X0,X1] :
      ( member(pair(X0,ap_parcontractE_sk2q(X0,X1,comb_app(X0,X1))),parcontract)
      | X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,comb_app(X0,X1))),ap_parcontractE_sk1q(X0,X1,comb_app(X0,X1)))
      | ~ member(comb_app(X0,X1),comb)
      | ap_parcontractE_c2(X0,X1,comb_app(X0,X1))
      | ap_parcontractE_c1(X0,X1,comb_app(X0,X1)) ),
    inference(resolution,[status(thm)],[f555,f123]) ).

fof(f1229,definition,
    ( sQ96_spl
  <=> ap_parcontractE_c2(combS,combS,ap_parcontractE_sk2q(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS))) ),
    introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).

fof(f1230,plain,
    ( ~ sQ96_spl
    | ap_parcontractE_c2(combS,combS,ap_parcontractE_sk2q(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS))) ),
    inference(component_clause,[status(thm)],[f1229]) ).

fof(f1232,definition,
    ( sQ97_spl
  <=> ap_parcontractE_c3(combS,combS,ap_parcontractE_sk2q(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS))) ),
    introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).

fof(f1233,plain,
    ( ~ sQ97_spl
    | ap_parcontractE_c3(combS,combS,ap_parcontractE_sk2q(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS))) ),
    inference(component_clause,[status(thm)],[f1232]) ).

fof(f1243,plain,
    ( ~ sQ97_spl
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,ap_parcontractE_sk2q(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS)))),ap_parcontractE_sk1q(combS,combS,ap_parcontractE_sk2q(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS)))) ),
    inference(resolution,[status(thm)],[f1233,f122]) ).

fof(f1245,plain,
    ( ~ sQ97_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1243,f58]) ).

fof(f1246,plain,
    ~ sQ97_spl,
    inference(contradiction_clause,[status(thm)],[f1245]) ).

fof(f1249,plain,
    ( ~ sQ96_spl
    | combS = comb_app(combK,ap_parcontractE_sk2q(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS))) ),
    inference(resolution,[status(thm)],[f1230,f116]) ).

fof(f1250,plain,
    ( ~ sQ96_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1249,f58]) ).

fof(f1251,plain,
    ~ sQ96_spl,
    inference(contradiction_clause,[status(thm)],[f1250]) ).

fof(f1274,plain,
    ( ~ sQ16_spl
    | combS = comb_app(combK,comb_app(combS,combS)) ),
    inference(resolution,[status(thm)],[f296,f116]) ).

fof(f1275,plain,
    ( ~ sQ16_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1274,f58]) ).

fof(f1276,plain,
    ~ sQ16_spl,
    inference(contradiction_clause,[status(thm)],[f1275]) ).

fof(f1419,definition,
    ( sQ123_spl
  <=> combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p)),comb_app(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p))))),ap_parcontractE_sk1q(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p)),comb_app(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p))))) ),
    introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).

fof(f1420,plain,
    ( ~ sQ123_spl
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p)),comb_app(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p))))),ap_parcontractE_sk1q(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p)),comb_app(combS,ap_parcontractE_sk2s(combS,p,comb_app(combS,p))))) ),
    inference(component_clause,[status(thm)],[f1419]) ).

fof(f1517,plain,
    ( ~ sQ123_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1420,f58]) ).

fof(f1518,plain,
    ~ sQ123_spl,
    inference(contradiction_clause,[status(thm)],[f1517]) ).

fof(f1523,plain,
    ( ~ sQ17_spl
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,comb_app(combS,combS))),ap_parcontractE_sk1q(combS,combS,comb_app(combS,combS))) ),
    inference(resolution,[status(thm)],[f299,f122]) ).

fof(f1525,plain,
    ( ~ sQ17_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1523,f58]) ).

fof(f1526,plain,
    ~ sQ17_spl,
    inference(contradiction_clause,[status(thm)],[f1525]) ).

fof(f1532,definition,
    ( sQ144_spl
  <=> combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,p,comb_app(combS,p))),ap_parcontractE_sk1q(combS,p,comb_app(combS,p))) ),
    introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).

fof(f1533,plain,
    ( ~ sQ144_spl
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,p,comb_app(combS,p))),ap_parcontractE_sk1q(combS,p,comb_app(combS,p))) ),
    inference(component_clause,[status(thm)],[f1532]) ).

fof(f1543,plain,
    ( ~ sQ144_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1533,f58]) ).

fof(f1544,plain,
    ~ sQ144_spl,
    inference(contradiction_clause,[status(thm)],[f1543]) ).

fof(f1545,plain,
    ( sQ41_spl
    | ~ member(p,comb)
    | ~ member(combS,comb) ),
    inference(resolution,[status(thm)],[f451,f70]) ).

fof(f1547,plain,
    ( sQ41_spl
    | ~ sQ36_spl
    | ~ sQ3_spl ),
    inference(split_clause,[status(thm)],[f1545,f139,f378,f449]) ).

fof(f1549,plain,
    ( ~ sQ41_spl
    | member(p,comb) ),
    inference(resolution,[status(thm)],[f450,f67]) ).

fof(f1550,plain,
    ( ~ sQ41_spl
    | sQ36_spl ),
    inference(split_clause,[status(thm)],[f1549,f378,f449]) ).

fof(f1555,plain,
    ! [X0] :
      ( comb_app(combK,X0) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(combK,X0),combK,X0)),ap_contractE_sk1q(comb_app(combK,X0),combK,X0))
      | ~ member(combK,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(combK,X0),combK,X0)
      | ap_contractE_c1(comb_app(combK,X0),combK,X0) ),
    inference(resolution,[status(thm)],[f743,f95]) ).

fof(f1556,plain,
    ! [X0] :
      ( comb_app(combK,X0) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(combK,X0),combS,X0)),ap_contractE_sk1q(comb_app(combK,X0),combS,X0))
      | ~ member(combS,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(combK,X0),combS,X0)
      | ap_contractE_c1(comb_app(combK,X0),combS,X0) ),
    inference(resolution,[status(thm)],[f743,f96]) ).

fof(f1557,definition,
    ! [X0] :
      ( sQ146_spl
    <=> ( comb_app(combK,X0) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(combK,X0),combK,X0)),ap_contractE_sk1q(comb_app(combK,X0),combK,X0))
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(combK,X0),combK,X0)
        | ap_contractE_c1(comb_app(combK,X0),combK,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).

fof(f1560,plain,
    ( ~ sQ1_spl
    | sQ146_spl ),
    inference(split_clause,[status(thm)],[f1555,f1557,f132]) ).

fof(f1561,definition,
    ! [X0] :
      ( sQ147_spl
    <=> ( comb_app(combK,X0) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(combK,X0),combS,X0)),ap_contractE_sk1q(comb_app(combK,X0),combS,X0))
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(combK,X0),combS,X0)
        | ap_contractE_c1(comb_app(combK,X0),combS,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).

fof(f1564,plain,
    ( ~ sQ3_spl
    | sQ147_spl ),
    inference(split_clause,[status(thm)],[f1556,f1561,f139]) ).

fof(f1662,definition,
    ( sQ159_spl
  <=> ap_parcontractE_c2(combK,combS,ap_parcontractE_sk2q(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS))) ),
    introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).

fof(f1663,plain,
    ( ~ sQ159_spl
    | ap_parcontractE_c2(combK,combS,ap_parcontractE_sk2q(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS))) ),
    inference(component_clause,[status(thm)],[f1662]) ).

fof(f1665,definition,
    ( sQ160_spl
  <=> ap_parcontractE_c3(combK,combS,ap_parcontractE_sk2q(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS))) ),
    introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).

fof(f1666,plain,
    ( ~ sQ160_spl
    | ap_parcontractE_c3(combK,combS,ap_parcontractE_sk2q(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS))) ),
    inference(component_clause,[status(thm)],[f1665]) ).

fof(f1679,plain,
    ( ~ sQ160_spl
    | combK = comb_app(comb_app(combS,ap_parcontractE_sk1p(combK,combS,ap_parcontractE_sk2q(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS)))),ap_parcontractE_sk1q(combK,combS,ap_parcontractE_sk2q(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS)))) ),
    inference(resolution,[status(thm)],[f1666,f122]) ).

fof(f1681,plain,
    ( ~ sQ160_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1679,f57]) ).

fof(f1682,plain,
    ~ sQ160_spl,
    inference(contradiction_clause,[status(thm)],[f1681]) ).

fof(f1685,plain,
    ( ~ sQ159_spl
    | combK = comb_app(combK,ap_parcontractE_sk2q(comb_app(combK,combS),combS,comb_app(comb_app(combK,combS),combS))) ),
    inference(resolution,[status(thm)],[f1663,f116]) ).

fof(f1686,plain,
    ( ~ sQ159_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1685,f57]) ).

fof(f1687,plain,
    ~ sQ159_spl,
    inference(contradiction_clause,[status(thm)],[f1686]) ).

fof(f1698,plain,
    ! [X0] :
      ( X0 = comb_app(comb_app(ap_contractE_sk1p(comb_app(combK,X0),combK,X0),combK),comb_app(ap_contractE_sk1q(comb_app(combK,X0),combK,X0),combK))
      | ~ member(combK,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(combK,X0),combK,X0)
      | ap_contractE_c1(comb_app(combK,X0),combK,X0) ),
    inference(resolution,[status(thm)],[f746,f95]) ).

fof(f1699,plain,
    ! [X0] :
      ( X0 = comb_app(comb_app(ap_contractE_sk1p(comb_app(combK,X0),combS,X0),combS),comb_app(ap_contractE_sk1q(comb_app(combK,X0),combS,X0),combS))
      | ~ member(combS,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(combK,X0),combS,X0)
      | ap_contractE_c1(comb_app(combK,X0),combS,X0) ),
    inference(resolution,[status(thm)],[f746,f96]) ).

fof(f1700,definition,
    ! [X0] :
      ( sQ162_spl
    <=> ( X0 = comb_app(comb_app(ap_contractE_sk1p(comb_app(combK,X0),combK,X0),combK),comb_app(ap_contractE_sk1q(comb_app(combK,X0),combK,X0),combK))
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(combK,X0),combK,X0)
        | ap_contractE_c1(comb_app(combK,X0),combK,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).

fof(f1703,plain,
    ( ~ sQ1_spl
    | sQ162_spl ),
    inference(split_clause,[status(thm)],[f1698,f1700,f132]) ).

fof(f1704,definition,
    ! [X0] :
      ( sQ163_spl
    <=> ( X0 = comb_app(comb_app(ap_contractE_sk1p(comb_app(combK,X0),combS,X0),combS),comb_app(ap_contractE_sk1q(comb_app(combK,X0),combS,X0),combS))
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(combK,X0),combS,X0)
        | ap_contractE_c1(comb_app(combK,X0),combS,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).

fof(f1707,plain,
    ( ~ sQ3_spl
    | sQ163_spl ),
    inference(split_clause,[status(thm)],[f1699,f1704,f139]) ).

fof(f1845,definition,
    ! [X0,X1,X2] :
      ( sQ179_spl
    <=> ( ap_parcontractE_sk2s(X0,combK,comb_app(X1,X2)) = combK
        | ~ member(pair(combK,X2),parcontract)
        | ~ member(pair(X0,X1),parcontract) ) ),
    introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).

fof(f1846,plain,
    ! [X0,X1,X2] :
      ( ~ sQ179_spl
      | ap_parcontractE_sk2s(X0,combK,comb_app(X1,X2)) = combK
      | ~ member(pair(combK,X2),parcontract)
      | ~ member(pair(X0,X1),parcontract) ),
    inference(component_clause,[status(thm)],[f1845]) ).

fof(f1867,plain,
    ! [X0,X1] :
      ( comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))),ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))))
      | ~ member(combK,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ),
    inference(resolution,[status(thm)],[f749,f95]) ).

fof(f1868,plain,
    ! [X0,X1] :
      ( comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))),ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))))
      | ~ member(combS,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ),
    inference(resolution,[status(thm)],[f749,f96]) ).

fof(f1871,definition,
    ! [X0,X1] :
      ( sQ182_spl
    <=> ( comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))),ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
        | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ) ),
    introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).

fof(f1874,plain,
    ( ~ sQ1_spl
    | sQ182_spl ),
    inference(split_clause,[status(thm)],[f1867,f1871,f132]) ).

fof(f1875,definition,
    ! [X0,X1] :
      ( sQ183_spl
    <=> ( comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))),ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
        | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ) ),
    introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).

fof(f1878,plain,
    ( ~ sQ3_spl
    | sQ183_spl ),
    inference(split_clause,[status(thm)],[f1868,f1875,f139]) ).

fof(f1899,plain,
    ( ~ sQ82_spl
    | member(comb_app(combS,p),comb) ),
    inference(resolution,[status(thm)],[f1002,f65]) ).

fof(f1978,definition,
    ( sQ190_spl
  <=> member(pair(comb_app(combS,combS),comb_app(combS,combS)),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).

fof(f1980,plain,
    ( sQ190_spl
    | ~ member(pair(comb_app(combS,combS),comb_app(combS,combS)),parcontract) ),
    inference(component_clause,[status(thm)],[f1978]) ).

fof(f1983,definition,
    ( sQ191_spl
  <=> member(pair(comb_app(combK,combS),comb_app(combK,combS)),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).

fof(f1985,plain,
    ( sQ191_spl
    | ~ member(pair(comb_app(combK,combS),comb_app(combK,combS)),parcontract) ),
    inference(component_clause,[status(thm)],[f1983]) ).

fof(f1993,definition,
    ( sQ193_spl
  <=> member(pair(comb_app(combS,p),comb_app(combS,p)),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).

fof(f1995,plain,
    ( sQ193_spl
    | ~ member(pair(comb_app(combS,p),comb_app(combS,p)),parcontract) ),
    inference(component_clause,[status(thm)],[f1993]) ).

fof(f2254,definition,
    ( sQ223_spl
  <=> ap_parcontractE_c2(comb_app(comb_app(combS,p),q),p,comb_app(comb_app(p,p),comb_app(q,p))) ),
    introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).

fof(f2255,plain,
    ( ~ sQ223_spl
    | ap_parcontractE_c2(comb_app(comb_app(combS,p),q),p,comb_app(comb_app(p,p),comb_app(q,p))) ),
    inference(component_clause,[status(thm)],[f2254]) ).

fof(f2400,plain,
    ! [X0,X1] :
      ( ~ sQ179_spl
      | ~ member(combK,comb)
      | ap_parcontractE_sk2s(X0,combK,comb_app(X1,combK)) = combK
      | ~ member(pair(X0,X1),parcontract) ),
    inference(resolution,[status(thm)],[f1846,f97]) ).

fof(f2405,definition,
    ! [X0,X1] :
      ( sQ251_spl
    <=> ( ap_parcontractE_sk2s(X0,combK,comb_app(X1,combK)) = combK
        | ~ member(pair(X0,X1),parcontract) ) ),
    introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).

fof(f2408,plain,
    ( ~ sQ179_spl
    | ~ sQ1_spl
    | sQ251_spl ),
    inference(split_clause,[status(thm)],[f2400,f2405,f132,f1845]) ).

fof(f2483,plain,
    ! [X0,X1] :
      ( comb_app(comb_app(X0,combK),comb_app(X1,combK)) = comb_app(comb_app(ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK),comb_app(ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK))
      | ~ member(combK,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ),
    inference(resolution,[status(thm)],[f834,f95]) ).

fof(f2484,plain,
    ! [X0,X1] :
      ( comb_app(comb_app(X0,combS),comb_app(X1,combS)) = comb_app(comb_app(ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS),comb_app(ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS))
      | ~ member(combS,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
      | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ),
    inference(resolution,[status(thm)],[f834,f96]) ).

fof(f2491,definition,
    ! [X0,X1] :
      ( sQ255_spl
    <=> ( comb_app(comb_app(X0,combK),comb_app(X1,combK)) = comb_app(comb_app(ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK),comb_app(ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
        | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ) ),
    introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).

fof(f2494,plain,
    ( ~ sQ1_spl
    | sQ255_spl ),
    inference(split_clause,[status(thm)],[f2483,f2491,f132]) ).

fof(f2495,definition,
    ! [X0,X1] :
      ( sQ256_spl
    <=> ( comb_app(comb_app(X0,combS),comb_app(X1,combS)) = comb_app(comb_app(ap_contractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS),comb_app(ap_contractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
        | ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ) ),
    introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).

fof(f2498,plain,
    ( ~ sQ3_spl
    | sQ256_spl ),
    inference(split_clause,[status(thm)],[f2484,f2495,f139]) ).

fof(f2544,plain,
    ( ~ sQ223_spl
    | comb_app(comb_app(combS,p),q) = comb_app(combK,comb_app(comb_app(p,p),comb_app(q,p))) ),
    inference(resolution,[status(thm)],[f2255,f116]) ).

fof(f2647,plain,
    ! [X0,X1] :
      ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) = combK
      | comb_app(comb_app(X0,combK),comb_app(X1,combK)) = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK),comb_app(ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK))
      | ~ member(combK,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ),
    inference(resolution,[status(thm)],[f869,f103]) ).

fof(f2648,plain,
    ! [X0,X1] :
      ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) = combS
      | comb_app(comb_app(X0,combS),comb_app(X1,combS)) = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS),comb_app(ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS))
      | ~ member(combS,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ),
    inference(resolution,[status(thm)],[f869,f106]) ).

fof(f2670,definition,
    ! [X0,X1] :
      ( sQ270_spl
    <=> ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) = combK
        | comb_app(comb_app(X0,combK),comb_app(X1,combK)) = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK),comb_app(ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))),combK))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
        | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ) ),
    introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).

fof(f2673,plain,
    ( ~ sQ1_spl
    | sQ270_spl ),
    inference(split_clause,[status(thm)],[f2647,f2670,f132]) ).

fof(f2674,definition,
    ! [X0,X1] :
      ( sQ271_spl
    <=> ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) = combS
        | comb_app(comb_app(X0,combS),comb_app(X1,combS)) = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS),comb_app(ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))),combS))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
        | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ) ),
    introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).

fof(f2677,plain,
    ( ~ sQ3_spl
    | sQ271_spl ),
    inference(split_clause,[status(thm)],[f2648,f2674,f139]) ).

fof(f2890,plain,
    ! [X0] :
      ( ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0) = combK
      | X0 = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(combK,X0),combK,X0),combK),comb_app(ap_parcontractE_sk1q(comb_app(combK,X0),combK,X0),combK))
      | ~ member(combK,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(combK,X0),combK,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),combK,X0) ),
    inference(resolution,[status(thm)],[f838,f103]) ).

fof(f2891,plain,
    ! [X0] :
      ( ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0) = combS
      | X0 = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(combK,X0),combS,X0),combS),comb_app(ap_parcontractE_sk1q(comb_app(combK,X0),combS,X0),combS))
      | ~ member(combS,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(combK,X0),combS,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),combS,X0) ),
    inference(resolution,[status(thm)],[f838,f106]) ).

fof(f2911,definition,
    ! [X0] :
      ( sQ285_spl
    <=> ( ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0) = combK
        | X0 = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(combK,X0),combK,X0),combK),comb_app(ap_parcontractE_sk1q(comb_app(combK,X0),combK,X0),combK))
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(combK,X0),combK,X0)
        | ap_parcontractE_c1(comb_app(combK,X0),combK,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).

fof(f2914,plain,
    ( ~ sQ1_spl
    | sQ285_spl ),
    inference(split_clause,[status(thm)],[f2890,f2911,f132]) ).

fof(f2915,definition,
    ! [X0] :
      ( sQ286_spl
    <=> ( ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0) = combS
        | X0 = comb_app(comb_app(ap_parcontractE_sk1p(comb_app(combK,X0),combS,X0),combS),comb_app(ap_parcontractE_sk1q(comb_app(combK,X0),combS,X0),combS))
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(combK,X0),combS,X0)
        | ap_parcontractE_c1(comb_app(combK,X0),combS,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition]) ).

fof(f2918,plain,
    ( ~ sQ3_spl
    | sQ286_spl ),
    inference(split_clause,[status(thm)],[f2891,f2915,f139]) ).

fof(f3306,plain,
    ! [X0] :
      ( ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0) = combK
      | comb_app(combK,X0) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(combK,X0),combK,X0)),ap_parcontractE_sk1q(comb_app(combK,X0),combK,X0))
      | ~ member(combK,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(combK,X0),combK,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),combK,X0) ),
    inference(resolution,[status(thm)],[f841,f103]) ).

fof(f3307,plain,
    ! [X0] :
      ( ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0) = combS
      | comb_app(combK,X0) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(combK,X0),combS,X0)),ap_parcontractE_sk1q(comb_app(combK,X0),combS,X0))
      | ~ member(combS,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(combK,X0),combS,X0)
      | ap_parcontractE_c1(comb_app(combK,X0),combS,X0) ),
    inference(resolution,[status(thm)],[f841,f106]) ).

fof(f3327,definition,
    ! [X0] :
      ( sQ301_spl
    <=> ( ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0) = combK
        | comb_app(combK,X0) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(combK,X0),combK,X0)),ap_parcontractE_sk1q(comb_app(combK,X0),combK,X0))
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(combK,X0),combK,X0)
        | ap_parcontractE_c1(comb_app(combK,X0),combK,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition]) ).

fof(f3330,plain,
    ( ~ sQ1_spl
    | sQ301_spl ),
    inference(split_clause,[status(thm)],[f3306,f3327,f132]) ).

fof(f3331,definition,
    ! [X0] :
      ( sQ302_spl
    <=> ( ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0) = combS
        | comb_app(combK,X0) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(combK,X0),combS,X0)),ap_parcontractE_sk1q(comb_app(combK,X0),combS,X0))
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(combK,X0),combS,X0)
        | ap_parcontractE_c1(comb_app(combK,X0),combS,X0) ) ),
    introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).

fof(f3334,plain,
    ( ~ sQ3_spl
    | sQ302_spl ),
    inference(split_clause,[status(thm)],[f3307,f3331,f139]) ).

fof(f3342,plain,
    ( ~ sQ223_spl
    | comb_app(combS,p) = combK ),
    inference(resolution,[status(thm)],[f2544,f60]) ).

fof(f3424,plain,
    ( ~ sQ223_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f3342,f57]) ).

fof(f3425,plain,
    ~ sQ223_spl,
    inference(contradiction_clause,[status(thm)],[f3424]) ).

fof(f3752,plain,
    ! [X0,X1] :
      ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) = combK
      | comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))),ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))))
      | ~ member(combK,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ),
    inference(resolution,[status(thm)],[f872,f103]) ).

fof(f3753,plain,
    ! [X0,X1] :
      ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) = combS
      | comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))),ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))))
      | ~ member(combS,comb)
      | ~ member(X1,comb)
      | ~ member(X0,comb)
      | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
      | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ),
    inference(resolution,[status(thm)],[f872,f106]) ).

fof(f3771,definition,
    ! [X0,X1] :
      ( sQ359_spl
    <=> ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) = combK
        | comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))),ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))
        | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))) ) ),
    introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).

fof(f3774,plain,
    ( ~ sQ1_spl
    | sQ359_spl ),
    inference(split_clause,[status(thm)],[f3752,f3771,f132]) ).

fof(f3775,definition,
    ! [X0,X1] :
      ( sQ360_spl
    <=> ( ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) = combS
        | comb_app(comb_app(combS,X0),X1) = comb_app(comb_app(combS,ap_parcontractE_sk1p(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))),ap_parcontractE_sk1q(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))))
        | ~ member(X1,comb)
        | ~ member(X0,comb)
        | ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))
        | ap_parcontractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))) ) ),
    introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).

fof(f3778,plain,
    ( ~ sQ3_spl
    | sQ360_spl ),
    inference(split_clause,[status(thm)],[f3753,f3775,f139]) ).

fof(f3821,plain,
    ! [X0] :
      ( sQ82_spl
      | ~ ap_parcontractE_c1(comb_app(combS,p),q,X0) ),
    inference(resolution,[status(thm)],[f1003,f109]) ).

fof(f3911,definition,
    ( sQ383_spl
  <=> comb_app(combS,combS) = comb_app(ap_parcontractE_sk2q(combS,combS,comb_app(combS,combS)),ap_parcontractE_sk2s(combS,combS,comb_app(combS,combS))) ),
    introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).

fof(f3922,definition,
    ( sQ386_spl
  <=> comb_app(combK,combS) = comb_app(ap_parcontractE_sk2q(combK,combS,comb_app(combK,combS)),ap_parcontractE_sk2s(combK,combS,comb_app(combK,combS))) ),
    introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).

fof(f3935,plain,
    ( sQ54_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f547,f149]) ).

fof(f3936,plain,
    sQ54_spl,
    inference(contradiction_clause,[status(thm)],[f3935]) ).

fof(f3939,plain,
    ( sQ190_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1980,f165]) ).

fof(f3940,plain,
    sQ190_spl,
    inference(contradiction_clause,[status(thm)],[f3939]) ).

fof(f3942,plain,
    ( sQ191_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f1985,f160]) ).

fof(f3943,plain,
    sQ191_spl,
    inference(contradiction_clause,[status(thm)],[f3942]) ).

fof(f4182,plain,
    ( sQ16_spl
    | comb_app(combS,combS) = comb_app(ap_parcontractE_sk2q(combS,combS,comb_app(combS,combS)),ap_parcontractE_sk2s(combS,combS,comb_app(combS,combS)))
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,comb_app(combS,combS))),ap_parcontractE_sk1q(combS,combS,comb_app(combS,combS)))
    | ~ member(pair(combS,combS),parcontract)
    | ~ member(pair(combS,combS),parcontract)
    | ap_parcontractE_c1(combS,combS,comb_app(combS,combS)) ),
    inference(resolution,[status(thm)],[f981,f297]) ).

fof(f4184,plain,
    ( sQ20_spl
    | comb_app(combK,combS) = comb_app(ap_parcontractE_sk2q(combK,combS,comb_app(combK,combS)),ap_parcontractE_sk2s(combK,combS,comb_app(combK,combS)))
    | combK = comb_app(comb_app(combS,ap_parcontractE_sk1p(combK,combS,comb_app(combK,combS))),ap_parcontractE_sk1q(combK,combS,comb_app(combK,combS)))
    | ~ member(pair(combS,combS),parcontract)
    | ~ member(pair(combK,combK),parcontract)
    | ap_parcontractE_c1(combK,combS,comb_app(combK,combS)) ),
    inference(resolution,[status(thm)],[f981,f310]) ).

fof(f4211,definition,
    ( sQ417_spl
  <=> combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,comb_app(combS,combS))),ap_parcontractE_sk1q(combS,combS,comb_app(combS,combS))) ),
    introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).

fof(f4212,plain,
    ( ~ sQ417_spl
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,comb_app(combS,combS))),ap_parcontractE_sk1q(combS,combS,comb_app(combS,combS))) ),
    inference(component_clause,[status(thm)],[f4211]) ).

fof(f4214,plain,
    ( sQ16_spl
    | sQ383_spl
    | sQ417_spl
    | ~ sQ55_spl
    | sQ15_spl ),
    inference(split_clause,[status(thm)],[f4182,f292,f548,f4211,f3911,f295]) ).

fof(f4216,definition,
    ( sQ418_spl
  <=> combK = comb_app(comb_app(combS,ap_parcontractE_sk1p(combK,combS,comb_app(combK,combS))),ap_parcontractE_sk1q(combK,combS,comb_app(combK,combS))) ),
    introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).

fof(f4217,plain,
    ( ~ sQ418_spl
    | combK = comb_app(comb_app(combS,ap_parcontractE_sk1p(combK,combS,comb_app(combK,combS))),ap_parcontractE_sk1q(combK,combS,comb_app(combK,combS))) ),
    inference(component_clause,[status(thm)],[f4216]) ).

fof(f4219,plain,
    ( sQ20_spl
    | sQ386_spl
    | sQ418_spl
    | ~ sQ55_spl
    | ~ sQ54_spl
    | sQ19_spl ),
    inference(split_clause,[status(thm)],[f4184,f305,f545,f548,f4216,f3922,f308]) ).

fof(f4227,plain,
    ( ~ sQ418_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f4217,f57]) ).

fof(f4228,plain,
    ~ sQ418_spl,
    inference(contradiction_clause,[status(thm)],[f4227]) ).

fof(f4229,plain,
    ( ~ sQ417_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f4212,f58]) ).

fof(f4230,plain,
    ~ sQ417_spl,
    inference(contradiction_clause,[status(thm)],[f4229]) ).

fof(f4449,plain,
    ( ~ sQ82_spl
    | sQ41_spl ),
    inference(split_clause,[status(thm)],[f1899,f449,f1001]) ).

fof(f4560,definition,
    ( sQ444_spl
  <=> ap_parcontractE_c2(comb_app(comb_app(combS,combS),combS),combS,comb_app(comb_app(comb_app(combS,combS),combS),combS)) ),
    introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition]) ).

fof(f4561,plain,
    ( ~ sQ444_spl
    | ap_parcontractE_c2(comb_app(comb_app(combS,combS),combS),combS,comb_app(comb_app(comb_app(combS,combS),combS),combS)) ),
    inference(component_clause,[status(thm)],[f4560]) ).

fof(f4573,definition,
    ( sQ448_spl
  <=> ap_parcontractE_c2(comb_app(comb_app(combK,combS),combS),combS,comb_app(comb_app(comb_app(combK,combS),combS),combS)) ),
    introduced(definition,[new_symbols(definition,[sQ448_spl])],[split_symbol_definition]) ).

fof(f4574,plain,
    ( ~ sQ448_spl
    | ap_parcontractE_c2(comb_app(comb_app(combK,combS),combS),combS,comb_app(comb_app(comb_app(combK,combS),combS),combS)) ),
    inference(component_clause,[status(thm)],[f4573]) ).

fof(f4591,definition,
    ( sQ453_spl
  <=> member(pair(combS,ap_parcontractE_sk2s(combS,combS,comb_app(combS,combS))),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ453_spl])],[split_symbol_definition]) ).

fof(f4595,definition,
    ( sQ454_spl
  <=> member(pair(combS,ap_parcontractE_sk2s(combK,combS,comb_app(combK,combS))),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition]) ).

fof(f4757,definition,
    ( sQ472_spl
  <=> member(pair(combS,ap_parcontractE_sk2q(combS,combS,comb_app(combS,combS))),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition]) ).

fof(f4761,definition,
    ( sQ473_spl
  <=> member(pair(combK,ap_parcontractE_sk2q(combK,combS,comb_app(combK,combS))),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ473_spl])],[split_symbol_definition]) ).

fof(f4948,plain,
    ( member(pair(combS,ap_parcontractE_sk2s(combS,combS,comb_app(combS,combS))),parcontract)
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,comb_app(combS,combS))),ap_parcontractE_sk1q(combS,combS,comb_app(combS,combS)))
    | ap_parcontractE_c2(combS,combS,comb_app(combS,combS))
    | ap_parcontractE_c1(combS,combS,comb_app(combS,combS)) ),
    inference(resolution,[status(thm)],[f1024,f155]) ).

fof(f4949,plain,
    ( ~ sQ5_spl
    | member(pair(combS,ap_parcontractE_sk2s(combK,combS,comb_app(combK,combS))),parcontract)
    | combK = comb_app(comb_app(combS,ap_parcontractE_sk1p(combK,combS,comb_app(combK,combS))),ap_parcontractE_sk1q(combK,combS,comb_app(combK,combS)))
    | ap_parcontractE_c2(combK,combS,comb_app(combK,combS))
    | ap_parcontractE_c1(combK,combS,comb_app(combK,combS)) ),
    inference(resolution,[status(thm)],[f1024,f185]) ).

fof(f4970,plain,
    ( sQ453_spl
    | sQ417_spl
    | sQ16_spl
    | sQ15_spl ),
    inference(split_clause,[status(thm)],[f4948,f292,f295,f4211,f4591]) ).

fof(f4971,plain,
    ( ~ sQ5_spl
    | sQ454_spl
    | sQ418_spl
    | sQ20_spl
    | sQ19_spl ),
    inference(split_clause,[status(thm)],[f4949,f305,f308,f4216,f4595,f184]) ).

fof(f4978,plain,
    ( member(pair(combS,ap_parcontractE_sk2q(combS,combS,comb_app(combS,combS))),parcontract)
    | combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,comb_app(combS,combS))),ap_parcontractE_sk1q(combS,combS,comb_app(combS,combS)))
    | ap_parcontractE_c2(combS,combS,comb_app(combS,combS))
    | ap_parcontractE_c1(combS,combS,comb_app(combS,combS)) ),
    inference(resolution,[status(thm)],[f1025,f155]) ).

fof(f4979,plain,
    ( ~ sQ5_spl
    | member(pair(combK,ap_parcontractE_sk2q(combK,combS,comb_app(combK,combS))),parcontract)
    | combK = comb_app(comb_app(combS,ap_parcontractE_sk1p(combK,combS,comb_app(combK,combS))),ap_parcontractE_sk1q(combK,combS,comb_app(combK,combS)))
    | ap_parcontractE_c2(combK,combS,comb_app(combK,combS))
    | ap_parcontractE_c1(combK,combS,comb_app(combK,combS)) ),
    inference(resolution,[status(thm)],[f1025,f185]) ).

fof(f4994,plain,
    ( sQ472_spl
    | sQ417_spl
    | sQ16_spl
    | sQ15_spl ),
    inference(split_clause,[status(thm)],[f4978,f292,f295,f4211,f4757]) ).

fof(f4995,plain,
    ( ~ sQ5_spl
    | sQ473_spl
    | sQ418_spl
    | sQ20_spl
    | sQ19_spl ),
    inference(split_clause,[status(thm)],[f4979,f305,f308,f4216,f4761,f184]) ).

fof(f5058,definition,
    ( sQ505_spl
  <=> member(comb_app(p,p),comb) ),
    introduced(definition,[new_symbols(definition,[sQ505_spl])],[split_symbol_definition]) ).

fof(f5060,plain,
    ( sQ505_spl
    | ~ member(comb_app(p,p),comb) ),
    inference(component_clause,[status(thm)],[f5058]) ).

fof(f5111,plain,
    ( sQ505_spl
    | ~ member(p,comb)
    | ~ member(p,comb) ),
    inference(resolution,[status(thm)],[f5060,f70]) ).

fof(f5113,plain,
    ( sQ505_spl
    | ~ sQ36_spl ),
    inference(split_clause,[status(thm)],[f5111,f378,f5058]) ).

fof(f5231,plain,
    ( sQ193_spl
    | ~ member(pair(p,p),parcontract)
    | ~ member(pair(combS,combS),parcontract) ),
    inference(resolution,[status(thm)],[f1995,f100]) ).

fof(f5233,plain,
    ( sQ193_spl
    | ~ sQ79_spl
    | ~ sQ55_spl ),
    inference(split_clause,[status(thm)],[f5231,f548,f722,f1993]) ).

fof(f5766,plain,
    ( ~ sQ448_spl
    | comb_app(comb_app(combK,combS),combS) = comb_app(combK,comb_app(comb_app(comb_app(combK,combS),combS),combS)) ),
    inference(resolution,[status(thm)],[f4574,f116]) ).

fof(f5774,plain,
    ( ~ sQ444_spl
    | comb_app(comb_app(combS,combS),combS) = comb_app(combK,comb_app(comb_app(comb_app(combS,combS),combS),combS)) ),
    inference(resolution,[status(thm)],[f4561,f116]) ).

fof(f6384,plain,
    ( ~ sQ448_spl
    | combS = comb_app(comb_app(comb_app(combK,combS),combS),combS) ),
    inference(resolution,[status(thm)],[f5766,f62]) ).

fof(f6484,plain,
    ( ~ sQ448_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f6384,f58]) ).

fof(f6485,plain,
    ~ sQ448_spl,
    inference(contradiction_clause,[status(thm)],[f6484]) ).

fof(f6486,plain,
    ( ~ sQ444_spl
    | combS = comb_app(comb_app(comb_app(combS,combS),combS),combS) ),
    inference(resolution,[status(thm)],[f5774,f62]) ).

fof(f6586,plain,
    ( ~ sQ444_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f6486,f58]) ).

fof(f6587,plain,
    ~ sQ444_spl,
    inference(contradiction_clause,[status(thm)],[f6586]) ).

fof(f6592,definition,
    ( sQ698_spl
  <=> member(comb_app(comb_app(comb_app(combK,combS),combS),combS),comb) ),
    introduced(definition,[new_symbols(definition,[sQ698_spl])],[split_symbol_definition]) ).

fof(f6594,plain,
    ( sQ698_spl
    | ~ member(comb_app(comb_app(comb_app(combK,combS),combS),combS),comb) ),
    inference(component_clause,[status(thm)],[f6592]) ).

fof(f6600,definition,
    ( sQ700_spl
  <=> member(pair(comb_app(comb_app(combK,combS),combS),comb_app(comb_app(combK,combS),combS)),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ700_spl])],[split_symbol_definition]) ).

fof(f6602,plain,
    ( sQ700_spl
    | ~ member(pair(comb_app(comb_app(combK,combS),combS),comb_app(comb_app(combK,combS),combS)),parcontract) ),
    inference(component_clause,[status(thm)],[f6600]) ).

fof(f6605,plain,
    ( sQ700_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f6602,f170]) ).

fof(f6606,plain,
    sQ700_spl,
    inference(contradiction_clause,[status(thm)],[f6605]) ).

fof(f6607,plain,
    ( sQ698_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f6594,f168]) ).

fof(f6608,plain,
    sQ698_spl,
    inference(contradiction_clause,[status(thm)],[f6607]) ).

fof(f6613,definition,
    ( sQ701_spl
  <=> member(comb_app(comb_app(comb_app(combS,combS),combS),combS),comb) ),
    introduced(definition,[new_symbols(definition,[sQ701_spl])],[split_symbol_definition]) ).

fof(f6615,plain,
    ( sQ701_spl
    | ~ member(comb_app(comb_app(comb_app(combS,combS),combS),combS),comb) ),
    inference(component_clause,[status(thm)],[f6613]) ).

fof(f6621,definition,
    ( sQ703_spl
  <=> member(pair(comb_app(comb_app(combS,combS),combS),comb_app(comb_app(combS,combS),combS)),parcontract) ),
    introduced(definition,[new_symbols(definition,[sQ703_spl])],[split_symbol_definition]) ).

fof(f6623,plain,
    ( sQ703_spl
    | ~ member(pair(comb_app(comb_app(combS,combS),combS),comb_app(comb_app(combS,combS),combS)),parcontract) ),
    inference(component_clause,[status(thm)],[f6621]) ).

fof(f6626,plain,
    ( sQ703_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f6623,f175]) ).

fof(f6627,plain,
    sQ703_spl,
    inference(contradiction_clause,[status(thm)],[f6626]) ).

fof(f6628,plain,
    ( sQ701_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f6615,f173]) ).

fof(f6629,plain,
    sQ701_spl,
    inference(contradiction_clause,[status(thm)],[f6628]) ).

fof(f7133,plain,
    ( ~ sQ34_spl
    | ~ sQ75_spl
    | r != comb_app(ap_parcontractE_sk2q(comb_app(combS,p),q,r),ap_parcontractE_sk2s(comb_app(combS,p),q,r)) ),
    inference(backward_demodulation,[status(thm)],[f7134,f1017]) ).

fof(f7134,plain,
    ( ~ sQ75_spl
    | ap_parcontractE_sk2q(comb_app(combS,p),q,r) = comb_app(combS,ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))) ),
    inference(forward_demodulation,[status(thm)],[f1018,f685]) ).

fof(f7231,plain,
    ( ~ sQ34_spl
    | ~ sQ75_spl
    | r != r ),
    inference(forward_demodulation,[status(thm)],[f357,f7133]) ).

fof(f7232,plain,
    ( ~ sQ34_spl
    | ~ sQ75_spl
    | $false ),
    inference(trivial_equality_resolution,[status(thm)],[f7231]) ).

fof(f7233,plain,
    ( ~ sQ34_spl
    | ~ sQ75_spl ),
    inference(contradiction_clause,[status(thm)],[f7232]) ).

fof(f8027,plain,
    ( ~ sQ33_spl
    | combS = comb_app(combS,ap_parcontractE_sk1p(comb_app(combS,p),q,r)) ),
    inference(resolution,[status(thm)],[f370,f60]) ).

fof(f8125,plain,
    ( ~ sQ33_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f8027,f58]) ).

fof(f8126,plain,
    ~ sQ33_spl,
    inference(contradiction_clause,[status(thm)],[f8125]) ).

fof(f8128,plain,
    ( ~ sQ31_spl
    | sQ82_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f345,f3821]) ).

fof(f8129,plain,
    ( ~ sQ31_spl
    | sQ82_spl ),
    inference(contradiction_clause,[status(thm)],[f8128]) ).

fof(f8130,plain,
    ( ~ sQ34_spl
    | ~ sQ72_spl
    | sQ80_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f707,f756]) ).

fof(f8131,plain,
    ( ~ sQ34_spl
    | ~ sQ72_spl
    | sQ80_spl ),
    inference(contradiction_clause,[status(thm)],[f8130]) ).

fof(f8133,plain,
    ( ~ sQ73_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f695,f58]) ).

fof(f8134,plain,
    ~ sQ73_spl,
    inference(contradiction_clause,[status(thm)],[f8133]) ).

fof(f8135,plain,
    $false,
    inference(sat_refutation,[status(thm)],[f135,f142,f147,f151,f187,f202,f208,f215,f221,f242,f255,f261,f270,f274,f304,f317,f356,f381,f390,f398,f403,f529,f684,f692,f727,f729,f731,f739,f757,f821,f923,f975,f1010,f1246,f1251,f1276,f1518,f1526,f1544,f1547,f1550,f1560,f1564,f1682,f1687,f1703,f1707,f1874,f1878,f2408,f2494,f2498,f2673,f2677,f2914,f2918,f3330,f3334,f3425,f3774,f3778,f3936,f3940,f3943,f4214,f4219,f4228,f4230,f4449,f4970,f4971,f4994,f4995,f5113,f5233,f6485,f6587,f6606,f6608,f6627,f6629,f7233,f8126,f8129,f8131,f8134]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : COL094-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04  % Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37  % Computer : n016.cluster.edu
% 0.09/0.37  % Model    : x86_64 x86_64
% 0.09/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37  % Memory   : 8046.5625MB
% 0.09/0.37  % OS       : Linux 6.8.0-71-generic
% 0.09/0.37  % CPULimit : 300
% 0.09/0.37  % WCLimit  : 300
% 0.09/0.37  % DateTime : Mon Sep 21 14:14:39 UTC 2026
% 0.09/0.37  % CPUTime  : 
% 0.09/0.39  % Drodi V4.1.1
% 35.42/5.30  % Refutation found
% 35.42/5.30  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 35.42/5.30  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.51/5.87  % Elapsed time: 5.477423 seconds
% 5.51/5.87  % CPU time: 39.224670 seconds
% 5.51/5.87  % Total memory used: 392.746 MB
% 5.51/5.87  % Net memory used: 362.639 MB
%------------------------------------------------------------------------------