%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET837-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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 12:42:04 PM UTC 2026
% Result : Unsatisfiable 5.59s 2.06s
% Output : Refutation 8.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 22
% Syntax : Number of formulae : 126 ( 13 unt; 9 def)
% Number of atoms : 367 ( 24 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 444 ( 203 ~; 234 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-3 aty)
% Number of variables : 76 ( 0 sgn 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f215,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,c_union(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUnCI_0) ).
fof(f216,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,c_union(X1,X3,X2),X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUnCI_1) ).
fof(f217,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_union(X1,X2,X3),X3)
| c_in(X0,X2,X3)
| c_in(X0,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUnE_0) ).
fof(f378,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X1,X3,tc_set(X2))
| ~ c_in(X0,X1,X2)
| c_in(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetD_0) ).
fof(f379,axiom,
! [X2,X0,X1] :
( c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_0) ).
fof(f380,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_1) ).
fof(f381,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_set(X2))
| ~ c_lessequals(X1,X0,tc_set(X2))
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Osubset__antisym_0) ).
fof(f382,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2))
| X0 = X1 ),
inference(reorient_equations,[],[f381]) ).
fof(f1434,negated_conjecture,
( v_X = c_union(v_Y,v_Z,t_a)
| c_lessequals(v_Y,v_X,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1435,negated_conjecture,
( v_X = c_union(v_Y,v_Z,t_a)
| c_lessequals(v_Z,v_X,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1436,negated_conjecture,
( c_lessequals(v_Y,v_x,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X != c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1437,negated_conjecture,
( c_lessequals(v_Z,v_x,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X != c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1438,negated_conjecture,
( ~ c_lessequals(v_X,v_x,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X != c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f1439,negated_conjecture,
! [X0] :
( v_X = c_union(v_Y,v_Z,t_a)
| c_lessequals(v_X,X0,tc_set(t_a))
| ~ c_lessequals(v_Z,X0,tc_set(t_a))
| ~ c_lessequals(v_Y,X0,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f1440,definition,
sF0 = c_union(v_Y,v_Z,t_a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1441,plain,
c_union(v_Y,v_Z,t_a) = sF0,
inference(reorient_equations,[],[f1440]) ).
fof(f1442,definition,
sF1 = tc_set(t_a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1443,plain,
tc_set(t_a) = sF1,
inference(reorient_equations,[],[f1442]) ).
fof(f1444,plain,
( v_X = sF0
| c_lessequals(v_Y,v_X,sF1) ),
inference(definition_folding,[],[f1434,f1443,f1441]) ).
fof(f1445,plain,
( v_X = sF0
| c_lessequals(v_Z,v_X,sF1) ),
inference(definition_folding,[],[f1435,f1443,f1441]) ).
fof(f1446,plain,
( c_lessequals(v_Y,v_x,sF1)
| ~ c_lessequals(v_Z,v_X,sF1)
| ~ c_lessequals(v_Y,v_X,sF1)
| v_X != sF0 ),
inference(definition_folding,[],[f1436,f1441,f1443,f1443,f1443]) ).
fof(f1447,plain,
( c_lessequals(v_Z,v_x,sF1)
| ~ c_lessequals(v_Z,v_X,sF1)
| ~ c_lessequals(v_Y,v_X,sF1)
| v_X != sF0 ),
inference(definition_folding,[],[f1437,f1441,f1443,f1443,f1443]) ).
fof(f1448,plain,
( ~ c_lessequals(v_X,v_x,sF1)
| ~ c_lessequals(v_Z,v_X,sF1)
| ~ c_lessequals(v_Y,v_X,sF1)
| v_X != sF0 ),
inference(definition_folding,[],[f1438,f1441,f1443,f1443,f1443]) ).
fof(f1449,plain,
! [X0] :
( v_X = sF0
| c_lessequals(v_X,X0,sF1)
| ~ c_lessequals(v_Z,X0,sF1)
| ~ c_lessequals(v_Y,X0,sF1) ),
inference(definition_folding,[],[f1439,f1443,f1443,f1443,f1441]) ).
fof(f1451,definition,
( spl2_1
<=> ! [X0] :
( c_lessequals(v_X,X0,sF1)
| ~ c_lessequals(v_Y,X0,sF1)
| ~ c_lessequals(v_Z,X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f1452,plain,
( ! [X0] :
( c_lessequals(v_X,X0,sF1)
| ~ c_lessequals(v_Y,X0,sF1)
| ~ c_lessequals(v_Z,X0,sF1) )
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1454,definition,
( spl2_2
<=> v_X = sF0 ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f1455,plain,
( v_X != sF0
| spl2_2 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1456,plain,
( v_X = sF0
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1457,plain,
( spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f1449,f1454,f1451]) ).
fof(f1459,definition,
( spl2_3
<=> c_lessequals(v_Y,v_X,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f1460,plain,
( c_lessequals(v_Y,v_X,sF1)
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f1459]) ).
fof(f1461,plain,
( ~ c_lessequals(v_Y,v_X,sF1)
| spl2_3 ),
inference(avatar_component_clause,[],[f1459]) ).
fof(f1463,definition,
( spl2_4
<=> c_lessequals(v_Z,v_X,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f1464,plain,
( c_lessequals(v_Z,v_X,sF1)
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f1463]) ).
fof(f1467,definition,
( spl2_5
<=> c_lessequals(v_X,v_x,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f1469,plain,
( ~ c_lessequals(v_X,v_x,sF1)
| spl2_5 ),
inference(avatar_component_clause,[],[f1467]) ).
fof(f1470,plain,
( ~ spl2_2
| ~ spl2_3
| ~ spl2_4
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1448,f1467,f1463,f1459,f1454]) ).
fof(f1472,definition,
( spl2_6
<=> c_lessequals(v_Z,v_x,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f1474,plain,
( c_lessequals(v_Z,v_x,sF1)
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f1472]) ).
fof(f1475,plain,
( ~ spl2_2
| ~ spl2_3
| ~ spl2_4
| spl2_6 ),
inference(avatar_split_clause,[],[f1447,f1472,f1463,f1459,f1454]) ).
fof(f1477,definition,
( spl2_7
<=> c_lessequals(v_Y,v_x,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f1479,plain,
( c_lessequals(v_Y,v_x,sF1)
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f1477]) ).
fof(f1480,plain,
( ~ spl2_2
| ~ spl2_3
| ~ spl2_4
| spl2_7 ),
inference(avatar_split_clause,[],[f1446,f1477,f1463,f1459,f1454]) ).
fof(f1481,plain,
( spl2_4
| spl2_2 ),
inference(avatar_split_clause,[],[f1445,f1454,f1463]) ).
fof(f1482,plain,
( spl2_3
| spl2_2 ),
inference(avatar_split_clause,[],[f1444,f1454,f1459]) ).
fof(f1484,plain,
( v_X = c_union(v_Y,v_Z,t_a)
| ~ spl2_2 ),
inference(backward_demodulation,[],[f1441,f1456]) ).
fof(f1487,plain,
! [X0,X1] :
( ~ c_lessequals(X1,X0,sF1)
| ~ c_lessequals(X0,X1,sF1)
| X0 = X1 ),
inference(superposition,[],[f382,f1443]) ).
fof(f1492,plain,
( ! [X0] :
( c_in(X0,v_Z,t_a)
| ~ c_in(X0,v_X,t_a)
| c_in(X0,v_Y,t_a) )
| ~ spl2_2 ),
inference(superposition,[],[f217,f1484]) ).
fof(f1496,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,sF1)
| ~ c_in(X2,X0,t_a)
| c_in(X2,X1,t_a) ),
inference(superposition,[],[f378,f1443]) ).
fof(f1498,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Main_OsubsetI__1(X0,c_union(X1,X2,X3),X3),X2,X3)
| c_lessequals(X0,c_union(X1,X2,X3),tc_set(X3)) ),
inference(resolution,[],[f215,f380]) ).
fof(f1500,plain,
( ! [X0] :
( c_in(X0,v_X,t_a)
| ~ c_in(X0,v_Z,t_a) )
| ~ spl2_2 ),
inference(superposition,[],[f215,f1484]) ).
fof(f1501,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Z,t_a)
| c_lessequals(X0,v_X,tc_set(t_a)) )
| ~ spl2_2 ),
inference(resolution,[],[f1500,f380]) ).
fof(f1502,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Z,t_a)
| c_lessequals(X0,v_X,sF1) )
| ~ spl2_2 ),
inference(forward_demodulation,[],[f1501,f1443]) ).
fof(f1503,plain,
( c_lessequals(v_Z,v_X,sF1)
| c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ spl2_2 ),
inference(resolution,[],[f1502,f379]) ).
fof(f1505,plain,
( c_lessequals(v_Z,v_X,sF1)
| c_lessequals(v_Z,v_X,sF1)
| ~ spl2_2 ),
inference(forward_demodulation,[],[f1503,f1443]) ).
fof(f1506,plain,
( c_lessequals(v_Z,v_X,sF1)
| ~ spl2_2 ),
inference(duplicate_literal_removal,[],[f1505]) ).
fof(f1507,plain,
( spl2_4
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f1506,f1454,f1463]) ).
fof(f1508,plain,
( ! [X0] :
( c_in(X0,v_X,t_a)
| ~ c_in(X0,v_Z,t_a) )
| ~ spl2_4 ),
inference(resolution,[],[f1464,f1496]) ).
fof(f1519,plain,
! [X2,X0,X1] :
( c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2))
| c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)) ),
inference(resolution,[],[f1498,f379]) ).
fof(f1524,plain,
! [X2,X0,X1] : c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)),
inference(duplicate_literal_removal,[],[f1519]) ).
fof(f1536,plain,
( ! [X0] :
( c_in(X0,v_X,t_a)
| ~ c_in(X0,v_Y,t_a) )
| ~ spl2_2 ),
inference(superposition,[],[f216,f1484]) ).
fof(f1537,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)
| c_lessequals(X0,v_X,tc_set(t_a)) )
| ~ spl2_2 ),
inference(resolution,[],[f1536,f380]) ).
fof(f1540,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)
| c_lessequals(X0,v_X,sF1) )
| ~ spl2_2 ),
inference(forward_demodulation,[],[f1537,f1443]) ).
fof(f1542,plain,
( c_lessequals(v_Y,v_X,sF1)
| c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ spl2_2 ),
inference(resolution,[],[f1540,f379]) ).
fof(f1544,plain,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ spl2_2
| spl2_3 ),
inference(forward_subsumption_resolution,[],[f1542,f1461]) ).
fof(f1545,plain,
( c_lessequals(v_Y,v_X,sF1)
| ~ spl2_2
| spl2_3 ),
inference(forward_demodulation,[],[f1544,f1443]) ).
fof(f1546,plain,
( $false
| ~ spl2_2
| spl2_3 ),
inference(forward_subsumption_resolution,[],[f1545,f1461]) ).
fof(f1547,plain,
( ~ spl2_2
| spl2_3 ),
inference(avatar_contradiction_clause,[],[f1546]) ).
fof(f1548,plain,
( ! [X0] :
( c_in(X0,v_x,t_a)
| ~ c_in(X0,v_Z,t_a) )
| ~ spl2_6 ),
inference(resolution,[],[f1474,f1496]) ).
fof(f1559,plain,
( ! [X0] :
( c_in(X0,v_x,t_a)
| ~ c_in(X0,v_Y,t_a) )
| ~ spl2_7 ),
inference(resolution,[],[f1479,f1496]) ).
fof(f1570,plain,
( ! [X0] :
( c_in(X0,v_X,t_a)
| ~ c_in(X0,v_Y,t_a) )
| ~ spl2_3 ),
inference(resolution,[],[f1460,f1496]) ).
fof(f1581,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_Z,t_a)
| c_lessequals(X0,v_x,tc_set(t_a)) )
| ~ spl2_6 ),
inference(resolution,[],[f1548,f380]) ).
fof(f1584,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_Z,t_a)
| c_lessequals(X0,v_x,sF1) )
| ~ spl2_6 ),
inference(forward_demodulation,[],[f1581,f1443]) ).
fof(f1586,plain,
( ! [X0] :
( c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_Y,t_a)
| ~ c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_X,t_a)
| c_lessequals(X0,v_x,sF1) )
| ~ spl2_2
| ~ spl2_6 ),
inference(resolution,[],[f1584,f1492]) ).
fof(f1587,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_Y,t_a)
| c_lessequals(X0,v_x,tc_set(t_a)) )
| ~ spl2_7 ),
inference(resolution,[],[f1559,f380]) ).
fof(f1590,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_Y,t_a)
| c_lessequals(X0,v_x,sF1) )
| ~ spl2_7 ),
inference(forward_demodulation,[],[f1587,f1443]) ).
fof(f1595,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_X,t_a)
| c_lessequals(X0,v_x,sF1)
| c_lessequals(X0,v_x,sF1) )
| ~ spl2_2
| ~ spl2_6
| ~ spl2_7 ),
inference(resolution,[],[f1586,f1590]) ).
fof(f1596,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_X,t_a)
| c_lessequals(X0,v_x,sF1) )
| ~ spl2_2
| ~ spl2_6
| ~ spl2_7 ),
inference(duplicate_literal_removal,[],[f1595]) ).
fof(f1597,plain,
( c_lessequals(v_X,v_x,sF1)
| c_lessequals(v_X,v_x,tc_set(t_a))
| ~ spl2_2
| ~ spl2_6
| ~ spl2_7 ),
inference(resolution,[],[f1596,f379]) ).
fof(f1600,plain,
( c_lessequals(v_X,v_x,tc_set(t_a))
| ~ spl2_2
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f1597,f1469]) ).
fof(f1601,plain,
( c_lessequals(v_X,v_x,sF1)
| ~ spl2_2
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(forward_demodulation,[],[f1600,f1443]) ).
fof(f1602,plain,
( $false
| ~ spl2_2
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f1601,f1469]) ).
fof(f1603,plain,
( ~ spl2_2
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(avatar_contradiction_clause,[],[f1602]) ).
fof(f1604,plain,
! [X0] :
( c_in(X0,sF0,t_a)
| ~ c_in(X0,v_Y,t_a) ),
inference(superposition,[],[f216,f1441]) ).
fof(f1605,plain,
c_lessequals(v_Z,sF0,tc_set(t_a)),
inference(superposition,[],[f1524,f1441]) ).
fof(f1608,plain,
! [X0] :
( c_in(X0,v_Z,t_a)
| ~ c_in(X0,sF0,t_a)
| c_in(X0,v_Y,t_a) ),
inference(superposition,[],[f217,f1441]) ).
fof(f1610,plain,
c_lessequals(v_Z,sF0,sF1),
inference(forward_demodulation,[],[f1605,f1443]) ).
fof(f1659,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Z,t_a)
| c_lessequals(X0,v_X,tc_set(t_a)) )
| ~ spl2_4 ),
inference(resolution,[],[f1508,f380]) ).
fof(f1662,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Z,t_a)
| c_lessequals(X0,v_X,sF1) )
| ~ spl2_4 ),
inference(forward_demodulation,[],[f1659,f1443]) ).
fof(f1664,plain,
( ! [X0] :
( c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)
| ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),sF0,t_a)
| c_lessequals(X0,v_X,sF1) )
| ~ spl2_4 ),
inference(resolution,[],[f1662,f1608]) ).
fof(f1674,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)
| c_lessequals(X0,v_X,tc_set(t_a)) )
| ~ spl2_3 ),
inference(resolution,[],[f1570,f380]) ).
fof(f1677,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)
| c_lessequals(X0,v_X,sF1) )
| ~ spl2_3 ),
inference(forward_demodulation,[],[f1674,f1443]) ).
fof(f1679,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),sF0,t_a)
| c_lessequals(X0,v_X,sF1)
| c_lessequals(X0,v_X,sF1) )
| ~ spl2_3
| ~ spl2_4 ),
inference(resolution,[],[f1664,f1677]) ).
fof(f1680,plain,
( ! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),sF0,t_a)
| c_lessequals(X0,v_X,sF1) )
| ~ spl2_3
| ~ spl2_4 ),
inference(duplicate_literal_removal,[],[f1679]) ).
fof(f1681,plain,
( c_lessequals(sF0,v_X,sF1)
| c_lessequals(sF0,v_X,tc_set(t_a))
| ~ spl2_3
| ~ spl2_4 ),
inference(resolution,[],[f1680,f379]) ).
fof(f1682,plain,
( c_lessequals(sF0,v_X,sF1)
| c_lessequals(sF0,v_X,sF1)
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_demodulation,[],[f1681,f1443]) ).
fof(f1683,plain,
( c_lessequals(sF0,v_X,sF1)
| ~ spl2_3
| ~ spl2_4 ),
inference(duplicate_literal_removal,[],[f1682]) ).
fof(f1685,plain,
( ~ c_lessequals(v_X,sF0,sF1)
| v_X = sF0
| ~ spl2_3
| ~ spl2_4 ),
inference(resolution,[],[f1683,f1487]) ).
fof(f1686,plain,
( ~ c_lessequals(v_X,sF0,sF1)
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_subsumption_resolution,[],[f1685,f1455]) ).
fof(f1687,plain,
( ~ c_lessequals(v_Y,sF0,sF1)
| ~ c_lessequals(v_Z,sF0,sF1)
| ~ spl2_1
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(resolution,[],[f1686,f1452]) ).
fof(f1688,plain,
( ~ c_lessequals(v_Y,sF0,sF1)
| ~ spl2_1
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_subsumption_resolution,[],[f1687,f1610]) ).
fof(f1697,plain,
! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,sF0,t_a),v_Y,t_a)
| c_lessequals(X0,sF0,tc_set(t_a)) ),
inference(resolution,[],[f1604,f380]) ).
fof(f1700,plain,
! [X0] :
( ~ c_in(c_Main_OsubsetI__1(X0,sF0,t_a),v_Y,t_a)
| c_lessequals(X0,sF0,sF1) ),
inference(forward_demodulation,[],[f1697,f1443]) ).
fof(f1701,plain,
( c_lessequals(v_Y,sF0,sF1)
| c_lessequals(v_Y,sF0,tc_set(t_a)) ),
inference(resolution,[],[f1700,f379]) ).
fof(f1702,plain,
( c_lessequals(v_Y,sF0,tc_set(t_a))
| ~ spl2_1
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_subsumption_resolution,[],[f1701,f1688]) ).
fof(f1703,plain,
( c_lessequals(v_Y,sF0,sF1)
| ~ spl2_1
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_demodulation,[],[f1702,f1443]) ).
fof(f1704,plain,
( $false
| ~ spl2_1
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_subsumption_resolution,[],[f1703,f1688]) ).
fof(f1705,plain,
( ~ spl2_1
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(avatar_contradiction_clause,[],[f1704]) ).
cnf(s1,plain,
( spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s2,plain,
( ~ spl2_2
| ~ spl2_3
| ~ spl2_4
| ~ spl2_5 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s3,plain,
( ~ spl2_2
| ~ spl2_3
| ~ spl2_4
| spl2_6 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s4,plain,
( ~ spl2_2
| ~ spl2_3
| ~ spl2_4
| spl2_7 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s5,plain,
( spl2_2
| spl2_4 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s6,plain,
( spl2_2
| spl2_3 ),
inference(sat_conversion,[],[f1482]) ).
cnf(s7,plain,
( ~ spl2_2
| spl2_4 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s9,plain,
( ~ spl2_2
| spl2_3 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s13,plain,
( ~ spl2_2
| spl2_5
| ~ spl2_6
| ~ spl2_7 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s18,plain,
( ~ spl2_1
| spl2_2
| ~ spl2_3
| ~ spl2_4 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s19,plain,
( ~ spl2_3
| ~ spl2_2
| ~ spl2_4 ),
inference(rat,[],[s13,s2,s3,s4]) ).
cnf(s20,plain,
~ spl2_2,
inference(rat,[],[s19,s7,s9]) ).
cnf(s21,plain,
spl2_3,
inference(rat,[],[s6,s20]) ).
cnf(s22,plain,
spl2_4,
inference(rat,[],[s5,s20]) ).
cnf(s23,plain,
spl2_1,
inference(rat,[],[s1,s20]) ).
cnf(s24,plain,
$false,
inference(rat,[],[s18,s22,s20,s21,s23]) ).
fof(f1706,plain,
$false,
inference(avatar_sat_refutation,[],[s24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET837-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.37 % Computer : n018.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 28 02:59:09 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.41 Running first-order theorem proving
% 0.08/0.41 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
% 5.59/2.06 % (2953063)Input is clausal, will run a generic CNF schedule.
% 5.59/2.06 % (2953074)dis-21_1_sil=8000:lcm=predicate:random_seed=3249347835: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)
% 5.59/2.06 % (2953074)Instruction limit reached!
% 5.59/2.06 % (2953074)------------------------------
% 5.59/2.06 % (2953074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953074)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953074)Termination reason: Instruction limit
% 5.59/2.06 % (2953074)Termination phase: Saturation
% 5.59/2.06 % (2953074)Time elapsed: 0.038 s
% 5.59/2.06 % (2953074)Peak memory usage: 89 MB
% 5.59/2.06 % (2953074)Instructions burned: 119 (million)
% 5.59/2.06 % (2953070)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2588943575:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.59/2.06 % (2953069)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3041265905:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.59/2.06 % (2953072)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1906280648:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.59/2.06 % (2953068)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=1455970627:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.59/2.06 % (2953071)lrs+10_1_sil=8000:sp=occurrence:random_seed=2115436376:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.59/2.06 % (2953071)Refutation not found, incomplete strategy
% 5.59/2.06 % (2953071)------------------------------
% 5.59/2.06 % (2953071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953071)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953071)Termination reason: Refutation not found, incomplete strategy
% 5.59/2.06 % (2953071)Time elapsed: 0.005 s
% 5.59/2.06 % (2953071)Peak memory usage: 89 MB
% 5.59/2.06 % (2953071)Instructions burned: 5 (million)
% 5.59/2.06 % (2953073)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3590183087:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.59/2.06 % (2953072)Instruction limit reached!
% 5.59/2.06 % (2953072)------------------------------
% 5.59/2.06 % (2953072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953072)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953072)Termination reason: Instruction limit
% 5.59/2.06 % (2953072)Termination phase: Saturation
% 5.59/2.06 % (2953072)Time elapsed: 0.067 s
% 5.59/2.06 % (2953072)Peak memory usage: 88 MB
% 5.59/2.06 % (2953072)Instructions burned: 115 (million)
% 5.59/2.06 % (2953081)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=2968073051:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.59/2.06 % (2953081)Refutation not found, incomplete strategy
% 5.59/2.06 % (2953081)------------------------------
% 5.59/2.06 % (2953081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953081)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953081)Termination reason: Refutation not found, incomplete strategy
% 5.59/2.06 % (2953081)Time elapsed: 0.002 s
% 5.59/2.06 % (2953081)Peak memory usage: 89 MB
% 5.59/2.06 % (2953081)Instructions burned: 4 (million)
% 5.59/2.06 % (2953073)Instruction limit reached!
% 5.59/2.06 % (2953073)------------------------------
% 5.59/2.06 % (2953073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953073)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953073)Termination reason: Instruction limit
% 5.59/2.06 % (2953073)Termination phase: Saturation
% 5.59/2.06 % (2953073)Time elapsed: 0.120 s
% 5.59/2.06 % (2953073)Peak memory usage: 90 MB
% 5.59/2.06 % (2953073)Instructions burned: 181 (million)
% 5.59/2.06 % (2953083)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4237830993: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)
% 5.59/2.06 % (2953071)------------------------------
% 5.59/2.06 % (2953071)------------------------------
% 5.59/2.06 % (2953081)------------------------------
% 5.59/2.06 % (2953081)------------------------------
% 5.59/2.06 % (2953085)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3002950513:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 5.59/2.06 % (2953085)Refutation not found, incomplete strategy
% 5.59/2.06 % (2953085)------------------------------
% 5.59/2.06 % (2953085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953085)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953085)Termination reason: Refutation not found, incomplete strategy
% 5.59/2.06 % (2953085)Time elapsed: 0.009 s
% 5.59/2.06 % (2953085)Peak memory usage: 89 MB
% 5.59/2.06 % (2953085)Instructions burned: 12 (million)
% 5.59/2.06 % (2953083)Instruction limit reached!
% 5.59/2.06 % (2953083)------------------------------
% 5.59/2.06 % (2953083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953083)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953083)Termination reason: Instruction limit
% 5.59/2.06 % (2953083)Termination phase: Saturation
% 5.59/2.06 % (2953083)Time elapsed: 0.112 s
% 5.59/2.06 % (2953083)Peak memory usage: 91 MB
% 5.59/2.06 % (2953083)Instructions burned: 189 (million)
% 5.59/2.06 % (2953088)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=182659421:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.59/2.06 % (2953087)lrs+10_64_to=lpo:sil=8000:random_seed=2951056895:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.59/2.06 % (2953088)Instruction limit reached!
% 5.59/2.06 % (2953088)------------------------------
% 5.59/2.06 % (2953088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953088)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953088)Termination reason: Instruction limit
% 5.59/2.06 % (2953088)Termination phase: Saturation
% 5.59/2.06 % (2953088)Time elapsed: 0.070 s
% 5.59/2.06 % (2953088)Peak memory usage: 90 MB
% 5.59/2.06 % (2953088)Instructions burned: 199 (million)
% 5.59/2.06 % (2953087)Instruction limit reached!
% 5.59/2.06 % (2953087)------------------------------
% 5.59/2.06 % (2953087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953087)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953087)Termination reason: Instruction limit
% 5.59/2.06 % (2953087)Termination phase: Saturation
% 5.59/2.06 % (2953087)Time elapsed: 0.081 s
% 5.59/2.06 % (2953087)Peak memory usage: 90 MB
% 5.59/2.06 % (2953087)Instructions burned: 127 (million)
% 5.59/2.06 % (2953090)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3156156244:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 5.59/2.06 % (2953085)------------------------------
% 5.59/2.06 % (2953085)------------------------------
% 5.59/2.06 % (2953093)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3698994859:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.59/2.06 % (2953090)Instruction limit reached!
% 5.59/2.06 % (2953090)------------------------------
% 5.59/2.06 % (2953090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953090)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953090)Termination reason: Instruction limit
% 5.59/2.06 % (2953090)Termination phase: Saturation
% 5.59/2.06 % (2953090)Time elapsed: 0.095 s
% 5.59/2.06 % (2953090)Peak memory usage: 91 MB
% 5.59/2.06 % (2953090)Instructions burned: 158 (million)
% 5.59/2.06 % (2953094)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=507026472:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.59/2.06 % (2953094)Instruction limit reached!
% 5.59/2.06 % (2953094)------------------------------
% 5.59/2.06 % (2953094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953094)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953094)Termination reason: Instruction limit
% 5.59/2.06 % (2953094)Termination phase: Saturation
% 5.59/2.06 % (2953094)Time elapsed: 0.056 s
% 5.59/2.06 % (2953094)Peak memory usage: 89 MB
% 5.59/2.06 % (2953094)Instructions burned: 107 (million)
% 5.59/2.06 % (2953096)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3977780586:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 5.59/2.06 % (2953070)First to succeed.
% 5.59/2.06 % (2953070)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2953063"
% 5.59/2.06 % (2953098)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2197479481:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 5.59/2.06 % (2953068)Also succeeded, but the first one will report.
% 5.59/2.06 % (2953096)Instruction limit reached!
% 5.59/2.06 % (2953096)------------------------------
% 5.59/2.06 % (2953096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953096)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953096)Termination reason: Instruction limit
% 5.59/2.06 % (2953096)Termination phase: Saturation
% 5.59/2.06 % (2953096)Time elapsed: 0.072 s
% 5.59/2.06 % (2953096)Peak memory usage: 89 MB
% 5.59/2.06 % (2953096)Instructions burned: 107 (million)
% 5.59/2.06 % (2953101)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=519711099:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 5.59/2.06 % (2953098)Instruction limit reached!
% 5.59/2.06 % (2953098)------------------------------
% 5.59/2.06 % (2953098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/2.06 % (2953098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/2.06 % (2953098)CaDiCaL version: 2.1.3
% 5.59/2.06 % (2953098)Termination reason: Instruction limit
% 5.59/2.06 % (2953098)Termination phase: Saturation
% 5.59/2.06 % (2953098)Time elapsed: 0.128 s
% 5.59/2.06 % (2953098)Peak memory usage: 89 MB
% 5.59/2.06 % (2953098)Instructions burned: 242 (million)
% 5.59/2.06 % (2953103)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2952002649:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 5.59/2.06 % (2953070)Refutation found. Thanks to Tanya!
% 5.59/2.06 % SZS status Unsatisfiable for theBenchmark
% 5.59/2.06 % SZS output start Proof for theBenchmark
% See solution above
% 8.94/2.25 % (2953070)------------------------------
% 8.94/2.25 % (2953070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.25 % (2953070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.25 % (2953070)CaDiCaL version: 2.1.3
% 8.94/2.25 % (2953070)Termination reason: Refutation
% 8.94/2.25 % (2953070)Time elapsed: 0.754 s
% 8.94/2.25 % (2953070)Peak memory usage: 137 MB
% 8.94/2.25 % (2953070)Instructions burned: 1140 (million)
% 8.94/2.25 % (2953070)------------------------------
% 8.94/2.25 % (2953070)------------------------------
% 8.94/2.25 % (2953063)Success in time 1.207 s
% 8.94/2.25 % Vampire exiting
%------------------------------------------------------------------------------