%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWC359+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:02:08 AM UTC 2026
% Result : Theorem 234.85s 255.11s
% Output : Proof 235.88s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('SWC001+0.ax',ax1) ).
fof(ax2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('SWC001+0.ax',ax2) ).
fof(ax3,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ( memberP(U,V)
<=> ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('SWC001+0.ax',ax3) ).
fof(ax4,axiom,
! [U] :
( ssList(U)
=> ( singletonP(U)
<=> ? [V] :
( cons(V,nil) = U
& ssItem(V) ) ) ),
file('SWC001+0.ax',ax4) ).
fof(ax5,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( frontsegP(U,V)
<=> ? [W] :
( app(V,W) = U
& ssList(W) ) ) ) ),
file('SWC001+0.ax',ax5) ).
fof(ax6,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( rearsegP(U,V)
<=> ? [W] :
( app(W,V) = U
& ssList(W) ) ) ) ),
file('SWC001+0.ax',ax6) ).
fof(ax7,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('SWC001+0.ax',ax7) ).
fof(ax8,axiom,
! [U] :
( ssList(U)
=> ( cyclefreeP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> ~ ( leq(W,V)
& leq(V,W) ) ) ) ) ) ) ) ) ),
file('SWC001+0.ax',ax8) ).
fof(ax9,axiom,
! [U] :
( ssList(U)
=> ( totalorderP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> ( leq(W,V)
| leq(V,W) ) ) ) ) ) ) ) ) ),
file('SWC001+0.ax',ax9) ).
fof(ax10,axiom,
! [U] :
( ssList(U)
=> ( strictorderP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> ( lt(W,V)
| lt(V,W) ) ) ) ) ) ) ) ) ),
file('SWC001+0.ax',ax10) ).
fof(ax11,axiom,
! [U] :
( ssList(U)
=> ( totalorderedP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> leq(V,W) ) ) ) ) ) ) ) ),
file('SWC001+0.ax',ax11) ).
fof(ax12,axiom,
! [U] :
( ssList(U)
=> ( strictorderedP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> lt(V,W) ) ) ) ) ) ) ) ),
file('SWC001+0.ax',ax12) ).
fof(ax13,axiom,
! [U] :
( ssList(U)
=> ( duplicatefreeP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> V != W ) ) ) ) ) ) ) ),
file('SWC001+0.ax',ax13) ).
fof(ax14,axiom,
! [U] :
( ssList(U)
=> ( equalelemsP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ( app(X,cons(V,cons(W,Y))) = U
=> V = W ) ) ) ) ) ) ),
file('SWC001+0.ax',ax14) ).
fof(ax15,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('SWC001+0.ax',ax15) ).
fof(ax16,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ssList(cons(V,U)) ) ),
file('SWC001+0.ax',ax16) ).
fof(ax17,axiom,
ssList(nil),
file('SWC001+0.ax',ax17) ).
fof(ax18,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) != U ) ),
file('SWC001+0.ax',ax18) ).
fof(ax19,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssItem(X)
=> ( cons(W,U) = cons(X,V)
=> ( V = U
& W = X ) ) ) ) ) ),
file('SWC001+0.ax',ax19) ).
fof(ax20,axiom,
! [U] :
( ssList(U)
=> ( ? [V] :
( ? [W] :
( cons(W,V) = U
& ssItem(W) )
& ssList(V) )
| nil = U ) ),
file('SWC001+0.ax',ax20) ).
fof(ax21,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> nil != cons(V,U) ) ),
file('SWC001+0.ax',ax21) ).
fof(ax22,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssItem(hd(U)) ) ),
file('SWC001+0.ax',ax22) ).
fof(ax23,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> hd(cons(V,U)) = V ) ),
file('SWC001+0.ax',ax23) ).
fof(ax24,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssList(tl(U)) ) ),
file('SWC001+0.ax',ax24) ).
fof(ax25,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> tl(cons(V,U)) = U ) ),
file('SWC001+0.ax',ax25) ).
fof(ax26,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ssList(app(U,V)) ) ),
file('SWC001+0.ax',ax26) ).
fof(ax27,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssItem(W)
=> cons(W,app(V,U)) = app(cons(W,V),U) ) ) ),
file('SWC001+0.ax',ax27) ).
fof(ax28,axiom,
! [U] :
( ssList(U)
=> app(nil,U) = U ),
file('SWC001+0.ax',ax28) ).
fof(ax29,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( ( leq(V,U)
& leq(U,V) )
=> U = V ) ) ),
file('SWC001+0.ax',ax29) ).
fof(ax30,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ( ( leq(V,W)
& leq(U,V) )
=> leq(U,W) ) ) ) ),
file('SWC001+0.ax',ax30) ).
fof(ax31,axiom,
! [U] :
( ssItem(U)
=> leq(U,U) ),
file('SWC001+0.ax',ax31) ).
fof(ax32,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( geq(U,V)
<=> leq(V,U) ) ) ),
file('SWC001+0.ax',ax32) ).
fof(ax33,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( lt(U,V)
=> ~ lt(V,U) ) ) ),
file('SWC001+0.ax',ax33) ).
fof(ax34,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ( ( lt(V,W)
& lt(U,V) )
=> lt(U,W) ) ) ) ),
file('SWC001+0.ax',ax34) ).
fof(ax35,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( gt(U,V)
<=> lt(V,U) ) ) ),
file('SWC001+0.ax',ax35) ).
fof(ax36,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( memberP(app(V,W),U)
<=> ( memberP(W,U)
| memberP(V,U) ) ) ) ) ),
file('SWC001+0.ax',ax36) ).
fof(ax37,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssList(W)
=> ( memberP(cons(V,W),U)
<=> ( memberP(W,U)
| U = V ) ) ) ) ),
file('SWC001+0.ax',ax37) ).
fof(ax38,axiom,
! [U] :
( ssItem(U)
=> ~ memberP(nil,U) ),
file('SWC001+0.ax',ax38) ).
fof(ax39,axiom,
~ singletonP(nil),
file('SWC001+0.ax',ax39) ).
fof(ax40,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( frontsegP(V,W)
& frontsegP(U,V) )
=> frontsegP(U,W) ) ) ) ),
file('SWC001+0.ax',ax40) ).
fof(ax41,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( frontsegP(V,U)
& frontsegP(U,V) )
=> U = V ) ) ),
file('SWC001+0.ax',ax41) ).
fof(ax42,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,U) ),
file('SWC001+0.ax',ax42) ).
fof(ax43,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( frontsegP(U,V)
=> frontsegP(app(U,W),V) ) ) ) ),
file('SWC001+0.ax',ax43) ).
fof(ax44,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( frontsegP(cons(U,W),cons(V,X))
<=> ( frontsegP(W,X)
& U = V ) ) ) ) ) ),
file('SWC001+0.ax',ax44) ).
fof(ax45,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,nil) ),
file('SWC001+0.ax',ax45) ).
fof(ax46,axiom,
! [U] :
( ssList(U)
=> ( frontsegP(nil,U)
<=> nil = U ) ),
file('SWC001+0.ax',ax46) ).
fof(ax47,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( rearsegP(V,W)
& rearsegP(U,V) )
=> rearsegP(U,W) ) ) ) ),
file('SWC001+0.ax',ax47) ).
fof(ax48,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( rearsegP(V,U)
& rearsegP(U,V) )
=> U = V ) ) ),
file('SWC001+0.ax',ax48) ).
fof(ax49,axiom,
! [U] :
( ssList(U)
=> rearsegP(U,U) ),
file('SWC001+0.ax',ax49) ).
fof(ax50,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( rearsegP(U,V)
=> rearsegP(app(W,U),V) ) ) ) ),
file('SWC001+0.ax',ax50) ).
fof(ax51,axiom,
! [U] :
( ssList(U)
=> rearsegP(U,nil) ),
file('SWC001+0.ax',ax51) ).
fof(ax52,axiom,
! [U] :
( ssList(U)
=> ( rearsegP(nil,U)
<=> nil = U ) ),
file('SWC001+0.ax',ax52) ).
fof(ax53,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( segmentP(V,W)
& segmentP(U,V) )
=> segmentP(U,W) ) ) ) ),
file('SWC001+0.ax',ax53) ).
fof(ax54,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( segmentP(V,U)
& segmentP(U,V) )
=> U = V ) ) ),
file('SWC001+0.ax',ax54) ).
fof(ax55,axiom,
! [U] :
( ssList(U)
=> segmentP(U,U) ),
file('SWC001+0.ax',ax55) ).
fof(ax56,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( segmentP(U,V)
=> segmentP(app(app(W,U),X),V) ) ) ) ) ),
file('SWC001+0.ax',ax56) ).
fof(ax57,axiom,
! [U] :
( ssList(U)
=> segmentP(U,nil) ),
file('SWC001+0.ax',ax57) ).
fof(ax58,axiom,
! [U] :
( ssList(U)
=> ( segmentP(nil,U)
<=> nil = U ) ),
file('SWC001+0.ax',ax58) ).
fof(ax59,axiom,
! [U] :
( ssItem(U)
=> cyclefreeP(cons(U,nil)) ),
file('SWC001+0.ax',ax59) ).
fof(ax60,axiom,
cyclefreeP(nil),
file('SWC001+0.ax',ax60) ).
fof(ax61,axiom,
! [U] :
( ssItem(U)
=> totalorderP(cons(U,nil)) ),
file('SWC001+0.ax',ax61) ).
fof(ax62,axiom,
totalorderP(nil),
file('SWC001+0.ax',ax62) ).
fof(ax63,axiom,
! [U] :
( ssItem(U)
=> strictorderP(cons(U,nil)) ),
file('SWC001+0.ax',ax63) ).
fof(ax64,axiom,
strictorderP(nil),
file('SWC001+0.ax',ax64) ).
fof(ax65,axiom,
! [U] :
( ssItem(U)
=> totalorderedP(cons(U,nil)) ),
file('SWC001+0.ax',ax65) ).
fof(ax66,axiom,
totalorderedP(nil),
file('SWC001+0.ax',ax66) ).
fof(ax67,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssList(V)
=> ( totalorderedP(cons(U,V))
<=> ( ( leq(U,hd(V))
& totalorderedP(V)
& nil != V )
| nil = V ) ) ) ),
file('SWC001+0.ax',ax67) ).
fof(ax68,axiom,
! [U] :
( ssItem(U)
=> strictorderedP(cons(U,nil)) ),
file('SWC001+0.ax',ax68) ).
fof(ax69,axiom,
strictorderedP(nil),
file('SWC001+0.ax',ax69) ).
fof(ax70,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssList(V)
=> ( strictorderedP(cons(U,V))
<=> ( ( lt(U,hd(V))
& strictorderedP(V)
& nil != V )
| nil = V ) ) ) ),
file('SWC001+0.ax',ax70) ).
fof(ax71,axiom,
! [U] :
( ssItem(U)
=> duplicatefreeP(cons(U,nil)) ),
file('SWC001+0.ax',ax71) ).
fof(ax72,axiom,
duplicatefreeP(nil),
file('SWC001+0.ax',ax72) ).
fof(ax73,axiom,
! [U] :
( ssItem(U)
=> equalelemsP(cons(U,nil)) ),
file('SWC001+0.ax',ax73) ).
fof(ax74,axiom,
equalelemsP(nil),
file('SWC001+0.ax',ax74) ).
fof(ax75,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ? [V] :
( hd(U) = V
& ssItem(V) ) ) ),
file('SWC001+0.ax',ax75) ).
fof(ax76,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ? [V] :
( tl(U) = V
& ssList(V) ) ) ),
file('SWC001+0.ax',ax76) ).
fof(ax77,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( tl(V) = tl(U)
& hd(V) = hd(U)
& nil != U
& nil != V )
=> V = U ) ) ),
file('SWC001+0.ax',ax77) ).
fof(ax78,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> cons(hd(U),tl(U)) = U ) ),
file('SWC001+0.ax',ax78) ).
fof(ax79,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( app(W,V) = app(U,V)
=> W = U ) ) ) ),
file('SWC001+0.ax',ax79) ).
fof(ax80,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( app(V,W) = app(V,U)
=> W = U ) ) ) ),
file('SWC001+0.ax',ax80) ).
fof(ax81,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) = app(cons(V,nil),U) ) ),
file('SWC001+0.ax',ax81) ).
fof(ax82,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> app(app(U,V),W) = app(U,app(V,W)) ) ) ),
file('SWC001+0.ax',ax82) ).
fof(ax83,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( nil = app(U,V)
<=> ( nil = U
& nil = V ) ) ) ),
file('SWC001+0.ax',ax83) ).
fof(ax84,axiom,
! [U] :
( ssList(U)
=> app(U,nil) = U ),
file('SWC001+0.ax',ax84) ).
fof(ax85,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( nil != U
=> hd(app(U,V)) = hd(U) ) ) ),
file('SWC001+0.ax',ax85) ).
fof(ax86,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( nil != U
=> tl(app(U,V)) = app(tl(U),V) ) ) ),
file('SWC001+0.ax',ax86) ).
fof(ax87,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( ( geq(V,U)
& geq(U,V) )
=> U = V ) ) ),
file('SWC001+0.ax',ax87) ).
fof(ax88,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ( ( geq(V,W)
& geq(U,V) )
=> geq(U,W) ) ) ) ),
file('SWC001+0.ax',ax88) ).
fof(ax89,axiom,
! [U] :
( ssItem(U)
=> geq(U,U) ),
file('SWC001+0.ax',ax89) ).
fof(ax90,axiom,
! [U] :
( ssItem(U)
=> ~ lt(U,U) ),
file('SWC001+0.ax',ax90) ).
fof(ax91,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ( ( lt(V,W)
& leq(U,V) )
=> lt(U,W) ) ) ) ),
file('SWC001+0.ax',ax91) ).
fof(ax92,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( leq(U,V)
=> ( lt(U,V)
| U = V ) ) ) ),
file('SWC001+0.ax',ax92) ).
fof(ax93,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( lt(U,V)
<=> ( leq(U,V)
& U != V ) ) ) ),
file('SWC001+0.ax',ax93) ).
fof(ax94,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( gt(U,V)
=> ~ gt(V,U) ) ) ),
file('SWC001+0.ax',ax94) ).
fof(ax95,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ( ( gt(V,W)
& gt(U,V) )
=> gt(U,W) ) ) ) ),
file('SWC001+0.ax',ax95) ).
fof(co1,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( segmentP(V,U)
| ? [Y] :
( equalelemsP(Y)
& segmentP(Y,W)
& segmentP(X,Y)
& neq(W,Y)
& ssList(Y) )
| ~ equalelemsP(W)
| ~ segmentP(X,W)
| ~ neq(V,nil)
| U != W
| V != X ) ) ) ) ),
file('theBenchmark.p',co1) ).
fof(f_1_1,plain,
! [U] :
( ! [V] :
( ( ( neq(U,V)
| U = V )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax1]) ).
fof(f_1_2,plain,
! [U_1] :
( ! [U_0] :
( ( ( neq(U_1,U_0)
| U_1 = U_0 )
& ( U_1 != U_0
| ~ neq(U_1,U_0) ) )
| ~ ssItem(U_0) )
| ~ ssItem(U_1) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_1,U_0] :
( neq(U_1,U_0)
| U_1 = U_0
| ~ sP0(U_1,U_0) )
& ! [U_1,U_0] :
( U_1 != U_0
| ~ neq(U_1,U_0)
| ~ sP0(U_1,U_0) )
& ! [U_1,U_0] :
( sP0(U_1,U_0)
| ~ ssItem(U_0)
| ~ ssItem(U_1) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_1_2]) ).
cnf(f_1_4,plain,
( sP0(U_1,U_0)
| ~ ssItem(U_0)
| ~ ssItem(U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_5,plain,
( U_1 != U_0
| ~ neq(U_1,U_0)
| ~ sP0(U_1,U_0) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_6,plain,
( neq(U_1,U_0)
| U_1 = U_0
| ~ sP0(U_1,U_0) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax2]) ).
fof(f_2_2,plain,
? [U_3] :
( ? [U_2] :
( U_3 != U_2
& ssItem(U_2) )
& ssItem(U_3) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ? [U_2] :
( sK1 != U_2
& ssItem(U_2) )
& ssItem(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_3,sK1)],[f_2_2]) ).
fof(f_2_4,plain,
( sK1 != sK2
& ssItem(sK2)
& ssItem(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_2,sK2)],[f_2_3]) ).
fof(f_2_5,plain,
( sK1 != sK2
& ssItem(sK2)
& ssItem(sK1) ),
inference(definitional_conversion,[status(esa)],[f_2_4]) ).
cnf(f_2_6,plain,
ssItem(sK1),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_7,plain,
ssItem(sK2),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_8,plain,
sK1 != sK2,
inference(clausify,[status(thm)],[f_2_5]) ).
fof(f_3_1,plain,
! [U] :
( ! [V] :
( ( ( memberP(U,V)
| ! [W] :
( ! [X] :
( app(W,cons(V,X)) != U
| ~ ssList(X) )
| ~ ssList(W) ) )
& ( ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) )
| ~ memberP(U,V) ) )
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax3]) ).
fof(f_3_2,plain,
! [U_9] :
( ! [U_8] :
( ( ( memberP(U_9,U_8)
| ! [U_7] :
( ! [U_6] :
( app(U_7,cons(U_8,U_6)) != U_9
| ~ ssList(U_6) )
| ~ ssList(U_7) ) )
& ( ? [U_5] :
( ? [U_4] :
( app(U_5,cons(U_8,U_4)) = U_9
& ssList(U_4) )
& ssList(U_5) )
| ~ memberP(U_9,U_8) ) )
| ~ ssItem(U_8) )
| ~ ssList(U_9) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
! [U_9] :
( ! [U_8] :
( ( ( memberP(U_9,U_8)
| ! [U_7] :
( ! [U_6] :
( app(U_7,cons(U_8,U_6)) != U_9
| ~ ssList(U_6) )
| ~ ssList(U_7) ) )
& ( ( ? [U_4] :
( app(sK3(U_9,U_8),cons(U_8,U_4)) = U_9
& ssList(U_4) )
& ssList(sK3(U_9,U_8)) )
| ~ memberP(U_9,U_8) ) )
| ~ ssItem(U_8) )
| ~ ssList(U_9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_5,sK3(U_9,U_8))],[f_3_2]) ).
fof(f_3_4,plain,
! [U_9] :
( ! [U_8] :
( ( ( memberP(U_9,U_8)
| ! [U_7] :
( ! [U_6] :
( app(U_7,cons(U_8,U_6)) != U_9
| ~ ssList(U_6) )
| ~ ssList(U_7) ) )
& ( ( app(sK3(U_9,U_8),cons(U_8,sK4(U_9,U_8))) = U_9
& ssList(sK4(U_9,U_8))
& ssList(sK3(U_9,U_8)) )
| ~ memberP(U_9,U_8) ) )
| ~ ssItem(U_8) )
| ~ ssList(U_9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_4,sK4(U_9,U_8))],[f_3_3]) ).
fof(f_3_5,plain,
( ! [U_8,U_9] :
( app(sK3(U_9,U_8),cons(U_8,sK4(U_9,U_8))) = U_9
| ~ sP1(U_8,U_9) )
& ! [U_8,U_9] :
( ssList(sK4(U_9,U_8))
| ~ sP1(U_8,U_9) )
& ! [U_8,U_9] :
( ssList(sK3(U_9,U_8))
| ~ sP1(U_8,U_9) )
& ! [U_8,U_7,U_9,U_6] :
( memberP(U_9,U_8)
| app(U_7,cons(U_8,U_6)) != U_9
| ~ ssList(U_6)
| ~ ssList(U_7)
| ~ sP2(U_8,U_7,U_9,U_6) )
& ! [U_8,U_7,U_9,U_6] :
( sP1(U_8,U_9)
| ~ memberP(U_9,U_8)
| ~ sP2(U_8,U_7,U_9,U_6) )
& ! [U_8,U_7,U_9,U_6] :
( sP2(U_8,U_7,U_9,U_6)
| ~ ssItem(U_8)
| ~ ssList(U_9) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP1,sP2])],[f_3_4]) ).
cnf(f_3_6,plain,
( sP2(U_8,U_7,U_9,U_6)
| ~ ssItem(U_8)
| ~ ssList(U_9) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_7,plain,
( sP1(U_8,U_9)
| ~ memberP(U_9,U_8)
| ~ sP2(U_8,U_7,U_9,U_6) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_8,plain,
( memberP(U_9,U_8)
| app(U_7,cons(U_8,U_6)) != U_9
| ~ ssList(U_6)
| ~ ssList(U_7)
| ~ sP2(U_8,U_7,U_9,U_6) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_9,plain,
( ssList(sK3(U_9,U_8))
| ~ sP1(U_8,U_9) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_10,plain,
( ssList(sK4(U_9,U_8))
| ~ sP1(U_8,U_9) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_11,plain,
( app(sK3(U_9,U_8),cons(U_8,sK4(U_9,U_8))) = U_9
| ~ sP1(U_8,U_9) ),
inference(clausify,[status(thm)],[f_3_5]) ).
fof(f_4_1,plain,
! [U] :
( ( ( singletonP(U)
| ! [V] :
( cons(V,nil) != U
| ~ ssItem(V) ) )
& ( ? [V] :
( cons(V,nil) = U
& ssItem(V) )
| ~ singletonP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax4]) ).
fof(f_4_2,plain,
! [U_12] :
( ( ( singletonP(U_12)
| ! [U_11] :
( cons(U_11,nil) != U_12
| ~ ssItem(U_11) ) )
& ( ? [U_10] :
( cons(U_10,nil) = U_12
& ssItem(U_10) )
| ~ singletonP(U_12) ) )
| ~ ssList(U_12) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
! [U_12] :
( ( ( singletonP(U_12)
| ! [U_11] :
( cons(U_11,nil) != U_12
| ~ ssItem(U_11) ) )
& ( ( cons(sK5(U_12),nil) = U_12
& ssItem(sK5(U_12)) )
| ~ singletonP(U_12) ) )
| ~ ssList(U_12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_10,sK5(U_12))],[f_4_2]) ).
fof(f_4_4,plain,
( ! [U_12] :
( cons(sK5(U_12),nil) = U_12
| ~ sP3(U_12) )
& ! [U_12] :
( ssItem(sK5(U_12))
| ~ sP3(U_12) )
& ! [U_12,U_11] :
( singletonP(U_12)
| cons(U_11,nil) != U_12
| ~ ssItem(U_11)
| ~ sP4(U_12,U_11) )
& ! [U_12,U_11] :
( sP3(U_12)
| ~ singletonP(U_12)
| ~ sP4(U_12,U_11) )
& ! [U_12,U_11] :
( sP4(U_12,U_11)
| ~ ssList(U_12) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP3,sP4])],[f_4_3]) ).
cnf(f_4_5,plain,
( sP4(U_12,U_11)
| ~ ssList(U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_6,plain,
( sP3(U_12)
| ~ singletonP(U_12)
| ~ sP4(U_12,U_11) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_7,plain,
( singletonP(U_12)
| cons(U_11,nil) != U_12
| ~ ssItem(U_11)
| ~ sP4(U_12,U_11) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_8,plain,
( ssItem(sK5(U_12))
| ~ sP3(U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_9,plain,
( cons(sK5(U_12),nil) = U_12
| ~ sP3(U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
fof(f_5_1,plain,
! [U] :
( ! [V] :
( ( ( frontsegP(U,V)
| ! [W] :
( app(V,W) != U
| ~ ssList(W) ) )
& ( ? [W] :
( app(V,W) = U
& ssList(W) )
| ~ frontsegP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax5]) ).
fof(f_5_2,plain,
! [U_16] :
( ! [U_15] :
( ( ( frontsegP(U_16,U_15)
| ! [U_14] :
( app(U_15,U_14) != U_16
| ~ ssList(U_14) ) )
& ( ? [U_13] :
( app(U_15,U_13) = U_16
& ssList(U_13) )
| ~ frontsegP(U_16,U_15) ) )
| ~ ssList(U_15) )
| ~ ssList(U_16) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_16] :
( ! [U_15] :
( ( ( frontsegP(U_16,U_15)
| ! [U_14] :
( app(U_15,U_14) != U_16
| ~ ssList(U_14) ) )
& ( ( app(U_15,sK6(U_16,U_15)) = U_16
& ssList(sK6(U_16,U_15)) )
| ~ frontsegP(U_16,U_15) ) )
| ~ ssList(U_15) )
| ~ ssList(U_16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_13,sK6(U_16,U_15))],[f_5_2]) ).
fof(f_5_4,plain,
( ! [U_16,U_15] :
( app(U_15,sK6(U_16,U_15)) = U_16
| ~ sP5(U_16,U_15) )
& ! [U_16,U_15] :
( ssList(sK6(U_16,U_15))
| ~ sP5(U_16,U_15) )
& ! [U_16,U_14,U_15] :
( frontsegP(U_16,U_15)
| app(U_15,U_14) != U_16
| ~ ssList(U_14)
| ~ sP6(U_16,U_14,U_15) )
& ! [U_16,U_14,U_15] :
( sP5(U_16,U_15)
| ~ frontsegP(U_16,U_15)
| ~ sP6(U_16,U_14,U_15) )
& ! [U_16,U_14,U_15] :
( sP6(U_16,U_14,U_15)
| ~ ssList(U_15)
| ~ ssList(U_16) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP5,sP6])],[f_5_3]) ).
cnf(f_5_5,plain,
( sP6(U_16,U_14,U_15)
| ~ ssList(U_15)
| ~ ssList(U_16) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_6,plain,
( sP5(U_16,U_15)
| ~ frontsegP(U_16,U_15)
| ~ sP6(U_16,U_14,U_15) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_7,plain,
( frontsegP(U_16,U_15)
| app(U_15,U_14) != U_16
| ~ ssList(U_14)
| ~ sP6(U_16,U_14,U_15) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_8,plain,
( ssList(sK6(U_16,U_15))
| ~ sP5(U_16,U_15) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_9,plain,
( app(U_15,sK6(U_16,U_15)) = U_16
| ~ sP5(U_16,U_15) ),
inference(clausify,[status(thm)],[f_5_4]) ).
fof(f_6_1,plain,
! [U] :
( ! [V] :
( ( ( rearsegP(U,V)
| ! [W] :
( app(W,V) != U
| ~ ssList(W) ) )
& ( ? [W] :
( app(W,V) = U
& ssList(W) )
| ~ rearsegP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax6]) ).
fof(f_6_2,plain,
! [U_20] :
( ! [U_19] :
( ( ( rearsegP(U_20,U_19)
| ! [U_18] :
( app(U_18,U_19) != U_20
| ~ ssList(U_18) ) )
& ( ? [U_17] :
( app(U_17,U_19) = U_20
& ssList(U_17) )
| ~ rearsegP(U_20,U_19) ) )
| ~ ssList(U_19) )
| ~ ssList(U_20) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_20] :
( ! [U_19] :
( ( ( rearsegP(U_20,U_19)
| ! [U_18] :
( app(U_18,U_19) != U_20
| ~ ssList(U_18) ) )
& ( ( app(sK7(U_20,U_19),U_19) = U_20
& ssList(sK7(U_20,U_19)) )
| ~ rearsegP(U_20,U_19) ) )
| ~ ssList(U_19) )
| ~ ssList(U_20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_17,sK7(U_20,U_19))],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_19,U_20] :
( app(sK7(U_20,U_19),U_19) = U_20
| ~ sP7(U_19,U_20) )
& ! [U_19,U_20] :
( ssList(sK7(U_20,U_19))
| ~ sP7(U_19,U_20) )
& ! [U_19,U_20,U_18] :
( rearsegP(U_20,U_19)
| app(U_18,U_19) != U_20
| ~ ssList(U_18)
| ~ sP8(U_19,U_20,U_18) )
& ! [U_19,U_20,U_18] :
( sP7(U_19,U_20)
| ~ rearsegP(U_20,U_19)
| ~ sP8(U_19,U_20,U_18) )
& ! [U_19,U_20,U_18] :
( sP8(U_19,U_20,U_18)
| ~ ssList(U_19)
| ~ ssList(U_20) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP7,sP8])],[f_6_3]) ).
cnf(f_6_5,plain,
( sP8(U_19,U_20,U_18)
| ~ ssList(U_19)
| ~ ssList(U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_6,plain,
( sP7(U_19,U_20)
| ~ rearsegP(U_20,U_19)
| ~ sP8(U_19,U_20,U_18) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_7,plain,
( rearsegP(U_20,U_19)
| app(U_18,U_19) != U_20
| ~ ssList(U_18)
| ~ sP8(U_19,U_20,U_18) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_8,plain,
( ssList(sK7(U_20,U_19))
| ~ sP7(U_19,U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_9,plain,
( app(sK7(U_20,U_19),U_19) = U_20
| ~ sP7(U_19,U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
fof(f_7_1,plain,
! [U] :
( ! [V] :
( ( ( segmentP(U,V)
| ! [W] :
( ! [X] :
( app(app(W,V),X) != U
| ~ ssList(X) )
| ~ ssList(W) ) )
& ( ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) )
| ~ segmentP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax7]) ).
fof(f_7_2,plain,
! [U_26] :
( ! [U_25] :
( ( ( segmentP(U_26,U_25)
| ! [U_24] :
( ! [U_23] :
( app(app(U_24,U_25),U_23) != U_26
| ~ ssList(U_23) )
| ~ ssList(U_24) ) )
& ( ? [U_22] :
( ? [U_21] :
( app(app(U_22,U_25),U_21) = U_26
& ssList(U_21) )
& ssList(U_22) )
| ~ segmentP(U_26,U_25) ) )
| ~ ssList(U_25) )
| ~ ssList(U_26) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_26] :
( ! [U_25] :
( ( ( segmentP(U_26,U_25)
| ! [U_24] :
( ! [U_23] :
( app(app(U_24,U_25),U_23) != U_26
| ~ ssList(U_23) )
| ~ ssList(U_24) ) )
& ( ( ? [U_21] :
( app(app(sK8(U_26,U_25),U_25),U_21) = U_26
& ssList(U_21) )
& ssList(sK8(U_26,U_25)) )
| ~ segmentP(U_26,U_25) ) )
| ~ ssList(U_25) )
| ~ ssList(U_26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_22,sK8(U_26,U_25))],[f_7_2]) ).
fof(f_7_4,plain,
! [U_26] :
( ! [U_25] :
( ( ( segmentP(U_26,U_25)
| ! [U_24] :
( ! [U_23] :
( app(app(U_24,U_25),U_23) != U_26
| ~ ssList(U_23) )
| ~ ssList(U_24) ) )
& ( ( app(app(sK8(U_26,U_25),U_25),sK9(U_26,U_25)) = U_26
& ssList(sK9(U_26,U_25))
& ssList(sK8(U_26,U_25)) )
| ~ segmentP(U_26,U_25) ) )
| ~ ssList(U_25) )
| ~ ssList(U_26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_21,sK9(U_26,U_25))],[f_7_3]) ).
fof(f_7_5,plain,
( ! [U_25,U_26] :
( app(app(sK8(U_26,U_25),U_25),sK9(U_26,U_25)) = U_26
| ~ sP9(U_25,U_26) )
& ! [U_25,U_26] :
( ssList(sK9(U_26,U_25))
| ~ sP9(U_25,U_26) )
& ! [U_25,U_26] :
( ssList(sK8(U_26,U_25))
| ~ sP9(U_25,U_26) )
& ! [U_24,U_25,U_23,U_26] :
( segmentP(U_26,U_25)
| app(app(U_24,U_25),U_23) != U_26
| ~ ssList(U_23)
| ~ ssList(U_24)
| ~ sP10(U_24,U_25,U_23,U_26) )
& ! [U_24,U_25,U_23,U_26] :
( sP9(U_25,U_26)
| ~ segmentP(U_26,U_25)
| ~ sP10(U_24,U_25,U_23,U_26) )
& ! [U_24,U_25,U_23,U_26] :
( sP10(U_24,U_25,U_23,U_26)
| ~ ssList(U_25)
| ~ ssList(U_26) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP9,sP10])],[f_7_4]) ).
cnf(f_7_6,plain,
( sP10(U_24,U_25,U_23,U_26)
| ~ ssList(U_25)
| ~ ssList(U_26) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_7,plain,
( sP9(U_25,U_26)
| ~ segmentP(U_26,U_25)
| ~ sP10(U_24,U_25,U_23,U_26) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_8,plain,
( segmentP(U_26,U_25)
| app(app(U_24,U_25),U_23) != U_26
| ~ ssList(U_23)
| ~ ssList(U_24)
| ~ sP10(U_24,U_25,U_23,U_26) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_9,plain,
( ssList(sK8(U_26,U_25))
| ~ sP9(U_25,U_26) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_10,plain,
( ssList(sK9(U_26,U_25))
| ~ sP9(U_25,U_26) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_11,plain,
( app(app(sK8(U_26,U_25),U_25),sK9(U_26,U_25)) = U_26
| ~ sP9(U_25,U_26) ),
inference(clausify,[status(thm)],[f_7_5]) ).
fof(f_8_1,plain,
! [U] :
( ( ( cyclefreeP(U)
| ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( leq(W,V)
& leq(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) ) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( ~ leq(W,V)
| ~ leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ cyclefreeP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax8]) ).
fof(f_8_2,plain,
! [U_37] :
( ( ( cyclefreeP(U_37)
| ? [U_36] :
( ? [U_35] :
( ? [U_34] :
( ? [U_33] :
( ? [U_32] :
( leq(U_35,U_36)
& leq(U_36,U_35)
& app(app(U_34,cons(U_36,U_33)),cons(U_35,U_32)) = U_37
& ssList(U_32) )
& ssList(U_33) )
& ssList(U_34) )
& ssItem(U_35) )
& ssItem(U_36) ) )
& ( ! [U_31] :
( ! [U_30] :
( ! [U_29] :
( ! [U_28] :
( ! [U_27] :
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27) )
| ~ ssList(U_28) )
| ~ ssList(U_29) )
| ~ ssItem(U_30) )
| ~ ssItem(U_31) )
| ~ cyclefreeP(U_37) ) )
| ~ ssList(U_37) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
! [U_37] :
( ( ( cyclefreeP(U_37)
| ( ? [U_35] :
( ? [U_34] :
( ? [U_33] :
( ? [U_32] :
( leq(U_35,sK10(U_37))
& leq(sK10(U_37),U_35)
& app(app(U_34,cons(sK10(U_37),U_33)),cons(U_35,U_32)) = U_37
& ssList(U_32) )
& ssList(U_33) )
& ssList(U_34) )
& ssItem(U_35) )
& ssItem(sK10(U_37)) ) )
& ( ! [U_31] :
( ! [U_30] :
( ! [U_29] :
( ! [U_28] :
( ! [U_27] :
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27) )
| ~ ssList(U_28) )
| ~ ssList(U_29) )
| ~ ssItem(U_30) )
| ~ ssItem(U_31) )
| ~ cyclefreeP(U_37) ) )
| ~ ssList(U_37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_36,sK10(U_37))],[f_8_2]) ).
fof(f_8_4,plain,
! [U_37] :
( ( ( cyclefreeP(U_37)
| ( ? [U_34] :
( ? [U_33] :
( ? [U_32] :
( leq(sK11(U_37),sK10(U_37))
& leq(sK10(U_37),sK11(U_37))
& app(app(U_34,cons(sK10(U_37),U_33)),cons(sK11(U_37),U_32)) = U_37
& ssList(U_32) )
& ssList(U_33) )
& ssList(U_34) )
& ssItem(sK11(U_37))
& ssItem(sK10(U_37)) ) )
& ( ! [U_31] :
( ! [U_30] :
( ! [U_29] :
( ! [U_28] :
( ! [U_27] :
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27) )
| ~ ssList(U_28) )
| ~ ssList(U_29) )
| ~ ssItem(U_30) )
| ~ ssItem(U_31) )
| ~ cyclefreeP(U_37) ) )
| ~ ssList(U_37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_35,sK11(U_37))],[f_8_3]) ).
fof(f_8_5,plain,
! [U_37] :
( ( ( cyclefreeP(U_37)
| ( ? [U_33] :
( ? [U_32] :
( leq(sK11(U_37),sK10(U_37))
& leq(sK10(U_37),sK11(U_37))
& app(app(sK12(U_37),cons(sK10(U_37),U_33)),cons(sK11(U_37),U_32)) = U_37
& ssList(U_32) )
& ssList(U_33) )
& ssList(sK12(U_37))
& ssItem(sK11(U_37))
& ssItem(sK10(U_37)) ) )
& ( ! [U_31] :
( ! [U_30] :
( ! [U_29] :
( ! [U_28] :
( ! [U_27] :
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27) )
| ~ ssList(U_28) )
| ~ ssList(U_29) )
| ~ ssItem(U_30) )
| ~ ssItem(U_31) )
| ~ cyclefreeP(U_37) ) )
| ~ ssList(U_37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_34,sK12(U_37))],[f_8_4]) ).
fof(f_8_6,plain,
! [U_37] :
( ( ( cyclefreeP(U_37)
| ( ? [U_32] :
( leq(sK11(U_37),sK10(U_37))
& leq(sK10(U_37),sK11(U_37))
& app(app(sK12(U_37),cons(sK10(U_37),sK13(U_37))),cons(sK11(U_37),U_32)) = U_37
& ssList(U_32) )
& ssList(sK13(U_37))
& ssList(sK12(U_37))
& ssItem(sK11(U_37))
& ssItem(sK10(U_37)) ) )
& ( ! [U_31] :
( ! [U_30] :
( ! [U_29] :
( ! [U_28] :
( ! [U_27] :
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27) )
| ~ ssList(U_28) )
| ~ ssList(U_29) )
| ~ ssItem(U_30) )
| ~ ssItem(U_31) )
| ~ cyclefreeP(U_37) ) )
| ~ ssList(U_37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_33,sK13(U_37))],[f_8_5]) ).
fof(f_8_7,plain,
! [U_37] :
( ( ( cyclefreeP(U_37)
| ( leq(sK11(U_37),sK10(U_37))
& leq(sK10(U_37),sK11(U_37))
& app(app(sK12(U_37),cons(sK10(U_37),sK13(U_37))),cons(sK11(U_37),sK14(U_37))) = U_37
& ssList(sK14(U_37))
& ssList(sK13(U_37))
& ssList(sK12(U_37))
& ssItem(sK11(U_37))
& ssItem(sK10(U_37)) ) )
& ( ! [U_31] :
( ! [U_30] :
( ! [U_29] :
( ! [U_28] :
( ! [U_27] :
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27) )
| ~ ssList(U_28) )
| ~ ssList(U_29) )
| ~ ssItem(U_30) )
| ~ ssItem(U_31) )
| ~ cyclefreeP(U_37) ) )
| ~ ssList(U_37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_32,sK14(U_37))],[f_8_6]) ).
fof(f_8_8,plain,
( ! [U_37] :
( leq(sK11(U_37),sK10(U_37))
| ~ sP11(U_37) )
& ! [U_37] :
( leq(sK10(U_37),sK11(U_37))
| ~ sP11(U_37) )
& ! [U_37] :
( app(app(sK12(U_37),cons(sK10(U_37),sK13(U_37))),cons(sK11(U_37),sK14(U_37))) = U_37
| ~ sP11(U_37) )
& ! [U_37] :
( ssList(sK14(U_37))
| ~ sP11(U_37) )
& ! [U_37] :
( ssList(sK13(U_37))
| ~ sP11(U_37) )
& ! [U_37] :
( ssList(sK12(U_37))
| ~ sP11(U_37) )
& ! [U_37] :
( ssItem(sK11(U_37))
| ~ sP11(U_37) )
& ! [U_37] :
( ssItem(sK10(U_37))
| ~ sP11(U_37) )
& ! [U_30,U_31,U_29,U_28,U_27,U_37] :
( cyclefreeP(U_37)
| sP11(U_37)
| ~ sP12(U_30,U_31,U_29,U_28,U_27,U_37) )
& ! [U_30,U_31,U_29,U_28,U_27,U_37] :
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27)
| ~ ssList(U_28)
| ~ ssList(U_29)
| ~ ssItem(U_30)
| ~ ssItem(U_31)
| ~ cyclefreeP(U_37)
| ~ sP12(U_30,U_31,U_29,U_28,U_27,U_37) )
& ! [U_30,U_31,U_29,U_28,U_27,U_37] :
( sP12(U_30,U_31,U_29,U_28,U_27,U_37)
| ~ ssList(U_37) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP11,sP12])],[f_8_7]) ).
cnf(f_8_9,plain,
( sP12(U_30,U_31,U_29,U_28,U_27,U_37)
| ~ ssList(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_10,plain,
( ~ leq(U_30,U_31)
| ~ leq(U_31,U_30)
| app(app(U_29,cons(U_31,U_28)),cons(U_30,U_27)) != U_37
| ~ ssList(U_27)
| ~ ssList(U_28)
| ~ ssList(U_29)
| ~ ssItem(U_30)
| ~ ssItem(U_31)
| ~ cyclefreeP(U_37)
| ~ sP12(U_30,U_31,U_29,U_28,U_27,U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_11,plain,
( cyclefreeP(U_37)
| sP11(U_37)
| ~ sP12(U_30,U_31,U_29,U_28,U_27,U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_12,plain,
( ssItem(sK10(U_37))
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_13,plain,
( ssItem(sK11(U_37))
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_14,plain,
( ssList(sK12(U_37))
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_15,plain,
( ssList(sK13(U_37))
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_16,plain,
( ssList(sK14(U_37))
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_17,plain,
( app(app(sK12(U_37),cons(sK10(U_37),sK13(U_37))),cons(sK11(U_37),sK14(U_37))) = U_37
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_18,plain,
( leq(sK10(U_37),sK11(U_37))
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
cnf(f_8_19,plain,
( leq(sK11(U_37),sK10(U_37))
| ~ sP11(U_37) ),
inference(clausify,[status(thm)],[f_8_8]) ).
fof(f_9_1,plain,
! [U] :
( ( ( totalorderP(U)
| ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ leq(W,V)
& ~ leq(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) ) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(W,V)
| leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ totalorderP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax9]) ).
fof(f_9_2,plain,
! [U_48] :
( ( ( totalorderP(U_48)
| ? [U_47] :
( ? [U_46] :
( ? [U_45] :
( ? [U_44] :
( ? [U_43] :
( ~ leq(U_46,U_47)
& ~ leq(U_47,U_46)
& app(app(U_45,cons(U_47,U_44)),cons(U_46,U_43)) = U_48
& ssList(U_43) )
& ssList(U_44) )
& ssList(U_45) )
& ssItem(U_46) )
& ssItem(U_47) ) )
& ( ! [U_42] :
( ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ! [U_38] :
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38) )
| ~ ssList(U_39) )
| ~ ssList(U_40) )
| ~ ssItem(U_41) )
| ~ ssItem(U_42) )
| ~ totalorderP(U_48) ) )
| ~ ssList(U_48) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
! [U_48] :
( ( ( totalorderP(U_48)
| ( ? [U_46] :
( ? [U_45] :
( ? [U_44] :
( ? [U_43] :
( ~ leq(U_46,sK15(U_48))
& ~ leq(sK15(U_48),U_46)
& app(app(U_45,cons(sK15(U_48),U_44)),cons(U_46,U_43)) = U_48
& ssList(U_43) )
& ssList(U_44) )
& ssList(U_45) )
& ssItem(U_46) )
& ssItem(sK15(U_48)) ) )
& ( ! [U_42] :
( ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ! [U_38] :
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38) )
| ~ ssList(U_39) )
| ~ ssList(U_40) )
| ~ ssItem(U_41) )
| ~ ssItem(U_42) )
| ~ totalorderP(U_48) ) )
| ~ ssList(U_48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_47,sK15(U_48))],[f_9_2]) ).
fof(f_9_4,plain,
! [U_48] :
( ( ( totalorderP(U_48)
| ( ? [U_45] :
( ? [U_44] :
( ? [U_43] :
( ~ leq(sK16(U_48),sK15(U_48))
& ~ leq(sK15(U_48),sK16(U_48))
& app(app(U_45,cons(sK15(U_48),U_44)),cons(sK16(U_48),U_43)) = U_48
& ssList(U_43) )
& ssList(U_44) )
& ssList(U_45) )
& ssItem(sK16(U_48))
& ssItem(sK15(U_48)) ) )
& ( ! [U_42] :
( ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ! [U_38] :
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38) )
| ~ ssList(U_39) )
| ~ ssList(U_40) )
| ~ ssItem(U_41) )
| ~ ssItem(U_42) )
| ~ totalorderP(U_48) ) )
| ~ ssList(U_48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_46,sK16(U_48))],[f_9_3]) ).
fof(f_9_5,plain,
! [U_48] :
( ( ( totalorderP(U_48)
| ( ? [U_44] :
( ? [U_43] :
( ~ leq(sK16(U_48),sK15(U_48))
& ~ leq(sK15(U_48),sK16(U_48))
& app(app(sK17(U_48),cons(sK15(U_48),U_44)),cons(sK16(U_48),U_43)) = U_48
& ssList(U_43) )
& ssList(U_44) )
& ssList(sK17(U_48))
& ssItem(sK16(U_48))
& ssItem(sK15(U_48)) ) )
& ( ! [U_42] :
( ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ! [U_38] :
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38) )
| ~ ssList(U_39) )
| ~ ssList(U_40) )
| ~ ssItem(U_41) )
| ~ ssItem(U_42) )
| ~ totalorderP(U_48) ) )
| ~ ssList(U_48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_45,sK17(U_48))],[f_9_4]) ).
fof(f_9_6,plain,
! [U_48] :
( ( ( totalorderP(U_48)
| ( ? [U_43] :
( ~ leq(sK16(U_48),sK15(U_48))
& ~ leq(sK15(U_48),sK16(U_48))
& app(app(sK17(U_48),cons(sK15(U_48),sK18(U_48))),cons(sK16(U_48),U_43)) = U_48
& ssList(U_43) )
& ssList(sK18(U_48))
& ssList(sK17(U_48))
& ssItem(sK16(U_48))
& ssItem(sK15(U_48)) ) )
& ( ! [U_42] :
( ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ! [U_38] :
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38) )
| ~ ssList(U_39) )
| ~ ssList(U_40) )
| ~ ssItem(U_41) )
| ~ ssItem(U_42) )
| ~ totalorderP(U_48) ) )
| ~ ssList(U_48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_44,sK18(U_48))],[f_9_5]) ).
fof(f_9_7,plain,
! [U_48] :
( ( ( totalorderP(U_48)
| ( ~ leq(sK16(U_48),sK15(U_48))
& ~ leq(sK15(U_48),sK16(U_48))
& app(app(sK17(U_48),cons(sK15(U_48),sK18(U_48))),cons(sK16(U_48),sK19(U_48))) = U_48
& ssList(sK19(U_48))
& ssList(sK18(U_48))
& ssList(sK17(U_48))
& ssItem(sK16(U_48))
& ssItem(sK15(U_48)) ) )
& ( ! [U_42] :
( ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ! [U_38] :
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38) )
| ~ ssList(U_39) )
| ~ ssList(U_40) )
| ~ ssItem(U_41) )
| ~ ssItem(U_42) )
| ~ totalorderP(U_48) ) )
| ~ ssList(U_48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_43,sK19(U_48))],[f_9_6]) ).
fof(f_9_8,plain,
( ! [U_48] :
( ~ leq(sK16(U_48),sK15(U_48))
| ~ sP13(U_48) )
& ! [U_48] :
( ~ leq(sK15(U_48),sK16(U_48))
| ~ sP13(U_48) )
& ! [U_48] :
( app(app(sK17(U_48),cons(sK15(U_48),sK18(U_48))),cons(sK16(U_48),sK19(U_48))) = U_48
| ~ sP13(U_48) )
& ! [U_48] :
( ssList(sK19(U_48))
| ~ sP13(U_48) )
& ! [U_48] :
( ssList(sK18(U_48))
| ~ sP13(U_48) )
& ! [U_48] :
( ssList(sK17(U_48))
| ~ sP13(U_48) )
& ! [U_48] :
( ssItem(sK16(U_48))
| ~ sP13(U_48) )
& ! [U_48] :
( ssItem(sK15(U_48))
| ~ sP13(U_48) )
& ! [U_42,U_41,U_48,U_40,U_39,U_38] :
( totalorderP(U_48)
| sP13(U_48)
| ~ sP14(U_42,U_41,U_48,U_40,U_39,U_38) )
& ! [U_42,U_41,U_48,U_40,U_39,U_38] :
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38)
| ~ ssList(U_39)
| ~ ssList(U_40)
| ~ ssItem(U_41)
| ~ ssItem(U_42)
| ~ totalorderP(U_48)
| ~ sP14(U_42,U_41,U_48,U_40,U_39,U_38) )
& ! [U_42,U_41,U_48,U_40,U_39,U_38] :
( sP14(U_42,U_41,U_48,U_40,U_39,U_38)
| ~ ssList(U_48) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP13,sP14])],[f_9_7]) ).
cnf(f_9_9,plain,
( sP14(U_42,U_41,U_48,U_40,U_39,U_38)
| ~ ssList(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_10,plain,
( leq(U_41,U_42)
| leq(U_42,U_41)
| app(app(U_40,cons(U_42,U_39)),cons(U_41,U_38)) != U_48
| ~ ssList(U_38)
| ~ ssList(U_39)
| ~ ssList(U_40)
| ~ ssItem(U_41)
| ~ ssItem(U_42)
| ~ totalorderP(U_48)
| ~ sP14(U_42,U_41,U_48,U_40,U_39,U_38) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_11,plain,
( totalorderP(U_48)
| sP13(U_48)
| ~ sP14(U_42,U_41,U_48,U_40,U_39,U_38) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_12,plain,
( ssItem(sK15(U_48))
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_13,plain,
( ssItem(sK16(U_48))
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_14,plain,
( ssList(sK17(U_48))
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_15,plain,
( ssList(sK18(U_48))
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_16,plain,
( ssList(sK19(U_48))
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_17,plain,
( app(app(sK17(U_48),cons(sK15(U_48),sK18(U_48))),cons(sK16(U_48),sK19(U_48))) = U_48
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_18,plain,
( ~ leq(sK15(U_48),sK16(U_48))
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_19,plain,
( ~ leq(sK16(U_48),sK15(U_48))
| ~ sP13(U_48) ),
inference(clausify,[status(thm)],[f_9_8]) ).
fof(f_10_1,plain,
! [U] :
( ( ( strictorderP(U)
| ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ lt(W,V)
& ~ lt(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) ) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(W,V)
| lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ strictorderP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax10]) ).
fof(f_10_2,plain,
! [U_59] :
( ( ( strictorderP(U_59)
| ? [U_58] :
( ? [U_57] :
( ? [U_56] :
( ? [U_55] :
( ? [U_54] :
( ~ lt(U_57,U_58)
& ~ lt(U_58,U_57)
& app(app(U_56,cons(U_58,U_55)),cons(U_57,U_54)) = U_59
& ssList(U_54) )
& ssList(U_55) )
& ssList(U_56) )
& ssItem(U_57) )
& ssItem(U_58) ) )
& ( ! [U_53] :
( ! [U_52] :
( ! [U_51] :
( ! [U_50] :
( ! [U_49] :
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49) )
| ~ ssList(U_50) )
| ~ ssList(U_51) )
| ~ ssItem(U_52) )
| ~ ssItem(U_53) )
| ~ strictorderP(U_59) ) )
| ~ ssList(U_59) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
! [U_59] :
( ( ( strictorderP(U_59)
| ( ? [U_57] :
( ? [U_56] :
( ? [U_55] :
( ? [U_54] :
( ~ lt(U_57,sK20(U_59))
& ~ lt(sK20(U_59),U_57)
& app(app(U_56,cons(sK20(U_59),U_55)),cons(U_57,U_54)) = U_59
& ssList(U_54) )
& ssList(U_55) )
& ssList(U_56) )
& ssItem(U_57) )
& ssItem(sK20(U_59)) ) )
& ( ! [U_53] :
( ! [U_52] :
( ! [U_51] :
( ! [U_50] :
( ! [U_49] :
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49) )
| ~ ssList(U_50) )
| ~ ssList(U_51) )
| ~ ssItem(U_52) )
| ~ ssItem(U_53) )
| ~ strictorderP(U_59) ) )
| ~ ssList(U_59) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_58,sK20(U_59))],[f_10_2]) ).
fof(f_10_4,plain,
! [U_59] :
( ( ( strictorderP(U_59)
| ( ? [U_56] :
( ? [U_55] :
( ? [U_54] :
( ~ lt(sK21(U_59),sK20(U_59))
& ~ lt(sK20(U_59),sK21(U_59))
& app(app(U_56,cons(sK20(U_59),U_55)),cons(sK21(U_59),U_54)) = U_59
& ssList(U_54) )
& ssList(U_55) )
& ssList(U_56) )
& ssItem(sK21(U_59))
& ssItem(sK20(U_59)) ) )
& ( ! [U_53] :
( ! [U_52] :
( ! [U_51] :
( ! [U_50] :
( ! [U_49] :
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49) )
| ~ ssList(U_50) )
| ~ ssList(U_51) )
| ~ ssItem(U_52) )
| ~ ssItem(U_53) )
| ~ strictorderP(U_59) ) )
| ~ ssList(U_59) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_57,sK21(U_59))],[f_10_3]) ).
fof(f_10_5,plain,
! [U_59] :
( ( ( strictorderP(U_59)
| ( ? [U_55] :
( ? [U_54] :
( ~ lt(sK21(U_59),sK20(U_59))
& ~ lt(sK20(U_59),sK21(U_59))
& app(app(sK22(U_59),cons(sK20(U_59),U_55)),cons(sK21(U_59),U_54)) = U_59
& ssList(U_54) )
& ssList(U_55) )
& ssList(sK22(U_59))
& ssItem(sK21(U_59))
& ssItem(sK20(U_59)) ) )
& ( ! [U_53] :
( ! [U_52] :
( ! [U_51] :
( ! [U_50] :
( ! [U_49] :
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49) )
| ~ ssList(U_50) )
| ~ ssList(U_51) )
| ~ ssItem(U_52) )
| ~ ssItem(U_53) )
| ~ strictorderP(U_59) ) )
| ~ ssList(U_59) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_56,sK22(U_59))],[f_10_4]) ).
fof(f_10_6,plain,
! [U_59] :
( ( ( strictorderP(U_59)
| ( ? [U_54] :
( ~ lt(sK21(U_59),sK20(U_59))
& ~ lt(sK20(U_59),sK21(U_59))
& app(app(sK22(U_59),cons(sK20(U_59),sK23(U_59))),cons(sK21(U_59),U_54)) = U_59
& ssList(U_54) )
& ssList(sK23(U_59))
& ssList(sK22(U_59))
& ssItem(sK21(U_59))
& ssItem(sK20(U_59)) ) )
& ( ! [U_53] :
( ! [U_52] :
( ! [U_51] :
( ! [U_50] :
( ! [U_49] :
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49) )
| ~ ssList(U_50) )
| ~ ssList(U_51) )
| ~ ssItem(U_52) )
| ~ ssItem(U_53) )
| ~ strictorderP(U_59) ) )
| ~ ssList(U_59) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_55,sK23(U_59))],[f_10_5]) ).
fof(f_10_7,plain,
! [U_59] :
( ( ( strictorderP(U_59)
| ( ~ lt(sK21(U_59),sK20(U_59))
& ~ lt(sK20(U_59),sK21(U_59))
& app(app(sK22(U_59),cons(sK20(U_59),sK23(U_59))),cons(sK21(U_59),sK24(U_59))) = U_59
& ssList(sK24(U_59))
& ssList(sK23(U_59))
& ssList(sK22(U_59))
& ssItem(sK21(U_59))
& ssItem(sK20(U_59)) ) )
& ( ! [U_53] :
( ! [U_52] :
( ! [U_51] :
( ! [U_50] :
( ! [U_49] :
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49) )
| ~ ssList(U_50) )
| ~ ssList(U_51) )
| ~ ssItem(U_52) )
| ~ ssItem(U_53) )
| ~ strictorderP(U_59) ) )
| ~ ssList(U_59) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_54,sK24(U_59))],[f_10_6]) ).
fof(f_10_8,plain,
( ! [U_59] :
( ~ lt(sK21(U_59),sK20(U_59))
| ~ sP15(U_59) )
& ! [U_59] :
( ~ lt(sK20(U_59),sK21(U_59))
| ~ sP15(U_59) )
& ! [U_59] :
( app(app(sK22(U_59),cons(sK20(U_59),sK23(U_59))),cons(sK21(U_59),sK24(U_59))) = U_59
| ~ sP15(U_59) )
& ! [U_59] :
( ssList(sK24(U_59))
| ~ sP15(U_59) )
& ! [U_59] :
( ssList(sK23(U_59))
| ~ sP15(U_59) )
& ! [U_59] :
( ssList(sK22(U_59))
| ~ sP15(U_59) )
& ! [U_59] :
( ssItem(sK21(U_59))
| ~ sP15(U_59) )
& ! [U_59] :
( ssItem(sK20(U_59))
| ~ sP15(U_59) )
& ! [U_50,U_52,U_53,U_59,U_49,U_51] :
( strictorderP(U_59)
| sP15(U_59)
| ~ sP16(U_50,U_52,U_53,U_59,U_49,U_51) )
& ! [U_50,U_52,U_53,U_59,U_49,U_51] :
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49)
| ~ ssList(U_50)
| ~ ssList(U_51)
| ~ ssItem(U_52)
| ~ ssItem(U_53)
| ~ strictorderP(U_59)
| ~ sP16(U_50,U_52,U_53,U_59,U_49,U_51) )
& ! [U_50,U_52,U_53,U_59,U_49,U_51] :
( sP16(U_50,U_52,U_53,U_59,U_49,U_51)
| ~ ssList(U_59) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP15,sP16])],[f_10_7]) ).
cnf(f_10_9,plain,
( sP16(U_50,U_52,U_53,U_59,U_49,U_51)
| ~ ssList(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_10,plain,
( lt(U_52,U_53)
| lt(U_53,U_52)
| app(app(U_51,cons(U_53,U_50)),cons(U_52,U_49)) != U_59
| ~ ssList(U_49)
| ~ ssList(U_50)
| ~ ssList(U_51)
| ~ ssItem(U_52)
| ~ ssItem(U_53)
| ~ strictorderP(U_59)
| ~ sP16(U_50,U_52,U_53,U_59,U_49,U_51) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_11,plain,
( strictorderP(U_59)
| sP15(U_59)
| ~ sP16(U_50,U_52,U_53,U_59,U_49,U_51) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_12,plain,
( ssItem(sK20(U_59))
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_13,plain,
( ssItem(sK21(U_59))
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_14,plain,
( ssList(sK22(U_59))
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_15,plain,
( ssList(sK23(U_59))
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_16,plain,
( ssList(sK24(U_59))
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_17,plain,
( app(app(sK22(U_59),cons(sK20(U_59),sK23(U_59))),cons(sK21(U_59),sK24(U_59))) = U_59
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_18,plain,
( ~ lt(sK20(U_59),sK21(U_59))
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
cnf(f_10_19,plain,
( ~ lt(sK21(U_59),sK20(U_59))
| ~ sP15(U_59) ),
inference(clausify,[status(thm)],[f_10_8]) ).
fof(f_11_1,plain,
! [U] :
( ( ( totalorderedP(U)
| ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ leq(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) ) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ totalorderedP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax11]) ).
fof(f_11_2,plain,
! [U_70] :
( ( ( totalorderedP(U_70)
| ? [U_69] :
( ? [U_68] :
( ? [U_67] :
( ? [U_66] :
( ? [U_65] :
( ~ leq(U_69,U_68)
& app(app(U_67,cons(U_69,U_66)),cons(U_68,U_65)) = U_70
& ssList(U_65) )
& ssList(U_66) )
& ssList(U_67) )
& ssItem(U_68) )
& ssItem(U_69) ) )
& ( ! [U_64] :
( ! [U_63] :
( ! [U_62] :
( ! [U_61] :
( ! [U_60] :
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60) )
| ~ ssList(U_61) )
| ~ ssList(U_62) )
| ~ ssItem(U_63) )
| ~ ssItem(U_64) )
| ~ totalorderedP(U_70) ) )
| ~ ssList(U_70) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
! [U_70] :
( ( ( totalorderedP(U_70)
| ( ? [U_68] :
( ? [U_67] :
( ? [U_66] :
( ? [U_65] :
( ~ leq(sK25(U_70),U_68)
& app(app(U_67,cons(sK25(U_70),U_66)),cons(U_68,U_65)) = U_70
& ssList(U_65) )
& ssList(U_66) )
& ssList(U_67) )
& ssItem(U_68) )
& ssItem(sK25(U_70)) ) )
& ( ! [U_64] :
( ! [U_63] :
( ! [U_62] :
( ! [U_61] :
( ! [U_60] :
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60) )
| ~ ssList(U_61) )
| ~ ssList(U_62) )
| ~ ssItem(U_63) )
| ~ ssItem(U_64) )
| ~ totalorderedP(U_70) ) )
| ~ ssList(U_70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_69,sK25(U_70))],[f_11_2]) ).
fof(f_11_4,plain,
! [U_70] :
( ( ( totalorderedP(U_70)
| ( ? [U_67] :
( ? [U_66] :
( ? [U_65] :
( ~ leq(sK25(U_70),sK26(U_70))
& app(app(U_67,cons(sK25(U_70),U_66)),cons(sK26(U_70),U_65)) = U_70
& ssList(U_65) )
& ssList(U_66) )
& ssList(U_67) )
& ssItem(sK26(U_70))
& ssItem(sK25(U_70)) ) )
& ( ! [U_64] :
( ! [U_63] :
( ! [U_62] :
( ! [U_61] :
( ! [U_60] :
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60) )
| ~ ssList(U_61) )
| ~ ssList(U_62) )
| ~ ssItem(U_63) )
| ~ ssItem(U_64) )
| ~ totalorderedP(U_70) ) )
| ~ ssList(U_70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_68,sK26(U_70))],[f_11_3]) ).
fof(f_11_5,plain,
! [U_70] :
( ( ( totalorderedP(U_70)
| ( ? [U_66] :
( ? [U_65] :
( ~ leq(sK25(U_70),sK26(U_70))
& app(app(sK27(U_70),cons(sK25(U_70),U_66)),cons(sK26(U_70),U_65)) = U_70
& ssList(U_65) )
& ssList(U_66) )
& ssList(sK27(U_70))
& ssItem(sK26(U_70))
& ssItem(sK25(U_70)) ) )
& ( ! [U_64] :
( ! [U_63] :
( ! [U_62] :
( ! [U_61] :
( ! [U_60] :
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60) )
| ~ ssList(U_61) )
| ~ ssList(U_62) )
| ~ ssItem(U_63) )
| ~ ssItem(U_64) )
| ~ totalorderedP(U_70) ) )
| ~ ssList(U_70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_67,sK27(U_70))],[f_11_4]) ).
fof(f_11_6,plain,
! [U_70] :
( ( ( totalorderedP(U_70)
| ( ? [U_65] :
( ~ leq(sK25(U_70),sK26(U_70))
& app(app(sK27(U_70),cons(sK25(U_70),sK28(U_70))),cons(sK26(U_70),U_65)) = U_70
& ssList(U_65) )
& ssList(sK28(U_70))
& ssList(sK27(U_70))
& ssItem(sK26(U_70))
& ssItem(sK25(U_70)) ) )
& ( ! [U_64] :
( ! [U_63] :
( ! [U_62] :
( ! [U_61] :
( ! [U_60] :
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60) )
| ~ ssList(U_61) )
| ~ ssList(U_62) )
| ~ ssItem(U_63) )
| ~ ssItem(U_64) )
| ~ totalorderedP(U_70) ) )
| ~ ssList(U_70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_66,sK28(U_70))],[f_11_5]) ).
fof(f_11_7,plain,
! [U_70] :
( ( ( totalorderedP(U_70)
| ( ~ leq(sK25(U_70),sK26(U_70))
& app(app(sK27(U_70),cons(sK25(U_70),sK28(U_70))),cons(sK26(U_70),sK29(U_70))) = U_70
& ssList(sK29(U_70))
& ssList(sK28(U_70))
& ssList(sK27(U_70))
& ssItem(sK26(U_70))
& ssItem(sK25(U_70)) ) )
& ( ! [U_64] :
( ! [U_63] :
( ! [U_62] :
( ! [U_61] :
( ! [U_60] :
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60) )
| ~ ssList(U_61) )
| ~ ssList(U_62) )
| ~ ssItem(U_63) )
| ~ ssItem(U_64) )
| ~ totalorderedP(U_70) ) )
| ~ ssList(U_70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_65,sK29(U_70))],[f_11_6]) ).
fof(f_11_8,plain,
( ! [U_70] :
( ~ leq(sK25(U_70),sK26(U_70))
| ~ sP17(U_70) )
& ! [U_70] :
( app(app(sK27(U_70),cons(sK25(U_70),sK28(U_70))),cons(sK26(U_70),sK29(U_70))) = U_70
| ~ sP17(U_70) )
& ! [U_70] :
( ssList(sK29(U_70))
| ~ sP17(U_70) )
& ! [U_70] :
( ssList(sK28(U_70))
| ~ sP17(U_70) )
& ! [U_70] :
( ssList(sK27(U_70))
| ~ sP17(U_70) )
& ! [U_70] :
( ssItem(sK26(U_70))
| ~ sP17(U_70) )
& ! [U_70] :
( ssItem(sK25(U_70))
| ~ sP17(U_70) )
& ! [U_64,U_60,U_63,U_61,U_70,U_62] :
( totalorderedP(U_70)
| sP17(U_70)
| ~ sP18(U_64,U_60,U_63,U_61,U_70,U_62) )
& ! [U_64,U_60,U_63,U_61,U_70,U_62] :
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60)
| ~ ssList(U_61)
| ~ ssList(U_62)
| ~ ssItem(U_63)
| ~ ssItem(U_64)
| ~ totalorderedP(U_70)
| ~ sP18(U_64,U_60,U_63,U_61,U_70,U_62) )
& ! [U_64,U_60,U_63,U_61,U_70,U_62] :
( sP18(U_64,U_60,U_63,U_61,U_70,U_62)
| ~ ssList(U_70) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP17,sP18])],[f_11_7]) ).
cnf(f_11_9,plain,
( sP18(U_64,U_60,U_63,U_61,U_70,U_62)
| ~ ssList(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_10,plain,
( leq(U_64,U_63)
| app(app(U_62,cons(U_64,U_61)),cons(U_63,U_60)) != U_70
| ~ ssList(U_60)
| ~ ssList(U_61)
| ~ ssList(U_62)
| ~ ssItem(U_63)
| ~ ssItem(U_64)
| ~ totalorderedP(U_70)
| ~ sP18(U_64,U_60,U_63,U_61,U_70,U_62) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_11,plain,
( totalorderedP(U_70)
| sP17(U_70)
| ~ sP18(U_64,U_60,U_63,U_61,U_70,U_62) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_12,plain,
( ssItem(sK25(U_70))
| ~ sP17(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_13,plain,
( ssItem(sK26(U_70))
| ~ sP17(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_14,plain,
( ssList(sK27(U_70))
| ~ sP17(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_15,plain,
( ssList(sK28(U_70))
| ~ sP17(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_16,plain,
( ssList(sK29(U_70))
| ~ sP17(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_17,plain,
( app(app(sK27(U_70),cons(sK25(U_70),sK28(U_70))),cons(sK26(U_70),sK29(U_70))) = U_70
| ~ sP17(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
cnf(f_11_18,plain,
( ~ leq(sK25(U_70),sK26(U_70))
| ~ sP17(U_70) ),
inference(clausify,[status(thm)],[f_11_8]) ).
fof(f_12_1,plain,
! [U] :
( ( ( strictorderedP(U)
| ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ lt(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) ) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ strictorderedP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax12]) ).
fof(f_12_2,plain,
! [U_81] :
( ( ( strictorderedP(U_81)
| ? [U_80] :
( ? [U_79] :
( ? [U_78] :
( ? [U_77] :
( ? [U_76] :
( ~ lt(U_80,U_79)
& app(app(U_78,cons(U_80,U_77)),cons(U_79,U_76)) = U_81
& ssList(U_76) )
& ssList(U_77) )
& ssList(U_78) )
& ssItem(U_79) )
& ssItem(U_80) ) )
& ( ! [U_75] :
( ! [U_74] :
( ! [U_73] :
( ! [U_72] :
( ! [U_71] :
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71) )
| ~ ssList(U_72) )
| ~ ssList(U_73) )
| ~ ssItem(U_74) )
| ~ ssItem(U_75) )
| ~ strictorderedP(U_81) ) )
| ~ ssList(U_81) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
! [U_81] :
( ( ( strictorderedP(U_81)
| ( ? [U_79] :
( ? [U_78] :
( ? [U_77] :
( ? [U_76] :
( ~ lt(sK30(U_81),U_79)
& app(app(U_78,cons(sK30(U_81),U_77)),cons(U_79,U_76)) = U_81
& ssList(U_76) )
& ssList(U_77) )
& ssList(U_78) )
& ssItem(U_79) )
& ssItem(sK30(U_81)) ) )
& ( ! [U_75] :
( ! [U_74] :
( ! [U_73] :
( ! [U_72] :
( ! [U_71] :
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71) )
| ~ ssList(U_72) )
| ~ ssList(U_73) )
| ~ ssItem(U_74) )
| ~ ssItem(U_75) )
| ~ strictorderedP(U_81) ) )
| ~ ssList(U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_80,sK30(U_81))],[f_12_2]) ).
fof(f_12_4,plain,
! [U_81] :
( ( ( strictorderedP(U_81)
| ( ? [U_78] :
( ? [U_77] :
( ? [U_76] :
( ~ lt(sK30(U_81),sK31(U_81))
& app(app(U_78,cons(sK30(U_81),U_77)),cons(sK31(U_81),U_76)) = U_81
& ssList(U_76) )
& ssList(U_77) )
& ssList(U_78) )
& ssItem(sK31(U_81))
& ssItem(sK30(U_81)) ) )
& ( ! [U_75] :
( ! [U_74] :
( ! [U_73] :
( ! [U_72] :
( ! [U_71] :
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71) )
| ~ ssList(U_72) )
| ~ ssList(U_73) )
| ~ ssItem(U_74) )
| ~ ssItem(U_75) )
| ~ strictorderedP(U_81) ) )
| ~ ssList(U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_79,sK31(U_81))],[f_12_3]) ).
fof(f_12_5,plain,
! [U_81] :
( ( ( strictorderedP(U_81)
| ( ? [U_77] :
( ? [U_76] :
( ~ lt(sK30(U_81),sK31(U_81))
& app(app(sK32(U_81),cons(sK30(U_81),U_77)),cons(sK31(U_81),U_76)) = U_81
& ssList(U_76) )
& ssList(U_77) )
& ssList(sK32(U_81))
& ssItem(sK31(U_81))
& ssItem(sK30(U_81)) ) )
& ( ! [U_75] :
( ! [U_74] :
( ! [U_73] :
( ! [U_72] :
( ! [U_71] :
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71) )
| ~ ssList(U_72) )
| ~ ssList(U_73) )
| ~ ssItem(U_74) )
| ~ ssItem(U_75) )
| ~ strictorderedP(U_81) ) )
| ~ ssList(U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_78,sK32(U_81))],[f_12_4]) ).
fof(f_12_6,plain,
! [U_81] :
( ( ( strictorderedP(U_81)
| ( ? [U_76] :
( ~ lt(sK30(U_81),sK31(U_81))
& app(app(sK32(U_81),cons(sK30(U_81),sK33(U_81))),cons(sK31(U_81),U_76)) = U_81
& ssList(U_76) )
& ssList(sK33(U_81))
& ssList(sK32(U_81))
& ssItem(sK31(U_81))
& ssItem(sK30(U_81)) ) )
& ( ! [U_75] :
( ! [U_74] :
( ! [U_73] :
( ! [U_72] :
( ! [U_71] :
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71) )
| ~ ssList(U_72) )
| ~ ssList(U_73) )
| ~ ssItem(U_74) )
| ~ ssItem(U_75) )
| ~ strictorderedP(U_81) ) )
| ~ ssList(U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(U_77,sK33(U_81))],[f_12_5]) ).
fof(f_12_7,plain,
! [U_81] :
( ( ( strictorderedP(U_81)
| ( ~ lt(sK30(U_81),sK31(U_81))
& app(app(sK32(U_81),cons(sK30(U_81),sK33(U_81))),cons(sK31(U_81),sK34(U_81))) = U_81
& ssList(sK34(U_81))
& ssList(sK33(U_81))
& ssList(sK32(U_81))
& ssItem(sK31(U_81))
& ssItem(sK30(U_81)) ) )
& ( ! [U_75] :
( ! [U_74] :
( ! [U_73] :
( ! [U_72] :
( ! [U_71] :
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71) )
| ~ ssList(U_72) )
| ~ ssList(U_73) )
| ~ ssItem(U_74) )
| ~ ssItem(U_75) )
| ~ strictorderedP(U_81) ) )
| ~ ssList(U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(U_76,sK34(U_81))],[f_12_6]) ).
fof(f_12_8,plain,
( ! [U_81] :
( ~ lt(sK30(U_81),sK31(U_81))
| ~ sP19(U_81) )
& ! [U_81] :
( app(app(sK32(U_81),cons(sK30(U_81),sK33(U_81))),cons(sK31(U_81),sK34(U_81))) = U_81
| ~ sP19(U_81) )
& ! [U_81] :
( ssList(sK34(U_81))
| ~ sP19(U_81) )
& ! [U_81] :
( ssList(sK33(U_81))
| ~ sP19(U_81) )
& ! [U_81] :
( ssList(sK32(U_81))
| ~ sP19(U_81) )
& ! [U_81] :
( ssItem(sK31(U_81))
| ~ sP19(U_81) )
& ! [U_81] :
( ssItem(sK30(U_81))
| ~ sP19(U_81) )
& ! [U_72,U_74,U_81,U_75,U_73,U_71] :
( strictorderedP(U_81)
| sP19(U_81)
| ~ sP20(U_72,U_74,U_81,U_75,U_73,U_71) )
& ! [U_72,U_74,U_81,U_75,U_73,U_71] :
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71)
| ~ ssList(U_72)
| ~ ssList(U_73)
| ~ ssItem(U_74)
| ~ ssItem(U_75)
| ~ strictorderedP(U_81)
| ~ sP20(U_72,U_74,U_81,U_75,U_73,U_71) )
& ! [U_72,U_74,U_81,U_75,U_73,U_71] :
( sP20(U_72,U_74,U_81,U_75,U_73,U_71)
| ~ ssList(U_81) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP19,sP20])],[f_12_7]) ).
cnf(f_12_9,plain,
( sP20(U_72,U_74,U_81,U_75,U_73,U_71)
| ~ ssList(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_10,plain,
( lt(U_75,U_74)
| app(app(U_73,cons(U_75,U_72)),cons(U_74,U_71)) != U_81
| ~ ssList(U_71)
| ~ ssList(U_72)
| ~ ssList(U_73)
| ~ ssItem(U_74)
| ~ ssItem(U_75)
| ~ strictorderedP(U_81)
| ~ sP20(U_72,U_74,U_81,U_75,U_73,U_71) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_11,plain,
( strictorderedP(U_81)
| sP19(U_81)
| ~ sP20(U_72,U_74,U_81,U_75,U_73,U_71) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_12,plain,
( ssItem(sK30(U_81))
| ~ sP19(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_13,plain,
( ssItem(sK31(U_81))
| ~ sP19(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_14,plain,
( ssList(sK32(U_81))
| ~ sP19(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_15,plain,
( ssList(sK33(U_81))
| ~ sP19(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_16,plain,
( ssList(sK34(U_81))
| ~ sP19(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_17,plain,
( app(app(sK32(U_81),cons(sK30(U_81),sK33(U_81))),cons(sK31(U_81),sK34(U_81))) = U_81
| ~ sP19(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_18,plain,
( ~ lt(sK30(U_81),sK31(U_81))
| ~ sP19(U_81) ),
inference(clausify,[status(thm)],[f_12_8]) ).
fof(f_13_1,plain,
! [U] :
( ( ( duplicatefreeP(U)
| ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( V = W
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) ) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( V != W
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ duplicatefreeP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax13]) ).
fof(f_13_2,plain,
! [U_92] :
( ( ( duplicatefreeP(U_92)
| ? [U_91] :
( ? [U_90] :
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( U_91 = U_90
& app(app(U_89,cons(U_91,U_88)),cons(U_90,U_87)) = U_92
& ssList(U_87) )
& ssList(U_88) )
& ssList(U_89) )
& ssItem(U_90) )
& ssItem(U_91) ) )
& ( ! [U_86] :
( ! [U_85] :
( ! [U_84] :
( ! [U_83] :
( ! [U_82] :
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82) )
| ~ ssList(U_83) )
| ~ ssList(U_84) )
| ~ ssItem(U_85) )
| ~ ssItem(U_86) )
| ~ duplicatefreeP(U_92) ) )
| ~ ssList(U_92) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
! [U_92] :
( ( ( duplicatefreeP(U_92)
| ( ? [U_90] :
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( sK35(U_92) = U_90
& app(app(U_89,cons(sK35(U_92),U_88)),cons(U_90,U_87)) = U_92
& ssList(U_87) )
& ssList(U_88) )
& ssList(U_89) )
& ssItem(U_90) )
& ssItem(sK35(U_92)) ) )
& ( ! [U_86] :
( ! [U_85] :
( ! [U_84] :
( ! [U_83] :
( ! [U_82] :
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82) )
| ~ ssList(U_83) )
| ~ ssList(U_84) )
| ~ ssItem(U_85) )
| ~ ssItem(U_86) )
| ~ duplicatefreeP(U_92) ) )
| ~ ssList(U_92) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(U_91,sK35(U_92))],[f_13_2]) ).
fof(f_13_4,plain,
! [U_92] :
( ( ( duplicatefreeP(U_92)
| ( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( sK35(U_92) = sK36(U_92)
& app(app(U_89,cons(sK35(U_92),U_88)),cons(sK36(U_92),U_87)) = U_92
& ssList(U_87) )
& ssList(U_88) )
& ssList(U_89) )
& ssItem(sK36(U_92))
& ssItem(sK35(U_92)) ) )
& ( ! [U_86] :
( ! [U_85] :
( ! [U_84] :
( ! [U_83] :
( ! [U_82] :
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82) )
| ~ ssList(U_83) )
| ~ ssList(U_84) )
| ~ ssItem(U_85) )
| ~ ssItem(U_86) )
| ~ duplicatefreeP(U_92) ) )
| ~ ssList(U_92) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(U_90,sK36(U_92))],[f_13_3]) ).
fof(f_13_5,plain,
! [U_92] :
( ( ( duplicatefreeP(U_92)
| ( ? [U_88] :
( ? [U_87] :
( sK35(U_92) = sK36(U_92)
& app(app(sK37(U_92),cons(sK35(U_92),U_88)),cons(sK36(U_92),U_87)) = U_92
& ssList(U_87) )
& ssList(U_88) )
& ssList(sK37(U_92))
& ssItem(sK36(U_92))
& ssItem(sK35(U_92)) ) )
& ( ! [U_86] :
( ! [U_85] :
( ! [U_84] :
( ! [U_83] :
( ! [U_82] :
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82) )
| ~ ssList(U_83) )
| ~ ssList(U_84) )
| ~ ssItem(U_85) )
| ~ ssItem(U_86) )
| ~ duplicatefreeP(U_92) ) )
| ~ ssList(U_92) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(U_89,sK37(U_92))],[f_13_4]) ).
fof(f_13_6,plain,
! [U_92] :
( ( ( duplicatefreeP(U_92)
| ( ? [U_87] :
( sK35(U_92) = sK36(U_92)
& app(app(sK37(U_92),cons(sK35(U_92),sK38(U_92))),cons(sK36(U_92),U_87)) = U_92
& ssList(U_87) )
& ssList(sK38(U_92))
& ssList(sK37(U_92))
& ssItem(sK36(U_92))
& ssItem(sK35(U_92)) ) )
& ( ! [U_86] :
( ! [U_85] :
( ! [U_84] :
( ! [U_83] :
( ! [U_82] :
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82) )
| ~ ssList(U_83) )
| ~ ssList(U_84) )
| ~ ssItem(U_85) )
| ~ ssItem(U_86) )
| ~ duplicatefreeP(U_92) ) )
| ~ ssList(U_92) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(U_88,sK38(U_92))],[f_13_5]) ).
fof(f_13_7,plain,
! [U_92] :
( ( ( duplicatefreeP(U_92)
| ( sK35(U_92) = sK36(U_92)
& app(app(sK37(U_92),cons(sK35(U_92),sK38(U_92))),cons(sK36(U_92),sK39(U_92))) = U_92
& ssList(sK39(U_92))
& ssList(sK38(U_92))
& ssList(sK37(U_92))
& ssItem(sK36(U_92))
& ssItem(sK35(U_92)) ) )
& ( ! [U_86] :
( ! [U_85] :
( ! [U_84] :
( ! [U_83] :
( ! [U_82] :
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82) )
| ~ ssList(U_83) )
| ~ ssList(U_84) )
| ~ ssItem(U_85) )
| ~ ssItem(U_86) )
| ~ duplicatefreeP(U_92) ) )
| ~ ssList(U_92) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(U_87,sK39(U_92))],[f_13_6]) ).
fof(f_13_8,plain,
( ! [U_92] :
( sK35(U_92) = sK36(U_92)
| ~ sP21(U_92) )
& ! [U_92] :
( app(app(sK37(U_92),cons(sK35(U_92),sK38(U_92))),cons(sK36(U_92),sK39(U_92))) = U_92
| ~ sP21(U_92) )
& ! [U_92] :
( ssList(sK39(U_92))
| ~ sP21(U_92) )
& ! [U_92] :
( ssList(sK38(U_92))
| ~ sP21(U_92) )
& ! [U_92] :
( ssList(sK37(U_92))
| ~ sP21(U_92) )
& ! [U_92] :
( ssItem(sK36(U_92))
| ~ sP21(U_92) )
& ! [U_92] :
( ssItem(sK35(U_92))
| ~ sP21(U_92) )
& ! [U_82,U_84,U_86,U_83,U_85,U_92] :
( duplicatefreeP(U_92)
| sP21(U_92)
| ~ sP22(U_82,U_84,U_86,U_83,U_85,U_92) )
& ! [U_82,U_84,U_86,U_83,U_85,U_92] :
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82)
| ~ ssList(U_83)
| ~ ssList(U_84)
| ~ ssItem(U_85)
| ~ ssItem(U_86)
| ~ duplicatefreeP(U_92)
| ~ sP22(U_82,U_84,U_86,U_83,U_85,U_92) )
& ! [U_82,U_84,U_86,U_83,U_85,U_92] :
( sP22(U_82,U_84,U_86,U_83,U_85,U_92)
| ~ ssList(U_92) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP21,sP22])],[f_13_7]) ).
cnf(f_13_9,plain,
( sP22(U_82,U_84,U_86,U_83,U_85,U_92)
| ~ ssList(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_10,plain,
( U_86 != U_85
| app(app(U_84,cons(U_86,U_83)),cons(U_85,U_82)) != U_92
| ~ ssList(U_82)
| ~ ssList(U_83)
| ~ ssList(U_84)
| ~ ssItem(U_85)
| ~ ssItem(U_86)
| ~ duplicatefreeP(U_92)
| ~ sP22(U_82,U_84,U_86,U_83,U_85,U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_11,plain,
( duplicatefreeP(U_92)
| sP21(U_92)
| ~ sP22(U_82,U_84,U_86,U_83,U_85,U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_12,plain,
( ssItem(sK35(U_92))
| ~ sP21(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_13,plain,
( ssItem(sK36(U_92))
| ~ sP21(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_14,plain,
( ssList(sK37(U_92))
| ~ sP21(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_15,plain,
( ssList(sK38(U_92))
| ~ sP21(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_16,plain,
( ssList(sK39(U_92))
| ~ sP21(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_17,plain,
( app(app(sK37(U_92),cons(sK35(U_92),sK38(U_92))),cons(sK36(U_92),sK39(U_92))) = U_92
| ~ sP21(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
cnf(f_13_18,plain,
( sK35(U_92) = sK36(U_92)
| ~ sP21(U_92) ),
inference(clausify,[status(thm)],[f_13_8]) ).
fof(f_14_1,plain,
! [U] :
( ( ( equalelemsP(U)
| ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( V != W
& app(X,cons(V,cons(W,Y))) = U
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) ) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( V = W
| app(X,cons(V,cons(W,Y))) != U
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ equalelemsP(U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax14]) ).
fof(f_14_2,plain,
! [U_101] :
( ( ( equalelemsP(U_101)
| ? [U_100] :
( ? [U_99] :
( ? [U_98] :
( ? [U_97] :
( U_100 != U_99
& app(U_98,cons(U_100,cons(U_99,U_97))) = U_101
& ssList(U_97) )
& ssList(U_98) )
& ssItem(U_99) )
& ssItem(U_100) ) )
& ( ! [U_96] :
( ! [U_95] :
( ! [U_94] :
( ! [U_93] :
( U_96 = U_95
| app(U_94,cons(U_96,cons(U_95,U_93))) != U_101
| ~ ssList(U_93) )
| ~ ssList(U_94) )
| ~ ssItem(U_95) )
| ~ ssItem(U_96) )
| ~ equalelemsP(U_101) ) )
| ~ ssList(U_101) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
! [U_101] :
( ( ( equalelemsP(U_101)
| ( ? [U_99] :
( ? [U_98] :
( ? [U_97] :
( sK40(U_101) != U_99
& app(U_98,cons(sK40(U_101),cons(U_99,U_97))) = U_101
& ssList(U_97) )
& ssList(U_98) )
& ssItem(U_99) )
& ssItem(sK40(U_101)) ) )
& ( ! [U_96] :
( ! [U_95] :
( ! [U_94] :
( ! [U_93] :
( U_96 = U_95
| app(U_94,cons(U_96,cons(U_95,U_93))) != U_101
| ~ ssList(U_93) )
| ~ ssList(U_94) )
| ~ ssItem(U_95) )
| ~ ssItem(U_96) )
| ~ equalelemsP(U_101) ) )
| ~ ssList(U_101) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(U_100,sK40(U_101))],[f_14_2]) ).
fof(f_14_4,plain,
! [U_101] :
( ( ( equalelemsP(U_101)
| ( ? [U_98] :
( ? [U_97] :
( sK40(U_101) != sK41(U_101)
& app(U_98,cons(sK40(U_101),cons(sK41(U_101),U_97))) = U_101
& ssList(U_97) )
& ssList(U_98) )
& ssItem(sK41(U_101))
& ssItem(sK40(U_101)) ) )
& ( ! [U_96] :
( ! [U_95] :
( ! [U_94] :
( ! [U_93] :
( U_96 = U_95
| app(U_94,cons(U_96,cons(U_95,U_93))) != U_101
| ~ ssList(U_93) )
| ~ ssList(U_94) )
| ~ ssItem(U_95) )
| ~ ssItem(U_96) )
| ~ equalelemsP(U_101) ) )
| ~ ssList(U_101) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(U_99,sK41(U_101))],[f_14_3]) ).
fof(f_14_5,plain,
! [U_101] :
( ( ( equalelemsP(U_101)
| ( ? [U_97] :
( sK40(U_101) != sK41(U_101)
& app(sK42(U_101),cons(sK40(U_101),cons(sK41(U_101),U_97))) = U_101
& ssList(U_97) )
& ssList(sK42(U_101))
& ssItem(sK41(U_101))
& ssItem(sK40(U_101)) ) )
& ( ! [U_96] :
( ! [U_95] :
( ! [U_94] :
( ! [U_93] :
( U_96 = U_95
| app(U_94,cons(U_96,cons(U_95,U_93))) != U_101
| ~ ssList(U_93) )
| ~ ssList(U_94) )
| ~ ssItem(U_95) )
| ~ ssItem(U_96) )
| ~ equalelemsP(U_101) ) )
| ~ ssList(U_101) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(U_98,sK42(U_101))],[f_14_4]) ).
fof(f_14_6,plain,
! [U_101] :
( ( ( equalelemsP(U_101)
| ( sK40(U_101) != sK41(U_101)
& app(sK42(U_101),cons(sK40(U_101),cons(sK41(U_101),sK43(U_101)))) = U_101
& ssList(sK43(U_101))
& ssList(sK42(U_101))
& ssItem(sK41(U_101))
& ssItem(sK40(U_101)) ) )
& ( ! [U_96] :
( ! [U_95] :
( ! [U_94] :
( ! [U_93] :
( U_96 = U_95
| app(U_94,cons(U_96,cons(U_95,U_93))) != U_101
| ~ ssList(U_93) )
| ~ ssList(U_94) )
| ~ ssItem(U_95) )
| ~ ssItem(U_96) )
| ~ equalelemsP(U_101) ) )
| ~ ssList(U_101) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(U_97,sK43(U_101))],[f_14_5]) ).
fof(f_14_7,plain,
( ! [U_101] :
( sK40(U_101) != sK41(U_101)
| ~ sP23(U_101) )
& ! [U_101] :
( app(sK42(U_101),cons(sK40(U_101),cons(sK41(U_101),sK43(U_101)))) = U_101
| ~ sP23(U_101) )
& ! [U_101] :
( ssList(sK43(U_101))
| ~ sP23(U_101) )
& ! [U_101] :
( ssList(sK42(U_101))
| ~ sP23(U_101) )
& ! [U_101] :
( ssItem(sK41(U_101))
| ~ sP23(U_101) )
& ! [U_101] :
( ssItem(sK40(U_101))
| ~ sP23(U_101) )
& ! [U_96,U_93,U_94,U_101,U_95] :
( equalelemsP(U_101)
| sP23(U_101)
| ~ sP24(U_96,U_93,U_94,U_101,U_95) )
& ! [U_96,U_93,U_94,U_101,U_95] :
( U_96 = U_95
| app(U_94,cons(U_96,cons(U_95,U_93))) != U_101
| ~ ssList(U_93)
| ~ ssList(U_94)
| ~ ssItem(U_95)
| ~ ssItem(U_96)
| ~ equalelemsP(U_101)
| ~ sP24(U_96,U_93,U_94,U_101,U_95) )
& ! [U_96,U_93,U_94,U_101,U_95] :
( sP24(U_96,U_93,U_94,U_101,U_95)
| ~ ssList(U_101) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP23,sP24])],[f_14_6]) ).
cnf(f_14_8,plain,
( sP24(U_96,U_93,U_94,U_101,U_95)
| ~ ssList(U_101) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_9,plain,
( U_96 = U_95
| app(U_94,cons(U_96,cons(U_95,U_93))) != U_101
| ~ ssList(U_93)
| ~ ssList(U_94)
| ~ ssItem(U_95)
| ~ ssItem(U_96)
| ~ equalelemsP(U_101)
| ~ sP24(U_96,U_93,U_94,U_101,U_95) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_10,plain,
( equalelemsP(U_101)
| sP23(U_101)
| ~ sP24(U_96,U_93,U_94,U_101,U_95) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_11,plain,
( ssItem(sK40(U_101))
| ~ sP23(U_101) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_12,plain,
( ssItem(sK41(U_101))
| ~ sP23(U_101) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_13,plain,
( ssList(sK42(U_101))
| ~ sP23(U_101) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_14,plain,
( ssList(sK43(U_101))
| ~ sP23(U_101) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_15,plain,
( app(sK42(U_101),cons(sK40(U_101),cons(sK41(U_101),sK43(U_101)))) = U_101
| ~ sP23(U_101) ),
inference(clausify,[status(thm)],[f_14_7]) ).
cnf(f_14_16,plain,
( sK40(U_101) != sK41(U_101)
| ~ sP23(U_101) ),
inference(clausify,[status(thm)],[f_14_7]) ).
fof(f_15_1,plain,
! [U] :
( ! [V] :
( ( ( neq(U,V)
| U = V )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax15]) ).
fof(f_15_2,plain,
! [U_103] :
( ! [U_102] :
( ( ( neq(U_103,U_102)
| U_103 = U_102 )
& ( U_103 != U_102
| ~ neq(U_103,U_102) ) )
| ~ ssList(U_102) )
| ~ ssList(U_103) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_103,U_102] :
( neq(U_103,U_102)
| U_103 = U_102
| ~ sP25(U_103,U_102) )
& ! [U_103,U_102] :
( U_103 != U_102
| ~ neq(U_103,U_102)
| ~ sP25(U_103,U_102) )
& ! [U_103,U_102] :
( sP25(U_103,U_102)
| ~ ssList(U_102)
| ~ ssList(U_103) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP25])],[f_15_2]) ).
cnf(f_15_4,plain,
( sP25(U_103,U_102)
| ~ ssList(U_102)
| ~ ssList(U_103) ),
inference(clausify,[status(thm)],[f_15_3]) ).
cnf(f_15_5,plain,
( U_103 != U_102
| ~ neq(U_103,U_102)
| ~ sP25(U_103,U_102) ),
inference(clausify,[status(thm)],[f_15_3]) ).
cnf(f_15_6,plain,
( neq(U_103,U_102)
| U_103 = U_102
| ~ sP25(U_103,U_102) ),
inference(clausify,[status(thm)],[f_15_3]) ).
fof(f_16_1,plain,
! [U] :
( ! [V] :
( ssList(cons(V,U))
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax16]) ).
fof(f_16_2,plain,
! [U_105] :
( ! [U_104] :
( ssList(cons(U_104,U_105))
| ~ ssItem(U_104) )
| ~ ssList(U_105) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
! [U_105,U_104] :
( ssList(cons(U_104,U_105))
| ~ ssItem(U_104)
| ~ ssList(U_105) ),
inference(definitional_conversion,[status(esa)],[f_16_2]) ).
cnf(f_16_4,plain,
( ssList(cons(U_104,U_105))
| ~ ssItem(U_104)
| ~ ssList(U_105) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
ssList(nil),
inference(fof_nnf,[status(thm)],[ax17]) ).
fof(f_17_2,plain,
ssList(nil),
inference(definitional_conversion,[status(esa)],[f_17_1]) ).
cnf(f_17_3,plain,
ssList(nil),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [U] :
( ! [V] :
( cons(V,U) != U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax18]) ).
fof(f_18_2,plain,
! [U_107] :
( ! [U_106] :
( cons(U_106,U_107) != U_107
| ~ ssItem(U_106) )
| ~ ssList(U_107) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
! [U_107,U_106] :
( cons(U_106,U_107) != U_107
| ~ ssItem(U_106)
| ~ ssList(U_107) ),
inference(definitional_conversion,[status(esa)],[f_18_2]) ).
cnf(f_18_4,plain,
( cons(U_106,U_107) != U_107
| ~ ssItem(U_106)
| ~ ssList(U_107) ),
inference(clausify,[status(thm)],[f_18_3]) ).
fof(f_19_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( ( V = U
& W = X )
| cons(W,U) != cons(X,V)
| ~ ssItem(X) )
| ~ ssItem(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax19]) ).
fof(f_19_2,plain,
! [U_111] :
( ! [U_110] :
( ! [U_109] :
( ! [U_108] :
( ( U_110 = U_111
& U_109 = U_108 )
| cons(U_109,U_111) != cons(U_108,U_110)
| ~ ssItem(U_108) )
| ~ ssItem(U_109) )
| ~ ssList(U_110) )
| ~ ssList(U_111) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_110,U_111,U_108,U_109] :
( U_110 = U_111
| ~ sP26(U_110,U_111,U_108,U_109) )
& ! [U_110,U_111,U_108,U_109] :
( U_109 = U_108
| ~ sP26(U_110,U_111,U_108,U_109) )
& ! [U_110,U_111,U_108,U_109] :
( sP26(U_110,U_111,U_108,U_109)
| cons(U_109,U_111) != cons(U_108,U_110)
| ~ ssItem(U_108)
| ~ ssItem(U_109)
| ~ ssList(U_110)
| ~ ssList(U_111) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP26])],[f_19_2]) ).
cnf(f_19_4,plain,
( sP26(U_110,U_111,U_108,U_109)
| cons(U_109,U_111) != cons(U_108,U_110)
| ~ ssItem(U_108)
| ~ ssItem(U_109)
| ~ ssList(U_110)
| ~ ssList(U_111) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( U_109 = U_108
| ~ sP26(U_110,U_111,U_108,U_109) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_6,plain,
( U_110 = U_111
| ~ sP26(U_110,U_111,U_108,U_109) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [U] :
( ? [V] :
( ? [W] :
( cons(W,V) = U
& ssItem(W) )
& ssList(V) )
| nil = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax20]) ).
fof(f_20_2,plain,
! [U_114] :
( ? [U_113] :
( ? [U_112] :
( cons(U_112,U_113) = U_114
& ssItem(U_112) )
& ssList(U_113) )
| nil = U_114
| ~ ssList(U_114) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
! [U_114] :
( ( ? [U_112] :
( cons(U_112,sK44(U_114)) = U_114
& ssItem(U_112) )
& ssList(sK44(U_114)) )
| nil = U_114
| ~ ssList(U_114) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(U_113,sK44(U_114))],[f_20_2]) ).
fof(f_20_4,plain,
! [U_114] :
( ( cons(sK45(U_114),sK44(U_114)) = U_114
& ssItem(sK45(U_114))
& ssList(sK44(U_114)) )
| nil = U_114
| ~ ssList(U_114) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(U_112,sK45(U_114))],[f_20_3]) ).
fof(f_20_5,plain,
( ! [U_114] :
( cons(sK45(U_114),sK44(U_114)) = U_114
| ~ sP27(U_114) )
& ! [U_114] :
( ssItem(sK45(U_114))
| ~ sP27(U_114) )
& ! [U_114] :
( ssList(sK44(U_114))
| ~ sP27(U_114) )
& ! [U_114] :
( sP27(U_114)
| nil = U_114
| ~ ssList(U_114) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP27])],[f_20_4]) ).
cnf(f_20_6,plain,
( sP27(U_114)
| nil = U_114
| ~ ssList(U_114) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_7,plain,
( ssList(sK44(U_114))
| ~ sP27(U_114) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_8,plain,
( ssItem(sK45(U_114))
| ~ sP27(U_114) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_9,plain,
( cons(sK45(U_114),sK44(U_114)) = U_114
| ~ sP27(U_114) ),
inference(clausify,[status(thm)],[f_20_5]) ).
fof(f_21_1,plain,
! [U] :
( ! [V] :
( nil != cons(V,U)
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax21]) ).
fof(f_21_2,plain,
! [U_116] :
( ! [U_115] :
( nil != cons(U_115,U_116)
| ~ ssItem(U_115) )
| ~ ssList(U_116) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
! [U_116,U_115] :
( nil != cons(U_115,U_116)
| ~ ssItem(U_115)
| ~ ssList(U_116) ),
inference(definitional_conversion,[status(esa)],[f_21_2]) ).
cnf(f_21_4,plain,
( nil != cons(U_115,U_116)
| ~ ssItem(U_115)
| ~ ssList(U_116) ),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [U] :
( ssItem(hd(U))
| nil = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax22]) ).
fof(f_22_2,plain,
! [U_117] :
( ssItem(hd(U_117))
| nil = U_117
| ~ ssList(U_117) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
! [U_117] :
( ssItem(hd(U_117))
| nil = U_117
| ~ ssList(U_117) ),
inference(definitional_conversion,[status(esa)],[f_22_2]) ).
cnf(f_22_4,plain,
( ssItem(hd(U_117))
| nil = U_117
| ~ ssList(U_117) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
! [U] :
( ! [V] :
( hd(cons(V,U)) = V
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax23]) ).
fof(f_23_2,plain,
! [U_119] :
( ! [U_118] :
( hd(cons(U_118,U_119)) = U_118
| ~ ssItem(U_118) )
| ~ ssList(U_119) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
! [U_118,U_119] :
( hd(cons(U_118,U_119)) = U_118
| ~ ssItem(U_118)
| ~ ssList(U_119) ),
inference(definitional_conversion,[status(esa)],[f_23_2]) ).
cnf(f_23_4,plain,
( hd(cons(U_118,U_119)) = U_118
| ~ ssItem(U_118)
| ~ ssList(U_119) ),
inference(clausify,[status(thm)],[f_23_3]) ).
fof(f_24_1,plain,
! [U] :
( ssList(tl(U))
| nil = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax24]) ).
fof(f_24_2,plain,
! [U_120] :
( ssList(tl(U_120))
| nil = U_120
| ~ ssList(U_120) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
! [U_120] :
( ssList(tl(U_120))
| nil = U_120
| ~ ssList(U_120) ),
inference(definitional_conversion,[status(esa)],[f_24_2]) ).
cnf(f_24_4,plain,
( ssList(tl(U_120))
| nil = U_120
| ~ ssList(U_120) ),
inference(clausify,[status(thm)],[f_24_3]) ).
fof(f_25_1,plain,
! [U] :
( ! [V] :
( tl(cons(V,U)) = U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax25]) ).
fof(f_25_2,plain,
! [U_122] :
( ! [U_121] :
( tl(cons(U_121,U_122)) = U_122
| ~ ssItem(U_121) )
| ~ ssList(U_122) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
! [U_121,U_122] :
( tl(cons(U_121,U_122)) = U_122
| ~ ssItem(U_121)
| ~ ssList(U_122) ),
inference(definitional_conversion,[status(esa)],[f_25_2]) ).
cnf(f_25_4,plain,
( tl(cons(U_121,U_122)) = U_122
| ~ ssItem(U_121)
| ~ ssList(U_122) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [U] :
( ! [V] :
( ssList(app(U,V))
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax26]) ).
fof(f_26_2,plain,
! [U_124] :
( ! [U_123] :
( ssList(app(U_124,U_123))
| ~ ssList(U_123) )
| ~ ssList(U_124) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
! [U_124,U_123] :
( ssList(app(U_124,U_123))
| ~ ssList(U_123)
| ~ ssList(U_124) ),
inference(definitional_conversion,[status(esa)],[f_26_2]) ).
cnf(f_26_4,plain,
( ssList(app(U_124,U_123))
| ~ ssList(U_123)
| ~ ssList(U_124) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( cons(W,app(V,U)) = app(cons(W,V),U)
| ~ ssItem(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax27]) ).
fof(f_27_2,plain,
! [U_127] :
( ! [U_126] :
( ! [U_125] :
( cons(U_125,app(U_126,U_127)) = app(cons(U_125,U_126),U_127)
| ~ ssItem(U_125) )
| ~ ssList(U_126) )
| ~ ssList(U_127) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
! [U_126,U_125,U_127] :
( cons(U_125,app(U_126,U_127)) = app(cons(U_125,U_126),U_127)
| ~ ssItem(U_125)
| ~ ssList(U_126)
| ~ ssList(U_127) ),
inference(definitional_conversion,[status(esa)],[f_27_2]) ).
cnf(f_27_4,plain,
( cons(U_125,app(U_126,U_127)) = app(cons(U_125,U_126),U_127)
| ~ ssItem(U_125)
| ~ ssList(U_126)
| ~ ssList(U_127) ),
inference(clausify,[status(thm)],[f_27_3]) ).
fof(f_28_1,plain,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax28]) ).
fof(f_28_2,plain,
! [U_128] :
( app(nil,U_128) = U_128
| ~ ssList(U_128) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
! [U_128] :
( app(nil,U_128) = U_128
| ~ ssList(U_128) ),
inference(definitional_conversion,[status(esa)],[f_28_2]) ).
cnf(f_28_4,plain,
( app(nil,U_128) = U_128
| ~ ssList(U_128) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [U] :
( ! [V] :
( U = V
| ~ leq(V,U)
| ~ leq(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax29]) ).
fof(f_29_2,plain,
! [U_130] :
( ! [U_129] :
( U_130 = U_129
| ~ leq(U_129,U_130)
| ~ leq(U_130,U_129)
| ~ ssItem(U_129) )
| ~ ssItem(U_130) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
! [U_130,U_129] :
( U_130 = U_129
| ~ leq(U_129,U_130)
| ~ leq(U_130,U_129)
| ~ ssItem(U_129)
| ~ ssItem(U_130) ),
inference(definitional_conversion,[status(esa)],[f_29_2]) ).
cnf(f_29_4,plain,
( U_130 = U_129
| ~ leq(U_129,U_130)
| ~ leq(U_130,U_129)
| ~ ssItem(U_129)
| ~ ssItem(U_130) ),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_30_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( leq(U,W)
| ~ leq(V,W)
| ~ leq(U,V)
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax30]) ).
fof(f_30_2,plain,
! [U_133] :
( ! [U_132] :
( ! [U_131] :
( leq(U_133,U_131)
| ~ leq(U_132,U_131)
| ~ leq(U_133,U_132)
| ~ ssItem(U_131) )
| ~ ssItem(U_132) )
| ~ ssItem(U_133) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
! [U_132,U_133,U_131] :
( leq(U_133,U_131)
| ~ leq(U_132,U_131)
| ~ leq(U_133,U_132)
| ~ ssItem(U_131)
| ~ ssItem(U_132)
| ~ ssItem(U_133) ),
inference(definitional_conversion,[status(esa)],[f_30_2]) ).
cnf(f_30_4,plain,
( leq(U_133,U_131)
| ~ leq(U_132,U_131)
| ~ leq(U_133,U_132)
| ~ ssItem(U_131)
| ~ ssItem(U_132)
| ~ ssItem(U_133) ),
inference(clausify,[status(thm)],[f_30_3]) ).
fof(f_31_1,plain,
! [U] :
( leq(U,U)
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax31]) ).
fof(f_31_2,plain,
! [U_134] :
( leq(U_134,U_134)
| ~ ssItem(U_134) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
! [U_134] :
( leq(U_134,U_134)
| ~ ssItem(U_134) ),
inference(definitional_conversion,[status(esa)],[f_31_2]) ).
cnf(f_31_4,plain,
( leq(U_134,U_134)
| ~ ssItem(U_134) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [U] :
( ! [V] :
( ( ( geq(U,V)
| ~ leq(V,U) )
& ( leq(V,U)
| ~ geq(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax32]) ).
fof(f_32_2,plain,
! [U_136] :
( ! [U_135] :
( ( ( geq(U_136,U_135)
| ~ leq(U_135,U_136) )
& ( leq(U_135,U_136)
| ~ geq(U_136,U_135) ) )
| ~ ssItem(U_135) )
| ~ ssItem(U_136) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
( ! [U_135,U_136] :
( geq(U_136,U_135)
| ~ leq(U_135,U_136)
| ~ sP28(U_135,U_136) )
& ! [U_135,U_136] :
( leq(U_135,U_136)
| ~ geq(U_136,U_135)
| ~ sP28(U_135,U_136) )
& ! [U_135,U_136] :
( sP28(U_135,U_136)
| ~ ssItem(U_135)
| ~ ssItem(U_136) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP28])],[f_32_2]) ).
cnf(f_32_4,plain,
( sP28(U_135,U_136)
| ~ ssItem(U_135)
| ~ ssItem(U_136) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_5,plain,
( leq(U_135,U_136)
| ~ geq(U_136,U_135)
| ~ sP28(U_135,U_136) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_6,plain,
( geq(U_136,U_135)
| ~ leq(U_135,U_136)
| ~ sP28(U_135,U_136) ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [U] :
( ! [V] :
( ~ lt(V,U)
| ~ lt(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax33]) ).
fof(f_33_2,plain,
! [U_138] :
( ! [U_137] :
( ~ lt(U_137,U_138)
| ~ lt(U_138,U_137)
| ~ ssItem(U_137) )
| ~ ssItem(U_138) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
! [U_138,U_137] :
( ~ lt(U_137,U_138)
| ~ lt(U_138,U_137)
| ~ ssItem(U_137)
| ~ ssItem(U_138) ),
inference(definitional_conversion,[status(esa)],[f_33_2]) ).
cnf(f_33_4,plain,
( ~ lt(U_137,U_138)
| ~ lt(U_138,U_137)
| ~ ssItem(U_137)
| ~ ssItem(U_138) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_34_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( lt(U,W)
| ~ lt(V,W)
| ~ lt(U,V)
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax34]) ).
fof(f_34_2,plain,
! [U_141] :
( ! [U_140] :
( ! [U_139] :
( lt(U_141,U_139)
| ~ lt(U_140,U_139)
| ~ lt(U_141,U_140)
| ~ ssItem(U_139) )
| ~ ssItem(U_140) )
| ~ ssItem(U_141) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
! [U_139,U_140,U_141] :
( lt(U_141,U_139)
| ~ lt(U_140,U_139)
| ~ lt(U_141,U_140)
| ~ ssItem(U_139)
| ~ ssItem(U_140)
| ~ ssItem(U_141) ),
inference(definitional_conversion,[status(esa)],[f_34_2]) ).
cnf(f_34_4,plain,
( lt(U_141,U_139)
| ~ lt(U_140,U_139)
| ~ lt(U_141,U_140)
| ~ ssItem(U_139)
| ~ ssItem(U_140)
| ~ ssItem(U_141) ),
inference(clausify,[status(thm)],[f_34_3]) ).
fof(f_35_1,plain,
! [U] :
( ! [V] :
( ( ( gt(U,V)
| ~ lt(V,U) )
& ( lt(V,U)
| ~ gt(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax35]) ).
fof(f_35_2,plain,
! [U_143] :
( ! [U_142] :
( ( ( gt(U_143,U_142)
| ~ lt(U_142,U_143) )
& ( lt(U_142,U_143)
| ~ gt(U_143,U_142) ) )
| ~ ssItem(U_142) )
| ~ ssItem(U_143) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_142,U_143] :
( gt(U_143,U_142)
| ~ lt(U_142,U_143)
| ~ sP29(U_142,U_143) )
& ! [U_142,U_143] :
( lt(U_142,U_143)
| ~ gt(U_143,U_142)
| ~ sP29(U_142,U_143) )
& ! [U_142,U_143] :
( sP29(U_142,U_143)
| ~ ssItem(U_142)
| ~ ssItem(U_143) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP29])],[f_35_2]) ).
cnf(f_35_4,plain,
( sP29(U_142,U_143)
| ~ ssItem(U_142)
| ~ ssItem(U_143) ),
inference(clausify,[status(thm)],[f_35_3]) ).
cnf(f_35_5,plain,
( lt(U_142,U_143)
| ~ gt(U_143,U_142)
| ~ sP29(U_142,U_143) ),
inference(clausify,[status(thm)],[f_35_3]) ).
cnf(f_35_6,plain,
( gt(U_143,U_142)
| ~ lt(U_142,U_143)
| ~ sP29(U_142,U_143) ),
inference(clausify,[status(thm)],[f_35_3]) ).
fof(f_36_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( ( memberP(app(V,W),U)
| ( ~ memberP(W,U)
& ~ memberP(V,U) ) )
& ( memberP(W,U)
| memberP(V,U)
| ~ memberP(app(V,W),U) ) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax36]) ).
fof(f_36_2,plain,
! [U_146] :
( ! [U_145] :
( ! [U_144] :
( ( ( memberP(app(U_145,U_144),U_146)
| ( ~ memberP(U_144,U_146)
& ~ memberP(U_145,U_146) ) )
& ( memberP(U_144,U_146)
| memberP(U_145,U_146)
| ~ memberP(app(U_145,U_144),U_146) ) )
| ~ ssList(U_144) )
| ~ ssList(U_145) )
| ~ ssItem(U_146) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
( ! [U_146,U_145,U_144] :
( ~ memberP(U_144,U_146)
| ~ sP30(U_146,U_145,U_144) )
& ! [U_146,U_145,U_144] :
( ~ memberP(U_145,U_146)
| ~ sP30(U_146,U_145,U_144) )
& ! [U_146,U_145,U_144] :
( memberP(app(U_145,U_144),U_146)
| sP30(U_146,U_145,U_144)
| ~ sP31(U_146,U_145,U_144) )
& ! [U_146,U_145,U_144] :
( memberP(U_144,U_146)
| memberP(U_145,U_146)
| ~ memberP(app(U_145,U_144),U_146)
| ~ sP31(U_146,U_145,U_144) )
& ! [U_146,U_145,U_144] :
( sP31(U_146,U_145,U_144)
| ~ ssList(U_144)
| ~ ssList(U_145)
| ~ ssItem(U_146) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP30,sP31])],[f_36_2]) ).
cnf(f_36_4,plain,
( sP31(U_146,U_145,U_144)
| ~ ssList(U_144)
| ~ ssList(U_145)
| ~ ssItem(U_146) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_5,plain,
( memberP(U_144,U_146)
| memberP(U_145,U_146)
| ~ memberP(app(U_145,U_144),U_146)
| ~ sP31(U_146,U_145,U_144) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_6,plain,
( memberP(app(U_145,U_144),U_146)
| sP30(U_146,U_145,U_144)
| ~ sP31(U_146,U_145,U_144) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_7,plain,
( ~ memberP(U_145,U_146)
| ~ sP30(U_146,U_145,U_144) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_8,plain,
( ~ memberP(U_144,U_146)
| ~ sP30(U_146,U_145,U_144) ),
inference(clausify,[status(thm)],[f_36_3]) ).
fof(f_37_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( ( memberP(cons(V,W),U)
| ( ~ memberP(W,U)
& U != V ) )
& ( memberP(W,U)
| U = V
| ~ memberP(cons(V,W),U) ) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax37]) ).
fof(f_37_2,plain,
! [U_149] :
( ! [U_148] :
( ! [U_147] :
( ( ( memberP(cons(U_148,U_147),U_149)
| ( ~ memberP(U_147,U_149)
& U_149 != U_148 ) )
& ( memberP(U_147,U_149)
| U_149 = U_148
| ~ memberP(cons(U_148,U_147),U_149) ) )
| ~ ssList(U_147) )
| ~ ssItem(U_148) )
| ~ ssItem(U_149) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_149,U_147,U_148] :
( ~ memberP(U_147,U_149)
| ~ sP32(U_149,U_147,U_148) )
& ! [U_149,U_147,U_148] :
( U_149 != U_148
| ~ sP32(U_149,U_147,U_148) )
& ! [U_149,U_147,U_148] :
( memberP(cons(U_148,U_147),U_149)
| sP32(U_149,U_147,U_148)
| ~ sP33(U_149,U_147,U_148) )
& ! [U_149,U_147,U_148] :
( memberP(U_147,U_149)
| U_149 = U_148
| ~ memberP(cons(U_148,U_147),U_149)
| ~ sP33(U_149,U_147,U_148) )
& ! [U_149,U_147,U_148] :
( sP33(U_149,U_147,U_148)
| ~ ssList(U_147)
| ~ ssItem(U_148)
| ~ ssItem(U_149) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP32,sP33])],[f_37_2]) ).
cnf(f_37_4,plain,
( sP33(U_149,U_147,U_148)
| ~ ssList(U_147)
| ~ ssItem(U_148)
| ~ ssItem(U_149) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_5,plain,
( memberP(U_147,U_149)
| U_149 = U_148
| ~ memberP(cons(U_148,U_147),U_149)
| ~ sP33(U_149,U_147,U_148) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_6,plain,
( memberP(cons(U_148,U_147),U_149)
| sP32(U_149,U_147,U_148)
| ~ sP33(U_149,U_147,U_148) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_7,plain,
( U_149 != U_148
| ~ sP32(U_149,U_147,U_148) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_8,plain,
( ~ memberP(U_147,U_149)
| ~ sP32(U_149,U_147,U_148) ),
inference(clausify,[status(thm)],[f_37_3]) ).
fof(f_38_1,plain,
! [U] :
( ~ memberP(nil,U)
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax38]) ).
fof(f_38_2,plain,
! [U_150] :
( ~ memberP(nil,U_150)
| ~ ssItem(U_150) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
! [U_150] :
( ~ memberP(nil,U_150)
| ~ ssItem(U_150) ),
inference(definitional_conversion,[status(esa)],[f_38_2]) ).
cnf(f_38_4,plain,
( ~ memberP(nil,U_150)
| ~ ssItem(U_150) ),
inference(clausify,[status(thm)],[f_38_3]) ).
fof(f_39_1,plain,
~ singletonP(nil),
inference(fof_nnf,[status(thm)],[ax39]) ).
fof(f_39_2,plain,
~ singletonP(nil),
inference(definitional_conversion,[status(esa)],[f_39_1]) ).
cnf(f_39_3,plain,
~ singletonP(nil),
inference(clausify,[status(thm)],[f_39_2]) ).
fof(f_40_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( frontsegP(U,W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax40]) ).
fof(f_40_2,plain,
! [U_153] :
( ! [U_152] :
( ! [U_151] :
( frontsegP(U_153,U_151)
| ~ frontsegP(U_152,U_151)
| ~ frontsegP(U_153,U_152)
| ~ ssList(U_151) )
| ~ ssList(U_152) )
| ~ ssList(U_153) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
! [U_151,U_153,U_152] :
( frontsegP(U_153,U_151)
| ~ frontsegP(U_152,U_151)
| ~ frontsegP(U_153,U_152)
| ~ ssList(U_151)
| ~ ssList(U_152)
| ~ ssList(U_153) ),
inference(definitional_conversion,[status(esa)],[f_40_2]) ).
cnf(f_40_4,plain,
( frontsegP(U_153,U_151)
| ~ frontsegP(U_152,U_151)
| ~ frontsegP(U_153,U_152)
| ~ ssList(U_151)
| ~ ssList(U_152)
| ~ ssList(U_153) ),
inference(clausify,[status(thm)],[f_40_3]) ).
fof(f_41_1,plain,
! [U] :
( ! [V] :
( U = V
| ~ frontsegP(V,U)
| ~ frontsegP(U,V)
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax41]) ).
fof(f_41_2,plain,
! [U_155] :
( ! [U_154] :
( U_155 = U_154
| ~ frontsegP(U_154,U_155)
| ~ frontsegP(U_155,U_154)
| ~ ssList(U_154) )
| ~ ssList(U_155) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
! [U_154,U_155] :
( U_155 = U_154
| ~ frontsegP(U_154,U_155)
| ~ frontsegP(U_155,U_154)
| ~ ssList(U_154)
| ~ ssList(U_155) ),
inference(definitional_conversion,[status(esa)],[f_41_2]) ).
cnf(f_41_4,plain,
( U_155 = U_154
| ~ frontsegP(U_154,U_155)
| ~ frontsegP(U_155,U_154)
| ~ ssList(U_154)
| ~ ssList(U_155) ),
inference(clausify,[status(thm)],[f_41_3]) ).
fof(f_42_1,plain,
! [U] :
( frontsegP(U,U)
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax42]) ).
fof(f_42_2,plain,
! [U_156] :
( frontsegP(U_156,U_156)
| ~ ssList(U_156) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
! [U_156] :
( frontsegP(U_156,U_156)
| ~ ssList(U_156) ),
inference(definitional_conversion,[status(esa)],[f_42_2]) ).
cnf(f_42_4,plain,
( frontsegP(U_156,U_156)
| ~ ssList(U_156) ),
inference(clausify,[status(thm)],[f_42_3]) ).
fof(f_43_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( frontsegP(app(U,W),V)
| ~ frontsegP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax43]) ).
fof(f_43_2,plain,
! [U_159] :
( ! [U_158] :
( ! [U_157] :
( frontsegP(app(U_159,U_157),U_158)
| ~ frontsegP(U_159,U_158)
| ~ ssList(U_157) )
| ~ ssList(U_158) )
| ~ ssList(U_159) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
fof(f_43_3,plain,
! [U_158,U_159,U_157] :
( frontsegP(app(U_159,U_157),U_158)
| ~ frontsegP(U_159,U_158)
| ~ ssList(U_157)
| ~ ssList(U_158)
| ~ ssList(U_159) ),
inference(definitional_conversion,[status(esa)],[f_43_2]) ).
cnf(f_43_4,plain,
( frontsegP(app(U_159,U_157),U_158)
| ~ frontsegP(U_159,U_158)
| ~ ssList(U_157)
| ~ ssList(U_158)
| ~ ssList(U_159) ),
inference(clausify,[status(thm)],[f_43_3]) ).
fof(f_44_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( ( ( frontsegP(cons(U,W),cons(V,X))
| ~ frontsegP(W,X)
| U != V )
& ( ( frontsegP(W,X)
& U = V )
| ~ frontsegP(cons(U,W),cons(V,X)) ) )
| ~ ssList(X) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax44]) ).
fof(f_44_2,plain,
! [U_163] :
( ! [U_162] :
( ! [U_161] :
( ! [U_160] :
( ( ( frontsegP(cons(U_163,U_161),cons(U_162,U_160))
| ~ frontsegP(U_161,U_160)
| U_163 != U_162 )
& ( ( frontsegP(U_161,U_160)
& U_163 = U_162 )
| ~ frontsegP(cons(U_163,U_161),cons(U_162,U_160)) ) )
| ~ ssList(U_160) )
| ~ ssList(U_161) )
| ~ ssItem(U_162) )
| ~ ssItem(U_163) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_163,U_160,U_161,U_162] :
( frontsegP(U_161,U_160)
| ~ sP34(U_163,U_160,U_161,U_162) )
& ! [U_163,U_160,U_161,U_162] :
( U_163 = U_162
| ~ sP34(U_163,U_160,U_161,U_162) )
& ! [U_163,U_160,U_161,U_162] :
( frontsegP(cons(U_163,U_161),cons(U_162,U_160))
| ~ frontsegP(U_161,U_160)
| U_163 != U_162
| ~ sP35(U_163,U_160,U_161,U_162) )
& ! [U_163,U_160,U_161,U_162] :
( sP34(U_163,U_160,U_161,U_162)
| ~ frontsegP(cons(U_163,U_161),cons(U_162,U_160))
| ~ sP35(U_163,U_160,U_161,U_162) )
& ! [U_163,U_160,U_161,U_162] :
( sP35(U_163,U_160,U_161,U_162)
| ~ ssList(U_160)
| ~ ssList(U_161)
| ~ ssItem(U_162)
| ~ ssItem(U_163) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP34,sP35])],[f_44_2]) ).
cnf(f_44_4,plain,
( sP35(U_163,U_160,U_161,U_162)
| ~ ssList(U_160)
| ~ ssList(U_161)
| ~ ssItem(U_162)
| ~ ssItem(U_163) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_5,plain,
( sP34(U_163,U_160,U_161,U_162)
| ~ frontsegP(cons(U_163,U_161),cons(U_162,U_160))
| ~ sP35(U_163,U_160,U_161,U_162) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_6,plain,
( frontsegP(cons(U_163,U_161),cons(U_162,U_160))
| ~ frontsegP(U_161,U_160)
| U_163 != U_162
| ~ sP35(U_163,U_160,U_161,U_162) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_7,plain,
( U_163 = U_162
| ~ sP34(U_163,U_160,U_161,U_162) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_8,plain,
( frontsegP(U_161,U_160)
| ~ sP34(U_163,U_160,U_161,U_162) ),
inference(clausify,[status(thm)],[f_44_3]) ).
fof(f_45_1,plain,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax45]) ).
fof(f_45_2,plain,
! [U_164] :
( frontsegP(U_164,nil)
| ~ ssList(U_164) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
! [U_164] :
( frontsegP(U_164,nil)
| ~ ssList(U_164) ),
inference(definitional_conversion,[status(esa)],[f_45_2]) ).
cnf(f_45_4,plain,
( frontsegP(U_164,nil)
| ~ ssList(U_164) ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [U] :
( ( ( frontsegP(nil,U)
| nil != U )
& ( nil = U
| ~ frontsegP(nil,U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax46]) ).
fof(f_46_2,plain,
! [U_165] :
( ( ( frontsegP(nil,U_165)
| nil != U_165 )
& ( nil = U_165
| ~ frontsegP(nil,U_165) ) )
| ~ ssList(U_165) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
( ! [U_165] :
( frontsegP(nil,U_165)
| nil != U_165
| ~ sP36(U_165) )
& ! [U_165] :
( nil = U_165
| ~ frontsegP(nil,U_165)
| ~ sP36(U_165) )
& ! [U_165] :
( sP36(U_165)
| ~ ssList(U_165) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP36])],[f_46_2]) ).
cnf(f_46_4,plain,
( sP36(U_165)
| ~ ssList(U_165) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_5,plain,
( nil = U_165
| ~ frontsegP(nil,U_165)
| ~ sP36(U_165) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_6,plain,
( frontsegP(nil,U_165)
| nil != U_165
| ~ sP36(U_165) ),
inference(clausify,[status(thm)],[f_46_3]) ).
fof(f_47_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( rearsegP(U,W)
| ~ rearsegP(V,W)
| ~ rearsegP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax47]) ).
fof(f_47_2,plain,
! [U_168] :
( ! [U_167] :
( ! [U_166] :
( rearsegP(U_168,U_166)
| ~ rearsegP(U_167,U_166)
| ~ rearsegP(U_168,U_167)
| ~ ssList(U_166) )
| ~ ssList(U_167) )
| ~ ssList(U_168) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
! [U_166,U_167,U_168] :
( rearsegP(U_168,U_166)
| ~ rearsegP(U_167,U_166)
| ~ rearsegP(U_168,U_167)
| ~ ssList(U_166)
| ~ ssList(U_167)
| ~ ssList(U_168) ),
inference(definitional_conversion,[status(esa)],[f_47_2]) ).
cnf(f_47_4,plain,
( rearsegP(U_168,U_166)
| ~ rearsegP(U_167,U_166)
| ~ rearsegP(U_168,U_167)
| ~ ssList(U_166)
| ~ ssList(U_167)
| ~ ssList(U_168) ),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,plain,
! [U] :
( ! [V] :
( U = V
| ~ rearsegP(V,U)
| ~ rearsegP(U,V)
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax48]) ).
fof(f_48_2,plain,
! [U_170] :
( ! [U_169] :
( U_170 = U_169
| ~ rearsegP(U_169,U_170)
| ~ rearsegP(U_170,U_169)
| ~ ssList(U_169) )
| ~ ssList(U_170) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
! [U_170,U_169] :
( U_170 = U_169
| ~ rearsegP(U_169,U_170)
| ~ rearsegP(U_170,U_169)
| ~ ssList(U_169)
| ~ ssList(U_170) ),
inference(definitional_conversion,[status(esa)],[f_48_2]) ).
cnf(f_48_4,plain,
( U_170 = U_169
| ~ rearsegP(U_169,U_170)
| ~ rearsegP(U_170,U_169)
| ~ ssList(U_169)
| ~ ssList(U_170) ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
! [U] :
( rearsegP(U,U)
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax49]) ).
fof(f_49_2,plain,
! [U_171] :
( rearsegP(U_171,U_171)
| ~ ssList(U_171) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
! [U_171] :
( rearsegP(U_171,U_171)
| ~ ssList(U_171) ),
inference(definitional_conversion,[status(esa)],[f_49_2]) ).
cnf(f_49_4,plain,
( rearsegP(U_171,U_171)
| ~ ssList(U_171) ),
inference(clausify,[status(thm)],[f_49_3]) ).
fof(f_50_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( rearsegP(app(W,U),V)
| ~ rearsegP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax50]) ).
fof(f_50_2,plain,
! [U_174] :
( ! [U_173] :
( ! [U_172] :
( rearsegP(app(U_172,U_174),U_173)
| ~ rearsegP(U_174,U_173)
| ~ ssList(U_172) )
| ~ ssList(U_173) )
| ~ ssList(U_174) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
! [U_172,U_173,U_174] :
( rearsegP(app(U_172,U_174),U_173)
| ~ rearsegP(U_174,U_173)
| ~ ssList(U_172)
| ~ ssList(U_173)
| ~ ssList(U_174) ),
inference(definitional_conversion,[status(esa)],[f_50_2]) ).
cnf(f_50_4,plain,
( rearsegP(app(U_172,U_174),U_173)
| ~ rearsegP(U_174,U_173)
| ~ ssList(U_172)
| ~ ssList(U_173)
| ~ ssList(U_174) ),
inference(clausify,[status(thm)],[f_50_3]) ).
fof(f_51_1,plain,
! [U] :
( rearsegP(U,nil)
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax51]) ).
fof(f_51_2,plain,
! [U_175] :
( rearsegP(U_175,nil)
| ~ ssList(U_175) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
! [U_175] :
( rearsegP(U_175,nil)
| ~ ssList(U_175) ),
inference(definitional_conversion,[status(esa)],[f_51_2]) ).
cnf(f_51_4,plain,
( rearsegP(U_175,nil)
| ~ ssList(U_175) ),
inference(clausify,[status(thm)],[f_51_3]) ).
fof(f_52_1,plain,
! [U] :
( ( ( rearsegP(nil,U)
| nil != U )
& ( nil = U
| ~ rearsegP(nil,U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax52]) ).
fof(f_52_2,plain,
! [U_176] :
( ( ( rearsegP(nil,U_176)
| nil != U_176 )
& ( nil = U_176
| ~ rearsegP(nil,U_176) ) )
| ~ ssList(U_176) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
( ! [U_176] :
( rearsegP(nil,U_176)
| nil != U_176
| ~ sP37(U_176) )
& ! [U_176] :
( nil = U_176
| ~ rearsegP(nil,U_176)
| ~ sP37(U_176) )
& ! [U_176] :
( sP37(U_176)
| ~ ssList(U_176) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP37])],[f_52_2]) ).
cnf(f_52_4,plain,
( sP37(U_176)
| ~ ssList(U_176) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_5,plain,
( nil = U_176
| ~ rearsegP(nil,U_176)
| ~ sP37(U_176) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_6,plain,
( rearsegP(nil,U_176)
| nil != U_176
| ~ sP37(U_176) ),
inference(clausify,[status(thm)],[f_52_3]) ).
fof(f_53_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( segmentP(U,W)
| ~ segmentP(V,W)
| ~ segmentP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax53]) ).
fof(f_53_2,plain,
! [U_179] :
( ! [U_178] :
( ! [U_177] :
( segmentP(U_179,U_177)
| ~ segmentP(U_178,U_177)
| ~ segmentP(U_179,U_178)
| ~ ssList(U_177) )
| ~ ssList(U_178) )
| ~ ssList(U_179) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
! [U_178,U_179,U_177] :
( segmentP(U_179,U_177)
| ~ segmentP(U_178,U_177)
| ~ segmentP(U_179,U_178)
| ~ ssList(U_177)
| ~ ssList(U_178)
| ~ ssList(U_179) ),
inference(definitional_conversion,[status(esa)],[f_53_2]) ).
cnf(f_53_4,plain,
( segmentP(U_179,U_177)
| ~ segmentP(U_178,U_177)
| ~ segmentP(U_179,U_178)
| ~ ssList(U_177)
| ~ ssList(U_178)
| ~ ssList(U_179) ),
inference(clausify,[status(thm)],[f_53_3]) ).
fof(f_54_1,plain,
! [U] :
( ! [V] :
( U = V
| ~ segmentP(V,U)
| ~ segmentP(U,V)
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax54]) ).
fof(f_54_2,plain,
! [U_181] :
( ! [U_180] :
( U_181 = U_180
| ~ segmentP(U_180,U_181)
| ~ segmentP(U_181,U_180)
| ~ ssList(U_180) )
| ~ ssList(U_181) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
! [U_180,U_181] :
( U_181 = U_180
| ~ segmentP(U_180,U_181)
| ~ segmentP(U_181,U_180)
| ~ ssList(U_180)
| ~ ssList(U_181) ),
inference(definitional_conversion,[status(esa)],[f_54_2]) ).
cnf(f_54_4,plain,
( U_181 = U_180
| ~ segmentP(U_180,U_181)
| ~ segmentP(U_181,U_180)
| ~ ssList(U_180)
| ~ ssList(U_181) ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_1,plain,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax55]) ).
fof(f_55_2,plain,
! [U_182] :
( segmentP(U_182,U_182)
| ~ ssList(U_182) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
! [U_182] :
( segmentP(U_182,U_182)
| ~ ssList(U_182) ),
inference(definitional_conversion,[status(esa)],[f_55_2]) ).
cnf(f_55_4,plain,
( segmentP(U_182,U_182)
| ~ ssList(U_182) ),
inference(clausify,[status(thm)],[f_55_3]) ).
fof(f_56_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( segmentP(app(app(W,U),X),V)
| ~ segmentP(U,V)
| ~ ssList(X) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax56]) ).
fof(f_56_2,plain,
! [U_186] :
( ! [U_185] :
( ! [U_184] :
( ! [U_183] :
( segmentP(app(app(U_184,U_186),U_183),U_185)
| ~ segmentP(U_186,U_185)
| ~ ssList(U_183) )
| ~ ssList(U_184) )
| ~ ssList(U_185) )
| ~ ssList(U_186) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
! [U_184,U_185,U_183,U_186] :
( segmentP(app(app(U_184,U_186),U_183),U_185)
| ~ segmentP(U_186,U_185)
| ~ ssList(U_183)
| ~ ssList(U_184)
| ~ ssList(U_185)
| ~ ssList(U_186) ),
inference(definitional_conversion,[status(esa)],[f_56_2]) ).
cnf(f_56_4,plain,
( segmentP(app(app(U_184,U_186),U_183),U_185)
| ~ segmentP(U_186,U_185)
| ~ ssList(U_183)
| ~ ssList(U_184)
| ~ ssList(U_185)
| ~ ssList(U_186) ),
inference(clausify,[status(thm)],[f_56_3]) ).
fof(f_57_1,plain,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax57]) ).
fof(f_57_2,plain,
! [U_187] :
( segmentP(U_187,nil)
| ~ ssList(U_187) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
! [U_187] :
( segmentP(U_187,nil)
| ~ ssList(U_187) ),
inference(definitional_conversion,[status(esa)],[f_57_2]) ).
cnf(f_57_4,plain,
( segmentP(U_187,nil)
| ~ ssList(U_187) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [U] :
( ( ( segmentP(nil,U)
| nil != U )
& ( nil = U
| ~ segmentP(nil,U) ) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax58]) ).
fof(f_58_2,plain,
! [U_188] :
( ( ( segmentP(nil,U_188)
| nil != U_188 )
& ( nil = U_188
| ~ segmentP(nil,U_188) ) )
| ~ ssList(U_188) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_188] :
( segmentP(nil,U_188)
| nil != U_188
| ~ sP38(U_188) )
& ! [U_188] :
( nil = U_188
| ~ segmentP(nil,U_188)
| ~ sP38(U_188) )
& ! [U_188] :
( sP38(U_188)
| ~ ssList(U_188) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP38])],[f_58_2]) ).
cnf(f_58_4,plain,
( sP38(U_188)
| ~ ssList(U_188) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_5,plain,
( nil = U_188
| ~ segmentP(nil,U_188)
| ~ sP38(U_188) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_6,plain,
( segmentP(nil,U_188)
| nil != U_188
| ~ sP38(U_188) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_59_1,plain,
! [U] :
( cyclefreeP(cons(U,nil))
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax59]) ).
fof(f_59_2,plain,
! [U_189] :
( cyclefreeP(cons(U_189,nil))
| ~ ssItem(U_189) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
! [U_189] :
( cyclefreeP(cons(U_189,nil))
| ~ ssItem(U_189) ),
inference(definitional_conversion,[status(esa)],[f_59_2]) ).
cnf(f_59_4,plain,
( cyclefreeP(cons(U_189,nil))
| ~ ssItem(U_189) ),
inference(clausify,[status(thm)],[f_59_3]) ).
fof(f_60_1,plain,
cyclefreeP(nil),
inference(fof_nnf,[status(thm)],[ax60]) ).
fof(f_60_2,plain,
cyclefreeP(nil),
inference(definitional_conversion,[status(esa)],[f_60_1]) ).
cnf(f_60_3,plain,
cyclefreeP(nil),
inference(clausify,[status(thm)],[f_60_2]) ).
fof(f_61_1,plain,
! [U] :
( totalorderP(cons(U,nil))
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax61]) ).
fof(f_61_2,plain,
! [U_190] :
( totalorderP(cons(U_190,nil))
| ~ ssItem(U_190) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
fof(f_61_3,plain,
! [U_190] :
( totalorderP(cons(U_190,nil))
| ~ ssItem(U_190) ),
inference(definitional_conversion,[status(esa)],[f_61_2]) ).
cnf(f_61_4,plain,
( totalorderP(cons(U_190,nil))
| ~ ssItem(U_190) ),
inference(clausify,[status(thm)],[f_61_3]) ).
fof(f_62_1,plain,
totalorderP(nil),
inference(fof_nnf,[status(thm)],[ax62]) ).
fof(f_62_2,plain,
totalorderP(nil),
inference(definitional_conversion,[status(esa)],[f_62_1]) ).
cnf(f_62_3,plain,
totalorderP(nil),
inference(clausify,[status(thm)],[f_62_2]) ).
fof(f_63_1,plain,
! [U] :
( strictorderP(cons(U,nil))
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax63]) ).
fof(f_63_2,plain,
! [U_191] :
( strictorderP(cons(U_191,nil))
| ~ ssItem(U_191) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
fof(f_63_3,plain,
! [U_191] :
( strictorderP(cons(U_191,nil))
| ~ ssItem(U_191) ),
inference(definitional_conversion,[status(esa)],[f_63_2]) ).
cnf(f_63_4,plain,
( strictorderP(cons(U_191,nil))
| ~ ssItem(U_191) ),
inference(clausify,[status(thm)],[f_63_3]) ).
fof(f_64_1,plain,
strictorderP(nil),
inference(fof_nnf,[status(thm)],[ax64]) ).
fof(f_64_2,plain,
strictorderP(nil),
inference(definitional_conversion,[status(esa)],[f_64_1]) ).
cnf(f_64_3,plain,
strictorderP(nil),
inference(clausify,[status(thm)],[f_64_2]) ).
fof(f_65_1,plain,
! [U] :
( totalorderedP(cons(U,nil))
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax65]) ).
fof(f_65_2,plain,
! [U_192] :
( totalorderedP(cons(U_192,nil))
| ~ ssItem(U_192) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
fof(f_65_3,plain,
! [U_192] :
( totalorderedP(cons(U_192,nil))
| ~ ssItem(U_192) ),
inference(definitional_conversion,[status(esa)],[f_65_2]) ).
cnf(f_65_4,plain,
( totalorderedP(cons(U_192,nil))
| ~ ssItem(U_192) ),
inference(clausify,[status(thm)],[f_65_3]) ).
fof(f_66_1,plain,
totalorderedP(nil),
inference(fof_nnf,[status(thm)],[ax66]) ).
fof(f_66_2,plain,
totalorderedP(nil),
inference(definitional_conversion,[status(esa)],[f_66_1]) ).
cnf(f_66_3,plain,
totalorderedP(nil),
inference(clausify,[status(thm)],[f_66_2]) ).
fof(f_67_1,plain,
! [U] :
( ! [V] :
( ( ( totalorderedP(cons(U,V))
| ( ( ~ leq(U,hd(V))
| ~ totalorderedP(V)
| nil = V )
& nil != V ) )
& ( ( leq(U,hd(V))
& totalorderedP(V)
& nil != V )
| nil = V
| ~ totalorderedP(cons(U,V)) ) )
| ~ ssList(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax67]) ).
fof(f_67_2,plain,
! [U_194] :
( ! [U_193] :
( ( ( totalorderedP(cons(U_194,U_193))
| ( ( ~ leq(U_194,hd(U_193))
| ~ totalorderedP(U_193)
| nil = U_193 )
& nil != U_193 ) )
& ( ( leq(U_194,hd(U_193))
& totalorderedP(U_193)
& nil != U_193 )
| nil = U_193
| ~ totalorderedP(cons(U_194,U_193)) ) )
| ~ ssList(U_193) )
| ~ ssItem(U_194) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_194,U_193] :
( ~ leq(U_194,hd(U_193))
| ~ totalorderedP(U_193)
| nil = U_193
| ~ sP40(U_194,U_193) )
& ! [U_194,U_193] :
( nil != U_193
| ~ sP40(U_194,U_193) )
& ! [U_194,U_193] :
( leq(U_194,hd(U_193))
| ~ sP39(U_194,U_193) )
& ! [U_194,U_193] :
( totalorderedP(U_193)
| ~ sP39(U_194,U_193) )
& ! [U_194,U_193] :
( nil != U_193
| ~ sP39(U_194,U_193) )
& ! [U_194,U_193] :
( totalorderedP(cons(U_194,U_193))
| sP40(U_194,U_193)
| ~ sP41(U_194,U_193) )
& ! [U_194,U_193] :
( sP39(U_194,U_193)
| nil = U_193
| ~ totalorderedP(cons(U_194,U_193))
| ~ sP41(U_194,U_193) )
& ! [U_194,U_193] :
( sP41(U_194,U_193)
| ~ ssList(U_193)
| ~ ssItem(U_194) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP39,sP40,sP41])],[f_67_2]) ).
cnf(f_67_4,plain,
( sP41(U_194,U_193)
| ~ ssList(U_193)
| ~ ssItem(U_194) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_5,plain,
( sP39(U_194,U_193)
| nil = U_193
| ~ totalorderedP(cons(U_194,U_193))
| ~ sP41(U_194,U_193) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_6,plain,
( totalorderedP(cons(U_194,U_193))
| sP40(U_194,U_193)
| ~ sP41(U_194,U_193) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_7,plain,
( nil != U_193
| ~ sP39(U_194,U_193) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_8,plain,
( totalorderedP(U_193)
| ~ sP39(U_194,U_193) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_9,plain,
( leq(U_194,hd(U_193))
| ~ sP39(U_194,U_193) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_10,plain,
( nil != U_193
| ~ sP40(U_194,U_193) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_11,plain,
( ~ leq(U_194,hd(U_193))
| ~ totalorderedP(U_193)
| nil = U_193
| ~ sP40(U_194,U_193) ),
inference(clausify,[status(thm)],[f_67_3]) ).
fof(f_68_1,plain,
! [U] :
( strictorderedP(cons(U,nil))
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax68]) ).
fof(f_68_2,plain,
! [U_195] :
( strictorderedP(cons(U_195,nil))
| ~ ssItem(U_195) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
! [U_195] :
( strictorderedP(cons(U_195,nil))
| ~ ssItem(U_195) ),
inference(definitional_conversion,[status(esa)],[f_68_2]) ).
cnf(f_68_4,plain,
( strictorderedP(cons(U_195,nil))
| ~ ssItem(U_195) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_1,plain,
strictorderedP(nil),
inference(fof_nnf,[status(thm)],[ax69]) ).
fof(f_69_2,plain,
strictorderedP(nil),
inference(definitional_conversion,[status(esa)],[f_69_1]) ).
cnf(f_69_3,plain,
strictorderedP(nil),
inference(clausify,[status(thm)],[f_69_2]) ).
fof(f_70_1,plain,
! [U] :
( ! [V] :
( ( ( strictorderedP(cons(U,V))
| ( ( ~ lt(U,hd(V))
| ~ strictorderedP(V)
| nil = V )
& nil != V ) )
& ( ( lt(U,hd(V))
& strictorderedP(V)
& nil != V )
| nil = V
| ~ strictorderedP(cons(U,V)) ) )
| ~ ssList(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax70]) ).
fof(f_70_2,plain,
! [U_197] :
( ! [U_196] :
( ( ( strictorderedP(cons(U_197,U_196))
| ( ( ~ lt(U_197,hd(U_196))
| ~ strictorderedP(U_196)
| nil = U_196 )
& nil != U_196 ) )
& ( ( lt(U_197,hd(U_196))
& strictorderedP(U_196)
& nil != U_196 )
| nil = U_196
| ~ strictorderedP(cons(U_197,U_196)) ) )
| ~ ssList(U_196) )
| ~ ssItem(U_197) ),
inference(variable_rename,[status(thm)],[f_70_1]) ).
fof(f_70_3,plain,
( ! [U_196,U_197] :
( ~ lt(U_197,hd(U_196))
| ~ strictorderedP(U_196)
| nil = U_196
| ~ sP43(U_196,U_197) )
& ! [U_196,U_197] :
( nil != U_196
| ~ sP43(U_196,U_197) )
& ! [U_196,U_197] :
( lt(U_197,hd(U_196))
| ~ sP42(U_196,U_197) )
& ! [U_196,U_197] :
( strictorderedP(U_196)
| ~ sP42(U_196,U_197) )
& ! [U_196,U_197] :
( nil != U_196
| ~ sP42(U_196,U_197) )
& ! [U_196,U_197] :
( strictorderedP(cons(U_197,U_196))
| sP43(U_196,U_197)
| ~ sP44(U_196,U_197) )
& ! [U_196,U_197] :
( sP42(U_196,U_197)
| nil = U_196
| ~ strictorderedP(cons(U_197,U_196))
| ~ sP44(U_196,U_197) )
& ! [U_196,U_197] :
( sP44(U_196,U_197)
| ~ ssList(U_196)
| ~ ssItem(U_197) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP42,sP43,sP44])],[f_70_2]) ).
cnf(f_70_4,plain,
( sP44(U_196,U_197)
| ~ ssList(U_196)
| ~ ssItem(U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_5,plain,
( sP42(U_196,U_197)
| nil = U_196
| ~ strictorderedP(cons(U_197,U_196))
| ~ sP44(U_196,U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_6,plain,
( strictorderedP(cons(U_197,U_196))
| sP43(U_196,U_197)
| ~ sP44(U_196,U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_7,plain,
( nil != U_196
| ~ sP42(U_196,U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_8,plain,
( strictorderedP(U_196)
| ~ sP42(U_196,U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_9,plain,
( lt(U_197,hd(U_196))
| ~ sP42(U_196,U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_10,plain,
( nil != U_196
| ~ sP43(U_196,U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_11,plain,
( ~ lt(U_197,hd(U_196))
| ~ strictorderedP(U_196)
| nil = U_196
| ~ sP43(U_196,U_197) ),
inference(clausify,[status(thm)],[f_70_3]) ).
fof(f_71_1,plain,
! [U] :
( duplicatefreeP(cons(U,nil))
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax71]) ).
fof(f_71_2,plain,
! [U_198] :
( duplicatefreeP(cons(U_198,nil))
| ~ ssItem(U_198) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
fof(f_71_3,plain,
! [U_198] :
( duplicatefreeP(cons(U_198,nil))
| ~ ssItem(U_198) ),
inference(definitional_conversion,[status(esa)],[f_71_2]) ).
cnf(f_71_4,plain,
( duplicatefreeP(cons(U_198,nil))
| ~ ssItem(U_198) ),
inference(clausify,[status(thm)],[f_71_3]) ).
fof(f_72_1,plain,
duplicatefreeP(nil),
inference(fof_nnf,[status(thm)],[ax72]) ).
fof(f_72_2,plain,
duplicatefreeP(nil),
inference(definitional_conversion,[status(esa)],[f_72_1]) ).
cnf(f_72_3,plain,
duplicatefreeP(nil),
inference(clausify,[status(thm)],[f_72_2]) ).
fof(f_73_1,plain,
! [U] :
( equalelemsP(cons(U,nil))
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax73]) ).
fof(f_73_2,plain,
! [U_199] :
( equalelemsP(cons(U_199,nil))
| ~ ssItem(U_199) ),
inference(variable_rename,[status(thm)],[f_73_1]) ).
fof(f_73_3,plain,
! [U_199] :
( equalelemsP(cons(U_199,nil))
| ~ ssItem(U_199) ),
inference(definitional_conversion,[status(esa)],[f_73_2]) ).
cnf(f_73_4,plain,
( equalelemsP(cons(U_199,nil))
| ~ ssItem(U_199) ),
inference(clausify,[status(thm)],[f_73_3]) ).
fof(f_74_1,plain,
equalelemsP(nil),
inference(fof_nnf,[status(thm)],[ax74]) ).
fof(f_74_2,plain,
equalelemsP(nil),
inference(definitional_conversion,[status(esa)],[f_74_1]) ).
cnf(f_74_3,plain,
equalelemsP(nil),
inference(clausify,[status(thm)],[f_74_2]) ).
fof(f_75_1,plain,
! [U] :
( ? [V] :
( hd(U) = V
& ssItem(V) )
| nil = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax75]) ).
fof(f_75_2,plain,
! [U_201] :
( ? [U_200] :
( hd(U_201) = U_200
& ssItem(U_200) )
| nil = U_201
| ~ ssList(U_201) ),
inference(variable_rename,[status(thm)],[f_75_1]) ).
fof(f_75_3,plain,
! [U_201] :
( ( hd(U_201) = sK46(U_201)
& ssItem(sK46(U_201)) )
| nil = U_201
| ~ ssList(U_201) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(U_200,sK46(U_201))],[f_75_2]) ).
fof(f_75_4,plain,
( ! [U_201] :
( hd(U_201) = sK46(U_201)
| ~ sP45(U_201) )
& ! [U_201] :
( ssItem(sK46(U_201))
| ~ sP45(U_201) )
& ! [U_201] :
( sP45(U_201)
| nil = U_201
| ~ ssList(U_201) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP45])],[f_75_3]) ).
cnf(f_75_5,plain,
( sP45(U_201)
| nil = U_201
| ~ ssList(U_201) ),
inference(clausify,[status(thm)],[f_75_4]) ).
cnf(f_75_6,plain,
( ssItem(sK46(U_201))
| ~ sP45(U_201) ),
inference(clausify,[status(thm)],[f_75_4]) ).
cnf(f_75_7,plain,
( hd(U_201) = sK46(U_201)
| ~ sP45(U_201) ),
inference(clausify,[status(thm)],[f_75_4]) ).
fof(f_76_1,plain,
! [U] :
( ? [V] :
( tl(U) = V
& ssList(V) )
| nil = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax76]) ).
fof(f_76_2,plain,
! [U_203] :
( ? [U_202] :
( tl(U_203) = U_202
& ssList(U_202) )
| nil = U_203
| ~ ssList(U_203) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
fof(f_76_3,plain,
! [U_203] :
( ( tl(U_203) = sK47(U_203)
& ssList(sK47(U_203)) )
| nil = U_203
| ~ ssList(U_203) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(U_202,sK47(U_203))],[f_76_2]) ).
fof(f_76_4,plain,
( ! [U_203] :
( tl(U_203) = sK47(U_203)
| ~ sP46(U_203) )
& ! [U_203] :
( ssList(sK47(U_203))
| ~ sP46(U_203) )
& ! [U_203] :
( sP46(U_203)
| nil = U_203
| ~ ssList(U_203) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP46])],[f_76_3]) ).
cnf(f_76_5,plain,
( sP46(U_203)
| nil = U_203
| ~ ssList(U_203) ),
inference(clausify,[status(thm)],[f_76_4]) ).
cnf(f_76_6,plain,
( ssList(sK47(U_203))
| ~ sP46(U_203) ),
inference(clausify,[status(thm)],[f_76_4]) ).
cnf(f_76_7,plain,
( tl(U_203) = sK47(U_203)
| ~ sP46(U_203) ),
inference(clausify,[status(thm)],[f_76_4]) ).
fof(f_77_1,plain,
! [U] :
( ! [V] :
( V = U
| tl(V) != tl(U)
| hd(V) != hd(U)
| nil = U
| nil = V
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax77]) ).
fof(f_77_2,plain,
! [U_205] :
( ! [U_204] :
( U_204 = U_205
| tl(U_204) != tl(U_205)
| hd(U_204) != hd(U_205)
| nil = U_205
| nil = U_204
| ~ ssList(U_204) )
| ~ ssList(U_205) ),
inference(variable_rename,[status(thm)],[f_77_1]) ).
fof(f_77_3,plain,
! [U_205,U_204] :
( U_204 = U_205
| tl(U_204) != tl(U_205)
| hd(U_204) != hd(U_205)
| nil = U_205
| nil = U_204
| ~ ssList(U_204)
| ~ ssList(U_205) ),
inference(definitional_conversion,[status(esa)],[f_77_2]) ).
cnf(f_77_4,plain,
( U_204 = U_205
| tl(U_204) != tl(U_205)
| hd(U_204) != hd(U_205)
| nil = U_205
| nil = U_204
| ~ ssList(U_204)
| ~ ssList(U_205) ),
inference(clausify,[status(thm)],[f_77_3]) ).
fof(f_78_1,plain,
! [U] :
( cons(hd(U),tl(U)) = U
| nil = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax78]) ).
fof(f_78_2,plain,
! [U_206] :
( cons(hd(U_206),tl(U_206)) = U_206
| nil = U_206
| ~ ssList(U_206) ),
inference(variable_rename,[status(thm)],[f_78_1]) ).
fof(f_78_3,plain,
! [U_206] :
( cons(hd(U_206),tl(U_206)) = U_206
| nil = U_206
| ~ ssList(U_206) ),
inference(definitional_conversion,[status(esa)],[f_78_2]) ).
cnf(f_78_4,plain,
( cons(hd(U_206),tl(U_206)) = U_206
| nil = U_206
| ~ ssList(U_206) ),
inference(clausify,[status(thm)],[f_78_3]) ).
fof(f_79_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( W = U
| app(W,V) != app(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax79]) ).
fof(f_79_2,plain,
! [U_209] :
( ! [U_208] :
( ! [U_207] :
( U_207 = U_209
| app(U_207,U_208) != app(U_209,U_208)
| ~ ssList(U_207) )
| ~ ssList(U_208) )
| ~ ssList(U_209) ),
inference(variable_rename,[status(thm)],[f_79_1]) ).
fof(f_79_3,plain,
! [U_207,U_208,U_209] :
( U_207 = U_209
| app(U_207,U_208) != app(U_209,U_208)
| ~ ssList(U_207)
| ~ ssList(U_208)
| ~ ssList(U_209) ),
inference(definitional_conversion,[status(esa)],[f_79_2]) ).
cnf(f_79_4,plain,
( U_207 = U_209
| app(U_207,U_208) != app(U_209,U_208)
| ~ ssList(U_207)
| ~ ssList(U_208)
| ~ ssList(U_209) ),
inference(clausify,[status(thm)],[f_79_3]) ).
fof(f_80_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( W = U
| app(V,W) != app(V,U)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax80]) ).
fof(f_80_2,plain,
! [U_212] :
( ! [U_211] :
( ! [U_210] :
( U_210 = U_212
| app(U_211,U_210) != app(U_211,U_212)
| ~ ssList(U_210) )
| ~ ssList(U_211) )
| ~ ssList(U_212) ),
inference(variable_rename,[status(thm)],[f_80_1]) ).
fof(f_80_3,plain,
! [U_212,U_211,U_210] :
( U_210 = U_212
| app(U_211,U_210) != app(U_211,U_212)
| ~ ssList(U_210)
| ~ ssList(U_211)
| ~ ssList(U_212) ),
inference(definitional_conversion,[status(esa)],[f_80_2]) ).
cnf(f_80_4,plain,
( U_210 = U_212
| app(U_211,U_210) != app(U_211,U_212)
| ~ ssList(U_210)
| ~ ssList(U_211)
| ~ ssList(U_212) ),
inference(clausify,[status(thm)],[f_80_3]) ).
fof(f_81_1,plain,
! [U] :
( ! [V] :
( cons(V,U) = app(cons(V,nil),U)
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax81]) ).
fof(f_81_2,plain,
! [U_214] :
( ! [U_213] :
( cons(U_213,U_214) = app(cons(U_213,nil),U_214)
| ~ ssItem(U_213) )
| ~ ssList(U_214) ),
inference(variable_rename,[status(thm)],[f_81_1]) ).
fof(f_81_3,plain,
! [U_214,U_213] :
( cons(U_213,U_214) = app(cons(U_213,nil),U_214)
| ~ ssItem(U_213)
| ~ ssList(U_214) ),
inference(definitional_conversion,[status(esa)],[f_81_2]) ).
cnf(f_81_4,plain,
( cons(U_213,U_214) = app(cons(U_213,nil),U_214)
| ~ ssItem(U_213)
| ~ ssList(U_214) ),
inference(clausify,[status(thm)],[f_81_3]) ).
fof(f_82_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( app(app(U,V),W) = app(U,app(V,W))
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax82]) ).
fof(f_82_2,plain,
! [U_217] :
( ! [U_216] :
( ! [U_215] :
( app(app(U_217,U_216),U_215) = app(U_217,app(U_216,U_215))
| ~ ssList(U_215) )
| ~ ssList(U_216) )
| ~ ssList(U_217) ),
inference(variable_rename,[status(thm)],[f_82_1]) ).
fof(f_82_3,plain,
! [U_215,U_216,U_217] :
( app(app(U_217,U_216),U_215) = app(U_217,app(U_216,U_215))
| ~ ssList(U_215)
| ~ ssList(U_216)
| ~ ssList(U_217) ),
inference(definitional_conversion,[status(esa)],[f_82_2]) ).
cnf(f_82_4,plain,
( app(app(U_217,U_216),U_215) = app(U_217,app(U_216,U_215))
| ~ ssList(U_215)
| ~ ssList(U_216)
| ~ ssList(U_217) ),
inference(clausify,[status(thm)],[f_82_3]) ).
fof(f_83_1,plain,
! [U] :
( ! [V] :
( ( ( nil = app(U,V)
| nil != U
| nil != V )
& ( ( nil = U
& nil = V )
| nil != app(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax83]) ).
fof(f_83_2,plain,
! [U_219] :
( ! [U_218] :
( ( ( nil = app(U_219,U_218)
| nil != U_219
| nil != U_218 )
& ( ( nil = U_219
& nil = U_218 )
| nil != app(U_219,U_218) ) )
| ~ ssList(U_218) )
| ~ ssList(U_219) ),
inference(variable_rename,[status(thm)],[f_83_1]) ).
fof(f_83_3,plain,
( ! [U_219,U_218] :
( nil = U_219
| ~ sP47(U_219,U_218) )
& ! [U_219,U_218] :
( nil = U_218
| ~ sP47(U_219,U_218) )
& ! [U_219,U_218] :
( nil = app(U_219,U_218)
| nil != U_219
| nil != U_218
| ~ sP48(U_219,U_218) )
& ! [U_219,U_218] :
( sP47(U_219,U_218)
| nil != app(U_219,U_218)
| ~ sP48(U_219,U_218) )
& ! [U_219,U_218] :
( sP48(U_219,U_218)
| ~ ssList(U_218)
| ~ ssList(U_219) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP47,sP48])],[f_83_2]) ).
cnf(f_83_4,plain,
( sP48(U_219,U_218)
| ~ ssList(U_218)
| ~ ssList(U_219) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_5,plain,
( sP47(U_219,U_218)
| nil != app(U_219,U_218)
| ~ sP48(U_219,U_218) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_6,plain,
( nil = app(U_219,U_218)
| nil != U_219
| nil != U_218
| ~ sP48(U_219,U_218) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_7,plain,
( nil = U_218
| ~ sP47(U_219,U_218) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_8,plain,
( nil = U_219
| ~ sP47(U_219,U_218) ),
inference(clausify,[status(thm)],[f_83_3]) ).
fof(f_84_1,plain,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax84]) ).
fof(f_84_2,plain,
! [U_220] :
( app(U_220,nil) = U_220
| ~ ssList(U_220) ),
inference(variable_rename,[status(thm)],[f_84_1]) ).
fof(f_84_3,plain,
! [U_220] :
( app(U_220,nil) = U_220
| ~ ssList(U_220) ),
inference(definitional_conversion,[status(esa)],[f_84_2]) ).
cnf(f_84_4,plain,
( app(U_220,nil) = U_220
| ~ ssList(U_220) ),
inference(clausify,[status(thm)],[f_84_3]) ).
fof(f_85_1,plain,
! [U] :
( ! [V] :
( hd(app(U,V)) = hd(U)
| nil = U
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax85]) ).
fof(f_85_2,plain,
! [U_222] :
( ! [U_221] :
( hd(app(U_222,U_221)) = hd(U_222)
| nil = U_222
| ~ ssList(U_221) )
| ~ ssList(U_222) ),
inference(variable_rename,[status(thm)],[f_85_1]) ).
fof(f_85_3,plain,
! [U_221,U_222] :
( hd(app(U_222,U_221)) = hd(U_222)
| nil = U_222
| ~ ssList(U_221)
| ~ ssList(U_222) ),
inference(definitional_conversion,[status(esa)],[f_85_2]) ).
cnf(f_85_4,plain,
( hd(app(U_222,U_221)) = hd(U_222)
| nil = U_222
| ~ ssList(U_221)
| ~ ssList(U_222) ),
inference(clausify,[status(thm)],[f_85_3]) ).
fof(f_86_1,plain,
! [U] :
( ! [V] :
( tl(app(U,V)) = app(tl(U),V)
| nil = U
| ~ ssList(V) )
| ~ ssList(U) ),
inference(fof_nnf,[status(thm)],[ax86]) ).
fof(f_86_2,plain,
! [U_224] :
( ! [U_223] :
( tl(app(U_224,U_223)) = app(tl(U_224),U_223)
| nil = U_224
| ~ ssList(U_223) )
| ~ ssList(U_224) ),
inference(variable_rename,[status(thm)],[f_86_1]) ).
fof(f_86_3,plain,
! [U_224,U_223] :
( tl(app(U_224,U_223)) = app(tl(U_224),U_223)
| nil = U_224
| ~ ssList(U_223)
| ~ ssList(U_224) ),
inference(definitional_conversion,[status(esa)],[f_86_2]) ).
cnf(f_86_4,plain,
( tl(app(U_224,U_223)) = app(tl(U_224),U_223)
| nil = U_224
| ~ ssList(U_223)
| ~ ssList(U_224) ),
inference(clausify,[status(thm)],[f_86_3]) ).
fof(f_87_1,plain,
! [U] :
( ! [V] :
( U = V
| ~ geq(V,U)
| ~ geq(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax87]) ).
fof(f_87_2,plain,
! [U_226] :
( ! [U_225] :
( U_226 = U_225
| ~ geq(U_225,U_226)
| ~ geq(U_226,U_225)
| ~ ssItem(U_225) )
| ~ ssItem(U_226) ),
inference(variable_rename,[status(thm)],[f_87_1]) ).
fof(f_87_3,plain,
! [U_226,U_225] :
( U_226 = U_225
| ~ geq(U_225,U_226)
| ~ geq(U_226,U_225)
| ~ ssItem(U_225)
| ~ ssItem(U_226) ),
inference(definitional_conversion,[status(esa)],[f_87_2]) ).
cnf(f_87_4,plain,
( U_226 = U_225
| ~ geq(U_225,U_226)
| ~ geq(U_226,U_225)
| ~ ssItem(U_225)
| ~ ssItem(U_226) ),
inference(clausify,[status(thm)],[f_87_3]) ).
fof(f_88_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( geq(U,W)
| ~ geq(V,W)
| ~ geq(U,V)
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax88]) ).
fof(f_88_2,plain,
! [U_229] :
( ! [U_228] :
( ! [U_227] :
( geq(U_229,U_227)
| ~ geq(U_228,U_227)
| ~ geq(U_229,U_228)
| ~ ssItem(U_227) )
| ~ ssItem(U_228) )
| ~ ssItem(U_229) ),
inference(variable_rename,[status(thm)],[f_88_1]) ).
fof(f_88_3,plain,
! [U_227,U_229,U_228] :
( geq(U_229,U_227)
| ~ geq(U_228,U_227)
| ~ geq(U_229,U_228)
| ~ ssItem(U_227)
| ~ ssItem(U_228)
| ~ ssItem(U_229) ),
inference(definitional_conversion,[status(esa)],[f_88_2]) ).
cnf(f_88_4,plain,
( geq(U_229,U_227)
| ~ geq(U_228,U_227)
| ~ geq(U_229,U_228)
| ~ ssItem(U_227)
| ~ ssItem(U_228)
| ~ ssItem(U_229) ),
inference(clausify,[status(thm)],[f_88_3]) ).
fof(f_89_1,plain,
! [U] :
( geq(U,U)
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax89]) ).
fof(f_89_2,plain,
! [U_230] :
( geq(U_230,U_230)
| ~ ssItem(U_230) ),
inference(variable_rename,[status(thm)],[f_89_1]) ).
fof(f_89_3,plain,
! [U_230] :
( geq(U_230,U_230)
| ~ ssItem(U_230) ),
inference(definitional_conversion,[status(esa)],[f_89_2]) ).
cnf(f_89_4,plain,
( geq(U_230,U_230)
| ~ ssItem(U_230) ),
inference(clausify,[status(thm)],[f_89_3]) ).
fof(f_90_1,plain,
! [U] :
( ~ lt(U,U)
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax90]) ).
fof(f_90_2,plain,
! [U_231] :
( ~ lt(U_231,U_231)
| ~ ssItem(U_231) ),
inference(variable_rename,[status(thm)],[f_90_1]) ).
fof(f_90_3,plain,
! [U_231] :
( ~ lt(U_231,U_231)
| ~ ssItem(U_231) ),
inference(definitional_conversion,[status(esa)],[f_90_2]) ).
cnf(f_90_4,plain,
( ~ lt(U_231,U_231)
| ~ ssItem(U_231) ),
inference(clausify,[status(thm)],[f_90_3]) ).
fof(f_91_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( lt(U,W)
| ~ lt(V,W)
| ~ leq(U,V)
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax91]) ).
fof(f_91_2,plain,
! [U_234] :
( ! [U_233] :
( ! [U_232] :
( lt(U_234,U_232)
| ~ lt(U_233,U_232)
| ~ leq(U_234,U_233)
| ~ ssItem(U_232) )
| ~ ssItem(U_233) )
| ~ ssItem(U_234) ),
inference(variable_rename,[status(thm)],[f_91_1]) ).
fof(f_91_3,plain,
! [U_234,U_232,U_233] :
( lt(U_234,U_232)
| ~ lt(U_233,U_232)
| ~ leq(U_234,U_233)
| ~ ssItem(U_232)
| ~ ssItem(U_233)
| ~ ssItem(U_234) ),
inference(definitional_conversion,[status(esa)],[f_91_2]) ).
cnf(f_91_4,plain,
( lt(U_234,U_232)
| ~ lt(U_233,U_232)
| ~ leq(U_234,U_233)
| ~ ssItem(U_232)
| ~ ssItem(U_233)
| ~ ssItem(U_234) ),
inference(clausify,[status(thm)],[f_91_3]) ).
fof(f_92_1,plain,
! [U] :
( ! [V] :
( lt(U,V)
| U = V
| ~ leq(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax92]) ).
fof(f_92_2,plain,
! [U_236] :
( ! [U_235] :
( lt(U_236,U_235)
| U_236 = U_235
| ~ leq(U_236,U_235)
| ~ ssItem(U_235) )
| ~ ssItem(U_236) ),
inference(variable_rename,[status(thm)],[f_92_1]) ).
fof(f_92_3,plain,
! [U_235,U_236] :
( lt(U_236,U_235)
| U_236 = U_235
| ~ leq(U_236,U_235)
| ~ ssItem(U_235)
| ~ ssItem(U_236) ),
inference(definitional_conversion,[status(esa)],[f_92_2]) ).
cnf(f_92_4,plain,
( lt(U_236,U_235)
| U_236 = U_235
| ~ leq(U_236,U_235)
| ~ ssItem(U_235)
| ~ ssItem(U_236) ),
inference(clausify,[status(thm)],[f_92_3]) ).
fof(f_93_1,plain,
! [U] :
( ! [V] :
( ( ( lt(U,V)
| ~ leq(U,V)
| U = V )
& ( ( leq(U,V)
& U != V )
| ~ lt(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax93]) ).
fof(f_93_2,plain,
! [U_238] :
( ! [U_237] :
( ( ( lt(U_238,U_237)
| ~ leq(U_238,U_237)
| U_238 = U_237 )
& ( ( leq(U_238,U_237)
& U_238 != U_237 )
| ~ lt(U_238,U_237) ) )
| ~ ssItem(U_237) )
| ~ ssItem(U_238) ),
inference(variable_rename,[status(thm)],[f_93_1]) ).
fof(f_93_3,plain,
( ! [U_238,U_237] :
( leq(U_238,U_237)
| ~ sP49(U_238,U_237) )
& ! [U_238,U_237] :
( U_238 != U_237
| ~ sP49(U_238,U_237) )
& ! [U_238,U_237] :
( lt(U_238,U_237)
| ~ leq(U_238,U_237)
| U_238 = U_237
| ~ sP50(U_238,U_237) )
& ! [U_238,U_237] :
( sP49(U_238,U_237)
| ~ lt(U_238,U_237)
| ~ sP50(U_238,U_237) )
& ! [U_238,U_237] :
( sP50(U_238,U_237)
| ~ ssItem(U_237)
| ~ ssItem(U_238) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP49,sP50])],[f_93_2]) ).
cnf(f_93_4,plain,
( sP50(U_238,U_237)
| ~ ssItem(U_237)
| ~ ssItem(U_238) ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_5,plain,
( sP49(U_238,U_237)
| ~ lt(U_238,U_237)
| ~ sP50(U_238,U_237) ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_6,plain,
( lt(U_238,U_237)
| ~ leq(U_238,U_237)
| U_238 = U_237
| ~ sP50(U_238,U_237) ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_7,plain,
( U_238 != U_237
| ~ sP49(U_238,U_237) ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_8,plain,
( leq(U_238,U_237)
| ~ sP49(U_238,U_237) ),
inference(clausify,[status(thm)],[f_93_3]) ).
fof(f_94_1,plain,
! [U] :
( ! [V] :
( ~ gt(V,U)
| ~ gt(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax94]) ).
fof(f_94_2,plain,
! [U_240] :
( ! [U_239] :
( ~ gt(U_239,U_240)
| ~ gt(U_240,U_239)
| ~ ssItem(U_239) )
| ~ ssItem(U_240) ),
inference(variable_rename,[status(thm)],[f_94_1]) ).
fof(f_94_3,plain,
! [U_240,U_239] :
( ~ gt(U_239,U_240)
| ~ gt(U_240,U_239)
| ~ ssItem(U_239)
| ~ ssItem(U_240) ),
inference(definitional_conversion,[status(esa)],[f_94_2]) ).
cnf(f_94_4,plain,
( ~ gt(U_239,U_240)
| ~ gt(U_240,U_239)
| ~ ssItem(U_239)
| ~ ssItem(U_240) ),
inference(clausify,[status(thm)],[f_94_3]) ).
fof(f_95_1,plain,
! [U] :
( ! [V] :
( ! [W] :
( gt(U,W)
| ~ gt(V,W)
| ~ gt(U,V)
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(fof_nnf,[status(thm)],[ax95]) ).
fof(f_95_2,plain,
! [U_243] :
( ! [U_242] :
( ! [U_241] :
( gt(U_243,U_241)
| ~ gt(U_242,U_241)
| ~ gt(U_243,U_242)
| ~ ssItem(U_241) )
| ~ ssItem(U_242) )
| ~ ssItem(U_243) ),
inference(variable_rename,[status(thm)],[f_95_1]) ).
fof(f_95_3,plain,
! [U_242,U_241,U_243] :
( gt(U_243,U_241)
| ~ gt(U_242,U_241)
| ~ gt(U_243,U_242)
| ~ ssItem(U_241)
| ~ ssItem(U_242)
| ~ ssItem(U_243) ),
inference(definitional_conversion,[status(esa)],[f_95_2]) ).
cnf(f_95_4,plain,
( gt(U_243,U_241)
| ~ gt(U_242,U_241)
| ~ gt(U_243,U_242)
| ~ ssItem(U_241)
| ~ ssItem(U_242)
| ~ ssItem(U_243) ),
inference(clausify,[status(thm)],[f_95_3]) ).
fof(f_96_1,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( segmentP(V,U)
| ? [Y] :
( equalelemsP(Y)
& segmentP(Y,W)
& segmentP(X,Y)
& neq(W,Y)
& ssList(Y) )
| ~ equalelemsP(W)
| ~ segmentP(X,W)
| ~ neq(V,nil)
| U != W
| V != X ) ) ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_96_2,negated_conjecture,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ~ segmentP(V,U)
& ! [Y] :
( ~ equalelemsP(Y)
| ~ segmentP(Y,W)
| ~ segmentP(X,Y)
| ~ neq(W,Y)
| ~ ssList(Y) )
& equalelemsP(W)
& segmentP(X,W)
& neq(V,nil)
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(fof_nnf,[status(thm)],[f_96_1]) ).
fof(f_96_3,negated_conjecture,
? [U_248] :
( ? [U_247] :
( ? [U_246] :
( ? [U_245] :
( ~ segmentP(U_247,U_248)
& ! [U_244] :
( ~ equalelemsP(U_244)
| ~ segmentP(U_244,U_246)
| ~ segmentP(U_245,U_244)
| ~ neq(U_246,U_244)
| ~ ssList(U_244) )
& equalelemsP(U_246)
& segmentP(U_245,U_246)
& neq(U_247,nil)
& U_248 = U_246
& U_247 = U_245
& ssList(U_245) )
& ssList(U_246) )
& ssList(U_247) )
& ssList(U_248) ),
inference(variable_rename,[status(thm)],[f_96_2]) ).
fof(f_96_4,negated_conjecture,
( ? [U_247] :
( ? [U_246] :
( ? [U_245] :
( ~ segmentP(U_247,sK48)
& ! [U_244] :
( ~ equalelemsP(U_244)
| ~ segmentP(U_244,U_246)
| ~ segmentP(U_245,U_244)
| ~ neq(U_246,U_244)
| ~ ssList(U_244) )
& equalelemsP(U_246)
& segmentP(U_245,U_246)
& neq(U_247,nil)
& sK48 = U_246
& U_247 = U_245
& ssList(U_245) )
& ssList(U_246) )
& ssList(U_247) )
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(U_248,sK48)],[f_96_3]) ).
fof(f_96_5,negated_conjecture,
( ? [U_246] :
( ? [U_245] :
( ~ segmentP(sK49,sK48)
& ! [U_244] :
( ~ equalelemsP(U_244)
| ~ segmentP(U_244,U_246)
| ~ segmentP(U_245,U_244)
| ~ neq(U_246,U_244)
| ~ ssList(U_244) )
& equalelemsP(U_246)
& segmentP(U_245,U_246)
& neq(sK49,nil)
& sK48 = U_246
& sK49 = U_245
& ssList(U_245) )
& ssList(U_246) )
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(U_247,sK49)],[f_96_4]) ).
fof(f_96_6,negated_conjecture,
( ? [U_245] :
( ~ segmentP(sK49,sK48)
& ! [U_244] :
( ~ equalelemsP(U_244)
| ~ segmentP(U_244,sK50)
| ~ segmentP(U_245,U_244)
| ~ neq(sK50,U_244)
| ~ ssList(U_244) )
& equalelemsP(sK50)
& segmentP(U_245,sK50)
& neq(sK49,nil)
& sK48 = sK50
& sK49 = U_245
& ssList(U_245) )
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(U_246,sK50)],[f_96_5]) ).
fof(f_96_7,negated_conjecture,
( ~ segmentP(sK49,sK48)
& ! [U_244] :
( ~ equalelemsP(U_244)
| ~ segmentP(U_244,sK50)
| ~ segmentP(sK51,U_244)
| ~ neq(sK50,U_244)
| ~ ssList(U_244) )
& equalelemsP(sK50)
& segmentP(sK51,sK50)
& neq(sK49,nil)
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(U_245,sK51)],[f_96_6]) ).
fof(f_96_8,negated_conjecture,
( ~ segmentP(sK49,sK48)
& ! [U_244] :
( ~ equalelemsP(U_244)
| ~ segmentP(U_244,sK50)
| ~ segmentP(sK51,U_244)
| ~ neq(sK50,U_244)
| ~ ssList(U_244) )
& equalelemsP(sK50)
& segmentP(sK51,sK50)
& neq(sK49,nil)
& sK48 = sK50
& sK49 = sK51
& ssList(sK51)
& ssList(sK50)
& ssList(sK49)
& ssList(sK48) ),
inference(definitional_conversion,[status(esa)],[f_96_7]) ).
cnf(f_96_9,negated_conjecture,
ssList(sK48),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_10,negated_conjecture,
ssList(sK49),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_11,negated_conjecture,
ssList(sK50),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_12,negated_conjecture,
ssList(sK51),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_13,negated_conjecture,
sK49 = sK51,
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_14,negated_conjecture,
sK48 = sK50,
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_15,negated_conjecture,
neq(sK49,nil),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_16,negated_conjecture,
segmentP(sK51,sK50),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_17,negated_conjecture,
equalelemsP(sK50),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_18,negated_conjecture,
( ~ equalelemsP(U_244)
| ~ segmentP(U_244,sK50)
| ~ segmentP(sK51,U_244)
| ~ neq(sK50,U_244)
| ~ ssList(U_244) ),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(f_96_19,negated_conjecture,
~ segmentP(sK49,sK48),
inference(clausify,[status(thm)],[f_96_8]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( cons(Eq_x_0,Eq_x_1) = cons(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( app(Eq_x_0,Eq_x_1) = app(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( hd(Eq_x_0) = hd(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( tl(Eq_x_0) = tl(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( sK3(Eq_x_0,Eq_x_1) = sK3(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( sK4(Eq_x_0,Eq_x_1) = sK4(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( sK5(Eq_x_0) = sK5(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( sK6(Eq_x_0,Eq_x_1) = sK6(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( sK7(Eq_x_0,Eq_x_1) = sK7(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( sK8(Eq_x_0,Eq_x_1) = sK8(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( sK9(Eq_x_0,Eq_x_1) = sK9(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( sK10(Eq_x_0) = sK10(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( sK11(Eq_x_0) = sK11(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( sK12(Eq_x_0) = sK12(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( sK13(Eq_x_0) = sK13(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( sK14(Eq_x_0) = sK14(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( sK15(Eq_x_0) = sK15(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( sK16(Eq_x_0) = sK16(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( sK17(Eq_x_0) = sK17(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( sK18(Eq_x_0) = sK18(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( sK19(Eq_x_0) = sK19(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( sK20(Eq_x_0) = sK20(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( sK21(Eq_x_0) = sK21(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( sK22(Eq_x_0) = sK22(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( sK23(Eq_x_0) = sK23(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( sK24(Eq_x_0) = sK24(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( sK25(Eq_x_0) = sK25(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( sK26(Eq_x_0) = sK26(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( sK27(Eq_x_0) = sK27(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( sK28(Eq_x_0) = sK28(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( sK29(Eq_x_0) = sK29(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( sK30(Eq_x_0) = sK30(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( sK31(Eq_x_0) = sK31(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( sK32(Eq_x_0) = sK32(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( sK33(Eq_x_0) = sK33(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( sK34(Eq_x_0) = sK34(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_40,axiom,
( sK35(Eq_x_0) = sK35(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( sK36(Eq_x_0) = sK36(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_42,axiom,
( sK37(Eq_x_0) = sK37(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_43,axiom,
( sK38(Eq_x_0) = sK38(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_44,axiom,
( sK39(Eq_x_0) = sK39(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_45,axiom,
( sK40(Eq_x_0) = sK40(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_46,axiom,
( sK41(Eq_x_0) = sK41(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_47,axiom,
( sK42(Eq_x_0) = sK42(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_48,axiom,
( sK43(Eq_x_0) = sK43(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_49,axiom,
( sK44(Eq_x_0) = sK44(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_50,axiom,
( sK45(Eq_x_0) = sK45(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_51,axiom,
( sK46(Eq_x_0) = sK46(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_52,axiom,
( sK47(Eq_x_0) = sK47(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_53,axiom,
( ssItem(Eq_y_0)
| ~ ssItem(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_54,axiom,
( neq(Eq_y_0,Eq_y_1)
| ~ neq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_55,axiom,
( ssList(Eq_y_0)
| ~ ssList(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_56,axiom,
( memberP(Eq_y_0,Eq_y_1)
| ~ memberP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_57,axiom,
( singletonP(Eq_y_0)
| ~ singletonP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_58,axiom,
( frontsegP(Eq_y_0,Eq_y_1)
| ~ frontsegP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_59,axiom,
( rearsegP(Eq_y_0,Eq_y_1)
| ~ rearsegP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_60,axiom,
( segmentP(Eq_y_0,Eq_y_1)
| ~ segmentP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_61,axiom,
( cyclefreeP(Eq_y_0)
| ~ cyclefreeP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_62,axiom,
( leq(Eq_y_0,Eq_y_1)
| ~ leq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_63,axiom,
( totalorderP(Eq_y_0)
| ~ totalorderP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_64,axiom,
( strictorderP(Eq_y_0)
| ~ strictorderP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_65,axiom,
( lt(Eq_y_0,Eq_y_1)
| ~ lt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_66,axiom,
( totalorderedP(Eq_y_0)
| ~ totalorderedP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_67,axiom,
( strictorderedP(Eq_y_0)
| ~ strictorderedP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_68,axiom,
( duplicatefreeP(Eq_y_0)
| ~ duplicatefreeP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_69,axiom,
( equalelemsP(Eq_y_0)
| ~ equalelemsP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_70,axiom,
( geq(Eq_y_0,Eq_y_1)
| ~ geq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_71,axiom,
( gt(Eq_y_0,Eq_y_1)
| ~ gt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_72,axiom,
( sP0(Eq_y_0,Eq_y_1)
| ~ sP0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_73,axiom,
( sP1(Eq_y_0,Eq_y_1)
| ~ sP1(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_74,axiom,
( sP2(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP2(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_75,axiom,
( sP3(Eq_y_0)
| ~ sP3(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_76,axiom,
( sP4(Eq_y_0,Eq_y_1)
| ~ sP4(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_77,axiom,
( sP5(Eq_y_0,Eq_y_1)
| ~ sP5(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_78,axiom,
( sP6(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP6(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_79,axiom,
( sP7(Eq_y_0,Eq_y_1)
| ~ sP7(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_80,axiom,
( sP8(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP8(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_81,axiom,
( sP9(Eq_y_0,Eq_y_1)
| ~ sP9(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_82,axiom,
( sP10(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP10(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_83,axiom,
( sP11(Eq_y_0)
| ~ sP11(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_84,axiom,
( sP12(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| ~ sP12(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_85,axiom,
( sP13(Eq_y_0)
| ~ sP13(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_86,axiom,
( sP14(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| ~ sP14(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_87,axiom,
( sP15(Eq_y_0)
| ~ sP15(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_88,axiom,
( sP16(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| ~ sP16(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_89,axiom,
( sP17(Eq_y_0)
| ~ sP17(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_90,axiom,
( sP18(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| ~ sP18(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_91,axiom,
( sP19(Eq_y_0)
| ~ sP19(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_92,axiom,
( sP20(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| ~ sP20(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_93,axiom,
( sP21(Eq_y_0)
| ~ sP21(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_94,axiom,
( sP22(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| ~ sP22(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_95,axiom,
( sP23(Eq_y_0)
| ~ sP23(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_96,axiom,
( sP24(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| ~ sP24(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_97,axiom,
( sP25(Eq_y_0,Eq_y_1)
| ~ sP25(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_98,axiom,
( sP26(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP26(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_99,axiom,
( sP27(Eq_y_0)
| ~ sP27(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_100,axiom,
( sP28(Eq_y_0,Eq_y_1)
| ~ sP28(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_101,axiom,
( sP29(Eq_y_0,Eq_y_1)
| ~ sP29(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_102,axiom,
( sP30(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP30(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_103,axiom,
( sP31(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP31(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_104,axiom,
( sP32(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP32(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_105,axiom,
( sP33(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP33(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_106,axiom,
( sP34(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP34(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_107,axiom,
( sP35(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP35(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_108,axiom,
( sP36(Eq_y_0)
| ~ sP36(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_109,axiom,
( sP37(Eq_y_0)
| ~ sP37(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_110,axiom,
( sP38(Eq_y_0)
| ~ sP38(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_111,axiom,
( sP39(Eq_y_0,Eq_y_1)
| ~ sP39(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_112,axiom,
( sP40(Eq_y_0,Eq_y_1)
| ~ sP40(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_113,axiom,
( sP41(Eq_y_0,Eq_y_1)
| ~ sP41(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_114,axiom,
( sP42(Eq_y_0,Eq_y_1)
| ~ sP42(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_115,axiom,
( sP43(Eq_y_0,Eq_y_1)
| ~ sP43(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_116,axiom,
( sP44(Eq_y_0,Eq_y_1)
| ~ sP44(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_117,axiom,
( sP45(Eq_y_0)
| ~ sP45(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_118,axiom,
( sP46(Eq_y_0)
| ~ sP46(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_119,axiom,
( sP47(Eq_y_0,Eq_y_1)
| ~ sP47(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_120,axiom,
( sP48(Eq_y_0,Eq_y_1)
| ~ sP48(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_121,axiom,
( sP49(Eq_y_0,Eq_y_1)
| ~ sP49(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_122,axiom,
( sP50(Eq_y_0,Eq_y_1)
| ~ sP50(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC359+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/20.29 % CPULimit : 300
% 0.07/20.29 % WCLimit : 300
% 0.07/20.29 % DateTime : Sun Sep 20 02:44:58 UTC 2026
% 0.19/20.30 % CPUTime :
% 234.85/255.11 % SZS status Theorem for theBenchmark
% 234.85/255.11 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------