CSE_E---1.7.TMO-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : SWC066+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 : n024.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 05:18:07 PM UTC 2026

% Result   : Timeout 288.04s 144.84s
% Output   : None 
% Verified : 
% SZS Type : -

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