%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN159-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 01:49:48 PM UTC 2026
% Result : Unsatisfiable 3.55s 1.16s
% Output : Refutation 3.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 102
% Syntax : Number of formulae : 353 ( 79 unt; 44 def)
% Number of atoms : 878 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 1053 ( 528 ~; 481 |; 0 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 76 ( 75 usr; 45 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 251 ( 0 sgn 251 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
s0(d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(f5,axiom,
s0(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
fof(f7,axiom,
n0(d,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
fof(f11,axiom,
n0(e,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_11) ).
fof(f13,axiom,
r0(e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_13) ).
fof(f14,axiom,
! [X0] : p0(b,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_14) ).
fof(f17,axiom,
! [X0] : q0(X0,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_17) ).
fof(f18,axiom,
p0(c,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(f19,axiom,
! [X0,X1] : m0(X0,d,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_19) ).
fof(f20,axiom,
l0(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_20) ).
fof(f24,axiom,
l0(c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_24) ).
fof(f26,axiom,
n0(d,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_26) ).
fof(f27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_27) ).
fof(f30,axiom,
n0(e,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_34) ).
fof(f36,axiom,
q0(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_36) ).
fof(f37,axiom,
n0(b,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_37) ).
fof(f39,axiom,
! [X0,X1] :
( ~ n0(X1,X0)
| k1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_001) ).
fof(f40,axiom,
! [X0,X1] :
( l1(X0,X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_002) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( l1(X0,X1)
| ~ p0(X2,X0)
| ~ r0(X3)
| ~ m0(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_003) ).
fof(f42,axiom,
! [X0,X1] :
( l1(X0,X0)
| ~ k1(X0)
| ~ l0(X1)
| ~ l1(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_004) ).
fof(f88,axiom,
! [X0,X1] :
( n1(X0,X1,X0)
| ~ s0(b)
| ~ l0(X0)
| ~ p0(b,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_050) ).
fof(f95,axiom,
! [X0] :
( n1(X0,X0,X0)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_057) ).
fof(f123,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_085) ).
fof(f131,axiom,
! [X0,X1] :
( q1(X0,X0,X0)
| ~ q0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_093) ).
fof(f154,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_116) ).
fof(f162,axiom,
! [X0,X1] :
( r1(X0)
| ~ q0(X0,X1)
| ~ s0(d)
| ~ q1(d,X1,d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_124) ).
fof(f163,axiom,
! [X0] :
( ~ p0(X0,X0)
| s1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_125) ).
fof(f164,axiom,
! [X2,X0,X1] :
( s1(X0)
| ~ q0(X0,X1)
| ~ s1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_126) ).
fof(f169,axiom,
! [X0,X1] :
( l2(X0,X1)
| ~ s1(X0)
| ~ n0(e,X1)
| ~ l2(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_131) ).
fof(f171,axiom,
! [X2,X3,X0,X1] :
( l2(X0,X0)
| ~ p0(X1,X1)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_133) ).
fof(f175,axiom,
! [X2,X0,X1] :
( ~ p1(X1,X2,X0)
| n2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_137) ).
fof(f203,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_165) ).
fof(f208,axiom,
! [X0] :
( p2(X0,e,X0)
| ~ n1(X0,e,e) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_170) ).
fof(f223,axiom,
! [X2,X0,X1] :
( q2(X0,X0,X0)
| ~ n1(X1,d,X2)
| ~ k1(X0)
| ~ q2(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_185) ).
fof(f224,axiom,
! [X0,X1] :
( q2(X0,X0,X1)
| ~ l1(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_186) ).
fof(f226,axiom,
! [X0] :
( r2(X0)
| ~ r1(X0)
| ~ l0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_188) ).
fof(f228,axiom,
( s2(d)
| ~ s1(a)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_190) ).
fof(f231,axiom,
! [X0,X1] :
( k3(X0,X0,X0)
| ~ s1(X0)
| ~ q2(d,X1,d)
| ~ s2(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_193) ).
fof(f248,axiom,
! [X0] :
( k3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_210) ).
fof(f274,axiom,
! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_236) ).
fof(f277,axiom,
( m3(b,b,b)
| ~ l2(a,b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_239) ).
fof(f278,axiom,
! [X2,X0,X1] :
( ~ p2(X1,X2,X0)
| n3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_240) ).
fof(f284,axiom,
! [X0] :
( p3(X0,X0,X0)
| ~ l2(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_246) ).
fof(f293,axiom,
! [X2,X0,X1] :
( ~ q2(X2,X0,X1)
| q3(X0,X1)
| ~ n0(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_255) ).
fof(f296,axiom,
! [X2,X0,X1] :
( q3(X0,X0)
| ~ r2(X0)
| ~ s1(X1)
| ~ l2(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_258) ).
fof(f312,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_274) ).
fof(f315,axiom,
! [X2,X0,X1] :
( ~ p3(X1,X2,X0)
| l4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_277) ).
fof(f322,axiom,
! [X0,X1] :
( n4(X0,X0)
| ~ k4(X1)
| ~ m3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_284) ).
fof(f324,axiom,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ q3(X1,X2)
| ~ n3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_286) ).
fof(f325,axiom,
! [X0,X1] :
( p4(X0,X1,X0)
| ~ k3(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_287) ).
fof(f327,axiom,
! [X2,X3,X0,X1] :
( p4(X0,X0,X0)
| ~ l4(X0)
| ~ n0(X0,X1)
| ~ p4(X2,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_289) ).
fof(f333,axiom,
! [X2,X3,X0,X1,X4] :
( ~ m3(X3,X4,X3)
| ~ k3(X2,X2,X0)
| ~ q2(X3,X1,X0)
| q4(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_295) ).
fof(f334,axiom,
! [X2,X0,X1] :
( q4(X0,X0)
| ~ r1(X0)
| ~ l4(X1)
| ~ q4(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_296) ).
fof(f345,axiom,
! [X2,X3,X0,X1,X4] :
( ~ p4(X4,X4,X1)
| ~ q4(X2,X3)
| ~ n4(X0,X3)
| n5(X0,X1)
| ~ n5(X4,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_307) ).
fof(f354,axiom,
! [X2,X0,X1] :
( n5(X0,X0)
| ~ p4(X1,X0,X0)
| ~ s1(X0)
| ~ p4(b,b,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_316) ).
fof(f369,negated_conjecture,
~ n5(a,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f396,definition,
( spl0_8
<=> ! [X2,X1] : ~ q3(X1,X2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f397,plain,
( ! [X2,X1] : ~ q3(X1,X2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f503,definition,
( spl0_39
<=> ! [X2,X3] : ~ p4(X2,X3,X2) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f504,plain,
( ! [X2,X3] : ~ p4(X2,X3,X2)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f506,definition,
( spl0_40
<=> ! [X0,X1] :
( p4(X0,X0,X0)
| ~ n0(X0,X1)
| ~ l4(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f507,plain,
( ! [X0,X1] :
( p4(X0,X0,X0)
| ~ n0(X0,X1)
| ~ l4(X0) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f508,plain,
( spl0_39
| spl0_40 ),
inference(avatar_split_clause,[],[f327,f506,f503]) ).
fof(f527,definition,
( spl0_46
<=> s0(d) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f528,plain,
( ~ s0(d)
| spl0_46 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f530,definition,
( spl0_47
<=> ! [X0,X1] :
( r1(X0)
| ~ q1(d,X1,d)
| ~ q0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f531,plain,
( ! [X0,X1] :
( ~ q1(d,X1,d)
| r1(X0)
| ~ q0(X0,X1) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f532,plain,
( ~ spl0_46
| spl0_47 ),
inference(avatar_split_clause,[],[f162,f530,f527]) ).
fof(f649,definition,
( spl0_82
<=> ! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f650,plain,
( ! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) )
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f671,plain,
spl0_82,
inference(avatar_split_clause,[],[f274,f649]) ).
fof(f673,definition,
( spl0_88
<=> ! [X2] : ~ l2(X2,X2) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f674,plain,
( ! [X2] : ~ l2(X2,X2)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f676,definition,
( spl0_89
<=> ! [X1] : ~ s1(X1) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f677,plain,
( ! [X1] : ~ s1(X1)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f679,definition,
( spl0_90
<=> ! [X0] :
( q3(X0,X0)
| ~ r2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f680,plain,
( ! [X0] :
( q3(X0,X0)
| ~ r2(X0) )
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f681,plain,
( spl0_88
| spl0_89
| spl0_90 ),
inference(avatar_split_clause,[],[f296,f679,f676,f673]) ).
fof(f690,definition,
( spl0_93
<=> ! [X0] :
( p4(X0,X0,X0)
| ~ n3(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f691,plain,
( ! [X0] :
( p4(X0,X0,X0)
| ~ n3(X0) )
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f692,plain,
( spl0_8
| spl0_93 ),
inference(avatar_split_clause,[],[f324,f690,f396]) ).
fof(f737,definition,
( spl0_106
<=> s2(d) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f758,definition,
( spl0_112
<=> l2(a,b) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f759,plain,
( ~ l2(a,b)
| spl0_112 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f761,definition,
( spl0_113
<=> m3(b,b,b) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f762,plain,
( m3(b,b,b)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f763,plain,
( ~ spl0_112
| spl0_113 ),
inference(avatar_split_clause,[],[f277,f761,f758]) ).
fof(f783,definition,
( spl0_119
<=> ! [X2,X1] :
( ~ n1(X1,d,X2)
| ~ q2(X2,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f784,plain,
( ! [X2,X1] :
( ~ q2(X2,X2,X1)
| ~ n1(X1,d,X2) )
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f786,definition,
( spl0_120
<=> ! [X0] :
( q2(X0,X0,X0)
| ~ k1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f787,plain,
( ! [X0] :
( q2(X0,X0,X0)
| ~ k1(X0) )
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f788,plain,
( spl0_119
| spl0_120 ),
inference(avatar_split_clause,[],[f223,f786,f783]) ).
fof(f797,definition,
( spl0_123
<=> q1(e,e,e) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f798,plain,
( ~ q1(e,e,e)
| spl0_123 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f821,definition,
( spl0_130
<=> ! [X1] :
( ~ l0(X1)
| ~ l1(X1,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f822,plain,
( ! [X1] :
( ~ l1(X1,X1)
| ~ l0(X1) )
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f824,definition,
( spl0_131
<=> ! [X0] :
( l1(X0,X0)
| ~ k1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f825,plain,
( ! [X0] :
( l1(X0,X0)
| ~ k1(X0) )
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f826,plain,
( spl0_130
| spl0_131 ),
inference(avatar_split_clause,[],[f42,f824,f821]) ).
fof(f835,definition,
( spl0_134
<=> ! [X2] : ~ l0(X2) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f836,plain,
( ! [X2] : ~ l0(X2)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f901,definition,
( spl0_152
<=> s0(b) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f902,plain,
( ~ s0(b)
| spl0_152 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f945,definition,
( spl0_164
<=> ! [X2,X1] :
( ~ l4(X1)
| ~ q4(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f946,plain,
( ! [X2,X1] :
( ~ q4(X1,X2)
| ~ l4(X1) )
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f948,definition,
( spl0_165
<=> ! [X0] :
( q4(X0,X0)
| ~ r1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f949,plain,
( ! [X0] :
( q4(X0,X0)
| ~ r1(X0) )
| ~ spl0_165 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f950,plain,
( spl0_164
| spl0_165 ),
inference(avatar_split_clause,[],[f334,f948,f945]) ).
fof(f958,definition,
( spl0_168
<=> q4(b,b) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f959,plain,
( q4(b,b)
| ~ spl0_168 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f962,definition,
( spl0_169
<=> n3(e) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f963,plain,
( ~ n3(e)
| spl0_169 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f965,definition,
( spl0_170
<=> q3(e,b) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f966,plain,
( ~ q3(e,b)
| spl0_170 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f968,definition,
( spl0_171
<=> n0(c,d) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f969,plain,
( ~ n0(c,d)
| spl0_171 ),
inference(avatar_component_clause,[],[f968]) ).
fof(f971,definition,
( spl0_172
<=> k4(c) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f972,plain,
( k4(c)
| ~ spl0_172 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f973,plain,
( ~ spl0_169
| ~ spl0_170
| ~ spl0_171
| spl0_172 ),
inference(avatar_split_clause,[],[f312,f971,f968,f965,f962]) ).
fof(f986,definition,
( spl0_176
<=> ! [X0,X1] :
( s1(X0)
| ~ q0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f987,plain,
( ! [X0,X1] :
( ~ q0(X0,X1)
| s1(X0) )
| ~ spl0_176 ),
inference(avatar_component_clause,[],[f986]) ).
fof(f988,plain,
( spl0_89
| spl0_176 ),
inference(avatar_split_clause,[],[f164,f986,f676]) ).
fof(f990,definition,
( spl0_177
<=> ! [X1] : ~ p0(X1,X1) ),
introduced(definition,[new_symbols(definition,[spl0_177])],[avatar_definition]) ).
fof(f991,plain,
( ! [X1] : ~ p0(X1,X1)
| ~ spl0_177 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f993,definition,
( spl0_178
<=> ! [X2,X0,X3] :
( l2(X0,X0)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f994,plain,
( ! [X2,X3,X0] :
( l2(X0,X0)
| ~ s1(X2)
| ~ m0(X3,X2,X0) )
| ~ spl0_178 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f995,plain,
( spl0_177
| spl0_178 ),
inference(avatar_split_clause,[],[f171,f993,f990]) ).
fof(f1021,definition,
( spl0_186
<=> s1(a) ),
introduced(definition,[new_symbols(definition,[spl0_186])],[avatar_definition]) ).
fof(f1022,plain,
( ~ s1(a)
| spl0_186 ),
inference(avatar_component_clause,[],[f1021]) ).
fof(f1023,plain,
( s2(d)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f1024,plain,
( ~ spl0_46
| ~ spl0_186
| spl0_106 ),
inference(avatar_split_clause,[],[f228,f737,f1021,f527]) ).
fof(f1030,definition,
( spl0_188
<=> ! [X1] :
( ~ q2(d,X1,d)
| ~ s2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f1031,plain,
( ! [X1] :
( ~ q2(d,X1,d)
| ~ s2(X1) )
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f1030]) ).
fof(f1033,definition,
( spl0_189
<=> ! [X0] :
( k3(X0,X0,X0)
| ~ s1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_189])],[avatar_definition]) ).
fof(f1034,plain,
( ! [X0] :
( k3(X0,X0,X0)
| ~ s1(X0) )
| ~ spl0_189 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1035,plain,
( spl0_188
| spl0_189 ),
inference(avatar_split_clause,[],[f231,f1033,f1030]) ).
fof(f1055,definition,
( spl0_195
<=> ! [X1] : ~ k4(X1) ),
introduced(definition,[new_symbols(definition,[spl0_195])],[avatar_definition]) ).
fof(f1056,plain,
( ! [X1] : ~ k4(X1)
| ~ spl0_195 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1058,definition,
( spl0_196
<=> ! [X0] :
( n4(X0,X0)
| ~ m3(X0,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_196])],[avatar_definition]) ).
fof(f1059,plain,
( ! [X0] :
( ~ m3(X0,X0,X0)
| n4(X0,X0) )
| ~ spl0_196 ),
inference(avatar_component_clause,[],[f1058]) ).
fof(f1060,plain,
( spl0_195
| spl0_196 ),
inference(avatar_split_clause,[],[f322,f1058,f1055]) ).
fof(f1129,definition,
( spl0_216
<=> ! [X0,X1] :
( n1(X0,X1,X0)
| ~ p0(b,X1)
| ~ l0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1130,plain,
( ! [X0,X1] :
( n1(X0,X1,X0)
| ~ p0(b,X1)
| ~ l0(X0) )
| ~ spl0_216 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1131,plain,
( ~ spl0_152
| spl0_216 ),
inference(avatar_split_clause,[],[f88,f1129,f901]) ).
fof(f1144,definition,
( spl0_220
<=> ! [X3] : ~ r0(X3) ),
introduced(definition,[new_symbols(definition,[spl0_220])],[avatar_definition]) ).
fof(f1145,plain,
( ! [X3] : ~ r0(X3)
| ~ spl0_220 ),
inference(avatar_component_clause,[],[f1144]) ).
fof(f1147,definition,
( spl0_221
<=> ! [X2,X0,X1] :
( l1(X0,X1)
| ~ m0(X1,X0,X2)
| ~ p0(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f1148,plain,
( ! [X2,X0,X1] :
( ~ m0(X1,X0,X2)
| l1(X0,X1)
| ~ p0(X2,X0) )
| ~ spl0_221 ),
inference(avatar_component_clause,[],[f1147]) ).
fof(f1149,plain,
( spl0_220
| spl0_221 ),
inference(avatar_split_clause,[],[f41,f1147,f1144]) ).
fof(f1225,definition,
( spl0_241
<=> n1(e,e,e) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1226,plain,
( ~ n1(e,e,e)
| spl0_241 ),
inference(avatar_component_clause,[],[f1225]) ).
fof(f1242,definition,
( spl0_246
<=> ! [X2,X1] :
( ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f1243,plain,
( ! [X2,X1] :
( ~ p2(X1,X1,X2)
| ~ q1(X1,X2,X1) )
| ~ spl0_246 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1245,definition,
( spl0_247
<=> ! [X0] : p2(X0,X0,X0) ),
introduced(definition,[new_symbols(definition,[spl0_247])],[avatar_definition]) ).
fof(f1246,plain,
( ! [X0] : p2(X0,X0,X0)
| ~ spl0_247 ),
inference(avatar_component_clause,[],[f1245]) ).
fof(f1247,plain,
( spl0_246
| spl0_247 ),
inference(avatar_split_clause,[],[f203,f1245,f1242]) ).
fof(f1298,definition,
( spl0_262
<=> ! [X2] : ~ p4(b,b,X2) ),
introduced(definition,[new_symbols(definition,[spl0_262])],[avatar_definition]) ).
fof(f1299,plain,
( ! [X2] : ~ p4(b,b,X2)
| ~ spl0_262 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1301,definition,
( spl0_263
<=> ! [X0,X1] :
( n5(X0,X0)
| ~ s1(X0)
| ~ p4(X1,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_263])],[avatar_definition]) ).
fof(f1302,plain,
( ! [X0,X1] :
( n5(X0,X0)
| ~ s1(X0)
| ~ p4(X1,X0,X0) )
| ~ spl0_263 ),
inference(avatar_component_clause,[],[f1301]) ).
fof(f1303,plain,
( spl0_262
| spl0_263 ),
inference(avatar_split_clause,[],[f354,f1301,f1298]) ).
fof(f1393,plain,
( $false
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f528,f1]) ).
fof(f1394,plain,
spl0_46,
inference(avatar_contradiction_clause,[],[f1393]) ).
fof(f1403,plain,
( $false
| ~ spl0_134 ),
inference(resolution,[],[f836,f20]) ).
fof(f1406,plain,
~ spl0_134,
inference(avatar_contradiction_clause,[],[f1403]) ).
fof(f1411,plain,
( $false
| spl0_152 ),
inference(forward_subsumption_resolution,[],[f902,f5]) ).
fof(f1412,plain,
spl0_152,
inference(avatar_contradiction_clause,[],[f1411]) ).
fof(f1413,plain,
( $false
| ~ spl0_220 ),
inference(resolution,[],[f1145,f9]) ).
fof(f1416,plain,
~ spl0_220,
inference(avatar_contradiction_clause,[],[f1413]) ).
fof(f1417,plain,
( $false
| ~ spl0_177 ),
inference(resolution,[],[f991,f14]) ).
fof(f1418,plain,
~ spl0_177,
inference(avatar_contradiction_clause,[],[f1417]) ).
fof(f1477,plain,
k1(b),
inference(resolution,[],[f39,f7]) ).
fof(f1483,plain,
k1(d),
inference(resolution,[],[f39,f34]) ).
fof(f1500,plain,
( ! [X0] : ~ p0(X0,X0)
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f163,f677]) ).
fof(f1501,plain,
( spl0_177
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f1500,f676,f990]) ).
fof(f1502,plain,
( ! [X2,X3,X0] :
( ~ s1(X2)
| ~ m0(X3,X2,X0) )
| ~ spl0_88
| ~ spl0_178 ),
inference(forward_subsumption_resolution,[],[f994,f674]) ).
fof(f1507,plain,
( ! [X0] : s1(X0)
| ~ spl0_176 ),
inference(resolution,[],[f987,f17]) ).
fof(f1511,plain,
( s1(a)
| ~ spl0_176 ),
inference(resolution,[],[f987,f36]) ).
fof(f1514,plain,
( $false
| ~ spl0_176
| spl0_186 ),
inference(forward_subsumption_resolution,[],[f1511,f1022]) ).
fof(f1515,plain,
( ~ spl0_176
| spl0_186 ),
inference(avatar_contradiction_clause,[],[f1514]) ).
fof(f1549,plain,
( ! [X0,X1] :
( ~ n0(X0,X1)
| ~ l0(X1) )
| ~ spl0_130 ),
inference(resolution,[],[f40,f822]) ).
fof(f1567,plain,
( ~ l0(c)
| ~ spl0_130 ),
inference(resolution,[],[f1549,f26]) ).
fof(f1575,plain,
( $false
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1567,f24]) ).
fof(f1576,plain,
~ spl0_130,
inference(avatar_contradiction_clause,[],[f1575]) ).
fof(f1578,plain,
( ~ r0(e)
| spl0_123 ),
inference(resolution,[],[f154,f798]) ).
fof(f1579,plain,
( $false
| spl0_123 ),
inference(forward_subsumption_resolution,[],[f1578,f13]) ).
fof(f1580,plain,
spl0_123,
inference(avatar_contradiction_clause,[],[f1579]) ).
fof(f1617,plain,
( ! [X2,X3,X0] : ~ m0(X3,X2,X0)
| ~ spl0_88
| ~ spl0_176
| ~ spl0_178 ),
inference(forward_subsumption_resolution,[],[f1502,f1507]) ).
fof(f1618,plain,
( $false
| ~ spl0_88
| ~ spl0_176
| ~ spl0_178 ),
inference(resolution,[],[f1617,f19]) ).
fof(f1637,plain,
( ~ spl0_88
| ~ spl0_176
| ~ spl0_178 ),
inference(avatar_contradiction_clause,[],[f1618]) ).
fof(f1638,plain,
( ! [X0] : ~ r2(X0)
| ~ spl0_8
| ~ spl0_90 ),
inference(forward_subsumption_resolution,[],[f680,f397]) ).
fof(f1639,plain,
( ! [X2,X3,X0] :
( ~ m0(X3,X2,X0)
| l2(X0,X0) )
| ~ spl0_176
| ~ spl0_178 ),
inference(forward_subsumption_resolution,[],[f994,f1507]) ).
fof(f1653,plain,
! [X0,X1] :
( ~ p0(X0,X1)
| n2(X1) ),
inference(resolution,[],[f123,f175]) ).
fof(f1682,plain,
! [X0] : n2(X0),
inference(resolution,[],[f1653,f14]) ).
fof(f1685,plain,
( ~ l1(d,d)
| ~ s2(d)
| ~ spl0_188 ),
inference(resolution,[],[f224,f1031]) ).
fof(f1686,plain,
( ~ l1(d,d)
| ~ spl0_106
| ~ spl0_188 ),
inference(forward_subsumption_resolution,[],[f1685,f1023]) ).
fof(f1695,plain,
( ~ k1(d)
| ~ spl0_106
| ~ spl0_131
| ~ spl0_188 ),
inference(resolution,[],[f1686,f825]) ).
fof(f1697,plain,
( $false
| ~ spl0_106
| ~ spl0_131
| ~ spl0_188 ),
inference(forward_subsumption_resolution,[],[f1695,f1483]) ).
fof(f1698,plain,
( ~ spl0_106
| ~ spl0_131
| ~ spl0_188 ),
inference(avatar_contradiction_clause,[],[f1697]) ).
fof(f1699,plain,
( ! [X0] : k3(X0,X0,X0)
| ~ spl0_176
| ~ spl0_189 ),
inference(forward_subsumption_resolution,[],[f1034,f1507]) ).
fof(f1704,plain,
! [X0] :
( ~ l2(X0,X0)
| l4(X0) ),
inference(resolution,[],[f284,f315]) ).
fof(f1743,plain,
( ! [X0] : l2(X0,X0)
| ~ spl0_176
| ~ spl0_178 ),
inference(resolution,[],[f1639,f19]) ).
fof(f1762,plain,
( ! [X0] : l4(X0)
| ~ spl0_176
| ~ spl0_178 ),
inference(resolution,[],[f1743,f1704]) ).
fof(f1818,plain,
( ! [X0,X1] : ~ k3(X0,X0,X1)
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f325,f504]) ).
fof(f1821,plain,
( ! [X0] : ~ n2(X0)
| ~ spl0_39 ),
inference(resolution,[],[f1818,f248]) ).
fof(f1825,plain,
( $false
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1821,f1682]) ).
fof(f1826,plain,
~ spl0_39,
inference(avatar_contradiction_clause,[],[f1825]) ).
fof(f1848,plain,
( ! [X0,X1] :
( p4(X0,X0,X0)
| ~ n0(X0,X1) )
| ~ spl0_40
| ~ spl0_176
| ~ spl0_178 ),
inference(forward_subsumption_resolution,[],[f507,f1762]) ).
fof(f1849,plain,
( ! [X0] : ~ n0(b,X0)
| ~ spl0_40
| ~ spl0_176
| ~ spl0_178
| ~ spl0_262 ),
inference(resolution,[],[f1848,f1299]) ).
fof(f1850,plain,
( $false
| ~ spl0_40
| ~ spl0_176
| ~ spl0_178
| ~ spl0_262 ),
inference(resolution,[],[f1849,f37]) ).
fof(f1851,plain,
( ~ spl0_40
| ~ spl0_176
| ~ spl0_178
| ~ spl0_262 ),
inference(avatar_contradiction_clause,[],[f1850]) ).
fof(f1852,plain,
( ! [X0,X1] :
( ~ p4(X1,X0,X0)
| n5(X0,X0) )
| ~ spl0_176
| ~ spl0_263 ),
inference(forward_subsumption_resolution,[],[f1302,f1507]) ).
fof(f1865,plain,
( ! [X0] :
( ~ k3(X0,X0,X0)
| n5(X0,X0) )
| ~ spl0_176
| ~ spl0_263 ),
inference(resolution,[],[f325,f1852]) ).
fof(f1866,plain,
( ! [X0] : n5(X0,X0)
| ~ spl0_176
| ~ spl0_189
| ~ spl0_263 ),
inference(forward_subsumption_resolution,[],[f1865,f1699]) ).
fof(f1887,plain,
( ! [X0,X1] :
( ~ n1(X0,d,X1)
| ~ l1(X0,X1) )
| ~ spl0_119 ),
inference(resolution,[],[f784,f224]) ).
fof(f1954,plain,
( ~ q1(e,e,e)
| ~ n1(e,e,e)
| ~ spl0_246 ),
inference(resolution,[],[f1243,f208]) ).
fof(f1959,plain,
( ~ spl0_241
| ~ spl0_123
| ~ spl0_246 ),
inference(avatar_split_clause,[],[f1954,f1242,f797,f1225]) ).
fof(f1971,plain,
( ! [X0] : n3(X0)
| ~ spl0_247 ),
inference(resolution,[],[f1246,f278]) ).
fof(f2055,plain,
( ! [X0] :
( ~ r1(X0)
| ~ l0(X0) )
| ~ spl0_8
| ~ spl0_90 ),
inference(forward_subsumption_resolution,[],[f226,f1638]) ).
fof(f2057,plain,
( ! [X0,X1] :
( r1(X0)
| ~ q0(X0,d)
| ~ q0(X1,d) )
| ~ spl0_47 ),
inference(resolution,[],[f531,f131]) ).
fof(f2079,plain,
( ! [X0,X1] :
( r1(X0)
| ~ q0(X1,d) )
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f2057,f17]) ).
fof(f2086,definition,
( spl0_300
<=> ! [X0] : r1(X0) ),
introduced(definition,[new_symbols(definition,[spl0_300])],[avatar_definition]) ).
fof(f2087,plain,
( ! [X0] : r1(X0)
| ~ spl0_300 ),
inference(avatar_component_clause,[],[f2086]) ).
fof(f2111,plain,
( ! [X0] : r1(X0)
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f2079,f17]) ).
fof(f2116,plain,
( spl0_300
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f2111,f530,f2086]) ).
fof(f2117,plain,
( ! [X0] : ~ l0(X0)
| ~ spl0_8
| ~ spl0_90
| ~ spl0_300 ),
inference(resolution,[],[f2087,f2055]) ).
fof(f2124,plain,
( spl0_134
| ~ spl0_8
| ~ spl0_90
| ~ spl0_300 ),
inference(avatar_split_clause,[],[f2117,f2086,f679,f396,f835]) ).
fof(f2126,plain,
( ! [X0] : p4(X0,X0,X0)
| ~ spl0_93
| ~ spl0_247 ),
inference(forward_subsumption_resolution,[],[f691,f1971]) ).
fof(f2167,plain,
( ! [X0,X1] :
( n1(X0,X1,X0)
| ~ l0(X0) )
| ~ spl0_216 ),
inference(forward_subsumption_resolution,[],[f1130,f14]) ).
fof(f2209,plain,
( ! [X0] :
( ~ l1(X0,X0)
| ~ l0(X0) )
| ~ spl0_119
| ~ spl0_216 ),
inference(resolution,[],[f1887,f2167]) ).
fof(f2212,plain,
( spl0_130
| ~ spl0_119
| ~ spl0_216 ),
inference(avatar_split_clause,[],[f2209,f1129,f783,f821]) ).
fof(f2274,plain,
! [X0,X1] :
( q3(X0,X1)
| ~ n0(X0,X0)
| ~ l1(X1,X0) ),
inference(resolution,[],[f293,f224]) ).
fof(f2367,plain,
( l1(b,e)
| ~ p0(c,b)
| ~ spl0_221 ),
inference(resolution,[],[f1148,f27]) ).
fof(f2407,plain,
( l1(b,e)
| ~ spl0_221 ),
inference(forward_subsumption_resolution,[],[f2367,f18]) ).
fof(f2417,plain,
( ! [X0,X1] :
( l2(X0,X1)
| ~ n0(e,X1)
| ~ l2(X1,X1) )
| ~ spl0_176 ),
inference(forward_subsumption_resolution,[],[f169,f1507]) ).
fof(f2418,plain,
( ! [X0,X1] :
( l2(X0,X1)
| ~ n0(e,X1) )
| ~ spl0_176
| ~ spl0_178 ),
inference(forward_subsumption_resolution,[],[f2417,f1743]) ).
fof(f2422,plain,
( ~ n0(e,b)
| spl0_112
| ~ spl0_176
| ~ spl0_178 ),
inference(resolution,[],[f2418,f759]) ).
fof(f2427,plain,
( $false
| spl0_112
| ~ spl0_176
| ~ spl0_178 ),
inference(forward_subsumption_resolution,[],[f2422,f11]) ).
fof(f2428,plain,
( spl0_112
| ~ spl0_176
| ~ spl0_178 ),
inference(avatar_contradiction_clause,[],[f2427]) ).
fof(f2780,plain,
( ~ r0(e)
| spl0_241 ),
inference(resolution,[],[f1226,f95]) ).
fof(f2792,plain,
( $false
| spl0_241 ),
inference(forward_subsumption_resolution,[],[f2780,f13]) ).
fof(f2793,plain,
spl0_241,
inference(avatar_contradiction_clause,[],[f2792]) ).
fof(f2948,plain,
( ! [X0] :
( n4(X0,X0)
| ~ n2(X0) )
| ~ spl0_82
| ~ spl0_196 ),
inference(resolution,[],[f1059,f650]) ).
fof(f2965,plain,
( ! [X0] : n4(X0,X0)
| ~ spl0_82
| ~ spl0_196 ),
inference(forward_subsumption_resolution,[],[f2948,f1682]) ).
fof(f3036,plain,
( ! [X2,X0,X1] :
( ~ k3(X0,X0,X1)
| ~ q2(b,X2,X1)
| q4(X1,X2) )
| ~ spl0_113 ),
inference(resolution,[],[f333,f762]) ).
fof(f3079,plain,
( ~ n0(e,e)
| ~ l1(b,e)
| spl0_170 ),
inference(resolution,[],[f2274,f966]) ).
fof(f3083,plain,
( ~ l1(b,e)
| spl0_170 ),
inference(forward_subsumption_resolution,[],[f3079,f30]) ).
fof(f3084,plain,
( $false
| spl0_170
| ~ spl0_221 ),
inference(forward_subsumption_resolution,[],[f3083,f2407]) ).
fof(f3085,plain,
( spl0_170
| ~ spl0_221 ),
inference(avatar_contradiction_clause,[],[f3084]) ).
fof(f3086,plain,
( $false
| spl0_169
| ~ spl0_247 ),
inference(forward_subsumption_resolution,[],[f963,f1971]) ).
fof(f3087,plain,
( spl0_169
| ~ spl0_247 ),
inference(avatar_contradiction_clause,[],[f3086]) ).
fof(f3088,plain,
( $false
| spl0_171 ),
inference(forward_subsumption_resolution,[],[f969,f34]) ).
fof(f3089,plain,
spl0_171,
inference(avatar_contradiction_clause,[],[f3088]) ).
fof(f3090,plain,
( $false
| ~ spl0_172
| ~ spl0_195 ),
inference(forward_subsumption_resolution,[],[f972,f1056]) ).
fof(f3091,plain,
( ~ spl0_172
| ~ spl0_195 ),
inference(avatar_contradiction_clause,[],[f3090]) ).
fof(f3127,plain,
( ! [X2,X3,X0,X1] :
( ~ q4(X0,X1)
| ~ n4(X2,X1)
| n5(X2,X3)
| ~ n5(X3,X3) )
| ~ spl0_93
| ~ spl0_247 ),
inference(resolution,[],[f345,f2126]) ).
fof(f3138,plain,
( ! [X2,X3,X0,X1] :
( n5(X2,X3)
| ~ n4(X2,X1)
| ~ q4(X0,X1) )
| ~ spl0_93
| ~ spl0_176
| ~ spl0_189
| ~ spl0_247
| ~ spl0_263 ),
inference(forward_subsumption_resolution,[],[f3127,f1866]) ).
fof(f3192,plain,
( ! [X0,X1] :
( ~ q4(X1,X0)
| ~ n4(a,X0) )
| ~ spl0_93
| ~ spl0_176
| ~ spl0_189
| ~ spl0_247
| ~ spl0_263 ),
inference(resolution,[],[f3138,f369]) ).
fof(f3514,plain,
( ! [X0,X1] :
( ~ q2(b,X0,X1)
| q4(X1,X0) )
| ~ spl0_113
| ~ spl0_176
| ~ spl0_189 ),
inference(resolution,[],[f3036,f1699]) ).
fof(f3790,plain,
( q4(b,b)
| ~ k1(b)
| ~ spl0_113
| ~ spl0_120
| ~ spl0_176
| ~ spl0_189 ),
inference(resolution,[],[f3514,f787]) ).
fof(f3813,plain,
( q4(b,b)
| ~ spl0_113
| ~ spl0_120
| ~ spl0_176
| ~ spl0_189 ),
inference(forward_subsumption_resolution,[],[f3790,f1477]) ).
fof(f3822,plain,
( spl0_168
| ~ spl0_113
| ~ spl0_120
| ~ spl0_176
| ~ spl0_189 ),
inference(avatar_split_clause,[],[f3813,f1033,f986,f786,f761,f958]) ).
fof(f3824,plain,
( ~ l4(b)
| ~ spl0_164
| ~ spl0_168 ),
inference(resolution,[],[f959,f946]) ).
fof(f3825,plain,
( $false
| ~ spl0_164
| ~ spl0_168
| ~ spl0_176
| ~ spl0_178 ),
inference(forward_subsumption_resolution,[],[f3824,f1762]) ).
fof(f3826,plain,
( ~ spl0_164
| ~ spl0_168
| ~ spl0_176
| ~ spl0_178 ),
inference(avatar_contradiction_clause,[],[f3825]) ).
fof(f3827,plain,
( ! [X0] : q4(X0,X0)
| ~ spl0_165
| ~ spl0_300 ),
inference(forward_subsumption_resolution,[],[f949,f2087]) ).
fof(f3829,plain,
( ! [X0] : ~ n4(a,X0)
| ~ spl0_93
| ~ spl0_165
| ~ spl0_176
| ~ spl0_189
| ~ spl0_247
| ~ spl0_263
| ~ spl0_300 ),
inference(resolution,[],[f3827,f3192]) ).
fof(f3830,plain,
( $false
| ~ spl0_82
| ~ spl0_93
| ~ spl0_165
| ~ spl0_176
| ~ spl0_189
| ~ spl0_196
| ~ spl0_247
| ~ spl0_263
| ~ spl0_300 ),
inference(resolution,[],[f3829,f2965]) ).
fof(f3832,plain,
( ~ spl0_82
| ~ spl0_93
| ~ spl0_165
| ~ spl0_176
| ~ spl0_189
| ~ spl0_196
| ~ spl0_247
| ~ spl0_263
| ~ spl0_300 ),
inference(avatar_contradiction_clause,[],[f3830]) ).
cnf(s18,plain,
( spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f508]) ).
cnf(s21,plain,
( ~ spl0_46
| spl0_47 ),
inference(sat_conversion,[],[f532]) ).
cnf(s39,plain,
spl0_82,
inference(sat_conversion,[],[f671]) ).
cnf(s40,plain,
( spl0_88
| spl0_89
| spl0_90 ),
inference(sat_conversion,[],[f681]) ).
cnf(s42,plain,
( spl0_8
| spl0_93 ),
inference(sat_conversion,[],[f692]) ).
cnf(s52,plain,
( ~ spl0_112
| spl0_113 ),
inference(sat_conversion,[],[f763]) ).
cnf(s56,plain,
( spl0_119
| spl0_120 ),
inference(sat_conversion,[],[f788]) ).
cnf(s61,plain,
( spl0_130
| spl0_131 ),
inference(sat_conversion,[],[f826]) ).
cnf(s83,plain,
( spl0_164
| spl0_165 ),
inference(sat_conversion,[],[f950]) ).
cnf(s85,plain,
( ~ spl0_169
| ~ spl0_170
| ~ spl0_171
| spl0_172 ),
inference(sat_conversion,[],[f973]) ).
cnf(s88,plain,
( spl0_89
| spl0_176 ),
inference(sat_conversion,[],[f988]) ).
cnf(s89,plain,
( spl0_177
| spl0_178 ),
inference(sat_conversion,[],[f995]) ).
cnf(s93,plain,
( ~ spl0_46
| spl0_106
| ~ spl0_186 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s95,plain,
( spl0_188
| spl0_189 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s98,plain,
( spl0_195
| spl0_196 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s109,plain,
( ~ spl0_152
| spl0_216 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s112,plain,
( spl0_220
| spl0_221 ),
inference(sat_conversion,[],[f1149]) ).
cnf(s132,plain,
( spl0_246
| spl0_247 ),
inference(sat_conversion,[],[f1247]) ).
cnf(s140,plain,
( spl0_262
| spl0_263 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s155,plain,
spl0_46,
inference(sat_conversion,[],[f1394]) ).
cnf(s161,plain,
~ spl0_134,
inference(sat_conversion,[],[f1406]) ).
cnf(s164,plain,
spl0_152,
inference(sat_conversion,[],[f1412]) ).
cnf(s166,plain,
~ spl0_220,
inference(sat_conversion,[],[f1416]) ).
cnf(s167,plain,
~ spl0_177,
inference(sat_conversion,[],[f1418]) ).
cnf(s204,plain,
( ~ spl0_89
| spl0_177 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s206,plain,
( ~ spl0_176
| spl0_186 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s227,plain,
~ spl0_130,
inference(sat_conversion,[],[f1576]) ).
cnf(s229,plain,
spl0_123,
inference(sat_conversion,[],[f1580]) ).
cnf(s249,plain,
( ~ spl0_88
| ~ spl0_176
| ~ spl0_178 ),
inference(sat_conversion,[],[f1637]) ).
cnf(s254,plain,
( ~ spl0_106
| ~ spl0_131
| ~ spl0_188 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s272,plain,
~ spl0_39,
inference(sat_conversion,[],[f1826]) ).
cnf(s283,plain,
( ~ spl0_40
| ~ spl0_176
| ~ spl0_178
| ~ spl0_262 ),
inference(sat_conversion,[],[f1851]) ).
cnf(s293,plain,
( ~ spl0_123
| ~ spl0_241
| ~ spl0_246 ),
inference(sat_conversion,[],[f1959]) ).
cnf(s314,plain,
( ~ spl0_47
| spl0_300 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s318,plain,
( ~ spl0_8
| ~ spl0_90
| spl0_134
| ~ spl0_300 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s326,plain,
( ~ spl0_119
| spl0_130
| ~ spl0_216 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s340,plain,
( spl0_112
| ~ spl0_176
| ~ spl0_178 ),
inference(sat_conversion,[],[f2428]) ).
cnf(s380,plain,
spl0_241,
inference(sat_conversion,[],[f2793]) ).
cnf(s413,plain,
( spl0_170
| ~ spl0_221 ),
inference(sat_conversion,[],[f3085]) ).
cnf(s414,plain,
( spl0_169
| ~ spl0_247 ),
inference(sat_conversion,[],[f3087]) ).
cnf(s415,plain,
spl0_171,
inference(sat_conversion,[],[f3089]) ).
cnf(s416,plain,
( ~ spl0_172
| ~ spl0_195 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s513,plain,
( ~ spl0_113
| ~ spl0_120
| spl0_168
| ~ spl0_176
| ~ spl0_189 ),
inference(sat_conversion,[],[f3822]) ).
cnf(s514,plain,
( ~ spl0_164
| ~ spl0_168
| ~ spl0_176
| ~ spl0_178 ),
inference(sat_conversion,[],[f3826]) ).
cnf(s515,plain,
( ~ spl0_82
| ~ spl0_93
| ~ spl0_165
| ~ spl0_176
| ~ spl0_189
| ~ spl0_196
| ~ spl0_247
| ~ spl0_263
| ~ spl0_300 ),
inference(sat_conversion,[],[f3832]) ).
cnf(s530,plain,
( ~ spl0_123
| ~ spl0_246 ),
inference(rat,[],[s293,s380]) ).
cnf(s531,plain,
~ spl0_246,
inference(rat,[],[s530,s229]) ).
cnf(s534,plain,
~ spl0_89,
inference(rat,[],[s204,s167]) ).
cnf(s547,plain,
spl0_247,
inference(rat,[],[s132,s531]) ).
cnf(s548,plain,
spl0_169,
inference(rat,[],[s414,s547]) ).
cnf(s570,plain,
spl0_221,
inference(rat,[],[s112,s166]) ).
cnf(s571,plain,
spl0_170,
inference(rat,[],[s413,s570]) ).
cnf(s579,plain,
spl0_216,
inference(rat,[],[s109,s164]) ).
cnf(s581,plain,
~ spl0_119,
inference(rat,[],[s326,s227,s579]) ).
cnf(s590,plain,
( spl0_106
| ~ spl0_186 ),
inference(rat,[],[s93,s155]) ).
cnf(s592,plain,
spl0_178,
inference(rat,[],[s89,s167]) ).
cnf(s593,plain,
spl0_176,
inference(rat,[],[s88,s534]) ).
cnf(s597,plain,
spl0_112,
inference(rat,[],[s340,s592,s593]) ).
cnf(s600,plain,
~ spl0_88,
inference(rat,[],[s249,s592,s593]) ).
cnf(s601,plain,
spl0_186,
inference(rat,[],[s206,s593]) ).
cnf(s603,plain,
spl0_106,
inference(rat,[],[s590,s601]) ).
cnf(s608,plain,
spl0_172,
inference(rat,[],[s85,s415,s571,s548]) ).
cnf(s609,plain,
~ spl0_195,
inference(rat,[],[s416,s608]) ).
cnf(s610,plain,
spl0_196,
inference(rat,[],[s98,s609]) ).
cnf(s634,plain,
spl0_131,
inference(rat,[],[s61,s227]) ).
cnf(s637,plain,
~ spl0_188,
inference(rat,[],[s254,s603,s634]) ).
cnf(s640,plain,
spl0_189,
inference(rat,[],[s95,s637]) ).
cnf(s646,plain,
spl0_120,
inference(rat,[],[s56,s581]) ).
cnf(s650,plain,
spl0_113,
inference(rat,[],[s52,s597]) ).
cnf(s651,plain,
spl0_168,
inference(rat,[],[s513,s640,s593,s646,s650]) ).
cnf(s652,plain,
~ spl0_164,
inference(rat,[],[s514,s592,s593,s651]) ).
cnf(s653,plain,
spl0_165,
inference(rat,[],[s83,s652]) ).
cnf(s661,plain,
spl0_90,
inference(rat,[],[s40,s534,s600]) ).
cnf(s676,plain,
spl0_47,
inference(rat,[],[s21,s155]) ).
cnf(s677,plain,
spl0_300,
inference(rat,[],[s314,s676]) ).
cnf(s686,plain,
~ spl0_8,
inference(rat,[],[s318,s661,s161,s677]) ).
cnf(s691,plain,
spl0_93,
inference(rat,[],[s42,s686]) ).
cnf(s694,plain,
~ spl0_263,
inference(rat,[],[s515,s677,s39,s547,s610,s640,s593,s653,s691]) ).
cnf(s695,plain,
spl0_262,
inference(rat,[],[s140,s694]) ).
cnf(s696,plain,
~ spl0_40,
inference(rat,[],[s283,s593,s592,s695]) ).
cnf(s698,plain,
$false,
inference(rat,[],[s18,s696,s272]) ).
fof(f3833,plain,
$false,
inference(avatar_sat_refutation,[],[s698]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN159-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n011.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 15:37:30 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 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
% 3.55/1.16 % (3475719)Input is clausal, will run a generic CNF schedule.
% 3.55/1.16 % (3475861)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=1095990823:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.55/1.16 % (3475862)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2710151647:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.55/1.16 % (3475866)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1677590999:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.55/1.16 % (3475871)dis-21_1_sil=8000:lcm=predicate:random_seed=2782776739: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)
% 3.55/1.16 % (3475865)lrs+10_1_sil=8000:sp=occurrence:random_seed=3247224888:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.55/1.16 % (3475868)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3074892429:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.55/1.16 % (3475863)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2578417435:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.55/1.16 % (3475865)Refutation not found, incomplete strategy
% 3.55/1.16 % (3475865)------------------------------
% 3.55/1.16 % (3475865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.55/1.16 % (3475865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.55/1.16 % (3475865)CaDiCaL version: 2.1.3
% 3.55/1.16 % (3475865)Termination reason: Refutation not found, incomplete strategy
% 3.55/1.16 % (3475865)Time elapsed: 0.032 s
% 3.55/1.16 % (3475865)Peak memory usage: 89 MB
% 3.55/1.16 % (3475865)Instructions burned: 49 (million)
% 3.55/1.16 % (3475866)First to succeed.
% 3.55/1.16 % (3475866)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3475719"
% 3.55/1.16 % (3475868)Also succeeded, but the first one will report.
% 3.55/1.16 % (3475871)Instruction limit reached!
% 3.55/1.16 % (3475871)------------------------------
% 3.55/1.16 % (3475871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.55/1.16 % (3475871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.55/1.16 % (3475871)CaDiCaL version: 2.1.3
% 3.55/1.16 % (3475871)Termination reason: Instruction limit
% 3.55/1.16 % (3475871)Termination phase: Saturation
% 3.55/1.16 % (3475871)Time elapsed: 0.056 s
% 3.55/1.16 % (3475871)Peak memory usage: 89 MB
% 3.55/1.16 % (3475871)Instructions burned: 118 (million)
% 3.55/1.16 % (3475929)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=2422355674:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.55/1.16 % (3475929)Refutation not found, incomplete strategy
% 3.55/1.16 % (3475929)------------------------------
% 3.55/1.16 % (3475929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.55/1.16 % (3475929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.55/1.16 % (3475929)CaDiCaL version: 2.1.3
% 3.55/1.16 % (3475929)Termination reason: Refutation not found, incomplete strategy
% 3.55/1.16 % (3475929)Time elapsed: 0.002 s
% 3.55/1.16 % (3475929)Peak memory usage: 88 MB
% 3.55/1.16 % (3475929)Instructions burned: 2 (million)
% 3.55/1.16 % (3475865)------------------------------
% 3.55/1.16 % (3475865)------------------------------
% 3.55/1.16 % (3475866)Refutation found. Thanks to Tanya!
% 3.55/1.16 % SZS status Unsatisfiable for theBenchmark
% 3.55/1.16 % SZS output start Proof for theBenchmark
% See solution above
% 3.93/1.36 % (3475866)------------------------------
% 3.93/1.36 % (3475866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.93/1.36 % (3475866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.93/1.36 % (3475866)CaDiCaL version: 2.1.3
% 3.93/1.36 % (3475866)Termination reason: Refutation
% 3.93/1.36 % (3475866)Time elapsed: 0.046 s
% 3.93/1.36 % (3475866)Peak memory usage: 91 MB
% 3.93/1.36 % (3475866)Instructions burned: 71 (million)
% 3.93/1.36 % (3475866)------------------------------
% 3.93/1.36 % (3475866)------------------------------
% 3.93/1.36 % (3475719)Success in time 0.471 s
% 3.93/1.36 % Vampire exiting
%------------------------------------------------------------------------------