%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU156+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:47:28 PM UTC 2026
% Result : Theorem 2.19s 1.16s
% Output : Refutation 2.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 18
% Syntax : Number of formulae : 151 ( 26 unt; 12 def)
% Number of atoms : 425 ( 167 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 470 ( 196 ~; 225 |; 33 &)
% ( 14 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 11 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-3 aty)
% Number of variables : 96 ( 0 sgn 87 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f7,axiom,
! [X0,X1] :
( X1 = singleton(X0)
<=> ! [X2] :
( in(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
fof(f10,axiom,
! [X0,X1,X2] :
( X2 = unordered_pair(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( X3 = X0
| X3 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tarski) ).
fof(f16,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f61,conjecture,
! [X0,X1,X2,X3] :
( ordered_pair(X0,X1) = ordered_pair(X2,X3)
=> ( X0 = X2
& X1 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_zfmisc_1) ).
fof(f62,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ordered_pair(X0,X1) = ordered_pair(X2,X3)
=> ( X0 = X2
& X1 = X3 ) ),
inference(negated_conjecture,[status(cth)],[f61]) ).
fof(f76,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f109,plain,
? [X0,X1,X2,X3] :
( ( X0 != X2
| X1 != X3 )
& ordered_pair(X0,X1) = ordered_pair(X2,X3) ),
inference(ennf_transformation,[],[f62]) ).
fof(f133,plain,
( ( sK0 != sK2
| sK1 != sK3 )
& ordered_pair(sK0,sK1) = ordered_pair(sK2,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f109]) ).
fof(f138,plain,
! [X0,X1] :
( ( X1 = singleton(X0)
| ? [X2] :
( ( X0 != X2
| ~ in(X2,X1) )
& ( X2 = X0
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| X0 != X2 )
& ( X2 = X0
| ~ in(X2,X1) ) )
| singleton(X0) != X1 ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f139,plain,
! [X0,X1] :
( ( X1 = singleton(X0)
| ? [X2] :
( ( X0 != X2
| ~ in(X2,X1) )
& ( X2 = X0
| in(X2,X1) ) ) )
& ( ! [X3] :
( ( in(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ in(X3,X1) ) )
| singleton(X0) != X1 ) ),
inference(rectify,[],[f138]) ).
fof(f140,plain,
! [X0,X1] :
( ( X1 = singleton(X0)
| ( ( sK6(X0,X1) != X0
| ~ in(sK6(X0,X1),X1) )
& ( sK6(X0,X1) = X0
| in(sK6(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( in(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ in(X3,X1) ) )
| singleton(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X2,sK6(X0,X1))],[f139]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ in(X3,X2) )
& ( X3 = X0
| X3 = X1
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( X0 != X3
& X1 != X3 ) )
& ( X3 = X0
| X3 = X1
| ~ in(X3,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f164,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ in(X3,X2) )
& ( X3 = X0
| X3 = X1
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( X0 != X3
& X1 != X3 ) )
& ( X3 = X0
| X3 = X1
| ~ in(X3,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(flattening,[],[f163]) ).
fof(f165,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ in(X3,X2) )
& ( X3 = X0
| X3 = X1
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( X0 != X4
& X1 != X4 ) )
& ( X0 = X4
| X1 = X4
| ~ in(X4,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(rectify,[],[f164]) ).
fof(f166,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ( ( ( sK15(X0,X1,X2) != X0
& sK15(X0,X1,X2) != X1 )
| ~ in(sK15(X0,X1,X2),X2) )
& ( sK15(X0,X1,X2) = X0
| sK15(X0,X1,X2) = X1
| in(sK15(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( X0 != X4
& X1 != X4 ) )
& ( X0 = X4
| X1 = X4
| ~ in(X4,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X3,sK15(X0,X1,X2))],[f165]) ).
fof(f197,plain,
ordered_pair(sK0,sK1) = ordered_pair(sK2,sK3),
inference(cnf_transformation,[],[f133]) ).
fof(f198,plain,
( sK0 != sK2
| sK1 != sK3 ),
inference(cnf_transformation,[],[f133]) ).
fof(f214,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f76]) ).
fof(f222,plain,
! [X3,X0,X1] :
( X0 = X3
| ~ in(X3,X1)
| singleton(X0) != X1 ),
inference(cnf_transformation,[],[f140]) ).
fof(f264,plain,
! [X2,X0,X1,X4] :
( X0 = X4
| X1 = X4
| ~ in(X4,X2)
| unordered_pair(X0,X1) != X2 ),
inference(cnf_transformation,[],[f166]) ).
fof(f265,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| X1 != X4
| unordered_pair(X0,X1) != X2 ),
inference(cnf_transformation,[],[f166]) ).
fof(f266,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| X0 != X4
| unordered_pair(X0,X1) != X2 ),
inference(cnf_transformation,[],[f166]) ).
fof(f270,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f284,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f16]) ).
fof(f288,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f284,f214]) ).
fof(f304,plain,
unordered_pair(unordered_pair(sK0,sK1),unordered_pair(sK0,sK0)) = unordered_pair(unordered_pair(sK2,sK3),unordered_pair(sK2,sK2)),
inference(definition_unfolding,[],[f197,f288,f288]) ).
fof(f313,plain,
! [X3,X0,X1] :
( X0 = X3
| ~ in(X3,X1)
| unordered_pair(X0,X0) != X1 ),
inference(definition_unfolding,[],[f222,f214]) ).
fof(f331,definition,
~ sP21(sK0),
introduced(definition,[new_symbols(definition,[sP21])],[inequality_splitting_name_introduction]) ).
fof(f332,definition,
~ sP22(sK1),
introduced(definition,[new_symbols(definition,[sP22])],[inequality_splitting_name_introduction]) ).
fof(f333,plain,
( sP21(sK2)
| sP22(sK3) ),
inference(inequality_splitting,[],[f198,f332,f331]) ).
fof(f343,plain,
! [X3,X0] :
( ~ in(X3,unordered_pair(X0,X0))
| X0 = X3 ),
inference(equality_resolution,[],[f313]) ).
fof(f355,plain,
! [X2,X1,X4] :
( in(X4,X2)
| unordered_pair(X4,X1) != X2 ),
inference(equality_resolution,[],[f266]) ).
fof(f356,plain,
! [X1,X4] : in(X4,unordered_pair(X4,X1)),
inference(equality_resolution,[],[f355]) ).
fof(f357,plain,
! [X2,X0,X4] :
( in(X4,X2)
| unordered_pair(X0,X4) != X2 ),
inference(equality_resolution,[],[f265]) ).
fof(f358,plain,
! [X0,X4] : in(X4,unordered_pair(X0,X4)),
inference(equality_resolution,[],[f357]) ).
fof(f359,plain,
! [X0,X1,X4] :
( ~ in(X4,unordered_pair(X0,X1))
| X1 = X4
| X0 = X4 ),
inference(equality_resolution,[],[f264]) ).
fof(f366,plain,
unordered_pair(unordered_pair(sK0,sK1),unordered_pair(sK0,sK0)) = unordered_pair(unordered_pair(sK2,sK2),unordered_pair(sK2,sK3)),
inference(forward_demodulation,[],[f304,f270]) ).
fof(f368,definition,
( spl26_1
<=> sP22(sK3) ),
introduced(definition,[new_symbols(definition,[spl26_1])],[avatar_definition]) ).
fof(f370,plain,
( sP22(sK3)
| ~ spl26_1 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f372,definition,
( spl26_2
<=> sP21(sK2) ),
introduced(definition,[new_symbols(definition,[spl26_2])],[avatar_definition]) ).
fof(f374,plain,
( sP21(sK2)
| ~ spl26_2 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f375,plain,
( spl26_1
| spl26_2 ),
inference(avatar_split_clause,[],[f333,f372,f368]) ).
fof(f376,plain,
unordered_pair(unordered_pair(sK2,sK2),unordered_pair(sK2,sK3)) = unordered_pair(unordered_pair(sK0,sK0),unordered_pair(sK0,sK1)),
inference(forward_demodulation,[],[f366,f270]) ).
fof(f377,plain,
! [X0] :
( ~ in(X0,unordered_pair(unordered_pair(sK0,sK0),unordered_pair(sK0,sK1)))
| unordered_pair(sK2,sK3) = X0
| unordered_pair(sK2,sK2) = X0 ),
inference(superposition,[],[f359,f376]) ).
fof(f378,plain,
in(unordered_pair(sK2,sK3),unordered_pair(unordered_pair(sK0,sK0),unordered_pair(sK0,sK1))),
inference(superposition,[],[f358,f376]) ).
fof(f379,plain,
in(unordered_pair(sK2,sK2),unordered_pair(unordered_pair(sK0,sK0),unordered_pair(sK0,sK1))),
inference(superposition,[],[f356,f376]) ).
fof(f380,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK2,sK3)
| unordered_pair(sK0,sK0) = unordered_pair(sK2,sK3) ),
inference(resolution,[],[f378,f359]) ).
fof(f384,definition,
( spl26_3
<=> unordered_pair(sK0,sK0) = unordered_pair(sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl26_3])],[avatar_definition]) ).
fof(f386,plain,
( unordered_pair(sK0,sK0) = unordered_pair(sK2,sK3)
| ~ spl26_3 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f388,definition,
( spl26_4
<=> unordered_pair(sK0,sK1) = unordered_pair(sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl26_4])],[avatar_definition]) ).
fof(f389,plain,
( unordered_pair(sK0,sK1) != unordered_pair(sK2,sK3)
| spl26_4 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f390,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK2,sK3)
| ~ spl26_4 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f391,plain,
( spl26_3
| spl26_4 ),
inference(avatar_split_clause,[],[f380,f388,f384]) ).
fof(f395,plain,
( in(sK3,unordered_pair(sK0,sK0))
| ~ spl26_3 ),
inference(superposition,[],[f358,f386]) ).
fof(f396,plain,
( in(sK2,unordered_pair(sK0,sK0))
| ~ spl26_3 ),
inference(superposition,[],[f356,f386]) ).
fof(f398,plain,
( sK0 = sK3
| sK0 = sK3
| ~ spl26_3 ),
inference(resolution,[],[f395,f359]) ).
fof(f413,plain,
( sK0 = sK2
| sK0 = sK2
| ~ spl26_3 ),
inference(resolution,[],[f396,f359]) ).
fof(f416,plain,
( sK0 = sK2
| ~ spl26_3 ),
inference(duplicate_literal_removal,[],[f413]) ).
fof(f424,plain,
( sP21(sK0)
| ~ spl26_2
| ~ spl26_3 ),
inference(superposition,[],[f374,f416]) ).
fof(f425,plain,
( $false
| ~ spl26_2
| ~ spl26_3 ),
inference(forward_subsumption_resolution,[],[f424,f331]) ).
fof(f426,plain,
( ~ spl26_2
| ~ spl26_3 ),
inference(avatar_contradiction_clause,[],[f425]) ).
fof(f440,plain,
( in(sK3,unordered_pair(sK0,sK1))
| ~ spl26_4 ),
inference(superposition,[],[f358,f390]) ).
fof(f441,plain,
( in(sK2,unordered_pair(sK0,sK1))
| ~ spl26_4 ),
inference(superposition,[],[f356,f390]) ).
fof(f449,plain,
( sK1 = sK3
| sK0 = sK3
| ~ spl26_4 ),
inference(resolution,[],[f440,f359]) ).
fof(f453,definition,
( spl26_5
<=> sK0 = sK3 ),
introduced(definition,[new_symbols(definition,[spl26_5])],[avatar_definition]) ).
fof(f455,plain,
( sK0 = sK3
| ~ spl26_5 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f457,definition,
( spl26_6
<=> sK1 = sK3 ),
introduced(definition,[new_symbols(definition,[spl26_6])],[avatar_definition]) ).
fof(f458,plain,
( sK1 != sK3
| spl26_6 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( sK1 = sK3
| ~ spl26_6 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f460,plain,
( spl26_5
| spl26_6
| ~ spl26_4 ),
inference(avatar_split_clause,[],[f449,f388,f457,f453]) ).
fof(f478,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK2,sK0)
| ~ spl26_4
| ~ spl26_5 ),
inference(superposition,[],[f390,f455]) ).
fof(f485,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK0,sK2)
| ~ spl26_4
| ~ spl26_5 ),
inference(forward_demodulation,[],[f478,f270]) ).
fof(f502,plain,
( sK1 = sK2
| sK0 = sK2
| ~ spl26_4 ),
inference(resolution,[],[f441,f359]) ).
fof(f507,definition,
( spl26_7
<=> sK0 = sK2 ),
introduced(definition,[new_symbols(definition,[spl26_7])],[avatar_definition]) ).
fof(f508,plain,
( sK0 != sK2
| spl26_7 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( sK0 = sK2
| ~ spl26_7 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f511,definition,
( spl26_8
<=> sK1 = sK2 ),
introduced(definition,[new_symbols(definition,[spl26_8])],[avatar_definition]) ).
fof(f513,plain,
( sK1 = sK2
| ~ spl26_8 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f514,plain,
( spl26_7
| spl26_8
| ~ spl26_4 ),
inference(avatar_split_clause,[],[f502,f388,f511,f507]) ).
fof(f521,plain,
( sP21(sK0)
| ~ spl26_2
| ~ spl26_7 ),
inference(superposition,[],[f374,f509]) ).
fof(f533,plain,
( $false
| ~ spl26_2
| ~ spl26_7 ),
inference(forward_subsumption_resolution,[],[f521,f331]) ).
fof(f534,plain,
( ~ spl26_2
| ~ spl26_7 ),
inference(avatar_contradiction_clause,[],[f533]) ).
fof(f648,plain,
( in(sK1,unordered_pair(sK0,sK2))
| ~ spl26_4
| ~ spl26_5 ),
inference(superposition,[],[f358,f485]) ).
fof(f671,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK2,sK2)
| unordered_pair(sK0,sK0) = unordered_pair(sK2,sK2) ),
inference(resolution,[],[f379,f359]) ).
fof(f677,plain,
( unordered_pair(sK2,sK2) = unordered_pair(sK0,sK2)
| unordered_pair(sK0,sK0) = unordered_pair(sK2,sK2)
| ~ spl26_4
| ~ spl26_5 ),
inference(forward_demodulation,[],[f671,f485]) ).
fof(f679,definition,
( spl26_9
<=> unordered_pair(sK0,sK0) = unordered_pair(sK2,sK2) ),
introduced(definition,[new_symbols(definition,[spl26_9])],[avatar_definition]) ).
fof(f681,plain,
( unordered_pair(sK0,sK0) = unordered_pair(sK2,sK2)
| ~ spl26_9 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f683,definition,
( spl26_10
<=> unordered_pair(sK2,sK2) = unordered_pair(sK0,sK2) ),
introduced(definition,[new_symbols(definition,[spl26_10])],[avatar_definition]) ).
fof(f685,plain,
( unordered_pair(sK2,sK2) = unordered_pair(sK0,sK2)
| ~ spl26_10 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f686,plain,
( spl26_9
| spl26_10
| ~ spl26_4
| ~ spl26_5 ),
inference(avatar_split_clause,[],[f677,f453,f388,f683,f679]) ).
fof(f691,plain,
( unordered_pair(sK2,sK2) = unordered_pair(sK0,sK2)
| unordered_pair(sK0,sK0) = unordered_pair(sK2,sK2)
| ~ spl26_8 ),
inference(forward_demodulation,[],[f671,f513]) ).
fof(f692,plain,
( spl26_9
| spl26_10
| ~ spl26_8 ),
inference(avatar_split_clause,[],[f691,f511,f683,f679]) ).
fof(f797,plain,
( ! [X0] :
( ~ in(X0,unordered_pair(sK0,sK2))
| sK2 = X0 )
| ~ spl26_10 ),
inference(superposition,[],[f343,f685]) ).
fof(f1309,plain,
( sK0 = sK2
| ~ spl26_10 ),
inference(resolution,[],[f797,f356]) ).
fof(f1331,plain,
( $false
| spl26_7
| ~ spl26_10 ),
inference(forward_subsumption_resolution,[],[f1309,f508]) ).
fof(f1332,plain,
( spl26_7
| ~ spl26_10 ),
inference(avatar_contradiction_clause,[],[f1331]) ).
fof(f1389,plain,
( sP22(sK1)
| ~ spl26_1
| ~ spl26_6 ),
inference(superposition,[],[f370,f459]) ).
fof(f1399,plain,
( $false
| ~ spl26_1
| ~ spl26_6 ),
inference(forward_subsumption_resolution,[],[f1389,f332]) ).
fof(f1400,plain,
( ~ spl26_1
| ~ spl26_6 ),
inference(avatar_contradiction_clause,[],[f1399]) ).
fof(f1403,plain,
( sK0 = sK3
| ~ spl26_3 ),
inference(duplicate_literal_removal,[],[f398]) ).
fof(f1408,plain,
( spl26_5
| ~ spl26_3 ),
inference(avatar_split_clause,[],[f1403,f384,f453]) ).
fof(f1414,plain,
( in(sK1,unordered_pair(sK0,sK0))
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(forward_demodulation,[],[f648,f509]) ).
fof(f1416,plain,
( sK0 != sK1
| ~ spl26_5
| spl26_6 ),
inference(forward_demodulation,[],[f458,f455]) ).
fof(f1854,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK2,sK3)
| unordered_pair(sK0,sK1) = unordered_pair(sK2,sK2) ),
inference(resolution,[],[f377,f358]) ).
fof(f1954,plain,
( sK0 = sK1
| sK0 = sK1
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(resolution,[],[f1414,f359]) ).
fof(f1958,plain,
( sK0 = sK1
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(duplicate_literal_removal,[],[f1954]) ).
fof(f1963,plain,
( unordered_pair(sK0,sK1) != unordered_pair(sK2,sK0)
| spl26_4
| ~ spl26_5 ),
inference(forward_demodulation,[],[f389,f455]) ).
fof(f1979,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK2,sK0)
| unordered_pair(sK0,sK1) = unordered_pair(sK2,sK2)
| ~ spl26_5 ),
inference(forward_demodulation,[],[f1854,f455]) ).
fof(f1981,plain,
( unordered_pair(sK0,sK1) != unordered_pair(sK0,sK2)
| spl26_4
| ~ spl26_5 ),
inference(forward_demodulation,[],[f1963,f270]) ).
fof(f1996,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK0,sK2)
| unordered_pair(sK0,sK1) = unordered_pair(sK2,sK2)
| ~ spl26_5 ),
inference(forward_demodulation,[],[f1979,f270]) ).
fof(f1998,plain,
( unordered_pair(sK0,sK1) != unordered_pair(sK0,sK0)
| spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(forward_demodulation,[],[f1981,f509]) ).
fof(f2013,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK0,sK0)
| unordered_pair(sK0,sK1) = unordered_pair(sK2,sK2)
| ~ spl26_5
| ~ spl26_7 ),
inference(forward_demodulation,[],[f1996,f509]) ).
fof(f2026,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK2,sK2)
| spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(forward_subsumption_resolution,[],[f2013,f1998]) ).
fof(f2038,plain,
( unordered_pair(sK0,sK1) = unordered_pair(sK0,sK0)
| spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(forward_demodulation,[],[f2026,f509]) ).
fof(f2061,plain,
( $false
| spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(forward_subsumption_resolution,[],[f2038,f1998]) ).
fof(f2062,plain,
( spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(avatar_contradiction_clause,[],[f2061]) ).
fof(f2087,plain,
( $false
| ~ spl26_3
| spl26_7 ),
inference(forward_subsumption_resolution,[],[f416,f508]) ).
fof(f2088,plain,
( ~ spl26_3
| spl26_7 ),
inference(avatar_contradiction_clause,[],[f2087]) ).
fof(f2201,plain,
( $false
| ~ spl26_4
| ~ spl26_5
| spl26_6
| ~ spl26_7 ),
inference(forward_subsumption_resolution,[],[f1958,f1416]) ).
fof(f2202,plain,
( ~ spl26_4
| ~ spl26_5
| spl26_6
| ~ spl26_7 ),
inference(avatar_contradiction_clause,[],[f2201]) ).
fof(f2493,plain,
( in(sK2,unordered_pair(sK0,sK0))
| ~ spl26_9 ),
inference(superposition,[],[f358,f681]) ).
fof(f2519,plain,
( sK0 = sK2
| sK0 = sK2
| ~ spl26_9 ),
inference(resolution,[],[f2493,f359]) ).
fof(f2523,plain,
( sK0 = sK2
| ~ spl26_9 ),
inference(duplicate_literal_removal,[],[f2519]) ).
fof(f2526,plain,
( $false
| spl26_7
| ~ spl26_9 ),
inference(forward_subsumption_resolution,[],[f2523,f508]) ).
fof(f2527,plain,
( spl26_7
| ~ spl26_9 ),
inference(avatar_contradiction_clause,[],[f2526]) ).
cnf(s1,plain,
( spl26_1
| spl26_2 ),
inference(sat_conversion,[],[f375]) ).
cnf(s2,plain,
( spl26_3
| spl26_4 ),
inference(sat_conversion,[],[f391]) ).
cnf(s3,plain,
( ~ spl26_2
| ~ spl26_3 ),
inference(sat_conversion,[],[f426]) ).
cnf(s4,plain,
( ~ spl26_4
| spl26_5
| spl26_6 ),
inference(sat_conversion,[],[f460]) ).
cnf(s5,plain,
( ~ spl26_4
| spl26_7
| spl26_8 ),
inference(sat_conversion,[],[f514]) ).
cnf(s7,plain,
( ~ spl26_2
| ~ spl26_7 ),
inference(sat_conversion,[],[f534]) ).
cnf(s9,plain,
( ~ spl26_4
| ~ spl26_5
| spl26_9
| spl26_10 ),
inference(sat_conversion,[],[f686]) ).
cnf(s10,plain,
( ~ spl26_8
| spl26_9
| spl26_10 ),
inference(sat_conversion,[],[f692]) ).
cnf(s15,plain,
( spl26_7
| ~ spl26_10 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s18,plain,
( ~ spl26_1
| ~ spl26_6 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s19,plain,
( ~ spl26_3
| spl26_5 ),
inference(sat_conversion,[],[f1408]) ).
cnf(s26,plain,
( spl26_4
| ~ spl26_5
| ~ spl26_7 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s28,plain,
( ~ spl26_3
| spl26_7 ),
inference(sat_conversion,[],[f2088]) ).
cnf(s34,plain,
( ~ spl26_4
| ~ spl26_5
| spl26_6
| ~ spl26_7 ),
inference(sat_conversion,[],[f2202]) ).
cnf(s40,plain,
( spl26_7
| ~ spl26_9 ),
inference(sat_conversion,[],[f2527]) ).
cnf(s41,plain,
~ spl26_2,
inference(rat,[],[s5,s10,s2,s15,s40,s3,s7]) ).
cnf(s42,plain,
spl26_1,
inference(rat,[],[s1,s41]) ).
cnf(s43,plain,
~ spl26_6,
inference(rat,[],[s18,s42]) ).
cnf(s44,plain,
( ~ spl26_5
| ~ spl26_4 ),
inference(rat,[],[s9,s15,s40,s34,s43]) ).
cnf(s45,plain,
~ spl26_4,
inference(rat,[],[s44,s4,s43]) ).
cnf(s46,plain,
spl26_3,
inference(rat,[],[s2,s45]) ).
cnf(s47,plain,
spl26_7,
inference(rat,[],[s28,s46]) ).
cnf(s49,plain,
spl26_5,
inference(rat,[],[s19,s46]) ).
cnf(s51,plain,
$false,
inference(rat,[],[s26,s45,s47,s49]) ).
fof(f2528,plain,
$false,
inference(avatar_sat_refutation,[],[s51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU156+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 03:47:12 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/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
% 2.19/1.16 % (3558933)Detected formulas, will run a generic FOF schedule.
% 2.19/1.16 % (3559015)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3215292906:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.19/1.16 % (3559015)First to succeed.
% 2.19/1.16 % (3559015)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3558933"
% 2.19/1.16 % (3559013)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2480868081:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.19/1.16 % (3559014)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=864729339:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.19/1.16 % (3559016)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3054105903:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.19/1.16 % (3559018)dis-21_1_sil=8000:lcm=predicate:random_seed=3222269821:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.19/1.16 % (3559012)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=3882840663:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.19/1.16 % (3559017)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3671376988:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.19/1.16 % (3559016)Instruction limit reached!
% 2.19/1.16 % (3559016)------------------------------
% 2.19/1.16 % (3559016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.19/1.16 % (3559016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/1.16 % (3559016)CaDiCaL version: 2.1.3
% 2.19/1.16 % (3559016)Termination reason: Instruction limit
% 2.19/1.16 % (3559016)Termination phase: Saturation
% 2.19/1.16 % (3559016)Time elapsed: 0.073 s
% 2.19/1.16 % (3559016)Peak memory usage: 88 MB
% 2.19/1.16 % (3559016)Instructions burned: 119 (million)
% 2.19/1.16 % (3559018)Instruction limit reached!
% 2.19/1.16 % (3559018)------------------------------
% 2.19/1.16 % (3559018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.19/1.16 % (3559018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/1.16 % (3559018)CaDiCaL version: 2.1.3
% 2.19/1.16 % (3559018)Termination reason: Instruction limit
% 2.19/1.16 % (3559018)Termination phase: Saturation
% 2.19/1.16 % (3559018)Time elapsed: 0.086 s
% 2.19/1.16 % (3559018)Peak memory usage: 89 MB
% 2.19/1.16 % (3559018)Instructions burned: 130 (million)
% 2.19/1.16 % (3559015)Refutation found. Thanks to Tanya!
% 2.19/1.16 % SZS status Theorem for theBenchmark
% 2.19/1.16 % SZS output start Proof for theBenchmark
% See solution above
% 2.84/1.36 % (3559015)------------------------------
% 2.84/1.36 % (3559015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.84/1.36 % (3559015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/1.36 % (3559015)CaDiCaL version: 2.1.3
% 2.84/1.36 % (3559015)Termination reason: Refutation
% 2.84/1.36 % (3559015)Time elapsed: 0.037 s
% 2.84/1.36 % (3559015)Peak memory usage: 90 MB
% 2.84/1.36 % (3559015)Instructions burned: 107 (million)
% 2.84/1.36 % (3559015)------------------------------
% 2.84/1.36 % (3559015)------------------------------
% 2.84/1.36 % (3558933)Success in time 0.318 s
% 2.84/1.36 % Vampire exiting
%------------------------------------------------------------------------------