%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : COM130+1 : TPTP v9.2.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:13:18 PM UTC 2026
% Result : Theorem 1.48s 1.80s
% Output : CNFRefutation 1.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 4
% Syntax : Number of formulae : 22 ( 9 unt; 0 def)
% Number of atoms : 76 ( 38 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 90 ( 36 ~; 27 |; 17 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 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 : 88 ( 7 sgn 61 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof('T-subst-abs-1',conjecture,
! [X15,X20,X9,X11,X21,X10,X12,X34] :
( ( X9 = X21
& vtcheck(X20,X11,X15)
& vtcheck(vbind(X9,X15,X20),vabs(X21,X10,X12),X34) )
=> vtcheck(X20,vsubst(X9,X11,vabs(X21,X10,X12)),X34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-subst-abs-1') ).
fof(subst3,axiom,
! [X11,X9,X1,X4,X6,X19,X21,X15,X12] :
( ( X1 = X9
& X4 = X11
& X6 = vabs(X21,X15,X12) )
=> ( X9 = X21
=> ( X19 = vsubst(X1,X4,X6)
=> X19 = vabs(X21,X15,X12) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax',subst3) ).
fof('T-Strong',axiom,
! [X9,X10,X20,X11,X15] :
( ( ~ visFreeVar(X9,X11)
& vtcheck(vbind(X9,X10,X20),X11,X15) )
=> vtcheck(X20,X11,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-Strong') ).
fof(isFreeVar1,axiom,
! [X15,X1,X4,X9,X14,X11] :
( ( X1 = X14
& X4 = vabs(X9,X15,X11) )
=> ( ( ( X9 != X14
& visFreeVar(X14,X11) )
=> visFreeVar(X1,X4) )
& ( visFreeVar(X1,X4)
=> ( X9 != X14
& visFreeVar(X14,X11) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax',isFreeVar1) ).
fof(c_0_4,negated_conjecture,
~ ! [X15,X20,X9,X11,X21,X10,X12,X34] :
( ( X9 = X21
& vtcheck(X20,X11,X15)
& vtcheck(vbind(X9,X15,X20),vabs(X21,X10,X12),X34) )
=> vtcheck(X20,vsubst(X9,X11,vabs(X21,X10,X12)),X34) ),
inference(assume_negation,[status(cth)],['T-subst-abs-1']) ).
fof(c_0_5,negated_conjecture,
( esk34_0 = esk36_0
& vtcheck(esk33_0,esk35_0,esk32_0)
& vtcheck(vbind(esk34_0,esk32_0,esk33_0),vabs(esk36_0,esk37_0,esk38_0),esk39_0)
& ~ vtcheck(esk33_0,vsubst(esk34_0,esk35_0,vabs(esk36_0,esk37_0,esk38_0)),esk39_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])]) ).
fof(c_0_6,plain,
! [X504,X505,X506,X507,X508,X509,X510,X511,X512] :
( X506 != X505
| X507 != X504
| X508 != vabs(X510,X511,X512)
| X505 != X510
| X509 != vsubst(X506,X507,X508)
| X509 = vabs(X510,X511,X512) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subst3])]) ).
fof(c_0_7,plain,
! [X9,X10,X20,X11,X15] :
( ( ~ visFreeVar(X9,X11)
& vtcheck(vbind(X9,X10,X20),X11,X15) )
=> vtcheck(X20,X11,X15) ),
inference(fof_simplification,[status(thm)],['T-Strong']) ).
cnf(c_0_8,negated_conjecture,
~ vtcheck(esk33_0,vsubst(esk34_0,esk35_0,vabs(esk36_0,esk37_0,esk38_0)),esk39_0),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_9,negated_conjecture,
esk34_0 = esk36_0,
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_10,plain,
( X9 = vabs(X6,X7,X8)
| X1 != X2
| X3 != X4
| X5 != vabs(X6,X7,X8)
| X2 != X6
| X9 != vsubst(X1,X3,X5) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
fof(c_0_11,plain,
! [X407,X408,X409,X410,X411,X412] :
( ( X410 = X411
| ~ visFreeVar(X411,X412)
| visFreeVar(X408,X409)
| X408 != X411
| X409 != vabs(X410,X407,X412) )
& ( X410 != X411
| ~ visFreeVar(X408,X409)
| X408 != X411
| X409 != vabs(X410,X407,X412) )
& ( visFreeVar(X411,X412)
| ~ visFreeVar(X408,X409)
| X408 != X411
| X409 != vabs(X410,X407,X412) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[isFreeVar1])])]) ).
fof(c_0_12,plain,
! [X636,X637,X638,X639,X640] :
( visFreeVar(X636,X639)
| ~ vtcheck(vbind(X636,X637,X638),X639,X640)
| vtcheck(X638,X639,X640) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])]) ).
cnf(c_0_13,negated_conjecture,
vtcheck(vbind(esk34_0,esk32_0,esk33_0),vabs(esk36_0,esk37_0,esk38_0),esk39_0),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_14,negated_conjecture,
~ vtcheck(esk33_0,vsubst(esk34_0,esk35_0,vabs(esk34_0,esk37_0,esk38_0)),esk39_0),
inference(rw,[status(thm)],[c_0_8,c_0_9]) ).
cnf(c_0_15,plain,
vsubst(X1,X2,vabs(X1,X3,X4)) = vabs(X1,X3,X4),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_10])])])])]) ).
cnf(c_0_16,plain,
( X1 != X2
| ~ visFreeVar(X3,X4)
| X3 != X2
| X4 != vabs(X1,X5,X6) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_17,plain,
( visFreeVar(X1,X2)
| vtcheck(X4,X2,X5)
| ~ vtcheck(vbind(X1,X3,X4),X2,X5) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_18,negated_conjecture,
vtcheck(vbind(esk34_0,esk32_0,esk33_0),vabs(esk34_0,esk37_0,esk38_0),esk39_0),
inference(rw,[status(thm)],[c_0_13,c_0_9]) ).
cnf(c_0_19,negated_conjecture,
~ vtcheck(esk33_0,vabs(esk34_0,esk37_0,esk38_0),esk39_0),
inference(rw,[status(thm)],[c_0_14,c_0_15]) ).
cnf(c_0_20,plain,
~ visFreeVar(X1,vabs(X1,X2,X3)),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_16])])]) ).
cnf(c_0_21,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_17,c_0_18]),c_0_19]),c_0_20]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM130+1 : TPTP v9.2.1. Released v6.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n015.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 16:22:17 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 1.48/1.80 % Version : CSE_E---1.7
% 1.48/1.80 % Problem : theBenchmark.p
% 1.48/1.80 % SZS status Theorem for theBenchmark.p
% 1.48/1.80 % SZS output start CNFRefutation
% See solution above
% 1.48/1.80 % Total time : 1.423s
%------------------------------------------------------------------------------