%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM149+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 12:10:29 PM UTC 2026
% Result : Theorem 0.14s 0.46s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 40 ( 11 unt; 2 def)
% Number of atoms : 147 ( 74 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 164 ( 57 ~; 52 |; 47 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 21 ( 21 usr; 4 con; 0-3 aty)
% Number of variables : 178 ( 130 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [VTyp0] : vnoType != vsomeType(VTyp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [Vx,VVar0,VCtx0,RESULT] :
( ( VCtx0 = vempty
& VVar0 = Vx )
=> ( RESULT = vlookup(VVar0,VCtx0)
=> RESULT = vnoType ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [Ve,VT,VC] :
( vtcheck(VC,Ve,VT)
=> ( ? [Ve1,Ve2,VS] :
( vtcheck(VC,Ve2,VS)
& vtcheck(VC,Ve1,varrow(VS,VT))
& Ve = vapp(Ve1,Ve2) )
| ? [Vx,Ve2,VT1,VT2] :
( vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
& VT = varrow(VT1,VT2)
& Ve = vabs(Vx,VT1,Ve2) )
| ? [Vx] :
( vlookup(Vx,VC) = vsomeType(VT)
& Ve = vvar(Vx) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,conjecture,
! [VT,Vx] :
( ( ~ visValue(vvar(Vx))
& vtcheck(vempty,vvar(Vx),VT) )
=> ? [Veout] : vreduce(vvar(Vx)) = vsomeExp(Veout) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
~ ! [VT,Vx] :
( ( ~ visValue(vvar(Vx))
& vtcheck(vempty,vvar(Vx),VT) )
=> ? [Veout] : vreduce(vvar(Vx)) = vsomeExp(Veout) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f74,plain,
! [X0,X1,X2,X3] : vvar(X0) != vabs(X1,X2,X3),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f75,plain,
! [X0,X1,X2] : vvar(X0) != vapp(X1,X2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f115,plain,
! [X0] : vnoType != vsomeType(X0),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f124,plain,
! [Vx,VVar0,VCtx0,RESULT] :
( RESULT = vnoType
| RESULT != vlookup(VVar0,VCtx0)
| VCtx0 != vempty
| VVar0 != Vx ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f125,plain,
! [VVar0,VCtx0] :
( ! [RESULT] :
( RESULT = vnoType
| RESULT != vlookup(VVar0,VCtx0) )
| VCtx0 != vempty
| ! [Vx] : VVar0 != Vx ),
inference(miniscoping,[status(thm)],[f124]) ).
fof(f126,plain,
! [X0,X1,X2,X3] :
( X3 = vnoType
| X3 != vlookup(X0,X2)
| X2 != vempty
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f238,plain,
! [Ve,VT,VC] :
( ? [Ve1,Ve2,VS] :
( vtcheck(VC,Ve2,VS)
& vtcheck(VC,Ve1,varrow(VS,VT))
& Ve = vapp(Ve1,Ve2) )
| ? [Vx,Ve2,VT1,VT2] :
( vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
& VT = varrow(VT1,VT2)
& Ve = vabs(Vx,VT1,Ve2) )
| ? [Vx] :
( vlookup(Vx,VC) = vsomeType(VT)
& Ve = vvar(Vx) )
| ~ vtcheck(VC,Ve,VT) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f239,definition,
! [Ve,VT,VC] :
( sP3_prd(VC,VT,Ve)
<=> ( ? [Vx,Ve2,VT1,VT2] :
( vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
& VT = varrow(VT1,VT2)
& Ve = vabs(Vx,VT1,Ve2) )
| ? [Vx] :
( vlookup(Vx,VC) = vsomeType(VT)
& Ve = vvar(Vx) ) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f240,plain,
! [Ve,VT,VC] :
( ? [Ve1,Ve2,VS] :
( vtcheck(VC,Ve2,VS)
& vtcheck(VC,Ve1,varrow(VS,VT))
& Ve = vapp(Ve1,Ve2) )
| sP3_prd(VC,VT,Ve)
| ~ vtcheck(VC,Ve,VT) ),
inference(formula_renaming,[status(thm)],[f238,f239]) ).
fof(f241,plain,
! [Ve,VT,VC] :
( ? [Ve2,VS] :
( vtcheck(VC,Ve2,VS)
& ? [Ve1] :
( vtcheck(VC,Ve1,varrow(VS,VT))
& Ve = vapp(Ve1,Ve2) ) )
| sP3_prd(VC,VT,Ve)
| ~ vtcheck(VC,Ve,VT) ),
inference(miniscoping,[status(thm)],[f240]) ).
fof(f242,plain,
! [Ve,VT,VC] :
( ( vtcheck(VC,sK18_skl(VC,VT,Ve),sK19_skl(VC,VT,Ve))
& vtcheck(VC,sK20_skl(VC,VT,Ve),varrow(sK19_skl(VC,VT,Ve),VT))
& Ve = vapp(sK20_skl(VC,VT,Ve),sK18_skl(VC,VT,Ve)) )
| sP3_prd(VC,VT,Ve)
| ~ vtcheck(VC,Ve,VT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(Ve2,sK18_skl(VC,VT,Ve)),skolemize(VS,sK19_skl(VC,VT,Ve)),skolemize(Ve1,sK20_skl(VC,VT,Ve))],[f241]) ).
fof(f243,plain,
! [X0,X1,X2] :
( X1 = vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1))
| sP3_prd(X0,X2,X1)
| ~ vtcheck(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f252,plain,
? [VT,Vx] :
( ! [Veout] : vreduce(vvar(Vx)) != vsomeExp(Veout)
& ~ visValue(vvar(Vx))
& vtcheck(vempty,vvar(Vx),VT) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f253,plain,
? [Vx] :
( ! [Veout] : vreduce(vvar(Vx)) != vsomeExp(Veout)
& ~ visValue(vvar(Vx))
& ? [VT] : vtcheck(vempty,vvar(Vx),VT) ),
inference(miniscoping,[status(thm)],[f252]) ).
fof(f254,plain,
( ! [Veout] : vreduce(vvar(sK21_skl)) != vsomeExp(Veout)
& ~ visValue(vvar(sK21_skl))
& vtcheck(vempty,vvar(sK21_skl),sK22_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(Vx,sK21_skl),skolemize(VT,sK22_skl)],[f253]) ).
fof(f255,plain,
vtcheck(vempty,vvar(sK21_skl),sK22_skl),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f295,definition,
! [Ve,VT,VC,Vx] :
( sP7_prd(Vx,VC,VT,Ve)
<=> ( vlookup(Vx,VC) = vsomeType(VT)
& Ve = vvar(Vx) ) ),
introduced(definition,[new_symbols(definition,[sP7_prd])],[]) ).
fof(f296,plain,
! [Ve,VT,VC] :
( sP3_prd(VC,VT,Ve)
<=> ( ? [Vx,Ve2,VT1,VT2] :
( vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
& VT = varrow(VT1,VT2)
& Ve = vabs(Vx,VT1,Ve2) )
| ? [Vx] : sP7_prd(Vx,VC,VT,Ve) ) ),
inference(formula_renaming,[status(thm)],[f239,f295]) ).
fof(f297,plain,
! [Ve,VT,VC] :
( ( ( ! [Vx,Ve2,VT1,VT2] :
( ~ vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
| VT != varrow(VT1,VT2)
| Ve != vabs(Vx,VT1,Ve2) )
& ! [Vx] : ~ sP7_prd(Vx,VC,VT,Ve) )
| sP3_prd(VC,VT,Ve) )
& ( ? [Vx,Ve2,VT1,VT2] :
( vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
& VT = varrow(VT1,VT2)
& Ve = vabs(Vx,VT1,Ve2) )
| ? [Vx] : sP7_prd(Vx,VC,VT,Ve)
| ~ sP3_prd(VC,VT,Ve) ) ),
inference(NNF_transformation,[status(thm)],[f296]) ).
fof(f298,plain,
( ! [Ve,VT,VC] :
( ( ! [Vx,Ve2,VT1,VT2] :
( ~ vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
| VT != varrow(VT1,VT2)
| Ve != vabs(Vx,VT1,Ve2) )
& ! [Vx] : ~ sP7_prd(Vx,VC,VT,Ve) )
| sP3_prd(VC,VT,Ve) )
& ! [Ve,VT,VC] :
( ? [Vx,Ve2,VT1,VT2] :
( vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
& VT = varrow(VT1,VT2)
& Ve = vabs(Vx,VT1,Ve2) )
| ? [Vx] : sP7_prd(Vx,VC,VT,Ve)
| ~ sP3_prd(VC,VT,Ve) ) ),
inference(miniscoping,[status(thm)],[f297]) ).
fof(f299,plain,
( ! [Ve,VT,VC] :
( ( ! [Vx,Ve2,VT1,VT2] :
( ~ vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)
| VT != varrow(VT1,VT2)
| Ve != vabs(Vx,VT1,Ve2) )
& ! [Vx] : ~ sP7_prd(Vx,VC,VT,Ve) )
| sP3_prd(VC,VT,Ve) )
& ! [Ve,VT,VC] :
( ( vtcheck(vbind(sK41_skl(VC,VT,Ve),sK43_skl(VC,VT,Ve),VC),sK42_skl(VC,VT,Ve),sK44_skl(VC,VT,Ve))
& VT = varrow(sK43_skl(VC,VT,Ve),sK44_skl(VC,VT,Ve))
& Ve = vabs(sK41_skl(VC,VT,Ve),sK43_skl(VC,VT,Ve),sK42_skl(VC,VT,Ve)) )
| sP7_prd(sK40_skl(VC,VT,Ve),VC,VT,Ve)
| ~ sP3_prd(VC,VT,Ve) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl,sK41_skl,sK42_skl,sK43_skl,sK44_skl]),skolemize(Vx,sK40_skl(VC,VT,Ve)),skolemize(Vx,sK41_skl(VC,VT,Ve)),skolemize(Ve2,sK42_skl(VC,VT,Ve)),skolemize(VT1,sK43_skl(VC,VT,Ve)),skolemize(VT2,sK44_skl(VC,VT,Ve))],[f298]) ).
fof(f300,plain,
! [X0,X1,X2] :
( X2 = vabs(sK41_skl(X0,X1,X2),sK43_skl(X0,X1,X2),sK42_skl(X0,X1,X2))
| sP7_prd(sK40_skl(X0,X1,X2),X0,X1,X2)
| ~ sP3_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f335,plain,
! [Ve,VT,VC,Vx] :
( ( vlookup(Vx,VC) != vsomeType(VT)
| Ve != vvar(Vx)
| sP7_prd(Vx,VC,VT,Ve) )
& ( ( vlookup(Vx,VC) = vsomeType(VT)
& Ve = vvar(Vx) )
| ~ sP7_prd(Vx,VC,VT,Ve) ) ),
inference(NNF_transformation,[status(thm)],[f295]) ).
fof(f336,plain,
( ! [Ve,VT,VC,Vx] :
( vlookup(Vx,VC) != vsomeType(VT)
| Ve != vvar(Vx)
| sP7_prd(Vx,VC,VT,Ve) )
& ! [Ve,VT,VC,Vx] :
( ( vlookup(Vx,VC) = vsomeType(VT)
& Ve = vvar(Vx) )
| ~ sP7_prd(Vx,VC,VT,Ve) ) ),
inference(miniscoping,[status(thm)],[f335]) ).
fof(f338,plain,
! [X0,X1,X2,X3] :
( vlookup(X0,X1) = vsomeType(X2)
| ~ sP7_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f417,plain,
! [X0] : vlookup(X0,vempty) = vnoType,
inference(destructive_equality_resolution,[status(thm)],[f126]) ).
fof(f489,plain,
! [X0,X1,X2] :
( sP3_prd(X0,X2,vvar(X1))
| ~ vtcheck(X0,vvar(X1),X2) ),
inference(resolution,[status(thm)],[f243,f75]) ).
fof(f492,plain,
sP3_prd(vempty,sK22_skl,vvar(sK21_skl)),
inference(resolution,[status(thm)],[f489,f255]) ).
fof(f498,plain,
! [X0,X1,X2] :
( sP7_prd(sK40_skl(X0,X1,vvar(X2)),X0,X1,vvar(X2))
| ~ sP3_prd(X0,X1,vvar(X2)) ),
inference(resolution,[status(thm)],[f300,f74]) ).
fof(f503,plain,
! [X0,X1,X2] :
( vlookup(sK40_skl(X0,X1,vvar(X2)),X0) = vsomeType(X1)
| ~ sP3_prd(X0,X1,vvar(X2)) ),
inference(resolution,[status(thm)],[f498,f338]) ).
fof(f506,plain,
! [X0,X1] :
( vnoType = vsomeType(X0)
| ~ sP3_prd(vempty,X0,vvar(X1)) ),
inference(paramodulation,[status(thm)],[f417,f503]) ).
fof(f508,plain,
! [X0,X1] : ~ sP3_prd(vempty,X0,vvar(X1)),
inference(forward_subsumption_resolution,[status(thm)],[f506,f115]) ).
fof(f509,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f492,f508]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM149+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n019.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 14:18:50 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.46 % Refutation found
% 0.14/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.48 % Elapsed time: 0.106939 seconds
% 0.14/0.48 % CPU time: 0.600193 seconds
% 0.14/0.48 % Total memory used: 125.601 MB
% 0.14/0.48 % Net memory used: 125.138 MB
%------------------------------------------------------------------------------