%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC420-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:55 PM UTC 2026
% Result : Unsatisfiable 1.51s 0.69s
% Output : Refutation 2.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 32
% Syntax : Number of formulae : 160 ( 22 unt; 11 def)
% Number of atoms : 548 ( 104 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 752 ( 364 ~; 377 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 12 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 122 ( 0 sgn 122 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,axiom,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f74,axiom,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f76,axiom,
! [X0] :
( ssItem(hd(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f97,axiom,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f112,axiom,
! [X0] :
( cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f118,axiom,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f161,axiom,
! [X2,X0,X1] :
( app(app(X2,X1),X0) = app(X2,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f201,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_2) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
neq(sk2,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
! [X2,X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| app(app(X1,cons(X0,nil)),X2) != sk2
| app(app(X2,cons(X0,nil)),X1) != sk1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,plain,
! [X2,X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| sk2 != app(app(X1,cons(X0,nil)),X2)
| sk1 != app(app(X2,cons(X0,nil)),X1) ),
inference(reorient_equations,[],[f207]) ).
fof(f209,negated_conjecture,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(X1,cons(X0,nil)) = sk3
| app(cons(X0,nil),X1) != sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f210,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| sk3 = app(X1,cons(X0,nil))
| app(cons(X0,nil),X1) != sk4 ),
inference(reorient_equations,[],[f209]) ).
fof(f218,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(equality_resolution,[],[f118]) ).
fof(f229,plain,
! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X3) ),
inference(equality_resolution,[],[f193]) ).
fof(f240,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1) ),
inference(duplicate_literal_removal,[],[f218]) ).
fof(f243,definition,
( spl0_1
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f244,plain,
( nil = sk4
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f245,plain,
( nil != sk4
| spl0_1 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f256,definition,
( spl0_4
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f257,plain,
( ssList(nil)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f284,definition,
( spl0_10
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f285,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f287,definition,
( spl0_11
<=> ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f288,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ~ ssList(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f289,plain,
( spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f72,f287,f284]) ).
fof(f292,plain,
spl0_4,
inference(avatar_split_clause,[],[f8,f256]) ).
fof(f295,plain,
( nil != sk2
| spl0_1 ),
inference(forward_demodulation,[],[f245,f204]) ).
fof(f296,plain,
! [X0,X1] :
( app(cons(X0,nil),X1) != sk2
| ~ ssItem(X0)
| ~ ssList(X1)
| sk3 = app(X1,cons(X0,nil)) ),
inference(forward_demodulation,[],[f210,f204]) ).
fof(f297,plain,
! [X2,X0,X1] :
( sk3 != app(app(X2,cons(X0,nil)),X1)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| sk2 != app(app(X1,cons(X0,nil)),X2) ),
inference(forward_demodulation,[],[f208,f205]) ).
fof(f308,plain,
! [X0,X1] :
( sk3 != app(X0,cons(X1,nil))
| ~ ssItem(X1)
| ~ ssList(nil)
| ~ ssList(X0)
| sk2 != app(app(nil,cons(X1,nil)),X0)
| ~ ssList(app(X0,cons(X1,nil))) ),
inference(superposition,[],[f297,f73]) ).
fof(f309,plain,
( ! [X0,X1] :
( sk3 != app(X0,cons(X1,nil))
| ~ ssItem(X1)
| ~ ssList(X0)
| sk2 != app(app(nil,cons(X1,nil)),X0)
| ~ ssList(app(X0,cons(X1,nil))) )
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f308,f257]) ).
fof(f311,plain,
( ! [X0,X1] :
( ~ ssList(app(X0,cons(X1,nil)))
| ~ ssList(X0)
| sk2 != app(app(nil,cons(X1,nil)),X0)
| sk3 != app(X0,cons(X1,nil)) )
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f309,f285]) ).
fof(f329,plain,
( ! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(cons(X1,nil))
| ~ ssList(X0)
| sk2 != app(app(nil,cons(X1,nil)),X0)
| sk3 != app(X0,cons(X1,nil)) )
| ~ spl0_4
| ~ spl0_10 ),
inference(resolution,[],[f85,f311]) ).
fof(f336,plain,
( ! [X0,X1] :
( ~ ssList(cons(X1,nil))
| ~ ssList(X0)
| sk2 != app(app(nil,cons(X1,nil)),X0)
| sk3 != app(X0,cons(X1,nil)) )
| ~ spl0_4
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f329]) ).
fof(f338,plain,
( ! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f86,f285]) ).
fof(f340,plain,
( ! [X0,X1] :
( ~ ssList(nil)
| ~ ssList(X0)
| sk2 != app(app(nil,cons(X1,nil)),X0)
| sk3 != app(X0,cons(X1,nil)) )
| ~ spl0_4
| ~ spl0_10 ),
inference(resolution,[],[f338,f336]) ).
fof(f349,plain,
( ! [X0,X1] :
( sk3 != app(X0,cons(X1,nil))
| sk2 != app(app(nil,cons(X1,nil)),X0)
| ~ ssList(X0) )
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f340,f257]) ).
fof(f394,plain,
( ! [X0,X1] :
( cons(X0,X1) = app(cons(X0,nil),X1)
| ~ ssList(X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f126,f285]) ).
fof(f396,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk2
| ~ ssItem(X0)
| ~ ssList(X1)
| sk3 = app(X1,cons(X0,nil))
| ~ ssList(X1) )
| ~ spl0_10 ),
inference(superposition,[],[f296,f394]) ).
fof(f408,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk2
| ~ ssItem(X0)
| ~ ssList(X1)
| sk3 = app(X1,cons(X0,nil)) )
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f396]) ).
fof(f412,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk2
| ~ ssList(X1)
| sk3 = app(X1,cons(X0,nil)) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f408,f285]) ).
fof(f414,plain,
( ! [X0] :
( sk2 != X0
| ~ ssList(skaf82(X0))
| sk3 = app(skaf82(X0),cons(skaf83(X0),nil))
| ~ ssList(X0)
| nil = X0 )
| ~ spl0_10 ),
inference(superposition,[],[f412,f112]) ).
fof(f415,plain,
( ! [X0] :
( sk2 != X0
| sk3 = app(skaf82(X0),cons(skaf83(X0),nil))
| ~ ssList(X0)
| nil = X0 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f414,f13]) ).
fof(f422,plain,
( sk3 = app(skaf82(sk2),cons(skaf83(sk2),nil))
| ~ ssList(sk2)
| nil = sk2
| ~ spl0_10 ),
inference(equality_resolution,[],[f415]) ).
fof(f423,plain,
( sk3 = app(skaf82(sk2),cons(skaf83(sk2),nil))
| nil = sk2
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f422,f201]) ).
fof(f424,plain,
( sk3 = app(skaf82(sk2),cons(skaf83(sk2),nil))
| spl0_1
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f423,f295]) ).
fof(f426,plain,
( sk3 != sk3
| sk2 != app(app(nil,cons(skaf83(sk2),nil)),skaf82(sk2))
| ~ ssList(skaf82(sk2))
| spl0_1
| ~ spl0_4
| ~ spl0_10 ),
inference(superposition,[],[f349,f424]) ).
fof(f433,plain,
( sk2 != app(app(nil,cons(skaf83(sk2),nil)),skaf82(sk2))
| ~ ssList(skaf82(sk2))
| spl0_1
| ~ spl0_4
| ~ spl0_10 ),
inference(trivial_inequality_removal,[],[f426]) ).
fof(f438,plain,
( sk2 != app(app(nil,cons(skaf83(sk2),nil)),skaf82(sk2))
| spl0_1
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f433,f13]) ).
fof(f444,definition,
( spl0_13
<=> ssList(cons(skaf83(sk2),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f446,plain,
( ~ ssList(cons(skaf83(sk2),nil))
| spl0_13 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f455,plain,
( sk2 != app(cons(skaf83(sk2),nil),skaf82(sk2))
| ~ ssList(cons(skaf83(sk2),nil))
| spl0_1
| ~ spl0_4
| ~ spl0_10 ),
inference(superposition,[],[f438,f74]) ).
fof(f457,definition,
( spl0_15
<=> sk2 = app(cons(skaf83(sk2),nil),skaf82(sk2)) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f459,plain,
( sk2 != app(cons(skaf83(sk2),nil),skaf82(sk2))
| spl0_15 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f460,plain,
( ~ spl0_13
| ~ spl0_15
| spl0_1
| ~ spl0_4
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f455,f284,f256,f243,f457,f444]) ).
fof(f461,plain,
( ~ ssList(nil)
| ~ spl0_10
| spl0_13 ),
inference(resolution,[],[f446,f338]) ).
fof(f462,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f461,f257]) ).
fof(f463,plain,
( ~ spl0_4
| ~ spl0_10
| spl0_13 ),
inference(avatar_contradiction_clause,[],[f462]) ).
fof(f484,plain,
( sk2 != cons(skaf83(sk2),skaf82(sk2))
| ~ ssList(skaf82(sk2))
| ~ spl0_10
| spl0_15 ),
inference(superposition,[],[f459,f394]) ).
fof(f485,plain,
( sk2 != cons(skaf83(sk2),skaf82(sk2))
| ~ spl0_10
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f484,f13]) ).
fof(f512,definition,
( spl0_17
<=> nil = sk2 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f513,plain,
( nil != sk2
| spl0_17 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( nil = sk2
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f521,plain,
( nil = sk2
| ~ spl0_1 ),
inference(superposition,[],[f204,f244]) ).
fof(f523,plain,
( spl0_17
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f521,f243,f512]) ).
fof(f580,plain,
! [X0] :
( skaf83(X0) = hd(X0)
| ~ ssList(skaf82(X0))
| ~ ssItem(skaf83(X0))
| ~ ssList(X0)
| nil = X0 ),
inference(superposition,[],[f97,f112]) ).
fof(f584,plain,
! [X0] :
( skaf83(X0) = hd(X0)
| ~ ssItem(skaf83(X0))
| ~ ssList(X0)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f580,f13]) ).
fof(f586,plain,
! [X0] :
( skaf83(X0) = hd(X0)
| ~ ssList(X0)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f584,f12]) ).
fof(f761,plain,
! [X2,X0,X1] :
( ssList(app(X0,app(X1,X2)))
| ~ ssList(app(X0,X1))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(superposition,[],[f85,f161]) ).
fof(f782,plain,
! [X2,X0,X1] :
( ssList(app(X0,app(X1,X2)))
| ~ ssList(app(X0,X1))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literal_removal,[],[f761]) ).
fof(f798,plain,
! [X2,X0,X1] :
( ssList(app(X0,app(X1,X2)))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f782,f85]) ).
fof(f1100,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f229,f288]) ).
fof(f1109,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(app(X1,cons(X2,X0)))
| ~ ssList(cons(X2,X3)) )
| ~ spl0_11 ),
inference(resolution,[],[f1100,f85]) ).
fof(f1125,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(app(X1,cons(X2,X0))) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1109,f86]) ).
fof(f1134,definition,
( spl0_24
<=> ! [X3] : ~ ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f1135,plain,
( ! [X3] : ~ ssList(X3)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f1134]) ).
fof(f1137,definition,
( spl0_25
<=> ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X1,cons(X2,X0)))
| ~ ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f1138,plain,
( ! [X2,X0,X1] :
( ~ ssList(app(X1,cons(X2,X0)))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X2) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f1137]) ).
fof(f1139,plain,
( spl0_24
| spl0_25
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1125,f287,f1137,f1134]) ).
fof(f1199,plain,
( neq(nil,nil)
| ~ spl0_17 ),
inference(superposition,[],[f206,f514]) ).
fof(f1252,plain,
( ~ ssList(nil)
| ~ spl0_17 ),
inference(resolution,[],[f1199,f240]) ).
fof(f1253,plain,
( $false
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1252,f257]) ).
fof(f1254,plain,
( ~ spl0_4
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1253]) ).
fof(f1282,plain,
( sk2 != sk2
| ~ ssList(sk2)
| nil = sk2
| ~ spl0_10
| spl0_15 ),
inference(superposition,[],[f485,f112]) ).
fof(f1283,plain,
( ~ ssList(sk2)
| nil = sk2
| ~ spl0_10
| spl0_15 ),
inference(trivial_inequality_removal,[],[f1282]) ).
fof(f1284,plain,
( nil = sk2
| ~ spl0_10
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1283,f201]) ).
fof(f1285,plain,
( $false
| ~ spl0_10
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1284,f513]) ).
fof(f1286,plain,
( ~ spl0_10
| spl0_15
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
fof(f1358,definition,
( spl0_32
<=> hd(cons(skaf83(sk2),nil)) = hd(sk2) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f1359,plain,
( hd(cons(skaf83(sk2),nil)) != hd(sk2)
| spl0_32 ),
inference(avatar_component_clause,[],[f1358]) ).
fof(f1360,plain,
( hd(cons(skaf83(sk2),nil)) = hd(sk2)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f1358]) ).
fof(f1705,plain,
( skaf83(sk2) = hd(sk2)
| ~ ssList(nil)
| ~ ssItem(skaf83(sk2))
| ~ spl0_32 ),
inference(superposition,[],[f97,f1360]) ).
fof(f1714,plain,
( skaf83(sk2) = hd(sk2)
| ~ ssItem(skaf83(sk2))
| ~ spl0_4
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1705,f257]) ).
fof(f1722,definition,
( spl0_39
<=> ssItem(hd(sk2)) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f1723,plain,
( ~ ssItem(hd(sk2))
| spl0_39 ),
inference(avatar_component_clause,[],[f1722]) ).
fof(f1724,plain,
( ssItem(hd(sk2))
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f1722]) ).
fof(f1734,plain,
( skaf83(sk2) = hd(sk2)
| ~ spl0_4
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1714,f12]) ).
fof(f1736,plain,
( skaf83(sk2) != hd(sk2)
| ~ ssList(nil)
| ~ ssItem(skaf83(sk2))
| spl0_32 ),
inference(superposition,[],[f1359,f97]) ).
fof(f1737,plain,
( skaf83(sk2) != hd(sk2)
| ~ ssItem(skaf83(sk2))
| ~ spl0_4
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f1736,f257]) ).
fof(f1738,plain,
( skaf83(sk2) != hd(sk2)
| ~ spl0_4
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f1737,f12]) ).
fof(f2200,plain,
( hd(sk2) != hd(sk2)
| ~ ssList(sk2)
| nil = sk2
| ~ spl0_4
| spl0_32 ),
inference(superposition,[],[f1738,f586]) ).
fof(f2201,plain,
( ~ ssList(sk2)
| nil = sk2
| ~ spl0_4
| spl0_32 ),
inference(trivial_inequality_removal,[],[f2200]) ).
fof(f2204,plain,
( nil = sk2
| ~ spl0_4
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f2201,f201]) ).
fof(f2223,plain,
( $false
| ~ spl0_4
| spl0_17
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f2204,f513]) ).
fof(f2224,plain,
( ~ spl0_4
| spl0_17
| spl0_32 ),
inference(avatar_contradiction_clause,[],[f2223]) ).
fof(f2267,plain,
( ~ ssList(sk2)
| nil = sk2
| spl0_39 ),
inference(resolution,[],[f1723,f76]) ).
fof(f2268,plain,
( nil = sk2
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f2267,f201]) ).
fof(f2269,plain,
( $false
| spl0_17
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f2268,f513]) ).
fof(f2270,plain,
( spl0_17
| spl0_39 ),
inference(avatar_contradiction_clause,[],[f2269]) ).
fof(f2448,plain,
( sk2 = cons(hd(sk2),skaf82(sk2))
| ~ ssList(sk2)
| nil = sk2
| ~ spl0_4
| ~ spl0_32 ),
inference(superposition,[],[f112,f1734]) ).
fof(f2449,plain,
( sk2 = cons(hd(sk2),skaf82(sk2))
| nil = sk2
| ~ spl0_4
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f2448,f201]) ).
fof(f2450,plain,
( sk2 = cons(hd(sk2),skaf82(sk2))
| ~ spl0_4
| spl0_17
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f2449,f513]) ).
fof(f2822,plain,
( ! [X0] :
( ~ ssList(app(X0,sk2))
| ~ ssList(X0)
| ~ ssList(skaf82(sk2))
| ~ ssItem(hd(sk2)) )
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32 ),
inference(superposition,[],[f1138,f2450]) ).
fof(f2831,plain,
( ! [X0] :
( ~ ssList(app(X0,sk2))
| ~ ssList(X0)
| ~ ssItem(hd(sk2)) )
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f2822,f13]) ).
fof(f2838,plain,
( ! [X0] :
( ~ ssList(app(X0,sk2))
| ~ ssList(X0) )
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f2831,f1724]) ).
fof(f3143,plain,
( ! [X0,X1] :
( ~ ssList(app(X0,app(X1,sk2)))
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(sk2) )
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(superposition,[],[f2838,f161]) ).
fof(f3146,plain,
( ! [X0,X1] :
( ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(sk2) )
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f3143,f798]) ).
fof(f3150,plain,
( ! [X0,X1] :
( ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f3146,f201]) ).
fof(f3155,plain,
( ! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f3150,f85]) ).
fof(f3157,plain,
( spl0_24
| spl0_24
| ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f3155,f1722,f1358,f1137,f512,f256,f1134,f1134]) ).
fof(f3159,plain,
( $false
| ~ spl0_24 ),
inference(resolution,[],[f1135,f13]) ).
fof(f3231,plain,
~ spl0_24,
inference(avatar_contradiction_clause,[],[f3159]) ).
cnf(s8,plain,
( spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f289]) ).
cnf(s11,plain,
spl0_4,
inference(sat_conversion,[],[f292]) ).
cnf(s14,plain,
( spl0_1
| ~ spl0_4
| ~ spl0_10
| ~ spl0_13
| ~ spl0_15 ),
inference(sat_conversion,[],[f460]) ).
cnf(s15,plain,
( ~ spl0_4
| ~ spl0_10
| spl0_13 ),
inference(sat_conversion,[],[f463]) ).
cnf(s18,plain,
( ~ spl0_1
| spl0_17 ),
inference(sat_conversion,[],[f523]) ).
cnf(s26,plain,
( ~ spl0_11
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s39,plain,
( ~ spl0_4
| ~ spl0_17 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s43,plain,
( ~ spl0_10
| spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s65,plain,
( ~ spl0_4
| spl0_17
| spl0_32 ),
inference(sat_conversion,[],[f2224]) ).
cnf(s67,plain,
( spl0_17
| spl0_39 ),
inference(sat_conversion,[],[f2270]) ).
cnf(s116,plain,
( spl0_24
| spl0_17
| ~ spl0_4
| spl0_24
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(sat_conversion,[],[f3157]) ).
cnf(s117,plain,
( ~ spl0_4
| spl0_17
| spl0_24
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(rat,[],[s116]) ).
cnf(s151,plain,
~ spl0_24,
inference(sat_conversion,[],[f3231]) ).
cnf(s153,plain,
( ~ spl0_4
| spl0_17
| ~ spl0_25
| ~ spl0_32
| ~ spl0_39 ),
inference(rat,[],[s117,s151]) ).
cnf(s161,plain,
( ~ spl0_11
| spl0_25 ),
inference(rat,[],[s26,s151]) ).
cnf(s163,plain,
~ spl0_17,
inference(rat,[],[s39,s11]) ).
cnf(s164,plain,
spl0_39,
inference(rat,[],[s67,s163]) ).
cnf(s165,plain,
spl0_32,
inference(rat,[],[s65,s11,s163]) ).
cnf(s166,plain,
~ spl0_1,
inference(rat,[],[s18,s163]) ).
cnf(s169,plain,
~ spl0_25,
inference(rat,[],[s153,s164,s163,s11,s165]) ).
cnf(s170,plain,
~ spl0_11,
inference(rat,[],[s161,s169]) ).
cnf(s171,plain,
spl0_10,
inference(rat,[],[s8,s170]) ).
cnf(s172,plain,
spl0_15,
inference(rat,[],[s43,s163,s171]) ).
cnf(s174,plain,
spl0_13,
inference(rat,[],[s15,s11,s171]) ).
cnf(s175,plain,
$false,
inference(rat,[],[s14,s172,s166,s11,s174,s171]) ).
fof(f3233,plain,
$false,
inference(avatar_sat_refutation,[],[s175]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC420-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.01/0.17 % Computer : n012.cluster.edu
% 0.01/0.17 % Model : x86_64 x86_64
% 0.01/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.01/0.17 % Memory : 8046.5625MB
% 0.01/0.17 % OS : Linux 6.8.0-71-generic
% 0.01/0.17 % CPULimit : 300
% 0.01/0.17 % WCLimit : 300
% 0.01/0.17 % DateTime : Mon Sep 28 09:35:34 UTC 2026
% 0.01/0.17 % CPUTime :
% 0.01/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.01/0.19 Running first-order theorem proving
% 0.01/0.19 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.51/0.69 % (3258505)Input is clausal, will run a generic CNF schedule.
% 1.51/0.69 % (3258514)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2416939381:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 1.51/0.69 % (3258516)dis-21_1_sil=8000:lcm=predicate:random_seed=1299477546: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)
% 1.51/0.69 % (3258512)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1090319861:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 1.51/0.69 % (3258513)lrs+10_1_sil=8000:sp=occurrence:random_seed=178115986:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 1.51/0.69 % (3258515)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1973186616:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 1.51/0.69 % (3258511)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3811366660:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 1.51/0.69 % (3258510)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=3110995549:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 1.51/0.69 % (3258514)Instruction limit reached!
% 1.51/0.69 % (3258514)------------------------------
% 1.51/0.69 % (3258514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.69 % (3258514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.69 % (3258514)CaDiCaL version: 2.1.3
% 1.51/0.69 % (3258514)Termination reason: Instruction limit
% 1.51/0.69 % (3258514)Termination phase: Saturation
% 1.51/0.69 % (3258514)Time elapsed: 0.028 s
% 1.51/0.69 % (3258514)Peak memory usage: 88 MB
% 1.51/0.69 % (3258514)Instructions burned: 124 (million)
% 1.51/0.69 % (3258516)Instruction limit reached!
% 1.51/0.69 % (3258516)------------------------------
% 1.51/0.69 % (3258516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.69 % (3258516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.69 % (3258516)CaDiCaL version: 2.1.3
% 1.51/0.69 % (3258516)Termination reason: Instruction limit
% 1.51/0.69 % (3258516)Termination phase: Saturation
% 1.51/0.69 % (3258516)Time elapsed: 0.031 s
% 1.51/0.69 % (3258516)Peak memory usage: 89 MB
% 1.51/0.69 % (3258516)Instructions burned: 117 (million)
% 1.51/0.69 % (3258513)Instruction limit reached!
% 1.51/0.69 % (3258513)------------------------------
% 1.51/0.69 % (3258513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.69 % (3258513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.69 % (3258513)CaDiCaL version: 2.1.3
% 1.51/0.69 % (3258513)Termination reason: Instruction limit
% 1.51/0.69 % (3258513)Termination phase: Saturation
% 1.51/0.69 % (3258513)Time elapsed: 0.032 s
% 1.51/0.69 % (3258513)Peak memory usage: 89 MB
% 1.51/0.69 % (3258513)Instructions burned: 110 (million)
% 1.51/0.69 % (3258515)First to succeed.
% 1.51/0.69 % (3258515)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3258505"
% 1.51/0.69 % (3258525)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3041629334:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 1.51/0.69 % (3258526)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3879365701:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 1.51/0.69 % (3258524)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=3371593043:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 1.51/0.69 % (3258526)Refutation not found, incomplete strategy
% 1.51/0.69 % (3258526)------------------------------
% 1.51/0.69 % (3258526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.69 % (3258526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.69 % (3258526)CaDiCaL version: 2.1.3
% 1.51/0.69 % (3258524)Refutation not found, incomplete strategy
% 1.51/0.69 % (3258524)------------------------------
% 1.51/0.69 % (3258524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.69 % (3258526)Termination reason: Refutation not found, incomplete strategy
% 1.51/0.69 % (3258526)Time elapsed: 0.001 s
% 1.51/0.69 % (3258526)Peak memory usage: 88 MB
% 1.51/0.69 % (3258524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.69 % (3258526)Instructions burned: 2 (million)
% 1.51/0.69 % (3258524)CaDiCaL version: 2.1.3
% 1.51/0.69 % (3258524)Termination reason: Refutation not found, incomplete strategy
% 1.51/0.69 % (3258524)Time elapsed: 0.001 s
% 1.51/0.69 % (3258524)Peak memory usage: 88 MB
% 1.51/0.69 % (3258524)Instructions burned: 1 (million)
% 1.51/0.69 % (3258525)Instruction limit reached!
% 1.51/0.69 % (3258525)------------------------------
% 1.51/0.69 % (3258525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.51/0.69 % (3258525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.69 % (3258525)CaDiCaL version: 2.1.3
% 1.51/0.69 % (3258525)Termination reason: Instruction limit
% 1.51/0.69 % (3258525)Termination phase: Saturation
% 1.51/0.69 % (3258525)Time elapsed: 0.050 s
% 1.51/0.69 % (3258525)Peak memory usage: 90 MB
% 1.51/0.69 % (3258525)Instructions burned: 191 (million)
% 1.51/0.69 % (3258515)Refutation found. Thanks to Tanya!
% 1.51/0.69 % SZS status Unsatisfiable for theBenchmark
% 1.51/0.69 % SZS output start Proof for theBenchmark
% See solution above
% 2.34/0.79 % (3258515)------------------------------
% 2.34/0.79 % (3258515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.34/0.79 % (3258515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.34/0.79 % (3258515)CaDiCaL version: 2.1.3
% 2.34/0.79 % (3258515)Termination reason: Refutation
% 2.34/0.79 % (3258515)Time elapsed: 0.041 s
% 2.34/0.79 % (3258515)Peak memory usage: 90 MB
% 2.34/0.79 % (3258515)Instructions burned: 114 (million)
% 2.34/0.79 % (3258515)------------------------------
% 2.34/0.79 % (3258515)------------------------------
% 2.34/0.79 % (3258505)Success in time 0.311 s
% 2.34/0.79 % Vampire exiting
%------------------------------------------------------------------------------