%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC120-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 : n002.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:45 PM UTC 2026
% Result : Unsatisfiable 1.57s 0.76s
% Output : Refutation 1.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 33
% Syntax : Number of formulae : 157 ( 31 unt; 13 def)
% Number of atoms : 410 ( 59 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 416 ( 163 ~; 240 |; 0 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 14 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 56 ( 0 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause50) ).
fof(f59,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause59) ).
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(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(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(f142,axiom,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause131) ).
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(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)
| neq(sk2,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f210,negated_conjecture,
! [X0,X1] :
( ~ ssList(X0)
| sk4 = X0
| ~ ssList(X1)
| tl(sk4) != X1
| app(sk3,X1) != X0
| ~ neq(nil,sk4)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
( ~ neq(sk1,nil)
| ~ segmentP(sk2,sk1)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f213,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f214,plain,
( neq(sk4,nil)
| neq(sk4,nil) ),
inference(definition_unfolding,[],[f206,f204,f204]) ).
fof(f218,plain,
( ~ neq(sk3,nil)
| ~ segmentP(sk4,sk3)
| ~ neq(sk4,nil) ),
inference(definition_unfolding,[],[f211,f205,f204,f205]) ).
fof(f225,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(equality_resolution,[],[f118]) ).
fof(f233,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(f245,plain,
! [X0] :
( ~ ssList(X0)
| sk4 = X0
| ~ ssList(tl(sk4))
| app(sk3,tl(sk4)) != X0
| ~ neq(nil,sk4)
| ~ neq(sk4,nil) ),
inference(equality_resolution,[],[f210]) ).
fof(f246,plain,
( ~ ssList(app(sk3,tl(sk4)))
| sk4 = app(sk3,tl(sk4))
| ~ ssList(tl(sk4))
| ~ neq(nil,sk4)
| ~ neq(sk4,nil) ),
inference(equality_resolution,[],[f245]) ).
fof(f251,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f293,plain,
! [X0,X1] : ~ ssList(skaf46(X0,X1)),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f301,plain,
! [X0] :
( rearsegP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f316,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f317,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f318,plain,
! [X0] :
( ~ ssItem(hd(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f327,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f341,plain,
! [X0,X1] :
( cons(X0,X1) != X1
| ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f342,plain,
! [X0,X1] :
( ~ neq(X1,X0)
| ssList(X1)
| ssList(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f346,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f357,plain,
! [X1] :
( neq(X1,X1)
| ssList(X1)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f225]) ).
fof(f373,plain,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f415,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,[],[f233]) ).
fof(f428,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f429,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f432,plain,
( ~ neq(sk4,nil)
| ~ neq(sk4,nil) ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f436,plain,
( ssList(app(sk3,tl(sk4)))
| sk4 = app(sk3,tl(sk4))
| ssList(tl(sk4))
| neq(nil,sk4)
| neq(sk4,nil) ),
inference(consistent_polarity_flipping,[],[f246]) ).
fof(f437,plain,
( neq(sk3,nil)
| ~ segmentP(sk4,sk3)
| neq(sk4,nil) ),
inference(consistent_polarity_flipping,[],[f218]) ).
fof(f438,plain,
~ neq(sk4,nil),
inference(duplicate_literal_removal,[],[f432]) ).
fof(f443,plain,
! [X1] :
( neq(X1,X1)
| ssList(X1) ),
inference(duplicate_literal_removal,[],[f357]) ).
fof(f446,definition,
( spl0_1
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f447,plain,
( ~ neq(sk4,nil)
| spl0_1 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f450,definition,
( spl0_2
<=> segmentP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f454,definition,
( spl0_3
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f456,plain,
( neq(sk3,nil)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f457,plain,
( spl0_1
| ~ spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f437,f454,f450,f446]) ).
fof(f459,definition,
( spl0_4
<=> neq(nil,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f461,plain,
( neq(nil,sk4)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f463,definition,
( spl0_5
<=> ssList(tl(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f464,plain,
( ~ ssList(tl(sk4))
| spl0_5 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f465,plain,
( ssList(tl(sk4))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f467,definition,
( spl0_6
<=> sk4 = app(sk3,tl(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f469,plain,
( sk4 = app(sk3,tl(sk4))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f471,definition,
( spl0_7
<=> ssList(app(sk3,tl(sk4))) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f473,plain,
( ssList(app(sk3,tl(sk4)))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f474,plain,
( spl0_1
| spl0_4
| spl0_5
| spl0_6
| spl0_7 ),
inference(avatar_split_clause,[],[f436,f471,f467,f463,f459,f446]) ).
fof(f477,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f438,f446]) ).
fof(f483,definition,
( spl0_9
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f484,plain,
( ~ ssList(nil)
| spl0_9 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f519,plain,
~ spl0_9,
inference(avatar_split_clause,[],[f251,f483]) ).
fof(f698,plain,
( ssList(nil)
| ssList(sk4)
| nil = sk4
| ~ spl0_4 ),
inference(resolution,[],[f342,f461]) ).
fof(f701,plain,
( ssList(sk4)
| nil = sk4
| ~ spl0_4
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f698,f484]) ).
fof(f702,plain,
( nil = sk4
| ~ spl0_4
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f701,f429]) ).
fof(f706,plain,
( ~ neq(nil,nil)
| spl0_1
| ~ spl0_4
| spl0_9 ),
inference(superposition,[],[f447,f702]) ).
fof(f713,plain,
( ssList(sk4)
| nil = sk4
| ~ spl0_5 ),
inference(resolution,[],[f465,f317]) ).
fof(f714,plain,
( nil = sk4
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f713,f429]) ).
fof(f717,plain,
( ~ neq(nil,nil)
| spl0_1
| ~ spl0_5 ),
inference(superposition,[],[f447,f714]) ).
fof(f732,plain,
( ssList(nil)
| spl0_1
| ~ spl0_5 ),
inference(resolution,[],[f443,f717]) ).
fof(f734,plain,
( $false
| spl0_1
| ~ spl0_5
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f732,f484]) ).
fof(f735,plain,
( spl0_1
| ~ spl0_5
| spl0_9 ),
inference(avatar_contradiction_clause,[],[f734]) ).
fof(f741,plain,
( tl(sk4) = app(nil,tl(sk4))
| spl0_5 ),
inference(resolution,[],[f464,f316]) ).
fof(f750,plain,
( ssList(nil)
| spl0_1
| ~ spl0_4
| spl0_9 ),
inference(resolution,[],[f706,f443]) ).
fof(f752,plain,
( $false
| spl0_1
| ~ spl0_4
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f750,f484]) ).
fof(f753,plain,
( spl0_1
| ~ spl0_4
| spl0_9 ),
inference(avatar_contradiction_clause,[],[f752]) ).
fof(f924,definition,
( spl0_17
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f925,plain,
( nil != sk4
| spl0_17 ),
inference(avatar_component_clause,[],[f924]) ).
fof(f926,plain,
( nil = sk4
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f924]) ).
fof(f928,definition,
( spl0_18
<=> sk4 = cons(hd(sk4),tl(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f930,plain,
( sk4 = cons(hd(sk4),tl(sk4))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f933,definition,
( spl0_19
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f935,plain,
( nil = sk3
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f1065,plain,
( ssList(sk3)
| ssList(nil)
| nil = sk3
| ~ spl0_3 ),
inference(resolution,[],[f456,f342]) ).
fof(f1066,plain,
( ssList(nil)
| nil = sk3
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1065,f428]) ).
fof(f1076,plain,
( nil = sk3
| ~ spl0_3
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f1066,f484]) ).
fof(f1077,plain,
( spl0_19
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f1076,f483,f454,f933]) ).
fof(f1348,plain,
( ssList(sk3)
| ssList(tl(sk4))
| ~ spl0_7 ),
inference(resolution,[],[f473,f327]) ).
fof(f1349,plain,
( ssList(tl(sk4))
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1348,f428]) ).
fof(f1350,plain,
( $false
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1349,f464]) ).
fof(f1351,plain,
( spl0_5
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f1350]) ).
fof(f1363,plain,
( sk4 = app(nil,tl(sk4))
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f469,f935]) ).
fof(f1365,plain,
( sk4 = tl(sk4)
| spl0_5
| ~ spl0_6
| ~ spl0_19 ),
inference(superposition,[],[f1363,f741]) ).
fof(f1375,plain,
! [X0] :
( ssList(X0)
| ssList(X0)
| app(skaf46(X0,X0),X0) = X0
| ssList(X0) ),
inference(resolution,[],[f373,f301]) ).
fof(f1378,plain,
! [X0] :
( ssList(X0)
| app(skaf46(X0,X0),X0) = X0 ),
inference(duplicate_literal_removal,[],[f1375]) ).
fof(f1436,plain,
( neq(nil,nil)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f456,f935]) ).
fof(f1800,definition,
( spl0_33
<=> sk4 = tl(sk4) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f1802,plain,
( sk4 = tl(sk4)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f1800]) ).
fof(f1808,plain,
( spl0_33
| spl0_5
| ~ spl0_6
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1365,f933,f467,f463,f1800]) ).
fof(f2094,plain,
( sk4 = cons(hd(sk4),sk4)
| ~ spl0_18
| ~ spl0_33 ),
inference(forward_demodulation,[],[f930,f1802]) ).
fof(f2135,plain,
( sk4 != sk4
| ssItem(hd(sk4))
| ssList(sk4)
| ~ spl0_18
| ~ spl0_33 ),
inference(superposition,[],[f341,f2094]) ).
fof(f2154,plain,
( ssItem(hd(sk4))
| ssList(sk4)
| ~ spl0_18
| ~ spl0_33 ),
inference(trivial_inequality_removal,[],[f2135]) ).
fof(f2167,plain,
( ssItem(hd(sk4))
| ~ spl0_18
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2154,f429]) ).
fof(f2169,definition,
( spl0_35
<=> ssItem(hd(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f2171,plain,
( ssItem(hd(sk4))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f2169]) ).
fof(f2212,plain,
( spl0_35
| ~ spl0_18
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f2167,f1800,f928,f2169]) ).
fof(f2237,plain,
( ssList(sk4)
| nil = sk4
| ~ spl0_35 ),
inference(resolution,[],[f2171,f318]) ).
fof(f2238,plain,
( nil = sk4
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2237,f429]) ).
fof(f2239,plain,
( $false
| spl0_17
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2238,f925]) ).
fof(f2240,plain,
( spl0_17
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f2239]) ).
fof(f6791,plain,
( sk4 = cons(hd(sk4),tl(sk4))
| nil = sk4 ),
inference(resolution,[],[f429,f346]) ).
fof(f11638,plain,
sk3 = app(skaf46(sk3,sk3),sk3),
inference(resolution,[],[f1378,f428]) ).
fof(f11649,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(skaf46(sk3,sk3))
| ssList(sk3)
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(superposition,[],[f415,f11638]) ).
fof(f11654,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(skaf46(sk3,sk3))
| ssList(sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f11649,f327]) ).
fof(f11660,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f11654,f293]) ).
fof(f11665,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f11660,f428]) ).
fof(f12398,plain,
( segmentP(sk4,sk3)
| ssList(tl(sk4))
| ~ spl0_6 ),
inference(superposition,[],[f11665,f469]) ).
fof(f12605,plain,
( spl0_17
| spl0_18 ),
inference(avatar_split_clause,[],[f6791,f928,f924]) ).
fof(f12684,plain,
( segmentP(sk4,sk3)
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f12398,f464]) ).
fof(f12769,plain,
( spl0_2
| spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f12684,f467,f463,f450]) ).
fof(f13034,plain,
( ~ neq(nil,nil)
| spl0_1
| ~ spl0_17 ),
inference(superposition,[],[f447,f926]) ).
fof(f13128,plain,
( $false
| spl0_1
| ~ spl0_3
| ~ spl0_17
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f13034,f1436]) ).
fof(f13129,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_17
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f13128]) ).
cnf(s1,plain,
( spl0_1
| ~ spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f457]) ).
cnf(s2,plain,
( spl0_1
| spl0_4
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f474]) ).
cnf(s5,plain,
~ spl0_1,
inference(sat_conversion,[],[f477]) ).
cnf(s15,plain,
~ spl0_9,
inference(sat_conversion,[],[f519]) ).
cnf(s19,plain,
( spl0_1
| ~ spl0_5
| spl0_9 ),
inference(sat_conversion,[],[f735]) ).
cnf(s20,plain,
( spl0_1
| ~ spl0_4
| spl0_9 ),
inference(sat_conversion,[],[f753]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_9
| spl0_19 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s41,plain,
( spl0_5
| ~ spl0_7 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s45,plain,
( spl0_5
| ~ spl0_6
| ~ spl0_19
| spl0_33 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s59,plain,
( ~ spl0_18
| ~ spl0_33
| spl0_35 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s62,plain,
( spl0_17
| ~ spl0_35 ),
inference(sat_conversion,[],[f2240]) ).
cnf(s455,plain,
( spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f12605]) ).
cnf(s507,plain,
( spl0_2
| spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f12769]) ).
cnf(s584,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_17
| ~ spl0_19 ),
inference(sat_conversion,[],[f13129]) ).
cnf(s608,plain,
~ spl0_4,
inference(rat,[],[s20,s15,s5]) ).
cnf(s609,plain,
~ spl0_5,
inference(rat,[],[s19,s15,s5]) ).
cnf(s612,plain,
~ spl0_7,
inference(rat,[],[s41,s609]) ).
cnf(s613,plain,
spl0_6,
inference(rat,[],[s2,s612,s609,s608,s5]) ).
cnf(s619,plain,
spl0_2,
inference(rat,[],[s507,s609,s613]) ).
cnf(s620,plain,
spl0_3,
inference(rat,[],[s1,s619,s5]) ).
cnf(s621,plain,
spl0_19,
inference(rat,[],[s32,s15,s620]) ).
cnf(s625,plain,
spl0_33,
inference(rat,[],[s45,s613,s609,s621]) ).
cnf(s626,plain,
~ spl0_17,
inference(rat,[],[s584,s620,s5,s621]) ).
cnf(s637,plain,
spl0_18,
inference(rat,[],[s455,s626]) ).
cnf(s644,plain,
~ spl0_35,
inference(rat,[],[s62,s626]) ).
cnf(s650,plain,
$false,
inference(rat,[],[s59,s625,s644,s637]) ).
fof(f13138,plain,
$false,
inference(avatar_sat_refutation,[],[s650]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC120-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.12/0.38 % Computer : n002.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 08:02:22 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/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
% 1.57/0.75 % (200300)Will run a generic schedule for satisfiability detection.
% 1.57/0.75 % (200310)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1690463956:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.57/0.75 % (200306)% WARNING: option uhcvi not known.
% 1.57/0.75 % (200305)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3472196897_2999 on theBenchmark for (2999ds/0Mi)
% 1.57/0.75 % (200306)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1470569397:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.57/0.75 % (200307)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1093034525:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.57/0.75 % (200308)dis+10_1_sil=32000:sp=arity:random_seed=3295221767:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.57/0.75 % (200309)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1130191092:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.57/0.75 % (200311)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1000926019:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.57/0.75 % TRYING [1]
% 1.57/0.75 % TRYING [2]
% 1.57/0.75 % TRYING [3]
% 1.57/0.75 % (200310)Instruction limit reached!
% 1.57/0.75 % (200310)------------------------------
% 1.57/0.75 % (200310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.75 % (200310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.75 % (200310)CaDiCaL version: 2.1.3
% 1.57/0.75 % (200310)Termination reason: Instruction limit
% 1.57/0.75 % (200310)Termination phase: Saturation
% 1.57/0.75 % (200310)Time elapsed: 0.038 s
% 1.57/0.75 % (200310)Peak memory usage: 14 MB
% 1.57/0.75 % (200310)Instructions burned: 132 (million)
% 1.57/0.75 % TRYING [4]
% 1.57/0.75 % (200319)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3476500548:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.57/0.75 % TRYING [1]
% 1.57/0.75 % TRYING [2]
% 1.57/0.75 % TRYING [3]
% 1.57/0.75 % (200308)Instruction limit reached!
% 1.57/0.75 % (200308)------------------------------
% 1.57/0.75 % (200308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.75 % (200308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.75 % (200308)CaDiCaL version: 2.1.3
% 1.57/0.75 % (200308)Termination reason: Instruction limit
% 1.57/0.75 % (200308)Termination phase: Saturation
% 1.57/0.75 % (200308)Time elapsed: 0.059 s
% 1.57/0.75 % (200308)Peak memory usage: 13 MB
% 1.57/0.75 % (200308)Instructions burned: 103 (million)
% 1.57/0.75 % (200309)Instruction limit reached!
% 1.57/0.75 % (200309)------------------------------
% 1.57/0.75 % (200309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.75 % (200309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.75 % (200309)CaDiCaL version: 2.1.3
% 1.57/0.75 % (200309)Termination reason: Instruction limit
% 1.57/0.75 % (200309)Termination phase: Saturation
% 1.57/0.75 % (200309)Time elapsed: 0.061 s
% 1.57/0.75 % (200309)Peak memory usage: 13 MB
% 1.57/0.75 % (200309)Instructions burned: 118 (million)
% 1.57/0.75 % TRYING [4]
% 1.57/0.75 % (200321)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=931950419:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.57/0.75 % (200322)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=1482766476:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.57/0.76 % (200311)Instruction limit reached!
% 1.57/0.76 % (200311)------------------------------
% 1.57/0.76 % (200311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.76 % (200311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.76 % (200311)CaDiCaL version: 2.1.3
% 1.57/0.76 % (200311)Termination reason: Instruction limit
% 1.57/0.76 % (200311)Termination phase: Saturation
% 1.57/0.76 % (200311)Time elapsed: 0.090 s
% 1.57/0.76 % (200311)Peak memory usage: 14 MB
% 1.57/0.76 % (200311)Instructions burned: 160 (million)
% 1.57/0.76 % TRYING [5]
% 1.57/0.76 % TRYING [5]
% 1.57/0.76 % (200325)ott-21_1_sil=16000:fs=off:random_seed=2152341381:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.57/0.76 % (200321)Instruction limit reached!
% 1.57/0.76 % (200321)------------------------------
% 1.57/0.76 % (200321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.76 % (200321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.76 % (200321)CaDiCaL version: 2.1.3
% 1.57/0.76 % (200321)Termination reason: Instruction limit
% 1.57/0.76 % (200321)Termination phase: Saturation
% 1.57/0.76 % (200321)Time elapsed: 0.066 s
% 1.57/0.76 % (200321)Peak memory usage: 13 MB
% 1.57/0.76 % (200321)Instructions burned: 131 (million)
% 1.57/0.76 % (200327)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=278876150:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.57/0.76 % TRYING [6]
% 1.57/0.76 % (200319)Instruction limit reached!
% 1.57/0.76 % (200319)------------------------------
% 1.57/0.76 % (200319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.76 % (200319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.76 % (200319)CaDiCaL version: 2.1.3
% 1.57/0.76 % (200319)Termination reason: Instruction limit
% 1.57/0.76 % (200319)Termination phase: Finite model building constraint generation
% 1.57/0.76 % (200319)Time elapsed: 0.150 s
% 1.57/0.76 % (200319)Peak memory usage: 36 MB
% 1.57/0.76 % (200319)Instructions burned: 718 (million)
% 1.57/0.76 % (200325)Instruction limit reached!
% 1.57/0.76 % (200325)------------------------------
% 1.57/0.76 % (200325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.76 % (200325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.76 % (200325)CaDiCaL version: 2.1.3
% 1.57/0.76 % (200325)Termination reason: Instruction limit
% 1.57/0.76 % (200325)Termination phase: Saturation
% 1.57/0.76 % (200325)Time elapsed: 0.091 s
% 1.57/0.76 % (200325)Peak memory usage: 13 MB
% 1.57/0.76 % (200325)Instructions burned: 180 (million)
% 1.57/0.76 % (200329)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=632240866:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.57/0.76 % TRYING [1]
% 1.57/0.76 % TRYING [2]
% 1.57/0.76 % TRYING [3]
% 1.57/0.76 % (200331)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2822045610:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.57/0.76 % TRYING [4]
% 1.57/0.76 % TRYING [6]
% 1.57/0.76 % (200306) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-200300-200306"...
% 1.57/0.76 % (200306)...printing done.
% 1.57/0.76 % (200306)Refutation found. Thanks to Tanya!
% 1.57/0.76 % SZS status Unsatisfiable for theBenchmark
% 1.57/0.76 % SZS output start Proof for theBenchmark
% See solution above
% 1.57/0.76 % (200306)------------------------------
% 1.57/0.76 % (200306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.57/0.76 % (200306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.57/0.76 % (200306)CaDiCaL version: 2.1.3
% 1.57/0.76 % (200306)Termination reason: Refutation
% 1.57/0.76 % (200306)Time elapsed: 0.280 s
% 1.57/0.76 % (200306)Peak memory usage: 17 MB
% 1.57/0.76 % (200306)Instructions burned: 498 (million)
% 1.57/0.76 % (200300)Success in time 0.333 s
% 1.57/0.76 % Vampire exiting
%------------------------------------------------------------------------------