%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC187+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:05:01 PM UTC 2026
% Result : Theorem 6.38s 1.91s
% Output : Refutation 6.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 60
% Syntax : Number of formulae : 443 ( 51 unt; 35 def)
% Number of atoms : 1634 ( 178 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 2192 (1001 ~;1018 |; 54 &)
% ( 54 <=>; 65 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 36 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 302 ( 0 sgn 268 !; 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/sandbox2/benchmark/Axioms/SWC001+0.ax',ax3) ).
fof(f4,axiom,
! [X0] :
( ssList(X0)
=> ( singletonP(X0)
<=> ? [X1] :
( ssItem(X1)
& cons(X1,nil) = X0 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax4) ).
fof(f5,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( frontsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X1,X2) = X0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax5) ).
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/sandbox2/benchmark/Axioms/SWC001+0.ax',ax7) ).
fof(f8,axiom,
! [X0] :
( ssList(X0)
=> ( cyclefreeP(X0)
<=> ! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssList(X3)
=> ! [X4] :
( ssList(X4)
=> ! [X5] :
( ssList(X5)
=> ( app(app(X3,cons(X1,X4)),cons(X2,X5)) = X0
=> ~ ( leq(X1,X2)
& leq(X2,X1) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax8) ).
fof(f16,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ssList(cons(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax16) ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SWC001+0.ax',ax20) ).
fof(f26,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ssList(app(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax26) ).
fof(f28,axiom,
! [X0] :
( ssList(X0)
=> app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax28) ).
fof(f31,axiom,
! [X0] :
( ssItem(X0)
=> leq(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax31) ).
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/sandbox2/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/sandbox2/benchmark/Axioms/SWC001+0.ax',ax37) ).
fof(f38,axiom,
! [X0] :
( ssItem(X0)
=> ~ memberP(nil,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax38) ).
fof(f39,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax39) ).
fof(f41,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( ( frontsegP(X0,X1)
& frontsegP(X1,X0) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SWC001+0.ax',ax44) ).
fof(f45,axiom,
! [X0] :
( ssList(X0)
=> frontsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax45) ).
fof(f58,axiom,
! [X0] :
( ssList(X0)
=> ( segmentP(nil,X0)
<=> nil = X0 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax58) ).
fof(f59,axiom,
! [X0] :
( ssItem(X0)
=> cyclefreeP(cons(X0,nil)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax59) ).
fof(f80,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( app(X1,X2) = app(X1,X0)
=> X2 = X0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax80) ).
fof(f81,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> cons(X1,X0) = app(cons(X1,nil),X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax81) ).
fof(f84,axiom,
! [X0] :
( ssList(X0)
=> app(X0,nil) = X0 ),
file('/export/starexec/sandbox2/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
| ( ~ memberP(X5,X4)
& ~ memberP(X6,X4) ) ) ) ) )
| ( ! [X7] :
( ssItem(X7)
=> ( cons(X7,nil) != X2
| ~ memberP(X3,X7) ) )
& ( nil != X3
| nil != X2 ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/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
| ( ~ memberP(X5,X4)
& ~ memberP(X6,X4) ) ) ) ) )
| ( ! [X7] :
( ssItem(X7)
=> ( cons(X7,nil) != X2
| ~ memberP(X3,X7) ) )
& ( 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(f100,plain,
! [X0] :
( ( singletonP(X0)
<=> ? [X1] :
( ssItem(X1)
& cons(X1,nil) = X0 ) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f101,plain,
! [X0] :
( ! [X1] :
( ( frontsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X1,X2) = X0 ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f5]) ).
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(f104,plain,
! [X0] :
( ( cyclefreeP(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ leq(X1,X2)
| ~ leq(X2,X1)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5) )
| ~ ssList(X4) )
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ~ ssItem(X1) ) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f105,plain,
! [X0] :
( ( cyclefreeP(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ leq(X1,X2)
| ~ leq(X2,X1)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5) )
| ~ ssList(X4) )
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ~ ssItem(X1) ) )
| ~ ssList(X0) ),
inference(flattening,[],[f104]) ).
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(f139,plain,
! [X0] :
( leq(X0,X0)
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f31]) ).
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(f176,plain,
! [X0] :
( ( segmentP(nil,X0)
<=> nil = X0 )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f58]) ).
fof(f177,plain,
! [X0] :
( cyclefreeP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f59]) ).
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(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] :
( ? [X5] :
( ? [X6] :
( app(app(X5,cons(X4,nil)),X6) = X0
& ( memberP(X5,X4)
| memberP(X6,X4) )
& ssList(X6) )
& ssList(X5) )
& ssItem(X4) )
& ( ? [X7] :
( cons(X7,nil) = X2
& memberP(X3,X7)
& ssItem(X7) )
| ( 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
& ( memberP(X5,X4)
| memberP(X6,X4) )
& ssList(X6) )
& ssList(X5) )
& ssItem(X4) )
& ( ? [X7] :
( cons(X7,nil) = X2
& memberP(X3,X7)
& ssItem(X7) )
| ( nil = X3
& nil = X2 ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(flattening,[],[f221]) ).
fof(f229,plain,
! [X0,X1] :
( ~ memberP(X0,X1)
| ~ ssItem(X1)
| app(sK2(X0,X1),cons(X1,sK3(X0,X1))) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f230,plain,
! [X0,X1] :
( ssList(sK3(X0,X1))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f231,plain,
! [X0,X1] :
( ssList(sK2(X0,X1))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f234,plain,
! [X0,X1] :
( ~ ssList(X0)
| cons(X1,nil) != X0
| ~ ssItem(X1)
| singletonP(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| app(X1,X2) != X0
| ~ ssList(X2)
| frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
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(f245,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ ssList(X5)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ leq(X2,X1)
| ~ leq(X1,X2)
| ~ cyclefreeP(X0) ),
inference(cnf_transformation,[],[f105]) ).
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(f323,plain,
! [X0] :
( ~ ssItem(X0)
| leq(X0,X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f331,plain,
! [X2,X0,X1] :
( ~ memberP(X2,X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssItem(X0)
| memberP(app(X1,X2),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(f335,plain,
! [X2,X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| X0 != X1
| memberP(cons(X1,X2),X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f336,plain,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f337,plain,
~ singletonP(nil),
inference(cnf_transformation,[],[f39]) ).
fof(f339,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f341,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
inference(cnf_transformation,[],[f155]) ).
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(f361,plain,
! [X0] :
( ~ segmentP(nil,X0)
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f362,plain,
! [X0] :
( cyclefreeP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f177]) ).
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(f392,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ~ ssList(X0)
| 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,
( memberP(sK54,sK51)
| memberP(sK53,sK51) ),
inference(cnf_transformation,[],[f222]) ).
fof(f412,plain,
ssList(sK54),
inference(cnf_transformation,[],[f222]) ).
fof(f413,plain,
sK47 = app(app(sK53,cons(sK51,nil)),sK54),
inference(cnf_transformation,[],[f222]) ).
fof(f414,plain,
ssList(sK53),
inference(cnf_transformation,[],[f222]) ).
fof(f418,plain,
( nil = sK49
| ssItem(sK52) ),
inference(cnf_transformation,[],[f222]) ).
fof(f420,plain,
( nil = sK49
| sK49 = cons(sK52,nil) ),
inference(cnf_transformation,[],[f222]) ).
fof(f421,plain,
ssItem(sK51),
inference(cnf_transformation,[],[f222]) ).
fof(f423,plain,
sK47 = sK49,
inference(cnf_transformation,[],[f222]) ).
fof(f425,plain,
ssList(sK49),
inference(cnf_transformation,[],[f222]) ).
fof(f430,plain,
sK49 = app(app(sK53,cons(sK51,nil)),sK54),
inference(definition_unfolding,[],[f413,f423]) ).
fof(f433,plain,
! [X1] :
( ~ ssList(cons(X1,nil))
| ~ ssItem(X1)
| singletonP(cons(X1,nil)) ),
inference(equality_resolution,[],[f234]) ).
fof(f434,plain,
! [X2,X1] :
( ~ ssList(app(X1,X2))
| ~ ssList(X1)
| ~ ssList(X2)
| frontsegP(app(X1,X2),X1) ),
inference(equality_resolution,[],[f237]) ).
fof(f436,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(f437,plain,
! [X2,X3,X1,X4,X5] :
( ~ ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ ssList(X5)
| ~ leq(X2,X1)
| ~ leq(X1,X2)
| ~ cyclefreeP(app(app(X3,cons(X1,X4)),cons(X2,X5))) ),
inference(equality_resolution,[],[f245]) ).
fof(f446,plain,
! [X2,X1] :
( ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f335]) ).
fof(f447,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(f456,plain,
! [X1] :
( ~ singletonP(cons(X1,nil))
| ~ ssItem(X1)
| ~ ssList(cons(X1,nil)) ),
inference(consistent_polarity_flipping,[],[f433]) ).
fof(f461,plain,
! [X2,X3,X1,X4,X5] :
( ~ cyclefreeP(app(app(X3,cons(X1,X4)),cons(X2,X5)))
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ ssList(X5)
| leq(X2,X1)
| leq(X1,X2)
| ~ ssList(app(app(X3,cons(X1,X4)),cons(X2,X5))) ),
inference(consistent_polarity_flipping,[],[f437]) ).
fof(f486,plain,
! [X0] :
( ~ leq(X0,X0)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f493,plain,
singletonP(nil),
inference(consistent_polarity_flipping,[],[f337]) ).
fof(f517,plain,
! [X2,X3,X1] :
( ~ frontsegP(X2,X3)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssItem(X1)
| frontsegP(cons(X1,X2),cons(X1,X3)) ),
inference(duplicate_literal_removal,[],[f447]) ).
fof(f518,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssList(X2)
| ~ ssItem(X1) ),
inference(duplicate_literal_removal,[],[f446]) ).
fof(f523,definition,
( spl55_1
<=> memberP(sK53,sK51) ),
introduced(definition,[new_symbols(definition,[spl55_1])],[avatar_definition]) ).
fof(f524,plain,
( ~ memberP(sK53,sK51)
| spl55_1 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( memberP(sK53,sK51)
| ~ spl55_1 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl55_2
<=> memberP(sK54,sK51) ),
introduced(definition,[new_symbols(definition,[spl55_2])],[avatar_definition]) ).
fof(f529,plain,
( memberP(sK54,sK51)
| ~ spl55_2 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f530,plain,
( spl55_1
| spl55_2 ),
inference(avatar_split_clause,[],[f411,f527,f523]) ).
fof(f532,definition,
( spl55_3
<=> ssItem(sK52) ),
introduced(definition,[new_symbols(definition,[spl55_3])],[avatar_definition]) ).
fof(f534,plain,
( ssItem(sK52)
| ~ spl55_3 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f546,definition,
( spl55_6
<=> sK49 = cons(sK52,nil) ),
introduced(definition,[new_symbols(definition,[spl55_6])],[avatar_definition]) ).
fof(f548,plain,
( sK49 = cons(sK52,nil)
| ~ spl55_6 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f551,definition,
( spl55_7
<=> nil = sK49 ),
introduced(definition,[new_symbols(definition,[spl55_7])],[avatar_definition]) ).
fof(f553,plain,
( nil = sK49
| ~ spl55_7 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f554,plain,
( spl55_3
| spl55_7 ),
inference(avatar_split_clause,[],[f418,f551,f532]) ).
fof(f556,plain,
( spl55_6
| spl55_7 ),
inference(avatar_split_clause,[],[f420,f551,f546]) ).
fof(f562,definition,
( spl55_9
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl55_9])],[avatar_definition]) ).
fof(f563,plain,
( ssList(nil)
| ~ spl55_9 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f591,plain,
spl55_9,
inference(avatar_split_clause,[],[f306,f562]) ).
fof(f592,plain,
( cyclefreeP(sK49)
| ~ ssItem(sK52)
| ~ spl55_6 ),
inference(superposition,[],[f362,f548]) ).
fof(f593,plain,
( cyclefreeP(sK49)
| ~ spl55_3
| ~ spl55_6 ),
inference(forward_subsumption_resolution,[],[f592,f534]) ).
fof(f621,plain,
sK49 = app(nil,sK49),
inference(resolution,[],[f320,f425]) ).
fof(f640,plain,
sK49 = app(sK49,nil),
inference(resolution,[],[f397,f425]) ).
fof(f686,plain,
( memberP(sK49,sK52)
| ~ ssList(nil)
| ~ ssItem(sK52)
| ~ spl55_6 ),
inference(superposition,[],[f518,f548]) ).
fof(f687,plain,
( memberP(sK49,sK52)
| ~ ssItem(sK52)
| ~ spl55_6
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f686,f563]) ).
fof(f688,plain,
( memberP(sK49,sK52)
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f687,f534]) ).
fof(f770,definition,
( spl55_16
<=> nil = sK54 ),
introduced(definition,[new_symbols(definition,[spl55_16])],[avatar_definition]) ).
fof(f771,plain,
( nil != sK54
| spl55_16 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f772,plain,
( nil = sK54
| ~ spl55_16 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f779,definition,
( spl55_18
<=> nil = sK53 ),
introduced(definition,[new_symbols(definition,[spl55_18])],[avatar_definition]) ).
fof(f780,plain,
( nil != sK53
| spl55_18 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f781,plain,
( nil = sK53
| ~ spl55_18 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f833,plain,
( memberP(nil,sK51)
| ~ spl55_2
| ~ spl55_16 ),
inference(superposition,[],[f529,f772]) ).
fof(f861,definition,
( spl55_25
<=> cyclefreeP(sK49) ),
introduced(definition,[new_symbols(definition,[spl55_25])],[avatar_definition]) ).
fof(f863,plain,
( cyclefreeP(sK49)
| ~ spl55_25 ),
inference(avatar_component_clause,[],[f861]) ).
fof(f897,definition,
( spl55_32
<=> memberP(sK49,sK52) ),
introduced(definition,[new_symbols(definition,[spl55_32])],[avatar_definition]) ).
fof(f899,plain,
( memberP(sK49,sK52)
| ~ spl55_32 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f1007,plain,
( sK53 = cons(sK44(sK53),sK43(sK53))
| nil = sK53 ),
inference(resolution,[],[f310,f414]) ).
fof(f1060,plain,
( ~ ssItem(sK51)
| ~ spl55_2
| ~ spl55_16 ),
inference(resolution,[],[f833,f336]) ).
fof(f1061,plain,
( $false
| ~ spl55_2
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f1060,f421]) ).
fof(f1062,plain,
( ~ spl55_2
| ~ spl55_16 ),
inference(avatar_contradiction_clause,[],[f1061]) ).
fof(f1063,plain,
( memberP(nil,sK51)
| ~ spl55_1
| ~ spl55_18 ),
inference(forward_demodulation,[],[f525,f781]) ).
fof(f1065,plain,
( ~ ssItem(sK51)
| ~ spl55_1
| ~ spl55_18 ),
inference(resolution,[],[f1063,f336]) ).
fof(f1066,plain,
( $false
| ~ spl55_1
| ~ spl55_18 ),
inference(forward_subsumption_resolution,[],[f1065,f421]) ).
fof(f1067,plain,
( ~ spl55_1
| ~ spl55_18 ),
inference(avatar_contradiction_clause,[],[f1066]) ).
fof(f1069,definition,
( spl55_35
<=> sK53 = cons(sK44(sK53),sK43(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_35])],[avatar_definition]) ).
fof(f1071,plain,
( sK53 = cons(sK44(sK53),sK43(sK53))
| ~ spl55_35 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1072,plain,
( spl55_18
| spl55_35 ),
inference(avatar_split_clause,[],[f1007,f1069,f779]) ).
fof(f1079,definition,
( spl55_37
<=> ssList(app(sK53,cons(sK51,nil))) ),
introduced(definition,[new_symbols(definition,[spl55_37])],[avatar_definition]) ).
fof(f1080,plain,
( ssList(app(sK53,cons(sK51,nil)))
| ~ spl55_37 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1081,plain,
( ~ ssList(app(sK53,cons(sK51,nil)))
| spl55_37 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1141,plain,
! [X2,X1] :
( frontsegP(app(X1,X2),X1)
| ~ ssList(X2)
| ~ ssList(X1) ),
inference(forward_subsumption_resolution,[],[f434,f318]) ).
fof(f1142,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X1)
| ~ frontsegP(X1,app(X1,X0))
| ~ ssList(app(X1,X0))
| app(X1,X0) = X1 ),
inference(resolution,[],[f1141,f339]) ).
fof(f1144,plain,
( frontsegP(sK49,app(sK53,cons(sK51,nil)))
| ~ ssList(sK54)
| ~ ssList(app(sK53,cons(sK51,nil))) ),
inference(superposition,[],[f1141,f430]) ).
fof(f1156,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X1,app(X1,X0))
| ~ ssList(app(X1,X0))
| app(X1,X0) = X1 ),
inference(duplicate_literal_removal,[],[f1142]) ).
fof(f1157,plain,
( frontsegP(sK49,app(sK53,cons(sK51,nil)))
| ~ ssList(app(sK53,cons(sK51,nil))) ),
inference(forward_subsumption_resolution,[],[f1144,f412]) ).
fof(f1159,plain,
! [X0,X1] :
( ~ frontsegP(X1,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| app(X1,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f1156,f318]) ).
fof(f1278,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssList(sK54)
| ~ ssItem(sK51)
| memberP(app(X0,sK54),sK51) )
| ~ spl55_2 ),
inference(resolution,[],[f331,f529]) ).
fof(f1280,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssItem(sK51)
| memberP(app(X0,sK54),sK51) )
| ~ spl55_2 ),
inference(forward_subsumption_resolution,[],[f1278,f412]) ).
fof(f1282,plain,
( ! [X0] :
( memberP(app(X0,sK54),sK51)
| ~ ssList(X0) )
| ~ spl55_2 ),
inference(forward_subsumption_resolution,[],[f1280,f421]) ).
fof(f1303,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X0,X2))
| frontsegP(app(app(X0,X2),X1),X0)
| ~ ssList(X2)
| ~ ssList(X0) ),
inference(resolution,[],[f341,f1141]) ).
fof(f1304,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X0,X2))
| frontsegP(app(app(X0,X2),X1),X0)
| ~ ssList(X2) ),
inference(duplicate_literal_removal,[],[f1303]) ).
fof(f1308,plain,
! [X2,X0,X1] :
( frontsegP(app(app(X0,X2),X1),X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1304,f318]) ).
fof(f1566,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,f430]) ).
fof(f1588,plain,
! [X0] :
( sK49 != app(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ ssList(X0)
| sK54 = X0 ),
inference(forward_subsumption_resolution,[],[f1566,f412]) ).
fof(f1667,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(nil)
| ~ ssItem(X1)
| frontsegP(cons(X1,X0),cons(X1,nil))
| ~ ssList(X0) ),
inference(resolution,[],[f517,f345]) ).
fof(f1670,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(nil)
| ~ ssItem(X1)
| frontsegP(cons(X1,X0),cons(X1,nil)) ),
inference(duplicate_literal_removal,[],[f1667]) ).
fof(f1674,plain,
( ! [X0,X1] :
( frontsegP(cons(X1,X0),cons(X1,nil))
| ~ ssItem(X1)
| ~ ssList(X0) )
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f1670,f563]) ).
fof(f1745,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssItem(sK52)
| ~ ssList(nil)
| memberP(nil,X0)
| sK52 = X0
| ~ ssItem(X0) )
| ~ spl55_6 ),
inference(superposition,[],[f333,f548]) ).
fof(f1784,plain,
( ~ ssItem(sK51)
| sK53 = app(sK2(sK53,sK51),cons(sK51,sK3(sK53,sK51)))
| ~ ssList(sK53)
| ~ spl55_1 ),
inference(resolution,[],[f229,f525]) ).
fof(f1787,plain,
( sK53 = app(sK2(sK53,sK51),cons(sK51,sK3(sK53,sK51)))
| ~ ssList(sK53)
| ~ spl55_1 ),
inference(forward_subsumption_resolution,[],[f1784,f421]) ).
fof(f1790,plain,
( sK53 = app(sK2(sK53,sK51),cons(sK51,sK3(sK53,sK51)))
| ~ spl55_1 ),
inference(forward_subsumption_resolution,[],[f1787,f414]) ).
fof(f1837,plain,
( ~ ssList(cons(sK51,nil))
| ~ ssList(sK53)
| spl55_37 ),
inference(resolution,[],[f1081,f318]) ).
fof(f1838,plain,
( ~ ssList(cons(sK51,nil))
| spl55_37 ),
inference(forward_subsumption_resolution,[],[f1837,f414]) ).
fof(f1844,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| sK52 = X0
| ~ ssItem(sK52) )
| ~ spl55_6 ),
inference(superposition,[],[f343,f548]) ).
fof(f1855,plain,
( ~ ssItem(sK51)
| ~ ssList(nil)
| spl55_37 ),
inference(resolution,[],[f1838,f305]) ).
fof(f1856,plain,
( ~ ssList(nil)
| spl55_37 ),
inference(forward_subsumption_resolution,[],[f1855,f421]) ).
fof(f1857,plain,
( $false
| ~ spl55_9
| spl55_37 ),
inference(forward_subsumption_resolution,[],[f1856,f563]) ).
fof(f1858,plain,
( ~ spl55_9
| spl55_37 ),
inference(avatar_contradiction_clause,[],[f1857]) ).
fof(f1878,plain,
( ~ ssList(sK49)
| ~ ssList(cons(sK51,nil))
| ~ ssList(sK54)
| ~ ssList(sK53)
| segmentP(sK49,cons(sK51,nil)) ),
inference(superposition,[],[f436,f430]) ).
fof(f1881,plain,
( ~ ssList(cons(sK51,nil))
| ~ ssList(sK54)
| ~ ssList(sK53)
| segmentP(sK49,cons(sK51,nil)) ),
inference(forward_subsumption_resolution,[],[f1878,f425]) ).
fof(f1888,plain,
( ~ ssList(cons(sK51,nil))
| ~ ssList(sK53)
| segmentP(sK49,cons(sK51,nil)) ),
inference(forward_subsumption_resolution,[],[f1881,f412]) ).
fof(f1894,plain,
( ~ ssList(cons(sK51,nil))
| segmentP(sK49,cons(sK51,nil)) ),
inference(forward_subsumption_resolution,[],[f1888,f414]) ).
fof(f1899,plain,
( segmentP(nil,cons(sK51,nil))
| ~ ssList(cons(sK51,nil))
| ~ spl55_7 ),
inference(forward_demodulation,[],[f1894,f553]) ).
fof(f1905,definition,
( spl55_54
<=> ssList(cons(sK51,nil)) ),
introduced(definition,[new_symbols(definition,[spl55_54])],[avatar_definition]) ).
fof(f1906,plain,
( ssList(cons(sK51,nil))
| ~ spl55_54 ),
inference(avatar_component_clause,[],[f1905]) ).
fof(f1907,plain,
( ~ ssList(cons(sK51,nil))
| spl55_54 ),
inference(avatar_component_clause,[],[f1905]) ).
fof(f1909,definition,
( spl55_55
<=> segmentP(nil,cons(sK51,nil)) ),
introduced(definition,[new_symbols(definition,[spl55_55])],[avatar_definition]) ).
fof(f1911,plain,
( segmentP(nil,cons(sK51,nil))
| ~ spl55_55 ),
inference(avatar_component_clause,[],[f1909]) ).
fof(f1912,plain,
( ~ spl55_54
| spl55_55
| ~ spl55_7 ),
inference(avatar_split_clause,[],[f1899,f551,f1909,f1905]) ).
fof(f1913,plain,
( ~ ssItem(sK51)
| ~ ssList(nil)
| spl55_54 ),
inference(resolution,[],[f1907,f305]) ).
fof(f1914,plain,
( ~ ssList(nil)
| spl55_54 ),
inference(forward_subsumption_resolution,[],[f1913,f421]) ).
fof(f1915,plain,
( $false
| ~ spl55_9
| spl55_54 ),
inference(forward_subsumption_resolution,[],[f1914,f563]) ).
fof(f1916,plain,
( ~ spl55_9
| spl55_54 ),
inference(avatar_contradiction_clause,[],[f1915]) ).
fof(f1931,definition,
( spl55_57
<=> nil = cons(sK51,nil) ),
introduced(definition,[new_symbols(definition,[spl55_57])],[avatar_definition]) ).
fof(f1933,plain,
( nil = cons(sK51,nil)
| ~ spl55_57 ),
inference(avatar_component_clause,[],[f1931]) ).
fof(f1950,plain,
( nil = cons(sK51,nil)
| ~ ssList(cons(sK51,nil))
| ~ spl55_55 ),
inference(resolution,[],[f1911,f361]) ).
fof(f1963,plain,
( nil = cons(sK51,nil)
| ~ spl55_54
| ~ spl55_55 ),
inference(forward_subsumption_resolution,[],[f1950,f1906]) ).
fof(f1970,plain,
( spl55_57
| ~ spl55_54
| ~ spl55_55 ),
inference(avatar_split_clause,[],[f1963,f1909,f1905,f1931]) ).
fof(f1985,plain,
( ~ singletonP(nil)
| ~ ssItem(sK51)
| ~ ssList(nil)
| ~ spl55_57 ),
inference(superposition,[],[f456,f1933]) ).
fof(f2012,plain,
( ~ ssItem(sK51)
| ~ ssList(nil)
| ~ spl55_57 ),
inference(forward_subsumption_resolution,[],[f1985,f493]) ).
fof(f2024,plain,
( ~ ssList(nil)
| ~ spl55_57 ),
inference(forward_subsumption_resolution,[],[f2012,f421]) ).
fof(f2028,plain,
( $false
| ~ spl55_9
| ~ spl55_57 ),
inference(forward_subsumption_resolution,[],[f2024,f563]) ).
fof(f2029,plain,
( ~ spl55_9
| ~ spl55_57 ),
inference(avatar_contradiction_clause,[],[f2028]) ).
fof(f2031,plain,
( spl55_25
| ~ spl55_3
| ~ spl55_6 ),
inference(avatar_split_clause,[],[f593,f546,f532,f861]) ).
fof(f2039,plain,
( spl55_32
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f688,f562,f546,f532,f897]) ).
fof(f2054,definition,
( spl55_64
<=> frontsegP(sK49,app(sK53,cons(sK51,nil))) ),
introduced(definition,[new_symbols(definition,[spl55_64])],[avatar_definition]) ).
fof(f2056,plain,
( frontsegP(sK49,app(sK53,cons(sK51,nil)))
| ~ spl55_64 ),
inference(avatar_component_clause,[],[f2054]) ).
fof(f2057,plain,
( ~ spl55_37
| spl55_64 ),
inference(avatar_split_clause,[],[f1157,f2054,f1079]) ).
fof(f2082,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssItem(sK52)
| memberP(nil,X0)
| sK52 = X0
| ~ ssItem(X0) )
| ~ spl55_6
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f1745,f563]) ).
fof(f2090,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ~ ssList(X1)
| sK52 = X0
| ~ ssItem(sK52) )
| ~ spl55_6
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f1844,f563]) ).
fof(f2117,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssItem(sK52)
| sK52 = X0
| ~ ssItem(X0) )
| ~ spl55_6
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f2082,f336]) ).
fof(f2142,definition,
( spl55_78
<=> ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| sK52 = X0
| ~ ssList(X1)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_78])],[avatar_definition]) ).
fof(f2143,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| sK52 = X0
| ~ ssList(X1)
| ~ ssItem(X0) )
| ~ spl55_78 ),
inference(avatar_component_clause,[],[f2142]) ).
fof(f2144,plain,
( ~ spl55_3
| spl55_78
| ~ spl55_6
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f2090,f562,f546,f2142,f532]) ).
fof(f2154,definition,
( spl55_81
<=> ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssItem(X0)
| sK52 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl55_81])],[avatar_definition]) ).
fof(f2155,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ~ ssItem(X0)
| sK52 = X0 )
| ~ spl55_81 ),
inference(avatar_component_clause,[],[f2154]) ).
fof(f2156,plain,
( ~ spl55_3
| spl55_81
| ~ spl55_6
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f2117,f562,f546,f2154,f532]) ).
fof(f2160,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sK52,X0) = app(cons(sK52,nil),X0) )
| ~ spl55_3 ),
inference(resolution,[],[f534,f392]) ).
fof(f2164,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sK52,X0) = app(sK49,X0) )
| ~ spl55_3
| ~ spl55_6 ),
inference(forward_demodulation,[],[f2160,f548]) ).
fof(f2198,plain,
( ! [X2,X0,X1] :
( ~ cyclefreeP(app(app(X0,cons(X1,X2)),sK49))
| ~ ssItem(X1)
| ~ ssItem(sK52)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(nil)
| leq(sK52,X1)
| leq(X1,sK52)
| ~ ssList(app(app(X0,cons(X1,X2)),sK49)) )
| ~ spl55_6 ),
inference(superposition,[],[f461,f548]) ).
fof(f2200,plain,
( ! [X2,X0,X1] :
( ~ cyclefreeP(app(app(X0,cons(X1,X2)),sK49))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(nil)
| leq(sK52,X1)
| leq(X1,sK52)
| ~ ssList(app(app(X0,cons(X1,X2)),sK49)) )
| ~ spl55_3
| ~ spl55_6 ),
inference(forward_subsumption_resolution,[],[f2198,f534]) ).
fof(f2202,plain,
( ! [X2,X0,X1] :
( ~ cyclefreeP(app(app(X0,cons(X1,X2)),sK49))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| leq(sK52,X1)
| leq(X1,sK52)
| ~ ssList(app(app(X0,cons(X1,X2)),sK49)) )
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f2200,f563]) ).
fof(f2421,plain,
( memberP(sK53,sK44(sK53))
| ~ ssList(sK43(sK53))
| ~ ssItem(sK44(sK53))
| ~ spl55_35 ),
inference(superposition,[],[f518,f1071]) ).
fof(f2425,definition,
( spl55_93
<=> ssList(sK43(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_93])],[avatar_definition]) ).
fof(f2426,plain,
( ssList(sK43(sK53))
| ~ spl55_93 ),
inference(avatar_component_clause,[],[f2425]) ).
fof(f2427,plain,
( ~ ssList(sK43(sK53))
| spl55_93 ),
inference(avatar_component_clause,[],[f2425]) ).
fof(f2429,definition,
( spl55_94
<=> ssItem(sK44(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_94])],[avatar_definition]) ).
fof(f2430,plain,
( ssItem(sK44(sK53))
| ~ spl55_94 ),
inference(avatar_component_clause,[],[f2429]) ).
fof(f2431,plain,
( ~ ssItem(sK44(sK53))
| spl55_94 ),
inference(avatar_component_clause,[],[f2429]) ).
fof(f2441,definition,
( spl55_97
<=> memberP(sK53,sK44(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_97])],[avatar_definition]) ).
fof(f2443,plain,
( memberP(sK53,sK44(sK53))
| ~ spl55_97 ),
inference(avatar_component_clause,[],[f2441]) ).
fof(f2444,plain,
( ~ spl55_94
| ~ spl55_93
| spl55_97
| ~ spl55_35 ),
inference(avatar_split_clause,[],[f2421,f1069,f2441,f2425,f2429]) ).
fof(f2793,plain,
( ~ ssList(sK53)
| nil = sK53
| spl55_93 ),
inference(resolution,[],[f2427,f312]) ).
fof(f2794,plain,
( nil = sK53
| spl55_93 ),
inference(forward_subsumption_resolution,[],[f2793,f414]) ).
fof(f2851,plain,
( ~ ssList(sK53)
| nil = sK53
| spl55_94 ),
inference(resolution,[],[f2431,f311]) ).
fof(f2852,plain,
( nil = sK53
| spl55_94 ),
inference(forward_subsumption_resolution,[],[f2851,f414]) ).
fof(f2853,plain,
( $false
| spl55_18
| spl55_94 ),
inference(forward_subsumption_resolution,[],[f2852,f780]) ).
fof(f2854,plain,
( spl55_18
| spl55_94 ),
inference(avatar_contradiction_clause,[],[f2853]) ).
fof(f3179,definition,
( spl55_213
<=> sK49 = app(sK53,cons(sK51,nil)) ),
introduced(definition,[new_symbols(definition,[spl55_213])],[avatar_definition]) ).
fof(f3180,plain,
( sK49 != app(sK53,cons(sK51,nil))
| spl55_213 ),
inference(avatar_component_clause,[],[f3179]) ).
fof(f3181,plain,
( sK49 = app(sK53,cons(sK51,nil))
| ~ spl55_213 ),
inference(avatar_component_clause,[],[f3179]) ).
fof(f4244,plain,
( cons(sK52,sK49) = app(sK49,sK49)
| ~ spl55_3
| ~ spl55_6 ),
inference(resolution,[],[f2164,f425]) ).
fof(f4321,definition,
( spl55_359
<=> sK51 = sK52 ),
introduced(definition,[new_symbols(definition,[spl55_359])],[avatar_definition]) ).
fof(f4323,plain,
( sK51 = sK52
| ~ spl55_359 ),
inference(avatar_component_clause,[],[f4321]) ).
fof(f4794,definition,
( spl55_435
<=> sK52 = sK44(sK53) ),
introduced(definition,[new_symbols(definition,[spl55_435])],[avatar_definition]) ).
fof(f4796,plain,
( sK52 = sK44(sK53)
| ~ spl55_435 ),
inference(avatar_component_clause,[],[f4794]) ).
fof(f5281,definition,
( spl55_498
<=> sK49 = sK53 ),
introduced(definition,[new_symbols(definition,[spl55_498])],[avatar_definition]) ).
fof(f5282,plain,
( sK49 = sK53
| ~ spl55_498 ),
inference(avatar_component_clause,[],[f5281]) ).
fof(f5366,definition,
( spl55_506
<=> frontsegP(sK49,sK53) ),
introduced(definition,[new_symbols(definition,[spl55_506])],[avatar_definition]) ).
fof(f5367,plain,
( frontsegP(sK49,sK53)
| ~ spl55_506 ),
inference(avatar_component_clause,[],[f5366]) ).
fof(f5486,definition,
( spl55_523
<=> frontsegP(sK53,sK49) ),
introduced(definition,[new_symbols(definition,[spl55_523])],[avatar_definition]) ).
fof(f5497,plain,
( ~ frontsegP(sK49,sK53)
| sK52 = sK44(sK53)
| ~ ssList(sK43(sK53))
| ~ ssItem(sK44(sK53))
| ~ spl55_35
| ~ spl55_78 ),
inference(superposition,[],[f2143,f1071]) ).
fof(f5506,plain,
( ~ frontsegP(sK49,sK53)
| sK52 = sK44(sK53)
| ~ ssItem(sK44(sK53))
| ~ spl55_35
| ~ spl55_78
| ~ spl55_93 ),
inference(forward_subsumption_resolution,[],[f5497,f2426]) ).
fof(f5513,plain,
( ~ frontsegP(sK49,sK53)
| sK52 = sK44(sK53)
| ~ spl55_35
| ~ spl55_78
| ~ spl55_93
| ~ spl55_94 ),
inference(forward_subsumption_resolution,[],[f5506,f2430]) ).
fof(f5518,plain,
( spl55_435
| ~ spl55_506
| ~ spl55_35
| ~ spl55_78
| ~ spl55_93
| ~ spl55_94 ),
inference(avatar_split_clause,[],[f5513,f2429,f2425,f2142,f1069,f5366,f4794]) ).
fof(f6248,plain,
( frontsegP(sK49,app(sK53,cons(sK52,nil)))
| ~ spl55_64
| ~ spl55_359 ),
inference(superposition,[],[f2056,f4323]) ).
fof(f6258,plain,
( frontsegP(sK49,app(sK53,sK49))
| ~ spl55_6
| ~ spl55_64
| ~ spl55_359 ),
inference(forward_demodulation,[],[f6248,f548]) ).
fof(f6496,plain,
( ~ cyclefreeP(app(sK53,sK49))
| ~ ssItem(sK51)
| ~ ssList(sK2(sK53,sK51))
| ~ ssList(sK3(sK53,sK51))
| leq(sK52,sK51)
| leq(sK51,sK52)
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9 ),
inference(superposition,[],[f2202,f1790]) ).
fof(f6502,plain,
( ~ cyclefreeP(app(sK53,sK49))
| ~ ssList(sK2(sK53,sK51))
| ~ ssList(sK3(sK53,sK51))
| leq(sK52,sK51)
| leq(sK51,sK52)
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f6496,f421]) ).
fof(f6511,definition,
( spl55_581
<=> leq(sK52,sK52) ),
introduced(definition,[new_symbols(definition,[spl55_581])],[avatar_definition]) ).
fof(f6512,plain,
( ~ leq(sK52,sK52)
| spl55_581 ),
inference(avatar_component_clause,[],[f6511]) ).
fof(f6513,plain,
( leq(sK52,sK52)
| ~ spl55_581 ),
inference(avatar_component_clause,[],[f6511]) ).
fof(f6519,plain,
( ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ ssList(sK3(sK53,sK51))
| leq(sK52,sK51)
| leq(sK51,sK52)
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359 ),
inference(forward_demodulation,[],[f6502,f4323]) ).
fof(f6527,plain,
( ~ ssList(sK3(sK53,sK52))
| ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| leq(sK52,sK51)
| leq(sK51,sK52)
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359 ),
inference(forward_demodulation,[],[f6519,f4323]) ).
fof(f6544,plain,
( leq(sK52,sK52)
| ~ ssList(sK3(sK53,sK52))
| ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| leq(sK51,sK52)
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359 ),
inference(forward_demodulation,[],[f6527,f4323]) ).
fof(f6545,plain,
( leq(sK52,sK52)
| leq(sK52,sK52)
| ~ ssList(sK3(sK53,sK52))
| ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359 ),
inference(forward_demodulation,[],[f6544,f4323]) ).
fof(f6548,definition,
( spl55_586
<=> ssList(app(sK53,sK49)) ),
introduced(definition,[new_symbols(definition,[spl55_586])],[avatar_definition]) ).
fof(f6549,plain,
( ssList(app(sK53,sK49))
| ~ spl55_586 ),
inference(avatar_component_clause,[],[f6548]) ).
fof(f6550,plain,
( ~ ssList(app(sK53,sK49))
| spl55_586 ),
inference(avatar_component_clause,[],[f6548]) ).
fof(f6556,definition,
( spl55_588
<=> ssList(sK2(sK53,sK52)) ),
introduced(definition,[new_symbols(definition,[spl55_588])],[avatar_definition]) ).
fof(f6557,plain,
( ssList(sK2(sK53,sK52))
| ~ spl55_588 ),
inference(avatar_component_clause,[],[f6556]) ).
fof(f6558,plain,
( ~ ssList(sK2(sK53,sK52))
| spl55_588 ),
inference(avatar_component_clause,[],[f6556]) ).
fof(f6560,definition,
( spl55_589
<=> ssList(sK3(sK53,sK52)) ),
introduced(definition,[new_symbols(definition,[spl55_589])],[avatar_definition]) ).
fof(f6561,plain,
( ssList(sK3(sK53,sK52))
| ~ spl55_589 ),
inference(avatar_component_clause,[],[f6560]) ).
fof(f6562,plain,
( ~ ssList(sK3(sK53,sK52))
| spl55_589 ),
inference(avatar_component_clause,[],[f6560]) ).
fof(f8318,plain,
( ~ ssItem(sK52)
| ~ spl55_581 ),
inference(resolution,[],[f6513,f486]) ).
fof(f8322,plain,
( $false
| ~ spl55_3
| ~ spl55_581 ),
inference(forward_subsumption_resolution,[],[f8318,f534]) ).
fof(f8323,plain,
( ~ spl55_3
| ~ spl55_581 ),
inference(avatar_contradiction_clause,[],[f8322]) ).
fof(f8930,plain,
( frontsegP(sK53,cons(sK44(sK53),nil))
| ~ ssItem(sK44(sK53))
| ~ ssList(sK43(sK53))
| ~ spl55_9
| ~ spl55_35 ),
inference(superposition,[],[f1674,f1071]) ).
fof(f8942,plain,
( frontsegP(sK53,cons(sK44(sK53),nil))
| ~ ssList(sK43(sK53))
| ~ spl55_9
| ~ spl55_35
| ~ spl55_94 ),
inference(forward_subsumption_resolution,[],[f8930,f2430]) ).
fof(f11668,plain,
( frontsegP(sK49,sK53)
| ~ ssList(sK54)
| ~ ssList(sK53)
| ~ ssList(cons(sK51,nil)) ),
inference(superposition,[],[f1308,f430]) ).
fof(f11705,plain,
( frontsegP(sK49,sK53)
| ~ ssList(sK53)
| ~ ssList(cons(sK51,nil)) ),
inference(forward_subsumption_resolution,[],[f11668,f412]) ).
fof(f11706,plain,
( frontsegP(sK49,sK53)
| ~ ssList(cons(sK51,nil)) ),
inference(forward_subsumption_resolution,[],[f11705,f414]) ).
fof(f11707,plain,
( frontsegP(sK49,sK53)
| ~ spl55_54 ),
inference(forward_subsumption_resolution,[],[f11706,f1906]) ).
fof(f11708,plain,
( spl55_506
| ~ spl55_54 ),
inference(avatar_split_clause,[],[f11707,f1905,f5366]) ).
fof(f12895,plain,
( ~ ssList(sK53)
| ~ frontsegP(sK53,sK49)
| ~ ssList(sK49)
| sK49 = sK53
| ~ spl55_506 ),
inference(resolution,[],[f5367,f339]) ).
fof(f12898,plain,
( ~ frontsegP(sK53,sK49)
| ~ ssList(sK49)
| sK49 = sK53
| ~ spl55_506 ),
inference(forward_subsumption_resolution,[],[f12895,f414]) ).
fof(f12904,plain,
( ~ frontsegP(sK53,sK49)
| sK49 = sK53
| ~ spl55_506 ),
inference(forward_subsumption_resolution,[],[f12898,f425]) ).
fof(f21400,plain,
( ~ ssItem(sK52)
| ~ ssList(sK53)
| ~ memberP(sK53,sK52)
| spl55_588 ),
inference(resolution,[],[f6558,f231]) ).
fof(f21401,plain,
( ~ ssList(sK53)
| ~ memberP(sK53,sK52)
| ~ spl55_3
| spl55_588 ),
inference(forward_subsumption_resolution,[],[f21400,f534]) ).
fof(f21402,plain,
( ~ memberP(sK53,sK52)
| ~ spl55_3
| spl55_588 ),
inference(forward_subsumption_resolution,[],[f21401,f414]) ).
fof(f35566,plain,
( leq(sK52,sK52)
| ~ ssList(sK3(sK53,sK52))
| ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359 ),
inference(duplicate_literal_removal,[],[f6545]) ).
fof(f37097,plain,
( ~ ssList(sK49)
| ~ ssList(sK53)
| spl55_586 ),
inference(resolution,[],[f6550,f318]) ).
fof(f37098,plain,
( ~ ssList(sK53)
| spl55_586 ),
inference(forward_subsumption_resolution,[],[f37097,f425]) ).
fof(f37099,plain,
( $false
| spl55_586 ),
inference(forward_subsumption_resolution,[],[f37098,f414]) ).
fof(f37100,plain,
spl55_586,
inference(avatar_contradiction_clause,[],[f37099]) ).
fof(f38352,plain,
( ~ ssItem(sK52)
| ~ ssList(sK53)
| ~ memberP(sK53,sK52)
| spl55_589 ),
inference(resolution,[],[f6562,f230]) ).
fof(f39914,plain,
( memberP(sK53,sK52)
| ~ spl55_97
| ~ spl55_435 ),
inference(superposition,[],[f2443,f4796]) ).
fof(f39924,plain,
( $false
| ~ spl55_3
| ~ spl55_97
| ~ spl55_435
| spl55_588 ),
inference(forward_subsumption_resolution,[],[f39914,f21402]) ).
fof(f39925,plain,
( ~ spl55_3
| ~ spl55_97
| ~ spl55_435
| spl55_588 ),
inference(avatar_contradiction_clause,[],[f39924]) ).
fof(f40171,plain,
( spl55_498
| ~ spl55_523
| ~ spl55_506 ),
inference(avatar_split_clause,[],[f12904,f5366,f5486,f5281]) ).
fof(f40195,plain,
( memberP(sK49,sK51)
| ~ spl55_1
| ~ spl55_498 ),
inference(superposition,[],[f525,f5282]) ).
fof(f40345,plain,
( ssList(sK3(sK49,sK52))
| ~ spl55_498
| ~ spl55_589 ),
inference(forward_demodulation,[],[f6561,f5282]) ).
fof(f40472,plain,
( ssList(sK2(sK49,sK52))
| ~ spl55_498
| ~ spl55_588 ),
inference(forward_demodulation,[],[f6557,f5282]) ).
fof(f41250,plain,
( ~ ssItem(sK51)
| sK51 = sK52
| ~ spl55_1
| ~ spl55_81
| ~ spl55_498 ),
inference(resolution,[],[f40195,f2155]) ).
fof(f41299,plain,
( sK51 = sK52
| ~ spl55_1
| ~ spl55_81
| ~ spl55_498 ),
inference(forward_subsumption_resolution,[],[f41250,f421]) ).
fof(f41360,plain,
( frontsegP(sK49,app(sK49,sK49))
| ~ spl55_6
| ~ spl55_64
| ~ spl55_359
| ~ spl55_498 ),
inference(forward_demodulation,[],[f6258,f5282]) ).
fof(f41777,plain,
( ~ ssList(sK3(sK53,sK52))
| ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ ssList(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| spl55_581 ),
inference(forward_subsumption_resolution,[],[f35566,f6512]) ).
fof(f42032,plain,
( ~ ssList(sK53)
| ~ memberP(sK53,sK52)
| ~ spl55_3
| spl55_589 ),
inference(forward_subsumption_resolution,[],[f38352,f534]) ).
fof(f42044,plain,
( spl55_359
| ~ spl55_1
| ~ spl55_81
| ~ spl55_498 ),
inference(avatar_split_clause,[],[f41299,f5281,f2154,f523,f4321]) ).
fof(f42426,plain,
( ~ memberP(sK53,sK52)
| ~ spl55_3
| spl55_589 ),
inference(forward_subsumption_resolution,[],[f42032,f414]) ).
fof(f42860,plain,
( ~ memberP(sK49,sK52)
| ~ spl55_3
| ~ spl55_498
| spl55_589 ),
inference(forward_demodulation,[],[f42426,f5282]) ).
fof(f42935,plain,
( $false
| ~ spl55_3
| ~ spl55_32
| ~ spl55_498
| spl55_589 ),
inference(forward_subsumption_resolution,[],[f42860,f899]) ).
fof(f42936,plain,
( ~ spl55_3
| ~ spl55_32
| ~ spl55_498
| spl55_589 ),
inference(avatar_contradiction_clause,[],[f42935]) ).
fof(f43083,plain,
( ~ ssList(sK3(sK53,sK52))
| ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| spl55_581
| ~ spl55_586 ),
inference(forward_subsumption_resolution,[],[f41777,f6549]) ).
fof(f43127,plain,
( ~ ssList(sK3(sK49,sK52))
| ~ ssList(sK2(sK53,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| ~ spl55_498
| spl55_581
| ~ spl55_586 ),
inference(forward_demodulation,[],[f43083,f5282]) ).
fof(f43141,definition,
( spl55_4185
<=> cyclefreeP(app(sK49,sK49)) ),
introduced(definition,[new_symbols(definition,[spl55_4185])],[avatar_definition]) ).
fof(f43142,plain,
( ~ cyclefreeP(app(sK49,sK49))
| spl55_4185 ),
inference(avatar_component_clause,[],[f43141]) ).
fof(f43157,plain,
( ~ ssList(sK2(sK49,sK52))
| ~ ssList(sK3(sK49,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| ~ spl55_498
| spl55_581
| ~ spl55_586 ),
inference(forward_demodulation,[],[f43127,f5282]) ).
fof(f43163,plain,
( ~ ssList(sK3(sK49,sK52))
| ~ cyclefreeP(app(sK53,sK49))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| ~ spl55_498
| spl55_581
| ~ spl55_586
| ~ spl55_588 ),
inference(forward_subsumption_resolution,[],[f43157,f40472]) ).
fof(f43169,plain,
( ~ cyclefreeP(app(sK49,sK49))
| ~ ssList(sK3(sK49,sK52))
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| ~ spl55_498
| spl55_581
| ~ spl55_586
| ~ spl55_588 ),
inference(forward_demodulation,[],[f43163,f5282]) ).
fof(f43171,definition,
( spl55_4186
<=> ssList(sK3(sK49,sK52)) ),
introduced(definition,[new_symbols(definition,[spl55_4186])],[avatar_definition]) ).
fof(f43178,plain,
( ~ spl55_4186
| ~ spl55_4185
| ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| ~ spl55_498
| spl55_581
| ~ spl55_586
| ~ spl55_588 ),
inference(avatar_split_clause,[],[f43169,f6556,f6548,f6511,f5281,f4321,f562,f546,f532,f523,f43141,f43171]) ).
fof(f43359,plain,
( spl55_4186
| ~ spl55_498
| ~ spl55_589 ),
inference(avatar_split_clause,[],[f40345,f6560,f5281,f43171]) ).
fof(f44802,plain,
( sK49 = app(sK53,cons(sK52,nil))
| ~ spl55_213
| ~ spl55_359 ),
inference(forward_demodulation,[],[f3181,f4323]) ).
fof(f44803,plain,
( sK49 = app(sK53,sK49)
| ~ spl55_6
| ~ spl55_213
| ~ spl55_359 ),
inference(forward_demodulation,[],[f44802,f548]) ).
fof(f44804,plain,
( sK49 = app(sK49,sK49)
| ~ spl55_6
| ~ spl55_213
| ~ spl55_359
| ~ spl55_498 ),
inference(forward_demodulation,[],[f44803,f5282]) ).
fof(f44807,plain,
( ~ cyclefreeP(sK49)
| ~ spl55_6
| ~ spl55_213
| ~ spl55_359
| ~ spl55_498
| spl55_4185 ),
inference(superposition,[],[f43142,f44804]) ).
fof(f44866,plain,
( $false
| ~ spl55_6
| ~ spl55_25
| ~ spl55_213
| ~ spl55_359
| ~ spl55_498
| spl55_4185 ),
inference(forward_subsumption_resolution,[],[f44807,f863]) ).
fof(f44867,plain,
( ~ spl55_6
| ~ spl55_25
| ~ spl55_213
| ~ spl55_359
| ~ spl55_498
| spl55_4185 ),
inference(avatar_contradiction_clause,[],[f44866]) ).
fof(f44873,plain,
( sK49 != app(sK53,cons(sK52,nil))
| spl55_213
| ~ spl55_359 ),
inference(forward_demodulation,[],[f3180,f4323]) ).
fof(f44877,plain,
( ! [X0] :
( sK49 != app(app(sK53,cons(sK51,nil)),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl55_37 ),
inference(forward_subsumption_resolution,[],[f1588,f1080]) ).
fof(f45502,plain,
( sK49 != app(sK53,sK49)
| ~ spl55_6
| spl55_213
| ~ spl55_359 ),
inference(forward_demodulation,[],[f44873,f548]) ).
fof(f45505,plain,
( ! [X0] :
( sK49 != app(app(sK53,cons(sK52,nil)),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl55_37
| ~ spl55_359 ),
inference(forward_demodulation,[],[f44877,f4323]) ).
fof(f45600,plain,
( sK49 != app(sK49,sK49)
| ~ spl55_6
| spl55_213
| ~ spl55_359
| ~ spl55_498 ),
inference(forward_demodulation,[],[f45502,f5282]) ).
fof(f45603,plain,
( ! [X0] :
( sK49 != app(app(sK53,sK49),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl55_6
| ~ spl55_37
| ~ spl55_359 ),
inference(forward_demodulation,[],[f45505,f548]) ).
fof(f50425,plain,
( sK49 != cons(sK52,sK49)
| ~ spl55_3
| ~ spl55_6
| spl55_213
| ~ spl55_359
| ~ spl55_498 ),
inference(superposition,[],[f45600,f4244]) ).
fof(f50444,plain,
( ~ frontsegP(sK49,cons(sK52,sK49))
| ~ ssList(sK49)
| ~ ssList(sK49)
| sK49 = cons(sK52,sK49)
| ~ spl55_3
| ~ spl55_6 ),
inference(superposition,[],[f1159,f4244]) ).
fof(f50461,plain,
( ~ frontsegP(sK49,cons(sK52,sK49))
| ~ ssList(sK49)
| sK49 = cons(sK52,sK49)
| ~ spl55_3
| ~ spl55_6 ),
inference(duplicate_literal_removal,[],[f50444]) ).
fof(f50480,plain,
( ~ frontsegP(sK49,cons(sK52,sK49))
| sK49 = cons(sK52,sK49)
| ~ spl55_3
| ~ spl55_6 ),
inference(forward_subsumption_resolution,[],[f50461,f425]) ).
fof(f50499,definition,
( spl55_5163
<=> sK49 = cons(sK52,sK49) ),
introduced(definition,[new_symbols(definition,[spl55_5163])],[avatar_definition]) ).
fof(f50508,definition,
( spl55_5165
<=> frontsegP(sK49,cons(sK52,sK49)) ),
introduced(definition,[new_symbols(definition,[spl55_5165])],[avatar_definition]) ).
fof(f50511,plain,
( spl55_5163
| ~ spl55_5165
| ~ spl55_3
| ~ spl55_6 ),
inference(avatar_split_clause,[],[f50480,f546,f532,f50508,f50499]) ).
fof(f53572,plain,
( ~ memberP(sK49,sK51)
| spl55_1
| ~ spl55_498 ),
inference(forward_demodulation,[],[f524,f5282]) ).
fof(f54347,plain,
( memberP(sK49,sK51)
| ~ ssList(app(sK53,cons(sK51,nil)))
| ~ spl55_2 ),
inference(superposition,[],[f1282,f430]) ).
fof(f54353,plain,
( ~ ssList(app(sK53,cons(sK51,nil)))
| spl55_1
| ~ spl55_2
| ~ spl55_498 ),
inference(forward_subsumption_resolution,[],[f54347,f53572]) ).
fof(f54378,plain,
( $false
| spl55_1
| ~ spl55_2
| ~ spl55_37
| ~ spl55_498 ),
inference(forward_subsumption_resolution,[],[f54353,f1080]) ).
fof(f54379,plain,
( spl55_1
| ~ spl55_2
| ~ spl55_37
| ~ spl55_498 ),
inference(avatar_contradiction_clause,[],[f54378]) ).
fof(f54380,plain,
( spl55_18
| spl55_93 ),
inference(avatar_split_clause,[],[f2794,f2425,f779]) ).
fof(f54475,plain,
( memberP(sK49,sK51)
| ~ spl55_2
| ~ spl55_37 ),
inference(forward_subsumption_resolution,[],[f54347,f1080]) ).
fof(f54482,plain,
( frontsegP(sK53,cons(sK52,nil))
| ~ ssList(sK43(sK53))
| ~ spl55_9
| ~ spl55_35
| ~ spl55_94
| ~ spl55_435 ),
inference(forward_demodulation,[],[f8942,f4796]) ).
fof(f54599,plain,
( frontsegP(sK53,sK49)
| ~ ssList(sK43(sK53))
| ~ spl55_6
| ~ spl55_9
| ~ spl55_35
| ~ spl55_94
| ~ spl55_435 ),
inference(forward_demodulation,[],[f54482,f548]) ).
fof(f54642,plain,
( ~ spl55_93
| spl55_523
| ~ spl55_6
| ~ spl55_9
| ~ spl55_35
| ~ spl55_94
| ~ spl55_435 ),
inference(avatar_split_clause,[],[f54599,f4794,f2429,f1069,f562,f546,f5486,f2425]) ).
fof(f56061,plain,
( ~ ssItem(sK51)
| sK51 = sK52
| ~ spl55_2
| ~ spl55_37
| ~ spl55_81 ),
inference(resolution,[],[f54475,f2155]) ).
fof(f56110,plain,
( sK51 = sK52
| ~ spl55_2
| ~ spl55_37
| ~ spl55_81 ),
inference(forward_subsumption_resolution,[],[f56061,f421]) ).
fof(f56990,plain,
( ! [X0] :
( sK49 != app(app(nil,sK49),X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl55_6
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(forward_demodulation,[],[f45603,f781]) ).
fof(f57751,plain,
( spl55_359
| ~ spl55_2
| ~ spl55_37
| ~ spl55_81 ),
inference(avatar_split_clause,[],[f56110,f2154,f1079,f527,f4321]) ).
fof(f58309,plain,
( ! [X0] :
( sK49 != app(sK49,X0)
| ~ ssList(X0)
| sK54 = X0 )
| ~ spl55_6
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(forward_demodulation,[],[f56990,f621]) ).
fof(f60393,plain,
( sK49 != sK49
| ~ ssList(nil)
| nil = sK54
| ~ spl55_6
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(superposition,[],[f58309,f640]) ).
fof(f60398,plain,
( ~ ssList(nil)
| nil = sK54
| ~ spl55_6
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(trivial_inequality_removal,[],[f60393]) ).
fof(f60406,plain,
( nil = sK54
| ~ spl55_6
| ~ spl55_9
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(forward_subsumption_resolution,[],[f60398,f563]) ).
fof(f60413,plain,
( $false
| ~ spl55_6
| ~ spl55_9
| spl55_16
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(forward_subsumption_resolution,[],[f60406,f771]) ).
fof(f60414,plain,
( ~ spl55_6
| ~ spl55_9
| spl55_16
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(avatar_contradiction_clause,[],[f60413]) ).
fof(f61163,plain,
( ~ spl55_5163
| ~ spl55_3
| ~ spl55_6
| spl55_213
| ~ spl55_359
| ~ spl55_498 ),
inference(avatar_split_clause,[],[f50425,f5281,f4321,f3179,f546,f532,f50499]) ).
fof(f61826,plain,
( frontsegP(sK49,cons(sK52,sK49))
| ~ spl55_3
| ~ spl55_6
| ~ spl55_64
| ~ spl55_359
| ~ spl55_498 ),
inference(forward_demodulation,[],[f41360,f4244]) ).
fof(f63033,plain,
( spl55_5165
| ~ spl55_3
| ~ spl55_6
| ~ spl55_64
| ~ spl55_359
| ~ spl55_498 ),
inference(avatar_split_clause,[],[f61826,f5281,f4321,f2054,f546,f532,f50508]) ).
cnf(s1,plain,
( spl55_1
| spl55_2 ),
inference(sat_conversion,[],[f530]) ).
cnf(s5,plain,
( spl55_3
| spl55_7 ),
inference(sat_conversion,[],[f554]) ).
cnf(s7,plain,
( spl55_6
| spl55_7 ),
inference(sat_conversion,[],[f556]) ).
cnf(s16,plain,
spl55_9,
inference(sat_conversion,[],[f591]) ).
cnf(s39,plain,
( ~ spl55_2
| ~ spl55_16 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s40,plain,
( ~ spl55_1
| ~ spl55_18 ),
inference(sat_conversion,[],[f1067]) ).
cnf(s41,plain,
( spl55_18
| spl55_35 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s64,plain,
( ~ spl55_9
| spl55_37 ),
inference(sat_conversion,[],[f1858]) ).
cnf(s65,plain,
( ~ spl55_7
| ~ spl55_54
| spl55_55 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s66,plain,
( ~ spl55_9
| spl55_54 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s71,plain,
( ~ spl55_54
| ~ spl55_55
| spl55_57 ),
inference(sat_conversion,[],[f1970]) ).
cnf(s76,plain,
( ~ spl55_9
| ~ spl55_57 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s77,plain,
( ~ spl55_3
| ~ spl55_6
| spl55_25 ),
inference(sat_conversion,[],[f2031]) ).
cnf(s85,plain,
( ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| spl55_32 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s90,plain,
( ~ spl55_37
| spl55_64 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s110,plain,
( ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| spl55_78 ),
inference(sat_conversion,[],[f2144]) ).
cnf(s113,plain,
( ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| spl55_81 ),
inference(sat_conversion,[],[f2156]) ).
cnf(s127,plain,
( ~ spl55_35
| ~ spl55_93
| ~ spl55_94
| spl55_97 ),
inference(sat_conversion,[],[f2444]) ).
cnf(s191,plain,
( spl55_18
| spl55_94 ),
inference(sat_conversion,[],[f2854]) ).
cnf(s508,plain,
( ~ spl55_35
| ~ spl55_78
| ~ spl55_93
| ~ spl55_94
| spl55_435
| ~ spl55_506 ),
inference(sat_conversion,[],[f5518]) ).
cnf(s670,plain,
( ~ spl55_3
| ~ spl55_581 ),
inference(sat_conversion,[],[f8323]) ).
cnf(s915,plain,
( ~ spl55_54
| spl55_506 ),
inference(sat_conversion,[],[f11708]) ).
cnf(s3647,plain,
spl55_586,
inference(sat_conversion,[],[f37100]) ).
cnf(s4294,plain,
( ~ spl55_3
| ~ spl55_97
| ~ spl55_435
| spl55_588 ),
inference(sat_conversion,[],[f39925]) ).
cnf(s4444,plain,
( spl55_498
| ~ spl55_506
| ~ spl55_523 ),
inference(sat_conversion,[],[f40171]) ).
cnf(s4709,plain,
( ~ spl55_1
| ~ spl55_81
| spl55_359
| ~ spl55_498 ),
inference(sat_conversion,[],[f42044]) ).
cnf(s4909,plain,
( ~ spl55_3
| ~ spl55_32
| ~ spl55_498
| spl55_589 ),
inference(sat_conversion,[],[f42936]) ).
cnf(s4966,plain,
( ~ spl55_1
| ~ spl55_3
| ~ spl55_6
| ~ spl55_9
| ~ spl55_359
| ~ spl55_498
| spl55_581
| ~ spl55_586
| ~ spl55_588
| ~ spl55_4185
| ~ spl55_4186 ),
inference(sat_conversion,[],[f43178]) ).
cnf(s4985,plain,
( ~ spl55_498
| ~ spl55_589
| spl55_4186 ),
inference(sat_conversion,[],[f43359]) ).
cnf(s5197,plain,
( ~ spl55_6
| ~ spl55_25
| ~ spl55_213
| ~ spl55_359
| ~ spl55_498
| spl55_4185 ),
inference(sat_conversion,[],[f44867]) ).
cnf(s5996,plain,
( ~ spl55_3
| ~ spl55_6
| spl55_5163
| ~ spl55_5165 ),
inference(sat_conversion,[],[f50511]) ).
cnf(s6538,plain,
( spl55_1
| ~ spl55_2
| ~ spl55_37
| ~ spl55_498 ),
inference(sat_conversion,[],[f54379]) ).
cnf(s6539,plain,
( spl55_18
| spl55_93 ),
inference(sat_conversion,[],[f54380]) ).
cnf(s6618,plain,
( ~ spl55_6
| ~ spl55_9
| ~ spl55_35
| ~ spl55_93
| ~ spl55_94
| ~ spl55_435
| spl55_523 ),
inference(sat_conversion,[],[f54642]) ).
cnf(s7089,plain,
( ~ spl55_2
| ~ spl55_37
| ~ spl55_81
| spl55_359 ),
inference(sat_conversion,[],[f57751]) ).
cnf(s7714,plain,
( ~ spl55_6
| ~ spl55_9
| spl55_16
| ~ spl55_18
| ~ spl55_37
| ~ spl55_359 ),
inference(sat_conversion,[],[f60414]) ).
cnf(s8062,plain,
( ~ spl55_3
| ~ spl55_6
| spl55_213
| ~ spl55_359
| ~ spl55_498
| ~ spl55_5163 ),
inference(sat_conversion,[],[f61163]) ).
cnf(s9133,plain,
( ~ spl55_3
| ~ spl55_6
| ~ spl55_64
| ~ spl55_359
| ~ spl55_498
| spl55_5165 ),
inference(sat_conversion,[],[f63033]) ).
cnf(s9561,plain,
~ spl55_57,
inference(rat,[],[s76,s16]) ).
cnf(s9562,plain,
spl55_54,
inference(rat,[],[s66,s16]) ).
cnf(s9563,plain,
spl55_37,
inference(rat,[],[s64,s16]) ).
cnf(s9595,plain,
spl55_506,
inference(rat,[],[s915,s9562]) ).
cnf(s9603,plain,
~ spl55_55,
inference(rat,[],[s71,s9561,s9562]) ).
cnf(s9608,plain,
~ spl55_7,
inference(rat,[],[s65,s9603,s9562]) ).
cnf(s9611,plain,
spl55_64,
inference(rat,[],[s90,s9563]) ).
cnf(s9688,plain,
spl55_6,
inference(rat,[],[s7,s9608]) ).
cnf(s9690,plain,
spl55_3,
inference(rat,[],[s5,s9608]) ).
cnf(s9704,plain,
~ spl55_581,
inference(rat,[],[s670,s9690]) ).
cnf(s9706,plain,
spl55_81,
inference(rat,[],[s113,s9688,s16,s9690]) ).
cnf(s9708,plain,
spl55_78,
inference(rat,[],[s110,s9688,s16,s9690]) ).
cnf(s9717,plain,
spl55_32,
inference(rat,[],[s85,s9688,s16,s9690]) ).
cnf(s9724,plain,
spl55_25,
inference(rat,[],[s77,s9688,s9690]) ).
cnf(s9882,plain,
spl55_1,
inference(rat,[],[s6618,s508,s41,s191,s6539,s7714,s4444,s39,s6538,s7089,s1,s16,s9688,s9708,s9595,s9563,s9706]) ).
cnf(s9885,plain,
~ spl55_18,
inference(rat,[],[s40,s9882]) ).
cnf(s9920,plain,
spl55_93,
inference(rat,[],[s6539,s9885]) ).
cnf(s9922,plain,
spl55_94,
inference(rat,[],[s191,s9885]) ).
cnf(s9924,plain,
spl55_35,
inference(rat,[],[s41,s9885]) ).
cnf(s9976,plain,
spl55_435,
inference(rat,[],[s508,s9595,s9920,s9922,s9708,s9924]) ).
cnf(s9998,plain,
spl55_97,
inference(rat,[],[s127,s9920,s9922,s9924]) ).
cnf(s10028,plain,
spl55_523,
inference(rat,[],[s6618,s9924,s9920,s9922,s9688,s16,s9976]) ).
cnf(s10031,plain,
spl55_588,
inference(rat,[],[s4294,s9976,s9690,s9998]) ).
cnf(s10034,plain,
spl55_498,
inference(rat,[],[s4444,s9595,s10028]) ).
cnf(s10042,plain,
spl55_589,
inference(rat,[],[s4909,s9717,s9690,s10034]) ).
cnf(s10046,plain,
spl55_359,
inference(rat,[],[s4709,s9882,s9706,s10034]) ).
cnf(s10054,plain,
spl55_4186,
inference(rat,[],[s4985,s10034,s10042]) ).
cnf(s10118,plain,
spl55_5165,
inference(rat,[],[s9133,s10034,s9690,s9688,s9611,s10046]) ).
cnf(s10123,plain,
~ spl55_4185,
inference(rat,[],[s4966,s10054,s10034,s10031,s3647,s9704,s9882,s9690,s16,s9688,s10046]) ).
cnf(s10180,plain,
spl55_5163,
inference(rat,[],[s5996,s9690,s9688,s10118]) ).
cnf(s10224,plain,
~ spl55_213,
inference(rat,[],[s5197,s10034,s10046,s9724,s9688,s10123]) ).
cnf(s10240,plain,
$false,
inference(rat,[],[s8062,s10046,s10034,s9690,s9688,s10180,s10224]) ).
fof(f63771,plain,
$false,
inference(avatar_sat_refutation,[],[s10240]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC187+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n017.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 28 08:17:06 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.41 Running first-order model finding
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.38/1.91 % (3393596)Will run a generic schedule for satisfiability detection.
% 6.38/1.91 % (3393603)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1981919869:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.38/1.91 % (3393602)% WARNING: option uhcvi not known.
% 6.38/1.91 % (3393601)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2014929188_2999 on theBenchmark for (2999ds/0Mi)
% 6.38/1.91 % (3393604)dis+10_1_sil=32000:sp=arity:random_seed=583527141:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.38/1.91 % (3393602)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3536625370:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.38/1.91 % (3393606)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=821812208:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.38/1.91 % (3393605)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2806236350:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.38/1.91 % (3393607)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=315783944:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.38/1.91 % TRYING [1]
% 6.38/1.91 % TRYING [2]
% 6.38/1.91 % TRYING [3]
% 6.38/1.91 % TRYING [4]
% 6.38/1.91 % (3393604)Instruction limit reached!
% 6.38/1.91 % (3393604)------------------------------
% 6.38/1.91 % (3393604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393604)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393604)Termination reason: Instruction limit
% 6.38/1.91 % (3393604)Termination phase: Saturation
% 6.38/1.91 % (3393604)Time elapsed: 0.063 s
% 6.38/1.91 % (3393604)Peak memory usage: 13 MB
% 6.38/1.91 % (3393604)Instructions burned: 104 (million)
% 6.38/1.91 % (3393605)Instruction limit reached!
% 6.38/1.91 % (3393605)------------------------------
% 6.38/1.91 % (3393605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393605)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393605)Termination reason: Instruction limit
% 6.38/1.91 % (3393605)Termination phase: Saturation
% 6.38/1.91 % (3393605)Time elapsed: 0.071 s
% 6.38/1.91 % (3393605)Peak memory usage: 13 MB
% 6.38/1.91 % (3393605)Instructions burned: 116 (million)
% 6.38/1.91 % (3393606)Instruction limit reached!
% 6.38/1.91 % (3393606)------------------------------
% 6.38/1.91 % (3393606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393606)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393606)Termination reason: Instruction limit
% 6.38/1.91 % (3393606)Termination phase: Saturation
% 6.38/1.91 % (3393606)Time elapsed: 0.080 s
% 6.38/1.91 % (3393606)Peak memory usage: 13 MB
% 6.38/1.91 % (3393606)Instructions burned: 136 (million)
% 6.38/1.91 % (3393615)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1559414213:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.38/1.91 % TRYING [5]
% 6.38/1.91 % (3393616)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3803043940:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.38/1.91 % TRYING [1]
% 6.38/1.91 % TRYING [2]
% 6.38/1.91 % (3393617)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=846462415:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.38/1.91 % TRYING [3]
% 6.38/1.91 % (3393607)Instruction limit reached!
% 6.38/1.91 % (3393607)------------------------------
% 6.38/1.91 % (3393607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393607)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393607)Termination reason: Instruction limit
% 6.38/1.91 % (3393607)Termination phase: Saturation
% 6.38/1.91 % (3393607)Time elapsed: 0.104 s
% 6.38/1.91 % (3393607)Peak memory usage: 15 MB
% 6.38/1.91 % (3393607)Instructions burned: 160 (million)
% 6.38/1.91 % TRYING [4]
% 6.38/1.91 % (3393621)ott-21_1_sil=16000:fs=off:random_seed=161677388:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.38/1.91 % (3393616)Instruction limit reached!
% 6.38/1.91 % (3393616)------------------------------
% 6.38/1.91 % (3393616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393616)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393616)Termination reason: Instruction limit
% 6.38/1.91 % (3393616)Termination phase: Saturation
% 6.38/1.91 % (3393616)Time elapsed: 0.071 s
% 6.38/1.91 % (3393616)Peak memory usage: 13 MB
% 6.38/1.91 % (3393616)Instructions burned: 131 (million)
% 6.38/1.91 % TRYING [5]
% 6.38/1.91 % (3393623)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=933595546:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.38/1.91 % (3393621)Instruction limit reached!
% 6.38/1.91 % (3393621)------------------------------
% 6.38/1.91 % (3393621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393621)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393621)Termination reason: Instruction limit
% 6.38/1.91 % (3393621)Termination phase: Saturation
% 6.38/1.91 % (3393621)Time elapsed: 0.086 s
% 6.38/1.91 % (3393621)Peak memory usage: 13 MB
% 6.38/1.91 % (3393621)Instructions burned: 181 (million)
% 6.38/1.91 % TRYING [6]
% 6.38/1.91 % (3393625)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3483983313:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.38/1.91 % TRYING [1]
% 6.38/1.91 % TRYING [2]
% 6.38/1.91 % TRYING [3]
% 6.38/1.91 % TRYING [4]
% 6.38/1.91 % TRYING [6]
% 6.38/1.91 % (3393615)Instruction limit reached!
% 6.38/1.91 % (3393615)------------------------------
% 6.38/1.91 % (3393615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393615)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393615)Termination reason: Instruction limit
% 6.38/1.91 % (3393615)Termination phase: Finite model building constraint generation
% 6.38/1.91 % (3393615)Time elapsed: 0.289 s
% 6.38/1.91 % (3393615)Peak memory usage: 28 MB
% 6.38/1.91 % (3393615)Instructions burned: 718 (million)
% 6.38/1.91 % (3393627)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2832570229:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 6.38/1.91 % TRYING [5]
% 6.38/1.91 % (3393617)Instruction limit reached!
% 6.38/1.91 % (3393617)------------------------------
% 6.38/1.91 % (3393617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393617)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393617)Termination reason: Instruction limit
% 6.38/1.91 % (3393617)Termination phase: Saturation
% 6.38/1.91 % (3393617)Time elapsed: 0.371 s
% 6.38/1.91 % (3393617)Peak memory usage: 24 MB
% 6.38/1.91 % (3393617)Instructions burned: 686 (million)
% 6.38/1.91 % (3393629)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3924427112:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 6.38/1.91 % TRYING [7]
% 6.38/1.91 % (3393623)Instruction limit reached!
% 6.38/1.91 % (3393623)------------------------------
% 6.38/1.91 % (3393623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393623)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393623)Termination reason: Instruction limit
% 6.38/1.91 % (3393623)Termination phase: Saturation
% 6.38/1.91 % (3393623)Time elapsed: 0.328 s
% 6.38/1.91 % (3393623)Peak memory usage: 14 MB
% 6.38/1.91 % (3393623)Instructions burned: 477 (million)
% 6.38/1.91 % (3393631)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=1438606968: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)
% 6.38/1.91 % (3393625)Instruction limit reached!
% 6.38/1.91 % (3393625)------------------------------
% 6.38/1.91 % (3393625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393625)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393625)Termination reason: Instruction limit
% 6.38/1.91 % (3393625)Termination phase: Finite model building SAT solving
% 6.38/1.91 % (3393625)Time elapsed: 0.351 s
% 6.38/1.91 % (3393625)Peak memory usage: 23 MB
% 6.38/1.91 % (3393625)Instructions burned: 866 (million)
% 6.38/1.91 % TRYING [14]
% 6.38/1.91 % (3393633)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1617140106:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 6.38/1.91 % (3393629)Instruction limit reached!
% 6.38/1.91 % (3393629)------------------------------
% 6.38/1.91 % (3393629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393629)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393629)Termination reason: Instruction limit
% 6.38/1.91 % (3393629)Termination phase: Finite model building constraint generation
% 6.38/1.91 % (3393629)Time elapsed: 0.323 s
% 6.38/1.91 % (3393629)Peak memory usage: 70 MB
% 6.38/1.91 % (3393629)Instructions burned: 892 (million)
% 6.38/1.91 % (3393635)fmb+10_1_sil=64000:random_seed=2208409507:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 6.38/1.91 % TRYING [1]
% 6.38/1.91 % TRYING [2]
% 6.38/1.91 % TRYING [3]
% 6.38/1.91 % (3393631)Instruction limit reached!
% 6.38/1.91 % (3393631)------------------------------
% 6.38/1.91 % (3393631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393631)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393631)Termination reason: Instruction limit
% 6.38/1.91 % (3393631)Termination phase: Saturation
% 6.38/1.91 % (3393631)Time elapsed: 0.353 s
% 6.38/1.91 % (3393631)Peak memory usage: 21 MB
% 6.38/1.91 % (3393631)Instructions burned: 692 (million)
% 6.38/1.91 % (3393637)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=421783152:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 6.38/1.91 % TRYING [4]
% 6.38/1.91 % TRYING [20]
% 6.38/1.91 % TRYING [5]
% 6.38/1.91 % (3393627)Instruction limit reached!
% 6.38/1.91 % (3393627)------------------------------
% 6.38/1.91 % (3393627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393627)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393627)Termination reason: Instruction limit
% 6.38/1.91 % (3393627)Termination phase: Saturation
% 6.38/1.91 % (3393627)Time elapsed: 0.660 s
% 6.38/1.91 % (3393627)Peak memory usage: 27 MB
% 6.38/1.91 % (3393627)Instructions burned: 1180 (million)
% 6.38/1.91 % (3393633)Instruction limit reached!
% 6.38/1.91 % (3393633)------------------------------
% 6.38/1.91 % (3393633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393633)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393633)Termination reason: Instruction limit
% 6.38/1.91 % (3393633)Termination phase: Saturation
% 6.38/1.91 % (3393633)Time elapsed: 0.471 s
% 6.38/1.91 % (3393633)Peak memory usage: 20 MB
% 6.38/1.91 % (3393633)Instructions burned: 881 (million)
% 6.38/1.91 % (3393639)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3946556402:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 6.38/1.91 % TRYING [8]
% 6.38/1.91 % (3393640)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=540782091:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 6.38/1.91 % TRYING [8]
% 6.38/1.91 % TRYING [6]
% 6.38/1.91 % (3393639)Instruction limit reached!
% 6.38/1.91 % (3393639)------------------------------
% 6.38/1.91 % (3393639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.91 % (3393639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.91 % (3393639)CaDiCaL version: 2.1.3
% 6.38/1.91 % (3393639)Termination reason: Instruction limit
% 6.38/1.91 % (3393639)Termination phase: Finite model building constraint generation
% 6.38/1.91 % (3393639)Time elapsed: 0.337 s
% 6.38/1.91 % (3393639)Peak memory usage: 69 MB
% 6.38/1.91 % (3393639)Instructions burned: 920 (million)
% 6.38/1.91 % (3393602) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3393596-3393602"...
% 6.38/1.91 % (3393602)...printing done.
% 6.38/1.91 % (3393602)Refutation found. Thanks to Tanya!
% 6.38/1.91 % SZS status Theorem for theBenchmark
% 6.38/1.91 % SZS output start Proof for theBenchmark
% See solution above
% 6.38/1.92 % (3393602)------------------------------
% 6.38/1.92 % (3393602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.92 % (3393602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.92 % (3393602)CaDiCaL version: 2.1.3
% 6.38/1.92 % (3393602)Termination reason: Refutation
% 6.38/1.92 % (3393602)Time elapsed: 1.435 s
% 6.38/1.92 % (3393602)Peak memory usage: 44 MB
% 6.38/1.92 % (3393602)Instructions burned: 2769 (million)
% 6.38/1.92 % (3393596)Success in time 1.491 s
% 6.38/1.92 % Vampire exiting
%------------------------------------------------------------------------------