%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC307-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 : n020.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:28 PM UTC 2026
% Result : Unsatisfiable 50.28s 17.44s
% Output : Refutation 50.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 95
% Syntax : Number of formulae : 525 ( 78 unt; 44 def)
% Number of atoms : 1645 ( 226 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1743 ( 623 ~;1076 |; 0 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 45 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-2 aty)
% Number of variables : 312 ( 0 sgn 312 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f11,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause11) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause50) ).
fof(f59,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause59) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f76,axiom,
! [X0] :
( ~ ssList(X0)
| ssItem(hd(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause76) ).
fof(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause80) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f98,axiom,
! [X0,X1] :
( cons(X0,X1) != nil
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ~ ssItem(X0)
| ~ ssList(X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause100) ).
fof(f102,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
fof(f103,axiom,
! [X0] :
( ~ singletonP(X0)
| ~ ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause101) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f121,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause118) ).
fof(f122,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
inference(reorient_equations,[],[f121]) ).
fof(f123,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause119) ).
fof(f124,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
inference(reorient_equations,[],[f123]) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f138,axiom,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause129) ).
fof(f139,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f138]) ).
fof(f142,axiom,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause131) ).
fof(f148,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause138) ).
fof(f155,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| frontsegP(X2,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause144) ).
fof(f162,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause150) ).
fof(f163,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause151) ).
fof(f166,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause154) ).
fof(f184,axiom,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X3 = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause171) ).
fof(f185,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X1 = X3 ),
inference(reorient_equations,[],[f184]) ).
fof(f188,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| frontsegP(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause174) ).
fof(f190,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause176) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause178) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_1) ).
fof(f201,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_2) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
segmentP(sk4,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f213,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f212]) ).
fof(f215,negated_conjecture,
( singletonP(sk3)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f216,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f217,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f218,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f213,f205]) ).
fof(f226,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f228,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f230,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f235,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(equality_resolution,[],[f192]) ).
fof(f236,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(equality_resolution,[],[f193]) ).
fof(f245,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f249,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f286,plain,
! [X0,X1] : ~ ssList(skaf46(X0,X1)),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f294,plain,
! [X0] :
( rearsegP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f295,plain,
! [X0] :
( frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f306,plain,
! [X0] :
( memberP(nil,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f307,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f308,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f309,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f310,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f311,plain,
! [X0] :
( ~ ssItem(hd(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f315,plain,
! [X0] :
( ~ segmentP(nil,X0)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f320,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f321,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f331,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f332,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| hd(cons(X0,X1)) = X0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f333,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f335,plain,
! [X0,X1] :
( ~ neq(X1,X0)
| ssList(X1)
| ssList(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f336,plain,
! [X0] :
( ~ singletonP(X0)
| ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f339,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f344,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f351,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f226]) ).
fof(f353,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f354,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X1 ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f355,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f364,plain,
! [X0,X1] :
( ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f366,plain,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f372,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f373,plain,
! [X2,X1] :
( ssList(X2)
| ssItem(X1)
| ssItem(X1)
| ~ memberP(cons(X1,X2),X1) ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f379,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f385,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ssList(X1)
| ssList(X0)
| ssList(X2)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f386,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ssList(X0)
| ssList(X1)
| ssList(X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f389,plain,
! [X2,X0,X1] :
( ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X2) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f406,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ssItem(X2)
| ssItem(X0)
| ssList(X3)
| ssList(X1)
| X1 = X3 ),
inference(consistent_polarity_flipping,[],[f185]) ).
fof(f409,plain,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| ssItem(X0)
| frontsegP(X1,X3) ),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f411,plain,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| ssItem(X0)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f413,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f414,plain,
! [X2,X3,X0,X1] :
( ssList(X3)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f236]) ).
fof(f421,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f216]) ).
fof(f422,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f217]) ).
fof(f425,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f426,plain,
~ ssItem(sk6),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f427,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f428,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f429,plain,
~ ssList(sk9),
inference(consistent_polarity_flipping,[],[f211]) ).
fof(f431,plain,
( singletonP(sk3)
| neq(sk4,nil) ),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f432,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(duplicate_literal_removal,[],[f413]) ).
fof(f434,plain,
! [X2,X1] :
( ~ memberP(cons(X1,X2),X1)
| ssItem(X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f373]) ).
fof(f439,definition,
( spl0_1
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f441,plain,
( neq(sk4,nil)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f443,definition,
( spl0_2
<=> singletonP(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f445,plain,
( singletonP(sk3)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f446,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f431,f443,f439]) ).
fof(f452,definition,
( spl0_4
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f453,plain,
( ~ ssList(nil)
| spl0_4 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f480,definition,
( spl0_10
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f481,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f483,definition,
( spl0_11
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f484,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f485,plain,
( spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f307,f483,f480]) ).
fof(f488,plain,
~ spl0_4,
inference(avatar_split_clause,[],[f245,f452]) ).
fof(f529,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f308,f421]) ).
fof(f565,plain,
sk8 = app(nil,sk8),
inference(resolution,[],[f309,f428]) ).
fof(f592,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f321,f481]) ).
fof(f594,plain,
( ! [X0,X1] :
( ssList(X0)
| cons(X1,X0) = app(nil,cons(X1,X0)) )
| ~ spl0_10 ),
inference(resolution,[],[f592,f309]) ).
fof(f600,plain,
( ! [X0,X1] :
( nil != cons(X0,X1)
| ssList(X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f333,f481]) ).
fof(f642,plain,
( ! [X0,X1] :
( ssList(X1)
| hd(cons(X0,X1)) = X0 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f332,f481]) ).
fof(f644,plain,
( ! [X0,X1] : hd(cons(X0,skaf82(X1))) = X0
| ~ spl0_10 ),
inference(resolution,[],[f642,f249]) ).
fof(f681,plain,
( ssList(sk3)
| sk3 = cons(skaf44(sk3),nil)
| ~ spl0_2 ),
inference(resolution,[],[f336,f445]) ).
fof(f682,plain,
( sk3 = cons(skaf44(sk3),nil)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f681,f421]) ).
fof(f710,plain,
( ! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil)) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f351,f481]) ).
fof(f759,definition,
( spl0_14
<=> nil = sk8 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f761,plain,
( nil = sk8
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f768,definition,
( spl0_16
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f770,plain,
( nil = sk7
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f772,definition,
( spl0_17
<=> sk7 = cons(hd(sk7),tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f774,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f777,definition,
( spl0_18
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f779,plain,
( nil = sk4
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f786,definition,
( spl0_20
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f787,plain,
( nil != sk3
| spl0_20 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f790,definition,
( spl0_21
<=> sk3 = cons(hd(sk3),tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f792,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f825,plain,
! [X0] :
( ssList(X0)
| nil = tl(X0)
| tl(X0) = cons(skaf83(tl(X0)),skaf82(tl(X0)))
| nil = X0 ),
inference(resolution,[],[f344,f310]) ).
fof(f842,definition,
( spl0_24
<=> sk7 = cons(skaf83(sk7),skaf82(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f844,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f857,plain,
( nil != sk3
| ssList(sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
inference(superposition,[],[f353,f218]) ).
fof(f863,plain,
( nil != sk3
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f857,f429]) ).
fof(f865,definition,
( spl0_27
<=> nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f867,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f869,definition,
( spl0_28
<=> ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f871,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f869]) ).
fof(f872,plain,
( spl0_27
| spl0_28
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f863,f786,f869,f865]) ).
fof(f885,plain,
( ! [X0,X1] :
( ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f355,f481]) ).
fof(f925,plain,
( ! [X0] : cons(X0,sk8) = app(cons(X0,nil),sk8)
| ~ spl0_10 ),
inference(resolution,[],[f885,f428]) ).
fof(f956,plain,
( segmentP(nil,sk3)
| ~ spl0_18 ),
inference(superposition,[],[f206,f779]) ).
fof(f958,plain,
( ssList(sk3)
| nil = sk3
| ~ spl0_18 ),
inference(resolution,[],[f956,f315]) ).
fof(f959,plain,
( nil = sk3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f958,f421]) ).
fof(f1007,definition,
( spl0_31
<=> ssList(tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f1008,plain,
( ~ ssList(tl(sk3))
| spl0_31 ),
inference(avatar_component_clause,[],[f1007]) ).
fof(f1009,plain,
( ssList(tl(sk3))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f1007]) ).
fof(f1011,definition,
( spl0_32
<=> ssItem(hd(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f1012,plain,
( ~ ssItem(hd(sk3))
| spl0_32 ),
inference(avatar_component_clause,[],[f1011]) ).
fof(f1013,plain,
( ssItem(hd(sk3))
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f1011]) ).
fof(f1073,plain,
! [X0] :
( ssList(X0)
| tl(cons(sk5,X0)) = X0 ),
inference(resolution,[],[f331,f425]) ).
fof(f1199,plain,
! [X0] :
( ssList(X0)
| cons(sk5,X0) = app(cons(sk5,nil),X0) ),
inference(resolution,[],[f355,f425]) ).
fof(f1277,definition,
( spl0_42
<=> nil = tl(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f1279,plain,
( nil = tl(sk3)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1339,plain,
( ssList(sk4)
| ssList(nil)
| nil = sk4
| ~ spl0_1 ),
inference(resolution,[],[f441,f335]) ).
fof(f1340,plain,
( ssList(nil)
| nil = sk4
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f1339,f422]) ).
fof(f1342,plain,
( nil = sk4
| ~ spl0_1
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1340,f453]) ).
fof(f1354,plain,
( spl0_20
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f959,f777,f786]) ).
fof(f1359,plain,
( spl0_18
| ~ spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f1342,f452,f439,f777]) ).
fof(f1482,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f379,f320]) ).
fof(f1483,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ssList(X0)
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(resolution,[],[f1482,f364]) ).
fof(f1490,plain,
( frontsegP(sk3,app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(sk9) ),
inference(superposition,[],[f1482,f218]) ).
fof(f1497,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1483]) ).
fof(f1498,plain,
( frontsegP(sk3,app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
inference(forward_subsumption_resolution,[],[f1490,f429]) ).
fof(f1499,plain,
! [X0,X1] :
( ~ frontsegP(X0,app(X0,X1))
| ssList(X1)
| ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1497,f320]) ).
fof(f1596,plain,
! [X0] :
( ssList(X0)
| ssList(X0)
| app(skaf46(X0,X0),X0) = X0
| ssList(X0) ),
inference(resolution,[],[f366,f294]) ).
fof(f1599,plain,
! [X0] :
( ssList(X0)
| app(skaf46(X0,X0),X0) = X0 ),
inference(duplicate_literal_removal,[],[f1596]) ).
fof(f1629,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,X2))
| frontsegP(app(app(X1,X2),X0),X1)
| ssList(X1)
| ssList(X2) ),
inference(resolution,[],[f372,f1482]) ).
fof(f1630,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,X2))
| frontsegP(app(app(X1,X2),X0),X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f1629]) ).
fof(f1634,plain,
! [X2,X0,X1] :
( frontsegP(app(app(X1,X2),X0),X1)
| ssList(X1)
| ssList(X0)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1630,f320]) ).
fof(f1640,plain,
( frontsegP(sk3,app(app(app(nil,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1498,f770]) ).
fof(f1761,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(app(X1,X2))
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X1)
| ssList(X2) ),
inference(resolution,[],[f389,f1482]) ).
fof(f1762,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(app(X1,X2))
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f1761]) ).
fof(f1766,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1762,f320]) ).
fof(f1903,plain,
! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| ssList(sk3)
| ssList(nil)
| nil = X0 ),
inference(superposition,[],[f385,f529]) ).
fof(f1916,plain,
! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1903,f421]) ).
fof(f1938,plain,
( ! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| nil = X0 )
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1916,f453]) ).
fof(f2002,plain,
! [X0] :
( sk8 != app(X0,sk8)
| ssList(X0)
| ssList(sk8)
| ssList(nil)
| nil = X0 ),
inference(superposition,[],[f386,f565]) ).
fof(f2021,plain,
! [X0] :
( sk8 != app(X0,sk8)
| ssList(X0)
| ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f2002,f428]) ).
fof(f2043,plain,
( ! [X0] :
( sk8 != app(X0,sk8)
| ssList(X0)
| nil = X0 )
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f2021,f453]) ).
fof(f2094,plain,
! [X0,X1] :
( ssList(nil)
| ssList(X0)
| ssItem(X1)
| frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) ),
inference(resolution,[],[f432,f295]) ).
fof(f2099,plain,
! [X0,X1] :
( ssList(nil)
| ssList(X0)
| ssItem(X1)
| frontsegP(cons(X1,X0),cons(X1,nil)) ),
inference(duplicate_literal_removal,[],[f2094]) ).
fof(f2102,plain,
( ! [X0,X1] :
( frontsegP(cons(X1,X0),cons(X1,nil))
| ssItem(X1)
| ssList(X0) )
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f2099,f453]) ).
fof(f2594,definition,
( spl0_79
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f2595,plain,
( ~ ssList(cons(sk6,nil))
| spl0_79 ),
inference(avatar_component_clause,[],[f2594]) ).
fof(f2596,plain,
( ssList(cons(sk6,nil))
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f2594]) ).
fof(f2620,plain,
( ssList(nil)
| ssItem(sk6)
| ~ spl0_79 ),
inference(resolution,[],[f2596,f321]) ).
fof(f2621,plain,
( ssItem(sk6)
| spl0_4
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f2620,f453]) ).
fof(f2622,plain,
( $false
| spl0_4
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f2621,f426]) ).
fof(f2623,plain,
( spl0_4
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f2622]) ).
fof(f2625,plain,
( cons(sk6,nil) = app(nil,cons(sk6,nil))
| spl0_79 ),
inference(resolution,[],[f2595,f309]) ).
fof(f2641,definition,
( spl0_83
<=> nil = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f2642,plain,
( nil != cons(sk6,nil)
| spl0_83 ),
inference(avatar_component_clause,[],[f2641]) ).
fof(f2643,plain,
( nil = cons(sk6,nil)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f2641]) ).
fof(f2696,plain,
( singletonP(nil)
| ssList(nil)
| ssItem(sk6)
| ~ spl0_83 ),
inference(superposition,[],[f351,f2643]) ).
fof(f2722,plain,
( ssList(nil)
| ssItem(sk6)
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f2696,f11]) ).
fof(f2733,plain,
( ssItem(sk6)
| spl0_4
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f2722,f453]) ).
fof(f2737,plain,
( $false
| spl0_4
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f2733,f426]) ).
fof(f2738,plain,
( spl0_4
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f2737]) ).
fof(f2756,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f414,f484]) ).
fof(f2784,definition,
( spl0_91
<=> ! [X3] : ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f2785,plain,
( ! [X3] : ssList(X3)
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f2784]) ).
fof(f2787,definition,
( spl0_92
<=> ! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,cons(X2,X0)))
| ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f2788,plain,
( ! [X2,X0,X1] :
( ssList(app(X1,cons(X2,X0)))
| ssList(X1)
| ssList(X0)
| ssItem(X2) )
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f2787]) ).
fof(f3014,plain,
sk7 = tl(cons(sk5,sk7)),
inference(resolution,[],[f1073,f427]) ).
fof(f3152,plain,
( cons(sk5,nil) = app(cons(sk5,nil),nil)
| spl0_4 ),
inference(resolution,[],[f1199,f453]) ).
fof(f3692,definition,
( spl0_119
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f3694,plain,
( nil = cons(sk5,nil)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f3692]) ).
fof(f3696,definition,
( spl0_120
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f3697,plain,
( ~ ssList(cons(sk5,nil))
| spl0_120 ),
inference(avatar_component_clause,[],[f3696]) ).
fof(f3698,plain,
( ssList(cons(sk5,nil))
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f3696]) ).
fof(f4025,plain,
( $false
| ~ spl0_91 ),
inference(backward_subsumption_resolution,[],[f429,f2785]) ).
fof(f4059,plain,
~ spl0_91,
inference(avatar_contradiction_clause,[],[f4025]) ).
fof(f4166,plain,
( ! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ssItem(X2)
| ssList(X3)
| ssList(X1)
| X1 = X3 )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f406,f481]) ).
fof(f4167,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| frontsegP(X1,X3) )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f409,f481]) ).
fof(f4169,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| X0 = X2 )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f411,f481]) ).
fof(f4203,plain,
( ! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ssList(X3)
| ssList(X1)
| X1 = X3 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f4166,f481]) ).
fof(f4204,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| frontsegP(X1,X3) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f4167,f481]) ).
fof(f4205,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| X0 = X2 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f4169,f481]) ).
fof(f5366,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_120 ),
inference(resolution,[],[f3698,f321]) ).
fof(f5367,plain,
( ssItem(sk5)
| spl0_4
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f5366,f453]) ).
fof(f5368,plain,
( $false
| spl0_4
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f5367,f425]) ).
fof(f5369,plain,
( spl0_4
| ~ spl0_120 ),
inference(avatar_contradiction_clause,[],[f5368]) ).
fof(f5430,definition,
( spl0_131
<=> ssList(app(app(app(sk7,cons(sk5,nil)),nil),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f5431,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),nil),cons(sk6,nil)))
| spl0_131 ),
inference(avatar_component_clause,[],[f5430]) ).
fof(f5432,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),nil),cons(sk6,nil)))
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f5430]) ).
fof(f5454,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| nil = sk7 ),
inference(resolution,[],[f427,f339]) ).
fof(f5489,plain,
( spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f5454,f772,f768]) ).
fof(f5668,definition,
( spl0_140
<=> nil = cons(sk5,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f5669,plain,
( nil != cons(sk5,sk7)
| spl0_140 ),
inference(avatar_component_clause,[],[f5668]) ).
fof(f5670,plain,
( nil = cons(sk5,sk7)
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f5668]) ).
fof(f5672,definition,
( spl0_141
<=> ssList(cons(sk5,sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f5673,plain,
( ~ ssList(cons(sk5,sk7))
| spl0_141 ),
inference(avatar_component_clause,[],[f5672]) ).
fof(f5674,plain,
( ssList(cons(sk5,sk7))
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f5672]) ).
fof(f5683,plain,
( ~ memberP(nil,sk5)
| ssItem(sk5)
| ssList(sk7)
| ~ spl0_140 ),
inference(superposition,[],[f434,f5670]) ).
fof(f5689,plain,
( ssItem(sk5)
| ssList(sk7)
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f5683,f306]) ).
fof(f5693,plain,
( ssList(sk7)
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f5689,f425]) ).
fof(f5695,plain,
( $false
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f5693,f427]) ).
fof(f5696,plain,
~ spl0_140,
inference(avatar_contradiction_clause,[],[f5695]) ).
fof(f5705,plain,
( ssList(sk7)
| ssItem(sk5)
| ~ spl0_141 ),
inference(resolution,[],[f5674,f321]) ).
fof(f5706,plain,
( ssItem(sk5)
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f5705,f427]) ).
fof(f5707,plain,
( $false
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f5706,f425]) ).
fof(f5708,plain,
~ spl0_141,
inference(avatar_contradiction_clause,[],[f5707]) ).
fof(f6111,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0)))
| ssList(cons(X2,X3)) )
| ~ spl0_11 ),
inference(resolution,[],[f2756,f320]) ).
fof(f6116,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0))) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f6111,f321]) ).
fof(f6119,plain,
( spl0_91
| spl0_92
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f6116,f483,f2787,f2784]) ).
fof(f6282,definition,
( spl0_162
<=> ssList(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f6283,plain,
( ~ ssList(sk9)
| spl0_162 ),
inference(avatar_component_clause,[],[f6282]) ).
fof(f6304,plain,
~ spl0_162,
inference(avatar_split_clause,[],[f429,f6282]) ).
fof(f6741,definition,
( spl0_200
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_200])],[avatar_definition]) ).
fof(f6743,plain,
( ssList(tl(sk7))
| ~ spl0_200 ),
inference(avatar_component_clause,[],[f6741]) ).
fof(f6745,definition,
( spl0_201
<=> ssItem(hd(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f6747,plain,
( ssItem(hd(sk7))
| ~ spl0_201 ),
inference(avatar_component_clause,[],[f6745]) ).
fof(f6851,plain,
( ssList(sk7)
| nil = sk7
| ~ spl0_200 ),
inference(resolution,[],[f6743,f310]) ).
fof(f6852,plain,
( nil = sk7
| ~ spl0_200 ),
inference(forward_subsumption_resolution,[],[f6851,f427]) ).
fof(f7000,plain,
( ssList(sk7)
| nil = sk7
| ~ spl0_201 ),
inference(resolution,[],[f6747,f311]) ).
fof(f7001,plain,
( nil = sk7
| ~ spl0_201 ),
inference(forward_subsumption_resolution,[],[f7000,f427]) ).
fof(f7289,plain,
( ssList(app(app(sk7,cons(sk5,nil)),nil))
| ssList(cons(sk6,nil))
| ~ spl0_131 ),
inference(resolution,[],[f5432,f320]) ).
fof(f7994,plain,
( ssList(app(app(sk7,cons(sk5,nil)),nil))
| spl0_79
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f7289,f2595]) ).
fof(f8028,definition,
( spl0_271
<=> ssList(app(app(sk7,cons(sk5,nil)),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_271])],[avatar_definition]) ).
fof(f8030,plain,
( ssList(app(app(sk7,cons(sk5,nil)),nil))
| ~ spl0_271 ),
inference(avatar_component_clause,[],[f8028]) ).
fof(f8034,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f421,f339]) ).
fof(f8085,plain,
( spl0_20
| spl0_21 ),
inference(avatar_split_clause,[],[f8034,f790,f786]) ).
fof(f8523,plain,
( ssList(sk3)
| nil = sk3
| ~ spl0_31 ),
inference(resolution,[],[f1009,f310]) ).
fof(f8524,plain,
( nil = sk3
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f8523,f421]) ).
fof(f8525,plain,
( $false
| spl0_20
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f8524,f787]) ).
fof(f8526,plain,
( spl0_20
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f8525]) ).
fof(f8669,plain,
( ssList(sk3)
| nil = sk3
| ~ spl0_32 ),
inference(resolution,[],[f1013,f311]) ).
fof(f8670,plain,
( nil = sk3
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f8669,f421]) ).
fof(f8671,plain,
( $false
| spl0_20
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f8670,f787]) ).
fof(f8672,plain,
( spl0_20
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f8671]) ).
fof(f9592,plain,
( sk3 = cons(hd(sk3),nil)
| ~ spl0_21
| ~ spl0_42 ),
inference(superposition,[],[f792,f1279]) ).
fof(f17293,plain,
( frontsegP(sk3,app(app(app(nil,cons(sk5,nil)),nil),cons(sk6,nil)))
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1640,f761]) ).
fof(f17300,plain,
( spl0_16
| ~ spl0_201 ),
inference(avatar_split_clause,[],[f7001,f6745,f768]) ).
fof(f17414,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),nil),cons(sk6,nil)))
| frontsegP(sk3,app(app(app(nil,cons(sk5,nil)),nil),cons(sk6,nil)))
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_demodulation,[],[f17293,f761]) ).
fof(f17457,plain,
( spl0_16
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f6852,f6741,f768]) ).
fof(f21356,plain,
( frontsegP(sk7,cons(hd(sk7),nil))
| ssItem(hd(sk7))
| ssList(tl(sk7))
| spl0_4
| ~ spl0_17 ),
inference(superposition,[],[f2102,f774]) ).
fof(f21949,plain,
( ! [X0] :
( ssList(app(X0,sk3))
| ssList(X0)
| ssList(tl(sk3))
| ssItem(hd(sk3)) )
| ~ spl0_21
| ~ spl0_92 ),
inference(superposition,[],[f2788,f792]) ).
fof(f21959,plain,
( ! [X0] :
( ssList(app(X0,sk3))
| ssList(X0)
| ssItem(hd(sk3)) )
| ~ spl0_21
| spl0_31
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f21949,f1008]) ).
fof(f21969,plain,
( ! [X0] :
( ssList(app(X0,sk3))
| ssList(X0) )
| ~ spl0_21
| spl0_31
| spl0_32
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f21959,f1012]) ).
fof(f23140,definition,
( spl0_639
<=> frontsegP(sk7,cons(hd(sk7),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_639])],[avatar_definition]) ).
fof(f23142,plain,
( frontsegP(sk7,cons(hd(sk7),nil))
| ~ spl0_639 ),
inference(avatar_component_clause,[],[f23140]) ).
fof(f23143,plain,
( spl0_200
| spl0_201
| spl0_639
| spl0_4
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f21356,f772,f452,f23140,f6745,f6741]) ).
fof(f29276,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),sk8))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(sk9)
| ssList(cons(sk6,nil)) ),
inference(superposition,[],[f1634,f218]) ).
fof(f29285,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),sk8))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| spl0_162 ),
inference(forward_subsumption_resolution,[],[f29276,f6283]) ).
fof(f29290,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),sk8))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_79
| spl0_162 ),
inference(forward_subsumption_resolution,[],[f29285,f2595]) ).
fof(f30796,definition,
( spl0_811
<=> sk3 = cons(hd(sk3),nil) ),
introduced(definition,[new_symbols(definition,[spl0_811])],[avatar_definition]) ).
fof(f30798,plain,
( sk3 = cons(hd(sk3),nil)
| ~ spl0_811 ),
inference(avatar_component_clause,[],[f30796]) ).
fof(f31913,plain,
( ! [X0] :
( ssList(X0)
| ssList(X0)
| ssList(sk3) )
| ~ spl0_21
| spl0_31
| spl0_32
| ~ spl0_92 ),
inference(resolution,[],[f21969,f320]) ).
fof(f31917,plain,
( ! [X0] :
( ssList(X0)
| ssList(sk3) )
| ~ spl0_21
| spl0_31
| spl0_32
| ~ spl0_92 ),
inference(duplicate_literal_removal,[],[f31913]) ).
fof(f31923,plain,
( ! [X0] : ssList(X0)
| ~ spl0_21
| spl0_31
| spl0_32
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f31917,f421]) ).
fof(f31926,plain,
( spl0_91
| ~ spl0_21
| spl0_31
| spl0_32
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f31923,f2787,f1011,f1007,f790,f2784]) ).
fof(f33231,definition,
( spl0_1015
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_1015])],[avatar_definition]) ).
fof(f33232,plain,
( ~ ssList(sk8)
| spl0_1015 ),
inference(avatar_component_clause,[],[f33231]) ).
fof(f33512,definition,
( spl0_1044
<=> frontsegP(sk3,app(app(nil,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_1044])],[avatar_definition]) ).
fof(f33514,plain,
( frontsegP(sk3,app(app(nil,cons(sk5,nil)),sk8))
| ~ spl0_1044 ),
inference(avatar_component_clause,[],[f33512]) ).
fof(f33527,plain,
~ spl0_1015,
inference(avatar_split_clause,[],[f428,f33231]) ).
fof(f33630,plain,
( sk8 = app(skaf46(sk8,sk8),sk8)
| spl0_1015 ),
inference(resolution,[],[f33232,f1599]) ).
fof(f35159,plain,
( ! [X0] : cons(X0,cons(sk6,nil)) = app(cons(X0,nil),cons(sk6,nil))
| ~ spl0_10
| spl0_79 ),
inference(resolution,[],[f885,f2595]) ).
fof(f35491,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ssList(nil)
| ssList(X1)
| nil = X1 )
| ~ spl0_2
| ~ spl0_10 ),
inference(superposition,[],[f4203,f682]) ).
fof(f35502,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ssList(X1)
| nil = X1 )
| ~ spl0_2
| spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f35491,f453]) ).
fof(f35523,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(nil)
| frontsegP(nil,X1) )
| ~ spl0_2
| ~ spl0_10 ),
inference(superposition,[],[f4204,f682]) ).
fof(f35546,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| frontsegP(nil,X1) )
| ~ spl0_2
| spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f35523,f453]) ).
fof(f35564,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(tl(sk3))
| hd(sk3) = X0 )
| ~ spl0_10
| ~ spl0_21 ),
inference(superposition,[],[f4205,f792]) ).
fof(f35586,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| hd(sk3) = X0 )
| ~ spl0_10
| ~ spl0_21
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f35564,f1008]) ).
fof(f42804,plain,
( spl0_811
| ~ spl0_21
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f9592,f1277,f790,f30796]) ).
fof(f43884,plain,
( ! [X0] : cons(X0,sk7) = app(nil,cons(X0,sk7))
| ~ spl0_10 ),
inference(resolution,[],[f594,f427]) ).
fof(f43888,plain,
( ! [X0] : cons(X0,nil) = app(nil,cons(X0,nil))
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f43884,f770]) ).
fof(f85306,plain,
( nil = tl(cons(sk5,sk7))
| tl(cons(sk5,sk7)) = cons(skaf83(tl(cons(sk5,sk7))),skaf82(tl(cons(sk5,sk7))))
| nil = cons(sk5,sk7)
| spl0_141 ),
inference(resolution,[],[f825,f5673]) ).
fof(f85360,plain,
( nil = tl(cons(sk5,sk7))
| tl(cons(sk5,sk7)) = cons(skaf83(tl(cons(sk5,sk7))),skaf82(tl(cons(sk5,sk7))))
| spl0_140
| spl0_141 ),
inference(forward_subsumption_resolution,[],[f85306,f5669]) ).
fof(f85383,plain,
( nil = sk7
| tl(cons(sk5,sk7)) = cons(skaf83(tl(cons(sk5,sk7))),skaf82(tl(cons(sk5,sk7))))
| spl0_140
| spl0_141 ),
inference(forward_demodulation,[],[f85360,f3014]) ).
fof(f92102,plain,
( frontsegP(sk8,skaf46(sk8,sk8))
| ssList(skaf46(sk8,sk8))
| ssList(sk8)
| spl0_1015 ),
inference(superposition,[],[f1482,f33630]) ).
fof(f92120,plain,
( frontsegP(sk8,skaf46(sk8,sk8))
| ssList(sk8)
| spl0_1015 ),
inference(forward_subsumption_resolution,[],[f92102,f286]) ).
fof(f92130,plain,
( frontsegP(sk8,skaf46(sk8,sk8))
| spl0_1015 ),
inference(forward_subsumption_resolution,[],[f92120,f33232]) ).
fof(f92136,definition,
( spl0_1861
<=> sk8 = skaf46(sk8,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_1861])],[avatar_definition]) ).
fof(f92138,plain,
( sk8 = skaf46(sk8,sk8)
| ~ spl0_1861 ),
inference(avatar_component_clause,[],[f92136]) ).
fof(f92140,definition,
( spl0_1862
<=> frontsegP(skaf46(sk8,sk8),sk8) ),
introduced(definition,[new_symbols(definition,[spl0_1862])],[avatar_definition]) ).
fof(f92142,plain,
( ~ frontsegP(skaf46(sk8,sk8),sk8)
| spl0_1862 ),
inference(avatar_component_clause,[],[f92140]) ).
fof(f93803,plain,
( ~ frontsegP(skaf46(sk8,sk8),sk8)
| ssList(skaf46(sk8,sk8))
| ssList(sk8)
| sk8 = skaf46(sk8,sk8)
| spl0_1015 ),
inference(resolution,[],[f92130,f364]) ).
fof(f93804,plain,
( ~ frontsegP(skaf46(sk8,sk8),sk8)
| ssList(sk8)
| sk8 = skaf46(sk8,sk8)
| spl0_1015 ),
inference(forward_subsumption_resolution,[],[f93803,f286]) ).
fof(f93809,plain,
( ~ frontsegP(skaf46(sk8,sk8),sk8)
| sk8 = skaf46(sk8,sk8)
| spl0_1015 ),
inference(forward_subsumption_resolution,[],[f93804,f33232]) ).
fof(f93814,plain,
( spl0_1861
| ~ spl0_1862
| spl0_1015 ),
inference(avatar_split_clause,[],[f93809,f33231,f92140,f92136]) ).
fof(f117059,plain,
( ~ frontsegP(nil,cons(sk6,nil))
| ssList(cons(sk6,nil))
| ssList(nil)
| nil = cons(sk6,nil)
| spl0_79 ),
inference(superposition,[],[f1499,f2625]) ).
fof(f128324,plain,
( sk8 != sk8
| ssList(skaf46(sk8,sk8))
| nil = skaf46(sk8,sk8)
| spl0_4
| spl0_1015 ),
inference(superposition,[],[f2043,f33630]) ).
fof(f128326,plain,
( ssList(skaf46(sk8,sk8))
| nil = skaf46(sk8,sk8)
| spl0_4
| spl0_1015 ),
inference(trivial_inequality_removal,[],[f128324]) ).
fof(f128327,plain,
( nil = skaf46(sk8,sk8)
| spl0_4
| spl0_1015 ),
inference(forward_subsumption_resolution,[],[f128326,f286]) ).
fof(f133693,plain,
( sk3 != sk3
| ssList(tl(sk3))
| nil = tl(sk3)
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_21 ),
inference(superposition,[],[f35502,f792]) ).
fof(f133698,plain,
( ssList(tl(sk3))
| nil = tl(sk3)
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_21 ),
inference(trivial_inequality_removal,[],[f133693]) ).
fof(f133960,plain,
( nil = sk8
| spl0_4
| spl0_1015
| ~ spl0_1861 ),
inference(forward_demodulation,[],[f92138,f128327]) ).
fof(f134047,plain,
( ~ frontsegP(nil,sk8)
| spl0_4
| spl0_1015
| spl0_1862 ),
inference(forward_demodulation,[],[f92142,f128327]) ).
fof(f134281,definition,
( spl0_3764
<=> ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_3764])],[avatar_definition]) ).
fof(f134283,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_3764 ),
inference(avatar_component_clause,[],[f134281]) ).
fof(f134285,definition,
( spl0_3765
<=> frontsegP(sk3,app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_3765])],[avatar_definition]) ).
fof(f134287,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_3765 ),
inference(avatar_component_clause,[],[f134285]) ).
fof(f134288,plain,
( spl0_3764
| spl0_3765
| spl0_79
| spl0_162 ),
inference(avatar_split_clause,[],[f29290,f6282,f2594,f134285,f134281]) ).
fof(f135400,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| nil = sk7
| spl0_140
| spl0_141 ),
inference(forward_demodulation,[],[f85383,f3014]) ).
fof(f135755,definition,
( spl0_3887
<=> sk3 = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_3887])],[avatar_definition]) ).
fof(f135756,plain,
( sk3 = sk7
| ~ spl0_3887 ),
inference(avatar_component_clause,[],[f135755]) ).
fof(f135769,definition,
( spl0_3890
<=> frontsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_3890])],[avatar_definition]) ).
fof(f135770,plain,
( frontsegP(sk3,sk7)
| ~ spl0_3890 ),
inference(avatar_component_clause,[],[f135769]) ).
fof(f136437,plain,
( spl0_16
| spl0_24
| spl0_140
| spl0_141 ),
inference(avatar_split_clause,[],[f135400,f5672,f5668,f842,f768]) ).
fof(f138912,plain,
( hd(sk7) = skaf83(sk7)
| ~ spl0_10
| ~ spl0_24 ),
inference(superposition,[],[f644,f844]) ).
fof(f139388,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| ~ spl0_28 ),
inference(resolution,[],[f871,f320]) ).
fof(f139389,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_28
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f139388,f2595]) ).
fof(f139390,plain,
( spl0_3764
| ~ spl0_28
| spl0_79 ),
inference(avatar_split_clause,[],[f139389,f2594,f869,f134281]) ).
fof(f140406,definition,
( spl0_4221
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_4221])],[avatar_definition]) ).
fof(f140407,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_4221 ),
inference(avatar_component_clause,[],[f140406]) ).
fof(f140408,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_4221 ),
inference(avatar_component_clause,[],[f140406]) ).
fof(f140415,plain,
( spl0_271
| spl0_79
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f7994,f5430,f2594,f8028]) ).
fof(f140416,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(nil)
| ~ spl0_271 ),
inference(resolution,[],[f8030,f320]) ).
fof(f140417,plain,
( ssList(app(sk7,cons(sk5,nil)))
| spl0_4
| ~ spl0_271 ),
inference(forward_subsumption_resolution,[],[f140416,f453]) ).
fof(f140418,plain,
( spl0_4221
| spl0_4
| ~ spl0_271 ),
inference(avatar_split_clause,[],[f140417,f8028,f452,f140406]) ).
fof(f143283,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_4221 ),
inference(resolution,[],[f140408,f320]) ).
fof(f143284,plain,
( ssList(cons(sk5,nil))
| ~ spl0_4221 ),
inference(forward_subsumption_resolution,[],[f143283,f427]) ).
fof(f143285,plain,
( $false
| spl0_120
| ~ spl0_4221 ),
inference(forward_subsumption_resolution,[],[f143284,f3697]) ).
fof(f143286,plain,
( spl0_120
| ~ spl0_4221 ),
inference(avatar_contradiction_clause,[],[f143285]) ).
fof(f148815,plain,
( nil = tl(sk3)
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_21
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f133698,f1008]) ).
fof(f149101,plain,
( spl0_42
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_21
| spl0_31 ),
inference(avatar_split_clause,[],[f148815,f1007,f790,f480,f452,f443,f1277]) ).
fof(f160508,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_3764 ),
inference(resolution,[],[f134283,f320]) ).
fof(f160509,plain,
( ssList(sk8)
| ~ spl0_3764
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f160508,f140407]) ).
fof(f160510,plain,
( $false
| spl0_1015
| ~ spl0_3764
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f160509,f33232]) ).
fof(f160511,plain,
( spl0_1015
| ~ spl0_3764
| spl0_4221 ),
inference(avatar_contradiction_clause,[],[f160510]) ).
fof(f161657,plain,
( nil != nil
| ssList(cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_27 ),
inference(superposition,[],[f354,f867]) ).
fof(f161682,plain,
( ssList(cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_27 ),
inference(trivial_inequality_removal,[],[f161657]) ).
fof(f161707,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_27
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f161682,f2595]) ).
fof(f161785,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_27
| spl0_79
| spl0_83 ),
inference(forward_subsumption_resolution,[],[f161707,f2642]) ).
fof(f161856,plain,
( spl0_3764
| ~ spl0_27
| spl0_79
| spl0_83 ),
inference(avatar_split_clause,[],[f161785,f2641,f2594,f865,f134281]) ).
fof(f167829,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(sk3)
| frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_3765 ),
inference(resolution,[],[f134287,f1766]) ).
fof(f167840,plain,
( ssList(sk3)
| frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_3765
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f167829,f140407]) ).
fof(f167846,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_3765
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f167840,f421]) ).
fof(f167856,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| spl0_1015
| ~ spl0_3765
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f167846,f33232]) ).
fof(f214530,definition,
( spl0_7517
<=> hd(sk3) = hd(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_7517])],[avatar_definition]) ).
fof(f214532,plain,
( hd(sk3) = hd(sk7)
| ~ spl0_7517 ),
inference(avatar_component_clause,[],[f214530]) ).
fof(f214534,definition,
( spl0_7518
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_7518])],[avatar_definition]) ).
fof(f214890,plain,
( ~ frontsegP(sk3,sk7)
| ssList(skaf82(sk7))
| hd(sk3) = skaf83(sk7)
| ~ spl0_10
| ~ spl0_21
| ~ spl0_24
| spl0_31 ),
inference(superposition,[],[f35586,f844]) ).
fof(f253010,plain,
( ssList(sk7)
| ssList(sk3)
| frontsegP(sk3,sk7)
| ssList(cons(sk5,nil))
| spl0_1015
| ~ spl0_3765
| spl0_4221 ),
inference(resolution,[],[f167856,f1766]) ).
fof(f253021,plain,
( ssList(sk3)
| frontsegP(sk3,sk7)
| ssList(cons(sk5,nil))
| spl0_1015
| ~ spl0_3765
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f253010,f427]) ).
fof(f253027,plain,
( frontsegP(sk3,sk7)
| ssList(cons(sk5,nil))
| spl0_1015
| ~ spl0_3765
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f253021,f421]) ).
fof(f253042,plain,
( ~ frontsegP(sk3,sk7)
| hd(sk3) = skaf83(sk7)
| ~ spl0_10
| ~ spl0_21
| ~ spl0_24
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f214890,f249]) ).
fof(f253054,plain,
( frontsegP(sk3,sk7)
| spl0_120
| spl0_1015
| ~ spl0_3765
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f253027,f3697]) ).
fof(f253057,plain,
( hd(sk3) = hd(sk7)
| ~ frontsegP(sk3,sk7)
| ~ spl0_10
| ~ spl0_21
| ~ spl0_24
| spl0_31 ),
inference(forward_demodulation,[],[f253042,f138912]) ).
fof(f253066,plain,
( spl0_3890
| spl0_120
| spl0_1015
| ~ spl0_3765
| spl0_4221 ),
inference(avatar_split_clause,[],[f253054,f140406,f134285,f33231,f3696,f135769]) ).
fof(f253067,plain,
( ~ spl0_3890
| spl0_7517
| ~ spl0_10
| ~ spl0_21
| ~ spl0_24
| spl0_31 ),
inference(avatar_split_clause,[],[f253057,f1007,f842,f790,f480,f214530,f135769]) ).
fof(f253078,plain,
( ~ frontsegP(sk7,sk3)
| ssList(sk7)
| ssList(sk3)
| sk3 = sk7
| ~ spl0_3890 ),
inference(resolution,[],[f135770,f364]) ).
fof(f254104,plain,
( frontsegP(sk7,cons(hd(sk3),nil))
| ~ spl0_639
| ~ spl0_7517 ),
inference(superposition,[],[f23142,f214532]) ).
fof(f254133,plain,
( frontsegP(sk7,sk3)
| ~ spl0_639
| ~ spl0_811
| ~ spl0_7517 ),
inference(forward_demodulation,[],[f254104,f30798]) ).
fof(f254246,plain,
( ~ frontsegP(sk7,sk3)
| ssList(sk3)
| sk3 = sk7
| ~ spl0_3890 ),
inference(forward_subsumption_resolution,[],[f253078,f427]) ).
fof(f254249,plain,
( spl0_7518
| ~ spl0_639
| ~ spl0_811
| ~ spl0_7517 ),
inference(avatar_split_clause,[],[f254133,f214530,f30796,f23140,f214534]) ).
fof(f254322,plain,
( ~ frontsegP(sk7,sk3)
| sk3 = sk7
| ~ spl0_3890 ),
inference(forward_subsumption_resolution,[],[f254246,f421]) ).
fof(f254360,plain,
( spl0_3887
| ~ spl0_7518
| ~ spl0_3890 ),
inference(avatar_split_clause,[],[f254322,f135769,f214534,f135755]) ).
fof(f254629,plain,
( frontsegP(sk3,app(sk3,cons(sk5,nil)))
| spl0_1015
| ~ spl0_3765
| ~ spl0_3887
| spl0_4221 ),
inference(superposition,[],[f167856,f135756]) ).
fof(f320700,definition,
( spl0_9523
<=> sk3 = app(sk3,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_9523])],[avatar_definition]) ).
fof(f320702,plain,
( sk3 = app(sk3,cons(sk5,nil))
| ~ spl0_9523 ),
inference(avatar_component_clause,[],[f320700]) ).
fof(f325020,plain,
( sk3 != sk3
| ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_4
| ~ spl0_9523 ),
inference(superposition,[],[f1938,f320702]) ).
fof(f325065,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_4
| ~ spl0_9523 ),
inference(trivial_inequality_removal,[],[f325020]) ).
fof(f325091,plain,
( nil = cons(sk5,nil)
| spl0_4
| spl0_120
| ~ spl0_9523 ),
inference(forward_subsumption_resolution,[],[f325065,f3697]) ).
fof(f326067,plain,
( ~ frontsegP(nil,cons(sk6,nil))
| ssList(nil)
| nil = cons(sk6,nil)
| ~ spl0_10
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f117059,f592]) ).
fof(f328146,plain,
( spl0_119
| spl0_4
| spl0_120
| ~ spl0_9523 ),
inference(avatar_split_clause,[],[f325091,f320700,f3696,f452,f3692]) ).
fof(f328262,plain,
( ~ frontsegP(nil,cons(sk6,nil))
| ssList(nil)
| ~ spl0_10
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f326067,f600]) ).
fof(f329062,plain,
( ~ frontsegP(nil,cons(sk6,nil))
| spl0_4
| ~ spl0_10
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f328262,f453]) ).
fof(f334652,plain,
( singletonP(nil)
| ssList(nil)
| ~ spl0_10
| ~ spl0_119 ),
inference(superposition,[],[f710,f3694]) ).
fof(f334828,plain,
( ssList(nil)
| ~ spl0_10
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f334652,f11]) ).
fof(f334878,plain,
( $false
| spl0_4
| ~ spl0_10
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f334828,f453]) ).
fof(f334879,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f334878]) ).
fof(f608882,plain,
( ssList(cons(sk5,nil))
| ssList(sk3)
| sk3 = app(sk3,cons(sk5,nil))
| spl0_1015
| ~ spl0_3765
| ~ spl0_3887
| spl0_4221 ),
inference(resolution,[],[f254629,f1499]) ).
fof(f608895,plain,
( ssList(sk3)
| sk3 = app(sk3,cons(sk5,nil))
| spl0_120
| spl0_1015
| ~ spl0_3765
| ~ spl0_3887
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f608882,f3697]) ).
fof(f608901,plain,
( sk3 = app(sk3,cons(sk5,nil))
| spl0_120
| spl0_1015
| ~ spl0_3765
| ~ spl0_3887
| spl0_4221 ),
inference(forward_subsumption_resolution,[],[f608895,f421]) ).
fof(f608903,plain,
( spl0_9523
| spl0_120
| spl0_1015
| ~ spl0_3765
| ~ spl0_3887
| spl0_4221 ),
inference(avatar_split_clause,[],[f608901,f140406,f135755,f134285,f33231,f3696,f320700]) ).
fof(f614576,plain,
( frontsegP(sk3,app(app(nil,cons(sk5,nil)),sk8))
| ~ spl0_16
| ~ spl0_3765 ),
inference(superposition,[],[f134287,f770]) ).
fof(f614805,plain,
( spl0_1044
| ~ spl0_16
| ~ spl0_3765 ),
inference(avatar_split_clause,[],[f614576,f134285,f768,f33512]) ).
fof(f621857,plain,
( frontsegP(sk3,app(cons(sk5,nil),sk8))
| ~ spl0_10
| ~ spl0_16
| ~ spl0_1044 ),
inference(superposition,[],[f33514,f43888]) ).
fof(f621993,plain,
( frontsegP(sk3,cons(sk5,sk8))
| ~ spl0_10
| ~ spl0_16
| ~ spl0_1044 ),
inference(forward_demodulation,[],[f621857,f925]) ).
fof(f631272,plain,
( ssList(sk8)
| frontsegP(nil,sk8)
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_16
| ~ spl0_1044 ),
inference(resolution,[],[f621993,f35546]) ).
fof(f631282,plain,
( frontsegP(nil,sk8)
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_16
| spl0_1015
| ~ spl0_1044 ),
inference(forward_subsumption_resolution,[],[f631272,f33232]) ).
fof(f631289,plain,
( $false
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_16
| spl0_1015
| ~ spl0_1044
| spl0_1862 ),
inference(forward_subsumption_resolution,[],[f631282,f134047]) ).
fof(f631290,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_16
| spl0_1015
| ~ spl0_1044
| spl0_1862 ),
inference(avatar_contradiction_clause,[],[f631289]) ).
fof(f631305,plain,
( frontsegP(sk3,app(app(app(nil,cons(sk5,nil)),nil),cons(sk6,nil)))
| ~ spl0_14
| ~ spl0_16
| spl0_131 ),
inference(forward_subsumption_resolution,[],[f17414,f5431]) ).
fof(f631517,plain,
( spl0_14
| spl0_4
| spl0_1015
| ~ spl0_1861 ),
inference(avatar_split_clause,[],[f133960,f92136,f33231,f452,f759]) ).
fof(f631746,plain,
( frontsegP(sk3,app(app(cons(sk5,nil),nil),cons(sk6,nil)))
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_131 ),
inference(forward_demodulation,[],[f631305,f43888]) ).
fof(f631921,plain,
( frontsegP(sk3,app(cons(sk5,nil),cons(sk6,nil)))
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_131 ),
inference(forward_demodulation,[],[f631746,f3152]) ).
fof(f631999,plain,
( frontsegP(sk3,cons(sk5,cons(sk6,nil)))
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_79
| spl0_131 ),
inference(forward_demodulation,[],[f631921,f35159]) ).
fof(f637901,plain,
( ssList(cons(sk6,nil))
| frontsegP(nil,cons(sk6,nil))
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_79
| spl0_131 ),
inference(resolution,[],[f631999,f35546]) ).
fof(f637912,plain,
( frontsegP(nil,cons(sk6,nil))
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_79
| spl0_131 ),
inference(forward_subsumption_resolution,[],[f637901,f2595]) ).
fof(f637920,plain,
( $false
| ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_79
| spl0_131 ),
inference(forward_subsumption_resolution,[],[f637912,f329062]) ).
fof(f637921,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_79
| spl0_131 ),
inference(avatar_contradiction_clause,[],[f637920]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f446]) ).
cnf(s8,plain,
( spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f485]) ).
cnf(s11,plain,
~ spl0_4,
inference(sat_conversion,[],[f488]) ).
cnf(s22,plain,
( ~ spl0_20
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f872]) ).
cnf(s47,plain,
( ~ spl0_18
| spl0_20 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s50,plain,
( ~ spl0_1
| spl0_4
| spl0_18 ),
inference(sat_conversion,[],[f1359]) ).
cnf(s81,plain,
( spl0_4
| ~ spl0_79 ),
inference(sat_conversion,[],[f2623]) ).
cnf(s91,plain,
( spl0_4
| ~ spl0_83 ),
inference(sat_conversion,[],[f2738]) ).
cnf(s175,plain,
~ spl0_91,
inference(sat_conversion,[],[f4059]) ).
cnf(s193,plain,
( spl0_4
| ~ spl0_120 ),
inference(sat_conversion,[],[f5369]) ).
cnf(s207,plain,
( spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f5489]) ).
cnf(s219,plain,
~ spl0_140,
inference(sat_conversion,[],[f5696]) ).
cnf(s220,plain,
~ spl0_141,
inference(sat_conversion,[],[f5708]) ).
cnf(s236,plain,
( ~ spl0_11
| spl0_91
| spl0_92 ),
inference(sat_conversion,[],[f6119]) ).
cnf(s255,plain,
~ spl0_162,
inference(sat_conversion,[],[f6304]) ).
cnf(s416,plain,
( spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f8085]) ).
cnf(s457,plain,
( spl0_20
| ~ spl0_31 ),
inference(sat_conversion,[],[f8526]) ).
cnf(s476,plain,
( spl0_20
| ~ spl0_32 ),
inference(sat_conversion,[],[f8672]) ).
cnf(s864,plain,
( spl0_16
| ~ spl0_201 ),
inference(sat_conversion,[],[f17300]) ).
cnf(s912,plain,
( spl0_16
| ~ spl0_200 ),
inference(sat_conversion,[],[f17457]) ).
cnf(s1129,plain,
( spl0_4
| ~ spl0_17
| spl0_200
| spl0_201
| spl0_639 ),
inference(sat_conversion,[],[f23143]) ).
cnf(s1670,plain,
( ~ spl0_21
| spl0_31
| spl0_32
| spl0_91
| ~ spl0_92 ),
inference(sat_conversion,[],[f31926]) ).
cnf(s1984,plain,
~ spl0_1015,
inference(sat_conversion,[],[f33527]) ).
cnf(s3007,plain,
( ~ spl0_21
| ~ spl0_42
| spl0_811 ),
inference(sat_conversion,[],[f42804]) ).
cnf(s3769,plain,
( spl0_1015
| spl0_1861
| ~ spl0_1862 ),
inference(sat_conversion,[],[f93814]) ).
cnf(s6227,plain,
( spl0_79
| spl0_162
| spl0_3764
| spl0_3765 ),
inference(sat_conversion,[],[f134288]) ).
cnf(s6480,plain,
( spl0_16
| spl0_24
| spl0_140
| spl0_141 ),
inference(sat_conversion,[],[f136437]) ).
cnf(s6888,plain,
( ~ spl0_28
| spl0_79
| spl0_3764 ),
inference(sat_conversion,[],[f139390]) ).
cnf(s6985,plain,
( spl0_79
| ~ spl0_131
| spl0_271 ),
inference(sat_conversion,[],[f140415]) ).
cnf(s6987,plain,
( spl0_4
| ~ spl0_271
| spl0_4221 ),
inference(sat_conversion,[],[f140418]) ).
cnf(s7024,plain,
( spl0_120
| ~ spl0_4221 ),
inference(sat_conversion,[],[f143286]) ).
cnf(s7730,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_21
| spl0_31
| spl0_42 ),
inference(sat_conversion,[],[f149101]) ).
cnf(s9122,plain,
( spl0_1015
| ~ spl0_3764
| spl0_4221 ),
inference(sat_conversion,[],[f160511]) ).
cnf(s9252,plain,
( ~ spl0_27
| spl0_79
| spl0_83
| spl0_3764 ),
inference(sat_conversion,[],[f161856]) ).
cnf(s13154,plain,
( spl0_120
| spl0_1015
| ~ spl0_3765
| spl0_3890
| spl0_4221 ),
inference(sat_conversion,[],[f253066]) ).
cnf(s13155,plain,
( ~ spl0_10
| ~ spl0_21
| ~ spl0_24
| spl0_31
| ~ spl0_3890
| spl0_7517 ),
inference(sat_conversion,[],[f253067]) ).
cnf(s13573,plain,
( ~ spl0_639
| ~ spl0_811
| ~ spl0_7517
| spl0_7518 ),
inference(sat_conversion,[],[f254249]) ).
cnf(s13582,plain,
( spl0_3887
| ~ spl0_3890
| ~ spl0_7518 ),
inference(sat_conversion,[],[f254360]) ).
cnf(s16064,plain,
( spl0_4
| spl0_119
| spl0_120
| ~ spl0_9523 ),
inference(sat_conversion,[],[f328146]) ).
cnf(s17133,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_119 ),
inference(sat_conversion,[],[f334879]) ).
cnf(s21735,plain,
( spl0_120
| spl0_1015
| ~ spl0_3765
| ~ spl0_3887
| spl0_4221
| spl0_9523 ),
inference(sat_conversion,[],[f608903]) ).
cnf(s22397,plain,
( ~ spl0_16
| spl0_1044
| ~ spl0_3765 ),
inference(sat_conversion,[],[f614805]) ).
cnf(s23088,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_16
| spl0_1015
| ~ spl0_1044
| spl0_1862 ),
inference(sat_conversion,[],[f631290]) ).
cnf(s23111,plain,
( spl0_4
| spl0_14
| spl0_1015
| ~ spl0_1861 ),
inference(sat_conversion,[],[f631517]) ).
cnf(s23650,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_16
| spl0_79
| spl0_131 ),
inference(sat_conversion,[],[f637921]) ).
cnf(s23973,plain,
~ spl0_120,
inference(rat,[],[s193,s11]) ).
cnf(s23975,plain,
~ spl0_83,
inference(rat,[],[s91,s11]) ).
cnf(s23976,plain,
~ spl0_79,
inference(rat,[],[s81,s11]) ).
cnf(s23999,plain,
~ spl0_4221,
inference(rat,[],[s7024,s23973]) ).
cnf(s24015,plain,
~ spl0_3764,
inference(rat,[],[s9122,s1984,s23999]) ).
cnf(s24016,plain,
~ spl0_271,
inference(rat,[],[s6987,s11,s23999]) ).
cnf(s24225,plain,
spl0_3765,
inference(rat,[],[s6227,s23976,s255,s24015]) ).
cnf(s24226,plain,
~ spl0_27,
inference(rat,[],[s9252,s23976,s23975,s24015]) ).
cnf(s24227,plain,
~ spl0_28,
inference(rat,[],[s6888,s23976,s24015]) ).
cnf(s24228,plain,
~ spl0_131,
inference(rat,[],[s6985,s23976,s24016]) ).
cnf(s24229,plain,
spl0_3890,
inference(rat,[],[s13154,s23999,s23973,s1984,s24225]) ).
cnf(s24230,plain,
~ spl0_20,
inference(rat,[],[s22,s24227,s24226]) ).
cnf(s24332,plain,
~ spl0_32,
inference(rat,[],[s476,s24230]) ).
cnf(s24333,plain,
~ spl0_31,
inference(rat,[],[s457,s24230]) ).
cnf(s24334,plain,
spl0_21,
inference(rat,[],[s416,s24230]) ).
cnf(s24340,plain,
~ spl0_18,
inference(rat,[],[s47,s24230]) ).
cnf(s24661,plain,
~ spl0_92,
inference(rat,[],[s1670,s24333,s175,s24332,s24334]) ).
cnf(s24891,plain,
~ spl0_1,
inference(rat,[],[s50,s11,s24340]) ).
cnf(s24892,plain,
~ spl0_11,
inference(rat,[],[s236,s175,s24661]) ).
cnf(s25520,plain,
spl0_10,
inference(rat,[],[s8,s24892]) ).
cnf(s25559,plain,
~ spl0_119,
inference(rat,[],[s17133,s11,s25520]) ).
cnf(s25821,plain,
~ spl0_9523,
inference(rat,[],[s16064,s23973,s11,s25559]) ).
cnf(s27046,plain,
~ spl0_3887,
inference(rat,[],[s21735,s24225,s23999,s23973,s1984,s25821]) ).
cnf(s27650,plain,
~ spl0_7518,
inference(rat,[],[s13582,s24229,s27046]) ).
cnf(s27748,plain,
spl0_2,
inference(rat,[],[s1,s24891]) ).
cnf(s27762,plain,
spl0_42,
inference(rat,[],[s7730,s25520,s24333,s24334,s11,s27748]) ).
cnf(s27885,plain,
spl0_811,
inference(rat,[],[s3007,s24334,s27762]) ).
cnf(s27941,plain,
spl0_16,
inference(rat,[],[s13573,s1129,s13155,s207,s864,s912,s6480,s27885,s27650,s11,s24334,s24333,s24229,s25520,s219,s220]) ).
cnf(s27953,plain,
spl0_1044,
inference(rat,[],[s22397,s24225,s27941]) ).
cnf(s28095,plain,
~ spl0_14,
inference(rat,[],[s23650,s24228,s23976,s27748,s25520,s11,s27941]) ).
cnf(s28097,plain,
spl0_1862,
inference(rat,[],[s23088,s27941,s27748,s1984,s25520,s11,s27953]) ).
cnf(s28299,plain,
~ spl0_1861,
inference(rat,[],[s23111,s11,s1984,s28095]) ).
cnf(s28338,plain,
$false,
inference(rat,[],[s3769,s1984,s28097,s28299]) ).
fof(f637931,plain,
$false,
inference(avatar_sat_refutation,[],[s28338]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC307-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.07/0.19 % Computer : n020.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 09:01:19 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 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
% 25.35/3.90 % (42512)Will run a generic schedule for satisfiability detection.
% 25.35/3.90 % (42523)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=654211030:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 25.35/3.90 % (42518)% WARNING: option uhcvi not known.
% 25.35/3.90 % (42517)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2002127105_2999 on theBenchmark for (2999ds/0Mi)
% 25.35/3.90 % (42519)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=973724566:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 25.35/3.90 % (42520)dis+10_1_sil=32000:sp=arity:random_seed=2563735936:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 25.35/3.90 % (42518)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=902859049:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 25.35/3.90 % (42522)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2208544862:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 25.35/3.90 % (42521)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3602421790:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 25.35/3.90 % TRYING [1]
% 25.35/3.90 % TRYING [2]
% 25.35/3.90 % TRYING [3]
% 25.35/3.90 % TRYING [4]
% 25.35/3.90 % (42523)Instruction limit reached!
% 25.35/3.90 % (42523)------------------------------
% 25.35/3.90 % (42523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.35/3.90 % (42523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/3.90 % (42523)CaDiCaL version: 2.1.3
% 25.35/3.90 % (42523)Termination reason: Instruction limit
% 25.35/3.90 % (42523)Termination phase: Saturation
% 25.35/3.90 % (42523)Time elapsed: 0.049 s
% 25.35/3.90 % (42523)Peak memory usage: 14 MB
% 25.35/3.90 % (42523)Instructions burned: 161 (million)
% 25.35/3.90 % (42531)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3094151130:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 25.35/3.90 % (42520)Instruction limit reached!
% 25.35/3.90 % (42520)------------------------------
% 25.35/3.90 % (42520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.35/3.90 % (42520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/3.90 % (42520)CaDiCaL version: 2.1.3
% 25.35/3.90 % (42520)Termination reason: Instruction limit
% 25.35/3.90 % (42520)Termination phase: Saturation
% 25.35/3.90 % (42520)Time elapsed: 0.056 s
% 25.35/3.90 % (42520)Peak memory usage: 13 MB
% 25.35/3.90 % (42520)Instructions burned: 103 (million)
% 25.35/3.90 % (42521)Instruction limit reached!
% 25.35/3.90 % (42521)------------------------------
% 25.35/3.90 % (42521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.35/3.90 % (42521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/3.90 % (42521)CaDiCaL version: 2.1.3
% 25.35/3.90 % (42521)Termination reason: Instruction limit
% 25.35/3.90 % (42521)Termination phase: Saturation
% 25.35/3.90 % (42521)Time elapsed: 0.058 s
% 25.35/3.90 % (42521)Peak memory usage: 13 MB
% 25.35/3.90 % (42521)Instructions burned: 117 (million)
% 25.35/3.90 % TRYING [1]
% 25.35/3.90 % TRYING [2]
% 25.35/3.90 % TRYING [3]
% 25.35/3.90 % (42522)Instruction limit reached!
% 25.35/3.90 % (42522)------------------------------
% 25.35/3.90 % (42522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.35/3.90 % (42522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/3.90 % (42522)CaDiCaL version: 2.1.3
% 25.35/3.90 % (42522)Termination reason: Instruction limit
% 25.35/3.90 % (42522)Termination phase: Saturation
% 25.35/3.90 % (42522)Time elapsed: 0.065 s
% 25.35/3.90 % (42522)Peak memory usage: 14 MB
% 25.35/3.90 % (42522)Instructions burned: 131 (million)
% 25.35/3.90 % TRYING [4]
% 25.35/3.90 % (42533)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3766799635:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 25.35/3.90 % (42534)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=1766745552:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 25.35/3.90 % (42535)ott-21_1_sil=16000:fs=off:random_seed=1682546052:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 25.35/3.90 % TRYING [5]
% 25.35/3.90 % TRYING [5]
% 25.35/3.90 % (42533)Instruction limit reached!
% 25.35/3.90 % (42533)------------------------------
% 25.35/3.90 % (42533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.35/3.90 % (42533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.91/6.76 % (42533)CaDiCaL version: 2.1.3
% 45.91/6.76 % (42533)Termination reason: Instruction limit
% 45.91/6.76 % (42533)Termination phase: Saturation
% 45.91/6.76 % (42533)Time elapsed: 0.070 s
% 45.91/6.76 % (42533)Peak memory usage: 14 MB
% 45.91/6.76 % (42533)Instructions burned: 132 (million)
% 45.91/6.76 % (42539)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3515808021:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 45.91/6.76 % (42535)Instruction limit reached!
% 45.91/6.76 % (42535)------------------------------
% 45.91/6.76 % (42535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.91/6.76 % (42535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.91/6.76 % (42535)CaDiCaL version: 2.1.3
% 45.91/6.76 % (42535)Termination reason: Instruction limit
% 45.91/6.76 % (42535)Termination phase: Saturation
% 45.91/6.76 % (42535)Time elapsed: 0.092 s
% 45.91/6.76 % (42535)Peak memory usage: 13 MB
% 45.91/6.76 % (42535)Instructions burned: 187 (million)
% 45.91/6.76 % (42541)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1134381755:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 45.91/6.76 % TRYING [6]
% 45.91/6.76 % TRYING [1]
% 45.91/6.76 % TRYING [2]
% 45.91/6.76 % (42531)Instruction limit reached!
% 45.91/6.76 % (42531)------------------------------
% 45.91/6.76 % (42531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.91/6.76 % (42531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.91/6.76 % (42531)CaDiCaL version: 2.1.3
% 45.91/6.76 % (42531)Termination reason: Instruction limit
% 45.91/6.76 % (42531)Termination phase: Finite model building constraint generation
% 45.91/6.76 % (42531)Time elapsed: 0.153 s
% 45.91/6.76 % (42531)Peak memory usage: 34 MB
% 45.91/6.76 % (42531)Instructions burned: 722 (million)
% 45.91/6.76 % TRYING [3]
% 45.91/6.76 % (42543)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=108336528:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 45.91/6.76 % TRYING [4]
% 45.91/6.76 % TRYING [6]
% 45.91/6.76 % TRYING [5]
% 45.91/6.76 % (42534)Instruction limit reached!
% 45.91/6.76 % (42534)------------------------------
% 45.91/6.76 % (42534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.91/6.76 % (42534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.91/6.76 % (42534)CaDiCaL version: 2.1.3
% 45.91/6.76 % (42534)Termination reason: Instruction limit
% 45.91/6.76 % (42534)Termination phase: Saturation
% 45.91/6.76 % (42534)Time elapsed: 0.376 s
% 45.91/6.76 % (42534)Peak memory usage: 21 MB
% 45.91/6.76 % (42534)Instructions burned: 685 (million)
% 45.91/6.76 % (42539)Instruction limit reached!
% 45.91/6.76 % (42539)------------------------------
% 45.91/6.76 % (42539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.91/6.76 % (42539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.91/6.76 % (42539)CaDiCaL version: 2.1.3
% 45.91/6.76 % (42539)Termination reason: Instruction limit
% 45.91/6.76 % (42539)Termination phase: Saturation
% 45.91/6.76 % (42539)Time elapsed: 0.293 s
% 45.91/6.76 % (42539)Peak memory usage: 13 MB
% 45.91/6.76 % (42539)Instructions burned: 478 (million)
% 45.91/6.76 % (42545)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1671853903:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 45.91/6.76 % (42546)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=4003510793:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 45.91/6.76 % (42541)Instruction limit reached!
% 45.91/6.76 % (42541)------------------------------
% 45.91/6.76 % (42541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.91/6.76 % (42541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.91/6.76 % (42541)CaDiCaL version: 2.1.3
% 45.91/6.76 % (42541)Termination reason: Instruction limit
% 45.91/6.76 % (42541)Termination phase: Finite model building SAT solving
% 45.91/6.76 % (42541)Time elapsed: 0.338 s
% 45.91/6.76 % (42541)Peak memory usage: 22 MB
% 45.91/6.76 % (42541)Instructions burned: 866 (million)
% 45.91/6.76 % (42549)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1377780169:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 45.91/6.76 % TRYING [14]
% 45.91/6.76 % (42543)Instruction limit reached!
% 45.91/6.76 % (42543)------------------------------
% 45.91/6.76 % (42543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.91/6.76 % (42543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.00/13.93 % (42543)CaDiCaL version: 2.1.3
% 97.00/13.93 % (42543)Termination reason: Instruction limit
% 97.00/13.93 % (42543)Termination phase: Saturation
% 97.00/13.93 % (42543)Time elapsed: 0.378 s
% 97.00/13.93 % (42543)Peak memory usage: 26 MB
% 97.00/13.93 % (42543)Instructions burned: 1181 (million)
% 97.00/13.93 % (42551)fmb+10_1_sil=64000:random_seed=2102767791:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 97.00/13.93 % TRYING [1]
% 97.00/13.93 % TRYING [2]
% 97.00/13.93 % TRYING [3]
% 97.00/13.93 % TRYING [4]
% 97.00/13.93 % TRYING [5]
% 97.00/13.93 % TRYING [7]
% 97.00/13.93 % (42545)Instruction limit reached!
% 97.00/13.93 % (42545)------------------------------
% 97.00/13.93 % (42545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.00/13.93 % (42545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.00/13.93 % (42545)CaDiCaL version: 2.1.3
% 97.00/13.93 % (42545)Termination reason: Instruction limit
% 97.00/13.93 % (42545)Termination phase: Finite model building constraint generation
% 97.00/13.93 % (42545)Time elapsed: 0.327 s
% 97.00/13.93 % (42545)Peak memory usage: 73 MB
% 97.00/13.93 % (42545)Instructions burned: 891 (million)
% 97.00/13.93 % (42553)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=875866762:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 97.00/13.93 % TRYING [20]
% 97.00/13.93 % (42546)Instruction limit reached!
% 97.00/13.93 % (42546)------------------------------
% 97.00/13.93 % (42546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.00/13.93 % (42546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.00/13.93 % (42546)CaDiCaL version: 2.1.3
% 97.00/13.93 % (42546)Termination reason: Instruction limit
% 97.00/13.93 % (42546)Termination phase: Saturation
% 97.00/13.93 % (42546)Time elapsed: 0.374 s
% 97.00/13.93 % (42546)Peak memory usage: 21 MB
% 97.00/13.93 % (42546)Instructions burned: 692 (million)
% 97.00/13.93 % (42555)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2098672169:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 97.00/13.93 % TRYING [8]
% 97.00/13.93 % TRYING [6]
% 97.00/13.93 % (42549)Instruction limit reached!
% 97.00/13.93 % (42549)------------------------------
% 97.00/13.93 % (42549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.00/13.93 % (42549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.00/13.93 % (42549)CaDiCaL version: 2.1.3
% 97.00/13.93 % (42549)Termination reason: Instruction limit
% 97.00/13.93 % (42549)Termination phase: Saturation
% 97.00/13.93 % (42549)Time elapsed: 0.485 s
% 97.00/13.93 % (42549)Peak memory usage: 20 MB
% 97.00/13.93 % (42549)Instructions burned: 880 (million)
% 97.00/13.93 % (42557)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=540100123:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 97.00/13.93 % (42555)Instruction limit reached!
% 97.00/13.93 % (42555)------------------------------
% 97.00/13.93 % (42555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.00/13.93 % (42555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.00/13.93 % (42555)CaDiCaL version: 2.1.3
% 97.00/13.93 % (42555)Termination reason: Instruction limit
% 97.00/13.93 % (42555)Termination phase: Finite model building constraint generation
% 97.00/13.93 % (42555)Time elapsed: 0.333 s
% 97.00/13.93 % (42555)Peak memory usage: 79 MB
% 97.00/13.93 % (42555)Instructions burned: 923 (million)
% 97.00/13.93 % (42559)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1622777123:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 97.00/13.93 % TRYING [7]
% 97.00/13.93 % (42559)Instruction limit reached!
% 97.00/13.93 % (42559)------------------------------
% 97.00/13.93 % (42559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.00/13.93 % (42559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.00/13.93 % (42559)CaDiCaL version: 2.1.3
% 97.00/13.93 % (42559)Termination reason: Instruction limit
% 97.00/13.93 % (42559)Termination phase: Saturation
% 97.00/13.93 % (42559)Time elapsed: 0.631 s
% 97.00/13.93 % (42559)Peak memory usage: 15 MB
% 97.00/13.93 % (42559)Instructions burned: 1473 (million)
% 97.00/13.93 % (42561)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1602426886:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 97.00/13.93 % TRYING [77]
% 97.00/13.93 % TRYING [8]
% 97.00/13.93 % TRYING [8]
% 97.00/13.93 % (42557)Instruction limit reached!
% 97.00/13.93 % (42557)------------------------------
% 97.00/13.93 % (42557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.00/13.93 % (42557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.00/13.93 % (42557)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42557)Termination reason: Instruction limit
% 50.28/17.44 % (42557)Termination phase: Saturation
% 50.28/17.44 % (42557)Time elapsed: 2.572 s
% 50.28/17.44 % (42557)Peak memory usage: 52 MB
% 50.28/17.44 % (42557)Instructions burned: 5132 (million)
% 50.28/17.44 % (42563)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2193583333:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 50.28/17.44 % TRYING [16]
% 50.28/17.44 % (42553)Instruction limit reached!
% 50.28/17.44 % (42553)------------------------------
% 50.28/17.44 % (42553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42553)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42553)Termination reason: Instruction limit
% 50.28/17.44 % (42553)Termination phase: Finite model building constraint generation
% 50.28/17.44 % (42553)Time elapsed: 3.272 s
% 50.28/17.44 % (42553)Peak memory usage: 589 MB
% 50.28/17.44 % (42553)Instructions burned: 9518 (million)
% 50.28/17.44 % (42561)Instruction limit reached!
% 50.28/17.44 % (42561)------------------------------
% 50.28/17.44 % (42561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42561)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42561)Termination reason: Instruction limit
% 50.28/17.44 % (42561)Termination phase: Finite model building constraint generation
% 50.28/17.44 % (42561)Time elapsed: 2.261 s
% 50.28/17.44 % (42561)Peak memory usage: 427 MB
% 50.28/17.44 % (42561)Instructions burned: 6326 (million)
% 50.28/17.44 % (42565)ott-2_1_sil=16000:newcnf=on:random_seed=4242367077:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 50.28/17.44 % (42567)ott+10_1_sil=32000:tgt=ground:random_seed=198593353:i=5114:av=off_2957 on theBenchmark for (2957ds/5114Mi)
% 50.28/17.44 % (42563)Instruction limit reached!
% 50.28/17.44 % (42563)------------------------------
% 50.28/17.44 % (42563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42563)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42563)Termination reason: Instruction limit
% 50.28/17.44 % (42563)Termination phase: Finite model building constraint generation
% 50.28/17.44 % (42563)Time elapsed: 0.749 s
% 50.28/17.44 % (42563)Peak memory usage: 138 MB
% 50.28/17.44 % (42563)Instructions burned: 2175 (million)
% 50.28/17.44 % (42569)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2083481889:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 50.28/17.44 % TRYING [1]
% 50.28/17.44 % TRYING [2]
% 50.28/17.44 % TRYING [3]
% 50.28/17.44 % TRYING [4]
% 50.28/17.44 % TRYING [5]
% 50.28/17.44 % TRYING [9]
% 50.28/17.44 % (42565)Instruction limit reached!
% 50.28/17.44 % (42565)------------------------------
% 50.28/17.44 % (42565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42565)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42565)Termination reason: Instruction limit
% 50.28/17.44 % (42565)Termination phase: Saturation
% 50.28/17.44 % (42565)Time elapsed: 0.440 s
% 50.28/17.44 % (42565)Peak memory usage: 22 MB
% 50.28/17.44 % (42565)Instructions burned: 871 (million)
% 50.28/17.44 % (42571)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2964858384:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi)
% 50.28/17.44 % TRYING [6]
% 50.28/17.44 % TRYING [9]
% 50.28/17.44 % TRYING [7]
% 50.28/17.44 % (42551)Instruction limit reached!
% 50.28/17.44 % (42551)------------------------------
% 50.28/17.44 % (42551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42551)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42551)Termination reason: Instruction limit
% 50.28/17.44 % (42551)Termination phase: Finite model building constraint generation
% 50.28/17.44 % (42551)Time elapsed: 4.791 s
% 50.28/17.44 % (42551)Peak memory usage: 241 MB
% 50.28/17.44 % (42551)Instructions burned: 22062 (million)
% 50.28/17.44 % (42573)dis+21_1_sil=32000:sas=cadical:random_seed=2817870158:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 50.28/17.44 % TRYING [8]
% 50.28/17.44 % (42571)Instruction limit reached!
% 50.28/17.44 % (42571)------------------------------
% 50.28/17.44 % (42571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42571)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42571)Termination reason: Instruction limit
% 50.28/17.44 % (42571)Termination phase: Saturation
% 50.28/17.44 % (42571)Time elapsed: 1.835 s
% 50.28/17.44 % (42571)Peak memory usage: 40 MB
% 50.28/17.44 % (42571)Instructions burned: 3512 (million)
% 50.28/17.44 % (42573)Instruction limit reached!
% 50.28/17.44 % (42573)------------------------------
% 50.28/17.44 % (42573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42573)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42573)Termination reason: Instruction limit
% 50.28/17.44 % (42573)Termination phase: Saturation
% 50.28/17.44 % (42573)Time elapsed: 1.068 s
% 50.28/17.44 % (42573)Peak memory usage: 41 MB
% 50.28/17.44 % (42573)Instructions burned: 3774 (million)
% 50.28/17.44 % (42575)ott+11_1_sil=16000:gs=on:random_seed=739363209:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi)
% 50.28/17.44 % (42576)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2198441591:fmbsr=1.6:i=67534_2934 on theBenchmark for (2934ds/67534Mi)
% 50.28/17.44 % TRYING [7]
% 50.28/17.44 % (42567)Instruction limit reached!
% 50.28/17.44 % (42567)------------------------------
% 50.28/17.44 % (42567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42567)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42567)Termination reason: Instruction limit
% 50.28/17.44 % (42567)Termination phase: Saturation
% 50.28/17.44 % (42567)Time elapsed: 2.774 s
% 50.28/17.44 % (42567)Peak memory usage: 69 MB
% 50.28/17.44 % (42567)Instructions burned: 5115 (million)
% 50.28/17.44 % (42579)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1381820190:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2929 on theBenchmark for (2929ds/4591Mi)
% 50.28/17.44 % (42575)Instruction limit reached!
% 50.28/17.44 % (42575)------------------------------
% 50.28/17.44 % (42575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42575)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42575)Termination reason: Instruction limit
% 50.28/17.44 % (42575)Termination phase: Saturation
% 50.28/17.44 % (42575)Time elapsed: 0.962 s
% 50.28/17.44 % (42575)Peak memory usage: 17 MB
% 50.28/17.44 % (42575)Instructions burned: 2252 (million)
% 50.28/17.44 % (42581)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1419734661:i=29340_2924 on theBenchmark for (2924ds/29340Mi)
% 50.28/17.44 % TRYING [8]
% 50.28/17.44 % TRYING [9]
% 50.28/17.44 % TRYING [10]
% 50.28/17.44 % (42579)Instruction limit reached!
% 50.28/17.44 % (42579)------------------------------
% 50.28/17.44 % (42579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42579)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42579)Termination reason: Instruction limit
% 50.28/17.44 % (42579)Termination phase: Saturation
% 50.28/17.44 % (42579)Time elapsed: 2.175 s
% 50.28/17.44 % (42579)Peak memory usage: 57 MB
% 50.28/17.44 % (42579)Instructions burned: 4591 (million)
% 50.28/17.44 % (42583)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=913323172:i=5211_2907 on theBenchmark for (2907ds/5211Mi)
% 50.28/17.44 % TRYING [9]
% 50.28/17.44 % TRYING [10]
% 50.28/17.44 % (42583)Instruction limit reached!
% 50.28/17.44 % (42583)------------------------------
% 50.28/17.44 % (42583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42583)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42583)Termination reason: Instruction limit
% 50.28/17.44 % (42583)Termination phase: Saturation
% 50.28/17.44 % (42583)Time elapsed: 2.542 s
% 50.28/17.44 % (42583)Peak memory usage: 48 MB
% 50.28/17.44 % (42583)Instructions burned: 5212 (million)
% 50.28/17.44 % (42585)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3134064425:i=5497:nm=2_2881 on theBenchmark for (2881ds/5497Mi)
% 50.28/17.44 % TRYING [17]
% 50.28/17.44 % (42585)Instruction limit reached!
% 50.28/17.44 % (42585)------------------------------
% 50.28/17.44 % (42585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.44 % (42585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.44 % (42585)CaDiCaL version: 2.1.3
% 50.28/17.44 % (42585)Termination reason: Instruction limit
% 50.28/17.44 % (42585)Termination phase: Finite model building constraint generation
% 50.28/17.44 % (42585)Time elapsed: 1.859 s
% 50.28/17.44 % (42585)Peak memory usage: 344 MB
% 50.28/17.44 % (42585)Instructions burned: 5499 (million)
% 50.28/17.44 % (42587)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2536335163:fmbsr=2:i=46332_2862 on theBenchmark for (2862ds/46332Mi)
% 50.28/17.44 % TRYING [15]
% 50.28/17.44 % TRYING [10]
% 50.28/17.44 % (42518) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-42512-42518"...
% 50.28/17.44 % (42518)...printing done.
% 50.28/17.44 % (42518)Refutation found. Thanks to Tanya!
% 50.28/17.44 % SZS status Unsatisfiable for theBenchmark
% 50.28/17.44 % SZS output start Proof for theBenchmark
% See solution above
% 50.28/17.45 % (42518)------------------------------
% 50.28/17.45 % (42518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.28/17.45 % (42518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.28/17.45 % (42518)CaDiCaL version: 2.1.3
% 50.28/17.45 % (42518)Termination reason: Refutation
% 50.28/17.45 % (42518)Time elapsed: 17.010 s
% 50.28/17.45 % (42518)Peak memory usage: 267 MB
% 50.28/17.45 % (42518)Instructions burned: 32837 (million)
% 50.28/17.45 % (42512)Success in time 17.209 s
% 50.28/17.45 % Vampire exiting
%------------------------------------------------------------------------------