Drodi-SAT---4.1.1.UNS-Ass.s

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

% Computer : n011.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:09:07 PM UTC 2026

% Result   : Unsatisfiable 104.76s 13.66s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : COL094-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35  % Computer : n011.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Mon Sep 21 14:09:56 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 0.08/0.37  % Drodi V4.1.1
% 104.76/13.66  % Refutation found
% 104.76/13.66  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 104.76/13.66  % SZS output start CNFRefutation for theBenchmark
% 104.76/13.66  fof(f1,axiom,(
% 104.76/13.66    combK != combS ),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f3,axiom,(
% 104.76/13.66    (![P,Q]: (combS != comb_app(P,Q) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f4,axiom,(
% 104.76/13.66    (![P1,Q1,P2,Q2]: (( comb_app(P1,Q1) != comb_app(P2,Q2)| P1 = P2 ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f5,axiom,(
% 104.76/13.66    (![P1,Q1,P2,Q2]: (( comb_app(P1,Q1) != comb_app(P2,Q2)| Q1 = Q2 ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f7,axiom,(
% 104.76/13.66    (![P,Q]: (( ~ member(comb_app(P,Q),comb)| member(P,comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f8,axiom,(
% 104.76/13.66    (![P,Q]: (( ~ member(comb_app(P,Q),comb)| member(Q,comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f9,axiom,(
% 104.76/13.66    member(combK,comb) ),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f10,axiom,(
% 104.76/13.66    member(combS,comb) ),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f11,axiom,(
% 104.76/13.66    (![P,Q]: (( ~ member(P,comb)| ~ member(Q,comb)| member(comb_app(P,Q),comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f13,axiom,(
% 104.76/13.66    (![P,Q]: (( ~ member(P,comb)| ~ member(Q,comb)| member(pair(comb_app(comb_app(combK,P),Q),P),contract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f14,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ member(P,comb)| ~ member(Q,comb)| ~ member(R,comb)| member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),contract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f15,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ member(pair(comb_app(P,Q),R),contract)| ap_contractE_c1(P,Q,R)| ap_contractE_c2(P,Q,R)| ap_contractE_c3(P,Q,R)| ap_contractE_c4(P,Q,R) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f27,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_contractE_c4(P,Q,R)| member(pair(Q,ap_contractE_sk3q(P,Q,R)),contract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f30,axiom,(
% 104.76/13.66    (![R]: (~ member(pair(combK,R),contract) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f31,axiom,(
% 104.76/13.66    (![R]: (~ member(pair(combS,R),contract) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f32,axiom,(
% 104.76/13.66    (![P]: (( ~ member(P,comb)| member(pair(P,P),parcontract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f33,axiom,(
% 104.76/13.66    (![P,Q]: (( ~ member(P,comb)| ~ member(Q,comb)| member(pair(comb_app(comb_app(combK,P),Q),P),parcontract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f34,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ member(P,comb)| ~ member(Q,comb)| ~ member(R,comb)| member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),parcontract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f35,axiom,(
% 104.76/13.66    (![P,Q,R,S]: (( ~ member(pair(P,Q),parcontract)| ~ member(pair(R,S),parcontract)| member(pair(comb_app(P,R),comb_app(Q,S)),parcontract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f36,axiom,(
% 104.76/13.66    (![R]: (( ~ member(pair(combK,R),parcontract)| member(combK,comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f37,axiom,(
% 104.76/13.66    (![R]: (( ~ member(pair(combK,R),parcontract)| R = combK ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f38,axiom,(
% 104.76/13.66    (![R]: (( ~ member(pair(combS,R),parcontract)| member(combS,comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f39,axiom,(
% 104.76/13.66    (![R]: (( ~ member(pair(combS,R),parcontract)| R = combS ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f40,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ member(pair(comb_app(P,Q),R),parcontract)| ap_parcontractE_c1(P,Q,R)| ap_parcontractE_c2(P,Q,R)| ap_parcontractE_c3(P,Q,R)| ap_parcontractE_c4(P,Q,R) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f41,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c1(P,Q,R)| member(comb_app(P,Q),comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f42,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c1(P,Q,R)| R = comb_app(P,Q) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f44,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c2(P,Q,R)| member(Q,comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f45,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c2(P,Q,R)| P = comb_app(combK,R) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f48,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c3(P,Q,R)| member(Q,comb) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f50,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c3(P,Q,R)| P = comb_app(comb_app(combS,ap_parcontractE_sk1p(P,Q,R)),ap_parcontractE_sk1q(P,Q,R)) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f51,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c4(P,Q,R)| member(pair(P,ap_parcontractE_sk2q(P,Q,R)),parcontract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f52,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c4(P,Q,R)| member(pair(Q,ap_parcontractE_sk2s(P,Q,R)),parcontract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f53,axiom,(
% 104.76/13.66    (![P,Q,R]: (( ~ ap_parcontractE_c4(P,Q,R)| R = comb_app(ap_parcontractE_sk2q(P,Q,R),ap_parcontractE_sk2s(P,Q,R)) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f54,hypothesis,(
% 104.76/13.66    member(pair(comb_app(comb_app(combS,p),q),r),parcontract) ),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f55,negated_conjecture,(
% 104.76/13.66    (![PP,QP]: (( r != comb_app(comb_app(combS,PP),QP)| ~ member(pair(p,PP),parcontract)| ~ member(pair(q,QP),parcontract) ) ))),
% 104.76/13.66    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.76/13.66  fof(f56,plain,(
% 104.76/13.66    ~combK=combS),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f1])).
% 104.76/13.66  fof(f58,plain,(
% 104.76/13.66    ![X0,X1]: (~combS=comb_app(X0,X1))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f3])).
% 104.76/13.66  fof(f59,plain,(
% 104.76/13.66    ![P1,P2]: ((![Q1,Q2]: ~comb_app(P1,Q1)=comb_app(P2,Q2))|P1=P2)),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f4])).
% 104.76/13.66  fof(f60,plain,(
% 104.76/13.66    ![X0,X1,X2,X3]: (~comb_app(X0,X1)=comb_app(X2,X3)|X0=X2)),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f59])).
% 104.76/13.66  fof(f61,plain,(
% 104.76/13.66    ![Q1,Q2]: ((![P1,P2]: ~comb_app(P1,Q1)=comb_app(P2,Q2))|Q1=Q2)),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f5])).
% 104.76/13.66  fof(f62,plain,(
% 104.76/13.66    ![X0,X1,X2,X3]: (~comb_app(X0,X1)=comb_app(X2,X3)|X1=X3)),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f61])).
% 104.76/13.66  fof(f64,plain,(
% 104.76/13.66    ![P]: ((![Q]: ~member(comb_app(P,Q),comb))|member(P,comb))),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f7])).
% 104.76/13.66  fof(f65,plain,(
% 104.76/13.66    ![X0,X1]: (~member(comb_app(X0,X1),comb)|member(X0,comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f64])).
% 104.76/13.66  fof(f66,plain,(
% 104.76/13.66    ![Q]: ((![P]: ~member(comb_app(P,Q),comb))|member(Q,comb))),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f8])).
% 104.76/13.66  fof(f67,plain,(
% 104.76/13.66    ![X0,X1]: (~member(comb_app(X0,X1),comb)|member(X1,comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f66])).
% 104.76/13.66  fof(f68,plain,(
% 104.76/13.66    member(combK,comb)),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f9])).
% 104.76/13.66  fof(f69,plain,(
% 104.76/13.66    member(combS,comb)),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f10])).
% 104.76/13.66  fof(f70,plain,(
% 104.76/13.66    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|member(comb_app(X0,X1),comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f11])).
% 104.76/13.66  fof(f72,plain,(
% 104.76/13.66    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|member(pair(comb_app(comb_app(combK,X0),X1),X0),contract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f13])).
% 104.76/13.66  fof(f73,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|member(pair(comb_app(comb_app(comb_app(combS,X0),X1),X2),comb_app(comb_app(X0,X2),comb_app(X1,X2))),contract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f14])).
% 104.76/13.66  fof(f74,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~member(pair(comb_app(X0,X1),X2),contract)|ap_contractE_c1(X0,X1,X2)|ap_contractE_c2(X0,X1,X2)|ap_contractE_c3(X0,X1,X2)|ap_contractE_c4(X0,X1,X2))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f15])).
% 104.76/13.66  fof(f91,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_contractE_c4(X0,X1,X2)|member(pair(X1,ap_contractE_sk3q(X0,X1,X2)),contract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f27])).
% 104.76/13.66  fof(f95,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combK,X0),contract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f30])).
% 104.76/13.66  fof(f96,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combS,X0),contract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f31])).
% 104.76/13.66  fof(f97,plain,(
% 104.76/13.66    ![X0]: (~member(X0,comb)|member(pair(X0,X0),parcontract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f32])).
% 104.76/13.66  fof(f98,plain,(
% 104.76/13.66    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|member(pair(comb_app(comb_app(combK,X0),X1),X0),parcontract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f33])).
% 104.76/13.66  fof(f99,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|member(pair(comb_app(comb_app(comb_app(combS,X0),X1),X2),comb_app(comb_app(X0,X2),comb_app(X1,X2))),parcontract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f34])).
% 104.76/13.66  fof(f100,plain,(
% 104.76/13.66    ![X0,X1,X2,X3]: (~member(pair(X0,X1),parcontract)|~member(pair(X2,X3),parcontract)|member(pair(comb_app(X0,X2),comb_app(X1,X3)),parcontract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f35])).
% 104.76/13.66  fof(f101,plain,(
% 104.76/13.66    (![R]: ~member(pair(combK,R),parcontract))|member(combK,comb)),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f36])).
% 104.76/13.66  fof(f102,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combK,X0),parcontract)|member(combK,comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f101])).
% 104.76/13.66  fof(f103,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combK,X0),parcontract)|X0=combK)),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f37])).
% 104.76/13.66  fof(f104,plain,(
% 104.76/13.66    (![R]: ~member(pair(combS,R),parcontract))|member(combS,comb)),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f38])).
% 104.76/13.66  fof(f105,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combS,X0),parcontract)|member(combS,comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f104])).
% 104.76/13.66  fof(f106,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combS,X0),parcontract)|X0=combS)),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f39])).
% 104.76/13.66  fof(f107,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~member(pair(comb_app(X0,X1),X2),parcontract)|ap_parcontractE_c1(X0,X1,X2)|ap_parcontractE_c2(X0,X1,X2)|ap_parcontractE_c3(X0,X1,X2)|ap_parcontractE_c4(X0,X1,X2))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f40])).
% 104.76/13.66  fof(f108,plain,(
% 104.76/13.66    ![P,Q]: ((![R]: ~ap_parcontractE_c1(P,Q,R))|member(comb_app(P,Q),comb))),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f41])).
% 104.76/13.66  fof(f109,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c1(X0,X1,X2)|member(comb_app(X0,X1),comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f108])).
% 104.76/13.66  fof(f110,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c1(X0,X1,X2)|X2=comb_app(X0,X1))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f42])).
% 104.76/13.66  fof(f113,plain,(
% 104.76/13.66    ![Q]: ((![P,R]: ~ap_parcontractE_c2(P,Q,R))|member(Q,comb))),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f44])).
% 104.76/13.66  fof(f114,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c2(X0,X1,X2)|member(X1,comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f113])).
% 104.76/13.66  fof(f115,plain,(
% 104.76/13.66    ![P,R]: ((![Q]: ~ap_parcontractE_c2(P,Q,R))|P=comb_app(combK,R))),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f45])).
% 104.76/13.66  fof(f116,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c2(X0,X1,X2)|X0=comb_app(combK,X2))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f115])).
% 104.76/13.66  fof(f119,plain,(
% 104.76/13.66    ![Q]: ((![P,R]: ~ap_parcontractE_c3(P,Q,R))|member(Q,comb))),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f48])).
% 104.76/13.66  fof(f120,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c3(X0,X1,X2)|member(X1,comb))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f119])).
% 104.76/13.66  fof(f122,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c3(X0,X1,X2)|X0=comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,X2)),ap_parcontractE_sk1q(X0,X1,X2)))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f50])).
% 104.76/13.66  fof(f123,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c4(X0,X1,X2)|member(pair(X0,ap_parcontractE_sk2q(X0,X1,X2)),parcontract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f51])).
% 104.76/13.66  fof(f124,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c4(X0,X1,X2)|member(pair(X1,ap_parcontractE_sk2s(X0,X1,X2)),parcontract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f52])).
% 104.76/13.66  fof(f125,plain,(
% 104.76/13.66    ![X0,X1,X2]: (~ap_parcontractE_c4(X0,X1,X2)|X2=comb_app(ap_parcontractE_sk2q(X0,X1,X2),ap_parcontractE_sk2s(X0,X1,X2)))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f53])).
% 104.76/13.66  fof(f126,plain,(
% 104.76/13.66    member(pair(comb_app(comb_app(combS,p),q),r),parcontract)),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f54])).
% 104.76/13.66  fof(f127,plain,(
% 104.76/13.66    ![QP]: ((![PP]: (~r=comb_app(comb_app(combS,PP),QP)|~member(pair(p,PP),parcontract)))|~member(pair(q,QP),parcontract))),
% 104.76/13.66    inference(miniscoping,[status(thm)],[f55])).
% 104.76/13.66  fof(f128,plain,(
% 104.76/13.66    ![X0,X1]: (~r=comb_app(comb_app(combS,X0),X1)|~member(pair(p,X0),parcontract)|~member(pair(q,X1),parcontract))),
% 104.76/13.66    inference(cnf_transformation,[status(thm)],[f127])).
% 104.76/13.66  fof(f129,definition,(
% 104.76/13.66    ![X0]: (sQ0_spl <=> (~member(pair(combK,X0),parcontract)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f130,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combK,X0),parcontract)|~sQ0_spl)),
% 104.76/13.66    inference(component_clause,[status(thm)],[f129])).
% 104.76/13.66  fof(f132,definition,(
% 104.76/13.66    sQ1_spl <=> (member(combK,comb))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f135,plain,(
% 104.76/13.66    sQ0_spl|sQ1_spl),
% 104.76/13.66    inference(split_clause,[status(thm)],[f102,f129,f132])).
% 104.76/13.66  fof(f136,definition,(
% 104.76/13.66    ![X0]: (sQ2_spl <=> (~member(pair(combS,X0),parcontract)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f137,plain,(
% 104.76/13.66    ![X0]: (~member(pair(combS,X0),parcontract)|~sQ2_spl)),
% 104.76/13.66    inference(component_clause,[status(thm)],[f136])).
% 104.76/13.66  fof(f139,definition,(
% 104.76/13.66    sQ3_spl <=> (member(combS,comb))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f142,plain,(
% 104.76/13.66    sQ2_spl|sQ3_spl),
% 104.76/13.66    inference(split_clause,[status(thm)],[f105,f136,f139])).
% 104.76/13.66  fof(f145,plain,(
% 104.76/13.66    member(pair(combS,combS),parcontract)),
% 104.76/13.66    inference(resolution,[status(thm)],[f97,f69])).
% 104.76/13.66  fof(f146,plain,(
% 104.76/13.66    $false|~sQ2_spl),
% 104.76/13.66    inference(forward_subsumption_resolution,[status(thm)],[f145,f137])).
% 104.76/13.66  fof(f147,plain,(
% 104.76/13.66    ~sQ2_spl),
% 104.76/13.66    inference(contradiction_clause,[status(thm)],[f146])).
% 104.76/13.66  fof(f148,plain,(
% 104.76/13.66    member(pair(combK,combK),parcontract)),
% 104.76/13.66    inference(resolution,[status(thm)],[f68,f97])).
% 104.76/13.66  fof(f149,plain,(
% 104.76/13.66    $false|~sQ0_spl),
% 104.76/13.66    inference(forward_subsumption_resolution,[status(thm)],[f148,f130])).
% 104.76/13.66  fof(f150,plain,(
% 104.76/13.66    ~sQ0_spl),
% 104.76/13.66    inference(contradiction_clause,[status(thm)],[f149])).
% 104.76/13.66  fof(f152,plain,(
% 104.76/13.66    ![X0]: (~member(X0,comb)|member(comb_app(X0,combS),comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f70,f69])).
% 104.76/13.66  fof(f154,plain,(
% 104.76/13.66    member(comb_app(combK,combS),comb)),
% 104.76/13.66    inference(resolution,[status(thm)],[f152,f68])).
% 104.76/13.66  fof(f155,plain,(
% 104.76/13.66    member(comb_app(combS,combS),comb)),
% 104.76/13.66    inference(resolution,[status(thm)],[f152,f69])).
% 104.76/13.66  fof(f158,plain,(
% 104.76/13.66    member(comb_app(comb_app(combK,combS),combS),comb)),
% 104.76/13.66    inference(resolution,[status(thm)],[f154,f152])).
% 104.76/13.66  fof(f159,plain,(
% 104.76/13.66    ![X0]: (~member(X0,comb)|member(comb_app(X0,comb_app(combK,combS)),comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f154,f70])).
% 104.76/13.66  fof(f163,plain,(
% 104.76/13.66    member(comb_app(comb_app(combS,combS),combS),comb)),
% 104.76/13.66    inference(resolution,[status(thm)],[f155,f152])).
% 104.76/13.66  fof(f164,plain,(
% 104.76/13.66    ![X0]: (~member(X0,comb)|member(comb_app(X0,comb_app(combS,combS)),comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f155,f70])).
% 104.76/13.66  fof(f165,plain,(
% 104.76/13.66    member(pair(comb_app(combS,combS),comb_app(combS,combS)),parcontract)),
% 104.76/13.66    inference(resolution,[status(thm)],[f155,f97])).
% 104.76/13.66  fof(f169,plain,(
% 104.76/13.66    ![X0]: (~member(X0,comb)|member(comb_app(X0,comb_app(comb_app(combK,combS),combS)),comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f158,f70])).
% 104.76/13.66  fof(f171,plain,(
% 104.76/13.66    ![X0]: (~member(X0,comb)|member(comb_app(combK,combS),comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f159,f67])).
% 104.76/13.66  fof(f174,plain,(
% 104.76/13.66    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|member(comb_app(X1,comb_app(X0,comb_app(combK,combS))),comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f159,f70])).
% 104.76/13.66  fof(f176,definition,(
% 104.76/13.66    ![X0]: (sQ4_spl <=> (~member(X0,comb)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f177,plain,(
% 104.76/13.66    ![X0]: (~member(X0,comb)|~sQ4_spl)),
% 104.76/13.66    inference(component_clause,[status(thm)],[f176])).
% 104.76/13.66  fof(f179,definition,(
% 104.76/13.66    sQ5_spl <=> (member(comb_app(combK,combS),comb))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f182,plain,(
% 104.76/13.66    sQ4_spl|sQ5_spl),
% 104.76/13.66    inference(split_clause,[status(thm)],[f171,f176,f179])).
% 104.76/13.66  fof(f183,plain,(
% 104.76/13.66    $false|~sQ4_spl),
% 104.76/13.66    inference(backward_subsumption_resolution,[status(thm)],[f158,f177])).
% 104.76/13.66  fof(f203,plain,(
% 104.76/13.66    ~sQ4_spl),
% 104.76/13.66    inference(contradiction_clause,[status(thm)],[f183])).
% 104.76/13.66  fof(f211,plain,(
% 104.76/13.66    ![X0,X1,X2]: (ap_parcontractE_c1(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_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|ap_parcontractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|~member(X0,comb)|~member(X1,comb)|~member(X2,comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f107,f99])).
% 104.76/13.66  fof(f212,plain,(
% 104.76/13.66    ap_parcontractE_c1(comb_app(combS,p),q,r)|ap_parcontractE_c2(comb_app(combS,p),q,r)|ap_parcontractE_c3(comb_app(combS,p),q,r)|ap_parcontractE_c4(comb_app(combS,p),q,r)),
% 104.76/13.66    inference(resolution,[status(thm)],[f107,f126])).
% 104.76/13.66  fof(f214,plain,(
% 104.76/13.66    ![X0,X1,X2,X3]: (ap_parcontractE_c1(X0,X1,comb_app(X2,X3))|ap_parcontractE_c2(X0,X1,comb_app(X2,X3))|ap_parcontractE_c3(X0,X1,comb_app(X2,X3))|ap_parcontractE_c4(X0,X1,comb_app(X2,X3))|~member(pair(X0,X2),parcontract)|~member(pair(X1,X3),parcontract))),
% 104.76/13.66    inference(resolution,[status(thm)],[f107,f100])).
% 104.76/13.66  fof(f231,definition,(
% 104.76/13.66    sQ11_spl <=> (ap_parcontractE_c2(combS,combS,comb_app(combS,combS)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f232,plain,(
% 104.76/13.66    ap_parcontractE_c2(combS,combS,comb_app(combS,combS))|~sQ11_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f231])).
% 104.76/13.66  fof(f234,definition,(
% 104.76/13.66    sQ12_spl <=> (ap_parcontractE_c3(combS,combS,comb_app(combS,combS)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f235,plain,(
% 104.76/13.66    ap_parcontractE_c3(combS,combS,comb_app(combS,combS))|~sQ12_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f234])).
% 104.76/13.66  fof(f241,definition,(
% 104.76/13.66    sQ14_spl <=> (ap_parcontractE_c1(comb_app(combS,p),q,r))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f242,plain,(
% 104.76/13.66    ap_parcontractE_c1(comb_app(combS,p),q,r)|~sQ14_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f241])).
% 104.76/13.66  fof(f244,definition,(
% 104.76/13.66    sQ15_spl <=> (ap_parcontractE_c2(comb_app(combS,p),q,r))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f245,plain,(
% 104.76/13.66    ap_parcontractE_c2(comb_app(combS,p),q,r)|~sQ15_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f244])).
% 104.76/13.66  fof(f247,definition,(
% 104.76/13.66    sQ16_spl <=> (ap_parcontractE_c3(comb_app(combS,p),q,r))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f248,plain,(
% 104.76/13.66    ap_parcontractE_c3(comb_app(combS,p),q,r)|~sQ16_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f247])).
% 104.76/13.66  fof(f250,definition,(
% 104.76/13.66    sQ17_spl <=> (ap_parcontractE_c4(comb_app(combS,p),q,r))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f251,plain,(
% 104.76/13.66    ap_parcontractE_c4(comb_app(combS,p),q,r)|~sQ17_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f250])).
% 104.76/13.66  fof(f253,plain,(
% 104.76/13.66    sQ14_spl|sQ15_spl|sQ16_spl|sQ17_spl),
% 104.76/13.66    inference(split_clause,[status(thm)],[f212,f241,f244,f247,f250])).
% 104.76/13.66  fof(f254,plain,(
% 104.76/13.66    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))|~sQ16_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f248,f122])).
% 104.76/13.66  fof(f256,plain,(
% 104.76/13.66    member(pair(comb_app(combS,p),ap_parcontractE_sk2q(comb_app(combS,p),q,r)),parcontract)|~sQ17_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f123,f251])).
% 104.76/13.66  fof(f257,plain,(
% 104.76/13.66    member(pair(q,ap_parcontractE_sk2s(comb_app(combS,p),q,r)),parcontract)|~sQ17_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f124,f251])).
% 104.76/13.66  fof(f258,plain,(
% 104.76/13.66    comb_app(combS,p)=comb_app(combK,r)|~sQ15_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f245,f116])).
% 104.76/13.66  fof(f259,plain,(
% 104.76/13.66    ![X0,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_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|ap_parcontractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X0,X2),comb_app(X1,X2))=comb_app(comb_app(comb_app(combS,X0),X1),X2))),
% 104.76/13.66    inference(resolution,[status(thm)],[f211,f110])).
% 104.76/13.66  fof(f260,plain,(
% 104.76/13.66    ![X0,X1,X2,X3]: (ap_parcontractE_c2(X0,X1,comb_app(X2,X3))|ap_parcontractE_c3(X0,X1,comb_app(X2,X3))|ap_parcontractE_c4(X0,X1,comb_app(X2,X3))|~member(pair(X0,X2),parcontract)|~member(pair(X1,X3),parcontract)|comb_app(X2,X3)=comb_app(X0,X1))),
% 104.76/13.66    inference(resolution,[status(thm)],[f214,f110])).
% 104.76/13.66  fof(f261,plain,(
% 104.76/13.66    r=comb_app(comb_app(combS,p),q)|~sQ14_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f242,f110])).
% 104.76/13.66  fof(f264,plain,(
% 104.76/13.66    combS=comb_app(combS,ap_parcontractE_sk1p(comb_app(combS,p),q,r))|~sQ16_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f254,f60])).
% 104.76/13.66  fof(f286,plain,(
% 104.76/13.66    $false|~sQ16_spl),
% 104.76/13.66    inference(forward_subsumption_resolution,[status(thm)],[f264,f58])).
% 104.76/13.66  fof(f287,plain,(
% 104.76/13.66    ~sQ16_spl),
% 104.76/13.66    inference(contradiction_clause,[status(thm)],[f286])).
% 104.76/13.66  fof(f288,plain,(
% 104.76/13.66    ap_parcontractE_c1(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_c3(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))|ap_parcontractE_c4(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))|~sQ17_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f256,f107])).
% 104.76/13.66  fof(f289,definition,(
% 104.76/13.66    sQ18_spl <=> (ap_parcontractE_c1(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f290,plain,(
% 104.76/13.66    ap_parcontractE_c1(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))|~sQ18_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f289])).
% 104.76/13.66  fof(f292,definition,(
% 104.76/13.66    sQ19_spl <=> (ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f293,plain,(
% 104.76/13.66    ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))|~sQ19_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f292])).
% 104.76/13.66  fof(f295,definition,(
% 104.76/13.66    sQ20_spl <=> (ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f296,plain,(
% 104.76/13.66    ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))|~sQ20_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f295])).
% 104.76/13.66  fof(f298,definition,(
% 104.76/13.66    sQ21_spl <=> (ap_parcontractE_c4(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f299,plain,(
% 104.76/13.66    ap_parcontractE_c4(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))|~sQ21_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f298])).
% 104.76/13.66  fof(f301,plain,(
% 104.76/13.66    sQ18_spl|sQ19_spl|sQ20_spl|sQ21_spl|~sQ17_spl),
% 104.76/13.66    inference(split_clause,[status(thm)],[f288,f289,f292,f295,f298,f250])).
% 104.76/13.66  fof(f303,plain,(
% 104.76/13.66    combS=combK|~sQ15_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f258,f60])).
% 104.76/13.66  fof(f332,plain,(
% 104.76/13.66    $false|~sQ15_spl),
% 104.76/13.66    inference(forward_subsumption_resolution,[status(thm)],[f303,f56])).
% 104.76/13.66  fof(f333,plain,(
% 104.76/13.66    ~sQ15_spl),
% 104.76/13.66    inference(contradiction_clause,[status(thm)],[f332])).
% 104.76/13.66  fof(f337,plain,(
% 104.76/13.66    combS=comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,combS,comb_app(combS,combS))),ap_parcontractE_sk1q(combS,combS,comb_app(combS,combS)))|~sQ12_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f235,f122])).
% 104.76/13.66  fof(f338,plain,(
% 104.76/13.66    $false|~sQ12_spl),
% 104.76/13.66    inference(forward_subsumption_resolution,[status(thm)],[f337,f58])).
% 104.76/13.66  fof(f339,plain,(
% 104.76/13.66    ~sQ12_spl),
% 104.76/13.66    inference(contradiction_clause,[status(thm)],[f338])).
% 104.76/13.66  fof(f342,plain,(
% 104.76/13.66    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|member(pair(comb_app(X0,X1),comb_app(X0,X1)),parcontract))),
% 104.76/13.66    inference(resolution,[status(thm)],[f70,f97])).
% 104.76/13.66  fof(f347,plain,(
% 104.76/13.66    ![X0,X1]: (member(X0,comb)|~member(X1,comb)|~member(X0,comb))),
% 104.76/13.66    inference(resolution,[status(thm)],[f67,f70])).
% 104.76/13.66  fof(f350,definition,(
% 104.76/13.66    ![X0]: (sQ22_spl <=> (member(X0,comb)|~member(X0,comb)))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f353,plain,(
% 104.76/13.66    sQ22_spl|sQ4_spl),
% 104.76/13.66    inference(split_clause,[status(thm)],[f347,f350,f176])).
% 104.76/13.66  fof(f361,plain,(
% 104.76/13.66    combS=comb_app(combK,comb_app(combS,combS))|~sQ11_spl),
% 104.76/13.66    inference(resolution,[status(thm)],[f232,f116])).
% 104.76/13.66  fof(f362,plain,(
% 104.76/13.66    $false|~sQ11_spl),
% 104.76/13.66    inference(forward_subsumption_resolution,[status(thm)],[f361,f58])).
% 104.76/13.66  fof(f363,plain,(
% 104.76/13.66    ~sQ11_spl),
% 104.76/13.66    inference(contradiction_clause,[status(thm)],[f362])).
% 104.76/13.66  fof(f366,plain,(
% 104.76/13.66    ![X0,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_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X0,X2),comb_app(X1,X2))=comb_app(comb_app(comb_app(combS,X0),X1),X2)|comb_app(comb_app(X0,X2),comb_app(X1,X2))=comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))))),
% 104.76/13.66    inference(resolution,[status(thm)],[f259,f125])).
% 104.76/13.66  fof(f367,plain,(
% 104.76/13.66    ![X0,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_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X0,X2),comb_app(X1,X2))=comb_app(comb_app(comb_app(combS,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))),
% 104.76/13.66    inference(resolution,[status(thm)],[f259,f124])).
% 104.76/13.66  fof(f368,plain,(
% 104.76/13.66    ![X0,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_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X0,X2),comb_app(X1,X2))=comb_app(comb_app(comb_app(combS,X0),X1),X2)|member(pair(comb_app(comb_app(combS,X0),X1),ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))),parcontract))),
% 104.76/13.66    inference(resolution,[status(thm)],[f259,f123])).
% 104.76/13.66  fof(f370,plain,(
% 104.76/13.66    ![X0,X1,X2,X3]: (ap_parcontractE_c2(X0,X1,comb_app(X2,X3))|ap_parcontractE_c3(X0,X1,comb_app(X2,X3))|~member(pair(X0,X2),parcontract)|~member(pair(X1,X3),parcontract)|comb_app(X2,X3)=comb_app(X0,X1)|member(pair(X1,ap_parcontractE_sk2s(X0,X1,comb_app(X2,X3))),parcontract))),
% 104.76/13.66    inference(resolution,[status(thm)],[f260,f124])).
% 104.76/13.66  fof(f371,plain,(
% 104.76/13.66    ![X0,X1,X2,X3]: (ap_parcontractE_c2(X0,X1,comb_app(X2,X3))|ap_parcontractE_c3(X0,X1,comb_app(X2,X3))|~member(pair(X0,X2),parcontract)|~member(pair(X1,X3),parcontract)|comb_app(X2,X3)=comb_app(X0,X1)|member(pair(X0,ap_parcontractE_sk2q(X0,X1,comb_app(X2,X3))),parcontract))),
% 104.76/13.66    inference(resolution,[status(thm)],[f260,f123])).
% 104.76/13.66  fof(f380,plain,(
% 104.76/13.66    ~member(r,comb)|member(comb_app(combS,p),comb)|~sQ14_spl),
% 104.76/13.66    inference(paramodulation,[status(thm)],[f261,f65])).
% 104.76/13.66  fof(f381,plain,(
% 104.76/13.66    ~member(r,comb)|member(q,comb)|~sQ14_spl),
% 104.76/13.66    inference(paramodulation,[status(thm)],[f261,f67])).
% 104.76/13.66  fof(f401,definition,(
% 104.76/13.66    sQ24_spl <=> (member(p,comb))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f403,plain,(
% 104.76/13.66    ~member(p,comb)|sQ24_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f401])).
% 104.76/13.66  fof(f404,definition,(
% 104.76/13.66    sQ25_spl <=> (member(q,comb))),
% 104.76/13.66    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 104.76/13.66  fof(f405,plain,(
% 104.76/13.66    member(q,comb)|~sQ25_spl),
% 104.76/13.66    inference(component_clause,[status(thm)],[f404])).
% 104.76/13.67  fof(f422,definition,(
% 104.76/13.67    sQ29_spl <=> (member(comb_app(combS,p),comb))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f423,plain,(
% 104.76/13.67    member(comb_app(combS,p),comb)|~sQ29_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f422])).
% 104.76/13.67  fof(f424,plain,(
% 104.76/13.67    ~member(comb_app(combS,p),comb)|sQ29_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f422])).
% 104.76/13.67  fof(f438,definition,(
% 104.76/13.67    sQ33_spl <=> (member(r,comb))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f441,plain,(
% 104.76/13.67    ~sQ33_spl|sQ29_spl|~sQ14_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f380,f438,f422,f241])).
% 104.76/13.67  fof(f442,plain,(
% 104.76/13.67    ~sQ33_spl|sQ25_spl|~sQ14_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f381,f438,f404,f241])).
% 104.76/13.67  fof(f483,plain,(
% 104.76/13.67    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c1(comb_app(combK,X0),X1,X0)|ap_parcontractE_c2(comb_app(combK,X0),X1,X0)|ap_parcontractE_c3(comb_app(combK,X0),X1,X0)|ap_parcontractE_c4(comb_app(combK,X0),X1,X0))),
% 104.76/13.67    inference(resolution,[status(thm)],[f98,f107])).
% 104.76/13.67  fof(f484,plain,(
% 104.76/13.67    ![X0,X1,X2]: (~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|ap_contractE_c1(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_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|ap_contractE_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2))))),
% 104.76/13.67    inference(resolution,[status(thm)],[f73,f74])).
% 104.76/13.67  fof(f500,plain,(
% 104.76/13.67    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|ap_contractE_c1(comb_app(combK,X0),X1,X0)|ap_contractE_c2(comb_app(combK,X0),X1,X0)|ap_contractE_c3(comb_app(combK,X0),X1,X0)|ap_contractE_c4(comb_app(combK,X0),X1,X0))),
% 104.76/13.67    inference(resolution,[status(thm)],[f72,f74])).
% 104.76/13.67  fof(f515,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|member(comb_app(combS,combS),comb))),
% 104.76/13.67    inference(resolution,[status(thm)],[f164,f67])).
% 104.76/13.67  fof(f517,definition,(
% 104.76/13.67    sQ44_spl <=> (member(comb_app(combS,combS),comb))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f520,plain,(
% 104.76/13.67    sQ4_spl|sQ44_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f515,f176,f517])).
% 104.76/13.67  fof(f523,definition,(
% 104.76/13.67    sQ45_spl <=> (r=r)),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f525,plain,(
% 104.76/13.67    ~r=r|sQ45_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f523])).
% 104.76/13.67  fof(f530,plain,(
% 104.76/13.67    $false|sQ45_spl),
% 104.76/13.67    inference(trivial_equality_resolution,[status(thm)],[f525])).
% 104.76/13.67  fof(f531,plain,(
% 104.76/13.67    sQ45_spl),
% 104.76/13.67    inference(contradiction_clause,[status(thm)],[f530])).
% 104.76/13.67  fof(f545,plain,(
% 104.76/13.67    ap_parcontractE_sk2q(comb_app(combS,p),q,r)=comb_app(combS,p)|~sQ18_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f290,f110])).
% 104.76/13.67  fof(f546,plain,(
% 104.76/13.67    ap_parcontractE_c1(combS,p,comb_app(combS,p))|~sQ18_spl),
% 104.76/13.67    inference(backward_demodulation,[status(thm)],[f545,f290])).
% 104.76/13.67  fof(f560,plain,(
% 104.76/13.67    ![X0,X1,X2]: (~ap_parcontractE_c1(X0,X1,X2)|member(X0,comb))),
% 104.76/13.67    inference(resolution,[status(thm)],[f109,f65])).
% 104.76/13.67  fof(f561,plain,(
% 104.76/13.67    ![X0,X1,X2]: (~ap_parcontractE_c1(X0,X1,X2)|member(X1,comb))),
% 104.76/13.67    inference(resolution,[status(thm)],[f109,f67])).
% 104.76/13.67  fof(f563,plain,(
% 104.76/13.67    ![X0]: (~ap_parcontractE_c1(comb_app(combS,p),q,X0)|member(r,comb)|~sQ14_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f261,f109])).
% 104.76/13.67  fof(f564,definition,(
% 104.76/13.67    ![X0]: (sQ48_spl <=> (~ap_parcontractE_c1(comb_app(combS,p),q,X0)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f565,plain,(
% 104.76/13.67    ![X0]: (~ap_parcontractE_c1(comb_app(combS,p),q,X0)|~sQ48_spl)),
% 104.76/13.67    inference(component_clause,[status(thm)],[f564])).
% 104.76/13.67  fof(f567,plain,(
% 104.76/13.67    sQ48_spl|sQ33_spl|~sQ14_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f563,f564,f438,f241])).
% 104.76/13.67  fof(f568,plain,(
% 104.76/13.67    $false|~sQ48_spl|~sQ14_spl),
% 104.76/13.67    inference(backward_subsumption_resolution,[status(thm)],[f242,f565])).
% 104.76/13.67  fof(f570,plain,(
% 104.76/13.67    ~sQ48_spl|~sQ14_spl),
% 104.76/13.67    inference(contradiction_clause,[status(thm)],[f568])).
% 104.76/13.67  fof(f580,plain,(
% 104.76/13.67    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)))|~sQ21_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f299,f125])).
% 104.76/13.67  fof(f581,plain,(
% 104.76/13.67    member(pair(p,ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))),parcontract)|~sQ21_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f299,f124])).
% 104.76/13.67  fof(f582,plain,(
% 104.76/13.67    member(pair(combS,ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))),parcontract)|~sQ21_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f299,f123])).
% 104.76/13.67  fof(f585,plain,(
% 104.76/13.67    combS=comb_app(combK,ap_parcontractE_sk2q(comb_app(combS,p),q,r))|~sQ19_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f293,f116])).
% 104.76/13.67  fof(f620,plain,(
% 104.76/13.67    ![X0,X1,X2]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|~member(X0,comb)|~member(X1,comb)|~member(q,comb)|comb_app(comb_app(X0,q),comb_app(X1,q))=comb_app(comb_app(comb_app(combS,X0),X1),q)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q))))|~member(pair(p,X2),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f367,f128])).
% 104.76/13.67  fof(f622,plain,(
% 104.76/13.67    ![X0,X1]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|~member(X0,comb)|~member(X1,comb)|~member(combS,comb)|comb_app(comb_app(X0,combS),comb_app(X1,combS))=comb_app(comb_app(comb_app(combS,X0),X1),combS)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))=combS)),
% 104.76/13.67    inference(resolution,[status(thm)],[f367,f106])).
% 104.76/13.67  fof(f623,plain,(
% 104.76/13.67    ![X0,X1]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|~member(X0,comb)|~member(X1,comb)|~member(combK,comb)|comb_app(comb_app(X0,combK),comb_app(X1,combK))=comb_app(comb_app(comb_app(combS,X0),X1),combK)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))=combK)),
% 104.76/13.67    inference(resolution,[status(thm)],[f367,f103])).
% 104.76/13.67  fof(f627,definition,(
% 104.76/13.67    ![X0,X1,X2]: (sQ52_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|~member(X0,comb)|~member(X1,comb)|comb_app(comb_app(X0,q),comb_app(X1,q))=comb_app(comb_app(comb_app(combS,X0),X1),q)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q))))|~member(pair(p,X2),parcontract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f628,plain,(
% 104.76/13.67    ![X0,X1,X2]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|~member(X0,comb)|~member(X1,comb)|comb_app(comb_app(X0,q),comb_app(X1,q))=comb_app(comb_app(comb_app(combS,X0),X1),q)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q))))|~member(pair(p,X2),parcontract)|~sQ52_spl)),
% 104.76/13.67    inference(component_clause,[status(thm)],[f627])).
% 104.76/13.67  fof(f630,plain,(
% 104.76/13.67    sQ52_spl|~sQ25_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f620,f627,f404])).
% 104.76/13.67  fof(f631,definition,(
% 104.76/13.67    ![X0,X1]: (sQ53_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|~member(X0,comb)|~member(X1,comb)|comb_app(comb_app(X0,combS),comb_app(X1,combS))=comb_app(comb_app(comb_app(combS,X0),X1),combS)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))=combS))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f634,plain,(
% 104.76/13.67    sQ53_spl|~sQ3_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f622,f631,f139])).
% 104.76/13.67  fof(f635,definition,(
% 104.76/13.67    ![X0,X1]: (sQ54_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|~member(X0,comb)|~member(X1,comb)|comb_app(comb_app(X0,combK),comb_app(X1,combK))=comb_app(comb_app(comb_app(combS,X0),X1),combK)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))=combK))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f638,plain,(
% 104.76/13.67    sQ54_spl|~sQ1_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f623,f635,f132])).
% 104.76/13.67  fof(f715,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|~member(X0,comb)|~member(X1,comb)|comb_app(comb_app(X0,q),comb_app(X1,q))=comb_app(comb_app(comb_app(combS,X0),X1),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q))))|ap_parcontractE_c2(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|~member(X2,comb)|~member(X3,comb)|~member(p,comb)|comb_app(comb_app(X2,p),comb_app(X3,p))=comb_app(comb_app(comb_app(combS,X2),X3),p)|~sQ52_spl)),
% 104.76/13.67    inference(resolution,[status(thm)],[f628,f367])).
% 104.76/13.67  fof(f716,definition,(
% 104.76/13.67    ![X0,X1,X2,X3]: (sQ62_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q)))|~member(X0,comb)|~member(X1,comb)|comb_app(comb_app(X0,q),comb_app(X1,q))=comb_app(comb_app(comb_app(combS,X0),X1),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),q,comb_app(comb_app(X0,q),comb_app(X1,q))))|ap_parcontractE_c2(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|~member(X2,comb)|~member(X3,comb)|comb_app(comb_app(X2,p),comb_app(X3,p))=comb_app(comb_app(comb_app(combS,X2),X3),p)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f719,plain,(
% 104.76/13.67    sQ62_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f715,f716,f401,f627])).
% 104.76/13.67  fof(f855,definition,(
% 104.76/13.67    sQ86_spl <=> (comb_app(comb_app(combS,p),comb_app(combS,p))=comb_app(comb_app(comb_app(combS,combS),combS),p))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f856,plain,(
% 104.76/13.67    comb_app(comb_app(combS,p),comb_app(combS,p))=comb_app(comb_app(comb_app(combS,combS),combS),p)|~sQ86_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f855])).
% 104.76/13.67  fof(f973,definition,(
% 104.76/13.67    sQ99_spl <=> (ap_parcontractE_c2(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f974,plain,(
% 104.76/13.67    ap_parcontractE_c2(comb_app(combS,combS),combS,comb_app(comb_app(combS,combS),combS))|~sQ99_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f973])).
% 104.76/13.67  fof(f984,plain,(
% 104.76/13.67    ![X0,X1,X2,X3,X4]: (ap_parcontractE_c2(X0,p,comb_app(X1,X2))|ap_parcontractE_c3(X0,p,comb_app(X1,X2))|~member(pair(X0,X1),parcontract)|~member(pair(p,X2),parcontract)|comb_app(X1,X2)=comb_app(X0,p)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|~member(X3,comb)|~member(X4,comb)|comb_app(comb_app(X3,q),comb_app(X4,q))=comb_app(comb_app(comb_app(combS,X3),X4),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(X0,p,comb_app(X1,X2))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q))))|~sQ52_spl)),
% 104.76/13.67    inference(resolution,[status(thm)],[f370,f628])).
% 104.76/13.67  fof(f985,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (ap_parcontractE_c2(X0,q,comb_app(X1,X2))|ap_parcontractE_c3(X0,q,comb_app(X1,X2))|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|comb_app(X1,X2)=comb_app(X0,q)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f370,f128])).
% 104.76/13.67  fof(f991,definition,(
% 104.76/13.67    sQ102_spl <=> (member(pair(combS,combS),parcontract))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f993,plain,(
% 104.76/13.67    ~member(pair(combS,combS),parcontract)|sQ102_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f991])).
% 104.76/13.67  fof(f1001,plain,(
% 104.76/13.67    ![X0,X1,X2,X3,X4]: (ap_parcontractE_c2(p,X0,comb_app(X1,X2))|ap_parcontractE_c3(p,X0,comb_app(X1,X2))|~member(pair(p,X1),parcontract)|~member(pair(X0,X2),parcontract)|comb_app(X1,X2)=comb_app(p,X0)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|~member(X3,comb)|~member(X4,comb)|comb_app(comb_app(X3,q),comb_app(X4,q))=comb_app(comb_app(comb_app(combS,X3),X4),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2q(p,X0,comb_app(X1,X2))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q))))|~sQ52_spl)),
% 104.76/13.67    inference(resolution,[status(thm)],[f371,f628])).
% 104.76/13.67  fof(f1002,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (ap_parcontractE_c2(q,X0,comb_app(X1,X2))|ap_parcontractE_c3(q,X0,comb_app(X1,X2))|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|comb_app(X1,X2)=comb_app(q,X0)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))|~member(pair(p,X3),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f371,f128])).
% 104.76/13.67  fof(f1027,plain,(
% 104.76/13.67    comb_app(combS,combS)=comb_app(combK,comb_app(comb_app(combS,combS),combS))|~sQ99_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f974,f116])).
% 104.76/13.67  fof(f1028,plain,(
% 104.76/13.67    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c2(comb_app(combK,X0),X1,X0)|ap_parcontractE_c3(comb_app(combK,X0),X1,X0)|ap_parcontractE_c4(comb_app(combK,X0),X1,X0)|X0=comb_app(comb_app(combK,X0),X1))),
% 104.76/13.67    inference(resolution,[status(thm)],[f483,f110])).
% 104.76/13.67  fof(f1031,plain,(
% 104.76/13.67    ![X0,X1,X2]: (~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|ap_contractE_c1(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_c3(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(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))),
% 104.76/13.67    inference(resolution,[status(thm)],[f484,f91])).
% 104.76/13.67  fof(f1058,plain,(
% 104.76/13.67    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|ap_contractE_c1(comb_app(combK,X0),X1,X0)|ap_contractE_c2(comb_app(combK,X0),X1,X0)|ap_contractE_c3(comb_app(combK,X0),X1,X0)|member(pair(X1,ap_contractE_sk3q(comb_app(combK,X0),X1,X0)),contract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f500,f91])).
% 104.76/13.67  fof(f1060,plain,(
% 104.76/13.67    ![X0,X1]: (member(comb_app(combK,X0),comb)|~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c2(comb_app(combK,X0),X1,X0)|ap_parcontractE_c3(comb_app(combK,X0),X1,X0)|ap_parcontractE_c4(comb_app(combK,X0),X1,X0))),
% 104.76/13.67    inference(resolution,[status(thm)],[f560,f483])).
% 104.76/13.67  fof(f1062,plain,(
% 104.76/13.67    ![X0,X1,X2]: (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(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_c4(comb_app(comb_app(combS,X0),X1),X2,comb_app(comb_app(X0,X2),comb_app(X1,X2)))|~member(X0,comb)|~member(X1,comb)|~member(X2,comb))),
% 104.76/13.67    inference(resolution,[status(thm)],[f560,f211])).
% 104.76/13.67  fof(f1066,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c2(X0,X1,comb_app(X2,X3))|ap_parcontractE_c3(X0,X1,comb_app(X2,X3))|ap_parcontractE_c4(X0,X1,comb_app(X2,X3))|~member(pair(X0,X2),parcontract)|~member(pair(X1,X3),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f560,f214])).
% 104.76/13.67  fof(f1074,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c2(X1,X0,comb_app(X2,X3))|ap_parcontractE_c3(X1,X0,comb_app(X2,X3))|ap_parcontractE_c4(X1,X0,comb_app(X2,X3))|~member(pair(X1,X2),parcontract)|~member(pair(X0,X3),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f561,f214])).
% 104.76/13.67  fof(f1079,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c3(X1,X0,comb_app(X2,X3))|ap_parcontractE_c4(X1,X0,comb_app(X2,X3))|~member(pair(X1,X2),parcontract)|~member(pair(X0,X3),parcontract))),
% 104.76/13.67    inference(forward_subsumption_resolution,[status(thm)],[f1074,f114])).
% 104.76/13.67  fof(f1081,plain,(
% 104.76/13.67    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c2(comb_app(combK,X0),X1,X0)|ap_parcontractE_c3(comb_app(combK,X0),X1,X0)|X0=comb_app(comb_app(combK,X0),X1)|member(pair(X1,ap_parcontractE_sk2s(comb_app(combK,X0),X1,X0)),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1028,f124])).
% 104.76/13.67  fof(f1087,plain,(
% 104.76/13.67    ~member(combS,comb)|~member(combS,comb)|~member(p,comb)|member(pair(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(comb_app(combS,p),comb_app(combS,p))),contract)|~sQ86_spl),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f73])).
% 104.76/13.67  fof(f1088,plain,(
% 104.76/13.67    ~member(combS,comb)|~member(combS,comb)|~member(p,comb)|member(pair(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(comb_app(combS,p),comb_app(combS,p))),parcontract)|~sQ86_spl),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f99])).
% 104.76/13.67  fof(f1089,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|ap_contractE_c1(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_contractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_contractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_contractE_c4(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f484])).
% 104.76/13.67  fof(f1090,plain,(
% 104.76/13.67    ![X0]: (~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|ap_contractE_c1(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_contractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_contractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_contractE_c4(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f484])).
% 104.76/13.67  fof(f1094,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)|member(pair(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))),parcontract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f368])).
% 104.76/13.67  fof(f1095,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)|member(pair(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),ap_parcontractE_sk2q(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))),parcontract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f368])).
% 104.76/13.67  fof(f1096,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)|member(pair(p,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))),parcontract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f367])).
% 104.76/13.67  fof(f1097,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)|member(pair(p,ap_parcontractE_sk2s(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))),parcontract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f367])).
% 104.76/13.67  fof(f1098,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))))|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f366])).
% 104.76/13.67  fof(f1099,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))),ap_parcontractE_sk2s(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))))|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f366])).
% 104.76/13.67  fof(f1107,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|member(pair(comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p),comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p)))),contract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f73])).
% 104.76/13.67  fof(f1108,plain,(
% 104.76/13.67    ![X0]: (~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|member(pair(comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p),comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p))),contract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f73])).
% 104.76/13.67  fof(f1110,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c4(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))|~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f259])).
% 104.76/13.67  fof(f1111,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c4(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f259])).
% 104.76/13.67  fof(f1112,plain,(
% 104.76/13.67    ~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|member(pair(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(comb_app(combS,p),comb_app(combS,p))),parcontract)|~sQ86_spl),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f342])).
% 104.76/13.67  fof(f1113,plain,(
% 104.76/13.67    ~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|member(pair(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(comb_app(comb_app(combS,combS),combS),p)),parcontract)|~sQ86_spl),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f342])).
% 104.76/13.67  fof(f1116,plain,(
% 104.76/13.67    ~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|member(comb_app(comb_app(combS,p),comb_app(combS,p)),comb)|~sQ86_spl),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f70])).
% 104.76/13.67  fof(f1118,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c1(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))|ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c4(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f211])).
% 104.76/13.67  fof(f1119,plain,(
% 104.76/13.67    ![X0]: (ap_parcontractE_c1(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))|ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c4(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f211])).
% 104.76/13.67  fof(f1121,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|~member(comb_app(comb_app(combS,combS),combS),comb)|~member(p,comb)|member(pair(comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p),comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p)))),parcontract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f99])).
% 104.76/13.67  fof(f1122,plain,(
% 104.76/13.67    ![X0]: (~member(comb_app(comb_app(combS,combS),combS),comb)|~member(X0,comb)|~member(p,comb)|member(pair(comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p),comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p))),parcontract)|~sQ86_spl)),
% 104.76/13.67    inference(paramodulation,[status(thm)],[f856,f99])).
% 104.76/13.67  fof(f1207,definition,(
% 104.76/13.67    sQ109_spl <=> (member(pair(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(comb_app(combS,p),comb_app(combS,p))),contract))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1210,plain,(
% 104.76/13.67    ~sQ3_spl|~sQ24_spl|sQ109_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1087,f139,f401,f1207,f855])).
% 104.76/13.67  fof(f1211,definition,(
% 104.76/13.67    sQ110_spl <=> (member(pair(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(comb_app(combS,p),comb_app(combS,p))),parcontract))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1214,plain,(
% 104.76/13.67    ~sQ3_spl|~sQ24_spl|sQ110_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1088,f139,f401,f1211,f855])).
% 104.76/13.67  fof(f1215,definition,(
% 104.76/13.67    ![X0]: (sQ111_spl <=> (~member(X0,comb)|ap_contractE_c1(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_contractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_contractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_contractE_c4(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1218,definition,(
% 104.76/13.67    sQ112_spl <=> (member(comb_app(comb_app(combS,combS),combS),comb))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1220,plain,(
% 104.76/13.67    ~member(comb_app(comb_app(combS,combS),combS),comb)|sQ112_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f1218])).
% 104.76/13.67  fof(f1221,plain,(
% 104.76/13.67    sQ111_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1089,f1215,f1218,f401,f855])).
% 104.76/13.67  fof(f1222,definition,(
% 104.76/13.67    ![X0]: (sQ113_spl <=> (~member(X0,comb)|ap_contractE_c1(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_contractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_contractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_contractE_c4(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1225,plain,(
% 104.76/13.67    ~sQ112_spl|sQ113_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1090,f1218,f1222,f401,f855])).
% 104.76/13.67  fof(f1268,definition,(
% 104.76/13.67    ![X0]: (sQ114_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)|member(pair(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))),parcontract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1271,plain,(
% 104.76/13.67    sQ114_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1094,f1268,f1218,f401,f855])).
% 104.76/13.67  fof(f1272,definition,(
% 104.76/13.67    ![X0]: (sQ115_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(X0,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)|member(pair(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),ap_parcontractE_sk2q(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))),parcontract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1275,plain,(
% 104.76/13.67    sQ115_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1095,f1272,f1218,f401,f855])).
% 104.76/13.67  fof(f1276,definition,(
% 104.76/13.67    ![X0]: (sQ116_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)|member(pair(p,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))),parcontract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1279,plain,(
% 104.76/13.67    sQ116_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1096,f1276,f1218,f401,f855])).
% 104.76/13.67  fof(f1280,definition,(
% 104.76/13.67    ![X0]: (sQ117_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(X0,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)|member(pair(p,ap_parcontractE_sk2s(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))),parcontract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1283,plain,(
% 104.76/13.67    sQ117_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1097,f1280,f1218,f401,f855])).
% 104.76/13.67  fof(f1284,definition,(
% 104.76/13.67    ![X0]: (sQ118_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))))))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1287,plain,(
% 104.76/13.67    sQ118_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1098,f1284,f1218,f401,f855])).
% 104.76/13.67  fof(f1288,definition,(
% 104.76/13.67    ![X0]: (sQ119_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(X0,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(ap_parcontractE_sk2q(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))),ap_parcontractE_sk2s(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))))))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1291,plain,(
% 104.76/13.67    sQ119_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1099,f1288,f1218,f401,f855])).
% 104.76/13.67  fof(f1308,definition,(
% 104.76/13.67    sQ125_spl <=> (member(pair(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(comb_app(combS,p),comb_app(combS,p))),parcontract))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1312,definition,(
% 104.76/13.67    sQ126_spl <=> (member(pair(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(comb_app(comb_app(combS,combS),combS),p)),parcontract))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1316,definition,(
% 104.76/13.67    sQ127_spl <=> (member(comb_app(comb_app(combS,p),comb_app(combS,p)),comb))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1332,definition,(
% 104.76/13.67    ![X0]: (sQ131_spl <=> (~member(X0,comb)|member(pair(comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p),comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p)))),contract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1335,plain,(
% 104.76/13.67    sQ131_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1107,f1332,f1218,f401,f855])).
% 104.76/13.67  fof(f1336,definition,(
% 104.76/13.67    ![X0]: (sQ132_spl <=> (~member(X0,comb)|member(pair(comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p),comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p))),contract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1339,plain,(
% 104.76/13.67    ~sQ112_spl|sQ132_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1108,f1218,f1336,f401,f855])).
% 104.76/13.67  fof(f1352,definition,(
% 104.76/13.67    ![X0]: (sQ133_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c4(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))|~member(X0,comb)|comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p))=comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1355,plain,(
% 104.76/13.67    sQ133_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1110,f1352,f1218,f401,f855])).
% 104.76/13.67  fof(f1356,definition,(
% 104.76/13.67    ![X0]: (sQ134_spl <=> (ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c4(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))|~member(X0,comb)|comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p))=comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1359,plain,(
% 104.76/13.67    sQ134_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1111,f1356,f1218,f401,f855])).
% 104.76/13.67  fof(f1360,plain,(
% 104.76/13.67    ~sQ112_spl|~sQ24_spl|sQ125_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1112,f1218,f401,f1308,f855])).
% 104.76/13.67  fof(f1361,plain,(
% 104.76/13.67    ~sQ112_spl|~sQ24_spl|sQ126_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1113,f1218,f401,f1312,f855])).
% 104.76/13.67  fof(f1364,plain,(
% 104.76/13.67    ~sQ112_spl|~sQ24_spl|sQ127_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1116,f1218,f401,f1316,f855])).
% 104.76/13.67  fof(f1377,definition,(
% 104.76/13.67    ![X0]: (sQ135_spl <=> (ap_parcontractE_c1(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p))))|ap_parcontractE_c2(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|ap_parcontractE_c4(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p,comb_app(comb_app(X0,p),comb_app(comb_app(comb_app(combS,combS),combS),p)))|~member(X0,comb)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1380,plain,(
% 104.76/13.67    sQ135_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1118,f1377,f1218,f401,f855])).
% 104.76/13.67  fof(f1381,definition,(
% 104.76/13.67    ![X0]: (sQ136_spl <=> (ap_parcontractE_c1(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p)))|ap_parcontractE_c2(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|ap_parcontractE_c4(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p,comb_app(comb_app(comb_app(comb_app(combS,combS),combS),p),comb_app(X0,p)))|~member(X0,comb)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1384,plain,(
% 104.76/13.67    sQ136_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1119,f1381,f1218,f401,f855])).
% 104.76/13.67  fof(f1391,definition,(
% 104.76/13.67    ![X0]: (sQ137_spl <=> (~member(X0,comb)|member(pair(comb_app(comb_app(comb_app(combS,X0),comb_app(comb_app(combS,combS),combS)),p),comb_app(comb_app(X0,p),comb_app(comb_app(combS,p),comb_app(combS,p)))),parcontract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1394,plain,(
% 104.76/13.67    sQ137_spl|~sQ112_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1121,f1391,f1218,f401,f855])).
% 104.76/13.67  fof(f1395,definition,(
% 104.76/13.67    ![X0]: (sQ138_spl <=> (~member(X0,comb)|member(pair(comb_app(comb_app(comb_app(combS,comb_app(comb_app(combS,combS),combS)),X0),p),comb_app(comb_app(comb_app(combS,p),comb_app(combS,p)),comb_app(X0,p))),parcontract)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f1398,plain,(
% 104.76/13.67    ~sQ112_spl|sQ138_spl|~sQ24_spl|~sQ86_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f1122,f1218,f1395,f401,f855])).
% 104.76/13.67  fof(f2252,definition,(
% 104.76/13.67    sQ139_spl <=> (ap_parcontractE_c1(combS,p,comb_app(combS,p)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2253,plain,(
% 104.76/13.67    ap_parcontractE_c1(combS,p,comb_app(combS,p))|~sQ139_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f2252])).
% 104.76/13.67  fof(f2255,definition,(
% 104.76/13.67    sQ140_spl <=> (ap_parcontractE_c2(combS,p,comb_app(combS,p)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2256,plain,(
% 104.76/13.67    ap_parcontractE_c2(combS,p,comb_app(combS,p))|~sQ140_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f2255])).
% 104.76/13.67  fof(f2258,definition,(
% 104.76/13.67    sQ141_spl <=> (ap_parcontractE_c3(combS,p,comb_app(combS,p)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2259,plain,(
% 104.76/13.67    ap_parcontractE_c3(combS,p,comb_app(combS,p))|~sQ141_spl),
% 104.76/13.67    inference(component_clause,[status(thm)],[f2258])).
% 104.76/13.67  fof(f2261,definition,(
% 104.76/13.67    sQ142_spl <=> (ap_parcontractE_c4(combS,p,comb_app(combS,p)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2374,plain,(
% 104.76/13.67    ![X0,X1,X2]: (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(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)))|~member(X0,comb)|~member(X1,comb)|~member(X2,comb)|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))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1062,f124])).
% 104.76/13.67  fof(f2408,plain,(
% 104.76/13.67    combS=comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,p,comb_app(combS,p))),ap_parcontractE_sk1q(combS,p,comb_app(combS,p)))|~sQ141_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f2259,f122])).
% 104.76/13.67  fof(f2413,plain,(
% 104.76/13.67    combS=comb_app(combK,comb_app(combS,p))|~sQ140_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f2256,f116])).
% 104.76/13.67  fof(f2471,plain,(
% 104.76/13.67    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|~member(combS,comb)|ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_contractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS))))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1031,f96])).
% 104.76/13.67  fof(f2472,plain,(
% 104.76/13.67    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|~member(combK,comb)|ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_contractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK))))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1031,f95])).
% 104.76/13.67  fof(f2476,definition,(
% 104.76/13.67    ![X0,X1]: (sQ153_spl <=> (~member(X0,comb)|~member(X1,comb)|ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_contractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2479,plain,(
% 104.76/13.67    sQ153_spl|~sQ3_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f2471,f2476,f139])).
% 104.76/13.67  fof(f2480,definition,(
% 104.76/13.67    ![X0,X1]: (sQ154_spl <=> (~member(X0,comb)|~member(X1,comb)|ap_contractE_c1(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_contractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_contractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2483,plain,(
% 104.76/13.67    sQ154_spl|~sQ1_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f2472,f2480,f132])).
% 104.76/13.67  fof(f2512,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|~member(combS,comb)|ap_contractE_c1(comb_app(combK,X0),combS,X0)|ap_contractE_c2(comb_app(combK,X0),combS,X0)|ap_contractE_c3(comb_app(combK,X0),combS,X0))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1058,f96])).
% 104.76/13.67  fof(f2513,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|~member(combK,comb)|ap_contractE_c1(comb_app(combK,X0),combK,X0)|ap_contractE_c2(comb_app(combK,X0),combK,X0)|ap_contractE_c3(comb_app(combK,X0),combK,X0))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1058,f95])).
% 104.76/13.67  fof(f2514,definition,(
% 104.76/13.67    ![X0]: (sQ158_spl <=> (~member(X0,comb)|ap_contractE_c1(comb_app(combK,X0),combS,X0)|ap_contractE_c2(comb_app(combK,X0),combS,X0)|ap_contractE_c3(comb_app(combK,X0),combS,X0)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2517,plain,(
% 104.76/13.67    sQ158_spl|~sQ3_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f2512,f2514,f139])).
% 104.76/13.67  fof(f2518,definition,(
% 104.76/13.67    ![X0]: (sQ159_spl <=> (~member(X0,comb)|ap_contractE_c1(comb_app(combK,X0),combK,X0)|ap_contractE_c2(comb_app(combK,X0),combK,X0)|ap_contractE_c3(comb_app(combK,X0),combK,X0)))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2521,plain,(
% 104.76/13.67    sQ159_spl|~sQ1_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f2513,f2518,f132])).
% 104.76/13.67  fof(f2522,plain,(
% 104.76/13.67    member(p,comb)|~sQ139_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f2253,f561])).
% 104.76/13.67  fof(f2525,plain,(
% 104.76/13.67    $false|sQ24_spl|~sQ139_spl),
% 104.76/13.67    inference(forward_subsumption_resolution,[status(thm)],[f2522,f403])).
% 104.76/13.67  fof(f2526,plain,(
% 104.76/13.67    sQ24_spl|~sQ139_spl),
% 104.76/13.67    inference(contradiction_clause,[status(thm)],[f2525])).
% 104.76/13.67  fof(f2542,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c2(X0,X1,comb_app(X2,X3))|ap_parcontractE_c3(X0,X1,comb_app(X2,X3))|~member(pair(X0,X2),parcontract)|~member(pair(X1,X3),parcontract)|member(pair(X1,ap_parcontractE_sk2s(X0,X1,comb_app(X2,X3))),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1066,f124])).
% 104.76/13.67  fof(f2543,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c2(X0,X1,comb_app(X2,X3))|ap_parcontractE_c3(X0,X1,comb_app(X2,X3))|~member(pair(X0,X2),parcontract)|~member(pair(X1,X3),parcontract)|member(pair(X0,ap_parcontractE_sk2q(X0,X1,comb_app(X2,X3))),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1066,f123])).
% 104.76/13.67  fof(f2548,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c3(X1,X0,comb_app(X2,X3))|~member(pair(X1,X2),parcontract)|~member(pair(X0,X3),parcontract)|member(pair(X0,ap_parcontractE_sk2s(X1,X0,comb_app(X2,X3))),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1079,f124])).
% 104.76/13.67  fof(f2549,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c3(X1,X0,comb_app(X2,X3))|~member(pair(X1,X2),parcontract)|~member(pair(X0,X3),parcontract)|member(pair(X1,ap_parcontractE_sk2q(X1,X0,comb_app(X2,X3))),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1079,f123])).
% 104.76/13.67  fof(f2552,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|~member(pair(X1,X2),parcontract)|~member(pair(X0,X3),parcontract)|member(pair(X0,ap_parcontractE_sk2s(X1,X0,comb_app(X2,X3))),parcontract))),
% 104.76/13.67    inference(forward_subsumption_resolution,[status(thm)],[f2548,f120])).
% 104.76/13.67  fof(f2553,plain,(
% 104.76/13.67    ![X0,X1,X2,X3]: (member(X0,comb)|~member(pair(X1,X2),parcontract)|~member(pair(X0,X3),parcontract)|member(pair(X1,ap_parcontractE_sk2q(X1,X0,comb_app(X2,X3))),parcontract))),
% 104.76/13.67    inference(forward_subsumption_resolution,[status(thm)],[f2549,f120])).
% 104.76/13.67  fof(f2562,plain,(
% 104.76/13.67    combS=comb_app(comb_app(combS,combS),combS)|~sQ99_spl),
% 104.76/13.67    inference(resolution,[status(thm)],[f1027,f62])).
% 104.76/13.67  fof(f2627,plain,(
% 104.76/13.67    $false|~sQ99_spl),
% 104.76/13.67    inference(forward_subsumption_resolution,[status(thm)],[f2562,f58])).
% 104.76/13.67  fof(f2628,plain,(
% 104.76/13.67    ~sQ99_spl),
% 104.76/13.67    inference(contradiction_clause,[status(thm)],[f2627])).
% 104.76/13.67  fof(f2630,plain,(
% 104.76/13.67    ![X0,X1]: (member(comb_app(combK,X0),comb)|~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c2(comb_app(combK,X0),X1,X0)|ap_parcontractE_c3(comb_app(combK,X0),X1,X0)|member(pair(X1,ap_parcontractE_sk2s(comb_app(combK,X0),X1,X0)),parcontract))),
% 104.76/13.67    inference(resolution,[status(thm)],[f1060,f124])).
% 104.76/13.67  fof(f2643,plain,(
% 104.76/13.67    ![X0,X1,X2]: (~member(X0,comb)|~member(p,comb)|ap_parcontractE_c2(comb_app(combK,X0),p,X0)|ap_parcontractE_c3(comb_app(combK,X0),p,X0)|X0=comb_app(comb_app(combK,X0),p)|ap_parcontractE_c2(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X1,q),comb_app(X2,q))=comb_app(comb_app(comb_app(combS,X1),X2),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X0),p,X0)),ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q))))|~sQ52_spl)),
% 104.76/13.67    inference(resolution,[status(thm)],[f1081,f628])).
% 104.76/13.67  fof(f2647,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|~member(combS,comb)|ap_parcontractE_c2(comb_app(combK,X0),combS,X0)|ap_parcontractE_c3(comb_app(combK,X0),combS,X0)|X0=comb_app(comb_app(combK,X0),combS)|ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0)=combS)),
% 104.76/13.67    inference(resolution,[status(thm)],[f1081,f106])).
% 104.76/13.67  fof(f2648,plain,(
% 104.76/13.67    ![X0]: (~member(X0,comb)|~member(combK,comb)|ap_parcontractE_c2(comb_app(combK,X0),combK,X0)|ap_parcontractE_c3(comb_app(combK,X0),combK,X0)|X0=comb_app(comb_app(combK,X0),combK)|ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0)=combK)),
% 104.76/13.67    inference(resolution,[status(thm)],[f1081,f103])).
% 104.76/13.67  fof(f2649,definition,(
% 104.76/13.67    ![X0,X1,X2]: (sQ162_spl <=> (~member(X0,comb)|ap_parcontractE_c2(comb_app(combK,X0),p,X0)|ap_parcontractE_c3(comb_app(combK,X0),p,X0)|X0=comb_app(comb_app(combK,X0),p)|ap_parcontractE_c2(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X1,q),comb_app(X2,q))=comb_app(comb_app(comb_app(combS,X1),X2),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X0),p,X0)),ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q))))))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2652,plain,(
% 104.76/13.67    sQ162_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f2643,f2649,f401,f627])).
% 104.76/13.67  fof(f2661,definition,(
% 104.76/13.67    ![X0]: (sQ165_spl <=> (~member(X0,comb)|ap_parcontractE_c2(comb_app(combK,X0),combS,X0)|ap_parcontractE_c3(comb_app(combK,X0),combS,X0)|X0=comb_app(comb_app(combK,X0),combS)|ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0)=combS))),
% 104.76/13.67    introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 104.76/13.67  fof(f2664,plain,(
% 104.76/13.67    sQ165_spl|~sQ3_spl),
% 104.76/13.67    inference(split_clause,[status(thm)],[f2647,f2661,f139])).
% 104.76/13.67  fof(f2665,definition,(
% 104.76/13.67    ![X0]: (sQ166_spl <=> (~member(X0,comb)|ap_parcontractE_c2(comb_app(combK,X0),combK,X0)|ap_parcontractE_c3(comb_app(combK,X0),combK,X0)|X0=comb_app(comb_app(combK,X0),combK)|ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0)=combK))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f2668,plain,(
% 104.76/13.69    sQ166_spl|~sQ1_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f2648,f2665,f132])).
% 104.76/13.69  fof(f2699,plain,(
% 104.76/13.69    member(p,comb)|~sQ29_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f423,f67])).
% 104.76/13.69  fof(f2700,plain,(
% 104.76/13.69    member(pair(comb_app(combS,p),comb_app(combS,p)),parcontract)|~sQ29_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f423,f97])).
% 104.76/13.69  fof(f2701,plain,(
% 104.76/13.69    $false|sQ24_spl|~sQ29_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f2699,f403])).
% 104.76/13.69  fof(f2702,plain,(
% 104.76/13.69    sQ24_spl|~sQ29_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f2701])).
% 104.76/13.69  fof(f2703,plain,(
% 104.76/13.69    member(pair(q,q),parcontract)|~sQ25_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f405,f97])).
% 104.76/13.69  fof(f2708,plain,(
% 104.76/13.69    ![X0]: (~r=comb_app(comb_app(combS,X0),q)|~member(pair(p,X0),parcontract)|~sQ25_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2703,f128])).
% 104.76/13.69  fof(f2709,plain,(
% 104.76/13.69    ap_parcontractE_c1(combS,p,comb_app(combS,p))|ap_parcontractE_c2(combS,p,comb_app(combS,p))|ap_parcontractE_c3(combS,p,comb_app(combS,p))|ap_parcontractE_c4(combS,p,comb_app(combS,p))|~sQ29_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f2700,f107])).
% 104.76/13.69  fof(f2710,plain,(
% 104.76/13.69    sQ139_spl|sQ140_spl|sQ141_spl|sQ142_spl|~sQ29_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f2709,f2252,f2255,f2258,f2261,f422])).
% 104.76/13.69  fof(f2738,definition,(
% 104.76/13.69    sQ174_spl <=> (member(pair(comb_app(combS,p),comb_app(combS,p)),parcontract))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f2740,plain,(
% 104.76/13.69    ~member(pair(comb_app(combS,p),comb_app(combS,p)),parcontract)|sQ174_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f2738])).
% 104.76/13.69  fof(f2750,plain,(
% 104.76/13.69    $false|~sQ29_spl|sQ174_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f2740,f2700])).
% 104.76/13.69  fof(f2751,plain,(
% 104.76/13.69    ~sQ29_spl|sQ174_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f2750])).
% 104.76/13.69  fof(f2768,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (ap_parcontractE_c2(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2))|ap_parcontractE_c3(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2))|~member(pair(X0,X2),parcontract)|comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2)=comb_app(p,X0)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|~member(X3,comb)|~member(X4,comb)|comb_app(comb_app(X3,q),comb_app(X4,q))=comb_app(comb_app(comb_app(combS,X3),X4),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2q(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q))))|~member(X1,comb)|~member(p,comb)|ap_parcontractE_c2(comb_app(combK,X1),p,X1)|ap_parcontractE_c3(comb_app(combK,X1),p,X1)|X1=comb_app(comb_app(combK,X1),p)|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f1001,f1081])).
% 104.76/13.69  fof(f2769,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (ap_parcontractE_c2(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3))|ap_parcontractE_c3(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3))|~member(pair(X0,X3),parcontract)|comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3)=comb_app(p,X0)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2q(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))|ap_parcontractE_c2(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p)))|~member(X1,comb)|~member(X2,comb)|~member(p,comb)|comb_app(comb_app(X1,p),comb_app(X2,p))=comb_app(comb_app(comb_app(combS,X1),X2),p)|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f1001,f367])).
% 104.76/13.69  fof(f2771,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (sQ179_spl <=> (ap_parcontractE_c2(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2))|ap_parcontractE_c3(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2))|~member(pair(X0,X2),parcontract)|comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2)=comb_app(p,X0)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|~member(X3,comb)|~member(X4,comb)|comb_app(comb_app(X3,q),comb_app(X4,q))=comb_app(comb_app(comb_app(combS,X3),X4),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2q(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(combK,X1),p,X1),X2))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q))))|~member(X1,comb)|ap_parcontractE_c2(comb_app(combK,X1),p,X1)|ap_parcontractE_c3(comb_app(combK,X1),p,X1)|X1=comb_app(comb_app(combK,X1),p)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f2774,plain,(
% 104.76/13.69    sQ179_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f2768,f2771,f401,f627])).
% 104.76/13.69  fof(f2775,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ180_spl <=> (ap_parcontractE_c2(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3))|ap_parcontractE_c3(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3))|~member(pair(X0,X3),parcontract)|comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3)=comb_app(p,X0)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2q(p,X0,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p))),X3))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))|ap_parcontractE_c2(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X1),X2),p,comb_app(comb_app(X1,p),comb_app(X2,p)))|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X1,p),comb_app(X2,p))=comb_app(comb_app(comb_app(combS,X1),X2),p)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f2778,plain,(
% 104.76/13.69    sQ180_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f2769,f2775,f401,f627])).
% 104.76/13.69  fof(f2781,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (ap_parcontractE_c2(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2)))|ap_parcontractE_c3(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2)))|~member(pair(X0,X1),parcontract)|comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2))=comb_app(X0,p)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|~member(X3,comb)|~member(X4,comb)|comb_app(comb_app(X3,q),comb_app(X4,q))=comb_app(comb_app(comb_app(combS,X3),X4),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2)))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q))))|~member(X2,comb)|~member(p,comb)|ap_parcontractE_c2(comb_app(combK,X2),p,X2)|ap_parcontractE_c3(comb_app(combK,X2),p,X2)|X2=comb_app(comb_app(combK,X2),p)|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f984,f1081])).
% 104.76/13.69  fof(f2782,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (ap_parcontractE_c2(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))))|ap_parcontractE_c3(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))))|~member(pair(X0,X1),parcontract)|comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p))))=comb_app(X0,p)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))|ap_parcontractE_c2(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|~member(X2,comb)|~member(X3,comb)|~member(p,comb)|comb_app(comb_app(X2,p),comb_app(X3,p))=comb_app(comb_app(comb_app(combS,X2),X3),p)|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f984,f367])).
% 104.76/13.69  fof(f2784,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (sQ181_spl <=> (ap_parcontractE_c2(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2)))|ap_parcontractE_c3(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2)))|~member(pair(X0,X1),parcontract)|comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2))=comb_app(X0,p)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q)))|~member(X3,comb)|~member(X4,comb)|comb_app(comb_app(X3,q),comb_app(X4,q))=comb_app(comb_app(comb_app(combS,X3),X4),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(combK,X2),p,X2)))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),q,comb_app(comb_app(X3,q),comb_app(X4,q))))|~member(X2,comb)|ap_parcontractE_c2(comb_app(combK,X2),p,X2)|ap_parcontractE_c3(comb_app(combK,X2),p,X2)|X2=comb_app(comb_app(combK,X2),p)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f2787,plain,(
% 104.76/13.69    sQ181_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f2781,f2784,f401,f627])).
% 104.76/13.69  fof(f2788,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ182_spl <=> (ap_parcontractE_c2(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))))|ap_parcontractE_c3(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))))|~member(pair(X0,X1),parcontract)|comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p))))=comb_app(X0,p)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(X0,p,comb_app(X1,ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))|ap_parcontractE_c2(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X2),X3),p,comb_app(comb_app(X2,p),comb_app(X3,p)))|~member(X2,comb)|~member(X3,comb)|comb_app(comb_app(X2,p),comb_app(X3,p))=comb_app(comb_app(comb_app(combS,X2),X3),p)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f2791,plain,(
% 104.76/13.69    sQ182_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f2782,f2788,f401,f627])).
% 104.76/13.69  fof(f2793,definition,(
% 104.76/13.69    sQ183_spl <=> (member(pair(comb_app(combS,combS),comb_app(combS,combS)),parcontract))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f2795,plain,(
% 104.76/13.69    ~member(pair(comb_app(combS,combS),comb_app(combS,combS)),parcontract)|sQ183_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f2793])).
% 104.76/13.69  fof(f2803,plain,(
% 104.76/13.69    $false|sQ102_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f993,f145])).
% 104.76/13.69  fof(f2804,plain,(
% 104.76/13.69    sQ102_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f2803])).
% 104.76/13.69  fof(f2805,plain,(
% 104.76/13.69    $false|sQ183_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f2795,f165])).
% 104.76/13.69  fof(f2806,plain,(
% 104.76/13.69    sQ183_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f2805])).
% 104.76/13.69  fof(f2824,plain,(
% 104.76/13.69    $false|sQ112_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f1220,f163])).
% 104.76/13.69  fof(f2825,plain,(
% 104.76/13.69    sQ112_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f2824])).
% 104.76/13.69  fof(f2826,plain,(
% 104.76/13.69    $false|~sQ141_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f2408,f58])).
% 104.76/13.69  fof(f2827,plain,(
% 104.76/13.69    ~sQ141_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f2826])).
% 104.76/13.69  fof(f2889,plain,(
% 104.76/13.69    ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(comb_app(combS,p),q,r))=combS|~sQ21_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f582,f106])).
% 104.76/13.69  fof(f2891,plain,(
% 104.76/13.69    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)))|~sQ21_spl),
% 104.76/13.69    inference(backward_demodulation,[status(thm)],[f2889,f580])).
% 104.76/13.69  fof(f3009,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|~member(X0,comb)|~member(X1,comb)|~member(p,comb)|ap_parcontractE_c2(X2,p,comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))))|ap_parcontractE_c3(X2,p,comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))))|~member(pair(X2,X3),parcontract)|comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))))=comb_app(X2,p)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(X2,p,comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2374,f984])).
% 104.76/13.69  fof(f3010,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|~member(X0,comb)|~member(X1,comb)|~member(p,comb)|ap_parcontractE_c2(p,X2,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3))|ap_parcontractE_c3(p,X2,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3))|~member(pair(X2,X3),parcontract)|comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3)=comb_app(p,X2)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2q(p,X2,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2374,f1001])).
% 104.76/13.69  fof(f3011,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|~member(X0,comb)|~member(X1,comb)|~member(p,comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X2),X3),q,comb_app(comb_app(X2,q),comb_app(X3,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X2),X3),q,comb_app(comb_app(X2,q),comb_app(X3,q)))|~member(X2,comb)|~member(X3,comb)|comb_app(comb_app(X2,q),comb_app(X3,q))=comb_app(comb_app(comb_app(combS,X2),X3),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),q,comb_app(comb_app(X2,q),comb_app(X3,q))))|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2374,f628])).
% 104.76/13.69  fof(f3016,plain,(
% 104.76/13.69    ![X0,X1]: (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|~member(X0,comb)|~member(X1,comb)|~member(combS,comb)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))=combS)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2374,f106])).
% 104.76/13.69  fof(f3017,plain,(
% 104.76/13.69    ![X0,X1]: (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|~member(X0,comb)|~member(X1,comb)|~member(combK,comb)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))=combK)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2374,f103])).
% 104.76/13.69  fof(f3025,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ213_spl <=> (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c2(X2,p,comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))))|ap_parcontractE_c3(X2,p,comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))))|~member(pair(X2,X3),parcontract)|comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))))=comb_app(X2,p)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(X2,p,comb_app(X3,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3028,plain,(
% 104.76/13.69    sQ213_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3009,f3025,f401,f627])).
% 104.76/13.69  fof(f3029,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ214_spl <=> (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c2(p,X2,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3))|ap_parcontractE_c3(p,X2,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3))|~member(pair(X2,X3),parcontract)|comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3)=comb_app(p,X2)|ap_parcontractE_c2(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q)))|~member(X4,comb)|~member(X5,comb)|comb_app(comb_app(X4,q),comb_app(X5,q))=comb_app(comb_app(comb_app(combS,X4),X5),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2q(p,X2,comb_app(ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p))),X3))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X4),X5),q,comb_app(comb_app(X4,q),comb_app(X5,q))))))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3032,plain,(
% 104.76/13.69    sQ214_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3010,f3029,f401,f627])).
% 104.76/13.69  fof(f3033,definition,(
% 104.76/13.69    ![X0,X1,X2,X3]: (sQ215_spl <=> (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))|~member(X0,comb)|~member(X1,comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X2),X3),q,comb_app(comb_app(X2,q),comb_app(X3,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X2),X3),q,comb_app(comb_app(X2,q),comb_app(X3,q)))|~member(X2,comb)|~member(X3,comb)|comb_app(comb_app(X2,q),comb_app(X3,q))=comb_app(comb_app(comb_app(combS,X2),X3),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),p,comb_app(comb_app(X0,p),comb_app(X1,p)))),ap_parcontractE_sk2s(comb_app(comb_app(combS,X2),X3),q,comb_app(comb_app(X2,q),comb_app(X3,q))))))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3036,plain,(
% 104.76/13.69    sQ215_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3011,f3033,f401,f627])).
% 104.76/13.69  fof(f3049,definition,(
% 104.76/13.69    ![X0,X1]: (sQ219_spl <=> (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))|~member(X0,comb)|~member(X1,comb)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combS,comb_app(comb_app(X0,combS),comb_app(X1,combS)))=combS))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3052,plain,(
% 104.76/13.69    sQ219_spl|~sQ3_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3016,f3049,f139])).
% 104.76/13.69  fof(f3053,definition,(
% 104.76/13.69    ![X0,X1]: (sQ220_spl <=> (member(comb_app(comb_app(combS,X0),X1),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|ap_parcontractE_c3(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))|~member(X0,comb)|~member(X1,comb)|ap_parcontractE_sk2s(comb_app(comb_app(combS,X0),X1),combK,comb_app(comb_app(X0,combK),comb_app(X1,combK)))=combK))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3056,plain,(
% 104.76/13.69    sQ220_spl|~sQ1_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3017,f3053,f132])).
% 104.76/13.69  fof(f3760,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c2(X0,q,comb_app(X1,X2))|ap_parcontractE_c3(X0,q,comb_app(X1,X2))|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f2542,f128])).
% 104.76/13.69  fof(f3777,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (member(q,comb)|ap_parcontractE_c2(q,X0,comb_app(X1,X2))|ap_parcontractE_c3(q,X0,comb_app(X1,X2))|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|ap_parcontractE_c2(X3,q,comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2))))|ap_parcontractE_c3(X3,q,comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2))))|~member(pair(X3,X4),parcontract)|comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))=comb_app(X3,q)|~r=comb_app(comb_app(combS,X5),ap_parcontractE_sk2s(X3,q,comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))))|~member(pair(p,X5),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f2543,f985])).
% 104.76/13.69  fof(f3778,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (member(q,comb)|ap_parcontractE_c2(q,X0,comb_app(X1,X2))|ap_parcontractE_c3(q,X0,comb_app(X1,X2))|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|ap_parcontractE_c2(q,X3,comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4))|ap_parcontractE_c3(q,X3,comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4))|~member(pair(X3,X4),parcontract)|comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4)=comb_app(q,X3)|~r=comb_app(comb_app(combS,X5),ap_parcontractE_sk2q(q,X3,comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4)))|~member(pair(p,X5),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f2543,f1002])).
% 104.76/13.69  fof(f3779,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (member(q,comb)|ap_parcontractE_c2(q,X0,comb_app(X1,X2))|ap_parcontractE_c3(q,X0,comb_app(X1,X2))|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))|~member(pair(p,X3),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f2543,f128])).
% 104.76/13.69  fof(f3809,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ319_spl <=> (ap_parcontractE_c2(q,X0,comb_app(X1,X2))|ap_parcontractE_c3(q,X0,comb_app(X1,X2))|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|ap_parcontractE_c2(X3,q,comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2))))|ap_parcontractE_c3(X3,q,comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2))))|~member(pair(X3,X4),parcontract)|comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))=comb_app(X3,q)|~r=comb_app(comb_app(combS,X5),ap_parcontractE_sk2s(X3,q,comb_app(X4,ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))))|~member(pair(p,X5),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3812,plain,(
% 104.76/13.69    sQ25_spl|sQ319_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3777,f404,f3809])).
% 104.76/13.69  fof(f3813,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ320_spl <=> (ap_parcontractE_c2(q,X0,comb_app(X1,X2))|ap_parcontractE_c3(q,X0,comb_app(X1,X2))|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|ap_parcontractE_c2(q,X3,comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4))|ap_parcontractE_c3(q,X3,comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4))|~member(pair(X3,X4),parcontract)|comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4)=comb_app(q,X3)|~r=comb_app(comb_app(combS,X5),ap_parcontractE_sk2q(q,X3,comb_app(ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)),X4)))|~member(pair(p,X5),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3816,plain,(
% 104.76/13.69    sQ25_spl|sQ320_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3778,f404,f3813])).
% 104.76/13.69  fof(f3817,definition,(
% 104.76/13.69    ![X0,X1,X2,X3]: (sQ321_spl <=> (ap_parcontractE_c2(q,X0,comb_app(X1,X2))|ap_parcontractE_c3(q,X0,comb_app(X1,X2))|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))|~member(pair(p,X3),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f3820,plain,(
% 104.76/13.69    sQ25_spl|sQ321_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f3779,f404,f3817])).
% 104.76/13.69  fof(f4017,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (member(X0,comb)|ap_parcontractE_c3(X0,q,comb_app(X1,X2))|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract)|member(q,comb))),
% 104.76/13.69    inference(resolution,[status(thm)],[f3760,f114])).
% 104.76/13.69  fof(f4020,definition,(
% 104.76/13.69    ![X0,X1,X2,X3]: (sQ328_spl <=> (member(X0,comb)|ap_parcontractE_c3(X0,q,comb_app(X1,X2))|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4023,plain,(
% 104.76/13.69    sQ328_spl|sQ25_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4017,f4020,f404])).
% 104.76/13.69  fof(f4054,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (member(q,comb)|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|ap_parcontractE_c2(X3,q,comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2))))|ap_parcontractE_c3(X3,q,comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2))))|~member(pair(X3,X4),parcontract)|comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))=comb_app(X3,q)|~r=comb_app(comb_app(combS,X5),ap_parcontractE_sk2s(X3,q,comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))))|~member(pair(p,X5),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f2552,f985])).
% 104.76/13.69  fof(f4055,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (member(q,comb)|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f2552,f128])).
% 104.76/13.69  fof(f4083,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ336_spl <=> (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|ap_parcontractE_c2(X3,q,comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2))))|ap_parcontractE_c3(X3,q,comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2))))|~member(pair(X3,X4),parcontract)|comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))=comb_app(X3,q)|~r=comb_app(comb_app(combS,X5),ap_parcontractE_sk2s(X3,q,comb_app(X4,ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))))|~member(pair(p,X5),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4086,plain,(
% 104.76/13.69    sQ25_spl|sQ336_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4054,f404,f4083])).
% 104.76/13.69  fof(f4087,definition,(
% 104.76/13.69    ![X0,X1,X2,X3]: (sQ337_spl <=> (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4088,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract)|~sQ337_spl)),
% 104.76/13.69    inference(component_clause,[status(thm)],[f4087])).
% 104.76/13.69  fof(f4090,plain,(
% 104.76/13.69    sQ25_spl|sQ337_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4055,f404,f4087])).
% 104.76/13.69  fof(f4106,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (member(X0,comb)|~member(pair(q,X1),parcontract)|~member(pair(X0,X2),parcontract)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2q(q,X0,comb_app(X1,X2)))|~member(pair(p,X3),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f2553,f128])).
% 104.76/13.69  fof(f4150,plain,(
% 104.76/13.69    ![X0,X1,X2]: (member(comb_app(combK,X0),comb)|~member(X0,comb)|~member(p,comb)|ap_parcontractE_c2(comb_app(combK,X0),p,X0)|ap_parcontractE_c3(comb_app(combK,X0),p,X0)|ap_parcontractE_c2(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X1,q),comb_app(X2,q))=comb_app(comb_app(comb_app(combS,X1),X2),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X0),p,X0)),ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q))))|~sQ52_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2630,f628])).
% 104.76/13.69  fof(f4153,plain,(
% 104.76/13.69    ![X0]: (member(comb_app(combK,X0),comb)|~member(X0,comb)|~member(combS,comb)|ap_parcontractE_c2(comb_app(combK,X0),combS,X0)|ap_parcontractE_c3(comb_app(combK,X0),combS,X0)|ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0)=combS)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2630,f106])).
% 104.76/13.69  fof(f4154,plain,(
% 104.76/13.69    ![X0]: (member(comb_app(combK,X0),comb)|~member(X0,comb)|~member(combK,comb)|ap_parcontractE_c2(comb_app(combK,X0),combK,X0)|ap_parcontractE_c3(comb_app(combK,X0),combK,X0)|ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0)=combK)),
% 104.76/13.69    inference(resolution,[status(thm)],[f2630,f103])).
% 104.76/13.69  fof(f4168,definition,(
% 104.76/13.69    ![X0,X1,X2]: (sQ349_spl <=> (member(comb_app(combK,X0),comb)|~member(X0,comb)|ap_parcontractE_c2(comb_app(combK,X0),p,X0)|ap_parcontractE_c3(comb_app(combK,X0),p,X0)|ap_parcontractE_c2(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|ap_parcontractE_c3(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q)))|~member(X1,comb)|~member(X2,comb)|comb_app(comb_app(X1,q),comb_app(X2,q))=comb_app(comb_app(comb_app(combS,X1),X2),q)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X0),p,X0)),ap_parcontractE_sk2s(comb_app(comb_app(combS,X1),X2),q,comb_app(comb_app(X1,q),comb_app(X2,q))))))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4171,plain,(
% 104.76/13.69    sQ349_spl|~sQ24_spl|~sQ52_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4150,f4168,f401,f627])).
% 104.76/13.69  fof(f4176,definition,(
% 104.76/13.69    ![X0]: (sQ351_spl <=> (member(comb_app(combK,X0),comb)|~member(X0,comb)|ap_parcontractE_c2(comb_app(combK,X0),combS,X0)|ap_parcontractE_c3(comb_app(combK,X0),combS,X0)|ap_parcontractE_sk2s(comb_app(combK,X0),combS,X0)=combS))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ351_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4179,plain,(
% 104.76/13.69    sQ351_spl|~sQ3_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4153,f4176,f139])).
% 104.76/13.69  fof(f4180,definition,(
% 104.76/13.69    ![X0]: (sQ352_spl <=> (member(comb_app(combK,X0),comb)|~member(X0,comb)|ap_parcontractE_c2(comb_app(combK,X0),combK,X0)|ap_parcontractE_c3(comb_app(combK,X0),combK,X0)|ap_parcontractE_sk2s(comb_app(combK,X0),combK,X0)=combK))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4183,plain,(
% 104.76/13.69    sQ352_spl|~sQ1_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4154,f4180,f132])).
% 104.76/13.69  fof(f4190,plain,(
% 104.76/13.69    ![X0,X1]: (~member(X0,comb)|~member(X1,comb)|member(comb_app(X0,comb_app(combK,combS)),comb))),
% 104.76/13.69    inference(resolution,[status(thm)],[f174,f67])).
% 104.76/13.69  fof(f4197,definition,(
% 104.76/13.69    ![X0]: (sQ353_spl <=> (~member(X0,comb)|member(comb_app(X0,comb_app(combK,combS)),comb)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4200,plain,(
% 104.76/13.69    sQ353_spl|sQ4_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4190,f4197,f176])).
% 104.76/13.69  fof(f4225,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2s(X0,q,comb_app(X1,ap_parcontractE_sk2q(q,X3,comb_app(X4,X5)))))|~member(pair(p,X2),parcontract)|member(q,comb)|ap_parcontractE_c2(q,X3,comb_app(X4,X5))|ap_parcontractE_c3(q,X3,comb_app(X4,X5))|~member(pair(q,X4),parcontract)|~member(pair(X3,X5),parcontract)|~sQ337_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f4088,f2543])).
% 104.76/13.69  fof(f4231,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2s(X0,q,comb_app(X1,ap_parcontractE_sk2s(X3,q,comb_app(X4,X5)))))|~member(pair(p,X2),parcontract)|member(q,comb)|~member(pair(X3,X4),parcontract)|~member(pair(q,X5),parcontract)|~sQ337_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f4088,f2552])).
% 104.76/13.69  fof(f4234,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ355_spl <=> (~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2s(X0,q,comb_app(X1,ap_parcontractE_sk2q(q,X3,comb_app(X4,X5)))))|~member(pair(p,X2),parcontract)|ap_parcontractE_c2(q,X3,comb_app(X4,X5))|ap_parcontractE_c3(q,X3,comb_app(X4,X5))|~member(pair(q,X4),parcontract)|~member(pair(X3,X5),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4237,plain,(
% 104.76/13.69    sQ355_spl|sQ25_spl|~sQ337_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4225,f4234,f404,f4087])).
% 104.76/13.69  fof(f4254,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ360_spl <=> (~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2s(X0,q,comb_app(X1,ap_parcontractE_sk2s(X3,q,comb_app(X4,X5)))))|~member(pair(p,X2),parcontract)|~member(pair(X3,X4),parcontract)|~member(pair(q,X5),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4257,plain,(
% 104.76/13.69    sQ360_spl|sQ25_spl|~sQ337_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4231,f4254,f404,f4087])).
% 104.76/13.69  fof(f4370,plain,(
% 104.76/13.69    ![X0]: (~member(X0,comb)|member(comb_app(comb_app(combK,combS),combS),comb))),
% 104.76/13.69    inference(resolution,[status(thm)],[f169,f67])).
% 104.76/13.69  fof(f4376,definition,(
% 104.76/13.69    sQ361_spl <=> (member(comb_app(comb_app(combK,combS),combS),comb))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4379,plain,(
% 104.76/13.69    sQ4_spl|sQ361_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f4370,f176,f4376])).
% 104.76/13.69  fof(f4904,definition,(
% 104.76/13.69    sQ401_spl <=> (member(comb_app(comb_app(comb_app(combS,combS),combS),q),comb))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f4905,plain,(
% 104.76/13.69    member(comb_app(comb_app(comb_app(combS,combS),combS),q),comb)|~sQ401_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f4904])).
% 104.76/13.69  fof(f4906,plain,(
% 104.76/13.69    ~member(comb_app(comb_app(comb_app(combS,combS),combS),q),comb)|sQ401_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f4904])).
% 104.76/13.69  fof(f5187,definition,(
% 104.76/13.69    ![X0]: (sQ448_spl <=> (~ap_parcontractE_c1(comb_app(comb_app(combS,combS),combS),q,X0)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ448_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f5188,plain,(
% 104.76/13.69    ![X0]: (~ap_parcontractE_c1(comb_app(comb_app(combS,combS),combS),q,X0)|~sQ448_spl)),
% 104.76/13.69    inference(component_clause,[status(thm)],[f5187])).
% 104.76/13.69  fof(f5190,definition,(
% 104.76/13.69    sQ449_spl <=> (ap_parcontractE_c1(comb_app(comb_app(combS,combS),combS),q,comb_app(comb_app(combS,q),comb_app(combS,q))))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f5191,plain,(
% 104.76/13.69    ap_parcontractE_c1(comb_app(comb_app(combS,combS),combS),q,comb_app(comb_app(combS,q),comb_app(combS,q)))|~sQ449_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f5190])).
% 104.76/13.69  fof(f5627,plain,(
% 104.76/13.69    $false|~sQ448_spl|~sQ449_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f5191,f5188])).
% 104.76/13.69  fof(f5628,plain,(
% 104.76/13.69    ~sQ448_spl|~sQ449_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f5627])).
% 104.76/13.69  fof(f5631,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (member(X0,comb)|~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2q(q,X0,comb_app(ap_parcontractE_sk2q(q,X3,comb_app(X4,X5)),X1)))|~member(pair(p,X2),parcontract)|member(q,comb)|ap_parcontractE_c2(q,X3,comb_app(X4,X5))|ap_parcontractE_c3(q,X3,comb_app(X4,X5))|~member(pair(q,X4),parcontract)|~member(pair(X3,X5),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f4106,f2543])).
% 104.76/13.69  fof(f5637,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (member(X0,comb)|~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2q(q,X0,comb_app(ap_parcontractE_sk2s(X3,q,comb_app(X4,X5)),X1)))|~member(pair(p,X2),parcontract)|member(q,comb)|~member(pair(X3,X4),parcontract)|~member(pair(q,X5),parcontract))),
% 104.76/13.69    inference(resolution,[status(thm)],[f4106,f2552])).
% 104.76/13.69  fof(f5640,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ464_spl <=> (member(X0,comb)|~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2q(q,X0,comb_app(ap_parcontractE_sk2q(q,X3,comb_app(X4,X5)),X1)))|~member(pair(p,X2),parcontract)|ap_parcontractE_c2(q,X3,comb_app(X4,X5))|ap_parcontractE_c3(q,X3,comb_app(X4,X5))|~member(pair(q,X4),parcontract)|~member(pair(X3,X5),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f5643,plain,(
% 104.76/13.69    sQ464_spl|sQ25_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f5631,f5640,f404])).
% 104.76/13.69  fof(f5660,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4,X5]: (sQ469_spl <=> (member(X0,comb)|~member(pair(X0,X1),parcontract)|~r=comb_app(comb_app(combS,X2),ap_parcontractE_sk2q(q,X0,comb_app(ap_parcontractE_sk2s(X3,q,comb_app(X4,X5)),X1)))|~member(pair(p,X2),parcontract)|~member(pair(X3,X4),parcontract)|~member(pair(q,X5),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f5663,plain,(
% 104.76/13.69    sQ469_spl|sQ25_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f5637,f5660,f404])).
% 104.76/13.69  fof(f5908,definition,(
% 104.76/13.69    sQ480_spl <=> (combS=comb_app(combK,comb_app(combS,combS)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f5909,plain,(
% 104.76/13.69    combS=comb_app(combK,comb_app(combS,combS))|~sQ480_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f5908])).
% 104.76/13.69  fof(f5917,plain,(
% 104.76/13.69    $false|~sQ480_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f5909,f58])).
% 104.76/13.69  fof(f5918,plain,(
% 104.76/13.69    ~sQ480_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f5917])).
% 104.76/13.69  fof(f6011,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (ap_parcontractE_c3(X0,q,comb_app(X1,X2))|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|comb_app(X1,X2)=comb_app(X0,q)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract)|member(q,comb))),
% 104.76/13.69    inference(resolution,[status(thm)],[f985,f114])).
% 104.76/13.69  fof(f6014,definition,(
% 104.76/13.69    ![X0,X1,X2,X3]: (sQ488_spl <=> (ap_parcontractE_c3(X0,q,comb_app(X1,X2))|~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|comb_app(X1,X2)=comb_app(X0,q)|~r=comb_app(comb_app(combS,X3),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(pair(p,X3),parcontract)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ488_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f6017,plain,(
% 104.76/13.69    sQ488_spl|sQ25_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f6011,f6014,f404])).
% 104.76/13.69  fof(f6034,plain,(
% 104.76/13.69    ![X0]: (~ap_parcontractE_c1(comb_app(comb_app(combS,combS),combS),q,X0)|sQ401_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f4906,f109])).
% 104.76/13.69  fof(f6036,plain,(
% 104.76/13.69    sQ448_spl|sQ401_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f6034,f5187,f4904])).
% 104.76/13.69  fof(f6075,plain,(
% 104.76/13.69    member(q,comb)|~sQ401_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f4905,f67])).
% 104.76/13.69  fof(f6366,plain,(
% 104.76/13.69    member(pair(p,p),parcontract)|~sQ29_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f2699,f97])).
% 104.76/13.69  fof(f6444,plain,(
% 104.76/13.69    ~r=comb_app(comb_app(combS,p),q)|~sQ29_spl|~sQ25_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f6366,f2708])).
% 104.76/13.69  fof(f6447,plain,(
% 104.76/13.69    ~r=r|~sQ14_spl|~sQ29_spl|~sQ25_spl),
% 104.76/13.69    inference(forward_demodulation,[status(thm)],[f261,f6444])).
% 104.76/13.69  fof(f6448,plain,(
% 104.76/13.69    $false|~sQ14_spl|~sQ29_spl|~sQ25_spl),
% 104.76/13.69    inference(trivial_equality_resolution,[status(thm)],[f6447])).
% 104.76/13.69  fof(f6449,plain,(
% 104.76/13.69    ~sQ14_spl|~sQ29_spl|~sQ25_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f6448])).
% 104.76/13.69  fof(f6452,plain,(
% 104.76/13.69    sQ25_spl|~sQ401_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f6075,f404,f4904])).
% 104.76/13.69  fof(f6823,plain,(
% 104.76/13.69    r=comb_app(ap_parcontractE_sk2q(comb_app(combS,p),q,r),ap_parcontractE_sk2s(comb_app(combS,p),q,r))|~sQ17_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f251,f125])).
% 104.76/13.69  fof(f6827,plain,(
% 104.76/13.69    ![X0]: (~r=comb_app(comb_app(combS,X0),ap_parcontractE_sk2s(comb_app(combS,p),q,r))|~member(pair(p,X0),parcontract)|~sQ17_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f257,f128])).
% 104.76/13.69  fof(f7556,definition,(
% 104.76/13.69    sQ688_spl <=> (member(pair(combK,ap_contractE_sk3q(r,combK,comb_app(comb_app(p,combK),comb_app(q,combK)))),contract))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ688_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f7557,plain,(
% 104.76/13.69    member(pair(combK,ap_contractE_sk3q(r,combK,comb_app(comb_app(p,combK),comb_app(q,combK)))),contract)|~sQ688_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f7556])).
% 104.76/13.69  fof(f7628,definition,(
% 104.76/13.69    sQ710_spl <=> (member(pair(combS,ap_contractE_sk3q(r,combS,comb_app(comb_app(p,combS),comb_app(q,combS)))),contract))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ710_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f7629,plain,(
% 104.76/13.69    member(pair(combS,ap_contractE_sk3q(r,combS,comb_app(comb_app(p,combS),comb_app(q,combS)))),contract)|~sQ710_spl),
% 104.76/13.69    inference(component_clause,[status(thm)],[f7628])).
% 104.76/13.69  fof(f7632,plain,(
% 104.76/13.69    $false|~sQ710_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f7629,f96])).
% 104.76/13.69  fof(f7633,plain,(
% 104.76/13.69    ~sQ710_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f7632])).
% 104.76/13.69  fof(f7634,plain,(
% 104.76/13.69    $false|~sQ688_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f7557,f95])).
% 104.76/13.69  fof(f7635,plain,(
% 104.76/13.69    ~sQ688_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f7634])).
% 104.76/13.69  fof(f7642,plain,(
% 104.76/13.69    ~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))|~sQ17_spl|~sQ21_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f6827,f581])).
% 104.76/13.69  fof(f7653,plain,(
% 104.76/13.69    ~r=comb_app(ap_parcontractE_sk2q(comb_app(combS,p),q,r),ap_parcontractE_sk2s(comb_app(combS,p),q,r))|~sQ17_spl|~sQ21_spl),
% 104.76/13.69    inference(forward_demodulation,[status(thm)],[f2891,f7642])).
% 104.76/13.69  fof(f7654,plain,(
% 104.76/13.69    ~r=r|~sQ17_spl|~sQ21_spl),
% 104.76/13.69    inference(forward_demodulation,[status(thm)],[f6823,f7653])).
% 104.76/13.69  fof(f7655,plain,(
% 104.76/13.69    $false|~sQ17_spl|~sQ21_spl),
% 104.76/13.69    inference(trivial_equality_resolution,[status(thm)],[f7654])).
% 104.76/13.69  fof(f7656,plain,(
% 104.76/13.69    ~sQ17_spl|~sQ21_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f7655])).
% 104.76/13.69  fof(f7681,plain,(
% 104.76/13.69    $false|~sQ19_spl),
% 104.76/13.69    inference(forward_subsumption_resolution,[status(thm)],[f585,f58])).
% 104.76/13.69  fof(f7682,plain,(
% 104.76/13.69    ~sQ19_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f7681])).
% 104.76/13.69  fof(f7683,plain,(
% 104.76/13.69    r=comb_app(comb_app(combS,p),ap_parcontractE_sk2s(comb_app(combS,p),q,r))|~sQ18_spl|~sQ17_spl),
% 104.76/13.69    inference(backward_demodulation,[status(thm)],[f545,f6823])).
% 104.76/13.69  fof(f7945,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X3),p,X3)),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|member(comb_app(combK,X3),comb)|~member(X3,comb)|~member(p,comb)|ap_parcontractE_c2(comb_app(combK,X3),p,X3)|ap_parcontractE_c3(comb_app(combK,X3),p,X3)|~sQ337_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f4088,f2630])).
% 104.76/13.69  fof(f7946,plain,(
% 104.76/13.69    ![X0,X1,X2,X3]: (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X3),p,X3)),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(X3,comb)|~member(p,comb)|ap_parcontractE_c2(comb_app(combK,X3),p,X3)|ap_parcontractE_c3(comb_app(combK,X3),p,X3)|X3=comb_app(comb_app(combK,X3),p)|~sQ337_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f4088,f1081])).
% 104.76/13.69  fof(f7947,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|member(comb_app(comb_app(combS,X3),X4),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|~member(X3,comb)|~member(X4,comb)|~member(p,comb)|~sQ337_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f4088,f2374])).
% 104.76/13.69  fof(f7948,plain,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|~member(X3,comb)|~member(X4,comb)|~member(p,comb)|comb_app(comb_app(X3,p),comb_app(X4,p))=comb_app(comb_app(comb_app(combS,X3),X4),p)|~sQ337_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f4088,f367])).
% 104.76/13.69  fof(f7956,definition,(
% 104.76/13.69    ![X0,X1,X2,X3]: (sQ718_spl <=> (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X3),p,X3)),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|member(comb_app(combK,X3),comb)|~member(X3,comb)|ap_parcontractE_c2(comb_app(combK,X3),p,X3)|ap_parcontractE_c3(comb_app(combK,X3),p,X3)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ718_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f7959,plain,(
% 104.76/13.69    sQ718_spl|~sQ24_spl|~sQ337_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f7945,f7956,f401,f4087])).
% 104.76/13.69  fof(f7960,definition,(
% 104.76/13.69    ![X0,X1,X2,X3]: (sQ719_spl <=> (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(combK,X3),p,X3)),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|~member(X3,comb)|ap_parcontractE_c2(comb_app(combK,X3),p,X3)|ap_parcontractE_c3(comb_app(combK,X3),p,X3)|X3=comb_app(comb_app(combK,X3),p)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ719_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f7963,plain,(
% 104.76/13.69    sQ719_spl|~sQ24_spl|~sQ337_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f7946,f7960,f401,f4087])).
% 104.76/13.69  fof(f7964,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (sQ720_spl <=> (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|member(comb_app(comb_app(combS,X3),X4),comb)|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|~member(X3,comb)|~member(X4,comb)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ720_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f7967,plain,(
% 104.76/13.69    sQ720_spl|~sQ24_spl|~sQ337_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f7947,f7964,f401,f4087])).
% 104.76/13.69  fof(f7968,definition,(
% 104.76/13.69    ![X0,X1,X2,X3,X4]: (sQ721_spl <=> (~member(pair(X0,X1),parcontract)|~member(pair(q,X2),parcontract)|~r=comb_app(comb_app(combS,ap_parcontractE_sk2s(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))),ap_parcontractE_sk2s(X0,q,comb_app(X1,X2)))|ap_parcontractE_c2(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|ap_parcontractE_c3(comb_app(comb_app(combS,X3),X4),p,comb_app(comb_app(X3,p),comb_app(X4,p)))|~member(X3,comb)|~member(X4,comb)|comb_app(comb_app(X3,p),comb_app(X4,p))=comb_app(comb_app(comb_app(combS,X3),X4),p)))),
% 104.76/13.69    introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition])).
% 104.76/13.69  fof(f7971,plain,(
% 104.76/13.69    sQ721_spl|~sQ24_spl|~sQ337_spl),
% 104.76/13.69    inference(split_clause,[status(thm)],[f7948,f7968,f401,f4087])).
% 104.76/13.69  fof(f7977,plain,(
% 104.76/13.69    ~r=comb_app(comb_app(combS,p),ap_parcontractE_sk2s(comb_app(combS,p),q,r))|~sQ29_spl|~sQ17_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f6366,f6827])).
% 104.76/13.69  fof(f7979,plain,(
% 104.76/13.69    ~r=r|~sQ18_spl|~sQ29_spl|~sQ17_spl),
% 104.76/13.69    inference(forward_demodulation,[status(thm)],[f7683,f7977])).
% 104.76/13.69  fof(f7980,plain,(
% 104.76/13.69    $false|~sQ18_spl|~sQ29_spl|~sQ17_spl),
% 104.76/13.69    inference(trivial_equality_resolution,[status(thm)],[f7979])).
% 104.76/13.69  fof(f7981,plain,(
% 104.76/13.69    ~sQ18_spl|~sQ29_spl|~sQ17_spl),
% 104.76/13.69    inference(contradiction_clause,[status(thm)],[f7980])).
% 104.76/13.69  fof(f8915,plain,(
% 104.76/13.69    ![X0]: (~ap_parcontractE_c1(combS,p,X0)|sQ29_spl)),
% 104.76/13.69    inference(resolution,[status(thm)],[f424,f109])).
% 104.76/13.69  fof(f8916,plain,(
% 104.76/13.69    ~member(combS,comb)|~member(p,comb)|sQ29_spl),
% 104.76/13.69    inference(resolution,[status(thm)],[f424,f70])).
% 104.76/13.69  fof(f8917,plain,(
% 104.76/13.69    $false|sQ29_spl|~sQ18_spl),
% 6.97/13.97    inference(backward_subsumption_resolution,[status(thm)],[f546,f8915])).
% 6.97/13.97  fof(f8918,plain,(
% 6.97/13.97    ~sQ3_spl|~sQ24_spl|sQ29_spl),
% 6.97/13.97    inference(split_clause,[status(thm)],[f8916,f139,f401,f422])).
% 6.97/13.97  fof(f8919,plain,(
% 6.97/13.97    sQ29_spl|~sQ18_spl),
% 6.97/13.97    inference(contradiction_clause,[status(thm)],[f8917])).
% 6.97/13.97  fof(f9308,definition,(
% 6.97/13.97    sQ834_spl <=> (member(pair(combK,ap_contractE_sk3q(r,combK,comb_app(comb_app(p,combK),comb_app(ap_parcontractE_sk2s(comb_app(combS,p),q,r),combK)))),contract))),
% 6.97/13.97    introduced(definition,[new_symbols(definition,[sQ834_spl])],[split_symbol_definition])).
% 6.97/13.97  fof(f9309,plain,(
% 6.97/13.97    member(pair(combK,ap_contractE_sk3q(r,combK,comb_app(comb_app(p,combK),comb_app(ap_parcontractE_sk2s(comb_app(combS,p),q,r),combK)))),contract)|~sQ834_spl),
% 6.97/13.97    inference(component_clause,[status(thm)],[f9308])).
% 6.97/13.97  fof(f9399,definition,(
% 6.97/13.97    sQ862_spl <=> (member(pair(combS,ap_contractE_sk3q(r,combS,comb_app(comb_app(p,combS),comb_app(ap_parcontractE_sk2s(comb_app(combS,p),q,r),combS)))),contract))),
% 6.97/13.97    introduced(definition,[new_symbols(definition,[sQ862_spl])],[split_symbol_definition])).
% 6.97/13.97  fof(f9400,plain,(
% 6.97/13.97    member(pair(combS,ap_contractE_sk3q(r,combS,comb_app(comb_app(p,combS),comb_app(ap_parcontractE_sk2s(comb_app(combS,p),q,r),combS)))),contract)|~sQ862_spl),
% 6.97/13.97    inference(component_clause,[status(thm)],[f9399])).
% 6.97/13.97  fof(f9403,plain,(
% 6.97/13.97    $false|~sQ862_spl),
% 6.97/13.97    inference(forward_subsumption_resolution,[status(thm)],[f9400,f96])).
% 6.97/13.97  fof(f9404,plain,(
% 6.97/13.97    ~sQ862_spl),
% 6.97/13.97    inference(contradiction_clause,[status(thm)],[f9403])).
% 6.97/13.97  fof(f9405,plain,(
% 6.97/13.97    $false|~sQ834_spl),
% 6.97/13.97    inference(forward_subsumption_resolution,[status(thm)],[f9309,f95])).
% 6.97/13.97  fof(f9406,plain,(
% 6.97/13.97    ~sQ834_spl),
% 6.97/13.97    inference(contradiction_clause,[status(thm)],[f9405])).
% 6.97/13.97  fof(f9452,plain,(
% 6.97/13.97    $false|~sQ140_spl),
% 6.97/13.97    inference(forward_subsumption_resolution,[status(thm)],[f2413,f58])).
% 6.97/13.97  fof(f9453,plain,(
% 6.97/13.97    ~sQ140_spl),
% 6.97/13.97    inference(contradiction_clause,[status(thm)],[f9452])).
% 6.97/13.97  fof(f9461,plain,(
% 6.97/13.97    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)))|~sQ20_spl),
% 6.97/13.97    inference(resolution,[status(thm)],[f296,f122])).
% 6.97/13.97  fof(f9462,plain,(
% 6.97/13.97    $false|~sQ20_spl),
% 6.97/13.97    inference(forward_subsumption_resolution,[status(thm)],[f9461,f58])).
% 6.97/13.97  fof(f9463,plain,(
% 6.97/13.97    ~sQ20_spl),
% 6.97/13.97    inference(contradiction_clause,[status(thm)],[f9462])).
% 6.97/13.97  fof(f9464,plain,(
% 6.97/13.97    $false),
% 6.97/13.97    inference(sat_refutation,[status(thm)],[f135,f142,f147,f150,f182,f203,f253,f287,f301,f333,f339,f353,f363,f441,f442,f520,f531,f567,f570,f630,f634,f638,f719,f1210,f1214,f1221,f1225,f1271,f1275,f1279,f1283,f1287,f1291,f1335,f1339,f1355,f1359,f1360,f1361,f1364,f1380,f1384,f1394,f1398,f2479,f2483,f2517,f2521,f2526,f2628,f2652,f2664,f2668,f2702,f2710,f2751,f2774,f2778,f2787,f2791,f2804,f2806,f2825,f2827,f3028,f3032,f3036,f3052,f3056,f3812,f3816,f3820,f4023,f4086,f4090,f4171,f4179,f4183,f4200,f4237,f4257,f4379,f5628,f5643,f5663,f5918,f6017,f6036,f6449,f6452,f7633,f7635,f7656,f7682,f7959,f7963,f7967,f7971,f7981,f8918,f8919,f9404,f9406,f9453,f9463])).
% 6.97/13.97  % SZS output end CNFRefutation for theBenchmark.p
% 6.97/13.97  % Elapsed time: 13.604107 seconds
% 6.97/13.97  % CPU time: 106.278439 seconds
% 6.97/13.97  % Total memory used: 1.360 GB
% 6.97/13.97  % Net memory used: 1.222 GB
%------------------------------------------------------------------------------