%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : COM140+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 : n009.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:20 PM UTC 2026
% Result : Theorem 23.47s 14.25s
% Output : CNFRefutation 23.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 90 ( 27 unt; 0 def)
% Number of atoms : 253 ( 114 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 269 ( 106 ~; 113 |; 27 &)
% ( 0 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-3 aty)
% Number of variables : 317 ( 71 sgn 116 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof('gensym-is-fresh',axiom,
! [X14,X11] :
( vgensym(X11) = X14
=> ~ visFreeVar(X14,X11) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax','gensym-is-fresh') ).
fof(isFreeVar2,axiom,
! [X1,X4,X12,X14,X13] :
( ( X1 = X14
& X4 = vapp(X12,X13) )
=> ( ( ( visFreeVar(X14,X12)
| visFreeVar(X14,X13) )
=> visFreeVar(X1,X4) )
& ( visFreeVar(X1,X4)
=> ( visFreeVar(X14,X12)
| visFreeVar(X14,X13) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax',isFreeVar2) ).
fof(subst2,axiom,
! [X1,X4,X6,X19,X12,X9,X11,X13] :
( ( X1 = X9
& X4 = X11
& X6 = vapp(X12,X13) )
=> ( X19 = vsubst(X1,X4,X6)
=> X19 = vapp(vsubst(X9,X11,X12),vsubst(X9,X11,X13)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax',subst2) ).
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('T-Weak-abs-2',conjecture,
! [X9,X10,X20,X21,X36,X15] :
( ( X9 = X21
& vlookup(X9,X20) = vnoType
& vtcheck(X20,vabs(X21,X36,veabs),X15) )
=> vtcheck(vbind(X9,X10,X20),vabs(X21,X36,veabs),X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-Weak-abs-2') ).
fof(subst0,axiom,
! [X9,X21,X1,X4,X6,X19,X11] :
( ( X1 = X9
& X4 = X11
& X6 = vvar(X21) )
=> ( X9 = X21
=> ( X19 = vsubst(X1,X4,X6)
=> X19 = X11 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax',subst0) ).
fof(isFreeVar0,axiom,
! [X1,X4,X9,X14] :
( ( X1 = X14
& X4 = vvar(X9) )
=> ( ( X9 = X14
=> visFreeVar(X1,X4) )
& ( visFreeVar(X1,X4)
=> X9 = X14 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax',isFreeVar0) ).
fof('alpha-equiv-typing',axiom,
! [X11,X20,X12,X15] :
( ( vtcheck(X20,X11,X15)
& valphaEquivalent(X11,X12) )
=> vtcheck(X20,X12,X15) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+1.ax','alpha-equiv-typing') ).
fof('alpha-equiv-subst-abs',axiom,
! [X10,X9,X21,X11] :
( ~ visFreeVar(X21,X11)
=> valphaEquivalent(vabs(X9,X10,X11),vabs(X21,X10,vsubst(X9,vvar(X21),X11))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+1.ax','alpha-equiv-subst-abs') ).
fof('T-Weak-abs-1-gen',axiom,
! [X9,X10,X20,X21,X36,X12,X15] :
( ( X9 != X21
& vlookup(X9,X20) = vnoType
& vtcheck(X20,vabs(X21,X36,X12),X15) )
=> vtcheck(vbind(X9,X10,X20),vabs(X21,X36,X12),X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-Weak-abs-1-gen') ).
fof('alpha-equiv-sym',axiom,
! [X13,X12] :
( valphaEquivalent(X12,X13)
=> valphaEquivalent(X13,X12) ),
file('/export/starexec/sandbox2/benchmark/Axioms/COM001+1.ax','alpha-equiv-sym') ).
fof(c_0_11,plain,
! [X14,X11] :
( vgensym(X11) = X14
=> ~ visFreeVar(X14,X11) ),
inference(fof_simplification,[status(thm)],['gensym-is-fresh']) ).
fof(c_0_12,plain,
! [X484,X485] :
( vgensym(X485) != X484
| ~ visFreeVar(X484,X485) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])]) ).
fof(c_0_13,plain,
! [X417,X418,X419,X420,X421] :
( ( ~ visFreeVar(X420,X419)
| visFreeVar(X417,X418)
| X417 != X420
| X418 != vapp(X419,X421) )
& ( ~ visFreeVar(X420,X421)
| visFreeVar(X417,X418)
| X417 != X420
| X418 != vapp(X419,X421) )
& ( ~ visFreeVar(X417,X418)
| visFreeVar(X420,X419)
| visFreeVar(X420,X421)
| X417 != X420
| X418 != vapp(X419,X421) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[isFreeVar2])])]) ).
cnf(c_0_14,plain,
( vgensym(X1) != X2
| ~ visFreeVar(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_15,plain,
( visFreeVar(X3,X4)
| ~ visFreeVar(X1,X2)
| X3 != X1
| X4 != vapp(X5,X2) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
fof(c_0_16,plain,
! [X500,X501,X502,X503,X504,X505,X506,X507] :
( X500 != X505
| X501 != X506
| X502 != vapp(X504,X507)
| X503 != vsubst(X500,X501,X502)
| X503 = vapp(vsubst(X505,X506,X504),vsubst(X505,X506,X507)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subst2])]) ).
fof(c_0_17,plain,
! [X411,X412,X413,X414,X415,X416] :
( ( X414 = X415
| ~ visFreeVar(X415,X416)
| visFreeVar(X412,X413)
| X412 != X415
| X413 != vabs(X414,X411,X416) )
& ( X414 != X415
| ~ visFreeVar(X412,X413)
| X412 != X415
| X413 != vabs(X414,X411,X416) )
& ( visFreeVar(X415,X416)
| ~ visFreeVar(X412,X413)
| X412 != X415
| X413 != vabs(X414,X411,X416) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[isFreeVar1])])]) ).
fof(c_0_18,negated_conjecture,
~ ! [X9,X10,X20,X21,X36,X15] :
( ( X9 = X21
& vlookup(X9,X20) = vnoType
& vtcheck(X20,vabs(X21,X36,veabs),X15) )
=> vtcheck(vbind(X9,X10,X20),vabs(X21,X36,veabs),X15) ),
inference(assume_negation,[status(cth)],['T-Weak-abs-2']) ).
cnf(c_0_19,plain,
~ visFreeVar(vgensym(X1),X1),
inference(er,[status(thm)],[c_0_14]) ).
cnf(c_0_20,plain,
( visFreeVar(X1,vapp(X2,X3))
| ~ visFreeVar(X1,X3) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_15])]) ).
cnf(c_0_21,plain,
( X8 = vapp(vsubst(X2,X4,X6),vsubst(X2,X4,X7))
| X1 != X2
| X3 != X4
| X5 != vapp(X6,X7)
| X8 != vsubst(X1,X3,X5) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_22,plain,
! [X486,X487,X488,X489,X490,X491,X492] :
( X488 != X486
| X489 != X492
| X490 != vvar(X487)
| X486 != X487
| X491 != vsubst(X488,X489,X490)
| X491 = X492 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[subst0])]) ).
cnf(c_0_23,plain,
( X1 = X2
| visFreeVar(X4,X5)
| ~ visFreeVar(X2,X3)
| X4 != X2
| X5 != vabs(X1,X6,X3) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
fof(c_0_24,plain,
! [X407,X408,X409,X410] :
( ( X409 != X410
| visFreeVar(X407,X408)
| X407 != X410
| X408 != vvar(X409) )
& ( ~ visFreeVar(X407,X408)
| X409 = X410
| X407 != X410
| X408 != vvar(X409) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[isFreeVar0])])]) ).
fof(c_0_25,negated_conjecture,
( esk32_0 = esk35_0
& vlookup(esk32_0,esk34_0) = vnoType
& vtcheck(esk34_0,vabs(esk35_0,esk36_0,veabs),esk37_0)
& ~ vtcheck(vbind(esk32_0,esk33_0,esk34_0),vabs(esk35_0,esk36_0,veabs),esk37_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])]) ).
cnf(c_0_26,plain,
( visFreeVar(X3,X4)
| ~ visFreeVar(X1,X2)
| X3 != X1
| X4 != vapp(X2,X5) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_27,plain,
~ visFreeVar(vgensym(vapp(X1,X2)),X2),
inference(spm,[status(thm)],[c_0_19,c_0_20]) ).
cnf(c_0_28,plain,
vapp(vsubst(X1,X2,X3),vsubst(X1,X2,X4)) = vsubst(X1,X2,vapp(X3,X4)),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_21])])])]) ).
cnf(c_0_29,plain,
( X7 = X4
| X1 != X2
| X3 != X4
| X5 != vvar(X6)
| X2 != X6
| X7 != vsubst(X1,X3,X5) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_30,plain,
( X1 = X2
| visFreeVar(X2,vabs(X1,X3,X4))
| ~ visFreeVar(X2,X4) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_23])]) ).
cnf(c_0_31,plain,
( visFreeVar(X3,X4)
| X1 != X2
| X3 != X2
| X4 != vvar(X1) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
fof(c_0_32,plain,
! [X645,X646,X647,X648] :
( ~ vtcheck(X646,X645,X648)
| ~ valphaEquivalent(X645,X647)
| vtcheck(X646,X647,X648) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['alpha-equiv-typing'])]) ).
cnf(c_0_33,negated_conjecture,
vtcheck(esk34_0,vabs(esk35_0,esk36_0,veabs),esk37_0),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_34,negated_conjecture,
esk32_0 = esk35_0,
inference(split_conjunct,[status(thm)],[c_0_25]) ).
fof(c_0_35,plain,
! [X10,X9,X21,X11] :
( ~ visFreeVar(X21,X11)
=> valphaEquivalent(vabs(X9,X10,X11),vabs(X21,X10,vsubst(X9,vvar(X21),X11))) ),
inference(fof_simplification,[status(thm)],['alpha-equiv-subst-abs']) ).
cnf(c_0_36,plain,
( visFreeVar(X1,vapp(X2,X3))
| ~ visFreeVar(X1,X2) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_26])]) ).
cnf(c_0_37,plain,
~ visFreeVar(vgensym(vsubst(X1,X2,vapp(X3,X4))),vsubst(X1,X2,X4)),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_38,plain,
vsubst(X1,X2,vvar(X1)) = X2,
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_29])])])])]) ).
cnf(c_0_39,plain,
( visFreeVar(X1,X2)
| ~ visFreeVar(X3,X4)
| X3 != X1
| X4 != vabs(X5,X6,X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_40,plain,
( X1 = X2
| visFreeVar(X2,vabs(X1,X3,vapp(X4,X5)))
| ~ visFreeVar(X2,X5) ),
inference(spm,[status(thm)],[c_0_30,c_0_20]) ).
cnf(c_0_41,plain,
visFreeVar(X1,vvar(X1)),
inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_31])])]) ).
cnf(c_0_42,plain,
( vtcheck(X1,X4,X3)
| ~ vtcheck(X1,X2,X3)
| ~ valphaEquivalent(X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_43,negated_conjecture,
vtcheck(esk34_0,vabs(esk32_0,esk36_0,veabs),esk37_0),
inference(rw,[status(thm)],[c_0_33,c_0_34]) ).
fof(c_0_44,plain,
! [X641,X642,X643,X644] :
( visFreeVar(X643,X644)
| valphaEquivalent(vabs(X642,X641,X644),vabs(X643,X641,vsubst(X642,vvar(X643),X644))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])]) ).
cnf(c_0_45,plain,
( X1 = X2
| visFreeVar(X2,vabs(X1,X3,vapp(X4,X5)))
| ~ visFreeVar(X2,X4) ),
inference(spm,[status(thm)],[c_0_30,c_0_36]) ).
cnf(c_0_46,plain,
~ visFreeVar(vgensym(vsubst(X1,X2,vapp(X3,vvar(X1)))),X2),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_47,plain,
( visFreeVar(X1,X2)
| ~ visFreeVar(X1,vabs(X3,X4,X2)) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_39])]) ).
cnf(c_0_48,plain,
( X1 = X2
| visFreeVar(X2,vabs(X1,X3,vapp(X4,vvar(X2)))) ),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
fof(c_0_49,plain,
! [X652,X653,X654,X655,X656,X657,X658] :
( X652 = X655
| vlookup(X652,X654) != vnoType
| ~ vtcheck(X654,vabs(X655,X656,X657),X658)
| vtcheck(vbind(X652,X653,X654),vabs(X655,X656,X657),X658) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['T-Weak-abs-1-gen'])]) ).
cnf(c_0_50,negated_conjecture,
( vtcheck(esk34_0,X1,esk37_0)
| ~ valphaEquivalent(vabs(esk32_0,esk36_0,veabs),X1) ),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
cnf(c_0_51,plain,
( visFreeVar(X1,X2)
| valphaEquivalent(vabs(X3,X4,X2),vabs(X1,X4,vsubst(X3,vvar(X1),X2))) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_52,plain,
( X1 = X2
| visFreeVar(X2,vabs(X1,X3,vapp(vvar(X2),X4))) ),
inference(spm,[status(thm)],[c_0_45,c_0_41]) ).
cnf(c_0_53,plain,
~ visFreeVar(vgensym(vsubst(X1,vapp(X2,X3),vapp(X4,vvar(X1)))),X3),
inference(spm,[status(thm)],[c_0_46,c_0_20]) ).
cnf(c_0_54,plain,
( X1 = X2
| visFreeVar(X2,vapp(X3,vvar(X2))) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_55,plain,
( X1 = X2
| vtcheck(vbind(X1,X7,X3),vabs(X2,X4,X5),X6)
| vlookup(X1,X3) != vnoType
| ~ vtcheck(X3,vabs(X2,X4,X5),X6) ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
cnf(c_0_56,negated_conjecture,
( vtcheck(esk34_0,vabs(X1,esk36_0,vsubst(esk32_0,vvar(X1),veabs)),esk37_0)
| visFreeVar(X1,veabs) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_57,plain,
( X1 = X2
| visFreeVar(X2,vapp(vvar(X2),X3)) ),
inference(spm,[status(thm)],[c_0_47,c_0_52]) ).
cnf(c_0_58,plain,
( visFreeVar(X1,vapp(X2,vvar(X1)))
| ~ visFreeVar(X1,X3) ),
inference(spm,[status(thm)],[c_0_53,c_0_54]) ).
cnf(c_0_59,negated_conjecture,
( X1 = X2
| vtcheck(vbind(X1,X3,esk34_0),vabs(X2,esk36_0,vsubst(esk32_0,vvar(X2),veabs)),esk37_0)
| visFreeVar(X2,veabs)
| vlookup(X1,esk34_0) != vnoType ),
inference(spm,[status(thm)],[c_0_55,c_0_56]) ).
cnf(c_0_60,negated_conjecture,
vlookup(esk32_0,esk34_0) = vnoType,
inference(split_conjunct,[status(thm)],[c_0_25]) ).
fof(c_0_61,plain,
! [X636,X637] :
( ~ valphaEquivalent(X637,X636)
| valphaEquivalent(X636,X637) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['alpha-equiv-sym'])]) ).
cnf(c_0_62,plain,
( visFreeVar(X1,vapp(vvar(X1),X2))
| ~ visFreeVar(X1,X3) ),
inference(spm,[status(thm)],[c_0_53,c_0_57]) ).
cnf(c_0_63,plain,
visFreeVar(X1,vapp(X2,vvar(X1))),
inference(spm,[status(thm)],[c_0_58,c_0_41]) ).
cnf(c_0_64,negated_conjecture,
( esk32_0 = X1
| vtcheck(vbind(esk32_0,X2,esk34_0),vabs(X1,esk36_0,vsubst(esk32_0,vvar(X1),veabs)),esk37_0)
| visFreeVar(X1,veabs) ),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_65,plain,
( valphaEquivalent(X2,X1)
| ~ valphaEquivalent(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_66,plain,
visFreeVar(X1,vapp(vvar(X1),X2)),
inference(spm,[status(thm)],[c_0_62,c_0_63]) ).
cnf(c_0_67,plain,
( X1 = X2
| visFreeVar(X2,vabs(X1,X3,vapp(vapp(X4,vvar(X2)),X5))) ),
inference(spm,[status(thm)],[c_0_45,c_0_63]) ).
cnf(c_0_68,plain,
~ visFreeVar(vgensym(vapp(X1,X2)),X1),
inference(spm,[status(thm)],[c_0_19,c_0_36]) ).
cnf(c_0_69,negated_conjecture,
~ vtcheck(vbind(esk32_0,esk33_0,esk34_0),vabs(esk35_0,esk36_0,veabs),esk37_0),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_70,negated_conjecture,
( esk32_0 = X1
| vtcheck(vbind(esk32_0,X2,esk34_0),X3,esk37_0)
| visFreeVar(X1,veabs)
| ~ valphaEquivalent(vabs(X1,esk36_0,vsubst(esk32_0,vvar(X1),veabs)),X3) ),
inference(spm,[status(thm)],[c_0_42,c_0_64]) ).
cnf(c_0_71,plain,
( valphaEquivalent(vabs(X1,X2,vsubst(X3,vvar(X1),X4)),vabs(X3,X2,X4))
| visFreeVar(X1,X4) ),
inference(spm,[status(thm)],[c_0_65,c_0_51]) ).
cnf(c_0_72,plain,
( X1 = X2
| visFreeVar(X2,vabs(X1,X3,vapp(X4,vapp(vvar(X2),X5)))) ),
inference(spm,[status(thm)],[c_0_40,c_0_66]) ).
cnf(c_0_73,plain,
( X1 = X2
| visFreeVar(X2,vapp(vapp(X3,vvar(X2)),X4)) ),
inference(spm,[status(thm)],[c_0_47,c_0_67]) ).
cnf(c_0_74,plain,
~ visFreeVar(vgensym(vapp(vapp(X1,X2),X3)),X2),
inference(spm,[status(thm)],[c_0_68,c_0_20]) ).
cnf(c_0_75,negated_conjecture,
~ vtcheck(vbind(esk32_0,esk33_0,esk34_0),vabs(esk32_0,esk36_0,veabs),esk37_0),
inference(rw,[status(thm)],[c_0_69,c_0_34]) ).
cnf(c_0_76,negated_conjecture,
( esk32_0 = X1
| vtcheck(vbind(esk32_0,X2,esk34_0),vabs(esk32_0,esk36_0,veabs),esk37_0)
| visFreeVar(X1,veabs) ),
inference(spm,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_77,plain,
( X1 = X2
| visFreeVar(X2,vapp(X3,vapp(vvar(X2),X4))) ),
inference(spm,[status(thm)],[c_0_47,c_0_72]) ).
cnf(c_0_78,plain,
( visFreeVar(X1,vapp(vapp(X2,vvar(X1)),X3))
| ~ visFreeVar(X1,X4) ),
inference(spm,[status(thm)],[c_0_53,c_0_73]) ).
cnf(c_0_79,plain,
~ visFreeVar(vgensym(vapp(vsubst(X1,X2,vapp(X3,X4)),X5)),vsubst(X1,X2,X4)),
inference(spm,[status(thm)],[c_0_74,c_0_28]) ).
cnf(c_0_80,negated_conjecture,
( esk32_0 = X1
| visFreeVar(X1,veabs) ),
inference(spm,[status(thm)],[c_0_75,c_0_76]) ).
cnf(c_0_81,plain,
( visFreeVar(X1,vapp(X2,vapp(vvar(X1),X3)))
| ~ visFreeVar(X1,X4) ),
inference(spm,[status(thm)],[c_0_53,c_0_77]) ).
cnf(c_0_82,plain,
visFreeVar(X1,vapp(vapp(X2,vvar(X1)),X3)),
inference(spm,[status(thm)],[c_0_78,c_0_66]) ).
cnf(c_0_83,plain,
~ visFreeVar(vgensym(vapp(vsubst(X1,X2,vapp(X3,vvar(X1))),X4)),X2),
inference(spm,[status(thm)],[c_0_79,c_0_38]) ).
cnf(c_0_84,negated_conjecture,
vgensym(vapp(X1,veabs)) = esk32_0,
inference(spm,[status(thm)],[c_0_27,c_0_80]) ).
cnf(c_0_85,plain,
visFreeVar(X1,vapp(X2,vapp(vvar(X1),X3))),
inference(spm,[status(thm)],[c_0_81,c_0_82]) ).
cnf(c_0_86,plain,
vapp(vsubst(X1,X2,X3),X2) = vsubst(X1,X2,vapp(X3,vvar(X1))),
inference(spm,[status(thm)],[c_0_28,c_0_38]) ).
cnf(c_0_87,negated_conjecture,
~ visFreeVar(esk32_0,X1),
inference(spm,[status(thm)],[c_0_83,c_0_84]) ).
cnf(c_0_88,plain,
visFreeVar(X1,vsubst(X2,vapp(vvar(X1),X3),vapp(X4,vvar(X2)))),
inference(spm,[status(thm)],[c_0_85,c_0_86]) ).
cnf(c_0_89,negated_conjecture,
$false,
inference(spm,[status(thm)],[c_0_87,c_0_88]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM140+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.15/0.33 % Computer : n009.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 16:21:56 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 23.47/14.25 % Version : CSE_E---1.7
% 23.47/14.25 % Problem : theBenchmark.p
% 23.47/14.25 % SZS status Theorem for theBenchmark.p
% 23.47/14.25 % SZS output start CNFRefutation
% See solution above
% 23.57/14.34 % Total time : 10.436s
%------------------------------------------------------------------------------