↑ Up

CSE_E---1.7.THM-CRf.s

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

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

% Result   : Theorem 0.40s 1.62s
% Output   : CNFRefutation 0.84s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : SWC040+1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12  % Command    : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33  % Computer : n004.cluster.edu
% 0.16/0.33  % Model    : x86_64 x86_64
% 0.16/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33  % Memory   : 8042.1875MB
% 0.16/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33  % CPULimit   : 300
% 0.16/0.33  % WCLimit    : 300
% 0.16/0.33  % DateTime   : Tue May  5 04:17:47 EDT 2026
% 0.16/0.33  % CPUTime    : 
% 0.16/0.34  % start to proof: theBenchmark
% 0.40/1.62  % Version  : CSE_E---1.7
% 0.40/1.62  % Problem  : theBenchmark.p
% 0.40/1.62  % SZS status Theorem for theBenchmark.p
% 0.40/1.62  % SZS output start CNFRefutation
% 0.40/1.62  fof(ax94, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)=>~(gt(X2,X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax94)).
% 0.40/1.62  fof(ax33, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)=>~(lt(X2,X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax33)).
% 0.40/1.62  fof(co1, conjecture, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(nil!=X2|X2!=X4|X1!=X3|nil=X1|(nil!=X3&nil=X4)|(![X5]:(ssItem(X5)=>![X6]:(ssList(X6)=>(app(cons(X5,nil),X6)!=X3|app(X6,cons(X5,nil))!=X4)))&neq(X4,nil))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.40/1.62  fof(ax90, axiom, ![X1]:(ssItem(X1)=>~(lt(X1,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax90)).
% 0.40/1.62  fof(ax38, axiom, ![X1]:(ssItem(X1)=>~(memberP(nil,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax38)).
% 0.40/1.62  fof(ax8, axiom, ![X1]:(ssList(X1)=>(cyclefreeP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>~((leq(X2,X3)&leq(X3,X2))))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax8)).
% 0.40/1.62  fof(ax10, axiom, ![X1]:(ssList(X1)=>(strictorderP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>(lt(X2,X3)|lt(X3,X2)))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax10)).
% 0.40/1.62  fof(ax9, axiom, ![X1]:(ssList(X1)=>(totalorderP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>(leq(X2,X3)|leq(X3,X2)))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax9)).
% 0.40/1.62  fof(ax12, axiom, ![X1]:(ssList(X1)=>(strictorderedP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>lt(X2,X3))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax12)).
% 0.40/1.62  fof(ax11, axiom, ![X1]:(ssList(X1)=>(totalorderedP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>leq(X2,X3))))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax11)).
% 0.40/1.62  fof(ax13, axiom, ![X1]:(ssList(X1)=>(duplicatefreeP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>![X6]:(ssList(X6)=>(app(app(X4,cons(X2,X5)),cons(X3,X6))=X1=>X2!=X3)))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax13)).
% 0.40/1.62  fof(ax14, axiom, ![X1]:(ssList(X1)=>(equalelemsP(X1)<=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssList(X4)=>![X5]:(ssList(X5)=>(app(X4,cons(X2,cons(X3,X5)))=X1=>X2=X3))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax14)).
% 0.40/1.62  fof(ax7, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(segmentP(X1,X2)<=>?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(app(X3,X2),X4)=X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax7)).
% 0.40/1.62  fof(ax3, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>(memberP(X1,X2)<=>?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(X3,cons(X2,X4))=X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax3)).
% 0.40/1.62  fof(ax44, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(frontsegP(cons(X1,X3),cons(X2,X4))<=>(X1=X2&frontsegP(X3,X4))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax44)).
% 0.40/1.62  fof(ax56, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(segmentP(X1,X2)=>segmentP(app(app(X3,X1),X4),X2)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax56)).
% 0.40/1.62  fof(ax36, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(memberP(app(X2,X3),X1)<=>(memberP(X2,X1)|memberP(X3,X1)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax36)).
% 0.40/1.62  fof(ax37, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssList(X3)=>(memberP(cons(X2,X3),X1)<=>(X1=X2|memberP(X3,X1)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax37)).
% 0.40/1.62  fof(ax82, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>app(app(X1,X2),X3)=app(X1,app(X2,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax82)).
% 0.40/1.62  fof(ax27, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssItem(X3)=>cons(X3,app(X2,X1))=app(cons(X3,X2),X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax27)).
% 0.40/1.62  fof(ax70, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssList(X2)=>(strictorderedP(cons(X1,X2))<=>(nil=X2|((nil!=X2&strictorderedP(X2))&lt(X1,hd(X2))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax70)).
% 0.40/1.62  fof(ax67, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssList(X2)=>(totalorderedP(cons(X1,X2))<=>(nil=X2|((nil!=X2&totalorderedP(X2))&leq(X1,hd(X2))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax67)).
% 0.40/1.62  fof(ax50, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(rearsegP(X1,X2)=>rearsegP(app(X3,X1),X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax50)).
% 0.40/1.62  fof(ax43, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(frontsegP(X1,X2)=>frontsegP(app(X1,X3),X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax43)).
% 0.40/1.62  fof(ax95, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((gt(X1,X2)&gt(X2,X3))=>gt(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax95)).
% 0.40/1.62  fof(ax88, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((geq(X1,X2)&geq(X2,X3))=>geq(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax88)).
% 0.40/1.62  fof(ax34, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((lt(X1,X2)&lt(X2,X3))=>lt(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax34)).
% 0.40/1.62  fof(ax91, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((leq(X1,X2)&lt(X2,X3))=>lt(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax91)).
% 0.40/1.62  fof(ax30, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssItem(X3)=>((leq(X1,X2)&leq(X2,X3))=>leq(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax30)).
% 0.40/1.62  fof(ax53, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((segmentP(X1,X2)&segmentP(X2,X3))=>segmentP(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax53)).
% 0.40/1.62  fof(ax47, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((rearsegP(X1,X2)&rearsegP(X2,X3))=>rearsegP(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax47)).
% 0.40/1.62  fof(ax40, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((frontsegP(X1,X2)&frontsegP(X2,X3))=>frontsegP(X1,X3))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax40)).
% 0.40/1.62  fof(ax6, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(rearsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X3,X2)=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax6)).
% 0.40/1.62  fof(ax5, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(frontsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X2,X3)=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax5)).
% 0.40/1.62  fof(ax19, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssItem(X3)=>![X4]:(ssItem(X4)=>(cons(X3,X1)=cons(X4,X2)=>(X3=X4&X2=X1)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax19)).
% 0.40/1.62  fof(ax79, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X3,X2)=app(X1,X2)=>X3=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax79)).
% 0.40/1.62  fof(ax80, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X2,X3)=app(X2,X1)=>X3=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax80)).
% 0.40/1.62  fof(ax86, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil!=X1=>tl(app(X1,X2))=app(tl(X1),X2)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax86)).
% 0.40/1.62  fof(ax81, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>cons(X2,X1)=app(cons(X2,nil),X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax81)).
% 0.40/1.62  fof(ax54, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((segmentP(X1,X2)&segmentP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax54)).
% 0.40/1.62  fof(ax48, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((rearsegP(X1,X2)&rearsegP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax48)).
% 0.40/1.62  fof(ax41, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((frontsegP(X1,X2)&frontsegP(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax41)).
% 0.40/1.62  fof(ax87, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>((geq(X1,X2)&geq(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax87)).
% 0.40/1.62  fof(ax29, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>((leq(X1,X2)&leq(X2,X1))=>X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax29)).
% 0.40/1.62  fof(ax93, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)<=>(X1!=X2&leq(X1,X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax93)).
% 0.40/1.62  fof(ax92, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(leq(X1,X2)=>(X1=X2|lt(X1,X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax92)).
% 0.40/1.62  fof(ax35, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)<=>lt(X2,X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax35)).
% 0.40/1.62  fof(ax32, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(geq(X1,X2)<=>leq(X2,X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax32)).
% 0.40/1.62  fof(ax85, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil!=X1=>hd(app(X1,X2))=hd(X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax85)).
% 0.40/1.62  fof(ax77, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((((nil!=X2&nil!=X1)&hd(X2)=hd(X1))&tl(X2)=tl(X1))=>X2=X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax77)).
% 0.40/1.62  fof(ax25, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>tl(cons(X2,X1))=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax25)).
% 0.40/1.62  fof(ax23, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>hd(cons(X2,X1))=X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax23)).
% 0.40/1.62  fof(ax26, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>ssList(app(X1,X2)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax26)).
% 0.40/1.62  fof(ax16, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>ssList(cons(X2,X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax16)).
% 0.40/1.62  fof(ax15, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(neq(X1,X2)<=>X1!=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax15)).
% 0.40/1.62  fof(ax1, axiom, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(neq(X1,X2)<=>X1!=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax1)).
% 0.40/1.62  fof(ax4, axiom, ![X1]:(ssList(X1)=>(singletonP(X1)<=>?[X2]:(ssItem(X2)&cons(X2,nil)=X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax4)).
% 0.40/1.62  fof(ax83, axiom, ![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(nil=app(X1,X2)<=>(nil=X2&nil=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax83)).
% 0.40/1.62  fof(ax18, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>cons(X2,X1)!=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax18)).
% 0.40/1.62  fof(ax21, axiom, ![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>nil!=cons(X2,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax21)).
% 0.40/1.62  fof(ax20, axiom, ![X1]:(ssList(X1)=>(nil=X1|?[X2]:(ssList(X2)&?[X3]:(ssItem(X3)&cons(X3,X2)=X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax20)).
% 0.40/1.62  fof(ax78, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>cons(hd(X1),tl(X1))=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax78)).
% 0.40/1.62  fof(ax73, axiom, ![X1]:(ssItem(X1)=>equalelemsP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax73)).
% 0.40/1.62  fof(ax71, axiom, ![X1]:(ssItem(X1)=>duplicatefreeP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax71)).
% 0.40/1.62  fof(ax68, axiom, ![X1]:(ssItem(X1)=>strictorderedP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax68)).
% 0.40/1.62  fof(ax65, axiom, ![X1]:(ssItem(X1)=>totalorderedP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax65)).
% 0.40/1.62  fof(ax63, axiom, ![X1]:(ssItem(X1)=>strictorderP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax63)).
% 0.40/1.62  fof(ax61, axiom, ![X1]:(ssItem(X1)=>totalorderP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax61)).
% 0.40/1.62  fof(ax59, axiom, ![X1]:(ssItem(X1)=>cyclefreeP(cons(X1,nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax59)).
% 0.40/1.62  fof(ax58, axiom, ![X1]:(ssList(X1)=>(segmentP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax58)).
% 0.40/1.62  fof(ax52, axiom, ![X1]:(ssList(X1)=>(rearsegP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax52)).
% 0.40/1.62  fof(ax46, axiom, ![X1]:(ssList(X1)=>(frontsegP(nil,X1)<=>nil=X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax46)).
% 0.40/1.62  fof(ax89, axiom, ![X1]:(ssItem(X1)=>geq(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax89)).
% 0.40/1.62  fof(ax31, axiom, ![X1]:(ssItem(X1)=>leq(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax31)).
% 0.40/1.62  fof(ax55, axiom, ![X1]:(ssList(X1)=>segmentP(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax55)).
% 0.40/1.62  fof(ax49, axiom, ![X1]:(ssList(X1)=>rearsegP(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax49)).
% 0.40/1.62  fof(ax42, axiom, ![X1]:(ssList(X1)=>frontsegP(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax42)).
% 0.40/1.62  fof(ax28, axiom, ![X1]:(ssList(X1)=>app(nil,X1)=X1), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax28)).
% 0.40/1.62  fof(ax84, axiom, ![X1]:(ssList(X1)=>app(X1,nil)=X1), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax84)).
% 0.40/1.62  fof(ax57, axiom, ![X1]:(ssList(X1)=>segmentP(X1,nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax57)).
% 0.40/1.62  fof(ax51, axiom, ![X1]:(ssList(X1)=>rearsegP(X1,nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax51)).
% 0.40/1.62  fof(ax45, axiom, ![X1]:(ssList(X1)=>frontsegP(X1,nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax45)).
% 0.40/1.62  fof(ax76, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>?[X2]:(ssList(X2)&tl(X1)=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax76)).
% 0.40/1.62  fof(ax24, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>ssList(tl(X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax24)).
% 0.40/1.62  fof(ax75, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>?[X2]:(ssItem(X2)&hd(X1)=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax75)).
% 0.40/1.62  fof(ax22, axiom, ![X1]:(ssList(X1)=>(nil!=X1=>ssItem(hd(X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax22)).
% 0.40/1.62  fof(ax39, axiom, ~(singletonP(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax39)).
% 0.40/1.62  fof(ax2, axiom, ?[X1]:(ssItem(X1)&?[X2]:(ssItem(X2)&X1!=X2)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax2)).
% 0.40/1.62  fof(ax74, axiom, equalelemsP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax74)).
% 0.40/1.62  fof(ax72, axiom, duplicatefreeP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax72)).
% 0.40/1.62  fof(ax69, axiom, strictorderedP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax69)).
% 0.40/1.62  fof(ax66, axiom, totalorderedP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax66)).
% 0.40/1.62  fof(ax64, axiom, strictorderP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax64)).
% 0.40/1.62  fof(ax62, axiom, totalorderP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax62)).
% 0.40/1.62  fof(ax60, axiom, cyclefreeP(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax60)).
% 0.40/1.62  fof(ax17, axiom, ssList(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax17)).
% 0.40/1.62  fof(i_0_96, plain, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(gt(X1,X2)=>~gt(X2,X1)))), inference(fof_simplification,[status(thm)],[ax94])).
% 0.40/1.62  fof(i_0_97, plain, ![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>(lt(X1,X2)=>~lt(X2,X1)))), inference(fof_simplification,[status(thm)],[ax33])).
% 0.40/1.62  fof(i_0_98, negated_conjecture, ~(![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(nil!=X2|X2!=X4|X1!=X3|nil=X1|(nil!=X3&nil=X4)|(![X5]:(ssItem(X5)=>![X6]:(ssList(X6)=>(app(cons(X5,nil),X6)!=X3|app(X6,cons(X5,nil))!=X4)))&neq(X4,nil)))))))), inference(assume_negation,[status(cth)],[co1])).
% 0.40/1.62  fof(i_0_99, plain, ![X1]:(ssItem(X1)=>~lt(X1,X1)), inference(fof_simplification,[status(thm)],[ax90])).
% 0.40/1.62  fof(i_0_100, plain, ![X1]:(ssItem(X1)=>~memberP(nil,X1)), inference(fof_simplification,[status(thm)],[ax38])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  fof(i_0_130, 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])])])])).
% 0.40/1.62  fof(i_0_131, 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])])])).
% 0.40/1.62  fof(i_0_132, 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])])])).
% 0.40/1.62  fof(i_0_133, 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])])])).
% 0.40/1.62  fof(i_0_134, 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])])])).
% 0.40/1.62  fof(i_0_135, 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])])])).
% 0.40/1.62  fof(i_0_136, 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])])])).
% 0.40/1.62  fof(i_0_137, 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])])])).
% 0.40/1.62  fof(i_0_138, 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])])])).
% 0.40/1.62  fof(i_0_139, 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])])])).
% 0.40/1.62  fof(i_0_140, 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_96])])])).
% 0.40/1.62  fof(i_0_141, 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_97])])])).
% 0.40/1.62  fof(i_0_142, 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])])])])).
% 0.40/1.62  fof(i_0_143, 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])])])).
% 0.40/1.62  fof(i_0_144, 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])])])])).
% 0.40/1.62  fof(i_0_145, 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])])])])).
% 0.40/1.62  fof(i_0_146, negated_conjecture, (ssList(esk48_0)&(ssList(esk49_0)&(ssList(esk50_0)&(ssList(esk51_0)&(((((nil=esk49_0&esk49_0=esk51_0)&esk48_0=esk50_0)&nil!=esk48_0)&(nil=esk50_0|nil!=esk51_0))&((ssItem(esk52_0)|~neq(esk51_0,nil))&((ssList(esk53_0)|~neq(esk51_0,nil))&((app(cons(esk52_0,nil),esk53_0)=esk50_0|~neq(esk51_0,nil))&(app(esk53_0,cons(esk52_0,nil))=esk51_0|~neq(esk51_0,nil)))))))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_98])])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  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])])).
% 0.40/1.62  fof(i_0_161, plain, ![X415]:(~ssItem(X415)|equalelemsP(cons(X415,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax73])])).
% 0.40/1.62  fof(i_0_162, plain, ![X414]:(~ssItem(X414)|duplicatefreeP(cons(X414,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax71])])).
% 0.40/1.62  fof(i_0_163, plain, ![X411]:(~ssItem(X411)|strictorderedP(cons(X411,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax68])])).
% 0.40/1.62  fof(i_0_164, plain, ![X408]:(~ssItem(X408)|totalorderedP(cons(X408,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax65])])).
% 0.40/1.62  fof(i_0_165, plain, ![X407]:(~ssItem(X407)|strictorderP(cons(X407,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax63])])).
% 0.40/1.62  fof(i_0_166, plain, ![X406]:(~ssItem(X406)|totalorderP(cons(X406,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax61])])).
% 0.40/1.62  fof(i_0_167, plain, ![X405]:(~ssItem(X405)|cyclefreeP(cons(X405,nil))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax59])])).
% 0.40/1.62  fof(i_0_168, plain, ![X447]:(~ssItem(X447)|~lt(X447,X447)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_99])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  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])])])).
% 0.40/1.62  fof(i_0_172, plain, ![X366]:(~ssItem(X366)|~memberP(nil,X366)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_100])])).
% 0.40/1.62  fof(i_0_173, plain, ![X446]:(~ssItem(X446)|geq(X446,X446)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax89])])).
% 0.40/1.62  fof(i_0_174, plain, ![X350]:(~ssItem(X350)|leq(X350,X350)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax31])])).
% 0.40/1.62  fof(i_0_175, plain, ![X398]:(~ssList(X398)|segmentP(X398,X398)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax55])])).
% 0.40/1.62  fof(i_0_176, plain, ![X387]:(~ssList(X387)|rearsegP(X387,X387)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax49])])).
% 0.40/1.62  fof(i_0_177, plain, ![X372]:(~ssList(X372)|frontsegP(X372,X372)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax42])])).
% 0.40/1.62  fof(i_0_178, plain, ![X344]:(~ssList(X344)|app(nil,X344)=X344), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax28])])).
% 0.40/1.62  fof(i_0_179, plain, ![X436]:(~ssList(X436)|app(X436,nil)=X436), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax84])])).
% 0.40/1.62  fof(i_0_180, plain, ![X403]:(~ssList(X403)|segmentP(X403,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax57])])).
% 0.40/1.62  fof(i_0_181, plain, ![X391]:(~ssList(X391)|rearsegP(X391,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax51])])).
% 0.40/1.62  fof(i_0_182, plain, ![X380]:(~ssList(X380)|frontsegP(X380,nil)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax45])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  fof(i_0_184, plain, ![X336]:(~ssList(X336)|(nil=X336|ssList(tl(X336)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax24])])).
% 0.40/1.62  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])])])])).
% 0.40/1.62  fof(i_0_186, plain, ![X333]:(~ssList(X333)|(nil=X333|ssItem(hd(X333)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax22])])).
% 0.40/1.62  fof(i_0_187, plain, ~singletonP(nil), inference(fof_simplification,[status(thm)],[ax39])).
% 0.40/1.62  fof(i_0_188, plain, (ssItem(esk1_0)&(ssItem(esk2_0)&esk1_0!=esk2_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[ax2])])).
% 0.40/1.62  cnf(i_0_189, plain, (~cyclefreeP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~leq(X2,X3)|~leq(X3,X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_190, plain, (lt(X2,X3)|lt(X3,X2)|~strictorderP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_191, plain, (leq(X2,X3)|leq(X3,X2)|~totalorderP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_192, plain, (lt(X2,X3)|~strictorderedP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_193, plain, (leq(X2,X3)|~totalorderedP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_194, plain, (~duplicatefreeP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|~ssList(X6)|app(app(X4,cons(X2,X5)),cons(X3,X6))!=X1|X2!=X3|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_195, plain, (app(app(esk37_1(X1),cons(esk35_1(X1),esk38_1(X1))),cons(esk36_1(X1),esk39_1(X1)))=X1|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_196, plain, (app(app(esk32_1(X1),cons(esk30_1(X1),esk33_1(X1))),cons(esk31_1(X1),esk34_1(X1)))=X1|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_197, plain, (app(app(esk27_1(X1),cons(esk25_1(X1),esk28_1(X1))),cons(esk26_1(X1),esk29_1(X1)))=X1|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_198, plain, (app(app(esk22_1(X1),cons(esk20_1(X1),esk23_1(X1))),cons(esk21_1(X1),esk24_1(X1)))=X1|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_199, plain, (app(app(esk17_1(X1),cons(esk15_1(X1),esk18_1(X1))),cons(esk16_1(X1),esk19_1(X1)))=X1|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_200, plain, (app(app(esk12_1(X1),cons(esk10_1(X1),esk13_1(X1))),cons(esk11_1(X1),esk14_1(X1)))=X1|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_201, plain, (X2=X3|~equalelemsP(X1)|~ssItem(X2)|~ssItem(X3)|~ssList(X4)|~ssList(X5)|app(X4,cons(X2,cons(X3,X5)))!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.40/1.62  cnf(i_0_202, plain, (app(esk42_1(X1),cons(esk40_1(X1),cons(esk41_1(X1),esk43_1(X1))))=X1|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.40/1.62  cnf(i_0_203, plain, (app(app(esk8_2(X1,X2),X2),esk9_2(X1,X2))=X1|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.40/1.62  cnf(i_0_204, plain, (app(esk3_2(X1,X2),cons(X2,esk4_2(X1,X2)))=X1|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.40/1.62  cnf(i_0_205, plain, (frontsegP(X1,X2)|~frontsegP(cons(X3,X1),cons(X4,X2))|~ssList(X2)|~ssList(X1)|~ssItem(X4)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 0.40/1.62  cnf(i_0_206, plain, (segmentP(app(app(X3,X1),X4),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~segmentP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.40/1.62  cnf(i_0_207, plain, (X1=X2|~frontsegP(cons(X1,X3),cons(X2,X4))|~ssList(X4)|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 0.40/1.62  cnf(i_0_208, plain, (frontsegP(cons(X1,X3),cons(X2,X4))|X1!=X2|~frontsegP(X3,X4)|~ssList(X4)|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 0.40/1.62  cnf(i_0_209, plain, (memberP(X1,X3)|memberP(X2,X3)|~memberP(app(X1,X2),X3)|~ssList(X2)|~ssList(X1)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.40/1.62  cnf(i_0_210, plain, (segmentP(X4,X3)|~ssList(X1)|~ssList(X2)|app(app(X1,X3),X2)!=X4|~ssList(X3)|~ssList(X4)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.40/1.62  cnf(i_0_211, plain, (memberP(X4,X3)|~ssList(X1)|~ssList(X2)|app(X1,cons(X3,X2))!=X4|~ssItem(X3)|~ssList(X4)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.40/1.62  cnf(i_0_212, plain, (X3=X1|memberP(X2,X3)|~memberP(cons(X1,X2),X3)|~ssList(X2)|~ssItem(X1)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.40/1.62  cnf(i_0_213, plain, (app(app(X1,X2),X3)=app(X1,app(X2,X3))|~ssList(X1)|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.40/1.62  cnf(i_0_214, plain, (cons(X3,app(X2,X1))=app(cons(X3,X2),X1)|~ssList(X1)|~ssList(X2)|~ssItem(X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.40/1.62  cnf(i_0_215, plain, (nil=X1|strictorderedP(cons(X2,X1))|~strictorderedP(X1)|~lt(X2,hd(X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.40/1.62  cnf(i_0_216, plain, (nil=X1|totalorderedP(cons(X2,X1))|~totalorderedP(X1)|~leq(X2,hd(X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.40/1.62  cnf(i_0_217, plain, (rearsegP(app(X3,X1),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~rearsegP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.40/1.62  cnf(i_0_218, plain, (frontsegP(app(X1,X3),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~frontsegP(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 0.40/1.62  cnf(i_0_219, plain, (memberP(app(X1,X3),X2)|~memberP(X1,X2)|~ssList(X3)|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.40/1.62  cnf(i_0_220, plain, (memberP(app(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssList(X3)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.40/1.62  cnf(i_0_221, plain, (memberP(cons(X3,X1),X2)|~memberP(X1,X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.40/1.62  cnf(i_0_222, plain, (lt(X1,hd(X2))|nil=X2|~strictorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.40/1.62  cnf(i_0_223, plain, (leq(X1,hd(X2))|nil=X2|~totalorderedP(cons(X1,X2))|~ssList(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.40/1.62  cnf(i_0_224, plain, (gt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~gt(X1,X2)|~gt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.40/1.62  cnf(i_0_225, plain, (geq(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~geq(X1,X2)|~geq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 0.40/1.62  cnf(i_0_226, plain, (lt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~lt(X1,X2)|~lt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.40/1.62  cnf(i_0_227, plain, (lt(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~leq(X1,X2)|~lt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.40/1.62  cnf(i_0_228, plain, (leq(X1,X3)|~ssItem(X1)|~ssItem(X2)|~ssItem(X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_124]), ['final']).
% 0.40/1.62  cnf(i_0_229, plain, (segmentP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~segmentP(X1,X2)|~segmentP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_125]), ['final']).
% 0.40/1.62  cnf(i_0_230, plain, (rearsegP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~rearsegP(X1,X2)|~rearsegP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_126]), ['final']).
% 0.40/1.62  cnf(i_0_231, plain, (frontsegP(X1,X3)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~frontsegP(X1,X2)|~frontsegP(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_127]), ['final']).
% 0.40/1.62  cnf(i_0_232, plain, (app(esk7_2(X1,X2),X2)=X1|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.40/1.62  cnf(i_0_233, plain, (app(X1,esk6_2(X2,X1))=X2|~frontsegP(X2,X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 0.40/1.62  cnf(i_0_234, plain, (X1=X2|cons(X1,X3)!=cons(X2,X4)|~ssItem(X2)|~ssItem(X1)|~ssList(X4)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 0.40/1.62  cnf(i_0_235, plain, (X1=X2|cons(X3,X2)!=cons(X4,X1)|~ssItem(X4)|~ssItem(X3)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 0.40/1.62  cnf(i_0_236, plain, (strictorderedP(X1)|nil=X1|~strictorderedP(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.40/1.62  cnf(i_0_237, plain, (totalorderedP(X1)|nil=X1|~totalorderedP(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.40/1.62  cnf(i_0_238, plain, (X3=X1|~ssList(X1)|~ssList(X2)|~ssList(X3)|app(X3,X2)!=app(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_131]), ['final']).
% 0.40/1.62  cnf(i_0_239, plain, (X3=X1|~ssList(X1)|~ssList(X2)|~ssList(X3)|app(X2,X3)!=app(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_132]), ['final']).
% 0.40/1.62  cnf(i_0_240, plain, (ssList(esk9_2(X1,X2))|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.40/1.62  cnf(i_0_241, plain, (ssList(esk8_2(X1,X2))|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.40/1.62  cnf(i_0_242, plain, (ssList(esk7_2(X1,X2))|~rearsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.40/1.62  cnf(i_0_243, plain, (ssList(esk6_2(X1,X2))|~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 0.40/1.62  cnf(i_0_244, plain, (ssList(esk4_2(X1,X2))|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.40/1.62  cnf(i_0_245, plain, (ssList(esk3_2(X1,X2))|~memberP(X1,X2)|~ssItem(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_109]), ['final']).
% 0.40/1.62  cnf(i_0_246, plain, (nil=X1|tl(app(X1,X2))=app(tl(X1),X2)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_133]), ['final']).
% 0.40/1.62  cnf(i_0_247, plain, (memberP(cons(X2,X3),X1)|X1!=X2|~ssList(X3)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.40/1.62  cnf(i_0_248, plain, (cons(X2,X1)=app(cons(X2,nil),X1)|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_134]), ['final']).
% 0.40/1.62  cnf(i_0_249, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~segmentP(X1,X2)|~segmentP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_135]), ['final']).
% 0.40/1.62  cnf(i_0_250, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)|~rearsegP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_136]), ['final']).
% 0.40/1.62  cnf(i_0_251, plain, (X1=X2|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)|~frontsegP(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_137]), ['final']).
% 0.40/1.62  cnf(i_0_252, plain, (X1=X2|~ssItem(X1)|~ssItem(X2)|~geq(X1,X2)|~geq(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_138]), ['final']).
% 0.40/1.62  cnf(i_0_253, plain, (X1=X2|~ssItem(X1)|~ssItem(X2)|~leq(X1,X2)|~leq(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_139]), ['final']).
% 0.40/1.62  cnf(i_0_254, plain, (rearsegP(X3,X2)|~ssList(X1)|app(X1,X2)!=X3|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.40/1.62  cnf(i_0_255, plain, (frontsegP(X3,X2)|~ssList(X1)|app(X2,X1)!=X3|~ssList(X2)|~ssList(X3)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 0.40/1.62  cnf(i_0_256, plain, (~ssItem(X1)|~ssItem(X2)|~gt(X1,X2)|~gt(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_140]), ['final']).
% 0.40/1.62  cnf(i_0_257, plain, (~ssItem(X1)|~ssItem(X2)|~lt(X1,X2)|~lt(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.40/1.62  cnf(i_0_258, plain, (X1=X2|lt(X1,X2)|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.40/1.62  cnf(i_0_259, plain, (X1=X2|lt(X1,X2)|~ssItem(X1)|~ssItem(X2)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_143]), ['final']).
% 0.40/1.62  cnf(i_0_260, plain, (strictorderedP(X1)|~lt(esk30_1(X1),esk31_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_261, plain, (totalorderedP(X1)|~leq(esk25_1(X1),esk26_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_262, plain, (strictorderP(X1)|~lt(esk21_1(X1),esk20_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_263, plain, (strictorderP(X1)|~lt(esk20_1(X1),esk21_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_264, plain, (totalorderP(X1)|~leq(esk16_1(X1),esk15_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_265, plain, (totalorderP(X1)|~leq(esk15_1(X1),esk16_1(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_266, plain, (gt(X2,X1)|~lt(X1,X2)|~ssItem(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_144]), ['final']).
% 0.40/1.62  cnf(i_0_267, plain, (geq(X2,X1)|~leq(X1,X2)|~ssItem(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_145]), ['final']).
% 0.40/1.62  cnf(i_0_268, plain, (lt(X2,X1)|~gt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_144]), ['final']).
% 0.40/1.62  cnf(i_0_269, plain, (leq(X1,X2)|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.40/1.62  cnf(i_0_270, plain, (leq(X2,X1)|~geq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_145]), ['final']).
% 0.40/1.62  cnf(i_0_271, negated_conjecture, (app(cons(esk52_0,nil),esk53_0)=esk50_0|~neq(esk51_0,nil)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_272, negated_conjecture, (app(esk53_0,cons(esk52_0,nil))=esk51_0|~neq(esk51_0,nil)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  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']).
% 0.40/1.62  cnf(i_0_274, plain, (strictorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.40/1.62  cnf(i_0_275, plain, (totalorderedP(cons(X2,X1))|nil!=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.40/1.62  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']).
% 0.40/1.62  cnf(i_0_277, plain, (tl(cons(X2,X1))=X1|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_149]), ['final']).
% 0.40/1.62  cnf(i_0_278, plain, (hd(cons(X2,X1))=X2|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_150]), ['final']).
% 0.40/1.62  cnf(i_0_279, plain, (ssList(app(X1,X2))|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_151]), ['final']).
% 0.40/1.62  cnf(i_0_280, plain, (ssList(cons(X2,X1))|~ssList(X1)|~ssItem(X2)), inference(split_conjunct,[status(thm)],[i_0_152]), ['final']).
% 0.40/1.62  cnf(i_0_281, plain, (~neq(X1,X2)|X1!=X2|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 0.40/1.62  cnf(i_0_282, plain, (X1!=X2|~lt(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.40/1.62  cnf(i_0_283, plain, (~neq(X1,X2)|X1!=X2|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 0.40/1.62  cnf(i_0_284, plain, (singletonP(X2)|~ssItem(X1)|cons(X1,nil)!=X2|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 0.40/1.62  cnf(i_0_285, plain, (nil=X1|nil!=app(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_156]), ['final']).
% 0.40/1.62  cnf(i_0_286, plain, (nil=X1|nil!=app(X2,X1)|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_156]), ['final']).
% 0.40/1.62  cnf(i_0_287, plain, (leq(esk11_1(X1),esk10_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_288, plain, (leq(esk10_1(X1),esk11_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_289, plain, (~ssList(X1)|~ssItem(X2)|cons(X2,X1)!=X1), inference(split_conjunct,[status(thm)],[i_0_157]), ['final']).
% 0.40/1.62  cnf(i_0_290, plain, (~ssList(X1)|~ssItem(X2)|nil!=cons(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 0.40/1.62  cnf(i_0_291, plain, (cons(esk45_1(X1),esk44_1(X1))=X1|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 0.40/1.62  cnf(i_0_292, plain, (nil=X1|cons(hd(X1),tl(X1))=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_160]), ['final']).
% 0.40/1.62  cnf(i_0_293, plain, (equalelemsP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_161]), ['final']).
% 0.40/1.62  cnf(i_0_294, plain, (duplicatefreeP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_162]), ['final']).
% 0.40/1.62  cnf(i_0_295, plain, (strictorderedP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_163]), ['final']).
% 0.40/1.62  cnf(i_0_296, plain, (totalorderedP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_164]), ['final']).
% 0.40/1.62  cnf(i_0_297, plain, (strictorderP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_165]), ['final']).
% 0.40/1.62  cnf(i_0_298, plain, (totalorderP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_166]), ['final']).
% 0.40/1.62  cnf(i_0_299, plain, (cyclefreeP(cons(X1,nil))|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_167]), ['final']).
% 0.40/1.62  cnf(i_0_300, plain, (cons(esk5_1(X1),nil)=X1|~singletonP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 0.40/1.62  cnf(i_0_301, plain, (nil=app(X2,X1)|nil!=X1|nil!=X2|~ssList(X1)|~ssList(X2)), inference(split_conjunct,[status(thm)],[i_0_156]), ['final']).
% 0.40/1.62  cnf(i_0_302, plain, (X1=X2|neq(X1,X2)|~ssList(X2)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 0.40/1.62  cnf(i_0_303, plain, (X1=X2|neq(X1,X2)|~ssItem(X2)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 0.40/1.62  cnf(i_0_304, plain, (~ssItem(X1)|~lt(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_168]), ['final']).
% 0.40/1.62  cnf(i_0_305, plain, (nil=X1|~segmentP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 0.40/1.62  cnf(i_0_306, plain, (nil=X1|~rearsegP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 0.40/1.62  cnf(i_0_307, plain, (nil=X1|~frontsegP(nil,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.40/1.62  cnf(i_0_308, plain, (~ssItem(X1)|~memberP(nil,X1)), inference(split_conjunct,[status(thm)],[i_0_172]), ['final']).
% 0.40/1.62  cnf(i_0_309, plain, (ssItem(esk5_1(X1))|~singletonP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 0.40/1.62  cnf(i_0_310, plain, (equalelemsP(X1)|esk40_1(X1)!=esk41_1(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.40/1.62  cnf(i_0_311, plain, (segmentP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 0.40/1.62  cnf(i_0_312, plain, (rearsegP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 0.40/1.62  cnf(i_0_313, plain, (frontsegP(nil,X1)|nil!=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.40/1.62  cnf(i_0_314, plain, (ssList(esk43_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.40/1.62  cnf(i_0_315, plain, (ssList(esk42_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.40/1.62  cnf(i_0_316, plain, (ssItem(esk41_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.40/1.62  cnf(i_0_317, plain, (ssItem(esk40_1(X1))|equalelemsP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.40/1.62  cnf(i_0_318, plain, (ssList(esk39_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_319, plain, (ssList(esk38_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_320, plain, (ssList(esk37_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_321, plain, (ssItem(esk36_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_322, plain, (ssItem(esk35_1(X1))|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_323, plain, (ssList(esk34_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_324, plain, (ssList(esk33_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_325, plain, (ssList(esk32_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_326, plain, (ssItem(esk31_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_327, plain, (ssItem(esk30_1(X1))|strictorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.40/1.62  cnf(i_0_328, plain, (ssList(esk29_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_329, plain, (ssList(esk28_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_330, plain, (ssList(esk27_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_331, plain, (ssItem(esk26_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_332, plain, (ssItem(esk25_1(X1))|totalorderedP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.40/1.62  cnf(i_0_333, plain, (ssList(esk24_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_334, plain, (ssList(esk23_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_335, plain, (ssList(esk22_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_336, plain, (ssItem(esk21_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_337, plain, (ssItem(esk20_1(X1))|strictorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_102]), ['final']).
% 0.40/1.62  cnf(i_0_338, plain, (ssList(esk19_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_339, plain, (ssList(esk18_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_340, plain, (ssList(esk17_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_341, plain, (ssItem(esk16_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_342, plain, (ssItem(esk15_1(X1))|totalorderP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_103]), ['final']).
% 0.40/1.62  cnf(i_0_343, plain, (ssList(esk14_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_344, plain, (ssList(esk13_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_345, plain, (ssList(esk12_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_346, plain, (ssItem(esk11_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_347, plain, (ssItem(esk10_1(X1))|cyclefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.40/1.62  cnf(i_0_348, plain, (geq(X1,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 0.40/1.62  cnf(i_0_349, plain, (leq(X1,X1)|~ssItem(X1)), inference(split_conjunct,[status(thm)],[i_0_174]), ['final']).
% 0.40/1.62  cnf(i_0_350, plain, (segmentP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_175]), ['final']).
% 0.40/1.62  cnf(i_0_351, plain, (rearsegP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_176]), ['final']).
% 0.40/1.62  cnf(i_0_352, plain, (frontsegP(X1,X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_177]), ['final']).
% 0.40/1.62  cnf(i_0_353, negated_conjecture, (ssList(esk53_0)|~neq(esk51_0,nil)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_354, negated_conjecture, (ssItem(esk52_0)|~neq(esk51_0,nil)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_355, plain, (app(nil,X1)=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_178]), ['final']).
% 0.40/1.62  cnf(i_0_356, plain, (app(X1,nil)=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_179]), ['final']).
% 0.40/1.62  cnf(i_0_357, plain, (esk35_1(X1)=esk36_1(X1)|duplicatefreeP(X1)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.40/1.62  cnf(i_0_358, plain, (segmentP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_180]), ['final']).
% 0.40/1.62  cnf(i_0_359, plain, (rearsegP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.40/1.62  cnf(i_0_360, plain, (frontsegP(X1,nil)|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_182]), ['final']).
% 0.40/1.62  cnf(i_0_361, plain, (ssList(esk47_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_183]), ['final']).
% 0.40/1.62  cnf(i_0_362, plain, (ssList(esk44_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 0.40/1.62  cnf(i_0_363, plain, (nil=X1|ssList(tl(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_184]), ['final']).
% 0.40/1.62  cnf(i_0_364, plain, (ssItem(esk46_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_185]), ['final']).
% 0.40/1.62  cnf(i_0_365, plain, (ssItem(esk45_1(X1))|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 0.40/1.62  cnf(i_0_366, plain, (nil=X1|ssItem(hd(X1))|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_186]), ['final']).
% 0.40/1.62  cnf(i_0_367, plain, (tl(X1)=esk47_1(X1)|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_183]), ['final']).
% 0.40/1.62  cnf(i_0_368, plain, (hd(X1)=esk46_1(X1)|nil=X1|~ssList(X1)), inference(split_conjunct,[status(thm)],[i_0_185]), ['final']).
% 0.40/1.62  cnf(i_0_369, plain, (~singletonP(nil)), inference(split_conjunct,[status(thm)],[i_0_187]), ['final']).
% 0.40/1.62  cnf(i_0_370, plain, (equalelemsP(nil)), inference(split_conjunct,[status(thm)],[ax74]), ['final']).
% 0.40/1.62  cnf(i_0_371, plain, (duplicatefreeP(nil)), inference(split_conjunct,[status(thm)],[ax72]), ['final']).
% 0.40/1.62  cnf(i_0_372, plain, (strictorderedP(nil)), inference(split_conjunct,[status(thm)],[ax69]), ['final']).
% 0.40/1.62  cnf(i_0_373, plain, (totalorderedP(nil)), inference(split_conjunct,[status(thm)],[ax66]), ['final']).
% 0.40/1.62  cnf(i_0_374, plain, (strictorderP(nil)), inference(split_conjunct,[status(thm)],[ax64]), ['final']).
% 0.40/1.62  cnf(i_0_375, plain, (totalorderP(nil)), inference(split_conjunct,[status(thm)],[ax62]), ['final']).
% 0.40/1.62  cnf(i_0_376, plain, (cyclefreeP(nil)), inference(split_conjunct,[status(thm)],[ax60]), ['final']).
% 0.40/1.62  cnf(i_0_377, negated_conjecture, (ssList(esk51_0)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_378, negated_conjecture, (ssList(esk50_0)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_379, negated_conjecture, (ssList(esk49_0)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_380, negated_conjecture, (ssList(esk48_0)), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_381, plain, (ssList(nil)), inference(split_conjunct,[status(thm)],[ax17]), ['final']).
% 0.40/1.62  cnf(i_0_382, plain, (ssItem(esk2_0)), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 0.40/1.62  cnf(i_0_383, plain, (ssItem(esk1_0)), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 0.40/1.62  cnf(i_0_384, negated_conjecture, (nil=esk50_0|nil!=esk51_0), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_385, negated_conjecture, (nil!=esk48_0), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_386, plain, (esk1_0!=esk2_0), inference(split_conjunct,[status(thm)],[i_0_188]), ['final']).
% 0.40/1.62  cnf(i_0_387, negated_conjecture, (esk49_0=esk51_0), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_388, negated_conjecture, (esk48_0=esk50_0), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_389, negated_conjecture, (nil=esk49_0), inference(split_conjunct,[status(thm)],[i_0_146]), ['final']).
% 0.40/1.62  cnf(i_0_390, axiom, (X1=X1)).
% 0.40/1.62  cnf(i_0_391, axiom, (X1=X2|X2!=X1)).
% 0.40/1.62  cnf(i_0_392, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.40/1.62  cnf(i_0_393, axiom, (X1!=X2|app(X1,X3)=app(X2,X3))).
% 0.40/1.62  cnf(i_0_394, axiom, (X1!=X2|app(X3,X1)=app(X3,X2))).
% 0.40/1.62  cnf(i_0_395, axiom, (X1!=X2|cons(X1,X3)=cons(X2,X3))).
% 0.40/1.62  cnf(i_0_396, axiom, (X1!=X2|cons(X3,X1)=cons(X3,X2))).
% 0.40/1.62  cnf(i_0_397, axiom, (X1!=X2|esk40_1(X1)=esk40_1(X2))).
% 0.40/1.62  cnf(i_0_398, axiom, (X1!=X2|esk41_1(X1)=esk41_1(X2))).
% 0.40/1.62  cnf(i_0_399, axiom, (X1!=X2|esk35_1(X1)=esk35_1(X2))).
% 0.40/1.62  cnf(i_0_400, axiom, (X1!=X2|hd(X1)=hd(X2))).
% 0.40/1.62  cnf(i_0_401, axiom, (X1!=X2|tl(X1)=tl(X2))).
% 0.40/1.62  cnf(i_0_402, axiom, (X1!=X2|esk47_1(X1)=esk47_1(X2))).
% 0.40/1.62  cnf(i_0_403, axiom, (X1!=X2|esk46_1(X1)=esk46_1(X2))).
% 0.40/1.62  cnf(i_0_404, axiom, (X1!=X2|esk36_1(X1)=esk36_1(X2))).
% 0.40/1.62  cnf(i_0_405, axiom, (X1!=X2|~cyclefreeP(X1)|cyclefreeP(X2))).
% 0.40/1.62  cnf(i_0_406, axiom, (X1!=X2|~duplicatefreeP(X1)|duplicatefreeP(X2))).
% 0.40/1.62  cnf(i_0_407, axiom, (X1!=X2|~equalelemsP(X1)|equalelemsP(X2))).
% 0.40/1.62  cnf(i_0_408, axiom, (X1!=X2|~segmentP(X1,X3)|segmentP(X2,X3))).
% 0.40/1.62  cnf(i_0_409, axiom, (X1!=X2|~segmentP(X3,X1)|segmentP(X3,X2))).
% 0.40/1.62  cnf(i_0_410, axiom, (X1!=X2|~memberP(X1,X3)|memberP(X2,X3))).
% 0.40/1.62  cnf(i_0_411, axiom, (X1!=X2|~memberP(X3,X1)|memberP(X3,X2))).
% 0.40/1.62  cnf(i_0_412, axiom, (X1!=X2|~frontsegP(X1,X3)|frontsegP(X2,X3))).
% 0.40/1.62  cnf(i_0_413, axiom, (X1!=X2|~frontsegP(X3,X1)|frontsegP(X3,X2))).
% 0.40/1.62  cnf(i_0_414, axiom, (X1!=X2|~rearsegP(X1,X3)|rearsegP(X2,X3))).
% 0.40/1.62  cnf(i_0_415, axiom, (X1!=X2|~rearsegP(X3,X1)|rearsegP(X3,X2))).
% 0.40/1.62  cnf(i_0_416, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.40/1.63  cnf(i_0_417, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.40/1.63  cnf(i_0_418, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.40/1.63  cnf(i_0_419, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.40/1.63  cnf(i_0_420, axiom, (X1!=X2|~neq(X1,X3)|neq(X2,X3))).
% 0.40/1.63  cnf(i_0_421, axiom, (X1!=X2|~neq(X3,X1)|neq(X3,X2))).
% 0.40/1.63  cnf(i_0_422, axiom, (X1!=X2|~singletonP(X1)|singletonP(X2))).
% 0.40/1.63  cnf(i_0_423, axiom, (X1!=X2|~ssItem(X1)|ssItem(X2))).
% 0.40/1.63  cnf(i_0_424, axiom, (X1!=X2|~ssList(X1)|ssList(X2))).
% 0.40/1.63  cnf(i_0_425, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.40/1.63  cnf(i_0_426, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.40/1.63  cnf(i_0_427, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.40/1.63  cnf(i_0_428, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.40/1.63  cnf(i_0_429, axiom, (X1!=X2|~strictorderP(X1)|strictorderP(X2))).
% 0.40/1.63  cnf(i_0_430, axiom, (X1!=X2|~totalorderP(X1)|totalorderP(X2))).
% 0.40/1.63  cnf(i_0_431, axiom, (X1!=X2|~strictorderedP(X1)|strictorderedP(X2))).
% 0.40/1.63  cnf(i_0_432, axiom, (X1!=X2|~totalorderedP(X1)|totalorderedP(X2))).
% 0.84/2.06  cnf(i_0_390, axiom, (X1=X1)).
% 0.84/2.06  cnf(i_0_391, axiom, (X1=X2|X2!=X1)).
% 0.84/2.06  cnf(i_0_392, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.84/2.06  cnf(i_0_393, axiom, (X1!=X2|app(X1,X3)=app(X2,X3))).
% 0.84/2.06  cnf(i_0_394, axiom, (X1!=X2|app(X3,X1)=app(X3,X2))).
% 0.84/2.06  cnf(i_0_395, axiom, (X1!=X2|cons(X1,X3)=cons(X2,X3))).
% 0.84/2.06  cnf(i_0_396, axiom, (X1!=X2|cons(X3,X1)=cons(X3,X2))).
% 0.84/2.06  cnf(i_0_397, axiom, (X1!=X2|esk40_1(X1)=esk40_1(X2))).
% 0.84/2.06  cnf(i_0_398, axiom, (X1!=X2|esk41_1(X1)=esk41_1(X2))).
% 0.84/2.06  cnf(i_0_399, axiom, (X1!=X2|esk35_1(X1)=esk35_1(X2))).
% 0.84/2.06  cnf(i_0_400, axiom, (X1!=X2|hd(X1)=hd(X2))).
% 0.84/2.06  cnf(i_0_401, axiom, (X1!=X2|tl(X1)=tl(X2))).
% 0.84/2.06  cnf(i_0_402, axiom, (X1!=X2|esk47_1(X1)=esk47_1(X2))).
% 0.84/2.06  cnf(i_0_403, axiom, (X1!=X2|esk46_1(X1)=esk46_1(X2))).
% 0.84/2.06  cnf(i_0_404, axiom, (X1!=X2|esk36_1(X1)=esk36_1(X2))).
% 0.84/2.06  cnf(i_0_405, axiom, (X1!=X2|~cyclefreeP(X1)|cyclefreeP(X2))).
% 0.84/2.06  cnf(i_0_406, axiom, (X1!=X2|~duplicatefreeP(X1)|duplicatefreeP(X2))).
% 0.84/2.06  cnf(i_0_407, axiom, (X1!=X2|~equalelemsP(X1)|equalelemsP(X2))).
% 0.84/2.06  cnf(i_0_408, axiom, (X1!=X2|~segmentP(X1,X3)|segmentP(X2,X3))).
% 0.84/2.06  cnf(i_0_409, axiom, (X1!=X2|~segmentP(X3,X1)|segmentP(X3,X2))).
% 0.84/2.06  cnf(i_0_410, axiom, (X1!=X2|~memberP(X1,X3)|memberP(X2,X3))).
% 0.84/2.06  cnf(i_0_411, axiom, (X1!=X2|~memberP(X3,X1)|memberP(X3,X2))).
% 0.84/2.06  cnf(i_0_412, axiom, (X1!=X2|~frontsegP(X1,X3)|frontsegP(X2,X3))).
% 0.84/2.06  cnf(i_0_413, axiom, (X1!=X2|~frontsegP(X3,X1)|frontsegP(X3,X2))).
% 0.84/2.06  cnf(i_0_414, axiom, (X1!=X2|~rearsegP(X1,X3)|rearsegP(X2,X3))).
% 0.84/2.06  cnf(i_0_415, axiom, (X1!=X2|~rearsegP(X3,X1)|rearsegP(X3,X2))).
% 0.84/2.06  cnf(i_0_416, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.84/2.06  cnf(i_0_417, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.84/2.06  cnf(i_0_418, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.84/2.06  cnf(i_0_419, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.84/2.06  cnf(i_0_420, axiom, (X1!=X2|~neq(X1,X3)|neq(X2,X3))).
% 0.84/2.06  cnf(i_0_421, axiom, (X1!=X2|~neq(X3,X1)|neq(X3,X2))).
% 0.84/2.06  cnf(i_0_422, axiom, (X1!=X2|~singletonP(X1)|singletonP(X2))).
% 0.84/2.06  cnf(i_0_423, axiom, (X1!=X2|~ssItem(X1)|ssItem(X2))).
% 0.84/2.06  cnf(i_0_424, axiom, (X1!=X2|~ssList(X1)|ssList(X2))).
% 0.84/2.06  cnf(i_0_425, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.84/2.06  cnf(i_0_426, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.84/2.06  cnf(i_0_427, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.84/2.06  cnf(i_0_428, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.84/2.06  cnf(i_0_429, axiom, (X1!=X2|~strictorderP(X1)|strictorderP(X2))).
% 0.84/2.06  cnf(i_0_430, axiom, (X1!=X2|~totalorderP(X1)|totalorderP(X2))).
% 0.84/2.06  cnf(i_0_431, axiom, (X1!=X2|~strictorderedP(X1)|strictorderedP(X2))).
% 0.84/2.06  cnf(i_0_432, axiom, (X1!=X2|~totalorderedP(X1)|totalorderedP(X2))).
% 0.84/2.06  cnf(i_0_433, plain, (~leq(X1,X2)|~leq(X2,X1)|~ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~cyclefreeP(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[189])).
% 0.84/2.06  cnf(i_0_434, plain, (lt(X1,X2)|~ssItem(X2)|~ssItem(X1)|~ssList(app(app(X3,cons(X2,X4)),cons(X1,X5)))|lt(X2,X1)|~strictorderP(app(app(X3,cons(X2,X4)),cons(X1,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[190])).
% 0.84/2.06  cnf(i_0_435, plain, (leq(X1,X2)|~ssItem(X2)|~ssItem(X1)|~ssList(app(app(X3,cons(X2,X4)),cons(X1,X5)))|leq(X2,X1)|~totalorderP(app(app(X3,cons(X2,X4)),cons(X1,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[191])).
% 0.84/2.06  cnf(i_0_436, plain, (~ssItem(X1)|~ssItem(X2)|~ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))|lt(X1,X2)|~strictorderedP(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[192])).
% 0.84/2.06  cnf(i_0_437, plain, (~ssItem(X1)|~ssItem(X2)|~ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))|leq(X1,X2)|~totalorderedP(app(app(X3,cons(X1,X4)),cons(X2,X5)))|~ssList(X3)|~ssList(X4)|~ssList(X5)), inference(equality_inference,[],[193])).
% 0.84/2.06  cnf(i_0_438, plain, (~ssItem(X1)|~ssItem(X2)|~ssList(app(X3,cons(X1,cons(X2,X4))))|X1=X2|~equalelemsP(app(X3,cons(X1,cons(X2,X4))))|~ssList(X3)|~ssList(X4)), inference(equality_inference,[],[201])).
% 0.84/2.06  cnf(i_0_439, plain, (~frontsegP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X1),cons(X3,X2))), inference(equality_inference,[],[208])).
% 0.84/2.06  cnf(i_0_440, plain, (~ssList(X1)|~ssList(app(app(X2,X1),X3))|segmentP(app(app(X2,X1),X3),X1)|~ssList(X2)|~ssList(X3)), inference(equality_inference,[],[210])).
% 0.84/2.06  cnf(i_0_441, plain, (~ssItem(X1)|~ssList(app(X2,cons(X1,X3)))|memberP(app(X2,cons(X1,X3)),X1)|~ssList(X2)|~ssList(X3)), inference(equality_inference,[],[211])).
% 0.84/2.06  cnf(i_0_442, plain, (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X2)|X1=X1), inference(equality_inference,[],[234])).
% 0.84/2.06  cnf(i_0_443, plain, (~ssItem(X1)|~ssItem(X1)|~ssList(X2)|~ssList(X2)|X2=X2), inference(equality_inference,[],[235])).
% 0.84/2.06  cnf(i_0_444, plain, (~ssList(X1)|~ssList(X1)|X1=X1|~ssList(X2)), inference(equality_inference,[],[238])).
% 0.84/2.06  cnf(i_0_445, plain, (~ssList(X1)|~ssList(X1)|X1=X1|~ssList(X2)), inference(equality_inference,[],[239])).
% 0.84/2.06  cnf(i_0_446, plain, (~ssList(X1)|~ssItem(X2)|~ssItem(X2)|memberP(cons(X2,X1),X2)), inference(equality_inference,[],[247])).
% 0.84/2.06  cnf(i_0_447, plain, (~ssList(X1)|~ssList(app(X2,X1))|rearsegP(app(X2,X1),X1)|~ssList(X2)), inference(equality_inference,[],[254])).
% 0.84/2.06  cnf(i_0_448, plain, (~ssList(X1)|~ssList(app(X1,X2))|frontsegP(app(X1,X2),X1)|~ssList(X2)), inference(equality_inference,[],[255])).
% 0.84/2.06  cnf(i_0_449, plain, (~ssList(nil)|~ssItem(X1)|strictorderedP(cons(X1,nil))), inference(equality_inference,[],[274])).
% 0.84/2.06  cnf(i_0_450, plain, (~ssList(nil)|~ssItem(X1)|totalorderedP(cons(X1,nil))), inference(equality_inference,[],[275])).
% 0.84/2.06  cnf(i_0_451, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(equality_inference,[],[281])).
% 0.84/2.06  cnf(i_0_452, plain, (~lt(X1,X1)|~ssItem(X1)|~ssItem(X1)), inference(equality_inference,[],[282])).
% 0.84/2.06  cnf(i_0_453, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(equality_inference,[],[283])).
% 0.84/2.06  cnf(i_0_454, plain, (~ssList(cons(X1,nil))|singletonP(cons(X1,nil))|~ssItem(X1)), inference(equality_inference,[],[284])).
% 0.84/2.06  cnf(i_0_455, plain, (~ssList(nil)|segmentP(nil,nil)), inference(equality_inference,[],[311])).
% 0.84/2.06  cnf(i_0_456, plain, (~ssList(nil)|rearsegP(nil,nil)), inference(equality_inference,[],[312])).
% 0.84/2.06  cnf(i_0_457, plain, (~ssList(nil)|frontsegP(nil,nil)), inference(equality_inference,[],[313])).
% 0.84/2.06  cnf(i_0_458, plain, (esk51_0=esk49_0), inference(scs_inference,[],[i_0_387,i_0_391])).
% 0.84/2.06  cnf(i_0_459, plain, (geq(esk2_0,esk2_0)), inference(scs_inference,[],[i_0_387,i_0_382,i_0_391,i_0_348])).
% 0.84/2.06  cnf(i_0_460, plain, (~ssItem(X1)|geq(X1,X1)), inference(rename_variables,[],[i_0_348])).
% 0.84/2.06  cnf(i_0_461, plain, (leq(esk2_0,esk2_0)), inference(scs_inference,[],[i_0_387,i_0_382,i_0_391,i_0_348,i_0_349])).
% 0.84/2.06  cnf(i_0_462, plain, (~ssItem(X1)|leq(X1,X1)), inference(rename_variables,[],[i_0_349])).
% 0.84/2.06  cnf(i_0_463, plain, (segmentP(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350])).
% 0.84/2.06  cnf(i_0_464, plain, (~ssList(X1)|segmentP(X1,X1)), inference(rename_variables,[],[i_0_350])).
% 0.84/2.06  cnf(i_0_465, plain, (rearsegP(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351])).
% 0.84/2.06  cnf(i_0_466, plain, (~ssList(X1)|rearsegP(X1,X1)), inference(rename_variables,[],[i_0_351])).
% 0.84/2.06  cnf(i_0_467, plain, (frontsegP(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352])).
% 0.84/2.06  cnf(i_0_468, plain, (~ssList(X1)|frontsegP(X1,X1)), inference(rename_variables,[],[i_0_352])).
% 0.84/2.06  cnf(i_0_469, plain, (~neq(esk51_0,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451])).
% 0.84/2.06  cnf(i_0_470, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_451])).
% 0.84/2.06  cnf(i_0_471, plain, (~neq(esk2_0,esk2_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453])).
% 0.84/2.06  cnf(i_0_472, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_453])).
% 0.84/2.06  cnf(i_0_473, plain, (nil=esk51_0), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392])).
% 0.84/2.06  cnf(i_0_474, plain, (cyclefreeP(esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405])).
% 0.84/2.06  cnf(i_0_475, plain, (duplicatefreeP(esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_371,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406])).
% 0.84/2.06  cnf(i_0_476, plain, (equalelemsP(esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_370,i_0_371,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407])).
% 0.84/2.06  cnf(i_0_477, plain, (~neq(esk49_0,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_370,i_0_371,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420])).
% 0.84/2.06  cnf(i_0_478, plain, (~neq(esk51_0,esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_370,i_0_371,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421])).
% 0.84/2.06  cnf(i_0_479, plain, (strictorderP(esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_370,i_0_371,i_0_374,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429])).
% 0.84/2.06  cnf(i_0_480, plain, (totalorderP(esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_370,i_0_371,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430])).
% 0.84/2.06  cnf(i_0_481, plain, (strictorderedP(esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_370,i_0_371,i_0_372,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431])).
% 0.84/2.06  cnf(i_0_482, plain, (totalorderedP(esk49_0)), inference(scs_inference,[],[i_0_377,i_0_387,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432])).
% 0.84/2.06  cnf(i_0_483, plain, (segmentP(nil,esk49_0)), inference(scs_inference,[],[i_0_377,i_0_379,i_0_387,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311])).
% 0.84/2.06  cnf(i_0_484, plain, (nil!=X1|segmentP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_311])).
% 0.84/2.06  cnf(i_0_485, plain, (rearsegP(nil,esk49_0)), inference(scs_inference,[],[i_0_377,i_0_379,i_0_387,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312])).
% 0.84/2.06  cnf(i_0_486, plain, (nil!=X1|rearsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_312])).
% 0.84/2.06  cnf(i_0_487, plain, (frontsegP(nil,esk49_0)), inference(scs_inference,[],[i_0_377,i_0_379,i_0_387,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313])).
% 0.84/2.06  cnf(i_0_488, plain, (nil!=X1|frontsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_313])).
% 0.84/2.06  cnf(i_0_489, plain, (tl(esk48_0)=esk47_1(esk48_0)), inference(scs_inference,[],[i_0_377,i_0_379,i_0_380,i_0_385,i_0_387,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367])).
% 0.84/2.06  cnf(i_0_490, plain, (nil=X1|tl(X1)=esk47_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_367])).
% 0.84/2.06  cnf(i_0_491, plain, (hd(esk48_0)=esk46_1(esk48_0)), inference(scs_inference,[],[i_0_377,i_0_379,i_0_380,i_0_385,i_0_387,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367,i_0_368])).
% 0.84/2.06  cnf(i_0_492, plain, (nil=X1|hd(X1)=esk46_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_368])).
% 0.84/2.06  cnf(i_0_493, plain, (~neq(esk48_0,esk50_0)), inference(scs_inference,[],[i_0_377,i_0_378,i_0_379,i_0_380,i_0_385,i_0_387,i_0_388,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367,i_0_368,i_0_281])).
% 0.84/2.06  cnf(i_0_494, plain, (X1!=X2|~ssList(X2)|~ssList(X1)|~neq(X1,X2)), inference(rename_variables,[],[i_0_281])).
% 0.84/2.06  cnf(i_0_495, plain, (memberP(cons(esk2_0,esk51_0),esk2_0)), inference(scs_inference,[],[i_0_377,i_0_378,i_0_379,i_0_380,i_0_385,i_0_387,i_0_388,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367,i_0_368,i_0_281,i_0_446])).
% 0.84/2.06  cnf(i_0_496, plain, (~ssItem(X1)|~ssItem(X1)|memberP(cons(X1,X2),X1)|~ssList(X2)), inference(rename_variables,[],[i_0_446])).
% 0.84/2.06  cnf(i_0_497, plain, (frontsegP(cons(esk2_0,esk51_0),cons(esk2_0,esk51_0))), inference(scs_inference,[],[i_0_377,i_0_378,i_0_379,i_0_380,i_0_385,i_0_387,i_0_388,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367,i_0_368,i_0_281,i_0_446,i_0_439])).
% 0.84/2.06  cnf(i_0_498, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X2),cons(X3,X1))|~frontsegP(X2,X1)), inference(rename_variables,[],[i_0_439])).
% 0.84/2.06  cnf(i_0_499, plain, (ssItem(X1)|esk2_0!=X1), inference(scs_inference,[],[i_0_377,i_0_378,i_0_379,i_0_380,i_0_385,i_0_387,i_0_388,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367,i_0_368,i_0_281,i_0_446,i_0_439,i_0_423])).
% 0.84/2.06  cnf(i_0_500, plain, (ssList(X1)|esk50_0!=X1), inference(scs_inference,[],[i_0_377,i_0_378,i_0_379,i_0_380,i_0_385,i_0_387,i_0_388,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367,i_0_368,i_0_281,i_0_446,i_0_439,i_0_423,i_0_424])).
% 0.84/2.06  cnf(i_0_501, plain, (X1!=X2|~ssItem(X2)|~ssItem(X1)|~neq(X1,X2)), inference(rename_variables,[],[i_0_283])).
% 0.84/2.06  cnf(i_0_502, plain, (~ssItem(esk49_0)|memberP(app(esk51_0,cons(esk2_0,esk51_0)),esk2_0)|esk2_0!=esk51_0|esk50_0!=app(esk51_0,esk51_0)|~ssList(app(esk51_0,cons(esk2_0,esk51_0)))), inference(scs_inference,[],[i_0_377,i_0_378,i_0_379,i_0_380,i_0_385,i_0_387,i_0_388,i_0_389,i_0_370,i_0_371,i_0_372,i_0_373,i_0_374,i_0_375,i_0_376,i_0_382,i_0_391,i_0_348,i_0_349,i_0_350,i_0_351,i_0_352,i_0_451,i_0_453,i_0_392,i_0_405,i_0_406,i_0_407,i_0_420,i_0_421,i_0_429,i_0_430,i_0_431,i_0_432,i_0_311,i_0_312,i_0_313,i_0_367,i_0_368,i_0_281,i_0_446,i_0_439,i_0_423,i_0_424,i_0_283,i_0_447,i_0_448,i_0_267,i_0_270,i_0_302,i_0_303,i_0_441])).
% 0.84/2.06  cnf(i_0_503, plain, (ssItem(esk2_0)), inference(equality_inference,[],[499])).
% 0.84/2.06  cnf(i_0_504, plain, (ssList(esk50_0)), inference(equality_inference,[],[500])).
% 0.84/2.06  cnf(i_0_505, plain, (nil=esk50_0), inference(scs_inference,[],[i_0_473,i_0_384])).
% 0.84/2.06  cnf(i_0_506, plain, (segmentP(esk48_0,esk48_0)), inference(scs_inference,[],[i_0_380,i_0_350])).
% 0.84/2.06  cnf(i_0_507, plain, (~ssList(X1)|segmentP(X1,X1)), inference(rename_variables,[],[i_0_350])).
% 0.84/2.06  cnf(i_0_508, plain, (rearsegP(esk48_0,esk48_0)), inference(scs_inference,[],[i_0_380,i_0_350,i_0_351])).
% 0.84/2.06  cnf(i_0_509, plain, (~ssList(X1)|rearsegP(X1,X1)), inference(rename_variables,[],[i_0_351])).
% 0.84/2.06  cnf(i_0_510, plain, (frontsegP(esk48_0,esk48_0)), inference(scs_inference,[],[i_0_380,i_0_350,i_0_351,i_0_352])).
% 0.84/2.06  cnf(i_0_511, plain, (~ssList(X1)|frontsegP(X1,X1)), inference(rename_variables,[],[i_0_352])).
% 0.84/2.06  cnf(i_0_512, plain, (geq(esk1_0,esk1_0)), inference(scs_inference,[],[i_0_380,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348])).
% 0.84/2.06  cnf(i_0_513, plain, (~ssItem(X1)|geq(X1,X1)), inference(rename_variables,[],[i_0_348])).
% 0.84/2.06  cnf(i_0_514, plain, (leq(esk1_0,esk1_0)), inference(scs_inference,[],[i_0_380,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349])).
% 0.84/2.06  cnf(i_0_515, plain, (~ssItem(X1)|leq(X1,X1)), inference(rename_variables,[],[i_0_349])).
% 0.84/2.06  cnf(i_0_516, plain, (esk50_0=esk48_0), inference(scs_inference,[],[i_0_380,i_0_388,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391])).
% 0.84/2.06  cnf(i_0_517, plain, (~neq(esk48_0,esk48_0)), inference(scs_inference,[],[i_0_380,i_0_388,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451])).
% 0.84/2.06  cnf(i_0_518, plain, (~ssList(X1)|~ssList(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_451])).
% 0.84/2.06  cnf(i_0_519, plain, (~neq(esk1_0,esk1_0)), inference(scs_inference,[],[i_0_380,i_0_388,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453])).
% 0.84/2.06  cnf(i_0_520, plain, (~ssItem(X1)|~ssItem(X1)|~neq(X1,X1)), inference(rename_variables,[],[i_0_453])).
% 0.84/2.06  cnf(i_0_521, plain, (segmentP(nil,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_473,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311])).
% 0.84/2.06  cnf(i_0_522, plain, (nil!=X1|segmentP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_311])).
% 0.84/2.06  cnf(i_0_523, plain, (rearsegP(nil,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_473,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312])).
% 0.84/2.06  cnf(i_0_524, plain, (nil!=X1|rearsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_312])).
% 0.84/2.06  cnf(i_0_525, plain, (frontsegP(nil,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_473,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313])).
% 0.84/2.06  cnf(i_0_526, plain, (nil!=X1|frontsegP(nil,X1)|~ssList(X1)), inference(rename_variables,[],[i_0_313])).
% 0.84/2.06  cnf(i_0_527, plain, (nil!=esk50_0), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_473,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392])).
% 0.84/2.06  cnf(i_0_528, plain, (cyclefreeP(esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_473,i_0_474,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405])).
% 0.84/2.06  cnf(i_0_529, plain, (duplicatefreeP(esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_473,i_0_474,i_0_475,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406])).
% 0.84/2.06  cnf(i_0_530, plain, (equalelemsP(esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_473,i_0_474,i_0_475,i_0_476,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407])).
% 0.84/2.06  cnf(i_0_531, plain, (strictorderP(esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429])).
% 0.84/2.06  cnf(i_0_532, plain, (totalorderP(esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430])).
% 0.84/2.06  cnf(i_0_533, plain, (strictorderedP(esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431])).
% 0.84/2.06  cnf(i_0_534, plain, (totalorderedP(esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432])).
% 0.84/2.06  cnf(i_0_535, plain, (~neq(nil,esk51_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420])).
% 0.84/2.06  cnf(i_0_536, plain, (~neq(esk49_0,esk49_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420,i_0_421])).
% 0.84/2.06  cnf(i_0_537, plain, (memberP(cons(esk1_0,esk51_0),esk1_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_388,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420,i_0_421,i_0_446])).
% 0.84/2.06  cnf(i_0_538, plain, (~ssItem(X1)|~ssItem(X1)|memberP(cons(X1,X2),X1)|~ssList(X2)), inference(rename_variables,[],[i_0_446])).
% 0.84/2.06  cnf(i_0_539, plain, (~neq(nil,esk49_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_379,i_0_388,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_381,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420,i_0_421,i_0_446,i_0_281])).
% 0.84/2.06  cnf(i_0_540, plain, (X1!=X2|~ssList(X2)|~ssList(X1)|~neq(X1,X2)), inference(rename_variables,[],[i_0_281])).
% 0.84/2.06  cnf(i_0_541, plain, (frontsegP(cons(esk2_0,esk48_0),cons(esk2_0,esk48_0))), inference(scs_inference,[],[i_0_377,i_0_380,i_0_379,i_0_388,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_382,i_0_381,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420,i_0_421,i_0_446,i_0_281,i_0_439])).
% 0.84/2.06  cnf(i_0_542, plain, (~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X2),cons(X3,X1))|~frontsegP(X2,X1)), inference(rename_variables,[],[i_0_439])).
% 0.84/2.06  cnf(i_0_543, plain, (tl(esk50_0)=esk47_1(esk50_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_379,i_0_388,i_0_378,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_382,i_0_381,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420,i_0_421,i_0_446,i_0_281,i_0_439,i_0_367])).
% 0.84/2.06  cnf(i_0_544, plain, (nil=X1|tl(X1)=esk47_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_367])).
% 0.84/2.06  cnf(i_0_545, plain, (hd(esk50_0)=esk46_1(esk50_0)), inference(scs_inference,[],[i_0_377,i_0_380,i_0_379,i_0_388,i_0_378,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_382,i_0_381,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420,i_0_421,i_0_446,i_0_281,i_0_439,i_0_367,i_0_368])).
% 0.84/2.06  cnf(i_0_546, plain, (nil=X1|hd(X1)=esk46_1(X1)|~ssList(X1)), inference(rename_variables,[],[i_0_368])).
% 0.84/2.06  cnf(i_0_547, plain, (ssItem(X1)|esk1_0!=X1), inference(scs_inference,[],[i_0_377,i_0_380,i_0_379,i_0_388,i_0_378,i_0_385,i_0_387,i_0_389,i_0_477,i_0_473,i_0_474,i_0_475,i_0_476,i_0_479,i_0_480,i_0_481,i_0_482,i_0_382,i_0_381,i_0_383,i_0_350,i_0_351,i_0_352,i_0_348,i_0_349,i_0_391,i_0_451,i_0_453,i_0_311,i_0_312,i_0_313,i_0_392,i_0_405,i_0_406,i_0_407,i_0_429,i_0_430,i_0_431,i_0_432,i_0_420,i_0_421,i_0_446,i_0_281,i_0_439,i_0_367,i_0_368,i_0_423])).
% 0.84/2.06  cnf(i_0_548, plain, (X1!=X2|~ssItem(X2)|~ssItem(X1)|~neq(X1,X2)), inference(rename_variables,[],[i_0_283])).
% 0.84/2.06  cnf(i_0_550, plain, (ssItem(esk1_0)), inference(equality_inference,[],[547])).
% 0.84/2.06  cnf(i_0_551,plain, ($false), inference(scs_inference,[],[i_0+505, i_0_527]), ['proof']).
% 0.84/2.06  % SZS output end CNFRefutation
% 0.84/2.06  % Total time : 1.272s
%------------------------------------------------------------------------------