CSE_E---1.7.TMO-Non.f

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

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

% Result   : Timeout 297.92s 145.42s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : SWC045+1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12  % Command    : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32  % Computer : n010.cluster.edu
% 0.15/0.32  % Model    : x86_64 x86_64
% 0.15/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32  % Memory   : 8042.1875MB
% 0.15/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32  % CPULimit   : 300
% 0.15/0.32  % WCLimit    : 300
% 0.15/0.32  % DateTime   : Tue May  5 04:19:36 EDT 2026
% 0.15/0.33  % CPUTime    : 
% 0.15/0.34  % start to proof: theBenchmark
% 297.92/145.42  % Version  : CSE_E---1.7
% 297.92/145.42  % Problem  : theBenchmark.p
% 297.92/145.42  % SZS status Theorem for theBenchmark.p
% 297.92/145.42  % SZS output start CNFRefutation
% 297.92/145.42  fof(co1, conjecture, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(nil!=X2|X2!=X4|X1!=X3|nil=X1|?[X5]:(ssItem(X5)&((~(memberP(X3,X5))&?[X6]:(ssList(X6)&segmentP(X4,app(app(cons(X5,nil),X6),cons(X5,nil)))))|(![X6]:(ssList(X6)=>~(segmentP(X4,app(app(cons(X5,nil),X6),cons(X5,nil)))))&memberP(X3,X5))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 297.92/145.42  fof(ax94, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)=>~(gt(X2,X1))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax94)).
% 297.92/145.42  fof(ax33, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)=>~(lt(X2,X1))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax33)).
% 297.92/145.42  fof(ax90, axiom, ![X1]:(ssItem(X1)=>~(lt(X1,X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax90)).
% 297.92/145.42  fof(ax38, axiom, ![X1]:(ssItem(X1)=>~(memberP(nil,X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax38)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax8)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax10)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax9)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax12)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax11)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax13)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax14)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax7)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax3)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax44)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax56)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax36)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax37)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax82)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax27)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax70)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax67)).
% 297.92/145.42  fof(ax50, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(rearsegP(X1,X2)=>rearsegP(app(X3,X1),X2))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax50)).
% 297.92/145.42  fof(ax43, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(frontsegP(X1,X2)=>frontsegP(app(X1,X3),X2))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax43)).
% 297.92/145.42  fof(ax95, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((gt(X1,X2)&gt(X2,X3))=>gt(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax95)).
% 297.92/145.42  fof(ax88, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((geq(X1,X2)&geq(X2,X3))=>geq(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax88)).
% 297.92/145.42  fof(ax34, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((lt(X1,X2)&lt(X2,X3))=>lt(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax34)).
% 297.92/145.42  fof(ax91, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((leq(X1,X2)&lt(X2,X3))=>lt(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax91)).
% 297.92/145.42  fof(ax30, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((leq(X1,X2)&leq(X2,X3))=>leq(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax30)).
% 297.92/145.42  fof(ax53, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((segmentP(X1,X2)&segmentP(X2,X3))=>segmentP(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax53)).
% 297.92/145.42  fof(ax47, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((rearsegP(X1,X2)&rearsegP(X2,X3))=>rearsegP(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax47)).
% 297.92/145.42  fof(ax40, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((frontsegP(X1,X2)&frontsegP(X2,X3))=>frontsegP(X1,X3))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax40)).
% 297.92/145.42  fof(ax6, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(rearsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X3,X2)=X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax6)).
% 297.92/145.42  fof(ax5, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(frontsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X2,X3)=X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax5)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax19)).
% 297.92/145.42  fof(ax79, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X3,X2)=app(X1,X2)=>X3=X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax79)).
% 297.92/145.42  fof(ax80, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X2,X3)=app(X2,X1)=>X3=X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax80)).
% 297.92/145.42  fof(ax86, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil!=X1=>tl(app(X1,X2))=app(tl(X1),X2)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax86)).
% 297.92/145.42  fof(ax81, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>cons(X2,X1)=app(cons(X2,nil),X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax81)).
% 297.92/145.42  fof(ax54, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((segmentP(X1,X2)&segmentP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax54)).
% 297.92/145.42  fof(ax48, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((rearsegP(X1,X2)&rearsegP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax48)).
% 297.92/145.42  fof(ax41, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((frontsegP(X1,X2)&frontsegP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax41)).
% 297.92/145.42  fof(ax87, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>((geq(X1,X2)&geq(X2,X1))=>X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax87)).
% 297.92/145.42  fof(ax29, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>((leq(X1,X2)&leq(X2,X1))=>X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax29)).
% 297.92/145.42  fof(ax93, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)<=>(X1!=X2&leq(X1,X2))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax93)).
% 297.92/145.42  fof(ax92, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(leq(X1,X2)=>(X1=X2|lt(X1,X2))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax92)).
% 297.92/145.42  fof(ax35, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)<=>lt(X2,X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax35)).
% 297.92/145.42  fof(ax32, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(geq(X1,X2)<=>leq(X2,X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax32)).
% 297.92/145.42  fof(ax85, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil!=X1=>hd(app(X1,X2))=hd(X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax85)).
% 297.92/145.42  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/sandbox/benchmark/Axioms/SWC001+0.ax', ax77)).
% 297.92/145.42  fof(ax25, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>tl(cons(X2,X1))=X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax25)).
% 297.92/145.42  fof(ax23, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>hd(cons(X2,X1))=X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax23)).
% 297.92/145.42  fof(ax26, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>ssList(app(X1,X2)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax26)).
% 297.92/145.42  fof(ax16, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>ssList(cons(X2,X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax16)).
% 297.92/145.42  fof(ax15, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(neq(X1,X2)<=>X1!=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax15)).
% 297.92/145.42  fof(ax1, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(neq(X1,X2)<=>X1!=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax1)).
% 297.92/145.42  fof(ax4, axiom, ![X1]:(ssList(X1)=>(singletonP(X1)<=>?[X2]:(ssItem(X2)&cons(X2,nil)=X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax4)).
% 297.92/145.42  fof(ax83, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil=app(X1,X2)<=>(nil=X2&nil=X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax83)).
% 297.92/145.42  fof(ax18, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>cons(X2,X1)!=X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax18)).
% 297.92/145.42  fof(ax21, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>nil!=cons(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax21)).
% 297.92/145.42  fof(ax20, axiom, ![X1]:(ssList(X1)=>(nil=X1|?[X2]:(ssList(X2)&?[X3]:(ssItem(X3)&cons(X3,X2)=X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax20)).
% 297.92/145.42  fof(ax78, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>cons(hd(X1),tl(X1))=X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax78)).
% 297.92/145.42  fof(ax73, axiom, ![X1]:(ssItem(X1)=>equalelemsP(cons(X1,nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax73)).
% 297.92/145.42  fof(ax71, axiom, ![X1]:(ssItem(X1)=>duplicatefreeP(cons(X1,nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax71)).
% 297.92/145.42  fof(ax68, axiom, ![X1]:(ssItem(X1)=>strictorderedP(cons(X1,nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax68)).
% 297.92/145.42  fof(ax65, axiom, ![X1]:(ssItem(X1)=>totalorderedP(cons(X1,nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax65)).
% 297.92/145.42  fof(ax63, axiom, ![X1]:(ssItem(X1)=>strictorderP(cons(X1,nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax63)).
% 297.92/145.42  fof(ax61, axiom, ![X1]:(ssItem(X1)=>totalorderP(cons(X1,nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax61)).
% 297.92/145.42  fof(ax59, axiom, ![X1]:(ssItem(X1)=>cyclefreeP(cons(X1,nil))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax59)).
% 297.92/145.42  fof(ax58, axiom, ![X1]:(ssList(X1)=>(segmentP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax58)).
% 297.92/145.42  fof(ax52, axiom, ![X1]:(ssList(X1)=>(rearsegP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax52)).
% 297.92/145.42  fof(ax46, axiom, ![X1]:(ssList(X1)=>(frontsegP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax46)).
% 297.92/145.42  fof(ax89, axiom, ![X1]:(ssItem(X1)=>geq(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax89)).
% 297.92/145.42  fof(ax31, axiom, ![X1]:(ssItem(X1)=>leq(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax31)).
% 297.92/145.42  fof(ax55, axiom, ![X1]:(ssList(X1)=>segmentP(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax55)).
% 297.92/145.42  fof(ax49, axiom, ![X1]:(ssList(X1)=>rearsegP(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax49)).
% 297.92/145.42  fof(ax42, axiom, ![X1]:(ssList(X1)=>frontsegP(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax42)).
% 297.92/145.42  fof(ax28, axiom, ![X1]:(ssList(X1)=>app(nil,X1)=X1), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax28)).
% 297.92/145.42  fof(ax84, axiom, ![X1]:(ssList(X1)=>app(X1,nil)=X1), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax84)).
% 297.92/145.42  fof(ax57, axiom, ![X1]:(ssList(X1)=>segmentP(X1,nil)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax57)).
% 297.92/145.42  fof(ax51, axiom, ![X1]:(ssList(X1)=>rearsegP(X1,nil)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax51)).
% 297.92/145.42  fof(ax45, axiom, ![X1]:(ssList(X1)=>frontsegP(X1,nil)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax45)).
% 297.92/145.42  fof(ax76, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>?[X2]:(ssList(X2)&tl(X1)=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax76)).
% 297.92/145.42  fof(ax24, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>ssList(tl(X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax24)).
% 297.92/145.42  fof(ax75, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>?[X2]:(ssItem(X2)&hd(X1)=X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax75)).
% 297.92/145.42  fof(ax22, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>ssItem(hd(X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax22)).
% 297.92/145.42  fof(ax39, axiom, ~(singletonP(nil)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax39)).
% 297.92/145.42  fof(ax2, axiom, ?[X1]:(ssItem(X1)&?[X2]:(ssItem(X2)&X1!=X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax2)).
% 297.92/145.42  fof(ax74, axiom, equalelemsP(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax74)).
% 297.92/145.42  fof(ax72, axiom, duplicatefreeP(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax72)).
% 297.92/145.42  fof(ax69, axiom, strictorderedP(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax69)).
% 297.92/145.42  fof(ax66, axiom, totalorderedP(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax66)).
% 297.92/145.42  fof(ax64, axiom, strictorderP(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax64)).
% 297.92/145.42  fof(ax62, axiom, totalorderP(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax62)).
% 297.92/145.42  fof(ax60, axiom, cyclefreeP(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax60)).
% 297.92/145.42  fof(ax17, axiom, ssList(nil), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax', ax17)).
% 297.92/145.42  fof(i_0_96, negated_conjecture, ~(![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(nil!=X2|X2!=X4|X1!=X3|nil=X1|?[X5]:(ssItem(X5)&((~memberP(X3,X5)&?[X6]:(ssList(X6)&segmentP(X4,app(app(cons(X5,nil),X6),cons(X5,nil)))))|(![X6]:(ssList(X6)=>~segmentP(X4,app(app(cons(X5,nil),X6),cons(X5,nil))))&memberP(X3,X5)))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[co1])])).
% 297.92/145.42  fof(i_0_97, plain, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)=>~gt(X2,X1)))), inference(fof_simplification,[status(thm)],[ax94])).
% 297.92/145.42  fof(i_0_98, plain, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)=>~lt(X2,X1)))), inference(fof_simplification,[status(thm)],[ax33])).
% 297.92/145.42  fof(i_0_99, plain, ![X1]:(ssItem(X1)=>~lt(X1,X1)), inference(fof_simplification,[status(thm)],[ax90])).
% 297.92/145.42  fof(i_0_100, plain, ![X1]:(ssItem(X1)=>~memberP(nil,X1)), inference(fof_simplification,[status(thm)],[ax38])).
% 297.92/145.42  fof(i_0_101, negated_conjecture, ![X465, X466]:(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)&((memberP(esk50_0,X465)|(~ssList(X466)|~segmentP(esk51_0,app(app(cons(X465,nil),X466),cons(X465,nil))))|~ssItem(X465))&((ssList(esk52_1(X465))|~memberP(esk50_0,X465)|~ssItem(X465))&(segmentP(esk51_0,app(app(cons(X465,nil),esk52_1(X465)),cons(X465,nil)))|~memberP(esk50_0,X465)|~ssItem(X465))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_96])])])])])).
% 297.92/145.42  fof(i_0_102, plain, ![X244, X245, X246, X247, X248, X249]:((~cyclefreeP(X244)|(~ssItem(X245)|(~ssItem(X246)|(~ssList(X247)|(~ssList(X248)|(~ssList(X249)|(app(app(X247,cons(X245,X248)),cons(X246,X249))!=X244|(~leq(X245,X246)|~leq(X246,X245))))))))|~ssList(X244))&((ssItem(esk10_1(X244))|cyclefreeP(X244)|~ssList(X244))&((ssItem(esk11_1(X244))|cyclefreeP(X244)|~ssList(X244))&((ssList(esk12_1(X244))|cyclefreeP(X244)|~ssList(X244))&((ssList(esk13_1(X244))|cyclefreeP(X244)|~ssList(X244))&((ssList(esk14_1(X244))|cyclefreeP(X244)|~ssList(X244))&((app(app(esk12_1(X244),cons(esk10_1(X244),esk13_1(X244))),cons(esk11_1(X244),esk14_1(X244)))=X244|cyclefreeP(X244)|~ssList(X244))&((leq(esk10_1(X244),esk11_1(X244))|cyclefreeP(X244)|~ssList(X244))&(leq(esk11_1(X244),esk10_1(X244))|cyclefreeP(X244)|~ssList(X244)))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax8])])])])])).
% 297.92/145.42  fof(i_0_103, plain, ![X266, X267, X268, X269, X270, X271]:((~strictorderP(X266)|(~ssItem(X267)|(~ssItem(X268)|(~ssList(X269)|(~ssList(X270)|(~ssList(X271)|(app(app(X269,cons(X267,X270)),cons(X268,X271))!=X266|(lt(X267,X268)|lt(X268,X267))))))))|~ssList(X266))&((ssItem(esk20_1(X266))|strictorderP(X266)|~ssList(X266))&((ssItem(esk21_1(X266))|strictorderP(X266)|~ssList(X266))&((ssList(esk22_1(X266))|strictorderP(X266)|~ssList(X266))&((ssList(esk23_1(X266))|strictorderP(X266)|~ssList(X266))&((ssList(esk24_1(X266))|strictorderP(X266)|~ssList(X266))&((app(app(esk22_1(X266),cons(esk20_1(X266),esk23_1(X266))),cons(esk21_1(X266),esk24_1(X266)))=X266|strictorderP(X266)|~ssList(X266))&((~lt(esk20_1(X266),esk21_1(X266))|strictorderP(X266)|~ssList(X266))&(~lt(esk21_1(X266),esk20_1(X266))|strictorderP(X266)|~ssList(X266)))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax10])])])])])).
% 297.92/145.42  fof(i_0_104, plain, ![X255, X256, X257, X258, X259, X260]:((~totalorderP(X255)|(~ssItem(X256)|(~ssItem(X257)|(~ssList(X258)|(~ssList(X259)|(~ssList(X260)|(app(app(X258,cons(X256,X259)),cons(X257,X260))!=X255|(leq(X256,X257)|leq(X257,X256))))))))|~ssList(X255))&((ssItem(esk15_1(X255))|totalorderP(X255)|~ssList(X255))&((ssItem(esk16_1(X255))|totalorderP(X255)|~ssList(X255))&((ssList(esk17_1(X255))|totalorderP(X255)|~ssList(X255))&((ssList(esk18_1(X255))|totalorderP(X255)|~ssList(X255))&((ssList(esk19_1(X255))|totalorderP(X255)|~ssList(X255))&((app(app(esk17_1(X255),cons(esk15_1(X255),esk18_1(X255))),cons(esk16_1(X255),esk19_1(X255)))=X255|totalorderP(X255)|~ssList(X255))&((~leq(esk15_1(X255),esk16_1(X255))|totalorderP(X255)|~ssList(X255))&(~leq(esk16_1(X255),esk15_1(X255))|totalorderP(X255)|~ssList(X255)))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax9])])])])])).
% 297.92/145.42  fof(i_0_105, plain, ![X288, X289, X290, X291, X292, X293]:((~strictorderedP(X288)|(~ssItem(X289)|(~ssItem(X290)|(~ssList(X291)|(~ssList(X292)|(~ssList(X293)|(app(app(X291,cons(X289,X292)),cons(X290,X293))!=X288|lt(X289,X290)))))))|~ssList(X288))&((ssItem(esk30_1(X288))|strictorderedP(X288)|~ssList(X288))&((ssItem(esk31_1(X288))|strictorderedP(X288)|~ssList(X288))&((ssList(esk32_1(X288))|strictorderedP(X288)|~ssList(X288))&((ssList(esk33_1(X288))|strictorderedP(X288)|~ssList(X288))&((ssList(esk34_1(X288))|strictorderedP(X288)|~ssList(X288))&((app(app(esk32_1(X288),cons(esk30_1(X288),esk33_1(X288))),cons(esk31_1(X288),esk34_1(X288)))=X288|strictorderedP(X288)|~ssList(X288))&(~lt(esk30_1(X288),esk31_1(X288))|strictorderedP(X288)|~ssList(X288))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax12])])])])])).
% 297.92/145.42  fof(i_0_106, plain, ![X277, X278, X279, X280, X281, X282]:((~totalorderedP(X277)|(~ssItem(X278)|(~ssItem(X279)|(~ssList(X280)|(~ssList(X281)|(~ssList(X282)|(app(app(X280,cons(X278,X281)),cons(X279,X282))!=X277|leq(X278,X279)))))))|~ssList(X277))&((ssItem(esk25_1(X277))|totalorderedP(X277)|~ssList(X277))&((ssItem(esk26_1(X277))|totalorderedP(X277)|~ssList(X277))&((ssList(esk27_1(X277))|totalorderedP(X277)|~ssList(X277))&((ssList(esk28_1(X277))|totalorderedP(X277)|~ssList(X277))&((ssList(esk29_1(X277))|totalorderedP(X277)|~ssList(X277))&((app(app(esk27_1(X277),cons(esk25_1(X277),esk28_1(X277))),cons(esk26_1(X277),esk29_1(X277)))=X277|totalorderedP(X277)|~ssList(X277))&(~leq(esk25_1(X277),esk26_1(X277))|totalorderedP(X277)|~ssList(X277))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax11])])])])])).
% 297.92/145.42  fof(i_0_107, plain, ![X299, X300, X301, X302, X303, X304]:((~duplicatefreeP(X299)|(~ssItem(X300)|(~ssItem(X301)|(~ssList(X302)|(~ssList(X303)|(~ssList(X304)|(app(app(X302,cons(X300,X303)),cons(X301,X304))!=X299|X300!=X301))))))|~ssList(X299))&((ssItem(esk35_1(X299))|duplicatefreeP(X299)|~ssList(X299))&((ssItem(esk36_1(X299))|duplicatefreeP(X299)|~ssList(X299))&((ssList(esk37_1(X299))|duplicatefreeP(X299)|~ssList(X299))&((ssList(esk38_1(X299))|duplicatefreeP(X299)|~ssList(X299))&((ssList(esk39_1(X299))|duplicatefreeP(X299)|~ssList(X299))&((app(app(esk37_1(X299),cons(esk35_1(X299),esk38_1(X299))),cons(esk36_1(X299),esk39_1(X299)))=X299|duplicatefreeP(X299)|~ssList(X299))&(esk35_1(X299)=esk36_1(X299)|duplicatefreeP(X299)|~ssList(X299))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax13])])])])])).
% 297.92/145.42  fof(i_0_108, plain, ![X310, X311, X312, X313, X314]:((~equalelemsP(X310)|(~ssItem(X311)|(~ssItem(X312)|(~ssList(X313)|(~ssList(X314)|(app(X313,cons(X311,cons(X312,X314)))!=X310|X311=X312)))))|~ssList(X310))&((ssItem(esk40_1(X310))|equalelemsP(X310)|~ssList(X310))&((ssItem(esk41_1(X310))|equalelemsP(X310)|~ssList(X310))&((ssList(esk42_1(X310))|equalelemsP(X310)|~ssList(X310))&((ssList(esk43_1(X310))|equalelemsP(X310)|~ssList(X310))&((app(esk42_1(X310),cons(esk40_1(X310),cons(esk41_1(X310),esk43_1(X310))))=X310|equalelemsP(X310)|~ssList(X310))&(esk40_1(X310)!=esk41_1(X310)|equalelemsP(X310)|~ssList(X310)))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax14])])])])])).
% 297.92/145.42  fof(i_0_109, plain, ![X238, X239, X242, X243]:(((ssList(esk8_2(X238,X239))|~segmentP(X238,X239)|~ssList(X239)|~ssList(X238))&((ssList(esk9_2(X238,X239))|~segmentP(X238,X239)|~ssList(X239)|~ssList(X238))&(app(app(esk8_2(X238,X239),X239),esk9_2(X238,X239))=X238|~segmentP(X238,X239)|~ssList(X239)|~ssList(X238))))&(~ssList(X242)|(~ssList(X243)|app(app(X242,X239),X243)!=X238)|segmentP(X238,X239)|~ssList(X239)|~ssList(X238))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax7])])])])])).
% 297.92/145.42  fof(i_0_110, plain, ![X221, X222, X225, X226]:(((ssList(esk3_2(X221,X222))|~memberP(X221,X222)|~ssItem(X222)|~ssList(X221))&((ssList(esk4_2(X221,X222))|~memberP(X221,X222)|~ssItem(X222)|~ssList(X221))&(app(esk3_2(X221,X222),cons(X222,esk4_2(X221,X222)))=X221|~memberP(X221,X222)|~ssItem(X222)|~ssList(X221))))&(~ssList(X225)|(~ssList(X226)|app(X225,cons(X222,X226))!=X221)|memberP(X221,X222)|~ssItem(X222)|~ssList(X221))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])])).
% 297.92/145.42  fof(i_0_111, plain, ![X377, X378, X379, X380]:(((X377=X378|~frontsegP(cons(X377,X379),cons(X378,X380))|~ssList(X380)|~ssList(X379)|~ssItem(X378)|~ssItem(X377))&(frontsegP(X379,X380)|~frontsegP(cons(X377,X379),cons(X378,X380))|~ssList(X380)|~ssList(X379)|~ssItem(X378)|~ssItem(X377)))&(X377!=X378|~frontsegP(X379,X380)|frontsegP(cons(X377,X379),cons(X378,X380))|~ssList(X380)|~ssList(X379)|~ssItem(X378)|~ssItem(X377))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax44])])])])).
% 297.92/145.42  fof(i_0_112, plain, ![X400, X401, X402, X403]:(~ssList(X400)|(~ssList(X401)|(~ssList(X402)|(~ssList(X403)|(~segmentP(X400,X401)|segmentP(app(app(X402,X400),X403),X401)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax56])])])).
% 297.92/145.42  fof(i_0_113, plain, ![X361, X362, X363]:((~memberP(app(X362,X363),X361)|(memberP(X362,X361)|memberP(X363,X361))|~ssList(X363)|~ssList(X362)|~ssItem(X361))&((~memberP(X362,X361)|memberP(app(X362,X363),X361)|~ssList(X363)|~ssList(X362)|~ssItem(X361))&(~memberP(X363,X361)|memberP(app(X362,X363),X361)|~ssList(X363)|~ssList(X362)|~ssItem(X361)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax36])])])])).
% 297.92/145.42  fof(i_0_114, plain, ![X364, X365, X366]:((~memberP(cons(X365,X366),X364)|(X364=X365|memberP(X366,X364))|~ssList(X366)|~ssItem(X365)|~ssItem(X364))&((X364!=X365|memberP(cons(X365,X366),X364)|~ssList(X366)|~ssItem(X365)|~ssItem(X364))&(~memberP(X366,X364)|memberP(cons(X365,X366),X364)|~ssList(X366)|~ssItem(X365)|~ssItem(X364)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax37])])])])).
% 297.92/145.42  fof(i_0_115, plain, ![X432, X433, X434]:(~ssList(X432)|(~ssList(X433)|(~ssList(X434)|app(app(X432,X433),X434)=app(X432,app(X433,X434))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax82])])])).
% 297.92/145.42  fof(i_0_116, plain, ![X342, X343, X344]:(~ssList(X342)|(~ssList(X343)|(~ssItem(X344)|cons(X344,app(X343,X342))=app(cons(X344,X343),X342)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax27])])])).
% 297.92/145.42  fof(i_0_117, plain, ![X413, X414]:((((nil!=X414|nil=X414|~strictorderedP(cons(X413,X414))|~ssList(X414)|~ssItem(X413))&(strictorderedP(X414)|nil=X414|~strictorderedP(cons(X413,X414))|~ssList(X414)|~ssItem(X413)))&(lt(X413,hd(X414))|nil=X414|~strictorderedP(cons(X413,X414))|~ssList(X414)|~ssItem(X413)))&((nil!=X414|strictorderedP(cons(X413,X414))|~ssList(X414)|~ssItem(X413))&(nil=X414|~strictorderedP(X414)|~lt(X413,hd(X414))|strictorderedP(cons(X413,X414))|~ssList(X414)|~ssItem(X413)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax70])])])])).
% 297.92/145.42  fof(i_0_118, plain, ![X410, X411]:((((nil!=X411|nil=X411|~totalorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410))&(totalorderedP(X411)|nil=X411|~totalorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410)))&(leq(X410,hd(X411))|nil=X411|~totalorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410)))&((nil!=X411|totalorderedP(cons(X410,X411))|~ssList(X411)|~ssItem(X410))&(nil=X411|~totalorderedP(X411)|~leq(X410,hd(X411))|totalorderedP(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)],[ax67])])])])).
% 297.92/145.42  fof(i_0_119, plain, ![X389, X390, X391]:(~ssList(X389)|(~ssList(X390)|(~ssList(X391)|(~rearsegP(X389,X390)|rearsegP(app(X391,X389),X390))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax50])])])).
% 297.92/145.42  fof(i_0_120, plain, ![X374, X375, X376]:(~ssList(X374)|(~ssList(X375)|(~ssList(X376)|(~frontsegP(X374,X375)|frontsegP(app(X374,X376),X375))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax43])])])).
% 297.92/145.42  fof(i_0_121, plain, ![X458, X459, X460]:(~ssItem(X458)|(~ssItem(X459)|(~ssItem(X460)|(~gt(X458,X459)|~gt(X459,X460)|gt(X458,X460))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax95])])])).
% 297.92/145.42  fof(i_0_122, plain, ![X444, X445, X446]:(~ssItem(X444)|(~ssItem(X445)|(~ssItem(X446)|(~geq(X444,X445)|~geq(X445,X446)|geq(X444,X446))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax88])])])).
% 297.92/145.42  fof(i_0_123, plain, ![X356, X357, X358]:(~ssItem(X356)|(~ssItem(X357)|(~ssItem(X358)|(~lt(X356,X357)|~lt(X357,X358)|lt(X356,X358))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax34])])])).
% 297.92/145.42  fof(i_0_124, plain, ![X449, X450, X451]:(~ssItem(X449)|(~ssItem(X450)|(~ssItem(X451)|(~leq(X449,X450)|~lt(X450,X451)|lt(X449,X451))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax91])])])).
% 297.92/145.42  fof(i_0_125, plain, ![X348, X349, X350]:(~ssItem(X348)|(~ssItem(X349)|(~ssItem(X350)|(~leq(X348,X349)|~leq(X349,X350)|leq(X348,X350))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax30])])])).
% 297.92/145.42  fof(i_0_126, plain, ![X394, X395, X396]:(~ssList(X394)|(~ssList(X395)|(~ssList(X396)|(~segmentP(X394,X395)|~segmentP(X395,X396)|segmentP(X394,X396))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax53])])])).
% 297.92/145.42  fof(i_0_127, plain, ![X383, X384, X385]:(~ssList(X383)|(~ssList(X384)|(~ssList(X385)|(~rearsegP(X383,X384)|~rearsegP(X384,X385)|rearsegP(X383,X385))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax47])])])).
% 297.92/145.42  fof(i_0_128, plain, ![X368, X369, X370]:(~ssList(X368)|(~ssList(X369)|(~ssList(X370)|(~frontsegP(X368,X369)|~frontsegP(X369,X370)|frontsegP(X368,X370))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax40])])])).
% 297.92/145.42  fof(i_0_129, plain, ![X234, X235, X237]:(((ssList(esk7_2(X234,X235))|~rearsegP(X234,X235)|~ssList(X235)|~ssList(X234))&(app(esk7_2(X234,X235),X235)=X234|~rearsegP(X234,X235)|~ssList(X235)|~ssList(X234)))&(~ssList(X237)|app(X237,X235)!=X234|rearsegP(X234,X235)|~ssList(X235)|~ssList(X234))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax6])])])])])).
% 297.92/145.42  fof(i_0_130, plain, ![X230, X231, X233]:(((ssList(esk6_2(X230,X231))|~frontsegP(X230,X231)|~ssList(X231)|~ssList(X230))&(app(X231,esk6_2(X230,X231))=X230|~frontsegP(X230,X231)|~ssList(X231)|~ssList(X230)))&(~ssList(X233)|app(X231,X233)!=X230|frontsegP(X230,X231)|~ssList(X231)|~ssList(X230))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax5])])])])])).
% 297.92/145.42  fof(i_0_131, plain, ![X325, X326, X327, X328]:((X327=X328|cons(X327,X325)!=cons(X328,X326)|~ssItem(X328)|~ssItem(X327)|~ssList(X326)|~ssList(X325))&(X326=X325|cons(X327,X325)!=cons(X328,X326)|~ssItem(X328)|~ssItem(X327)|~ssList(X326)|~ssList(X325))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax19])])])])).
% 297.92/145.42  fof(i_0_132, plain, ![X424, X425, X426]:(~ssList(X424)|(~ssList(X425)|(~ssList(X426)|(app(X426,X425)!=app(X424,X425)|X426=X424)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax79])])])).
% 297.92/145.42  fof(i_0_133, plain, ![X427, X428, X429]:(~ssList(X427)|(~ssList(X428)|(~ssList(X429)|(app(X428,X429)!=app(X428,X427)|X429=X427)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax80])])])).
% 297.92/145.42  fof(i_0_134, plain, ![X440, X441]:(~ssList(X440)|(~ssList(X441)|(nil=X440|tl(app(X440,X441))=app(tl(X440),X441)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax86])])])).
% 297.92/145.42  fof(i_0_135, plain, ![X430, X431]:(~ssList(X430)|(~ssItem(X431)|cons(X431,X430)=app(cons(X431,nil),X430))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax81])])])).
% 297.92/145.42  fof(i_0_136, plain, ![X397, X398]:(~ssList(X397)|(~ssList(X398)|(~segmentP(X397,X398)|~segmentP(X398,X397)|X397=X398))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax54])])])).
% 297.92/145.42  fof(i_0_137, plain, ![X386, X387]:(~ssList(X386)|(~ssList(X387)|(~rearsegP(X386,X387)|~rearsegP(X387,X386)|X386=X387))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax48])])])).
% 297.92/145.42  fof(i_0_138, plain, ![X371, X372]:(~ssList(X371)|(~ssList(X372)|(~frontsegP(X371,X372)|~frontsegP(X372,X371)|X371=X372))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax41])])])).
% 297.92/145.42  fof(i_0_139, plain, ![X442, X443]:(~ssItem(X442)|(~ssItem(X443)|(~geq(X442,X443)|~geq(X443,X442)|X442=X443))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax87])])])).
% 297.92/145.42  fof(i_0_140, plain, ![X346, X347]:(~ssItem(X346)|(~ssItem(X347)|(~leq(X346,X347)|~leq(X347,X346)|X346=X347))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax29])])])).
% 297.92/145.42  fof(i_0_141, plain, ![X456, X457]:(~ssItem(X456)|(~ssItem(X457)|(~gt(X456,X457)|~gt(X457,X456)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_97])])])).
% 297.92/145.42  fof(i_0_142, plain, ![X354, X355]:(~ssItem(X354)|(~ssItem(X355)|(~lt(X354,X355)|~lt(X355,X354)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_98])])])).
% 297.92/145.42  fof(i_0_143, plain, ![X454, X455]:(((X454!=X455|~lt(X454,X455)|~ssItem(X455)|~ssItem(X454))&(leq(X454,X455)|~lt(X454,X455)|~ssItem(X455)|~ssItem(X454)))&(X454=X455|~leq(X454,X455)|lt(X454,X455)|~ssItem(X455)|~ssItem(X454))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax93])])])])).
% 297.92/145.42  fof(i_0_144, plain, ![X452, X453]:(~ssItem(X452)|(~ssItem(X453)|(~leq(X452,X453)|(X452=X453|lt(X452,X453))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax92])])])).
% 297.92/145.42  fof(i_0_145, plain, ![X359, X360]:((~gt(X359,X360)|lt(X360,X359)|~ssItem(X360)|~ssItem(X359))&(~lt(X360,X359)|gt(X359,X360)|~ssItem(X360)|~ssItem(X359))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax35])])])])).
% 297.92/145.42  fof(i_0_146, plain, ![X352, X353]:((~geq(X352,X353)|leq(X353,X352)|~ssItem(X353)|~ssItem(X352))&(~leq(X353,X352)|geq(X352,X353)|~ssItem(X353)|~ssItem(X352))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax32])])])])).
% 297.92/145.42  fof(i_0_147, plain, ![X438, X439]:(~ssList(X438)|(~ssList(X439)|(nil=X438|hd(app(X438,X439))=hd(X438)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax85])])])).
% 297.92/145.42  fof(i_0_148, plain, ![X421, X422]:(~ssList(X421)|(~ssList(X422)|(nil=X422|nil=X421|hd(X422)!=hd(X421)|tl(X422)!=tl(X421)|X422=X421))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax77])])])).
% 297.92/145.42  fof(i_0_149, plain, ![X338, X339]:(~ssList(X338)|(~ssItem(X339)|tl(cons(X339,X338))=X338)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax25])])])).
% 297.92/145.42  fof(i_0_150, plain, ![X335, X336]:(~ssList(X335)|(~ssItem(X336)|hd(cons(X336,X335))=X336)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax23])])])).
% 297.92/145.42  fof(i_0_151, plain, ![X340, X341]:(~ssList(X340)|(~ssList(X341)|ssList(app(X340,X341)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax26])])])).
% 297.92/145.42  fof(i_0_152, plain, ![X321, X322]:(~ssList(X321)|(~ssItem(X322)|ssList(cons(X322,X321)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax16])])])).
% 297.92/145.42  fof(i_0_153, plain, ![X319, X320]:((~neq(X319,X320)|X319!=X320|~ssList(X320)|~ssList(X319))&(X319=X320|neq(X319,X320)|~ssList(X320)|~ssList(X319))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax15])])])])).
% 297.92/145.42  fof(i_0_154, plain, ![X217, X218]:((~neq(X217,X218)|X217!=X218|~ssItem(X218)|~ssItem(X217))&(X217=X218|neq(X217,X218)|~ssItem(X218)|~ssItem(X217))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax1])])])])).
% 297.92/145.42  fof(i_0_155, plain, ![X227, X229]:(((ssItem(esk5_1(X227))|~singletonP(X227)|~ssList(X227))&(cons(esk5_1(X227),nil)=X227|~singletonP(X227)|~ssList(X227)))&(~ssItem(X229)|cons(X229,nil)!=X227|singletonP(X227)|~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)],[ax4])])])])])).
% 297.92/145.42  fof(i_0_156, plain, ![X435, X436]:(((nil=X436|nil!=app(X435,X436)|~ssList(X436)|~ssList(X435))&(nil=X435|nil!=app(X435,X436)|~ssList(X436)|~ssList(X435)))&(nil!=X436|nil!=X435|nil=app(X435,X436)|~ssList(X436)|~ssList(X435))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax83])])])])).
% 297.92/145.42  fof(i_0_157, plain, ![X323, X324]:(~ssList(X323)|(~ssItem(X324)|cons(X324,X323)!=X323)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax18])])])).
% 297.92/145.42  fof(i_0_158, plain, ![X332, X333]:(~ssList(X332)|(~ssItem(X333)|nil!=cons(X333,X332))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax21])])])).
% 297.92/145.42  fof(i_0_159, plain, ![X329]:((ssList(esk44_1(X329))|nil=X329|~ssList(X329))&((ssItem(esk45_1(X329))|nil=X329|~ssList(X329))&(cons(esk45_1(X329),esk44_1(X329))=X329|nil=X329|~ssList(X329)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax20])])])])).
% 297.92/145.42  fof(i_0_160, plain, ![X423]:(~ssList(X423)|(nil=X423|cons(hd(X423),tl(X423))=X423)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax78])])).
% 297.92/145.42  fof(i_0_161, plain, ![X416]:(~ssItem(X416)|equalelemsP(cons(X416,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax73])])).
% 297.92/145.42  fof(i_0_162, plain, ![X415]:(~ssItem(X415)|duplicatefreeP(cons(X415,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax71])])).
% 297.92/145.42  fof(i_0_163, plain, ![X412]:(~ssItem(X412)|strictorderedP(cons(X412,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax68])])).
% 297.92/145.42  fof(i_0_164, plain, ![X409]:(~ssItem(X409)|totalorderedP(cons(X409,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax65])])).
% 297.92/145.42  fof(i_0_165, plain, ![X408]:(~ssItem(X408)|strictorderP(cons(X408,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax63])])).
% 297.92/145.42  fof(i_0_166, plain, ![X407]:(~ssItem(X407)|totalorderP(cons(X407,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax61])])).
% 297.92/145.42  fof(i_0_167, plain, ![X406]:(~ssItem(X406)|cyclefreeP(cons(X406,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax59])])).
% 297.92/145.42  fof(i_0_168, plain, ![X448]:(~ssItem(X448)|~lt(X448,X448)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_99])])).
% 297.92/145.42  fof(i_0_169, plain, ![X405]:((~segmentP(nil,X405)|nil=X405|~ssList(X405))&(nil!=X405|segmentP(nil,X405)|~ssList(X405))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax58])])])).
% 297.92/145.42  fof(i_0_170, plain, ![X393]:((~rearsegP(nil,X393)|nil=X393|~ssList(X393))&(nil!=X393|rearsegP(nil,X393)|~ssList(X393))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax52])])])).
% 297.92/145.42  fof(i_0_171, plain, ![X382]:((~frontsegP(nil,X382)|nil=X382|~ssList(X382))&(nil!=X382|frontsegP(nil,X382)|~ssList(X382))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax46])])])).
% 297.92/145.42  fof(i_0_172, plain, ![X367]:(~ssItem(X367)|~memberP(nil,X367)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_100])])).
% 297.92/145.42  fof(i_0_173, plain, ![X447]:(~ssItem(X447)|geq(X447,X447)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax89])])).
% 297.92/145.42  fof(i_0_174, plain, ![X351]:(~ssItem(X351)|leq(X351,X351)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax31])])).
% 297.92/145.42  fof(i_0_175, plain, ![X399]:(~ssList(X399)|segmentP(X399,X399)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax55])])).
% 297.92/145.42  fof(i_0_176, plain, ![X388]:(~ssList(X388)|rearsegP(X388,X388)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax49])])).
% 297.92/145.42  fof(i_0_177, plain, ![X373]:(~ssList(X373)|frontsegP(X373,X373)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax42])])).
% 297.92/145.42  fof(i_0_178, plain, ![X345]:(~ssList(X345)|app(nil,X345)=X345), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax28])])).
% 297.92/145.42  fof(i_0_179, plain, ![X437]:(~ssList(X437)|app(X437,nil)=X437), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax84])])).
% 297.92/145.42  fof(i_0_180, plain, ![X404]:(~ssList(X404)|segmentP(X404,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax57])])).
% 297.92/145.42  fof(i_0_181, plain, ![X392]:(~ssList(X392)|rearsegP(X392,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax51])])).
% 297.92/145.42  fof(i_0_182, plain, ![X381]:(~ssList(X381)|frontsegP(X381,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax45])])).
% 297.92/145.42  fof(i_0_183, plain, ![X419]:((ssList(esk47_1(X419))|nil=X419|~ssList(X419))&(tl(X419)=esk47_1(X419)|nil=X419|~ssList(X419))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax76])])])])).
% 297.92/145.42  fof(i_0_184, plain, ![X337]:(~ssList(X337)|(nil=X337|ssList(tl(X337)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax24])])).
% 297.92/145.42  fof(i_0_185, plain, ![X417]:((ssItem(esk46_1(X417))|nil=X417|~ssList(X417))&(hd(X417)=esk46_1(X417)|nil=X417|~ssList(X417))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax75])])])])).
% 297.92/145.42  fof(i_0_186, plain, ![X334]:(~ssList(X334)|(nil=X334|ssItem(hd(X334)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax22])])).
% 297.92/145.42  fof(i_0_187, plain, ~singletonP(nil), inference(fof_simplification,[status(thm)],[ax39])).
% 297.92/145.42  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])])).
% 297.92/145.42  cnf(i_0_189, negated_conjecture, (memberP(esk50_0,X1)|~ssList(X2)|~segmentP(esk51_0,app(app(cons(X1,nil),X2),cons(X1,nil)))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_190, 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_102]), ['final']).
% 297.92/145.42  cnf(i_0_191, negated_conjecture, (segmentP(esk51_0,app(app(cons(X1,nil),esk52_1(X1)),cons(X1,nil)))|~memberP(esk50_0,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_192, 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_103]), ['final']).
% 297.92/145.42  cnf(i_0_193, 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_104]), ['final']).
% 297.92/145.42  cnf(i_0_194, 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_105]), ['final']).
% 297.92/145.42  cnf(i_0_195, 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_106]), ['final']).
% 297.92/145.42  cnf(i_0_196, 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_107]), ['final']).
% 297.92/145.42  cnf(i_0_197, 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_107]), ['final']).
% 297.92/145.42  cnf(i_0_198, 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_105]), ['final']).
% 297.92/145.42  cnf(i_0_199, 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_106]), ['final']).
% 297.92/145.42  cnf(i_0_200, 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_103]), ['final']).
% 297.92/145.42  cnf(i_0_201, 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_104]), ['final']).
% 297.92/145.42  cnf(i_0_202, 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_102]), ['final']).
% 297.92/145.42  cnf(i_0_203, 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_108]), ['final']).
% 297.92/145.42  cnf(i_0_204, 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_108]), ['final']).
% 297.92/145.42  cnf(i_0_205, 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_109]), ['final']).
% 297.92/145.42  cnf(i_0_206, 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_110]), ['final']).
% 297.92/145.42  cnf(i_0_207, 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_111]), ['final']).
% 297.92/145.42  cnf(i_0_208, 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_112]), ['final']).
% 297.92/145.42  cnf(i_0_209, 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_111]), ['final']).
% 297.92/145.42  cnf(i_0_210, 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_111]), ['final']).
% 297.92/145.42  cnf(i_0_211, 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_113]), ['final']).
% 297.92/145.42  cnf(i_0_212, 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_109]), ['final']).
% 297.92/145.42  cnf(i_0_213, 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_110]), ['final']).
% 297.92/145.42  cnf(i_0_214, plain, (X3=X1|memberP(X2,X3)|~memberP(cons(X1,X2),X3)|~ssList(X2)|~ssItem(X1)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 297.92/145.42  cnf(i_0_215, plain, (app(app(X1,X2),X3)=app(X1,app(X2,X3))|~ssList(X1)|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 297.92/145.42  cnf(i_0_216, plain, (cons(X3,app(X2,X1))=app(cons(X3,X2),X1)|~ssList(X1)|~ssList(X2)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 297.92/145.42  cnf(i_0_217, plain, (nil=X1|strictorderedP(cons(X2,X1))|~strictorderedP(X1)|~lt(X2,hd(X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 297.92/145.42  cnf(i_0_218, plain, (nil=X1|totalorderedP(cons(X2,X1))|~totalorderedP(X1)|~leq(X2,hd(X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 297.92/145.42  cnf(i_0_219, plain, (rearsegP(app(X3,X1),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~rearsegP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 297.92/145.42  cnf(i_0_220, plain, (frontsegP(app(X1,X3),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~frontsegP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 297.92/145.42  cnf(i_0_221, plain, (memberP(app(X1,X3),X2)|~memberP(X1,X2)|~ssList(X3)|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 297.92/145.42  cnf(i_0_222, plain, (memberP(app(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssList(X3)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 297.92/145.42  cnf(i_0_223, plain, (memberP(cons(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 297.92/145.42  cnf(i_0_224, plain, (lt(X1,hd(X2))|nil=X2|~strictorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 297.92/145.42  cnf(i_0_225, plain, (leq(X1,hd(X2))|nil=X2|~totalorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 297.92/145.42  cnf(i_0_226, plain, (gt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~gt(X1,X2)|~gt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 297.92/145.42  cnf(i_0_227, plain, (geq(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~geq(X1,X2)|~geq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 297.92/145.42  cnf(i_0_228, plain, (lt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~lt(X1,X2)|~lt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 297.92/145.42  cnf(i_0_229, plain, (lt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~leq(X1,X2)|~lt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_124]), ['final']).
% 297.92/145.42  cnf(i_0_230, plain, (leq(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_125]), ['final']).
% 297.92/145.42  cnf(i_0_231, plain, (segmentP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~segmentP(X1,X2)|~segmentP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_126]), ['final']).
% 297.92/145.42  cnf(i_0_232, plain, (rearsegP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~rearsegP(X1,X2)|~rearsegP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_127]), ['final']).
% 297.92/145.42  cnf(i_0_233, plain, (frontsegP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~frontsegP(X1,X2)|~frontsegP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 297.92/145.42  cnf(i_0_234, plain, (app(esk7_2(X1,X2),X2)=X1|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 297.92/145.42  cnf(i_0_235, plain, (app(X1,esk6_2(X2,X1))=X2|~frontsegP(X2,X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 297.92/145.42  cnf(i_0_236, plain, (X1=X2|cons(X1,X3)!=cons(X2,X4)|~ssItem(X2)|~ssItem(X1)|~ssList(X4)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_131]), ['final']).
% 297.92/145.42  cnf(i_0_237, plain, (X1=X2|cons(X3,X2)!=cons(X4,X1)|~ssItem(X4)|~ssItem(X3)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_131]), ['final']).
% 297.92/145.42  cnf(i_0_238, plain, (strictorderedP(X1)|nil=X1|~strictorderedP(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 297.92/145.42  cnf(i_0_239, plain, (totalorderedP(X1)|nil=X1|~totalorderedP(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 297.92/145.42  cnf(i_0_240, plain, (X3=X1|~ssList(X1)|~ssList(X2)|~ssList(X3)|app(X3,X2)!=app(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_132]), ['final']).
% 297.92/145.42  cnf(i_0_241, plain, (X3=X1|~ssList(X1)|~ssList(X2)|~ssList(X3)|app(X2,X3)!=app(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_133]), ['final']).
% 297.92/145.42  cnf(i_0_242, plain, (ssList(esk9_2(X1,X2))|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 297.92/145.42  cnf(i_0_243, plain, (ssList(esk8_2(X1,X2))|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 297.92/145.42  cnf(i_0_244, plain, (ssList(esk7_2(X1,X2))|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 297.92/145.42  cnf(i_0_245, plain, (ssList(esk6_2(X1,X2))|~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 297.92/145.42  cnf(i_0_246, plain, (ssList(esk4_2(X1,X2))|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 297.92/145.42  cnf(i_0_247, plain, (ssList(esk3_2(X1,X2))|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 297.92/145.42  cnf(i_0_248, plain, (nil=X1|tl(app(X1,X2))=app(tl(X1),X2)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_134]), ['final']).
% 297.92/145.42  cnf(i_0_249, plain, (memberP(cons(X2,X3),X1)|X1!=X2|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 297.92/145.42  cnf(i_0_250, plain, (cons(X2,X1)=app(cons(X2,nil),X1)|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_135]), ['final']).
% 297.92/145.42  cnf(i_0_251, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~segmentP(X1,X2)|~segmentP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_136]), ['final']).
% 297.92/145.42  cnf(i_0_252, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)|~rearsegP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_137]), ['final']).
% 297.92/145.42  cnf(i_0_253, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)|~frontsegP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_138]), ['final']).
% 297.92/145.42  cnf(i_0_254, plain, (X1=X2|~ssItem(X1)|~ssItem(X2)|~geq(X1,X2)|~geq(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_139]), ['final']).
% 297.92/145.42  cnf(i_0_255, plain, (X1=X2|~ssItem(X1)|~ssItem(X2)|~leq(X1,X2)|~leq(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_140]), ['final']).
% 297.92/145.42  cnf(i_0_256, plain, (rearsegP(X3,X2)|~ssList(X1)|app(X1,X2)!=X3|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 297.92/145.42  cnf(i_0_257, plain, (frontsegP(X3,X2)|~ssList(X1)|app(X2,X1)!=X3|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 297.92/145.42  cnf(i_0_258, plain, (~ssItem(X1)|~ssItem(X2)|~gt(X1,X2)|~gt(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 297.92/145.42  cnf(i_0_259, plain, (~ssItem(X1)|~ssItem(X2)|~lt(X1,X2)|~lt(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 297.92/145.42  cnf(i_0_260, plain, (X1=X2|lt(X1,X2)|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_143]), ['final']).
% 297.92/145.42  cnf(i_0_261, plain, (X1=X2|lt(X1,X2)|~ssItem(X1)|~ssItem(X2)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_144]), ['final']).
% 297.92/145.42  cnf(i_0_262, plain, (strictorderedP(X1)|~lt(esk30_1(X1),esk31_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 297.92/145.42  cnf(i_0_263, plain, (totalorderedP(X1)|~leq(esk25_1(X1),esk26_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 297.92/145.42  cnf(i_0_264, plain, (strictorderP(X1)|~lt(esk21_1(X1),esk20_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 297.92/145.42  cnf(i_0_265, plain, (strictorderP(X1)|~lt(esk20_1(X1),esk21_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 297.92/145.42  cnf(i_0_266, plain, (totalorderP(X1)|~leq(esk16_1(X1),esk15_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 297.92/145.42  cnf(i_0_267, plain, (totalorderP(X1)|~leq(esk15_1(X1),esk16_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 297.92/145.42  cnf(i_0_268, plain, (gt(X2,X1)|~lt(X1,X2)|~ssItem(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_145]), ['final']).
% 297.92/145.42  cnf(i_0_269, plain, (geq(X2,X1)|~leq(X1,X2)|~ssItem(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 297.92/145.42  cnf(i_0_270, plain, (lt(X2,X1)|~gt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_145]), ['final']).
% 297.92/145.42  cnf(i_0_271, plain, (leq(X1,X2)|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_143]), ['final']).
% 297.92/145.42  cnf(i_0_272, plain, (leq(X2,X1)|~geq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 297.92/145.42  cnf(i_0_273, plain, (nil=X1|hd(app(X1,X2))=hd(X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_147]), ['final']).
% 297.92/145.42  cnf(i_0_274, plain, (strictorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 297.92/145.42  cnf(i_0_275, plain, (totalorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 297.92/145.42  cnf(i_0_276, 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_148]), ['final']).
% 297.92/145.42  cnf(i_0_277, plain, (tl(cons(X2,X1))=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_149]), ['final']).
% 297.92/145.42  cnf(i_0_278, plain, (hd(cons(X2,X1))=X2|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_150]), ['final']).
% 297.92/145.42  cnf(i_0_279, plain, (ssList(app(X1,X2))|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_151]), ['final']).
% 297.92/145.42  cnf(i_0_280, plain, (ssList(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_152]), ['final']).
% 297.92/145.42  cnf(i_0_281, plain, (~neq(X1,X2)|X1!=X2|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 297.92/145.42  cnf(i_0_282, plain, (X1!=X2|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_143]), ['final']).
% 297.92/145.42  cnf(i_0_283, plain, (~neq(X1,X2)|X1!=X2|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 297.92/145.42  cnf(i_0_284, plain, (singletonP(X2)|~ssItem(X1)|cons(X1,nil)!=X2|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 297.92/145.42  cnf(i_0_285, plain, (nil=X1|nil!=app(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_156]), ['final']).
% 297.92/145.42  cnf(i_0_286, plain, (nil=X1|nil!=app(X2,X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_156]), ['final']).
% 297.92/145.42  cnf(i_0_287, plain, (leq(esk11_1(X1),esk10_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 297.92/145.42  cnf(i_0_288, plain, (leq(esk10_1(X1),esk11_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 297.92/145.42  cnf(i_0_289, plain, (~ssList(X1)|~ssItem(X2)|cons(X2,X1)!=X1), inference(split_conjunct,[status(thm)],[i_0_157]), ['final']).
% 297.92/145.42  cnf(i_0_290, negated_conjecture, (ssList(esk52_1(X1))|~memberP(esk50_0,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_291, plain, (~ssList(X1)|~ssItem(X2)|nil!=cons(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 297.92/145.42  cnf(i_0_292, plain, (cons(esk45_1(X1),esk44_1(X1))=X1|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 297.92/145.42  cnf(i_0_293, plain, (nil=X1|cons(hd(X1),tl(X1))=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_160]), ['final']).
% 297.92/145.42  cnf(i_0_294, plain, (equalelemsP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_161]), ['final']).
% 297.92/145.42  cnf(i_0_295, plain, (duplicatefreeP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_162]), ['final']).
% 297.92/145.42  cnf(i_0_296, plain, (strictorderedP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_163]), ['final']).
% 297.92/145.42  cnf(i_0_297, plain, (totalorderedP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_164]), ['final']).
% 297.92/145.42  cnf(i_0_298, plain, (strictorderP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_165]), ['final']).
% 297.92/145.42  cnf(i_0_299, plain, (totalorderP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_166]), ['final']).
% 297.92/145.42  cnf(i_0_300, plain, (cyclefreeP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_167]), ['final']).
% 297.92/145.42  cnf(i_0_301, plain, (cons(esk5_1(X1),nil)=X1|~singletonP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 297.92/145.42  cnf(i_0_302, plain, (nil=app(X2,X1)|nil!=X1|nil!=X2|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_156]), ['final']).
% 297.92/145.42  cnf(i_0_303, plain, (X1=X2|neq(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 297.92/145.42  cnf(i_0_304, plain, (X1=X2|neq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 297.92/145.42  cnf(i_0_305, plain, (~ssItem(X1)|~lt(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_168]), ['final']).
% 297.92/145.42  cnf(i_0_306, plain, (nil=X1|~segmentP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 297.92/145.42  cnf(i_0_307, plain, (nil=X1|~rearsegP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 297.92/145.42  cnf(i_0_308, plain, (nil=X1|~frontsegP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 297.92/145.42  cnf(i_0_309, plain, (~ssItem(X1)|~memberP(nil,X1)), inference(split_conjunct,[status(thm)],[i_0_172]), ['final']).
% 297.92/145.42  cnf(i_0_310, plain, (ssItem(esk5_1(X1))|~singletonP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 297.92/145.42  cnf(i_0_311, plain, (equalelemsP(X1)|esk40_1(X1)!=esk41_1(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 297.92/145.42  cnf(i_0_312, plain, (segmentP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 297.92/145.42  cnf(i_0_313, plain, (rearsegP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 297.92/145.42  cnf(i_0_314, plain, (frontsegP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 297.92/145.42  cnf(i_0_315, plain, (ssList(esk43_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 297.92/145.42  cnf(i_0_316, plain, (ssList(esk42_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 297.92/145.42  cnf(i_0_317, plain, (ssItem(esk41_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 297.92/145.42  cnf(i_0_318, plain, (ssItem(esk40_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 297.92/145.42  cnf(i_0_319, plain, (ssList(esk39_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 297.92/145.42  cnf(i_0_320, plain, (ssList(esk38_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 297.92/145.42  cnf(i_0_321, plain, (ssList(esk37_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 297.92/145.42  cnf(i_0_322, plain, (ssItem(esk36_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 297.92/145.42  cnf(i_0_323, plain, (ssItem(esk35_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 297.92/145.42  cnf(i_0_324, plain, (ssList(esk34_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 297.92/145.42  cnf(i_0_325, plain, (ssList(esk33_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 297.92/145.42  cnf(i_0_326, plain, (ssList(esk32_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 297.92/145.42  cnf(i_0_327, plain, (ssItem(esk31_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 297.92/145.42  cnf(i_0_328, plain, (ssItem(esk30_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 297.92/145.42  cnf(i_0_329, plain, (ssList(esk29_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 297.92/145.42  cnf(i_0_330, plain, (ssList(esk28_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 297.92/145.42  cnf(i_0_331, plain, (ssList(esk27_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 297.92/145.42  cnf(i_0_332, plain, (ssItem(esk26_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 297.92/145.42  cnf(i_0_333, plain, (ssItem(esk25_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 297.92/145.42  cnf(i_0_334, plain, (ssList(esk24_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 297.92/145.42  cnf(i_0_335, plain, (ssList(esk23_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 297.92/145.42  cnf(i_0_336, plain, (ssList(esk22_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 297.92/145.42  cnf(i_0_337, plain, (ssItem(esk21_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 297.92/145.42  cnf(i_0_338, plain, (ssItem(esk20_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 297.92/145.42  cnf(i_0_339, plain, (ssList(esk19_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 297.92/145.42  cnf(i_0_340, plain, (ssList(esk18_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 297.92/145.42  cnf(i_0_341, plain, (ssList(esk17_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 297.92/145.42  cnf(i_0_342, plain, (ssItem(esk16_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 297.92/145.42  cnf(i_0_343, plain, (ssItem(esk15_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 297.92/145.42  cnf(i_0_344, plain, (ssList(esk14_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 297.92/145.42  cnf(i_0_345, plain, (ssList(esk13_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 297.92/145.42  cnf(i_0_346, plain, (ssList(esk12_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 297.92/145.42  cnf(i_0_347, plain, (ssItem(esk11_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 297.92/145.42  cnf(i_0_348, plain, (ssItem(esk10_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 297.92/145.42  cnf(i_0_349, plain, (geq(X1,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 297.92/145.42  cnf(i_0_350, plain, (leq(X1,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_174]), ['final']).
% 297.92/145.42  cnf(i_0_351, plain, (segmentP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_175]), ['final']).
% 297.92/145.42  cnf(i_0_352, plain, (rearsegP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_176]), ['final']).
% 297.92/145.42  cnf(i_0_353, plain, (frontsegP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_177]), ['final']).
% 297.92/145.42  cnf(i_0_354, plain, (app(nil,X1)=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_178]), ['final']).
% 297.92/145.42  cnf(i_0_355, plain, (app(X1,nil)=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_179]), ['final']).
% 297.92/145.42  cnf(i_0_356, plain, (esk35_1(X1)=esk36_1(X1)|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 297.92/145.42  cnf(i_0_357, plain, (segmentP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_180]), ['final']).
% 297.92/145.42  cnf(i_0_358, plain, (rearsegP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 297.92/145.42  cnf(i_0_359, plain, (frontsegP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_182]), ['final']).
% 297.92/145.42  cnf(i_0_360, plain, (ssList(esk47_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_183]), ['final']).
% 297.92/145.42  cnf(i_0_361, plain, (ssList(esk44_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 297.92/145.42  cnf(i_0_362, plain, (nil=X1|ssList(tl(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_184]), ['final']).
% 297.92/145.42  cnf(i_0_363, plain, (ssItem(esk46_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_185]), ['final']).
% 297.92/145.42  cnf(i_0_364, plain, (ssItem(esk45_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 297.92/145.42  cnf(i_0_365, plain, (nil=X1|ssItem(hd(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_186]), ['final']).
% 297.92/145.42  cnf(i_0_366, plain, (tl(X1)=esk47_1(X1)|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_183]), ['final']).
% 297.92/145.42  cnf(i_0_367, plain, (hd(X1)=esk46_1(X1)|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_185]), ['final']).
% 297.92/145.42  cnf(i_0_368, plain, (~singletonP(nil)), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 297.92/145.42  cnf(i_0_369, plain, (equalelemsP(nil)), inference(split_conjunct,[status(thm)],[ax74]), ['final']).
% 297.92/145.42  cnf(i_0_370, plain, (duplicatefreeP(nil)), inference(split_conjunct,[status(thm)],[ax72]), ['final']).
% 297.92/145.42  cnf(i_0_371, plain, (strictorderedP(nil)), inference(split_conjunct,[status(thm)],[ax69]), ['final']).
% 297.92/145.42  cnf(i_0_372, plain, (totalorderedP(nil)), inference(split_conjunct,[status(thm)],[ax66]), ['final']).
% 297.92/145.42  cnf(i_0_373, plain, (strictorderP(nil)), inference(split_conjunct,[status(thm)],[ax64]), ['final']).
% 297.92/145.42  cnf(i_0_374, plain, (totalorderP(nil)), inference(split_conjunct,[status(thm)],[ax62]), ['final']).
% 297.92/145.42  cnf(i_0_375, plain, (cyclefreeP(nil)), inference(split_conjunct,[status(thm)],[ax60]), ['final']).
% 297.92/145.42  cnf(i_0_376, negated_conjecture, (ssList(esk51_0)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_377, negated_conjecture, (ssList(esk50_0)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_378, negated_conjecture, (ssList(esk49_0)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_379, negated_conjecture, (ssList(esk48_0)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_380, plain, (ssList(nil)), inference(split_conjunct,[status(thm)],[ax17]), ['final']).
% 297.92/145.42  cnf(i_0_381, plain, (ssItem(esk2_0)), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 297.92/145.42  cnf(i_0_382, plain, (ssItem(esk1_0)), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 297.92/145.42  cnf(i_0_383, negated_conjecture, (nil!=esk48_0), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_384, plain, (esk1_0!=esk2_0), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 297.92/145.42  cnf(i_0_385, negated_conjecture, (esk49_0=esk51_0), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_386, negated_conjecture, (esk48_0=esk50_0), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_387, negated_conjecture, (nil=esk49_0), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 297.92/145.42  cnf(i_0_388, axiom, (X1=X1)).
% 297.92/145.42  cnf(i_0_389, axiom, (X1=X2|X2!=X1)).
% 297.92/145.42  cnf(i_0_390, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 297.92/145.42  cnf(i_0_391, axiom, (X1!=X2|app(X1,X3)=app(X2,X3))).
% 297.92/145.42  cnf(i_0_392, axiom, (X1!=X2|app(X3,X1)=app(X3,X2))).
% 297.92/145.42  cnf(i_0_393, axiom, (X1!=X2|cons(X1,X3)=cons(X2,X3))).
% 297.92/145.42  cnf(i_0_394, axiom, (X1!=X2|cons(X3,X1)=cons(X3,X2))).
% 297.92/145.42  cnf(i_0_395, axiom, (X1!=X2|esk40_1(X1)=esk40_1(X2))).
% 297.92/145.42  cnf(i_0_396, axiom, (X1!=X2|esk41_1(X1)=esk41_1(X2))).
% 297.92/145.42  cnf(i_0_397, axiom, (X1!=X2|hd(X1)=hd(X2))).
% 297.92/145.42  cnf(i_0_398, axiom, (X1!=X2|tl(X1)=tl(X2))).
% 297.92/145.42  cnf(i_0_399, axiom, (X1!=X2|esk47_1(X1)=esk47_1(X2))).
% 297.92/145.42  cnf(i_0_400, axiom, (X1!=X2|esk35_1(X1)=esk35_1(X2))).
% 297.92/145.42  cnf(i_0_401, axiom, (X1!=X2|esk46_1(X1)=esk46_1(X2))).
% 297.92/145.42  cnf(i_0_402, axiom, (X1!=X2|esk36_1(X1)=esk36_1(X2))).
% 297.92/145.42  cnf(i_0_403, axiom, (X1!=X2|~memberP(X1,X3)|memberP(X2,X3))).
% 297.92/145.42  cnf(i_0_404, axiom, (X1!=X2|~memberP(X3,X1)|memberP(X3,X2))).
% 297.92/145.42  cnf(i_0_405, axiom, (X1!=X2|~strictorderedP(X1)|strictorderedP(X2))).
% 297.92/145.42  cnf(i_0_406, axiom, (X1!=X2|~totalorderedP(X1)|totalorderedP(X2))).
% 297.92/145.42  cnf(i_0_407, axiom, (X1!=X2|~duplicatefreeP(X1)|duplicatefreeP(X2))).
% 297.92/145.42  cnf(i_0_408, axiom, (X1!=X2|~equalelemsP(X1)|equalelemsP(X2))).
% 297.92/145.42  cnf(i_0_409, axiom, (X1!=X2|~frontsegP(X1,X3)|frontsegP(X2,X3))).
% 297.92/145.42  cnf(i_0_410, axiom, (X1!=X2|~frontsegP(X3,X1)|frontsegP(X3,X2))).
% 297.92/145.42  cnf(i_0_411, axiom, (X1!=X2|~rearsegP(X1,X3)|rearsegP(X2,X3))).
% 297.92/145.42  cnf(i_0_412, axiom, (X1!=X2|~rearsegP(X3,X1)|rearsegP(X3,X2))).
% 297.92/145.42  cnf(i_0_413, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 297.92/145.42  cnf(i_0_414, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 297.92/145.42  cnf(i_0_415, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 297.92/145.42  cnf(i_0_416, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 297.92/145.43  cnf(i_0_417, axiom, (X1!=X2|~neq(X1,X3)|neq(X2,X3))).
% 297.92/145.43  cnf(i_0_418, axiom, (X1!=X2|~neq(X3,X1)|neq(X3,X2))).
% 297.92/145.43  cnf(i_0_419, axiom, (X1!=X2|~singletonP(X1)|singletonP(X2))).
% 297.92/145.43  cnf(i_0_420, axiom, (X1!=X2|~ssList(X1)|ssList(X2))).
% 297.92/145.43  cnf(i_0_421, axiom, (X1!=X2|~segmentP(X1,X3)|segmentP(X2,X3))).
% 297.92/145.43  cnf(i_0_422, axiom, (X1!=X2|~segmentP(X3,X1)|segmentP(X3,X2))).
% 297.92/145.43  cnf(i_0_423, axiom, (X1!=X2|~ssItem(X1)|ssItem(X2))).
% 297.92/145.43  cnf(i_0_424, axiom, (X1!=X2|~cyclefreeP(X1)|cyclefreeP(X2))).
% 297.92/145.43  cnf(i_0_425, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 297.92/145.43  cnf(i_0_426, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 297.92/145.43  cnf(i_0_427, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 297.92/145.43  cnf(i_0_428, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 297.92/145.43  cnf(i_0_429, axiom, (X1!=X2|~strictorderP(X1)|strictorderP(X2))).
% 297.92/145.43  cnf(i_0_430, axiom, (X1!=X2|~totalorderP(X1)|totalorderP(X2))).
% 300.02/147.50  Terminated
%------------------------------------------------------------------------------