%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : COM141+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 08:14:53 AM UTC 2026
% Result : Theorem 173.45s 173.73s
% Output : Proof 173.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM141+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n020.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sun Sep 20 15:22:17 UTC 2026
% 0.09/0.35 % CPUTime :
% 173.45/173.73 % SZS status Theorem for theBenchmark
% 173.45/173.73 % SZS output start Proof for theBenchmark
% 173.65/173.99 fof(EQ-var, axiom,
% 173.65/173.99 ! [ VVar0,VVar1 ] : ( ( vvar(VVar0) = vvar(VVar1) => VVar0 = VVar1 ) & ( VVar0 = VVar1 => vvar(VVar0) = vvar(VVar1) ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-var) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-abs, axiom,
% 173.65/173.99 ! [ VVar0,VTyp0,VExp0,VVar1,VTyp1,VExp1 ] : ( ( vabs(VVar0, VTyp0, VExp0) = vabs(VVar1, VTyp1, VExp1) => ( VVar0 = VVar1 & VTyp0 = VTyp1 & VExp0 = VExp1 ) ) & ( ( VVar0 = VVar1 & VTyp0 = VTyp1 & VExp0 = VExp1 ) => vabs(VVar0, VTyp0, VExp0) = vabs(VVar1, VTyp1, VExp1) ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-abs) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-app, axiom,
% 173.65/173.99 ! [ VExp0,VExp1,VExp2,VExp3 ] : ( ( vapp(VExp0, VExp1) = vapp(VExp2, VExp3) => ( VExp0 = VExp2 & VExp1 = VExp3 ) ) & ( ( VExp0 = VExp2 & VExp1 = VExp3 ) => vapp(VExp0, VExp1) = vapp(VExp2, VExp3) ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-app) ).
% 173.65/173.99
% 173.65/173.99 fof(DIFF-var-abs, axiom,
% 173.65/173.99 ! [ VVar0,VVar1,VTyp0,VExp0 ] : ~( vvar(VVar0) = vabs(VVar1, VTyp0, VExp0) ),
% 173.65/173.99 file('COM001+0.ax', DIFF-var-abs) ).
% 173.65/173.99
% 173.65/173.99 fof(DIFF-var-app, axiom,
% 173.65/173.99 ! [ VVar0,VExp0,VExp1 ] : ~( vvar(VVar0) = vapp(VExp0, VExp1) ),
% 173.65/173.99 file('COM001+0.ax', DIFF-var-app) ).
% 173.65/173.99
% 173.65/173.99 fof(DIFF-abs-app, axiom,
% 173.65/173.99 ! [ VVar0,VTyp0,VExp0,VExp1,VExp2 ] : ~( vabs(VVar0, VTyp0, VExp0) = vapp(VExp1, VExp2) ),
% 173.65/173.99 file('COM001+0.ax', DIFF-abs-app) ).
% 173.65/173.99
% 173.65/173.99 fof(isValue0, axiom,
% 173.65/173.99 ! [ Vx,VS,Ve,VExp0 ] : ( VExp0 = vabs(Vx, VS, Ve) => visValue(VExp0) ),
% 173.65/173.99 file('COM001+0.ax', isValue0) ).
% 173.65/173.99
% 173.65/173.99 fof(isValue1, axiom,
% 173.65/173.99 ! [ Vx,VExp0 ] : ( VExp0 = vvar(Vx) => ~( visValue(VExp0) ) ),
% 173.65/173.99 file('COM001+0.ax', isValue1) ).
% 173.65/173.99
% 173.65/173.99 fof(isValue2, axiom,
% 173.65/173.99 ! [ Ve1,Ve2,VExp0 ] : ( VExp0 = vapp(Ve1, Ve2) => ~( visValue(VExp0) ) ),
% 173.65/173.99 file('COM001+0.ax', isValue2) ).
% 173.65/173.99
% 173.65/173.99 fof(isFreeVar0, axiom,
% 173.65/173.99 ! [ VVar0,VExp0,Vx,Vv ] : ( ( VVar0 = Vv & VExp0 = vvar(Vx) ) => ( ( Vx = Vv => visFreeVar(VVar0, VExp0) ) & ( visFreeVar(VVar0, VExp0) => Vx = Vv ) ) ),
% 173.65/173.99 file('COM001+0.ax', isFreeVar0) ).
% 173.65/173.99
% 173.65/173.99 fof(isFreeVar1, axiom,
% 173.65/173.99 ! [ VT,VVar0,VExp0,Vx,Vv,Ve ] : ( ( VVar0 = Vv & VExp0 = vabs(Vx, VT, Ve) ) => ( ( ( ~( Vx = Vv ) & visFreeVar(Vv, Ve) ) => visFreeVar(VVar0, VExp0) ) & ( visFreeVar(VVar0, VExp0) => ( ~( Vx = Vv ) & visFreeVar(Vv, Ve) ) ) ) ),
% 173.65/173.99 file('COM001+0.ax', isFreeVar1) ).
% 173.65/173.99
% 173.65/173.99 fof(isFreeVar2, axiom,
% 173.65/173.99 ! [ VVar0,VExp0,Ve1,Vv,Ve2 ] : ( ( VVar0 = Vv & VExp0 = vapp(Ve1, Ve2) ) => ( ( ( visFreeVar(Vv, Ve1) | visFreeVar(Vv, Ve2) ) => visFreeVar(VVar0, VExp0) ) & ( visFreeVar(VVar0, VExp0) => ( visFreeVar(Vv, Ve1) | visFreeVar(Vv, Ve2) ) ) ) ),
% 173.65/173.99 file('COM001+0.ax', isFreeVar2) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-empty, axiom,
% 173.65/173.99 ( ( vempty = vempty => $true ) & ( $true => vempty = vempty ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-empty) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-bind, axiom,
% 173.65/173.99 ! [ VVar0,VTyp0,VCtx0,VVar1,VTyp1,VCtx1 ] : ( ( vbind(VVar0, VTyp0, VCtx0) = vbind(VVar1, VTyp1, VCtx1) => ( VVar0 = VVar1 & VTyp0 = VTyp1 & VCtx0 = VCtx1 ) ) & ( ( VVar0 = VVar1 & VTyp0 = VTyp1 & VCtx0 = VCtx1 ) => vbind(VVar0, VTyp0, VCtx0) = vbind(VVar1, VTyp1, VCtx1) ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-bind) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-noType, axiom,
% 173.65/173.99 ( ( vnoType = vnoType => $true ) & ( $true => vnoType = vnoType ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-noType) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-someType, axiom,
% 173.65/173.99 ! [ VTyp0,VTyp1 ] : ( ( vsomeType(VTyp0) = vsomeType(VTyp1) => VTyp0 = VTyp1 ) & ( VTyp0 = VTyp1 => vsomeType(VTyp0) = vsomeType(VTyp1) ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-someType) ).
% 173.65/173.99
% 173.65/173.99 fof(DIFF-empty-bind, axiom,
% 173.65/173.99 ! [ VVar0,VTyp0,VCtx0 ] : ~( vempty = vbind(VVar0, VTyp0, VCtx0) ),
% 173.65/173.99 file('COM001+0.ax', DIFF-empty-bind) ).
% 173.65/173.99
% 173.65/173.99 fof(DIFF-noType-someType, axiom,
% 173.65/173.99 ! [ VTyp0 ] : ~( vnoType = vsomeType(VTyp0) ),
% 173.65/173.99 file('COM001+0.ax', DIFF-noType-someType) ).
% 173.65/173.99
% 173.65/173.99 fof(isSomeType0, axiom,
% 173.65/173.99 ! [ VOptTyp0 ] : ( VOptTyp0 = vnoType => ~( visSomeType(VOptTyp0) ) ),
% 173.65/173.99 file('COM001+0.ax', isSomeType0) ).
% 173.65/173.99
% 173.65/173.99 fof(isSomeType1, axiom,
% 173.65/173.99 ! [ Ve,VOptTyp0 ] : ( VOptTyp0 = vsomeType(Ve) => visSomeType(VOptTyp0) ),
% 173.65/173.99 file('COM001+0.ax', isSomeType1) ).
% 173.65/173.99
% 173.65/173.99 fof(getSomeType0, axiom,
% 173.65/173.99 ! [ VOptTyp0,RESULT,Ve ] : ( VOptTyp0 = vsomeType(Ve) => ( RESULT = vgetSomeType(VOptTyp0) => RESULT = Ve ) ),
% 173.65/173.99 file('COM001+0.ax', getSomeType0) ).
% 173.65/173.99
% 173.65/173.99 fof(lookup0, axiom,
% 173.65/173.99 ! [ Vx,VVar0,VCtx0,RESULT ] : ( ( VVar0 = Vx & VCtx0 = vempty ) => ( RESULT = vlookup(VVar0, VCtx0) => RESULT = vnoType ) ),
% 173.65/173.99 file('COM001+0.ax', lookup0) ).
% 173.65/173.99
% 173.65/173.99 fof(lookup1, axiom,
% 173.65/173.99 ! [ VC,Vx,Vy,VVar0,VCtx0,RESULT,VTy ] : ( ( VVar0 = Vx & VCtx0 = vbind(Vy, VTy, VC) ) => ( Vx = Vy => ( RESULT = vlookup(VVar0, VCtx0) => RESULT = vsomeType(VTy) ) ) ),
% 173.65/173.99 file('COM001+0.ax', lookup1) ).
% 173.65/173.99
% 173.65/173.99 fof(lookup2, axiom,
% 173.65/173.99 ! [ VTy,Vy,VVar0,VCtx0,RESULT,Vx,VC ] : ( ( VVar0 = Vx & VCtx0 = vbind(Vy, VTy, VC) ) => ( ~( Vx = Vy ) => ( RESULT = vlookup(VVar0, VCtx0) => RESULT = vlookup(Vx, VC) ) ) ),
% 173.65/173.99 file('COM001+0.ax', lookup2) ).
% 173.65/173.99
% 173.65/173.99 fof(lookup-INV, axiom,
% 173.65/173.99 ! [ VVar0,VCtx0,RESULT ] : ( vlookup(VVar0, VCtx0) = RESULT => ( ? [ Vx ] : ( VVar0 = Vx & VCtx0 = vempty & RESULT = vnoType ) | ? [ VC,Vx,Vy,VTy ] : ( VVar0 = Vx & VCtx0 = vbind(Vy, VTy, VC) & Vx = Vy & RESULT = vsomeType(VTy) ) | ? [ VTy,Vy,Vx,VC ] : ( VVar0 = Vx & VCtx0 = vbind(Vy, VTy, VC) & ~( Vx = Vy ) & RESULT = vlookup(Vx, VC) ) ) ),
% 173.65/173.99 file('COM001+0.ax', lookup-INV) ).
% 173.65/173.99
% 173.65/173.99 fof(T-Context-Duplicate, axiom,
% 173.65/173.99 ! [ Vy,VTy,Vx,VTx,VC,Ve,VT ] : ( ( Vx = Vy & vtcheck(vbind(Vx, VTx, vbind(Vy, VTy, VC)), Ve, VT) ) => vtcheck(vbind(Vx, VTx, VC), Ve, VT) ),
% 173.65/173.99 file('COM001+0.ax', T-Context-Duplicate) ).
% 173.65/173.99
% 173.65/173.99 fof(T-Context-Swap, axiom,
% 173.65/173.99 ! [ Vy,VTy,Vx,VTx,VC,Ve,VT ] : ( ( ~( Vx = Vy ) & vtcheck(vbind(Vx, VTx, vbind(Vy, VTy, VC)), Ve, VT) ) => vtcheck(vbind(Vy, VTy, vbind(Vx, VTx, VC)), Ve, VT) ),
% 173.65/173.99 file('COM001+0.ax', T-Context-Swap) ).
% 173.65/173.99
% 173.65/173.99 fof(gensym-is-fresh, axiom,
% 173.65/173.99 ! [ Vv,Ve ] : ( vgensym(Ve) = Vv => ~( visFreeVar(Vv, Ve) ) ),
% 173.65/173.99 file('COM001+0.ax', gensym-is-fresh) ).
% 173.65/173.99
% 173.65/173.99 fof(subst0, axiom,
% 173.65/173.99 ! [ Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve ] : ( ( VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy) ) => ( Vx = Vy => ( RESULT = vsubst(VVar0, VExp0, VExp1) => RESULT = Ve ) ) ),
% 173.65/173.99 file('COM001+0.ax', subst0) ).
% 173.65/173.99
% 173.65/173.99 fof(subst1, axiom,
% 173.65/173.99 ! [ Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy ] : ( ( VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy) ) => ( ~( Vx = Vy ) => ( RESULT = vsubst(VVar0, VExp0, VExp1) => RESULT = vvar(Vy) ) ) ),
% 173.65/173.99 file('COM001+0.ax', subst1) ).
% 173.65/173.99
% 173.65/173.99 fof(subst2, axiom,
% 173.65/173.99 ! [ VVar0,VExp0,VExp1,RESULT,Ve1,Vx,Ve,Ve2 ] : ( ( VVar0 = Vx & VExp0 = Ve & VExp1 = vapp(Ve1, Ve2) ) => ( RESULT = vsubst(VVar0, VExp0, VExp1) => RESULT = vapp(vsubst(Vx, Ve, Ve1), vsubst(Vx, Ve, Ve2)) ) ),
% 173.65/173.99 file('COM001+0.ax', subst2) ).
% 173.65/173.99
% 173.65/173.99 fof(subst3, axiom,
% 173.65/173.99 ! [ Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1 ] : ( ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) ) => ( Vx = Vy => ( RESULT = vsubst(VVar0, VExp0, VExp1) => RESULT = vabs(Vy, VT, Ve1) ) ) ),
% 173.65/173.99 file('COM001+0.ax', subst3) ).
% 173.65/173.99
% 173.65/173.99 fof(subst4, axiom,
% 173.65/173.99 ! [ VVar0,VExp0,VExp1,RESULT,Vx,Ve,VT,Vy,Vfresh,Ve1 ] : ( ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) ) => ( ( ~( Vx = Vy ) & visFreeVar(Vy, Ve) & Vfresh = vgensym(vapp(vapp(Ve, Ve1), vvar(Vx))) ) => ( RESULT = vsubst(VVar0, VExp0, VExp1) => RESULT = vsubst(Vx, Ve, vabs(Vfresh, VT, vsubst(Vy, vvar(Vfresh), Ve1))) ) ) ),
% 173.65/173.99 file('COM001+0.ax', subst4) ).
% 173.65/173.99
% 173.65/173.99 fof(subst5, axiom,
% 173.65/173.99 ! [ VVar0,VExp0,VExp1,RESULT,Vy,VT,Vx,Ve,Ve1 ] : ( ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) ) => ( ( ~( Vx = Vy ) & ~( visFreeVar(Vy, Ve) ) ) => ( RESULT = vsubst(VVar0, VExp0, VExp1) => RESULT = vabs(Vy, VT, vsubst(Vx, Ve, Ve1)) ) ) ),
% 173.65/173.99 file('COM001+0.ax', subst5) ).
% 173.65/173.99
% 173.65/173.99 fof(subst-INV, axiom,
% 173.65/173.99 ! [ VVar0,VExp0,VExp1,RESULT ] : ( vsubst(VVar0, VExp0, VExp1) = RESULT => ( ? [ Vx,Vy,Ve ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy) & Vx = Vy & RESULT = Ve ) | ? [ Ve,Vx,Vy ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy) & ~( Vx = Vy ) & RESULT = vvar(Vy) ) | ? [ Ve1,Vx,Ve,Ve2 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vapp(Ve1, Ve2) & RESULT = vapp(vsubst(Vx, Ve, Ve1), vsubst(Vx, Ve, Ve2)) ) | ? [ Ve,Vx,Vy,VT,Ve1 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) & Vx = Vy & RESULT = vabs(Vy, VT, Ve1) ) | ? [ Vx,Ve,VT,Vy,Vfresh,Ve1 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) & ~( Vx = Vy ) & visFreeVar(Vy, Ve) & Vfresh = vgensym(vapp(vapp(Ve, Ve1), vvar(Vx))) & RESULT = vsubst(Vx, Ve, vabs(Vfresh, VT, vsubst(Vy, vvar(Vfresh), Ve1))) ) | ? [ Vy,VT,Vx,Ve,Ve1 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) & ~( Vx = Vy ) & ~( visFreeVar(Vy, Ve) ) & RESULT = vabs(Vy, VT, vsubst(Vx, Ve, Ve1)) ) ) ),
% 173.65/173.99 file('COM001+0.ax', subst-INV) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-noExp, axiom,
% 173.65/173.99 ( ( vnoExp = vnoExp => $true ) & ( $true => vnoExp = vnoExp ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-noExp) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-someExp, axiom,
% 173.65/173.99 ! [ VExp0,VExp1 ] : ( ( vsomeExp(VExp0) = vsomeExp(VExp1) => VExp0 = VExp1 ) & ( VExp0 = VExp1 => vsomeExp(VExp0) = vsomeExp(VExp1) ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-someExp) ).
% 173.65/173.99
% 173.65/173.99 fof(DIFF-noExp-someExp, axiom,
% 173.65/173.99 ! [ VExp0 ] : ~( vnoExp = vsomeExp(VExp0) ),
% 173.65/173.99 file('COM001+0.ax', DIFF-noExp-someExp) ).
% 173.65/173.99
% 173.65/173.99 fof(isSomeExp0, axiom,
% 173.65/173.99 ! [ VOptExp0 ] : ( VOptExp0 = vnoExp => ~( visSomeExp(VOptExp0) ) ),
% 173.65/173.99 file('COM001+0.ax', isSomeExp0) ).
% 173.65/173.99
% 173.65/173.99 fof(isSomeExp1, axiom,
% 173.65/173.99 ! [ Ve,VOptExp0 ] : ( VOptExp0 = vsomeExp(Ve) => visSomeExp(VOptExp0) ),
% 173.65/173.99 file('COM001+0.ax', isSomeExp1) ).
% 173.65/173.99
% 173.65/173.99 fof(getSomeExp0, axiom,
% 173.65/173.99 ! [ VOptExp0,RESULT,Ve ] : ( VOptExp0 = vsomeExp(Ve) => ( RESULT = vgetSomeExp(VOptExp0) => RESULT = Ve ) ),
% 173.65/173.99 file('COM001+0.ax', getSomeExp0) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce0, axiom,
% 173.65/173.99 ! [ Vx,VExp0,RESULT ] : ( VExp0 = vvar(Vx) => ( RESULT = vreduce(VExp0) => RESULT = vnoExp ) ),
% 173.65/173.99 file('COM001+0.ax', reduce0) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce1, axiom,
% 173.65/173.99 ! [ Vx,VS,Ve,VExp0,RESULT ] : ( VExp0 = vabs(Vx, VS, Ve) => ( RESULT = vreduce(VExp0) => RESULT = vnoExp ) ),
% 173.65/173.99 file('COM001+0.ax', reduce1) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce2, axiom,
% 173.65/173.99 ! [ Ve2,VExp0,RESULT,Vx,VS,Ve1,Ve2red ] : ( VExp0 = vapp(vabs(Vx, VS, Ve1), Ve2) => ( ( Ve2red = vreduce(Ve2) & visSomeExp(Ve2red) ) => ( RESULT = vreduce(VExp0) => RESULT = vsomeExp(vapp(vabs(Vx, VS, Ve1), vgetSomeExp(Ve2red))) ) ) ),
% 173.65/173.99 file('COM001+0.ax', reduce2) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce3, axiom,
% 173.65/173.99 ! [ VS,Ve2red,VExp0,RESULT,Vx,Ve2,Ve1 ] : ( VExp0 = vapp(vabs(Vx, VS, Ve1), Ve2) => ( ( Ve2red = vreduce(Ve2) & ~( visSomeExp(Ve2red) ) & visValue(Ve2) ) => ( RESULT = vreduce(VExp0) => RESULT = vsomeExp(vsubst(Vx, Ve2, Ve1)) ) ) ),
% 173.65/173.99 file('COM001+0.ax', reduce3) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce4, axiom,
% 173.65/173.99 ! [ Vx,VS,Ve1,Ve2red,Ve2,VExp0,RESULT ] : ( VExp0 = vapp(vabs(Vx, VS, Ve1), Ve2) => ( ( Ve2red = vreduce(Ve2) & ~( visSomeExp(Ve2red) ) & ~( visValue(Ve2) ) ) => ( RESULT = vreduce(VExp0) => RESULT = vnoExp ) ) ),
% 173.65/173.99 file('COM001+0.ax', reduce4) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce5, axiom,
% 173.65/173.99 ! [ Ve1,VExp0,RESULT,Ve1red,Ve2 ] : ( ( VExp0 = vapp(Ve1, Ve2) & ! [ VVx0,VVS0,VVe10 ] : ~( Ve1 = vabs(VVx0, VVS0, VVe10) ) ) => ( ( Ve1red = vreduce(Ve1) & visSomeExp(Ve1red) ) => ( RESULT = vreduce(VExp0) => RESULT = vsomeExp(vapp(vgetSomeExp(Ve1red), Ve2)) ) ) ),
% 173.65/173.99 file('COM001+0.ax', reduce5) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce6, axiom,
% 173.65/173.99 ! [ Ve2,Ve1,Ve1red,VExp0,RESULT ] : ( ( VExp0 = vapp(Ve1, Ve2) & ! [ VVx0,VVS0,VVe10 ] : ~( Ve1 = vabs(VVx0, VVS0, VVe10) ) ) => ( ( Ve1red = vreduce(Ve1) & ~( visSomeExp(Ve1red) ) ) => ( RESULT = vreduce(VExp0) => RESULT = vnoExp ) ) ),
% 173.65/173.99 file('COM001+0.ax', reduce6) ).
% 173.65/173.99
% 173.65/173.99 fof(reduce-INV, axiom,
% 173.65/173.99 ! [ VExp0,RESULT ] : ( vreduce(VExp0) = RESULT => ( ? [ Vx ] : ( VExp0 = vvar(Vx) & RESULT = vnoExp ) | ? [ Vx,VS,Ve ] : ( VExp0 = vabs(Vx, VS, Ve) & RESULT = vnoExp ) | ? [ Ve2,Vx,VS,Ve1,Ve2red ] : ( VExp0 = vapp(vabs(Vx, VS, Ve1), Ve2) & Ve2red = vreduce(Ve2) & visSomeExp(Ve2red) & RESULT = vsomeExp(vapp(vabs(Vx, VS, Ve1), vgetSomeExp(Ve2red))) ) | ? [ VS,Ve2red,Vx,Ve2,Ve1 ] : ( VExp0 = vapp(vabs(Vx, VS, Ve1), Ve2) & Ve2red = vreduce(Ve2) & ~( visSomeExp(Ve2red) ) & visValue(Ve2) & RESULT = vsomeExp(vsubst(Vx, Ve2, Ve1)) ) | ? [ Vx,VS,Ve1,Ve2red,Ve2 ] : ( VExp0 = vapp(vabs(Vx, VS, Ve1), Ve2) & Ve2red = vreduce(Ve2) & ~( visSomeExp(Ve2red) ) & ~( visValue(Ve2) ) & RESULT = vnoExp ) | ? [ Ve1,Ve1red,Ve2 ] : ( VExp0 = vapp(Ve1, Ve2) & ! [ VVx0,VVS0,VVe10 ] : ~( Ve1 = vabs(VVx0, VVS0, VVe10) ) & Ve1red = vreduce(Ve1) & visSomeExp(Ve1red) & RESULT = vsomeExp(vapp(vgetSomeExp(Ve1red), Ve2)) ) | ? [ Ve2,Ve1,Ve1red ] : ( VExp0 = vapp(Ve1, Ve2) & ! [ VVx0,VVS0,VVe10 ] : ~( Ve1 = vabs(VVx0, VVS0, VVe10) ) & Ve1red = vreduce(Ve1) & ~( visSomeExp(Ve1red) ) & RESULT = vnoExp ) ) ),
% 173.65/173.99 file('COM001+0.ax', reduce-INV) ).
% 173.65/173.99
% 173.65/173.99 fof(EQ-arrow, axiom,
% 173.65/173.99 ! [ VTyp0,VTyp1,VTyp2,VTyp3 ] : ( ( varrow(VTyp0, VTyp1) = varrow(VTyp2, VTyp3) => ( VTyp0 = VTyp2 & VTyp1 = VTyp3 ) ) & ( ( VTyp0 = VTyp2 & VTyp1 = VTyp3 ) => varrow(VTyp0, VTyp1) = varrow(VTyp2, VTyp3) ) ),
% 173.65/173.99 file('COM001+0.ax', EQ-arrow) ).
% 173.65/173.99
% 173.65/173.99 fof(T-var, axiom,
% 173.65/173.99 ! [ VC,Vx,VT ] : ( vlookup(Vx, VC) = vsomeType(VT) => vtcheck(VC, vvar(Vx), VT) ),
% 173.65/173.99 file('COM001+0.ax', T-var) ).
% 173.65/173.99
% 173.65/173.99 fof(T-abs, axiom,
% 173.65/173.99 ! [ VC,Vx,Ve,VS,VT ] : ( vtcheck(vbind(Vx, VS, VC), Ve, VT) => vtcheck(VC, vabs(Vx, VS, Ve), varrow(VS, VT)) ),
% 173.65/173.99 file('COM001+0.ax', T-abs) ).
% 173.65/173.99
% 173.65/173.99 fof(T-app, axiom,
% 173.65/173.99 ! [ VS,VC,Ve1,Ve2,VT ] : ( ( vtcheck(VC, Ve1, varrow(VS, VT)) & vtcheck(VC, Ve2, VS) ) => vtcheck(VC, vapp(Ve1, Ve2), VT) ),
% 173.65/173.99 file('COM001+0.ax', T-app) ).
% 173.65/173.99
% 173.65/173.99 fof(T-inv, axiom,
% 173.65/173.99 ! [ Ve,VT,VC ] : ( vtcheck(VC, Ve, VT) => ( ? [ Vx ] : ( Ve = vvar(Vx) & vlookup(Vx, VC) = vsomeType(VT) ) | ? [ Vx,Ve2,VT1,VT2 ] : ( Ve = vabs(Vx, VT1, Ve2) & VT = varrow(VT1, VT2) & vtcheck(vbind(Vx, VT1, VC), Ve2, VT2) ) | ? [ Ve1,Ve2,VS ] : ( Ve = vapp(Ve1, Ve2) & vtcheck(VC, Ve1, varrow(VS, VT)) & vtcheck(VC, Ve2, VS) ) ) ),
% 173.65/173.99 file('COM001+0.ax', T-inv) ).
% 173.65/173.99
% 173.65/173.99 fof(T-Weak-abs-IH, axiom,
% 173.65/173.99 ! [ Vx,VS,VC,VT ] : ( ( vlookup(Vx, VC) = vnoType & vtcheck(VC, veabs, VT) ) => vtcheck(vbind(Vx, VS, VC), veabs, VT) ),
% 173.65/173.99 file('theBenchmark.p', T-Weak-abs-IH) ).
% 173.65/173.99
% 173.65/173.99 fof(T-Weak-abs-1, axiom,
% 173.65/173.99 ! [ Vx,VS,VC,Vy,VS1,VT ] : ( ( ~( Vx = Vy ) & vlookup(Vx, VC) = vnoType & vtcheck(VC, vabs(Vy, VS1, veabs), VT) ) => vtcheck(vbind(Vx, VS, VC), vabs(Vy, VS1, veabs), VT) ),
% 173.65/173.99 file('theBenchmark.p', T-Weak-abs-1) ).
% 173.65/173.99
% 173.65/173.99 fof(T-Weak-abs-2, axiom,
% 173.65/173.99 ! [ Vx,VS,VC,Vy,VS1,VT ] : ( ( Vx = Vy & vlookup(Vx, VC) = vnoType & vtcheck(VC, vabs(Vy, VS1, veabs), VT) ) => vtcheck(vbind(Vx, VS, VC), vabs(Vy, VS1, veabs), VT) ),
% 173.65/173.99 file('theBenchmark.p', T-Weak-abs-2) ).
% 173.65/173.99
% 173.65/173.99 fof(T-Weak-abs, conjecture,
% 173.65/173.99 ! [ Vx,VS,VC,Vy,VS1,VT ] : ( ( vlookup(Vx, VC) = vnoType & vtcheck(VC, vabs(Vy, VS1, veabs), VT) ) => vtcheck(vbind(Vx, VS, VC), vabs(Vy, VS1, veabs), VT) ),
% 173.65/173.99 file('theBenchmark.p', T-Weak-abs) ).
% 173.65/173.99
% 173.65/173.99 fof(f_1_1, plain,
% 173.65/173.99 ! [ VVar0,VVar1 ] : ( ( ~( vvar(VVar0) = vvar(VVar1) ) | VVar0 = VVar1 ) & ( ~( VVar0 = VVar1 ) | vvar(VVar0) = vvar(VVar1) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[EQ-var]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_1_2, plain,
% 173.65/173.99 ! [ U_1,U_0 ] : ( ( ~( vvar(U_1) = vvar(U_0) ) | U_1 = U_0 ) & ( ~( U_1 = U_0 ) | vvar(U_1) = vvar(U_0) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_1_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_1_3, plain,
% 173.65/173.99 ( ! [ U_4,U_2 ] : ( ~( vvar(U_4) = vvar(U_2) ) | U_4 = U_2 ) & ! [ U_5,U_3 ] : ( ~( U_5 = U_3 ) | vvar(U_5) = vvar(U_3) ) ),
% 173.65/173.99 inference(miniscope,[status(thm)],[f_1_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_1_4, plain,
% 173.65/173.99 ( vvar(U_4) != vvar(U_2) | U_4 = U_2 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_1_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_1_5, plain,
% 173.65/173.99 ( U_5 != U_3 | vvar(U_5) = vvar(U_3) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_1_3]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_2_1, plain,
% 173.65/173.99 ! [ VVar0,VTyp0,VExp0,VVar1,VTyp1,VExp1 ] : ( ( ~( vabs(VVar0, VTyp0, VExp0) = vabs(VVar1, VTyp1, VExp1) ) | ( VVar0 = VVar1 & VTyp0 = VTyp1 & VExp0 = VExp1 ) ) & ( ( ~( VVar0 = VVar1 ) | ~( VTyp0 = VTyp1 ) | ~( VExp0 = VExp1 ) ) | vabs(VVar0, VTyp0, VExp0) = vabs(VVar1, VTyp1, VExp1) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[EQ-abs]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_2_2, plain,
% 173.65/173.99 ! [ U_11,U_10,U_9,U_8,U_7,U_6 ] : ( ( ~( vabs(U_11, U_10, U_9) = vabs(U_8, U_7, U_6) ) | ( U_11 = U_8 & U_10 = U_7 & U_9 = U_6 ) ) & ( ( ~( U_11 = U_8 ) | ~( U_10 = U_7 ) | ~( U_9 = U_6 ) ) | vabs(U_11, U_10, U_9) = vabs(U_8, U_7, U_6) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_2_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_2_3, plain,
% 173.65/173.99 ( ! [ U_22,U_20,U_18,U_16,U_14,U_12 ] : ( ~( vabs(U_22, U_20, U_18) = vabs(U_16, U_14, U_12) ) | ( U_22 = U_16 & U_20 = U_14 & U_18 = U_12 ) ) & ! [ U_23,U_21,U_19,U_17,U_15,U_13 ] : ( ( ~( U_23 = U_17 ) | ~( U_21 = U_15 ) | ~( U_19 = U_13 ) ) | vabs(U_23, U_21, U_19) = vabs(U_17, U_15, U_13) ) ),
% 173.65/173.99 inference(miniscope,[status(thm)],[f_2_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_2_4, plain,
% 173.65/173.99 ( vabs(U_22, U_20, U_18) != vabs(U_16, U_14, U_12) | U_22 = U_16 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_2_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_2_5, plain,
% 173.65/173.99 ( vabs(U_22, U_20, U_18) != vabs(U_16, U_14, U_12) | U_20 = U_14 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_2_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_2_6, plain,
% 173.65/173.99 ( vabs(U_22, U_20, U_18) != vabs(U_16, U_14, U_12) | U_18 = U_12 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_2_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_2_7, plain,
% 173.65/173.99 ( U_23 != U_17 | U_21 != U_15 | U_19 != U_13 | vabs(U_23, U_21, U_19) = vabs(U_17, U_15, U_13) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_2_3]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_3_1, plain,
% 173.65/173.99 ! [ VExp0,VExp1,VExp2,VExp3 ] : ( ( ~( vapp(VExp0, VExp1) = vapp(VExp2, VExp3) ) | ( VExp0 = VExp2 & VExp1 = VExp3 ) ) & ( ( ~( VExp0 = VExp2 ) | ~( VExp1 = VExp3 ) ) | vapp(VExp0, VExp1) = vapp(VExp2, VExp3) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[EQ-app]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_3_2, plain,
% 173.65/173.99 ! [ U_27,U_26,U_25,U_24 ] : ( ( ~( vapp(U_27, U_26) = vapp(U_25, U_24) ) | ( U_27 = U_25 & U_26 = U_24 ) ) & ( ( ~( U_27 = U_25 ) | ~( U_26 = U_24 ) ) | vapp(U_27, U_26) = vapp(U_25, U_24) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_3_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_3_3, plain,
% 173.65/173.99 ( ! [ U_34,U_32,U_30,U_28 ] : ( ~( vapp(U_34, U_32) = vapp(U_30, U_28) ) | ( U_34 = U_30 & U_32 = U_28 ) ) & ! [ U_35,U_33,U_31,U_29 ] : ( ( ~( U_35 = U_31 ) | ~( U_33 = U_29 ) ) | vapp(U_35, U_33) = vapp(U_31, U_29) ) ),
% 173.65/173.99 inference(miniscope,[status(thm)],[f_3_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_3_4, plain,
% 173.65/173.99 ( vapp(U_34, U_32) != vapp(U_30, U_28) | U_34 = U_30 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_3_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_3_5, plain,
% 173.65/173.99 ( vapp(U_34, U_32) != vapp(U_30, U_28) | U_32 = U_28 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_3_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_3_6, plain,
% 173.65/173.99 ( U_35 != U_31 | U_33 != U_29 | vapp(U_35, U_33) = vapp(U_31, U_29) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_3_3]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_4_1, plain,
% 173.65/173.99 ! [ VVar0,VVar1,VTyp0,VExp0 ] : ~( vvar(VVar0) = vabs(VVar1, VTyp0, VExp0) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[DIFF-var-abs]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_4_2, plain,
% 173.65/173.99 ! [ U_39,U_38,U_37,U_36 ] : ~( vvar(U_39) = vabs(U_38, U_37, U_36) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_4_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_4_3, plain,
% 173.65/173.99 ( vvar(U_39) != vabs(U_38, U_37, U_36) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_4_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_5_1, plain,
% 173.65/173.99 ! [ VVar0,VExp0,VExp1 ] : ~( vvar(VVar0) = vapp(VExp0, VExp1) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[DIFF-var-app]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_5_2, plain,
% 173.65/173.99 ! [ U_42,U_41,U_40 ] : ~( vvar(U_42) = vapp(U_41, U_40) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_5_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_5_3, plain,
% 173.65/173.99 ( vvar(U_42) != vapp(U_41, U_40) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_5_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_6_1, plain,
% 173.65/173.99 ! [ VVar0,VTyp0,VExp0,VExp1,VExp2 ] : ~( vabs(VVar0, VTyp0, VExp0) = vapp(VExp1, VExp2) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[DIFF-abs-app]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_6_2, plain,
% 173.65/173.99 ! [ U_47,U_46,U_45,U_44,U_43 ] : ~( vabs(U_47, U_46, U_45) = vapp(U_44, U_43) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_6_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_6_3, plain,
% 173.65/173.99 ( vabs(U_47, U_46, U_45) != vapp(U_44, U_43) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_6_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_7_1, plain,
% 173.65/173.99 ! [ Vx,VS,Ve,VExp0 ] : ( ~( VExp0 = vabs(Vx, VS, Ve) ) | visValue(VExp0) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isValue0]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_7_2, plain,
% 173.65/173.99 ! [ U_51,U_50,U_49,U_48 ] : ( ~( U_48 = vabs(U_51, U_50, U_49) ) | visValue(U_48) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_7_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_7_3, plain,
% 173.65/173.99 ( U_48 != vabs(U_51, U_50, U_49) | visValue(U_48) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_7_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_8_1, plain,
% 173.65/173.99 ! [ Vx,VExp0 ] : ( ~( VExp0 = vvar(Vx) ) | ~( visValue(VExp0) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isValue1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_8_2, plain,
% 173.65/173.99 ! [ U_53,U_52 ] : ( ~( U_52 = vvar(U_53) ) | ~( visValue(U_52) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_8_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_8_3, plain,
% 173.65/173.99 ( U_52 != vvar(U_53) | ~visValue(U_52) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_8_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_9_1, plain,
% 173.65/173.99 ! [ Ve1,Ve2,VExp0 ] : ( ~( VExp0 = vapp(Ve1, Ve2) ) | ~( visValue(VExp0) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isValue2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_9_2, plain,
% 173.65/173.99 ! [ U_56,U_55,U_54 ] : ( ~( U_54 = vapp(U_56, U_55) ) | ~( visValue(U_54) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_9_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_9_3, plain,
% 173.65/173.99 ( U_54 != vapp(U_56, U_55) | ~visValue(U_54) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_9_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_10_1, plain,
% 173.65/173.99 ! [ VVar0,VExp0,Vx,Vv ] : ( ( ~( VVar0 = Vv ) | ~( VExp0 = vvar(Vx) ) ) | ( ( ~( Vx = Vv ) | visFreeVar(VVar0, VExp0) ) & ( ~( visFreeVar(VVar0, VExp0) ) | Vx = Vv ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isFreeVar0]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_10_2, plain,
% 173.65/173.99 ! [ U_60,U_59,U_58,U_57 ] : ( ( ~( U_60 = U_57 ) | ~( U_59 = vvar(U_58) ) ) | ( ( ~( U_58 = U_57 ) | visFreeVar(U_60, U_59) ) & ( ~( visFreeVar(U_60, U_59) ) | U_58 = U_57 ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_10_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_10_3, plain,
% 173.65/173.99 ( U_60 != U_57 | U_59 != vvar(U_58) | U_58 != U_57 | visFreeVar(U_60, U_59) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_10_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_10_4, plain,
% 173.65/173.99 ( U_60 != U_57 | U_59 != vvar(U_58) | ~visFreeVar(U_60, U_59) | U_58 = U_57 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_10_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_11_1, plain,
% 173.65/173.99 ! [ VT,VVar0,VExp0,Vx,Vv,Ve ] : ( ( ~( VVar0 = Vv ) | ~( VExp0 = vabs(Vx, VT, Ve) ) ) | ( ( ( Vx = Vv | ~( visFreeVar(Vv, Ve) ) ) | visFreeVar(VVar0, VExp0) ) & ( ~( visFreeVar(VVar0, VExp0) ) | ( ~( Vx = Vv ) & visFreeVar(Vv, Ve) ) ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isFreeVar1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_11_2, plain,
% 173.65/173.99 ! [ U_66,U_65,U_64,U_63,U_62,U_61 ] : ( ( ~( U_65 = U_62 ) | ~( U_64 = vabs(U_63, U_66, U_61) ) ) | ( ( ( U_63 = U_62 | ~( visFreeVar(U_62, U_61) ) ) | visFreeVar(U_65, U_64) ) & ( ~( visFreeVar(U_65, U_64) ) | ( ~( U_63 = U_62 ) & visFreeVar(U_62, U_61) ) ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_11_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_11_3, plain,
% 173.65/173.99 ( U_65 != U_62 | U_64 != vabs(U_63, U_66, U_61) | U_63 = U_62 | ~visFreeVar(U_62, U_61) | visFreeVar(U_65, U_64) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_11_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_11_4, plain,
% 173.65/173.99 ( U_65 != U_62 | U_64 != vabs(U_63, U_66, U_61) | ~visFreeVar(U_65, U_64) | U_63 != U_62 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_11_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_11_5, plain,
% 173.65/173.99 ( U_65 != U_62 | U_64 != vabs(U_63, U_66, U_61) | ~visFreeVar(U_65, U_64) | visFreeVar(U_62, U_61) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_11_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_12_1, plain,
% 173.65/173.99 ! [ VVar0,VExp0,Ve1,Vv,Ve2 ] : ( ( ~( VVar0 = Vv ) | ~( VExp0 = vapp(Ve1, Ve2) ) ) | ( ( ( ~( visFreeVar(Vv, Ve1) ) & ~( visFreeVar(Vv, Ve2) ) ) | visFreeVar(VVar0, VExp0) ) & ( ~( visFreeVar(VVar0, VExp0) ) | ( visFreeVar(Vv, Ve1) | visFreeVar(Vv, Ve2) ) ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isFreeVar2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_12_2, plain,
% 173.65/173.99 ! [ U_71,U_70,U_69,U_68,U_67 ] : ( ( ~( U_71 = U_68 ) | ~( U_70 = vapp(U_69, U_67) ) ) | ( ( ( ~( visFreeVar(U_68, U_69) ) & ~( visFreeVar(U_68, U_67) ) ) | visFreeVar(U_71, U_70) ) & ( ~( visFreeVar(U_71, U_70) ) | ( visFreeVar(U_68, U_69) | visFreeVar(U_68, U_67) ) ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_12_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_12_3, plain,
% 173.65/173.99 ( U_71 != U_68 | U_70 != vapp(U_69, U_67) | visFreeVar(U_71, U_70) | ~visFreeVar(U_68, U_69) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_12_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_12_4, plain,
% 173.65/173.99 ( U_71 != U_68 | U_70 != vapp(U_69, U_67) | visFreeVar(U_71, U_70) | ~visFreeVar(U_68, U_67) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_12_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_12_5, plain,
% 173.65/173.99 ( U_71 != U_68 | U_70 != vapp(U_69, U_67) | ~visFreeVar(U_71, U_70) | visFreeVar(U_68, U_69) | visFreeVar(U_68, U_67) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_12_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_13_1, plain,
% 173.65/173.99 ( ( ~( vempty = vempty ) | $true ) & ( ~( $true ) | vempty = vempty ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[EQ-empty]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_13_2, plain,
% 173.65/173.99 ( vempty != vempty | $true ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_13_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_13_3, plain,
% 173.65/173.99 ( ~$true | vempty = vempty ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_13_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_14_1, plain,
% 173.65/173.99 ! [ VVar0,VTyp0,VCtx0,VVar1,VTyp1,VCtx1 ] : ( ( ~( vbind(VVar0, VTyp0, VCtx0) = vbind(VVar1, VTyp1, VCtx1) ) | ( VVar0 = VVar1 & VTyp0 = VTyp1 & VCtx0 = VCtx1 ) ) & ( ( ~( VVar0 = VVar1 ) | ~( VTyp0 = VTyp1 ) | ~( VCtx0 = VCtx1 ) ) | vbind(VVar0, VTyp0, VCtx0) = vbind(VVar1, VTyp1, VCtx1) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[EQ-bind]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_14_2, plain,
% 173.65/173.99 ! [ U_77,U_76,U_75,U_74,U_73,U_72 ] : ( ( ~( vbind(U_77, U_76, U_75) = vbind(U_74, U_73, U_72) ) | ( U_77 = U_74 & U_76 = U_73 & U_75 = U_72 ) ) & ( ( ~( U_77 = U_74 ) | ~( U_76 = U_73 ) | ~( U_75 = U_72 ) ) | vbind(U_77, U_76, U_75) = vbind(U_74, U_73, U_72) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_14_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_14_3, plain,
% 173.65/173.99 ( ! [ U_88,U_86,U_84,U_82,U_80,U_78 ] : ( ~( vbind(U_88, U_86, U_84) = vbind(U_82, U_80, U_78) ) | ( U_88 = U_82 & U_86 = U_80 & U_84 = U_78 ) ) & ! [ U_89,U_87,U_85,U_83,U_81,U_79 ] : ( ( ~( U_89 = U_83 ) | ~( U_87 = U_81 ) | ~( U_85 = U_79 ) ) | vbind(U_89, U_87, U_85) = vbind(U_83, U_81, U_79) ) ),
% 173.65/173.99 inference(miniscope,[status(thm)],[f_14_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_14_4, plain,
% 173.65/173.99 ( vbind(U_88, U_86, U_84) != vbind(U_82, U_80, U_78) | U_88 = U_82 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_14_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_14_5, plain,
% 173.65/173.99 ( vbind(U_88, U_86, U_84) != vbind(U_82, U_80, U_78) | U_86 = U_80 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_14_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_14_6, plain,
% 173.65/173.99 ( vbind(U_88, U_86, U_84) != vbind(U_82, U_80, U_78) | U_84 = U_78 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_14_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_14_7, plain,
% 173.65/173.99 ( U_89 != U_83 | U_87 != U_81 | U_85 != U_79 | vbind(U_89, U_87, U_85) = vbind(U_83, U_81, U_79) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_14_3]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_15_1, plain,
% 173.65/173.99 ( ( ~( vnoType = vnoType ) | $true ) & ( ~( $true ) | vnoType = vnoType ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[EQ-noType]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_15_2, plain,
% 173.65/173.99 ( vnoType != vnoType | $true ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_15_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_15_3, plain,
% 173.65/173.99 ( ~$true | vnoType = vnoType ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_15_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_16_1, plain,
% 173.65/173.99 ! [ VTyp0,VTyp1 ] : ( ( ~( vsomeType(VTyp0) = vsomeType(VTyp1) ) | VTyp0 = VTyp1 ) & ( ~( VTyp0 = VTyp1 ) | vsomeType(VTyp0) = vsomeType(VTyp1) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[EQ-someType]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_16_2, plain,
% 173.65/173.99 ! [ U_91,U_90 ] : ( ( ~( vsomeType(U_91) = vsomeType(U_90) ) | U_91 = U_90 ) & ( ~( U_91 = U_90 ) | vsomeType(U_91) = vsomeType(U_90) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_16_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_16_3, plain,
% 173.65/173.99 ( ! [ U_94,U_92 ] : ( ~( vsomeType(U_94) = vsomeType(U_92) ) | U_94 = U_92 ) & ! [ U_95,U_93 ] : ( ~( U_95 = U_93 ) | vsomeType(U_95) = vsomeType(U_93) ) ),
% 173.65/173.99 inference(miniscope,[status(thm)],[f_16_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_16_4, plain,
% 173.65/173.99 ( vsomeType(U_94) != vsomeType(U_92) | U_94 = U_92 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_16_3]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_16_5, plain,
% 173.65/173.99 ( U_95 != U_93 | vsomeType(U_95) = vsomeType(U_93) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_16_3]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_17_1, plain,
% 173.65/173.99 ! [ VVar0,VTyp0,VCtx0 ] : ~( vempty = vbind(VVar0, VTyp0, VCtx0) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[DIFF-empty-bind]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_17_2, plain,
% 173.65/173.99 ! [ U_98,U_97,U_96 ] : ~( vempty = vbind(U_98, U_97, U_96) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_17_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_17_3, plain,
% 173.65/173.99 ( vempty != vbind(U_98, U_97, U_96) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_17_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_18_1, plain,
% 173.65/173.99 ! [ VTyp0 ] : ~( vnoType = vsomeType(VTyp0) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[DIFF-noType-someType]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_18_2, plain,
% 173.65/173.99 ! [ U_99 ] : ~( vnoType = vsomeType(U_99) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_18_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_18_3, plain,
% 173.65/173.99 ( vnoType != vsomeType(U_99) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_18_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_19_1, plain,
% 173.65/173.99 ! [ VOptTyp0 ] : ( ~( VOptTyp0 = vnoType ) | ~( visSomeType(VOptTyp0) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isSomeType0]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_19_2, plain,
% 173.65/173.99 ! [ U_100 ] : ( ~( U_100 = vnoType ) | ~( visSomeType(U_100) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_19_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_19_3, plain,
% 173.65/173.99 ( U_100 != vnoType | ~visSomeType(U_100) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_19_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_20_1, plain,
% 173.65/173.99 ! [ Ve,VOptTyp0 ] : ( ~( VOptTyp0 = vsomeType(Ve) ) | visSomeType(VOptTyp0) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[isSomeType1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_20_2, plain,
% 173.65/173.99 ! [ U_102,U_101 ] : ( ~( U_101 = vsomeType(U_102) ) | visSomeType(U_101) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_20_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_20_3, plain,
% 173.65/173.99 ( U_101 != vsomeType(U_102) | visSomeType(U_101) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_20_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_21_1, plain,
% 173.65/173.99 ! [ VOptTyp0,RESULT,Ve ] : ( ~( VOptTyp0 = vsomeType(Ve) ) | ( ~( RESULT = vgetSomeType(VOptTyp0) ) | RESULT = Ve ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[getSomeType0]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_21_2, plain,
% 173.65/173.99 ! [ U_105,U_104,U_103 ] : ( ~( U_105 = vsomeType(U_103) ) | ( ~( U_104 = vgetSomeType(U_105) ) | U_104 = U_103 ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_21_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_21_3, plain,
% 173.65/173.99 ( U_105 != vsomeType(U_103) | U_104 != vgetSomeType(U_105) | U_104 = U_103 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_21_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_22_1, plain,
% 173.65/173.99 ! [ Vx,VVar0,VCtx0,RESULT ] : ( ( ~( VVar0 = Vx ) | ~( VCtx0 = vempty ) ) | ( ~( RESULT = vlookup(VVar0, VCtx0) ) | RESULT = vnoType ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[lookup0]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_22_2, plain,
% 173.65/173.99 ! [ U_109,U_108,U_107,U_106 ] : ( ( ~( U_108 = U_109 ) | ~( U_107 = vempty ) ) | ( ~( U_106 = vlookup(U_108, U_107) ) | U_106 = vnoType ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_22_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_22_3, plain,
% 173.65/173.99 ! [ U_109,U_108,U_107 ] : ( ( ~( U_108 = U_109 ) | ~( U_107 = vempty ) ) | ! [ U_106 ] : ( ~( U_106 = vlookup(U_108, U_107) ) | U_106 = vnoType ) ),
% 173.65/173.99 inference(miniscope,[status(thm)],[f_22_2]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_22_4, plain,
% 173.65/173.99 ( U_108 != U_109 | U_107 != vempty | U_106 != vlookup(U_108, U_107) | U_106 = vnoType ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_22_3]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_23_1, plain,
% 173.65/173.99 ! [ VC,Vx,Vy,VVar0,VCtx0,RESULT,VTy ] : ( ( ~( VVar0 = Vx ) | ~( VCtx0 = vbind(Vy, VTy, VC) ) ) | ( ~( Vx = Vy ) | ( ~( RESULT = vlookup(VVar0, VCtx0) ) | RESULT = vsomeType(VTy) ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[lookup1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_23_2, plain,
% 173.65/173.99 ! [ U_116,U_115,U_114,U_113,U_112,U_111,U_110 ] : ( ( ~( U_113 = U_115 ) | ~( U_112 = vbind(U_114, U_110, U_116) ) ) | ( ~( U_115 = U_114 ) | ( ~( U_111 = vlookup(U_113, U_112) ) | U_111 = vsomeType(U_110) ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_23_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_23_3, plain,
% 173.65/173.99 ( U_113 != U_115 | U_112 != vbind(U_114, U_110, U_116) | U_115 != U_114 | U_111 != vlookup(U_113, U_112) | U_111 = vsomeType(U_110) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_23_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_24_1, plain,
% 173.65/173.99 ! [ VTy,Vy,VVar0,VCtx0,RESULT,Vx,VC ] : ( ( ~( VVar0 = Vx ) | ~( VCtx0 = vbind(Vy, VTy, VC) ) ) | ( Vx = Vy | ( ~( RESULT = vlookup(VVar0, VCtx0) ) | RESULT = vlookup(Vx, VC) ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[lookup2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_24_2, plain,
% 173.65/173.99 ! [ U_123,U_122,U_121,U_120,U_119,U_118,U_117 ] : ( ( ~( U_121 = U_118 ) | ~( U_120 = vbind(U_122, U_123, U_117) ) ) | ( U_118 = U_122 | ( ~( U_119 = vlookup(U_121, U_120) ) | U_119 = vlookup(U_118, U_117) ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_24_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_24_3, plain,
% 173.65/173.99 ( U_121 != U_118 | U_120 != vbind(U_122, U_123, U_117) | U_118 = U_122 | U_119 != vlookup(U_121, U_120) | U_119 = vlookup(U_118, U_117) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_24_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_1, plain,
% 173.65/173.99 ! [ VVar0,VCtx0,RESULT ] : ( ~( vlookup(VVar0, VCtx0) = RESULT ) | ( ? [ Vx ] : ( VVar0 = Vx & VCtx0 = vempty & RESULT = vnoType ) | ? [ VC,Vx,Vy,VTy ] : ( VVar0 = Vx & VCtx0 = vbind(Vy, VTy, VC) & Vx = Vy & RESULT = vsomeType(VTy) ) | ? [ VTy,Vy,Vx,VC ] : ( VVar0 = Vx & VCtx0 = vbind(Vy, VTy, VC) & ~( Vx = Vy ) & RESULT = vlookup(Vx, VC) ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[lookup-INV]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_2, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ? [ U_124 ] : ( U_135 = U_124 & U_134 = vempty & U_133 = vnoType ) | ? [ U_128,U_127,U_126,U_125 ] : ( U_135 = U_127 & U_134 = vbind(U_126, U_125, U_128) & U_127 = U_126 & U_133 = vsomeType(U_125) ) | ? [ U_132,U_131,U_130,U_129 ] : ( U_135 = U_130 & U_134 = vbind(U_131, U_132, U_129) & ~( U_130 = U_131 ) & U_133 = vlookup(U_130, U_129) ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_25_1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_3, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & ? [ U_124 ] : U_135 = U_124 ) | ? [ U_128,U_127 ] : ( U_135 = U_127 & ? [ U_126 ] : ( U_127 = U_126 & ? [ U_125 ] : ( U_134 = vbind(U_126, U_125, U_128) & U_133 = vsomeType(U_125) ) ) ) | ? [ U_132,U_131,U_130 ] : ( U_135 = U_130 & ~( U_130 = U_131 ) & ? [ U_129 ] : ( U_134 = vbind(U_131, U_132, U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(miniscope,[status(thm)],[f_25_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_4, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ? [ U_128,U_127 ] : ( U_135 = U_127 & ? [ U_126 ] : ( U_127 = U_126 & ? [ U_125 ] : ( U_134 = vbind(U_126, U_125, U_128) & U_133 = vsomeType(U_125) ) ) ) | ? [ U_132,U_131,U_130 ] : ( U_135 = U_130 & ~( U_130 = U_131 ) & ? [ U_129 ] : ( U_134 = vbind(U_131, U_132, U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_124,sK1(U_135, U_134, U_133))],[f_25_3]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_5, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ? [ U_127 ] : ( U_135 = U_127 & ? [ U_126 ] : ( U_127 = U_126 & ? [ U_125 ] : ( U_134 = vbind(U_126, U_125, sK2(U_135, U_134, U_133)) & U_133 = vsomeType(U_125) ) ) ) | ? [ U_132,U_131,U_130 ] : ( U_135 = U_130 & ~( U_130 = U_131 ) & ? [ U_129 ] : ( U_134 = vbind(U_131, U_132, U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_128,sK2(U_135, U_134, U_133))],[f_25_4]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_6, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ( U_135 = sK3(U_135, U_134, U_133) & ? [ U_126 ] : ( sK3(U_135, U_134, U_133) = U_126 & ? [ U_125 ] : ( U_134 = vbind(U_126, U_125, sK2(U_135, U_134, U_133)) & U_133 = vsomeType(U_125) ) ) ) | ? [ U_132,U_131,U_130 ] : ( U_135 = U_130 & ~( U_130 = U_131 ) & ? [ U_129 ] : ( U_134 = vbind(U_131, U_132, U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_127,sK3(U_135, U_134, U_133))],[f_25_5]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_7, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ( U_135 = sK3(U_135, U_134, U_133) & ( sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) & ? [ U_125 ] : ( U_134 = vbind(sK4(U_135, U_134, U_133), U_125, sK2(U_135, U_134, U_133)) & U_133 = vsomeType(U_125) ) ) ) | ? [ U_132,U_131,U_130 ] : ( U_135 = U_130 & ~( U_130 = U_131 ) & ? [ U_129 ] : ( U_134 = vbind(U_131, U_132, U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_126,sK4(U_135, U_134, U_133))],[f_25_6]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_8, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ( U_135 = sK3(U_135, U_134, U_133) & ( sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) & ( U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) & U_133 = vsomeType(sK5(U_135, U_134, U_133)) ) ) ) | ? [ U_132,U_131,U_130 ] : ( U_135 = U_130 & ~( U_130 = U_131 ) & ? [ U_129 ] : ( U_134 = vbind(U_131, U_132, U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_125,sK5(U_135, U_134, U_133))],[f_25_7]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_9, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ( U_135 = sK3(U_135, U_134, U_133) & ( sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) & ( U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) & U_133 = vsomeType(sK5(U_135, U_134, U_133)) ) ) ) | ? [ U_131,U_130 ] : ( U_135 = U_130 & ~( U_130 = U_131 ) & ? [ U_129 ] : ( U_134 = vbind(U_131, sK6(U_135, U_134, U_133), U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_132,sK6(U_135, U_134, U_133))],[f_25_8]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_10, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ( U_135 = sK3(U_135, U_134, U_133) & ( sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) & ( U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) & U_133 = vsomeType(sK5(U_135, U_134, U_133)) ) ) ) | ? [ U_130 ] : ( U_135 = U_130 & ~( U_130 = sK7(U_135, U_134, U_133) ) & ? [ U_129 ] : ( U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), U_129) & U_133 = vlookup(U_130, U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_131,sK7(U_135, U_134, U_133))],[f_25_9]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_11, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ( U_135 = sK3(U_135, U_134, U_133) & ( sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) & ( U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) & U_133 = vsomeType(sK5(U_135, U_134, U_133)) ) ) ) | ( U_135 = sK8(U_135, U_134, U_133) & ~( sK8(U_135, U_134, U_133) = sK7(U_135, U_134, U_133) ) & ? [ U_129 ] : ( U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), U_129) & U_133 = vlookup(sK8(U_135, U_134, U_133), U_129) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_130,sK8(U_135, U_134, U_133))],[f_25_10]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_25_12, plain,
% 173.65/173.99 ! [ U_135,U_134,U_133 ] : ( ~( vlookup(U_135, U_134) = U_133 ) | ( ( U_134 = vempty & U_133 = vnoType & U_135 = sK1(U_135, U_134, U_133) ) | ( U_135 = sK3(U_135, U_134, U_133) & ( sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) & ( U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) & U_133 = vsomeType(sK5(U_135, U_134, U_133)) ) ) ) | ( U_135 = sK8(U_135, U_134, U_133) & ~( sK8(U_135, U_134, U_133) = sK7(U_135, U_134, U_133) ) & ( U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) & U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) ) ) ) ),
% 173.65/173.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_129,sK9(U_135, U_134, U_133))],[f_25_11]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_13, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_134 = vempty | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_14, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_134 = vempty | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_15, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_134 = vempty | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_16, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_134 = vempty | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_17, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_133 = vnoType | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_18, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_133 = vnoType | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_19, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_133 = vnoType | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_20, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_133 = vnoType | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_21, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_22, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_23, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_24, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_135 = sK8(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_25, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_134 = vempty | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_26, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_134 = vempty | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_27, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_134 = vempty | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_28, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_134 = vempty | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_29, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_133 = vnoType | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_30, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_133 = vnoType | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_31, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_133 = vnoType | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_32, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_133 = vnoType | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_33, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_34, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_35, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_36, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | sK8(U_135, U_134, U_133) != sK7(U_135, U_134, U_133) | U_135 = sK1(U_135, U_134, U_133) | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_37, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_38, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_39, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_40, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_41, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_42, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_43, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_44, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_134 = vempty | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_45, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_46, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_47, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_48, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_49, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_50, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_51, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_52, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_133 = vnoType | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_53, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_54, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_55, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_56, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_134 = vbind(sK7(U_135, U_134, U_133), sK6(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_57, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | U_135 = sK3(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_58, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | sK3(U_135, U_134, U_133) = sK4(U_135, U_134, U_133) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_59, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | U_134 = vbind(sK4(U_135, U_134, U_133), sK5(U_135, U_134, U_133), sK2(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_25_60, plain,
% 173.65/173.99 ( vlookup(U_135, U_134) != U_133 | U_133 = vlookup(sK8(U_135, U_134, U_133), sK9(U_135, U_134, U_133)) | U_135 = sK1(U_135, U_134, U_133) | U_133 = vsomeType(sK5(U_135, U_134, U_133)) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_25_12]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_26_1, plain,
% 173.65/173.99 ! [ Vy,VTy,Vx,VTx,VC,Ve,VT ] : ( ( ~( Vx = Vy ) | ~( vtcheck(vbind(Vx, VTx, vbind(Vy, VTy, VC)), Ve, VT) ) ) | vtcheck(vbind(Vx, VTx, VC), Ve, VT) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[T-Context-Duplicate]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_26_2, plain,
% 173.65/173.99 ! [ U_142,U_141,U_140,U_139,U_138,U_137,U_136 ] : ( ( ~( U_140 = U_142 ) | ~( vtcheck(vbind(U_140, U_139, vbind(U_142, U_141, U_138)), U_137, U_136) ) ) | vtcheck(vbind(U_140, U_139, U_138), U_137, U_136) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_26_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_26_3, plain,
% 173.65/173.99 ( U_140 != U_142 | ~vtcheck(vbind(U_140, U_139, vbind(U_142, U_141, U_138)), U_137, U_136) | vtcheck(vbind(U_140, U_139, U_138), U_137, U_136) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_26_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_27_1, plain,
% 173.65/173.99 ! [ Vy,VTy,Vx,VTx,VC,Ve,VT ] : ( ( Vx = Vy | ~( vtcheck(vbind(Vx, VTx, vbind(Vy, VTy, VC)), Ve, VT) ) ) | vtcheck(vbind(Vy, VTy, vbind(Vx, VTx, VC)), Ve, VT) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[T-Context-Swap]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_27_2, plain,
% 173.65/173.99 ! [ U_149,U_148,U_147,U_146,U_145,U_144,U_143 ] : ( ( U_147 = U_149 | ~( vtcheck(vbind(U_147, U_146, vbind(U_149, U_148, U_145)), U_144, U_143) ) ) | vtcheck(vbind(U_149, U_148, vbind(U_147, U_146, U_145)), U_144, U_143) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_27_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_27_3, plain,
% 173.65/173.99 ( U_147 = U_149 | ~vtcheck(vbind(U_147, U_146, vbind(U_149, U_148, U_145)), U_144, U_143) | vtcheck(vbind(U_149, U_148, vbind(U_147, U_146, U_145)), U_144, U_143) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_27_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_28_1, plain,
% 173.65/173.99 ! [ Vv,Ve ] : ( ~( vgensym(Ve) = Vv ) | ~( visFreeVar(Vv, Ve) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[gensym-is-fresh]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_28_2, plain,
% 173.65/173.99 ! [ U_151,U_150 ] : ( ~( vgensym(U_150) = U_151 ) | ~( visFreeVar(U_151, U_150) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_28_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_28_3, plain,
% 173.65/173.99 ( vgensym(U_150) != U_151 | ~visFreeVar(U_151, U_150) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_28_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_29_1, plain,
% 173.65/173.99 ! [ Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve ] : ( ( ~( VVar0 = Vx ) | ~( VExp0 = Ve ) | ~( VExp1 = vvar(Vy) ) ) | ( ~( Vx = Vy ) | ( ~( RESULT = vsubst(VVar0, VExp0, VExp1) ) | RESULT = Ve ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[subst0]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_29_2, plain,
% 173.65/173.99 ! [ U_158,U_157,U_156,U_155,U_154,U_153,U_152 ] : ( ( ~( U_156 = U_158 ) | ~( U_155 = U_152 ) | ~( U_154 = vvar(U_157) ) ) | ( ~( U_158 = U_157 ) | ( ~( U_153 = vsubst(U_156, U_155, U_154) ) | U_153 = U_152 ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_29_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_29_3, plain,
% 173.65/173.99 ( U_156 != U_158 | U_155 != U_152 | U_154 != vvar(U_157) | U_158 != U_157 | U_153 != vsubst(U_156, U_155, U_154) | U_153 = U_152 ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_29_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_30_1, plain,
% 173.65/173.99 ! [ Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy ] : ( ( ~( VVar0 = Vx ) | ~( VExp0 = Ve ) | ~( VExp1 = vvar(Vy) ) ) | ( Vx = Vy | ( ~( RESULT = vsubst(VVar0, VExp0, VExp1) ) | RESULT = vvar(Vy) ) ) ),
% 173.65/173.99 inference(fof_nnf,[status(thm)],[subst1]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_30_2, plain,
% 173.65/173.99 ! [ U_165,U_164,U_163,U_162,U_161,U_160,U_159 ] : ( ( ~( U_163 = U_164 ) | ~( U_162 = U_165 ) | ~( U_161 = vvar(U_159) ) ) | ( U_164 = U_159 | ( ~( U_160 = vsubst(U_163, U_162, U_161) ) | U_160 = vvar(U_159) ) ) ),
% 173.65/173.99 inference(variable_rename,[status(thm)],[f_30_1]) ).
% 173.65/173.99
% 173.65/173.99 cnf(f_30_3, plain,
% 173.65/173.99 ( U_163 != U_164 | U_162 != U_165 | U_161 != vvar(U_159) | U_164 = U_159 | U_160 != vsubst(U_163, U_162, U_161) | U_160 = vvar(U_159) ),
% 173.65/173.99 inference(clausify,[status(thm)],[f_30_2]) ).
% 173.65/173.99
% 173.65/173.99 fof(f_31_1, plain,
% 173.65/173.99 ! [ VVar0,VExp0,VExp1,RESULT,Ve1,Vx,Ve,Ve2 ] : ( ( ~( VVar0 = Vx ) | ~( VExp0 = Ve ) | ~( VExp1 = vapp(Ve1, Ve2) ) ) | ( ~( RESULT = vsubst(VVar0, VExp0, VExp1) ) | RESULT = vapp(vsubst(Vx, Ve, Ve1), vsubst(Vx, Ve, Ve2)) ) ),
% 173.65/174.00 inference(fof_nnf,[status(thm)],[subst2]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_31_2, plain,
% 173.65/174.00 ! [ U_173,U_172,U_171,U_170,U_169,U_168,U_167,U_166 ] : ( ( ~( U_173 = U_168 ) | ~( U_172 = U_167 ) | ~( U_171 = vapp(U_169, U_166) ) ) | ( ~( U_170 = vsubst(U_173, U_172, U_171) ) | U_170 = vapp(vsubst(U_168, U_167, U_169), vsubst(U_168, U_167, U_166)) ) ),
% 173.65/174.00 inference(variable_rename,[status(thm)],[f_31_1]) ).
% 173.65/174.00
% 173.65/174.00 cnf(f_31_3, plain,
% 173.65/174.00 ( U_173 != U_168 | U_172 != U_167 | U_171 != vapp(U_169, U_166) | U_170 != vsubst(U_173, U_172, U_171) | U_170 = vapp(vsubst(U_168, U_167, U_169), vsubst(U_168, U_167, U_166)) ),
% 173.65/174.00 inference(clausify,[status(thm)],[f_31_2]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_32_1, plain,
% 173.65/174.00 ! [ Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1 ] : ( ( ~( VVar0 = Vx ) | ~( VExp0 = Ve ) | ~( VExp1 = vabs(Vy, VT, Ve1) ) ) | ( ~( Vx = Vy ) | ( ~( RESULT = vsubst(VVar0, VExp0, VExp1) ) | RESULT = vabs(Vy, VT, Ve1) ) ) ),
% 173.65/174.00 inference(fof_nnf,[status(thm)],[subst3]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_32_2, plain,
% 173.65/174.00 ! [ U_182,U_181,U_180,U_179,U_178,U_177,U_176,U_175,U_174 ] : ( ( ~( U_180 = U_181 ) | ~( U_179 = U_182 ) | ~( U_178 = vabs(U_176, U_175, U_174) ) ) | ( ~( U_181 = U_176 ) | ( ~( U_177 = vsubst(U_180, U_179, U_178) ) | U_177 = vabs(U_176, U_175, U_174) ) ) ),
% 173.65/174.00 inference(variable_rename,[status(thm)],[f_32_1]) ).
% 173.65/174.00
% 173.65/174.00 cnf(f_32_3, plain,
% 173.65/174.00 ( U_180 != U_181 | U_179 != U_182 | U_178 != vabs(U_176, U_175, U_174) | U_181 != U_176 | U_177 != vsubst(U_180, U_179, U_178) | U_177 = vabs(U_176, U_175, U_174) ),
% 173.65/174.00 inference(clausify,[status(thm)],[f_32_2]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_33_1, plain,
% 173.65/174.00 ! [ VVar0,VExp0,VExp1,RESULT,Vx,Ve,VT,Vy,Vfresh,Ve1 ] : ( ( ~( VVar0 = Vx ) | ~( VExp0 = Ve ) | ~( VExp1 = vabs(Vy, VT, Ve1) ) ) | ( ( Vx = Vy | ~( visFreeVar(Vy, Ve) ) | ~( Vfresh = vgensym(vapp(vapp(Ve, Ve1), vvar(Vx))) ) ) | ( ~( RESULT = vsubst(VVar0, VExp0, VExp1) ) | RESULT = vsubst(Vx, Ve, vabs(Vfresh, VT, vsubst(Vy, vvar(Vfresh), Ve1))) ) ) ),
% 173.65/174.00 inference(fof_nnf,[status(thm)],[subst4]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_33_2, plain,
% 173.65/174.00 ! [ U_192,U_191,U_190,U_189,U_188,U_187,U_186,U_185,U_184,U_183 ] : ( ( ~( U_192 = U_188 ) | ~( U_191 = U_187 ) | ~( U_190 = vabs(U_185, U_186, U_183) ) ) | ( ( U_188 = U_185 | ~( visFreeVar(U_185, U_187) ) | ~( U_184 = vgensym(vapp(vapp(U_187, U_183), vvar(U_188))) ) ) | ( ~( U_189 = vsubst(U_192, U_191, U_190) ) | U_189 = vsubst(U_188, U_187, vabs(U_184, U_186, vsubst(U_185, vvar(U_184), U_183))) ) ) ),
% 173.65/174.00 inference(variable_rename,[status(thm)],[f_33_1]) ).
% 173.65/174.00
% 173.65/174.00 cnf(f_33_3, plain,
% 173.65/174.00 ( U_192 != U_188 | U_191 != U_187 | U_190 != vabs(U_185, U_186, U_183) | U_188 = U_185 | ~visFreeVar(U_185, U_187) | U_184 != vgensym(vapp(vapp(U_187, U_183), vvar(U_188))) | U_189 != vsubst(U_192, U_191, U_190) | U_189 = vsubst(U_188, U_187, vabs(U_184, U_186, vsubst(U_185, vvar(U_184), U_183))) ),
% 173.65/174.00 inference(clausify,[status(thm)],[f_33_2]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_34_1, plain,
% 173.65/174.00 ! [ VVar0,VExp0,VExp1,RESULT,Vy,VT,Vx,Ve,Ve1 ] : ( ( ~( VVar0 = Vx ) | ~( VExp0 = Ve ) | ~( VExp1 = vabs(Vy, VT, Ve1) ) ) | ( ( Vx = Vy | visFreeVar(Vy, Ve) ) | ( ~( RESULT = vsubst(VVar0, VExp0, VExp1) ) | RESULT = vabs(Vy, VT, vsubst(Vx, Ve, Ve1)) ) ) ),
% 173.65/174.00 inference(fof_nnf,[status(thm)],[subst5]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_34_2, plain,
% 173.65/174.00 ! [ U_201,U_200,U_199,U_198,U_197,U_196,U_195,U_194,U_193 ] : ( ( ~( U_201 = U_195 ) | ~( U_200 = U_194 ) | ~( U_199 = vabs(U_197, U_196, U_193) ) ) | ( ( U_195 = U_197 | visFreeVar(U_197, U_194) ) | ( ~( U_198 = vsubst(U_201, U_200, U_199) ) | U_198 = vabs(U_197, U_196, vsubst(U_195, U_194, U_193)) ) ) ),
% 173.65/174.00 inference(variable_rename,[status(thm)],[f_34_1]) ).
% 173.65/174.00
% 173.65/174.00 cnf(f_34_3, plain,
% 173.65/174.00 ( U_201 != U_195 | U_200 != U_194 | U_199 != vabs(U_197, U_196, U_193) | U_195 = U_197 | visFreeVar(U_197, U_194) | U_198 != vsubst(U_201, U_200, U_199) | U_198 = vabs(U_197, U_196, vsubst(U_195, U_194, U_193)) ),
% 173.65/174.00 inference(clausify,[status(thm)],[f_34_2]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_1, plain,
% 173.65/174.00 ! [ VVar0,VExp0,VExp1,RESULT ] : ( ~( vsubst(VVar0, VExp0, VExp1) = RESULT ) | ( ? [ Vx,Vy,Ve ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy) & Vx = Vy & RESULT = Ve ) | ? [ Ve,Vx,Vy ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy) & ~( Vx = Vy ) & RESULT = vvar(Vy) ) | ? [ Ve1,Vx,Ve,Ve2 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vapp(Ve1, Ve2) & RESULT = vapp(vsubst(Vx, Ve, Ve1), vsubst(Vx, Ve, Ve2)) ) | ? [ Ve,Vx,Vy,VT,Ve1 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) & Vx = Vy & RESULT = vabs(Vy, VT, Ve1) ) | ? [ Vx,Ve,VT,Vy,Vfresh,Ve1 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) & ~( Vx = Vy ) & visFreeVar(Vy, Ve) & Vfresh = vgensym(vapp(vapp(Ve, Ve1), vvar(Vx))) & RESULT = vsubst(Vx, Ve, vabs(Vfresh, VT, vsubst(Vy, vvar(Vfresh), Ve1))) ) | ? [ Vy,VT,Vx,Ve,Ve1 ] : ( VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy, VT, Ve1) & ~( Vx = Vy ) & ~( visFreeVar(Vy, Ve) ) & RESULT = vabs(Vy, VT, vsubst(Vx, Ve, Ve1)) ) ) ),
% 173.65/174.00 inference(fof_nnf,[status(thm)],[subst-INV]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_2, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ? [ U_204,U_203,U_202 ] : ( U_231 = U_204 & U_230 = U_202 & U_229 = vvar(U_203) & U_204 = U_203 & U_228 = U_202 ) | ? [ U_207,U_206,U_205 ] : ( U_231 = U_206 & U_230 = U_207 & U_229 = vvar(U_205) & ~( U_206 = U_205 ) & U_228 = vvar(U_205) ) | ? [ U_211,U_210,U_209,U_208 ] : ( U_231 = U_210 & U_230 = U_209 & U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) | ? [ U_216,U_215,U_214,U_213,U_212 ] : ( U_231 = U_215 & U_230 = U_216 & U_229 = vabs(U_214, U_213, U_212) & U_215 = U_214 & U_228 = vabs(U_214, U_213, U_212) ) | ? [ U_222,U_221,U_220,U_219,U_218,U_217 ] : ( U_231 = U_222 & U_230 = U_221 & U_229 = vabs(U_219, U_220, U_217) & ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) | ? [ U_227,U_226,U_225,U_224,U_223 ] : ( U_231 = U_225 & U_230 = U_224 & U_229 = vabs(U_227, U_226, U_223) & ~( U_225 = U_227 ) & ~( visFreeVar(U_227, U_224) ) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ),
% 173.65/174.00 inference(variable_rename,[status(thm)],[f_35_1]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_3, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ? [ U_202 ] : ( U_230 = U_202 & U_228 = U_202 ) & ? [ U_204 ] : ( U_231 = U_204 & ? [ U_203 ] : ( U_229 = vvar(U_203) & U_204 = U_203 ) ) ) | ( ? [ U_206 ] : ( U_231 = U_206 & ? [ U_205 ] : ( U_229 = vvar(U_205) & ~( U_206 = U_205 ) & U_228 = vvar(U_205) ) ) & ? [ U_207 ] : U_230 = U_207 ) | ? [ U_211,U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(miniscope,[status(thm)],[f_35_2]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_4, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ? [ U_204 ] : ( U_231 = U_204 & ? [ U_203 ] : ( U_229 = vvar(U_203) & U_204 = U_203 ) ) ) | ( ? [ U_206 ] : ( U_231 = U_206 & ? [ U_205 ] : ( U_229 = vvar(U_205) & ~( U_206 = U_205 ) & U_228 = vvar(U_205) ) ) & ? [ U_207 ] : U_230 = U_207 ) | ? [ U_211,U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_202,sK10(U_231, U_230, U_229, U_228))],[f_35_3]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_5, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ? [ U_203 ] : ( U_229 = vvar(U_203) & sK11(U_231, U_230, U_229, U_228) = U_203 ) ) ) | ( ? [ U_206 ] : ( U_231 = U_206 & ? [ U_205 ] : ( U_229 = vvar(U_205) & ~( U_206 = U_205 ) & U_228 = vvar(U_205) ) ) & ? [ U_207 ] : U_230 = U_207 ) | ? [ U_211,U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_204,sK11(U_231, U_230, U_229, U_228))],[f_35_4]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_6, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ? [ U_206 ] : ( U_231 = U_206 & ? [ U_205 ] : ( U_229 = vvar(U_205) & ~( U_206 = U_205 ) & U_228 = vvar(U_205) ) ) & ? [ U_207 ] : U_230 = U_207 ) | ? [ U_211,U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_203,sK12(U_231, U_230, U_229, U_228))],[f_35_5]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_7, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ? [ U_205 ] : ( U_229 = vvar(U_205) & ~( sK13(U_231, U_230, U_229, U_228) = U_205 ) & U_228 = vvar(U_205) ) ) & ? [ U_207 ] : U_230 = U_207 ) | ? [ U_211,U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_206,sK13(U_231, U_230, U_229, U_228))],[f_35_6]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_8, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & ? [ U_207 ] : U_230 = U_207 ) | ? [ U_211,U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_205,sK14(U_231, U_230, U_229, U_228))],[f_35_7]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_9, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ? [ U_211,U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(U_211, U_208) & U_228 = vapp(vsubst(U_210, U_209, U_211), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_207,sK15(U_231, U_230, U_229, U_228))],[f_35_8]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_10, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ? [ U_210 ] : ( U_231 = U_210 & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), U_208) & U_228 = vapp(vsubst(U_210, U_209, sK16(U_231, U_230, U_229, U_228)), vsubst(U_210, U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_211,sK16(U_231, U_230, U_229, U_228))],[f_35_9]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_11, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ? [ U_209 ] : ( U_230 = U_209 & ? [ U_208 ] : ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), U_208) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), U_209, sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), U_209, U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_210,sK17(U_231, U_230, U_229, U_228))],[f_35_10]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_12, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ? [ U_208 ] : ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), U_208) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), U_208)) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_209,sK18(U_231, U_230, U_229, U_228))],[f_35_11]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_13, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ? [ U_215 ] : ( U_231 = U_215 & ? [ U_214 ] : ( U_215 = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_208,sK19(U_231, U_230, U_229, U_228))],[f_35_12]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_14, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ? [ U_214 ] : ( sK20(U_231, U_230, U_229, U_228) = U_214 & ? [ U_213,U_212 ] : ( U_229 = vabs(U_214, U_213, U_212) & U_228 = vabs(U_214, U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_215,sK20(U_231, U_230, U_229, U_228))],[f_35_13]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_15, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ? [ U_213,U_212 ] : ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), U_213, U_212) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), U_213, U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_214,sK21(U_231, U_230, U_229, U_228))],[f_35_14]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_16, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ? [ U_212 ] : ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), U_212) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), U_212) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_213,sK22(U_231, U_230, U_229, U_228))],[f_35_15]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_17, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & ? [ U_216 ] : U_230 = U_216 ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_212,sK23(U_231, U_230, U_229, U_228))],[f_35_16]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_18, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ? [ U_222 ] : ( U_231 = U_222 & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( U_222 = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(U_222))) & U_228 = vsubst(U_222, U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_216,sK24(U_231, U_230, U_229, U_228))],[f_35_17]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_19, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ? [ U_221 ] : ( U_230 = U_221 & ? [ U_220,U_219 ] : ( ~( sK25(U_231, U_230, U_229, U_228) = U_219 ) & visFreeVar(U_219, U_221) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(U_221, U_217), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), U_221, vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_222,sK25(U_231, U_230, U_229, U_228))],[f_35_18]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_20, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ? [ U_220,U_219 ] : ( ~( sK25(U_231, U_230, U_229, U_228) = U_219 ) & visFreeVar(U_219, sK26(U_231, U_230, U_229, U_228)) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, U_220, U_217) & U_218 = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), U_217), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(U_218, U_220, vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_221,sK26(U_231, U_230, U_229, U_228))],[f_35_19]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_21, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ? [ U_219 ] : ( ~( sK25(U_231, U_230, U_229, U_228) = U_219 ) & visFreeVar(U_219, sK26(U_231, U_230, U_229, U_228)) & ? [ U_218,U_217 ] : ( U_229 = vabs(U_219, sK27(U_231, U_230, U_229, U_228), U_217) & U_218 = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), U_217), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(U_218, sK27(U_231, U_230, U_229, U_228), vsubst(U_219, vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_220,sK27(U_231, U_230, U_229, U_228))],[f_35_20]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_22, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ? [ U_218,U_217 ] : ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), U_217) & U_218 = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), U_217), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(U_218, sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(U_218), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_219,sK28(U_231, U_230, U_229, U_228))],[f_35_21]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_23, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ? [ U_217 ] : ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), U_217) & sK29(U_231, U_230, U_229, U_228) = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), U_217), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(sK29(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(sK29(U_231, U_230, U_229, U_228)), U_217))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_218,sK29(U_231, U_230, U_229, U_228))],[f_35_22]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_24, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)) & sK29(U_231, U_230, U_229, U_228) = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(sK29(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(sK29(U_231, U_230, U_229, U_228)), sK30(U_231, U_230, U_229, U_228)))) ) ) ) ) | ? [ U_227,U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = U_227 ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(U_227, U_224) ) & ? [ U_223 ] : ( U_229 = vabs(U_227, U_226, U_223) & U_228 = vabs(U_227, U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_217,sK30(U_231, U_230, U_229, U_228))],[f_35_23]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_25, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)) & sK29(U_231, U_230, U_229, U_228) = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(sK29(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(sK29(U_231, U_230, U_229, U_228)), sK30(U_231, U_230, U_229, U_228)))) ) ) ) ) | ? [ U_226,U_225 ] : ( U_231 = U_225 & ~( U_225 = sK31(U_231, U_230, U_229, U_228) ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(sK31(U_231, U_230, U_229, U_228), U_224) ) & ? [ U_223 ] : ( U_229 = vabs(sK31(U_231, U_230, U_229, U_228), U_226, U_223) & U_228 = vabs(sK31(U_231, U_230, U_229, U_228), U_226, vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_227,sK31(U_231, U_230, U_229, U_228))],[f_35_24]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_26, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)) & sK29(U_231, U_230, U_229, U_228) = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(sK29(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(sK29(U_231, U_230, U_229, U_228)), sK30(U_231, U_230, U_229, U_228)))) ) ) ) ) | ? [ U_225 ] : ( U_231 = U_225 & ~( U_225 = sK31(U_231, U_230, U_229, U_228) ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(sK31(U_231, U_230, U_229, U_228), U_224) ) & ? [ U_223 ] : ( U_229 = vabs(sK31(U_231, U_230, U_229, U_228), sK32(U_231, U_230, U_229, U_228), U_223) & U_228 = vabs(sK31(U_231, U_230, U_229, U_228), sK32(U_231, U_230, U_229, U_228), vsubst(U_225, U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_226,sK32(U_231, U_230, U_229, U_228))],[f_35_25]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_27, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)) & sK29(U_231, U_230, U_229, U_228) = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(sK29(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(sK29(U_231, U_230, U_229, U_228)), sK30(U_231, U_230, U_229, U_228)))) ) ) ) ) | ( U_231 = sK33(U_231, U_230, U_229, U_228) & ~( sK33(U_231, U_230, U_229, U_228) = sK31(U_231, U_230, U_229, U_228) ) & ? [ U_224 ] : ( U_230 = U_224 & ~( visFreeVar(sK31(U_231, U_230, U_229, U_228), U_224) ) & ? [ U_223 ] : ( U_229 = vabs(sK31(U_231, U_230, U_229, U_228), sK32(U_231, U_230, U_229, U_228), U_223) & U_228 = vabs(sK31(U_231, U_230, U_229, U_228), sK32(U_231, U_230, U_229, U_228), vsubst(sK33(U_231, U_230, U_229, U_228), U_224, U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(U_225,sK33(U_231, U_230, U_229, U_228))],[f_35_26]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_28, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)) & sK29(U_231, U_230, U_229, U_228) = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(sK29(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(sK29(U_231, U_230, U_229, U_228)), sK30(U_231, U_230, U_229, U_228)))) ) ) ) ) | ( U_231 = sK33(U_231, U_230, U_229, U_228) & ~( sK33(U_231, U_230, U_229, U_228) = sK31(U_231, U_230, U_229, U_228) ) & ( U_230 = sK34(U_231, U_230, U_229, U_228) & ~( visFreeVar(sK31(U_231, U_230, U_229, U_228), sK34(U_231, U_230, U_229, U_228)) ) & ? [ U_223 ] : ( U_229 = vabs(sK31(U_231, U_230, U_229, U_228), sK32(U_231, U_230, U_229, U_228), U_223) & U_228 = vabs(sK31(U_231, U_230, U_229, U_228), sK32(U_231, U_230, U_229, U_228), vsubst(sK33(U_231, U_230, U_229, U_228), sK34(U_231, U_230, U_229, U_228), U_223)) ) ) ) ) ),
% 173.65/174.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(U_224,sK34(U_231, U_230, U_229, U_228))],[f_35_27]) ).
% 173.65/174.00
% 173.65/174.00 fof(f_35_29, plain,
% 173.65/174.00 ! [ U_231,U_230,U_229,U_228 ] : ( ~( vsubst(U_231, U_230, U_229) = U_228 ) | ( ( ( U_230 = sK10(U_231, U_230, U_229, U_228) & U_228 = sK10(U_231, U_230, U_229, U_228) ) & ( U_231 = sK11(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK12(U_231, U_230, U_229, U_228)) & sK11(U_231, U_230, U_229, U_228) = sK12(U_231, U_230, U_229, U_228) ) ) ) | ( ( U_231 = sK13(U_231, U_230, U_229, U_228) & ( U_229 = vvar(sK14(U_231, U_230, U_229, U_228)) & ~( sK13(U_231, U_230, U_229, U_228) = sK14(U_231, U_230, U_229, U_228) ) & U_228 = vvar(sK14(U_231, U_230, U_229, U_228)) ) ) & U_230 = sK15(U_231, U_230, U_229, U_228) ) | ( U_231 = sK17(U_231, U_230, U_229, U_228) & ( U_230 = sK18(U_231, U_230, U_229, U_228) & ( U_229 = vapp(sK16(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228)) & U_228 = vapp(vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK16(U_231, U_230, U_229, U_228)), vsubst(sK17(U_231, U_230, U_229, U_228), sK18(U_231, U_230, U_229, U_228), sK19(U_231, U_230, U_229, U_228))) ) ) ) | ( ( U_231 = sK20(U_231, U_230, U_229, U_228) & ( sK20(U_231, U_230, U_229, U_228) = sK21(U_231, U_230, U_229, U_228) & ( U_229 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) & U_228 = vabs(sK21(U_231, U_230, U_229, U_228), sK22(U_231, U_230, U_229, U_228), sK23(U_231, U_230, U_229, U_228)) ) ) ) & U_230 = sK24(U_231, U_230, U_229, U_228) ) | ( U_231 = sK25(U_231, U_230, U_229, U_228) & ( U_230 = sK26(U_231, U_230, U_229, U_228) & ( ~( sK25(U_231, U_230, U_229, U_228) = sK28(U_231, U_230, U_229, U_228) ) & visFreeVar(sK28(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228)) & ( U_229 = vabs(sK28(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)) & sK29(U_231, U_230, U_229, U_228) = vgensym(vapp(vapp(sK26(U_231, U_230, U_229, U_228), sK30(U_231, U_230, U_229, U_228)), vvar(sK25(U_231, U_230, U_229, U_228)))) & U_228 = vsubst(sK25(U_231, U_230, U_229, U_228), sK26(U_231, U_230, U_229, U_228), vabs(sK29(U_231, U_230, U_229, U_228), sK27(U_231, U_230, U_229, U_228), vsubst(sK28(U_231, U_230, U_229, U_228), vvar(sK29(U_231, U_230, U_229, U_228)), sK30(U_231, U_230, U_229, U_228)))) ) ) ) ) | ( U_231 = sK33(U_231, U_230, U_229, U_228) & ~( sK33(U_231, U_230, U_229, U_228) = sK31(U_231, U_230, U_229, U_228) ) & ( U_230 = sK34(U_231, U_230, U_229, U_228) & ~( visFreeVar(sK31(U_231, U_230, U_229, U_228), sK34(U_231, U_230, U_229, U_228)) ) & ( U_229 = vabs(sK31(U_231, U_230, U_229, U_228), sK32(U_231, U_230, U_229, U_228), sK35(U_231, U_230, U_229, U_228)) &