%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN156-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 : n019.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:47 PM UTC 2026
% Result : Unsatisfiable 3.09s 1.11s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 94
% Syntax : Number of formulae : 347 ( 88 unt; 48 def)
% Number of atoms : 797 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 879 ( 429 ~; 402 |; 0 &)
% ( 48 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 75 ( 74 usr; 49 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 168 ( 0 sgn 168 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
s0(d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(f2,axiom,
q0(e,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(f3,axiom,
n0(d,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
fof(f7,axiom,
n0(d,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
fof(f11,axiom,
n0(e,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_11) ).
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(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(f28,axiom,
k0(e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_28) ).
fof(f31,axiom,
m0(b,b,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_31) ).
fof(f32,axiom,
k0(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_32) ).
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(f39,axiom,
! [X0,X1] :
( k1(X0)
| ~ n0(X1,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(f42,axiom,
! [X0,X1] :
( l1(X0,X0)
| ~ k1(X0)
| ~ l0(X1)
| ~ l1(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_004) ).
fof(f59,axiom,
! [X0,X1] :
( m1(X0,X1,X0)
| ~ l0(X0)
| ~ k0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_021) ).
fof(f74,axiom,
! [X0,X1] :
( ~ m0(b,X1,X0)
| n1(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_036) ).
fof(f106,axiom,
! [X0] :
( p1(X0,X0,X0)
| ~ k0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_068) ).
fof(f145,axiom,
! [X0] :
( q1(e,X0,X0)
| ~ m0(X0,d,X0)
| ~ m0(e,d,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_107) ).
fof(f155,axiom,
( q1(d,d,d)
| ~ k0(e)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_117) ).
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(f175,axiom,
! [X2,X0,X1] :
( n2(X0)
| ~ p1(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_137) ).
fof(f192,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ q1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_154) ).
fof(f193,axiom,
! [X2,X0,X1] :
( p2(X0,X1,X1)
| ~ k1(X2)
| ~ p2(e,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_155) ).
fof(f214,axiom,
! [X0,X1] :
( p2(X0,X1,X0)
| ~ m1(X1,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_176) ).
fof(f224,axiom,
! [X0,X1] :
( ~ l1(X1,X0)
| q2(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_186) ).
fof(f225,axiom,
! [X2,X3,X0,X1] :
( ~ k0(X1)
| ~ r1(X1)
| ~ m0(X2,X3,X0)
| q2(X0,X1,X0)
| ~ q2(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_187) ).
fof(f226,axiom,
! [X0] :
( ~ l0(X0)
| ~ r1(X0)
| r2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_188) ).
fof(f227,axiom,
! [X0] :
( s2(X0)
| ~ q2(b,X0,b)
| ~ s1(b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_189) ).
fof(f228,axiom,
( s2(d)
| ~ s1(a)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_190) ).
fof(f265,axiom,
! [X2,X3,X0,X1] :
( m3(X0,X0,X0)
| ~ q0(X1,X2)
| ~ s0(X3)
| ~ s2(X2)
| ~ r2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_227) ).
fof(f274,axiom,
! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_236) ).
fof(f278,axiom,
! [X2,X0,X1] :
( n3(X0)
| ~ p2(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_240) ).
fof(f289,axiom,
! [X2,X3,X0,X1] :
( p3(X0,X1,X1)
| ~ m3(X1,X2,X3)
| ~ p2(X0,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_251) ).
fof(f293,axiom,
! [X2,X0,X1] :
( q3(X0,X1)
| ~ q2(X2,X0,X1)
| ~ n0(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_255) ).
fof(f295,axiom,
! [X2,X0,X1] :
( q3(X0,X1)
| ~ n1(X2,X0,X1)
| ~ s2(X0)
| ~ q3(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_257) ).
fof(f312,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_274) ).
fof(f319,axiom,
! [X0,X1] :
( ~ n4(X0,X0)
| ~ p3(X0,X1,X1)
| n4(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_281) ).
fof(f322,axiom,
! [X0,X1] :
( n4(X0,X0)
| ~ k4(X1)
| ~ m3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_284) ).
fof(f369,negated_conjecture,
~ n4(a,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f510,definition,
( spl0_37
<=> ! [X1] : ~ k4(X1) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f511,plain,
( ! [X1] : ~ k4(X1)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f513,definition,
( spl0_38
<=> ! [X0] :
( n4(X0,X0)
| ~ m3(X0,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f514,plain,
( ! [X0] :
( n4(X0,X0)
| ~ m3(X0,X0,X0) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( spl0_37
| spl0_38 ),
inference(avatar_split_clause,[],[f322,f513,f510]) ).
fof(f530,definition,
( spl0_42
<=> q1(d,d,d) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f531,plain,
( q1(d,d,d)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f551,definition,
( spl0_47
<=> n3(e) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f553,plain,
( ~ n3(e)
| spl0_47 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f555,definition,
( spl0_48
<=> q3(e,b) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f557,plain,
( ~ q3(e,b)
| spl0_48 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f559,definition,
( spl0_49
<=> n0(c,d) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f563,definition,
( spl0_50
<=> k4(c) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f565,plain,
( k4(c)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f566,plain,
( ~ spl0_47
| ~ spl0_48
| ~ spl0_49
| spl0_50 ),
inference(avatar_split_clause,[],[f312,f563,f559,f555,f551]) ).
fof(f602,definition,
( spl0_60
<=> ! [X1] : ~ s1(X1) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f603,plain,
( ! [X1] : ~ s1(X1)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f662,definition,
( spl0_75
<=> n2(e) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f663,plain,
( n2(e)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f664,plain,
( ~ n2(e)
| spl0_75 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f673,definition,
( spl0_78
<=> ! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f674,plain,
( ! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) )
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f699,definition,
( spl0_84
<=> ! [X3] : ~ s0(X3) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f700,plain,
( ! [X3] : ~ s0(X3)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f702,definition,
( spl0_85
<=> ! [X2,X1] :
( ~ q0(X1,X2)
| ~ s2(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f703,plain,
( ! [X2,X1] :
( ~ s2(X2)
| ~ q0(X1,X2) )
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f705,definition,
( spl0_86
<=> ! [X0] :
( m3(X0,X0,X0)
| ~ r2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f706,plain,
( ! [X0] :
( ~ r2(X0)
| m3(X0,X0,X0) )
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f707,plain,
( spl0_84
| spl0_85
| spl0_86 ),
inference(avatar_split_clause,[],[f265,f705,f702,f699]) ).
fof(f725,definition,
( spl0_91
<=> s2(d) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f726,plain,
( s2(d)
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f813,definition,
( spl0_113
<=> r2(a) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f814,plain,
( r2(a)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f855,definition,
( spl0_123
<=> s2(e) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f856,plain,
( s2(e)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f855]) ).
fof(f876,definition,
( spl0_128
<=> s0(d) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f877,plain,
( s0(d)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f880,definition,
( spl0_129
<=> s1(a) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f882,plain,
( ~ s1(a)
| spl0_129 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f883,plain,
( ~ spl0_128
| ~ spl0_129
| spl0_91 ),
inference(avatar_split_clause,[],[f228,f725,f880,f876]) ).
fof(f885,definition,
( spl0_130
<=> s1(b) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f889,definition,
( spl0_131
<=> ! [X0] :
( s2(X0)
| ~ q2(b,X0,b) ) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f890,plain,
( ! [X0] :
( ~ q2(b,X0,b)
| s2(X0) )
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f889]) ).
fof(f891,plain,
( ~ spl0_130
| spl0_131 ),
inference(avatar_split_clause,[],[f227,f889,f885]) ).
fof(f896,definition,
( spl0_133
<=> ! [X0] :
( q2(X0,X0,X0)
| ~ k1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f897,plain,
( ! [X0] :
( q2(X0,X0,X0)
| ~ k1(X0) )
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f900,definition,
( spl0_134
<=> l0(c) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f901,plain,
( l0(c)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f967,definition,
( spl0_151
<=> r1(e) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f969,plain,
( ~ r1(e)
| spl0_151 ),
inference(avatar_component_clause,[],[f967]) ).
fof(f1026,definition,
( spl0_166
<=> ! [X2] : ~ k1(X2) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1027,plain,
( ! [X2] : ~ k1(X2)
| ~ spl0_166 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1029,definition,
( spl0_167
<=> ! [X0,X1] :
( p2(X0,X1,X1)
| ~ p2(e,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1030,plain,
( ! [X0,X1] :
( p2(X0,X1,X1)
| ~ p2(e,X0,X1) )
| ~ spl0_167 ),
inference(avatar_component_clause,[],[f1029]) ).
fof(f1031,plain,
( spl0_166
| spl0_167 ),
inference(avatar_split_clause,[],[f193,f1029,f1026]) ).
fof(f1042,definition,
( spl0_170
<=> r1(a) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1043,plain,
( r1(a)
| ~ spl0_170 ),
inference(avatar_component_clause,[],[f1042]) ).
fof(f1044,plain,
( ~ r1(a)
| spl0_170 ),
inference(avatar_component_clause,[],[f1042]) ).
fof(f1094,definition,
( spl0_183
<=> r1(b) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1095,plain,
( r1(b)
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1096,plain,
( ~ r1(b)
| spl0_183 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1099,definition,
( spl0_184
<=> k0(b) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f1100,plain,
( k0(b)
| ~ spl0_184 ),
inference(avatar_component_clause,[],[f1099]) ).
fof(f1129,definition,
( spl0_191
<=> k1(b) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f1130,plain,
( k1(b)
| ~ spl0_191 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1131,plain,
( ~ k1(b)
| spl0_191 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1141,definition,
( spl0_194
<=> ! [X1] : ~ p0(X1,X1) ),
introduced(definition,[new_symbols(definition,[spl0_194])],[avatar_definition]) ).
fof(f1142,plain,
( ! [X1] : ~ p0(X1,X1)
| ~ spl0_194 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1148,definition,
( spl0_196
<=> l1(e,e) ),
introduced(definition,[new_symbols(definition,[spl0_196])],[avatar_definition]) ).
fof(f1149,plain,
( l1(e,e)
| ~ spl0_196 ),
inference(avatar_component_clause,[],[f1148]) ).
fof(f1150,plain,
( ~ l1(e,e)
| spl0_196 ),
inference(avatar_component_clause,[],[f1148]) ).
fof(f1157,definition,
( spl0_198
<=> ! [X0,X1] :
( s1(X0)
| ~ q0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_198])],[avatar_definition]) ).
fof(f1158,plain,
( ! [X0,X1] :
( s1(X0)
| ~ q0(X0,X1) )
| ~ spl0_198 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1159,plain,
( spl0_60
| spl0_198 ),
inference(avatar_split_clause,[],[f164,f1157,f602]) ).
fof(f1161,definition,
( spl0_199
<=> ! [X0,X1] :
( r1(X0)
| ~ q1(d,X1,d)
| ~ q0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_199])],[avatar_definition]) ).
fof(f1162,plain,
( ! [X0,X1] :
( r1(X0)
| ~ q1(d,X1,d)
| ~ q0(X0,X1) )
| ~ spl0_199 ),
inference(avatar_component_clause,[],[f1161]) ).
fof(f1163,plain,
( ~ spl0_128
| spl0_199 ),
inference(avatar_split_clause,[],[f162,f1161,f876]) ).
fof(f1186,definition,
( spl0_205
<=> k0(e) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f1187,plain,
( k0(e)
| ~ spl0_205 ),
inference(avatar_component_clause,[],[f1186]) ).
fof(f1189,plain,
( ~ spl0_128
| ~ spl0_205
| spl0_42 ),
inference(avatar_split_clause,[],[f155,f530,f1186,f876]) ).
fof(f1276,definition,
( spl0_227
<=> l0(a) ),
introduced(definition,[new_symbols(definition,[spl0_227])],[avatar_definition]) ).
fof(f1277,plain,
( l0(a)
| ~ spl0_227 ),
inference(avatar_component_clause,[],[f1276]) ).
fof(f1336,definition,
( spl0_241
<=> n0(e,b) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1337,plain,
( n0(e,b)
| ~ spl0_241 ),
inference(avatar_component_clause,[],[f1336]) ).
fof(f1340,definition,
( spl0_242
<=> ! [X0] :
( p1(X0,X0,X0)
| ~ k0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f1341,plain,
( ! [X0] :
( p1(X0,X0,X0)
| ~ k0(X0) )
| ~ spl0_242 ),
inference(avatar_component_clause,[],[f1340]) ).
fof(f1360,plain,
spl0_242,
inference(avatar_split_clause,[],[f106,f1340]) ).
fof(f1362,definition,
( spl0_247
<=> ! [X2,X1] : ~ m0(X1,X2,b) ),
introduced(definition,[new_symbols(definition,[spl0_247])],[avatar_definition]) ).
fof(f1363,plain,
( ! [X2,X1] : ~ m0(X1,X2,b)
| ~ spl0_247 ),
inference(avatar_component_clause,[],[f1362]) ).
fof(f1528,definition,
( spl0_287
<=> l1(c,c) ),
introduced(definition,[new_symbols(definition,[spl0_287])],[avatar_definition]) ).
fof(f1529,plain,
( l1(c,c)
| ~ spl0_287 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1530,plain,
( ~ l1(c,c)
| spl0_287 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1544,definition,
( spl0_291
<=> ! [X1] :
( ~ l0(X1)
| ~ l1(X1,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_291])],[avatar_definition]) ).
fof(f1545,plain,
( ! [X1] :
( ~ l1(X1,X1)
| ~ l0(X1) )
| ~ spl0_291 ),
inference(avatar_component_clause,[],[f1544]) ).
fof(f1547,definition,
( spl0_292
<=> ! [X0] :
( l1(X0,X0)
| ~ k1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_292])],[avatar_definition]) ).
fof(f1548,plain,
( ! [X0] :
( l1(X0,X0)
| ~ k1(X0) )
| ~ spl0_292 ),
inference(avatar_component_clause,[],[f1547]) ).
fof(f1549,plain,
( spl0_291
| spl0_292 ),
inference(avatar_split_clause,[],[f42,f1547,f1544]) ).
fof(f1554,plain,
spl0_49,
inference(avatar_split_clause,[],[f34,f559]) ).
fof(f1555,plain,
spl0_184,
inference(avatar_split_clause,[],[f32,f1099]) ).
fof(f1556,plain,
spl0_205,
inference(avatar_split_clause,[],[f28,f1186]) ).
fof(f1558,plain,
spl0_134,
inference(avatar_split_clause,[],[f24,f900]) ).
fof(f1560,plain,
spl0_227,
inference(avatar_split_clause,[],[f20,f1276]) ).
fof(f1563,plain,
spl0_241,
inference(avatar_split_clause,[],[f11,f1336]) ).
fof(f1568,plain,
spl0_128,
inference(avatar_split_clause,[],[f1,f876]) ).
fof(f1569,plain,
( $false
| ~ spl0_84
| ~ spl0_128 ),
inference(resolution,[],[f700,f877]) ).
fof(f1570,plain,
( ~ spl0_84
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f1569]) ).
fof(f1579,plain,
( $false
| ~ spl0_194 ),
inference(resolution,[],[f1142,f14]) ).
fof(f1580,plain,
~ spl0_194,
inference(avatar_contradiction_clause,[],[f1579]) ).
fof(f1602,plain,
( $false
| ~ spl0_247 ),
inference(resolution,[],[f1363,f19]) ).
fof(f1603,plain,
~ spl0_247,
inference(avatar_contradiction_clause,[],[f1602]) ).
fof(f1614,plain,
( ! [X0,X1] : ~ n0(X1,X0)
| ~ spl0_166 ),
inference(forward_subsumption_resolution,[],[f39,f1027]) ).
fof(f1616,plain,
( $false
| ~ spl0_166 ),
inference(resolution,[],[f1614,f3]) ).
fof(f1631,plain,
~ spl0_166,
inference(avatar_contradiction_clause,[],[f1616]) ).
fof(f1636,plain,
( ! [X0] : ~ n0(X0,b)
| spl0_191 ),
inference(resolution,[],[f39,f1131]) ).
fof(f1666,plain,
( $false
| spl0_191 ),
inference(resolution,[],[f1636,f7]) ).
fof(f1671,plain,
spl0_191,
inference(avatar_contradiction_clause,[],[f1666]) ).
fof(f1686,plain,
! [X0] :
( q1(e,X0,X0)
| ~ m0(e,d,X0) ),
inference(forward_subsumption_resolution,[],[f145,f19]) ).
fof(f1687,plain,
! [X0] : q1(e,X0,X0),
inference(forward_subsumption_resolution,[],[f1686,f19]) ).
fof(f1707,plain,
( ! [X0] : ~ p0(X0,X0)
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f163,f603]) ).
fof(f1708,plain,
( spl0_194
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f1707,f602,f1141]) ).
fof(f1710,plain,
s1(b),
inference(resolution,[],[f163,f14]) ).
fof(f1714,plain,
spl0_130,
inference(avatar_split_clause,[],[f1710,f885]) ).
fof(f1725,plain,
( ! [X0] : ~ q0(a,X0)
| spl0_129
| ~ spl0_198 ),
inference(resolution,[],[f1158,f882]) ).
fof(f1742,plain,
( $false
| spl0_129
| ~ spl0_198 ),
inference(resolution,[],[f1725,f36]) ).
fof(f1745,plain,
( spl0_129
| ~ spl0_198 ),
inference(avatar_contradiction_clause,[],[f1742]) ).
fof(f1756,plain,
( ! [X0] : ~ q0(X0,d)
| ~ spl0_85
| ~ spl0_91 ),
inference(resolution,[],[f703,f726]) ).
fof(f1757,plain,
( $false
| ~ spl0_85
| ~ spl0_91 ),
inference(forward_subsumption_resolution,[],[f1756,f17]) ).
fof(f1758,plain,
( ~ spl0_85
| ~ spl0_91 ),
inference(avatar_contradiction_clause,[],[f1757]) ).
fof(f1790,plain,
( ! [X0] : ~ n0(X0,e)
| spl0_196 ),
inference(resolution,[],[f40,f1150]) ).
fof(f1791,plain,
( ! [X0] : ~ n0(X0,c)
| spl0_287 ),
inference(resolution,[],[f40,f1530]) ).
fof(f1792,plain,
( $false
| spl0_196 ),
inference(resolution,[],[f1790,f3]) ).
fof(f1795,plain,
spl0_196,
inference(avatar_contradiction_clause,[],[f1792]) ).
fof(f1799,plain,
( $false
| spl0_287 ),
inference(resolution,[],[f1791,f26]) ).
fof(f1800,plain,
spl0_287,
inference(avatar_contradiction_clause,[],[f1799]) ).
fof(f1801,plain,
( ~ l0(c)
| ~ spl0_287
| ~ spl0_291 ),
inference(resolution,[],[f1529,f1545]) ).
fof(f1802,plain,
( $false
| ~ spl0_134
| ~ spl0_287
| ~ spl0_291 ),
inference(forward_subsumption_resolution,[],[f1801,f901]) ).
fof(f1803,plain,
( ~ spl0_134
| ~ spl0_287
| ~ spl0_291 ),
inference(avatar_contradiction_clause,[],[f1802]) ).
fof(f1823,plain,
( ! [X0,X1] : ~ p1(X0,X1,e)
| spl0_75 ),
inference(resolution,[],[f175,f664]) ).
fof(f1826,plain,
( ~ k0(e)
| spl0_75
| ~ spl0_242 ),
inference(resolution,[],[f1823,f1341]) ).
fof(f1829,plain,
( $false
| spl0_75
| ~ spl0_205
| ~ spl0_242 ),
inference(forward_subsumption_resolution,[],[f1826,f1187]) ).
fof(f1830,plain,
( spl0_75
| ~ spl0_205
| ~ spl0_242 ),
inference(avatar_contradiction_clause,[],[f1829]) ).
fof(f1835,plain,
spl0_78,
inference(avatar_split_clause,[],[f274,f673]) ).
fof(f1914,plain,
( ! [X0] :
( q2(X0,X0,X0)
| ~ k1(X0) )
| ~ spl0_292 ),
inference(resolution,[],[f224,f1548]) ).
fof(f1916,plain,
( q2(e,e,e)
| ~ spl0_196 ),
inference(resolution,[],[f224,f1149]) ).
fof(f1918,plain,
( spl0_133
| ~ spl0_292 ),
inference(avatar_split_clause,[],[f1914,f1547,f896]) ).
fof(f1998,plain,
n1(e,e,b),
inference(resolution,[],[f74,f31]) ).
fof(f2239,plain,
( ! [X0] :
( ~ q0(a,X0)
| ~ q1(d,X0,d) )
| spl0_170
| ~ spl0_199 ),
inference(resolution,[],[f1162,f1044]) ).
fof(f2240,plain,
( ! [X0] :
( ~ q0(b,X0)
| ~ q1(d,X0,d) )
| spl0_183
| ~ spl0_199 ),
inference(resolution,[],[f1162,f1096]) ).
fof(f2276,plain,
( ~ q1(d,d,d)
| spl0_170
| ~ spl0_199 ),
inference(resolution,[],[f2239,f17]) ).
fof(f2277,plain,
( $false
| ~ spl0_42
| spl0_170
| ~ spl0_199 ),
inference(forward_subsumption_resolution,[],[f2276,f531]) ).
fof(f2278,plain,
( ~ spl0_42
| spl0_170
| ~ spl0_199 ),
inference(avatar_contradiction_clause,[],[f2277]) ).
fof(f2289,plain,
( ~ r1(a)
| r2(a)
| ~ spl0_227 ),
inference(resolution,[],[f226,f1277]) ).
fof(f2292,plain,
( r2(a)
| ~ spl0_170
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f2289,f1043]) ).
fof(f2295,plain,
( spl0_113
| ~ spl0_170
| ~ spl0_227 ),
inference(avatar_split_clause,[],[f2292,f1276,f1042,f813]) ).
fof(f2297,plain,
( m3(a,a,a)
| ~ spl0_86
| ~ spl0_113 ),
inference(resolution,[],[f814,f706]) ).
fof(f2306,plain,
( ~ q1(d,d,d)
| spl0_183
| ~ spl0_199 ),
inference(resolution,[],[f2240,f17]) ).
fof(f2307,plain,
( $false
| ~ spl0_42
| spl0_183
| ~ spl0_199 ),
inference(forward_subsumption_resolution,[],[f2306,f531]) ).
fof(f2308,plain,
( ~ spl0_42
| spl0_183
| ~ spl0_199 ),
inference(avatar_contradiction_clause,[],[f2307]) ).
fof(f2690,plain,
( ! [X2,X0,X1] :
( ~ r1(b)
| ~ m0(X0,X1,X2)
| q2(X2,b,X2)
| ~ q2(b,b,b) )
| ~ spl0_184 ),
inference(resolution,[],[f225,f1100]) ).
fof(f2691,plain,
( ! [X2,X0,X1] :
( ~ r1(e)
| ~ m0(X0,X1,X2)
| q2(X2,e,X2)
| ~ q2(e,e,e) )
| ~ spl0_205 ),
inference(resolution,[],[f225,f1187]) ).
fof(f2692,plain,
( ! [X2,X0,X1] :
( ~ r1(e)
| ~ m0(X0,X1,X2)
| q2(X2,e,X2) )
| ~ spl0_196
| ~ spl0_205 ),
inference(forward_subsumption_resolution,[],[f2691,f1916]) ).
fof(f2693,plain,
( ! [X2,X0,X1] :
( ~ m0(X0,X1,X2)
| q2(X2,b,X2)
| ~ q2(b,b,b) )
| ~ spl0_183
| ~ spl0_184 ),
inference(forward_subsumption_resolution,[],[f2690,f1095]) ).
fof(f2695,definition,
( spl0_360
<=> ! [X2,X0,X1] :
( ~ m0(X0,X1,X2)
| q2(X2,e,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_360])],[avatar_definition]) ).
fof(f2696,plain,
( ! [X2,X0,X1] :
( q2(X2,e,X2)
| ~ m0(X0,X1,X2) )
| ~ spl0_360 ),
inference(avatar_component_clause,[],[f2695]) ).
fof(f2697,plain,
( spl0_360
| ~ spl0_151
| ~ spl0_196
| ~ spl0_205 ),
inference(avatar_split_clause,[],[f2692,f1186,f1148,f967,f2695]) ).
fof(f2699,definition,
( spl0_361
<=> q2(b,b,b) ),
introduced(definition,[new_symbols(definition,[spl0_361])],[avatar_definition]) ).
fof(f2701,plain,
( ~ q2(b,b,b)
| spl0_361 ),
inference(avatar_component_clause,[],[f2699]) ).
fof(f2703,definition,
( spl0_362
<=> ! [X2,X0,X1] :
( ~ m0(X0,X1,X2)
| q2(X2,b,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_362])],[avatar_definition]) ).
fof(f2704,plain,
( ! [X2,X0,X1] :
( q2(X2,b,X2)
| ~ m0(X0,X1,X2) )
| ~ spl0_362 ),
inference(avatar_component_clause,[],[f2703]) ).
fof(f2705,plain,
( ~ spl0_361
| spl0_362
| ~ spl0_183
| ~ spl0_184 ),
inference(avatar_split_clause,[],[f2693,f1099,f1094,f2703,f2699]) ).
fof(f2706,plain,
( ! [X0] :
( ~ q0(e,X0)
| ~ q1(d,X0,d) )
| spl0_151
| ~ spl0_199 ),
inference(resolution,[],[f969,f1162]) ).
fof(f2720,plain,
( ~ k1(b)
| ~ spl0_133
| spl0_361 ),
inference(resolution,[],[f2701,f897]) ).
fof(f2724,plain,
( $false
| ~ spl0_133
| ~ spl0_191
| spl0_361 ),
inference(forward_subsumption_resolution,[],[f2720,f1130]) ).
fof(f2725,plain,
( ~ spl0_133
| ~ spl0_191
| spl0_361 ),
inference(avatar_contradiction_clause,[],[f2724]) ).
fof(f2783,plain,
( ~ q1(d,d,d)
| spl0_151
| ~ spl0_199 ),
inference(resolution,[],[f2706,f2]) ).
fof(f2787,plain,
( $false
| ~ spl0_42
| spl0_151
| ~ spl0_199 ),
inference(forward_subsumption_resolution,[],[f2783,f531]) ).
fof(f2788,plain,
( ~ spl0_42
| spl0_151
| ~ spl0_199 ),
inference(avatar_contradiction_clause,[],[f2787]) ).
fof(f2803,plain,
( ! [X0,X1] :
( ~ m0(X0,X1,b)
| s2(e) )
| ~ spl0_131
| ~ spl0_360 ),
inference(resolution,[],[f2696,f890]) ).
fof(f2807,definition,
( spl0_374
<=> q3(b,e) ),
introduced(definition,[new_symbols(definition,[spl0_374])],[avatar_definition]) ).
fof(f2808,plain,
( q3(b,e)
| ~ spl0_374 ),
inference(avatar_component_clause,[],[f2807]) ).
fof(f2809,plain,
( ~ q3(b,e)
| spl0_374 ),
inference(avatar_component_clause,[],[f2807]) ).
fof(f2811,definition,
( spl0_375
<=> ! [X0] : ~ n1(X0,e,b) ),
introduced(definition,[new_symbols(definition,[spl0_375])],[avatar_definition]) ).
fof(f2812,plain,
( ! [X0] : ~ n1(X0,e,b)
| ~ spl0_375 ),
inference(avatar_component_clause,[],[f2811]) ).
fof(f2814,plain,
( spl0_123
| spl0_247
| ~ spl0_131
| ~ spl0_360 ),
inference(avatar_split_clause,[],[f2803,f2695,f889,f1362,f855]) ).
fof(f2816,plain,
( ! [X0] :
( ~ q2(X0,b,e)
| ~ n0(X0,b) )
| spl0_374 ),
inference(resolution,[],[f2809,f293]) ).
fof(f2852,plain,
( ! [X0,X1] :
( ~ n0(e,b)
| ~ m0(X0,X1,e) )
| ~ spl0_362
| spl0_374 ),
inference(resolution,[],[f2816,f2704]) ).
fof(f2855,plain,
( ! [X0,X1] : ~ m0(X0,X1,e)
| ~ spl0_241
| ~ spl0_362
| spl0_374 ),
inference(forward_subsumption_resolution,[],[f2852,f1337]) ).
fof(f2856,plain,
( $false
| ~ spl0_241
| ~ spl0_362
| spl0_374 ),
inference(resolution,[],[f2855,f19]) ).
fof(f2863,plain,
( ~ spl0_241
| ~ spl0_362
| spl0_374 ),
inference(avatar_contradiction_clause,[],[f2856]) ).
fof(f2864,plain,
( ! [X0,X1] : ~ p2(X0,X1,e)
| spl0_47 ),
inference(resolution,[],[f553,f278]) ).
fof(f2868,plain,
( ~ q1(e,e,e)
| spl0_47 ),
inference(resolution,[],[f2864,f192]) ).
fof(f2895,plain,
( $false
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f2868,f1687]) ).
fof(f2896,plain,
spl0_47,
inference(avatar_contradiction_clause,[],[f2895]) ).
fof(f2897,plain,
( $false
| ~ spl0_37
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f565,f511]) ).
fof(f2898,plain,
( ~ spl0_37
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f2897]) ).
fof(f2899,plain,
( ! [X0,X1] :
( n4(X0,X1)
| ~ p3(X0,X1,X1)
| ~ m3(X0,X0,X0) )
| ~ spl0_38 ),
inference(resolution,[],[f514,f319]) ).
fof(f2944,plain,
( ~ p3(a,e,e)
| ~ m3(a,a,a)
| ~ spl0_38 ),
inference(resolution,[],[f2899,f369]) ).
fof(f2947,plain,
( ~ p3(a,e,e)
| ~ spl0_38
| ~ spl0_86
| ~ spl0_113 ),
inference(forward_subsumption_resolution,[],[f2944,f2297]) ).
fof(f2950,plain,
( ! [X0,X1] :
( ~ p2(a,e,X1)
| ~ m3(e,X0,X1) )
| ~ spl0_38
| ~ spl0_86
| ~ spl0_113 ),
inference(resolution,[],[f2947,f289]) ).
fof(f2958,plain,
( ! [X0] :
( ~ m3(e,X0,e)
| ~ p2(e,a,e) )
| ~ spl0_38
| ~ spl0_86
| ~ spl0_113
| ~ spl0_167 ),
inference(resolution,[],[f2950,f1030]) ).
fof(f2960,definition,
( spl0_384
<=> p2(e,a,e) ),
introduced(definition,[new_symbols(definition,[spl0_384])],[avatar_definition]) ).
fof(f2962,plain,
( ~ p2(e,a,e)
| spl0_384 ),
inference(avatar_component_clause,[],[f2960]) ).
fof(f2964,definition,
( spl0_385
<=> ! [X0] : ~ m3(e,X0,e) ),
introduced(definition,[new_symbols(definition,[spl0_385])],[avatar_definition]) ).
fof(f2965,plain,
( ! [X0] : ~ m3(e,X0,e)
| ~ spl0_385 ),
inference(avatar_component_clause,[],[f2964]) ).
fof(f2966,plain,
( ~ spl0_384
| spl0_385
| ~ spl0_38
| ~ spl0_86
| ~ spl0_113
| ~ spl0_167 ),
inference(avatar_split_clause,[],[f2958,f1029,f813,f705,f513,f2964,f2960]) ).
fof(f3005,plain,
( ~ m1(a,e,a)
| spl0_384 ),
inference(resolution,[],[f2962,f214]) ).
fof(f3015,plain,
( ! [X0] :
( ~ n1(X0,e,b)
| ~ s2(e)
| ~ q3(b,e) )
| spl0_48 ),
inference(resolution,[],[f557,f295]) ).
fof(f3017,plain,
( ! [X0] :
( ~ n1(X0,e,b)
| ~ q3(b,e) )
| spl0_48
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f3015,f856]) ).
fof(f3018,plain,
( ! [X0] : ~ n1(X0,e,b)
| spl0_48
| ~ spl0_123
| ~ spl0_374 ),
inference(forward_subsumption_resolution,[],[f3017,f2808]) ).
fof(f3019,plain,
( spl0_375
| spl0_48
| ~ spl0_123
| ~ spl0_374 ),
inference(avatar_split_clause,[],[f3018,f2807,f855,f555,f2811]) ).
fof(f3023,plain,
( $false
| ~ spl0_375 ),
inference(resolution,[],[f2812,f1998]) ).
fof(f3025,plain,
~ spl0_375,
inference(avatar_contradiction_clause,[],[f3023]) ).
fof(f3043,plain,
( ~ n2(e)
| ~ spl0_78
| ~ spl0_385 ),
inference(resolution,[],[f2965,f674]) ).
fof(f3057,plain,
( $false
| ~ spl0_75
| ~ spl0_78
| ~ spl0_385 ),
inference(forward_subsumption_resolution,[],[f3043,f663]) ).
fof(f3058,plain,
( ~ spl0_75
| ~ spl0_78
| ~ spl0_385 ),
inference(avatar_contradiction_clause,[],[f3057]) ).
fof(f3095,plain,
( ~ l0(a)
| ~ k0(e)
| spl0_384 ),
inference(resolution,[],[f3005,f59]) ).
fof(f3097,plain,
( ~ k0(e)
| ~ spl0_227
| spl0_384 ),
inference(forward_subsumption_resolution,[],[f3095,f1277]) ).
fof(f3098,plain,
( $false
| ~ spl0_205
| ~ spl0_227
| spl0_384 ),
inference(forward_subsumption_resolution,[],[f3097,f1187]) ).
fof(f3099,plain,
( ~ spl0_205
| ~ spl0_227
| spl0_384 ),
inference(avatar_contradiction_clause,[],[f3098]) ).
cnf(s18,plain,
( spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f515]) ).
cnf(s22,plain,
( ~ spl0_47
| ~ spl0_48
| ~ spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f566]) ).
cnf(s37,plain,
( spl0_84
| spl0_85
| spl0_86 ),
inference(sat_conversion,[],[f707]) ).
cnf(s59,plain,
( spl0_91
| ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f883]) ).
cnf(s60,plain,
( ~ spl0_130
| spl0_131 ),
inference(sat_conversion,[],[f891]) ).
cnf(s76,plain,
( spl0_166
| spl0_167 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s91,plain,
( spl0_60
| spl0_198 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s92,plain,
( ~ spl0_128
| spl0_199 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s96,plain,
( spl0_42
| ~ spl0_128
| ~ spl0_205 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s124,plain,
spl0_242,
inference(sat_conversion,[],[f1360]) ).
cnf(s152,plain,
( spl0_291
| spl0_292 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s154,plain,
spl0_49,
inference(sat_conversion,[],[f1554]) ).
cnf(s155,plain,
spl0_184,
inference(sat_conversion,[],[f1555]) ).
cnf(s156,plain,
spl0_205,
inference(sat_conversion,[],[f1556]) ).
cnf(s158,plain,
spl0_134,
inference(sat_conversion,[],[f1558]) ).
cnf(s160,plain,
spl0_227,
inference(sat_conversion,[],[f1560]) ).
cnf(s163,plain,
spl0_241,
inference(sat_conversion,[],[f1563]) ).
cnf(s168,plain,
spl0_128,
inference(sat_conversion,[],[f1568]) ).
cnf(s169,plain,
( ~ spl0_84
| ~ spl0_128 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s174,plain,
~ spl0_194,
inference(sat_conversion,[],[f1580]) ).
cnf(s182,plain,
~ spl0_247,
inference(sat_conversion,[],[f1603]) ).
cnf(s193,plain,
~ spl0_166,
inference(sat_conversion,[],[f1631]) ).
cnf(s202,plain,
spl0_191,
inference(sat_conversion,[],[f1671]) ).
cnf(s209,plain,
( ~ spl0_60
| spl0_194 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s211,plain,
spl0_130,
inference(sat_conversion,[],[f1714]) ).
cnf(s218,plain,
( spl0_129
| ~ spl0_198 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s221,plain,
( ~ spl0_85
| ~ spl0_91 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s234,plain,
spl0_196,
inference(sat_conversion,[],[f1795]) ).
cnf(s236,plain,
spl0_287,
inference(sat_conversion,[],[f1800]) ).
cnf(s237,plain,
( ~ spl0_134
| ~ spl0_287
| ~ spl0_291 ),
inference(sat_conversion,[],[f1803]) ).
cnf(s248,plain,
( spl0_75
| ~ spl0_205
| ~ spl0_242 ),
inference(sat_conversion,[],[f1830]) ).
cnf(s249,plain,
spl0_78,
inference(sat_conversion,[],[f1835]) ).
cnf(s265,plain,
( spl0_133
| ~ spl0_292 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s335,plain,
( ~ spl0_42
| spl0_170
| ~ spl0_199 ),
inference(sat_conversion,[],[f2278]) ).
cnf(s340,plain,
( spl0_113
| ~ spl0_170
| ~ spl0_227 ),
inference(sat_conversion,[],[f2295]) ).
cnf(s341,plain,
( ~ spl0_42
| spl0_183
| ~ spl0_199 ),
inference(sat_conversion,[],[f2308]) ).
cnf(s389,plain,
( ~ spl0_151
| ~ spl0_196
| ~ spl0_205
| spl0_360 ),
inference(sat_conversion,[],[f2697]) ).
cnf(s390,plain,
( ~ spl0_183
| ~ spl0_184
| ~ spl0_361
| spl0_362 ),
inference(sat_conversion,[],[f2705]) ).
cnf(s392,plain,
( ~ spl0_133
| ~ spl0_191
| spl0_361 ),
inference(sat_conversion,[],[f2725]) ).
cnf(s404,plain,
( ~ spl0_42
| spl0_151
| ~ spl0_199 ),
inference(sat_conversion,[],[f2788]) ).
cnf(s409,plain,
( spl0_123
| ~ spl0_131
| spl0_247
| ~ spl0_360 ),
inference(sat_conversion,[],[f2814]) ).
cnf(s425,plain,
( ~ spl0_241
| ~ spl0_362
| spl0_374 ),
inference(sat_conversion,[],[f2863]) ).
cnf(s430,plain,
spl0_47,
inference(sat_conversion,[],[f2896]) ).
cnf(s431,plain,
( ~ spl0_37
| ~ spl0_50 ),
inference(sat_conversion,[],[f2898]) ).
cnf(s440,plain,
( ~ spl0_38
| ~ spl0_86
| ~ spl0_113
| ~ spl0_167
| ~ spl0_384
| spl0_385 ),
inference(sat_conversion,[],[f2966]) ).
cnf(s450,plain,
( spl0_48
| ~ spl0_123
| ~ spl0_374
| spl0_375 ),
inference(sat_conversion,[],[f3019]) ).
cnf(s451,plain,
~ spl0_375,
inference(sat_conversion,[],[f3025]) ).
cnf(s456,plain,
( ~ spl0_75
| ~ spl0_78
| ~ spl0_385 ),
inference(sat_conversion,[],[f3058]) ).
cnf(s463,plain,
( ~ spl0_205
| ~ spl0_227
| spl0_384 ),
inference(sat_conversion,[],[f3099]) ).
cnf(s466,plain,
( spl0_48
| ~ spl0_123
| ~ spl0_374 ),
inference(rat,[],[s450,s451]) ).
cnf(s480,plain,
~ spl0_60,
inference(rat,[],[s209,s174]) ).
cnf(s481,plain,
~ spl0_84,
inference(rat,[],[s169,s168]) ).
cnf(s489,plain,
~ spl0_291,
inference(rat,[],[s237,s236,s158]) ).
cnf(s490,plain,
spl0_384,
inference(rat,[],[s463,s160,s156]) ).
cnf(s494,plain,
spl0_292,
inference(rat,[],[s152,s489]) ).
cnf(s495,plain,
spl0_133,
inference(rat,[],[s265,s494]) ).
cnf(s496,plain,
spl0_361,
inference(rat,[],[s392,s202,s495]) ).
cnf(s524,plain,
spl0_75,
inference(rat,[],[s248,s156,s124]) ).
cnf(s525,plain,
~ spl0_385,
inference(rat,[],[s456,s249,s524]) ).
cnf(s552,plain,
spl0_42,
inference(rat,[],[s96,s156,s168]) ).
cnf(s557,plain,
spl0_199,
inference(rat,[],[s92,s168]) ).
cnf(s558,plain,
spl0_151,
inference(rat,[],[s404,s552,s557]) ).
cnf(s560,plain,
spl0_183,
inference(rat,[],[s341,s552,s557]) ).
cnf(s561,plain,
spl0_170,
inference(rat,[],[s335,s552,s557]) ).
cnf(s564,plain,
spl0_360,
inference(rat,[],[s389,s156,s234,s558]) ).
cnf(s566,plain,
spl0_362,
inference(rat,[],[s390,s496,s155,s560]) ).
cnf(s567,plain,
spl0_113,
inference(rat,[],[s340,s160,s561]) ).
cnf(s568,plain,
spl0_374,
inference(rat,[],[s425,s163,s566]) ).
cnf(s570,plain,
spl0_198,
inference(rat,[],[s91,s480]) ).
cnf(s572,plain,
spl0_129,
inference(rat,[],[s218,s570]) ).
cnf(s598,plain,
spl0_167,
inference(rat,[],[s76,s193]) ).
cnf(s613,plain,
spl0_131,
inference(rat,[],[s60,s211]) ).
cnf(s614,plain,
spl0_123,
inference(rat,[],[s409,s564,s182,s613]) ).
cnf(s616,plain,
spl0_48,
inference(rat,[],[s466,s568,s614]) ).
cnf(s617,plain,
spl0_91,
inference(rat,[],[s59,s572,s168]) ).
cnf(s619,plain,
~ spl0_85,
inference(rat,[],[s221,s617]) ).
cnf(s641,plain,
spl0_86,
inference(rat,[],[s37,s619,s481]) ).
cnf(s642,plain,
~ spl0_38,
inference(rat,[],[s440,s525,s490,s598,s567,s641]) ).
cnf(s652,plain,
spl0_50,
inference(rat,[],[s22,s154,s616,s430]) ).
cnf(s653,plain,
~ spl0_37,
inference(rat,[],[s431,s652]) ).
cnf(s655,plain,
$false,
inference(rat,[],[s18,s642,s653]) ).
fof(f3100,plain,
$false,
inference(avatar_sat_refutation,[],[s655]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN156-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n019.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 15:37:18 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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.09/1.11 % (4097655)Input is clausal, will run a generic CNF schedule.
% 3.09/1.11 % (4097663)lrs+10_1_sil=8000:sp=occurrence:random_seed=3523860487:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.09/1.11 % (4097663)Refutation not found, incomplete strategy
% 3.09/1.11 % (4097663)------------------------------
% 3.09/1.11 % (4097663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.11 % (4097663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.11 % (4097663)CaDiCaL version: 2.1.3
% 3.09/1.11 % (4097663)Termination reason: Refutation not found, incomplete strategy
% 3.09/1.11 % (4097663)Time elapsed: 0.011 s
% 3.09/1.11 % (4097663)Peak memory usage: 89 MB
% 3.09/1.11 % (4097663)Instructions burned: 26 (million)
% 3.09/1.11 % (4097664)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1388198112:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.09/1.11 % (4097660)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=1251450729:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.09/1.11 % (4097661)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1613089163:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.09/1.11 % (4097662)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3864632739:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.09/1.11 % (4097665)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=541289068:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.09/1.11 % (4097666)dis-21_1_sil=8000:lcm=predicate:random_seed=3342741314: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.09/1.11 % (4097665)First to succeed.
% 3.09/1.11 % (4097664)Also succeeded, but the first one will report.
% 3.09/1.11 % (4097665)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4097655"
% 3.09/1.11 % (4097666)Instruction limit reached!
% 3.09/1.11 % (4097666)------------------------------
% 3.09/1.11 % (4097666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.11 % (4097666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.11 % (4097666)CaDiCaL version: 2.1.3
% 3.09/1.11 % (4097666)Termination reason: Instruction limit
% 3.09/1.11 % (4097666)Termination phase: Saturation
% 3.09/1.11 % (4097666)Time elapsed: 0.055 s
% 3.09/1.11 % (4097666)Peak memory usage: 89 MB
% 3.09/1.11 % (4097666)Instructions burned: 117 (million)
% 3.09/1.11 % (4097663)------------------------------
% 3.09/1.11 % (4097663)------------------------------
% 3.09/1.11 % (4097674)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=1728801112:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.09/1.11 % (4097674)Refutation not found, incomplete strategy
% 3.09/1.11 % (4097674)------------------------------
% 3.09/1.11 % (4097674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.11 % (4097674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.11 % (4097674)CaDiCaL version: 2.1.3
% 3.09/1.11 % (4097674)Termination reason: Refutation not found, incomplete strategy
% 3.09/1.11 % (4097674)Time elapsed: 0.002 s
% 3.09/1.11 % (4097674)Peak memory usage: 87 MB
% 3.09/1.11 % (4097674)Instructions burned: 2 (million)
% 3.09/1.11 % (4097675)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4200671736: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)
% 3.09/1.11 % (4097675)Refutation not found, incomplete strategy
% 3.09/1.11 % (4097675)------------------------------
% 3.09/1.11 % (4097675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.11 % (4097675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.11 % (4097675)CaDiCaL version: 2.1.3
% 3.09/1.11 % (4097675)Termination reason: Refutation not found, incomplete strategy
% 3.09/1.11 % (4097675)Time elapsed: 0.008 s
% 3.09/1.11 % (4097675)Peak memory usage: 88 MB
% 3.09/1.11 % (4097675)Instructions burned: 25 (million)
% 3.09/1.11 % (4097665)Refutation found. Thanks to Tanya!
% 3.09/1.11 % SZS status Unsatisfiable for theBenchmark
% 3.09/1.11 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/1.30 % (4097665)------------------------------
% 0.20/1.30 % (4097665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/1.30 % (4097665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/1.30 % (4097665)CaDiCaL version: 2.1.3
% 0.20/1.30 % (4097665)Termination reason: Refutation
% 0.20/1.30 % (4097665)Time elapsed: 0.046 s
% 0.20/1.30 % (4097665)Peak memory usage: 90 MB
% 0.20/1.30 % (4097665)Instructions burned: 69 (million)
% 0.20/1.30 % (4097665)------------------------------
% 0.20/1.30 % (4097665)------------------------------
% 0.20/1.30 % (4097655)Success in time 0.456 s
% 0.20/1.30 % Vampire exiting
%------------------------------------------------------------------------------