CSE_E---1.7.UNS-CRf.s

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

% Computer : n024.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:01 PM UTC 2026

% Result   : Unsatisfiable 0.25s 1.51s
% Output   : CNFRefutation 0.54s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06  % Problem    : SWC040-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.06  % Command    : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.07/0.24  % Computer : n024.cluster.edu
% 0.07/0.24  % Model    : x86_64 x86_64
% 0.07/0.24  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.24  % Memory   : 8042.1875MB
% 0.07/0.24  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.07/0.24  % CPULimit   : 300
% 0.07/0.24  % WCLimit    : 300
% 0.07/0.24  % DateTime   : Mon May  4 23:17:26 EDT 2026
% 0.07/0.24  % CPUTime    : 
% 0.07/0.25  % start to proof: theBenchmark
% 0.25/1.51  % Version  : CSE_E---1.7
% 0.25/1.51  % Problem  : theBenchmark.p
% 0.25/1.51  % SZS status Unsatisfiable for theBenchmark.p
% 0.25/1.51  % SZS output start CNFRefutation
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause185)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause183)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause184)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause181)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause182)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause179)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause167)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause166)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause165)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause164)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause163)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause162)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause180)).
% 0.25/1.51  cnf(clause142, axiom, (equalelemsP(X1)|app(skaf80(X1),cons(skaf78(X1),cons(skaf79(X1),skaf81(X1))))=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause142)).
% 0.25/1.51  cnf(clause168, axiom, (app(app(skaf47(X1,X2),X2),skaf48(X2,X1))=X1|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause168)).
% 0.25/1.51  cnf(clause169, axiom, (app(skaf42(X1,X2),cons(X2,skaf43(X2,X1)))=X1|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause169)).
% 0.25/1.51  cnf(clause174, axiom, (frontsegP(X2,X4)|~frontsegP(cons(X1,X2),cons(X3,X4))|~ssList(X4)|~ssList(X2)|~ssItem(X3)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause174)).
% 0.25/1.51  cnf(clause172, axiom, (segmentP(app(app(X4,X1),X3),X2)|~segmentP(X1,X2)|~ssList(X3)|~ssList(X4)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause172)).
% 0.25/1.51  cnf(clause176, axiom, (X1=X3|~frontsegP(cons(X1,X2),cons(X3,X4))|~ssList(X4)|~ssList(X2)|~ssItem(X3)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause176)).
% 0.25/1.51  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/sandbox2/benchmark/Axioms/SWC001-0.ax', clause178)).
% 0.25/1.51  cnf(clause158, axiom, (memberP(X2,X3)|memberP(X1,X3)|~memberP(app(X1,X2),X3)|~ssList(X2)|~ssList(X1)|~ssItem(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause158)).
% 0.25/1.51  cnf(clause173, axiom, (segmentP(X4,X2)|app(app(X1,X2),X3)!=X4|~ssList(X3)|~ssList(X1)|~ssList(X2)|~ssList(X4)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause173)).
% 0.25/1.51  cnf(clause175, axiom, (memberP(X4,X2)|app(X1,cons(X2,X3))!=X4|~ssList(X3)|~ssList(X1)|~ssItem(X2)|~ssList(X4)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause175)).
% 0.25/1.51  cnf(clause161, axiom, (memberP(X2,X3)|X3=X1|~memberP(cons(X1,X2),X3)|~ssList(X2)|~ssItem(X1)|~ssItem(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause161)).
% 0.25/1.51  cnf(clause149, axiom, (app(app(X3,X2),X1)=app(X3,app(X2,X1))|~ssList(X1)|~ssList(X2)|~ssList(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause149)).
% 0.25/1.51  cnf(clause157, axiom, (cons(X1,app(X2,X3))=app(cons(X1,X2),X3)|~ssItem(X1)|~ssList(X2)|~ssList(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause157)).
% 0.25/1.51  cnf(clause159, axiom, (totalorderedP(cons(X1,X2))|nil=X2|~leq(X1,hd(X2))|~totalorderedP(X2)|~ssList(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause159)).
% 0.25/1.51  cnf(clause160, axiom, (strictorderedP(cons(X1,X2))|nil=X2|~lt(X1,hd(X2))|~strictorderedP(X2)|~ssList(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause160)).
% 0.25/1.51  cnf(clause140, axiom, (memberP(app(X1,X3),X2)|~memberP(X1,X2)|~ssList(X3)|~ssList(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause140)).
% 0.25/1.51  cnf(clause141, axiom, (memberP(app(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssList(X3)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause141)).
% 0.25/1.51  cnf(clause139, axiom, (memberP(cons(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause139)).
% 0.25/1.51  cnf(clause137, axiom, (frontsegP(app(X1,X3),X2)|~frontsegP(X1,X2)|~ssList(X3)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause137)).
% 0.25/1.51  cnf(clause136, axiom, (rearsegP(app(X3,X1),X2)|~rearsegP(X1,X2)|~ssList(X3)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause136)).
% 0.25/1.51  cnf(clause134, axiom, (lt(X1,hd(X2))|nil=X2|~strictorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause134)).
% 0.25/1.51  cnf(clause135, axiom, (leq(X1,hd(X2))|nil=X2|~totalorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause135)).
% 0.25/1.51  cnf(clause146, axiom, (gt(X1,X3)|~gt(X1,X2)|~gt(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause146)).
% 0.25/1.51  cnf(clause155, axiom, (lt(X1,X3)|~lt(X1,X2)|~lt(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause155)).
% 0.25/1.51  cnf(clause147, axiom, (lt(X1,X3)|~leq(X1,X2)|~lt(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause147)).
% 0.25/1.51  cnf(clause156, axiom, (leq(X1,X3)|~leq(X1,X2)|~leq(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause156)).
% 0.25/1.51  cnf(clause154, axiom, (frontsegP(X1,X3)|~frontsegP(X1,X2)|~frontsegP(X2,X3)|~ssList(X3)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause154)).
% 0.25/1.51  cnf(clause153, axiom, (rearsegP(X1,X3)|~rearsegP(X1,X2)|~rearsegP(X2,X3)|~ssList(X3)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause153)).
% 0.25/1.51  cnf(clause152, axiom, (segmentP(X1,X3)|~segmentP(X1,X2)|~segmentP(X2,X3)|~ssList(X3)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause152)).
% 0.25/1.51  cnf(clause148, axiom, (geq(X1,X3)|~geq(X1,X2)|~geq(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause148)).
% 0.25/1.51  cnf(clause131, axiom, (app(skaf46(X1,X2),X2)=X1|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause131)).
% 0.25/1.51  cnf(clause132, axiom, (app(X2,skaf45(X1,X2))=X1|~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause132)).
% 0.25/1.51  cnf(clause170, axiom, (X1=X3|cons(X1,X2)!=cons(X3,X4)|~ssItem(X3)|~ssItem(X1)|~ssList(X4)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause170)).
% 0.25/1.51  cnf(clause171, axiom, (X4=X2|cons(X1,X2)!=cons(X3,X4)|~ssItem(X3)|~ssItem(X1)|~ssList(X4)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause171)).
% 0.25/1.51  cnf(clause125, axiom, (totalorderedP(X2)|nil=X2|~totalorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause125)).
% 0.25/1.51  cnf(clause124, axiom, (strictorderedP(X2)|nil=X2|~strictorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause124)).
% 0.25/1.51  cnf(clause151, axiom, (X1=X3|app(X1,X2)!=app(X3,X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause151)).
% 0.25/1.51  cnf(clause150, axiom, (X2=X3|app(X1,X2)!=app(X1,X3)|~ssList(X2)|~ssList(X1)|~ssList(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause150)).
% 0.25/1.51  cnf(clause133, axiom, (nil=X2|tl(app(X2,X1))=app(tl(X2),X1)|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause133)).
% 0.25/1.51  cnf(clause138, axiom, (memberP(cons(X2,X3),X1)|X1!=X2|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause138)).
% 0.25/1.51  cnf(clause120, axiom, (app(cons(X1,nil),X2)=cons(X1,X2)|~ssItem(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause120)).
% 0.25/1.51  cnf(clause130, axiom, (X2=X1|~leq(X1,X2)|~leq(X2,X1)|~ssItem(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause130)).
% 0.25/1.51  cnf(clause126, axiom, (X2=X1|~geq(X1,X2)|~geq(X2,X1)|~ssItem(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause126)).
% 0.25/1.51  cnf(clause129, axiom, (X2=X1|~frontsegP(X1,X2)|~frontsegP(X2,X1)|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause129)).
% 0.25/1.51  cnf(clause128, axiom, (X2=X1|~rearsegP(X1,X2)|~rearsegP(X2,X1)|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause128)).
% 0.25/1.51  cnf(clause127, axiom, (X2=X1|~segmentP(X1,X2)|~segmentP(X2,X1)|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause127)).
% 0.25/1.51  cnf(clause144, axiom, (frontsegP(X3,X1)|app(X1,X2)!=X3|~ssList(X2)|~ssList(X1)|~ssList(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause144)).
% 0.25/1.51  cnf(clause143, axiom, (rearsegP(X3,X2)|app(X1,X2)!=X3|~ssList(X1)|~ssList(X2)|~ssList(X3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause143)).
% 0.25/1.51  cnf(clause110, axiom, (~gt(X1,X2)|~gt(X2,X1)|~ssItem(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause110)).
% 0.25/1.51  cnf(clause114, axiom, (~lt(X1,X2)|~lt(X2,X1)|~ssItem(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause114)).
% 0.25/1.51  cnf(clause122, axiom, (lt(X1,X2)|X1=X2|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause122)).
% 0.25/1.51  cnf(clause121, axiom, (lt(X1,X2)|X1=X2|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause121)).
% 0.25/1.51  cnf(clause95, axiom, (totalorderP(X1)|~leq(skaf54(X1),skaf55(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause95)).
% 0.25/1.51  cnf(clause94, axiom, (totalorderP(X1)|~leq(skaf55(X1),skaf54(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause94)).
% 0.25/1.51  cnf(clause93, axiom, (strictorderP(X1)|~lt(skaf59(X1),skaf60(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause93)).
% 0.25/1.51  cnf(clause92, axiom, (strictorderP(X1)|~lt(skaf60(X1),skaf59(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause92)).
% 0.25/1.51  cnf(clause91, axiom, (totalorderedP(X1)|~leq(skaf64(X1),skaf65(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause91)).
% 0.25/1.51  cnf(clause90, axiom, (strictorderedP(X1)|~lt(skaf69(X1),skaf70(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause90)).
% 0.25/1.51  cnf(clause106, axiom, (gt(X2,X1)|~lt(X1,X2)|~ssItem(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause106)).
% 0.25/1.51  cnf(clause105, axiom, (lt(X2,X1)|~gt(X1,X2)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause105)).
% 0.25/1.51  cnf(clause103, axiom, (leq(X1,X2)|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause103)).
% 0.25/1.51  cnf(clause107, axiom, (leq(X2,X1)|~geq(X1,X2)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause107)).
% 0.25/1.51  cnf(clause108, axiom, (geq(X2,X1)|~leq(X1,X2)|~ssItem(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause108)).
% 0.25/1.51  cnf(co1_12, negated_conjecture, (app(cons(sk5,nil),sk6)=sk3|~neq(sk4,nil)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_12)).
% 0.25/1.51  cnf(co1_13, negated_conjecture, (app(sk6,cons(sk5,nil))=sk4|~neq(sk4,nil)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_13)).
% 0.25/1.51  cnf(clause123, axiom, (nil=X2|hd(app(X2,X1))=hd(X2)|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause123)).
% 0.25/1.51  cnf(clause113, axiom, (totalorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause113)).
% 0.25/1.51  cnf(clause112, axiom, (strictorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause112)).
% 0.25/1.51  cnf(clause177, axiom, (nil=X2|X1=X2|nil=X1|tl(X1)!=tl(X2)|hd(X1)!=hd(X2)|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause177)).
% 0.25/1.51  cnf(clause97, axiom, (hd(cons(X1,X2))=X1|~ssItem(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause97)).
% 0.25/1.51  cnf(clause96, axiom, (tl(cons(X1,X2))=X2|~ssItem(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause96)).
% 0.25/1.51  cnf(clause85, axiom, (ssList(app(X2,X1))|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause85)).
% 0.25/1.51  cnf(clause86, axiom, (ssList(cons(X1,X2))|~ssItem(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause86)).
% 0.25/1.51  cnf(clause117, axiom, (X1!=X2|~neq(X1,X2)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause117)).
% 0.25/1.51  cnf(clause111, axiom, (X1!=X2|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause111)).
% 0.25/1.51  cnf(clause115, axiom, (X1!=X2|~neq(X1,X2)|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause115)).
% 0.25/1.51  cnf(clause116, axiom, (singletonP(X2)|cons(X1,nil)!=X2|~ssItem(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause116)).
% 0.25/1.51  cnf(clause118, axiom, (nil=X1|app(X1,X2)!=nil|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause118)).
% 0.25/1.51  cnf(clause119, axiom, (nil=X2|app(X1,X2)!=nil|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause119)).
% 0.25/1.51  cnf(clause88, axiom, (cyclefreeP(X1)|leq(skaf49(X1),skaf50(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause88)).
% 0.25/1.51  cnf(clause87, axiom, (cyclefreeP(X1)|leq(skaf50(X1),skaf49(X1))|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause87)).
% 0.25/1.51  cnf(clause99, axiom, (cons(X1,X2)!=X2|~ssItem(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause99)).
% 0.25/1.51  cnf(clause98, axiom, (cons(X1,X2)!=nil|~ssItem(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause98)).
% 0.25/1.51  cnf(clause104, axiom, (cons(hd(X1),tl(X1))=X1|nil=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause104)).
% 0.25/1.51  cnf(clause109, axiom, (cons(skaf83(X1),skaf82(X1))=X1|nil=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause109)).
% 0.25/1.51  cnf(clause70, axiom, (cyclefreeP(cons(X1,nil))|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause70)).
% 0.25/1.51  cnf(clause69, axiom, (totalorderP(cons(X1,nil))|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause69)).
% 0.25/1.51  cnf(clause68, axiom, (strictorderP(cons(X1,nil))|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause68)).
% 0.25/1.51  cnf(clause67, axiom, (totalorderedP(cons(X1,nil))|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause67)).
% 0.25/1.51  cnf(clause66, axiom, (strictorderedP(cons(X1,nil))|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause66)).
% 0.25/1.51  cnf(clause65, axiom, (duplicatefreeP(cons(X1,nil))|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause65)).
% 0.25/1.51  cnf(clause64, axiom, (equalelemsP(cons(X1,nil))|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause64)).
% 0.25/1.51  cnf(clause101, axiom, (cons(skaf44(X1),nil)=X1|~singletonP(X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause101)).
% 0.25/1.51  cnf(clause145, axiom, (app(X1,X2)=nil|nil!=X1|nil!=X2|~ssList(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause145)).
% 0.25/1.51  cnf(clause102, axiom, (neq(X2,X1)|X2=X1|~ssItem(X1)|~ssItem(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause102)).
% 0.25/1.51  cnf(clause100, axiom, (neq(X2,X1)|X2=X1|~ssList(X1)|~ssList(X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause100)).
% 0.25/1.51  cnf(clause53, axiom, (ssList(skaf42(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause53)).
% 0.25/1.51  cnf(clause52, axiom, (ssList(skaf43(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause52)).
% 0.25/1.51  cnf(clause51, axiom, (ssList(skaf45(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause51)).
% 0.25/1.51  cnf(clause50, axiom, (ssList(skaf46(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause50)).
% 0.25/1.51  cnf(clause49, axiom, (ssList(skaf47(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause49)).
% 0.25/1.51  cnf(clause48, axiom, (ssList(skaf48(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause48)).
% 0.25/1.51  cnf(clause63, axiom, (~lt(X1,X1)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause63)).
% 0.25/1.51  cnf(clause84, axiom, (nil=X1|~frontsegP(nil,X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause84)).
% 0.25/1.51  cnf(clause82, axiom, (nil=X1|~rearsegP(nil,X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause82)).
% 0.25/1.51  cnf(clause80, axiom, (nil=X1|~segmentP(nil,X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause80)).
% 0.25/1.51  cnf(clause71, axiom, (~memberP(nil,X1)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause71)).
% 0.25/1.51  cnf(clause89, axiom, (equalelemsP(X1)|skaf79(X1)!=skaf78(X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause89)).
% 0.25/1.51  cnf(clause83, axiom, (frontsegP(nil,X1)|nil!=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause83)).
% 0.25/1.51  cnf(clause81, axiom, (rearsegP(nil,X1)|nil!=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause81)).
% 0.25/1.51  cnf(clause79, axiom, (segmentP(nil,X1)|nil!=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause79)).
% 0.25/1.51  cnf(clause62, axiom, (leq(X1,X1)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause62)).
% 0.25/1.51  cnf(clause61, axiom, (frontsegP(X1,X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause61)).
% 0.25/1.51  cnf(clause59, axiom, (rearsegP(X1,X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause59)).
% 0.25/1.51  cnf(clause57, axiom, (segmentP(X1,X1)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause57)).
% 0.25/1.51  cnf(clause55, axiom, (geq(X1,X1)|~ssItem(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause55)).
% 0.25/1.51  cnf(co1_10, negated_conjecture, (ssItem(sk5)|~neq(sk4,nil)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_10)).
% 0.25/1.51  cnf(co1_11, negated_conjecture, (ssList(sk6)|~neq(sk4,nil)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_11)).
% 0.25/1.51  cnf(clause74, axiom, (app(nil,X1)=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause74)).
% 0.25/1.51  cnf(clause73, axiom, (app(X1,nil)=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause73)).
% 0.25/1.51  cnf(clause60, axiom, (frontsegP(X1,nil)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause60)).
% 0.25/1.51  cnf(clause58, axiom, (rearsegP(X1,nil)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause58)).
% 0.25/1.51  cnf(clause56, axiom, (segmentP(X1,nil)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause56)).
% 0.25/1.51  cnf(clause78, axiom, (ssItem(hd(X1))|nil=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause78)).
% 0.25/1.51  cnf(clause76, axiom, (ssItem(hd(X1))|nil=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause76)).
% 0.25/1.51  cnf(clause77, axiom, (ssList(tl(X1))|nil=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause77)).
% 0.25/1.51  cnf(clause75, axiom, (ssList(tl(X1))|nil=X1|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause75)).
% 0.25/1.51  cnf(clause72, axiom, (duplicatefreeP(X1)|ssItem(X2)|~ssList(X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause72)).
% 0.25/1.51  cnf(clause47, axiom, (ssItem(skaf44(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause47)).
% 0.25/1.51  cnf(clause46, axiom, (ssItem(skaf49(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause46)).
% 0.25/1.51  cnf(clause45, axiom, (ssItem(skaf50(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause45)).
% 0.25/1.51  cnf(clause41, axiom, (ssItem(skaf54(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause41)).
% 0.25/1.51  cnf(clause40, axiom, (ssItem(skaf55(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause40)).
% 0.25/1.51  cnf(clause36, axiom, (ssItem(skaf59(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause36)).
% 0.25/1.51  cnf(clause35, axiom, (ssItem(skaf60(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause35)).
% 0.25/1.51  cnf(clause31, axiom, (ssItem(skaf64(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause31)).
% 0.25/1.51  cnf(clause30, axiom, (ssItem(skaf65(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause30)).
% 0.25/1.51  cnf(clause26, axiom, (ssItem(skaf69(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause26)).
% 0.25/1.51  cnf(clause25, axiom, (ssItem(skaf70(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause25)).
% 0.25/1.51  cnf(clause21, axiom, (ssItem(skaf74(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause21)).
% 0.25/1.51  cnf(clause17, axiom, (ssItem(skaf78(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause17)).
% 0.25/1.51  cnf(clause16, axiom, (ssItem(skaf79(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause16)).
% 0.25/1.51  cnf(clause12, axiom, (ssItem(skaf83(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause12)).
% 0.25/1.51  cnf(clause44, axiom, (ssList(skaf51(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause44)).
% 0.25/1.51  cnf(clause43, axiom, (ssList(skaf52(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause43)).
% 0.25/1.51  cnf(clause42, axiom, (ssList(skaf53(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause42)).
% 0.25/1.51  cnf(clause39, axiom, (ssList(skaf56(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause39)).
% 0.25/1.51  cnf(clause38, axiom, (ssList(skaf57(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause38)).
% 0.25/1.51  cnf(clause37, axiom, (ssList(skaf58(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause37)).
% 0.25/1.51  cnf(clause34, axiom, (ssList(skaf61(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause34)).
% 0.25/1.51  cnf(clause33, axiom, (ssList(skaf62(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause33)).
% 0.25/1.51  cnf(clause32, axiom, (ssList(skaf63(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause32)).
% 0.25/1.51  cnf(clause29, axiom, (ssList(skaf66(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause29)).
% 0.25/1.51  cnf(clause28, axiom, (ssList(skaf67(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause28)).
% 0.25/1.51  cnf(clause27, axiom, (ssList(skaf68(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause27)).
% 0.25/1.51  cnf(clause24, axiom, (ssList(skaf71(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause24)).
% 0.25/1.51  cnf(clause23, axiom, (ssList(skaf72(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause23)).
% 0.25/1.51  cnf(clause22, axiom, (ssList(skaf73(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause22)).
% 0.25/1.51  cnf(clause20, axiom, (ssList(skaf75(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause20)).
% 0.25/1.51  cnf(clause19, axiom, (ssList(skaf76(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause19)).
% 0.25/1.51  cnf(clause18, axiom, (ssList(skaf77(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause18)).
% 0.25/1.51  cnf(clause15, axiom, (ssList(skaf80(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause15)).
% 0.25/1.51  cnf(clause14, axiom, (ssList(skaf81(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause14)).
% 0.25/1.51  cnf(clause13, axiom, (ssList(skaf82(X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause13)).
% 0.25/1.51  cnf(clause11, axiom, (~singletonP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause11)).
% 0.25/1.51  cnf(clause10, axiom, (ssItem(skac2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause10)).
% 0.25/1.51  cnf(clause9, axiom, (ssItem(skac3)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause9)).
% 0.25/1.51  cnf(co1_4, negated_conjecture, (ssList(sk4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_4)).
% 0.25/1.51  cnf(co1_3, negated_conjecture, (ssList(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_3)).
% 0.25/1.51  cnf(co1_2, negated_conjecture, (ssList(sk2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_2)).
% 0.25/1.51  cnf(co1_1, negated_conjecture, (ssList(sk1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_1)).
% 0.25/1.51  cnf(clause8, axiom, (ssList(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause8)).
% 0.25/1.51  cnf(clause7, axiom, (cyclefreeP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause7)).
% 0.25/1.51  cnf(clause6, axiom, (totalorderP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause6)).
% 0.25/1.51  cnf(clause5, axiom, (strictorderP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause5)).
% 0.25/1.51  cnf(clause4, axiom, (totalorderedP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause4)).
% 0.25/1.51  cnf(clause3, axiom, (strictorderedP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause3)).
% 0.25/1.51  cnf(clause2, axiom, (duplicatefreeP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause2)).
% 0.25/1.51  cnf(clause1, axiom, (equalelemsP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause1)).
% 0.25/1.51  cnf(co1_9, negated_conjecture, (nil=sk3|nil!=sk4), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_9)).
% 0.25/1.51  cnf(co1_8, negated_conjecture, (nil!=sk1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_8)).
% 0.25/1.51  cnf(clause54, axiom, (skac3!=skac2), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax', clause54)).
% 0.25/1.51  cnf(co1_6, negated_conjecture, (sk2=sk4), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_6)).
% 0.25/1.51  cnf(co1_7, negated_conjecture, (sk1=sk3), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_7)).
% 0.25/1.51  cnf(co1_5, negated_conjecture, (nil=sk2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1_5)).
% 0.25/1.51  cnf(i_0_198, 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']).
% 0.25/1.51  cnf(i_0_199, 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']).
% 0.25/1.51  cnf(i_0_200, 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']).
% 0.25/1.51  cnf(i_0_201, 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']).
% 0.25/1.51  cnf(i_0_202, 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']).
% 0.25/1.51  cnf(i_0_203, 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']).
% 0.25/1.51  cnf(i_0_204, axiom, (cyclefreeP(X1)|app(app(skaf51(X1),cons(skaf49(X1),skaf52(X1))),cons(skaf50(X1),skaf53(X1)))=X1|~ssList(X1)), clause167, ['final']).
% 0.25/1.51  cnf(i_0_205, axiom, (totalorderP(X1)|app(app(skaf56(X1),cons(skaf54(X1),skaf57(X1))),cons(skaf55(X1),skaf58(X1)))=X1|~ssList(X1)), clause166, ['final']).
% 0.25/1.51  cnf(i_0_206, axiom, (strictorderP(X1)|app(app(skaf61(X1),cons(skaf59(X1),skaf62(X1))),cons(skaf60(X1),skaf63(X1)))=X1|~ssList(X1)), clause165, ['final']).
% 0.25/1.51  cnf(i_0_207, axiom, (totalorderedP(X1)|app(app(skaf66(X1),cons(skaf64(X1),skaf67(X1))),cons(skaf65(X1),skaf68(X1)))=X1|~ssList(X1)), clause164, ['final']).
% 0.25/1.51  cnf(i_0_208, axiom, (strictorderedP(X1)|app(app(skaf71(X1),cons(skaf69(X1),skaf72(X1))),cons(skaf70(X1),skaf73(X1)))=X1|~ssList(X1)), clause163, ['final']).
% 0.25/1.51  cnf(i_0_209, axiom, (duplicatefreeP(X1)|app(app(skaf75(X1),cons(skaf74(X1),skaf76(X1))),cons(skaf74(X1),skaf77(X1)))=X1|~ssList(X1)), clause162, ['final']).
% 0.25/1.51  cnf(i_0_210, 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']).
% 0.25/1.51  cnf(i_0_211, axiom, (equalelemsP(X1)|app(skaf80(X1),cons(skaf78(X1),cons(skaf79(X1),skaf81(X1))))=X1|~ssList(X1)), clause142, ['final']).
% 0.25/1.51  cnf(i_0_212, axiom, (app(app(skaf47(X1,X2),X2),skaf48(X2,X1))=X1|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), clause168, ['final']).
% 0.25/1.51  cnf(i_0_213, axiom, (app(skaf42(X1,X2),cons(X2,skaf43(X2,X1)))=X1|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), clause169, ['final']).
% 0.25/1.51  cnf(i_0_214, axiom, (frontsegP(X2,X4)|~frontsegP(cons(X1,X2),cons(X3,X4))|~ssList(X4)|~ssList(X2)|~ssItem(X3)|~ssItem(X1)), clause174, ['final']).
% 0.25/1.51  cnf(i_0_215, axiom, (segmentP(app(app(X4,X1),X3),X2)|~segmentP(X1,X2)|~ssList(X3)|~ssList(X4)|~ssList(X2)|~ssList(X1)), clause172, ['final']).
% 0.25/1.51  cnf(i_0_216, axiom, (X1=X3|~frontsegP(cons(X1,X2),cons(X3,X4))|~ssList(X4)|~ssList(X2)|~ssItem(X3)|~ssItem(X1)), clause176, ['final']).
% 0.25/1.51  cnf(i_0_217, axiom, (frontsegP(cons(X3,X1),cons(X4,X2))|~frontsegP(X1,X2)|X3!=X4|~ssList(X2)|~ssList(X1)|~ssItem(X4)|~ssItem(X3)), clause178, ['final']).
% 0.25/1.51  cnf(i_0_218, axiom, (memberP(X2,X3)|memberP(X1,X3)|~memberP(app(X1,X2),X3)|~ssList(X2)|~ssList(X1)|~ssItem(X3)), clause158, ['final']).
% 0.25/1.51  cnf(i_0_219, axiom, (segmentP(X4,X2)|app(app(X1,X2),X3)!=X4|~ssList(X3)|~ssList(X1)|~ssList(X2)|~ssList(X4)), clause173, ['final']).
% 0.25/1.51  cnf(i_0_220, axiom, (memberP(X4,X2)|app(X1,cons(X2,X3))!=X4|~ssList(X3)|~ssList(X1)|~ssItem(X2)|~ssList(X4)), clause175, ['final']).
% 0.25/1.51  cnf(i_0_221, axiom, (memberP(X2,X3)|X3=X1|~memberP(cons(X1,X2),X3)|~ssList(X2)|~ssItem(X1)|~ssItem(X3)), clause161, ['final']).
% 0.25/1.51  cnf(i_0_222, axiom, (app(app(X3,X2),X1)=app(X3,app(X2,X1))|~ssList(X1)|~ssList(X2)|~ssList(X3)), clause149, ['final']).
% 0.25/1.51  cnf(i_0_223, axiom, (cons(X1,app(X2,X3))=app(cons(X1,X2),X3)|~ssItem(X1)|~ssList(X2)|~ssList(X3)), clause157, ['final']).
% 0.25/1.51  cnf(i_0_224, axiom, (totalorderedP(cons(X1,X2))|nil=X2|~leq(X1,hd(X2))|~totalorderedP(X2)|~ssList(X2)|~ssItem(X1)), clause159, ['final']).
% 0.25/1.51  cnf(i_0_225, axiom, (strictorderedP(cons(X1,X2))|nil=X2|~lt(X1,hd(X2))|~strictorderedP(X2)|~ssList(X2)|~ssItem(X1)), clause160, ['final']).
% 0.25/1.51  cnf(i_0_226, axiom, (memberP(app(X1,X3),X2)|~memberP(X1,X2)|~ssList(X3)|~ssList(X1)|~ssItem(X2)), clause140, ['final']).
% 0.25/1.51  cnf(i_0_227, axiom, (memberP(app(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssList(X3)|~ssItem(X2)), clause141, ['final']).
% 0.25/1.51  cnf(i_0_228, axiom, (memberP(cons(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X2)), clause139, ['final']).
% 0.25/1.51  cnf(i_0_229, axiom, (frontsegP(app(X1,X3),X2)|~frontsegP(X1,X2)|~ssList(X3)|~ssList(X2)|~ssList(X1)), clause137, ['final']).
% 0.25/1.51  cnf(i_0_230, axiom, (rearsegP(app(X3,X1),X2)|~rearsegP(X1,X2)|~ssList(X3)|~ssList(X2)|~ssList(X1)), clause136, ['final']).
% 0.25/1.51  cnf(i_0_231, axiom, (lt(X1,hd(X2))|nil=X2|~strictorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), clause134, ['final']).
% 0.25/1.51  cnf(i_0_232, axiom, (leq(X1,hd(X2))|nil=X2|~totalorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), clause135, ['final']).
% 0.25/1.51  cnf(i_0_233, axiom, (gt(X1,X3)|~gt(X1,X2)|~gt(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), clause146, ['final']).
% 0.25/1.51  cnf(i_0_234, axiom, (lt(X1,X3)|~lt(X1,X2)|~lt(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), clause155, ['final']).
% 0.25/1.51  cnf(i_0_235, axiom, (lt(X1,X3)|~leq(X1,X2)|~lt(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), clause147, ['final']).
% 0.25/1.51  cnf(i_0_236, axiom, (leq(X1,X3)|~leq(X1,X2)|~leq(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), clause156, ['final']).
% 0.25/1.51  cnf(i_0_237, axiom, (frontsegP(X1,X3)|~frontsegP(X1,X2)|~frontsegP(X2,X3)|~ssList(X3)|~ssList(X2)|~ssList(X1)), clause154, ['final']).
% 0.25/1.51  cnf(i_0_238, axiom, (rearsegP(X1,X3)|~rearsegP(X1,X2)|~rearsegP(X2,X3)|~ssList(X3)|~ssList(X2)|~ssList(X1)), clause153, ['final']).
% 0.25/1.51  cnf(i_0_239, axiom, (segmentP(X1,X3)|~segmentP(X1,X2)|~segmentP(X2,X3)|~ssList(X3)|~ssList(X2)|~ssList(X1)), clause152, ['final']).
% 0.25/1.51  cnf(i_0_240, axiom, (geq(X1,X3)|~geq(X1,X2)|~geq(X2,X3)|~ssItem(X3)|~ssItem(X2)|~ssItem(X1)), clause148, ['final']).
% 0.25/1.51  cnf(i_0_241, axiom, (app(skaf46(X1,X2),X2)=X1|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), clause131, ['final']).
% 0.25/1.51  cnf(i_0_242, axiom, (app(X2,skaf45(X1,X2))=X1|~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)), clause132, ['final']).
% 0.25/1.51  cnf(i_0_243, axiom, (X1=X3|cons(X1,X2)!=cons(X3,X4)|~ssItem(X3)|~ssItem(X1)|~ssList(X4)|~ssList(X2)), clause170, ['final']).
% 0.25/1.51  cnf(i_0_244, axiom, (X4=X2|cons(X1,X2)!=cons(X3,X4)|~ssItem(X3)|~ssItem(X1)|~ssList(X4)|~ssList(X2)), clause171, ['final']).
% 0.25/1.51  cnf(i_0_245, axiom, (totalorderedP(X2)|nil=X2|~totalorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), clause125, ['final']).
% 0.25/1.51  cnf(i_0_246, axiom, (strictorderedP(X2)|nil=X2|~strictorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), clause124, ['final']).
% 0.25/1.51  cnf(i_0_247, axiom, (X1=X3|app(X1,X2)!=app(X3,X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)), clause151, ['final']).
% 0.25/1.51  cnf(i_0_248, axiom, (X2=X3|app(X1,X2)!=app(X1,X3)|~ssList(X2)|~ssList(X1)|~ssList(X3)), clause150, ['final']).
% 0.25/1.51  cnf(i_0_249, axiom, (nil=X2|tl(app(X2,X1))=app(tl(X2),X1)|~ssList(X1)|~ssList(X2)), clause133, ['final']).
% 0.25/1.51  cnf(i_0_250, axiom, (memberP(cons(X2,X3),X1)|X1!=X2|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), clause138, ['final']).
% 0.25/1.51  cnf(i_0_251, axiom, (app(cons(X1,nil),X2)=cons(X1,X2)|~ssItem(X1)|~ssList(X2)), clause120, ['final']).
% 0.25/1.51  cnf(i_0_252, axiom, (X2=X1|~leq(X1,X2)|~leq(X2,X1)|~ssItem(X1)|~ssItem(X2)), clause130, ['final']).
% 0.25/1.51  cnf(i_0_253, axiom, (X2=X1|~geq(X1,X2)|~geq(X2,X1)|~ssItem(X1)|~ssItem(X2)), clause126, ['final']).
% 0.25/1.51  cnf(i_0_254, axiom, (X2=X1|~frontsegP(X1,X2)|~frontsegP(X2,X1)|~ssList(X1)|~ssList(X2)), clause129, ['final']).
% 0.25/1.51  cnf(i_0_255, axiom, (X2=X1|~rearsegP(X1,X2)|~rearsegP(X2,X1)|~ssList(X1)|~ssList(X2)), clause128, ['final']).
% 0.25/1.51  cnf(i_0_256, axiom, (X2=X1|~segmentP(X1,X2)|~segmentP(X2,X1)|~ssList(X1)|~ssList(X2)), clause127, ['final']).
% 0.25/1.51  cnf(i_0_257, axiom, (frontsegP(X3,X1)|app(X1,X2)!=X3|~ssList(X2)|~ssList(X1)|~ssList(X3)), clause144, ['final']).
% 0.25/1.51  cnf(i_0_258, axiom, (rearsegP(X3,X2)|app(X1,X2)!=X3|~ssList(X1)|~ssList(X2)|~ssList(X3)), clause143, ['final']).
% 0.25/1.51  cnf(i_0_259, axiom, (~gt(X1,X2)|~gt(X2,X1)|~ssItem(X1)|~ssItem(X2)), clause110, ['final']).
% 0.25/1.51  cnf(i_0_260, axiom, (~lt(X1,X2)|~lt(X2,X1)|~ssItem(X1)|~ssItem(X2)), clause114, ['final']).
% 0.25/1.51  cnf(i_0_261, axiom, (lt(X1,X2)|X1=X2|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)), clause122, ['final']).
% 0.25/1.51  cnf(i_0_262, axiom, (lt(X1,X2)|X1=X2|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)), clause121, ['final']).
% 0.25/1.51  cnf(i_0_263, axiom, (totalorderP(X1)|~leq(skaf54(X1),skaf55(X1))|~ssList(X1)), clause95, ['final']).
% 0.25/1.51  cnf(i_0_264, axiom, (totalorderP(X1)|~leq(skaf55(X1),skaf54(X1))|~ssList(X1)), clause94, ['final']).
% 0.25/1.51  cnf(i_0_265, axiom, (strictorderP(X1)|~lt(skaf59(X1),skaf60(X1))|~ssList(X1)), clause93, ['final']).
% 0.25/1.51  cnf(i_0_266, axiom, (strictorderP(X1)|~lt(skaf60(X1),skaf59(X1))|~ssList(X1)), clause92, ['final']).
% 0.25/1.51  cnf(i_0_267, axiom, (totalorderedP(X1)|~leq(skaf64(X1),skaf65(X1))|~ssList(X1)), clause91, ['final']).
% 0.25/1.51  cnf(i_0_268, axiom, (strictorderedP(X1)|~lt(skaf69(X1),skaf70(X1))|~ssList(X1)), clause90, ['final']).
% 0.25/1.51  cnf(i_0_269, axiom, (gt(X2,X1)|~lt(X1,X2)|~ssItem(X1)|~ssItem(X2)), clause106, ['final']).
% 0.25/1.51  cnf(i_0_270, axiom, (lt(X2,X1)|~gt(X1,X2)|~ssItem(X2)|~ssItem(X1)), clause105, ['final']).
% 0.25/1.51  cnf(i_0_271, axiom, (leq(X1,X2)|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), clause103, ['final']).
% 0.25/1.51  cnf(i_0_272, axiom, (leq(X2,X1)|~geq(X1,X2)|~ssItem(X2)|~ssItem(X1)), clause107, ['final']).
% 0.25/1.51  cnf(i_0_273, axiom, (geq(X2,X1)|~leq(X1,X2)|~ssItem(X1)|~ssItem(X2)), clause108, ['final']).
% 0.25/1.51  cnf(i_0_274, negated_conjecture, (app(cons(sk5,nil),sk6)=sk3|~neq(sk4,nil)), co1_12, ['final']).
% 0.25/1.51  cnf(i_0_275, negated_conjecture, (app(sk6,cons(sk5,nil))=sk4|~neq(sk4,nil)), co1_13, ['final']).
% 0.25/1.51  cnf(i_0_276, axiom, (nil=X2|hd(app(X2,X1))=hd(X2)|~ssList(X1)|~ssList(X2)), clause123, ['final']).
% 0.25/1.51  cnf(i_0_277, axiom, (totalorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), clause113, ['final']).
% 0.25/1.51  cnf(i_0_278, axiom, (strictorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), clause112, ['final']).
% 0.25/1.51  cnf(i_0_279, axiom, (nil=X2|X1=X2|nil=X1|tl(X1)!=tl(X2)|hd(X1)!=hd(X2)|~ssList(X1)|~ssList(X2)), clause177, ['final']).
% 0.25/1.51  cnf(i_0_280, axiom, (hd(cons(X1,X2))=X1|~ssItem(X1)|~ssList(X2)), clause97, ['final']).
% 0.25/1.51  cnf(i_0_281, axiom, (tl(cons(X1,X2))=X2|~ssItem(X1)|~ssList(X2)), clause96, ['final']).
% 0.25/1.51  cnf(i_0_282, axiom, (ssList(app(X2,X1))|~ssList(X1)|~ssList(X2)), clause85, ['final']).
% 0.25/1.51  cnf(i_0_283, axiom, (ssList(cons(X1,X2))|~ssItem(X1)|~ssList(X2)), clause86, ['final']).
% 0.25/1.51  cnf(i_0_284, axiom, (X1!=X2|~neq(X1,X2)|~ssItem(X2)|~ssItem(X1)), clause117, ['final']).
% 0.25/1.51  cnf(i_0_285, axiom, (X1!=X2|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), clause111, ['final']).
% 0.25/1.51  cnf(i_0_286, axiom, (X1!=X2|~neq(X1,X2)|~ssList(X2)|~ssList(X1)), clause115, ['final']).
% 0.25/1.51  cnf(i_0_287, axiom, (singletonP(X2)|cons(X1,nil)!=X2|~ssItem(X1)|~ssList(X2)), clause116, ['final']).
% 0.25/1.51  cnf(i_0_288, axiom, (nil=X1|app(X1,X2)!=nil|~ssList(X2)|~ssList(X1)), clause118, ['final']).
% 0.25/1.51  cnf(i_0_289, axiom, (nil=X2|app(X1,X2)!=nil|~ssList(X2)|~ssList(X1)), clause119, ['final']).
% 0.25/1.51  cnf(i_0_290, axiom, (cyclefreeP(X1)|leq(skaf49(X1),skaf50(X1))|~ssList(X1)), clause88, ['final']).
% 0.25/1.51  cnf(i_0_291, axiom, (cyclefreeP(X1)|leq(skaf50(X1),skaf49(X1))|~ssList(X1)), clause87, ['final']).
% 0.25/1.51  cnf(i_0_292, axiom, (cons(X1,X2)!=X2|~ssItem(X1)|~ssList(X2)), clause99, ['final']).
% 0.25/1.51  cnf(i_0_293, axiom, (cons(X1,X2)!=nil|~ssItem(X1)|~ssList(X2)), clause98, ['final']).
% 0.25/1.51  cnf(i_0_294, axiom, (cons(hd(X1),tl(X1))=X1|nil=X1|~ssList(X1)), clause104, ['final']).
% 0.25/1.51  cnf(i_0_295, axiom, (cons(skaf83(X1),skaf82(X1))=X1|nil=X1|~ssList(X1)), clause109, ['final']).
% 0.25/1.51  cnf(i_0_296, axiom, (cyclefreeP(cons(X1,nil))|~ssItem(X1)), clause70, ['final']).
% 0.25/1.51  cnf(i_0_297, axiom, (totalorderP(cons(X1,nil))|~ssItem(X1)), clause69, ['final']).
% 0.25/1.51  cnf(i_0_298, axiom, (strictorderP(cons(X1,nil))|~ssItem(X1)), clause68, ['final']).
% 0.25/1.51  cnf(i_0_299, axiom, (totalorderedP(cons(X1,nil))|~ssItem(X1)), clause67, ['final']).
% 0.25/1.51  cnf(i_0_300, axiom, (strictorderedP(cons(X1,nil))|~ssItem(X1)), clause66, ['final']).
% 0.25/1.51  cnf(i_0_301, axiom, (duplicatefreeP(cons(X1,nil))|~ssItem(X1)), clause65, ['final']).
% 0.25/1.51  cnf(i_0_302, axiom, (equalelemsP(cons(X1,nil))|~ssItem(X1)), clause64, ['final']).
% 0.25/1.51  cnf(i_0_303, axiom, (cons(skaf44(X1),nil)=X1|~singletonP(X1)|~ssList(X1)), clause101, ['final']).
% 0.25/1.51  cnf(i_0_304, axiom, (app(X1,X2)=nil|nil!=X1|nil!=X2|~ssList(X2)|~ssList(X1)), clause145, ['final']).
% 0.25/1.51  cnf(i_0_305, axiom, (neq(X2,X1)|X2=X1|~ssItem(X1)|~ssItem(X2)), clause102, ['final']).
% 0.25/1.51  cnf(i_0_306, axiom, (neq(X2,X1)|X2=X1|~ssList(X1)|~ssList(X2)), clause100, ['final']).
% 0.25/1.51  cnf(i_0_307, axiom, (ssList(skaf42(X1,X2))), clause53, ['final']).
% 0.25/1.51  cnf(i_0_308, axiom, (ssList(skaf43(X1,X2))), clause52, ['final']).
% 0.25/1.51  cnf(i_0_309, axiom, (ssList(skaf45(X1,X2))), clause51, ['final']).
% 0.25/1.51  cnf(i_0_310, axiom, (ssList(skaf46(X1,X2))), clause50, ['final']).
% 0.25/1.51  cnf(i_0_311, axiom, (ssList(skaf47(X1,X2))), clause49, ['final']).
% 0.25/1.51  cnf(i_0_312, axiom, (ssList(skaf48(X1,X2))), clause48, ['final']).
% 0.25/1.51  cnf(i_0_313, axiom, (~lt(X1,X1)|~ssItem(X1)), clause63, ['final']).
% 0.25/1.51  cnf(i_0_314, axiom, (nil=X1|~frontsegP(nil,X1)|~ssList(X1)), clause84, ['final']).
% 0.25/1.51  cnf(i_0_315, axiom, (nil=X1|~rearsegP(nil,X1)|~ssList(X1)), clause82, ['final']).
% 0.25/1.51  cnf(i_0_316, axiom, (nil=X1|~segmentP(nil,X1)|~ssList(X1)), clause80, ['final']).
% 0.25/1.51  cnf(i_0_317, axiom, (~memberP(nil,X1)|~ssItem(X1)), clause71, ['final']).
% 0.25/1.51  cnf(i_0_318, axiom, (equalelemsP(X1)|skaf79(X1)!=skaf78(X1)|~ssList(X1)), clause89, ['final']).
% 0.25/1.51  cnf(i_0_319, axiom, (frontsegP(nil,X1)|nil!=X1|~ssList(X1)), clause83, ['final']).
% 0.25/1.51  cnf(i_0_320, axiom, (rearsegP(nil,X1)|nil!=X1|~ssList(X1)), clause81, ['final']).
% 0.25/1.51  cnf(i_0_321, axiom, (segmentP(nil,X1)|nil!=X1|~ssList(X1)), clause79, ['final']).
% 0.25/1.51  cnf(i_0_322, axiom, (leq(X1,X1)|~ssItem(X1)), clause62, ['final']).
% 0.25/1.51  cnf(i_0_323, axiom, (frontsegP(X1,X1)|~ssList(X1)), clause61, ['final']).
% 0.25/1.51  cnf(i_0_324, axiom, (rearsegP(X1,X1)|~ssList(X1)), clause59, ['final']).
% 0.25/1.51  cnf(i_0_325, axiom, (segmentP(X1,X1)|~ssList(X1)), clause57, ['final']).
% 0.25/1.51  cnf(i_0_326, axiom, (geq(X1,X1)|~ssItem(X1)), clause55, ['final']).
% 0.25/1.51  cnf(i_0_327, negated_conjecture, (ssItem(sk5)|~neq(sk4,nil)), co1_10, ['final']).
% 0.25/1.51  cnf(i_0_328, negated_conjecture, (ssList(sk6)|~neq(sk4,nil)), co1_11, ['final']).
% 0.25/1.51  cnf(i_0_329, axiom, (app(nil,X1)=X1|~ssList(X1)), clause74, ['final']).
% 0.25/1.51  cnf(i_0_330, axiom, (app(X1,nil)=X1|~ssList(X1)), clause73, ['final']).
% 0.25/1.51  cnf(i_0_331, axiom, (frontsegP(X1,nil)|~ssList(X1)), clause60, ['final']).
% 0.25/1.51  cnf(i_0_332, axiom, (rearsegP(X1,nil)|~ssList(X1)), clause58, ['final']).
% 0.25/1.51  cnf(i_0_333, axiom, (segmentP(X1,nil)|~ssList(X1)), clause56, ['final']).
% 0.25/1.51  cnf(i_0_334, axiom, (ssItem(hd(X1))|nil=X1|~ssList(X1)), clause78, ['final']).
% 0.25/1.51  cnf(i_0_335, axiom, (ssItem(hd(X1))|nil=X1|~ssList(X1)), clause76, ['final']).
% 0.25/1.51  cnf(i_0_336, axiom, (ssList(tl(X1))|nil=X1|~ssList(X1)), clause77, ['final']).
% 0.25/1.51  cnf(i_0_337, axiom, (ssList(tl(X1))|nil=X1|~ssList(X1)), clause75, ['final']).
% 0.25/1.51  cnf(i_0_338, axiom, (duplicatefreeP(X1)|ssItem(X2)|~ssList(X1)), clause72, ['final']).
% 0.25/1.51  cnf(i_0_339, axiom, (ssItem(skaf44(X1))), clause47, ['final']).
% 0.25/1.51  cnf(i_0_340, axiom, (ssItem(skaf49(X1))), clause46, ['final']).
% 0.25/1.51  cnf(i_0_341, axiom, (ssItem(skaf50(X1))), clause45, ['final']).
% 0.25/1.51  cnf(i_0_342, axiom, (ssItem(skaf54(X1))), clause41, ['final']).
% 0.25/1.51  cnf(i_0_343, axiom, (ssItem(skaf55(X1))), clause40, ['final']).
% 0.25/1.51  cnf(i_0_344, axiom, (ssItem(skaf59(X1))), clause36, ['final']).
% 0.25/1.51  cnf(i_0_345, axiom, (ssItem(skaf60(X1))), clause35, ['final']).
% 0.25/1.51  cnf(i_0_346, axiom, (ssItem(skaf64(X1))), clause31, ['final']).
% 0.25/1.51  cnf(i_0_347, axiom, (ssItem(skaf65(X1))), clause30, ['final']).
% 0.25/1.51  cnf(i_0_348, axiom, (ssItem(skaf69(X1))), clause26, ['final']).
% 0.25/1.51  cnf(i_0_349, axiom, (ssItem(skaf70(X1))), clause25, ['final']).
% 0.25/1.51  cnf(i_0_350, axiom, (ssItem(skaf74(X1))), clause21, ['final']).
% 0.25/1.51  cnf(i_0_351, axiom, (ssItem(skaf78(X1))), clause17, ['final']).
% 0.25/1.51  cnf(i_0_352, axiom, (ssItem(skaf79(X1))), clause16, ['final']).
% 0.25/1.51  cnf(i_0_353, axiom, (ssItem(skaf83(X1))), clause12, ['final']).
% 0.25/1.51  cnf(i_0_354, axiom, (ssList(skaf51(X1))), clause44, ['final']).
% 0.25/1.51  cnf(i_0_355, axiom, (ssList(skaf52(X1))), clause43, ['final']).
% 0.25/1.51  cnf(i_0_356, axiom, (ssList(skaf53(X1))), clause42, ['final']).
% 0.25/1.51  cnf(i_0_357, axiom, (ssList(skaf56(X1))), clause39, ['final']).
% 0.25/1.51  cnf(i_0_358, axiom, (ssList(skaf57(X1))), clause38, ['final']).
% 0.25/1.51  cnf(i_0_359, axiom, (ssList(skaf58(X1))), clause37, ['final']).
% 0.25/1.51  cnf(i_0_360, axiom, (ssList(skaf61(X1))), clause34, ['final']).
% 0.25/1.51  cnf(i_0_361, axiom, (ssList(skaf62(X1))), clause33, ['final']).
% 0.25/1.51  cnf(i_0_362, axiom, (ssList(skaf63(X1))), clause32, ['final']).
% 0.25/1.51  cnf(i_0_363, axiom, (ssList(skaf66(X1))), clause29, ['final']).
% 0.25/1.51  cnf(i_0_364, axiom, (ssList(skaf67(X1))), clause28, ['final']).
% 0.25/1.51  cnf(i_0_365, axiom, (ssList(skaf68(X1))), clause27, ['final']).
% 0.25/1.51  cnf(i_0_366, axiom, (ssList(skaf71(X1))), clause24, ['final']).
% 0.25/1.51  cnf(i_0_367, axiom, (ssList(skaf72(X1))), clause23, ['final']).
% 0.25/1.51  cnf(i_0_368, axiom, (ssList(skaf73(X1))), clause22, ['final']).
% 0.25/1.51  cnf(i_0_369, axiom, (ssList(skaf75(X1))), clause20, ['final']).
% 0.25/1.51  cnf(i_0_370, axiom, (ssList(skaf76(X1))), clause19, ['final']).
% 0.25/1.51  cnf(i_0_371, axiom, (ssList(skaf77(X1))), clause18, ['final']).
% 0.25/1.51  cnf(i_0_372, axiom, (ssList(skaf80(X1))), clause15, ['final']).
% 0.25/1.51  cnf(i_0_373, axiom, (ssList(skaf81(X1))), clause14, ['final']).
% 0.25/1.51  cnf(i_0_374, axiom, (ssList(skaf82(X1))), clause13, ['final']).
% 0.25/1.51  cnf(i_0_375, axiom, (~singletonP(nil)), clause11, ['final']).
% 0.25/1.51  cnf(i_0_376, axiom, (ssItem(skac2)), clause10, ['final']).
% 0.25/1.51  cnf(i_0_377, axiom, (ssItem(skac3)), clause9, ['final']).
% 0.25/1.51  cnf(i_0_378, negated_conjecture, (ssList(sk4)), co1_4, ['final']).
% 0.25/1.51  cnf(i_0_379, negated_conjecture, (ssList(sk3)), co1_3, ['final']).
% 0.25/1.51  cnf(i_0_380, negated_conjecture, (ssList(sk2)), co1_2, ['final']).
% 0.25/1.51  cnf(i_0_381, negated_conjecture, (ssList(sk1)), co1_1, ['final']).
% 0.25/1.51  cnf(i_0_382, axiom, (ssList(nil)), clause8, ['final']).
% 0.25/1.51  cnf(i_0_383, axiom, (cyclefreeP(nil)), clause7, ['final']).
% 0.25/1.51  cnf(i_0_384, axiom, (totalorderP(nil)), clause6, ['final']).
% 0.25/1.51  cnf(i_0_385, axiom, (strictorderP(nil)), clause5, ['final']).
% 0.25/1.51  cnf(i_0_386, axiom, (totalorderedP(nil)), clause4, ['final']).
% 0.25/1.51  cnf(i_0_387, axiom, (strictorderedP(nil)), clause3, ['final']).
% 0.25/1.51  cnf(i_0_388, axiom, (duplicatefreeP(nil)), clause2, ['final']).
% 0.25/1.51  cnf(i_0_389, axiom, (equalelemsP(nil)), clause1, ['final']).
% 0.25/1.51  cnf(i_0_390, negated_conjecture, (nil=sk3|nil!=sk4), co1_9, ['final']).
% 0.25/1.51  cnf(i_0_391, negated_conjecture, (nil!=sk1), co1_8, ['final']).
% 0.25/1.51  cnf(i_0_392, axiom, (skac3!=skac2), clause54, ['final']).
% 0.25/1.51  cnf(i_0_393, negated_conjecture, (sk2=sk4), co1_6, ['final']).
% 0.25/1.51  cnf(i_0_394, negated_conjecture, (sk1=sk3), co1_7, ['final']).
% 0.25/1.51  cnf(i_0_395, negated_conjecture, (nil=sk2), co1_5, ['final']).
% 0.25/1.51  cnf(i_0_396, axiom, (X1=X1)).
% 0.25/1.51  cnf(i_0_397, axiom, (X1=X2|X2!=X1)).
% 0.25/1.51  cnf(i_0_398, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.51  cnf(i_0_399, axiom, (X1!=X2|app(X1,X3)=app(X2,X3))).
% 0.25/1.51  cnf(i_0_400, axiom, (X1!=X2|app(X3,X1)=app(X3,X2))).
% 0.25/1.51  cnf(i_0_401, axiom, (X1!=X2|cons(X1,X3)=cons(X2,X3))).
% 0.25/1.51  cnf(i_0_402, axiom, (X1!=X2|cons(X3,X1)=cons(X3,X2))).
% 0.25/1.51  cnf(i_0_403, axiom, (X1!=X2|skaf78(X1)=skaf78(X2))).
% 0.25/1.51  cnf(i_0_404, axiom, (X1!=X2|skaf79(X1)=skaf79(X2))).
% 0.25/1.51  cnf(i_0_405, axiom, (X1!=X2|hd(X1)=hd(X2))).
% 0.25/1.51  cnf(i_0_406, axiom, (X1!=X2|tl(X1)=tl(X2))).
% 0.25/1.51  cnf(i_0_407, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.25/1.51  cnf(i_0_408, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.25/1.51  cnf(i_0_409, axiom, (X1!=X2|~duplicatefreeP(X1)|duplicatefreeP(X2))).
% 0.25/1.51  cnf(i_0_410, axiom, (X1!=X2|~equalelemsP(X1)|equalelemsP(X2))).
% 0.25/1.51  cnf(i_0_411, axiom, (X1!=X2|~segmentP(X1,X3)|segmentP(X2,X3))).
% 0.25/1.51  cnf(i_0_412, axiom, (X1!=X2|~segmentP(X3,X1)|segmentP(X3,X2))).
% 0.25/1.51  cnf(i_0_413, axiom, (X1!=X2|~memberP(X1,X3)|memberP(X2,X3))).
% 0.25/1.51  cnf(i_0_414, axiom, (X1!=X2|~memberP(X3,X1)|memberP(X3,X2))).
% 0.25/1.51  cnf(i_0_415, axiom, (X1!=X2|~frontsegP(X1,X3)|frontsegP(X2,X3))).
% 0.25/1.51  cnf(i_0_416, axiom, (X1!=X2|~frontsegP(X3,X1)|frontsegP(X3,X2))).
% 0.25/1.51  cnf(i_0_417, axiom, (X1!=X2|~rearsegP(X1,X3)|rearsegP(X2,X3))).
% 0.25/1.51  cnf(i_0_418, axiom, (X1!=X2|~rearsegP(X3,X1)|rearsegP(X3,X2))).
% 0.25/1.51  cnf(i_0_419, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.25/1.51  cnf(i_0_420, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.25/1.51  cnf(i_0_421, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.25/1.51  cnf(i_0_422, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.25/1.51  cnf(i_0_423, axiom, (X1!=X2|~neq(X1,X3)|neq(X2,X3))).
% 0.25/1.51  cnf(i_0_424, axiom, (X1!=X2|~neq(X3,X1)|neq(X3,X2))).
% 0.25/1.51  cnf(i_0_425, axiom, (X1!=X2|~singletonP(X1)|singletonP(X2))).
% 0.25/1.51  cnf(i_0_426, axiom, (X1!=X2|~ssList(X1)|ssList(X2))).
% 0.25/1.52  cnf(i_0_427, axiom, (X1!=X2|~ssItem(X1)|ssItem(X2))).
% 0.25/1.52  cnf(i_0_428, axiom, (X1!=X2|~cyclefreeP(X1)|cyclefreeP(X2))).
% 0.25/1.52  cnf(i_0_429, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.25/1.52  cnf(i_0_430, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.25/1.52  cnf(i_0_431, axiom, (X1!=X2|~strictorderP(X1)|strictorderP(X2))).
% 0.25/1.52  cnf(i_0_432, axiom, (X1!=X2|~totalorderP(X1)|totalorderP(X2))).
% 0.25/1.52  cnf(i_0_433, axiom, (X1!=X2|~strictorderedP(X1)|strictorderedP(X2))).
% 0.25/1.52  cnf(i_0_434, axiom, (X1!=X2|~totalorderedP(X1)|totalorderedP(X2))).
% 0.54/1.88  cnf(i_0_396, axiom, (X1=X1)).
% 0.54/1.88  cnf(i_0_397, axiom, (X1=X2|X2!=X1)).
% 0.54/1.88  cnf(i_0_398, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.54/1.88  cnf(i_0_399, axiom, (X1!=X2|app(X1,X3)=app(X2,X3))).
% 0.54/1.88  cnf(i_0_400, axiom, (X1!=X2|app(X3,X1)=app(X3,X2))).
% 0.54/1.88  cnf(i_0_401, axiom, (X1!=X2|cons(X1,X3)=cons(X2,X3))).
% 0.54/1.88  cnf(i_0_402, axiom, (X1!=X2|cons(X3,X1)=cons(X3,X2))).
% 0.54/1.88  cnf(i_0_403, axiom, (X1!=X2|skaf78(X1)=skaf78(X2))).
% 0.54/1.88  cnf(i_0_404, axiom, (X1!=X2|skaf79(X1)=skaf79(X2))).
% 0.54/1.88  cnf(i_0_405, axiom, (X1!=X2|hd(X1)=hd(X2))).
% 0.54/1.88  cnf(i_0_406, axiom, (X1!=X2|tl(X1)=tl(X2))).
% 0.54/1.88  cnf(i_0_407, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.54/1.88  cnf(i_0_408, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.54/1.88  cnf(i_0_409, axiom, (X1!=X2|~duplicatefreeP(X1)|duplicatefreeP(X2))).
% 0.54/1.88  cnf(i_0_410, axiom, (X1!=X2|~equalelemsP(X1)|equalelemsP(X2))).
% 0.54/1.88  cnf(i_0_411, axiom, (X1!=X2|~segmentP(X1,X3)|segmentP(X2,X3))).
% 0.54/1.88  cnf(i_0_412, axiom, (X1!=X2|~segmentP(X3,X1)|segmentP(X3,X2))).
% 0.54/1.88  cnf(i_0_413, axiom, (X1!=X2|~memberP(X1,X3)|memberP(X2,X3))).
% 0.54/1.88  cnf(i_0_414, axiom, (X1!=X2|~memberP(X3,X1)|memberP(X3,X2))).
% 0.54/1.88  cnf(i_0_415, axiom, (X1!=X2|~frontsegP(X1,X3)|frontsegP(X2,X3))).
% 0.54/1.88  cnf(i_0_416, axiom, (X1!=X2|~frontsegP(X3,X1)|frontsegP(X3,X2))).
% 0.54/1.88  cnf(i_0_417, axiom, (X1!=X2|~rearsegP(X1,X3)|rearsegP(X2,X3))).
% 0.54/1.88  cnf(i_0_418, axiom, (X1!=X2|~rearsegP(X3,X1)|rearsegP(X3,X2))).
% 0.54/1.88  cnf(i_0_419, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.54/1.88  cnf(i_0_420, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.54/1.88  cnf(i_0_421, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.54/1.88  cnf(i_0_422, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.54/1.88  cnf(i_0_423, axiom, (X1!=X2|~neq(X1,X3)|neq(X2,X3))).
% 0.54/1.88  cnf(i_0_424, axiom, (X1!=X2|~neq(X3,X1)|neq(X3,X2))).
% 0.54/1.88  cnf(i_0_425, axiom, (X1!=X2|~singletonP(X1)|singletonP(X2))).
% 0.54/1.88  cnf(i_0_426, axiom, (X1!=X2|~ssList(X1)|ssList(X2))).
% 0.54/1.88  cnf(i_0_427, axiom, (X1!=X2|~ssItem(X1)|ssItem(X2))).
% 0.54/1.88  cnf(i_0_428, axiom, (X1!=X2|~cyclefreeP(X1)|cyclefreeP(X2))).
% 0.54/1.88  cnf(i_0_429, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.54/1.88  cnf(i_0_430, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.54/1.88  cnf(i_0_431, axiom, (X1!=X2|~strictorderP(X1)|strictorderP(X2))).
% 0.54/1.88  cnf(i_0_432, axiom, (X1!=X2|~totalorderP(X1)|totalorderP(X2))).
% 0.54/1.88  cnf(i_0_433, axiom, (X1!=X2|~strictorderedP(X1)|strictorderedP(X2))).
% 0.54/1.88  cnf(i_0_434, axiom, (X1!=X2|~totalorderedP(X1)|totalorderedP(X2))).
% 0.54/1.88  cnf(i_0_435, plain, (~leq(X1,X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~ssItem(X1)|~ssItem(X2)|~cyclefreeP(app(app(X5,cons(X2,X4)),cons(X1,X3)))|~ssList(app(app(X5,cons(X2,X4)),cons(X1,X3)))|~leq(X2,X1)), inference(equality_inference,[],[198])).
% 0.54/1.88  cnf(i_0_436, plain, (lt(X1,X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~ssItem(X1)|~ssItem(X2)|~strictorderP(app(app(X5,cons(X2,X4)),cons(X1,X3)))|~ssList(app(app(X5,cons(X2,X4)),cons(X1,X3)))|lt(X2,X1)), inference(equality_inference,[],[199])).
% 0.54/1.88  cnf(i_0_437, plain, (leq(X1,X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)|~ssItem(X1)|~ssItem(X2)|~totalorderP(app(app(X5,cons(X2,X4)),cons(X1,X3)))|~ssList(app(app(X5,cons(X2,X4)),cons(X1,X3)))|leq(X2,X1)), inference(equality_inference,[],[200])).
% 0.54/1.88  cnf(i_0_438, plain, (~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssItem(X4)|~ssItem(X5)|~strictorderedP(app(app(X3,cons(X5,X2)),cons(X4,X1)))|~ssList(app(app(X3,cons(X5,X2)),cons(X4,X1)))|lt(X5,X4)), inference(equality_inference,[],[201])).
% 0.54/1.88  cnf(i_0_439, plain, (~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssItem(X4)|~ssItem(X5)|~totalorderedP(app(app(X3,cons(X5,X2)),cons(X4,X1)))|~ssList(app(app(X3,cons(X5,X2)),cons(X4,X1)))|leq(X5,X4)), inference(equality_inference,[],[202])).
% 0.54/1.88  cnf(i_0_440, plain, (~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssItem(X4)|~duplicatefreeP(app(app(X3,cons(X4,X2)),cons(X4,X1)))|~ssList(app(app(X3,cons(X4,X2)),cons(X4,X1)))), inference(equality_inference,[],[203])).
% 0.54/1.88  cnf(i_0_441, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X4)|~equalelemsP(app(X2,cons(X4,cons(X3,X1))))|~ssList(app(X2,cons(X4,cons(X3,X1))))|X4=X3), inference(equality_inference,[],[210])).
% 0.54/1.88  cnf(i_0_442, plain, (~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X1),cons(X3,X2))), inference(equality_inference,[],[217])).
% 0.54/1.88  cnf(i_0_443, plain, (~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(app(app(X2,X3),X1))|segmentP(app(app(X2,X3),X1),X3)), inference(equality_inference,[],[219])).
% 0.54/1.88  cnf(i_0_444, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssList(app(X2,cons(X3,X1)))|memberP(app(X2,cons(X3,X1)),X3)), inference(equality_inference,[],[220])).
% 0.54/1.88  cnf(i_0_445, plain, (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X2)|X1=X1), inference(equality_inference,[],[243])).
% 0.54/1.88  cnf(i_0_446, plain, (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X2)|X2=X2), inference(equality_inference,[],[244])).
% 0.54/1.88  cnf(i_0_447, plain, (~ssList(X1)|~ssList(X2)|~ssList(X1)|X1=X1), inference(equality_inference,[],[247])).
% 0.54/1.88  cnf(i_0_448, plain, (~ssList(X1)|~ssList(X2)|~ssList(X1)|X1=X1), inference(equality_inference,[],[248])).
% 0.54/1.88  cnf(i_0_449, plain, (~ssList(X1)|~ssItem(X2)|~ssItem(X2)|memberP(cons(X2,X1),X2)), inference(equality_inference,[],[250])).
% 0.54/1.88  cnf(i_0_450, plain, (~ssList(X1)|~ssList(X2)|~ssList(app(X2,X1))|frontsegP(app(X2,X1),X2)), inference(equality_inference,[],[257])).
% 0.54/1.88  cnf(i_0_451, plain, (~ssList(X1)|~ssList(X2)|~ssList(app(X1,X2))|rearsegP(app(X1,X2),X2)), inference(equality_inference,[],[258])).
% 0.54/1.88  cnf(i_0_452, plain, (~ssList(nil)|~ssItem(X1)|totalorderedP(cons(X1,nil))), inference(equality_inference,[],[277])).
% 0.54/1.88  cnf(i_0_453, plain, (~ssList(nil)|~ssItem(X1)|strictorderedP(cons(X1,nil))), inference(equality_inference,[],[278])).
% 0.54/1.88  cnf(i_0_454, plain, (~neq(X1,X1)|~ssItem(X1)|~ssItem(X1)), inference(equality_inference,[],[284])).
% 0.54/1.88  cnf(i_0_455, plain, (~lt(X1,X1)|~ssItem(X1)|~ssItem(X1)), inference(equality_inference,[],[285])).
% 0.54/1.88  cnf(i_0_456, plain, (~neq(X1,X1)|~ssList(X1)|~ssList(X1)), inference(equality_inference,[],[286])).
% 0.54/1.88  cnf(i_0_457, plain, (~ssItem(X1)|~ssList(cons(X1,nil))|singletonP(cons(X1,nil))), inference(equality_inference,[],[287])).
% 0.54/1.88  cnf(i_0_458, plain, (~ssList(nil)|frontsegP(nil,nil)), inference(equality_inference,[],[319])).
% 0.54/1.88  cnf(i_0_459, plain, (~ssList(nil)|rearsegP(nil,nil)), inference(equality_inference,[],[320])).
% 0.54/1.88  cnf(i_0_460, plain, (~ssList(nil)|segmentP(nil,nil)), inference(equality_inference,[],[321])).
% 0.54/1.88  cnf(i_0_461, plain, (sk4=sk2), inference(scs_inference,[],[i_0_393,i_0_397])).
% 0.54/1.88  cnf(i_0_462, plain, (~lt(skac2,skac2)), inference(scs_inference,[],[i_0_393,i_0_376,i_0_397,i_0_313])).
% 0.54/1.88  cnf(i_0_463, plain, (~ssItem(X1)|~lt(X1,X1)), inference(rename_variables,[],[i_0_313])).
% 0.54/1.88  cnf(i_0_464, plain, (leq(skac2,skac2)), inference(scs_inference,[],[i_0_393,i_0_376,i_0_397,i_0_313,i_0_322])).
% 0.54/1.88  cnf(i_0_465, plain, (~ssItem(X1)|leq(X1,X1)), inference(rename_variables,[],[i_0_322])).
% 0.54/1.88  cnf(i_0_466, plain, (frontsegP(sk4,sk4)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_376,i_0_397,i_0_313,i_0_322,i_0_323])).
% 0.54/1.88  cnf(i_0_467, plain, (~ssList(X1)|frontsegP(X1,X1)), inference(rename_variables,[],[i_0_323])).
% 0.54/1.88  cnf(i_0_468, plain, (rearsegP(sk4,sk4)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_376,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324])).
% 0.54/1.88  cnf(i_0_469, plain, (~ssList(X1)|rearsegP(X1,X1)), inference(rename_variables,[],[i_0_324])).
% 0.54/1.88  cnf(i_0_470, plain, (segmentP(sk4,sk4)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_376,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325])).
% 0.54/1.88  cnf(i_0_471, plain, (~ssList(X1)|segmentP(X1,X1)), inference(rename_variables,[],[i_0_325])).
% 0.54/1.88  cnf(i_0_472, plain, (geq(skac2,skac2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_376,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326])).
% 0.54/1.88  cnf(i_0_473, plain, (~ssItem(X1)|geq(X1,X1)), inference(rename_variables,[],[i_0_326])).
% 0.54/1.88  cnf(i_0_474, plain, (~neq(skac2,skac2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_376,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454])).
% 0.54/1.88  cnf(i_0_475, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_454])).
% 0.54/1.88  cnf(i_0_476, plain, (~neq(sk4,sk4)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_376,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456])).
% 0.54/1.88  cnf(i_0_477, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_456])).
% 0.54/1.88  cnf(i_0_478, plain, (nil=sk4), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398])).
% 0.54/1.88  cnf(i_0_479, plain, (duplicatefreeP(sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_388,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409])).
% 0.54/1.88  cnf(i_0_480, plain, (equalelemsP(sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410])).
% 0.54/1.88  cnf(i_0_481, plain, (~neq(sk2,sk4)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423])).
% 0.54/1.88  cnf(i_0_482, plain, (~neq(sk4,sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424])).
% 0.54/1.88  cnf(i_0_483, plain, (cyclefreeP(sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_383,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428])).
% 0.54/1.88  cnf(i_0_484, plain, (strictorderP(sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_383,i_0_385,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431])).
% 0.54/1.88  cnf(i_0_485, plain, (totalorderP(sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_383,i_0_384,i_0_385,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432])).
% 0.54/1.88  cnf(i_0_486, plain, (strictorderedP(sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_383,i_0_384,i_0_385,i_0_387,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433])).
% 0.54/1.88  cnf(i_0_487, plain, (totalorderedP(sk2)), inference(scs_inference,[],[i_0_378,i_0_393,i_0_395,i_0_376,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434])).
% 0.54/1.88  cnf(i_0_488, plain, (frontsegP(nil,sk2)), inference(scs_inference,[],[i_0_378,i_0_380,i_0_393,i_0_395,i_0_376,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319])).
% 0.54/1.88  cnf(i_0_489, plain, (nil!=X1|frontsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_319])).
% 0.54/1.88  cnf(i_0_490, plain, (rearsegP(nil,sk2)), inference(scs_inference,[],[i_0_378,i_0_380,i_0_393,i_0_395,i_0_376,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320])).
% 0.54/1.88  cnf(i_0_491, plain, (nil!=X1|rearsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_320])).
% 0.54/1.88  cnf(i_0_492, plain, (segmentP(nil,sk2)), inference(scs_inference,[],[i_0_378,i_0_380,i_0_393,i_0_395,i_0_376,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321])).
% 0.54/1.88  cnf(i_0_493, plain, (nil!=X1|segmentP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_321])).
% 0.54/1.88  cnf(i_0_494, plain, (memberP(cons(skac2,sk4),skac2)), inference(scs_inference,[],[i_0_378,i_0_380,i_0_393,i_0_395,i_0_376,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449])).
% 0.54/1.88  cnf(i_0_495, plain, (~ssItem(X1)|~ssItem(X1)|memberP(cons(X1,X2),X1)|~ssList(X2)), inference(rename_variables,[],[i_0_449])).
% 0.54/1.88  cnf(i_0_496, plain, (neq(skac3,skac2)), inference(scs_inference,[],[i_0_378,i_0_380,i_0_393,i_0_395,i_0_376,i_0_377,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_392,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449,i_0_305])).
% 0.54/1.88  cnf(i_0_497, plain, (X1=X2|~ssItem(X2)|~ssItem(X1)|neq(X1,X2)), inference(rename_variables,[],[i_0_305])).
% 0.54/1.88  cnf(i_0_498, plain, (neq(nil,sk1)), inference(scs_inference,[],[i_0_378,i_0_380,i_0_381,i_0_391,i_0_393,i_0_395,i_0_376,i_0_377,i_0_382,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_392,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449,i_0_305,i_0_306])).
% 0.54/1.88  cnf(i_0_499, plain, (X1=X2|~ssList(X2)|~ssList(X1)|neq(X1,X2)), inference(rename_variables,[],[i_0_306])).
% 0.54/1.88  cnf(i_0_500, plain, (frontsegP(cons(skac2,sk4),cons(skac2,sk4))), inference(scs_inference,[],[i_0_378,i_0_380,i_0_381,i_0_391,i_0_393,i_0_395,i_0_376,i_0_377,i_0_382,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_392,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449,i_0_305,i_0_306,i_0_442])).
% 0.54/1.88  cnf(i_0_501, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X2),cons(X3,X1))|~frontsegP(X2,X1)), inference(rename_variables,[],[i_0_442])).
% 0.54/1.88  cnf(i_0_502, plain, (ssList(X1)|sk3!=X1), inference(scs_inference,[],[i_0_378,i_0_379,i_0_380,i_0_381,i_0_391,i_0_393,i_0_395,i_0_376,i_0_377,i_0_382,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_392,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449,i_0_305,i_0_306,i_0_442,i_0_426])).
% 0.54/1.88  cnf(i_0_503, plain, (frontsegP(app(sk4,sk4),sk4)|sk3!=app(sk4,sk4)), inference(scs_inference,[],[i_0_378,i_0_379,i_0_380,i_0_381,i_0_391,i_0_393,i_0_395,i_0_376,i_0_377,i_0_382,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_392,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449,i_0_305,i_0_306,i_0_442,i_0_426,i_0_450])).
% 0.54/1.88  cnf(i_0_504, plain, (~ssList(app(X1,X2))|frontsegP(app(X1,X2),X1)|~ssList(X2)|~ssList(X1)), inference(rename_variables,[],[i_0_450])).
% 0.54/1.88  cnf(i_0_505, plain, (rearsegP(app(sk4,sk4),sk4)|sk3!=app(sk4,sk4)), inference(scs_inference,[],[i_0_378,i_0_379,i_0_380,i_0_381,i_0_391,i_0_393,i_0_395,i_0_376,i_0_377,i_0_382,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_392,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449,i_0_305,i_0_306,i_0_442,i_0_426,i_0_450,i_0_451])).
% 0.54/1.88  cnf(i_0_506, plain, (~ssList(app(X1,X2))|rearsegP(app(X1,X2),X2)|~ssList(X1)|~ssList(X2)), inference(rename_variables,[],[i_0_451])).
% 0.54/1.88  cnf(i_0_507, plain, (~ssList(skac2)|sk3!=app(sk4,sk4)|totalorderP(skac2)|~lt(app(app(skaf51(skac2),cons(skaf49(skac2),skaf52(skac2))),cons(skaf50(skac2),skaf53(skac2))),skac2)|~lt(skac2,app(app(skaf56(skac2),cons(skaf54(skac2),skaf57(skac2))),cons(skaf55(skac2),skaf58(skac2))))), inference(scs_inference,[],[i_0_378,i_0_379,i_0_380,i_0_381,i_0_391,i_0_393,i_0_395,i_0_376,i_0_377,i_0_382,i_0_383,i_0_384,i_0_385,i_0_386,i_0_387,i_0_388,i_0_389,i_0_392,i_0_397,i_0_313,i_0_322,i_0_323,i_0_324,i_0_325,i_0_326,i_0_454,i_0_456,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_319,i_0_320,i_0_321,i_0_449,i_0_305,i_0_306,i_0_442,i_0_426,i_0_450,i_0_451,i_0_429,i_0_430,i_0_205])).
% 0.54/1.88  cnf(i_0_508, plain, (ssList(sk3)), inference(equality_inference,[],[502])).
% 0.54/1.88  cnf(i_0_509, plain, (nil=sk3), inference(scs_inference,[],[i_0_478,i_0_390])).
% 0.54/1.88  cnf(i_0_510, plain, (~lt(skaf44(X1),skaf44(X1))), inference(scs_inference,[],[i_0_339,i_0_313])).
% 0.54/1.88  cnf(i_0_511, plain, (~ssItem(X1)|~lt(X1,X1)), inference(rename_variables,[],[i_0_313])).
% 0.54/1.88  cnf(i_0_512, plain, (frontsegP(sk3,sk3)), inference(scs_inference,[],[i_0_379,i_0_339,i_0_313,i_0_323])).
% 0.54/1.88  cnf(i_0_513, plain, (~ssList(X1)|frontsegP(X1,X1)), inference(rename_variables,[],[i_0_323])).
% 0.54/1.88  cnf(i_0_514, plain, (rearsegP(sk3,sk3)), inference(scs_inference,[],[i_0_379,i_0_339,i_0_313,i_0_323,i_0_324])).
% 0.54/1.88  cnf(i_0_515, plain, (~ssList(X1)|rearsegP(X1,X1)), inference(rename_variables,[],[i_0_324])).
% 0.54/1.88  cnf(i_0_516, plain, (segmentP(sk3,sk3)), inference(scs_inference,[],[i_0_379,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325])).
% 0.54/1.88  cnf(i_0_517, plain, (~ssList(X1)|segmentP(X1,X1)), inference(rename_variables,[],[i_0_325])).
% 0.54/1.88  cnf(i_0_518, plain, (leq(skaf44(X1),skaf44(X1))), inference(scs_inference,[],[i_0_379,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322])).
% 0.54/1.88  cnf(i_0_519, plain, (~ssItem(X1)|leq(X1,X1)), inference(rename_variables,[],[i_0_322])).
% 0.54/1.88  cnf(i_0_520, plain, (geq(skaf44(X1),skaf44(X1))), inference(scs_inference,[],[i_0_379,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326])).
% 0.54/1.88  cnf(i_0_521, plain, (~ssItem(X1)|geq(X1,X1)), inference(rename_variables,[],[i_0_326])).
% 0.54/1.88  cnf(i_0_522, plain, (sk3=sk1), inference(scs_inference,[],[i_0_394,i_0_379,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397])).
% 0.54/1.88  cnf(i_0_523, plain, (~neq(skaf44(X1),skaf44(X1))), inference(scs_inference,[],[i_0_394,i_0_379,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454])).
% 0.54/1.88  cnf(i_0_524, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_454])).
% 0.54/1.88  cnf(i_0_525, plain, (~neq(sk3,sk3)), inference(scs_inference,[],[i_0_394,i_0_379,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456])).
% 0.54/1.88  cnf(i_0_526, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_456])).
% 0.54/1.88  cnf(i_0_527, plain, (frontsegP(nil,sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_379,i_0_478,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319])).
% 0.54/1.88  cnf(i_0_528, plain, (nil!=X1|frontsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_319])).
% 0.54/1.88  cnf(i_0_529, plain, (rearsegP(nil,sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_379,i_0_478,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320])).
% 0.54/1.88  cnf(i_0_530, plain, (nil!=X1|rearsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_320])).
% 0.54/1.88  cnf(i_0_531, plain, (segmentP(nil,sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_379,i_0_478,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321])).
% 0.54/1.88  cnf(i_0_532, plain, (nil!=X1|segmentP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_321])).
% 0.54/1.88  cnf(i_0_533, plain, (nil!=sk3), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_478,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398])).
% 0.54/1.88  cnf(i_0_534, plain, (duplicatefreeP(sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_478,i_0_479,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409])).
% 0.54/1.88  cnf(i_0_535, plain, (equalelemsP(sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_478,i_0_479,i_0_480,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410])).
% 0.54/1.88  cnf(i_0_536, plain, (~neq(nil,sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423])).
% 0.54/1.88  cnf(i_0_537, plain, (~neq(sk2,sk2)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424])).
% 0.54/1.88  cnf(i_0_538, plain, (cyclefreeP(sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428])).
% 0.54/1.88  cnf(i_0_539, plain, (strictorderP(sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431])).
% 0.54/1.88  cnf(i_0_540, plain, (totalorderP(sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432])).
% 0.54/1.88  cnf(i_0_541, plain, (strictorderedP(sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433])).
% 0.54/1.88  cnf(i_0_542, plain, (totalorderedP(sk4)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434])).
% 0.54/1.88  cnf(i_0_543, plain, (memberP(cons(skaf44(X1),sk4),skaf44(X1))), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_339,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449])).
% 0.54/1.88  cnf(i_0_544, plain, (~ssItem(X1)|~ssItem(X1)|memberP(cons(X1,X2),X1)|~ssList(X2)), inference(rename_variables,[],[i_0_449])).
% 0.54/1.88  cnf(i_0_545, plain, (neq(nil,sk3)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_339,i_0_382,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449,i_0_306])).
% 0.54/1.88  cnf(i_0_546, plain, (X1=X2|~ssList(X2)|~ssList(X1)|neq(X1,X2)), inference(rename_variables,[],[i_0_306])).
% 0.54/1.88  cnf(i_0_547, plain, (frontsegP(cons(skaf44(X1),sk4),cons(skaf44(X1),sk4))), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_466,i_0_339,i_0_382,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449,i_0_306,i_0_442])).
% 0.54/1.88  cnf(i_0_548, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X2),cons(X3,X1))|~frontsegP(X2,X1)), inference(rename_variables,[],[i_0_442])).
% 0.54/1.88  cnf(i_0_549, plain, (duplicatefreeP(sk3)|ssItem(X1)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_466,i_0_339,i_0_382,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449,i_0_306,i_0_442,i_0_338])).
% 0.54/1.88  cnf(i_0_550, plain, (~ssList(X1)|duplicatefreeP(X1)|ssItem(X2)), inference(rename_variables,[],[i_0_338])).
% 0.54/1.88  cnf(i_0_551, plain, (ssItem(X1)|skaf44(X2)!=X1), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_466,i_0_339,i_0_382,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449,i_0_306,i_0_442,i_0_338,i_0_427])).
% 0.54/1.88  cnf(i_0_552, plain, (X1!=skac2|~lt(X1,skac2)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_466,i_0_462,i_0_339,i_0_382,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449,i_0_306,i_0_442,i_0_338,i_0_427,i_0_429])).
% 0.54/1.88  cnf(i_0_553, plain, (X1!=skac2|~lt(skac2,X1)), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_466,i_0_462,i_0_339,i_0_382,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449,i_0_306,i_0_442,i_0_338,i_0_427,i_0_429,i_0_430])).
% 0.54/1.88  cnf(i_0_554, plain, (ssList(X1)|skaf42(X2,X3)!=X1), inference(scs_inference,[],[i_0_378,i_0_394,i_0_391,i_0_379,i_0_393,i_0_395,i_0_478,i_0_479,i_0_480,i_0_481,i_0_483,i_0_484,i_0_485,i_0_486,i_0_487,i_0_466,i_0_462,i_0_307,i_0_339,i_0_382,i_0_313,i_0_323,i_0_324,i_0_325,i_0_322,i_0_326,i_0_397,i_0_454,i_0_456,i_0_319,i_0_320,i_0_321,i_0_398,i_0_409,i_0_410,i_0_423,i_0_424,i_0_428,i_0_431,i_0_432,i_0_433,i_0_434,i_0_449,i_0_306,i_0_442,i_0_338,i_0_427,i_0_429,i_0_430,i_0_426])).
% 0.54/1.88  cnf(i_0_555, plain, (~neq(X1,X2)|~ssItem(X2)|~ssItem(X1)|X1!=X2), inference(rename_variables,[],[i_0_284])).
% 0.54/1.88  cnf(i_0_557, plain, (ssItem(skaf44(X1))), inference(equality_inference,[],[551])).
% 0.54/1.88  cnf(i_0_558, plain, (~lt(skac2,skac2)), inference(equality_inference,[],[552])).
% 0.54/1.88  cnf(i_0_559, plain, (~lt(skac2,skac2)), inference(equality_inference,[],[553])).
% 0.54/1.88  cnf(i_0_560, plain, (ssList(skaf42(X1,X2))), inference(equality_inference,[],[554])).
% 0.54/1.88  cnf(i_0_561,plain, ($false), inference(scs_inference,[],[i_0+509, i_0_533]), ['proof']).
% 0.54/1.88  % SZS output end CNFRefutation
% 0.54/1.88  % Total time : 1.261s
%------------------------------------------------------------------------------