%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC416+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 01:03:53 PM UTC 2026
% Result : Theorem 0.64s 0.95s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 22
% Syntax : Number of formulae : 131 ( 26 unt; 14 def)
% Number of atoms : 485 ( 106 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 620 ( 266 ~; 264 |; 53 &)
% ( 14 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 11 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 97 ( 0 sgn 81 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( neq(X0,X1)
<=> X0 != X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ssList(cons(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f21,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> nil != cons(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
fof(f23,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> hd(cons(X1,X0)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f83,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( nil = app(X0,X1)
<=> ( nil = X1
& nil = X0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax83) ).
fof(f85,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( nil != X0
=> hd(app(X0,X1)) = hd(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax85) ).
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( X1 != X3
| X0 != X2
| ( ( ~ neq(X1,nil)
| ? [X4] :
( ssList(X4)
& X1 = X4
& ? [X5] :
( ssList(X5)
& app(X5,X0) = X4
& ? [X6] :
( ssItem(X6)
& cons(X6,nil) = X5
& hd(X1) = X6
& neq(nil,X1) ) ) )
| ! [X7] :
( ssItem(X7)
=> app(cons(X7,nil),X2) != X3 ) )
& ( ~ neq(X1,nil)
| neq(X3,nil) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f97,negated_conjecture,
~ ! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( X1 != X3
| X0 != X2
| ( ( ~ neq(X1,nil)
| ? [X4] :
( ssList(X4)
& X1 = X4
& ? [X5] :
( ssList(X5)
& app(X5,X0) = X4
& ? [X6] :
( ssItem(X6)
& cons(X6,nil) = X5
& hd(X1) = X6
& neq(nil,X1) ) ) )
| ! [X7] :
( ssItem(X7)
=> app(cons(X7,nil),X2) != X3 ) )
& ( ~ neq(X1,nil)
| neq(X3,nil) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f98,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ( ( neq(X1,nil)
& ! [X4] :
( ~ ssList(X4)
| X1 != X4
| ! [X5] :
( ~ ssList(X5)
| app(X5,X0) != X4
| ! [X6] :
( ~ ssItem(X6)
| cons(X6,nil) != X5
| hd(X1) != X6
| ~ neq(nil,X1) ) ) )
& ? [X7] :
( app(cons(X7,nil),X2) = X3
& ssItem(X7) ) )
| ( neq(X1,nil)
& ~ neq(X3,nil) ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f99,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ( ( neq(X1,nil)
& ! [X4] :
( ~ ssList(X4)
| X1 != X4
| ! [X5] :
( ~ ssList(X5)
| app(X5,X0) != X4
| ! [X6] :
( ~ ssItem(X6)
| cons(X6,nil) != X5
| hd(X1) != X6
| ~ neq(nil,X1) ) ) )
& ? [X7] :
( app(cons(X7,nil),X2) = X3
& ssItem(X7) ) )
| ( neq(X1,nil)
& ~ neq(X3,nil) ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
! [X0] :
( ! [X1] :
( nil != cons(X1,X0)
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f106,plain,
! [X0] :
( ! [X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f108,plain,
! [X0] :
( ! [X1] :
( ( nil = app(X0,X1)
<=> ( nil = X1
& nil = X0 ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f118,plain,
! [X0] :
( ! [X1] :
( ( neq(X0,X1)
<=> X0 != X1 )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f120,plain,
! [X0] :
( ! [X1] :
( hd(app(X0,X1)) = hd(X0)
| nil = X0
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f85]) ).
fof(f121,plain,
! [X0] :
( ! [X1] :
( hd(app(X0,X1)) = hd(X0)
| nil = X0
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f120]) ).
fof(f124,plain,
! [X0] :
( ! [X1] :
( hd(cons(X1,X0)) = X1
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f127,plain,
( sK1 = sK3
& sK0 = sK2
& ( ( neq(sK1,nil)
& ! [X4] :
( ~ ssList(X4)
| sK1 != X4
| ! [X5] :
( ~ ssList(X5)
| app(X5,sK0) != X4
| ! [X6] :
( ~ ssItem(X6)
| cons(X6,nil) != X5
| hd(sK1) != X6
| ~ neq(nil,sK1) ) ) )
& sK3 = app(cons(sK4,nil),sK2)
& ssItem(sK4) )
| ( neq(sK1,nil)
& ~ neq(sK3,nil) ) )
& ssList(sK3)
& ssList(sK2)
& ssList(sK1)
& ssList(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X7,sK4)],[f99]) ).
fof(f130,plain,
! [X0] :
( ! [X1] :
( ( ( nil = app(X0,X1)
| nil != X1
| nil != X0 )
& ( ( nil = X1
& nil = X0 )
| nil != app(X0,X1) ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(nnf_transformation,[],[f108]) ).
fof(f131,plain,
! [X0] :
( ! [X1] :
( ( ( nil = app(X0,X1)
| nil != X1
| nil != X0 )
& ( ( nil = X1
& nil = X0 )
| nil != app(X0,X1) ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f130]) ).
fof(f132,plain,
! [X0] :
( ! [X1] :
( ( ( neq(X0,X1)
| X0 = X1 )
& ( X0 != X1
| ~ neq(X0,X1) ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(nnf_transformation,[],[f118]) ).
fof(f135,plain,
ssList(sK0),
inference(cnf_transformation,[],[f127]) ).
fof(f136,plain,
ssList(sK1),
inference(cnf_transformation,[],[f127]) ).
fof(f139,plain,
( ssItem(sK4)
| ~ neq(sK3,nil) ),
inference(cnf_transformation,[],[f127]) ).
fof(f141,plain,
( sK3 = app(cons(sK4,nil),sK2)
| ~ neq(sK3,nil) ),
inference(cnf_transformation,[],[f127]) ).
fof(f143,plain,
! [X6,X4,X5] :
( ~ ssList(X4)
| sK1 != X4
| ~ ssList(X5)
| app(X5,sK0) != X4
| ~ ssItem(X6)
| cons(X6,nil) != X5
| hd(sK1) != X6
| ~ neq(nil,sK1)
| ~ neq(sK3,nil) ),
inference(cnf_transformation,[],[f127]) ).
fof(f146,plain,
( neq(sK1,nil)
| neq(sK1,nil) ),
inference(cnf_transformation,[],[f127]) ).
fof(f147,plain,
sK0 = sK2,
inference(cnf_transformation,[],[f127]) ).
fof(f148,plain,
sK1 = sK3,
inference(cnf_transformation,[],[f127]) ).
fof(f152,plain,
! [X0,X1] :
( nil != cons(X1,X0)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f159,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f106]) ).
fof(f161,plain,
! [X0,X1] :
( nil = X0
| nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f172,plain,
! [X0,X1] :
( neq(X0,X1)
| X0 = X1
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f175,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f176,plain,
! [X0,X1] :
( hd(X0) = hd(app(X0,X1))
| nil = X0
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f179,plain,
! [X0,X1] :
( hd(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f181,plain,
( neq(sK3,nil)
| neq(sK3,nil) ),
inference(definition_unfolding,[],[f146,f148,f148]) ).
fof(f184,plain,
! [X6,X4,X5] :
( ~ ssList(X4)
| sK3 != X4
| ~ ssList(X5)
| app(X5,sK2) != X4
| ~ ssItem(X6)
| cons(X6,nil) != X5
| hd(sK3) != X6
| ~ neq(nil,sK3)
| ~ neq(sK3,nil) ),
inference(definition_unfolding,[],[f143,f148,f147,f148,f148]) ).
fof(f187,plain,
ssList(sK3),
inference(definition_unfolding,[],[f136,f148]) ).
fof(f188,plain,
ssList(sK2),
inference(definition_unfolding,[],[f135,f147]) ).
fof(f192,definition,
~ sP12(sK3),
introduced(definition,[new_symbols(definition,[sP12])],[inequality_splitting_name_introduction]) ).
fof(f193,definition,
~ sP13(hd(sK3)),
introduced(definition,[new_symbols(definition,[sP13])],[inequality_splitting_name_introduction]) ).
fof(f194,plain,
! [X6,X4,X5] :
( ~ ssList(X4)
| sP12(X4)
| ~ ssList(X5)
| app(X5,sK2) != X4
| ~ ssItem(X6)
| cons(X6,nil) != X5
| sP13(X6)
| ~ neq(nil,sK3)
| ~ neq(sK3,nil) ),
inference(inequality_splitting,[],[f184,f193,f192]) ).
fof(f197,definition,
~ sP15(nil),
introduced(definition,[new_symbols(definition,[sP15])],[inequality_splitting_name_introduction]) ).
fof(f198,plain,
! [X0,X1] :
( sP15(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(inequality_splitting,[],[f152,f197]) ).
fof(f204,definition,
~ sP19(nil),
introduced(definition,[new_symbols(definition,[sP19])],[inequality_splitting_name_introduction]) ).
fof(f205,plain,
! [X0,X1] :
( sP19(app(X0,X1))
| nil = X0
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(inequality_splitting,[],[f161,f204]) ).
fof(f208,plain,
! [X6,X5] :
( ~ ssList(app(X5,sK2))
| sP12(app(X5,sK2))
| ~ ssList(X5)
| ~ ssItem(X6)
| cons(X6,nil) != X5
| sP13(X6)
| ~ neq(nil,sK3)
| ~ neq(sK3,nil) ),
inference(equality_resolution,[],[f194]) ).
fof(f209,plain,
! [X6] :
( ~ ssList(app(cons(X6,nil),sK2))
| sP12(app(cons(X6,nil),sK2))
| ~ ssList(cons(X6,nil))
| ~ ssItem(X6)
| sP13(X6)
| ~ neq(nil,sK3)
| ~ neq(sK3,nil) ),
inference(equality_resolution,[],[f208]) ).
fof(f214,plain,
neq(sK3,nil),
inference(duplicate_literal_removal,[],[f181]) ).
fof(f216,definition,
( spl20_1
<=> neq(sK3,nil) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f220,definition,
( spl20_2
<=> ssItem(sK4) ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f222,plain,
( ssItem(sK4)
| ~ spl20_2 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,plain,
( ~ spl20_1
| spl20_2 ),
inference(avatar_split_clause,[],[f139,f220,f216]) ).
fof(f226,definition,
( spl20_3
<=> sK3 = app(cons(sK4,nil),sK2) ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
fof(f228,plain,
( sK3 = app(cons(sK4,nil),sK2)
| ~ spl20_3 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
( ~ spl20_1
| spl20_3 ),
inference(avatar_split_clause,[],[f141,f226,f216]) ).
fof(f232,definition,
( spl20_4
<=> neq(nil,sK3) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f234,plain,
( ~ neq(nil,sK3)
| spl20_4 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f236,definition,
( spl20_5
<=> ! [X6] :
( ~ ssList(app(cons(X6,nil),sK2))
| sP13(X6)
| ~ ssItem(X6)
| ~ ssList(cons(X6,nil))
| sP12(app(cons(X6,nil),sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f237,plain,
( ! [X6] :
( ~ ssList(app(cons(X6,nil),sK2))
| sP13(X6)
| ~ ssItem(X6)
| ~ ssList(cons(X6,nil))
| sP12(app(cons(X6,nil),sK2)) )
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f238,plain,
( ~ spl20_1
| ~ spl20_4
| spl20_5 ),
inference(avatar_split_clause,[],[f209,f236,f232,f216]) ).
fof(f243,plain,
spl20_1,
inference(avatar_split_clause,[],[f214,f216]) ).
fof(f247,definition,
( spl20_7
<=> nil = sK3 ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
fof(f249,plain,
( nil = sK3
| ~ spl20_7 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f264,plain,
( nil = sK3
| ~ ssList(sK3)
| ~ ssList(nil)
| spl20_4 ),
inference(resolution,[],[f234,f172]) ).
fof(f266,plain,
( nil = sK3
| ~ ssList(nil)
| spl20_4 ),
inference(forward_subsumption_resolution,[],[f264,f187]) ).
fof(f276,plain,
( nil = sK3
| spl20_4 ),
inference(forward_subsumption_resolution,[],[f266,f175]) ).
fof(f277,plain,
( spl20_7
| spl20_4 ),
inference(avatar_split_clause,[],[f276,f232,f247]) ).
fof(f288,plain,
( hd(sK3) = hd(cons(sK4,nil))
| nil = cons(sK4,nil)
| ~ ssList(sK2)
| ~ ssList(cons(sK4,nil))
| ~ spl20_3 ),
inference(superposition,[],[f176,f228]) ).
fof(f291,plain,
( sP19(sK3)
| nil = cons(sK4,nil)
| ~ ssList(sK2)
| ~ ssList(cons(sK4,nil))
| ~ spl20_3 ),
inference(superposition,[],[f205,f228]) ).
fof(f292,plain,
( sP19(sK3)
| nil = cons(sK4,nil)
| ~ ssList(cons(sK4,nil))
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f291,f188]) ).
fof(f295,plain,
( hd(sK3) = hd(cons(sK4,nil))
| nil = cons(sK4,nil)
| ~ ssList(cons(sK4,nil))
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f288,f188]) ).
fof(f304,definition,
( spl20_12
<=> ssList(cons(sK4,nil)) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
fof(f305,plain,
( ssList(cons(sK4,nil))
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( ~ ssList(cons(sK4,nil))
| spl20_12 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl20_13
<=> nil = cons(sK4,nil) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f310,plain,
( nil = cons(sK4,nil)
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f312,definition,
( spl20_14
<=> sP19(sK3) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
fof(f314,plain,
( sP19(sK3)
| ~ spl20_14 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f315,plain,
( ~ spl20_12
| spl20_13
| spl20_14
| ~ spl20_3 ),
inference(avatar_split_clause,[],[f292,f226,f312,f308,f304]) ).
fof(f335,definition,
( spl20_19
<=> hd(sK3) = hd(cons(sK4,nil)) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
fof(f337,plain,
( hd(sK3) = hd(cons(sK4,nil))
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f338,plain,
( ~ spl20_12
| spl20_13
| spl20_19
| ~ spl20_3 ),
inference(avatar_split_clause,[],[f295,f226,f335,f308,f304]) ).
fof(f360,plain,
( ~ ssList(sK3)
| sP13(sK4)
| ~ ssItem(sK4)
| ~ ssList(cons(sK4,nil))
| sP12(sK3)
| ~ spl20_3
| ~ spl20_5 ),
inference(superposition,[],[f237,f228]) ).
fof(f402,plain,
( ~ ssItem(sK4)
| ~ ssList(nil)
| spl20_12 ),
inference(resolution,[],[f306,f159]) ).
fof(f404,plain,
( ~ ssList(nil)
| ~ spl20_2
| spl20_12 ),
inference(forward_subsumption_resolution,[],[f402,f222]) ).
fof(f405,plain,
( $false
| ~ spl20_2
| spl20_12 ),
inference(forward_subsumption_resolution,[],[f404,f175]) ).
fof(f406,plain,
( ~ spl20_2
| spl20_12 ),
inference(avatar_contradiction_clause,[],[f405]) ).
fof(f411,plain,
( sP13(sK4)
| ~ ssItem(sK4)
| ~ ssList(cons(sK4,nil))
| sP12(sK3)
| ~ spl20_3
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f360,f187]) ).
fof(f417,plain,
( sP13(sK4)
| ~ ssList(cons(sK4,nil))
| sP12(sK3)
| ~ spl20_2
| ~ spl20_3
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f411,f222]) ).
fof(f423,plain,
( sP13(sK4)
| sP12(sK3)
| ~ spl20_2
| ~ spl20_3
| ~ spl20_5
| ~ spl20_12 ),
inference(forward_subsumption_resolution,[],[f417,f305]) ).
fof(f425,plain,
( sP13(sK4)
| ~ spl20_2
| ~ spl20_3
| ~ spl20_5
| ~ spl20_12 ),
inference(forward_subsumption_resolution,[],[f423,f192]) ).
fof(f452,plain,
( sP15(nil)
| ~ ssItem(sK4)
| ~ ssList(nil)
| ~ spl20_13 ),
inference(superposition,[],[f198,f310]) ).
fof(f454,plain,
( ~ ssItem(sK4)
| ~ ssList(nil)
| ~ spl20_13 ),
inference(forward_subsumption_resolution,[],[f452,f197]) ).
fof(f463,plain,
( ~ ssList(nil)
| ~ spl20_2
| ~ spl20_13 ),
inference(forward_subsumption_resolution,[],[f454,f222]) ).
fof(f472,plain,
( $false
| ~ spl20_2
| ~ spl20_13 ),
inference(forward_subsumption_resolution,[],[f463,f175]) ).
fof(f473,plain,
( ~ spl20_2
| ~ spl20_13 ),
inference(avatar_contradiction_clause,[],[f472]) ).
fof(f474,plain,
( sP19(nil)
| ~ spl20_7
| ~ spl20_14 ),
inference(forward_demodulation,[],[f314,f249]) ).
fof(f479,plain,
( $false
| ~ spl20_7
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f474,f204]) ).
fof(f480,plain,
( ~ spl20_7
| ~ spl20_14 ),
inference(avatar_contradiction_clause,[],[f479]) ).
fof(f491,plain,
( ~ sP13(hd(cons(sK4,nil)))
| ~ spl20_19 ),
inference(superposition,[],[f193,f337]) ).
fof(f504,plain,
( ~ sP13(sK4)
| ~ ssItem(sK4)
| ~ ssList(nil)
| ~ spl20_19 ),
inference(superposition,[],[f491,f179]) ).
fof(f507,plain,
( ~ ssItem(sK4)
| ~ ssList(nil)
| ~ spl20_2
| ~ spl20_3
| ~ spl20_5
| ~ spl20_12
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f504,f425]) ).
fof(f509,plain,
( ~ ssList(nil)
| ~ spl20_2
| ~ spl20_3
| ~ spl20_5
| ~ spl20_12
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f507,f222]) ).
fof(f510,plain,
( $false
| ~ spl20_2
| ~ spl20_3
| ~ spl20_5
| ~ spl20_12
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f509,f175]) ).
fof(f511,plain,
( ~ spl20_2
| ~ spl20_3
| ~ spl20_5
| ~ spl20_12
| ~ spl20_19 ),
inference(avatar_contradiction_clause,[],[f510]) ).
cnf(s1,plain,
( ~ spl20_1
| spl20_2 ),
inference(sat_conversion,[],[f223]) ).
cnf(s3,plain,
( ~ spl20_1
| spl20_3 ),
inference(sat_conversion,[],[f229]) ).
cnf(s5,plain,
( ~ spl20_1
| ~ spl20_4
| spl20_5 ),
inference(sat_conversion,[],[f238]) ).
cnf(s7,plain,
spl20_1,
inference(sat_conversion,[],[f243]) ).
cnf(s11,plain,
( spl20_4
| spl20_7 ),
inference(sat_conversion,[],[f277]) ).
cnf(s12,plain,
( ~ spl20_3
| ~ spl20_12
| spl20_13
| spl20_14 ),
inference(sat_conversion,[],[f315]) ).
cnf(s15,plain,
( ~ spl20_3
| ~ spl20_12
| spl20_13
| spl20_19 ),
inference(sat_conversion,[],[f338]) ).
cnf(s28,plain,
( ~ spl20_2
| spl20_12 ),
inference(sat_conversion,[],[f406]) ).
cnf(s31,plain,
( ~ spl20_2
| ~ spl20_13 ),
inference(sat_conversion,[],[f473]) ).
cnf(s32,plain,
( ~ spl20_7
| ~ spl20_14 ),
inference(sat_conversion,[],[f480]) ).
cnf(s33,plain,
( ~ spl20_2
| ~ spl20_3
| ~ spl20_5
| ~ spl20_12
| ~ spl20_19 ),
inference(sat_conversion,[],[f511]) ).
cnf(s34,plain,
( ~ spl20_4
| spl20_5 ),
inference(rat,[],[s5,s7]) ).
cnf(s35,plain,
spl20_3,
inference(rat,[],[s3,s7]) ).
cnf(s36,plain,
spl20_2,
inference(rat,[],[s1,s7]) ).
cnf(s37,plain,
~ spl20_13,
inference(rat,[],[s31,s36]) ).
cnf(s38,plain,
spl20_12,
inference(rat,[],[s28,s36]) ).
cnf(s43,plain,
spl20_19,
inference(rat,[],[s15,s37,s35,s38]) ).
cnf(s44,plain,
spl20_14,
inference(rat,[],[s12,s37,s35,s38]) ).
cnf(s45,plain,
~ spl20_5,
inference(rat,[],[s33,s43,s36,s35,s38]) ).
cnf(s46,plain,
~ spl20_7,
inference(rat,[],[s32,s44]) ).
cnf(s47,plain,
~ spl20_4,
inference(rat,[],[s34,s45]) ).
cnf(s48,plain,
$false,
inference(rat,[],[s11,s46,s47]) ).
fof(f512,plain,
$false,
inference(avatar_sat_refutation,[],[s48]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC416+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n001.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 09:39:10 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 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
% 0.64/0.95 % (245015)Detected formulas, will run a generic FOF schedule.
% 0.64/0.95 % (245023)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1789132534:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 0.64/0.95 % (245023)First to succeed.
% 0.64/0.95 % (245023)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-245015"
% 0.64/0.95 % (245025)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2716326751:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 0.64/0.95 % (245022)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=2678774402:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 0.64/0.95 % (245024)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1132614196:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 0.64/0.95 % (245020)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=1617423335:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 0.64/0.95 % (245021)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=3453451046:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 0.64/0.95 % (245026)dis-21_1_sil=8000:lcm=predicate:random_seed=4250910720: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)
% 0.64/0.95 % (245024)Also succeeded, but the first one will report.
% 0.64/0.95 % (245025)Also succeeded, but the first one will report.
% 0.64/0.95 % (245026)Instruction limit reached!
% 0.64/0.95 % (245026)------------------------------
% 0.64/0.95 % (245026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.64/0.95 % (245026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.95 % (245026)CaDiCaL version: 2.1.3
% 0.64/0.95 % (245026)Termination reason: Instruction limit
% 0.64/0.95 % (245026)Termination phase: Saturation
% 0.64/0.95 % (245026)Time elapsed: 0.073 s
% 0.64/0.95 % (245026)Peak memory usage: 90 MB
% 0.64/0.95 % (245026)Instructions burned: 129 (million)
% 0.64/0.95 % (245023)Refutation found. Thanks to Tanya!
% 0.64/0.95 % SZS status Theorem for theBenchmark
% 0.64/0.95 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/1.14 % (245023)------------------------------
% 0.19/1.14 % (245023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/1.14 % (245023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/1.14 % (245023)CaDiCaL version: 2.1.3
% 0.19/1.14 % (245023)Termination reason: Refutation
% 0.19/1.14 % (245023)Time elapsed: 0.006 s
% 0.19/1.14 % (245023)Peak memory usage: 90 MB
% 0.19/1.14 % (245023)Instructions burned: 13 (million)
% 0.19/1.14 % (245023)------------------------------
% 0.19/1.14 % (245023)------------------------------
% 0.19/1.14 % (245015)Success in time 0.275 s
% 0.19/1.14 % Vampire exiting
%------------------------------------------------------------------------------