%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN157-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 0.64s 0.97s
% Output : Refutation 2.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 63
% Syntax : Number of formulae : 225 ( 52 unt; 32 def)
% Number of atoms : 508 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 565 ( 282 ~; 251 |; 0 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 55 ( 54 usr; 33 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 130 ( 0 sgn 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
s0(d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(f14,axiom,
! [X0] : p0(b,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_14) ).
fof(f17,axiom,
! [X0] : q0(X0,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_17) ).
fof(f19,axiom,
! [X0,X1] : m0(X0,d,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_19) ).
fof(f20,axiom,
l0(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
fof(f24,axiom,
l0(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_24) ).
fof(f28,axiom,
k0(e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_28) ).
fof(f29,axiom,
q0(d,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_34) ).
fof(f36,axiom,
q0(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_36) ).
fof(f39,axiom,
! [X0,X1] :
( k1(X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_001) ).
fof(f126,axiom,
( p1(a,a,a)
| ~ l0(a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_088) ).
fof(f155,axiom,
( q1(d,d,d)
| ~ k0(e)
| ~ s0(d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_117) ).
fof(f158,axiom,
( q1(b,b,b)
| ~ r0(b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_120) ).
fof(f162,axiom,
! [X0,X1] :
( r1(X0)
| ~ q0(X0,X1)
| ~ s0(d)
| ~ q1(d,X1,d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_124) ).
fof(f163,axiom,
! [X0] :
( s1(X0)
| ~ p0(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_125) ).
fof(f164,axiom,
! [X2,X0,X1] :
( s1(X0)
| ~ q0(X0,X1)
| ~ s1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_126) ).
fof(f171,axiom,
! [X2,X3,X0,X1] :
( l2(X0,X0)
| ~ p0(X1,X1)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_133) ).
fof(f189,axiom,
( p2(d,d,d)
| ~ k1(d)
| ~ s0(d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_151) ).
fof(f203,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_165) ).
fof(f207,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ q1(X1,X1,X1)
| ~ p1(X0,X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_169) ).
fof(f226,axiom,
! [X0] :
( ~ r1(X0)
| r2(X0)
| ~ l0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_188) ).
fof(f228,axiom,
( s2(d)
| ~ s1(a)
| ~ s0(d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_190) ).
fof(f278,axiom,
! [X2,X0,X1] :
( n3(X0)
| ~ p2(X1,X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_240) ).
fof(f296,axiom,
! [X2,X0,X1] :
( q3(X0,X0)
| ~ r2(X0)
| ~ s1(X1)
| ~ l2(X2,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_258) ).
fof(f302,axiom,
! [X0] :
( ~ s2(X0)
| r3(X0,X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_264) ).
fof(f324,axiom,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ q3(X1,X2)
| ~ n3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_286) ).
fof(f326,axiom,
! [X2,X3,X0,X1] :
( p4(X0,X1,X1)
| ~ r3(X1,X1,X0)
| ~ p4(X2,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_288) ).
fof(f354,axiom,
! [X2,X0,X1] :
( n5(X0,X0)
| ~ p4(X1,X0,X0)
| ~ s1(X0)
| ~ p4(b,b,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_316) ).
fof(f369,negated_conjecture,
! [X0] : ~ n5(X0,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f395,definition,
( spl0_8
<=> ! [X2,X1] : ~ q3(X1,X2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f396,plain,
( ! [X2,X1] : ~ q3(X1,X2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f416,definition,
( spl0_14
<=> ! [X0] :
( p4(X0,X0,X0)
| ~ n3(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f417,plain,
( ! [X0] :
( ~ n3(X0)
| p4(X0,X0,X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f418,plain,
( spl0_8
| spl0_14 ),
inference(avatar_split_clause,[],[f324,f416,f395]) ).
fof(f428,definition,
( spl0_17
<=> ! [X0,X1] : ~ p4(X0,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f429,plain,
( ! [X0,X1] : ~ p4(X0,X0,X1)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f457,definition,
( spl0_25
<=> ! [X2,X1] :
( ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f458,plain,
( ! [X2,X1] :
( ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f460,definition,
( spl0_26
<=> ! [X0] : p2(X0,X0,X0) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f461,plain,
( ! [X0] : p2(X0,X0,X0)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f462,plain,
( spl0_25
| spl0_26 ),
inference(avatar_split_clause,[],[f203,f460,f457]) ).
fof(f498,definition,
( spl0_37
<=> ! [X2] : ~ p0(X2,X2) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f499,plain,
( ! [X2] : ~ p0(X2,X2)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f512,definition,
( spl0_41
<=> s0(d) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f513,plain,
( ~ s0(d)
| spl0_41 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f515,definition,
( spl0_42
<=> ! [X0,X1] :
( r1(X0)
| ~ q1(d,X1,d)
| ~ q0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f516,plain,
( ! [X0,X1] :
( r1(X0)
| ~ q1(d,X1,d)
| ~ q0(X0,X1) )
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f517,plain,
( ~ spl0_41
| spl0_42 ),
inference(avatar_split_clause,[],[f162,f515,f512]) ).
fof(f526,definition,
( spl0_45
<=> ! [X2] : ~ s1(X2) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f527,plain,
( ! [X2] : ~ s1(X2)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f529,definition,
( spl0_46
<=> ! [X0,X1] :
( s1(X0)
| ~ q0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f530,plain,
( ! [X0,X1] :
( s1(X0)
| ~ q0(X0,X1) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f531,plain,
( spl0_45
| spl0_46 ),
inference(avatar_split_clause,[],[f164,f529,f526]) ).
fof(f540,definition,
( spl0_49
<=> ! [X2] : ~ l2(X2,X2) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f541,plain,
( ! [X2] : ~ l2(X2,X2)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f543,definition,
( spl0_50
<=> ! [X0] :
( q3(X0,X0)
| ~ r2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f544,plain,
( ! [X0] :
( q3(X0,X0)
| ~ r2(X0) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f545,plain,
( spl0_49
| spl0_45
| spl0_50 ),
inference(avatar_split_clause,[],[f296,f543,f526,f540]) ).
fof(f569,definition,
( spl0_57
<=> ! [X1] : ~ q1(X1,X1,X1) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f570,plain,
( ! [X1] : ~ q1(X1,X1,X1)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f572,definition,
( spl0_58
<=> ! [X2,X0] :
( p2(X0,X0,X0)
| ~ p1(X0,X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f573,plain,
( ! [X2,X0] :
( ~ p1(X0,X2,X0)
| p2(X0,X0,X0) )
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f574,plain,
( spl0_57
| spl0_58 ),
inference(avatar_split_clause,[],[f207,f572,f569]) ).
fof(f628,definition,
( spl0_73
<=> q1(d,d,d) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f648,definition,
( spl0_79
<=> s1(d) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f649,plain,
( ~ s1(d)
| spl0_79 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f654,definition,
( spl0_81
<=> s2(d) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f655,plain,
( s2(d)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f691,definition,
( spl0_91
<=> k0(e) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f692,plain,
( ~ k0(e)
| spl0_91 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f832,definition,
( spl0_130
<=> q1(b,b,b) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f833,plain,
( q1(b,b,b)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f840,definition,
( spl0_132
<=> r0(b) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f841,plain,
( ~ r0(b)
| spl0_132 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f842,plain,
( ~ spl0_132
| spl0_130 ),
inference(avatar_split_clause,[],[f158,f832,f840]) ).
fof(f882,definition,
( spl0_144
<=> l0(a) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f883,plain,
( ~ l0(a)
| spl0_144 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f899,definition,
( spl0_149
<=> p1(a,a,a) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f900,plain,
( p1(a,a,a)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f907,plain,
( ~ spl0_144
| spl0_149 ),
inference(avatar_split_clause,[],[f126,f899,f882]) ).
fof(f932,definition,
( spl0_158
<=> p2(a,a,a) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f933,plain,
( p2(a,a,a)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f932]) ).
fof(f1107,definition,
( spl0_208
<=> ! [X0,X1] :
( p4(X0,X1,X1)
| ~ r3(X1,X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f1108,plain,
( ! [X0,X1] :
( p4(X0,X1,X1)
| ~ r3(X1,X1,X0) )
| ~ spl0_208 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1109,plain,
( spl0_17
| spl0_208 ),
inference(avatar_split_clause,[],[f326,f1107,f428]) ).
fof(f1182,definition,
( spl0_229
<=> ! [X2,X0,X3] :
( l2(X0,X0)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f1183,plain,
( ! [X2,X3,X0] :
( ~ s1(X2)
| l2(X0,X0)
| ~ m0(X3,X2,X0) )
| ~ spl0_229 ),
inference(avatar_component_clause,[],[f1182]) ).
fof(f1184,plain,
( spl0_37
| spl0_229 ),
inference(avatar_split_clause,[],[f171,f1182,f498]) ).
fof(f1220,definition,
( spl0_240
<=> ! [X2] : ~ p4(b,b,X2) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1221,plain,
( ! [X2] : ~ p4(b,b,X2)
| ~ spl0_240 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1223,definition,
( spl0_241
<=> ! [X0,X1] :
( n5(X0,X0)
| ~ s1(X0)
| ~ p4(X1,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1224,plain,
( ! [X0,X1] :
( n5(X0,X0)
| ~ s1(X0)
| ~ p4(X1,X0,X0) )
| ~ spl0_241 ),
inference(avatar_component_clause,[],[f1223]) ).
fof(f1225,plain,
( spl0_240
| spl0_241 ),
inference(avatar_split_clause,[],[f354,f1223,f1220]) ).
fof(f1319,plain,
( q1(d,d,d)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f1320,plain,
( ~ spl0_41
| ~ spl0_91
| spl0_73 ),
inference(avatar_split_clause,[],[f155,f628,f691,f512]) ).
fof(f1345,definition,
( spl0_276
<=> k1(d) ),
introduced(definition,[new_symbols(definition,[spl0_276])],[avatar_definition]) ).
fof(f1346,plain,
( ~ k1(d)
| spl0_276 ),
inference(avatar_component_clause,[],[f1345]) ).
fof(f1348,definition,
( spl0_277
<=> p2(d,d,d) ),
introduced(definition,[new_symbols(definition,[spl0_277])],[avatar_definition]) ).
fof(f1349,plain,
( p2(d,d,d)
| ~ spl0_277 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1350,plain,
( ~ spl0_41
| ~ spl0_276
| spl0_277 ),
inference(avatar_split_clause,[],[f189,f1348,f1345,f512]) ).
fof(f1376,definition,
( spl0_285
<=> s1(a) ),
introduced(definition,[new_symbols(definition,[spl0_285])],[avatar_definition]) ).
fof(f1377,plain,
( ~ s1(a)
| spl0_285 ),
inference(avatar_component_clause,[],[f1376]) ).
fof(f1378,plain,
( ~ spl0_41
| ~ spl0_285
| spl0_81 ),
inference(avatar_split_clause,[],[f228,f654,f1376,f512]) ).
fof(f1408,plain,
( $false
| spl0_41 ),
inference(resolution,[],[f1,f513]) ).
fof(f1411,plain,
spl0_41,
inference(avatar_contradiction_clause,[],[f1408]) ).
fof(f1416,plain,
( $false
| spl0_132 ),
inference(resolution,[],[f841,f9]) ).
fof(f1417,plain,
spl0_132,
inference(avatar_contradiction_clause,[],[f1416]) ).
fof(f1422,plain,
( $false
| spl0_144 ),
inference(resolution,[],[f883,f20]) ).
fof(f1423,plain,
spl0_144,
inference(avatar_contradiction_clause,[],[f1422]) ).
fof(f1427,plain,
( $false
| ~ spl0_57
| ~ spl0_130 ),
inference(resolution,[],[f833,f570]) ).
fof(f1428,plain,
( ~ spl0_57
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f1427]) ).
fof(f1435,plain,
( $false
| spl0_91 ),
inference(resolution,[],[f28,f692]) ).
fof(f1436,plain,
spl0_91,
inference(avatar_contradiction_clause,[],[f1435]) ).
fof(f1446,plain,
( ~ p2(d,d,d)
| ~ spl0_25
| ~ spl0_73 ),
inference(resolution,[],[f458,f1319]) ).
fof(f1450,plain,
( p2(a,a,a)
| ~ spl0_58
| ~ spl0_149 ),
inference(resolution,[],[f573,f900]) ).
fof(f1454,plain,
( spl0_158
| ~ spl0_58
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1450,f899,f572,f932]) ).
fof(f1460,plain,
( $false
| ~ spl0_25
| ~ spl0_73
| ~ spl0_277 ),
inference(resolution,[],[f1446,f1349]) ).
fof(f1461,plain,
( ~ spl0_25
| ~ spl0_73
| ~ spl0_277 ),
inference(avatar_contradiction_clause,[],[f1460]) ).
fof(f1530,plain,
( $false
| ~ spl0_37 ),
inference(resolution,[],[f14,f499]) ).
fof(f1536,plain,
~ spl0_37,
inference(avatar_contradiction_clause,[],[f1530]) ).
fof(f1744,plain,
( ! [X0] : ~ n0(X0,d)
| spl0_276 ),
inference(resolution,[],[f1346,f39]) ).
fof(f1747,plain,
( ! [X0] : ~ p0(X0,X0)
| ~ spl0_45 ),
inference(resolution,[],[f163,f527]) ).
fof(f1748,plain,
( spl0_37
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1747,f526,f498]) ).
fof(f1753,plain,
( ! [X0] : ~ q0(d,X0)
| ~ spl0_46
| spl0_79 ),
inference(resolution,[],[f530,f649]) ).
fof(f1754,plain,
( ! [X0] : ~ q0(a,X0)
| ~ spl0_46
| spl0_285 ),
inference(resolution,[],[f530,f1377]) ).
fof(f1766,plain,
( $false
| spl0_276 ),
inference(resolution,[],[f1744,f34]) ).
fof(f1767,plain,
spl0_276,
inference(avatar_contradiction_clause,[],[f1766]) ).
fof(f1772,plain,
( $false
| ~ spl0_46
| spl0_79 ),
inference(resolution,[],[f1753,f29]) ).
fof(f1777,plain,
( ~ spl0_46
| spl0_79 ),
inference(avatar_contradiction_clause,[],[f1772]) ).
fof(f1779,plain,
( $false
| ~ spl0_46
| spl0_285 ),
inference(resolution,[],[f1754,f36]) ).
fof(f1782,plain,
( ~ spl0_46
| spl0_285 ),
inference(avatar_contradiction_clause,[],[f1779]) ).
fof(f1813,plain,
( ! [X2,X3,X0,X1] :
( l2(X0,X0)
| ~ m0(X1,X2,X0)
| ~ q0(X2,X3) )
| ~ spl0_46
| ~ spl0_229 ),
inference(resolution,[],[f1183,f530]) ).
fof(f1862,plain,
( ! [X2,X3,X0,X1] :
( ~ q0(X1,X3)
| ~ m0(X0,X1,X2) )
| ~ spl0_46
| ~ spl0_49
| ~ spl0_229 ),
inference(resolution,[],[f1813,f541]) ).
fof(f1899,plain,
( ! [X2,X0,X1] : ~ m0(X0,X1,X2)
| ~ spl0_46
| ~ spl0_49
| ~ spl0_229 ),
inference(resolution,[],[f1862,f17]) ).
fof(f1909,plain,
( $false
| ~ spl0_46
| ~ spl0_49
| ~ spl0_229 ),
inference(resolution,[],[f1899,f19]) ).
fof(f1928,plain,
( ~ spl0_46
| ~ spl0_49
| ~ spl0_229 ),
inference(avatar_contradiction_clause,[],[f1909]) ).
fof(f1932,plain,
( ! [X0] : ~ r2(X0)
| ~ spl0_8
| ~ spl0_50 ),
inference(resolution,[],[f544,f396]) ).
fof(f2019,plain,
( ! [X0,X1] :
( r2(X0)
| ~ l0(X0)
| ~ q1(d,X1,d)
| ~ q0(X0,X1) )
| ~ spl0_42 ),
inference(resolution,[],[f226,f516]) ).
fof(f2020,plain,
( ! [X0,X1] :
( ~ l0(X0)
| ~ q1(d,X1,d)
| ~ q0(X0,X1) )
| ~ spl0_8
| ~ spl0_42
| ~ spl0_50 ),
inference(resolution,[],[f2019,f1932]) ).
fof(f2028,definition,
( spl0_324
<=> ! [X0] :
( ~ q1(d,X0,d)
| ~ q0(c,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_324])],[avatar_definition]) ).
fof(f2029,plain,
( ! [X0] :
( ~ q0(c,X0)
| ~ q1(d,X0,d) )
| ~ spl0_324 ),
inference(avatar_component_clause,[],[f2028]) ).
fof(f2050,plain,
( ! [X0] :
( ~ q1(d,X0,d)
| ~ q0(c,X0) )
| ~ spl0_8
| ~ spl0_42
| ~ spl0_50 ),
inference(resolution,[],[f2020,f24]) ).
fof(f2051,plain,
( spl0_324
| ~ spl0_8
| ~ spl0_42
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f2050,f543,f515,f395,f2028]) ).
fof(f2061,plain,
( ! [X2,X0,X1] :
( p4(X2,X2,X2)
| ~ p2(X0,X1,X2) )
| ~ spl0_14 ),
inference(resolution,[],[f278,f417]) ).
fof(f2073,plain,
( ! [X2,X0,X1] : ~ p2(X0,X1,X2)
| ~ spl0_14
| ~ spl0_17 ),
inference(resolution,[],[f2061,f429]) ).
fof(f2075,plain,
( $false
| ~ spl0_14
| ~ spl0_17
| ~ spl0_158 ),
inference(resolution,[],[f2073,f933]) ).
fof(f2081,plain,
( ~ spl0_14
| ~ spl0_17
| ~ spl0_158 ),
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2082,plain,
( ! [X0,X1] : ~ p2(X0,X1,b)
| ~ spl0_14
| ~ spl0_240 ),
inference(resolution,[],[f1221,f2061]) ).
fof(f2096,plain,
( $false
| ~ spl0_14
| ~ spl0_26
| ~ spl0_240 ),
inference(resolution,[],[f2082,f461]) ).
fof(f2098,plain,
( ~ spl0_14
| ~ spl0_26
| ~ spl0_240 ),
inference(avatar_contradiction_clause,[],[f2096]) ).
fof(f2099,plain,
( ! [X0] :
( ~ s1(d)
| ~ p4(X0,d,d) )
| ~ spl0_241 ),
inference(resolution,[],[f1224,f369]) ).
fof(f2101,definition,
( spl0_330
<=> ! [X0] : ~ p4(X0,d,d) ),
introduced(definition,[new_symbols(definition,[spl0_330])],[avatar_definition]) ).
fof(f2102,plain,
( ! [X0] : ~ p4(X0,d,d)
| ~ spl0_330 ),
inference(avatar_component_clause,[],[f2101]) ).
fof(f2108,plain,
( ~ q1(d,d,d)
| ~ spl0_324 ),
inference(resolution,[],[f2029,f17]) ).
fof(f2109,plain,
( ~ spl0_73
| ~ spl0_324 ),
inference(avatar_split_clause,[],[f2108,f2028,f628]) ).
fof(f2110,plain,
( spl0_330
| ~ spl0_79
| ~ spl0_241 ),
inference(avatar_split_clause,[],[f2099,f1223,f648,f2101]) ).
fof(f2111,plain,
( ! [X0] : ~ r3(d,d,X0)
| ~ spl0_208
| ~ spl0_330 ),
inference(resolution,[],[f2102,f1108]) ).
fof(f2113,plain,
( r3(d,d,d)
| ~ spl0_81 ),
inference(resolution,[],[f302,f655]) ).
fof(f2117,plain,
( $false
| ~ spl0_81
| ~ spl0_208
| ~ spl0_330 ),
inference(resolution,[],[f2113,f2111]) ).
fof(f2118,plain,
( ~ spl0_81
| ~ spl0_208
| ~ spl0_330 ),
inference(avatar_contradiction_clause,[],[f2117]) ).
cnf(s7,plain,
( spl0_8
| spl0_14 ),
inference(sat_conversion,[],[f418]) ).
cnf(s14,plain,
( spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f462]) ).
cnf(s21,plain,
( ~ spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f517]) ).
cnf(s23,plain,
( spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f531]) ).
cnf(s25,plain,
( spl0_45
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f545]) ).
cnf(s30,plain,
( spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f574]) ).
cnf(s74,plain,
( spl0_130
| ~ spl0_132 ),
inference(sat_conversion,[],[f842]) ).
cnf(s84,plain,
( ~ spl0_144
| spl0_149 ),
inference(sat_conversion,[],[f907]) ).
cnf(s112,plain,
( spl0_17
| spl0_208 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s124,plain,
( spl0_37
| spl0_229 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s129,plain,
( spl0_240
| spl0_241 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s142,plain,
( ~ spl0_41
| spl0_73
| ~ spl0_91 ),
inference(sat_conversion,[],[f1320]) ).
cnf(s145,plain,
( ~ spl0_41
| ~ spl0_276
| spl0_277 ),
inference(sat_conversion,[],[f1350]) ).
cnf(s149,plain,
( ~ spl0_41
| spl0_81
| ~ spl0_285 ),
inference(sat_conversion,[],[f1378]) ).
cnf(s155,plain,
spl0_41,
inference(sat_conversion,[],[f1411]) ).
cnf(s158,plain,
spl0_132,
inference(sat_conversion,[],[f1417]) ).
cnf(s161,plain,
spl0_144,
inference(sat_conversion,[],[f1423]) ).
cnf(s163,plain,
( ~ spl0_57
| ~ spl0_130 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s167,plain,
spl0_91,
inference(sat_conversion,[],[f1436]) ).
cnf(s169,plain,
( ~ spl0_58
| ~ spl0_149
| spl0_158 ),
inference(sat_conversion,[],[f1454]) ).
cnf(s172,plain,
( ~ spl0_25
| ~ spl0_73
| ~ spl0_277 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s185,plain,
~ spl0_37,
inference(sat_conversion,[],[f1536]) ).
cnf(s228,plain,
( spl0_37
| ~ spl0_45 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s232,plain,
spl0_276,
inference(sat_conversion,[],[f1767]) ).
cnf(s236,plain,
( ~ spl0_46
| spl0_79 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s238,plain,
( ~ spl0_46
| spl0_285 ),
inference(sat_conversion,[],[f1782]) ).
cnf(s257,plain,
( ~ spl0_46
| ~ spl0_49
| ~ spl0_229 ),
inference(sat_conversion,[],[f1928]) ).
cnf(s279,plain,
( ~ spl0_8
| ~ spl0_42
| ~ spl0_50
| spl0_324 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s285,plain,
( ~ spl0_14
| ~ spl0_17
| ~ spl0_158 ),
inference(sat_conversion,[],[f2081]) ).
cnf(s289,plain,
( ~ spl0_14
| ~ spl0_26
| ~ spl0_240 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s293,plain,
( ~ spl0_73
| ~ spl0_324 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s294,plain,
( ~ spl0_79
| ~ spl0_241
| spl0_330 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s295,plain,
( ~ spl0_81
| ~ spl0_208
| ~ spl0_330 ),
inference(sat_conversion,[],[f2118]) ).
cnf(s298,plain,
~ spl0_45,
inference(rat,[],[s228,s185]) ).
cnf(s304,plain,
( spl0_81
| ~ spl0_285 ),
inference(rat,[],[s149,s155]) ).
cnf(s305,plain,
spl0_277,
inference(rat,[],[s145,s232,s155]) ).
cnf(s308,plain,
spl0_73,
inference(rat,[],[s142,s167,s155]) ).
cnf(s309,plain,
~ spl0_324,
inference(rat,[],[s293,s308]) ).
cnf(s310,plain,
~ spl0_25,
inference(rat,[],[s172,s305,s308]) ).
cnf(s320,plain,
spl0_229,
inference(rat,[],[s124,s185]) ).
cnf(s342,plain,
spl0_149,
inference(rat,[],[s84,s161]) ).
cnf(s348,plain,
spl0_130,
inference(rat,[],[s74,s158]) ).
cnf(s349,plain,
~ spl0_57,
inference(rat,[],[s163,s348]) ).
cnf(s382,plain,
spl0_58,
inference(rat,[],[s30,s349]) ).
cnf(s383,plain,
spl0_158,
inference(rat,[],[s169,s342,s382]) ).
cnf(s391,plain,
( spl0_49
| spl0_50 ),
inference(rat,[],[s25,s298]) ).
cnf(s392,plain,
spl0_46,
inference(rat,[],[s23,s298]) ).
cnf(s396,plain,
~ spl0_49,
inference(rat,[],[s257,s320,s392]) ).
cnf(s398,plain,
spl0_285,
inference(rat,[],[s238,s392]) ).
cnf(s399,plain,
spl0_79,
inference(rat,[],[s236,s392]) ).
cnf(s403,plain,
spl0_50,
inference(rat,[],[s391,s396]) ).
cnf(s404,plain,
spl0_81,
inference(rat,[],[s304,s398]) ).
cnf(s414,plain,
spl0_42,
inference(rat,[],[s21,s155]) ).
cnf(s415,plain,
~ spl0_8,
inference(rat,[],[s279,s309,s403,s414]) ).
cnf(s432,plain,
spl0_26,
inference(rat,[],[s14,s310]) ).
cnf(s435,plain,
spl0_14,
inference(rat,[],[s7,s415]) ).
cnf(s436,plain,
~ spl0_240,
inference(rat,[],[s289,s432,s435]) ).
cnf(s438,plain,
~ spl0_17,
inference(rat,[],[s285,s383,s435]) ).
cnf(s439,plain,
spl0_241,
inference(rat,[],[s129,s436]) ).
cnf(s441,plain,
spl0_208,
inference(rat,[],[s112,s438]) ).
cnf(s442,plain,
spl0_330,
inference(rat,[],[s294,s399,s439]) ).
cnf(s443,plain,
$false,
inference(rat,[],[s295,s404,s442,s441]) ).
fof(f2119,plain,
$false,
inference(avatar_sat_refutation,[],[s443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN157-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n020.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 15:38:05 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.64/0.97 % (251317)Input is clausal, will run a generic CNF schedule.
% 0.64/0.97 % (251328)dis-21_1_sil=8000:lcm=predicate:random_seed=4106546176: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)
% 0.64/0.97 % (251328)First to succeed.
% 0.64/0.97 % (251328)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-251317"
% 0.64/0.97 % (251327)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2824594057:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.64/0.97 % (251322)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=2588528212:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.64/0.97 % (251323)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1836714806:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.64/0.97 % (251325)lrs+10_1_sil=8000:sp=occurrence:random_seed=78623059:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.64/0.97 % (251326)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1942787045:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.64/0.97 % (251324)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=723130491:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.64/0.97 % (251325)Also succeeded, but the first one will report.
% 0.64/0.97 % (251326)Also succeeded, but the first one will report.
% 0.64/0.97 % (251327)Also succeeded, but the first one will report.
% 0.64/0.97 % (251328)Refutation found. Thanks to Tanya!
% 0.64/0.97 % SZS status Unsatisfiable for theBenchmark
% 0.64/0.97 % SZS output start Proof for theBenchmark
% See solution above
% 2.79/1.17 % (251328)------------------------------
% 2.79/1.17 % (251328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.79/1.17 % (251328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/1.17 % (251328)CaDiCaL version: 2.1.3
% 2.79/1.17 % (251328)Termination reason: Refutation
% 2.79/1.17 % (251328)Time elapsed: 0.014 s
% 2.79/1.17 % (251328)Peak memory usage: 90 MB
% 2.79/1.17 % (251328)Instructions burned: 36 (million)
% 2.79/1.17 % (251328)------------------------------
% 2.79/1.17 % (251328)------------------------------
% 2.79/1.17 % (251317)Success in time 0.309 s
% 2.79/1.17 % Vampire exiting
%------------------------------------------------------------------------------