%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG017+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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 09:20:05 AM UTC 2026
% Result : Theorem 0.11s 0.26s
% Output : Refutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 18
% Syntax : Number of formulae : 111 ( 15 unt; 15 def)
% Number of atoms : 518 ( 275 equ)
% Maximal formula atoms : 48 ( 4 avg)
% Number of connectives : 549 ( 142 ~; 237 |; 155 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 18 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f11,axiom,
( e0 = op(e3,e3)
& e1 = op(e2,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,conjecture,
~ ( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f13,negated_conjecture,
~ ~ ( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ) ),
inference(negated_conjecture,[status(cth)],[f12]) ).
fof(f14,plain,
( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ) ),
inference(flattening,[],[f13]) ).
fof(f16,plain,
( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3) )
& ( op(e0,e0) != e1
| e1 != op(e1,e1)
| e1 != op(e2,e2)
| e1 != op(e3,e3) )
& ( op(e0,e0) != e2
| e2 != op(e1,e1)
| e2 != op(e2,e2)
| e2 != op(e3,e3) )
& ( op(e0,e0) != e3
| e3 != op(e1,e1)
| e3 != op(e2,e2)
| e3 != op(e3,e3) ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f17,plain,
( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3) )
& ( op(e0,e0) != e1
| e1 != op(e1,e1)
| e1 != op(e2,e2)
| e1 != op(e3,e3) )
& ( op(e0,e0) != e2
| e2 != op(e1,e1)
| e2 != op(e2,e2)
| e2 != op(e3,e3) )
& ( op(e0,e0) != e3
| e3 != op(e1,e1)
| e3 != op(e2,e2)
| e3 != op(e3,e3) ) ),
inference(flattening,[],[f16]) ).
fof(f148,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f196,plain,
e1 = op(e2,e3),
inference(cnf_transformation,[],[f11]) ).
fof(f197,plain,
e0 = op(e3,e3),
inference(cnf_transformation,[],[f11]) ).
fof(f199,plain,
( e0 = op(e2,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f200,plain,
( e0 = op(e1,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f201,plain,
( e0 = op(e0,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f203,plain,
( e1 = op(e2,e2)
| ~ sP0 ),
inference(cnf_transformation,[],[f17]) ).
fof(f206,plain,
( op(e0,e0) = e3
| e2 = op(e3,e3)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f207,plain,
( op(e0,e0) = e3
| e2 = op(e2,e2)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f208,plain,
( op(e0,e0) = e3
| e2 = op(e1,e1)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f209,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f210,plain,
( e3 = op(e1,e1)
| e2 = op(e3,e3)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f211,plain,
( e3 = op(e1,e1)
| e2 = op(e2,e2)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f212,plain,
( e3 = op(e1,e1)
| e2 = op(e1,e1)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f213,plain,
( e3 = op(e1,e1)
| op(e0,e0) = e2
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f214,plain,
( e3 = op(e2,e2)
| e2 = op(e3,e3)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f215,plain,
( e3 = op(e2,e2)
| e2 = op(e2,e2)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f216,plain,
( e3 = op(e2,e2)
| e2 = op(e1,e1)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f217,plain,
( e3 = op(e2,e2)
| op(e0,e0) = e2
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f218,plain,
( e3 = op(e3,e3)
| e2 = op(e3,e3)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f219,plain,
( e3 = op(e3,e3)
| e2 = op(e2,e2)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f220,plain,
( e3 = op(e3,e3)
| e2 = op(e1,e1)
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f221,plain,
( e3 = op(e3,e3)
| op(e0,e0) = e2
| sP0
| sP1 ),
inference(cnf_transformation,[],[f17]) ).
fof(f222,plain,
( e0 != op(e3,e3)
| e0 != op(e2,e2)
| e0 != op(e1,e1)
| e0 != op(e0,e0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f224,plain,
( e2 != op(e3,e3)
| e2 != op(e2,e2)
| e2 != op(e1,e1)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f17]) ).
fof(f225,plain,
( e3 != op(e3,e3)
| e3 != op(e2,e2)
| e3 != op(e1,e1)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f17]) ).
fof(f227,definition,
( spl2_1
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f231,definition,
( spl2_2
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f236,definition,
( spl2_3
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f239,plain,
( ~ spl2_1
| spl2_3 ),
inference(avatar_split_clause,[],[f199,f236,f227]) ).
fof(f241,definition,
( spl2_4
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f244,plain,
( ~ spl2_1
| spl2_4 ),
inference(avatar_split_clause,[],[f200,f241,f227]) ).
fof(f246,definition,
( spl2_5
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f249,plain,
( ~ spl2_1
| spl2_5 ),
inference(avatar_split_clause,[],[f201,f246,f227]) ).
fof(f251,definition,
( spl2_6
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f260,definition,
( spl2_8
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f263,plain,
( ~ spl2_6
| spl2_8 ),
inference(avatar_split_clause,[],[f203,f260,f251]) ).
fof(f275,definition,
( spl2_11
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f279,definition,
( spl2_12
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f282,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_12 ),
inference(avatar_split_clause,[],[f206,f279,f275,f251,f227]) ).
fof(f284,definition,
( spl2_13
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
fof(f287,plain,
( spl2_1
| spl2_6
| spl2_13
| spl2_12 ),
inference(avatar_split_clause,[],[f207,f279,f284,f251,f227]) ).
fof(f289,definition,
( spl2_14
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f292,plain,
( spl2_1
| spl2_6
| spl2_14
| spl2_12 ),
inference(avatar_split_clause,[],[f208,f279,f289,f251,f227]) ).
fof(f294,definition,
( spl2_15
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition]) ).
fof(f297,plain,
( spl2_1
| spl2_6
| spl2_15
| spl2_12 ),
inference(avatar_split_clause,[],[f209,f279,f294,f251,f227]) ).
fof(f299,definition,
( spl2_16
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition]) ).
fof(f302,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_16 ),
inference(avatar_split_clause,[],[f210,f299,f275,f251,f227]) ).
fof(f303,plain,
( spl2_1
| spl2_6
| spl2_13
| spl2_16 ),
inference(avatar_split_clause,[],[f211,f299,f284,f251,f227]) ).
fof(f304,plain,
( spl2_1
| spl2_6
| spl2_14
| spl2_16 ),
inference(avatar_split_clause,[],[f212,f299,f289,f251,f227]) ).
fof(f305,plain,
( spl2_1
| spl2_6
| spl2_15
| spl2_16 ),
inference(avatar_split_clause,[],[f213,f299,f294,f251,f227]) ).
fof(f307,definition,
( spl2_17
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f310,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_17 ),
inference(avatar_split_clause,[],[f214,f307,f275,f251,f227]) ).
fof(f311,plain,
( spl2_1
| spl2_6
| spl2_13
| spl2_17 ),
inference(avatar_split_clause,[],[f215,f307,f284,f251,f227]) ).
fof(f312,plain,
( spl2_1
| spl2_6
| spl2_14
| spl2_17 ),
inference(avatar_split_clause,[],[f216,f307,f289,f251,f227]) ).
fof(f313,plain,
( spl2_1
| spl2_6
| spl2_15
| spl2_17 ),
inference(avatar_split_clause,[],[f217,f307,f294,f251,f227]) ).
fof(f315,definition,
( spl2_18
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f318,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_18 ),
inference(avatar_split_clause,[],[f218,f315,f275,f251,f227]) ).
fof(f319,plain,
( spl2_1
| spl2_6
| spl2_13
| spl2_18 ),
inference(avatar_split_clause,[],[f219,f315,f284,f251,f227]) ).
fof(f320,plain,
( spl2_1
| spl2_6
| spl2_14
| spl2_18 ),
inference(avatar_split_clause,[],[f220,f315,f289,f251,f227]) ).
fof(f321,plain,
( spl2_1
| spl2_6
| spl2_15
| spl2_18 ),
inference(avatar_split_clause,[],[f221,f315,f294,f251,f227]) ).
fof(f322,plain,
( ~ spl2_5
| ~ spl2_4
| ~ spl2_3
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f222,f231,f236,f241,f246]) ).
fof(f324,plain,
( ~ spl2_15
| ~ spl2_14
| ~ spl2_13
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f224,f275,f284,f289,f294]) ).
fof(f325,plain,
( ~ spl2_12
| ~ spl2_16
| ~ spl2_17
| ~ spl2_18 ),
inference(avatar_split_clause,[],[f225,f315,f307,f299,f279]) ).
fof(f326,plain,
spl2_2,
inference(avatar_split_clause,[],[f197,f231]) ).
fof(f327,plain,
e1 != op(e2,e2),
inference(forward_demodulation,[],[f148,f196]) ).
fof(f629,plain,
~ spl2_8,
inference(avatar_split_clause,[],[f327,f260]) ).
cnf(s2,plain,
( ~ spl2_1
| spl2_3 ),
inference(sat_conversion,[],[f239]) ).
cnf(s3,plain,
( ~ spl2_1
| spl2_4 ),
inference(sat_conversion,[],[f244]) ).
cnf(s4,plain,
( ~ spl2_1
| spl2_5 ),
inference(sat_conversion,[],[f249]) ).
cnf(s6,plain,
( ~ spl2_6
| spl2_8 ),
inference(sat_conversion,[],[f263]) ).
cnf(s9,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_12 ),
inference(sat_conversion,[],[f282]) ).
cnf(s10,plain,
( spl2_1
| spl2_6
| spl2_12
| spl2_13 ),
inference(sat_conversion,[],[f287]) ).
cnf(s11,plain,
( spl2_1
| spl2_6
| spl2_12
| spl2_14 ),
inference(sat_conversion,[],[f292]) ).
cnf(s12,plain,
( spl2_1
| spl2_6
| spl2_12
| spl2_15 ),
inference(sat_conversion,[],[f297]) ).
cnf(s13,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_16 ),
inference(sat_conversion,[],[f302]) ).
cnf(s14,plain,
( spl2_1
| spl2_6
| spl2_13
| spl2_16 ),
inference(sat_conversion,[],[f303]) ).
cnf(s15,plain,
( spl2_1
| spl2_6
| spl2_14
| spl2_16 ),
inference(sat_conversion,[],[f304]) ).
cnf(s16,plain,
( spl2_1
| spl2_6
| spl2_15
| spl2_16 ),
inference(sat_conversion,[],[f305]) ).
cnf(s17,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_17 ),
inference(sat_conversion,[],[f310]) ).
cnf(s18,plain,
( spl2_1
| spl2_6
| spl2_13
| spl2_17 ),
inference(sat_conversion,[],[f311]) ).
cnf(s19,plain,
( spl2_1
| spl2_6
| spl2_14
| spl2_17 ),
inference(sat_conversion,[],[f312]) ).
cnf(s20,plain,
( spl2_1
| spl2_6
| spl2_15
| spl2_17 ),
inference(sat_conversion,[],[f313]) ).
cnf(s21,plain,
( spl2_1
| spl2_6
| spl2_11
| spl2_18 ),
inference(sat_conversion,[],[f318]) ).
cnf(s22,plain,
( spl2_1
| spl2_6
| spl2_13
| spl2_18 ),
inference(sat_conversion,[],[f319]) ).
cnf(s23,plain,
( spl2_1
| spl2_6
| spl2_14
| spl2_18 ),
inference(sat_conversion,[],[f320]) ).
cnf(s24,plain,
( spl2_1
| spl2_6
| spl2_15
| spl2_18 ),
inference(sat_conversion,[],[f321]) ).
cnf(s25,plain,
( ~ spl2_2
| ~ spl2_3
| ~ spl2_4
| ~ spl2_5 ),
inference(sat_conversion,[],[f322]) ).
cnf(s27,plain,
( ~ spl2_11
| ~ spl2_13
| ~ spl2_14
| ~ spl2_15 ),
inference(sat_conversion,[],[f324]) ).
cnf(s28,plain,
( ~ spl2_12
| ~ spl2_16
| ~ spl2_17
| ~ spl2_18 ),
inference(sat_conversion,[],[f325]) ).
cnf(s29,plain,
spl2_2,
inference(sat_conversion,[],[f326]) ).
cnf(s62,plain,
~ spl2_8,
inference(sat_conversion,[],[f629]) ).
cnf(s74,plain,
( ~ spl2_3
| ~ spl2_4
| ~ spl2_5 ),
inference(rat,[],[s25,s29]) ).
cnf(s75,plain,
~ spl2_6,
inference(rat,[],[s6,s62]) ).
cnf(s76,plain,
( spl2_11
| spl2_1 ),
inference(rat,[],[s28,s9,s13,s17,s21,s75]) ).
cnf(s77,plain,
( spl2_18
| spl2_1 ),
inference(rat,[],[s27,s22,s23,s24,s76,s75]) ).
cnf(s78,plain,
( spl2_17
| spl2_1 ),
inference(rat,[],[s27,s18,s19,s20,s76,s75]) ).
cnf(s79,plain,
( spl2_16
| spl2_1 ),
inference(rat,[],[s27,s14,s15,s16,s76,s75]) ).
cnf(s80,plain,
spl2_1,
inference(rat,[],[s27,s10,s11,s12,s28,s79,s78,s77,s76,s75]) ).
cnf(s81,plain,
spl2_5,
inference(rat,[],[s4,s80]) ).
cnf(s82,plain,
spl2_4,
inference(rat,[],[s3,s80]) ).
cnf(s83,plain,
spl2_3,
inference(rat,[],[s2,s80]) ).
cnf(s84,plain,
$false,
inference(rat,[],[s74,s81,s82,s83]) ).
fof(f635,plain,
$false,
inference(avatar_sat_refutation,[],[s84]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG017+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.18 % Computer : n001.cluster.edu
% 0.11/0.18 % Model : x86_64 x86_64
% 0.11/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.18 % Memory : 8046.5625MB
% 0.11/0.18 % OS : Linux 6.8.0-71-generic
% 0.11/0.18 % CPULimit : 300
% 0.11/0.18 % WCLimit : 300
% 0.11/0.18 % DateTime : Mon Sep 28 19:23:49 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.22 Running first-order model finding
% 0.11/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.11/0.26 % (644051)Will run a generic schedule for satisfiability detection.
% 0.11/0.26 % (644060)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2442443472:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.11/0.26 % (644060) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-644051-644060"...
% 0.11/0.26 % (644057)% WARNING: option uhcvi not known.
% 0.11/0.26 % (644060)...printing done.
% 0.11/0.26 % (644060)Refutation found. Thanks to Tanya!
% 0.11/0.26 % SZS status Theorem for theBenchmark
% 0.11/0.26 % SZS output start Proof for theBenchmark
% See solution above
% 0.11/0.26 % (644060)------------------------------
% 0.11/0.26 % (644060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.11/0.26 % (644060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.11/0.26 % (644060)CaDiCaL version: 2.1.3
% 0.11/0.26 % (644060)Termination reason: Refutation
% 0.11/0.26 % (644060)Time elapsed: 0.004 s
% 0.11/0.26 % (644060)Peak memory usage: 13 MB
% 0.11/0.26 % (644060)Instructions burned: 15 (million)
% 0.11/0.26 % (644051)Success in time 0.031 s
% 0.11/0.26 % Vampire exiting
%------------------------------------------------------------------------------