%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM144+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.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 22.37s 4.19s
% Output : Proof 22.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 3
% Syntax : Number of formulae : 17 ( 8 unt; 0 def)
% Number of atoms : 34 ( 25 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 31 ( 14 ~; 7 |; 6 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-3 aty)
% Number of variables : 46 ( 10 sgn 28 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f42,axiom,
! [Vx,VS,Ve,VExp0,RESULT] :
( VExp0 = vabs(Vx,VS,Ve)
=> ( RESULT = vreduce(VExp0)
=> RESULT = vnoExp ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reduce1) ).
fof(f42_nnf,plain,
! [Vx,VS,Ve,VExp0,RESULT] :
( RESULT = vnoExp
| RESULT != vreduce(VExp0)
| VExp0 != vabs(Vx,VS,Ve) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [VExp0,Vx,VS,Ve,RESULT] :
( RESULT = vnoExp
| RESULT != vreduce(VExp0)
| VExp0 != vabs(Vx,VS,Ve) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c204,plain,
( X4 = vnoExp
| X4 != vreduce(X3)
| X3 != vabs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p776,plain,
( X0 = vnoExp
| X0 != vreduce(vabs(X1,X2,X3)) ),
inference(equality_resolution,[status(thm)],[c204]) ).
cnf(p778,plain,
vreduce(vabs(X0,X1,X2)) = vnoExp,
inference(equality_resolution,[status(thm)],[p776]) ).
fof(f59,conjecture,
! [Vx,VS,VC,Veout,VT] :
( ( vtcheck(VC,vabs(Vx,VS,ve1),VT)
& vreduce(vabs(Vx,VS,ve1)) = vsomeExp(Veout) )
=> vtcheck(VC,Veout,VT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd31) ).
fof(f59_neg,negated_conjecture,
~ ! [Vx,VS,VC,Veout,VT] :
( ( vtcheck(VC,vabs(Vx,VS,ve1),VT)
& vreduce(vabs(Vx,VS,ve1)) = vsomeExp(Veout) )
=> vtcheck(VC,Veout,VT) ),
inference(negated_conjecture,[status(cth)],[f59]) ).
fof(f59_nnf,plain,
? [Vx,VS,VC,Veout,VT] :
( ~ vtcheck(VC,Veout,VT)
& vtcheck(VC,vabs(Vx,VS,ve1),VT)
& vreduce(vabs(Vx,VS,ve1)) = vsomeExp(Veout) ),
inference(nnf_transformation,[status(thm)],[f59_neg]) ).
fof(f59_sk,plain,
( ~ vtcheck(sk76,sk77,sk78)
& vtcheck(sk76,vabs(sk74,sk75,ve1),sk78)
& vreduce(vabs(sk74,sk75,ve1)) = vsomeExp(sk77) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk74,sk75,sk76,sk77,sk78])],[f59_nnf]) ).
cnf(c324,plain,
vreduce(vabs(sk74,sk75,ve1)) = vsomeExp(sk77),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(p779,plain,
vnoExp = vsomeExp(sk77),
inference(demodulation,[status(thm)],[p778,c324]) ).
fof(f37,axiom,
! [VExp0] : vnoExp != vsomeExp(VExp0),
file('/export/starexec/sandbox/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]) ).
cnf(p788,plain,
$false,
inference(resolution,[status(thm)],[p779,c199]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM144+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 08:00:40 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 22.37/4.19 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.37/4.19 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------