%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COL094-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:37:56 AM UTC 2026
% Result : Unsatisfiable 11.92s 2.39s
% Output : Refutation 12.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 43
% Syntax : Number of formulae : 241 ( 35 unt; 25 def)
% Number of atoms : 617 ( 113 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 649 ( 273 ~; 355 |; 0 &)
% ( 21 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 22 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 159 ( 0 sgn 159 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f157,axiom,
combK != combS,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',k_s) ).
fof(f159,axiom,
! [X0,X1] : combS != comb_app(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s_app) ).
fof(f160,axiom,
! [X2,X3,X0,X1] :
( comb_app(X0,X1) != comb_app(X2,X3)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',app_app1) ).
fof(f161,axiom,
! [X2,X3,X0,X1] :
( comb_app(X0,X1) != comb_app(X2,X3)
| X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',app_app2) ).
fof(f163,axiom,
! [X0,X1] :
( ~ member(comb_app(X0,X1),comb)
| member(X0,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_E1) ).
fof(f164,axiom,
! [X0,X1] :
( ~ member(comb_app(X0,X1),comb)
| member(X1,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_E2) ).
fof(f193,axiom,
! [X0] :
( member(pair(X0,X0),parcontract)
| ~ member(X0,comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',parcontract_intros1) ).
fof(f201,axiom,
! [X0] :
( ~ member(pair(combS,X0),parcontract)
| X0 = combS ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s_parcontractE2) ).
fof(f202,plain,
! [X0] :
( ~ member(pair(combS,X0),parcontract)
| combS = X0 ),
inference(reorient_equations,[],[f201]) ).
fof(f203,axiom,
! [X2,X0,X1] :
( ~ 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE1) ).
fof(f204,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c1(X0,X1,X2)
| member(comb_app(X0,X1),comb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE2) ).
fof(f205,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c1(X0,X1,X2)
| X2 = comb_app(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE3) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c1(X0,X1,X2)
| comb_app(X0,X1) = X2 ),
inference(reorient_equations,[],[f205]) ).
fof(f209,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c2(X0,X1,X2)
| X0 = comb_app(combK,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE6) ).
fof(f210,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c2(X0,X1,X2)
| comb_app(combK,X2) = X0 ),
inference(reorient_equations,[],[f209]) ).
fof(f216,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c3(X0,X1,X2)
| X0 = comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,X2)),ap_parcontractE_sk1q(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE11) ).
fof(f217,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c3(X0,X1,X2)
| comb_app(comb_app(combS,ap_parcontractE_sk1p(X0,X1,X2)),ap_parcontractE_sk1q(X0,X1,X2)) = X0 ),
inference(reorient_equations,[],[f216]) ).
fof(f218,axiom,
! [X2,X0,X1] :
( member(pair(X0,ap_parcontractE_sk2q(X0,X1,X2)),parcontract)
| ~ ap_parcontractE_c4(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE12) ).
fof(f219,axiom,
! [X2,X0,X1] :
( member(pair(X1,ap_parcontractE_sk2s(X0,X1,X2)),parcontract)
| ~ ap_parcontractE_c4(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE13) ).
fof(f220,axiom,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(X0,X1,X2)
| X2 = comb_app(ap_parcontractE_sk2q(X0,X1,X2),ap_parcontractE_sk2s(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_parcontractE14) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(X0,X1,X2)
| comb_app(ap_parcontractE_sk2q(X0,X1,X2),ap_parcontractE_sk2s(X0,X1,X2)) = X2 ),
inference(reorient_equations,[],[f220]) ).
fof(f222,axiom,
member(pair(comb_app(comb_app(combS,p),q),r),parcontract),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_parcontractD_h1) ).
fof(f223,negated_conjecture,
! [X0,X1] :
( r != comb_app(comb_app(combS,X0),X1)
| ~ member(pair(p,X0),parcontract)
| ~ member(pair(q,X1),parcontract) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_parcontractD_c1) ).
fof(f224,plain,
! [X0,X1] :
( comb_app(comb_app(combS,X0),X1) != r
| ~ member(pair(p,X0),parcontract)
| ~ member(pair(q,X1),parcontract) ),
inference(reorient_equations,[],[f223]) ).
fof(f235,definition,
! [X0] : sF0(X0) = comb_app(combS,X0),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f236,plain,
! [X0] : comb_app(combS,X0) = sF0(X0),
inference(reorient_equations,[],[f235]) ).
fof(f237,definition,
! [X0,X1] : sF1(X0,X1) = comb_app(sF0(X0),X1),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f238,plain,
! [X0,X1] : comb_app(sF0(X0),X1) = sF1(X0,X1),
inference(reorient_equations,[],[f237]) ).
fof(f239,definition,
! [X0] : sF2(X0) = pair(p,X0),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f240,plain,
! [X0] : pair(p,X0) = sF2(X0),
inference(reorient_equations,[],[f239]) ).
fof(f241,definition,
! [X1] : sF3(X1) = pair(q,X1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f242,plain,
! [X1] : pair(q,X1) = sF3(X1),
inference(reorient_equations,[],[f241]) ).
fof(f243,plain,
! [X0,X1] :
( r != sF1(X0,X1)
| ~ member(sF2(X0),parcontract)
| ~ member(sF3(X1),parcontract) ),
inference(definition_folding,[],[f224,f242,f240,f238,f236]) ).
fof(f262,plain,
! [X0,X1] :
( member(sF2(ap_parcontractE_sk2s(X0,p,X1)),parcontract)
| ~ ap_parcontractE_c4(X0,p,X1) ),
inference(superposition,[],[f219,f240]) ).
fof(f263,plain,
! [X0,X1] :
( member(sF3(ap_parcontractE_sk2s(X0,q,X1)),parcontract)
| ~ ap_parcontractE_c4(X0,q,X1) ),
inference(superposition,[],[f219,f242]) ).
fof(f266,plain,
( member(sF2(p),parcontract)
| ~ member(p,comb) ),
inference(superposition,[],[f193,f240]) ).
fof(f267,plain,
( member(sF3(q),parcontract)
| ~ member(q,comb) ),
inference(superposition,[],[f193,f242]) ).
fof(f269,definition,
( spl4_5
<=> member(q,comb) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f271,plain,
( ~ member(q,comb)
| spl4_5 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl4_6
<=> member(sF3(q),parcontract) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f276,plain,
( ~ spl4_5
| spl4_6 ),
inference(avatar_split_clause,[],[f267,f273,f269]) ).
fof(f278,definition,
( spl4_7
<=> member(p,comb) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f280,plain,
( ~ member(p,comb)
| spl4_7 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f282,definition,
( spl4_8
<=> member(sF2(p),parcontract) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f283,plain,
( ~ member(sF2(p),parcontract)
| spl4_8 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f284,plain,
( member(sF2(p),parcontract)
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,plain,
( ~ spl4_7
| spl4_8 ),
inference(avatar_split_clause,[],[f266,f282,f278]) ).
fof(f288,plain,
! [X0,X1] :
( ~ member(sF1(X0,X1),comb)
| member(sF0(X0),comb) ),
inference(superposition,[],[f163,f238]) ).
fof(f290,plain,
! [X0,X1] :
( ~ member(sF1(X0,X1),comb)
| member(X1,comb) ),
inference(superposition,[],[f164,f238]) ).
fof(f291,plain,
! [X0] :
( ~ member(sF0(X0),comb)
| member(X0,comb) ),
inference(superposition,[],[f164,f236]) ).
fof(f292,plain,
( 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) ),
inference(resolution,[],[f203,f222]) ).
fof(f294,plain,
! [X2,X3,X0,X1] :
( ap_parcontractE_c1(X0,X1,ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3))
| ap_parcontractE_c2(X0,X1,ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3))
| ap_parcontractE_c3(X0,X1,ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3))
| ap_parcontractE_c4(X0,X1,ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3))
| ~ ap_parcontractE_c4(comb_app(X0,X1),X2,X3) ),
inference(resolution,[],[f203,f218]) ).
fof(f298,plain,
( ap_parcontractE_c1(sF0(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) ),
inference(forward_demodulation,[],[f292,f236]) ).
fof(f299,plain,
( ap_parcontractE_c2(sF0(p),q,r)
| ap_parcontractE_c1(sF0(p),q,r)
| ap_parcontractE_c3(comb_app(combS,p),q,r)
| ap_parcontractE_c4(comb_app(combS,p),q,r) ),
inference(forward_demodulation,[],[f298,f236]) ).
fof(f300,plain,
( ap_parcontractE_c3(sF0(p),q,r)
| ap_parcontractE_c2(sF0(p),q,r)
| ap_parcontractE_c1(sF0(p),q,r)
| ap_parcontractE_c4(comb_app(combS,p),q,r) ),
inference(forward_demodulation,[],[f299,f236]) ).
fof(f301,plain,
( ap_parcontractE_c4(sF0(p),q,r)
| ap_parcontractE_c3(sF0(p),q,r)
| ap_parcontractE_c2(sF0(p),q,r)
| ap_parcontractE_c1(sF0(p),q,r) ),
inference(forward_demodulation,[],[f300,f236]) ).
fof(f303,definition,
( spl4_9
<=> ap_parcontractE_c1(sF0(p),q,r) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f305,plain,
( ap_parcontractE_c1(sF0(p),q,r)
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl4_10
<=> ap_parcontractE_c2(sF0(p),q,r) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f309,plain,
( ap_parcontractE_c2(sF0(p),q,r)
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f311,definition,
( spl4_11
<=> ap_parcontractE_c3(sF0(p),q,r) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f313,plain,
( ap_parcontractE_c3(sF0(p),q,r)
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl4_12
<=> ap_parcontractE_c4(sF0(p),q,r) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f317,plain,
( ap_parcontractE_c4(sF0(p),q,r)
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
( spl4_9
| spl4_10
| spl4_11
| spl4_12 ),
inference(avatar_split_clause,[],[f301,f315,f311,f307,f303]) ).
fof(f319,plain,
( r = comb_app(sF0(p),q)
| ~ spl4_9 ),
inference(resolution,[],[f305,f206]) ).
fof(f320,plain,
( r = sF1(p,q)
| ~ spl4_9 ),
inference(forward_demodulation,[],[f319,f238]) ).
fof(f321,plain,
( r != r
| ~ member(sF2(p),parcontract)
| ~ member(sF3(q),parcontract)
| ~ spl4_9 ),
inference(superposition,[],[f243,f320]) ).
fof(f322,plain,
( ~ member(sF2(p),parcontract)
| ~ member(sF3(q),parcontract)
| ~ spl4_9 ),
inference(trivial_inequality_removal,[],[f321]) ).
fof(f323,plain,
( ~ spl4_6
| ~ spl4_8
| ~ spl4_9 ),
inference(avatar_split_clause,[],[f322,f303,f282,f273]) ).
fof(f325,plain,
! [X0] : combS != sF0(X0),
inference(superposition,[],[f159,f236]) ).
fof(f326,plain,
( member(comb_app(sF0(p),q),comb)
| ~ spl4_9 ),
inference(resolution,[],[f204,f305]) ).
fof(f327,plain,
( member(sF1(p,q),comb)
| ~ spl4_9 ),
inference(forward_demodulation,[],[f326,f238]) ).
fof(f328,plain,
( member(r,comb)
| ~ spl4_9 ),
inference(forward_demodulation,[],[f327,f320]) ).
fof(f332,plain,
! [X2,X0,X1] :
( comb_app(X1,X2) != sF0(X0)
| X0 = X2 ),
inference(superposition,[],[f161,f236]) ).
fof(f337,plain,
! [X2,X0,X1] :
( comb_app(X1,X2) != sF0(X0)
| combS = X1 ),
inference(superposition,[],[f160,f236]) ).
fof(f346,plain,
! [X2,X3,X0,X1] :
( ap_parcontractE_c4(X0,X1,ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3))
| ap_parcontractE_c3(X0,X1,ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3))
| ap_parcontractE_c2(X0,X1,ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3))
| ~ ap_parcontractE_c4(comb_app(X0,X1),X2,X3)
| comb_app(X0,X1) = ap_parcontractE_sk2q(comb_app(X0,X1),X2,X3) ),
inference(resolution,[],[f294,f206]) ).
fof(f348,plain,
! [X2,X0,X1] :
( ap_parcontractE_c1(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c4(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ~ ap_parcontractE_c4(sF0(X0),X1,X2) ),
inference(superposition,[],[f294,f236]) ).
fof(f394,plain,
! [X0,X1] :
( ~ ap_parcontractE_c4(combS,X0,X1)
| combS = ap_parcontractE_sk2q(combS,X0,X1) ),
inference(resolution,[],[f202,f218]) ).
fof(f398,plain,
! [X2,X0,X1] :
( sF1(X0,X1) != sF0(X2)
| combS = sF0(X0) ),
inference(superposition,[],[f337,f238]) ).
fof(f399,plain,
! [X2,X0,X1] : sF1(X0,X1) != sF0(X2),
inference(forward_subsumption_resolution,[],[f398,f325]) ).
fof(f402,plain,
! [X2,X0,X1] :
( ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2))
| ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2))
| ~ ap_parcontractE_c4(comb_app(combS,X0),X1,X2)
| comb_app(combS,X0) = ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)) ),
inference(resolution,[],[f346,f394]) ).
fof(f404,plain,
! [X2,X0,X1] :
( ap_parcontractE_c4(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2) ),
inference(superposition,[],[f346,f236]) ).
fof(f405,plain,
! [X2,X0,X1] :
( ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2))
| ~ ap_parcontractE_c4(comb_app(combS,X0),X1,X2)
| comb_app(combS,X0) = ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)) ),
inference(forward_demodulation,[],[f402,f236]) ).
fof(f406,plain,
! [X2,X0,X1] :
( ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ~ ap_parcontractE_c4(comb_app(combS,X0),X1,X2)
| comb_app(combS,X0) = ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)) ),
inference(forward_demodulation,[],[f405,f236]) ).
fof(f407,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| comb_app(combS,X0) = ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)) ),
inference(forward_demodulation,[],[f406,f236]) ).
fof(f408,plain,
! [X2,X0,X1] :
( sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(comb_app(combS,X0),X1,X2)) ),
inference(forward_demodulation,[],[f407,f236]) ).
fof(f409,plain,
! [X2,X0,X1] :
( ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)) ),
inference(forward_demodulation,[],[f408,f236]) ).
fof(f428,plain,
! [X2,X0,X1] :
( sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| combS = comb_app(combK,ap_parcontractE_sk2q(sF0(X0),X1,X2)) ),
inference(resolution,[],[f409,f210]) ).
fof(f429,plain,
! [X2,X0,X1] :
( ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2) ),
inference(forward_subsumption_resolution,[],[f428,f159]) ).
fof(f430,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))),ap_parcontractE_sk1q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))) ),
inference(resolution,[],[f429,f217]) ).
fof(f431,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| combS = ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2) ),
inference(forward_subsumption_resolution,[],[f430,f159]) ).
fof(f500,plain,
( ~ member(r,comb)
| member(q,comb)
| ~ spl4_9 ),
inference(superposition,[],[f290,f320]) ).
fof(f503,plain,
( member(q,comb)
| ~ spl4_9 ),
inference(forward_subsumption_resolution,[],[f500,f328]) ).
fof(f506,plain,
( $false
| spl4_5
| ~ spl4_9 ),
inference(forward_subsumption_resolution,[],[f503,f271]) ).
fof(f507,plain,
( spl4_5
| ~ spl4_9 ),
inference(avatar_contradiction_clause,[],[f506]) ).
fof(f531,definition,
( spl4_15
<=> member(sF0(p),comb) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f532,plain,
( ~ member(sF0(p),comb)
| spl4_15 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f533,plain,
( member(sF0(p),comb)
| ~ spl4_15 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f543,definition,
( spl4_17
<=> member(r,comb) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f545,plain,
( member(r,comb)
| ~ spl4_17 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f566,plain,
( sF0(p) = comb_app(combK,r)
| ~ spl4_10 ),
inference(resolution,[],[f309,f210]) ).
fof(f581,plain,
( ! [X0] :
( sF0(X0) != sF0(p)
| combK = combS )
| ~ spl4_10 ),
inference(superposition,[],[f337,f566]) ).
fof(f587,plain,
( ! [X0] : sF0(X0) != sF0(p)
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f581,f157]) ).
fof(f605,plain,
( $false
| ~ spl4_10 ),
inference(equality_resolution,[],[f587]) ).
fof(f606,plain,
~ spl4_10,
inference(avatar_contradiction_clause,[],[f605]) ).
fof(f609,plain,
( sF0(p) = comb_app(comb_app(combS,ap_parcontractE_sk1p(sF0(p),q,r)),ap_parcontractE_sk1q(sF0(p),q,r))
| ~ spl4_11 ),
inference(resolution,[],[f313,f217]) ).
fof(f610,plain,
( sF0(p) = comb_app(sF0(ap_parcontractE_sk1p(sF0(p),q,r)),ap_parcontractE_sk1q(sF0(p),q,r))
| ~ spl4_11 ),
inference(forward_demodulation,[],[f609,f236]) ).
fof(f611,plain,
( sF0(p) = sF1(ap_parcontractE_sk1p(sF0(p),q,r),ap_parcontractE_sk1q(sF0(p),q,r))
| ~ spl4_11 ),
inference(forward_demodulation,[],[f610,f238]) ).
fof(f612,plain,
( $false
| ~ spl4_11 ),
inference(forward_subsumption_resolution,[],[f611,f399]) ).
fof(f613,plain,
~ spl4_11,
inference(avatar_contradiction_clause,[],[f612]) ).
fof(f614,plain,
( combS = ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| sF0(p) = ap_parcontractE_sk2q(sF0(p),q,r)
| ~ spl4_12 ),
inference(resolution,[],[f317,f431]) ).
fof(f617,definition,
( spl4_21
<=> sF0(p) = ap_parcontractE_sk2q(sF0(p),q,r) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f618,plain,
( sF0(p) != ap_parcontractE_sk2q(sF0(p),q,r)
| spl4_21 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f619,plain,
( sF0(p) = ap_parcontractE_sk2q(sF0(p),q,r)
| ~ spl4_21 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f621,definition,
( spl4_22
<=> combS = ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)) ),
introduced(definition,[new_symbols(definition,[spl4_22])],[avatar_definition]) ).
fof(f623,plain,
( combS = ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ~ spl4_22 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f624,plain,
( spl4_21
| spl4_22
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f614,f315,f621,f617]) ).
fof(f625,plain,
( spl4_17
| ~ spl4_9 ),
inference(avatar_split_clause,[],[f328,f303,f543]) ).
fof(f754,plain,
( ~ member(r,comb)
| member(sF0(p),comb)
| ~ spl4_9 ),
inference(superposition,[],[f288,f320]) ).
fof(f755,plain,
( member(sF0(p),comb)
| ~ spl4_9
| ~ spl4_17 ),
inference(forward_subsumption_resolution,[],[f754,f545]) ).
fof(f756,plain,
( $false
| ~ spl4_9
| spl4_15
| ~ spl4_17 ),
inference(forward_subsumption_resolution,[],[f755,f532]) ).
fof(f757,plain,
( ~ spl4_9
| spl4_15
| ~ spl4_17 ),
inference(avatar_contradiction_clause,[],[f756]) ).
fof(f760,plain,
( r = comb_app(ap_parcontractE_sk2q(sF0(p),q,r),ap_parcontractE_sk2s(sF0(p),q,r))
| ~ spl4_12 ),
inference(resolution,[],[f317,f221]) ).
fof(f1483,plain,
! [X2,X0,X1] :
( ap_parcontractE_c2(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ap_parcontractE_sk2q(sF0(X0),X1,X2) = comb_app(ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)),ap_parcontractE_sk2s(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))) ),
inference(resolution,[],[f404,f221]) ).
fof(f2582,definition,
( spl4_210
<=> member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract) ),
introduced(definition,[new_symbols(definition,[spl4_210])],[avatar_definition]) ).
fof(f2583,plain,
( member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract)
| ~ spl4_210 ),
inference(avatar_component_clause,[],[f2582]) ).
fof(f2584,plain,
( ~ member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract)
| spl4_210 ),
inference(avatar_component_clause,[],[f2582]) ).
fof(f3386,plain,
! [X2,X0,X1] :
( ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ap_parcontractE_sk2q(sF0(X0),X1,X2) = comb_app(ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)),ap_parcontractE_sk2s(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)))
| combS = comb_app(combK,ap_parcontractE_sk2q(sF0(X0),X1,X2)) ),
inference(resolution,[],[f1483,f210]) ).
fof(f3388,plain,
! [X2,X0,X1] :
( ap_parcontractE_c3(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))
| ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ap_parcontractE_sk2q(sF0(X0),X1,X2) = comb_app(ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)),ap_parcontractE_sk2s(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))) ),
inference(forward_subsumption_resolution,[],[f3386,f159]) ).
fof(f4367,plain,
( r = comb_app(sF0(p),ap_parcontractE_sk2s(sF0(p),q,r))
| ~ spl4_12
| ~ spl4_21 ),
inference(superposition,[],[f760,f619]) ).
fof(f4434,plain,
( ap_parcontractE_c1(combS,p,sF0(p))
| ap_parcontractE_c2(combS,p,sF0(p))
| ap_parcontractE_c3(combS,p,sF0(p))
| ap_parcontractE_c4(combS,p,sF0(p))
| ~ ap_parcontractE_c4(sF0(p),q,r)
| ~ spl4_21 ),
inference(superposition,[],[f348,f619]) ).
fof(f4440,plain,
( ap_parcontractE_c1(combS,p,sF0(p))
| ap_parcontractE_c2(combS,p,sF0(p))
| ap_parcontractE_c3(combS,p,sF0(p))
| ap_parcontractE_c4(combS,p,sF0(p))
| ~ spl4_12
| ~ spl4_21 ),
inference(forward_subsumption_resolution,[],[f4434,f317]) ).
fof(f4491,plain,
( r = sF1(p,ap_parcontractE_sk2s(sF0(p),q,r))
| ~ spl4_12
| ~ spl4_21 ),
inference(forward_demodulation,[],[f4367,f238]) ).
fof(f4493,definition,
( spl4_305
<=> ap_parcontractE_c4(combS,p,sF0(p)) ),
introduced(definition,[new_symbols(definition,[spl4_305])],[avatar_definition]) ).
fof(f4495,plain,
( ap_parcontractE_c4(combS,p,sF0(p))
| ~ spl4_305 ),
inference(avatar_component_clause,[],[f4493]) ).
fof(f4497,definition,
( spl4_306
<=> ap_parcontractE_c3(combS,p,sF0(p)) ),
introduced(definition,[new_symbols(definition,[spl4_306])],[avatar_definition]) ).
fof(f4499,plain,
( ap_parcontractE_c3(combS,p,sF0(p))
| ~ spl4_306 ),
inference(avatar_component_clause,[],[f4497]) ).
fof(f4501,definition,
( spl4_307
<=> ap_parcontractE_c2(combS,p,sF0(p)) ),
introduced(definition,[new_symbols(definition,[spl4_307])],[avatar_definition]) ).
fof(f4503,plain,
( ap_parcontractE_c2(combS,p,sF0(p))
| ~ spl4_307 ),
inference(avatar_component_clause,[],[f4501]) ).
fof(f4505,definition,
( spl4_308
<=> ap_parcontractE_c1(combS,p,sF0(p)) ),
introduced(definition,[new_symbols(definition,[spl4_308])],[avatar_definition]) ).
fof(f4507,plain,
( ap_parcontractE_c1(combS,p,sF0(p))
| ~ spl4_308 ),
inference(avatar_component_clause,[],[f4505]) ).
fof(f4508,plain,
( spl4_305
| spl4_306
| spl4_307
| spl4_308
| ~ spl4_12
| ~ spl4_21 ),
inference(avatar_split_clause,[],[f4440,f617,f315,f4505,f4501,f4497,f4493]) ).
fof(f4586,plain,
( member(comb_app(combS,p),comb)
| ~ spl4_308 ),
inference(resolution,[],[f4507,f204]) ).
fof(f4588,plain,
( member(sF0(p),comb)
| ~ spl4_308 ),
inference(forward_demodulation,[],[f4586,f236]) ).
fof(f4589,plain,
( member(p,comb)
| ~ spl4_15 ),
inference(resolution,[],[f533,f291]) ).
fof(f4590,plain,
( $false
| spl4_7
| ~ spl4_15 ),
inference(forward_subsumption_resolution,[],[f4589,f280]) ).
fof(f4591,plain,
( spl4_7
| ~ spl4_15 ),
inference(avatar_contradiction_clause,[],[f4590]) ).
fof(f4619,plain,
( r != r
| ~ member(sF2(p),parcontract)
| ~ member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract)
| ~ spl4_12
| ~ spl4_21 ),
inference(superposition,[],[f243,f4491]) ).
fof(f4631,plain,
( ~ member(sF2(p),parcontract)
| ~ member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract)
| ~ spl4_12
| ~ spl4_21 ),
inference(trivial_inequality_removal,[],[f4619]) ).
fof(f4633,plain,
( ~ member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract)
| ~ spl4_8
| ~ spl4_12
| ~ spl4_21 ),
inference(forward_subsumption_resolution,[],[f4631,f284]) ).
fof(f4635,plain,
( ~ spl4_210
| ~ spl4_8
| ~ spl4_12
| ~ spl4_21 ),
inference(avatar_split_clause,[],[f4633,f617,f315,f282,f2582]) ).
fof(f4897,plain,
( ~ ap_parcontractE_c4(sF0(p),q,r)
| spl4_210 ),
inference(resolution,[],[f2584,f263]) ).
fof(f4898,plain,
( $false
| ~ spl4_12
| spl4_210 ),
inference(forward_subsumption_resolution,[],[f4897,f317]) ).
fof(f4899,plain,
( ~ spl4_12
| spl4_210 ),
inference(avatar_contradiction_clause,[],[f4898]) ).
fof(f4948,plain,
( $false
| spl4_15
| ~ spl4_308 ),
inference(forward_subsumption_resolution,[],[f4588,f532]) ).
fof(f4949,plain,
( spl4_15
| ~ spl4_308 ),
inference(avatar_contradiction_clause,[],[f4948]) ).
fof(f5067,plain,
( combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,p,sF0(p))),ap_parcontractE_sk1q(combS,p,sF0(p)))
| ~ spl4_306 ),
inference(resolution,[],[f4499,f217]) ).
fof(f5068,plain,
( $false
| ~ spl4_306 ),
inference(forward_subsumption_resolution,[],[f5067,f159]) ).
fof(f5069,plain,
~ spl4_306,
inference(avatar_contradiction_clause,[],[f5068]) ).
fof(f5159,plain,
( combS = comb_app(combK,sF0(p))
| ~ spl4_307 ),
inference(resolution,[],[f4503,f210]) ).
fof(f5160,plain,
( $false
| ~ spl4_307 ),
inference(forward_subsumption_resolution,[],[f5159,f159]) ).
fof(f5161,plain,
~ spl4_307,
inference(avatar_contradiction_clause,[],[f5160]) ).
fof(f5208,plain,
( sF0(p) = comb_app(ap_parcontractE_sk2q(combS,p,sF0(p)),ap_parcontractE_sk2s(combS,p,sF0(p)))
| ~ spl4_305 ),
inference(resolution,[],[f4495,f221]) ).
fof(f5310,plain,
( ! [X0] :
( sF0(X0) != sF0(p)
| ap_parcontractE_sk2s(combS,p,sF0(p)) = X0 )
| ~ spl4_305 ),
inference(superposition,[],[f332,f5208]) ).
fof(f5668,plain,
( p = ap_parcontractE_sk2s(combS,p,sF0(p))
| ~ spl4_305 ),
inference(equality_resolution,[],[f5310]) ).
fof(f5671,plain,
( member(sF2(p),parcontract)
| ~ ap_parcontractE_c4(combS,p,sF0(p))
| ~ spl4_305 ),
inference(superposition,[],[f262,f5668]) ).
fof(f5675,plain,
( ~ ap_parcontractE_c4(combS,p,sF0(p))
| spl4_8
| ~ spl4_305 ),
inference(forward_subsumption_resolution,[],[f5671,f283]) ).
fof(f5680,plain,
( $false
| spl4_8
| ~ spl4_305 ),
inference(forward_subsumption_resolution,[],[f5675,f4495]) ).
fof(f5681,plain,
( spl4_8
| ~ spl4_305 ),
inference(avatar_contradiction_clause,[],[f5680]) ).
fof(f7057,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ap_parcontractE_sk2q(sF0(X0),X1,X2) = comb_app(ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)),ap_parcontractE_sk2s(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)))
| combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))),ap_parcontractE_sk1q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))) ),
inference(resolution,[],[f3388,f217]) ).
fof(f7058,plain,
! [X2,X0,X1] :
( ~ ap_parcontractE_c4(sF0(X0),X1,X2)
| sF0(X0) = ap_parcontractE_sk2q(sF0(X0),X1,X2)
| ap_parcontractE_sk2q(sF0(X0),X1,X2) = comb_app(ap_parcontractE_sk2q(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2)),ap_parcontractE_sk2s(combS,X0,ap_parcontractE_sk2q(sF0(X0),X1,X2))) ),
inference(forward_subsumption_resolution,[],[f7057,f159]) ).
fof(f7059,plain,
( sF0(p) = ap_parcontractE_sk2q(sF0(p),q,r)
| ap_parcontractE_sk2q(sF0(p),q,r) = comb_app(ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)),ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)))
| ~ spl4_12 ),
inference(resolution,[],[f7058,f317]) ).
fof(f7068,plain,
( ap_parcontractE_sk2q(sF0(p),q,r) = comb_app(ap_parcontractE_sk2q(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)),ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)))
| ~ spl4_12
| spl4_21 ),
inference(forward_subsumption_resolution,[],[f7059,f618]) ).
fof(f7073,plain,
( ap_parcontractE_sk2q(sF0(p),q,r) = comb_app(combS,ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)))
| ~ spl4_12
| spl4_21
| ~ spl4_22 ),
inference(forward_demodulation,[],[f7068,f623]) ).
fof(f7078,plain,
( ap_parcontractE_sk2q(sF0(p),q,r) = sF0(ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)))
| ~ spl4_12
| spl4_21
| ~ spl4_22 ),
inference(forward_demodulation,[],[f7073,f236]) ).
fof(f7091,plain,
( ! [X0] : comb_app(ap_parcontractE_sk2q(sF0(p),q,r),X0) = sF1(ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)),X0)
| ~ spl4_12
| spl4_21
| ~ spl4_22 ),
inference(superposition,[],[f238,f7078]) ).
fof(f7194,plain,
( ! [X0] :
( r != comb_app(ap_parcontractE_sk2q(sF0(p),q,r),X0)
| ~ member(sF2(ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))),parcontract)
| ~ member(sF3(X0),parcontract) )
| ~ spl4_12
| spl4_21
| ~ spl4_22 ),
inference(superposition,[],[f243,f7091]) ).
fof(f7219,definition,
( spl4_422
<=> member(sF2(ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))),parcontract) ),
introduced(definition,[new_symbols(definition,[spl4_422])],[avatar_definition]) ).
fof(f7221,plain,
( ~ member(sF2(ap_parcontractE_sk2s(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))),parcontract)
| spl4_422 ),
inference(avatar_component_clause,[],[f7219]) ).
fof(f7223,definition,
( spl4_423
<=> ! [X0] :
( r != comb_app(ap_parcontractE_sk2q(sF0(p),q,r),X0)
| ~ member(sF3(X0),parcontract) ) ),
introduced(definition,[new_symbols(definition,[spl4_423])],[avatar_definition]) ).
fof(f7224,plain,
( ! [X0] :
( r != comb_app(ap_parcontractE_sk2q(sF0(p),q,r),X0)
| ~ member(sF3(X0),parcontract) )
| ~ spl4_423 ),
inference(avatar_component_clause,[],[f7223]) ).
fof(f7225,plain,
( ~ spl4_422
| spl4_423
| ~ spl4_12
| spl4_21
| ~ spl4_22 ),
inference(avatar_split_clause,[],[f7194,f621,f617,f315,f7223,f7219]) ).
fof(f7227,plain,
( ~ ap_parcontractE_c4(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| spl4_422 ),
inference(resolution,[],[f7221,f262]) ).
fof(f7228,plain,
( ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ~ ap_parcontractE_c4(sF0(p),q,r)
| sF0(p) = ap_parcontractE_sk2q(sF0(p),q,r)
| spl4_422 ),
inference(resolution,[],[f7227,f404]) ).
fof(f7229,plain,
( ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| sF0(p) = ap_parcontractE_sk2q(sF0(p),q,r)
| ~ spl4_12
| spl4_422 ),
inference(forward_subsumption_resolution,[],[f7228,f317]) ).
fof(f7230,plain,
( ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ~ spl4_12
| spl4_21
| spl4_422 ),
inference(forward_subsumption_resolution,[],[f7229,f618]) ).
fof(f7232,definition,
( spl4_424
<=> ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)) ),
introduced(definition,[new_symbols(definition,[spl4_424])],[avatar_definition]) ).
fof(f7234,plain,
( ap_parcontractE_c2(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ~ spl4_424 ),
inference(avatar_component_clause,[],[f7232]) ).
fof(f7236,definition,
( spl4_425
<=> ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)) ),
introduced(definition,[new_symbols(definition,[spl4_425])],[avatar_definition]) ).
fof(f7238,plain,
( ap_parcontractE_c3(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))
| ~ spl4_425 ),
inference(avatar_component_clause,[],[f7236]) ).
fof(f7239,plain,
( spl4_424
| spl4_425
| ~ spl4_12
| spl4_21
| spl4_422 ),
inference(avatar_split_clause,[],[f7230,f7219,f617,f315,f7236,f7232]) ).
fof(f7241,plain,
( r != r
| ~ member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract)
| ~ spl4_12
| ~ spl4_423 ),
inference(superposition,[],[f7224,f760]) ).
fof(f7242,plain,
( ~ member(sF3(ap_parcontractE_sk2s(sF0(p),q,r)),parcontract)
| ~ spl4_12
| ~ spl4_423 ),
inference(trivial_inequality_removal,[],[f7241]) ).
fof(f7243,plain,
( $false
| ~ spl4_12
| ~ spl4_210
| ~ spl4_423 ),
inference(forward_subsumption_resolution,[],[f7242,f2583]) ).
fof(f7244,plain,
( ~ spl4_12
| ~ spl4_210
| ~ spl4_423 ),
inference(avatar_contradiction_clause,[],[f7243]) ).
fof(f7247,plain,
( combS = comb_app(combK,ap_parcontractE_sk2q(sF0(p),q,r))
| ~ spl4_424 ),
inference(resolution,[],[f7234,f210]) ).
fof(f7248,plain,
( $false
| ~ spl4_424 ),
inference(forward_subsumption_resolution,[],[f7247,f159]) ).
fof(f7249,plain,
~ spl4_424,
inference(avatar_contradiction_clause,[],[f7248]) ).
fof(f7256,plain,
( combS = comb_app(comb_app(combS,ap_parcontractE_sk1p(combS,p,ap_parcontractE_sk2q(sF0(p),q,r))),ap_parcontractE_sk1q(combS,p,ap_parcontractE_sk2q(sF0(p),q,r)))
| ~ spl4_425 ),
inference(resolution,[],[f7238,f217]) ).
fof(f7257,plain,
( $false
| ~ spl4_425 ),
inference(forward_subsumption_resolution,[],[f7256,f159]) ).
fof(f7258,plain,
~ spl4_425,
inference(avatar_contradiction_clause,[],[f7257]) ).
cnf(s5,plain,
( ~ spl4_5
| spl4_6 ),
inference(sat_conversion,[],[f276]) ).
cnf(s6,plain,
( ~ spl4_7
| spl4_8 ),
inference(sat_conversion,[],[f285]) ).
cnf(s7,plain,
( spl4_9
| spl4_10
| spl4_11
| spl4_12 ),
inference(sat_conversion,[],[f318]) ).
cnf(s8,plain,
( ~ spl4_6
| ~ spl4_8
| ~ spl4_9 ),
inference(sat_conversion,[],[f323]) ).
cnf(s12,plain,
( spl4_5
| ~ spl4_9 ),
inference(sat_conversion,[],[f507]) ).
cnf(s25,plain,
~ spl4_10,
inference(sat_conversion,[],[f606]) ).
cnf(s27,plain,
~ spl4_11,
inference(sat_conversion,[],[f613]) ).
cnf(s28,plain,
( ~ spl4_12
| spl4_21
| spl4_22 ),
inference(sat_conversion,[],[f624]) ).
cnf(s29,plain,
( ~ spl4_9
| spl4_17 ),
inference(sat_conversion,[],[f625]) ).
cnf(s30,plain,
( ~ spl4_9
| spl4_15
| ~ spl4_17 ),
inference(sat_conversion,[],[f757]) ).
cnf(s297,plain,
( ~ spl4_12
| ~ spl4_21
| spl4_305
| spl4_306
| spl4_307
| spl4_308 ),
inference(sat_conversion,[],[f4508]) ).
cnf(s298,plain,
( spl4_7
| ~ spl4_15 ),
inference(sat_conversion,[],[f4591]) ).
cnf(s299,plain,
( ~ spl4_8
| ~ spl4_12
| ~ spl4_21
| ~ spl4_210 ),
inference(sat_conversion,[],[f4635]) ).
cnf(s310,plain,
( ~ spl4_12
| spl4_210 ),
inference(sat_conversion,[],[f4899]) ).
cnf(s316,plain,
( spl4_15
| ~ spl4_308 ),
inference(sat_conversion,[],[f4949]) ).
cnf(s323,plain,
~ spl4_306,
inference(sat_conversion,[],[f5069]) ).
cnf(s331,plain,
~ spl4_307,
inference(sat_conversion,[],[f5161]) ).
cnf(s355,plain,
( spl4_8
| ~ spl4_305 ),
inference(sat_conversion,[],[f5681]) ).
cnf(s415,plain,
( ~ spl4_12
| spl4_21
| ~ spl4_22
| ~ spl4_422
| spl4_423 ),
inference(sat_conversion,[],[f7225]) ).
cnf(s416,plain,
( ~ spl4_12
| spl4_21
| spl4_422
| spl4_424
| spl4_425 ),
inference(sat_conversion,[],[f7239]) ).
cnf(s417,plain,
( ~ spl4_12
| ~ spl4_210
| ~ spl4_423 ),
inference(sat_conversion,[],[f7244]) ).
cnf(s418,plain,
~ spl4_424,
inference(sat_conversion,[],[f7249]) ).
cnf(s421,plain,
~ spl4_425,
inference(sat_conversion,[],[f7258]) ).
cnf(s423,plain,
( ~ spl4_12
| spl4_21
| spl4_422 ),
inference(rat,[],[s416,s421,s418]) ).
cnf(s424,plain,
( ~ spl4_12
| ~ spl4_21
| spl4_305
| spl4_308 ),
inference(rat,[],[s297,s331,s323]) ).
cnf(s430,plain,
( spl4_9
| spl4_12 ),
inference(rat,[],[s7,s27,s25]) ).
cnf(s432,plain,
( spl4_21
| ~ spl4_422
| ~ spl4_12
| spl4_423 ),
inference(rat,[],[s28,s415]) ).
cnf(s433,plain,
( spl4_21
| ~ spl4_12 ),
inference(rat,[],[s432,s423,s417,s310]) ).
cnf(s434,plain,
( ~ spl4_21
| ~ spl4_210
| ~ spl4_12 ),
inference(rat,[],[s316,s298,s424,s6,s355,s299]) ).
cnf(s435,plain,
~ spl4_12,
inference(rat,[],[s434,s433,s310]) ).
cnf(s436,plain,
spl4_9,
inference(rat,[],[s430,s435]) ).
cnf(s437,plain,
spl4_17,
inference(rat,[],[s29,s436]) ).
cnf(s438,plain,
spl4_5,
inference(rat,[],[s12,s436]) ).
cnf(s439,plain,
spl4_15,
inference(rat,[],[s30,s436,s437]) ).
cnf(s440,plain,
spl4_6,
inference(rat,[],[s5,s438]) ).
cnf(s441,plain,
spl4_7,
inference(rat,[],[s298,s439]) ).
cnf(s442,plain,
~ spl4_8,
inference(rat,[],[s8,s436,s440]) ).
cnf(s443,plain,
$false,
inference(rat,[],[s6,s442,s441]) ).
fof(f7261,plain,
$false,
inference(avatar_sat_refutation,[],[s443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL094-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n017.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 21:31:21 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.92/2.39 % (4061748)Input is clausal, will run a generic CNF schedule.
% 11.92/2.39 % (4061754)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1241252857:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.92/2.39 % (4061758)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=541706629:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.92/2.39 % (4061759)dis-21_1_sil=8000:lcm=predicate:random_seed=1064503818:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.92/2.39 % (4061755)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3483735123:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.92/2.39 % (4061757)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2264059994:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.92/2.39 % (4061756)lrs+10_1_sil=8000:sp=occurrence:random_seed=2507951083:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.92/2.39 % (4061753)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=714959652:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.92/2.39 % (4061756)Refutation not found, incomplete strategy
% 11.92/2.39 % (4061756)------------------------------
% 11.92/2.39 % (4061756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061756)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061756)Termination reason: Refutation not found, incomplete strategy
% 11.92/2.39 % (4061756)Time elapsed: 0.002 s
% 11.92/2.39 % (4061756)Peak memory usage: 88 MB
% 11.92/2.39 % (4061756)Instructions burned: 1 (million)
% 11.92/2.39 % (4061757)Refutation not found, incomplete strategy
% 11.92/2.39 % (4061757)------------------------------
% 11.92/2.39 % (4061757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061757)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061757)Termination reason: Refutation not found, incomplete strategy
% 11.92/2.39 % (4061757)Time elapsed: 0.003 s
% 11.92/2.39 % (4061757)Peak memory usage: 88 MB
% 11.92/2.39 % (4061757)Instructions burned: 2 (million)
% 11.92/2.39 % (4061759)Instruction limit reached!
% 11.92/2.39 % (4061759)------------------------------
% 11.92/2.39 % (4061759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061759)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061759)Termination reason: Instruction limit
% 11.92/2.39 % (4061759)Termination phase: Saturation
% 11.92/2.39 % (4061759)Time elapsed: 0.078 s
% 11.92/2.39 % (4061759)Peak memory usage: 89 MB
% 11.92/2.39 % (4061759)Instructions burned: 118 (million)
% 11.92/2.39 % (4061758)Instruction limit reached!
% 11.92/2.39 % (4061758)------------------------------
% 11.92/2.39 % (4061758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061758)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061758)Termination reason: Instruction limit
% 11.92/2.39 % (4061758)Termination phase: Saturation
% 11.92/2.39 % (4061758)Time elapsed: 0.124 s
% 11.92/2.39 % (4061758)Peak memory usage: 90 MB
% 11.92/2.39 % (4061758)Instructions burned: 181 (million)
% 11.92/2.39 % (4061757)------------------------------
% 11.92/2.39 % (4061757)------------------------------
% 11.92/2.39 % (4061756)------------------------------
% 11.92/2.39 % (4061756)------------------------------
% 11.92/2.39 % (4061767)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=689983362:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.92/2.39 % (4061767)Refutation not found, incomplete strategy
% 11.92/2.39 % (4061767)------------------------------
% 11.92/2.39 % (4061767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061767)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061767)Termination reason: Refutation not found, incomplete strategy
% 11.92/2.39 % (4061767)Time elapsed: 0.015 s
% 11.92/2.39 % (4061767)Peak memory usage: 88 MB
% 11.92/2.39 % (4061767)Instructions burned: 21 (million)
% 11.92/2.39 % (4061768)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3661841459:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.92/2.39 % (4061768)Instruction limit reached!
% 11.92/2.39 % (4061768)------------------------------
% 11.92/2.39 % (4061768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061768)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061768)Termination reason: Instruction limit
% 11.92/2.39 % (4061768)Termination phase: Saturation
% 11.92/2.39 % (4061768)Time elapsed: 0.096 s
% 11.92/2.39 % (4061768)Peak memory usage: 91 MB
% 11.92/2.39 % (4061768)Instructions burned: 190 (million)
% 11.92/2.39 % (4061771)lrs+10_64_to=lpo:sil=8000:random_seed=2488848381:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 11.92/2.39 % (4061770)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2404753949:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 11.92/2.39 % (4061770)Refutation not found, incomplete strategy
% 11.92/2.39 % (4061770)------------------------------
% 11.92/2.39 % (4061770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061770)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061770)Termination reason: Refutation not found, incomplete strategy
% 11.92/2.39 % (4061770)Time elapsed: 0.012 s
% 11.92/2.39 % (4061770)Peak memory usage: 88 MB
% 11.92/2.39 % (4061770)Instructions burned: 18 (million)
% 11.92/2.39 % (4061771)Instruction limit reached!
% 11.92/2.39 % (4061771)------------------------------
% 11.92/2.39 % (4061771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061771)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061771)Termination reason: Instruction limit
% 11.92/2.39 % (4061771)Termination phase: Saturation
% 11.92/2.39 % (4061771)Time elapsed: 0.079 s
% 11.92/2.39 % (4061771)Peak memory usage: 89 MB
% 11.92/2.39 % (4061771)Instructions burned: 127 (million)
% 11.92/2.39 % (4061767)------------------------------
% 11.92/2.39 % (4061767)------------------------------
% 11.92/2.39 % (4061773)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=122255149:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 11.92/2.39 % (4061773)Instruction limit reached!
% 11.92/2.39 % (4061773)------------------------------
% 11.92/2.39 % (4061773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061773)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061773)Termination reason: Instruction limit
% 11.92/2.39 % (4061773)Termination phase: Saturation
% 11.92/2.39 % (4061773)Time elapsed: 0.123 s
% 11.92/2.39 % (4061773)Peak memory usage: 91 MB
% 11.92/2.39 % (4061773)Instructions burned: 195 (million)
% 11.92/2.39 % (4061776)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=112328543:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 11.92/2.39 % (4061777)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2890545530:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 11.92/2.39 % (4061770)------------------------------
% 11.92/2.39 % (4061770)------------------------------
% 11.92/2.39 % (4061776)Instruction limit reached!
% 11.92/2.39 % (4061776)------------------------------
% 11.92/2.39 % (4061776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061776)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061776)Termination reason: Instruction limit
% 11.92/2.39 % (4061776)Termination phase: Saturation
% 11.92/2.39 % (4061776)Time elapsed: 0.093 s
% 11.92/2.39 % (4061776)Peak memory usage: 91 MB
% 11.92/2.39 % (4061776)Instructions burned: 157 (million)
% 11.92/2.39 % (4061779)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=4012108002:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 11.92/2.39 % (4061782)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2068469935:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 11.92/2.39 % (4061779)Instruction limit reached!
% 11.92/2.39 % (4061779)------------------------------
% 11.92/2.39 % (4061779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061779)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061779)Termination reason: Instruction limit
% 11.92/2.39 % (4061779)Termination phase: Saturation
% 11.92/2.39 % (4061779)Time elapsed: 0.060 s
% 11.92/2.39 % (4061779)Peak memory usage: 90 MB
% 11.92/2.39 % (4061779)Instructions burned: 108 (million)
% 11.92/2.39 % (4061782)Instruction limit reached!
% 11.92/2.39 % (4061782)------------------------------
% 11.92/2.39 % (4061782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061782)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061782)Termination reason: Instruction limit
% 11.92/2.39 % (4061782)Termination phase: Saturation
% 11.92/2.39 % (4061782)Time elapsed: 0.069 s
% 11.92/2.39 % (4061782)Peak memory usage: 89 MB
% 11.92/2.39 % (4061782)Instructions burned: 108 (million)
% 11.92/2.39 % (4061783)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=764383565:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 11.92/2.39 % (4061786)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1450776038:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 11.92/2.39 % (4061787)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2776495073:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 11.92/2.39 % (4061783)Instruction limit reached!
% 11.92/2.39 % (4061783)------------------------------
% 11.92/2.39 % (4061783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061783)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061783)Termination reason: Instruction limit
% 11.92/2.39 % (4061783)Termination phase: Saturation
% 11.92/2.39 % (4061783)Time elapsed: 0.155 s
% 11.92/2.39 % (4061783)Peak memory usage: 89 MB
% 11.92/2.39 % (4061783)Instructions burned: 242 (million)
% 11.92/2.39 % (4061787)Instruction limit reached!
% 11.92/2.39 % (4061787)------------------------------
% 11.92/2.39 % (4061787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061787)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061787)Termination reason: Instruction limit
% 11.92/2.39 % (4061787)Termination phase: Saturation
% 11.92/2.39 % (4061787)Time elapsed: 0.073 s
% 11.92/2.39 % (4061787)Peak memory usage: 90 MB
% 11.92/2.39 % (4061787)Instructions burned: 134 (million)
% 11.92/2.39 % (4061791)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=860927403:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 11.92/2.39 % (4061753)First to succeed.
% 11.92/2.39 % (4061753)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4061748"
% 11.92/2.39 % (4061792)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=762526660:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 11.92/2.39 % (4061777)Also succeeded, but the first one will report.
% 11.92/2.39 % (4061792)Instruction limit reached!
% 11.92/2.39 % (4061792)------------------------------
% 11.92/2.39 % (4061792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.39 % (4061792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.39 % (4061792)CaDiCaL version: 2.1.3
% 11.92/2.39 % (4061792)Termination reason: Instruction limit
% 11.92/2.39 % (4061792)Termination phase: Saturation
% 11.92/2.39 % (4061792)Time elapsed: 0.115 s
% 11.92/2.39 % (4061792)Peak memory usage: 90 MB
% 11.92/2.39 % (4061792)Instructions burned: 192 (million)
% 11.92/2.39 % (4061753)Refutation found. Thanks to Tanya!
% 11.92/2.39 % SZS status Unsatisfiable for theBenchmark
% 11.92/2.39 % SZS output start Proof for theBenchmark
% See solution above
% 12.66/2.59 % (4061753)------------------------------
% 12.66/2.59 % (4061753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.66/2.59 % (4061753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/2.59 % (4061753)CaDiCaL version: 2.1.3
% 12.66/2.59 % (4061753)Termination reason: Refutation
% 12.66/2.59 % (4061753)Time elapsed: 1.274 s
% 12.66/2.59 % (4061753)Peak memory usage: 137 MB
% 12.66/2.59 % (4061753)Instructions burned: 1939 (million)
% 12.66/2.59 % (4061753)------------------------------
% 12.66/2.59 % (4061753)------------------------------
% 12.66/2.59 % (4061748)Success in time 1.713 s
% 12.66/2.59 % Vampire exiting
%------------------------------------------------------------------------------