%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC295+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 : n001.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:05:26 PM UTC 2026
% Result : Theorem 13.34s 3.65s
% Output : Refutation 13.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 41
% Syntax : Number of formulae : 356 ( 35 unt; 20 def)
% Number of atoms : 1329 ( 199 equ)
% Maximal formula atoms : 24 ( 3 avg)
% Number of connectives : 1706 ( 733 ~; 816 |; 64 &)
% ( 34 <=>; 59 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 21 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 280 ( 0 sgn 246 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ( memberP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& app(X2,cons(X1,X3)) = X0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax3) ).
fof(f5,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( frontsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X1,X2) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax5) ).
fof(f6,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( rearsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X2,X1) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax6) ).
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(f20,axiom,
! [X0] :
( ssList(X0)
=> ( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax20) ).
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(f36,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( memberP(app(X1,X2),X0)
<=> ( memberP(X1,X0)
| memberP(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax36) ).
fof(f37,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssList(X2)
=> ( memberP(cons(X1,X2),X0)
<=> ( X0 = X1
| memberP(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax37) ).
fof(f38,axiom,
! [X0] :
( ssItem(X0)
=> ~ memberP(nil,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax38) ).
fof(f41,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( ( frontsegP(X0,X1)
& frontsegP(X1,X0) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax41) ).
fof(f43,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( frontsegP(X0,X1)
=> frontsegP(app(X0,X2),X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax43) ).
fof(f44,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( frontsegP(cons(X0,X2),cons(X1,X3))
<=> ( X0 = X1
& frontsegP(X2,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax44) ).
fof(f45,axiom,
! [X0] :
( ssList(X0)
=> frontsegP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax45) ).
fof(f46,axiom,
! [X0] :
( ssList(X0)
=> ( frontsegP(nil,X0)
<=> nil = X0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax46) ).
fof(f48,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( ( rearsegP(X0,X1)
& rearsegP(X1,X0) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax48) ).
fof(f51,axiom,
! [X0] :
( ssList(X0)
=> rearsegP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax51) ).
fof(f80,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( app(X1,X2) = app(X1,X0)
=> X2 = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax80) ).
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] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ssList(X6)
=> ( app(app(X5,cons(X4,nil)),X6) != X0
| ! [X7] :
( ssItem(X7)
=> ( ( ~ memberP(X5,X7)
| lt(X7,X4) )
& ( ~ memberP(X6,X7)
| lt(X4,X7) ) ) ) ) ) ) )
| ( ! [X8] :
( ssItem(X8)
=> ( cons(X8,nil) != X2
| ~ memberP(X3,X8)
| ? [X9] :
( ssItem(X9)
& X8 != X9
& memberP(X3,X9)
& leq(X8,X9) ) ) )
& ( nil != X3
| 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] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ssList(X6)
=> ( app(app(X5,cons(X4,nil)),X6) != X0
| ! [X7] :
( ssItem(X7)
=> ( ( ~ memberP(X5,X7)
| lt(X7,X4) )
& ( ~ memberP(X6,X7)
| lt(X4,X7) ) ) ) ) ) ) )
| ( ! [X8] :
( ssItem(X8)
=> ( cons(X8,nil) != X2
| ~ memberP(X3,X8)
| ? [X9] :
( ssItem(X9)
& X8 != X9
& memberP(X3,X9)
& leq(X8,X9) ) ) )
& ( nil != X3
| nil != X2 ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f99,plain,
! [X0] :
( ! [X1] :
( ( memberP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& app(X2,cons(X1,X3)) = X0 ) ) )
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f101,plain,
! [X0] :
( ! [X1] :
( ( frontsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X1,X2) = X0 ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f102,plain,
! [X0] :
( ! [X1] :
( ( rearsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X2,X1) = X0 ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f119,plain,
! [X0] :
( ! [X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f123,plain,
! [X0] :
( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f124,plain,
! [X0] :
( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) )
| ~ ssList(X0) ),
inference(flattening,[],[f123]) ).
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(f146,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( memberP(app(X1,X2),X0)
<=> ( memberP(X1,X0)
| memberP(X2,X0) ) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f147,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( memberP(cons(X1,X2),X0)
<=> ( X0 = X1
| memberP(X2,X0) ) )
| ~ ssList(X2) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f148,plain,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f151,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f152,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f151]) ).
fof(f154,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( frontsegP(app(X0,X2),X1)
| ~ frontsegP(X0,X1)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f155,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( frontsegP(app(X0,X2),X1)
| ~ frontsegP(X0,X1)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f154]) ).
fof(f156,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( frontsegP(cons(X0,X2),cons(X1,X3))
<=> ( X0 = X1
& frontsegP(X2,X3) ) )
| ~ ssList(X3) )
| ~ ssList(X2) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f157,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f45]) ).
fof(f158,plain,
! [X0] :
( ( frontsegP(nil,X0)
<=> nil = X0 )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f161,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ rearsegP(X0,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f162,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ rearsegP(X0,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f161]) ).
fof(f166,plain,
! [X0] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f196,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X0
| app(X1,X2) != app(X1,X0)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f80]) ).
fof(f197,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X0
| app(X1,X2) != app(X1,X0)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f196]) ).
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] :
( ? [X5] :
( ? [X6] :
( app(app(X5,cons(X4,nil)),X6) = X0
& ? [X7] :
( ( ( memberP(X5,X7)
& ~ lt(X7,X4) )
| ( memberP(X6,X7)
& ~ lt(X4,X7) ) )
& ssItem(X7) )
& ssList(X6) )
& ssList(X5) )
& ssItem(X4) )
& ( ? [X8] :
( cons(X8,nil) = X2
& memberP(X3,X8)
& ! [X9] :
( ~ ssItem(X9)
| X8 = X9
| ~ memberP(X3,X9)
| ~ leq(X8,X9) )
& ssItem(X8) )
| ( nil = X3
& 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] :
( ? [X5] :
( ? [X6] :
( app(app(X5,cons(X4,nil)),X6) = X0
& ? [X7] :
( ( ( memberP(X5,X7)
& ~ lt(X7,X4) )
| ( memberP(X6,X7)
& ~ lt(X4,X7) ) )
& ssItem(X7) )
& ssList(X6) )
& ssList(X5) )
& ssItem(X4) )
& ( ? [X8] :
( cons(X8,nil) = X2
& memberP(X3,X8)
& ! [X9] :
( ~ ssItem(X9)
| X8 = X9
| ~ memberP(X3,X9)
| ~ leq(X8,X9) )
& ssItem(X8) )
| ( nil = X3
& nil = X2 ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(flattening,[],[f221]) ).
fof(f228,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| app(X2,cons(X1,X3)) != X0
| ~ ssList(X3)
| ~ ssList(X2)
| memberP(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f235,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| app(X1,sK5(X0,X1)) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f236,plain,
! [X0,X1] :
( ssList(sK5(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| app(X1,X2) != X0
| ~ ssList(X2)
| frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f238,plain,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ ssList(X1)
| app(sK6(X0,X1),X1) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f239,plain,
! [X0,X1] :
( ssList(sK6(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f240,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| app(X2,X1) != X0
| ~ ssList(X2)
| rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f305,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f306,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f310,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK44(X0),sK43(X0)) = X0
| nil = X0 ),
inference(cnf_transformation,[],[f124]) ).
fof(f311,plain,
! [X0] :
( ssItem(sK44(X0))
| ~ ssList(X0)
| nil = X0 ),
inference(cnf_transformation,[],[f124]) ).
fof(f312,plain,
! [X0] :
( ssList(sK43(X0))
| ~ ssList(X0)
| nil = X0 ),
inference(cnf_transformation,[],[f124]) ).
fof(f318,plain,
! [X0,X1] :
( ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f320,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
inference(cnf_transformation,[],[f134]) ).
fof(f332,plain,
! [X2,X0,X1] :
( memberP(app(X1,X2),X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ memberP(X1,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f333,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X1,X2),X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| memberP(X2,X0)
| X0 = X1
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f336,plain,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f339,plain,
! [X0,X1] :
( ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f341,plain,
! [X2,X0,X1] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f342,plain,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X2),cons(X1,X3))
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| frontsegP(X2,X3)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f156]) ).
fof(f343,plain,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X2),cons(X1,X3))
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| X0 = X1
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f156]) ).
fof(f344,plain,
! [X2,X3,X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ frontsegP(X2,X3)
| X0 != X1
| frontsegP(cons(X0,X2),cons(X1,X3)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f345,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f347,plain,
! [X0] :
( ~ frontsegP(nil,X0)
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f349,plain,
! [X0,X1] :
( ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f162]) ).
fof(f352,plain,
! [X0] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f166]) ).
fof(f391,plain,
! [X2,X0,X1] :
( app(X1,X2) != app(X1,X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| X0 = X2 ),
inference(cnf_transformation,[],[f197]) ).
fof(f397,plain,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
inference(cnf_transformation,[],[f201]) ).
fof(f412,plain,
( memberP(sK54,sK55)
| memberP(sK53,sK55) ),
inference(cnf_transformation,[],[f222]) ).
fof(f415,plain,
ssItem(sK55),
inference(cnf_transformation,[],[f222]) ).
fof(f416,plain,
ssList(sK54),
inference(cnf_transformation,[],[f222]) ).
fof(f417,plain,
sK47 = app(app(sK53,cons(sK51,nil)),sK54),
inference(cnf_transformation,[],[f222]) ).
fof(f420,plain,
ssList(sK53),
inference(cnf_transformation,[],[f222]) ).
fof(f423,plain,
( nil = sK50
| sK49 = cons(sK52,nil) ),
inference(cnf_transformation,[],[f222]) ).
fof(f424,plain,
( nil = sK49
| ssItem(sK52) ),
inference(cnf_transformation,[],[f222]) ).
fof(f425,plain,
( nil = sK49
| memberP(sK50,sK52) ),
inference(cnf_transformation,[],[f222]) ).
fof(f427,plain,
ssItem(sK51),
inference(cnf_transformation,[],[f222]) ).
fof(f429,plain,
sK47 = sK49,
inference(cnf_transformation,[],[f222]) ).
fof(f431,plain,
ssList(sK49),
inference(cnf_transformation,[],[f222]) ).
fof(f436,plain,
sK49 = app(app(sK53,cons(sK51,nil)),sK54),
inference(definition_unfolding,[],[f417,f429]) ).
fof(f438,plain,
! [X2,X3,X1] :
( memberP(app(X2,cons(X1,X3)),X1)
| ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(app(X2,cons(X1,X3))) ),
inference(equality_resolution,[],[f228]) ).
fof(f440,plain,
! [X2,X1] :
( ~ ssList(app(X1,X2))
| ~ ssList(X1)
| ~ ssList(X2)
| frontsegP(app(X1,X2),X1) ),
inference(equality_resolution,[],[f237]) ).
fof(f441,plain,
! [X2,X1] :
( ~ ssList(app(X2,X1))
| ~ ssList(X1)
| ~ ssList(X2)
| rearsegP(app(X2,X1),X1) ),
inference(equality_resolution,[],[f240]) ).
fof(f453,plain,
! [X2,X3,X1] :
( ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ frontsegP(X2,X3)
| frontsegP(cons(X1,X2),cons(X1,X3)) ),
inference(equality_resolution,[],[f344]) ).
fof(f464,plain,
! [X2,X3,X1] :
( frontsegP(cons(X1,X2),cons(X1,X3))
| ~ ssList(X2)
| ~ ssList(X3)
| ~ frontsegP(X2,X3)
| ~ ssItem(X1) ),
inference(duplicate_literal_removal,[],[f453]) ).
fof(f470,definition,
( spl56_1
<=> ssItem(sK52) ),
introduced(definition,[new_symbols(definition,[spl56_1])],[avatar_definition]) ).
fof(f472,plain,
( ssItem(sK52)
| ~ spl56_1 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f474,definition,
( spl56_2
<=> nil = sK50 ),
introduced(definition,[new_symbols(definition,[spl56_2])],[avatar_definition]) ).
fof(f475,plain,
( nil != sK50
| spl56_2 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f476,plain,
( nil = sK50
| ~ spl56_2 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f480,definition,
( spl56_3
<=> nil = sK49 ),
introduced(definition,[new_symbols(definition,[spl56_3])],[avatar_definition]) ).
fof(f481,plain,
( nil != sK49
| spl56_3 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f482,plain,
( nil = sK49
| ~ spl56_3 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f483,plain,
( spl56_1
| spl56_3 ),
inference(avatar_split_clause,[],[f424,f480,f470]) ).
fof(f489,definition,
( spl56_5
<=> memberP(sK54,sK55) ),
introduced(definition,[new_symbols(definition,[spl56_5])],[avatar_definition]) ).
fof(f491,plain,
( memberP(sK54,sK55)
| ~ spl56_5 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f494,definition,
( spl56_6
<=> memberP(sK53,sK55) ),
introduced(definition,[new_symbols(definition,[spl56_6])],[avatar_definition]) ).
fof(f496,plain,
( memberP(sK53,sK55)
| ~ spl56_6 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f497,plain,
( spl56_6
| spl56_5 ),
inference(avatar_split_clause,[],[f412,f489,f494]) ).
fof(f503,plain,
( memberP(nil,sK52)
| nil = sK49
| ~ spl56_2 ),
inference(forward_demodulation,[],[f425,f476]) ).
fof(f505,definition,
( spl56_8
<=> memberP(nil,sK52) ),
introduced(definition,[new_symbols(definition,[spl56_8])],[avatar_definition]) ).
fof(f507,plain,
( memberP(nil,sK52)
| ~ spl56_8 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f508,plain,
( spl56_3
| spl56_8
| ~ spl56_2 ),
inference(avatar_split_clause,[],[f503,f474,f505,f480]) ).
fof(f532,plain,
sK49 = app(nil,sK49),
inference(resolution,[],[f320,f431]) ).
fof(f559,plain,
sK49 = app(sK49,nil),
inference(resolution,[],[f397,f431]) ).
fof(f977,plain,
! [X0,X1] :
( ~ frontsegP(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| sK5(X1,X0) = app(nil,sK5(X1,X0)) ),
inference(resolution,[],[f236,f320]) ).
fof(f1055,plain,
( sK53 = cons(sK44(sK53),sK43(sK53))
| nil = sK53 ),
inference(resolution,[],[f310,f420]) ).
fof(f1311,plain,
! [X2,X1] :
( frontsegP(app(X1,X2),X1)
| ~ ssList(X2)
| ~ ssList(X1) ),
inference(forward_subsumption_resolution,[],[f440,f318]) ).
fof(f1318,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X1,app(X1,X0))
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| app(X1,X0) = X1 ),
inference(resolution,[],[f1311,f339]) ).
fof(f1326,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X1,app(X1,X0))
| ~ ssList(app(X1,X0))
| app(X1,X0) = X1 ),
inference(duplicate_literal_removal,[],[f1318]) ).
fof(f1329,plain,
! [X0,X1] :
( ~ frontsegP(X1,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| app(X1,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f1326,f318]) ).
fof(f1331,plain,
! [X2,X1] :
( rearsegP(app(X2,X1),X1)
| ~ ssList(X2)
| ~ ssList(X1) ),
inference(forward_subsumption_resolution,[],[f441,f318]) ).
fof(f1333,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X1,app(X0,X1))
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| app(X0,X1) = X1 ),
inference(resolution,[],[f1331,f349]) ).
fof(f1341,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X1,app(X0,X1))
| ~ ssList(app(X0,X1))
| app(X0,X1) = X1 ),
inference(duplicate_literal_removal,[],[f1333]) ).
fof(f1344,plain,
! [X0,X1] :
( ~ rearsegP(X1,app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) = X1 ),
inference(forward_subsumption_resolution,[],[f1341,f318]) ).
fof(f1385,plain,
! [X0] :
( ~ ssList(nil)
| app(nil,sK5(X0,nil)) = X0
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[],[f235,f345]) ).
fof(f1388,plain,
! [X0] :
( ~ ssList(nil)
| app(nil,sK5(X0,nil)) = X0
| ~ ssList(X0) ),
inference(duplicate_literal_removal,[],[f1385]) ).
fof(f1394,plain,
! [X0] :
( ~ ssList(nil)
| app(sK6(X0,nil),nil) = X0
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[],[f238,f352]) ).
fof(f1397,plain,
! [X0] :
( ~ ssList(nil)
| app(sK6(X0,nil),nil) = X0
| ~ ssList(X0) ),
inference(duplicate_literal_removal,[],[f1394]) ).
fof(f1423,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X2,X0)
| ~ ssList(X2)
| ~ frontsegP(X0,app(X2,X1))
| ~ ssList(app(X2,X1))
| ~ ssList(X0)
| app(X2,X1) = X0 ),
inference(resolution,[],[f341,f339]) ).
fof(f1431,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X2,X0)
| ~ ssList(X2)
| ~ frontsegP(X0,app(X2,X1))
| ~ ssList(app(X2,X1))
| app(X2,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1423]) ).
fof(f1437,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X2,X1))
| ~ ssList(X1)
| ~ frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| app(X2,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1431,f318]) ).
fof(f1732,definition,
( spl56_13
<=> nil = sK53 ),
introduced(definition,[new_symbols(definition,[spl56_13])],[avatar_definition]) ).
fof(f1733,plain,
( nil != sK53
| spl56_13 ),
inference(avatar_component_clause,[],[f1732]) ).
fof(f1734,plain,
( nil = sK53
| ~ spl56_13 ),
inference(avatar_component_clause,[],[f1732]) ).
fof(f1810,definition,
( spl56_15
<=> nil = sK54 ),
introduced(definition,[new_symbols(definition,[spl56_15])],[avatar_definition]) ).
fof(f1811,plain,
( nil != sK54
| spl56_15 ),
inference(avatar_component_clause,[],[f1810]) ).
fof(f1812,plain,
( nil = sK54
| ~ spl56_15 ),
inference(avatar_component_clause,[],[f1810]) ).
fof(f2026,plain,
( memberP(nil,sK55)
| ~ spl56_5
| ~ spl56_15 ),
inference(superposition,[],[f491,f1812]) ).
fof(f2045,plain,
( ~ ssItem(sK55)
| ~ spl56_5
| ~ spl56_15 ),
inference(resolution,[],[f2026,f336]) ).
fof(f2046,plain,
( $false
| ~ spl56_5
| ~ spl56_15 ),
inference(forward_subsumption_resolution,[],[f2045,f415]) ).
fof(f2047,plain,
( ~ spl56_5
| ~ spl56_15 ),
inference(avatar_contradiction_clause,[],[f2046]) ).
fof(f2049,plain,
( memberP(nil,sK55)
| ~ spl56_6
| ~ spl56_13 ),
inference(forward_demodulation,[],[f496,f1734]) ).
fof(f2549,definition,
( spl56_18
<=> ssList(sK5(sK53,nil)) ),
introduced(definition,[new_symbols(definition,[spl56_18])],[avatar_definition]) ).
fof(f2550,plain,
( ssList(sK5(sK53,nil))
| ~ spl56_18 ),
inference(avatar_component_clause,[],[f2549]) ).
fof(f2551,plain,
( ~ ssList(sK5(sK53,nil))
| spl56_18 ),
inference(avatar_component_clause,[],[f2549]) ).
fof(f2553,definition,
( spl56_19
<=> frontsegP(sK53,nil) ),
introduced(definition,[new_symbols(definition,[spl56_19])],[avatar_definition]) ).
fof(f2554,plain,
( ~ frontsegP(sK53,nil)
| spl56_19 ),
inference(avatar_component_clause,[],[f2553]) ).
fof(f2555,plain,
( frontsegP(sK53,nil)
| ~ spl56_19 ),
inference(avatar_component_clause,[],[f2553]) ).
fof(f2568,plain,
( ~ ssList(sK53)
| spl56_19 ),
inference(resolution,[],[f2554,f345]) ).
fof(f2571,plain,
( $false
| spl56_19 ),
inference(forward_subsumption_resolution,[],[f2568,f420]) ).
fof(f2572,plain,
spl56_19,
inference(avatar_contradiction_clause,[],[f2571]) ).
fof(f2793,definition,
( spl56_20
<=> ssList(app(sK53,cons(sK51,nil))) ),
introduced(definition,[new_symbols(definition,[spl56_20])],[avatar_definition]) ).
fof(f2794,plain,
( ssList(app(sK53,cons(sK51,nil)))
| ~ spl56_20 ),
inference(avatar_component_clause,[],[f2793]) ).
fof(f2795,plain,
( ~ ssList(app(sK53,cons(sK51,nil)))
| spl56_20 ),
inference(avatar_component_clause,[],[f2793]) ).
fof(f2801,plain,
( ~ ssList(cons(sK51,nil))
| ~ ssList(sK53)
| spl56_20 ),
inference(resolution,[],[f2795,f318]) ).
fof(f2802,plain,
( ~ ssList(cons(sK51,nil))
| spl56_20 ),
inference(forward_subsumption_resolution,[],[f2801,f420]) ).
fof(f2803,plain,
( ~ ssItem(sK51)
| ~ ssList(nil)
| spl56_20 ),
inference(resolution,[],[f2802,f305]) ).
fof(f2804,plain,
( ~ ssList(nil)
| spl56_20 ),
inference(forward_subsumption_resolution,[],[f2803,f427]) ).
fof(f2872,plain,
( sK49 = cons(sK52,nil)
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f423,f475]) ).
fof(f2887,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssItem(sK52)
| ~ ssList(nil)
| memberP(nil,X0)
| sK52 = X0
| ~ ssItem(X0) )
| spl56_2 ),
inference(superposition,[],[f333,f2872]) ).
fof(f2905,plain,
( ! [X0] :
( frontsegP(cons(sK52,X0),sK49)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(X0,nil)
| ~ ssItem(sK52) )
| spl56_2 ),
inference(superposition,[],[f464,f2872]) ).
fof(f2924,plain,
! [X0] :
( memberP(sK49,X0)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ ssList(sK54)
| ~ memberP(app(sK53,cons(sK51,nil)),X0)
| ~ ssItem(X0) ),
inference(superposition,[],[f332,f436]) ).
fof(f2925,plain,
! [X0] :
( frontsegP(sK49,X0)
| ~ ssList(X0)
| ~ ssList(sK54)
| ~ frontsegP(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(app(sK53,cons(sK51,nil))) ),
inference(superposition,[],[f341,f436]) ).
fof(f2931,plain,
! [X0] :
( sK49 != app(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ ssList(X0)
| ~ ssList(sK54)
| sK54 = X0 ),
inference(superposition,[],[f391,f436]) ).
fof(f2935,plain,
( frontsegP(sK49,app(sK53,cons(sK51,nil)))
| ~ ssList(sK54)
| ~ ssList(app(sK53,cons(sK51,nil))) ),
inference(superposition,[],[f1311,f436]) ).
fof(f2936,plain,
( rearsegP(sK49,sK54)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ ssList(sK54) ),
inference(superposition,[],[f1331,f436]) ).
fof(f2939,plain,
( $false
| spl56_20 ),
inference(forward_subsumption_resolution,[],[f306,f2804]) ).
fof(f2940,plain,
spl56_20,
inference(avatar_contradiction_clause,[],[f2939]) ).
fof(f2959,plain,
( ! [X0] :
( frontsegP(cons(sK52,X0),sK49)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ frontsegP(X0,nil) )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f2905,f472]) ).
fof(f2975,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssList(nil)
| memberP(nil,X0)
| sK52 = X0
| ~ ssItem(X0) )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f2887,f472]) ).
fof(f2980,plain,
( rearsegP(sK49,sK54)
| ~ ssList(app(sK53,cons(sK51,nil))) ),
inference(forward_subsumption_resolution,[],[f2936,f416]) ).
fof(f2981,plain,
( frontsegP(sK49,app(sK53,cons(sK51,nil)))
| ~ ssList(app(sK53,cons(sK51,nil))) ),
inference(forward_subsumption_resolution,[],[f2935,f416]) ).
fof(f2983,plain,
! [X0] :
( sK49 != app(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ ssList(X0)
| sK54 = X0 ),
inference(forward_subsumption_resolution,[],[f2931,f416]) ).
fof(f2989,plain,
! [X0] :
( frontsegP(sK49,X0)
| ~ ssList(X0)
| ~ frontsegP(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(app(sK53,cons(sK51,nil))) ),
inference(forward_subsumption_resolution,[],[f2925,f416]) ).
fof(f2990,plain,
! [X0] :
( memberP(sK49,X0)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ memberP(app(sK53,cons(sK51,nil)),X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[],[f2924,f416]) ).
fof(f2995,plain,
( ! [X0] :
( frontsegP(cons(sK52,X0),sK49)
| ~ ssList(X0)
| ~ ssList(nil) )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f2959,f345]) ).
fof(f2996,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssList(nil)
| sK52 = X0
| ~ ssItem(X0) )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f2975,f336]) ).
fof(f3043,plain,
! [X0] :
( sK49 != app(sK49,X0)
| ~ ssList(sK49)
| ~ ssList(X0)
| ~ ssList(nil)
| nil = X0 ),
inference(superposition,[],[f391,f559]) ).
fof(f3048,plain,
! [X0] :
( sK49 != app(sK49,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f3043,f431]) ).
fof(f3054,plain,
! [X0] :
( sK49 != app(sK49,X0)
| ~ ssList(X0)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f3048,f306]) ).
fof(f3131,plain,
( rearsegP(sK49,sK54)
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f2980,f2794]) ).
fof(f3135,plain,
( ! [X0] :
( frontsegP(cons(sK52,X0),sK49)
| ~ ssList(X0) )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f2995,f306]) ).
fof(f3139,plain,
( frontsegP(sK49,sK49)
| ~ ssList(nil)
| ~ spl56_1
| spl56_2 ),
inference(superposition,[],[f3135,f2872]) ).
fof(f3140,plain,
( frontsegP(sK49,sK49)
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f3139,f306]) ).
fof(f3148,definition,
( spl56_22
<=> ssList(cons(sK51,nil)) ),
introduced(definition,[new_symbols(definition,[spl56_22])],[avatar_definition]) ).
fof(f3149,plain,
( ssList(cons(sK51,nil))
| ~ spl56_22 ),
inference(avatar_component_clause,[],[f3148]) ).
fof(f3150,plain,
( ~ ssList(cons(sK51,nil))
| spl56_22 ),
inference(avatar_component_clause,[],[f3148]) ).
fof(f3156,plain,
( ~ ssItem(sK51)
| ~ ssList(nil)
| spl56_22 ),
inference(resolution,[],[f3150,f305]) ).
fof(f3157,plain,
( ~ ssList(nil)
| spl56_22 ),
inference(forward_subsumption_resolution,[],[f3156,f427]) ).
fof(f3158,plain,
( $false
| spl56_22 ),
inference(forward_subsumption_resolution,[],[f3157,f306]) ).
fof(f3159,plain,
spl56_22,
inference(avatar_contradiction_clause,[],[f3158]) ).
fof(f3467,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| sK52 = X0
| ~ ssItem(X0) )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f2996,f306]) ).
fof(f4367,plain,
( frontsegP(sK49,app(sK53,cons(sK51,nil)))
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f2981,f2794]) ).
fof(f6595,plain,
( ! [X0] :
( ~ frontsegP(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(X0)
| frontsegP(sK49,X0) )
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f2989,f2794]) ).
fof(f6605,plain,
( ~ ssList(sK53)
| frontsegP(sK49,sK53)
| ~ ssList(cons(sK51,nil))
| ~ ssList(sK53)
| ~ spl56_20 ),
inference(resolution,[],[f6595,f1311]) ).
fof(f6613,plain,
( ~ ssList(sK53)
| frontsegP(sK49,sK53)
| ~ ssList(cons(sK51,nil))
| ~ spl56_20 ),
inference(duplicate_literal_removal,[],[f6605]) ).
fof(f6617,plain,
( frontsegP(sK49,sK53)
| ~ ssList(cons(sK51,nil))
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f6613,f420]) ).
fof(f6620,plain,
( frontsegP(sK49,sK53)
| ~ spl56_20
| ~ spl56_22 ),
inference(forward_subsumption_resolution,[],[f6617,f3149]) ).
fof(f6626,plain,
( ! [X0] :
( ~ memberP(app(sK53,cons(sK51,nil)),X0)
| memberP(sK49,X0)
| ~ ssItem(X0) )
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f2990,f2794]) ).
fof(f6632,plain,
( memberP(sK49,sK51)
| ~ ssItem(sK51)
| ~ ssItem(sK51)
| ~ ssList(nil)
| ~ ssList(sK53)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ spl56_20 ),
inference(resolution,[],[f6626,f438]) ).
fof(f6633,plain,
( memberP(sK49,sK51)
| ~ ssItem(sK51)
| ~ ssList(nil)
| ~ ssList(sK53)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ spl56_20 ),
inference(duplicate_literal_removal,[],[f6632]) ).
fof(f6636,plain,
( memberP(sK49,sK51)
| ~ ssList(nil)
| ~ ssList(sK53)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f6633,f427]) ).
fof(f6639,plain,
( memberP(sK49,sK51)
| ~ ssList(sK53)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f6636,f306]) ).
fof(f6642,plain,
( memberP(sK49,sK51)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f6639,f420]) ).
fof(f6643,plain,
( memberP(sK49,sK51)
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f6642,f2794]) ).
fof(f6644,plain,
( sK51 = sK52
| ~ ssItem(sK51)
| ~ spl56_1
| spl56_2
| ~ spl56_20 ),
inference(resolution,[],[f6643,f3467]) ).
fof(f6647,plain,
( sK51 = sK52
| ~ spl56_1
| spl56_2
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f6644,f427]) ).
fof(f6649,plain,
( ! [X0] :
( sK49 != app(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f2983,f2794]) ).
fof(f8447,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,sK5(X0,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f1388,f306]) ).
fof(f8494,plain,
sK53 = app(nil,sK5(sK53,nil)),
inference(resolution,[],[f8447,f420]) ).
fof(f8506,plain,
! [X0] :
( ~ ssList(X0)
| app(sK6(X0,nil),nil) = X0 ),
inference(forward_subsumption_resolution,[],[f1397,f306]) ).
fof(f8550,plain,
sK54 = app(sK6(sK54,nil),nil),
inference(resolution,[],[f8506,f416]) ).
fof(f11255,definition,
( spl56_38
<=> ssList(sK6(sK54,nil)) ),
introduced(definition,[new_symbols(definition,[spl56_38])],[avatar_definition]) ).
fof(f11256,plain,
( ssList(sK6(sK54,nil))
| ~ spl56_38 ),
inference(avatar_component_clause,[],[f11255]) ).
fof(f11257,plain,
( ~ ssList(sK6(sK54,nil))
| spl56_38 ),
inference(avatar_component_clause,[],[f11255]) ).
fof(f11259,definition,
( spl56_39
<=> rearsegP(sK54,nil) ),
introduced(definition,[new_symbols(definition,[spl56_39])],[avatar_definition]) ).
fof(f11260,plain,
( ~ rearsegP(sK54,nil)
| spl56_39 ),
inference(avatar_component_clause,[],[f11259]) ).
fof(f11273,plain,
( ~ ssList(nil)
| ~ ssList(sK54)
| ~ rearsegP(sK54,nil)
| spl56_38 ),
inference(resolution,[],[f11257,f239]) ).
fof(f11274,plain,
( ~ ssList(sK54)
| ~ rearsegP(sK54,nil)
| spl56_38 ),
inference(forward_subsumption_resolution,[],[f11273,f306]) ).
fof(f11275,plain,
( ~ rearsegP(sK54,nil)
| spl56_38 ),
inference(forward_subsumption_resolution,[],[f11274,f416]) ).
fof(f11286,plain,
( ~ spl56_39
| spl56_38 ),
inference(avatar_split_clause,[],[f11275,f11255,f11259]) ).
fof(f11293,plain,
( ~ ssList(sK54)
| spl56_39 ),
inference(resolution,[],[f11260,f352]) ).
fof(f11296,plain,
( $false
| spl56_39 ),
inference(forward_subsumption_resolution,[],[f11293,f416]) ).
fof(f11297,plain,
spl56_39,
inference(avatar_contradiction_clause,[],[f11296]) ).
fof(f13528,plain,
( ~ frontsegP(nil,sK53)
| ~ ssList(nil)
| ~ ssList(sK5(sK53,nil))
| nil = sK53 ),
inference(superposition,[],[f1329,f8494]) ).
fof(f13568,plain,
( ~ frontsegP(nil,sK53)
| ~ ssList(sK5(sK53,nil))
| nil = sK53 ),
inference(forward_subsumption_resolution,[],[f13528,f306]) ).
fof(f13582,plain,
( ~ frontsegP(nil,sK53)
| nil = sK53
| ~ spl56_18 ),
inference(forward_subsumption_resolution,[],[f13568,f2550]) ).
fof(f13589,plain,
( ~ frontsegP(nil,sK53)
| spl56_13
| ~ spl56_18 ),
inference(forward_subsumption_resolution,[],[f13582,f1733]) ).
fof(f13622,plain,
( ~ rearsegP(nil,sK54)
| ~ ssList(nil)
| ~ ssList(sK6(sK54,nil))
| nil = sK54 ),
inference(superposition,[],[f1344,f8550]) ).
fof(f13647,plain,
( ~ rearsegP(nil,sK54)
| ~ ssList(sK6(sK54,nil))
| nil = sK54 ),
inference(forward_subsumption_resolution,[],[f13622,f306]) ).
fof(f13662,plain,
( ~ rearsegP(nil,sK54)
| nil = sK54
| ~ spl56_38 ),
inference(forward_subsumption_resolution,[],[f13647,f11256]) ).
fof(f13671,plain,
( ~ rearsegP(nil,sK54)
| spl56_15
| ~ spl56_38 ),
inference(forward_subsumption_resolution,[],[f13662,f1811]) ).
fof(f18277,plain,
( ~ ssList(sK53)
| ~ ssList(nil)
| sK5(sK53,nil) = app(nil,sK5(sK53,nil))
| ~ spl56_19 ),
inference(resolution,[],[f977,f2555]) ).
fof(f18290,plain,
( ~ ssList(nil)
| sK5(sK53,nil) = app(nil,sK5(sK53,nil))
| ~ spl56_19 ),
inference(forward_subsumption_resolution,[],[f18277,f420]) ).
fof(f18305,plain,
( sK5(sK53,nil) = app(nil,sK5(sK53,nil))
| ~ spl56_19 ),
inference(forward_subsumption_resolution,[],[f18290,f306]) ).
fof(f18313,plain,
( sK53 = sK5(sK53,nil)
| ~ spl56_19 ),
inference(forward_demodulation,[],[f18305,f8494]) ).
fof(f24477,plain,
( ~ ssList(cons(sK51,nil))
| ~ frontsegP(sK53,sK49)
| ~ ssList(sK53)
| ~ ssList(sK49)
| sK49 = app(sK53,cons(sK51,nil))
| ~ spl56_20 ),
inference(resolution,[],[f1437,f4367]) ).
fof(f24562,plain,
( ~ frontsegP(sK53,sK49)
| ~ ssList(sK53)
| ~ ssList(sK49)
| sK49 = app(sK53,cons(sK51,nil))
| ~ spl56_20
| ~ spl56_22 ),
inference(forward_subsumption_resolution,[],[f24477,f3149]) ).
fof(f24579,plain,
( ~ frontsegP(sK53,sK49)
| ~ ssList(sK49)
| sK49 = app(sK53,cons(sK51,nil))
| ~ spl56_20
| ~ spl56_22 ),
inference(forward_subsumption_resolution,[],[f24562,f420]) ).
fof(f24588,plain,
( ~ frontsegP(sK53,sK49)
| sK49 = app(sK53,cons(sK51,nil))
| ~ spl56_20
| ~ spl56_22 ),
inference(forward_subsumption_resolution,[],[f24579,f431]) ).
fof(f24590,plain,
( sK49 = app(sK53,cons(sK52,nil))
| ~ frontsegP(sK53,sK49)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22 ),
inference(forward_demodulation,[],[f24588,f6647]) ).
fof(f24591,plain,
( sK49 = app(sK53,sK49)
| ~ frontsegP(sK53,sK49)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22 ),
inference(forward_demodulation,[],[f24590,f2872]) ).
fof(f24593,definition,
( spl56_40
<=> frontsegP(sK53,sK49) ),
introduced(definition,[new_symbols(definition,[spl56_40])],[avatar_definition]) ).
fof(f24595,plain,
( ~ frontsegP(sK53,sK49)
| spl56_40 ),
inference(avatar_component_clause,[],[f24593]) ).
fof(f24597,definition,
( spl56_41
<=> sK49 = app(sK53,sK49) ),
introduced(definition,[new_symbols(definition,[spl56_41])],[avatar_definition]) ).
fof(f24599,plain,
( sK49 = app(sK53,sK49)
| ~ spl56_41 ),
inference(avatar_component_clause,[],[f24597]) ).
fof(f24600,plain,
( ~ spl56_40
| spl56_41
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22 ),
inference(avatar_split_clause,[],[f24591,f3148,f2793,f474,f470,f24597,f24593]) ).
fof(f58338,definition,
( spl56_59
<=> sK49 = sK53 ),
introduced(definition,[new_symbols(definition,[spl56_59])],[avatar_definition]) ).
fof(f58339,plain,
( sK49 = sK53
| ~ spl56_59 ),
inference(avatar_component_clause,[],[f58338]) ).
fof(f58340,plain,
( sK49 != sK53
| spl56_59 ),
inference(avatar_component_clause,[],[f58338]) ).
fof(f58440,plain,
( ~ ssList(sK53)
| spl56_18
| ~ spl56_19 ),
inference(forward_demodulation,[],[f2551,f18313]) ).
fof(f58465,plain,
( $false
| spl56_18
| ~ spl56_19 ),
inference(forward_subsumption_resolution,[],[f58440,f420]) ).
fof(f58466,plain,
( spl56_18
| ~ spl56_19 ),
inference(avatar_contradiction_clause,[],[f58465]) ).
fof(f60288,plain,
( rearsegP(nil,sK54)
| ~ spl56_3
| ~ spl56_20 ),
inference(superposition,[],[f3131,f482]) ).
fof(f60305,plain,
( frontsegP(nil,sK53)
| ~ spl56_3
| ~ spl56_20
| ~ spl56_22 ),
inference(superposition,[],[f6620,f482]) ).
fof(f60375,plain,
( $false
| ~ spl56_3
| spl56_13
| ~ spl56_18
| ~ spl56_20
| ~ spl56_22 ),
inference(forward_subsumption_resolution,[],[f60305,f13589]) ).
fof(f60376,plain,
( ~ spl56_3
| spl56_13
| ~ spl56_18
| ~ spl56_20
| ~ spl56_22 ),
inference(avatar_contradiction_clause,[],[f60375]) ).
fof(f60380,plain,
( $false
| ~ spl56_3
| spl56_15
| ~ spl56_20
| ~ spl56_38 ),
inference(forward_subsumption_resolution,[],[f60288,f13671]) ).
fof(f60381,plain,
( ~ spl56_3
| spl56_15
| ~ spl56_20
| ~ spl56_38 ),
inference(avatar_contradiction_clause,[],[f60380]) ).
fof(f60559,plain,
( ~ ssItem(sK52)
| ~ spl56_8 ),
inference(resolution,[],[f507,f336]) ).
fof(f60640,plain,
( $false
| ~ spl56_1
| ~ spl56_8 ),
inference(forward_subsumption_resolution,[],[f60559,f472]) ).
fof(f60641,plain,
( ~ spl56_1
| ~ spl56_8 ),
inference(avatar_contradiction_clause,[],[f60640]) ).
fof(f60802,plain,
( sK49 = cons(sK52,nil)
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f423,f475]) ).
fof(f60822,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| frontsegP(nil,X1)
| ~ ssItem(sK52) )
| spl56_2 ),
inference(superposition,[],[f342,f60802]) ).
fof(f60824,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| sK52 = X0
| ~ ssItem(sK52) )
| spl56_2 ),
inference(superposition,[],[f343,f60802]) ).
fof(f60901,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(X1)
| sK52 = X0
| ~ ssItem(sK52) )
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f60824,f306]) ).
fof(f60903,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(X1)
| frontsegP(nil,X1)
| ~ ssItem(sK52) )
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f60822,f306]) ).
fof(f60950,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(X1)
| sK52 = X0 )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f60901,f472]) ).
fof(f60952,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(X1)
| frontsegP(nil,X1) )
| ~ spl56_1
| spl56_2 ),
inference(forward_subsumption_resolution,[],[f60903,f472]) ).
fof(f62112,definition,
( spl56_74
<=> sK53 = cons(sK44(sK53),sK43(sK53)) ),
introduced(definition,[new_symbols(definition,[spl56_74])],[avatar_definition]) ).
fof(f62114,plain,
( sK53 = cons(sK44(sK53),sK43(sK53))
| ~ spl56_74 ),
inference(avatar_component_clause,[],[f62112]) ).
fof(f62115,plain,
( spl56_13
| spl56_74 ),
inference(avatar_split_clause,[],[f1055,f62112,f1732]) ).
fof(f62116,plain,
( ~ ssItem(sK55)
| ~ spl56_6
| ~ spl56_13 ),
inference(resolution,[],[f2049,f336]) ).
fof(f62197,plain,
( $false
| ~ spl56_6
| ~ spl56_13 ),
inference(forward_subsumption_resolution,[],[f62116,f415]) ).
fof(f62198,plain,
( ~ spl56_6
| ~ spl56_13 ),
inference(avatar_contradiction_clause,[],[f62197]) ).
fof(f64126,plain,
( ! [X0] :
( sK49 != app(app(sK53,cons(sK52,nil)),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl56_1
| spl56_2
| ~ spl56_20 ),
inference(forward_demodulation,[],[f6649,f6647]) ).
fof(f64143,plain,
( ! [X0] :
( sK49 != app(app(sK53,sK49),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl56_1
| spl56_2
| ~ spl56_20 ),
inference(forward_demodulation,[],[f64126,f60802]) ).
fof(f64154,plain,
( ! [X0] :
( sK49 != app(app(nil,sK49),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl56_1
| spl56_2
| ~ spl56_13
| ~ spl56_20 ),
inference(forward_demodulation,[],[f64143,f1734]) ).
fof(f64160,plain,
( ! [X0] :
( sK49 != app(sK49,X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl56_1
| spl56_2
| ~ spl56_13
| ~ spl56_20 ),
inference(forward_demodulation,[],[f64154,f532]) ).
fof(f64185,plain,
( sK49 != sK49
| ~ ssList(nil)
| nil = sK54
| ~ spl56_1
| spl56_2
| ~ spl56_13
| ~ spl56_20 ),
inference(superposition,[],[f64160,f559]) ).
fof(f64186,plain,
( ~ ssList(nil)
| nil = sK54
| ~ spl56_1
| spl56_2
| ~ spl56_13
| ~ spl56_20 ),
inference(trivial_inequality_removal,[],[f64185]) ).
fof(f64187,plain,
( nil = sK54
| ~ spl56_1
| spl56_2
| ~ spl56_13
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f64186,f306]) ).
fof(f64188,plain,
( $false
| ~ spl56_1
| spl56_2
| ~ spl56_13
| spl56_15
| ~ spl56_20 ),
inference(forward_subsumption_resolution,[],[f64187,f1811]) ).
fof(f64189,plain,
( ~ spl56_1
| spl56_2
| ~ spl56_13
| spl56_15
| ~ spl56_20 ),
inference(avatar_contradiction_clause,[],[f64188]) ).
fof(f64247,plain,
( ~ frontsegP(sK49,sK53)
| ~ ssItem(sK44(sK53))
| ~ ssList(sK43(sK53))
| sK52 = sK44(sK53)
| ~ spl56_1
| spl56_2
| ~ spl56_74 ),
inference(superposition,[],[f60950,f62114]) ).
fof(f64249,plain,
( ~ frontsegP(sK49,sK53)
| ~ ssItem(sK44(sK53))
| ~ ssList(sK43(sK53))
| frontsegP(nil,sK43(sK53))
| ~ spl56_1
| spl56_2
| ~ spl56_74 ),
inference(superposition,[],[f60952,f62114]) ).
fof(f64252,plain,
( ~ ssItem(sK44(sK53))
| ~ ssList(sK43(sK53))
| frontsegP(nil,sK43(sK53))
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74 ),
inference(forward_subsumption_resolution,[],[f64249,f6620]) ).
fof(f64253,plain,
( ~ ssItem(sK44(sK53))
| ~ ssList(sK43(sK53))
| sK52 = sK44(sK53)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74 ),
inference(forward_subsumption_resolution,[],[f64247,f6620]) ).
fof(f76004,definition,
( spl56_81
<=> ssItem(sK44(sK53)) ),
introduced(definition,[new_symbols(definition,[spl56_81])],[avatar_definition]) ).
fof(f76005,plain,
( ssItem(sK44(sK53))
| ~ spl56_81 ),
inference(avatar_component_clause,[],[f76004]) ).
fof(f76006,plain,
( ~ ssItem(sK44(sK53))
| spl56_81 ),
inference(avatar_component_clause,[],[f76004]) ).
fof(f76008,definition,
( spl56_82
<=> ssList(sK43(sK53)) ),
introduced(definition,[new_symbols(definition,[spl56_82])],[avatar_definition]) ).
fof(f76009,plain,
( ssList(sK43(sK53))
| ~ spl56_82 ),
inference(avatar_component_clause,[],[f76008]) ).
fof(f76010,plain,
( ~ ssList(sK43(sK53))
| spl56_82 ),
inference(avatar_component_clause,[],[f76008]) ).
fof(f76016,plain,
( ~ ssList(sK53)
| nil = sK53
| spl56_81 ),
inference(resolution,[],[f76006,f311]) ).
fof(f76017,plain,
( nil = sK53
| spl56_81 ),
inference(forward_subsumption_resolution,[],[f76016,f420]) ).
fof(f76018,plain,
( $false
| spl56_13
| spl56_81 ),
inference(forward_subsumption_resolution,[],[f76017,f1733]) ).
fof(f76019,plain,
( spl56_13
| spl56_81 ),
inference(avatar_contradiction_clause,[],[f76018]) ).
fof(f76077,plain,
( ~ ssList(sK53)
| nil = sK53
| spl56_82 ),
inference(resolution,[],[f76010,f312]) ).
fof(f76078,plain,
( nil = sK53
| spl56_82 ),
inference(forward_subsumption_resolution,[],[f76077,f420]) ).
fof(f76079,plain,
( $false
| spl56_13
| spl56_82 ),
inference(forward_subsumption_resolution,[],[f76078,f1733]) ).
fof(f76080,plain,
( spl56_13
| spl56_82 ),
inference(avatar_contradiction_clause,[],[f76079]) ).
fof(f76572,plain,
( ~ ssList(sK43(sK53))
| frontsegP(nil,sK43(sK53))
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81 ),
inference(forward_subsumption_resolution,[],[f64252,f76005]) ).
fof(f76573,plain,
( frontsegP(nil,sK43(sK53))
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(forward_subsumption_resolution,[],[f76572,f76009]) ).
fof(f76574,plain,
( nil = sK43(sK53)
| ~ ssList(sK43(sK53))
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(resolution,[],[f76573,f347]) ).
fof(f76621,plain,
( nil = sK43(sK53)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(forward_subsumption_resolution,[],[f76574,f76009]) ).
fof(f76647,plain,
( ~ ssList(sK43(sK53))
| sK52 = sK44(sK53)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81 ),
inference(forward_subsumption_resolution,[],[f64253,f76005]) ).
fof(f76648,plain,
( sK52 = sK44(sK53)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(forward_subsumption_resolution,[],[f76647,f76009]) ).
fof(f76888,plain,
( sK53 = cons(sK44(sK53),nil)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(superposition,[],[f62114,f76621]) ).
fof(f76896,plain,
( sK53 = cons(sK52,nil)
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(forward_demodulation,[],[f76888,f76648]) ).
fof(f76897,plain,
( sK49 = sK53
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(forward_demodulation,[],[f76896,f60802]) ).
fof(f76898,plain,
( $false
| ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| spl56_59
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(forward_subsumption_resolution,[],[f76897,f58340]) ).
fof(f76899,plain,
( ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| spl56_59
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(avatar_contradiction_clause,[],[f76898]) ).
fof(f77384,plain,
( ~ frontsegP(sK49,sK49)
| spl56_40
| ~ spl56_59 ),
inference(superposition,[],[f24595,f58339]) ).
fof(f77450,plain,
( $false
| ~ spl56_1
| spl56_2
| spl56_40
| ~ spl56_59 ),
inference(forward_subsumption_resolution,[],[f77384,f3140]) ).
fof(f77451,plain,
( ~ spl56_1
| spl56_2
| spl56_40
| ~ spl56_59 ),
inference(avatar_contradiction_clause,[],[f77450]) ).
fof(f77466,plain,
( sK49 = app(sK49,sK49)
| ~ spl56_41
| ~ spl56_59 ),
inference(forward_demodulation,[],[f24599,f58339]) ).
fof(f77493,plain,
( sK49 != sK49
| ~ ssList(sK49)
| nil = sK49
| ~ spl56_41
| ~ spl56_59 ),
inference(superposition,[],[f3054,f77466]) ).
fof(f77551,plain,
( ~ ssList(sK49)
| nil = sK49
| ~ spl56_41
| ~ spl56_59 ),
inference(trivial_inequality_removal,[],[f77493]) ).
fof(f77568,plain,
( nil = sK49
| ~ spl56_41
| ~ spl56_59 ),
inference(forward_subsumption_resolution,[],[f77551,f431]) ).
fof(f77571,plain,
( $false
| spl56_3
| ~ spl56_41
| ~ spl56_59 ),
inference(forward_subsumption_resolution,[],[f77568,f481]) ).
fof(f77572,plain,
( spl56_3
| ~ spl56_41
| ~ spl56_59 ),
inference(avatar_contradiction_clause,[],[f77571]) ).
cnf(s2,plain,
( spl56_1
| spl56_3 ),
inference(sat_conversion,[],[f483]) ).
cnf(s4,plain,
( spl56_5
| spl56_6 ),
inference(sat_conversion,[],[f497]) ).
cnf(s6,plain,
( ~ spl56_2
| spl56_3
| spl56_8 ),
inference(sat_conversion,[],[f508]) ).
cnf(s13,plain,
( ~ spl56_5
| ~ spl56_15 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s17,plain,
spl56_19,
inference(sat_conversion,[],[f2572]) ).
cnf(s24,plain,
spl56_20,
inference(sat_conversion,[],[f2940]) ).
cnf(s26,plain,
spl56_22,
inference(sat_conversion,[],[f3159]) ).
cnf(s48,plain,
( spl56_38
| ~ spl56_39 ),
inference(sat_conversion,[],[f11286]) ).
cnf(s49,plain,
spl56_39,
inference(sat_conversion,[],[f11297]) ).
cnf(s50,plain,
( ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| ~ spl56_40
| spl56_41 ),
inference(sat_conversion,[],[f24600]) ).
cnf(s73,plain,
( spl56_18
| ~ spl56_19 ),
inference(sat_conversion,[],[f58466]) ).
cnf(s82,plain,
( ~ spl56_3
| spl56_13
| ~ spl56_18
| ~ spl56_20
| ~ spl56_22 ),
inference(sat_conversion,[],[f60376]) ).
cnf(s83,plain,
( ~ spl56_3
| spl56_15
| ~ spl56_20
| ~ spl56_38 ),
inference(sat_conversion,[],[f60381]) ).
cnf(s84,plain,
( ~ spl56_1
| ~ spl56_8 ),
inference(sat_conversion,[],[f60641]) ).
cnf(s86,plain,
( spl56_13
| spl56_74 ),
inference(sat_conversion,[],[f62115]) ).
cnf(s87,plain,
( ~ spl56_6
| ~ spl56_13 ),
inference(sat_conversion,[],[f62198]) ).
cnf(s90,plain,
( ~ spl56_1
| spl56_2
| ~ spl56_13
| spl56_15
| ~ spl56_20 ),
inference(sat_conversion,[],[f64189]) ).
cnf(s109,plain,
( spl56_13
| spl56_81 ),
inference(sat_conversion,[],[f76019]) ).
cnf(s110,plain,
( spl56_13
| spl56_82 ),
inference(sat_conversion,[],[f76080]) ).
cnf(s112,plain,
( ~ spl56_1
| spl56_2
| ~ spl56_20
| ~ spl56_22
| spl56_59
| ~ spl56_74
| ~ spl56_81
| ~ spl56_82 ),
inference(sat_conversion,[],[f76899]) ).
cnf(s120,plain,
( ~ spl56_1
| spl56_2
| spl56_40
| ~ spl56_59 ),
inference(sat_conversion,[],[f77451]) ).
cnf(s122,plain,
( spl56_3
| ~ spl56_41
| ~ spl56_59 ),
inference(sat_conversion,[],[f77572]) ).
cnf(s130,plain,
spl56_38,
inference(rat,[],[s48,s49]) ).
cnf(s140,plain,
spl56_18,
inference(rat,[],[s73,s17]) ).
cnf(s143,plain,
~ spl56_3,
inference(rat,[],[s4,s87,s13,s82,s83,s140,s24,s26,s130]) ).
cnf(s147,plain,
spl56_1,
inference(rat,[],[s2,s143]) ).
cnf(s149,plain,
~ spl56_8,
inference(rat,[],[s84,s147]) ).
cnf(s150,plain,
~ spl56_2,
inference(rat,[],[s6,s143,s149]) ).
cnf(s157,plain,
~ spl56_59,
inference(rat,[],[s50,s120,s122,s24,s26,s147,s150,s143]) ).
cnf(s158,plain,
spl56_13,
inference(rat,[],[s112,s86,s109,s110,s24,s26,s147,s150,s157]) ).
cnf(s160,plain,
~ spl56_6,
inference(rat,[],[s87,s158]) ).
cnf(s161,plain,
spl56_15,
inference(rat,[],[s90,s24,s150,s147,s158]) ).
cnf(s163,plain,
spl56_5,
inference(rat,[],[s4,s160]) ).
cnf(s164,plain,
$false,
inference(rat,[],[s13,s161,s163]) ).
fof(f77573,plain,
$false,
inference(avatar_sat_refutation,[],[s164]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC295+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n001.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 09:01:17 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.25 Running first-order model finding
% 0.10/0.25 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
% 22.89/3.58 % (230696)Will run a generic schedule for satisfiability detection.
% 22.89/3.58 % (230701)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1077801629_2999 on theBenchmark for (2999ds/0Mi)
% 22.89/3.58 % (230702)% WARNING: option uhcvi not known.
% 22.89/3.58 % (230703)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=638751860:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 22.89/3.58 % (230702)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2399994883:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 22.89/3.58 % (230704)dis+10_1_sil=32000:sp=arity:random_seed=3102749674:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 22.89/3.58 % (230707)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1151267925:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 22.89/3.58 % (230705)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1209570410:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 22.89/3.58 % (230706)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4112762653:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 22.89/3.58 % TRYING [1]
% 22.89/3.58 % TRYING [2]
% 22.89/3.58 % TRYING [3]
% 22.89/3.58 % TRYING [4]
% 22.89/3.58 % TRYING [5]
% 22.89/3.58 % (230704)Instruction limit reached!
% 22.89/3.58 % (230704)------------------------------
% 22.89/3.58 % (230704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.89/3.58 % (230704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.89/3.58 % (230704)CaDiCaL version: 2.1.3
% 22.89/3.58 % (230704)Termination reason: Instruction limit
% 22.89/3.58 % (230704)Termination phase: Saturation
% 22.89/3.58 % (230704)Time elapsed: 0.060 s
% 22.89/3.58 % (230704)Peak memory usage: 13 MB
% 22.89/3.58 % (230704)Instructions burned: 104 (million)
% 22.89/3.58 % (230705)Instruction limit reached!
% 22.89/3.58 % (230705)------------------------------
% 22.89/3.58 % (230705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.89/3.58 % (230705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.89/3.58 % (230705)CaDiCaL version: 2.1.3
% 22.89/3.58 % (230705)Termination reason: Instruction limit
% 22.89/3.58 % (230705)Termination phase: Saturation
% 22.89/3.58 % (230705)Time elapsed: 0.069 s
% 22.89/3.58 % (230705)Peak memory usage: 13 MB
% 22.89/3.58 % (230705)Instructions burned: 117 (million)
% 22.89/3.58 % (230706)Instruction limit reached!
% 22.89/3.58 % (230706)------------------------------
% 22.89/3.58 % (230706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.89/3.58 % (230706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.89/3.58 % (230706)CaDiCaL version: 2.1.3
% 22.89/3.58 % (230706)Termination reason: Instruction limit
% 22.89/3.58 % (230706)Termination phase: Saturation
% 22.89/3.58 % (230706)Time elapsed: 0.075 s
% 22.89/3.58 % (230706)Peak memory usage: 13 MB
% 22.89/3.58 % (230706)Instructions burned: 131 (million)
% 22.89/3.58 % (230715)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1477007842:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 22.89/3.58 % (230716)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2437441210:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 22.89/3.58 % (230717)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=916654818:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 22.89/3.58 % TRYING [1]
% 22.89/3.58 % TRYING [2]
% 22.89/3.58 % TRYING [3]
% 22.89/3.58 % TRYING [6]
% 22.89/3.58 % (230707)Instruction limit reached!
% 22.89/3.58 % (230707)------------------------------
% 22.89/3.58 % (230707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.89/3.58 % (230707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.89/3.58 % (230707)CaDiCaL version: 2.1.3
% 22.89/3.58 % (230707)Termination reason: Instruction limit
% 22.89/3.58 % (230707)Termination phase: Saturation
% 22.89/3.58 % (230707)Time elapsed: 0.111 s
% 22.89/3.58 % (230707)Peak memory usage: 14 MB
% 22.89/3.58 % (230707)Instructions burned: 159 (million)
% 22.89/3.58 % TRYING [4]
% 22.89/3.58 % (230721)ott-21_1_sil=16000:fs=off:random_seed=2558703099:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 22.89/3.58 % (230716)Instruction limit reached!
% 22.89/3.58 % (230716)------------------------------
% 22.89/3.58 % (230716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.89/3.58 % (230716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.64 % (230716)CaDiCaL version: 2.1.3
% 13.34/3.64 % (230716)Termination reason: Instruction limit
% 13.34/3.64 % (230716)Termination phase: Saturation
% 13.34/3.64 % (230716)Time elapsed: 0.071 s
% 13.34/3.64 % (230716)Peak memory usage: 13 MB
% 13.34/3.64 % (230716)Instructions burned: 132 (million)
% 13.34/3.64 % TRYING [5]
% 13.34/3.64 % (230723)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2356753018:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 13.34/3.64 % (230721)Instruction limit reached!
% 13.34/3.64 % (230721)------------------------------
% 13.34/3.64 % (230721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.64 % (230721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.64 % (230721)CaDiCaL version: 2.1.3
% 13.34/3.64 % (230721)Termination reason: Instruction limit
% 13.34/3.64 % (230721)Termination phase: Saturation
% 13.34/3.64 % (230721)Time elapsed: 0.089 s
% 13.34/3.64 % (230721)Peak memory usage: 13 MB
% 13.34/3.64 % (230721)Instructions burned: 181 (million)
% 13.34/3.64 % (230725)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2578311913:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 13.34/3.64 % TRYING [1]
% 13.34/3.64 % TRYING [2]
% 13.34/3.64 % TRYING [7]
% 13.34/3.64 % TRYING [3]
% 13.34/3.64 % TRYING [4]
% 13.34/3.64 % TRYING [6]
% 13.34/3.64 % (230715)Instruction limit reached!
% 13.34/3.64 % (230715)------------------------------
% 13.34/3.64 % (230715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.64 % (230715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.64 % (230715)CaDiCaL version: 2.1.3
% 13.34/3.64 % (230715)Termination reason: Instruction limit
% 13.34/3.64 % (230715)Termination phase: Finite model building constraint generation
% 13.34/3.64 % (230715)Time elapsed: 0.301 s
% 13.34/3.64 % (230715)Peak memory usage: 28 MB
% 13.34/3.64 % (230715)Instructions burned: 718 (million)
% 13.34/3.64 % (230727)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=399563975:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 13.34/3.64 % TRYING [5]
% 13.34/3.64 % (230717)Instruction limit reached!
% 13.34/3.64 % (230717)------------------------------
% 13.34/3.64 % (230717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.64 % (230717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.64 % (230717)CaDiCaL version: 2.1.3
% 13.34/3.64 % (230717)Termination reason: Instruction limit
% 13.34/3.64 % (230717)Termination phase: Saturation
% 13.34/3.64 % (230717)Time elapsed: 0.373 s
% 13.34/3.64 % (230717)Peak memory usage: 22 MB
% 13.34/3.64 % (230717)Instructions burned: 684 (million)
% 13.34/3.64 % (230729)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=915485612:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 13.34/3.64 % (230723)Instruction limit reached!
% 13.34/3.64 % (230723)------------------------------
% 13.34/3.64 % (230723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.64 % (230723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.64 % (230723)CaDiCaL version: 2.1.3
% 13.34/3.64 % (230723)Termination reason: Instruction limit
% 13.34/3.64 % (230723)Termination phase: Saturation
% 13.34/3.64 % (230723)Time elapsed: 0.326 s
% 13.34/3.64 % (230723)Peak memory usage: 14 MB
% 13.34/3.64 % (230723)Instructions burned: 478 (million)
% 13.34/3.64 % (230731)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=3733833301: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)
% 13.34/3.65 % (230725)Instruction limit reached!
% 13.34/3.65 % (230725)------------------------------
% 13.34/3.65 % (230725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230725)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230725)Termination reason: Instruction limit
% 13.34/3.65 % (230725)Termination phase: Finite model building SAT solving
% 13.34/3.65 % (230725)Time elapsed: 0.345 s
% 13.34/3.65 % (230725)Peak memory usage: 22 MB
% 13.34/3.65 % (230725)Instructions burned: 867 (million)
% 13.34/3.65 % TRYING [14]
% 13.34/3.65 % (230733)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3711664526:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 13.34/3.65 % TRYING [8]
% 13.34/3.65 % (230729)Instruction limit reached!
% 13.34/3.65 % (230729)------------------------------
% 13.34/3.65 % (230729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230729)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230729)Termination reason: Instruction limit
% 13.34/3.65 % (230729)Termination phase: Finite model building constraint generation
% 13.34/3.65 % (230729)Time elapsed: 0.323 s
% 13.34/3.65 % (230729)Peak memory usage: 70 MB
% 13.34/3.65 % (230729)Instructions burned: 892 (million)
% 13.34/3.65 % (230735)fmb+10_1_sil=64000:random_seed=1052487332:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 13.34/3.65 % TRYING [1]
% 13.34/3.65 % TRYING [2]
% 13.34/3.65 % TRYING [3]
% 13.34/3.65 % (230731)Instruction limit reached!
% 13.34/3.65 % (230731)------------------------------
% 13.34/3.65 % (230731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230731)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230731)Termination reason: Instruction limit
% 13.34/3.65 % (230731)Termination phase: Saturation
% 13.34/3.65 % (230731)Time elapsed: 0.360 s
% 13.34/3.65 % (230731)Peak memory usage: 22 MB
% 13.34/3.65 % (230731)Instructions burned: 693 (million)
% 13.34/3.65 % (230737)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2441415209:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 13.34/3.65 % TRYING [4]
% 13.34/3.65 % TRYING [20]
% 13.34/3.65 % TRYING [5]
% 13.34/3.65 % (230727)Instruction limit reached!
% 13.34/3.65 % (230727)------------------------------
% 13.34/3.65 % (230727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230727)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230727)Termination reason: Instruction limit
% 13.34/3.65 % (230727)Termination phase: Saturation
% 13.34/3.65 % (230727)Time elapsed: 0.653 s
% 13.34/3.65 % (230727)Peak memory usage: 25 MB
% 13.34/3.65 % (230727)Instructions burned: 1180 (million)
% 13.34/3.65 % (230739)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3810741883:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 13.34/3.65 % (230733)Instruction limit reached!
% 13.34/3.65 % (230733)------------------------------
% 13.34/3.65 % (230733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230733)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230733)Termination reason: Instruction limit
% 13.34/3.65 % (230733)Termination phase: Saturation
% 13.34/3.65 % (230733)Time elapsed: 0.481 s
% 13.34/3.65 % (230733)Peak memory usage: 20 MB
% 13.34/3.65 % (230733)Instructions burned: 880 (million)
% 13.34/3.65 % TRYING [8]
% 13.34/3.65 % (230741)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=979510743:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 13.34/3.65 % TRYING [6]
% 13.34/3.65 % (230739)Instruction limit reached!
% 13.34/3.65 % (230739)------------------------------
% 13.34/3.65 % (230739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230739)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230739)Termination reason: Instruction limit
% 13.34/3.65 % (230739)Termination phase: Finite model building constraint generation
% 13.34/3.65 % (230739)Time elapsed: 0.342 s
% 13.34/3.65 % (230739)Peak memory usage: 69 MB
% 13.34/3.65 % (230739)Instructions burned: 922 (million)
% 13.34/3.65 % (230743)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3609414998:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 13.34/3.65 % TRYING [9]
% 13.34/3.65 % TRYING [7]
% 13.34/3.65 % (230743)Instruction limit reached!
% 13.34/3.65 % (230743)------------------------------
% 13.34/3.65 % (230743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230743)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230743)Termination reason: Instruction limit
% 13.34/3.65 % (230743)Termination phase: Saturation
% 13.34/3.65 % (230743)Time elapsed: 0.647 s
% 13.34/3.65 % (230743)Peak memory usage: 16 MB
% 13.34/3.65 % (230743)Instructions burned: 1472 (million)
% 13.34/3.65 % (230745)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3579640092:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 13.34/3.65 % TRYING [77]
% 13.34/3.65 % (230741) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-230696-230741"...
% 13.34/3.65 % (230741)...printing done.
% 13.34/3.65 % (230741)Refutation found. Thanks to Tanya!
% 13.34/3.65 % SZS status Theorem for theBenchmark
% 13.34/3.65 % SZS output start Proof for theBenchmark
% See solution above
% 13.34/3.65 % (230741)------------------------------
% 13.34/3.65 % (230741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.34/3.65 % (230741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.65 % (230741)CaDiCaL version: 2.1.3
% 13.34/3.65 % (230741)Termination reason: Refutation
% 13.34/3.65 % (230741)Time elapsed: 2.150 s
% 13.34/3.65 % (230741)Peak memory usage: 42 MB
% 13.34/3.65 % (230741)Instructions burned: 3975 (million)
% 13.34/3.65 % (230696)Success in time 3.382 s
% 13.34/3.65 % Vampire exiting
%------------------------------------------------------------------------------