CSE_E---1.7.THM-CRf.s

%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : SWC036+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 : n004.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:17:59 PM UTC 2026

% Result   : Theorem 0.43s 1.61s
% Output   : CNFRefutation 0.85s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11  % Problem    : SWC036+1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.11  % 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.14/0.32  % Computer : n004.cluster.edu
% 0.14/0.32  % Model    : x86_64 x86_64
% 0.14/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32  % Memory   : 8042.1875MB
% 0.14/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32  % CPULimit   : 300
% 0.14/0.32  % WCLimit    : 300
% 0.14/0.32  % DateTime   : Tue May  5 04:17:17 EDT 2026
% 0.14/0.32  % CPUTime    : 
% 0.14/0.33  % start to proof: theBenchmark
% 0.43/1.61  % Version  : CSE_E---1.7
% 0.43/1.61  % Problem  : theBenchmark.p
% 0.43/1.61  % SZS status Theorem for theBenchmark.p
% 0.43/1.61  % SZS output start CNFRefutation
% 0.43/1.61  fof(ax94, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)=>~(gt(X2,X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax94)).
% 0.43/1.61  fof(ax33, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)=>~(lt(X2,X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax33)).
% 0.43/1.61  fof(ax90, axiom, ![X1]:(ssItem(X1)=>~(lt(X1,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax90)).
% 0.43/1.61  fof(ax38, axiom, ![X1]:(ssItem(X1)=>~(memberP(nil,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax38)).
% 0.43/1.61  fof(co1, conjecture, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(nil!=X2|X2!=X4|X1!=X3|nil=X1|(nil!=X3&nil=X4)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.43/1.61  fof(ax8, axiom, ![X1]:(ssList(X1)=>(cyclefreeP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>~((leq(X2,X3)&leq(X3,X2))))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax8)).
% 0.43/1.61  fof(ax10, axiom, ![X1]:(ssList(X1)=>(strictorderP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>(lt(X2,X3)|lt(X3,X2)))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax10)).
% 0.43/1.61  fof(ax9, axiom, ![X1]:(ssList(X1)=>(totalorderP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>(leq(X2,X3)|leq(X3,X2)))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax9)).
% 0.43/1.61  fof(ax12, axiom, ![X1]:(ssList(X1)=>(strictorderedP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>lt(X2,X3))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax12)).
% 0.43/1.61  fof(ax11, axiom, ![X1]:(ssList(X1)=>(totalorderedP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>leq(X2,X3))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax11)).
% 0.43/1.61  fof(ax13, axiom, ![X1]:(ssList(X1)=>(duplicatefreeP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>X2!=X3)))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax13)).
% 0.43/1.61  fof(ax14, axiom, ![X1]:(ssList(X1)=>(equalelemsP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>(app(X4,cons(X2,cons(X3,X5)))=X1=>X2=X3))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax14)).
% 0.43/1.61  fof(ax7, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(segmentP(X1,X2)<=>?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(app(X3,X2),X4)=X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax7)).
% 0.43/1.61  fof(ax3, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>(memberP(X1,X2)<=>?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(X3,cons(X2,X4))=X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax3)).
% 0.43/1.61  fof(ax44, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(frontsegP(cons(X1,X3),cons(X2,X4))<=>(X1=X2&frontsegP(X3,X4))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax44)).
% 0.43/1.61  fof(ax56, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(segmentP(X1,X2)=>segmentP(app(app(X3,X1),X4),X2)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax56)).
% 0.43/1.61  fof(ax36, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(memberP(app(X2,X3),X1)<=>(memberP(X2,X1)|memberP(X3,X1)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax36)).
% 0.43/1.61  fof(ax37, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssList(X3)=>(memberP(cons(X2,X3),X1)<=>(X1=X2|memberP(X3,X1)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax37)).
% 0.43/1.61  fof(ax82, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>app(app(X1,X2),X3)=app(X1,app(X2,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax82)).
% 0.43/1.61  fof(ax27, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssItem(X3)=>cons(X3,app(X2,X1))=app(cons(X3,X2),X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax27)).
% 0.43/1.61  fof(ax70, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssList(X2)=>(strictorderedP(cons(X1,X2))<=>(nil=X2|((nil!=X2&strictorderedP(X2))&lt(X1,hd(X2))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax70)).
% 0.43/1.61  fof(ax67, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssList(X2)=>(totalorderedP(cons(X1,X2))<=>(nil=X2|((nil!=X2&totalorderedP(X2))&leq(X1,hd(X2))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax67)).
% 0.43/1.61  fof(ax50, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(rearsegP(X1,X2)=>rearsegP(app(X3,X1),X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax50)).
% 0.43/1.61  fof(ax43, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(frontsegP(X1,X2)=>frontsegP(app(X1,X3),X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax43)).
% 0.43/1.61  fof(ax95, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((gt(X1,X2)&gt(X2,X3))=>gt(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax95)).
% 0.43/1.61  fof(ax88, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((geq(X1,X2)&geq(X2,X3))=>geq(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax88)).
% 0.43/1.61  fof(ax34, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((lt(X1,X2)&lt(X2,X3))=>lt(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax34)).
% 0.43/1.61  fof(ax91, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((leq(X1,X2)&lt(X2,X3))=>lt(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax91)).
% 0.43/1.61  fof(ax30, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((leq(X1,X2)&leq(X2,X3))=>leq(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax30)).
% 0.43/1.61  fof(ax53, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((segmentP(X1,X2)&segmentP(X2,X3))=>segmentP(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax53)).
% 0.43/1.61  fof(ax47, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((rearsegP(X1,X2)&rearsegP(X2,X3))=>rearsegP(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax47)).
% 0.43/1.61  fof(ax40, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((frontsegP(X1,X2)&frontsegP(X2,X3))=>frontsegP(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax40)).
% 0.43/1.61  fof(ax6, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(rearsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X3,X2)=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax6)).
% 0.43/1.61  fof(ax5, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(frontsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X2,X3)=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax5)).
% 0.43/1.61  fof(ax19, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssItem(X4)=>(cons(X3,X1)=cons(X4,X2)=>(X3=X4&X2=X1)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax19)).
% 0.43/1.61  fof(ax79, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X3,X2)=app(X1,X2)=>X3=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax79)).
% 0.43/1.61  fof(ax80, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X2,X3)=app(X2,X1)=>X3=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax80)).
% 0.43/1.61  fof(ax86, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil!=X1=>tl(app(X1,X2))=app(tl(X1),X2)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax86)).
% 0.43/1.61  fof(ax81, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>cons(X2,X1)=app(cons(X2,nil),X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax81)).
% 0.43/1.61  fof(ax54, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((segmentP(X1,X2)&segmentP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax54)).
% 0.43/1.61  fof(ax48, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((rearsegP(X1,X2)&rearsegP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax48)).
% 0.43/1.61  fof(ax41, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((frontsegP(X1,X2)&frontsegP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax41)).
% 0.43/1.61  fof(ax87, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>((geq(X1,X2)&geq(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax87)).
% 0.43/1.61  fof(ax29, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>((leq(X1,X2)&leq(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax29)).
% 0.43/1.61  fof(ax93, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)<=>(X1!=X2&leq(X1,X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax93)).
% 0.43/1.61  fof(ax92, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(leq(X1,X2)=>(X1=X2|lt(X1,X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax92)).
% 0.43/1.61  fof(ax35, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)<=>lt(X2,X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax35)).
% 0.43/1.61  fof(ax32, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(geq(X1,X2)<=>leq(X2,X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax32)).
% 0.43/1.61  fof(ax85, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil!=X1=>hd(app(X1,X2))=hd(X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax85)).
% 0.43/1.61  fof(ax77, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((((nil!=X2&nil!=X1)&hd(X2)=hd(X1))&tl(X2)=tl(X1))=>X2=X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax77)).
% 0.43/1.61  fof(ax25, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>tl(cons(X2,X1))=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax25)).
% 0.43/1.61  fof(ax23, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>hd(cons(X2,X1))=X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax23)).
% 0.43/1.61  fof(ax26, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>ssList(app(X1,X2)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax26)).
% 0.43/1.61  fof(ax16, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>ssList(cons(X2,X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax16)).
% 0.43/1.61  fof(ax15, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(neq(X1,X2)<=>X1!=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax15)).
% 0.43/1.61  fof(ax1, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(neq(X1,X2)<=>X1!=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax1)).
% 0.43/1.61  fof(ax4, axiom, ![X1]:(ssList(X1)=>(singletonP(X1)<=>?[X2]:(ssItem(X2)&cons(X2,nil)=X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax4)).
% 0.43/1.61  fof(ax83, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil=app(X1,X2)<=>(nil=X2&nil=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax83)).
% 0.43/1.61  fof(ax18, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>cons(X2,X1)!=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax18)).
% 0.43/1.61  fof(ax21, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>nil!=cons(X2,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax21)).
% 0.43/1.61  fof(ax20, axiom, ![X1]:(ssList(X1)=>(nil=X1|?[X2]:(ssList(X2)&?[X3]:(ssItem(X3)&cons(X3,X2)=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax20)).
% 0.43/1.61  fof(ax78, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>cons(hd(X1),tl(X1))=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax78)).
% 0.43/1.61  fof(ax73, axiom, ![X1]:(ssItem(X1)=>equalelemsP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax73)).
% 0.43/1.61  fof(ax71, axiom, ![X1]:(ssItem(X1)=>duplicatefreeP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax71)).
% 0.43/1.61  fof(ax68, axiom, ![X1]:(ssItem(X1)=>strictorderedP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax68)).
% 0.43/1.61  fof(ax65, axiom, ![X1]:(ssItem(X1)=>totalorderedP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax65)).
% 0.43/1.61  fof(ax63, axiom, ![X1]:(ssItem(X1)=>strictorderP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax63)).
% 0.43/1.61  fof(ax61, axiom, ![X1]:(ssItem(X1)=>totalorderP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax61)).
% 0.43/1.61  fof(ax59, axiom, ![X1]:(ssItem(X1)=>cyclefreeP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax59)).
% 0.43/1.61  fof(ax58, axiom, ![X1]:(ssList(X1)=>(segmentP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax58)).
% 0.43/1.61  fof(ax52, axiom, ![X1]:(ssList(X1)=>(rearsegP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax52)).
% 0.43/1.61  fof(ax46, axiom, ![X1]:(ssList(X1)=>(frontsegP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax46)).
% 0.43/1.61  fof(ax89, axiom, ![X1]:(ssItem(X1)=>geq(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax89)).
% 0.43/1.61  fof(ax31, axiom, ![X1]:(ssItem(X1)=>leq(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax31)).
% 0.43/1.61  fof(ax55, axiom, ![X1]:(ssList(X1)=>segmentP(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax55)).
% 0.43/1.61  fof(ax49, axiom, ![X1]:(ssList(X1)=>rearsegP(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax49)).
% 0.43/1.61  fof(ax42, axiom, ![X1]:(ssList(X1)=>frontsegP(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax42)).
% 0.43/1.61  fof(ax28, axiom, ![X1]:(ssList(X1)=>app(nil,X1)=X1), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax28)).
% 0.43/1.61  fof(ax84, axiom, ![X1]:(ssList(X1)=>app(X1,nil)=X1), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax84)).
% 0.43/1.61  fof(ax57, axiom, ![X1]:(ssList(X1)=>segmentP(X1,nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax57)).
% 0.43/1.61  fof(ax51, axiom, ![X1]:(ssList(X1)=>rearsegP(X1,nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax51)).
% 0.43/1.61  fof(ax45, axiom, ![X1]:(ssList(X1)=>frontsegP(X1,nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax45)).
% 0.43/1.61  fof(ax76, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>?[X2]:(ssList(X2)&tl(X1)=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax76)).
% 0.43/1.61  fof(ax24, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>ssList(tl(X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax24)).
% 0.43/1.61  fof(ax75, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>?[X2]:(ssItem(X2)&hd(X1)=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax75)).
% 0.43/1.61  fof(ax22, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>ssItem(hd(X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax22)).
% 0.43/1.61  fof(ax39, axiom, ~(singletonP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax39)).
% 0.43/1.61  fof(ax2, axiom, ?[X1]:(ssItem(X1)&?[X2]:(ssItem(X2)&X1!=X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax2)).
% 0.43/1.61  fof(ax74, axiom, equalelemsP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax74)).
% 0.43/1.61  fof(ax72, axiom, duplicatefreeP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax72)).
% 0.43/1.61  fof(ax69, axiom, strictorderedP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax69)).
% 0.43/1.61  fof(ax66, axiom, totalorderedP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax66)).
% 0.43/1.61  fof(ax64, axiom, strictorderP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax64)).
% 0.43/1.61  fof(ax62, axiom, totalorderP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax62)).
% 0.43/1.61  fof(ax60, axiom, cyclefreeP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax60)).
% 0.43/1.61  fof(ax17, axiom, ssList(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax17)).
% 0.43/1.61  fof(i_0_96, plain, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)=>~gt(X2,X1)))), inference(fof_simplification,[status(thm)],[ax94])).
% 0.43/1.61  fof(i_0_97, plain, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)=>~lt(X2,X1)))), inference(fof_simplification,[status(thm)],[ax33])).
% 0.43/1.61  fof(i_0_98, plain, ![X1]:(ssItem(X1)=>~lt(X1,X1)), inference(fof_simplification,[status(thm)],[ax90])).
% 0.43/1.61  fof(i_0_99, plain, ![X1]:(ssItem(X1)=>~memberP(nil,X1)), inference(fof_simplification,[status(thm)],[ax38])).
% 0.43/1.61  fof(i_0_100, negated_conjecture, ~(![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(nil!=X2|X2!=X4|X1!=X3|nil=X1|(nil!=X3&nil=X4))))))), inference(assume_negation,[status(cth)],[co1])).
% 0.43/1.61  fof(i_0_101, plain, ![X241, X242, X243, X244, X245, X246]:((~cyclefreeP(X241)|(~ssItem(X242)|(~ssItem(X243)|(~ssList(X244)|(~ssList(X245)|(~ssList(X246)|(app(app(X244,cons(X242,X245)),cons(X243,X246))!=X241|(~leq(X242,X243)|~leq(X243,X242))))))))|~ssList(X241))&((ssItem(esk10_1(X241))|cyclefreeP(X241)|~ssList(X241))&((ssItem(esk11_1(X241))|cyclefreeP(X241)|~ssList(X241))&((ssList(esk12_1(X241))|cyclefreeP(X241)|~ssList(X241))&((ssList(esk13_1(X241))|cyclefreeP(X241)|~ssList(X241))&((ssList(esk14_1(X241))|cyclefreeP(X241)|~ssList(X241))&((app(app(esk12_1(X241),cons(esk10_1(X241),esk13_1(X241))),cons(esk11_1(X241),esk14_1(X241)))=X241|cyclefreeP(X241)|~ssList(X241))&((leq(esk10_1(X241),esk11_1(X241))|cyclefreeP(X241)|~ssList(X241))&(leq(esk11_1(X241),esk10_1(X241))|cyclefreeP(X241)|~ssList(X241)))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax8])])])])])).
% 0.43/1.61  fof(i_0_102, plain, ![X263, X264, X265, X266, X267, X268]:((~strictorderP(X263)|(~ssItem(X264)|(~ssItem(X265)|(~ssList(X266)|(~ssList(X267)|(~ssList(X268)|(app(app(X266,cons(X264,X267)),cons(X265,X268))!=X263|(lt(X264,X265)|lt(X265,X264))))))))|~ssList(X263))&((ssItem(esk20_1(X263))|strictorderP(X263)|~ssList(X263))&((ssItem(esk21_1(X263))|strictorderP(X263)|~ssList(X263))&((ssList(esk22_1(X263))|strictorderP(X263)|~ssList(X263))&((ssList(esk23_1(X263))|strictorderP(X263)|~ssList(X263))&((ssList(esk24_1(X263))|strictorderP(X263)|~ssList(X263))&((app(app(esk22_1(X263),cons(esk20_1(X263),esk23_1(X263))),cons(esk21_1(X263),esk24_1(X263)))=X263|strictorderP(X263)|~ssList(X263))&((~lt(esk20_1(X263),esk21_1(X263))|strictorderP(X263)|~ssList(X263))&(~lt(esk21_1(X263),esk20_1(X263))|strictorderP(X263)|~ssList(X263)))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax10])])])])])).
% 0.43/1.61  fof(i_0_103, plain, ![X252, X253, X254, X255, X256, X257]:((~totalorderP(X252)|(~ssItem(X253)|(~ssItem(X254)|(~ssList(X255)|(~ssList(X256)|(~ssList(X257)|(app(app(X255,cons(X253,X256)),cons(X254,X257))!=X252|(leq(X253,X254)|leq(X254,X253))))))))|~ssList(X252))&((ssItem(esk15_1(X252))|totalorderP(X252)|~ssList(X252))&((ssItem(esk16_1(X252))|totalorderP(X252)|~ssList(X252))&((ssList(esk17_1(X252))|totalorderP(X252)|~ssList(X252))&((ssList(esk18_1(X252))|totalorderP(X252)|~ssList(X252))&((ssList(esk19_1(X252))|totalorderP(X252)|~ssList(X252))&((app(app(esk17_1(X252),cons(esk15_1(X252),esk18_1(X252))),cons(esk16_1(X252),esk19_1(X252)))=X252|totalorderP(X252)|~ssList(X252))&((~leq(esk15_1(X252),esk16_1(X252))|totalorderP(X252)|~ssList(X252))&(~leq(esk16_1(X252),esk15_1(X252))|totalorderP(X252)|~ssList(X252)))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax9])])])])])).
% 0.43/1.61  fof(i_0_104, plain, ![X285, X286, X287, X288, X289, X290]:((~strictorderedP(X285)|(~ssItem(X286)|(~ssItem(X287)|(~ssList(X288)|(~ssList(X289)|(~ssList(X290)|(app(app(X288,cons(X286,X289)),cons(X287,X290))!=X285|lt(X286,X287)))))))|~ssList(X285))&((ssItem(esk30_1(X285))|strictorderedP(X285)|~ssList(X285))&((ssItem(esk31_1(X285))|strictorderedP(X285)|~ssList(X285))&((ssList(esk32_1(X285))|strictorderedP(X285)|~ssList(X285))&((ssList(esk33_1(X285))|strictorderedP(X285)|~ssList(X285))&((ssList(esk34_1(X285))|strictorderedP(X285)|~ssList(X285))&((app(app(esk32_1(X285),cons(esk30_1(X285),esk33_1(X285))),cons(esk31_1(X285),esk34_1(X285)))=X285|strictorderedP(X285)|~ssList(X285))&(~lt(esk30_1(X285),esk31_1(X285))|strictorderedP(X285)|~ssList(X285))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax12])])])])])).
% 0.43/1.61  fof(i_0_105, plain, ![X274, X275, X276, X277, X278, X279]:((~totalorderedP(X274)|(~ssItem(X275)|(~ssItem(X276)|(~ssList(X277)|(~ssList(X278)|(~ssList(X279)|(app(app(X277,cons(X275,X278)),cons(X276,X279))!=X274|leq(X275,X276)))))))|~ssList(X274))&((ssItem(esk25_1(X274))|totalorderedP(X274)|~ssList(X274))&((ssItem(esk26_1(X274))|totalorderedP(X274)|~ssList(X274))&((ssList(esk27_1(X274))|totalorderedP(X274)|~ssList(X274))&((ssList(esk28_1(X274))|totalorderedP(X274)|~ssList(X274))&((ssList(esk29_1(X274))|totalorderedP(X274)|~ssList(X274))&((app(app(esk27_1(X274),cons(esk25_1(X274),esk28_1(X274))),cons(esk26_1(X274),esk29_1(X274)))=X274|totalorderedP(X274)|~ssList(X274))&(~leq(esk25_1(X274),esk26_1(X274))|totalorderedP(X274)|~ssList(X274))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax11])])])])])).
% 0.43/1.61  fof(i_0_106, plain, ![X296, X297, X298, X299, X300, X301]:((~duplicatefreeP(X296)|(~ssItem(X297)|(~ssItem(X298)|(~ssList(X299)|(~ssList(X300)|(~ssList(X301)|(app(app(X299,cons(X297,X300)),cons(X298,X301))!=X296|X297!=X298))))))|~ssList(X296))&((ssItem(esk35_1(X296))|duplicatefreeP(X296)|~ssList(X296))&((ssItem(esk36_1(X296))|duplicatefreeP(X296)|~ssList(X296))&((ssList(esk37_1(X296))|duplicatefreeP(X296)|~ssList(X296))&((ssList(esk38_1(X296))|duplicatefreeP(X296)|~ssList(X296))&((ssList(esk39_1(X296))|duplicatefreeP(X296)|~ssList(X296))&((app(app(esk37_1(X296),cons(esk35_1(X296),esk38_1(X296))),cons(esk36_1(X296),esk39_1(X296)))=X296|duplicatefreeP(X296)|~ssList(X296))&(esk35_1(X296)=esk36_1(X296)|duplicatefreeP(X296)|~ssList(X296))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax13])])])])])).
% 0.43/1.61  fof(i_0_107, plain, ![X307, X308, X309, X310, X311]:((~equalelemsP(X307)|(~ssItem(X308)|(~ssItem(X309)|(~ssList(X310)|(~ssList(X311)|(app(X310,cons(X308,cons(X309,X311)))!=X307|X308=X309)))))|~ssList(X307))&((ssItem(esk40_1(X307))|equalelemsP(X307)|~ssList(X307))&((ssItem(esk41_1(X307))|equalelemsP(X307)|~ssList(X307))&((ssList(esk42_1(X307))|equalelemsP(X307)|~ssList(X307))&((ssList(esk43_1(X307))|equalelemsP(X307)|~ssList(X307))&((app(esk42_1(X307),cons(esk40_1(X307),cons(esk41_1(X307),esk43_1(X307))))=X307|equalelemsP(X307)|~ssList(X307))&(esk40_1(X307)!=esk41_1(X307)|equalelemsP(X307)|~ssList(X307)))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax14])])])])])).
% 0.43/1.61  fof(i_0_108, plain, ![X235, X236, X239, X240]:(((ssList(esk8_2(X235,X236))|~segmentP(X235,X236)|~ssList(X236)|~ssList(X235))&((ssList(esk9_2(X235,X236))|~segmentP(X235,X236)|~ssList(X236)|~ssList(X235))&(app(app(esk8_2(X235,X236),X236),esk9_2(X235,X236))=X235|~segmentP(X235,X236)|~ssList(X236)|~ssList(X235))))&(~ssList(X239)|(~ssList(X240)|app(app(X239,X236),X240)!=X235)|segmentP(X235,X236)|~ssList(X236)|~ssList(X235))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax7])])])])])).
% 0.43/1.61  fof(i_0_109, plain, ![X218, X219, X222, X223]:(((ssList(esk3_2(X218,X219))|~memberP(X218,X219)|~ssItem(X219)|~ssList(X218))&((ssList(esk4_2(X218,X219))|~memberP(X218,X219)|~ssItem(X219)|~ssList(X218))&(app(esk3_2(X218,X219),cons(X219,esk4_2(X218,X219)))=X218|~memberP(X218,X219)|~ssItem(X219)|~ssList(X218))))&(~ssList(X222)|(~ssList(X223)|app(X222,cons(X219,X223))!=X218)|memberP(X218,X219)|~ssItem(X219)|~ssList(X218))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])])).
% 0.43/1.61  fof(i_0_110, plain, ![X374, X375, X376, X377]:(((X374=X375|~frontsegP(cons(X374,X376),cons(X375,X377))|~ssList(X377)|~ssList(X376)|~ssItem(X375)|~ssItem(X374))&(frontsegP(X376,X377)|~frontsegP(cons(X374,X376),cons(X375,X377))|~ssList(X377)|~ssList(X376)|~ssItem(X375)|~ssItem(X374)))&(X374!=X375|~frontsegP(X376,X377)|frontsegP(cons(X374,X376),cons(X375,X377))|~ssList(X377)|~ssList(X376)|~ssItem(X375)|~ssItem(X374))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax44])])])])).
% 0.43/1.61  fof(i_0_111, plain, ![X397, X398, X399, X400]:(~ssList(X397)|(~ssList(X398)|(~ssList(X399)|(~ssList(X400)|(~segmentP(X397,X398)|segmentP(app(app(X399,X397),X400),X398)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax56])])])).
% 0.43/1.61  fof(i_0_112, plain, ![X358, X359, X360]:((~memberP(app(X359,X360),X358)|(memberP(X359,X358)|memberP(X360,X358))|~ssList(X360)|~ssList(X359)|~ssItem(X358))&((~memberP(X359,X358)|memberP(app(X359,X360),X358)|~ssList(X360)|~ssList(X359)|~ssItem(X358))&(~memberP(X360,X358)|memberP(app(X359,X360),X358)|~ssList(X360)|~ssList(X359)|~ssItem(X358)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax36])])])])).
% 0.43/1.61  fof(i_0_113, plain, ![X361, X362, X363]:((~memberP(cons(X362,X363),X361)|(X361=X362|memberP(X363,X361))|~ssList(X363)|~ssItem(X362)|~ssItem(X361))&((X361!=X362|memberP(cons(X362,X363),X361)|~ssList(X363)|~ssItem(X362)|~ssItem(X361))&(~memberP(X363,X361)|memberP(cons(X362,X363),X361)|~ssList(X363)|~ssItem(X362)|~ssItem(X361)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax37])])])])).
% 0.43/1.61  fof(i_0_114, plain, ![X429, X430, X431]:(~ssList(X429)|(~ssList(X430)|(~ssList(X431)|app(app(X429,X430),X431)=app(X429,app(X430,X431))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax82])])])).
% 0.43/1.61  fof(i_0_115, plain, ![X339, X340, X341]:(~ssList(X339)|(~ssList(X340)|(~ssItem(X341)|cons(X341,app(X340,X339))=app(cons(X341,X340),X339)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax27])])])).
% 0.43/1.61  fof(i_0_116, plain, ![X410, X411]:((((nil!=X411|nil=X411|~strictorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410))&(strictorderedP(X411)|nil=X411|~strictorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410)))&(lt(X410,hd(X411))|nil=X411|~strictorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410)))&((nil!=X411|strictorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410))&(nil=X411|~strictorderedP(X411)|~lt(X410,hd(X411))|strictorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax70])])])])).
% 0.43/1.61  fof(i_0_117, plain, ![X407, X408]:((((nil!=X408|nil=X408|~totalorderedP(cons(X407,X408))|~ssList(X408)|~ssItem(X407))&(totalorderedP(X408)|nil=X408|~totalorderedP(cons(X407,X408))|~ssList(X408)|~ssItem(X407)))&(leq(X407,hd(X408))|nil=X408|~totalorderedP(cons(X407,X408))|~ssList(X408)|~ssItem(X407)))&((nil!=X408|totalorderedP(cons(X407,X408))|~ssList(X408)|~ssItem(X407))&(nil=X408|~totalorderedP(X408)|~leq(X407,hd(X408))|totalorderedP(cons(X407,X408))|~ssList(X408)|~ssItem(X407)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax67])])])])).
% 0.43/1.61  fof(i_0_118, plain, ![X386, X387, X388]:(~ssList(X386)|(~ssList(X387)|(~ssList(X388)|(~rearsegP(X386,X387)|rearsegP(app(X388,X386),X387))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax50])])])).
% 0.43/1.61  fof(i_0_119, plain, ![X371, X372, X373]:(~ssList(X371)|(~ssList(X372)|(~ssList(X373)|(~frontsegP(X371,X372)|frontsegP(app(X371,X373),X372))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax43])])])).
% 0.43/1.61  fof(i_0_120, plain, ![X455, X456, X457]:(~ssItem(X455)|(~ssItem(X456)|(~ssItem(X457)|(~gt(X455,X456)|~gt(X456,X457)|gt(X455,X457))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax95])])])).
% 0.43/1.61  fof(i_0_121, plain, ![X441, X442, X443]:(~ssItem(X441)|(~ssItem(X442)|(~ssItem(X443)|(~geq(X441,X442)|~geq(X442,X443)|geq(X441,X443))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax88])])])).
% 0.43/1.61  fof(i_0_122, plain, ![X353, X354, X355]:(~ssItem(X353)|(~ssItem(X354)|(~ssItem(X355)|(~lt(X353,X354)|~lt(X354,X355)|lt(X353,X355))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax34])])])).
% 0.43/1.61  fof(i_0_123, plain, ![X446, X447, X448]:(~ssItem(X446)|(~ssItem(X447)|(~ssItem(X448)|(~leq(X446,X447)|~lt(X447,X448)|lt(X446,X448))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax91])])])).
% 0.43/1.61  fof(i_0_124, plain, ![X345, X346, X347]:(~ssItem(X345)|(~ssItem(X346)|(~ssItem(X347)|(~leq(X345,X346)|~leq(X346,X347)|leq(X345,X347))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax30])])])).
% 0.43/1.61  fof(i_0_125, plain, ![X391, X392, X393]:(~ssList(X391)|(~ssList(X392)|(~ssList(X393)|(~segmentP(X391,X392)|~segmentP(X392,X393)|segmentP(X391,X393))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax53])])])).
% 0.43/1.61  fof(i_0_126, plain, ![X380, X381, X382]:(~ssList(X380)|(~ssList(X381)|(~ssList(X382)|(~rearsegP(X380,X381)|~rearsegP(X381,X382)|rearsegP(X380,X382))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax47])])])).
% 0.43/1.61  fof(i_0_127, plain, ![X365, X366, X367]:(~ssList(X365)|(~ssList(X366)|(~ssList(X367)|(~frontsegP(X365,X366)|~frontsegP(X366,X367)|frontsegP(X365,X367))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax40])])])).
% 0.43/1.61  fof(i_0_128, plain, ![X231, X232, X234]:(((ssList(esk7_2(X231,X232))|~rearsegP(X231,X232)|~ssList(X232)|~ssList(X231))&(app(esk7_2(X231,X232),X232)=X231|~rearsegP(X231,X232)|~ssList(X232)|~ssList(X231)))&(~ssList(X234)|app(X234,X232)!=X231|rearsegP(X231,X232)|~ssList(X232)|~ssList(X231))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax6])])])])])).
% 0.43/1.61  fof(i_0_129, plain, ![X227, X228, X230]:(((ssList(esk6_2(X227,X228))|~frontsegP(X227,X228)|~ssList(X228)|~ssList(X227))&(app(X228,esk6_2(X227,X228))=X227|~frontsegP(X227,X228)|~ssList(X228)|~ssList(X227)))&(~ssList(X230)|app(X228,X230)!=X227|frontsegP(X227,X228)|~ssList(X228)|~ssList(X227))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax5])])])])])).
% 0.43/1.61  fof(i_0_130, plain, ![X322, X323, X324, X325]:((X324=X325|cons(X324,X322)!=cons(X325,X323)|~ssItem(X325)|~ssItem(X324)|~ssList(X323)|~ssList(X322))&(X323=X322|cons(X324,X322)!=cons(X325,X323)|~ssItem(X325)|~ssItem(X324)|~ssList(X323)|~ssList(X322))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax19])])])])).
% 0.43/1.61  fof(i_0_131, plain, ![X421, X422, X423]:(~ssList(X421)|(~ssList(X422)|(~ssList(X423)|(app(X423,X422)!=app(X421,X422)|X423=X421)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax79])])])).
% 0.43/1.61  fof(i_0_132, plain, ![X424, X425, X426]:(~ssList(X424)|(~ssList(X425)|(~ssList(X426)|(app(X425,X426)!=app(X425,X424)|X426=X424)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax80])])])).
% 0.43/1.61  fof(i_0_133, plain, ![X437, X438]:(~ssList(X437)|(~ssList(X438)|(nil=X437|tl(app(X437,X438))=app(tl(X437),X438)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax86])])])).
% 0.43/1.61  fof(i_0_134, plain, ![X427, X428]:(~ssList(X427)|(~ssItem(X428)|cons(X428,X427)=app(cons(X428,nil),X427))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax81])])])).
% 0.43/1.61  fof(i_0_135, plain, ![X394, X395]:(~ssList(X394)|(~ssList(X395)|(~segmentP(X394,X395)|~segmentP(X395,X394)|X394=X395))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax54])])])).
% 0.43/1.61  fof(i_0_136, plain, ![X383, X384]:(~ssList(X383)|(~ssList(X384)|(~rearsegP(X383,X384)|~rearsegP(X384,X383)|X383=X384))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax48])])])).
% 0.43/1.61  fof(i_0_137, plain, ![X368, X369]:(~ssList(X368)|(~ssList(X369)|(~frontsegP(X368,X369)|~frontsegP(X369,X368)|X368=X369))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax41])])])).
% 0.43/1.61  fof(i_0_138, plain, ![X439, X440]:(~ssItem(X439)|(~ssItem(X440)|(~geq(X439,X440)|~geq(X440,X439)|X439=X440))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax87])])])).
% 0.43/1.61  fof(i_0_139, plain, ![X343, X344]:(~ssItem(X343)|(~ssItem(X344)|(~leq(X343,X344)|~leq(X344,X343)|X343=X344))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax29])])])).
% 0.43/1.61  fof(i_0_140, plain, ![X453, X454]:(~ssItem(X453)|(~ssItem(X454)|(~gt(X453,X454)|~gt(X454,X453)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_96])])])).
% 0.43/1.61  fof(i_0_141, plain, ![X351, X352]:(~ssItem(X351)|(~ssItem(X352)|(~lt(X351,X352)|~lt(X352,X351)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_97])])])).
% 0.43/1.61  fof(i_0_142, plain, ![X451, X452]:(((X451!=X452|~lt(X451,X452)|~ssItem(X452)|~ssItem(X451))&(leq(X451,X452)|~lt(X451,X452)|~ssItem(X452)|~ssItem(X451)))&(X451=X452|~leq(X451,X452)|lt(X451,X452)|~ssItem(X452)|~ssItem(X451))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax93])])])])).
% 0.43/1.61  fof(i_0_143, plain, ![X449, X450]:(~ssItem(X449)|(~ssItem(X450)|(~leq(X449,X450)|(X449=X450|lt(X449,X450))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax92])])])).
% 0.43/1.61  fof(i_0_144, plain, ![X356, X357]:((~gt(X356,X357)|lt(X357,X356)|~ssItem(X357)|~ssItem(X356))&(~lt(X357,X356)|gt(X356,X357)|~ssItem(X357)|~ssItem(X356))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax35])])])])).
% 0.43/1.61  fof(i_0_145, plain, ![X349, X350]:((~geq(X349,X350)|leq(X350,X349)|~ssItem(X350)|~ssItem(X349))&(~leq(X350,X349)|geq(X349,X350)|~ssItem(X350)|~ssItem(X349))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax32])])])])).
% 0.43/1.61  fof(i_0_146, plain, ![X435, X436]:(~ssList(X435)|(~ssList(X436)|(nil=X435|hd(app(X435,X436))=hd(X435)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax85])])])).
% 0.43/1.61  fof(i_0_147, plain, ![X418, X419]:(~ssList(X418)|(~ssList(X419)|(nil=X419|nil=X418|hd(X419)!=hd(X418)|tl(X419)!=tl(X418)|X419=X418))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax77])])])).
% 0.43/1.61  fof(i_0_148, plain, ![X335, X336]:(~ssList(X335)|(~ssItem(X336)|tl(cons(X336,X335))=X335)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax25])])])).
% 0.43/1.61  fof(i_0_149, plain, ![X332, X333]:(~ssList(X332)|(~ssItem(X333)|hd(cons(X333,X332))=X333)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax23])])])).
% 0.43/1.61  fof(i_0_150, plain, ![X337, X338]:(~ssList(X337)|(~ssList(X338)|ssList(app(X337,X338)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax26])])])).
% 0.43/1.61  fof(i_0_151, plain, ![X318, X319]:(~ssList(X318)|(~ssItem(X319)|ssList(cons(X319,X318)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax16])])])).
% 0.43/1.61  fof(i_0_152, plain, ![X316, X317]:((~neq(X316,X317)|X316!=X317|~ssList(X317)|~ssList(X316))&(X316=X317|neq(X316,X317)|~ssList(X317)|~ssList(X316))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax15])])])])).
% 0.43/1.61  fof(i_0_153, plain, ![X214, X215]:((~neq(X214,X215)|X214!=X215|~ssItem(X215)|~ssItem(X214))&(X214=X215|neq(X214,X215)|~ssItem(X215)|~ssItem(X214))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax1])])])])).
% 0.43/1.61  fof(i_0_154, plain, ![X224, X226]:(((ssItem(esk5_1(X224))|~singletonP(X224)|~ssList(X224))&(cons(esk5_1(X224),nil)=X224|~singletonP(X224)|~ssList(X224)))&(~ssItem(X226)|cons(X226,nil)!=X224|singletonP(X224)|~ssList(X224))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax4])])])])])).
% 0.43/1.61  fof(i_0_155, plain, ![X432, X433]:(((nil=X433|nil!=app(X432,X433)|~ssList(X433)|~ssList(X432))&(nil=X432|nil!=app(X432,X433)|~ssList(X433)|~ssList(X432)))&(nil!=X433|nil!=X432|nil=app(X432,X433)|~ssList(X433)|~ssList(X432))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax83])])])])).
% 0.43/1.61  fof(i_0_156, plain, ![X320, X321]:(~ssList(X320)|(~ssItem(X321)|cons(X321,X320)!=X320)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax18])])])).
% 0.43/1.61  fof(i_0_157, plain, ![X329, X330]:(~ssList(X329)|(~ssItem(X330)|nil!=cons(X330,X329))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax21])])])).
% 0.43/1.61  fof(i_0_158, plain, ![X326]:((ssList(esk44_1(X326))|nil=X326|~ssList(X326))&((ssItem(esk45_1(X326))|nil=X326|~ssList(X326))&(cons(esk45_1(X326),esk44_1(X326))=X326|nil=X326|~ssList(X326)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax20])])])])).
% 0.43/1.61  fof(i_0_159, plain, ![X420]:(~ssList(X420)|(nil=X420|cons(hd(X420),tl(X420))=X420)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax78])])).
% 0.43/1.61  fof(i_0_160, plain, ![X413]:(~ssItem(X413)|equalelemsP(cons(X413,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax73])])).
% 0.43/1.61  fof(i_0_161, plain, ![X412]:(~ssItem(X412)|duplicatefreeP(cons(X412,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax71])])).
% 0.43/1.61  fof(i_0_162, plain, ![X409]:(~ssItem(X409)|strictorderedP(cons(X409,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax68])])).
% 0.43/1.61  fof(i_0_163, plain, ![X406]:(~ssItem(X406)|totalorderedP(cons(X406,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax65])])).
% 0.43/1.61  fof(i_0_164, plain, ![X405]:(~ssItem(X405)|strictorderP(cons(X405,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax63])])).
% 0.43/1.61  fof(i_0_165, plain, ![X404]:(~ssItem(X404)|totalorderP(cons(X404,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax61])])).
% 0.43/1.61  fof(i_0_166, plain, ![X403]:(~ssItem(X403)|cyclefreeP(cons(X403,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax59])])).
% 0.43/1.61  fof(i_0_167, plain, ![X445]:(~ssItem(X445)|~lt(X445,X445)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_98])])).
% 0.43/1.61  fof(i_0_168, plain, ![X402]:((~segmentP(nil,X402)|nil=X402|~ssList(X402))&(nil!=X402|segmentP(nil,X402)|~ssList(X402))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax58])])])).
% 0.43/1.61  fof(i_0_169, plain, ![X390]:((~rearsegP(nil,X390)|nil=X390|~ssList(X390))&(nil!=X390|rearsegP(nil,X390)|~ssList(X390))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax52])])])).
% 0.43/1.61  fof(i_0_170, plain, ![X379]:((~frontsegP(nil,X379)|nil=X379|~ssList(X379))&(nil!=X379|frontsegP(nil,X379)|~ssList(X379))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax46])])])).
% 0.43/1.61  fof(i_0_171, plain, ![X364]:(~ssItem(X364)|~memberP(nil,X364)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_99])])).
% 0.43/1.61  fof(i_0_172, plain, ![X444]:(~ssItem(X444)|geq(X444,X444)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax89])])).
% 0.43/1.61  fof(i_0_173, plain, ![X348]:(~ssItem(X348)|leq(X348,X348)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax31])])).
% 0.43/1.61  fof(i_0_174, plain, ![X396]:(~ssList(X396)|segmentP(X396,X396)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax55])])).
% 0.43/1.61  fof(i_0_175, plain, ![X385]:(~ssList(X385)|rearsegP(X385,X385)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax49])])).
% 0.43/1.61  fof(i_0_176, plain, ![X370]:(~ssList(X370)|frontsegP(X370,X370)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax42])])).
% 0.43/1.61  fof(i_0_177, plain, ![X342]:(~ssList(X342)|app(nil,X342)=X342), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax28])])).
% 0.43/1.61  fof(i_0_178, plain, ![X434]:(~ssList(X434)|app(X434,nil)=X434), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax84])])).
% 0.43/1.61  fof(i_0_179, plain, ![X401]:(~ssList(X401)|segmentP(X401,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax57])])).
% 0.43/1.61  fof(i_0_180, plain, ![X389]:(~ssList(X389)|rearsegP(X389,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax51])])).
% 0.43/1.61  fof(i_0_181, plain, ![X378]:(~ssList(X378)|frontsegP(X378,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax45])])).
% 0.43/1.61  fof(i_0_182, plain, ![X416]:((ssList(esk47_1(X416))|nil=X416|~ssList(X416))&(tl(X416)=esk47_1(X416)|nil=X416|~ssList(X416))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax76])])])])).
% 0.43/1.61  fof(i_0_183, plain, ![X334]:(~ssList(X334)|(nil=X334|ssList(tl(X334)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax24])])).
% 0.43/1.61  fof(i_0_184, plain, ![X414]:((ssItem(esk46_1(X414))|nil=X414|~ssList(X414))&(hd(X414)=esk46_1(X414)|nil=X414|~ssList(X414))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax75])])])])).
% 0.43/1.61  fof(i_0_185, plain, ![X331]:(~ssList(X331)|(nil=X331|ssItem(hd(X331)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax22])])).
% 0.43/1.61  fof(i_0_186, plain, ~singletonP(nil), inference(fof_simplification,[status(thm)],[ax39])).
% 0.43/1.61  fof(i_0_187, negated_conjecture, (ssList(esk48_0)&(ssList(esk49_0)&(ssList(esk50_0)&(ssList(esk51_0)&((((nil=esk49_0&esk49_0=esk51_0)&esk48_0=esk50_0)&nil!=esk48_0)&(nil=esk50_0|nil!=esk51_0)))))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_100])])])).
% 0.43/1.61  fof(i_0_188, plain, (ssItem(esk1_0)&(ssItem(esk2_0)&esk1_0!=esk2_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[ax2])])).
% 0.43/1.61  cnf(i_0_189, plain, (~cyclefreeP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~leq(X2,X3)|~leq(X3,X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_190, plain, (lt(X2,X3)|lt(X3,X2)|~strictorderP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_191, plain, (leq(X2,X3)|leq(X3,X2)|~totalorderP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_192, plain, (lt(X2,X3)|~strictorderedP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_193, plain, (leq(X2,X3)|~totalorderedP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_194, plain, (~duplicatefreeP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|X2!=X3|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_195, plain, (app(app(esk37_1(X1),cons(esk35_1(X1),esk38_1(X1))),cons(esk36_1(X1),esk39_1(X1)))=X1|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_196, plain, (app(app(esk32_1(X1),cons(esk30_1(X1),esk33_1(X1))),cons(esk31_1(X1),esk34_1(X1)))=X1|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_197, plain, (app(app(esk27_1(X1),cons(esk25_1(X1),esk28_1(X1))),cons(esk26_1(X1),esk29_1(X1)))=X1|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_198, plain, (app(app(esk22_1(X1),cons(esk20_1(X1),esk23_1(X1))),cons(esk21_1(X1),esk24_1(X1)))=X1|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_199, plain, (app(app(esk17_1(X1),cons(esk15_1(X1),esk18_1(X1))),cons(esk16_1(X1),esk19_1(X1)))=X1|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_200, plain, (app(app(esk12_1(X1),cons(esk10_1(X1),esk13_1(X1))),cons(esk11_1(X1),esk14_1(X1)))=X1|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_201, plain, (X2=X3|~equalelemsP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|app(X4,cons(X2,cons(X3,X5)))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.43/1.61  cnf(i_0_202, plain, (app(esk42_1(X1),cons(esk40_1(X1),cons(esk41_1(X1),esk43_1(X1))))=X1|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.43/1.61  cnf(i_0_203, plain, (app(app(esk8_2(X1,X2),X2),esk9_2(X1,X2))=X1|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.43/1.61  cnf(i_0_204, plain, (app(esk3_2(X1,X2),cons(X2,esk4_2(X1,X2)))=X1|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.43/1.61  cnf(i_0_205, plain, (frontsegP(X1,X2)|~frontsegP(cons(X3,X1),cons(X4,X2))|~ssList(X2)|~ssList(X1)|~ssItem(X4)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 0.43/1.61  cnf(i_0_206, plain, (segmentP(app(app(X3,X1),X4),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~segmentP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.43/1.61  cnf(i_0_207, plain, (X1=X2|~frontsegP(cons(X1,X3),cons(X2,X4))|~ssList(X4)|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 0.43/1.61  cnf(i_0_208, plain, (frontsegP(cons(X1,X3),cons(X2,X4))|X1!=X2|~frontsegP(X3,X4)|~ssList(X4)|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 0.43/1.61  cnf(i_0_209, plain, (memberP(X1,X3)|memberP(X2,X3)|~memberP(app(X1,X2),X3)|~ssList(X2)|~ssList(X1)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.43/1.61  cnf(i_0_210, plain, (segmentP(X4,X3)|~ssList(X1)|~ssList(X2)|app(app(X1,X3),X2)!=X4|~ssList(X3)|~ssList(X4)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.43/1.61  cnf(i_0_211, plain, (memberP(X4,X3)|~ssList(X1)|~ssList(X2)|app(X1,cons(X3,X2))!=X4|~ssItem(X3)|~ssList(X4)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.43/1.61  cnf(i_0_212, plain, (X3=X1|memberP(X2,X3)|~memberP(cons(X1,X2),X3)|~ssList(X2)|~ssItem(X1)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.43/1.61  cnf(i_0_213, plain, (app(app(X1,X2),X3)=app(X1,app(X2,X3))|~ssList(X1)|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.43/1.61  cnf(i_0_214, plain, (cons(X3,app(X2,X1))=app(cons(X3,X2),X1)|~ssList(X1)|~ssList(X2)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.43/1.61  cnf(i_0_215, plain, (nil=X1|strictorderedP(cons(X2,X1))|~strictorderedP(X1)|~lt(X2,hd(X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.43/1.61  cnf(i_0_216, plain, (nil=X1|totalorderedP(cons(X2,X1))|~totalorderedP(X1)|~leq(X2,hd(X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.43/1.61  cnf(i_0_217, plain, (rearsegP(app(X3,X1),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~rearsegP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.43/1.61  cnf(i_0_218, plain, (frontsegP(app(X1,X3),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~frontsegP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 0.43/1.61  cnf(i_0_219, plain, (memberP(app(X1,X3),X2)|~memberP(X1,X2)|~ssList(X3)|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.43/1.61  cnf(i_0_220, plain, (memberP(app(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssList(X3)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.43/1.61  cnf(i_0_221, plain, (memberP(cons(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.43/1.61  cnf(i_0_222, plain, (lt(X1,hd(X2))|nil=X2|~strictorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.43/1.61  cnf(i_0_223, plain, (leq(X1,hd(X2))|nil=X2|~totalorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.43/1.61  cnf(i_0_224, plain, (gt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~gt(X1,X2)|~gt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.43/1.61  cnf(i_0_225, plain, (geq(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~geq(X1,X2)|~geq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 0.43/1.61  cnf(i_0_226, plain, (lt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~lt(X1,X2)|~lt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.43/1.61  cnf(i_0_227, plain, (lt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~leq(X1,X2)|~lt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.43/1.61  cnf(i_0_228, plain, (leq(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_124]), ['final']).
% 0.43/1.61  cnf(i_0_229, plain, (segmentP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~segmentP(X1,X2)|~segmentP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_125]), ['final']).
% 0.43/1.61  cnf(i_0_230, plain, (rearsegP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~rearsegP(X1,X2)|~rearsegP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_126]), ['final']).
% 0.43/1.61  cnf(i_0_231, plain, (frontsegP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~frontsegP(X1,X2)|~frontsegP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_127]), ['final']).
% 0.43/1.61  cnf(i_0_232, plain, (app(esk7_2(X1,X2),X2)=X1|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.43/1.61  cnf(i_0_233, plain, (app(X1,esk6_2(X2,X1))=X2|~frontsegP(X2,X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 0.43/1.61  cnf(i_0_234, plain, (X1=X2|cons(X1,X3)!=cons(X2,X4)|~ssItem(X2)|~ssItem(X1)|~ssList(X4)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 0.43/1.61  cnf(i_0_235, plain, (X1=X2|cons(X3,X2)!=cons(X4,X1)|~ssItem(X4)|~ssItem(X3)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 0.43/1.61  cnf(i_0_236, plain, (strictorderedP(X1)|nil=X1|~strictorderedP(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.43/1.61  cnf(i_0_237, plain, (totalorderedP(X1)|nil=X1|~totalorderedP(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.43/1.61  cnf(i_0_238, plain, (X3=X1|~ssList(X1)|~ssList(X2)|~ssList(X3)|app(X3,X2)!=app(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_131]), ['final']).
% 0.43/1.61  cnf(i_0_239, plain, (X3=X1|~ssList(X1)|~ssList(X2)|~ssList(X3)|app(X2,X3)!=app(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_132]), ['final']).
% 0.43/1.61  cnf(i_0_240, plain, (ssList(esk9_2(X1,X2))|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.43/1.61  cnf(i_0_241, plain, (ssList(esk8_2(X1,X2))|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.43/1.61  cnf(i_0_242, plain, (ssList(esk7_2(X1,X2))|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.43/1.61  cnf(i_0_243, plain, (ssList(esk6_2(X1,X2))|~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 0.43/1.61  cnf(i_0_244, plain, (ssList(esk4_2(X1,X2))|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.43/1.61  cnf(i_0_245, plain, (ssList(esk3_2(X1,X2))|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.43/1.61  cnf(i_0_246, plain, (nil=X1|tl(app(X1,X2))=app(tl(X1),X2)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_133]), ['final']).
% 0.43/1.61  cnf(i_0_247, plain, (memberP(cons(X2,X3),X1)|X1!=X2|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.43/1.61  cnf(i_0_248, plain, (cons(X2,X1)=app(cons(X2,nil),X1)|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_134]), ['final']).
% 0.43/1.61  cnf(i_0_249, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~segmentP(X1,X2)|~segmentP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_135]), ['final']).
% 0.43/1.61  cnf(i_0_250, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)|~rearsegP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_136]), ['final']).
% 0.43/1.61  cnf(i_0_251, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)|~frontsegP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_137]), ['final']).
% 0.43/1.61  cnf(i_0_252, plain, (X1=X2|~ssItem(X1)|~ssItem(X2)|~geq(X1,X2)|~geq(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_138]), ['final']).
% 0.43/1.61  cnf(i_0_253, plain, (X1=X2|~ssItem(X1)|~ssItem(X2)|~leq(X1,X2)|~leq(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_139]), ['final']).
% 0.43/1.61  cnf(i_0_254, plain, (rearsegP(X3,X2)|~ssList(X1)|app(X1,X2)!=X3|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.43/1.61  cnf(i_0_255, plain, (frontsegP(X3,X2)|~ssList(X1)|app(X2,X1)!=X3|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 0.43/1.61  cnf(i_0_256, plain, (~ssItem(X1)|~ssItem(X2)|~gt(X1,X2)|~gt(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_140]), ['final']).
% 0.43/1.61  cnf(i_0_257, plain, (~ssItem(X1)|~ssItem(X2)|~lt(X1,X2)|~lt(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.43/1.61  cnf(i_0_258, plain, (X1=X2|lt(X1,X2)|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.43/1.61  cnf(i_0_259, plain, (X1=X2|lt(X1,X2)|~ssItem(X1)|~ssItem(X2)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_143]), ['final']).
% 0.43/1.61  cnf(i_0_260, plain, (strictorderedP(X1)|~lt(esk30_1(X1),esk31_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_261, plain, (totalorderedP(X1)|~leq(esk25_1(X1),esk26_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_262, plain, (strictorderP(X1)|~lt(esk21_1(X1),esk20_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_263, plain, (strictorderP(X1)|~lt(esk20_1(X1),esk21_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_264, plain, (totalorderP(X1)|~leq(esk16_1(X1),esk15_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_265, plain, (totalorderP(X1)|~leq(esk15_1(X1),esk16_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_266, plain, (gt(X2,X1)|~lt(X1,X2)|~ssItem(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_144]), ['final']).
% 0.43/1.61  cnf(i_0_267, plain, (geq(X2,X1)|~leq(X1,X2)|~ssItem(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_145]), ['final']).
% 0.43/1.61  cnf(i_0_268, plain, (lt(X2,X1)|~gt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_144]), ['final']).
% 0.43/1.61  cnf(i_0_269, plain, (leq(X1,X2)|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.43/1.61  cnf(i_0_270, plain, (leq(X2,X1)|~geq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_145]), ['final']).
% 0.43/1.61  cnf(i_0_271, plain, (nil=X1|hd(app(X1,X2))=hd(X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.43/1.61  cnf(i_0_272, plain, (strictorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.43/1.61  cnf(i_0_273, plain, (totalorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.43/1.61  cnf(i_0_274, plain, (nil=X2|nil=X1|X2=X1|~ssList(X1)|~ssList(X2)|hd(X2)!=hd(X1)|tl(X2)!=tl(X1)), inference(split_conjunct,[status(thm)],[i_0_147]), ['final']).
% 0.43/1.61  cnf(i_0_275, plain, (tl(cons(X2,X1))=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_148]), ['final']).
% 0.43/1.61  cnf(i_0_276, plain, (hd(cons(X2,X1))=X2|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_149]), ['final']).
% 0.43/1.61  cnf(i_0_277, plain, (ssList(app(X1,X2))|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_150]), ['final']).
% 0.43/1.61  cnf(i_0_278, plain, (ssList(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_151]), ['final']).
% 0.43/1.61  cnf(i_0_279, plain, (~neq(X1,X2)|X1!=X2|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_152]), ['final']).
% 0.43/1.61  cnf(i_0_280, plain, (X1!=X2|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.43/1.61  cnf(i_0_281, plain, (~neq(X1,X2)|X1!=X2|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 0.43/1.61  cnf(i_0_282, plain, (singletonP(X2)|~ssItem(X1)|cons(X1,nil)!=X2|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 0.43/1.61  cnf(i_0_283, plain, (nil=X1|nil!=app(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 0.43/1.61  cnf(i_0_284, plain, (nil=X1|nil!=app(X2,X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 0.43/1.61  cnf(i_0_285, plain, (leq(esk11_1(X1),esk10_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_286, plain, (leq(esk10_1(X1),esk11_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_287, plain, (~ssList(X1)|~ssItem(X2)|cons(X2,X1)!=X1), inference(split_conjunct,[status(thm)],[i_0_156]), ['final']).
% 0.43/1.61  cnf(i_0_288, plain, (~ssList(X1)|~ssItem(X2)|nil!=cons(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_157]), ['final']).
% 0.43/1.61  cnf(i_0_289, plain, (cons(esk45_1(X1),esk44_1(X1))=X1|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 0.43/1.61  cnf(i_0_290, plain, (nil=X1|cons(hd(X1),tl(X1))=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 0.43/1.61  cnf(i_0_291, plain, (equalelemsP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_160]), ['final']).
% 0.43/1.61  cnf(i_0_292, plain, (duplicatefreeP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_161]), ['final']).
% 0.43/1.61  cnf(i_0_293, plain, (strictorderedP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_162]), ['final']).
% 0.43/1.61  cnf(i_0_294, plain, (totalorderedP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_163]), ['final']).
% 0.43/1.61  cnf(i_0_295, plain, (strictorderP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_164]), ['final']).
% 0.43/1.61  cnf(i_0_296, plain, (totalorderP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_165]), ['final']).
% 0.43/1.61  cnf(i_0_297, plain, (cyclefreeP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_166]), ['final']).
% 0.43/1.61  cnf(i_0_298, plain, (cons(esk5_1(X1),nil)=X1|~singletonP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 0.43/1.61  cnf(i_0_299, plain, (nil=app(X2,X1)|nil!=X1|nil!=X2|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 0.43/1.61  cnf(i_0_300, plain, (X1=X2|neq(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_152]), ['final']).
% 0.43/1.61  cnf(i_0_301, plain, (X1=X2|neq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 0.43/1.61  cnf(i_0_302, plain, (~ssItem(X1)|~lt(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_167]), ['final']).
% 0.43/1.61  cnf(i_0_303, plain, (nil=X1|~segmentP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_168]), ['final']).
% 0.43/1.61  cnf(i_0_304, plain, (nil=X1|~rearsegP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 0.43/1.61  cnf(i_0_305, plain, (nil=X1|~frontsegP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 0.43/1.61  cnf(i_0_306, plain, (~ssItem(X1)|~memberP(nil,X1)), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.43/1.61  cnf(i_0_307, plain, (ssItem(esk5_1(X1))|~singletonP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 0.43/1.61  cnf(i_0_308, plain, (equalelemsP(X1)|esk40_1(X1)!=esk41_1(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.43/1.61  cnf(i_0_309, plain, (segmentP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_168]), ['final']).
% 0.43/1.61  cnf(i_0_310, plain, (rearsegP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 0.43/1.61  cnf(i_0_311, plain, (frontsegP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 0.43/1.61  cnf(i_0_312, plain, (ssList(esk43_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.43/1.61  cnf(i_0_313, plain, (ssList(esk42_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.43/1.61  cnf(i_0_314, plain, (ssItem(esk41_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.43/1.61  cnf(i_0_315, plain, (ssItem(esk40_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.43/1.61  cnf(i_0_316, plain, (ssList(esk39_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_317, plain, (ssList(esk38_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_318, plain, (ssList(esk37_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_319, plain, (ssItem(esk36_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_320, plain, (ssItem(esk35_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_321, plain, (ssList(esk34_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_322, plain, (ssList(esk33_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_323, plain, (ssList(esk32_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_324, plain, (ssItem(esk31_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_325, plain, (ssItem(esk30_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.43/1.61  cnf(i_0_326, plain, (ssList(esk29_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_327, plain, (ssList(esk28_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_328, plain, (ssList(esk27_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_329, plain, (ssItem(esk26_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_330, plain, (ssItem(esk25_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.43/1.61  cnf(i_0_331, plain, (ssList(esk24_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_332, plain, (ssList(esk23_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_333, plain, (ssList(esk22_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_334, plain, (ssItem(esk21_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_335, plain, (ssItem(esk20_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.43/1.61  cnf(i_0_336, plain, (ssList(esk19_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_337, plain, (ssList(esk18_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_338, plain, (ssList(esk17_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_339, plain, (ssItem(esk16_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_340, plain, (ssItem(esk15_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.43/1.61  cnf(i_0_341, plain, (ssList(esk14_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_342, plain, (ssList(esk13_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_343, plain, (ssList(esk12_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_344, plain, (ssItem(esk11_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_345, plain, (ssItem(esk10_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.43/1.61  cnf(i_0_346, plain, (geq(X1,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_172]), ['final']).
% 0.43/1.61  cnf(i_0_347, plain, (leq(X1,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 0.43/1.61  cnf(i_0_348, plain, (segmentP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_174]), ['final']).
% 0.43/1.61  cnf(i_0_349, plain, (rearsegP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_175]), ['final']).
% 0.43/1.61  cnf(i_0_350, plain, (frontsegP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_176]), ['final']).
% 0.43/1.61  cnf(i_0_351, plain, (app(nil,X1)=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_177]), ['final']).
% 0.43/1.61  cnf(i_0_352, plain, (app(X1,nil)=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_178]), ['final']).
% 0.43/1.61  cnf(i_0_353, plain, (esk35_1(X1)=esk36_1(X1)|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.43/1.61  cnf(i_0_354, plain, (segmentP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_179]), ['final']).
% 0.43/1.61  cnf(i_0_355, plain, (rearsegP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_180]), ['final']).
% 0.43/1.61  cnf(i_0_356, plain, (frontsegP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.43/1.61  cnf(i_0_357, plain, (ssList(esk47_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_182]), ['final']).
% 0.43/1.61  cnf(i_0_358, plain, (ssList(esk44_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 0.43/1.61  cnf(i_0_359, plain, (nil=X1|ssList(tl(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_183]), ['final']).
% 0.43/1.61  cnf(i_0_360, plain, (ssItem(esk46_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_184]), ['final']).
% 0.43/1.61  cnf(i_0_361, plain, (ssItem(esk45_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 0.43/1.61  cnf(i_0_362, plain, (nil=X1|ssItem(hd(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_185]), ['final']).
% 0.43/1.61  cnf(i_0_363, plain, (tl(X1)=esk47_1(X1)|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_182]), ['final']).
% 0.43/1.61  cnf(i_0_364, plain, (hd(X1)=esk46_1(X1)|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_184]), ['final']).
% 0.43/1.61  cnf(i_0_365, plain, (~singletonP(nil)), inference(split_conjunct,[status(thm)],[i_0_186]), ['final']).
% 0.43/1.61  cnf(i_0_366, plain, (equalelemsP(nil)), inference(split_conjunct,[status(thm)],[ax74]), ['final']).
% 0.43/1.61  cnf(i_0_367, plain, (duplicatefreeP(nil)), inference(split_conjunct,[status(thm)],[ax72]), ['final']).
% 0.43/1.61  cnf(i_0_368, plain, (strictorderedP(nil)), inference(split_conjunct,[status(thm)],[ax69]), ['final']).
% 0.43/1.61  cnf(i_0_369, plain, (totalorderedP(nil)), inference(split_conjunct,[status(thm)],[ax66]), ['final']).
% 0.43/1.61  cnf(i_0_370, plain, (strictorderP(nil)), inference(split_conjunct,[status(thm)],[ax64]), ['final']).
% 0.43/1.61  cnf(i_0_371, plain, (totalorderP(nil)), inference(split_conjunct,[status(thm)],[ax62]), ['final']).
% 0.43/1.61  cnf(i_0_372, plain, (cyclefreeP(nil)), inference(split_conjunct,[status(thm)],[ax60]), ['final']).
% 0.43/1.61  cnf(i_0_373, negated_conjecture, (ssList(esk51_0)), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_374, negated_conjecture, (ssList(esk50_0)), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_375, negated_conjecture, (ssList(esk49_0)), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_376, negated_conjecture, (ssList(esk48_0)), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_377, plain, (ssList(nil)), inference(split_conjunct,[status(thm)],[ax17]), ['final']).
% 0.43/1.61  cnf(i_0_378, plain, (ssItem(esk2_0)), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 0.43/1.61  cnf(i_0_379, plain, (ssItem(esk1_0)), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 0.43/1.61  cnf(i_0_380, negated_conjecture, (nil=esk50_0|nil!=esk51_0), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_381, negated_conjecture, (nil!=esk48_0), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_382, plain, (esk1_0!=esk2_0), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 0.43/1.61  cnf(i_0_383, negated_conjecture, (esk49_0=esk51_0), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_384, negated_conjecture, (esk48_0=esk50_0), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_385, negated_conjecture, (nil=esk49_0), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.43/1.61  cnf(i_0_386, axiom, (X1=X1)).
% 0.43/1.61  cnf(i_0_387, axiom, (X1=X2|X2!=X1)).
% 0.43/1.61  cnf(i_0_388, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.43/1.61  cnf(i_0_389, axiom, (X1!=X2|app(X1,X3)=app(X2,X3))).
% 0.43/1.61  cnf(i_0_390, axiom, (X1!=X2|app(X3,X1)=app(X3,X2))).
% 0.43/1.61  cnf(i_0_391, axiom, (X1!=X2|cons(X1,X3)=cons(X2,X3))).
% 0.43/1.61  cnf(i_0_392, axiom, (X1!=X2|cons(X3,X1)=cons(X3,X2))).
% 0.43/1.61  cnf(i_0_393, axiom, (X1!=X2|esk40_1(X1)=esk40_1(X2))).
% 0.43/1.61  cnf(i_0_394, axiom, (X1!=X2|esk41_1(X1)=esk41_1(X2))).
% 0.43/1.61  cnf(i_0_395, axiom, (X1!=X2|esk35_1(X1)=esk35_1(X2))).
% 0.43/1.61  cnf(i_0_396, axiom, (X1!=X2|hd(X1)=hd(X2))).
% 0.43/1.61  cnf(i_0_397, axiom, (X1!=X2|tl(X1)=tl(X2))).
% 0.43/1.61  cnf(i_0_398, axiom, (X1!=X2|esk47_1(X1)=esk47_1(X2))).
% 0.43/1.61  cnf(i_0_399, axiom, (X1!=X2|esk46_1(X1)=esk46_1(X2))).
% 0.43/1.61  cnf(i_0_400, axiom, (X1!=X2|esk36_1(X1)=esk36_1(X2))).
% 0.43/1.61  cnf(i_0_401, axiom, (X1!=X2|~cyclefreeP(X1)|cyclefreeP(X2))).
% 0.43/1.61  cnf(i_0_402, axiom, (X1!=X2|~duplicatefreeP(X1)|duplicatefreeP(X2))).
% 0.43/1.61  cnf(i_0_403, axiom, (X1!=X2|~equalelemsP(X1)|equalelemsP(X2))).
% 0.43/1.61  cnf(i_0_404, axiom, (X1!=X2|~segmentP(X1,X3)|segmentP(X2,X3))).
% 0.43/1.61  cnf(i_0_405, axiom, (X1!=X2|~segmentP(X3,X1)|segmentP(X3,X2))).
% 0.43/1.61  cnf(i_0_406, axiom, (X1!=X2|~memberP(X1,X3)|memberP(X2,X3))).
% 0.43/1.61  cnf(i_0_407, axiom, (X1!=X2|~memberP(X3,X1)|memberP(X3,X2))).
% 0.43/1.61  cnf(i_0_408, axiom, (X1!=X2|~frontsegP(X1,X3)|frontsegP(X2,X3))).
% 0.43/1.61  cnf(i_0_409, axiom, (X1!=X2|~frontsegP(X3,X1)|frontsegP(X3,X2))).
% 0.43/1.61  cnf(i_0_410, axiom, (X1!=X2|~rearsegP(X1,X3)|rearsegP(X2,X3))).
% 0.43/1.61  cnf(i_0_411, axiom, (X1!=X2|~rearsegP(X3,X1)|rearsegP(X3,X2))).
% 0.43/1.61  cnf(i_0_412, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.43/1.61  cnf(i_0_413, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.43/1.61  cnf(i_0_414, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.43/1.62  cnf(i_0_415, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.43/1.62  cnf(i_0_416, axiom, (X1!=X2|~neq(X1,X3)|neq(X2,X3))).
% 0.43/1.62  cnf(i_0_417, axiom, (X1!=X2|~neq(X3,X1)|neq(X3,X2))).
% 0.43/1.62  cnf(i_0_418, axiom, (X1!=X2|~singletonP(X1)|singletonP(X2))).
% 0.43/1.62  cnf(i_0_419, axiom, (X1!=X2|~ssItem(X1)|ssItem(X2))).
% 0.43/1.62  cnf(i_0_420, axiom, (X1!=X2|~ssList(X1)|ssList(X2))).
% 0.43/1.62  cnf(i_0_421, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.43/1.62  cnf(i_0_422, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.43/1.62  cnf(i_0_423, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.43/1.62  cnf(i_0_424, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.43/1.62  cnf(i_0_425, axiom, (X1!=X2|~strictorderP(X1)|strictorderP(X2))).
% 0.43/1.62  cnf(i_0_426, axiom, (X1!=X2|~totalorderP(X1)|totalorderP(X2))).
% 0.43/1.62  cnf(i_0_427, axiom, (X1!=X2|~strictorderedP(X1)|strictorderedP(X2))).
% 0.43/1.62  cnf(i_0_428, axiom, (X1!=X2|~totalorderedP(X1)|totalorderedP(X2))).
% 0.85/2.11  cnf(i_0_386, axiom, (X1=X1)).
% 0.85/2.11  cnf(i_0_387, axiom, (X1=X2|X2!=X1)).
% 0.85/2.11  cnf(i_0_388, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.85/2.11  cnf(i_0_389, axiom, (X1!=X2|app(X1,X3)=app(X2,X3))).
% 0.85/2.11  cnf(i_0_390, axiom, (X1!=X2|app(X3,X1)=app(X3,X2))).
% 0.85/2.11  cnf(i_0_391, axiom, (X1!=X2|cons(X1,X3)=cons(X2,X3))).
% 0.85/2.11  cnf(i_0_392, axiom, (X1!=X2|cons(X3,X1)=cons(X3,X2))).
% 0.85/2.11  cnf(i_0_393, axiom, (X1!=X2|esk40_1(X1)=esk40_1(X2))).
% 0.85/2.11  cnf(i_0_394, axiom, (X1!=X2|esk41_1(X1)=esk41_1(X2))).
% 0.85/2.11  cnf(i_0_395, axiom, (X1!=X2|esk35_1(X1)=esk35_1(X2))).
% 0.85/2.11  cnf(i_0_396, axiom, (X1!=X2|hd(X1)=hd(X2))).
% 0.85/2.11  cnf(i_0_397, axiom, (X1!=X2|tl(X1)=tl(X2))).
% 0.85/2.11  cnf(i_0_398, axiom, (X1!=X2|esk47_1(X1)=esk47_1(X2))).
% 0.85/2.11  cnf(i_0_399, axiom, (X1!=X2|esk46_1(X1)=esk46_1(X2))).
% 0.85/2.11  cnf(i_0_400, axiom, (X1!=X2|esk36_1(X1)=esk36_1(X2))).
% 0.85/2.11  cnf(i_0_401, axiom, (X1!=X2|~cyclefreeP(X1)|cyclefreeP(X2))).
% 0.85/2.11  cnf(i_0_402, axiom, (X1!=X2|~duplicatefreeP(X1)|duplicatefreeP(X2))).
% 0.85/2.11  cnf(i_0_403, axiom, (X1!=X2|~equalelemsP(X1)|equalelemsP(X2))).
% 0.85/2.11  cnf(i_0_404, axiom, (X1!=X2|~segmentP(X1,X3)|segmentP(X2,X3))).
% 0.85/2.11  cnf(i_0_405, axiom, (X1!=X2|~segmentP(X3,X1)|segmentP(X3,X2))).
% 0.85/2.11  cnf(i_0_406, axiom, (X1!=X2|~memberP(X1,X3)|memberP(X2,X3))).
% 0.85/2.11  cnf(i_0_407, axiom, (X1!=X2|~memberP(X3,X1)|memberP(X3,X2))).
% 0.85/2.11  cnf(i_0_408, axiom, (X1!=X2|~frontsegP(X1,X3)|frontsegP(X2,X3))).
% 0.85/2.11  cnf(i_0_409, axiom, (X1!=X2|~frontsegP(X3,X1)|frontsegP(X3,X2))).
% 0.85/2.11  cnf(i_0_410, axiom, (X1!=X2|~rearsegP(X1,X3)|rearsegP(X2,X3))).
% 0.85/2.11  cnf(i_0_411, axiom, (X1!=X2|~rearsegP(X3,X1)|rearsegP(X3,X2))).
% 0.85/2.11  cnf(i_0_412, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.85/2.11  cnf(i_0_413, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.85/2.11  cnf(i_0_414, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.85/2.11  cnf(i_0_415, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.85/2.11  cnf(i_0_416, axiom, (X1!=X2|~neq(X1,X3)|neq(X2,X3))).
% 0.85/2.11  cnf(i_0_417, axiom, (X1!=X2|~neq(X3,X1)|neq(X3,X2))).
% 0.85/2.11  cnf(i_0_418, axiom, (X1!=X2|~singletonP(X1)|singletonP(X2))).
% 0.85/2.11  cnf(i_0_419, axiom, (X1!=X2|~ssItem(X1)|ssItem(X2))).
% 0.85/2.11  cnf(i_0_420, axiom, (X1!=X2|~ssList(X1)|ssList(X2))).
% 0.85/2.11  cnf(i_0_421, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.85/2.11  cnf(i_0_422, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.85/2.11  cnf(i_0_423, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.85/2.11  cnf(i_0_424, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.85/2.11  cnf(i_0_425, axiom, (X1!=X2|~strictorderP(X1)|strictorderP(X2))).
% 0.85/2.11  cnf(i_0_426, axiom, (X1!=X2|~totalorderP(X1)|totalorderP(X2))).
% 0.85/2.11  cnf(i_0_427, axiom, (X1!=X2|~strictorderedP(X1)|strictorderedP(X2))).
% 0.85/2.11  cnf(i_0_428, axiom, (X1!=X2|~totalorderedP(X1)|totalorderedP(X2))).
% 0.85/2.11  cnf(i_0_429, plain, (~leq(X1,X2)|~leq(X2,X1)|~ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~cyclefreeP(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[189])).
% 0.85/2.11  cnf(i_0_430, plain, (lt(X1,X2)|~ssItem(X2)|~ssItem(X1)|~ssList(app(app(X3,cons(X2,X4)),cons(X1,X5)))|lt(X2,X1)|~strictorderP(app(app(X3,cons(X2,X4)),cons(X1,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[190])).
% 0.85/2.11  cnf(i_0_431, plain, (leq(X1,X2)|~ssItem(X2)|~ssItem(X1)|~ssList(app(app(X3,cons(X2,X4)),cons(X1,X5)))|leq(X2,X1)|~totalorderP(app(app(X3,cons(X2,X4)),cons(X1,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[191])).
% 0.85/2.11  cnf(i_0_432, plain, (~ssItem(X1)|~ssItem(X2)|~ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))|lt(X1,X2)|~strictorderedP(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[192])).
% 0.85/2.11  cnf(i_0_433, plain, (~ssItem(X1)|~ssItem(X2)|~ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))|leq(X1,X2)|~totalorderedP(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[193])).
% 0.85/2.11  cnf(i_0_434, plain, (~ssItem(X1)|~ssItem(X2)|~ssList(app(X3,cons(X1,cons(X2,X4))))|X1=X2|~equalelemsP(app(X3,cons(X1,cons(X2,X4))))|~ssList(X3)|~ssList(X4)), inference(equality_inference,[],[201])).
% 0.85/2.11  cnf(i_0_435, plain, (~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X1),cons(X3,X2))), inference(equality_inference,[],[208])).
% 0.85/2.11  cnf(i_0_436, plain, (~ssList(X1)|~ssList(app(app(X2,X1),X3))|segmentP(app(app(X2,X1),X3),X1)|~ssList(X2)|~ssList(X3)), inference(equality_inference,[],[210])).
% 0.85/2.11  cnf(i_0_437, plain, (~ssItem(X1)|~ssList(app(X2,cons(X1,X3)))|memberP(app(X2,cons(X1,X3)),X1)|~ssList(X2)|~ssList(X3)), inference(equality_inference,[],[211])).
% 0.85/2.11  cnf(i_0_438, plain, (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X2)|X1=X1), inference(equality_inference,[],[234])).
% 0.85/2.11  cnf(i_0_439, plain, (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X2)|X2=X2), inference(equality_inference,[],[235])).
% 0.85/2.11  cnf(i_0_440, plain, (~ssList(X1)|~ssList(X1)|X1=X1|~ssList(X2)), inference(equality_inference,[],[238])).
% 0.85/2.11  cnf(i_0_441, plain, (~ssList(X1)|~ssList(X1)|X1=X1|~ssList(X2)), inference(equality_inference,[],[239])).
% 0.85/2.11  cnf(i_0_442, plain, (~ssList(X1)|~ssItem(X2)|~ssItem(X2)|memberP(cons(X2,X1),X2)), inference(equality_inference,[],[247])).
% 0.85/2.11  cnf(i_0_443, plain, (~ssList(X1)|~ssList(app(X2,X1))|rearsegP(app(X2,X1),X1)|~ssList(X2)), inference(equality_inference,[],[254])).
% 0.85/2.11  cnf(i_0_444, plain, (~ssList(X1)|~ssList(app(X1,X2))|frontsegP(app(X1,X2),X1)|~ssList(X2)), inference(equality_inference,[],[255])).
% 0.85/2.11  cnf(i_0_445, plain, (~ssList(nil)|~ssItem(X1)|strictorderedP(cons(X1,nil))), inference(equality_inference,[],[272])).
% 0.85/2.11  cnf(i_0_446, plain, (~ssList(nil)|~ssItem(X1)|totalorderedP(cons(X1,nil))), inference(equality_inference,[],[273])).
% 0.85/2.11  cnf(i_0_447, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(equality_inference,[],[279])).
% 0.85/2.11  cnf(i_0_448, plain, (~lt(X1,X1)|~ssItem(X1)|~ssItem(X1)), inference(equality_inference,[],[280])).
% 0.85/2.11  cnf(i_0_449, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(equality_inference,[],[281])).
% 0.85/2.11  cnf(i_0_450, plain, (~ssList(cons(X1,nil))|singletonP(cons(X1,nil))|~ssItem(X1)), inference(equality_inference,[],[282])).
% 0.85/2.11  cnf(i_0_451, plain, (~ssList(nil)|segmentP(nil,nil)), inference(equality_inference,[],[309])).
% 0.85/2.11  cnf(i_0_452, plain, (~ssList(nil)|rearsegP(nil,nil)), inference(equality_inference,[],[310])).
% 0.85/2.11  cnf(i_0_453, plain, (~ssList(nil)|frontsegP(nil,nil)), inference(equality_inference,[],[311])).
% 0.85/2.11  cnf(i_0_454, plain, (geq(esk2_0,esk2_0)), inference(scs_inference,[],[i_0_378,i_0_346])).
% 0.85/2.11  cnf(i_0_455, plain, (~ssItem(X1)|geq(X1,X1)), inference(rename_variables,[],[i_0_346])).
% 0.85/2.11  cnf(i_0_456, plain, (leq(esk2_0,esk2_0)), inference(scs_inference,[],[i_0_378,i_0_346,i_0_347])).
% 0.85/2.11  cnf(i_0_457, plain, (~ssItem(X1)|leq(X1,X1)), inference(rename_variables,[],[i_0_347])).
% 0.85/2.11  cnf(i_0_458, plain, (segmentP(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_378,i_0_346,i_0_347,i_0_348])).
% 0.85/2.11  cnf(i_0_459, plain, (~ssList(X1)|segmentP(X1,X1)), inference(rename_variables,[],[i_0_348])).
% 0.85/2.11  cnf(i_0_460, plain, (rearsegP(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349])).
% 0.85/2.11  cnf(i_0_461, plain, (~ssList(X1)|rearsegP(X1,X1)), inference(rename_variables,[],[i_0_349])).
% 0.85/2.11  cnf(i_0_462, plain, (frontsegP(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350])).
% 0.85/2.11  cnf(i_0_463, plain, (~ssList(X1)|frontsegP(X1,X1)), inference(rename_variables,[],[i_0_350])).
% 0.85/2.11  cnf(i_0_464, plain, (esk51_0=esk49_0), inference(scs_inference,[],[i_0_373,i_0_383,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387])).
% 0.85/2.11  cnf(i_0_465, plain, (~neq(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_383,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447])).
% 0.85/2.11  cnf(i_0_466, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_447])).
% 0.85/2.11  cnf(i_0_467, plain, (segmentP(nil,esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_383,i_0_385,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309])).
% 0.85/2.11  cnf(i_0_468, plain, (nil!=X1|segmentP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_309])).
% 0.85/2.11  cnf(i_0_469, plain, (rearsegP(nil,esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_383,i_0_385,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310])).
% 0.85/2.11  cnf(i_0_470, plain, (nil!=X1|rearsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_310])).
% 0.85/2.11  cnf(i_0_471, plain, (frontsegP(nil,esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_383,i_0_385,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311])).
% 0.85/2.11  cnf(i_0_472, plain, (nil!=X1|frontsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_311])).
% 0.85/2.11  cnf(i_0_473, plain, (tl(esk48_0)=esk47_1(esk48_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363])).
% 0.85/2.11  cnf(i_0_474, plain, (nil=X1|tl(X1)=esk47_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_363])).
% 0.85/2.11  cnf(i_0_475, plain, (hd(esk48_0)=esk46_1(esk48_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364])).
% 0.85/2.11  cnf(i_0_476, plain, (nil=X1|hd(X1)=esk46_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_364])).
% 0.85/2.11  cnf(i_0_477, plain, (~neq(esk2_0,esk2_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449])).
% 0.85/2.11  cnf(i_0_478, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_449])).
% 0.85/2.11  cnf(i_0_479, plain, (nil=esk51_0), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388])).
% 0.85/2.11  cnf(i_0_480, plain, (cyclefreeP(esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401])).
% 0.85/2.11  cnf(i_0_481, plain, (duplicatefreeP(esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_367,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402])).
% 0.85/2.11  cnf(i_0_482, plain, (equalelemsP(esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_366,i_0_367,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403])).
% 0.85/2.11  cnf(i_0_483, plain, (~neq(esk49_0,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_366,i_0_367,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416])).
% 0.85/2.11  cnf(i_0_484, plain, (~neq(esk51_0,esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_366,i_0_367,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417])).
% 0.85/2.11  cnf(i_0_485, plain, (strictorderP(esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_366,i_0_367,i_0_370,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425])).
% 0.85/2.11  cnf(i_0_486, plain, (totalorderP(esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_366,i_0_367,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426])).
% 0.85/2.11  cnf(i_0_487, plain, (strictorderedP(esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_366,i_0_367,i_0_368,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427])).
% 0.85/2.11  cnf(i_0_488, plain, (totalorderedP(esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_376,i_0_381,i_0_383,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428])).
% 0.85/2.11  cnf(i_0_489, plain, (~neq(esk48_0,esk50_0)), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279])).
% 0.85/2.11  cnf(i_0_490, plain, (X1!=X2|~ssList(X2)|~ssList(X1)|~neq(X1,X2)), inference(rename_variables,[],[i_0_279])).
% 0.85/2.11  cnf(i_0_491, plain, (memberP(cons(esk2_0,esk51_0),esk2_0)), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279,i_0_442])).
% 0.85/2.11  cnf(i_0_492, plain, (~ssItem(X1)|~ssItem(X1)|memberP(cons(X1,X2),X1)|~ssList(X2)), inference(rename_variables,[],[i_0_442])).
% 0.85/2.11  cnf(i_0_493, plain, (frontsegP(cons(esk2_0,esk51_0),cons(esk2_0,esk51_0))), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279,i_0_442,i_0_435])).
% 0.85/2.11  cnf(i_0_494, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X2),cons(X3,X1))|~frontsegP(X2,X1)), inference(rename_variables,[],[i_0_435])).
% 0.85/2.11  cnf(i_0_495, plain, (ssItem(X1)|esk2_0!=X1), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279,i_0_442,i_0_435,i_0_419])).
% 0.85/2.11  cnf(i_0_496, plain, (ssList(X1)|esk50_0!=X1), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279,i_0_442,i_0_435,i_0_419,i_0_420])).
% 0.85/2.11  cnf(i_0_497, plain, (rearsegP(app(esk51_0,esk51_0),esk51_0)|esk50_0!=app(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279,i_0_442,i_0_435,i_0_419,i_0_420,i_0_443])).
% 0.85/2.11  cnf(i_0_498, plain, (~ssList(X1)|rearsegP(app(X1,X2),X2)|~ssList(X2)|~ssList(app(X1,X2))), inference(rename_variables,[],[i_0_443])).
% 0.85/2.11  cnf(i_0_499, plain, (frontsegP(app(esk51_0,esk51_0),esk51_0)|esk50_0!=app(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279,i_0_442,i_0_435,i_0_419,i_0_420,i_0_443,i_0_444])).
% 0.85/2.11  cnf(i_0_500, plain, (~ssList(X1)|frontsegP(app(X2,X1),X2)|~ssList(X2)|~ssList(app(X2,X1))), inference(rename_variables,[],[i_0_444])).
% 0.85/2.11  cnf(i_0_501, plain, (~ssItem(esk49_0)|memberP(app(esk51_0,cons(esk2_0,esk51_0)),esk2_0)|esk2_0!=esk51_0|esk50_0!=app(esk51_0,esk51_0)|~ssList(app(esk51_0,cons(esk2_0,esk51_0)))), inference(scs_inference,[],[i_0_373,i_0_374,i_0_375,i_0_376,i_0_381,i_0_383,i_0_384,i_0_385,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_372,i_0_378,i_0_346,i_0_347,i_0_348,i_0_349,i_0_350,i_0_387,i_0_447,i_0_309,i_0_310,i_0_311,i_0_363,i_0_364,i_0_449,i_0_388,i_0_401,i_0_402,i_0_403,i_0_416,i_0_417,i_0_425,i_0_426,i_0_427,i_0_428,i_0_279,i_0_442,i_0_435,i_0_419,i_0_420,i_0_443,i_0_444,i_0_281,i_0_301,i_0_437])).
% 0.85/2.11  cnf(i_0_502, plain, (ssItem(esk2_0)), inference(equality_inference,[],[495])).
% 0.85/2.11  cnf(i_0_503, plain, (ssList(esk50_0)), inference(equality_inference,[],[496])).
% 0.85/2.11  cnf(i_0_504, plain, (nil=esk50_0), inference(scs_inference,[],[i_0_479,i_0_380])).
% 0.85/2.11  cnf(i_0_505, plain, (segmentP(esk49_0,esk49_0)), inference(scs_inference,[],[i_0_375,i_0_348])).
% 0.85/2.11  cnf(i_0_506, plain, (~ssList(X1)|segmentP(X1,X1)), inference(rename_variables,[],[i_0_348])).
% 0.85/2.11  cnf(i_0_507, plain, (rearsegP(esk49_0,esk49_0)), inference(scs_inference,[],[i_0_375,i_0_348,i_0_349])).
% 0.85/2.11  cnf(i_0_508, plain, (~ssList(X1)|rearsegP(X1,X1)), inference(rename_variables,[],[i_0_349])).
% 0.85/2.11  cnf(i_0_509, plain, (frontsegP(esk49_0,esk49_0)), inference(scs_inference,[],[i_0_375,i_0_348,i_0_349,i_0_350])).
% 0.85/2.11  cnf(i_0_510, plain, (~ssList(X1)|frontsegP(X1,X1)), inference(rename_variables,[],[i_0_350])).
% 0.85/2.11  cnf(i_0_511, plain, (geq(esk1_0,esk1_0)), inference(scs_inference,[],[i_0_375,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346])).
% 0.85/2.11  cnf(i_0_512, plain, (~ssItem(X1)|geq(X1,X1)), inference(rename_variables,[],[i_0_346])).
% 0.85/2.11  cnf(i_0_513, plain, (leq(esk1_0,esk1_0)), inference(scs_inference,[],[i_0_375,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347])).
% 0.85/2.11  cnf(i_0_514, plain, (~ssItem(X1)|leq(X1,X1)), inference(rename_variables,[],[i_0_347])).
% 0.85/2.11  cnf(i_0_515, plain, (esk50_0=esk48_0), inference(scs_inference,[],[i_0_375,i_0_384,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387])).
% 0.85/2.11  cnf(i_0_516, plain, (~neq(esk49_0,esk49_0)), inference(scs_inference,[],[i_0_375,i_0_384,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447])).
% 0.85/2.11  cnf(i_0_517, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_447])).
% 0.85/2.11  cnf(i_0_518, plain, (~neq(esk1_0,esk1_0)), inference(scs_inference,[],[i_0_375,i_0_384,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449])).
% 0.85/2.11  cnf(i_0_519, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_449])).
% 0.85/2.11  cnf(i_0_520, plain, (segmentP(nil,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_479,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309])).
% 0.85/2.11  cnf(i_0_521, plain, (nil!=X1|segmentP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_309])).
% 0.85/2.11  cnf(i_0_522, plain, (rearsegP(nil,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_479,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310])).
% 0.85/2.11  cnf(i_0_523, plain, (nil!=X1|rearsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_310])).
% 0.85/2.11  cnf(i_0_524, plain, (frontsegP(nil,esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_479,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311])).
% 0.85/2.11  cnf(i_0_525, plain, (nil!=X1|frontsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_311])).
% 0.85/2.11  cnf(i_0_526, plain, (nil!=esk50_0), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_479,i_0_379,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388])).
% 0.85/2.11  cnf(i_0_527, plain, (cyclefreeP(esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_379,i_0_480,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401])).
% 0.85/2.11  cnf(i_0_528, plain, (duplicatefreeP(esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_379,i_0_480,i_0_481,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402])).
% 0.85/2.11  cnf(i_0_529, plain, (equalelemsP(esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_379,i_0_480,i_0_481,i_0_482,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403])).
% 0.85/2.11  cnf(i_0_530, plain, (strictorderP(esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425])).
% 0.85/2.11  cnf(i_0_531, plain, (totalorderP(esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426])).
% 0.85/2.11  cnf(i_0_532, plain, (strictorderedP(esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427])).
% 0.85/2.11  cnf(i_0_533, plain, (totalorderedP(esk51_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428])).
% 0.85/2.11  cnf(i_0_534, plain, (~neq(esk50_0,esk50_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_489,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416])).
% 0.85/2.11  cnf(i_0_535, plain, (~neq(esk48_0,esk48_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_489,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417])).
% 0.85/2.11  cnf(i_0_536, plain, (memberP(cons(esk1_0,esk51_0),esk1_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_479,i_0_489,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442])).
% 0.85/2.11  cnf(i_0_537, plain, (~ssItem(X1)|~ssItem(X1)|memberP(cons(X1,X2),X1)|~ssList(X2)), inference(rename_variables,[],[i_0_442])).
% 0.85/2.11  cnf(i_0_538, plain, (~neq(nil,esk49_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279])).
% 0.85/2.11  cnf(i_0_539, plain, (X1!=X2|~ssList(X2)|~ssList(X1)|~neq(X1,X2)), inference(rename_variables,[],[i_0_279])).
% 0.85/2.11  cnf(i_0_540, plain, (frontsegP(cons(esk2_0,esk49_0),cons(esk2_0,esk49_0))), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_378,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279,i_0_435])).
% 0.85/2.11  cnf(i_0_541, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X2),cons(X3,X1))|~frontsegP(X2,X1)), inference(rename_variables,[],[i_0_435])).
% 0.85/2.11  cnf(i_0_542, plain, (tl(esk50_0)=esk47_1(esk50_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_374,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_378,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279,i_0_435,i_0_363])).
% 0.85/2.11  cnf(i_0_543, plain, (nil=X1|tl(X1)=esk47_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_363])).
% 0.85/2.11  cnf(i_0_544, plain, (hd(esk50_0)=esk46_1(esk50_0)), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_374,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_378,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279,i_0_435,i_0_363,i_0_364])).
% 0.85/2.11  cnf(i_0_545, plain, (nil=X1|hd(X1)=esk46_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_364])).
% 0.85/2.11  cnf(i_0_546, plain, (ssItem(X1)|esk1_0!=X1), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_374,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_378,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279,i_0_435,i_0_363,i_0_364,i_0_419])).
% 0.85/2.11  cnf(i_0_547, plain, (rearsegP(app(esk51_0,esk51_0),esk51_0)|~ssList(app(esk51_0,esk51_0))), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_374,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_378,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279,i_0_435,i_0_363,i_0_364,i_0_419,i_0_443])).
% 0.85/2.11  cnf(i_0_548, plain, (~ssList(X1)|rearsegP(app(X1,X2),X2)|~ssList(X2)|~ssList(app(X1,X2))), inference(rename_variables,[],[i_0_443])).
% 0.85/2.11  cnf(i_0_549, plain, (frontsegP(app(esk51_0,esk51_0),esk51_0)|~ssList(app(esk51_0,esk51_0))), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_374,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_378,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279,i_0_435,i_0_363,i_0_364,i_0_419,i_0_443,i_0_444])).
% 0.85/2.11  cnf(i_0_550, plain, (~ssList(X1)|frontsegP(app(X2,X1),X2)|~ssList(X2)|~ssList(app(X2,X1))), inference(rename_variables,[],[i_0_444])).
% 0.85/2.11  cnf(i_0_551, plain, (~ssItem(esk48_0)|segmentP(app(app(esk51_0,esk51_0),esk51_0),esk51_0)|esk1_0!=esk50_0|~ssList(app(app(esk51_0,esk51_0),esk51_0))), inference(scs_inference,[],[i_0_373,i_0_375,i_0_384,i_0_374,i_0_381,i_0_383,i_0_385,i_0_479,i_0_489,i_0_378,i_0_377,i_0_379,i_0_480,i_0_481,i_0_482,i_0_485,i_0_486,i_0_487,i_0_488,i_0_348,i_0_349,i_0_350,i_0_346,i_0_347,i_0_387,i_0_447,i_0_449,i_0_309,i_0_310,i_0_311,i_0_388,i_0_401,i_0_402,i_0_403,i_0_425,i_0_426,i_0_427,i_0_428,i_0_416,i_0_417,i_0_442,i_0_279,i_0_435,i_0_363,i_0_364,i_0_419,i_0_281,i_0_301,i_0_436])).
% 0.85/2.11  cnf(i_0_552, plain, (ssItem(esk1_0)), inference(equality_inference,[],[546])).
% 0.85/2.11  cnf(i_0_553,plain, ($false), inference(scs_inference,[],[i_0+504, i_0_526]), ['proof']).
% 0.85/2.11  % SZS output end CNFRefutation
% 0.85/2.11  % Total time : 1.271s
%------------------------------------------------------------------------------