%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC091-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:04:37 PM UTC 2026
% Result : Unsatisfiable 12.39s 2.28s
% Output : Refutation 12.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 55
% Syntax : Number of formulae : 259 ( 53 unt; 22 def)
% Number of atoms : 738 ( 78 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 775 ( 296 ~; 457 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 23 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 157 ( 0 sgn 157 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f51,axiom,
! [X0,X1] : ssList(skaf45(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause51) ).
fof(f56,axiom,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause56) ).
fof(f57,axiom,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause57) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f67,axiom,
! [X0] :
( ~ ssItem(X0)
| totalorderedP(cons(X0,nil)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause67) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f76,axiom,
! [X0] :
( ~ ssList(X0)
| ssItem(hd(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause76) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f100,axiom,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause100) ).
fof(f102,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
fof(f104,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause102) ).
fof(f105,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| neq(X1,X0)
| X0 = X1 ),
inference(reorient_equations,[],[f104]) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f143,axiom,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X1,skaf45(X0,X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause132) ).
fof(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause178) ).
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/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_1) ).
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,
frontsegP(sk4,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
totalorderedP(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,nil)
| ~ segmentP(sk2,X0)
| ~ segmentP(sk1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
! [X0] :
( ~ ssList(X0)
| ~ neq(sk3,X0)
| ~ frontsegP(sk4,X0)
| ~ segmentP(X0,sk3)
| ~ totalorderedP(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f212,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f213,plain,
neq(sk4,nil),
inference(definition_unfolding,[],[f206,f204]) ).
fof(f214,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,nil)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0) ),
inference(definition_unfolding,[],[f209,f204,f205]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),X2))
| segmentP(app(app(X0,X1),X2),X1) ),
inference(equality_resolution,[],[f187]) ).
fof(f231,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(equality_resolution,[],[f192]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(equality_resolution,[],[f193]) ).
fof(f243,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f247,plain,
! [X0] : ~ ssItem(skaf83(X0)),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f248,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f286,plain,
! [X0,X1] : ~ ssList(skaf45(X0,X1)),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f290,plain,
! [X0] :
( ~ segmentP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f291,plain,
! [X0] :
( ~ segmentP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f294,plain,
! [X0] :
( frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f301,plain,
! [X0] :
( ssItem(X0)
| ~ totalorderedP(cons(X0,nil)) ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f306,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f308,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f309,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f310,plain,
! [X0] :
( ~ ssItem(hd(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f319,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f320,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f333,plain,
! [X0,X1] :
( cons(X0,X1) != X1
| ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f334,plain,
! [X0,X1] :
( ~ neq(X1,X0)
| ssList(X1)
| ssList(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f336,plain,
! [X0,X1] :
( ~ neq(X1,X0)
| ssItem(X1)
| ssItem(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f338,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f343,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f354,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f366,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| app(X1,skaf45(X0,X1)) = X0 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f407,plain,
! [X2,X0,X1] :
( ~ segmentP(app(app(X0,X1),X2),X1)
| ssList(X0)
| ssList(X1)
| ssList(app(app(X0,X1),X2))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f412,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f413,plain,
! [X2,X3,X0,X1] :
( ssList(X3)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f420,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f211]) ).
fof(f421,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f424,plain,
~ neq(sk4,nil),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f425,plain,
~ totalorderedP(sk3),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f426,plain,
! [X0] :
( neq(X0,nil)
| ssList(X0)
| segmentP(sk4,X0)
| segmentP(sk3,X0) ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f427,plain,
! [X0] :
( ~ frontsegP(sk4,X0)
| neq(sk3,X0)
| ssList(X0)
| segmentP(X0,sk3)
| totalorderedP(X0) ),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f428,plain,
! [X3,X0,X1] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f412]) ).
fof(f439,definition,
( spl0_2
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f440,plain,
( ~ ssList(nil)
| spl0_2 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f444,definition,
( spl0_3
<=> ! [X1] :
( ssItem(X1)
| ~ totalorderedP(cons(X1,nil)) ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f445,plain,
( ! [X1] :
( ~ totalorderedP(cons(X1,nil))
| ssItem(X1) )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f467,definition,
( spl0_8
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f468,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f470,definition,
( spl0_9
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f471,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( spl0_8
| spl0_9 ),
inference(avatar_split_clause,[],[f306,f470,f467]) ).
fof(f473,plain,
spl0_3,
inference(avatar_split_clause,[],[f301,f444]) ).
fof(f475,plain,
~ spl0_2,
inference(avatar_split_clause,[],[f243,f439]) ).
fof(f487,plain,
( neq(sk3,sk3)
| ssList(sk3)
| segmentP(sk3,sk3)
| totalorderedP(sk3) ),
inference(resolution,[],[f427,f207]) ).
fof(f488,plain,
( neq(sk3,sk3)
| segmentP(sk3,sk3)
| totalorderedP(sk3) ),
inference(forward_subsumption_resolution,[],[f487,f420]) ).
fof(f489,plain,
( neq(sk3,sk3)
| segmentP(sk3,sk3) ),
inference(forward_subsumption_resolution,[],[f488,f425]) ).
fof(f491,definition,
( spl0_12
<=> segmentP(sk3,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f492,plain,
( ~ segmentP(sk3,sk3)
| spl0_12 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f493,plain,
( segmentP(sk3,sk3)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f495,definition,
( spl0_13
<=> neq(sk3,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f497,plain,
( neq(sk3,sk3)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f498,plain,
( spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f489,f495,f491]) ).
fof(f499,plain,
( ssList(sk3)
| ~ spl0_12 ),
inference(resolution,[],[f291,f493]) ).
fof(f500,plain,
( $false
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f499,f420]) ).
fof(f501,plain,
~ spl0_12,
inference(avatar_contradiction_clause,[],[f500]) ).
fof(f511,definition,
( spl0_15
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f512,plain,
( ~ neq(sk3,nil)
| spl0_15 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f513,plain,
( neq(sk3,nil)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f523,definition,
( spl0_17
<=> segmentP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f525,plain,
( segmentP(sk4,sk3)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f589,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f308,f420]) ).
fof(f591,plain,
! [X0] :
( ssList(X0)
| nil = X0
| tl(X0) = app(nil,tl(X0)) ),
inference(resolution,[],[f309,f308]) ).
fof(f796,plain,
( sk4 = cons(hd(sk4),tl(sk4))
| nil = sk4 ),
inference(resolution,[],[f338,f421]) ).
fof(f798,definition,
( spl0_21
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f799,plain,
( nil != sk4
| spl0_21 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f800,plain,
( nil = sk4
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f802,definition,
( spl0_22
<=> sk4 = cons(hd(sk4),tl(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f804,plain,
( sk4 = cons(hd(sk4),tl(sk4))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f805,plain,
( spl0_21
| spl0_22 ),
inference(avatar_split_clause,[],[f796,f802,f798]) ).
fof(f807,definition,
( spl0_23
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f809,plain,
( nil = sk3
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f848,plain,
( sk4 = cons(skaf83(sk4),skaf82(sk4))
| nil = sk4 ),
inference(resolution,[],[f343,f421]) ).
fof(f850,definition,
( spl0_25
<=> sk4 = cons(skaf83(sk4),skaf82(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f852,plain,
( sk4 = cons(skaf83(sk4),skaf82(sk4))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f850]) ).
fof(f853,plain,
( spl0_21
| spl0_25 ),
inference(avatar_split_clause,[],[f848,f850,f798]) ).
fof(f862,plain,
( ~ neq(nil,nil)
| ~ spl0_21 ),
inference(superposition,[],[f424,f800]) ).
fof(f937,plain,
( neq(nil,nil)
| ~ spl0_13
| ~ spl0_23 ),
inference(superposition,[],[f497,f809]) ).
fof(f981,plain,
( sk4 != tl(sk4)
| ssItem(hd(sk4))
| ssList(tl(sk4))
| ~ spl0_22 ),
inference(superposition,[],[f333,f804]) ).
fof(f985,definition,
( spl0_27
<=> ssList(tl(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f986,plain,
( ~ ssList(tl(sk4))
| spl0_27 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f987,plain,
( ssList(tl(sk4))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f989,definition,
( spl0_28
<=> ssItem(hd(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f991,plain,
( ssItem(hd(sk4))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f989]) ).
fof(f993,definition,
( spl0_29
<=> sk4 = tl(sk4) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f995,plain,
( sk4 != tl(sk4)
| spl0_29 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f996,plain,
( spl0_27
| spl0_28
| ~ spl0_29
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f981,f802,f993,f989,f985]) ).
fof(f1040,plain,
( ssList(sk3)
| ssList(nil)
| nil = sk3
| ~ spl0_15 ),
inference(resolution,[],[f513,f334]) ).
fof(f1041,plain,
( ssList(nil)
| nil = sk3
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1040,f420]) ).
fof(f1042,plain,
( nil = sk3
| spl0_2
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1041,f440]) ).
fof(f1043,plain,
( spl0_23
| spl0_2
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1042,f511,f439,f807]) ).
fof(f1180,plain,
( ssList(sk3)
| ssList(sk4)
| sk4 = app(sk3,skaf45(sk4,sk3)) ),
inference(resolution,[],[f366,f207]) ).
fof(f1187,plain,
( ssList(sk4)
| sk4 = app(sk3,skaf45(sk4,sk3)) ),
inference(forward_subsumption_resolution,[],[f1180,f420]) ).
fof(f1192,plain,
sk4 = app(sk3,skaf45(sk4,sk3)),
inference(forward_subsumption_resolution,[],[f1187,f421]) ).
fof(f1641,plain,
( ! [X0] :
( frontsegP(sk4,cons(hd(sk4),X0))
| ssList(X0)
| ssList(tl(sk4))
| ssItem(hd(sk4))
| ~ frontsegP(tl(sk4),X0) )
| ~ spl0_22 ),
inference(superposition,[],[f428,f804]) ).
fof(f1648,definition,
( spl0_38
<=> ! [X0] :
( frontsegP(sk4,cons(hd(sk4),X0))
| ~ frontsegP(tl(sk4),X0)
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f1649,plain,
( ! [X0] :
( ~ frontsegP(tl(sk4),X0)
| frontsegP(sk4,cons(hd(sk4),X0))
| ssList(X0) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f1648]) ).
fof(f1650,plain,
( spl0_28
| spl0_27
| spl0_38
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1641,f802,f1648,f985,f989]) ).
fof(f2053,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(nil)
| ssList(sk3)
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(superposition,[],[f407,f589]) ).
fof(f2060,plain,
( ! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(sk3)
| ssList(app(sk3,X0))
| ssList(X0) )
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f2053,f440]) ).
fof(f2062,plain,
( ! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(app(sk3,X0))
| ssList(X0) )
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f2060,f420]) ).
fof(f2192,plain,
( ssList(sk4)
| nil = sk4
| ~ spl0_28 ),
inference(resolution,[],[f991,f310]) ).
fof(f2193,plain,
( nil = sk4
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f2192,f421]) ).
fof(f2194,plain,
( $false
| spl0_21
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f2193,f799]) ).
fof(f2195,plain,
( spl0_21
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f2194]) ).
fof(f2206,plain,
( ssList(sk4)
| nil = sk4
| ~ spl0_27 ),
inference(resolution,[],[f987,f309]) ).
fof(f2207,plain,
( nil = sk4
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f2206,f421]) ).
fof(f2213,plain,
( $false
| ~ spl0_13
| ~ spl0_21
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f862,f937]) ).
fof(f2214,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2213]) ).
fof(f2224,plain,
( spl0_21
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f2207,f985,f798]) ).
fof(f2238,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f413,f471]) ).
fof(f2239,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0)))
| ssList(cons(X2,X3)) )
| ~ spl0_9 ),
inference(resolution,[],[f2238,f319]) ).
fof(f2250,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0))) )
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f2239,f320]) ).
fof(f2252,definition,
( spl0_71
<=> ! [X3] : ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f2253,plain,
( ! [X3] : ssList(X3)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f2252]) ).
fof(f2255,definition,
( spl0_72
<=> ! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,cons(X2,X0)))
| ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f2256,plain,
( ! [X2,X0,X1] :
( ssList(app(X1,cons(X2,X0)))
| ssList(X1)
| ssList(X0)
| ssItem(X2) )
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f2255]) ).
fof(f2257,plain,
( spl0_71
| spl0_72
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f2250,f470,f2255,f2252]) ).
fof(f8770,plain,
( nil = sk4
| tl(sk4) = app(nil,tl(sk4)) ),
inference(resolution,[],[f591,f421]) ).
fof(f8771,plain,
( tl(sk4) = app(nil,tl(sk4))
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f8770,f799]) ).
fof(f9137,plain,
( ! [X0] :
( ssList(app(X0,sk4))
| ssList(X0)
| ssList(skaf82(sk4))
| ssItem(skaf83(sk4)) )
| ~ spl0_25
| ~ spl0_72 ),
inference(superposition,[],[f2256,f852]) ).
fof(f9139,plain,
( ! [X0] :
( ssList(app(X0,sk4))
| ssList(X0)
| ssItem(skaf83(sk4)) )
| ~ spl0_25
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f9137,f248]) ).
fof(f9142,plain,
( ! [X0] :
( ssList(app(X0,sk4))
| ssList(X0) )
| ~ spl0_25
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f9139,f247]) ).
fof(f9915,plain,
( ! [X0] :
( ssList(X0)
| ssList(X0)
| ssList(sk4) )
| ~ spl0_25
| ~ spl0_72 ),
inference(resolution,[],[f9142,f319]) ).
fof(f9919,plain,
( ! [X0] :
( ssList(X0)
| ssList(sk4) )
| ~ spl0_25
| ~ spl0_72 ),
inference(duplicate_literal_removal,[],[f9915]) ).
fof(f9924,plain,
( ! [X0] : ssList(X0)
| ~ spl0_25
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f9919,f421]) ).
fof(f9929,plain,
( spl0_71
| ~ spl0_25
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f9924,f2255,f850,f2252]) ).
fof(f9999,plain,
( $false
| ~ spl0_71 ),
inference(backward_subsumption_resolution,[],[f421,f2253]) ).
fof(f10035,plain,
~ spl0_71,
inference(avatar_contradiction_clause,[],[f9999]) ).
fof(f10245,plain,
( ! [X0,X1] :
( ~ neq(X1,X0)
| ssItem(X1)
| X0 = X1 )
| ~ spl0_8 ),
inference(backward_subsumption_resolution,[],[f336,f468]) ).
fof(f10254,plain,
( ! [X0,X1] :
( ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) )
| ~ spl0_8 ),
inference(backward_subsumption_resolution,[],[f354,f468]) ).
fof(f10290,plain,
( ! [X1] : ~ totalorderedP(cons(X1,nil))
| ~ spl0_3
| ~ spl0_8 ),
inference(backward_subsumption_resolution,[],[f445,f468]) ).
fof(f10354,plain,
( ! [X0,X1] :
( ~ neq(X1,X0)
| X0 = X1 )
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f10245,f468]) ).
fof(f13982,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1) )
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f320,f468]) ).
fof(f14472,plain,
( ! [X0,X1] :
( ssList(X1)
| cons(X0,tl(X1)) = app(cons(X0,nil),tl(X1))
| nil = X1 )
| ~ spl0_8 ),
inference(resolution,[],[f10254,f309]) ).
fof(f28755,plain,
( ! [X0] :
( cons(X0,tl(sk4)) = app(cons(X0,nil),tl(sk4))
| nil = sk4 )
| ~ spl0_8 ),
inference(resolution,[],[f14472,f421]) ).
fof(f28756,plain,
( ! [X0] : cons(X0,tl(sk4)) = app(cons(X0,nil),tl(sk4))
| ~ spl0_8
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f28755,f799]) ).
fof(f61651,plain,
( frontsegP(sk4,cons(hd(sk4),nil))
| ssList(nil)
| ssList(tl(sk4))
| ~ spl0_38 ),
inference(resolution,[],[f1649,f294]) ).
fof(f61655,plain,
( frontsegP(sk4,cons(hd(sk4),nil))
| ssList(tl(sk4))
| spl0_2
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f61651,f440]) ).
fof(f61660,plain,
( frontsegP(sk4,cons(hd(sk4),nil))
| spl0_2
| spl0_27
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f61655,f986]) ).
fof(f63132,plain,
( neq(sk3,cons(hd(sk4),nil))
| ssList(cons(hd(sk4),nil))
| segmentP(cons(hd(sk4),nil),sk3)
| totalorderedP(cons(hd(sk4),nil))
| spl0_2
| spl0_27
| ~ spl0_38 ),
inference(resolution,[],[f61660,f427]) ).
fof(f63149,plain,
( neq(sk3,cons(hd(sk4),nil))
| ssList(cons(hd(sk4),nil))
| segmentP(cons(hd(sk4),nil),sk3)
| spl0_2
| ~ spl0_3
| ~ spl0_8
| spl0_27
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f63132,f10290]) ).
fof(f63155,definition,
( spl0_1268
<=> ssList(cons(hd(sk4),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1268])],[avatar_definition]) ).
fof(f63157,plain,
( ssList(cons(hd(sk4),nil))
| ~ spl0_1268 ),
inference(avatar_component_clause,[],[f63155]) ).
fof(f63181,plain,
( neq(nil,cons(hd(sk4),nil))
| ssList(cons(hd(sk4),nil))
| segmentP(cons(hd(sk4),nil),sk3)
| spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_23
| spl0_27
| ~ spl0_38 ),
inference(forward_demodulation,[],[f63149,f809]) ).
fof(f63192,plain,
( segmentP(cons(hd(sk4),nil),nil)
| neq(nil,cons(hd(sk4),nil))
| ssList(cons(hd(sk4),nil))
| spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_23
| spl0_27
| ~ spl0_38 ),
inference(forward_demodulation,[],[f63181,f809]) ).
fof(f63193,plain,
( neq(nil,cons(hd(sk4),nil))
| ssList(cons(hd(sk4),nil))
| spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_23
| spl0_27
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f63192,f290]) ).
fof(f63195,definition,
( spl0_1276
<=> neq(nil,cons(hd(sk4),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1276])],[avatar_definition]) ).
fof(f63197,plain,
( neq(nil,cons(hd(sk4),nil))
| ~ spl0_1276 ),
inference(avatar_component_clause,[],[f63195]) ).
fof(f63198,plain,
( spl0_1268
| spl0_1276
| spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_23
| spl0_27
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f63193,f1648,f985,f807,f467,f444,f439,f63195,f63155]) ).
fof(f64712,plain,
( nil = cons(hd(sk4),nil)
| ~ spl0_8
| ~ spl0_1276 ),
inference(resolution,[],[f63197,f10354]) ).
fof(f64716,definition,
( spl0_1285
<=> nil = cons(hd(sk4),nil) ),
introduced(definition,[new_symbols(definition,[spl0_1285])],[avatar_definition]) ).
fof(f64718,plain,
( nil = cons(hd(sk4),nil)
| ~ spl0_1285 ),
inference(avatar_component_clause,[],[f64716]) ).
fof(f64905,plain,
( spl0_1285
| ~ spl0_8
| ~ spl0_1276 ),
inference(avatar_split_clause,[],[f64712,f63195,f467,f64716]) ).
fof(f64950,plain,
( cons(hd(sk4),tl(sk4)) = app(nil,tl(sk4))
| ~ spl0_8
| spl0_21
| ~ spl0_1285 ),
inference(superposition,[],[f28756,f64718]) ).
fof(f65031,plain,
( tl(sk4) = cons(hd(sk4),tl(sk4))
| ~ spl0_8
| spl0_21
| ~ spl0_1285 ),
inference(forward_demodulation,[],[f64950,f8771]) ).
fof(f65067,plain,
( sk4 = tl(sk4)
| ~ spl0_8
| spl0_21
| ~ spl0_22
| ~ spl0_1285 ),
inference(forward_demodulation,[],[f65031,f804]) ).
fof(f65072,plain,
( $false
| ~ spl0_8
| spl0_21
| ~ spl0_22
| spl0_29
| ~ spl0_1285 ),
inference(forward_subsumption_resolution,[],[f65067,f995]) ).
fof(f65073,plain,
( ~ spl0_8
| spl0_21
| ~ spl0_22
| spl0_29
| ~ spl0_1285 ),
inference(avatar_contradiction_clause,[],[f65072]) ).
fof(f65074,plain,
( ssList(nil)
| ~ spl0_8
| ~ spl0_1268 ),
inference(resolution,[],[f63157,f13982]) ).
fof(f65075,plain,
( $false
| spl0_2
| ~ spl0_8
| ~ spl0_1268 ),
inference(forward_subsumption_resolution,[],[f65074,f440]) ).
fof(f65076,plain,
( spl0_2
| ~ spl0_8
| ~ spl0_1268 ),
inference(avatar_contradiction_clause,[],[f65075]) ).
fof(f65224,definition,
( spl0_1294
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_1294])],[avatar_definition]) ).
fof(f65225,plain,
( ~ ssList(sk3)
| spl0_1294 ),
inference(avatar_component_clause,[],[f65224]) ).
fof(f65463,plain,
~ spl0_1294,
inference(avatar_split_clause,[],[f420,f65224]) ).
fof(f66351,plain,
( ssList(sk3)
| segmentP(sk4,sk3)
| segmentP(sk3,sk3)
| spl0_15 ),
inference(resolution,[],[f512,f426]) ).
fof(f66352,plain,
( segmentP(sk4,sk3)
| segmentP(sk3,sk3)
| spl0_15
| spl0_1294 ),
inference(forward_subsumption_resolution,[],[f66351,f65225]) ).
fof(f66353,plain,
( segmentP(sk4,sk3)
| spl0_12
| spl0_15
| spl0_1294 ),
inference(forward_subsumption_resolution,[],[f66352,f492]) ).
fof(f66354,plain,
( spl0_17
| spl0_12
| spl0_15
| spl0_1294 ),
inference(avatar_split_clause,[],[f66353,f65224,f511,f491,f523]) ).
fof(f74039,plain,
( ~ segmentP(sk4,sk3)
| ssList(sk4)
| ssList(skaf45(sk4,sk3))
| spl0_2 ),
inference(superposition,[],[f2062,f1192]) ).
fof(f74052,plain,
( ssList(sk4)
| ssList(skaf45(sk4,sk3))
| spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f74039,f525]) ).
fof(f74062,plain,
( ssList(skaf45(sk4,sk3))
| spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f74052,f421]) ).
fof(f74064,plain,
( $false
| spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f74062,f286]) ).
fof(f74065,plain,
( spl0_2
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f74064]) ).
cnf(s7,plain,
( spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f472]) ).
cnf(s8,plain,
spl0_3,
inference(sat_conversion,[],[f473]) ).
cnf(s10,plain,
~ spl0_2,
inference(sat_conversion,[],[f475]) ).
cnf(s12,plain,
( spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f498]) ).
cnf(s13,plain,
~ spl0_12,
inference(sat_conversion,[],[f501]) ).
cnf(s17,plain,
( spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f805]) ).
cnf(s19,plain,
( spl0_21
| spl0_25 ),
inference(sat_conversion,[],[f853]) ).
cnf(s25,plain,
( ~ spl0_22
| spl0_27
| spl0_28
| ~ spl0_29 ),
inference(sat_conversion,[],[f996]) ).
cnf(s29,plain,
( spl0_2
| ~ spl0_15
| spl0_23 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s34,plain,
( ~ spl0_22
| spl0_27
| spl0_28
| spl0_38 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s70,plain,
( spl0_21
| ~ spl0_28 ),
inference(sat_conversion,[],[f2195]) ).
cnf(s74,plain,
( ~ spl0_13
| ~ spl0_21
| ~ spl0_23 ),
inference(sat_conversion,[],[f2214]) ).
cnf(s77,plain,
( spl0_21
| ~ spl0_27 ),
inference(sat_conversion,[],[f2224]) ).
cnf(s85,plain,
( ~ spl0_9
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f2257]) ).
cnf(s241,plain,
( ~ spl0_25
| spl0_71
| ~ spl0_72 ),
inference(sat_conversion,[],[f9929]) ).
cnf(s277,plain,
~ spl0_71,
inference(sat_conversion,[],[f10035]) ).
cnf(s1503,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_8
| ~ spl0_23
| spl0_27
| ~ spl0_38
| spl0_1268
| spl0_1276 ),
inference(sat_conversion,[],[f63198]) ).
cnf(s1537,plain,
( ~ spl0_8
| ~ spl0_1276
| spl0_1285 ),
inference(sat_conversion,[],[f64905]) ).
cnf(s1544,plain,
( ~ spl0_8
| spl0_21
| ~ spl0_22
| spl0_29
| ~ spl0_1285 ),
inference(sat_conversion,[],[f65073]) ).
cnf(s1545,plain,
( spl0_2
| ~ spl0_8
| ~ spl0_1268 ),
inference(sat_conversion,[],[f65076]) ).
cnf(s1578,plain,
~ spl0_1294,
inference(sat_conversion,[],[f65463]) ).
cnf(s1665,plain,
( spl0_12
| spl0_15
| spl0_17
| spl0_1294 ),
inference(sat_conversion,[],[f66354]) ).
cnf(s2240,plain,
( spl0_2
| ~ spl0_17 ),
inference(sat_conversion,[],[f74065]) ).
cnf(s2282,plain,
( ~ spl0_25
| ~ spl0_72 ),
inference(rat,[],[s241,s277]) ).
cnf(s2393,plain,
( ~ spl0_9
| spl0_72 ),
inference(rat,[],[s85,s277]) ).
cnf(s2394,plain,
spl0_13,
inference(rat,[],[s12,s13]) ).
cnf(s2396,plain,
~ spl0_17,
inference(rat,[],[s2240,s10]) ).
cnf(s2413,plain,
spl0_15,
inference(rat,[],[s1665,s1578,s13,s2396]) ).
cnf(s2426,plain,
spl0_23,
inference(rat,[],[s29,s10,s2413]) ).
cnf(s2494,plain,
~ spl0_21,
inference(rat,[],[s74,s2394,s2426]) ).
cnf(s2533,plain,
~ spl0_27,
inference(rat,[],[s77,s2494]) ).
cnf(s2534,plain,
~ spl0_28,
inference(rat,[],[s70,s2494]) ).
cnf(s2535,plain,
spl0_25,
inference(rat,[],[s19,s2494]) ).
cnf(s2536,plain,
spl0_22,
inference(rat,[],[s17,s2494]) ).
cnf(s2736,plain,
~ spl0_72,
inference(rat,[],[s2282,s2535]) ).
cnf(s2756,plain,
spl0_38,
inference(rat,[],[s34,s2533,s2534,s2536]) ).
cnf(s2760,plain,
~ spl0_29,
inference(rat,[],[s25,s2533,s2534,s2536]) ).
cnf(s2799,plain,
~ spl0_9,
inference(rat,[],[s2393,s2736]) ).
cnf(s2816,plain,
spl0_8,
inference(rat,[],[s7,s2799]) ).
cnf(s2828,plain,
~ spl0_1268,
inference(rat,[],[s1545,s10,s2816]) ).
cnf(s2829,plain,
~ spl0_1285,
inference(rat,[],[s1544,s2536,s2760,s2494,s2816]) ).
cnf(s2830,plain,
~ spl0_1276,
inference(rat,[],[s1537,s2829,s2816]) ).
cnf(s2886,plain,
$false,
inference(rat,[],[s1503,s2830,s8,s2756,s2533,s2426,s10,s2828,s2816]) ).
fof(f74066,plain,
$false,
inference(avatar_sat_refutation,[],[s2886]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC091-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 % Computer : n017.cluster.edu
% 0.09/0.40 % Model : x86_64 x86_64
% 0.09/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.40 % Memory : 8046.5625MB
% 0.09/0.40 % OS : Linux 6.8.0-71-generic
% 0.09/0.40 % CPULimit : 300
% 0.09/0.40 % WCLimit : 300
% 0.09/0.40 % DateTime : Mon Sep 28 07:44:36 UTC 2026
% 0.09/0.40 % CPUTime :
% 0.09/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.44 Running first-order model finding
% 0.09/0.44 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.39/2.28 % (3381229)Will run a generic schedule for satisfiability detection.
% 12.39/2.28 % (3381237)dis+10_1_sil=32000:sp=arity:random_seed=1630722430:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 12.39/2.28 % (3381235)% WARNING: option uhcvi not known.
% 12.39/2.28 % (3381234)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2210922930_2999 on theBenchmark for (2999ds/0Mi)
% 12.39/2.28 % (3381235)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3042186065:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 12.39/2.28 % (3381236)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2869760087:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 12.39/2.28 % (3381238)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2393098044:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 12.39/2.28 % (3381239)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4139894241:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 12.39/2.28 % (3381240)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1727477851:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 12.39/2.28 % TRYING [1]
% 12.39/2.28 % TRYING [2]
% 12.39/2.28 % TRYING [3]
% 12.39/2.28 % (3381237)Instruction limit reached!
% 12.39/2.28 % (3381237)------------------------------
% 12.39/2.28 % (3381237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381237)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381237)Termination reason: Instruction limit
% 12.39/2.28 % (3381237)Termination phase: Saturation
% 12.39/2.28 % (3381237)Time elapsed: 0.033 s
% 12.39/2.28 % (3381237)Peak memory usage: 13 MB
% 12.39/2.28 % (3381237)Instructions burned: 103 (million)
% 12.39/2.28 % TRYING [4]
% 12.39/2.28 % (3381248)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3718062533:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 12.39/2.28 % TRYING [1]
% 12.39/2.28 % TRYING [2]
% 12.39/2.28 % TRYING [3]
% 12.39/2.28 % TRYING [4]
% 12.39/2.28 % (3381238)Instruction limit reached!
% 12.39/2.28 % (3381238)------------------------------
% 12.39/2.28 % (3381238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381238)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381238)Termination reason: Instruction limit
% 12.39/2.28 % (3381238)Termination phase: Saturation
% 12.39/2.28 % (3381238)Time elapsed: 0.061 s
% 12.39/2.28 % (3381238)Peak memory usage: 13 MB
% 12.39/2.28 % (3381238)Instructions burned: 116 (million)
% 12.39/2.28 % (3381239)Instruction limit reached!
% 12.39/2.28 % (3381239)------------------------------
% 12.39/2.28 % (3381239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381239)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381239)Termination reason: Instruction limit
% 12.39/2.28 % (3381239)Termination phase: Saturation
% 12.39/2.28 % (3381239)Time elapsed: 0.069 s
% 12.39/2.28 % (3381239)Peak memory usage: 14 MB
% 12.39/2.28 % (3381239)Instructions burned: 132 (million)
% 12.39/2.28 % (3381250)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1120577751:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 12.39/2.28 % (3381251)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3828298647:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 12.39/2.28 % (3381240)Instruction limit reached!
% 12.39/2.28 % (3381240)------------------------------
% 12.39/2.28 % (3381240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381240)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381240)Termination reason: Instruction limit
% 12.39/2.28 % (3381240)Termination phase: Saturation
% 12.39/2.28 % (3381240)Time elapsed: 0.091 s
% 12.39/2.28 % (3381240)Peak memory usage: 14 MB
% 12.39/2.28 % (3381240)Instructions burned: 160 (million)
% 12.39/2.28 % TRYING [5]
% 12.39/2.28 % TRYING [5]
% 12.39/2.28 % (3381254)ott-21_1_sil=16000:fs=off:random_seed=2652583612:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 12.39/2.28 % (3381250)Instruction limit reached!
% 12.39/2.28 % (3381250)------------------------------
% 12.39/2.28 % (3381250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381250)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381250)Termination reason: Instruction limit
% 12.39/2.28 % (3381250)Termination phase: Saturation
% 12.39/2.28 % (3381250)Time elapsed: 0.068 s
% 12.39/2.28 % (3381250)Peak memory usage: 13 MB
% 12.39/2.28 % (3381250)Instructions burned: 131 (million)
% 12.39/2.28 % (3381256)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3720944454:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 12.39/2.28 % TRYING [6]
% 12.39/2.28 % (3381248)Instruction limit reached!
% 12.39/2.28 % (3381248)------------------------------
% 12.39/2.28 % (3381248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381248)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381248)Termination reason: Instruction limit
% 12.39/2.28 % (3381248)Termination phase: Finite model building constraint generation
% 12.39/2.28 % (3381248)Time elapsed: 0.157 s
% 12.39/2.28 % (3381248)Peak memory usage: 36 MB
% 12.39/2.28 % (3381248)Instructions burned: 721 (million)
% 12.39/2.28 % (3381254)Instruction limit reached!
% 12.39/2.28 % (3381254)------------------------------
% 12.39/2.28 % (3381254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381254)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381254)Termination reason: Instruction limit
% 12.39/2.28 % (3381254)Termination phase: Saturation
% 12.39/2.28 % (3381254)Time elapsed: 0.092 s
% 12.39/2.28 % (3381254)Peak memory usage: 13 MB
% 12.39/2.28 % (3381254)Instructions burned: 182 (million)
% 12.39/2.28 % (3381258)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3759005962:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 12.39/2.28 % TRYING [1]
% 12.39/2.28 % TRYING [2]
% 12.39/2.28 % TRYING [3]
% 12.39/2.28 % (3381259)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2425330554:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 12.39/2.28 % TRYING [4]
% 12.39/2.28 % TRYING [6]
% 12.39/2.28 % TRYING [5]
% 12.39/2.28 % (3381258)Instruction limit reached!
% 12.39/2.28 % (3381258)------------------------------
% 12.39/2.28 % (3381258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381258)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381258)Termination reason: Instruction limit
% 12.39/2.28 % (3381258)Termination phase: Finite model building SAT solving
% 12.39/2.28 % (3381258)Time elapsed: 0.181 s
% 12.39/2.28 % (3381258)Peak memory usage: 22 MB
% 12.39/2.28 % (3381258)Instructions burned: 870 (million)
% 12.39/2.28 % (3381262)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3888536917:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 12.39/2.28 % TRYING [14]
% 12.39/2.28 % (3381251)Instruction limit reached!
% 12.39/2.28 % (3381251)------------------------------
% 12.39/2.28 % (3381251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381251)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381251)Termination reason: Instruction limit
% 12.39/2.28 % (3381251)Termination phase: Saturation
% 12.39/2.28 % (3381251)Time elapsed: 0.412 s
% 12.39/2.28 % (3381251)Peak memory usage: 18 MB
% 12.39/2.28 % (3381251)Instructions burned: 684 (million)
% 12.39/2.28 % (3381256)Instruction limit reached!
% 12.39/2.28 % (3381256)------------------------------
% 12.39/2.28 % (3381256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381256)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381256)Termination reason: Instruction limit
% 12.39/2.28 % (3381256)Termination phase: Saturation
% 12.39/2.28 % (3381256)Time elapsed: 0.331 s
% 12.39/2.28 % (3381256)Peak memory usage: 14 MB
% 12.39/2.28 % (3381256)Instructions burned: 478 (million)
% 12.39/2.28 % (3381264)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3359193738:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 12.39/2.28 % (3381265)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1974146841:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 12.39/2.28 % (3381262)Instruction limit reached!
% 12.39/2.28 % (3381262)------------------------------
% 12.39/2.28 % (3381262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381262)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381262)Termination reason: Instruction limit
% 12.39/2.28 % (3381262)Termination phase: Finite model building constraint generation
% 12.39/2.28 % (3381262)Time elapsed: 0.180 s
% 12.39/2.28 % (3381262)Peak memory usage: 73 MB
% 12.39/2.28 % (3381262)Instructions burned: 894 (million)
% 12.39/2.28 % (3381268)fmb+10_1_sil=64000:random_seed=101491604:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 12.39/2.28 % TRYING [1]
% 12.39/2.28 % TRYING [2]
% 12.39/2.28 % TRYING [3]
% 12.39/2.28 % TRYING [4]
% 12.39/2.28 % TRYING [5]
% 12.39/2.28 % TRYING [7]
% 12.39/2.28 % (3381259)Instruction limit reached!
% 12.39/2.28 % (3381259)------------------------------
% 12.39/2.28 % (3381259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381259)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381259)Termination reason: Instruction limit
% 12.39/2.28 % (3381259)Termination phase: Saturation
% 12.39/2.28 % (3381259)Time elapsed: 0.667 s
% 12.39/2.28 % (3381259)Peak memory usage: 28 MB
% 12.39/2.28 % (3381259)Instructions burned: 1179 (million)
% 12.39/2.28 % (3381270)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2896083017:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 12.39/2.28 % TRYING [20]
% 12.39/2.28 % (3381264)Instruction limit reached!
% 12.39/2.28 % (3381264)------------------------------
% 12.39/2.28 % (3381264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381264)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381264)Termination reason: Instruction limit
% 12.39/2.28 % (3381264)Termination phase: Saturation
% 12.39/2.28 % (3381264)Time elapsed: 0.405 s
% 12.39/2.28 % (3381264)Peak memory usage: 21 MB
% 12.39/2.28 % (3381264)Instructions burned: 692 (million)
% 12.39/2.28 % TRYING [6]
% 12.39/2.28 % (3381272)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=665464189:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 12.39/2.28 % TRYING [8]
% 12.39/2.28 % (3381265)Instruction limit reached!
% 12.39/2.28 % (3381265)------------------------------
% 12.39/2.28 % (3381265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381265)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381265)Termination reason: Instruction limit
% 12.39/2.28 % (3381265)Termination phase: Saturation
% 12.39/2.28 % (3381265)Time elapsed: 0.474 s
% 12.39/2.28 % (3381265)Peak memory usage: 21 MB
% 12.39/2.28 % (3381265)Instructions burned: 879 (million)
% 12.39/2.28 % (3381274)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=420404318:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 12.39/2.28 % (3381272)Instruction limit reached!
% 12.39/2.28 % (3381272)------------------------------
% 12.39/2.28 % (3381272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381272)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381272)Termination reason: Instruction limit
% 12.39/2.28 % (3381272)Termination phase: Finite model building constraint generation
% 12.39/2.28 % (3381272)Time elapsed: 0.336 s
% 12.39/2.28 % (3381272)Peak memory usage: 79 MB
% 12.39/2.28 % (3381272)Instructions burned: 922 (million)
% 12.39/2.28 % (3381276)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=965255903:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 12.39/2.28 % TRYING [7]
% 12.39/2.28 % (3381235) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3381229-3381235"...
% 12.39/2.28 % (3381235)...printing done.
% 12.39/2.28 % (3381235)Refutation found. Thanks to Tanya!
% 12.39/2.28 % SZS status Unsatisfiable for theBenchmark
% 12.39/2.28 % SZS output start Proof for theBenchmark
% See solution above
% 12.39/2.28 % (3381235)------------------------------
% 12.39/2.28 % (3381235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.39/2.28 % (3381235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.39/2.28 % (3381235)CaDiCaL version: 2.1.3
% 12.39/2.28 % (3381235)Termination reason: Refutation
% 12.39/2.28 % (3381235)Time elapsed: 1.768 s
% 12.39/2.28 % (3381235)Peak memory usage: 44 MB
% 12.39/2.28 % (3381235)Instructions burned: 3355 (million)
% 12.39/2.28 % (3381229)Success in time 1.834 s
% 12.39/2.28 % Vampire exiting
%------------------------------------------------------------------------------