CSE_E---1.7.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : SWC245-1 : TPTP v9.2.1. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d

% Computer : n015.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 05:18:52 PM UTC 2026

% Result   : Unsatisfiable 200.82s 107.98s
% Output   : CNFRefutation 209.11s
% Verified : 
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_660)

% Comments : 
%------------------------------------------------------------------------------
cnf(co1_12,negated_conjecture,
    ( ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1
    | ~ leq(X1,sk5(X3,X2,X1)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).

cnf(clause185,axiom,
    ( ~ leq(X1,X2)
    | ~ leq(X2,X1)
    | app(app(X3,cons(X1,X4)),cons(X2,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X4)
    | ~ ssList(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1)
    | ~ cyclefreeP(X6)
    | ~ ssList(X6) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause185) ).

cnf(co1_9,negated_conjecture,
    ( memberP(X2,sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).

cnf(co1_10,negated_conjecture,
    ( memberP(X3,sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).

cnf(co1_11,negated_conjecture,
    ( lt(X1,sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).

cnf(co1_8,negated_conjecture,
    ( ssItem(sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).

cnf(clause183,axiom,
    ( lt(X2,X4)
    | lt(X4,X2)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ strictorderP(X6)
    | ~ ssList(X6) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause183) ).

cnf(clause184,axiom,
    ( leq(X2,X4)
    | leq(X4,X2)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ totalorderP(X6)
    | ~ ssList(X6) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause184) ).

cnf(clause181,axiom,
    ( lt(X2,X4)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ strictorderedP(X6)
    | ~ ssList(X6) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause181) ).

cnf(clause182,axiom,
    ( leq(X2,X4)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ totalorderedP(X6)
    | ~ ssList(X6) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause182) ).

cnf(clause179,axiom,
    ( app(app(X1,cons(X2,X3)),cons(X2,X4)) != X5
    | ~ ssList(X4)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2)
    | ~ duplicatefreeP(X5)
    | ~ ssList(X5) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).

cnf(clause167,axiom,
    ( cyclefreeP(X1)
    | app(app(skaf51(X1),cons(skaf49(X1),skaf52(X1))),cons(skaf50(X1),skaf53(X1))) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause167) ).

cnf(clause166,axiom,
    ( totalorderP(X1)
    | app(app(skaf56(X1),cons(skaf54(X1),skaf57(X1))),cons(skaf55(X1),skaf58(X1))) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause166) ).

cnf(clause165,axiom,
    ( strictorderP(X1)
    | app(app(skaf61(X1),cons(skaf59(X1),skaf62(X1))),cons(skaf60(X1),skaf63(X1))) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause165) ).

cnf(clause164,axiom,
    ( totalorderedP(X1)
    | app(app(skaf66(X1),cons(skaf64(X1),skaf67(X1))),cons(skaf65(X1),skaf68(X1))) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause164) ).

cnf(clause163,axiom,
    ( strictorderedP(X1)
    | app(app(skaf71(X1),cons(skaf69(X1),skaf72(X1))),cons(skaf70(X1),skaf73(X1))) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause163) ).

cnf(clause162,axiom,
    ( duplicatefreeP(X1)
    | app(app(skaf75(X1),cons(skaf74(X1),skaf76(X1))),cons(skaf74(X1),skaf77(X1))) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause162) ).

cnf(clause180,axiom,
    ( X2 = X3
    | app(X1,cons(X2,cons(X3,X4))) != X5
    | ~ ssList(X4)
    | ~ ssList(X1)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ equalelemsP(X5)
    | ~ ssList(X5) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause180) ).

cnf(clause142,axiom,
    ( equalelemsP(X1)
    | app(skaf80(X1),cons(skaf78(X1),cons(skaf79(X1),skaf81(X1)))) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause142) ).

cnf(clause168,axiom,
    ( app(app(skaf47(X1,X2),X2),skaf48(X2,X1)) = X1
    | ~ segmentP(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause168) ).

cnf(clause169,axiom,
    ( app(skaf42(X1,X2),cons(X2,skaf43(X2,X1))) = X1
    | ~ memberP(X1,X2)
    | ~ ssItem(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause169) ).

cnf(clause174,axiom,
    ( frontsegP(X2,X4)
    | ~ frontsegP(cons(X1,X2),cons(X3,X4))
    | ~ ssList(X4)
    | ~ ssList(X2)
    | ~ ssItem(X3)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause174) ).

cnf(clause172,axiom,
    ( segmentP(app(app(X4,X1),X3),X2)
    | ~ segmentP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X4)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause172) ).

cnf(co1_16,negated_conjecture,
    ( ~ ssItem(X1)
    | ~ ssList(X2)
    | app(cons(X1,nil),X2) != sk6
    | ~ ssList(X3)
    | app(X3,cons(X1,nil)) != sk3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_16) ).

cnf(clause176,axiom,
    ( X1 = X3
    | ~ frontsegP(cons(X1,X2),cons(X3,X4))
    | ~ ssList(X4)
    | ~ ssList(X2)
    | ~ ssItem(X3)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause176) ).

cnf(clause178,axiom,
    ( frontsegP(cons(X3,X1),cons(X4,X2))
    | ~ frontsegP(X1,X2)
    | X3 != X4
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause178) ).

cnf(clause158,axiom,
    ( memberP(X2,X3)
    | memberP(X1,X3)
    | ~ memberP(app(X1,X2),X3)
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssItem(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause158) ).

cnf(clause173,axiom,
    ( segmentP(X4,X2)
    | app(app(X1,X2),X3) != X4
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X4) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause173) ).

cnf(clause175,axiom,
    ( memberP(X4,X2)
    | app(X1,cons(X2,X3)) != X4
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2)
    | ~ ssList(X4) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause175) ).

cnf(clause161,axiom,
    ( memberP(X2,X3)
    | X3 = X1
    | ~ memberP(cons(X1,X2),X3)
    | ~ ssList(X2)
    | ~ ssItem(X1)
    | ~ ssItem(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause161) ).

cnf(clause149,axiom,
    ( app(app(X3,X2),X1) = app(X3,app(X2,X1))
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause149) ).

cnf(clause157,axiom,
    ( cons(X1,app(X2,X3)) = app(cons(X1,X2),X3)
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause157) ).

cnf(clause159,axiom,
    ( totalorderedP(cons(X1,X2))
    | nil = X2
    | ~ leq(X1,hd(X2))
    | ~ totalorderedP(X2)
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause159) ).

cnf(clause160,axiom,
    ( strictorderedP(cons(X1,X2))
    | nil = X2
    | ~ lt(X1,hd(X2))
    | ~ strictorderedP(X2)
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause160) ).

cnf(clause140,axiom,
    ( memberP(app(X1,X3),X2)
    | ~ memberP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause140) ).

cnf(clause141,axiom,
    ( memberP(app(X3,X1),X2)
    | ~ memberP(X1,X2)
    | ~ ssList(X1)
    | ~ ssList(X3)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause141) ).

cnf(clause139,axiom,
    ( memberP(cons(X3,X1),X2)
    | ~ memberP(X1,X2)
    | ~ ssList(X1)
    | ~ ssItem(X3)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause139) ).

cnf(clause137,axiom,
    ( frontsegP(app(X1,X3),X2)
    | ~ frontsegP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause137) ).

cnf(clause136,axiom,
    ( rearsegP(app(X3,X1),X2)
    | ~ rearsegP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause136) ).

cnf(clause134,axiom,
    ( lt(X1,hd(X2))
    | nil = X2
    | ~ strictorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause134) ).

cnf(clause135,axiom,
    ( leq(X1,hd(X2))
    | nil = X2
    | ~ totalorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause135) ).

cnf(clause146,axiom,
    ( gt(X1,X3)
    | ~ gt(X1,X2)
    | ~ gt(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause146) ).

cnf(clause155,axiom,
    ( lt(X1,X3)
    | ~ lt(X1,X2)
    | ~ lt(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause155) ).

cnf(clause147,axiom,
    ( lt(X1,X3)
    | ~ leq(X1,X2)
    | ~ lt(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause147) ).

cnf(clause156,axiom,
    ( leq(X1,X3)
    | ~ leq(X1,X2)
    | ~ leq(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause156) ).

cnf(clause154,axiom,
    ( frontsegP(X1,X3)
    | ~ frontsegP(X1,X2)
    | ~ frontsegP(X2,X3)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause154) ).

cnf(clause153,axiom,
    ( rearsegP(X1,X3)
    | ~ rearsegP(X1,X2)
    | ~ rearsegP(X2,X3)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause153) ).

cnf(clause152,axiom,
    ( segmentP(X1,X3)
    | ~ segmentP(X1,X2)
    | ~ segmentP(X2,X3)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause152) ).

cnf(clause148,axiom,
    ( geq(X1,X3)
    | ~ geq(X1,X2)
    | ~ geq(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause148) ).

cnf(clause131,axiom,
    ( app(skaf46(X1,X2),X2) = X1
    | ~ rearsegP(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause131) ).

cnf(clause132,axiom,
    ( app(X2,skaf45(X1,X2)) = X1
    | ~ frontsegP(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause132) ).

cnf(clause170,axiom,
    ( X1 = X3
    | cons(X1,X2) != cons(X3,X4)
    | ~ ssItem(X3)
    | ~ ssItem(X1)
    | ~ ssList(X4)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause170) ).

cnf(clause171,axiom,
    ( X4 = X2
    | cons(X1,X2) != cons(X3,X4)
    | ~ ssItem(X3)
    | ~ ssItem(X1)
    | ~ ssList(X4)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause171) ).

cnf(clause125,axiom,
    ( totalorderedP(X2)
    | nil = X2
    | ~ totalorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause125) ).

cnf(clause124,axiom,
    ( strictorderedP(X2)
    | nil = X2
    | ~ strictorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause124) ).

cnf(clause151,axiom,
    ( X1 = X3
    | app(X1,X2) != app(X3,X2)
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause151) ).

cnf(clause150,axiom,
    ( X2 = X3
    | app(X1,X2) != app(X1,X3)
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssList(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause150) ).

cnf(clause133,axiom,
    ( nil = X2
    | tl(app(X2,X1)) = app(tl(X2),X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause133) ).

cnf(clause138,axiom,
    ( memberP(cons(X2,X3),X1)
    | X1 != X2
    | ~ ssList(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause138) ).

cnf(clause120,axiom,
    ( app(cons(X1,nil),X2) = cons(X1,X2)
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause120) ).

cnf(clause130,axiom,
    ( X2 = X1
    | ~ leq(X1,X2)
    | ~ leq(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause130) ).

cnf(clause126,axiom,
    ( X2 = X1
    | ~ geq(X1,X2)
    | ~ geq(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause126) ).

cnf(clause129,axiom,
    ( X2 = X1
    | ~ frontsegP(X1,X2)
    | ~ frontsegP(X2,X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause129) ).

cnf(clause128,axiom,
    ( X2 = X1
    | ~ rearsegP(X1,X2)
    | ~ rearsegP(X2,X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause128) ).

cnf(clause127,axiom,
    ( X2 = X1
    | ~ segmentP(X1,X2)
    | ~ segmentP(X2,X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause127) ).

cnf(clause144,axiom,
    ( frontsegP(X3,X1)
    | app(X1,X2) != X3
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssList(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause144) ).

cnf(clause143,axiom,
    ( rearsegP(X3,X2)
    | app(X1,X2) != X3
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause143) ).

cnf(clause110,axiom,
    ( ~ gt(X1,X2)
    | ~ gt(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause110) ).

cnf(clause114,axiom,
    ( ~ lt(X1,X2)
    | ~ lt(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause114) ).

cnf(clause122,axiom,
    ( lt(X1,X2)
    | X1 = X2
    | ~ leq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause122) ).

cnf(clause121,axiom,
    ( lt(X1,X2)
    | X1 = X2
    | ~ leq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause121) ).

cnf(clause95,axiom,
    ( totalorderP(X1)
    | ~ leq(skaf54(X1),skaf55(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause95) ).

cnf(clause94,axiom,
    ( totalorderP(X1)
    | ~ leq(skaf55(X1),skaf54(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause94) ).

cnf(clause93,axiom,
    ( strictorderP(X1)
    | ~ lt(skaf59(X1),skaf60(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause93) ).

cnf(clause92,axiom,
    ( strictorderP(X1)
    | ~ lt(skaf60(X1),skaf59(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause92) ).

cnf(clause91,axiom,
    ( totalorderedP(X1)
    | ~ leq(skaf64(X1),skaf65(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause91) ).

cnf(clause90,axiom,
    ( strictorderedP(X1)
    | ~ lt(skaf69(X1),skaf70(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause90) ).

cnf(clause106,axiom,
    ( gt(X2,X1)
    | ~ lt(X1,X2)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause106) ).

cnf(clause105,axiom,
    ( lt(X2,X1)
    | ~ gt(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause105) ).

cnf(clause103,axiom,
    ( leq(X1,X2)
    | ~ lt(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause103) ).

cnf(clause107,axiom,
    ( leq(X2,X1)
    | ~ geq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause107) ).

cnf(clause108,axiom,
    ( geq(X2,X1)
    | ~ leq(X1,X2)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause108) ).

cnf(clause123,axiom,
    ( nil = X2
    | hd(app(X2,X1)) = hd(X2)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause123) ).

cnf(clause113,axiom,
    ( totalorderedP(cons(X2,X1))
    | nil != X1
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause113) ).

cnf(clause112,axiom,
    ( strictorderedP(cons(X2,X1))
    | nil != X1
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause112) ).

cnf(clause177,axiom,
    ( nil = X2
    | X1 = X2
    | nil = X1
    | tl(X1) != tl(X2)
    | hd(X1) != hd(X2)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause177) ).

cnf(clause97,axiom,
    ( hd(cons(X1,X2)) = X1
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause97) ).

cnf(clause96,axiom,
    ( tl(cons(X1,X2)) = X2
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause96) ).

cnf(clause85,axiom,
    ( ssList(app(X2,X1))
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).

cnf(clause86,axiom,
    ( ssList(cons(X1,X2))
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).

cnf(clause117,axiom,
    ( X1 != X2
    | ~ neq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause117) ).

cnf(clause111,axiom,
    ( X1 != X2
    | ~ lt(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause111) ).

cnf(clause115,axiom,
    ( X1 != X2
    | ~ neq(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause115) ).

cnf(clause116,axiom,
    ( singletonP(X2)
    | cons(X1,nil) != X2
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause116) ).

cnf(clause118,axiom,
    ( nil = X1
    | app(X1,X2) != nil
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause118) ).

cnf(clause119,axiom,
    ( nil = X2
    | app(X1,X2) != nil
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause119) ).

cnf(clause88,axiom,
    ( cyclefreeP(X1)
    | leq(skaf49(X1),skaf50(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause88) ).

cnf(clause87,axiom,
    ( cyclefreeP(X1)
    | leq(skaf50(X1),skaf49(X1))
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause87) ).

cnf(clause99,axiom,
    ( cons(X1,X2) != X2
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause99) ).

cnf(clause98,axiom,
    ( cons(X1,X2) != nil
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause98) ).

cnf(clause104,axiom,
    ( cons(hd(X1),tl(X1)) = X1
    | nil = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause104) ).

cnf(clause109,axiom,
    ( cons(skaf83(X1),skaf82(X1)) = X1
    | nil = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause109) ).

cnf(clause70,axiom,
    ( cyclefreeP(cons(X1,nil))
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause70) ).

cnf(clause69,axiom,
    ( totalorderP(cons(X1,nil))
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause69) ).

cnf(clause68,axiom,
    ( strictorderP(cons(X1,nil))
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause68) ).

cnf(clause67,axiom,
    ( totalorderedP(cons(X1,nil))
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause67) ).

cnf(clause66,axiom,
    ( strictorderedP(cons(X1,nil))
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause66) ).

cnf(clause65,axiom,
    ( duplicatefreeP(cons(X1,nil))
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause65) ).

cnf(clause64,axiom,
    ( equalelemsP(cons(X1,nil))
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause64) ).

cnf(clause101,axiom,
    ( cons(skaf44(X1),nil) = X1
    | ~ singletonP(X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause101) ).

cnf(clause145,axiom,
    ( app(X1,X2) = nil
    | nil != X1
    | nil != X2
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause145) ).

cnf(clause102,axiom,
    ( neq(X2,X1)
    | X2 = X1
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause102) ).

cnf(clause100,axiom,
    ( neq(X2,X1)
    | X2 = X1
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause100) ).

cnf(clause53,axiom,
    ssList(skaf42(X1,X2)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause53) ).

cnf(clause52,axiom,
    ssList(skaf43(X1,X2)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause52) ).

cnf(clause51,axiom,
    ssList(skaf45(X1,X2)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause51) ).

cnf(clause50,axiom,
    ssList(skaf46(X1,X2)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause50) ).

cnf(clause49,axiom,
    ssList(skaf47(X1,X2)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause49) ).

cnf(clause48,axiom,
    ssList(skaf48(X1,X2)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause48) ).

cnf(clause63,axiom,
    ( ~ lt(X1,X1)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause63) ).

cnf(clause84,axiom,
    ( nil = X1
    | ~ frontsegP(nil,X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause84) ).

cnf(clause82,axiom,
    ( nil = X1
    | ~ rearsegP(nil,X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause82) ).

cnf(clause80,axiom,
    ( nil = X1
    | ~ segmentP(nil,X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause80) ).

cnf(clause71,axiom,
    ( ~ memberP(nil,X1)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause71) ).

cnf(clause89,axiom,
    ( equalelemsP(X1)
    | skaf79(X1) != skaf78(X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause89) ).

cnf(clause83,axiom,
    ( frontsegP(nil,X1)
    | nil != X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause83) ).

cnf(clause81,axiom,
    ( rearsegP(nil,X1)
    | nil != X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause81) ).

cnf(clause79,axiom,
    ( segmentP(nil,X1)
    | nil != X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause79) ).

cnf(clause62,axiom,
    ( leq(X1,X1)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause62) ).

cnf(clause61,axiom,
    ( frontsegP(X1,X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause61) ).

cnf(clause59,axiom,
    ( rearsegP(X1,X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause59) ).

cnf(clause57,axiom,
    ( segmentP(X1,X1)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause57) ).

cnf(clause55,axiom,
    ( geq(X1,X1)
    | ~ ssItem(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause55) ).

cnf(clause74,axiom,
    ( app(nil,X1) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).

cnf(clause73,axiom,
    ( app(X1,nil) = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).

cnf(clause60,axiom,
    ( frontsegP(X1,nil)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause60) ).

cnf(clause58,axiom,
    ( rearsegP(X1,nil)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause58) ).

cnf(clause56,axiom,
    ( segmentP(X1,nil)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause56) ).

cnf(clause78,axiom,
    ( ssItem(hd(X1))
    | nil = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause78) ).

cnf(clause76,axiom,
    ( ssItem(hd(X1))
    | nil = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause76) ).

cnf(clause77,axiom,
    ( ssList(tl(X1))
    | nil = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause77) ).

cnf(clause75,axiom,
    ( ssList(tl(X1))
    | nil = X1
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).

cnf(clause72,axiom,
    ( duplicatefreeP(X1)
    | ssItem(X2)
    | ~ ssList(X1) ),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).

cnf(co1_14,negated_conjecture,
    app(sk3,sk6) = sk4,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_14) ).

cnf(clause47,axiom,
    ssItem(skaf44(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause47) ).

cnf(clause46,axiom,
    ssItem(skaf49(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause46) ).

cnf(clause45,axiom,
    ssItem(skaf50(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause45) ).

cnf(clause41,axiom,
    ssItem(skaf54(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause41) ).

cnf(clause40,axiom,
    ssItem(skaf55(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause40) ).

cnf(clause36,axiom,
    ssItem(skaf59(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause36) ).

cnf(clause35,axiom,
    ssItem(skaf60(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause35) ).

cnf(clause31,axiom,
    ssItem(skaf64(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause31) ).

cnf(clause30,axiom,
    ssItem(skaf65(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause30) ).

cnf(clause26,axiom,
    ssItem(skaf69(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause26) ).

cnf(clause25,axiom,
    ssItem(skaf70(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause25) ).

cnf(clause21,axiom,
    ssItem(skaf74(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause21) ).

cnf(clause17,axiom,
    ssItem(skaf78(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause17) ).

cnf(clause16,axiom,
    ssItem(skaf79(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause16) ).

cnf(clause12,axiom,
    ssItem(skaf83(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause12) ).

cnf(clause44,axiom,
    ssList(skaf51(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause44) ).

cnf(clause43,axiom,
    ssList(skaf52(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause43) ).

cnf(clause42,axiom,
    ssList(skaf53(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause42) ).

cnf(clause39,axiom,
    ssList(skaf56(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause39) ).

cnf(clause38,axiom,
    ssList(skaf57(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause38) ).

cnf(clause37,axiom,
    ssList(skaf58(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause37) ).

cnf(clause34,axiom,
    ssList(skaf61(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause34) ).

cnf(clause33,axiom,
    ssList(skaf62(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause33) ).

cnf(clause32,axiom,
    ssList(skaf63(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause32) ).

cnf(clause29,axiom,
    ssList(skaf66(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause29) ).

cnf(clause28,axiom,
    ssList(skaf67(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause28) ).

cnf(clause27,axiom,
    ssList(skaf68(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause27) ).

cnf(clause24,axiom,
    ssList(skaf71(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause24) ).

cnf(clause23,axiom,
    ssList(skaf72(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause23) ).

cnf(clause22,axiom,
    ssList(skaf73(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause22) ).

cnf(clause20,axiom,
    ssList(skaf75(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause20) ).

cnf(clause19,axiom,
    ssList(skaf76(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause19) ).

cnf(clause18,axiom,
    ssList(skaf77(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause18) ).

cnf(clause15,axiom,
    ssList(skaf80(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause15) ).

cnf(clause14,axiom,
    ssList(skaf81(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause14) ).

cnf(clause13,axiom,
    ssList(skaf82(X1)),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).

cnf(clause11,axiom,
    ~ singletonP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause11) ).

cnf(clause10,axiom,
    ssItem(skac2),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause10) ).

cnf(clause9,axiom,
    ssItem(skac3),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause9) ).

cnf(co1_13,negated_conjecture,
    ssList(sk6),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).

cnf(co1_4,negated_conjecture,
    ssList(sk4),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_4) ).

cnf(co1_3,negated_conjecture,
    ssList(sk3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).

cnf(co1_2,negated_conjecture,
    ssList(sk2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_2) ).

cnf(co1_1,negated_conjecture,
    ssList(sk1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_1) ).

cnf(clause8,axiom,
    ssList(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).

cnf(clause7,axiom,
    cyclefreeP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause7) ).

cnf(clause6,axiom,
    totalorderP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause6) ).

cnf(clause5,axiom,
    strictorderP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause5) ).

cnf(clause4,axiom,
    totalorderedP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause4) ).

cnf(clause3,axiom,
    strictorderedP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause3) ).

cnf(clause2,axiom,
    duplicatefreeP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause2) ).

cnf(co1_15,negated_conjecture,
    equalelemsP(sk3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).

cnf(clause1,axiom,
    equalelemsP(nil),
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause1) ).

cnf(co1_17,negated_conjecture,
    ( nil = sk4
    | nil != sk3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_17) ).

cnf(co1_7,negated_conjecture,
    nil != sk1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).

cnf(clause54,axiom,
    skac3 != skac2,
    file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause54) ).

cnf(co1_5,negated_conjecture,
    sk2 = sk4,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_5) ).

cnf(co1_6,negated_conjecture,
    sk1 = sk3,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).

cnf(i_0_202,negated_conjecture,
    ( ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1
    | ~ leq(X1,sk5(X3,X2,X1)) ),
    co1_12,
    [final] ).

cnf(i_0_203,axiom,
    ( ~ leq(X1,X2)
    | ~ leq(X2,X1)
    | app(app(X3,cons(X1,X4)),cons(X2,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X4)
    | ~ ssList(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1)
    | ~ cyclefreeP(X6)
    | ~ ssList(X6) ),
    clause185,
    [final] ).

cnf(i_0_204,negated_conjecture,
    ( memberP(X2,sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    co1_9,
    [final] ).

cnf(i_0_205,negated_conjecture,
    ( memberP(X3,sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    co1_10,
    [final] ).

cnf(i_0_206,negated_conjecture,
    ( lt(X1,sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    co1_11,
    [final] ).

cnf(i_0_207,negated_conjecture,
    ( ssItem(sk5(X3,X2,X1))
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3)
    | app(app(X2,cons(X1,nil)),X3) != sk1 ),
    co1_8,
    [final] ).

cnf(i_0_208,axiom,
    ( lt(X2,X4)
    | lt(X4,X2)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ strictorderP(X6)
    | ~ ssList(X6) ),
    clause183,
    [final] ).

cnf(i_0_209,axiom,
    ( leq(X2,X4)
    | leq(X4,X2)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ totalorderP(X6)
    | ~ ssList(X6) ),
    clause184,
    [final] ).

cnf(i_0_210,axiom,
    ( lt(X2,X4)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ strictorderedP(X6)
    | ~ ssList(X6) ),
    clause181,
    [final] ).

cnf(i_0_211,axiom,
    ( leq(X2,X4)
    | app(app(X1,cons(X2,X3)),cons(X4,X5)) != X6
    | ~ ssList(X5)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X2)
    | ~ totalorderedP(X6)
    | ~ ssList(X6) ),
    clause182,
    [final] ).

cnf(i_0_212,axiom,
    ( app(app(X1,cons(X2,X3)),cons(X2,X4)) != X5
    | ~ ssList(X4)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2)
    | ~ duplicatefreeP(X5)
    | ~ ssList(X5) ),
    clause179,
    [final] ).

cnf(i_0_213,axiom,
    ( cyclefreeP(X1)
    | app(app(skaf51(X1),cons(skaf49(X1),skaf52(X1))),cons(skaf50(X1),skaf53(X1))) = X1
    | ~ ssList(X1) ),
    clause167,
    [final] ).

cnf(i_0_214,axiom,
    ( totalorderP(X1)
    | app(app(skaf56(X1),cons(skaf54(X1),skaf57(X1))),cons(skaf55(X1),skaf58(X1))) = X1
    | ~ ssList(X1) ),
    clause166,
    [final] ).

cnf(i_0_215,axiom,
    ( strictorderP(X1)
    | app(app(skaf61(X1),cons(skaf59(X1),skaf62(X1))),cons(skaf60(X1),skaf63(X1))) = X1
    | ~ ssList(X1) ),
    clause165,
    [final] ).

cnf(i_0_216,axiom,
    ( totalorderedP(X1)
    | app(app(skaf66(X1),cons(skaf64(X1),skaf67(X1))),cons(skaf65(X1),skaf68(X1))) = X1
    | ~ ssList(X1) ),
    clause164,
    [final] ).

cnf(i_0_217,axiom,
    ( strictorderedP(X1)
    | app(app(skaf71(X1),cons(skaf69(X1),skaf72(X1))),cons(skaf70(X1),skaf73(X1))) = X1
    | ~ ssList(X1) ),
    clause163,
    [final] ).

cnf(i_0_218,axiom,
    ( duplicatefreeP(X1)
    | app(app(skaf75(X1),cons(skaf74(X1),skaf76(X1))),cons(skaf74(X1),skaf77(X1))) = X1
    | ~ ssList(X1) ),
    clause162,
    [final] ).

cnf(i_0_219,axiom,
    ( X2 = X3
    | app(X1,cons(X2,cons(X3,X4))) != X5
    | ~ ssList(X4)
    | ~ ssList(X1)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ equalelemsP(X5)
    | ~ ssList(X5) ),
    clause180,
    [final] ).

cnf(i_0_220,axiom,
    ( equalelemsP(X1)
    | app(skaf80(X1),cons(skaf78(X1),cons(skaf79(X1),skaf81(X1)))) = X1
    | ~ ssList(X1) ),
    clause142,
    [final] ).

cnf(i_0_221,axiom,
    ( app(app(skaf47(X1,X2),X2),skaf48(X2,X1)) = X1
    | ~ segmentP(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause168,
    [final] ).

cnf(i_0_222,axiom,
    ( app(skaf42(X1,X2),cons(X2,skaf43(X2,X1))) = X1
    | ~ memberP(X1,X2)
    | ~ ssItem(X2)
    | ~ ssList(X1) ),
    clause169,
    [final] ).

cnf(i_0_223,axiom,
    ( frontsegP(X2,X4)
    | ~ frontsegP(cons(X1,X2),cons(X3,X4))
    | ~ ssList(X4)
    | ~ ssList(X2)
    | ~ ssItem(X3)
    | ~ ssItem(X1) ),
    clause174,
    [final] ).

cnf(i_0_224,axiom,
    ( segmentP(app(app(X4,X1),X3),X2)
    | ~ segmentP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X4)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause172,
    [final] ).

cnf(i_0_225,negated_conjecture,
    ( ~ ssItem(X1)
    | ~ ssList(X2)
    | app(cons(X1,nil),X2) != sk6
    | ~ ssList(X3)
    | app(X3,cons(X1,nil)) != sk3 ),
    co1_16,
    [final] ).

cnf(i_0_226,axiom,
    ( X1 = X3
    | ~ frontsegP(cons(X1,X2),cons(X3,X4))
    | ~ ssList(X4)
    | ~ ssList(X2)
    | ~ ssItem(X3)
    | ~ ssItem(X1) ),
    clause176,
    [final] ).

cnf(i_0_227,axiom,
    ( frontsegP(cons(X3,X1),cons(X4,X2))
    | ~ frontsegP(X1,X2)
    | X3 != X4
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssItem(X4)
    | ~ ssItem(X3) ),
    clause178,
    [final] ).

cnf(i_0_228,axiom,
    ( memberP(X2,X3)
    | memberP(X1,X3)
    | ~ memberP(app(X1,X2),X3)
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssItem(X3) ),
    clause158,
    [final] ).

cnf(i_0_229,axiom,
    ( segmentP(X4,X2)
    | app(app(X1,X2),X3) != X4
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X4) ),
    clause173,
    [final] ).

cnf(i_0_230,axiom,
    ( memberP(X4,X2)
    | app(X1,cons(X2,X3)) != X4
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2)
    | ~ ssList(X4) ),
    clause175,
    [final] ).

cnf(i_0_231,axiom,
    ( memberP(X2,X3)
    | X3 = X1
    | ~ memberP(cons(X1,X2),X3)
    | ~ ssList(X2)
    | ~ ssItem(X1)
    | ~ ssItem(X3) ),
    clause161,
    [final] ).

cnf(i_0_232,axiom,
    ( app(app(X3,X2),X1) = app(X3,app(X2,X1))
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    clause149,
    [final] ).

cnf(i_0_233,axiom,
    ( cons(X1,app(X2,X3)) = app(cons(X1,X2),X3)
    | ~ ssItem(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    clause157,
    [final] ).

cnf(i_0_234,axiom,
    ( totalorderedP(cons(X1,X2))
    | nil = X2
    | ~ leq(X1,hd(X2))
    | ~ totalorderedP(X2)
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    clause159,
    [final] ).

cnf(i_0_235,axiom,
    ( strictorderedP(cons(X1,X2))
    | nil = X2
    | ~ lt(X1,hd(X2))
    | ~ strictorderedP(X2)
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    clause160,
    [final] ).

cnf(i_0_236,axiom,
    ( memberP(app(X1,X3),X2)
    | ~ memberP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    clause140,
    [final] ).

cnf(i_0_237,axiom,
    ( memberP(app(X3,X1),X2)
    | ~ memberP(X1,X2)
    | ~ ssList(X1)
    | ~ ssList(X3)
    | ~ ssItem(X2) ),
    clause141,
    [final] ).

cnf(i_0_238,axiom,
    ( memberP(cons(X3,X1),X2)
    | ~ memberP(X1,X2)
    | ~ ssList(X1)
    | ~ ssItem(X3)
    | ~ ssItem(X2) ),
    clause139,
    [final] ).

cnf(i_0_239,axiom,
    ( frontsegP(app(X1,X3),X2)
    | ~ frontsegP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause137,
    [final] ).

cnf(i_0_240,axiom,
    ( rearsegP(app(X3,X1),X2)
    | ~ rearsegP(X1,X2)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause136,
    [final] ).

cnf(i_0_241,axiom,
    ( lt(X1,hd(X2))
    | nil = X2
    | ~ strictorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    clause134,
    [final] ).

cnf(i_0_242,axiom,
    ( leq(X1,hd(X2))
    | nil = X2
    | ~ totalorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    clause135,
    [final] ).

cnf(i_0_243,axiom,
    ( gt(X1,X3)
    | ~ gt(X1,X2)
    | ~ gt(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause146,
    [final] ).

cnf(i_0_244,axiom,
    ( lt(X1,X3)
    | ~ lt(X1,X2)
    | ~ lt(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause155,
    [final] ).

cnf(i_0_245,axiom,
    ( lt(X1,X3)
    | ~ leq(X1,X2)
    | ~ lt(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause147,
    [final] ).

cnf(i_0_246,axiom,
    ( leq(X1,X3)
    | ~ leq(X1,X2)
    | ~ leq(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause156,
    [final] ).

cnf(i_0_247,axiom,
    ( frontsegP(X1,X3)
    | ~ frontsegP(X1,X2)
    | ~ frontsegP(X2,X3)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause154,
    [final] ).

cnf(i_0_248,axiom,
    ( rearsegP(X1,X3)
    | ~ rearsegP(X1,X2)
    | ~ rearsegP(X2,X3)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause153,
    [final] ).

cnf(i_0_249,axiom,
    ( segmentP(X1,X3)
    | ~ segmentP(X1,X2)
    | ~ segmentP(X2,X3)
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause152,
    [final] ).

cnf(i_0_250,axiom,
    ( geq(X1,X3)
    | ~ geq(X1,X2)
    | ~ geq(X2,X3)
    | ~ ssItem(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause148,
    [final] ).

cnf(i_0_251,axiom,
    ( app(skaf46(X1,X2),X2) = X1
    | ~ rearsegP(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause131,
    [final] ).

cnf(i_0_252,axiom,
    ( app(X2,skaf45(X1,X2)) = X1
    | ~ frontsegP(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause132,
    [final] ).

cnf(i_0_253,axiom,
    ( X1 = X3
    | cons(X1,X2) != cons(X3,X4)
    | ~ ssItem(X3)
    | ~ ssItem(X1)
    | ~ ssList(X4)
    | ~ ssList(X2) ),
    clause170,
    [final] ).

cnf(i_0_254,axiom,
    ( X4 = X2
    | cons(X1,X2) != cons(X3,X4)
    | ~ ssItem(X3)
    | ~ ssItem(X1)
    | ~ ssList(X4)
    | ~ ssList(X2) ),
    clause171,
    [final] ).

cnf(i_0_255,axiom,
    ( totalorderedP(X2)
    | nil = X2
    | ~ totalorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    clause125,
    [final] ).

cnf(i_0_256,axiom,
    ( strictorderedP(X2)
    | nil = X2
    | ~ strictorderedP(cons(X1,X2))
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    clause124,
    [final] ).

cnf(i_0_257,axiom,
    ( X1 = X3
    | app(X1,X2) != app(X3,X2)
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    clause151,
    [final] ).

cnf(i_0_258,axiom,
    ( X2 = X3
    | app(X1,X2) != app(X1,X3)
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssList(X3) ),
    clause150,
    [final] ).

cnf(i_0_259,axiom,
    ( nil = X2
    | tl(app(X2,X1)) = app(tl(X2),X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause133,
    [final] ).

cnf(i_0_260,axiom,
    ( memberP(cons(X2,X3),X1)
    | X1 != X2
    | ~ ssList(X3)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause138,
    [final] ).

cnf(i_0_261,axiom,
    ( app(cons(X1,nil),X2) = cons(X1,X2)
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    clause120,
    [final] ).

cnf(i_0_262,axiom,
    ( X2 = X1
    | ~ leq(X1,X2)
    | ~ leq(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    clause130,
    [final] ).

cnf(i_0_263,axiom,
    ( X2 = X1
    | ~ geq(X1,X2)
    | ~ geq(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    clause126,
    [final] ).

cnf(i_0_264,axiom,
    ( X2 = X1
    | ~ frontsegP(X1,X2)
    | ~ frontsegP(X2,X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause129,
    [final] ).

cnf(i_0_265,axiom,
    ( X2 = X1
    | ~ rearsegP(X1,X2)
    | ~ rearsegP(X2,X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause128,
    [final] ).

cnf(i_0_266,axiom,
    ( X2 = X1
    | ~ segmentP(X1,X2)
    | ~ segmentP(X2,X1)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause127,
    [final] ).

cnf(i_0_267,axiom,
    ( frontsegP(X3,X1)
    | app(X1,X2) != X3
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssList(X3) ),
    clause144,
    [final] ).

cnf(i_0_268,axiom,
    ( rearsegP(X3,X2)
    | app(X1,X2) != X3
    | ~ ssList(X1)
    | ~ ssList(X2)
    | ~ ssList(X3) ),
    clause143,
    [final] ).

cnf(i_0_269,axiom,
    ( ~ gt(X1,X2)
    | ~ gt(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    clause110,
    [final] ).

cnf(i_0_270,axiom,
    ( ~ lt(X1,X2)
    | ~ lt(X2,X1)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    clause114,
    [final] ).

cnf(i_0_271,axiom,
    ( lt(X1,X2)
    | X1 = X2
    | ~ leq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause122,
    [final] ).

cnf(i_0_272,axiom,
    ( lt(X1,X2)
    | X1 = X2
    | ~ leq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause121,
    [final] ).

cnf(i_0_273,axiom,
    ( totalorderP(X1)
    | ~ leq(skaf54(X1),skaf55(X1))
    | ~ ssList(X1) ),
    clause95,
    [final] ).

cnf(i_0_274,axiom,
    ( totalorderP(X1)
    | ~ leq(skaf55(X1),skaf54(X1))
    | ~ ssList(X1) ),
    clause94,
    [final] ).

cnf(i_0_275,axiom,
    ( strictorderP(X1)
    | ~ lt(skaf59(X1),skaf60(X1))
    | ~ ssList(X1) ),
    clause93,
    [final] ).

cnf(i_0_276,axiom,
    ( strictorderP(X1)
    | ~ lt(skaf60(X1),skaf59(X1))
    | ~ ssList(X1) ),
    clause92,
    [final] ).

cnf(i_0_277,axiom,
    ( totalorderedP(X1)
    | ~ leq(skaf64(X1),skaf65(X1))
    | ~ ssList(X1) ),
    clause91,
    [final] ).

cnf(i_0_278,axiom,
    ( strictorderedP(X1)
    | ~ lt(skaf69(X1),skaf70(X1))
    | ~ ssList(X1) ),
    clause90,
    [final] ).

cnf(i_0_279,axiom,
    ( gt(X2,X1)
    | ~ lt(X1,X2)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    clause106,
    [final] ).

cnf(i_0_280,axiom,
    ( lt(X2,X1)
    | ~ gt(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause105,
    [final] ).

cnf(i_0_281,axiom,
    ( leq(X1,X2)
    | ~ lt(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause103,
    [final] ).

cnf(i_0_282,axiom,
    ( leq(X2,X1)
    | ~ geq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause107,
    [final] ).

cnf(i_0_283,axiom,
    ( geq(X2,X1)
    | ~ leq(X1,X2)
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    clause108,
    [final] ).

cnf(i_0_284,axiom,
    ( nil = X2
    | hd(app(X2,X1)) = hd(X2)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause123,
    [final] ).

cnf(i_0_285,axiom,
    ( totalorderedP(cons(X2,X1))
    | nil != X1
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    clause113,
    [final] ).

cnf(i_0_286,axiom,
    ( strictorderedP(cons(X2,X1))
    | nil != X1
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    clause112,
    [final] ).

cnf(i_0_287,axiom,
    ( nil = X2
    | X1 = X2
    | nil = X1
    | tl(X1) != tl(X2)
    | hd(X1) != hd(X2)
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause177,
    [final] ).

cnf(i_0_288,axiom,
    ( hd(cons(X1,X2)) = X1
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    clause97,
    [final] ).

cnf(i_0_289,axiom,
    ( tl(cons(X1,X2)) = X2
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    clause96,
    [final] ).

cnf(i_0_290,axiom,
    ( ssList(app(X2,X1))
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause85,
    [final] ).

cnf(i_0_291,axiom,
    ( ssList(cons(X1,X2))
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    clause86,
    [final] ).

cnf(i_0_292,axiom,
    ( X1 != X2
    | ~ neq(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause117,
    [final] ).

cnf(i_0_293,axiom,
    ( X1 != X2
    | ~ lt(X1,X2)
    | ~ ssItem(X2)
    | ~ ssItem(X1) ),
    clause111,
    [final] ).

cnf(i_0_294,axiom,
    ( X1 != X2
    | ~ neq(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause115,
    [final] ).

cnf(i_0_295,axiom,
    ( singletonP(X2)
    | cons(X1,nil) != X2
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    clause116,
    [final] ).

cnf(i_0_296,axiom,
    ( nil = X1
    | app(X1,X2) != nil
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause118,
    [final] ).

cnf(i_0_297,axiom,
    ( nil = X2
    | app(X1,X2) != nil
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause119,
    [final] ).

cnf(i_0_298,axiom,
    ( cyclefreeP(X1)
    | leq(skaf49(X1),skaf50(X1))
    | ~ ssList(X1) ),
    clause88,
    [final] ).

cnf(i_0_299,axiom,
    ( cyclefreeP(X1)
    | leq(skaf50(X1),skaf49(X1))
    | ~ ssList(X1) ),
    clause87,
    [final] ).

cnf(i_0_300,axiom,
    ( cons(X1,X2) != X2
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    clause99,
    [final] ).

cnf(i_0_301,axiom,
    ( cons(X1,X2) != nil
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    clause98,
    [final] ).

cnf(i_0_302,axiom,
    ( cons(hd(X1),tl(X1)) = X1
    | nil = X1
    | ~ ssList(X1) ),
    clause104,
    [final] ).

cnf(i_0_303,axiom,
    ( cons(skaf83(X1),skaf82(X1)) = X1
    | nil = X1
    | ~ ssList(X1) ),
    clause109,
    [final] ).

cnf(i_0_304,axiom,
    ( cyclefreeP(cons(X1,nil))
    | ~ ssItem(X1) ),
    clause70,
    [final] ).

cnf(i_0_305,axiom,
    ( totalorderP(cons(X1,nil))
    | ~ ssItem(X1) ),
    clause69,
    [final] ).

cnf(i_0_306,axiom,
    ( strictorderP(cons(X1,nil))
    | ~ ssItem(X1) ),
    clause68,
    [final] ).

cnf(i_0_307,axiom,
    ( totalorderedP(cons(X1,nil))
    | ~ ssItem(X1) ),
    clause67,
    [final] ).

cnf(i_0_308,axiom,
    ( strictorderedP(cons(X1,nil))
    | ~ ssItem(X1) ),
    clause66,
    [final] ).

cnf(i_0_309,axiom,
    ( duplicatefreeP(cons(X1,nil))
    | ~ ssItem(X1) ),
    clause65,
    [final] ).

cnf(i_0_310,axiom,
    ( equalelemsP(cons(X1,nil))
    | ~ ssItem(X1) ),
    clause64,
    [final] ).

cnf(i_0_311,axiom,
    ( cons(skaf44(X1),nil) = X1
    | ~ singletonP(X1)
    | ~ ssList(X1) ),
    clause101,
    [final] ).

cnf(i_0_312,axiom,
    ( app(X1,X2) = nil
    | nil != X1
    | nil != X2
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    clause145,
    [final] ).

cnf(i_0_313,axiom,
    ( neq(X2,X1)
    | X2 = X1
    | ~ ssItem(X1)
    | ~ ssItem(X2) ),
    clause102,
    [final] ).

cnf(i_0_314,axiom,
    ( neq(X2,X1)
    | X2 = X1
    | ~ ssList(X1)
    | ~ ssList(X2) ),
    clause100,
    [final] ).

cnf(i_0_315,axiom,
    ssList(skaf42(X1,X2)),
    clause53,
    [final] ).

cnf(i_0_316,axiom,
    ssList(skaf43(X1,X2)),
    clause52,
    [final] ).

cnf(i_0_317,axiom,
    ssList(skaf45(X1,X2)),
    clause51,
    [final] ).

cnf(i_0_318,axiom,
    ssList(skaf46(X1,X2)),
    clause50,
    [final] ).

cnf(i_0_319,axiom,
    ssList(skaf47(X1,X2)),
    clause49,
    [final] ).

cnf(i_0_320,axiom,
    ssList(skaf48(X1,X2)),
    clause48,
    [final] ).

cnf(i_0_321,axiom,
    ( ~ lt(X1,X1)
    | ~ ssItem(X1) ),
    clause63,
    [final] ).

cnf(i_0_322,axiom,
    ( nil = X1
    | ~ frontsegP(nil,X1)
    | ~ ssList(X1) ),
    clause84,
    [final] ).

cnf(i_0_323,axiom,
    ( nil = X1
    | ~ rearsegP(nil,X1)
    | ~ ssList(X1) ),
    clause82,
    [final] ).

cnf(i_0_324,axiom,
    ( nil = X1
    | ~ segmentP(nil,X1)
    | ~ ssList(X1) ),
    clause80,
    [final] ).

cnf(i_0_325,axiom,
    ( ~ memberP(nil,X1)
    | ~ ssItem(X1) ),
    clause71,
    [final] ).

cnf(i_0_326,axiom,
    ( equalelemsP(X1)
    | skaf79(X1) != skaf78(X1)
    | ~ ssList(X1) ),
    clause89,
    [final] ).

cnf(i_0_327,axiom,
    ( frontsegP(nil,X1)
    | nil != X1
    | ~ ssList(X1) ),
    clause83,
    [final] ).

cnf(i_0_328,axiom,
    ( rearsegP(nil,X1)
    | nil != X1
    | ~ ssList(X1) ),
    clause81,
    [final] ).

cnf(i_0_329,axiom,
    ( segmentP(nil,X1)
    | nil != X1
    | ~ ssList(X1) ),
    clause79,
    [final] ).

cnf(i_0_330,axiom,
    ( leq(X1,X1)
    | ~ ssItem(X1) ),
    clause62,
    [final] ).

cnf(i_0_331,axiom,
    ( frontsegP(X1,X1)
    | ~ ssList(X1) ),
    clause61,
    [final] ).

cnf(i_0_332,axiom,
    ( rearsegP(X1,X1)
    | ~ ssList(X1) ),
    clause59,
    [final] ).

cnf(i_0_333,axiom,
    ( segmentP(X1,X1)
    | ~ ssList(X1) ),
    clause57,
    [final] ).

cnf(i_0_334,axiom,
    ( geq(X1,X1)
    | ~ ssItem(X1) ),
    clause55,
    [final] ).

cnf(i_0_335,axiom,
    ( app(nil,X1) = X1
    | ~ ssList(X1) ),
    clause74,
    [final] ).

cnf(i_0_336,axiom,
    ( app(X1,nil) = X1
    | ~ ssList(X1) ),
    clause73,
    [final] ).

cnf(i_0_337,axiom,
    ( frontsegP(X1,nil)
    | ~ ssList(X1) ),
    clause60,
    [final] ).

cnf(i_0_338,axiom,
    ( rearsegP(X1,nil)
    | ~ ssList(X1) ),
    clause58,
    [final] ).

cnf(i_0_339,axiom,
    ( segmentP(X1,nil)
    | ~ ssList(X1) ),
    clause56,
    [final] ).

cnf(i_0_340,axiom,
    ( ssItem(hd(X1))
    | nil = X1
    | ~ ssList(X1) ),
    clause78,
    [final] ).

cnf(i_0_341,axiom,
    ( ssItem(hd(X1))
    | nil = X1
    | ~ ssList(X1) ),
    clause76,
    [final] ).

cnf(i_0_342,axiom,
    ( ssList(tl(X1))
    | nil = X1
    | ~ ssList(X1) ),
    clause77,
    [final] ).

cnf(i_0_343,axiom,
    ( ssList(tl(X1))
    | nil = X1
    | ~ ssList(X1) ),
    clause75,
    [final] ).

cnf(i_0_344,axiom,
    ( duplicatefreeP(X1)
    | ssItem(X2)
    | ~ ssList(X1) ),
    clause72,
    [final] ).

cnf(i_0_345,negated_conjecture,
    app(sk3,sk6) = sk4,
    co1_14,
    [final] ).

cnf(i_0_346,axiom,
    ssItem(skaf44(X1)),
    clause47,
    [final] ).

cnf(i_0_347,axiom,
    ssItem(skaf49(X1)),
    clause46,
    [final] ).

cnf(i_0_348,axiom,
    ssItem(skaf50(X1)),
    clause45,
    [final] ).

cnf(i_0_349,axiom,
    ssItem(skaf54(X1)),
    clause41,
    [final] ).

cnf(i_0_350,axiom,
    ssItem(skaf55(X1)),
    clause40,
    [final] ).

cnf(i_0_351,axiom,
    ssItem(skaf59(X1)),
    clause36,
    [final] ).

cnf(i_0_352,axiom,
    ssItem(skaf60(X1)),
    clause35,
    [final] ).

cnf(i_0_353,axiom,
    ssItem(skaf64(X1)),
    clause31,
    [final] ).

cnf(i_0_354,axiom,
    ssItem(skaf65(X1)),
    clause30,
    [final] ).

cnf(i_0_355,axiom,
    ssItem(skaf69(X1)),
    clause26,
    [final] ).

cnf(i_0_356,axiom,
    ssItem(skaf70(X1)),
    clause25,
    [final] ).

cnf(i_0_357,axiom,
    ssItem(skaf74(X1)),
    clause21,
    [final] ).

cnf(i_0_358,axiom,
    ssItem(skaf78(X1)),
    clause17,
    [final] ).

cnf(i_0_359,axiom,
    ssItem(skaf79(X1)),
    clause16,
    [final] ).

cnf(i_0_360,axiom,
    ssItem(skaf83(X1)),
    clause12,
    [final] ).

cnf(i_0_361,axiom,
    ssList(skaf51(X1)),
    clause44,
    [final] ).

cnf(i_0_362,axiom,
    ssList(skaf52(X1)),
    clause43,
    [final] ).

cnf(i_0_363,axiom,
    ssList(skaf53(X1)),
    clause42,
    [final] ).

cnf(i_0_364,axiom,
    ssList(skaf56(X1)),
    clause39,
    [final] ).

cnf(i_0_365,axiom,
    ssList(skaf57(X1)),
    clause38,
    [final] ).

cnf(i_0_366,axiom,
    ssList(skaf58(X1)),
    clause37,
    [final] ).

cnf(i_0_367,axiom,
    ssList(skaf61(X1)),
    clause34,
    [final] ).

cnf(i_0_368,axiom,
    ssList(skaf62(X1)),
    clause33,
    [final] ).

cnf(i_0_369,axiom,
    ssList(skaf63(X1)),
    clause32,
    [final] ).

cnf(i_0_370,axiom,
    ssList(skaf66(X1)),
    clause29,
    [final] ).

cnf(i_0_371,axiom,
    ssList(skaf67(X1)),
    clause28,
    [final] ).

cnf(i_0_372,axiom,
    ssList(skaf68(X1)),
    clause27,
    [final] ).

cnf(i_0_373,axiom,
    ssList(skaf71(X1)),
    clause24,
    [final] ).

cnf(i_0_374,axiom,
    ssList(skaf72(X1)),
    clause23,
    [final] ).

cnf(i_0_375,axiom,
    ssList(skaf73(X1)),
    clause22,
    [final] ).

cnf(i_0_376,axiom,
    ssList(skaf75(X1)),
    clause20,
    [final] ).

cnf(i_0_377,axiom,
    ssList(skaf76(X1)),
    clause19,
    [final] ).

cnf(i_0_378,axiom,
    ssList(skaf77(X1)),
    clause18,
    [final] ).

cnf(i_0_379,axiom,
    ssList(skaf80(X1)),
    clause15,
    [final] ).

cnf(i_0_380,axiom,
    ssList(skaf81(X1)),
    clause14,
    [final] ).

cnf(i_0_381,axiom,
    ssList(skaf82(X1)),
    clause13,
    [final] ).

cnf(i_0_382,axiom,
    ~ singletonP(nil),
    clause11,
    [final] ).

cnf(i_0_383,axiom,
    ssItem(skac2),
    clause10,
    [final] ).

cnf(i_0_384,axiom,
    ssItem(skac3),
    clause9,
    [final] ).

cnf(i_0_385,negated_conjecture,
    ssList(sk6),
    co1_13,
    [final] ).

cnf(i_0_386,negated_conjecture,
    ssList(sk4),
    co1_4,
    [final] ).

cnf(i_0_387,negated_conjecture,
    ssList(sk3),
    co1_3,
    [final] ).

cnf(i_0_388,negated_conjecture,
    ssList(sk2),
    co1_2,
    [final] ).

cnf(i_0_389,negated_conjecture,
    ssList(sk1),
    co1_1,
    [final] ).

cnf(i_0_390,axiom,
    ssList(nil),
    clause8,
    [final] ).

cnf(i_0_391,axiom,
    cyclefreeP(nil),
    clause7,
    [final] ).

cnf(i_0_392,axiom,
    totalorderP(nil),
    clause6,
    [final] ).

cnf(i_0_393,axiom,
    strictorderP(nil),
    clause5,
    [final] ).

cnf(i_0_394,axiom,
    totalorderedP(nil),
    clause4,
    [final] ).

cnf(i_0_395,axiom,
    strictorderedP(nil),
    clause3,
    [final] ).

cnf(i_0_396,axiom,
    duplicatefreeP(nil),
    clause2,
    [final] ).

cnf(i_0_397,negated_conjecture,
    equalelemsP(sk3),
    co1_15,
    [final] ).

cnf(i_0_398,axiom,
    equalelemsP(nil),
    clause1,
    [final] ).

cnf(i_0_399,negated_conjecture,
    ( nil = sk4
    | nil != sk3 ),
    co1_17,
    [final] ).

cnf(i_0_400,negated_conjecture,
    nil != sk1,
    co1_7,
    [final] ).

cnf(i_0_401,axiom,
    skac3 != skac2,
    clause54,
    [final] ).

cnf(i_0_402,negated_conjecture,
    sk2 = sk4,
    co1_5,
    [final] ).

cnf(i_0_403,negated_conjecture,
    sk1 = sk3,
    co1_6,
    [final] ).

cnf(i_0_404,axiom,
    X1 = X1 ).

cnf(i_0_405,axiom,
    ( X1 = X2
    | X2 != X1 ) ).

cnf(i_0_406,axiom,
    ( X1 = X2
    | X1 != X3
    | X3 != X2 ) ).

cnf(i_0_407,axiom,
    ( X1 != X2
    | app(X1,X3) = app(X2,X3) ) ).

cnf(i_0_408,axiom,
    ( X1 != X2
    | app(X3,X1) = app(X3,X2) ) ).

cnf(i_0_409,axiom,
    ( X1 != X2
    | cons(X1,X3) = cons(X2,X3) ) ).

cnf(i_0_410,axiom,
    ( X1 != X2
    | cons(X3,X1) = cons(X3,X2) ) ).

cnf(i_0_411,axiom,
    ( X1 != X2
    | skaf78(X1) = skaf78(X2) ) ).

cnf(i_0_412,axiom,
    ( X1 != X2
    | skaf79(X1) = skaf79(X2) ) ).

cnf(i_0_413,axiom,
    ( X1 != X2
    | hd(X1) = hd(X2) ) ).

cnf(i_0_414,axiom,
    ( X1 != X2
    | tl(X1) = tl(X2) ) ).

cnf(i_0_415,axiom,
    ( X1 != X2
    | ~ ssItem(X1)
    | ssItem(X2) ) ).

cnf(i_0_416,axiom,
    ( X1 != X2
    | ~ totalorderedP(X1)
    | totalorderedP(X2) ) ).

cnf(i_0_417,axiom,
    ( X1 != X2
    | ~ duplicatefreeP(X1)
    | duplicatefreeP(X2) ) ).

cnf(i_0_418,axiom,
    ( X1 != X2
    | ~ equalelemsP(X1)
    | equalelemsP(X2) ) ).

cnf(i_0_419,axiom,
    ( X1 != X2
    | ~ segmentP(X1,X3)
    | segmentP(X2,X3) ) ).

cnf(i_0_420,axiom,
    ( X1 != X2
    | ~ segmentP(X3,X1)
    | segmentP(X3,X2) ) ).

cnf(i_0_421,axiom,
    ( X1 != X2
    | ~ frontsegP(X1,X3)
    | frontsegP(X2,X3) ) ).

cnf(i_0_422,axiom,
    ( X1 != X2
    | ~ frontsegP(X3,X1)
    | frontsegP(X3,X2) ) ).

cnf(i_0_423,axiom,
    ( X1 != X2
    | ~ rearsegP(X1,X3)
    | rearsegP(X2,X3) ) ).

cnf(i_0_424,axiom,
    ( X1 != X2
    | ~ rearsegP(X3,X1)
    | rearsegP(X3,X2) ) ).

cnf(i_0_425,axiom,
    ( X1 != X2
    | ~ gt(X1,X3)
    | gt(X2,X3) ) ).

cnf(i_0_426,axiom,
    ( X1 != X2
    | ~ gt(X3,X1)
    | gt(X3,X2) ) ).

cnf(i_0_427,axiom,
    ( X1 != X2
    | ~ geq(X1,X3)
    | geq(X2,X3) ) ).

cnf(i_0_428,axiom,
    ( X1 != X2
    | ~ geq(X3,X1)
    | geq(X3,X2) ) ).

cnf(i_0_429,axiom,
    ( X1 != X2
    | ~ neq(X1,X3)
    | neq(X2,X3) ) ).

cnf(i_0_430,axiom,
    ( X1 != X2
    | ~ neq(X3,X1)
    | neq(X3,X2) ) ).

cnf(i_0_431,axiom,
    ( X1 != X2
    | ~ singletonP(X1)
    | singletonP(X2) ) ).

cnf(i_0_432,axiom,
    ( X1 != X2
    | ~ ssList(X1)
    | ssList(X2) ) ).

cnf(i_0_433,axiom,
    ( X1 != X2
    | ~ leq(X1,X3)
    | leq(X2,X3) ) ).

cnf(i_0_434,axiom,
    ( X1 != X2
    | ~ leq(X3,X1)
    | leq(X3,X2) ) ).

cnf(i_0_435,axiom,
    ( X1 != X2
    | ~ cyclefreeP(X1)
    | cyclefreeP(X2) ) ).

cnf(i_0_436,axiom,
    ( X1 != X2
    | ~ memberP(X1,X3)
    | memberP(X2,X3) ) ).

cnf(i_0_437,axiom,
    ( X1 != X2
    | ~ memberP(X3,X1)
    | memberP(X3,X2) ) ).

cnf(i_0_438,axiom,
    ( X1 != X2
    | ~ lt(X1,X3)
    | lt(X2,X3) ) ).

cnf(i_0_439,axiom,
    ( X1 != X2
    | ~ lt(X3,X1)
    | lt(X3,X2) ) ).

cnf(i_0_440,axiom,
    ( X1 != X2
    | ~ strictorderP(X1)
    | strictorderP(X2) ) ).

cnf(i_0_441,axiom,
    ( X1 != X2
    | ~ totalorderP(X1)
    | totalorderP(X2) ) ).

cnf(i_0_442,axiom,
    ( X1 != X2
    | ~ strictorderedP(X1)
    | strictorderedP(X2) ) ).

cnf(i_0_2282,plain,
    app(cons(skaf55(X1),nil),skaf80(X2)) = cons(skaf55(X1),skaf80(X2)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261]) ).

cnf(i_0_2284,plain,
    frontsegP(sk4,app(sk3,sk6)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421]) ).

cnf(i_0_2285,plain,
    frontsegP(app(sk3,sk6),sk4),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422]) ).

cnf(i_0_2286,plain,
    rearsegP(app(sk3,sk6),sk4),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424]) ).

cnf(i_0_2287,plain,
    cons(skaf55(X1),skaf80(X2)) != app(nil,skaf80(X2)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406]) ).

cnf(i_0_2288,plain,
    ~ neq(hd(sk3),hd(sk3)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462]) ).

cnf(i_0_2290,plain,
    ~ neq(app(skaf80(X1),skaf80(X1)),app(skaf80(X1),skaf80(X1))),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464]) ).

cnf(i_0_2292,plain,
    ~ lt(skaf78(app(sk3,sk6)),skaf78(sk4)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_915,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438]) ).

cnf(i_0_2294,plain,
    ~ lt(skaf78(sk4),skaf78(app(sk3,sk6))),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_915,i_0_2293,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439]) ).

cnf(i_0_2296,plain,
    ~ neq(skaf78(sk4),skaf78(app(sk3,sk6))),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_915,i_0_2293,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430]) ).

cnf(i_0_2298,plain,
    neq(sk3,nil),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429]) ).

cnf(i_0_2299,plain,
    ~ gt(skaf55(X1),skaf55(X1)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269]) ).

cnf(i_0_2301,plain,
    ~ lt(hd(sk3),hd(sk3)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270]) ).

cnf(i_0_2303,plain,
    ~ gt(skaf60(X1),skaf60(X1)),
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280]) ).

cnf(i_0_2306,plain,
    app(sk3,skaf80(X1)) != nil,
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296]) ).

cnf(i_0_2308,plain,
    app(skaf80(X1),sk3) != nil,
    inference(scs_inference,[],[i_0_345,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297]) ).

cnf(i_0_2310,plain,
    app(skaf46(sk3,sk3),sk3) = sk3,
    inference(scs_inference,[],[i_0_345,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251]) ).

cnf(i_0_2312,plain,
    app(sk6,skaf45(sk6,sk6)) = sk6,
    inference(scs_inference,[],[i_0_345,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252]) ).

cnf(i_0_2314,plain,
    hd(app(sk3,skaf80(X1))) = hd(sk3),
    inference(scs_inference,[],[i_0_345,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284]) ).

cnf(i_0_2316,plain,
    app(app(skaf80(X1),skaf80(X1)),skaf80(X1)) = app(skaf80(X1),app(skaf80(X1),skaf80(X1))),
    inference(scs_inference,[],[i_0_345,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232]) ).

cnf(i_0_2318,plain,
    cons(skaf55(X1),app(skaf80(X2),skaf80(X2))) = app(cons(skaf55(X1),skaf80(X2)),skaf80(X2)),
    inference(scs_inference,[],[i_0_345,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233]) ).

cnf(i_0_2320,plain,
    tl(app(sk3,skaf80(X1))) = app(tl(sk3),skaf80(X1)),
    inference(scs_inference,[],[i_0_345,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259]) ).

cnf(i_0_2322,plain,
    app(app(skaf47(sk6,sk6),sk6),skaf48(sk6,sk6)) = sk6,
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221]) ).

cnf(i_0_2324,plain,
    memberP(cons(skaf55(X1),skaf80(X2)),skaf55(X1)),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457]) ).

cnf(i_0_2326,plain,
    memberP(app(cons(skaf55(X1),skaf80(X2)),skaf80(X2)),skaf55(X1)),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236]) ).

cnf(i_0_2328,plain,
    memberP(app(skaf80(X1),cons(skaf55(X2),skaf80(X1))),skaf55(X2)),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237]) ).

cnf(i_0_2330,plain,
    memberP(cons(skaf55(X1),cons(skaf55(X1),skaf80(X2))),skaf55(X1)),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238]) ).

cnf(i_0_2332,plain,
    frontsegP(app(sk6,skaf80(X1)),sk6),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239]) ).

cnf(i_0_2334,plain,
    rearsegP(app(skaf80(X1),sk3),sk3),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240]) ).

cnf(i_0_2336,plain,
    ~ strictorderedP(cons(hd(sk3),sk3)),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241]) ).

cnf(i_0_2338,plain,
    ~ memberP(app(nil,nil),skaf55(X1)),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_390,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228]) ).

cnf(i_0_2340,plain,
    segmentP(app(app(skaf80(X1),sk6),skaf80(X1)),sk6),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_390,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224]) ).

cnf(i_0_2342,plain,
    app(nil,cons(skaf55(X1),nil)) != nil,
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_390,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230]) ).

cnf(i_0_2344,plain,
    frontsegP(cons(skaf55(X1),skaf80(X2)),cons(skaf55(X1),skaf80(X2))),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_350,i_0_352,i_0_390,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450]) ).

cnf(i_0_2347,plain,
    app(app(skaf80(X1),cons(skaf55(X2),skaf80(X1))),cons(skaf55(X2),skaf80(X1))) != nil,
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_350,i_0_352,i_0_390,i_0_396,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212]) ).

cnf(i_0_2349,plain,
    app(app(skaf66(X1),cons(skaf55(X2),skaf66(X1))),cons(skaf55(X2),skaf66(X1))) != nil,
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_656,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_370,i_0_350,i_0_352,i_0_390,i_0_395,i_0_396,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212,i_0_210]) ).

cnf(i_0_2353,plain,
    app(app(skaf80(X1),cons(skac3,skaf80(X1))),cons(skac3,skaf80(X1))) != nil,
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_1015,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_656,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_370,i_0_350,i_0_352,i_0_384,i_0_390,i_0_395,i_0_396,i_0_391,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212,i_0_210,i_0_203]) ).

cnf(i_0_2355,plain,
    app(app(skaf80(X1),cons(skaf44(X2),skaf80(X1))),cons(skaf44(X2),skaf80(X1))) != nil,
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_1015,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_515,i_0_656,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_370,i_0_350,i_0_352,i_0_346,i_0_384,i_0_390,i_0_395,i_0_396,i_0_391,i_0_393,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212,i_0_210,i_0_203,i_0_208]) ).

cnf(i_0_2358,plain,
    nil != cons(hd(sk3),sk3),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_1015,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_515,i_0_656,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_370,i_0_350,i_0_352,i_0_346,i_0_384,i_0_390,i_0_395,i_0_396,i_0_391,i_0_393,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212,i_0_210,i_0_203,i_0_208,i_0_576]) ).

cnf(i_0_2359,plain,
    ~ neq(sk6,app(sk6,skaf45(sk6,sk6))),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_1015,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_515,i_0_656,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_370,i_0_350,i_0_352,i_0_346,i_0_384,i_0_390,i_0_395,i_0_396,i_0_391,i_0_393,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212,i_0_210,i_0_203,i_0_208,i_0_576,i_0_1999]) ).

cnf(i_0_2360,plain,
    ~ neq(app(sk6,skaf45(sk6,sk6)),sk6),
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_931,i_0_1370,i_0_533,i_0_1015,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_515,i_0_656,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_370,i_0_350,i_0_352,i_0_346,i_0_384,i_0_390,i_0_395,i_0_396,i_0_391,i_0_393,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212,i_0_210,i_0_203,i_0_208,i_0_576,i_0_1999,i_0_2086]) ).

cnf(i_0_617,plain,
    duplicatefreeP(nil),
    inference(equality_inference,[],[612]) ).

cnf(i_0_618,plain,
    cyclefreeP(nil),
    inference(equality_inference,[],[613]) ).

cnf(i_0_619,plain,
    strictorderP(nil),
    inference(equality_inference,[],[614]) ).

cnf(i_0_620,plain,
    equalelemsP(nil),
    inference(equality_inference,[],[615]) ).

cnf(i_0_621,plain,
    ssList(sk6),
    inference(equality_inference,[],[616]) ).

cnf(i_0_638,plain,
    ~ neq(app(sk3,sk6),app(sk3,sk6)),
    inference(scs_inference,[],[i_0_345,i_0_387,i_0_349,i_0_605,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_464,i_0_462,i_0_430]) ).

cnf(i_0_639,plain,
    ~ neq(app(sk3,sk6),sk2),
    inference(scs_inference,[],[i_0_345,i_0_387,i_0_349,i_0_605,i_0_565,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_464,i_0_462,i_0_430,i_0_429]) ).

cnf(i_0_640,plain,
    memberP(cons(skaf54(X1),sk3),skaf54(X1)),
    inference(scs_inference,[],[i_0_345,i_0_387,i_0_349,i_0_605,i_0_565,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_464,i_0_462,i_0_430,i_0_429,i_0_457]) ).

cnf(i_0_642,plain,
    frontsegP(cons(skaf54(X1),sk3),cons(skaf54(X1),sk3)),
    inference(scs_inference,[],[i_0_345,i_0_387,i_0_349,i_0_605,i_0_565,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_464,i_0_462,i_0_430,i_0_429,i_0_457,i_0_450]) ).

cnf(i_0_673,plain,
    ~ neq(sk3,sk1),
    inference(scs_inference,[],[i_0_345,i_0_486,i_0_527,i_0_316,i_0_350,i_0_564,i_0_600,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_464,i_0_462,i_0_430,i_0_429]) ).

cnf(i_0_674,plain,
    memberP(cons(skaf55(X1),sk2),skaf55(X1)),
    inference(scs_inference,[],[i_0_345,i_0_388,i_0_486,i_0_527,i_0_316,i_0_350,i_0_564,i_0_600,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_464,i_0_462,i_0_430,i_0_429,i_0_457]) ).

cnf(i_0_676,plain,
    frontsegP(cons(skaf55(X1),sk2),cons(skaf55(X1),sk2)),
    inference(scs_inference,[],[i_0_345,i_0_388,i_0_486,i_0_527,i_0_316,i_0_350,i_0_517,i_0_564,i_0_600,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_464,i_0_462,i_0_430,i_0_429,i_0_457,i_0_450]) ).

cnf(i_0_706,plain,
    ~ neq(sk1,sk3),
    inference(scs_inference,[],[i_0_527,i_0_317,i_0_351,i_0_600,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_462,i_0_464,i_0_430]) ).

cnf(i_0_707,plain,
    memberP(cons(skaf59(X1),sk4),skaf59(X1)),
    inference(scs_inference,[],[i_0_386,i_0_527,i_0_317,i_0_351,i_0_600,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_462,i_0_464,i_0_430,i_0_457]) ).

cnf(i_0_709,plain,
    frontsegP(cons(skaf59(X1),sk4),cons(skaf59(X1),sk4)),
    inference(scs_inference,[],[i_0_386,i_0_527,i_0_317,i_0_351,i_0_549,i_0_600,i_0_321,i_0_331,i_0_332,i_0_333,i_0_334,i_0_330,i_0_462,i_0_464,i_0_430,i_0_457,i_0_450]) ).

cnf(i_0_878,plain,
    ~ neq(skaf55(X1),skaf55(X1)),
    inference(equality_inference,[],[873]) ).

cnf(i_0_879,plain,
    ~ neq(skaf55(X1),skaf55(X1)),
    inference(equality_inference,[],[874]) ).

cnf(i_0_880,plain,
    ssItem(skaf70(X1)),
    inference(equality_inference,[],[875]) ).

cnf(i_0_881,plain,
    ~ lt(skaf65(X1),skaf65(X1)),
    inference(equality_inference,[],[876]) ).

cnf(i_0_882,plain,
    ~ lt(skaf65(X1),skaf65(X1)),
    inference(equality_inference,[],[877]) ).

cnf(i_0_1500,plain,
    ssItem(skaf44(X1)),
    inference(equality_inference,[],[1492]) ).

cnf(i_0_1501,plain,
    ~ lt(skaf44(X1),skaf44(X1)),
    inference(equality_inference,[],[1493]) ).

cnf(i_0_1502,plain,
    geq(skaf44(X1),skaf44(X1)),
    inference(equality_inference,[],[1495]) ).

cnf(i_0_1503,plain,
    leq(skaf44(X1),skaf44(X1)),
    inference(equality_inference,[],[1497]) ).

cnf(i_0_1785,plain,
    ~ neq(skaf43(X1,X2),skaf43(X1,X2)),
    inference(equality_inference,[],[1781]) ).

cnf(i_0_2008,plain,
    ~ neq(skaf43(X1,X2),skaf43(X1,X2)),
    inference(equality_inference,[],[2004]) ).

cnf(i_0_2009,plain,
    ~ neq(skaf46(X1,X2),skaf46(X1,X2)),
    inference(equality_inference,[],[2005]) ).

cnf(i_0_2385,plain,
    ~ memberP(nil,hd(sk3)),
    inference(scs_inference,[],[i_0_2268,i_0_325]) ).

cnf(i_0_2387,plain,
    frontsegP(tl(sk3),nil),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337]) ).

cnf(i_0_2389,plain,
    rearsegP(tl(sk3),nil),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338]) ).

cnf(i_0_2391,plain,
    segmentP(tl(sk3),nil),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339]) ).

cnf(i_0_2393,plain,
    cyclefreeP(cons(hd(sk3),nil)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304]) ).

cnf(i_0_2395,plain,
    totalorderP(cons(hd(sk3),nil)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305]) ).

cnf(i_0_2397,plain,
    strictorderP(cons(hd(sk3),nil)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306]) ).

cnf(i_0_2399,plain,
    totalorderedP(cons(hd(sk3),nil)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307]) ).

cnf(i_0_2401,plain,
    strictorderedP(cons(hd(sk3),nil)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308]) ).

cnf(i_0_2403,plain,
    duplicatefreeP(cons(hd(sk3),nil)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309]) ).

cnf(i_0_2405,plain,
    equalelemsP(cons(hd(sk3),nil)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310]) ).

cnf(i_0_2407,plain,
    app(nil,tl(sk3)) = tl(sk3),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335]) ).

cnf(i_0_2409,plain,
    app(tl(sk3),nil) = tl(sk3),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336]) ).

cnf(i_0_2411,plain,
    app(app(app(sk3,sk6),X1),X2) = app(app(sk4,X1),X2),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407]) ).

cnf(i_0_2412,plain,
    app(X1,app(app(sk3,sk6),X2)) = app(X1,app(sk4,X2)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408]) ).

cnf(i_0_2413,plain,
    cons(app(app(sk3,sk6),X1),X2) = cons(app(sk4,X1),X2),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409]) ).

cnf(i_0_2414,plain,
    cons(X1,app(app(sk3,sk6),X2)) = cons(X1,app(sk4,X2)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410]) ).

cnf(i_0_2415,plain,
    hd(app(app(sk3,sk6),X1)) = hd(app(sk4,X1)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413]) ).

cnf(i_0_2416,plain,
    tl(app(app(sk3,sk6),X1)) = tl(app(sk4,X1)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414]) ).

cnf(i_0_2417,plain,
    ~ neq(sk6,app(app(skaf47(sk6,sk6),sk6),skaf48(sk6,sk6))),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_2322,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999]) ).

cnf(i_0_2418,plain,
    ~ neq(app(app(skaf47(sk6,sk6),sk6),skaf48(sk6,sk6)),sk6),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_2322,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086]) ).

cnf(i_0_2419,plain,
    skaf78(app(app(sk3,sk6),X1)) = skaf78(app(sk4,X1)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_2322,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411]) ).

cnf(i_0_2420,plain,
    skaf79(app(app(sk3,sk6),X1)) = skaf79(app(sk4,X1)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2208,i_0_2322,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412]) ).

cnf(i_0_2421,plain,
    skaf80(X1) != cons(skaf55(X2),skaf80(X1)),
    inference(scs_inference,[],[i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405]) ).

cnf(i_0_2422,plain,
    ~ gt(skaf55(X1),hd(cons(skaf55(X1),skaf80(X2)))),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426]) ).

cnf(i_0_2423,plain,
    hd(cons(skaf55(X1),skaf80(X2))) = skaf55(X1),
    inference(rename_variables,[],[i_0_2274]) ).

cnf(i_0_2424,plain,
    ssList(app(tl(sk3),tl(sk3))),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290]) ).

cnf(i_0_2426,plain,
    cons(hd(sk3),tl(sk3)) != tl(sk3),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300]) ).

cnf(i_0_2428,plain,
    ~ frontsegP(nil,sk1),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322]) ).

cnf(i_0_2430,plain,
    ~ rearsegP(nil,sk1),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323]) ).

cnf(i_0_2432,plain,
    ~ segmentP(nil,sk1),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324]) ).

cnf(i_0_2434,plain,
    ssList(tl(sk1)),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343]) ).

cnf(i_0_2436,plain,
    cons(hd(sk3),tl(sk3)) != nil,
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301]) ).

cnf(i_0_2438,plain,
    hd(cons(hd(sk3),tl(sk3))) = hd(sk3),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288]) ).

cnf(i_0_2440,plain,
    tl(cons(hd(sk3),tl(sk3))) = tl(sk3),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289]) ).

cnf(i_0_2442,plain,
    cons(hd(sk1),tl(sk1)) = sk1,
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302]) ).

cnf(i_0_2444,plain,
    cons(skaf83(sk1),skaf82(sk1)) = sk1,
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303]) ).

cnf(i_0_2446,plain,
    app(cons(hd(sk3),nil),tl(sk3)) = cons(hd(sk3),tl(sk3)),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261]) ).

cnf(i_0_2448,plain,
    ssList(cons(hd(sk3),tl(sk3))),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291]) ).

cnf(i_0_2450,plain,
    ssItem(hd(sk1)),
    inference(scs_inference,[],[i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341]) ).

cnf(i_0_2452,plain,
    segmentP(sk1,sk3),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419]) ).

cnf(i_0_2453,plain,
    segmentP(sk3,sk1),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420]) ).

cnf(i_0_2454,plain,
    rearsegP(sk2,app(sk3,sk6)),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2322,i_0_2274,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423]) ).

cnf(i_0_2455,plain,
    geq(skaf79(sk4),skaf79(app(sk3,sk6))),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427]) ).

cnf(i_0_2457,plain,
    geq(skaf79(app(sk3,sk6)),skaf79(sk4)),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428]) ).

cnf(i_0_2459,plain,
    leq(skaf79(sk4),skaf79(app(sk3,sk6))),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433]) ).

cnf(i_0_2461,plain,
    leq(skaf79(app(sk3,sk6)),skaf79(sk4)),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2260,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434]) ).

cnf(i_0_2463,plain,
    memberP(cons(skaf79(app(sk3,sk6)),sk2),skaf79(sk4)),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2260,i_0_963,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437]) ).

cnf(i_0_2465,plain,
    frontsegP(sk2,app(sk3,sk6)),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2260,i_0_963,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421]) ).

cnf(i_0_2466,plain,
    frontsegP(app(sk3,sk6),sk2),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2260,i_0_963,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422]) ).

cnf(i_0_2467,plain,
    rearsegP(app(sk3,sk6),sk2),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424]) ).

cnf(i_0_2468,plain,
    app(app(sk3,sk6),app(sk3,sk6)) = app(sk4,sk4),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406]) ).

cnf(i_0_2471,plain,
    cons(skaf55(X1),nil) != cons(hd(sk3),sk3),
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2232,i_0_2336,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_527,i_0_400,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442]) ).

cnf(i_0_2472,plain,
    cons(hd(sk3),nil) != nil,
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2232,i_0_2336,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_400,i_0_390,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295]) ).

cnf(i_0_2474,plain,
    app(sk1,sk1) != nil,
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2232,i_0_2336,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_400,i_0_390,i_0_389,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296]) ).

cnf(i_0_2476,plain,
    app(sk3,sk3) != nil,
    inference(scs_inference,[],[i_0_628,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2232,i_0_2336,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297]) ).

cnf(i_0_2478,plain,
    app(skaf46(skaf82(X1),skaf82(X1)),skaf82(X1)) = skaf82(X1),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2232,i_0_2336,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251]) ).

cnf(i_0_2482,plain,
    ssList(cons(skaf55(X1),skaf80(X2))),
    inference(rename_variables,[],[i_0_2258]) ).

cnf(i_0_2484,plain,
    hd(app(sk1,sk1)) = hd(sk1),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284]) ).

cnf(i_0_2486,plain,
    app(app(tl(sk3),tl(sk3)),tl(sk3)) = app(tl(sk3),app(tl(sk3),tl(sk3))),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232]) ).

cnf(i_0_2488,plain,
    cons(hd(sk3),app(tl(sk3),tl(sk3))) = app(cons(hd(sk3),tl(sk3)),tl(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233]) ).

cnf(i_0_2490,plain,
    tl(app(sk1,sk1)) = app(tl(sk1),sk1),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259]) ).

cnf(i_0_2492,plain,
    app(app(skaf47(skaf82(X1),skaf82(X1)),skaf82(X1)),skaf48(skaf82(X1),skaf82(X1))) = skaf82(X1),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221]) ).

cnf(i_0_2495,plain,
    ~ gt(hd(sk3),hd(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280]) ).

cnf(i_0_2497,plain,
    frontsegP(app(tl(sk3),tl(sk3)),tl(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458]) ).

cnf(i_0_2499,plain,
    rearsegP(app(tl(sk3),tl(sk3)),tl(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459]) ).

cnf(i_0_2501,plain,
    ~ neq(cons(hd(sk3),tl(sk3)),sk3),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294]) ).

cnf(i_0_2504,plain,
    ssList(cons(skaf55(X1),skaf80(X2))),
    inference(rename_variables,[],[i_0_2258]) ).

cnf(i_0_3073,plain,
    memberP(cons(skaf55(X1),skaf80(X2)),skaf55(X1)),
    inference(rename_variables,[],[i_0_2324]) ).

cnf(i_0_652,plain,
    ssItem(skaf54(X1)),
    inference(equality_inference,[],[646]) ).

cnf(i_0_653,plain,
    ~ lt(skaf49(X1),skaf49(X1)),
    inference(equality_inference,[],[647]) ).

cnf(i_0_654,plain,
    ~ lt(skaf49(X1),skaf49(X1)),
    inference(equality_inference,[],[648]) ).

cnf(i_0_655,plain,
    ssList(skaf42(X1,X2)),
    inference(equality_inference,[],[649]) ).

cnf(i_0_686,plain,
    ssItem(skaf55(X1)),
    inference(equality_inference,[],[680]) ).

cnf(i_0_687,plain,
    ~ lt(skaf50(X1),skaf50(X1)),
    inference(equality_inference,[],[681]) ).

cnf(i_0_688,plain,
    ~ lt(skaf50(X1),skaf50(X1)),
    inference(equality_inference,[],[682]) ).

cnf(i_0_689,plain,
    ssList(skaf43(X1,X2)),
    inference(equality_inference,[],[683]) ).

cnf(i_0_718,plain,
    ssItem(skaf59(X1)),
    inference(equality_inference,[],[713]) ).

cnf(i_0_719,plain,
    ~ lt(skaf54(X1),skaf54(X1)),
    inference(equality_inference,[],[714]) ).

cnf(i_0_720,plain,
    ~ lt(skaf54(X1),skaf54(X1)),
    inference(equality_inference,[],[715]) ).

cnf(i_0_721,plain,
    ssList(skaf45(X1,X2)),
    inference(equality_inference,[],[716]) ).

cnf(i_0_722,plain,
    ~ neq(skaf44(X1),skaf44(X1)),
    inference(equality_inference,[],[717]) ).

cnf(i_0_817,plain,
    ~ neq(skaf50(X1),skaf50(X1)),
    inference(equality_inference,[],[812]) ).

cnf(i_0_818,plain,
    ssList(skaf48(X1,X2)),
    inference(equality_inference,[],[813]) ).

cnf(i_0_1555,plain,
    ~ neq(skaf50(X1),skaf50(X1)),
    inference(equality_inference,[],[1548]) ).

cnf(i_0_1556,plain,
    ~ lt(skaf70(X1),skaf70(X1)),
    inference(equality_inference,[],[1549]) ).

cnf(i_0_2362,plain,
    cons(skaf55(X1),sk2) != nil,
    inference(scs_inference,[],[i_0_345,i_0_480,i_0_626,i_0_660,i_0_662,i_0_674,i_0_931,i_0_1370,i_0_533,i_0_1015,i_0_917,i_0_2247,i_0_919,i_0_2251,i_0_476,i_0_658,i_0_1277,i_0_927,i_0_515,i_0_656,i_0_723,i_0_915,i_0_2293,i_0_403,i_0_379,i_0_2345,i_0_370,i_0_350,i_0_352,i_0_346,i_0_384,i_0_390,i_0_395,i_0_396,i_0_391,i_0_393,i_0_387,i_0_385,i_0_407,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_405,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_290,i_0_291,i_0_300,i_0_322,i_0_323,i_0_324,i_0_341,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_421,i_0_422,i_0_424,i_0_406,i_0_462,i_0_464,i_0_438,i_0_439,i_0_430,i_0_429,i_0_269,i_0_270,i_0_280,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_457,i_0_236,i_0_237,i_0_238,i_0_239,i_0_240,i_0_241,i_0_228,i_0_224,i_0_230,i_0_450,i_0_212,i_0_210,i_0_203,i_0_208,i_0_576,i_0_1999,i_0_2086,i_0_431,i_0_436]) ).

cnf(i_0_2363,plain,
    memberP(cons(skaf55(X1),sk2),skaf55(X1)),
    inference(rename_variables,[],[i_0_674]) ).

cnf(i_0_2503,plain,
    frontsegP(app(cons(skaf55(X1),skaf80(X2)),cons(skaf55(X1),skaf80(X2))),cons(skaf55(X1),skaf80(X2))),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239]) ).

cnf(i_0_2506,plain,
    rearsegP(app(skaf82(X1),skaf82(X1)),skaf82(X1)),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240]) ).

cnf(i_0_2509,plain,
    app(cons(hd(sk3),tl(sk3)),tl(sk3)) != app(tl(sk3),tl(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257]) ).

cnf(i_0_2511,plain,
    app(tl(sk3),cons(hd(sk3),tl(sk3))) != app(tl(sk3),tl(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258]) ).

cnf(i_0_2513,plain,
    app(sk3,nil) != nil,
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267]) ).

cnf(i_0_2515,plain,
    app(nil,sk3) != nil,
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268]) ).

cnf(i_0_2517,plain,
    ~ memberP(app(nil,nil),hd(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228]) ).

cnf(i_0_2519,plain,
    segmentP(app(app(skaf82(X1),skaf82(X1)),skaf82(X1)),skaf82(X1)),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224]) ).

cnf(i_0_2522,plain,
    app(nil,cons(hd(sk3),nil)) != nil,
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230]) ).

cnf(i_0_2524,plain,
    ~ frontsegP(cons(hd(sk3),nil),cons(hd(sk3),sk3)),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_533,i_0_400,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230,i_0_223]) ).

cnf(i_0_2526,plain,
    frontsegP(cons(skaf59(X1),skaf80(X2)),cons(skaf59(X1),nil)),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2218,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_351,i_0_533,i_0_400,i_0_379,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230,i_0_223,i_0_450]) ).

cnf(i_0_2531,plain,
    memberP(cons(hd(sk3),tl(sk3)),hd(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2218,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_351,i_0_533,i_0_400,i_0_379,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230,i_0_223,i_0_450,i_0_278,i_0_457]) ).

cnf(i_0_2533,plain,
    memberP(app(cons(hd(sk3),tl(sk3)),cons(hd(sk3),tl(sk3))),hd(sk3)),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2218,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_351,i_0_533,i_0_400,i_0_379,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230,i_0_223,i_0_450,i_0_278,i_0_457,i_0_236]) ).

cnf(i_0_2535,plain,
    ~ frontsegP(cons(skac3,tl(sk3)),cons(skac2,tl(sk3))),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2218,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_401,i_0_351,i_0_533,i_0_384,i_0_383,i_0_400,i_0_379,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230,i_0_223,i_0_450,i_0_278,i_0_457,i_0_236,i_0_226]) ).

cnf(i_0_2537,plain,
    app(app(nil,sk3),nil) != nil,
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_2266,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2218,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_401,i_0_351,i_0_533,i_0_384,i_0_383,i_0_400,i_0_379,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230,i_0_223,i_0_450,i_0_278,i_0_457,i_0_236,i_0_226,i_0_229]) ).

cnf(i_0_2539,plain,
    cons(hd(sk3),tl(sk3)) != cons(hd(sk3),cons(hd(sk3),tl(sk3))),
    inference(scs_inference,[],[i_0_628,i_0_2262,i_0_2264,i_0_2266,i_0_1321,i_0_1323,i_0_2299,i_0_2301,i_0_2218,i_0_2245,i_0_2268,i_0_2270,i_0_2284,i_0_2285,i_0_2286,i_0_2260,i_0_963,i_0_2208,i_0_2209,i_0_2213,i_0_2258,i_0_2482,i_0_2232,i_0_2336,i_0_2278,i_0_2344,i_0_2322,i_0_2274,i_0_949,i_0_2456,i_0_951,i_0_2460,i_0_559,i_0_382,i_0_527,i_0_381,i_0_2479,i_0_2493,i_0_2507,i_0_401,i_0_351,i_0_533,i_0_384,i_0_383,i_0_400,i_0_379,i_0_390,i_0_389,i_0_387,i_0_325,i_0_337,i_0_338,i_0_339,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_335,i_0_336,i_0_407,i_0_408,i_0_409,i_0_410,i_0_413,i_0_414,i_0_1999,i_0_2086,i_0_411,i_0_412,i_0_405,i_0_426,i_0_290,i_0_300,i_0_322,i_0_323,i_0_324,i_0_343,i_0_301,i_0_288,i_0_289,i_0_302,i_0_303,i_0_261,i_0_291,i_0_341,i_0_419,i_0_420,i_0_423,i_0_427,i_0_428,i_0_433,i_0_434,i_0_437,i_0_421,i_0_422,i_0_424,i_0_406,i_0_442,i_0_295,i_0_296,i_0_297,i_0_251,i_0_252,i_0_284,i_0_232,i_0_233,i_0_259,i_0_221,i_0_280,i_0_458,i_0_459,i_0_294,i_0_239,i_0_240,i_0_257,i_0_258,i_0_267,i_0_268,i_0_228,i_0_224,i_0_230,i_0_223,i_0_450,i_0_278,i_0_457,i_0_236,i_0_226,i_0_229,i_0_254]) ).

cnf(i_0_2544,plain,
    ~ memberP(nil,hd(sk1)),
    inference(scs_inference,[],[i_0_2450,i_0_325]) ).

cnf(i_0_2546,plain,
    frontsegP(tl(sk1),nil),
    inference(scs_inference,[],[i_0_2434,i_0_2450,i_0_325,i_0_337]) ).

cnf(c_0_2484,axiom,
    ( rearsegP(X1,nil)
    | ~ ssList(X1) ),
    i_0_338 ).

cnf(c_0_2485,negated_conjecture,
    ssList(sk4),
    i_0_386 ).

cnf(c_0_2486,axiom,
    ( rearsegP(app(X1,X2),X3)
    | ~ rearsegP(X2,X3)
    | ~ ssList(X1)
    | ~ ssList(X3)
    | ~ ssList(X2) ),
    i_0_240 ).

cnf(c_0_2487,negated_conjecture,
    rearsegP(sk4,nil),
    inference(spm,[status(thm)],[c_0_2484,c_0_2485]) ).

cnf(c_0_2488,axiom,
    ssList(nil),
    i_0_390 ).

cnf(c_0_2489,negated_conjecture,
    ( rearsegP(app(X1,sk4),nil)
    | ~ ssList(X1) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2486,c_0_2487]),c_0_2488]),c_0_2485])]) ).

cnf(c_0_2490,negated_conjecture,
    ssList(sk6),
    i_0_385 ).

cnf(c_0_2491,negated_conjecture,
    ssList(sk1),
    i_0_389 ).

cnf(c_0_2492,negated_conjecture,
    sk1 = sk3,
    i_0_403 ).

cnf(c_0_2493,axiom,
    ( app(skaf46(X1,X2),X2) = X1
    | ~ rearsegP(X1,X2)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    i_0_251 ).

cnf(c_0_2494,negated_conjecture,
    rearsegP(app(sk6,sk4),nil),
    inference(spm,[status(thm)],[c_0_2489,c_0_2490]) ).

cnf(c_0_2495,axiom,
    ( app(X1,nil) = X1
    | ~ ssList(X1) ),
    i_0_336 ).

cnf(c_0_2496,axiom,
    ssList(skaf46(X1,X2)),
    i_0_318 ).

cnf(c_0_2497,negated_conjecture,
    nil != sk1,
    i_0_400 ).

cnf(c_0_2498,axiom,
    ( app(app(X1,X2),X3) = app(X1,app(X2,X3))
    | ~ ssList(X3)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    i_0_232 ).

cnf(c_0_2499,negated_conjecture,
    app(sk3,sk6) = sk4,
    i_0_345 ).

cnf(c_0_2500,negated_conjecture,
    ssList(sk3),
    inference(rw,[status(thm)],[c_0_2491,c_0_2492]) ).

cnf(c_0_2501,negated_conjecture,
    ( app(skaf46(app(sk6,sk4),nil),nil) = app(sk6,sk4)
    | ~ ssList(app(sk6,sk4)) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2493,c_0_2494]),c_0_2488])]) ).

cnf(c_0_2502,plain,
    app(skaf46(X1,X2),nil) = skaf46(X1,X2),
    inference(spm,[status(thm)],[c_0_2495,c_0_2496]) ).

cnf(c_0_2503,axiom,
    ( nil = X1
    | app(X1,X2) != nil
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    i_0_296 ).

cnf(c_0_2504,negated_conjecture,
    nil != sk3,
    inference(rw,[status(thm)],[c_0_2497,c_0_2492]) ).

cnf(c_0_2505,axiom,
    ( ssList(tl(X1))
    | nil = X1
    | ~ ssList(X1) ),
    i_0_342 ).

cnf(c_0_2506,axiom,
    ( ssItem(hd(X1))
    | nil = X1
    | ~ ssList(X1) ),
    i_0_340 ).

cnf(c_0_2507,negated_conjecture,
    ( app(sk3,app(sk6,X1)) = app(sk4,X1)
    | ~ ssList(X1) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2498,c_0_2499]),c_0_2490]),c_0_2500])]) ).

cnf(c_0_2508,negated_conjecture,
    ( skaf46(app(sk6,sk4),nil) = app(sk6,sk4)
    | ~ ssList(app(sk6,sk4)) ),
    inference(rw,[status(thm)],[c_0_2501,c_0_2502]) ).

cnf(c_0_2509,axiom,
    ( ssList(app(X1,X2))
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    i_0_290 ).

cnf(c_0_2510,axiom,
    ( app(app(X1,cons(X2,X3)),cons(X2,X4)) != X5
    | ~ ssList(X4)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2)
    | ~ duplicatefreeP(X5)
    | ~ ssList(X5) ),
    i_0_212 ).

cnf(c_0_2511,axiom,
    ( cons(hd(X1),tl(X1)) = X1
    | nil = X1
    | ~ ssList(X1) ),
    i_0_302 ).

cnf(c_0_2512,negated_conjecture,
    sk4 != nil,
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2503,c_0_2499]),c_0_2490]),c_0_2500])]),c_0_2504]) ).

cnf(c_0_2513,axiom,
    ( nil = X1
    | hd(app(X1,X2)) = hd(X1)
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    i_0_284 ).

cnf(c_0_2514,axiom,
    ( memberP(cons(X1,X2),X3)
    | X3 != X1
    | ~ ssList(X2)
    | ~ ssItem(X1)
    | ~ ssItem(X3) ),
    i_0_260 ).

cnf(c_0_2515,negated_conjecture,
    ( sk4 = nil
    | ssList(tl(sk4)) ),
    inference(spm,[status(thm)],[c_0_2505,c_0_2485]) ).

cnf(c_0_2516,negated_conjecture,
    ( sk4 = nil
    | ssItem(hd(sk4)) ),
    inference(spm,[status(thm)],[c_0_2506,c_0_2485]) ).

cnf(c_0_2517,negated_conjecture,
    app(sk3,app(sk6,sk4)) = app(sk4,sk4),
    inference(spm,[status(thm)],[c_0_2507,c_0_2485]) ).

cnf(c_0_2518,negated_conjecture,
    skaf46(app(sk6,sk4),nil) = app(sk6,sk4),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2508,c_0_2509]),c_0_2485]),c_0_2490])]) ).

cnf(c_0_2519,plain,
    ( ~ duplicatefreeP(app(app(X1,cons(X2,X3)),cons(X2,X4)))
    | ~ ssList(app(app(X1,cons(X2,X3)),cons(X2,X4)))
    | ~ ssList(X4)
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    inference(er,[status(thm)],[c_0_2510]) ).

cnf(c_0_2520,axiom,
    ( app(skaf42(X1,X2),cons(X2,skaf43(X2,X1))) = X1
    | ~ memberP(X1,X2)
    | ~ ssItem(X2)
    | ~ ssList(X1) ),
    i_0_222 ).

cnf(c_0_2521,axiom,
    ssList(skaf43(X1,X2)),
    i_0_316 ).

cnf(c_0_2522,axiom,
    ssList(skaf42(X1,X2)),
    i_0_315 ).

cnf(c_0_2523,negated_conjecture,
    cons(hd(sk4),tl(sk4)) = sk4,
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2511,c_0_2485]),c_0_2512]) ).

cnf(c_0_2524,negated_conjecture,
    hd(sk4) = hd(sk3),
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2513,c_0_2499]),c_0_2490]),c_0_2500])]),c_0_2504]) ).

cnf(c_0_2525,plain,
    ssItem(hd(sk1)),
    i_0_2450 ).

cnf(c_0_2526,plain,
    ( memberP(cons(X1,X2),X1)
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    inference(er,[status(thm)],[c_0_2514]) ).

cnf(c_0_2527,negated_conjecture,
    ssList(tl(sk4)),
    inference(sr,[status(thm)],[c_0_2515,c_0_2512]) ).

cnf(c_0_2528,negated_conjecture,
    ssItem(hd(sk4)),
    inference(sr,[status(thm)],[c_0_2516,c_0_2512]) ).

cnf(c_0_2529,negated_conjecture,
    ( ssList(app(sk4,sk4))
    | ~ ssList(app(sk6,sk4)) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2509,c_0_2517]),c_0_2500])]) ).

cnf(c_0_2530,negated_conjecture,
    ssList(app(sk6,sk4)),
    inference(spm,[status(thm)],[c_0_2496,c_0_2518]) ).

cnf(c_0_2531,plain,
    ( ~ duplicatefreeP(app(X1,cons(X2,X3)))
    | ~ memberP(X1,X2)
    | ~ ssList(app(X1,cons(X2,X3)))
    | ~ ssList(X3)
    | ~ ssList(X1)
    | ~ ssItem(X2) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2519,c_0_2520]),c_0_2521]),c_0_2522])]) ).

cnf(c_0_2532,negated_conjecture,
    cons(hd(sk3),tl(sk4)) = sk4,
    inference(rw,[status(thm)],[c_0_2523,c_0_2524]) ).

cnf(c_0_2533,plain,
    ssItem(hd(sk3)),
    inference(rw,[status(thm)],[c_0_2525,c_0_2492]) ).

cnf(c_0_2534,negated_conjecture,
    memberP(sk4,hd(sk4)),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2526,c_0_2523]),c_0_2527]),c_0_2528])]) ).

cnf(c_0_2535,axiom,
    ( duplicatefreeP(X1)
    | ssItem(X2)
    | ~ ssList(X1) ),
    i_0_344 ).

cnf(c_0_2536,negated_conjecture,
    ssList(app(sk4,sk4)),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2529,c_0_2530])]) ).

cnf(c_0_2537,negated_conjecture,
    ( ~ duplicatefreeP(app(X1,sk4))
    | ~ memberP(X1,hd(sk3))
    | ~ ssList(app(X1,sk4))
    | ~ ssList(X1) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2531,c_0_2532]),c_0_2527]),c_0_2533])]) ).

cnf(c_0_2538,negated_conjecture,
    memberP(sk4,hd(sk3)),
    inference(rw,[status(thm)],[c_0_2534,c_0_2524]) ).

cnf(c_0_2539,axiom,
    ( app(nil,X1) = X1
    | ~ ssList(X1) ),
    i_0_335 ).

cnf(c_0_2540,axiom,
    ( ssList(cons(X1,X2))
    | ~ ssItem(X1)
    | ~ ssList(X2) ),
    i_0_291 ).

cnf(c_0_2541,negated_conjecture,
    ( duplicatefreeP(app(sk4,sk4))
    | ssItem(X1) ),
    inference(spm,[status(thm)],[c_0_2535,c_0_2536]) ).

cnf(c_0_2542,negated_conjecture,
    ~ duplicatefreeP(app(sk4,sk4)),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2537,c_0_2536]),c_0_2538]),c_0_2485])]) ).

cnf(c_0_2543,negated_conjecture,
    ( memberP(X1,sk5(X2,X1,X3))
    | ~ ssItem(X3)
    | ~ ssList(X1)
    | ~ ssList(X2)
    | app(app(X1,cons(X3,nil)),X2) != sk1 ),
    i_0_204 ).

cnf(c_0_2544,plain,
    ( app(nil,cons(X1,X2)) = cons(X1,X2)
    | ~ ssList(X2)
    | ~ ssItem(X1) ),
    inference(spm,[status(thm)],[c_0_2539,c_0_2540]) ).

cnf(c_0_2545,negated_conjecture,
    ssItem(X1),
    inference(sr,[status(thm)],[c_0_2541,c_0_2542]) ).

cnf(c_0_2546,negated_conjecture,
    ( memberP(X1,sk5(X2,X1,X3))
    | app(app(X1,cons(X3,nil)),X2) != sk3
    | ~ ssList(X2)
    | ~ ssList(X1)
    | ~ ssItem(X3) ),
    inference(rw,[status(thm)],[c_0_2543,c_0_2492]) ).

cnf(c_0_2547,plain,
    ( app(nil,cons(X1,X2)) = cons(X1,X2)
    | ~ ssList(X2) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2544,c_0_2545])]) ).

cnf(c_0_2548,axiom,
    ( ~ memberP(nil,X1)
    | ~ ssItem(X1) ),
    i_0_325 ).

cnf(c_0_2549,plain,
    cons(hd(sk1),tl(sk1)) = sk1,
    i_0_2442 ).

cnf(c_0_2550,negated_conjecture,
    ( memberP(X1,sk5(X2,X1,X3))
    | app(app(X1,cons(X3,nil)),X2) != sk3
    | ~ ssList(X2)
    | ~ ssList(X1) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2546,c_0_2545])]) ).

cnf(c_0_2551,plain,
    app(nil,cons(X1,nil)) = cons(X1,nil),
    inference(spm,[status(thm)],[c_0_2547,c_0_2488]) ).

cnf(c_0_2552,plain,
    ~ memberP(nil,X1),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2548,c_0_2545])]) ).

cnf(c_0_2553,plain,
    app(cons(hd(sk3),nil),tl(sk3)) = cons(hd(sk3),tl(sk3)),
    i_0_2446 ).

cnf(c_0_2554,plain,
    cons(hd(sk3),tl(sk3)) = sk3,
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2549,c_0_2492]),c_0_2492]),c_0_2492]) ).

cnf(c_0_2555,plain,
    ssList(tl(sk1)),
    i_0_2434 ).

cnf(c_0_2556,negated_conjecture,
    ( app(cons(X1,nil),X2) != sk3
    | ~ ssList(X2) ),
    inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2550,c_0_2551]),c_0_2488])]),c_0_2552]) ).

cnf(c_0_2557,plain,
    app(cons(hd(sk3),nil),tl(sk3)) = sk3,
    inference(rw,[status(thm)],[c_0_2553,c_0_2554]) ).

cnf(c_0_2558,plain,
    ssList(tl(sk3)),
    inference(rw,[status(thm)],[c_0_2555,c_0_2492]) ).

cnf(c_0_2559,plain,
    $false,
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2556,c_0_2557]),c_0_2558])]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : SWC245-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12  % Command    : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32  % Computer : n015.cluster.edu
% 0.15/0.32  % Model    : x86_64 x86_64
% 0.15/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32  % Memory   : 8042.1875MB
% 0.15/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33  % CPULimit   : 300
% 0.15/0.33  % WCLimit    : 300
% 0.15/0.33  % DateTime   : Tue May  5 04:38:46 EDT 2026
% 0.15/0.33  % CPUTime    : 
% 0.15/0.34  % start to proof: theBenchmark
% 200.82/107.98  % Version  : CSE_E---1.7
% 200.82/107.98  % Problem  : theBenchmark.p
% 200.82/107.98  % SZS status Unsatisfiable for theBenchmark.p
% 200.82/107.98  % SZS output start CNFRefutation
% See solution above
% 209.11/116.21  % Total time : 106.731s
%------------------------------------------------------------------------------