%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM130+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:27 PM UTC 2026
% Result : Theorem 0.13s 0.46s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 4
% Syntax : Number of formulae : 28 ( 10 unt; 0 def)
% Number of atoms : 96 ( 46 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 113 ( 45 ~; 35 |; 24 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-3 aty)
% Number of variables : 126 ( 110 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,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') ).
fof(f32,axiom,
! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1] :
( ( VExp1 = vabs(Vy,VT,Ve1)
& VExp0 = Ve
& VVar0 = Vx )
=> ( Vx = Vy
=> ( RESULT = vsubst(VVar0,VExp0,VExp1)
=> RESULT = vabs(Vy,VT,Ve1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [Vx,VS,VC,Ve,VT] :
( ( vtcheck(vbind(Vx,VS,VC),Ve,VT)
& ~ visFreeVar(Vx,Ve) )
=> vtcheck(VC,Ve,VT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,conjecture,
! [VT,VC,Vx,Ve,Vy,VS,Ve1,VT2] :
( ( vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2)
& vtcheck(VC,Ve,VT)
& Vx = Vy )
=> vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,negated_conjecture,
~ ! [VT,VC,Vx,Ve,Vy,VS,Ve1,VT2] :
( ( vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2)
& vtcheck(VC,Ve,VT)
& Vx = Vy )
=> vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2) ),
inference(negated_conjecture,[status(cth)],[f59]) ).
fof(f91,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(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f92,plain,
! [VVar0,VExp0,Vx,Vv,Ve] :
( ( ( ( visFreeVar(Vv,Ve)
& Vx != Vv )
| ~ visFreeVar(VVar0,VExp0) )
& ( visFreeVar(VVar0,VExp0)
| ~ visFreeVar(Vv,Ve)
| Vx = Vv ) )
| ! [VT] : VExp0 != vabs(Vx,VT,Ve)
| VVar0 != Vv ),
inference(miniscoping,[status(thm)],[f91]) ).
fof(f94,plain,
! [X0,X1,X2,X3,X4,X5] :
( X3 != X1
| ~ visFreeVar(X0,X2)
| X2 != vabs(X3,X4,X5)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f160,plain,
! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1] :
( RESULT = vabs(Vy,VT,Ve1)
| RESULT != vsubst(VVar0,VExp0,VExp1)
| Vx != Vy
| VExp1 != vabs(Vy,VT,Ve1)
| VExp0 != Ve
| VVar0 != Vx ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f161,plain,
! [Vx,VVar0,VExp0,VExp1,Vy,VT,Ve1] :
( ! [RESULT] :
( RESULT = vabs(Vy,VT,Ve1)
| RESULT != vsubst(VVar0,VExp0,VExp1) )
| Vx != Vy
| VExp1 != vabs(Vy,VT,Ve1)
| ! [Ve] : VExp0 != Ve
| VVar0 != Vx ),
inference(miniscoping,[status(thm)],[f160]) ).
fof(f162,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( X8 = vabs(X5,X6,X7)
| X8 != vsubst(X0,X2,X4)
| X1 != X5
| X4 != vabs(X5,X6,X7)
| X2 != X3
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f251,plain,
! [Vx,VS,VC,Ve,VT] :
( vtcheck(VC,Ve,VT)
| ~ vtcheck(vbind(Vx,VS,VC),Ve,VT)
| visFreeVar(Vx,Ve) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f252,plain,
! [VC,Ve,VT] :
( vtcheck(VC,Ve,VT)
| ! [Vx] :
( ! [VS] : ~ vtcheck(vbind(Vx,VS,VC),Ve,VT)
| visFreeVar(Vx,Ve) ) ),
inference(miniscoping,[status(thm)],[f251]) ).
fof(f253,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X3,X1,X4)
| ~ vtcheck(vbind(X0,X2,X3),X1,X4)
| visFreeVar(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f260,plain,
? [VT,VC,Vx,Ve,Vy,VS,Ve1,VT2] :
( ~ vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2)
& vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2)
& vtcheck(VC,Ve,VT)
& Vx = Vy ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f261,plain,
? [VC,Vx,Ve,Vy,VS,Ve1,VT2] :
( ~ vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2)
& ? [VT] :
( vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2)
& vtcheck(VC,Ve,VT)
& Vx = Vy ) ),
inference(miniscoping,[status(thm)],[f260]) ).
fof(f262,plain,
( ~ vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK24_skl,sK25_skl,sK26_skl)),sK27_skl)
& vtcheck(vbind(sK22_skl,sK28_skl,sK21_skl),vabs(sK24_skl,sK25_skl,sK26_skl),sK27_skl)
& vtcheck(sK21_skl,sK23_skl,sK28_skl)
& sK22_skl = sK24_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(VC,sK21_skl),skolemize(Vx,sK22_skl),skolemize(Ve,sK23_skl),skolemize(Vy,sK24_skl),skolemize(VS,sK25_skl),skolemize(Ve1,sK26_skl),skolemize(VT2,sK27_skl),skolemize(VT,sK28_skl)],[f261]) ).
fof(f263,plain,
sK22_skl = sK24_skl,
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f265,plain,
vtcheck(vbind(sK22_skl,sK28_skl,sK21_skl),vabs(sK24_skl,sK25_skl,sK26_skl),sK27_skl),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f266,plain,
~ vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK24_skl,sK25_skl,sK26_skl)),sK27_skl),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f418,plain,
! [X0,X1,X2] : ~ visFreeVar(X0,vabs(X0,X1,X2)),
inference(destructive_equality_resolution,[status(thm)],[f94]) ).
fof(f438,plain,
! [X0,X1,X2,X3] : vsubst(X0,X1,vabs(X0,X2,X3)) = vabs(X0,X2,X3),
inference(destructive_equality_resolution,[status(thm)],[f162]) ).
fof(f478,plain,
vtcheck(vbind(sK22_skl,sK28_skl,sK21_skl),vabs(sK22_skl,sK25_skl,sK26_skl),sK27_skl),
inference(forward_demodulation,[status(thm)],[f263,f265]) ).
fof(f479,plain,
~ vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK22_skl,sK25_skl,sK26_skl)),sK27_skl),
inference(forward_demodulation,[status(thm)],[f263,f266]) ).
fof(f480,plain,
~ vtcheck(sK21_skl,vabs(sK22_skl,sK25_skl,sK26_skl),sK27_skl),
inference(forward_demodulation,[status(thm)],[f438,f479]) ).
fof(f485,plain,
! [X0,X1,X2,X3,X4,X5] :
( vtcheck(X2,vabs(X0,X3,X4),X5)
| ~ vtcheck(vbind(X0,X1,X2),vabs(X0,X3,X4),X5) ),
inference(resolution,[status(thm)],[f253,f418]) ).
fof(f547,plain,
! [X0] : ~ vtcheck(vbind(sK22_skl,X0,sK21_skl),vabs(sK22_skl,sK25_skl,sK26_skl),sK27_skl),
inference(resolution,[status(thm)],[f485,f480]) ).
fof(f549,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f478,f547]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM130+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:19:01 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 0.13/0.46 % Refutation found
% 0.13/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.49 % Elapsed time: 0.108896 seconds
% 0.13/0.49 % CPU time: 0.548058 seconds
% 0.13/0.49 % Total memory used: 99.092 MB
% 0.13/0.49 % Net memory used: 98.428 MB
%------------------------------------------------------------------------------