%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN163-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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 02:06:55 PM UTC 2026
% Result : Unsatisfiable 0.20s 0.32s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 70
% Syntax : Number of formulae : 278 ( 64 unt; 32 def)
% Number of atoms : 619 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 664 ( 323 ~; 309 |; 0 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 58 ( 57 usr; 33 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 233 ( 0 sgn 233 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
n0(d,e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_3) ).
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
fof(f14,axiom,
! [X0] : p0(b,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
fof(f18,axiom,
p0(c,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_18) ).
fof(f19,axiom,
! [X0,X1] : m0(X0,d,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
fof(f24,axiom,
l0(c),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_24) ).
fof(f27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_27) ).
fof(f28,axiom,
k0(e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_28) ).
fof(f30,axiom,
n0(e,e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_30) ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_34) ).
fof(f39,axiom,
! [X0,X1] :
( k1(X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_001) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( l1(X0,X1)
| ~ p0(X2,X0)
| ~ r0(X3)
| ~ m0(X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_003) ).
fof(f43,axiom,
! [X0,X1] :
( m1(X0,X1,X0)
| ~ m0(X1,X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_005) ).
fof(f59,axiom,
! [X0,X1] :
( m1(X0,X1,X0)
| ~ l0(X0)
| ~ k0(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_021) ).
fof(f104,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_066) ).
fof(f107,axiom,
! [X0,X1] :
( p1(X0,X0,X1)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_069) ).
fof(f123,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_085) ).
fof(f159,axiom,
! [X2,X0,X1] :
( q1(X0,X0,X0)
| ~ m0(X1,X2,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_121) ).
fof(f165,axiom,
! [X2,X3,X0,X1] :
( k2(X0,X1)
| ~ m1(X2,X1,X0)
| ~ k1(X3)
| ~ k2(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_127) ).
fof(f167,axiom,
! [X0,X1] :
( k2(X0,X0)
| ~ q1(X1,X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_129) ).
fof(f175,axiom,
! [X2,X0,X1] :
( n2(X0)
| ~ p1(X1,X2,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_137) ).
fof(f193,axiom,
! [X2,X0,X1] :
( p2(X0,X1,X1)
| ~ k1(X2)
| ~ p2(e,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_155) ).
fof(f212,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ n2(X0)
| ~ k1(e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_174) ).
fof(f214,axiom,
! [X0,X1] :
( p2(X0,X1,X0)
| ~ m1(X1,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_176) ).
fof(f215,axiom,
! [X0,X1] :
( q2(X0,X1,X1)
| ~ k0(X1)
| ~ p1(X0,X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_177) ).
fof(f224,axiom,
! [X0,X1] :
( q2(X0,X0,X1)
| ~ l1(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_186) ).
fof(f232,axiom,
! [X0,X1] :
( k3(X0,X0,X1)
| ~ k2(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_194) ).
fof(f274,axiom,
! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_236) ).
fof(f278,axiom,
! [X2,X0,X1] :
( n3(X0)
| ~ p2(X1,X2,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_240) ).
fof(f293,axiom,
! [X2,X0,X1] :
( q3(X0,X1)
| ~ q2(X2,X0,X1)
| ~ n0(X2,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_255) ).
fof(f312,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_274) ).
fof(f322,axiom,
! [X0,X1] :
( n4(X0,X0)
| ~ k4(X1)
| ~ m3(X0,X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_284) ).
fof(f324,axiom,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ q3(X1,X2)
| ~ n3(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_286) ).
fof(f333,axiom,
! [X2,X3,X0,X1,X4] :
( q4(X0,X1)
| ~ k3(X2,X2,X0)
| ~ q2(X3,X1,X0)
| ~ m3(X3,X4,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_295) ).
fof(f336,axiom,
! [X2,X3,X0,X1] :
( r4(X0)
| ~ n3(X0)
| ~ q3(X1,X2)
| ~ p0(X3,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_298) ).
fof(f345,axiom,
! [X2,X3,X0,X1,X4] :
( n5(X0,X1)
| ~ q4(X2,X3)
| ~ n4(X0,X3)
| ~ p4(X4,X4,X1)
| ~ n5(X4,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_307) ).
fof(f352,axiom,
! [X0] :
( n5(X0,X0)
| ~ r4(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_314) ).
fof(f369,negated_conjecture,
~ n5(e,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f371,plain,
~ n0(d,e),
inference(consistent_polarity_flipping,[],[f3]) ).
fof(f381,plain,
! [X0,X1] : ~ m0(X0,d,X1),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f385,plain,
~ l0(c),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f388,plain,
~ m0(e,b,c),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f389,plain,
~ k0(e),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f391,plain,
~ n0(e,e),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f395,plain,
~ n0(c,d),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f400,plain,
! [X0,X1] :
( k1(X0)
| n0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f402,plain,
! [X2,X3,X0,X1] :
( l1(X0,X1)
| ~ p0(X2,X0)
| ~ r0(X3)
| m0(X1,X0,X2) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f404,plain,
! [X0,X1] :
( m1(X0,X1,X0)
| m0(X1,X1,X0) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f417,plain,
! [X0,X1] :
( k0(X1)
| l0(X0)
| m1(X0,X1,X0) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f458,plain,
! [X0,X1] :
( n0(X1,X0)
| p1(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f496,plain,
! [X2,X0,X1] :
( q1(X0,X0,X0)
| m0(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f501,plain,
! [X2,X3,X0,X1] :
( k2(X3,X1)
| ~ m1(X2,X1,X0)
| ~ k1(X3)
| ~ k2(X0,X1) ),
inference(consistent_polarity_flipping,[],[f165]) ).
fof(f503,plain,
! [X0,X1] :
( ~ q1(X1,X0,X0)
| ~ k2(X0,X0) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f508,plain,
! [X2,X0,X1] :
( ~ p1(X1,X2,X0)
| ~ n2(X0) ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f526,plain,
! [X2,X0,X1] :
( ~ p2(X0,X1,X1)
| ~ k1(X2)
| p2(e,X0,X1) ),
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f545,plain,
! [X0] :
( ~ p2(X0,X0,X0)
| n2(X0)
| ~ k1(e) ),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f547,plain,
! [X0,X1] :
( ~ p2(X0,X1,X0)
| ~ m1(X1,X0,X1) ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f548,plain,
! [X0,X1] :
( k0(X1)
| ~ q2(X0,X1,X1)
| ~ p1(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f557,plain,
! [X0,X1] :
( ~ q2(X0,X0,X1)
| ~ l1(X1,X0) ),
inference(consistent_polarity_flipping,[],[f224]) ).
fof(f565,plain,
! [X0,X1] :
( k2(X1,X0)
| k3(X0,X0,X1) ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f602,plain,
! [X0] :
( n2(X0)
| m3(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f274]) ).
fof(f605,plain,
! [X2,X0,X1] :
( p2(X1,X2,X0)
| ~ n3(X0) ),
inference(consistent_polarity_flipping,[],[f278]) ).
fof(f619,plain,
! [X2,X0,X1] :
( n0(X2,X0)
| q2(X2,X0,X1)
| ~ q3(X0,X1) ),
inference(consistent_polarity_flipping,[],[f293]) ).
fof(f634,plain,
( k4(c)
| n0(c,d)
| q3(e,b)
| n3(e) ),
inference(consistent_polarity_flipping,[],[f312]) ).
fof(f641,plain,
! [X2,X0,X1] :
( ~ p4(X0,X0,X0)
| q3(X1,X2)
| n3(X0) ),
inference(consistent_polarity_flipping,[],[f324]) ).
fof(f650,plain,
! [X2,X3,X0,X1,X4] :
( q4(X0,X1)
| ~ k3(X2,X2,X0)
| q2(X3,X1,X0)
| ~ m3(X3,X4,X3) ),
inference(consistent_polarity_flipping,[],[f333]) ).
fof(f652,plain,
! [X2,X3,X0,X1] :
( r4(X0)
| n3(X0)
| q3(X1,X2)
| ~ p0(X3,X0) ),
inference(consistent_polarity_flipping,[],[f336]) ).
fof(f656,plain,
! [X2,X3,X0,X1,X4] :
( n5(X4,X1)
| ~ q4(X2,X3)
| ~ n4(X0,X3)
| p4(X4,X4,X1)
| ~ n5(X0,X1) ),
inference(consistent_polarity_flipping,[],[f345]) ).
fof(f663,plain,
! [X0] :
( ~ n5(X0,X0)
| ~ r4(X0) ),
inference(consistent_polarity_flipping,[],[f352]) ).
fof(f673,plain,
n5(e,a),
inference(consistent_polarity_flipping,[],[f369]) ).
fof(f764,definition,
( spl0_24
<=> ! [X2,X1] : q3(X1,X2) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f765,plain,
( ! [X2,X1] : q3(X1,X2)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f767,definition,
( spl0_25
<=> ! [X0,X3] :
( r4(X0)
| ~ p0(X3,X0)
| n3(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f768,plain,
( ! [X3,X0] :
( r4(X0)
| ~ p0(X3,X0)
| n3(X0) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f769,plain,
( spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f652,f767,f764]) ).
fof(f791,definition,
( spl0_31
<=> n3(a) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f793,plain,
( n3(a)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f810,definition,
( spl0_36
<=> ! [X0] :
( ~ p4(X0,X0,X0)
| n3(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f811,plain,
( ! [X0] :
( n3(X0)
| ~ p4(X0,X0,X0) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f812,plain,
( spl0_24
| spl0_36 ),
inference(avatar_split_clause,[],[f641,f810,f764]) ).
fof(f814,definition,
( spl0_37
<=> ! [X1] : ~ k4(X1) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f815,plain,
( ! [X1] : ~ k4(X1)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f817,definition,
( spl0_38
<=> ! [X0] :
( n4(X0,X0)
| ~ m3(X0,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f818,plain,
( ! [X0] :
( n4(X0,X0)
| ~ m3(X0,X0,X0) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f819,plain,
( spl0_37
| spl0_38 ),
inference(avatar_split_clause,[],[f322,f817,f814]) ).
fof(f829,definition,
( spl0_41
<=> n4(e,e) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f830,plain,
( ~ n4(e,e)
| spl0_41 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f855,definition,
( spl0_47
<=> n3(e) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f859,definition,
( spl0_48
<=> q3(e,b) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f861,plain,
( q3(e,b)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f863,definition,
( spl0_49
<=> n0(c,d) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f864,plain,
( ~ n0(c,d)
| spl0_49 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f867,definition,
( spl0_50
<=> k4(c) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f869,plain,
( k4(c)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f870,plain,
( spl0_47
| spl0_48
| spl0_49
| spl0_50 ),
inference(avatar_split_clause,[],[f634,f867,f863,f859,f855]) ).
fof(f1007,definition,
( spl0_85
<=> r0(b) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f1008,plain,
( r0(b)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f1007]) ).
fof(f1193,definition,
( spl0_131
<=> l0(c) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1194,plain,
( ~ l0(c)
| spl0_131 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1218,definition,
( spl0_137
<=> k1(e) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1220,plain,
( ~ k1(e)
| spl0_137 ),
inference(avatar_component_clause,[],[f1218]) ).
fof(f1222,definition,
( spl0_138
<=> ! [X0] :
( ~ p2(X0,X0,X0)
| n2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1223,plain,
( ! [X0] :
( n2(X0)
| ~ p2(X0,X0,X0) )
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f1222]) ).
fof(f1224,plain,
( ~ spl0_137
| spl0_138 ),
inference(avatar_split_clause,[],[f545,f1222,f1218]) ).
fof(f1276,definition,
( spl0_152
<=> ! [X0] : ~ p2(X0,X0,X0) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1277,plain,
( ! [X0] : ~ p2(X0,X0,X0)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f1276]) ).
fof(f1319,definition,
( spl0_163
<=> ! [X2] : ~ k1(X2) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1320,plain,
( ! [X2] : ~ k1(X2)
| ~ spl0_163 ),
inference(avatar_component_clause,[],[f1319]) ).
fof(f1322,definition,
( spl0_164
<=> ! [X0,X1] :
( ~ p2(X0,X1,X1)
| p2(e,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1323,plain,
( ! [X0,X1] :
( p2(e,X0,X1)
| ~ p2(X0,X1,X1) )
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f1322]) ).
fof(f1324,plain,
( spl0_163
| spl0_164 ),
inference(avatar_split_clause,[],[f526,f1322,f1319]) ).
fof(f1363,definition,
( spl0_174
<=> p2(c,e,e) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f1364,plain,
( p2(c,e,e)
| ~ spl0_174 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1365,plain,
( ~ p2(c,e,e)
| spl0_174 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1425,definition,
( spl0_189
<=> ! [X1] : ~ p0(X1,X1) ),
introduced(definition,[new_symbols(definition,[spl0_189])],[avatar_definition]) ).
fof(f1426,plain,
( ! [X1] : ~ p0(X1,X1)
| ~ spl0_189 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1470,definition,
( spl0_200
<=> k0(e) ),
introduced(definition,[new_symbols(definition,[spl0_200])],[avatar_definition]) ).
fof(f1471,plain,
( ~ k0(e)
| spl0_200 ),
inference(avatar_component_clause,[],[f1470]) ).
fof(f1480,definition,
( spl0_202
<=> ! [X2] : ~ r0(X2) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f1481,plain,
( ! [X2] : ~ r0(X2)
| ~ spl0_202 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1789,definition,
( spl0_277
<=> ! [X2,X0,X1] :
( l1(X0,X1)
| m0(X1,X0,X2)
| ~ p0(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_277])],[avatar_definition]) ).
fof(f1790,plain,
( ! [X2,X0,X1] :
( l1(X0,X1)
| m0(X1,X0,X2)
| ~ p0(X2,X0) )
| ~ spl0_277 ),
inference(avatar_component_clause,[],[f1789]) ).
fof(f1791,plain,
( spl0_202
| spl0_277 ),
inference(avatar_split_clause,[],[f402,f1789,f1480]) ).
fof(f1792,plain,
~ spl0_49,
inference(avatar_split_clause,[],[f395,f863]) ).
fof(f1794,plain,
~ spl0_200,
inference(avatar_split_clause,[],[f389,f1470]) ).
fof(f1796,plain,
~ spl0_131,
inference(avatar_split_clause,[],[f385,f1193]) ).
fof(f1802,plain,
spl0_85,
inference(avatar_split_clause,[],[f9,f1007]) ).
fof(f1820,plain,
( $false
| ~ spl0_85
| ~ spl0_202 ),
inference(resolution,[],[f1481,f1008]) ).
fof(f1823,plain,
( ~ spl0_85
| ~ spl0_202 ),
inference(avatar_contradiction_clause,[],[f1820]) ).
fof(f1836,plain,
( $false
| ~ spl0_189 ),
inference(resolution,[],[f1426,f14]) ).
fof(f1837,plain,
~ spl0_189,
inference(avatar_contradiction_clause,[],[f1836]) ).
fof(f1848,plain,
( ! [X0,X1] : n0(X0,X1)
| ~ spl0_163 ),
inference(resolution,[],[f400,f1320]) ).
fof(f1849,plain,
( $false
| ~ spl0_163 ),
inference(resolution,[],[f1848,f371]) ).
fof(f1864,plain,
~ spl0_163,
inference(avatar_contradiction_clause,[],[f1849]) ).
fof(f1865,plain,
( ! [X0] : n0(X0,e)
| spl0_137 ),
inference(resolution,[],[f400,f1220]) ).
fof(f1869,plain,
( $false
| spl0_137 ),
inference(resolution,[],[f1865,f371]) ).
fof(f1872,plain,
spl0_137,
inference(avatar_contradiction_clause,[],[f1869]) ).
fof(f1979,plain,
( ~ n3(e)
| spl0_174 ),
inference(resolution,[],[f605,f1365]) ).
fof(f1980,plain,
( ~ spl0_47
| spl0_174 ),
inference(avatar_split_clause,[],[f1979,f1363,f855]) ).
fof(f2031,plain,
! [X0,X1] :
( ~ p0(X0,X1)
| ~ n2(X1) ),
inference(resolution,[],[f123,f508]) ).
fof(f2032,plain,
! [X0] : ~ n2(X0),
inference(resolution,[],[f2031,f14]) ).
fof(f2036,plain,
! [X0] : m3(X0,X0,X0),
inference(resolution,[],[f2032,f602]) ).
fof(f2054,plain,
( p1(d,d,d)
| spl0_49 ),
inference(resolution,[],[f458,f864]) ).
fof(f2094,definition,
( spl0_280
<=> ! [X0] : n0(X0,d) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f2095,plain,
( ! [X0] : n0(X0,d)
| ~ spl0_280 ),
inference(avatar_component_clause,[],[f2094]) ).
fof(f2159,plain,
( ! [X0] : ~ p2(X0,X0,X0)
| ~ spl0_138 ),
inference(resolution,[],[f1223,f2032]) ).
fof(f2160,plain,
( spl0_152
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f2159,f1222,f1276]) ).
fof(f2161,plain,
( ! [X0] : ~ n3(X0)
| ~ spl0_152 ),
inference(resolution,[],[f1277,f605]) ).
fof(f2162,plain,
( ! [X0] : ~ p4(X0,X0,X0)
| ~ spl0_36
| ~ spl0_152 ),
inference(resolution,[],[f2161,f811]) ).
fof(f2178,plain,
( ! [X0] :
( l0(X0)
| m1(X0,e,X0) )
| spl0_200 ),
inference(resolution,[],[f417,f1471]) ).
fof(f2186,plain,
( m1(c,e,c)
| spl0_131
| spl0_200 ),
inference(resolution,[],[f2178,f1194]) ).
fof(f2198,plain,
! [X2,X0,X1] :
( m0(X0,X1,X2)
| ~ k2(X2,X2) ),
inference(resolution,[],[f496,f503]) ).
fof(f2199,plain,
! [X0] : ~ k2(X0,X0),
inference(resolution,[],[f2198,f381]) ).
fof(f2368,plain,
( ! [X0] :
( ~ p2(X0,e,e)
| ~ m1(X0,e,X0) )
| ~ spl0_164 ),
inference(resolution,[],[f1323,f547]) ).
fof(f2518,plain,
( ! [X0] :
( ~ q2(X0,e,e)
| ~ p1(X0,X0,X0) )
| spl0_200 ),
inference(resolution,[],[f548,f1471]) ).
fof(f2531,plain,
! [X0] :
( q2(d,e,X0)
| ~ q3(e,X0) ),
inference(resolution,[],[f619,f371]) ).
fof(f2534,plain,
! [X0] :
( q2(e,e,X0)
| ~ q3(e,X0) ),
inference(resolution,[],[f619,f391]) ).
fof(f2539,plain,
( ~ q3(e,e)
| ~ p1(d,d,d)
| spl0_200 ),
inference(resolution,[],[f2531,f2518]) ).
fof(f2541,definition,
( spl0_298
<=> p1(d,d,d) ),
introduced(definition,[new_symbols(definition,[spl0_298])],[avatar_definition]) ).
fof(f2543,plain,
( ~ p1(d,d,d)
| spl0_298 ),
inference(avatar_component_clause,[],[f2541]) ).
fof(f2545,definition,
( spl0_299
<=> q3(e,e) ),
introduced(definition,[new_symbols(definition,[spl0_299])],[avatar_definition]) ).
fof(f2547,plain,
( ~ q3(e,e)
| spl0_299 ),
inference(avatar_component_clause,[],[f2545]) ).
fof(f2548,plain,
( ~ spl0_298
| ~ spl0_299
| spl0_200 ),
inference(avatar_split_clause,[],[f2539,f1470,f2545,f2541]) ).
fof(f2549,plain,
( $false
| ~ spl0_24
| spl0_299 ),
inference(resolution,[],[f2547,f765]) ).
fof(f2550,plain,
( ~ spl0_24
| spl0_299 ),
inference(avatar_contradiction_clause,[],[f2549]) ).
fof(f2551,plain,
( $false
| spl0_49
| spl0_298 ),
inference(resolution,[],[f2543,f2054]) ).
fof(f2558,plain,
( spl0_49
| spl0_298 ),
inference(avatar_contradiction_clause,[],[f2551]) ).
fof(f2571,plain,
! [X0] :
( ~ q3(e,X0)
| ~ l1(X0,e) ),
inference(resolution,[],[f2534,f557]) ).
fof(f2576,plain,
( ~ l1(b,e)
| ~ spl0_48 ),
inference(resolution,[],[f2571,f861]) ).
fof(f2755,definition,
( spl0_317
<=> k1(d) ),
introduced(definition,[new_symbols(definition,[spl0_317])],[avatar_definition]) ).
fof(f2757,plain,
( ~ k1(d)
| spl0_317 ),
inference(avatar_component_clause,[],[f2755]) ).
fof(f2773,plain,
( ! [X0] : n0(X0,d)
| spl0_317 ),
inference(resolution,[],[f2757,f400]) ).
fof(f2774,plain,
( spl0_280
| spl0_317 ),
inference(avatar_split_clause,[],[f2773,f2755,f2094]) ).
fof(f2775,plain,
( $false
| spl0_49
| ~ spl0_280 ),
inference(resolution,[],[f2095,f864]) ).
fof(f2776,plain,
( spl0_49
| ~ spl0_280 ),
inference(avatar_contradiction_clause,[],[f2775]) ).
fof(f3089,plain,
( ! [X0] :
( m0(e,b,X0)
| ~ p0(X0,b) )
| ~ spl0_48
| ~ spl0_277 ),
inference(resolution,[],[f1790,f2576]) ).
fof(f3105,plain,
( ~ p0(c,b)
| ~ spl0_48
| ~ spl0_277 ),
inference(resolution,[],[f3089,f388]) ).
fof(f3106,plain,
( $false
| ~ spl0_48
| ~ spl0_277 ),
inference(resolution,[],[f3105,f18]) ).
fof(f3107,plain,
( ~ spl0_48
| ~ spl0_277 ),
inference(avatar_contradiction_clause,[],[f3106]) ).
fof(f3108,plain,
( $false
| ~ spl0_37
| ~ spl0_50 ),
inference(resolution,[],[f869,f815]) ).
fof(f3109,plain,
( ~ spl0_37
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f3108]) ).
fof(f3111,plain,
( ~ m3(e,e,e)
| ~ spl0_38
| spl0_41 ),
inference(resolution,[],[f818,f830]) ).
fof(f3117,plain,
( ~ m1(c,e,c)
| ~ spl0_164
| ~ spl0_174 ),
inference(resolution,[],[f1364,f2368]) ).
fof(f3120,plain,
( $false
| ~ spl0_38
| spl0_41 ),
inference(resolution,[],[f3111,f2036]) ).
fof(f3121,plain,
( ~ spl0_38
| spl0_41 ),
inference(avatar_contradiction_clause,[],[f3120]) ).
fof(f3127,plain,
( $false
| spl0_131
| ~ spl0_164
| ~ spl0_174
| spl0_200 ),
inference(resolution,[],[f3117,f2186]) ).
fof(f3131,plain,
( spl0_131
| ~ spl0_164
| ~ spl0_174
| spl0_200 ),
inference(avatar_contradiction_clause,[],[f3127]) ).
fof(f3333,plain,
! [X2,X0,X1] :
( ~ m1(X0,X1,X2)
| ~ k1(X1)
| ~ k2(X2,X1) ),
inference(resolution,[],[f501,f2199]) ).
fof(f3360,plain,
! [X0,X1] :
( m0(X0,X0,X1)
| ~ k2(X1,X0)
| ~ k1(X0) ),
inference(resolution,[],[f3333,f404]) ).
fof(f3699,plain,
! [X0] :
( ~ k2(X0,d)
| ~ k1(d) ),
inference(resolution,[],[f3360,f381]) ).
fof(f3703,definition,
( spl0_399
<=> ! [X0] : ~ k2(X0,d) ),
introduced(definition,[new_symbols(definition,[spl0_399])],[avatar_definition]) ).
fof(f3704,plain,
( ! [X0] : ~ k2(X0,d)
| ~ spl0_399 ),
inference(avatar_component_clause,[],[f3703]) ).
fof(f3705,plain,
( ~ spl0_317
| spl0_399 ),
inference(avatar_split_clause,[],[f3699,f3703,f2755]) ).
fof(f3708,plain,
( ! [X0] : k3(d,d,X0)
| ~ spl0_399 ),
inference(resolution,[],[f3704,f565]) ).
fof(f4571,definition,
( spl0_473
<=> ! [X2] : ~ p0(X2,a) ),
introduced(definition,[new_symbols(definition,[spl0_473])],[avatar_definition]) ).
fof(f4572,plain,
( ! [X2] : ~ p0(X2,a)
| ~ spl0_473 ),
inference(avatar_component_clause,[],[f4571]) ).
fof(f4754,plain,
( $false
| ~ spl0_473 ),
inference(resolution,[],[f4572,f14]) ).
fof(f4755,plain,
~ spl0_473,
inference(avatar_contradiction_clause,[],[f4754]) ).
fof(f5607,plain,
! [X2,X3,X0,X1] :
( p4(X3,X3,X3)
| ~ n4(X2,X1)
| ~ q4(X0,X1)
| ~ n5(X2,X3)
| ~ r4(X3) ),
inference(resolution,[],[f656,f663]) ).
fof(f6143,plain,
( ! [X2,X3,X0,X1] :
( ~ n5(X0,X3)
| ~ q4(X2,X1)
| ~ n4(X0,X1)
| ~ r4(X3) )
| ~ spl0_36
| ~ spl0_152 ),
inference(resolution,[],[f5607,f2162]) ).
fof(f6150,plain,
( ! [X0,X1] :
( ~ q4(X0,X1)
| ~ n4(e,X1)
| ~ r4(a) )
| ~ spl0_36
| ~ spl0_152 ),
inference(resolution,[],[f6143,f673]) ).
fof(f6152,definition,
( spl0_582
<=> r4(a) ),
introduced(definition,[new_symbols(definition,[spl0_582])],[avatar_definition]) ).
fof(f6154,plain,
( ~ r4(a)
| spl0_582 ),
inference(avatar_component_clause,[],[f6152]) ).
fof(f6156,definition,
( spl0_583
<=> ! [X0,X1] :
( ~ q4(X0,X1)
| ~ n4(e,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_583])],[avatar_definition]) ).
fof(f6157,plain,
( ! [X0,X1] :
( ~ q4(X0,X1)
| ~ n4(e,X1) )
| ~ spl0_583 ),
inference(avatar_component_clause,[],[f6156]) ).
fof(f6158,plain,
( ~ spl0_582
| spl0_583
| ~ spl0_36
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f6150,f1276,f810,f6156,f6152]) ).
fof(f6159,plain,
( ! [X0] :
( ~ p0(X0,a)
| n3(a) )
| ~ spl0_25
| spl0_582 ),
inference(resolution,[],[f6154,f768]) ).
fof(f6160,plain,
( spl0_31
| spl0_473
| ~ spl0_25
| spl0_582 ),
inference(avatar_split_clause,[],[f6159,f6152,f767,f4571,f791]) ).
fof(f6162,plain,
( $false
| ~ spl0_31
| ~ spl0_152 ),
inference(resolution,[],[f793,f2161]) ).
fof(f6163,plain,
( ~ spl0_31
| ~ spl0_152 ),
inference(avatar_contradiction_clause,[],[f6162]) ).
fof(f6164,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ m3(X3,X4,X3)
| ~ k3(X1,X1,X2)
| q2(X3,X0,X2)
| ~ n4(e,X0) )
| ~ spl0_583 ),
inference(resolution,[],[f6157,f650]) ).
fof(f6171,plain,
( ! [X2,X3,X0,X1] :
( ~ k3(X0,X0,X1)
| q2(X2,X3,X1)
| ~ n4(e,X3) )
| ~ spl0_583 ),
inference(resolution,[],[f6164,f2036]) ).
fof(f6200,plain,
( ! [X2,X0,X1] :
( q2(X0,X1,X2)
| ~ n4(e,X1) )
| ~ spl0_399
| ~ spl0_583 ),
inference(resolution,[],[f6171,f3708]) ).
fof(f6353,plain,
( ! [X0] :
( ~ n4(e,e)
| ~ p1(X0,X0,X0) )
| spl0_200
| ~ spl0_399
| ~ spl0_583 ),
inference(resolution,[],[f6200,f2518]) ).
fof(f6373,definition,
( spl0_603
<=> ! [X0] : ~ p1(X0,X0,X0) ),
introduced(definition,[new_symbols(definition,[spl0_603])],[avatar_definition]) ).
fof(f6374,plain,
( ! [X0] : ~ p1(X0,X0,X0)
| ~ spl0_603 ),
inference(avatar_component_clause,[],[f6373]) ).
fof(f6375,plain,
( spl0_603
| ~ spl0_41
| spl0_200
| ~ spl0_399
| ~ spl0_583 ),
inference(avatar_split_clause,[],[f6353,f6156,f3703,f1470,f829,f6373]) ).
fof(f6399,plain,
( ! [X0] : ~ p0(X0,X0)
| ~ spl0_603 ),
inference(resolution,[],[f6374,f107]) ).
fof(f6406,plain,
( spl0_189
| ~ spl0_603 ),
inference(avatar_split_clause,[],[f6399,f6373,f1425]) ).
cnf(s11,plain,
( spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f769]) ).
cnf(s17,plain,
( spl0_24
| spl0_36 ),
inference(sat_conversion,[],[f812]) ).
cnf(s18,plain,
( spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f819]) ).
cnf(s22,plain,
( spl0_47
| spl0_48
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f870]) ).
cnf(s62,plain,
( ~ spl0_137
| spl0_138 ),
inference(sat_conversion,[],[f1224]) ).
cnf(s74,plain,
( spl0_163
| spl0_164 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s142,plain,
( spl0_202
| spl0_277 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s143,plain,
~ spl0_49,
inference(sat_conversion,[],[f1792]) ).
cnf(s145,plain,
~ spl0_200,
inference(sat_conversion,[],[f1794]) ).
cnf(s147,plain,
~ spl0_131,
inference(sat_conversion,[],[f1796]) ).
cnf(s153,plain,
spl0_85,
inference(sat_conversion,[],[f1802]) ).
cnf(s165,plain,
( ~ spl0_85
| ~ spl0_202 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s172,plain,
~ spl0_189,
inference(sat_conversion,[],[f1837]) ).
cnf(s183,plain,
~ spl0_163,
inference(sat_conversion,[],[f1864]) ).
cnf(s185,plain,
spl0_137,
inference(sat_conversion,[],[f1872]) ).
cnf(s221,plain,
( ~ spl0_47
| spl0_174 ),
inference(sat_conversion,[],[f1980]) ).
cnf(s244,plain,
( ~ spl0_138
| spl0_152 ),
inference(sat_conversion,[],[f2160]) ).
cnf(s268,plain,
( spl0_200
| ~ spl0_298
| ~ spl0_299 ),
inference(sat_conversion,[],[f2548]) ).
cnf(s269,plain,
( ~ spl0_24
| spl0_299 ),
inference(sat_conversion,[],[f2550]) ).
cnf(s270,plain,
( spl0_49
| spl0_298 ),
inference(sat_conversion,[],[f2558]) ).
cnf(s305,plain,
( spl0_280
| spl0_317 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s306,plain,
( spl0_49
| ~ spl0_280 ),
inference(sat_conversion,[],[f2776]) ).
cnf(s350,plain,
( ~ spl0_48
| ~ spl0_277 ),
inference(sat_conversion,[],[f3107]) ).
cnf(s351,plain,
( ~ spl0_37
| ~ spl0_50 ),
inference(sat_conversion,[],[f3109]) ).
cnf(s354,plain,
( ~ spl0_38
| spl0_41 ),
inference(sat_conversion,[],[f3121]) ).
cnf(s357,plain,
( spl0_131
| ~ spl0_164
| ~ spl0_174
| spl0_200 ),
inference(sat_conversion,[],[f3131]) ).
cnf(s406,plain,
( ~ spl0_317
| spl0_399 ),
inference(sat_conversion,[],[f3705]) ).
cnf(s507,plain,
~ spl0_473,
inference(sat_conversion,[],[f4755]) ).
cnf(s631,plain,
( ~ spl0_36
| ~ spl0_152
| ~ spl0_582
| spl0_583 ),
inference(sat_conversion,[],[f6158]) ).
cnf(s632,plain,
( ~ spl0_25
| spl0_31
| spl0_473
| spl0_582 ),
inference(sat_conversion,[],[f6160]) ).
cnf(s634,plain,
( ~ spl0_31
| ~ spl0_152 ),
inference(sat_conversion,[],[f6163]) ).
cnf(s658,plain,
( ~ spl0_41
| spl0_200
| ~ spl0_399
| ~ spl0_583
| spl0_603 ),
inference(sat_conversion,[],[f6375]) ).
cnf(s668,plain,
( spl0_189
| ~ spl0_603 ),
inference(sat_conversion,[],[f6406]) ).
cnf(s707,plain,
~ spl0_603,
inference(rat,[],[s668,s172]) ).
cnf(s719,plain,
~ spl0_202,
inference(rat,[],[s165,s153]) ).
cnf(s746,plain,
~ spl0_280,
inference(rat,[],[s306,s143]) ).
cnf(s747,plain,
spl0_298,
inference(rat,[],[s270,s143]) ).
cnf(s748,plain,
spl0_317,
inference(rat,[],[s305,s746]) ).
cnf(s752,plain,
~ spl0_299,
inference(rat,[],[s268,s145,s747]) ).
cnf(s753,plain,
spl0_399,
inference(rat,[],[s406,s748]) ).
cnf(s754,plain,
~ spl0_24,
inference(rat,[],[s269,s752]) ).
cnf(s760,plain,
spl0_277,
inference(rat,[],[s142,s719]) ).
cnf(s763,plain,
~ spl0_48,
inference(rat,[],[s350,s760]) ).
cnf(s894,plain,
spl0_164,
inference(rat,[],[s74,s183]) ).
cnf(s896,plain,
~ spl0_174,
inference(rat,[],[s357,s145,s147,s894]) ).
cnf(s897,plain,
~ spl0_47,
inference(rat,[],[s221,s896]) ).
cnf(s905,plain,
spl0_138,
inference(rat,[],[s62,s185]) ).
cnf(s906,plain,
spl0_152,
inference(rat,[],[s244,s905]) ).
cnf(s907,plain,
~ spl0_31,
inference(rat,[],[s634,s906]) ).
cnf(s956,plain,
spl0_50,
inference(rat,[],[s22,s143,s763,s897]) ).
cnf(s957,plain,
~ spl0_37,
inference(rat,[],[s351,s956]) ).
cnf(s959,plain,
spl0_38,
inference(rat,[],[s18,s957]) ).
cnf(s961,plain,
spl0_41,
inference(rat,[],[s354,s959]) ).
cnf(s963,plain,
~ spl0_583,
inference(rat,[],[s658,s707,s753,s145,s961]) ).
cnf(s965,plain,
spl0_36,
inference(rat,[],[s17,s754]) ).
cnf(s966,plain,
~ spl0_582,
inference(rat,[],[s631,s963,s906,s965]) ).
cnf(s969,plain,
~ spl0_25,
inference(rat,[],[s632,s907,s507,s966]) ).
cnf(s973,plain,
$false,
inference(rat,[],[s11,s969,s754]) ).
fof(f6407,plain,
$false,
inference(avatar_sat_refutation,[],[s973]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN163-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n011.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:15 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.32 % (3474864)Will run a generic schedule for satisfiability detection.
% 0.20/0.32 % (3474870)% WARNING: option uhcvi not known.
% 0.20/0.32 % (3474875)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=101781552:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.32 % (3474871)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=948062046:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.32 % (3474869)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4054090144_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.32 % (3474872)dis+10_1_sil=32000:sp=arity:random_seed=3502987585:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.32 % (3474873)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4205379543:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.32 % (3474870)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3272986952:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.32 % (3474874)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2950055306:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.32 % Detected minimum model sizes of [1]
% 0.20/0.32 % Detected maximum model sizes of [5]
% 0.20/0.32 % TRYING [1]
% 0.20/0.32 % TRYING [2]
% 0.20/0.32 % TRYING [3]
% 0.20/0.32 % TRYING [4]
% 0.20/0.32 % (3474875) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3474864-3474875"...
% 0.20/0.32 % (3474875)...printing done.
% 0.20/0.32 % (3474875)Refutation found. Thanks to Tanya!
% 0.20/0.32 % SZS status Unsatisfiable for theBenchmark
% 0.20/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.32 % (3474875)------------------------------
% 0.20/0.32 % (3474875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (3474875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (3474875)CaDiCaL version: 2.1.3
% 0.20/0.32 % (3474875)Termination reason: Refutation
% 0.20/0.32 % (3474875)Time elapsed: 0.050 s
% 0.20/0.32 % (3474875)Peak memory usage: 15 MB
% 0.20/0.32 % (3474875)Instructions burned: 135 (million)
% 0.20/0.32 % (3474864)Success in time 0.091 s
% 0.20/0.32 % Vampire exiting
%------------------------------------------------------------------------------