%------------------------------------------------------------------------------
% 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 : n018.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 : Theorem 8.51s 4.17s
% Output : Refutation 8.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 31
% Syntax : Number of formulae : 226 ( 33 unt; 15 def)
% Number of atoms : 789 ( 139 equ)
% Maximal formula atoms : 27 ( 3 avg)
% Number of connectives : 869 ( 306 ~; 451 |; 58 &)
% ( 21 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 16 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 172 ( 0 sgn 148 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0] :
( ssList(X0)
=> ( singletonP(X0)
<=> ? [X1] :
( ssItem(X1)
& cons(X1,nil) = X0 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax4) ).
fof(f7,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( segmentP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& app(app(X2,X1),X3) = X0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax7) ).
fof(f15,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( neq(X0,X1)
<=> X0 != X1 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax15) ).
fof(f16,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ssList(cons(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax16) ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax17) ).
fof(f22,axiom,
! [X0] :
( ssList(X0)
=> ( nil != X0
=> ssItem(hd(X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax22) ).
fof(f24,axiom,
! [X0] :
( ssList(X0)
=> ( nil != X0
=> ssList(tl(X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax24) ).
fof(f26,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ssList(app(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax26) ).
fof(f28,axiom,
! [X0] :
( ssList(X0)
=> app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax28) ).
fof(f39,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax39) ).
fof(f55,axiom,
! [X0] :
( ssList(X0)
=> segmentP(X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax55) ).
fof(f56,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( segmentP(X0,X1)
=> segmentP(app(app(X2,X0),X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax56) ).
fof(f78,axiom,
! [X0] :
( ssList(X0)
=> ( nil != X0
=> cons(hd(X0),tl(X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax78) ).
fof(f81,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> cons(X1,X0) = app(cons(X1,nil),X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax81) ).
fof(f84,axiom,
! [X0] :
( ssList(X0)
=> app(X0,nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax84) ).
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( X1 != X3
| X0 != X2
| ? [X4] :
( ssList(X4)
& neq(X4,nil)
& segmentP(X1,X4)
& segmentP(X0,X4) )
| ( nil != X2
& nil = X3 )
| ( nil = X1
& nil = X0 )
| ( neq(X3,nil)
& ( ~ neq(X2,nil)
| ? [X5] :
( ssList(X5)
& X3 != X5
& ? [X6] :
( ssList(X6)
& ? [X7] :
( ssList(X7)
& tl(X2) = X6
& app(X6,X7) = X5
& ? [X8] :
( ssItem(X8)
& cons(X8,nil) = X7
& hd(X2) = X8
& neq(nil,X2) )
& neq(nil,X2) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f97,negated_conjecture,
~ ! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( X1 != X3
| X0 != X2
| ? [X4] :
( ssList(X4)
& neq(X4,nil)
& segmentP(X1,X4)
& segmentP(X0,X4) )
| ( nil != X2
& nil = X3 )
| ( nil = X1
& nil = X0 )
| ( neq(X3,nil)
& ( ~ neq(X2,nil)
| ? [X5] :
( ssList(X5)
& X3 != X5
& ? [X6] :
( ssList(X6)
& ? [X7] :
( ssList(X7)
& tl(X2) = X6
& app(X6,X7) = X5
& ? [X8] :
( ssItem(X8)
& cons(X8,nil) = X7
& hd(X2) = X8
& neq(nil,X2) )
& neq(nil,X2) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f100,plain,
! [X0] :
( ( singletonP(X0)
<=> ? [X1] :
( ssItem(X1)
& cons(X1,nil) = X0 ) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f103,plain,
! [X0] :
( ! [X1] :
( ( segmentP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& app(app(X2,X1),X3) = X0 ) ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f118,plain,
! [X0] :
( ! [X1] :
( ( neq(X0,X1)
<=> X0 != X1 )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f119,plain,
! [X0] :
( ! [X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f126,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f127,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ~ ssList(X0) ),
inference(flattening,[],[f126]) ).
fof(f129,plain,
! [X0] :
( ssList(tl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f130,plain,
! [X0] :
( ssList(tl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(flattening,[],[f129]) ).
fof(f132,plain,
! [X0] :
( ! [X1] :
( ssList(app(X0,X1))
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f134,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f172,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f173,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( segmentP(app(app(X2,X0),X3),X1)
| ~ segmentP(X0,X1)
| ~ ssList(X3) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f174,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( segmentP(app(app(X2,X0),X3),X1)
| ~ segmentP(X0,X1)
| ~ ssList(X3) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f173]) ).
fof(f192,plain,
! [X0] :
( cons(hd(X0),tl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f78]) ).
fof(f193,plain,
! [X0] :
( cons(hd(X0),tl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(flattening,[],[f192]) ).
fof(f198,plain,
! [X0] :
( ! [X1] :
( cons(X1,X0) = app(cons(X1,nil),X0)
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f201,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f84]) ).
fof(f221,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ! [X4] :
( ~ ssList(X4)
| ~ neq(X4,nil)
| ~ segmentP(X1,X4)
| ~ segmentP(X0,X4) )
& ( nil = X2
| nil != X3 )
& ( nil != X1
| nil != X0 )
& ( ~ neq(X3,nil)
| ( neq(X2,nil)
& ! [X5] :
( ~ ssList(X5)
| X3 = X5
| ! [X6] :
( ~ ssList(X6)
| ! [X7] :
( ~ ssList(X7)
| tl(X2) != X6
| app(X6,X7) != X5
| ! [X8] :
( ~ ssItem(X8)
| cons(X8,nil) != X7
| hd(X2) != X8
| ~ neq(nil,X2) )
| ~ neq(nil,X2) ) ) ) ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f222,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ! [X4] :
( ~ ssList(X4)
| ~ neq(X4,nil)
| ~ segmentP(X1,X4)
| ~ segmentP(X0,X4) )
& ( nil = X2
| nil != X3 )
& ( nil != X1
| nil != X0 )
& ( ~ neq(X3,nil)
| ( neq(X2,nil)
& ! [X5] :
( ~ ssList(X5)
| X3 = X5
| ! [X6] :
( ~ ssList(X6)
| ! [X7] :
( ~ ssList(X7)
| tl(X2) != X6
| app(X6,X7) != X5
| ! [X8] :
( ~ ssItem(X8)
| cons(X8,nil) != X7
| hd(X2) != X8
| ~ neq(nil,X2) )
| ~ neq(nil,X2) ) ) ) ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(flattening,[],[f221]) ).
fof(f234,plain,
! [X0,X1] :
( ~ ssList(X0)
| cons(X1,nil) != X0
| ~ ssItem(X1)
| singletonP(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f241,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| app(app(X2,X1),X3) != X0
| ~ ssList(X3)
| ~ ssList(X2)
| segmentP(X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f303,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1
| neq(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f304,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| X0 != X1
| ~ neq(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f305,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ssList(cons(X1,X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f306,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f314,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| ssItem(hd(X0)) ),
inference(cnf_transformation,[],[f127]) ).
fof(f316,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| ssList(tl(X0)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f318,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f320,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
inference(cnf_transformation,[],[f134]) ).
fof(f337,plain,
~ singletonP(nil),
inference(cnf_transformation,[],[f39]) ).
fof(f357,plain,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,X0) ),
inference(cnf_transformation,[],[f172]) ).
fof(f358,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ segmentP(X0,X1)
| segmentP(app(app(X2,X0),X3),X1) ),
inference(cnf_transformation,[],[f174]) ).
fof(f389,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| cons(hd(X0),tl(X0)) = X0 ),
inference(cnf_transformation,[],[f193]) ).
fof(f392,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| cons(X1,X0) = app(cons(X1,nil),X0) ),
inference(cnf_transformation,[],[f198]) ).
fof(f397,plain,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
inference(cnf_transformation,[],[f201]) ).
fof(f411,plain,
! [X8,X6,X7,X5] :
( ~ neq(nil,sK49)
| hd(sK49) != X8
| cons(X8,nil) != X7
| ~ ssItem(X8)
| app(X6,X7) != X5
| tl(sK49) != X6
| ~ ssList(X7)
| ~ ssList(X6)
| sK50 = X5
| ~ ssList(X5)
| ~ neq(sK50,nil) ),
inference(cnf_transformation,[],[f222]) ).
fof(f412,plain,
! [X4] :
( ~ segmentP(sK47,X4)
| ~ segmentP(sK48,X4)
| ~ neq(X4,nil)
| ~ ssList(X4) ),
inference(cnf_transformation,[],[f222]) ).
fof(f413,plain,
( neq(sK49,nil)
| ~ neq(sK50,nil) ),
inference(cnf_transformation,[],[f222]) ).
fof(f414,plain,
( nil != sK50
| nil = sK49 ),
inference(cnf_transformation,[],[f222]) ).
fof(f415,plain,
( nil != sK47
| nil != sK48 ),
inference(cnf_transformation,[],[f222]) ).
fof(f417,plain,
sK47 = sK49,
inference(cnf_transformation,[],[f222]) ).
fof(f418,plain,
sK48 = sK50,
inference(cnf_transformation,[],[f222]) ).
fof(f420,plain,
ssList(sK48),
inference(cnf_transformation,[],[f222]) ).
fof(f421,plain,
ssList(sK47),
inference(cnf_transformation,[],[f222]) ).
fof(f422,plain,
ssList(sK49),
inference(definition_unfolding,[],[f421,f417]) ).
fof(f423,plain,
ssList(sK50),
inference(definition_unfolding,[],[f420,f418]) ).
fof(f424,plain,
( nil != sK49
| nil != sK50 ),
inference(definition_unfolding,[],[f415,f417,f418]) ).
fof(f425,plain,
! [X4] :
( ~ segmentP(sK49,X4)
| ~ segmentP(sK50,X4)
| ~ neq(X4,nil)
| ~ ssList(X4) ),
inference(definition_unfolding,[],[f412,f417,f418]) ).
fof(f428,plain,
! [X1] :
( ~ ssList(cons(X1,nil))
| ~ ssItem(X1)
| singletonP(cons(X1,nil)) ),
inference(equality_resolution,[],[f234]) ).
fof(f431,plain,
! [X2,X3,X1] :
( ~ ssList(app(app(X2,X1),X3))
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| segmentP(app(app(X2,X1),X3),X1) ),
inference(equality_resolution,[],[f241]) ).
fof(f440,plain,
! [X1] :
( ~ ssList(X1)
| ~ ssList(X1)
| ~ neq(X1,X1) ),
inference(equality_resolution,[],[f304]) ).
fof(f451,plain,
! [X6,X7,X5] :
( ~ neq(nil,sK49)
| cons(hd(sK49),nil) != X7
| ~ ssItem(hd(sK49))
| app(X6,X7) != X5
| tl(sK49) != X6
| ~ ssList(X7)
| ~ ssList(X6)
| sK50 = X5
| ~ ssList(X5)
| ~ neq(sK50,nil) ),
inference(equality_resolution,[],[f411]) ).
fof(f452,plain,
! [X6,X5] :
( ~ neq(nil,sK49)
| ~ ssItem(hd(sK49))
| app(X6,cons(hd(sK49),nil)) != X5
| tl(sK49) != X6
| ~ ssList(cons(hd(sK49),nil))
| ~ ssList(X6)
| sK50 = X5
| ~ ssList(X5)
| ~ neq(sK50,nil) ),
inference(equality_resolution,[],[f451]) ).
fof(f453,plain,
! [X6] :
( ~ neq(nil,sK49)
| ~ ssItem(hd(sK49))
| tl(sK49) != X6
| ~ ssList(cons(hd(sK49),nil))
| ~ ssList(X6)
| sK50 = app(X6,cons(hd(sK49),nil))
| ~ ssList(app(X6,cons(hd(sK49),nil)))
| ~ neq(sK50,nil) ),
inference(equality_resolution,[],[f452]) ).
fof(f454,plain,
( ~ neq(nil,sK49)
| ~ ssItem(hd(sK49))
| ~ ssList(cons(hd(sK49),nil))
| ~ ssList(tl(sK49))
| sK50 = app(tl(sK49),cons(hd(sK49),nil))
| ~ ssList(app(tl(sK49),cons(hd(sK49),nil)))
| ~ neq(sK50,nil) ),
inference(equality_resolution,[],[f453]) ).
fof(f459,plain,
! [X1] :
( ~ singletonP(cons(X1,nil))
| ~ ssItem(X1)
| ssList(cons(X1,nil)) ),
inference(consistent_polarity_flipping,[],[f428]) ).
fof(f471,plain,
! [X2,X3,X1] :
( segmentP(app(app(X2,X1),X3),X1)
| ssList(X1)
| ssList(X3)
| ssList(X2)
| ssList(app(app(X2,X1),X3)) ),
inference(consistent_polarity_flipping,[],[f431]) ).
fof(f530,plain,
! [X1] :
( ssList(X1)
| ssList(X1)
| ~ neq(X1,X1) ),
inference(consistent_polarity_flipping,[],[f440]) ).
fof(f531,plain,
! [X0,X1] :
( neq(X0,X1)
| ssList(X1)
| X0 = X1
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f532,plain,
! [X0,X1] :
( ~ ssList(cons(X1,X0))
| ~ ssItem(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f305]) ).
fof(f533,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f306]) ).
fof(f541,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f314]) ).
fof(f543,plain,
! [X0] :
( ~ ssList(tl(X0))
| nil = X0
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f316]) ).
fof(f545,plain,
! [X0,X1] :
( ~ ssList(app(X0,X1))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f318]) ).
fof(f547,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f320]) ).
fof(f561,plain,
singletonP(nil),
inference(consistent_polarity_flipping,[],[f337]) ).
fof(f581,plain,
! [X0] :
( segmentP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f357]) ).
fof(f582,plain,
! [X2,X3,X0,X1] :
( ~ segmentP(X0,X1)
| ssList(X1)
| ssList(X2)
| ssList(X3)
| ssList(X0)
| segmentP(app(app(X2,X0),X3),X1) ),
inference(consistent_polarity_flipping,[],[f358]) ).
fof(f605,plain,
! [X0] :
( ssList(X0)
| nil = X0
| cons(hd(X0),tl(X0)) = X0 ),
inference(consistent_polarity_flipping,[],[f389]) ).
fof(f608,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ssList(X0)
| cons(X1,X0) = app(cons(X1,nil),X0) ),
inference(consistent_polarity_flipping,[],[f392]) ).
fof(f613,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f397]) ).
fof(f627,plain,
~ ssList(sK49),
inference(consistent_polarity_flipping,[],[f422]) ).
fof(f628,plain,
~ ssList(sK50),
inference(consistent_polarity_flipping,[],[f423]) ).
fof(f631,plain,
! [X4] :
( ~ segmentP(sK50,X4)
| ~ segmentP(sK49,X4)
| ~ neq(X4,nil)
| ssList(X4) ),
inference(consistent_polarity_flipping,[],[f425]) ).
fof(f632,plain,
( ~ neq(nil,sK49)
| ~ ssItem(hd(sK49))
| ssList(cons(hd(sK49),nil))
| ssList(tl(sK49))
| sK50 = app(tl(sK49),cons(hd(sK49),nil))
| ssList(app(tl(sK49),cons(hd(sK49),nil)))
| ~ neq(sK50,nil) ),
inference(consistent_polarity_flipping,[],[f454]) ).
fof(f637,plain,
! [X1] :
( ~ neq(X1,X1)
| ssList(X1) ),
inference(duplicate_literal_removal,[],[f530]) ).
fof(f641,definition,
( spl51_1
<=> neq(sK50,nil) ),
introduced(definition,[new_symbols(definition,[spl51_1])],[avatar_definition]) ).
fof(f643,plain,
( ~ neq(sK50,nil)
| spl51_1 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f645,definition,
( spl51_2
<=> ssList(app(tl(sK49),cons(hd(sK49),nil))) ),
introduced(definition,[new_symbols(definition,[spl51_2])],[avatar_definition]) ).
fof(f647,plain,
( ssList(app(tl(sK49),cons(hd(sK49),nil)))
| ~ spl51_2 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f649,definition,
( spl51_3
<=> sK50 = app(tl(sK49),cons(hd(sK49),nil)) ),
introduced(definition,[new_symbols(definition,[spl51_3])],[avatar_definition]) ).
fof(f651,plain,
( sK50 = app(tl(sK49),cons(hd(sK49),nil))
| ~ spl51_3 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f653,definition,
( spl51_4
<=> ssList(tl(sK49)) ),
introduced(definition,[new_symbols(definition,[spl51_4])],[avatar_definition]) ).
fof(f654,plain,
( ~ ssList(tl(sK49))
| spl51_4 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f655,plain,
( ssList(tl(sK49))
| ~ spl51_4 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f657,definition,
( spl51_5
<=> ssList(cons(hd(sK49),nil)) ),
introduced(definition,[new_symbols(definition,[spl51_5])],[avatar_definition]) ).
fof(f658,plain,
( ~ ssList(cons(hd(sK49),nil))
| spl51_5 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f659,plain,
( ssList(cons(hd(sK49),nil))
| ~ spl51_5 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f661,definition,
( spl51_6
<=> ssItem(hd(sK49)) ),
introduced(definition,[new_symbols(definition,[spl51_6])],[avatar_definition]) ).
fof(f662,plain,
( ssItem(hd(sK49))
| ~ spl51_6 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f663,plain,
( ~ ssItem(hd(sK49))
| spl51_6 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f665,definition,
( spl51_7
<=> neq(nil,sK49) ),
introduced(definition,[new_symbols(definition,[spl51_7])],[avatar_definition]) ).
fof(f667,plain,
( ~ neq(nil,sK49)
| spl51_7 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f668,plain,
( ~ spl51_1
| spl51_2
| spl51_3
| spl51_4
| spl51_5
| ~ spl51_6
| ~ spl51_7 ),
inference(avatar_split_clause,[],[f632,f665,f661,f657,f653,f649,f645,f641]) ).
fof(f670,definition,
( spl51_8
<=> neq(sK49,nil) ),
introduced(definition,[new_symbols(definition,[spl51_8])],[avatar_definition]) ).
fof(f672,plain,
( neq(sK49,nil)
| ~ spl51_8 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f673,plain,
( ~ spl51_1
| spl51_8 ),
inference(avatar_split_clause,[],[f413,f670,f641]) ).
fof(f675,definition,
( spl51_9
<=> nil = sK49 ),
introduced(definition,[new_symbols(definition,[spl51_9])],[avatar_definition]) ).
fof(f676,plain,
( nil != sK49
| spl51_9 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f677,plain,
( nil = sK49
| ~ spl51_9 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f679,definition,
( spl51_10
<=> nil = sK50 ),
introduced(definition,[new_symbols(definition,[spl51_10])],[avatar_definition]) ).
fof(f681,plain,
( nil != sK50
| spl51_10 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f682,plain,
( spl51_9
| ~ spl51_10 ),
inference(avatar_split_clause,[],[f414,f679,f675]) ).
fof(f683,plain,
( ~ spl51_10
| ~ spl51_9 ),
inference(avatar_split_clause,[],[f424,f675,f679]) ).
fof(f689,definition,
( spl51_12
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl51_12])],[avatar_definition]) ).
fof(f690,plain,
( ~ ssList(nil)
| spl51_12 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f718,plain,
~ spl51_12,
inference(avatar_split_clause,[],[f533,f689]) ).
fof(f725,definition,
( spl51_18
<=> neq(nil,nil) ),
introduced(definition,[new_symbols(definition,[spl51_18])],[avatar_definition]) ).
fof(f726,plain,
( neq(nil,nil)
| ~ spl51_18 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f778,plain,
sK50 = app(sK50,nil),
inference(resolution,[],[f613,f628]) ).
fof(f829,plain,
( ssList(nil)
| nil = sK50
| ssList(sK50)
| spl51_1 ),
inference(resolution,[],[f531,f643]) ).
fof(f836,plain,
( nil = sK50
| ssList(sK50)
| spl51_1
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f829,f690]) ).
fof(f837,plain,
( ssList(sK50)
| spl51_1
| spl51_10
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f836,f681]) ).
fof(f838,plain,
( $false
| spl51_1
| spl51_10
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f837,f628]) ).
fof(f839,plain,
( spl51_1
| spl51_10
| spl51_12 ),
inference(avatar_contradiction_clause,[],[f838]) ).
fof(f846,plain,
( nil = sK49
| ssList(sK49)
| spl51_6 ),
inference(resolution,[],[f663,f541]) ).
fof(f847,plain,
( nil = sK49
| spl51_6 ),
inference(forward_subsumption_resolution,[],[f846,f627]) ).
fof(f848,plain,
( spl51_9
| spl51_6 ),
inference(avatar_split_clause,[],[f847,f661,f675]) ).
fof(f849,plain,
( neq(nil,nil)
| ~ spl51_8
| ~ spl51_9 ),
inference(superposition,[],[f672,f677]) ).
fof(f857,plain,
( spl51_18
| ~ spl51_8
| ~ spl51_9 ),
inference(avatar_split_clause,[],[f849,f675,f670,f725]) ).
fof(f860,plain,
( ssList(sK49)
| nil = sK49
| ssList(nil)
| spl51_7 ),
inference(resolution,[],[f667,f531]) ).
fof(f867,plain,
( nil = sK49
| ssList(nil)
| spl51_7 ),
inference(forward_subsumption_resolution,[],[f860,f627]) ).
fof(f868,plain,
( nil = sK49
| spl51_7
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f867,f690]) ).
fof(f869,plain,
( spl51_9
| spl51_7
| spl51_12 ),
inference(avatar_split_clause,[],[f868,f689,f665,f675]) ).
fof(f870,plain,
( ssList(cons(hd(sK49),nil))
| ssList(tl(sK49))
| ~ spl51_2 ),
inference(resolution,[],[f647,f545]) ).
fof(f871,plain,
( spl51_4
| spl51_5
| ~ spl51_2 ),
inference(avatar_split_clause,[],[f870,f645,f657,f653]) ).
fof(f872,plain,
( ~ ssItem(hd(sK49))
| ssList(nil)
| ~ spl51_5 ),
inference(resolution,[],[f659,f532]) ).
fof(f873,plain,
( ssList(nil)
| ~ spl51_5
| ~ spl51_6 ),
inference(forward_subsumption_resolution,[],[f872,f662]) ).
fof(f874,plain,
( $false
| ~ spl51_5
| ~ spl51_6
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f873,f690]) ).
fof(f875,plain,
( ~ spl51_5
| ~ spl51_6
| spl51_12 ),
inference(avatar_contradiction_clause,[],[f874]) ).
fof(f876,plain,
( nil = sK49
| ssList(sK49)
| ~ spl51_4 ),
inference(resolution,[],[f655,f543]) ).
fof(f877,plain,
( ssList(sK49)
| ~ spl51_4
| spl51_9 ),
inference(forward_subsumption_resolution,[],[f876,f676]) ).
fof(f878,plain,
( $false
| ~ spl51_4
| spl51_9 ),
inference(forward_subsumption_resolution,[],[f877,f627]) ).
fof(f879,plain,
( ~ spl51_4
| spl51_9 ),
inference(avatar_contradiction_clause,[],[f878]) ).
fof(f883,plain,
( cons(hd(sK49),nil) = app(nil,cons(hd(sK49),nil))
| spl51_5 ),
inference(resolution,[],[f658,f547]) ).
fof(f885,plain,
( ssList(nil)
| ~ spl51_18 ),
inference(resolution,[],[f726,f637]) ).
fof(f886,plain,
( $false
| spl51_12
| ~ spl51_18 ),
inference(forward_subsumption_resolution,[],[f885,f690]) ).
fof(f887,plain,
( spl51_12
| ~ spl51_18 ),
inference(avatar_contradiction_clause,[],[f886]) ).
fof(f1019,definition,
( spl51_27
<=> nil = cons(hd(sK49),nil) ),
introduced(definition,[new_symbols(definition,[spl51_27])],[avatar_definition]) ).
fof(f1020,plain,
( nil != cons(hd(sK49),nil)
| spl51_27 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1021,plain,
( nil = cons(hd(sK49),nil)
| ~ spl51_27 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1231,plain,
( nil = sK49
| sK49 = cons(hd(sK49),tl(sK49)) ),
inference(resolution,[],[f605,f627]) ).
fof(f1234,plain,
( sK49 = cons(hd(sK49),tl(sK49))
| spl51_9 ),
inference(forward_subsumption_resolution,[],[f1231,f676]) ).
fof(f1301,plain,
( ~ singletonP(nil)
| ~ ssItem(hd(sK49))
| ssList(nil)
| ~ spl51_27 ),
inference(superposition,[],[f459,f1021]) ).
fof(f1315,plain,
( ~ ssItem(hd(sK49))
| ssList(nil)
| ~ spl51_27 ),
inference(forward_subsumption_resolution,[],[f1301,f561]) ).
fof(f1323,plain,
( ssList(nil)
| ~ spl51_6
| ~ spl51_27 ),
inference(forward_subsumption_resolution,[],[f1315,f662]) ).
fof(f1328,plain,
( $false
| ~ spl51_6
| spl51_12
| ~ spl51_27 ),
inference(forward_subsumption_resolution,[],[f1323,f690]) ).
fof(f1329,plain,
( ~ spl51_6
| spl51_12
| ~ spl51_27 ),
inference(avatar_contradiction_clause,[],[f1328]) ).
fof(f1365,plain,
( ! [X0] :
( ssList(X0)
| cons(hd(sK49),X0) = app(cons(hd(sK49),nil),X0) )
| ~ spl51_6 ),
inference(resolution,[],[f608,f662]) ).
fof(f2239,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(X2)
| ssList(X0)
| segmentP(app(app(X1,X0),X2),X0)
| ssList(X0) ),
inference(resolution,[],[f582,f581]) ).
fof(f2243,plain,
! [X2,X0,X1] :
( segmentP(app(app(X1,X0),X2),X0)
| ssList(X1)
| ssList(X2)
| ssList(X0) ),
inference(duplicate_literal_removal,[],[f2239]) ).
fof(f2269,plain,
( ! [X0] :
( segmentP(app(sK50,X0),cons(hd(sK49),nil))
| ssList(cons(hd(sK49),nil))
| ssList(X0)
| ssList(tl(sK49))
| ssList(app(sK50,X0)) )
| ~ spl51_3 ),
inference(superposition,[],[f471,f651]) ).
fof(f2277,plain,
( ! [X0] :
( segmentP(app(sK50,X0),cons(hd(sK49),nil))
| ssList(X0)
| ssList(tl(sK49))
| ssList(app(sK50,X0)) )
| ~ spl51_3
| spl51_5 ),
inference(forward_subsumption_resolution,[],[f2269,f658]) ).
fof(f2280,plain,
( ! [X0] :
( segmentP(app(sK50,X0),cons(hd(sK49),nil))
| ssList(X0)
| ssList(app(sK50,X0)) )
| ~ spl51_3
| spl51_4
| spl51_5 ),
inference(forward_subsumption_resolution,[],[f2277,f654]) ).
fof(f4941,plain,
( cons(hd(sK49),tl(sK49)) = app(cons(hd(sK49),nil),tl(sK49))
| spl51_4
| ~ spl51_6 ),
inference(resolution,[],[f1365,f654]) ).
fof(f4974,plain,
( sK49 = app(cons(hd(sK49),nil),tl(sK49))
| spl51_4
| ~ spl51_6
| spl51_9 ),
inference(forward_demodulation,[],[f4941,f1234]) ).
fof(f5094,plain,
( segmentP(sK50,cons(hd(sK49),nil))
| ssList(nil)
| ssList(sK50)
| ~ spl51_3
| spl51_4
| spl51_5 ),
inference(superposition,[],[f2280,f778]) ).
fof(f5099,plain,
( segmentP(sK50,cons(hd(sK49),nil))
| ssList(sK50)
| ~ spl51_3
| spl51_4
| spl51_5
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f5094,f690]) ).
fof(f5104,plain,
( segmentP(sK50,cons(hd(sK49),nil))
| ~ spl51_3
| spl51_4
| spl51_5
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f5099,f628]) ).
fof(f11094,plain,
( ! [X0] :
( segmentP(app(cons(hd(sK49),nil),X0),cons(hd(sK49),nil))
| ssList(nil)
| ssList(X0)
| ssList(cons(hd(sK49),nil)) )
| spl51_5 ),
inference(superposition,[],[f2243,f883]) ).
fof(f11121,plain,
( ! [X0] :
( segmentP(app(cons(hd(sK49),nil),X0),cons(hd(sK49),nil))
| ssList(X0)
| ssList(cons(hd(sK49),nil)) )
| spl51_5
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f11094,f690]) ).
fof(f11139,plain,
( ! [X0] :
( segmentP(app(cons(hd(sK49),nil),X0),cons(hd(sK49),nil))
| ssList(X0) )
| spl51_5
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f11121,f658]) ).
fof(f39474,plain,
( ~ segmentP(sK49,cons(hd(sK49),nil))
| ~ neq(cons(hd(sK49),nil),nil)
| ssList(cons(hd(sK49),nil))
| ~ spl51_3
| spl51_4
| spl51_5
| spl51_12 ),
inference(resolution,[],[f5104,f631]) ).
fof(f39535,plain,
( ~ segmentP(sK49,cons(hd(sK49),nil))
| ~ neq(cons(hd(sK49),nil),nil)
| ~ spl51_3
| spl51_4
| spl51_5
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f39474,f658]) ).
fof(f39567,definition,
( spl51_1346
<=> neq(cons(hd(sK49),nil),nil) ),
introduced(definition,[new_symbols(definition,[spl51_1346])],[avatar_definition]) ).
fof(f39569,plain,
( ~ neq(cons(hd(sK49),nil),nil)
| spl51_1346 ),
inference(avatar_component_clause,[],[f39567]) ).
fof(f39571,definition,
( spl51_1347
<=> segmentP(sK49,cons(hd(sK49),nil)) ),
introduced(definition,[new_symbols(definition,[spl51_1347])],[avatar_definition]) ).
fof(f39574,plain,
( ~ spl51_1346
| ~ spl51_1347
| ~ spl51_3
| spl51_4
| spl51_5
| spl51_12 ),
inference(avatar_split_clause,[],[f39535,f689,f657,f653,f649,f39571,f39567]) ).
fof(f101894,plain,
( segmentP(sK49,cons(hd(sK49),nil))
| ssList(tl(sK49))
| spl51_4
| spl51_5
| ~ spl51_6
| spl51_9
| spl51_12 ),
inference(superposition,[],[f11139,f4974]) ).
fof(f101899,plain,
( segmentP(sK49,cons(hd(sK49),nil))
| spl51_4
| spl51_5
| ~ spl51_6
| spl51_9
| spl51_12 ),
inference(forward_subsumption_resolution,[],[f101894,f654]) ).
fof(f101931,plain,
( spl51_1347
| spl51_4
| spl51_5
| ~ spl51_6
| spl51_9
| spl51_12 ),
inference(avatar_split_clause,[],[f101899,f689,f675,f661,f657,f653,f39571]) ).
fof(f129157,plain,
( ssList(nil)
| nil = cons(hd(sK49),nil)
| ssList(cons(hd(sK49),nil))
| spl51_1346 ),
inference(resolution,[],[f39569,f531]) ).
fof(f129160,plain,
( nil = cons(hd(sK49),nil)
| ssList(cons(hd(sK49),nil))
| spl51_12
| spl51_1346 ),
inference(forward_subsumption_resolution,[],[f129157,f690]) ).
fof(f129166,plain,
( ssList(cons(hd(sK49),nil))
| spl51_12
| spl51_27
| spl51_1346 ),
inference(forward_subsumption_resolution,[],[f129160,f1020]) ).
fof(f129167,plain,
( $false
| spl51_5
| spl51_12
| spl51_27
| spl51_1346 ),
inference(forward_subsumption_resolution,[],[f129166,f658]) ).
fof(f129168,plain,
( spl51_5
| spl51_12
| spl51_27
| spl51_1346 ),
inference(avatar_contradiction_clause,[],[f129167]) ).
cnf(s1,plain,
( ~ spl51_1
| spl51_2
| spl51_3
| spl51_4
| spl51_5
| ~ spl51_6
| ~ spl51_7 ),
inference(sat_conversion,[],[f668]) ).
cnf(s2,plain,
( ~ spl51_1
| spl51_8 ),
inference(sat_conversion,[],[f673]) ).
cnf(s3,plain,
( spl51_9
| ~ spl51_10 ),
inference(sat_conversion,[],[f682]) ).
cnf(s4,plain,
( ~ spl51_9
| ~ spl51_10 ),
inference(sat_conversion,[],[f683]) ).
cnf(s13,plain,
~ spl51_12,
inference(sat_conversion,[],[f718]) ).
cnf(s16,plain,
( spl51_1
| spl51_10
| spl51_12 ),
inference(sat_conversion,[],[f839]) ).
cnf(s18,plain,
( spl51_6
| spl51_9 ),
inference(sat_conversion,[],[f848]) ).
cnf(s20,plain,
( ~ spl51_8
| ~ spl51_9
| spl51_18 ),
inference(sat_conversion,[],[f857]) ).
cnf(s23,plain,
( spl51_7
| spl51_9
| spl51_12 ),
inference(sat_conversion,[],[f869]) ).
cnf(s24,plain,
( ~ spl51_2
| spl51_4
| spl51_5 ),
inference(sat_conversion,[],[f871]) ).
cnf(s25,plain,
( ~ spl51_5
| ~ spl51_6
| spl51_12 ),
inference(sat_conversion,[],[f875]) ).
cnf(s26,plain,
( ~ spl51_4
| spl51_9 ),
inference(sat_conversion,[],[f879]) ).
cnf(s27,plain,
( spl51_12
| ~ spl51_18 ),
inference(sat_conversion,[],[f887]) ).
cnf(s44,plain,
( ~ spl51_6
| spl51_12
| ~ spl51_27 ),
inference(sat_conversion,[],[f1329]) ).
cnf(s1552,plain,
( ~ spl51_3
| spl51_4
| spl51_5
| spl51_12
| ~ spl51_1346
| ~ spl51_1347 ),
inference(sat_conversion,[],[f39574]) ).
cnf(s8154,plain,
( spl51_4
| spl51_5
| ~ spl51_6
| spl51_9
| spl51_12
| spl51_1347 ),
inference(sat_conversion,[],[f101931]) ).
cnf(s11051,plain,
( spl51_5
| spl51_12
| spl51_27
| spl51_1346 ),
inference(sat_conversion,[],[f129168]) ).
cnf(s11154,plain,
~ spl51_18,
inference(rat,[],[s27,s13]) ).
cnf(s11735,plain,
~ spl51_10,
inference(rat,[],[s3,s4]) ).
cnf(s11758,plain,
spl51_1,
inference(rat,[],[s16,s13,s11735]) ).
cnf(s12133,plain,
spl51_8,
inference(rat,[],[s2,s11758]) ).
cnf(s12136,plain,
~ spl51_9,
inference(rat,[],[s20,s11154,s12133]) ).
cnf(s12144,plain,
~ spl51_4,
inference(rat,[],[s26,s12136]) ).
cnf(s12145,plain,
spl51_7,
inference(rat,[],[s23,s13,s12136]) ).
cnf(s12146,plain,
spl51_6,
inference(rat,[],[s18,s12136]) ).
cnf(s12501,plain,
~ spl51_27,
inference(rat,[],[s44,s13,s12146]) ).
cnf(s12502,plain,
~ spl51_5,
inference(rat,[],[s25,s13,s12146]) ).
cnf(s12825,plain,
spl51_1346,
inference(rat,[],[s11051,s12501,s13,s12502]) ).
cnf(s12830,plain,
spl51_1347,
inference(rat,[],[s8154,s12144,s13,s12136,s12146,s12502]) ).
cnf(s12872,plain,
~ spl51_3,
inference(rat,[],[s1552,s12830,s12825,s13,s12144,s12502]) ).
cnf(s12873,plain,
~ spl51_2,
inference(rat,[],[s24,s12144,s12502]) ).
cnf(s13152,plain,
$false,
inference(rat,[],[s1,s12145,s12146,s12502,s12144,s11758,s12872,s12873]) ).
fof(f129169,plain,
$false,
inference(avatar_sat_refutation,[],[s13152]) ).
%------------------------------------------------------------------------------
%----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.11/0.37 % Computer : n018.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 07:45:39 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 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.03/2.47 % (3212531)Will run a generic schedule for satisfiability detection.
% 14.03/2.47 % (3212539)dis+10_1_sil=32000:sp=arity:random_seed=2072242742:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.03/2.47 % (3212538)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2504739259:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.03/2.47 % (3212540)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2437409944:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.03/2.47 % (3212536)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1860482425_2999 on theBenchmark for (2999ds/0Mi)
% 14.03/2.47 % (3212541)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1076954149:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.03/2.47 % (3212542)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1857046947:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.03/2.47 % (3212537)% WARNING: option uhcvi not known.
% 14.03/2.47 % (3212537)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3541980542:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.03/2.47 % TRYING [1]
% 14.03/2.47 % TRYING [2]
% 14.03/2.47 % TRYING [3]
% 14.03/2.47 % (3212539)Instruction limit reached!
% 14.03/2.47 % (3212539)------------------------------
% 14.03/2.47 % (3212539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.47 % (3212539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.47 % (3212539)CaDiCaL version: 2.1.3
% 14.03/2.47 % (3212539)Termination reason: Instruction limit
% 14.03/2.47 % (3212539)Termination phase: Saturation
% 14.03/2.47 % (3212539)Time elapsed: 0.034 s
% 14.03/2.47 % (3212539)Peak memory usage: 13 MB
% 14.03/2.47 % (3212539)Instructions burned: 103 (million)
% 14.03/2.47 % TRYING [4]
% 14.03/2.47 % (3212550)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1860602231:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.03/2.47 % TRYING [1]
% 14.03/2.47 % TRYING [2]
% 14.03/2.47 % TRYING [3]
% 14.03/2.47 % TRYING [4]
% 14.03/2.47 % (3212540)Instruction limit reached!
% 14.03/2.47 % (3212540)------------------------------
% 14.03/2.47 % (3212540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.47 % (3212540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.47 % (3212540)CaDiCaL version: 2.1.3
% 14.03/2.47 % (3212540)Termination reason: Instruction limit
% 14.03/2.47 % (3212540)Termination phase: Saturation
% 14.03/2.47 % (3212540)Time elapsed: 0.073 s
% 14.03/2.47 % (3212540)Peak memory usage: 13 MB
% 14.03/2.47 % (3212540)Instructions burned: 117 (million)
% 14.03/2.47 % (3212541)Instruction limit reached!
% 14.03/2.47 % (3212541)------------------------------
% 14.03/2.47 % (3212541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.47 % (3212541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.47 % (3212541)CaDiCaL version: 2.1.3
% 14.03/2.47 % (3212541)Termination reason: Instruction limit
% 14.03/2.47 % (3212541)Termination phase: Saturation
% 14.03/2.47 % (3212541)Time elapsed: 0.077 s
% 14.03/2.47 % (3212541)Peak memory usage: 14 MB
% 14.03/2.47 % (3212541)Instructions burned: 132 (million)
% 14.03/2.47 % TRYING [5]
% 14.03/2.47 % TRYING [5]
% 14.03/2.47 % (3212552)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=138760779:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.03/2.47 % (3212553)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=3215695337:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.03/2.47 % (3212542)Instruction limit reached!
% 14.03/2.47 % (3212542)------------------------------
% 14.03/2.47 % (3212542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.47 % (3212542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.47 % (3212542)CaDiCaL version: 2.1.3
% 14.03/2.47 % (3212542)Termination reason: Instruction limit
% 14.03/2.47 % (3212542)Termination phase: Saturation
% 14.03/2.47 % (3212542)Time elapsed: 0.103 s
% 14.03/2.47 % (3212542)Peak memory usage: 15 MB
% 14.03/2.47 % (3212542)Instructions burned: 160 (million)
% 14.03/2.47 % (3212556)ott-21_1_sil=16000:fs=off:random_seed=2307524081:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.03/2.47 % (3212552)Instruction limit reached!
% 14.03/2.47 % (3212552)------------------------------
% 14.03/2.47 % (3212552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212552)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212552)Termination reason: Instruction limit
% 8.51/4.17 % (3212552)Termination phase: Saturation
% 8.51/4.17 % (3212552)Time elapsed: 0.074 s
% 8.51/4.17 % (3212552)Peak memory usage: 13 MB
% 8.51/4.17 % (3212552)Instructions burned: 133 (million)
% 8.51/4.17 % TRYING [6]
% 8.51/4.17 % (3212558)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=495218699:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 8.51/4.17 % (3212550)Instruction limit reached!
% 8.51/4.17 % (3212550)------------------------------
% 8.51/4.17 % (3212550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212550)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212550)Termination reason: Instruction limit
% 8.51/4.17 % (3212550)Termination phase: Finite model building constraint generation
% 8.51/4.17 % (3212550)Time elapsed: 0.158 s
% 8.51/4.17 % (3212550)Peak memory usage: 27 MB
% 8.51/4.17 % (3212550)Instructions burned: 715 (million)
% 8.51/4.17 % (3212560)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1763034005:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.51/4.17 % TRYING [6]
% 8.51/4.17 % TRYING [1]
% 8.51/4.17 % (3212556)Instruction limit reached!
% 8.51/4.17 % (3212556)------------------------------
% 8.51/4.17 % (3212556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212556)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212556)Termination reason: Instruction limit
% 8.51/4.17 % (3212556)Termination phase: Saturation
% 8.51/4.17 % (3212556)Time elapsed: 0.093 s
% 8.51/4.17 % (3212556)Peak memory usage: 14 MB
% 8.51/4.17 % (3212556)Instructions burned: 181 (million)
% 8.51/4.17 % TRYING [2]
% 8.51/4.17 % TRYING [3]
% 8.51/4.17 % (3212562)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2656537603:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.51/4.17 % TRYING [4]
% 8.51/4.17 % TRYING [5]
% 8.51/4.17 % (3212560)Instruction limit reached!
% 8.51/4.17 % (3212560)------------------------------
% 8.51/4.17 % (3212560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212560)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212560)Termination reason: Instruction limit
% 8.51/4.17 % (3212560)Termination phase: Finite model building SAT solving
% 8.51/4.17 % (3212560)Time elapsed: 0.181 s
% 8.51/4.17 % (3212560)Peak memory usage: 23 MB
% 8.51/4.17 % (3212560)Instructions burned: 866 (million)
% 8.51/4.17 % (3212564)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1809573779:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 8.51/4.17 % TRYING [14]
% 8.51/4.17 % (3212553)Instruction limit reached!
% 8.51/4.17 % (3212553)------------------------------
% 8.51/4.17 % (3212553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212553)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212553)Termination reason: Instruction limit
% 8.51/4.17 % (3212553)Termination phase: Saturation
% 8.51/4.17 % (3212553)Time elapsed: 0.383 s
% 8.51/4.17 % (3212553)Peak memory usage: 21 MB
% 8.51/4.17 % (3212553)Instructions burned: 684 (million)
% 8.51/4.17 % (3212566)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=449500247: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)
% 8.51/4.17 % (3212558)Instruction limit reached!
% 8.51/4.17 % (3212558)------------------------------
% 8.51/4.17 % (3212558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212558)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212558)Termination reason: Instruction limit
% 8.51/4.17 % (3212558)Termination phase: Saturation
% 8.51/4.17 % (3212558)Time elapsed: 0.326 s
% 8.51/4.17 % (3212558)Peak memory usage: 14 MB
% 8.51/4.17 % (3212558)Instructions burned: 478 (million)
% 8.51/4.17 % TRYING [7]
% 8.51/4.17 % (3212568)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2088637432:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 8.51/4.17 % (3212564)Instruction limit reached!
% 8.51/4.17 % (3212564)------------------------------
% 8.51/4.17 % (3212564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212564)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212564)Termination reason: Instruction limit
% 8.51/4.17 % (3212564)Termination phase: Finite model building constraint generation
% 8.51/4.17 % (3212564)Time elapsed: 0.177 s
% 8.51/4.17 % (3212564)Peak memory usage: 70 MB
% 8.51/4.17 % (3212564)Instructions burned: 893 (million)
% 8.51/4.17 % (3212570)fmb+10_1_sil=64000:random_seed=2906293598:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 8.51/4.17 % TRYING [1]
% 8.51/4.17 % TRYING [2]
% 8.51/4.17 % TRYING [3]
% 8.51/4.17 % TRYING [4]
% 8.51/4.17 % TRYING [5]
% 8.51/4.17 % TRYING [6]
% 8.51/4.17 % (3212566)Instruction limit reached!
% 8.51/4.17 % (3212566)------------------------------
% 8.51/4.17 % (3212566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212566)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212566)Termination reason: Instruction limit
% 8.51/4.17 % (3212566)Termination phase: Saturation
% 8.51/4.17 % (3212566)Time elapsed: 0.377 s
% 8.51/4.17 % (3212566)Peak memory usage: 24 MB
% 8.51/4.17 % (3212566)Instructions burned: 694 (million)
% 8.51/4.17 % (3212572)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2394697554:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 8.51/4.17 % (3212562)Instruction limit reached!
% 8.51/4.17 % (3212562)------------------------------
% 8.51/4.17 % (3212562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212562)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212562)Termination reason: Instruction limit
% 8.51/4.17 % (3212562)Termination phase: Saturation
% 8.51/4.17 % (3212562)Time elapsed: 0.664 s
% 8.51/4.17 % (3212562)Peak memory usage: 28 MB
% 8.51/4.17 % (3212562)Instructions burned: 1180 (million)
% 8.51/4.17 % TRYING [20]
% 8.51/4.17 % (3212574)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=631957382:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 8.51/4.17 % TRYING [8]
% 8.51/4.17 % (3212568)Instruction limit reached!
% 8.51/4.17 % (3212568)------------------------------
% 8.51/4.17 % (3212568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212568)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212568)Termination reason: Instruction limit
% 8.51/4.17 % (3212568)Termination phase: Saturation
% 8.51/4.17 % (3212568)Time elapsed: 0.467 s
% 8.51/4.17 % (3212568)Peak memory usage: 22 MB
% 8.51/4.17 % (3212568)Instructions burned: 880 (million)
% 8.51/4.17 % (3212576)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2677528184:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 8.51/4.17 % TRYING [8]
% 8.51/4.17 % TRYING [7]
% 8.51/4.17 % (3212574)Instruction limit reached!
% 8.51/4.17 % (3212574)------------------------------
% 8.51/4.17 % (3212574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212574)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212574)Termination reason: Instruction limit
% 8.51/4.17 % (3212574)Termination phase: Finite model building constraint generation
% 8.51/4.17 % (3212574)Time elapsed: 0.338 s
% 8.51/4.17 % (3212574)Peak memory usage: 69 MB
% 8.51/4.17 % (3212574)Instructions burned: 920 (million)
% 8.51/4.17 % (3212578)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3609963184:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 8.51/4.17 % (3212578)Instruction limit reached!
% 8.51/4.17 % (3212578)------------------------------
% 8.51/4.17 % (3212578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.17 % (3212578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.17 % (3212578)CaDiCaL version: 2.1.3
% 8.51/4.17 % (3212578)Termination reason: Instruction limit
% 8.51/4.17 % (3212578)Termination phase: Saturation
% 8.51/4.17 % (3212578)Time elapsed: 0.713 s
% 8.51/4.17 % (3212578)Peak memory usage: 22 MB
% 8.51/4.17 % (3212578)Instructions burned: 1472 (million)
% 8.51/4.17 % (3212580)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=362938529:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 8.51/4.17 % TRYING [8]
% 8.51/4.17 % TRYING [77]
% 8.51/4.17 % TRYING [9]
% 8.51/4.17 % (3212537) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3212531-3212537"...
% 8.51/4.17 % (3212537)...printing done.
% 8.51/4.17 % (3212537)Refutation found. Thanks to Tanya!
% 8.51/4.17 % SZS status Theorem for theBenchmark
% 8.51/4.17 % SZS output start Proof for theBenchmark
% See solution above
% 8.51/4.18 % (3212537)------------------------------
% 8.51/4.18 % (3212537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.51/4.18 % (3212537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/4.18 % (3212537)CaDiCaL version: 2.1.3
% 8.51/4.18 % (3212537)Termination reason: Refutation
% 8.51/4.18 % (3212537)Time elapsed: 3.635 s
% 8.51/4.18 % (3212537)Peak memory usage: 76 MB
% 8.51/4.18 % (3212537)Instructions burned: 6798 (million)
% 8.51/4.18 % (3212531)Success in time 3.763 s
% 8.51/4.18 % Vampire exiting
%------------------------------------------------------------------------------