%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN142-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:52 PM UTC 2026
% Result : Unsatisfiable 0.19s 0.30s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 50
% Syntax : Number of formulae : 165 ( 46 unt; 19 def)
% Number of atoms : 406 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 474 ( 233 ~; 222 |; 0 &)
% ( 19 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 41 ( 40 usr; 20 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 132 ( 0 sgn 132 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
s0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_5) ).
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
fof(f12,axiom,
! [X0] : m0(a,X0,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_12) ).
fof(f14,axiom,
! [X0] : p0(b,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
fof(f17,axiom,
! [X0] : q0(X0,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_17) ).
fof(f19,axiom,
! [X0,X1] : m0(X0,d,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
fof(f20,axiom,
l0(a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_20) ).
fof(f32,axiom,
k0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_32) ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_34) ).
fof(f37,axiom,
n0(b,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_37) ).
fof(f40,axiom,
! [X0,X1] :
( ~ n0(X1,X0)
| l1(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_002) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( l1(X0,X1)
| ~ p0(X2,X0)
| ~ r0(X3)
| ~ m0(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_003) ).
fof(f88,axiom,
! [X0,X1] :
( n1(X0,X1,X0)
| ~ s0(b)
| ~ l0(X0)
| ~ p0(b,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_050) ).
fof(f92,axiom,
! [X2,X0,X1] :
( ~ l0(X2)
| n1(X0,X1,X1)
| ~ l1(X2,X0)
| ~ n1(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_054) ).
fof(f120,axiom,
! [X2,X3,X0,X1] :
( ~ p1(X2,X0,X3)
| ~ m0(X2,X0,X3)
| p1(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_082) ).
fof(f123,axiom,
! [X0,X1] :
( ~ p0(X1,X0)
| p1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_085) ).
fof(f126,axiom,
( p1(a,a,a)
| ~ l0(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_088) ).
fof(f163,axiom,
! [X0] :
( ~ p0(X0,X0)
| s1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_125) ).
fof(f164,axiom,
! [X2,X0,X1] :
( s1(X0)
| ~ q0(X0,X1)
| ~ s1(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_126) ).
fof(f171,axiom,
! [X2,X3,X0,X1] :
( l2(X0,X0)
| ~ p0(X1,X1)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_133) ).
fof(f175,axiom,
! [X2,X0,X1] :
( ~ p1(X1,X2,X0)
| n2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_137) ).
fof(f215,axiom,
! [X0,X1] :
( ~ k0(X1)
| q2(X0,X1,X1)
| ~ p1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_177) ).
fof(f220,axiom,
! [X2,X0,X1] :
( ~ q2(X1,X2,X0)
| ~ p1(X0,X0,X2)
| ~ n1(X1,X0,X2)
| q2(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_182) ).
fof(f224,axiom,
! [X0,X1] :
( ~ l1(X1,X0)
| q2(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_186) ).
fof(f227,axiom,
! [X0] :
( s2(X0)
| ~ q2(b,X0,b)
| ~ s1(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_189) ).
fof(f282,axiom,
! [X0] :
( ~ n2(X0)
| p3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_244) ).
fof(f311,axiom,
! [X2,X3,X0,X1] :
( ~ s2(X0)
| ~ q2(X2,X0,X2)
| s3(X0,X1)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_273) ).
fof(f317,axiom,
! [X2,X0,X1] :
( ~ s3(a,X0)
| ~ l2(X2,X1)
| m4(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_279) ).
fof(f337,axiom,
! [X2,X3,X0,X1] :
( ~ l1(X0,X2)
| ~ p3(X1,X2,X3)
| s4(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_299) ).
fof(f343,axiom,
! [X0] :
( m5(X0,X0)
| ~ s4(X0)
| ~ m4(e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_305) ).
fof(f369,negated_conjecture,
! [X0] : ~ m5(d,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f444,definition,
( spl0_20
<=> m4(e,e) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f446,plain,
( ~ m4(e,e)
| spl0_20 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f448,definition,
( spl0_21
<=> ! [X0] :
( m5(X0,X0)
| ~ s4(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f449,plain,
( ! [X0] :
( ~ s4(X0)
| m5(X0,X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f450,plain,
( ~ spl0_20
| spl0_21 ),
inference(avatar_split_clause,[],[f343,f448,f444]) ).
fof(f571,definition,
( spl0_52
<=> n0(c,d) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f572,plain,
( n0(c,d)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f607,definition,
( spl0_61
<=> ! [X1] : ~ s1(X1) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f608,plain,
( ! [X1] : ~ s1(X1)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f715,definition,
( spl0_88
<=> r0(b) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f716,plain,
( r0(b)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f886,definition,
( spl0_130
<=> s1(b) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f888,plain,
( ~ s1(b)
| spl0_130 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f890,definition,
( spl0_131
<=> ! [X0] :
( s2(X0)
| ~ q2(b,X0,b) ) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f891,plain,
( ! [X0] :
( ~ q2(b,X0,b)
| s2(X0) )
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f892,plain,
( ~ spl0_130
| spl0_131 ),
inference(avatar_split_clause,[],[f227,f890,f886]) ).
fof(f1091,definition,
( spl0_182
<=> k0(b) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f1092,plain,
( k0(b)
| ~ spl0_182 ),
inference(avatar_component_clause,[],[f1091]) ).
fof(f1133,definition,
( spl0_192
<=> ! [X1] : ~ p0(X1,X1) ),
introduced(definition,[new_symbols(definition,[spl0_192])],[avatar_definition]) ).
fof(f1134,plain,
( ! [X1] : ~ p0(X1,X1)
| ~ spl0_192 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1136,definition,
( spl0_193
<=> ! [X2,X0,X3] :
( l2(X0,X0)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_193])],[avatar_definition]) ).
fof(f1137,plain,
( ! [X2,X3,X0] :
( l2(X0,X0)
| ~ s1(X2)
| ~ m0(X3,X2,X0) )
| ~ spl0_193 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1138,plain,
( spl0_192
| spl0_193 ),
inference(avatar_split_clause,[],[f171,f1136,f1133]) ).
fof(f1149,definition,
( spl0_196
<=> ! [X0,X1] :
( s1(X0)
| ~ q0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_196])],[avatar_definition]) ).
fof(f1150,plain,
( ! [X0,X1] :
( ~ q0(X0,X1)
| s1(X0) )
| ~ spl0_196 ),
inference(avatar_component_clause,[],[f1149]) ).
fof(f1151,plain,
( spl0_61
| spl0_196 ),
inference(avatar_split_clause,[],[f164,f1149,f607]) ).
fof(f1162,definition,
( spl0_199
<=> s0(b) ),
introduced(definition,[new_symbols(definition,[spl0_199])],[avatar_definition]) ).
fof(f1188,definition,
( spl0_205
<=> ! [X2] : ~ r0(X2) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f1189,plain,
( ! [X2] : ~ r0(X2)
| ~ spl0_205 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1260,definition,
( spl0_223
<=> l0(a) ),
introduced(definition,[new_symbols(definition,[spl0_223])],[avatar_definition]) ).
fof(f1261,plain,
( l0(a)
| ~ spl0_223 ),
inference(avatar_component_clause,[],[f1260]) ).
fof(f1264,definition,
( spl0_224
<=> p1(a,a,a) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f1266,plain,
( p1(a,a,a)
| ~ spl0_224 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1267,plain,
( ~ spl0_223
| spl0_224 ),
inference(avatar_split_clause,[],[f126,f1264,f1260]) ).
fof(f1380,definition,
( spl0_252
<=> ! [X0,X1] :
( n1(X0,X1,X0)
| ~ p0(b,X1)
| ~ l0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f1381,plain,
( ! [X0,X1] :
( n1(X0,X1,X0)
| ~ p0(b,X1)
| ~ l0(X0) )
| ~ spl0_252 ),
inference(avatar_component_clause,[],[f1380]) ).
fof(f1382,plain,
( ~ spl0_199
| spl0_252 ),
inference(avatar_split_clause,[],[f88,f1380,f1162]) ).
fof(f1497,definition,
( spl0_280
<=> ! [X2,X0,X1] :
( l1(X0,X1)
| ~ m0(X1,X0,X2)
| ~ p0(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f1498,plain,
( ! [X2,X0,X1] :
( ~ p0(X2,X0)
| ~ m0(X1,X0,X2)
| l1(X0,X1) )
| ~ spl0_280 ),
inference(avatar_component_clause,[],[f1497]) ).
fof(f1499,plain,
( spl0_205
| spl0_280 ),
inference(avatar_split_clause,[],[f41,f1497,f1188]) ).
fof(f1500,plain,
spl0_52,
inference(avatar_split_clause,[],[f34,f571]) ).
fof(f1501,plain,
spl0_182,
inference(avatar_split_clause,[],[f32,f1091]) ).
fof(f1506,plain,
spl0_223,
inference(avatar_split_clause,[],[f20,f1260]) ).
fof(f1510,plain,
spl0_88,
inference(avatar_split_clause,[],[f9,f715]) ).
fof(f1512,plain,
spl0_199,
inference(avatar_split_clause,[],[f5,f1162]) ).
fof(f1535,plain,
( $false
| ~ spl0_88
| ~ spl0_205 ),
inference(resolution,[],[f1189,f716]) ).
fof(f1538,plain,
( ~ spl0_88
| ~ spl0_205 ),
inference(avatar_contradiction_clause,[],[f1535]) ).
fof(f1539,plain,
( $false
| ~ spl0_192 ),
inference(resolution,[],[f1134,f14]) ).
fof(f1540,plain,
~ spl0_192,
inference(avatar_contradiction_clause,[],[f1539]) ).
fof(f1547,plain,
( ! [X0,X1] :
( ~ l0(X0)
| n1(X0,X1,X0) )
| ~ spl0_252 ),
inference(forward_subsumption_resolution,[],[f1381,f14]) ).
fof(f1590,plain,
s1(b),
inference(resolution,[],[f163,f14]) ).
fof(f1591,plain,
( $false
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f1590,f608]) ).
fof(f1592,plain,
~ spl0_61,
inference(avatar_contradiction_clause,[],[f1591]) ).
fof(f1594,plain,
( $false
| spl0_130 ),
inference(forward_subsumption_resolution,[],[f1590,f888]) ).
fof(f1595,plain,
spl0_130,
inference(avatar_contradiction_clause,[],[f1594]) ).
fof(f1597,plain,
( ! [X0] : s1(X0)
| ~ spl0_196 ),
inference(resolution,[],[f1150,f17]) ).
fof(f1624,plain,
l1(a,a),
inference(resolution,[],[f40,f37]) ).
fof(f1625,plain,
( l1(d,d)
| ~ spl0_52 ),
inference(resolution,[],[f40,f572]) ).
fof(f1769,plain,
( ! [X0] : n1(a,X0,a)
| ~ spl0_223
| ~ spl0_252 ),
inference(resolution,[],[f1547,f1261]) ).
fof(f1797,plain,
! [X0] : p1(X0,X0,X0),
inference(resolution,[],[f123,f14]) ).
fof(f1820,plain,
! [X0] : n2(X0),
inference(resolution,[],[f1797,f175]) ).
fof(f1830,plain,
! [X0] : p3(X0,X0,X0),
inference(resolution,[],[f1820,f282]) ).
fof(f1898,plain,
( ! [X2,X3,X0] :
( ~ m0(X3,X2,X0)
| l2(X0,X0) )
| ~ spl0_193
| ~ spl0_196 ),
inference(forward_subsumption_resolution,[],[f1137,f1597]) ).
fof(f1951,plain,
( ! [X0] : l2(X0,X0)
| ~ spl0_193
| ~ spl0_196 ),
inference(resolution,[],[f1898,f19]) ).
fof(f2295,plain,
( ! [X0,X1] :
( ~ p3(X0,d,X1)
| s4(d) )
| ~ spl0_52 ),
inference(resolution,[],[f337,f1625]) ).
fof(f2337,definition,
( spl0_291
<=> s4(d) ),
introduced(definition,[new_symbols(definition,[spl0_291])],[avatar_definition]) ).
fof(f2339,plain,
( s4(d)
| ~ spl0_291 ),
inference(avatar_component_clause,[],[f2337]) ).
fof(f2341,definition,
( spl0_292
<=> ! [X0,X1] : ~ p3(X0,d,X1) ),
introduced(definition,[new_symbols(definition,[spl0_292])],[avatar_definition]) ).
fof(f2342,plain,
( ! [X0,X1] : ~ p3(X0,d,X1)
| ~ spl0_292 ),
inference(avatar_component_clause,[],[f2341]) ).
fof(f2343,plain,
( spl0_291
| spl0_292
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f2295,f571,f2341,f2337]) ).
fof(f2515,plain,
( ! [X0] :
( q2(X0,b,b)
| ~ p1(X0,X0,X0) )
| ~ spl0_182 ),
inference(resolution,[],[f215,f1092]) ).
fof(f2518,plain,
( ! [X0] : q2(X0,b,b)
| ~ spl0_182 ),
inference(forward_subsumption_resolution,[],[f2515,f1797]) ).
fof(f2590,plain,
( ! [X0,X1] :
( ~ m0(X0,X1,b)
| l1(X1,X0) )
| ~ spl0_280 ),
inference(resolution,[],[f1498,f14]) ).
fof(f2840,plain,
( ! [X0] :
( ~ m0(a,a,a)
| p1(a,X0,a) )
| ~ spl0_224 ),
inference(resolution,[],[f120,f1266]) ).
fof(f2879,plain,
( ! [X0] : p1(a,X0,a)
| ~ spl0_224 ),
inference(forward_subsumption_resolution,[],[f2840,f12]) ).
fof(f2894,plain,
( ! [X0,X1] :
( ~ m0(a,X0,a)
| p1(X0,X1,a) )
| ~ spl0_224 ),
inference(resolution,[],[f2879,f120]) ).
fof(f2899,plain,
( ! [X0,X1] : p1(X0,X1,a)
| ~ spl0_224 ),
inference(forward_subsumption_resolution,[],[f2894,f12]) ).
fof(f3080,plain,
( ! [X0,X1] :
( ~ l1(a,X0)
| n1(X0,X1,X1)
| ~ n1(X0,X1,X0) )
| ~ spl0_223 ),
inference(resolution,[],[f92,f1261]) ).
fof(f3220,plain,
( ! [X0] :
( ~ p1(b,b,b)
| ~ n1(X0,b,b)
| q2(b,X0,b) )
| ~ spl0_182 ),
inference(resolution,[],[f220,f2518]) ).
fof(f3226,plain,
( ! [X0] :
( ~ n1(X0,b,b)
| q2(b,X0,b) )
| ~ spl0_182 ),
inference(forward_subsumption_resolution,[],[f3220,f1797]) ).
fof(f3498,plain,
( ! [X0] : l1(d,X0)
| ~ spl0_280 ),
inference(resolution,[],[f2590,f19]) ).
fof(f3505,plain,
( ! [X0] : q2(X0,X0,d)
| ~ spl0_280 ),
inference(resolution,[],[f3498,f224]) ).
fof(f3522,plain,
( ! [X0] :
( ~ p1(d,d,X0)
| ~ n1(X0,d,X0)
| q2(d,X0,d) )
| ~ spl0_280 ),
inference(resolution,[],[f3505,f220]) ).
fof(f3853,plain,
( ! [X0] :
( n1(a,X0,X0)
| ~ n1(a,X0,a) )
| ~ spl0_223 ),
inference(resolution,[],[f3080,f1624]) ).
fof(f3854,plain,
( ! [X0] : n1(a,X0,X0)
| ~ spl0_223
| ~ spl0_252 ),
inference(forward_subsumption_resolution,[],[f3853,f1769]) ).
fof(f4191,plain,
( q2(b,a,b)
| ~ spl0_182
| ~ spl0_223
| ~ spl0_252 ),
inference(resolution,[],[f3226,f3854]) ).
fof(f4234,plain,
( s2(a)
| ~ spl0_131
| ~ spl0_182
| ~ spl0_223
| ~ spl0_252 ),
inference(resolution,[],[f4191,f891]) ).
fof(f4244,plain,
( ! [X2,X0,X1] :
( ~ q2(X0,a,X0)
| s3(a,X1)
| ~ m0(X0,X2,X1) )
| ~ spl0_131
| ~ spl0_182
| ~ spl0_223
| ~ spl0_252 ),
inference(resolution,[],[f4234,f311]) ).
fof(f5614,plain,
( ~ n1(a,d,a)
| q2(d,a,d)
| ~ spl0_224
| ~ spl0_280 ),
inference(resolution,[],[f3522,f2899]) ).
fof(f5615,plain,
( q2(d,a,d)
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(forward_subsumption_resolution,[],[f5614,f1769]) ).
fof(f6053,plain,
( ! [X0,X1] :
( ~ m0(d,X1,X0)
| s3(a,X0) )
| ~ spl0_131
| ~ spl0_182
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(resolution,[],[f4244,f5615]) ).
fof(f6272,plain,
( ! [X0] : s3(a,X0)
| ~ spl0_131
| ~ spl0_182
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(resolution,[],[f6053,f19]) ).
fof(f6273,plain,
( ! [X2,X0,X1] :
( ~ l2(X0,X1)
| m4(X2,X1) )
| ~ spl0_131
| ~ spl0_182
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(resolution,[],[f6272,f317]) ).
fof(f6280,plain,
( ! [X0,X1] : m4(X0,X1)
| ~ spl0_131
| ~ spl0_182
| ~ spl0_193
| ~ spl0_196
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(resolution,[],[f6273,f1951]) ).
fof(f6288,plain,
( $false
| spl0_20
| ~ spl0_131
| ~ spl0_182
| ~ spl0_193
| ~ spl0_196
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(resolution,[],[f6280,f446]) ).
fof(f6292,plain,
( spl0_20
| ~ spl0_131
| ~ spl0_182
| ~ spl0_193
| ~ spl0_196
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(avatar_contradiction_clause,[],[f6288]) ).
fof(f6294,plain,
( m5(d,d)
| ~ spl0_21
| ~ spl0_291 ),
inference(resolution,[],[f449,f2339]) ).
fof(f6299,plain,
( $false
| ~ spl0_21
| ~ spl0_291 ),
inference(forward_subsumption_resolution,[],[f6294,f369]) ).
fof(f6300,plain,
( ~ spl0_21
| ~ spl0_291 ),
inference(avatar_contradiction_clause,[],[f6299]) ).
fof(f6302,plain,
( $false
| ~ spl0_292 ),
inference(resolution,[],[f2342,f1830]) ).
fof(f6313,plain,
~ spl0_292,
inference(avatar_contradiction_clause,[],[f6302]) ).
cnf(s9,plain,
( ~ spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f450]) ).
cnf(s60,plain,
( ~ spl0_130
| spl0_131 ),
inference(sat_conversion,[],[f892]) ).
cnf(s88,plain,
( spl0_192
| spl0_193 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s90,plain,
( spl0_61
| spl0_196 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s108,plain,
( ~ spl0_223
| spl0_224 ),
inference(sat_conversion,[],[f1267]) ).
cnf(s125,plain,
( ~ spl0_199
| spl0_252 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s144,plain,
( spl0_205
| spl0_280 ),
inference(sat_conversion,[],[f1499]) ).
cnf(s145,plain,
spl0_52,
inference(sat_conversion,[],[f1500]) ).
cnf(s146,plain,
spl0_182,
inference(sat_conversion,[],[f1501]) ).
cnf(s151,plain,
spl0_223,
inference(sat_conversion,[],[f1506]) ).
cnf(s155,plain,
spl0_88,
inference(sat_conversion,[],[f1510]) ).
cnf(s157,plain,
spl0_199,
inference(sat_conversion,[],[f1512]) ).
cnf(s169,plain,
( ~ spl0_88
| ~ spl0_205 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s170,plain,
~ spl0_192,
inference(sat_conversion,[],[f1540]) ).
cnf(s191,plain,
~ spl0_61,
inference(sat_conversion,[],[f1592]) ).
cnf(s192,plain,
spl0_130,
inference(sat_conversion,[],[f1595]) ).
cnf(s289,plain,
( ~ spl0_52
| spl0_291
| spl0_292 ),
inference(sat_conversion,[],[f2343]) ).
cnf(s486,plain,
( spl0_20
| ~ spl0_131
| ~ spl0_182
| ~ spl0_193
| ~ spl0_196
| ~ spl0_223
| ~ spl0_224
| ~ spl0_252
| ~ spl0_280 ),
inference(sat_conversion,[],[f6292]) ).
cnf(s487,plain,
( ~ spl0_21
| ~ spl0_291 ),
inference(sat_conversion,[],[f6300]) ).
cnf(s493,plain,
~ spl0_292,
inference(sat_conversion,[],[f6313]) ).
cnf(s510,plain,
( ~ spl0_52
| spl0_291 ),
inference(rat,[],[s289,s493]) ).
cnf(s522,plain,
~ spl0_205,
inference(rat,[],[s169,s155]) ).
cnf(s539,plain,
spl0_291,
inference(rat,[],[s510,s145]) ).
cnf(s542,plain,
~ spl0_21,
inference(rat,[],[s487,s539]) ).
cnf(s543,plain,
spl0_280,
inference(rat,[],[s144,s522]) ).
cnf(s573,plain,
spl0_252,
inference(rat,[],[s125,s157]) ).
cnf(s593,plain,
spl0_224,
inference(rat,[],[s108,s151]) ).
cnf(s641,plain,
spl0_196,
inference(rat,[],[s90,s191]) ).
cnf(s649,plain,
spl0_193,
inference(rat,[],[s88,s170]) ).
cnf(s690,plain,
spl0_131,
inference(rat,[],[s60,s192]) ).
cnf(s691,plain,
spl0_20,
inference(rat,[],[s486,s543,s573,s593,s151,s641,s649,s146,s690]) ).
cnf(s759,plain,
$false,
inference(rat,[],[s9,s542,s691]) ).
fof(f6314,plain,
$false,
inference(avatar_sat_refutation,[],[s759]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN142-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 15:34:41 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.30 % (2496876)Will run a generic schedule for satisfiability detection.
% 0.19/0.30 % (2496886)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4030666793:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.30 % (2496882)% WARNING: option uhcvi not known.
% 0.19/0.30 % (2496881)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4162512639_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.30 % (2496882)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2105224849:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.30 % (2496883)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=824363452:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.30 % (2496884)dis+10_1_sil=32000:sp=arity:random_seed=4011661900:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.30 % (2496885)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=974036731:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.30 % (2496887)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3102632642:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.30 % Detected minimum model sizes of [1]
% 0.19/0.30 % Detected maximum model sizes of [5]
% 0.19/0.30 % TRYING [1]
% 0.19/0.30 % TRYING [2]
% 0.19/0.30 % TRYING [3]
% 0.19/0.30 % (2496886) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2496876-2496886"...
% 0.19/0.30 % (2496886)...printing done.
% 0.19/0.30 % (2496886)Refutation found. Thanks to Tanya!
% 0.19/0.30 % SZS status Unsatisfiable for theBenchmark
% 0.19/0.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.30 % (2496886)------------------------------
% 0.19/0.30 % (2496886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.30 % (2496886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.30 % (2496886)CaDiCaL version: 2.1.3
% 0.19/0.30 % (2496886)Termination reason: Refutation
% 0.19/0.30 % (2496886)Time elapsed: 0.039 s
% 0.19/0.30 % (2496886)Peak memory usage: 15 MB
% 0.19/0.30 % (2496886)Instructions burned: 103 (million)
% 0.19/0.30 % (2496876)Success in time 0.074 s
% 0.19/0.30 % Vampire exiting
%------------------------------------------------------------------------------