%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC073-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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:04:33 PM UTC 2026
% Result : Unsatisfiable 21.11s 3.49s
% Output : Refutation 21.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 40
% Syntax : Number of formulae : 184 ( 25 unt; 15 def)
% Number of atoms : 628 ( 69 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 867 ( 423 ~; 429 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 16 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 86 ( 0 sgn 86 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f11,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause11) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).
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(tl(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f76,axiom,
! [X0] :
( ssItem(hd(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause76) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
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] :
( neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
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(f118,axiom,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause115) ).
fof(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause116) ).
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(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(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(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_4) ).
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,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,nil)
| ~ segmentP(sk2,X0)
| ~ segmentP(sk1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
( nil = sk3
| nil != sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
( nil != sk2
| nil != sk1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
( ~ neq(sk4,nil)
| neq(sk3,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ neq(sk4,nil)
| ~ ssList(X0)
| sk4 = X0
| ~ ssList(X1)
| ~ ssList(X2)
| tl(sk3) != X1
| app(X1,X2) != X0
| ~ ssItem(X3)
| cons(X3,nil) != X2
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f213,plain,
! [X0] :
( ~ neq(X0,nil)
| ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0) ),
inference(definition_unfolding,[],[f206,f204,f205]) ).
fof(f214,plain,
( nil != sk4
| nil != sk3 ),
inference(definition_unfolding,[],[f208,f204,f205]) ).
fof(f221,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(equality_resolution,[],[f118]) ).
fof(f222,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(equality_resolution,[],[f119]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ ssList(app(app(X0,X1),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| segmentP(app(app(X0,X1),X2),X1) ),
inference(equality_resolution,[],[f187]) ).
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(f239,plain,
! [X2,X3,X0] :
( ~ neq(sk4,nil)
| ~ ssList(X0)
| sk4 = X0
| ~ ssList(tl(sk3))
| ~ ssList(X2)
| app(tl(sk3),X2) != X0
| ~ ssItem(X3)
| cons(X3,nil) != X2
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f210]) ).
fof(f240,plain,
! [X2,X3] :
( ~ neq(sk4,nil)
| ~ ssList(app(tl(sk3),X2))
| sk4 = app(tl(sk3),X2)
| ~ ssList(tl(sk3))
| ~ ssList(X2)
| ~ ssItem(X3)
| cons(X3,nil) != X2
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f239]) ).
fof(f241,plain,
! [X3] :
( ~ neq(sk4,nil)
| ~ ssList(app(tl(sk3),cons(X3,nil)))
| sk4 = app(tl(sk3),cons(X3,nil))
| ~ ssList(tl(sk3))
| ~ ssList(cons(X3,nil))
| ~ ssItem(X3)
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f240]) ).
fof(f242,plain,
( ~ neq(sk4,nil)
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil)))
| sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f241]) ).
fof(f248,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ duplicatefreeP(X0)
| ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f269,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(f273,plain,
( ~ neq(sk4,nil)
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil)))
| sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3) ),
inference(duplicate_literal_removal,[],[f242]) ).
fof(f278,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1) ),
inference(duplicate_literal_removal,[],[f221]) ).
fof(f281,definition,
( spl0_1
<=> neq(nil,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f283,plain,
( ~ neq(nil,sk3)
| spl0_1 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f285,definition,
( spl0_2
<=> ssItem(hd(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f286,plain,
( ssItem(hd(sk3))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f287,plain,
( ~ ssItem(hd(sk3))
| spl0_2 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f289,definition,
( spl0_3
<=> ssList(cons(hd(sk3),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f290,plain,
( ssList(cons(hd(sk3),nil))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f291,plain,
( ~ ssList(cons(hd(sk3),nil))
| spl0_3 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl0_4
<=> ssList(tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f294,plain,
( ssList(tl(sk3))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f295,plain,
( ~ ssList(tl(sk3))
| spl0_4 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl0_5
<=> sk4 = app(tl(sk3),cons(hd(sk3),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f299,plain,
( sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f301,definition,
( spl0_6
<=> ssList(app(tl(sk3),cons(hd(sk3),nil))) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f303,plain,
( ~ ssList(app(tl(sk3),cons(hd(sk3),nil)))
| spl0_6 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f305,definition,
( spl0_7
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f307,plain,
( ~ neq(sk4,nil)
| spl0_7 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f308,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f273,f305,f301,f297,f293,f289,f285,f281]) ).
fof(f310,definition,
( spl0_8
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f312,plain,
( neq(sk3,nil)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f313,plain,
( spl0_8
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f209,f305,f310]) ).
fof(f315,definition,
( spl0_9
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f316,plain,
( nil = sk3
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f317,plain,
( nil != sk3
| spl0_9 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f319,definition,
( spl0_10
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f321,plain,
( nil != sk4
| spl0_10 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f322,plain,
( ~ spl0_9
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f214,f319,f315]) ).
fof(f323,plain,
( ~ spl0_10
| spl0_9 ),
inference(avatar_split_clause,[],[f207,f315,f319]) ).
fof(f329,definition,
( spl0_12
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f330,plain,
( ssList(nil)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f357,definition,
( spl0_18
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f358,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f360,definition,
( spl0_19
<=> ! [X0] :
( ~ ssList(X0)
| ~ duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f361,plain,
( ! [X0] :
( ~ duplicatefreeP(X0)
| ~ ssList(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f248,f360,f357]) ).
fof(f365,plain,
spl0_12,
inference(avatar_split_clause,[],[f8,f329]) ).
fof(f407,plain,
sk4 = app(sk4,nil),
inference(resolution,[],[f73,f203]) ).
fof(f464,plain,
( ! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1) )
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f86,f358]) ).
fof(f546,plain,
( ~ ssList(sk4)
| ~ ssList(nil)
| nil = sk4
| spl0_7 ),
inference(resolution,[],[f102,f307]) ).
fof(f547,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| nil = X0
| ~ ssList(X0)
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0) ),
inference(resolution,[],[f102,f213]) ).
fof(f550,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| nil = X0
| ~ segmentP(sk4,X0)
| ~ segmentP(sk3,X0) ),
inference(duplicate_literal_removal,[],[f547]) ).
fof(f551,plain,
( ! [X0] :
( ~ segmentP(sk4,X0)
| nil = X0
| ~ ssList(X0)
| ~ segmentP(sk3,X0) )
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f550,f330]) ).
fof(f552,plain,
( ~ ssList(nil)
| nil = sk4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f546,f203]) ).
fof(f553,plain,
( nil = sk4
| spl0_7
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f552,f330]) ).
fof(f554,plain,
( $false
| spl0_7
| spl0_10
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f553,f321]) ).
fof(f555,plain,
( spl0_7
| spl0_10
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f554]) ).
fof(f556,plain,
( ~ ssList(nil)
| ~ ssList(sk3)
| nil = sk3
| spl0_1 ),
inference(resolution,[],[f283,f102]) ).
fof(f557,plain,
( ~ ssList(sk3)
| nil = sk3
| spl0_1
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f556,f330]) ).
fof(f558,plain,
( nil = sk3
| spl0_1
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f557,f202]) ).
fof(f559,plain,
( spl0_9
| spl0_1
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f558,f329,f281,f315]) ).
fof(f584,plain,
( neq(nil,nil)
| ~ spl0_8
| ~ spl0_9 ),
inference(superposition,[],[f312,f316]) ).
fof(f594,plain,
( ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| spl0_6 ),
inference(resolution,[],[f303,f85]) ).
fof(f595,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_6 ),
inference(avatar_split_clause,[],[f594,f301,f293,f289]) ).
fof(f606,plain,
( ~ ssList(nil)
| ~ ssItem(hd(sk3))
| spl0_3 ),
inference(resolution,[],[f86,f291]) ).
fof(f609,plain,
( ~ ssItem(hd(sk3))
| spl0_3
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f606,f330]) ).
fof(f610,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f609,f329,f289,f285]) ).
fof(f611,plain,
( ~ ssList(sk3)
| nil = sk3
| spl0_2 ),
inference(resolution,[],[f287,f76]) ).
fof(f612,plain,
( nil = sk3
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f611,f202]) ).
fof(f615,plain,
( spl0_9
| spl0_2 ),
inference(avatar_split_clause,[],[f612,f285,f315]) ).
fof(f646,plain,
( ~ ssList(nil)
| ~ spl0_8
| ~ spl0_9 ),
inference(resolution,[],[f584,f278]) ).
fof(f648,plain,
( $false
| ~ spl0_8
| ~ spl0_9
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f646,f330]) ).
fof(f649,plain,
( ~ spl0_8
| ~ spl0_9
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f648]) ).
fof(f654,plain,
( ~ ssList(sk3)
| nil = sk3
| spl0_4 ),
inference(resolution,[],[f295,f75]) ).
fof(f655,plain,
( nil = sk3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f654,f202]) ).
fof(f656,plain,
( spl0_9
| spl0_4 ),
inference(avatar_split_clause,[],[f655,f293,f315]) ).
fof(f659,plain,
( cons(hd(sk3),nil) = app(nil,cons(hd(sk3),nil))
| ~ spl0_3 ),
inference(resolution,[],[f290,f74]) ).
fof(f813,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f107,f202]) ).
fof(f816,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f813,f317]) ).
fof(f839,definition,
( spl0_28
<=> nil = cons(hd(sk3),nil) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f840,plain,
( nil != cons(hd(sk3),nil)
| spl0_28 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f841,plain,
( nil = cons(hd(sk3),nil)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f860,plain,
( singletonP(nil)
| ~ ssList(nil)
| ~ ssItem(hd(sk3))
| ~ spl0_28 ),
inference(superposition,[],[f222,f841]) ).
fof(f874,plain,
( ~ ssList(nil)
| ~ ssItem(hd(sk3))
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f860,f11]) ).
fof(f882,plain,
( ~ ssItem(hd(sk3))
| ~ spl0_12
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f874,f330]) ).
fof(f886,plain,
( $false
| ~ spl0_2
| ~ spl0_12
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f882,f286]) ).
fof(f887,plain,
( ~ spl0_2
| ~ spl0_12
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f886]) ).
fof(f1881,plain,
( ! [X0] :
( ~ ssList(app(sk4,X0))
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(X0)
| segmentP(app(sk4,X0),cons(hd(sk3),nil)) )
| ~ spl0_5 ),
inference(superposition,[],[f229,f299]) ).
fof(f1890,plain,
( ! [X0] :
( ~ ssList(app(sk4,X0))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(X0)
| segmentP(app(sk4,X0),cons(hd(sk3),nil)) )
| ~ spl0_4
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1881,f294]) ).
fof(f1895,plain,
( ! [X0] :
( segmentP(app(sk4,X0),cons(hd(sk3),nil))
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) )
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1890,f290]) ).
fof(f1942,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3) )
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f269,f361]) ).
fof(f1954,plain,
( ! [X0] :
( ~ ssList(app(sk4,cons(hd(sk3),X0)))
| ~ ssList(nil)
| ~ ssList(tl(sk3))
| ~ ssItem(hd(sk3))
| ~ ssList(X0) )
| ~ spl0_5
| ~ spl0_19 ),
inference(superposition,[],[f1942,f299]) ).
fof(f1957,plain,
( ! [X0] :
( ~ ssList(app(sk4,cons(hd(sk3),X0)))
| ~ ssList(tl(sk3))
| ~ ssItem(hd(sk3))
| ~ ssList(X0) )
| ~ spl0_5
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1954,f330]) ).
fof(f1961,plain,
( ! [X0] :
( ~ ssList(app(sk4,cons(hd(sk3),X0)))
| ~ ssItem(hd(sk3))
| ~ ssList(X0) )
| ~ spl0_4
| ~ spl0_5
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1957,f294]) ).
fof(f1970,plain,
( ! [X0] :
( ~ ssList(app(sk4,cons(hd(sk3),X0)))
| ~ ssList(X0) )
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1961,f286]) ).
fof(f1986,plain,
( ! [X0,X1] :
( ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) )
| ~ spl0_18 ),
inference(backward_subsumption_resolution,[],[f126,f358]) ).
fof(f2362,plain,
( ! [X0] : cons(X0,tl(sk3)) = app(cons(X0,nil),tl(sk3))
| ~ spl0_4
| ~ spl0_18 ),
inference(resolution,[],[f1986,f294]) ).
fof(f2535,definition,
( spl0_64
<=> ssList(app(sk4,sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f2536,plain,
( ssList(app(sk4,sk3))
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f2535]) ).
fof(f2537,plain,
( ~ ssList(app(sk4,sk3))
| spl0_64 ),
inference(avatar_component_clause,[],[f2535]) ).
fof(f2548,plain,
( ~ ssList(sk4)
| ~ ssList(sk3)
| spl0_64 ),
inference(resolution,[],[f2537,f85]) ).
fof(f2549,plain,
( ~ ssList(sk3)
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f2548,f203]) ).
fof(f2550,plain,
( $false
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f2549,f202]) ).
fof(f2551,plain,
spl0_64,
inference(avatar_contradiction_clause,[],[f2550]) ).
fof(f3640,plain,
( ~ ssList(app(sk4,sk3))
| ~ ssList(tl(sk3))
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_19 ),
inference(superposition,[],[f1970,f816]) ).
fof(f3641,plain,
( ~ ssList(tl(sk3))
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_19
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f3640,f2536]) ).
fof(f3643,plain,
( $false
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_19
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f3641,f294]) ).
fof(f3644,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_19
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f3643]) ).
fof(f4965,plain,
( ! [X0] :
( ~ ssList(app(cons(hd(sk3),nil),X0))
| ~ ssList(nil)
| ~ ssList(cons(hd(sk3),nil))
| ~ ssList(X0)
| segmentP(app(cons(hd(sk3),nil),X0),cons(hd(sk3),nil)) )
| ~ spl0_3 ),
inference(superposition,[],[f229,f659]) ).
fof(f4973,plain,
( ! [X0] :
( ~ ssList(app(cons(hd(sk3),nil),X0))
| ~ ssList(nil)
| ~ ssList(X0)
| segmentP(app(cons(hd(sk3),nil),X0),cons(hd(sk3),nil)) )
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4965,f464]) ).
fof(f4981,plain,
( ! [X0] :
( ~ ssList(app(cons(hd(sk3),nil),X0))
| ~ ssList(X0)
| segmentP(app(cons(hd(sk3),nil),X0),cons(hd(sk3),nil)) )
| ~ spl0_3
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4973,f330]) ).
fof(f5484,plain,
( segmentP(sk4,cons(hd(sk3),nil))
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5 ),
inference(superposition,[],[f1895,f407]) ).
fof(f5489,plain,
( segmentP(sk4,cons(hd(sk3),nil))
| ~ ssList(sk4)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f5484,f330]) ).
fof(f5494,plain,
( segmentP(sk4,cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f5489,f203]) ).
fof(f7698,plain,
( nil = cons(hd(sk3),nil)
| ~ ssList(cons(hd(sk3),nil))
| ~ segmentP(sk3,cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_12 ),
inference(resolution,[],[f5494,f551]) ).
fof(f7707,plain,
( ~ ssList(cons(hd(sk3),nil))
| ~ segmentP(sk3,cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_12
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f7698,f840]) ).
fof(f7712,plain,
( ~ segmentP(sk3,cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_12
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f7707,f290]) ).
fof(f121306,plain,
( ~ ssList(cons(hd(sk3),tl(sk3)))
| ~ ssList(tl(sk3))
| segmentP(cons(hd(sk3),tl(sk3)),cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| ~ spl0_12
| ~ spl0_18 ),
inference(superposition,[],[f4981,f2362]) ).
fof(f121314,plain,
( ~ ssList(tl(sk3))
| segmentP(cons(hd(sk3),tl(sk3)),cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f121306,f464]) ).
fof(f121353,plain,
( segmentP(cons(hd(sk3),tl(sk3)),cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f121314,f294]) ).
fof(f121387,plain,
( segmentP(sk3,cons(hd(sk3),nil))
| ~ spl0_3
| ~ spl0_4
| spl0_9
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f121353,f816]) ).
fof(f121388,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_18
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f121387,f7712]) ).
fof(f121389,plain,
( ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_18
| spl0_28 ),
inference(avatar_contradiction_clause,[],[f121388]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f308]) ).
cnf(s2,plain,
( ~ spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f313]) ).
cnf(s3,plain,
( ~ spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f322]) ).
cnf(s4,plain,
( spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f323]) ).
cnf(s11,plain,
( spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f362]) ).
cnf(s14,plain,
spl0_12,
inference(sat_conversion,[],[f365]) ).
cnf(s15,plain,
( spl0_7
| spl0_10
| ~ spl0_12 ),
inference(sat_conversion,[],[f555]) ).
cnf(s16,plain,
( spl0_1
| spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f559]) ).
cnf(s21,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_6 ),
inference(sat_conversion,[],[f595]) ).
cnf(s23,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_12 ),
inference(sat_conversion,[],[f610]) ).
cnf(s25,plain,
( spl0_2
| spl0_9 ),
inference(sat_conversion,[],[f615]) ).
cnf(s26,plain,
( ~ spl0_8
| ~ spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f649]) ).
cnf(s27,plain,
( spl0_4
| spl0_9 ),
inference(sat_conversion,[],[f656]) ).
cnf(s34,plain,
( ~ spl0_2
| ~ spl0_12
| ~ spl0_28 ),
inference(sat_conversion,[],[f887]) ).
cnf(s80,plain,
spl0_64,
inference(sat_conversion,[],[f2551]) ).
cnf(s108,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_19
| ~ spl0_64 ),
inference(sat_conversion,[],[f3644]) ).
cnf(s4718,plain,
( ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| spl0_9
| ~ spl0_12
| ~ spl0_18
| spl0_28 ),
inference(sat_conversion,[],[f121389]) ).
cnf(s4766,plain,
~ spl0_9,
inference(rat,[],[s15,s2,s3,s26,s14]) ).
cnf(s4776,plain,
spl0_4,
inference(rat,[],[s27,s4766]) ).
cnf(s4777,plain,
spl0_2,
inference(rat,[],[s25,s4766]) ).
cnf(s4778,plain,
spl0_1,
inference(rat,[],[s16,s14,s4766]) ).
cnf(s4779,plain,
~ spl0_10,
inference(rat,[],[s4,s4766]) ).
cnf(s4821,plain,
~ spl0_28,
inference(rat,[],[s34,s14,s4777]) ).
cnf(s4822,plain,
spl0_3,
inference(rat,[],[s23,s14,s4777]) ).
cnf(s4833,plain,
spl0_7,
inference(rat,[],[s15,s14,s4779]) ).
cnf(s4857,plain,
spl0_6,
inference(rat,[],[s21,s4776,s4822]) ).
cnf(s4885,plain,
spl0_5,
inference(rat,[],[s1,s4776,s4857,s4822,s4777,s4778,s4833]) ).
cnf(s4912,plain,
~ spl0_19,
inference(rat,[],[s108,s80,s4766,s14,s4776,s4777,s4885]) ).
cnf(s4914,plain,
~ spl0_18,
inference(rat,[],[s4718,s4821,s4766,s14,s4776,s4822,s4885]) ).
cnf(s4916,plain,
$false,
inference(rat,[],[s11,s4912,s4914]) ).
fof(f121390,plain,
$false,
inference(avatar_sat_refutation,[],[s4916]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC073-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.37 % Computer : n006.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 07:43:26 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 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
% 14.73/2.56 % (3805742)Will run a generic schedule for satisfiability detection.
% 14.73/2.56 % (3805747)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4154722939_2999 on theBenchmark for (2999ds/0Mi)
% 14.73/2.56 % (3805748)% WARNING: option uhcvi not known.
% 14.73/2.56 % TRYING [1]
% 14.73/2.56 % (3805751)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1379656973:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.73/2.56 % (3805748)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1511251967:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.73/2.56 % (3805749)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=317505746:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.73/2.56 % TRYING [2]
% 14.73/2.56 % (3805750)dis+10_1_sil=32000:sp=arity:random_seed=2322809072:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.73/2.56 % (3805753)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2623491816:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.73/2.56 % (3805752)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2101797558:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.73/2.56 % TRYING [3]
% 14.73/2.56 % TRYING [4]
% 14.73/2.56 % TRYING [5]
% 14.73/2.56 % (3805750)Instruction limit reached!
% 14.73/2.56 % (3805750)------------------------------
% 14.73/2.56 % (3805750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.56 % (3805750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.56 % (3805750)CaDiCaL version: 2.1.3
% 14.73/2.56 % (3805750)Termination reason: Instruction limit
% 14.73/2.56 % (3805750)Termination phase: Saturation
% 14.73/2.56 % (3805750)Time elapsed: 0.060 s
% 14.73/2.56 % (3805750)Peak memory usage: 13 MB
% 14.73/2.56 % (3805750)Instructions burned: 104 (million)
% 14.73/2.56 % (3805751)Instruction limit reached!
% 14.73/2.56 % (3805751)------------------------------
% 14.73/2.56 % (3805751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.56 % (3805751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.56 % (3805751)CaDiCaL version: 2.1.3
% 14.73/2.56 % (3805751)Termination reason: Instruction limit
% 14.73/2.56 % (3805751)Termination phase: Saturation
% 14.73/2.56 % (3805751)Time elapsed: 0.061 s
% 14.73/2.56 % (3805751)Peak memory usage: 13 MB
% 14.73/2.56 % (3805751)Instructions burned: 116 (million)
% 14.73/2.56 % (3805752)Instruction limit reached!
% 14.73/2.56 % (3805752)------------------------------
% 14.73/2.56 % (3805752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.56 % (3805752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.56 % (3805752)CaDiCaL version: 2.1.3
% 14.73/2.56 % (3805752)Termination reason: Instruction limit
% 14.73/2.56 % (3805752)Termination phase: Saturation
% 14.73/2.56 % (3805752)Time elapsed: 0.067 s
% 14.73/2.56 % (3805752)Peak memory usage: 14 MB
% 14.73/2.56 % (3805752)Instructions burned: 131 (million)
% 14.73/2.56 % (3805762)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2601028584:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.73/2.56 % (3805761)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3650239449:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.73/2.56 % (3805763)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=323249588:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.73/2.56 % TRYING [1]
% 14.73/2.56 % TRYING [2]
% 14.73/2.56 % (3805753)Instruction limit reached!
% 14.73/2.56 % (3805753)------------------------------
% 14.73/2.56 % (3805753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.56 % (3805753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.56 % (3805753)CaDiCaL version: 2.1.3
% 14.73/2.56 % (3805753)Termination reason: Instruction limit
% 14.73/2.56 % (3805753)Termination phase: Saturation
% 14.73/2.56 % (3805753)Time elapsed: 0.094 s
% 14.73/2.56 % (3805753)Peak memory usage: 14 MB
% 14.73/2.56 % (3805753)Instructions burned: 160 (million)
% 14.73/2.56 % TRYING [3]
% 14.73/2.56 % (3805767)ott-21_1_sil=16000:fs=off:random_seed=1913195208:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.73/2.56 % TRYING [4]
% 14.73/2.56 % TRYING [6]
% 14.73/2.56 % (3805762)Instruction limit reached!
% 14.73/2.56 % (3805762)------------------------------
% 14.73/2.56 % (3805762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805762)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805762)Termination reason: Instruction limit
% 21.11/3.49 % (3805762)Termination phase: Saturation
% 21.11/3.49 % (3805762)Time elapsed: 0.073 s
% 21.11/3.49 % (3805762)Peak memory usage: 14 MB
% 21.11/3.49 % (3805762)Instructions burned: 131 (million)
% 21.11/3.49 % (3805769)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1944154624:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 21.11/3.49 % TRYING [5]
% 21.11/3.49 % (3805767)Instruction limit reached!
% 21.11/3.49 % (3805767)------------------------------
% 21.11/3.49 % (3805767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805767)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805767)Termination reason: Instruction limit
% 21.11/3.49 % (3805767)Termination phase: Saturation
% 21.11/3.49 % (3805767)Time elapsed: 0.090 s
% 21.11/3.49 % (3805767)Peak memory usage: 13 MB
% 21.11/3.49 % (3805767)Instructions burned: 180 (million)
% 21.11/3.49 % (3805771)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=930706255:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 21.11/3.49 % TRYING [1]
% 21.11/3.49 % TRYING [2]
% 21.11/3.49 % TRYING [3]
% 21.11/3.49 % TRYING [4]
% 21.11/3.49 % TRYING [6]
% 21.11/3.49 % (3805761)Instruction limit reached!
% 21.11/3.49 % (3805761)------------------------------
% 21.11/3.49 % (3805761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805761)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805761)Termination reason: Instruction limit
% 21.11/3.49 % (3805761)Termination phase: Finite model building constraint generation
% 21.11/3.49 % (3805761)Time elapsed: 0.285 s
% 21.11/3.49 % (3805761)Peak memory usage: 36 MB
% 21.11/3.49 % (3805761)Instructions burned: 714 (million)
% 21.11/3.49 % (3805773)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2052815259:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 21.11/3.49 % TRYING [5]
% 21.11/3.49 % TRYING [7]
% 21.11/3.49 % (3805769)Instruction limit reached!
% 21.11/3.49 % (3805769)------------------------------
% 21.11/3.49 % (3805769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805769)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805769)Termination reason: Instruction limit
% 21.11/3.49 % (3805769)Termination phase: Saturation
% 21.11/3.49 % (3805769)Time elapsed: 0.307 s
% 21.11/3.49 % (3805769)Peak memory usage: 14 MB
% 21.11/3.49 % (3805769)Instructions burned: 478 (million)
% 21.11/3.49 % (3805775)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2763508260:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 21.11/3.49 % (3805763)Instruction limit reached!
% 21.11/3.49 % (3805763)------------------------------
% 21.11/3.49 % (3805763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805763)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805763)Termination reason: Instruction limit
% 21.11/3.49 % (3805763)Termination phase: Saturation
% 21.11/3.49 % (3805763)Time elapsed: 0.436 s
% 21.11/3.49 % (3805763)Peak memory usage: 19 MB
% 21.11/3.49 % (3805763)Instructions burned: 684 (million)
% 21.11/3.49 % (3805777)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=2006459092: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)
% 21.11/3.49 % (3805771)Instruction limit reached!
% 21.11/3.49 % (3805771)------------------------------
% 21.11/3.49 % (3805771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805771)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805771)Termination reason: Instruction limit
% 21.11/3.49 % (3805771)Termination phase: Finite model building SAT solving
% 21.11/3.49 % (3805771)Time elapsed: 0.348 s
% 21.11/3.49 % (3805771)Peak memory usage: 23 MB
% 21.11/3.49 % (3805771)Instructions burned: 866 (million)
% 21.11/3.49 % (3805779)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2609993381:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 21.11/3.49 % TRYING [14]
% 21.11/3.49 % (3805775)Instruction limit reached!
% 21.11/3.49 % (3805775)------------------------------
% 21.11/3.49 % (3805775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805775)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805775)Termination reason: Instruction limit
% 21.11/3.49 % (3805775)Termination phase: Finite model building constraint generation
% 21.11/3.49 % (3805775)Time elapsed: 0.326 s
% 21.11/3.49 % (3805775)Peak memory usage: 72 MB
% 21.11/3.49 % (3805775)Instructions burned: 891 (million)
% 21.11/3.49 % (3805781)fmb+10_1_sil=64000:random_seed=817754291:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 21.11/3.49 % TRYING [1]
% 21.11/3.49 % TRYING [2]
% 21.11/3.49 % TRYING [3]
% 21.11/3.49 % (3805777)Instruction limit reached!
% 21.11/3.49 % (3805777)------------------------------
% 21.11/3.49 % (3805777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805777)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805777)Termination reason: Instruction limit
% 21.11/3.49 % (3805777)Termination phase: Saturation
% 21.11/3.49 % (3805777)Time elapsed: 0.387 s
% 21.11/3.49 % (3805777)Peak memory usage: 19 MB
% 21.11/3.49 % (3805777)Instructions burned: 693 (million)
% 21.11/3.49 % TRYING [4]
% 21.11/3.49 % (3805783)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1422473361:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 21.11/3.49 % TRYING [20]
% 21.11/3.49 % (3805779)Instruction limit reached!
% 21.11/3.49 % (3805779)------------------------------
% 21.11/3.49 % (3805779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805779)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805779)Termination reason: Instruction limit
% 21.11/3.49 % (3805779)Termination phase: Saturation
% 21.11/3.49 % (3805779)Time elapsed: 0.469 s
% 21.11/3.49 % (3805779)Peak memory usage: 21 MB
% 21.11/3.49 % (3805779)Instructions burned: 879 (million)
% 21.11/3.49 % (3805773)Instruction limit reached!
% 21.11/3.49 % (3805773)------------------------------
% 21.11/3.49 % (3805773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805773)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805773)Termination reason: Instruction limit
% 21.11/3.49 % (3805773)Termination phase: Saturation
% 21.11/3.49 % (3805773)Time elapsed: 0.684 s
% 21.11/3.49 % (3805773)Peak memory usage: 28 MB
% 21.11/3.49 % (3805773)Instructions burned: 1180 (million)
% 21.11/3.49 % TRYING [8]
% 21.11/3.49 % (3805785)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=317911636:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 21.11/3.49 % TRYING [5]
% 21.11/3.49 % (3805786)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2502576925:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 21.11/3.49 % TRYING [8]
% 21.11/3.49 % (3805785)Instruction limit reached!
% 21.11/3.49 % (3805785)------------------------------
% 21.11/3.49 % (3805785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805785)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805785)Termination reason: Instruction limit
% 21.11/3.49 % (3805785)Termination phase: Finite model building constraint generation
% 21.11/3.49 % (3805785)Time elapsed: 0.331 s
% 21.11/3.49 % (3805785)Peak memory usage: 79 MB
% 21.11/3.49 % (3805785)Instructions burned: 922 (million)
% 21.11/3.49 % (3805789)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2320026361:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 21.11/3.49 % TRYING [6]
% 21.11/3.49 % (3805789)Instruction limit reached!
% 21.11/3.49 % (3805789)------------------------------
% 21.11/3.49 % (3805789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.49 % (3805789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.49 % (3805789)CaDiCaL version: 2.1.3
% 21.11/3.49 % (3805789)Termination reason: Instruction limit
% 21.11/3.49 % (3805789)Termination phase: Saturation
% 21.11/3.49 % (3805789)Time elapsed: 0.642 s
% 21.11/3.49 % (3805789)Peak memory usage: 15 MB
% 21.11/3.49 % (3805789)Instructions burned: 1472 (million)
% 21.11/3.49 % (3805791)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2343013416:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 21.11/3.49 % TRYING [77]
% 21.11/3.49 % TRYING [9]
% 21.11/3.49 % TRYING [7]
% 21.11/3.49 % (3805748) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3805742-3805748"...
% 21.11/3.49 % (3805748)...printing done.
% 21.11/3.49 % (3805748)Refutation found. Thanks to Tanya!
% 21.11/3.49 % SZS status Unsatisfiable for theBenchmark
% 21.11/3.49 % SZS output start Proof for theBenchmark
% See solution above
% 21.11/3.50 % (3805748)------------------------------
% 21.11/3.50 % (3805748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.11/3.50 % (3805748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.11/3.50 % (3805748)CaDiCaL version: 2.1.3
% 21.11/3.50 % (3805748)Termination reason: Refutation
% 21.11/3.50 % (3805748)Time elapsed: 2.982 s
% 21.11/3.50 % (3805748)Peak memory usage: 65 MB
% 21.11/3.50 % (3805748)Instructions burned: 5239 (million)
% 21.11/3.50 % (3805742)Success in time 3.076 s
% 21.11/3.50 % Vampire exiting
%------------------------------------------------------------------------------