%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM141+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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 : Fri Sep 25 01:03:40 PM UTC 2026
% Result : Theorem 61.85s 8.98s
% Output : Proof 61.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 20
% Syntax : Number of formulae : 121 ( 69 unt; 0 def)
% Number of atoms : 387 ( 285 equ)
% Maximal formula atoms : 33 ( 3 avg)
% Number of connectives : 417 ( 151 ~; 93 |; 159 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-5 aty)
% Number of functors : 77 ( 77 usr; 12 con; 0-4 aty)
% Number of variables : 402 ( 33 sgn 177 !; 108 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f56,axiom,
! [Vx,VS,VC,Vy,VS1,VT] :
( ( vtcheck(VC,vabs(Vy,VS1,veabs),VT)
& vlookup(Vx,VC) = vnoType
& Vx = Vy )
=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd28) ).
fof(f56_nnf,plain,
! [Vx,VS,VC,Vy,VS1,VT] :
( vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)
| ~ vtcheck(VC,vabs(Vy,VS1,veabs),VT)
| vlookup(Vx,VC) != vnoType
| Vx != Vy ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [Vx,Vy,VC,VS1,VT,VS] :
( vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)
| ~ vtcheck(VC,vabs(Vy,VS1,veabs),VT)
| vlookup(Vx,VC) != vnoType
| Vx != Vy ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c321,plain,
( vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)
| ~ vtcheck(X2,vabs(X3,X4,veabs),X5)
| vlookup(X0,X2) != vnoType
| X0 != X3 ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(t236,plain,
ifeq(X1,X2,ifeq(vlookup(X1,X3),vnoType,ifeq(vtcheck(X3,vabs(X2,X4,veabs),X5),true,vtcheck(vbind(X1,X6,X3),vabs(X2,X4,veabs),X5),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c321]) ).
cnf(t262,plain,
ifeq(X1,X2,ifeq(vlookup(X1,X3),vnoType,ifeq(vtcheck(X3,vabs(X2,X4,veabs),X5),true,vtcheck(vbind(X1,X6,X3),vabs(X2,X4,veabs),X5),true),true),true) = true,
inference(orient,[status(thm)],[t236]) ).
fof(f57,conjecture,
! [Vx,VS,VC,Vy,VS1,VT] :
( ( vtcheck(VC,vabs(Vy,VS1,veabs),VT)
& vlookup(Vx,VC) = vnoType )
=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd29) ).
fof(f57_neg,negated_conjecture,
~ ! [Vx,VS,VC,Vy,VS1,VT] :
( ( vtcheck(VC,vabs(Vy,VS1,veabs),VT)
& vlookup(Vx,VC) = vnoType )
=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f57_nnf,plain,
? [Vx,VS,VC,Vy,VS1,VT] :
( ~ vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)
& vtcheck(VC,vabs(Vy,VS1,veabs),VT)
& vlookup(Vx,VC) = vnoType ),
inference(nnf_transformation,[status(thm)],[f57_neg]) ).
fof(f57_sk,plain,
( ~ vtcheck(vbind(sk74,sk75,sk76),vabs(sk77,sk78,veabs),sk79)
& vtcheck(sk76,vabs(sk77,sk78,veabs),sk79)
& vlookup(sk74,sk76) = vnoType ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk74,sk75,sk76,sk77,sk78,sk79])],[f57_nnf]) ).
cnf(c324,plain,
~ vtcheck(vbind(sk74,sk75,sk76),vabs(sk77,sk78,veabs),sk79),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(t178,plain,
vtcheck(vbind(sk74,sk75,sk76),vabs(sk77,sk78,veabs),sk79) = false,
inference(equality_encoding,[status(esa)],[c324]) ).
cnf(t291,plain,
vtcheck(vbind(sk74,sk75,sk76),vabs(sk77,sk78,veabs),sk79) = false,
inference(orient,[status(thm)],[t178]) ).
cnf(t26,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t254,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t26]) ).
fof(f55,axiom,
! [Vx,VS,VC,Vy,VS1,VT] :
( ( vtcheck(VC,vabs(Vy,VS1,veabs),VT)
& vlookup(Vx,VC) = vnoType
& Vx != Vy )
=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd27) ).
fof(f55_nnf,plain,
! [Vx,VS,VC,Vy,VS1,VT] :
( vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)
| ~ vtcheck(VC,vabs(Vy,VS1,veabs),VT)
| vlookup(Vx,VC) != vnoType
| Vx = Vy ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
! [Vx,Vy,VC,VS1,VT,VS] :
( vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)
| ~ vtcheck(VC,vabs(Vy,VS1,veabs),VT)
| vlookup(Vx,VC) != vnoType
| Vx = Vy ),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c320,plain,
( vtcheck(vbind(X0,X1,X2),vabs(X3,X4,veabs),X5)
| ~ vtcheck(X2,vabs(X3,X4,veabs),X5)
| vlookup(X0,X2) != vnoType
| X0 = X3 ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(t237,plain,
ifeq(vlookup(X1,X2),vnoType,ifeq(vtcheck(X2,vabs(X3,X4,veabs),X5),true,or(eq(X1,X3),vtcheck(vbind(X1,X6,X2),vabs(X3,X4,veabs),X5)),true),true) = true,
inference(equality_encoding,[status(esa)],[c320]) ).
cnf(t268,plain,
ifeq(vlookup(X1,X2),vnoType,ifeq(vtcheck(X2,vabs(X3,X4,veabs),X5),true,or(eq(X1,X3),vtcheck(vbind(X1,X6,X2),vabs(X3,X4,veabs),X5)),true),true) = true,
inference(orient,[status(thm)],[t237]) ).
cnf(t297,plain,
true = ifeq(vlookup(sk74,sk76),vnoType,ifeq(vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),true,or(eq(sk74,sk77),false),true),true),
inference(cp,[status(thm)],[t268,t291]) ).
cnf(c322,plain,
vlookup(sk74,sk76) = vnoType,
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(t7,plain,
vlookup(sk74,sk76) = vnoType,
inference(equality_encoding,[status(esa)],[c322]) ).
cnf(t483,plain,
vlookup(sk74,sk76) = vnoType,
inference(orient,[status(thm)],[t7]) ).
cnf(t576,plain,
true = ifeq(vnoType,vnoType,ifeq(vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),true,or(eq(sk74,sk77),false),true),true),
inference(step,[status(thm)],[t297,t483]) ).
cnf(t13,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t238,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t13]) ).
cnf(t577,plain,
true = ifeq(vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),true,or(eq(sk74,sk77),false),true),
inference(step,[status(thm)],[t576,t238]) ).
cnf(c323,plain,
vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(t45,plain,
vtcheck(sk76,vabs(sk77,sk78,veabs),sk79) = true,
inference(equality_encoding,[status(esa)],[c323]) ).
cnf(t279,plain,
vtcheck(sk76,vabs(sk77,sk78,veabs),sk79) = true,
inference(orient,[status(thm)],[t45]) ).
cnf(t578,plain,
true = ifeq(true,true,or(eq(sk74,sk77),false),true),
inference(step,[status(thm)],[t577,t279]) ).
cnf(t579,plain,
true = or(eq(sk74,sk77),false),
inference(step,[status(thm)],[t578,t238]) ).
cnf(t3,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t255,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t580,plain,
true = eq(sk74,sk77),
inference(step,[status(thm)],[t579,t255]) ).
cnf(t505,plain,
eq(sk74,sk77) = true,
inference(orient,[status(thm)],[t580]) ).
cnf(t506,plain,
sk77 = ifeq(true,true,sk74,sk77),
inference(cp,[status(thm)],[t254,t505]) ).
cnf(t581,plain,
sk77 = sk74,
inference(step,[status(thm)],[t506,t238]) ).
cnf(t510,plain,
sk74 = sk77,
inference(orient,[status(thm)],[t581]) ).
cnf(t583,plain,
vtcheck(vbind(sk77,sk75,sk76),vabs(sk77,sk78,veabs),sk79) = false,
inference(step,[status(thm)],[t291,t510]) ).
cnf(t512,plain,
vtcheck(vbind(sk77,sk75,sk76),vabs(sk77,sk78,veabs),sk79) = false,
inference(rw,[status(thm)],[t583]) ).
cnf(t525,plain,
vtcheck(vbind(sk77,sk75,sk76),vabs(sk77,sk78,veabs),sk79) = false,
inference(orient,[status(thm)],[t512]) ).
cnf(t529,plain,
true = ifeq(sk77,sk77,ifeq(vlookup(sk77,sk76),vnoType,ifeq(vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),true,false,true),true),true),
inference(cp,[status(thm)],[t262,t525]) ).
cnf(t584,plain,
true = ifeq(vlookup(sk77,sk76),vnoType,ifeq(vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),true,false,true),true),
inference(step,[status(thm)],[t529,t238]) ).
cnf(t582,plain,
vlookup(sk77,sk76) = vnoType,
inference(step,[status(thm)],[t483,t510]) ).
cnf(t511,plain,
vlookup(sk77,sk76) = vnoType,
inference(rw,[status(thm)],[t582]) ).
cnf(t513,plain,
vlookup(sk77,sk76) = vnoType,
inference(orient,[status(thm)],[t511]) ).
cnf(t585,plain,
true = ifeq(vnoType,vnoType,ifeq(vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),true,false,true),true),
inference(step,[status(thm)],[t584,t513]) ).
cnf(t586,plain,
true = ifeq(vtcheck(sk76,vabs(sk77,sk78,veabs),sk79),true,false,true),
inference(step,[status(thm)],[t585,t238]) ).
cnf(t587,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t586,t279]) ).
cnf(t588,plain,
true = false,
inference(step,[status(thm)],[t587,t238]) ).
cnf(t532,plain,
false = true,
inference(orient,[status(thm)],[t588]) ).
fof(f3,axiom,
! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd3) ).
fof(f3_nnf,plain,
! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c9,plain,
vvar(X0) != vabs(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
fof(f4,axiom,
! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd4) ).
fof(f4_nnf,plain,
! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c10,plain,
vvar(X0) != vapp(X1,X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
fof(f5,axiom,
! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd5) ).
fof(f5_nnf,plain,
! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c11,plain,
vabs(X0,X1,X2) != vapp(X3,X4),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f7,axiom,
! [Vx,VExp0] :
( VExp0 = vvar(Vx)
=> ~ visValue(VExp0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isValue1) ).
fof(f7_nnf,plain,
! [Vx,VExp0] :
( ~ visValue(VExp0)
| VExp0 != vvar(Vx) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [VExp0,Vx] :
( ~ visValue(VExp0)
| VExp0 != vvar(Vx) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c13,plain,
( ~ visValue(X1)
| X1 != vvar(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f8,axiom,
! [Ve1,Ve2,VExp0] :
( VExp0 = vapp(Ve1,Ve2)
=> ~ visValue(VExp0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isValue2) ).
fof(f8_nnf,plain,
! [Ve1,Ve2,VExp0] :
( ~ visValue(VExp0)
| VExp0 != vapp(Ve1,Ve2) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [VExp0,Ve1,Ve2] :
( ~ visValue(VExp0)
| VExp0 != vapp(Ve1,Ve2) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c14,plain,
( ~ visValue(X2)
| X2 != vapp(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f10,axiom,
! [VT,VVar0,VExp0,Vx,Vv,Ve] :
( ( VExp0 = vabs(Vx,VT,Ve)
& VVar0 = Vv )
=> ( ( visFreeVar(VVar0,VExp0)
=> ( visFreeVar(Vv,Ve)
& Vx != Vv ) )
& ( ( visFreeVar(Vv,Ve)
& Vx != Vv )
=> visFreeVar(VVar0,VExp0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isFreeVar1) ).
fof(f10_nnf,plain,
! [VT,VVar0,VExp0,Vx,Vv,Ve] :
( ( ( ( visFreeVar(Vv,Ve)
& Vx != Vv )
| ~ visFreeVar(VVar0,VExp0) )
& ( visFreeVar(VVar0,VExp0)
| ~ visFreeVar(Vv,Ve)
| Vx = Vv ) )
| VExp0 != vabs(Vx,VT,Ve)
| VVar0 != Vv ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [VVar0,Vv,VExp0,Vx,VT,Ve] :
( ( ( ( visFreeVar(Vv,Ve)
& Vx != Vv )
| ~ visFreeVar(VVar0,VExp0) )
& ( visFreeVar(VVar0,VExp0)
| ~ visFreeVar(Vv,Ve)
| Vx = Vv ) )
| VExp0 != vabs(Vx,VT,Ve)
| VVar0 != Vv ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c18,plain,
( X3 != X4
| ~ visFreeVar(X1,X2)
| X2 != vabs(X3,X0,X5)
| X1 != X4 ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f16,axiom,
! [VVar0,VTyp0,VCtx0] : vempty != vbind(VVar0,VTyp0,VCtx0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd10) ).
fof(f16_nnf,plain,
! [VVar0,VTyp0,VCtx0] : vempty != vbind(VVar0,VTyp0,VCtx0),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [VVar0,VTyp0,VCtx0] : vempty != vbind(VVar0,VTyp0,VCtx0),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c33,plain,
vempty != vbind(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f17,axiom,
! [VTyp0] : vnoType != vsomeType(VTyp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd11) ).
fof(f17_nnf,plain,
! [VTyp0] : vnoType != vsomeType(VTyp0),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [VTyp0] : vnoType != vsomeType(VTyp0),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c34,plain,
vnoType != vsomeType(X0),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f18,axiom,
! [VOptTyp0] :
( VOptTyp0 = vnoType
=> ~ visSomeType(VOptTyp0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isSomeType0) ).
fof(f18_nnf,plain,
! [VOptTyp0] :
( ~ visSomeType(VOptTyp0)
| VOptTyp0 != vnoType ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [VOptTyp0] :
( ~ visSomeType(VOptTyp0)
| VOptTyp0 != vnoType ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c35,plain,
( ~ visSomeType(X0)
| X0 != vnoType ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f27,axiom,
! [Vv,Ve] :
( vgensym(Ve) = Vv
=> ~ visFreeVar(Vv,Ve) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd15) ).
fof(f27_nnf,plain,
! [Vv,Ve] :
( ~ visFreeVar(Vv,Ve)
| vgensym(Ve) != Vv ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [Ve,Vv] :
( ~ visFreeVar(Vv,Ve)
| vgensym(Ve) != Vv ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c91,plain,
( ~ visFreeVar(X0,X1)
| vgensym(X1) != X0 ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
fof(f34,axiom,
! [VVar0,VExp0,VExp1,RESULT] :
( vsubst(VVar0,VExp0,VExp1) = RESULT
=> ( ? [Vy,VT,Vx,Ve,Ve1] :
( RESULT = vabs(Vy,VT,vsubst(Vx,Ve,Ve1))
& ~ visFreeVar(Vy,Ve)
& Vx != Vy
& VExp1 = vabs(Vy,VT,Ve1)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Vx,Ve,VT,Vy,Vfresh,Ve1] :
( RESULT = vsubst(Vx,Ve,vabs(Vfresh,VT,vsubst(Vy,vvar(Vfresh),Ve1)))
& Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx)))
& visFreeVar(Vy,Ve)
& Vx != Vy
& VExp1 = vabs(Vy,VT,Ve1)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Ve,Vx,Vy,VT,Ve1] :
( RESULT = vabs(Vy,VT,Ve1)
& Vx = Vy
& VExp1 = vabs(Vy,VT,Ve1)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Ve1,Vx,Ve,Ve2] :
( RESULT = vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2))
& VExp1 = vapp(Ve1,Ve2)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Ve,Vx,Vy] :
( RESULT = vvar(Vy)
& Vx != Vy
& VExp1 = vvar(Vy)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Vx,Vy,Ve] :
( RESULT = Ve
& Vx = Vy
& VExp1 = vvar(Vy)
& VExp0 = Ve
& VVar0 = Vx ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd16) ).
fof(f34_nnf,plain,
! [VVar0,VExp0,VExp1,RESULT] :
( ? [Vy,VT,Vx,Ve,Ve1] :
( RESULT = vabs(Vy,VT,vsubst(Vx,Ve,Ve1))
& ~ visFreeVar(Vy,Ve)
& Vx != Vy
& VExp1 = vabs(Vy,VT,Ve1)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Vx,Ve,VT,Vy,Vfresh,Ve1] :
( RESULT = vsubst(Vx,Ve,vabs(Vfresh,VT,vsubst(Vy,vvar(Vfresh),Ve1)))
& Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx)))
& visFreeVar(Vy,Ve)
& Vx != Vy
& VExp1 = vabs(Vy,VT,Ve1)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Ve,Vx,Vy,VT,Ve1] :
( RESULT = vabs(Vy,VT,Ve1)
& Vx = Vy
& VExp1 = vabs(Vy,VT,Ve1)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Ve1,Vx,Ve,Ve2] :
( RESULT = vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2))
& VExp1 = vapp(Ve1,Ve2)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Ve,Vx,Vy] :
( RESULT = vvar(Vy)
& Vx != Vy
& VExp1 = vvar(Vy)
& VExp0 = Ve
& VVar0 = Vx )
| ? [Vx,Vy,Ve] :
( RESULT = Ve
& Vx = Vy
& VExp1 = vvar(Vy)
& VExp0 = Ve
& VVar0 = Vx )
| vsubst(VVar0,VExp0,VExp1) != RESULT ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [VVar0,VExp0,VExp1,RESULT] :
( ( RESULT = vabs(sk30(VVar0,VExp0,VExp1,RESULT),sk31(VVar0,VExp0,VExp1,RESULT),vsubst(sk32(VVar0,VExp0,VExp1,RESULT),sk33(VVar0,VExp0,VExp1,RESULT),sk34(VVar0,VExp0,VExp1,RESULT)))
& ~ visFreeVar(sk30(VVar0,VExp0,VExp1,RESULT),sk33(VVar0,VExp0,VExp1,RESULT))
& sk32(VVar0,VExp0,VExp1,RESULT) != sk30(VVar0,VExp0,VExp1,RESULT)
& VExp1 = vabs(sk30(VVar0,VExp0,VExp1,RESULT),sk31(VVar0,VExp0,VExp1,RESULT),sk34(VVar0,VExp0,VExp1,RESULT))
& VExp0 = sk33(VVar0,VExp0,VExp1,RESULT)
& VVar0 = sk32(VVar0,VExp0,VExp1,RESULT) )
| ( RESULT = vsubst(sk24(VVar0,VExp0,VExp1,RESULT),sk25(VVar0,VExp0,VExp1,RESULT),vabs(sk28(VVar0,VExp0,VExp1,RESULT),sk26(VVar0,VExp0,VExp1,RESULT),vsubst(sk27(VVar0,VExp0,VExp1,RESULT),vvar(sk28(VVar0,VExp0,VExp1,RESULT)),sk29(VVar0,VExp0,VExp1,RESULT))))
& sk28(VVar0,VExp0,VExp1,RESULT) = vgensym(vapp(vapp(sk25(VVar0,VExp0,VExp1,RESULT),sk29(VVar0,VExp0,VExp1,RESULT)),vvar(sk24(VVar0,VExp0,VExp1,RESULT))))
& visFreeVar(sk27(VVar0,VExp0,VExp1,RESULT),sk25(VVar0,VExp0,VExp1,RESULT))
& sk24(VVar0,VExp0,VExp1,RESULT) != sk27(VVar0,VExp0,VExp1,RESULT)
& VExp1 = vabs(sk27(VVar0,VExp0,VExp1,RESULT),sk26(VVar0,VExp0,VExp1,RESULT),sk29(VVar0,VExp0,VExp1,RESULT))
& VExp0 = sk25(VVar0,VExp0,VExp1,RESULT)
& VVar0 = sk24(VVar0,VExp0,VExp1,RESULT) )
| ( RESULT = vabs(sk21(VVar0,VExp0,VExp1,RESULT),sk22(VVar0,VExp0,VExp1,RESULT),sk23(VVar0,VExp0,VExp1,RESULT))
& sk20(VVar0,VExp0,VExp1,RESULT) = sk21(VVar0,VExp0,VExp1,RESULT)
& VExp1 = vabs(sk21(VVar0,VExp0,VExp1,RESULT),sk22(VVar0,VExp0,VExp1,RESULT),sk23(VVar0,VExp0,VExp1,RESULT))
& VExp0 = sk19(VVar0,VExp0,VExp1,RESULT)
& VVar0 = sk20(VVar0,VExp0,VExp1,RESULT) )
| ( RESULT = vapp(vsubst(sk16(VVar0,VExp0,VExp1,RESULT),sk17(VVar0,VExp0,VExp1,RESULT),sk15(VVar0,VExp0,VExp1,RESULT)),vsubst(sk16(VVar0,VExp0,VExp1,RESULT),sk17(VVar0,VExp0,VExp1,RESULT),sk18(VVar0,VExp0,VExp1,RESULT)))
& VExp1 = vapp(sk15(VVar0,VExp0,VExp1,RESULT),sk18(VVar0,VExp0,VExp1,RESULT))
& VExp0 = sk17(VVar0,VExp0,VExp1,RESULT)
& VVar0 = sk16(VVar0,VExp0,VExp1,RESULT) )
| ( RESULT = vvar(sk14(VVar0,VExp0,VExp1,RESULT))
& sk13(VVar0,VExp0,VExp1,RESULT) != sk14(VVar0,VExp0,VExp1,RESULT)
& VExp1 = vvar(sk14(VVar0,VExp0,VExp1,RESULT))
& VExp0 = sk12(VVar0,VExp0,VExp1,RESULT)
& VVar0 = sk13(VVar0,VExp0,VExp1,RESULT) )
| ( RESULT = sk11(VVar0,VExp0,VExp1,RESULT)
& sk9(VVar0,VExp0,VExp1,RESULT) = sk10(VVar0,VExp0,VExp1,RESULT)
& VExp1 = vvar(sk10(VVar0,VExp0,VExp1,RESULT))
& VExp0 = sk11(VVar0,VExp0,VExp1,RESULT)
& VVar0 = sk9(VVar0,VExp0,VExp1,RESULT) )
| vsubst(VVar0,VExp0,VExp1) != RESULT ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9,sk10,sk11,sk12,sk13,sk14,sk15,sk16,sk17,sk18,sk19,sk20,sk21,sk22,sk23,sk24,sk25,sk26,sk27,sk28,sk29,sk30,sk31,sk32,sk33,sk34])],[f34_nnf]) ).
cnf(c117,plain,
( sk13(X0,X1,X2,X3) != sk14(X0,X1,X2,X3)
| ~ def6(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31])],[f34_sk]) ).
cnf(c159,plain,
( sk24(X0,X1,X2,X3) != sk27(X0,X1,X2,X3)
| ~ def20(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31])],[f34_sk]) ).
cnf(c180,plain,
( sk32(X0,X1,X2,X3) != sk30(X0,X1,X2,X3)
| ~ def27(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31])],[f34_sk]) ).
cnf(c183,plain,
( ~ visFreeVar(sk30(X0,X1,X2,X3),sk33(X0,X1,X2,X3))
| ~ def28(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31])],[f34_sk]) ).
fof(f37,axiom,
! [VExp0] : vnoExp != vsomeExp(VExp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd19) ).
fof(f37_nnf,plain,
! [VExp0] : vnoExp != vsomeExp(VExp0),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [VExp0] : vnoExp != vsomeExp(VExp0),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c199,plain,
vnoExp != vsomeExp(X0),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
fof(f38,axiom,
! [VOptExp0] :
( VOptExp0 = vnoExp
=> ~ visSomeExp(VOptExp0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isSomeExp0) ).
fof(f38_nnf,plain,
! [VOptExp0] :
( ~ visSomeExp(VOptExp0)
| VOptExp0 != vnoExp ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [VOptExp0] :
( ~ visSomeExp(VOptExp0)
| VOptExp0 != vnoExp ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c200,plain,
( ~ visSomeExp(X0)
| X0 != vnoExp ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f48,axiom,
! [VExp0,RESULT] :
( vreduce(VExp0) = RESULT
=> ( ? [Ve2,Ve1,Ve1red] :
( RESULT = vnoExp
& ~ visSomeExp(Ve1red)
& Ve1red = vreduce(Ve1)
& ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10)
& VExp0 = vapp(Ve1,Ve2) )
| ? [Ve1,Ve1red,Ve2] :
( RESULT = vsomeExp(vapp(vgetSomeExp(Ve1red),Ve2))
& visSomeExp(Ve1red)
& Ve1red = vreduce(Ve1)
& ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10)
& VExp0 = vapp(Ve1,Ve2) )
| ? [Vx,VS,Ve1,Ve2red,Ve2] :
( RESULT = vnoExp
& ~ visValue(Ve2)
& ~ visSomeExp(Ve2red)
& Ve2red = vreduce(Ve2)
& VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) )
| ? [VS,Ve2red,Vx,Ve2,Ve1] :
( RESULT = vsomeExp(vsubst(Vx,Ve2,Ve1))
& visValue(Ve2)
& ~ visSomeExp(Ve2red)
& Ve2red = vreduce(Ve2)
& VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) )
| ? [Ve2,Vx,VS,Ve1,Ve2red] :
( RESULT = vsomeExp(vapp(vabs(Vx,VS,Ve1),vgetSomeExp(Ve2red)))
& visSomeExp(Ve2red)
& Ve2red = vreduce(Ve2)
& VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) )
| ? [Vx,VS,Ve] :
( RESULT = vnoExp
& VExp0 = vabs(Vx,VS,Ve) )
| ? [Vx] :
( RESULT = vnoExp
& VExp0 = vvar(Vx) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd20) ).
fof(f48_nnf,plain,
! [VExp0,RESULT] :
( ? [Ve2,Ve1,Ve1red] :
( RESULT = vnoExp
& ~ visSomeExp(Ve1red)
& Ve1red = vreduce(Ve1)
& ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10)
& VExp0 = vapp(Ve1,Ve2) )
| ? [Ve1,Ve1red,Ve2] :
( RESULT = vsomeExp(vapp(vgetSomeExp(Ve1red),Ve2))
& visSomeExp(Ve1red)
& Ve1red = vreduce(Ve1)
& ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10)
& VExp0 = vapp(Ve1,Ve2) )
| ? [Vx,VS,Ve1,Ve2red,Ve2] :
( RESULT = vnoExp
& ~ visValue(Ve2)
& ~ visSomeExp(Ve2red)
& Ve2red = vreduce(Ve2)
& VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) )
| ? [VS,Ve2red,Vx,Ve2,Ve1] :
( RESULT = vsomeExp(vsubst(Vx,Ve2,Ve1))
& visValue(Ve2)
& ~ visSomeExp(Ve2red)
& Ve2red = vreduce(Ve2)
& VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) )
| ? [Ve2,Vx,VS,Ve1,Ve2red] :
( RESULT = vsomeExp(vapp(vabs(Vx,VS,Ve1),vgetSomeExp(Ve2red)))
& visSomeExp(Ve2red)
& Ve2red = vreduce(Ve2)
& VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) )
| ? [Vx,VS,Ve] :
( RESULT = vnoExp
& VExp0 = vabs(Vx,VS,Ve) )
| ? [Vx] :
( RESULT = vnoExp
& VExp0 = vvar(Vx) )
| vreduce(VExp0) != RESULT ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [VExp0,RESULT,VVx0,VVS0,VVe10] :
( ( RESULT = vnoExp
& ~ visSomeExp(sk65(VExp0,RESULT))
& sk65(VExp0,RESULT) = vreduce(sk64(VExp0,RESULT))
& sk64(VExp0,RESULT) != vabs(VVx0,VVS0,VVe10)
& VExp0 = vapp(sk64(VExp0,RESULT),sk63(VExp0,RESULT)) )
| ( RESULT = vsomeExp(vapp(vgetSomeExp(sk61(VExp0,RESULT)),sk62(VExp0,RESULT)))
& visSomeExp(sk61(VExp0,RESULT))
& sk61(VExp0,RESULT) = vreduce(sk60(VExp0,RESULT))
& sk60(VExp0,RESULT) != vabs(VVx0,VVS0,VVe10)
& VExp0 = vapp(sk60(VExp0,RESULT),sk62(VExp0,RESULT)) )
| ( RESULT = vnoExp
& ~ visValue(sk59(VExp0,RESULT))
& ~ visSomeExp(sk58(VExp0,RESULT))
& sk58(VExp0,RESULT) = vreduce(sk59(VExp0,RESULT))
& VExp0 = vapp(vabs(sk55(VExp0,RESULT),sk56(VExp0,RESULT),sk57(VExp0,RESULT)),sk59(VExp0,RESULT)) )
| ( RESULT = vsomeExp(vsubst(sk52(VExp0,RESULT),sk53(VExp0,RESULT),sk54(VExp0,RESULT)))
& visValue(sk53(VExp0,RESULT))
& ~ visSomeExp(sk51(VExp0,RESULT))
& sk51(VExp0,RESULT) = vreduce(sk53(VExp0,RESULT))
& VExp0 = vapp(vabs(sk52(VExp0,RESULT),sk50(VExp0,RESULT),sk54(VExp0,RESULT)),sk53(VExp0,RESULT)) )
| ( RESULT = vsomeExp(vapp(vabs(sk46(VExp0,RESULT),sk47(VExp0,RESULT),sk48(VExp0,RESULT)),vgetSomeExp(sk49(VExp0,RESULT))))
& visSomeExp(sk49(VExp0,RESULT))
& sk49(VExp0,RESULT) = vreduce(sk45(VExp0,RESULT))
& VExp0 = vapp(vabs(sk46(VExp0,RESULT),sk47(VExp0,RESULT),sk48(VExp0,RESULT)),sk45(VExp0,RESULT)) )
| ( RESULT = vnoExp
& VExp0 = vabs(sk42(VExp0,RESULT),sk43(VExp0,RESULT),sk44(VExp0,RESULT)) )
| ( RESULT = vnoExp
& VExp0 = vvar(sk41(VExp0,RESULT)) )
| vreduce(VExp0) != RESULT ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk41,sk42,sk43,sk44,sk45,sk46,sk47,sk48,sk49,sk50,sk51,sk52,sk53,sk54,sk55,sk56,sk57,sk58,sk59,sk60,sk61,sk62,sk63,sk64,sk65])],[f48_nnf]) ).
cnf(c235,plain,
( ~ visSomeExp(sk51(X0,X1))
| ~ def40(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59])],[f48_sk]) ).
cnf(c250,plain,
( ~ visSomeExp(sk58(X0,X1))
| ~ def45(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59])],[f48_sk]) ).
cnf(c253,plain,
( ~ visValue(sk59(X0,X1))
| ~ def46(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59])],[f48_sk]) ).
cnf(c262,plain,
( sk60(X0,X1) != vabs(X9,X10,X11)
| ~ def49(X0,X1,X9,X10,X11) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59])],[f48_sk]) ).
cnf(c277,plain,
( sk64(X0,X1) != vabs(X9,X10,X11)
| ~ def54(X0,X1,X9,X10,X11) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59])],[f48_sk]) ).
cnf(c283,plain,
( ~ visSomeExp(sk65(X0,X1))
| ~ def56(X0,X1,X9,X10,X11) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59])],[f48_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c10,c11,c13,c14,c18,c33,c34,c35,c91,c117,c159,c180,c183,c199,c200,c235,c250,c253,c262,c277,c283,c324]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t532]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM141+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.97 % Computer : n010.cluster.edu
% 0.09/0.97 % Model : x86_64 x86_64
% 0.09/0.97 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.97 % Memory : 8046.5625MB
% 0.09/0.97 % OS : Linux 6.8.0-71-generic
% 0.09/0.97 % CPULimit : 300
% 0.09/0.97 % WCLimit : 300
% 0.09/0.97 % DateTime : Fri Sep 25 07:55:33 UTC 2026
% 0.09/0.97 % CPUTime :
% 0.09/0.97 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 61.85/8.98 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.85/8.98 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------