%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : COM148+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:12:32 PM UTC 2026
% Result : Theorem 249.34s 36.79s
% Output : CNFRefutation 249.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 21
% Syntax : Number of formulae : 136 ( 31 unt; 0 def)
% Number of atoms : 1031 ( 648 equ)
% Maximal formula atoms : 400 ( 7 avg)
% Number of connectives : 1218 ( 323 ~; 632 |; 220 &)
% ( 2 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 87 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 54 ( 54 usr; 7 con; 0-5 aty)
% Number of variables : 458 ( 60 sgn 195 !; 101 ?)
% Comments :
%------------------------------------------------------------------------------
fof('T-Progress-T-app',conjecture,
! [X15] :
( ( ~ visValue(vapp(ve1,ve2))
& vtcheck(vempty,vapp(ve1,ve2),X15) )
=> ? [X35] : vreduce(vapp(ve1,ve2)) = vsomeExp(X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Progress-T-app') ).
fof('DIFF-abs-app',axiom,
! [X1,X3,X4,X6,X7] : vabs(X1,X3,X4) != vapp(X6,X7),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','DIFF-abs-app') ).
fof('DIFF-var-app',axiom,
! [X1,X4,X6] : vvar(X1) != vapp(X4,X6),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','DIFF-var-app') ).
fof('T-inv',axiom,
! [X11,X15,X20] :
( vtcheck(X20,X11,X15)
=> ( ? [X12,X13,X10] :
( vtcheck(X20,X13,X10)
& vtcheck(X20,X12,varrow(X10,X15))
& X11 = vapp(X12,X13) )
| ? [X9,X13,X33,X34] :
( vtcheck(vbind(X9,X33,X20),X13,X34)
& X15 = varrow(X33,X34)
& X11 = vabs(X9,X33,X13) )
| ? [X9] :
( vlookup(X9,X20) = vsomeType(X15)
& X11 = vvar(X9) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','T-inv') ).
fof('EQ-app',axiom,
! [X4,X6,X7,X8] :
( ( ( X6 = X8
& X4 = X7 )
=> vapp(X4,X6) = vapp(X7,X8) )
& ( vapp(X4,X6) = vapp(X7,X8)
=> ( X6 = X8
& X4 = X7 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','EQ-app') ).
fof('reduce-INV',axiom,
! [X4,X19] :
( vreduce(X4) = X19
=> ( ? [X13,X12,X27] :
( X19 = vnoExp
& ~ visSomeExp(X27)
& X27 = vreduce(X12)
& ! [X28,X29,X30] : X12 != vabs(X28,X29,X30)
& X4 = vapp(X12,X13) )
| ? [X12,X27,X13] :
( X19 = vsomeExp(vapp(vgetSomeExp(X27),X13))
& visSomeExp(X27)
& X27 = vreduce(X12)
& ! [X28,X29,X30] : X12 != vabs(X28,X29,X30)
& X4 = vapp(X12,X13) )
| ? [X9,X10,X12,X26,X13] :
( X19 = vnoExp
& ~ visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X10,X26,X9,X13,X12] :
( X19 = vsomeExp(vsubst(X9,X13,X12))
& visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X13,X9,X10,X12,X26] :
( X19 = vsomeExp(vapp(vabs(X9,X10,X12),vgetSomeExp(X26)))
& visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X9,X10,X11] :
( X19 = vnoExp
& X4 = vabs(X9,X10,X11) )
| ? [X9] :
( X19 = vnoExp
& X4 = vvar(X9) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','reduce-INV') ).
fof('T-Progress-T-app-IH1',axiom,
! [X15] :
( ( ~ visValue(ve1)
& vtcheck(vempty,ve1,X15) )
=> ? [X35] : vreduce(ve1) = vsomeExp(X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Progress-T-app-IH1') ).
fof(reduce5,axiom,
! [X12,X4,X19,X27,X13] :
( ( ! [X28,X29,X30] : X12 != vabs(X28,X29,X30)
& X4 = vapp(X12,X13) )
=> ( ( visSomeExp(X27)
& X27 = vreduce(X12) )
=> ( X19 = vreduce(X4)
=> X19 = vsomeExp(vapp(vgetSomeExp(X27),X13)) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',reduce5) ).
fof(isValue2,axiom,
! [X12,X13,X4] :
( X4 = vapp(X12,X13)
=> ~ visValue(X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',isValue2) ).
fof(isValue1,axiom,
! [X9,X4] :
( X4 = vvar(X9)
=> ~ visValue(X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',isValue1) ).
fof(isSomeExp1,axiom,
! [X11,X25] :
( X25 = vsomeExp(X11)
=> visSomeExp(X25) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',isSomeExp1) ).
fof(isValue0,axiom,
! [X9,X10,X11,X4] :
( X4 = vabs(X9,X10,X11)
=> visValue(X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',isValue0) ).
fof(getSomeExp0,axiom,
! [X25,X19,X11] :
( X25 = vsomeExp(X11)
=> ( X19 = vgetSomeExp(X25)
=> X19 = X11 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',getSomeExp0) ).
fof(reduce0,axiom,
! [X9,X4,X19] :
( X4 = vvar(X9)
=> ( X19 = vreduce(X4)
=> X19 = vnoExp ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',reduce0) ).
fof('DIFF-noExp-someExp',axiom,
! [X4] : vnoExp != vsomeExp(X4),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax','DIFF-noExp-someExp') ).
fof(reduce1,axiom,
! [X9,X10,X11,X4,X19] :
( X4 = vabs(X9,X10,X11)
=> ( X19 = vreduce(X4)
=> X19 = vnoExp ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',reduce1) ).
fof(reduce3,axiom,
! [X10,X26,X4,X19,X9,X13,X12] :
( X4 = vapp(vabs(X9,X10,X12),X13)
=> ( ( visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13) )
=> ( X19 = vreduce(X4)
=> X19 = vsomeExp(vsubst(X9,X13,X12)) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',reduce3) ).
fof(reduce2,axiom,
! [X13,X4,X19,X9,X10,X12,X26] :
( X4 = vapp(vabs(X9,X10,X12),X13)
=> ( ( visSomeExp(X26)
& X26 = vreduce(X13) )
=> ( X19 = vreduce(X4)
=> X19 = vsomeExp(vapp(vabs(X9,X10,X12),vgetSomeExp(X26))) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',reduce2) ).
fof('T-Progress-T-app-IH2',axiom,
! [X15] :
( ( ~ visValue(ve2)
& vtcheck(vempty,ve2,X15) )
=> ? [X35] : vreduce(ve2) = vsomeExp(X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Progress-T-app-IH2') ).
fof(c_0_19,negated_conjecture,
~ ! [X15] :
( ( ~ visValue(vapp(ve1,ve2))
& vtcheck(vempty,vapp(ve1,ve2),X15) )
=> ? [X35] : vreduce(vapp(ve1,ve2)) = vsomeExp(X35) ),
inference(assume_negation,[status(cth)],['T-Progress-T-app']) ).
fof(c_0_20,negated_conjecture,
~ ! [X15] :
( ( ~ visValue(vapp(ve1,ve2))
& vtcheck(vempty,vapp(ve1,ve2),X15) )
=> ? [X35] : vreduce(vapp(ve1,ve2)) = vsomeExp(X35) ),
inference(fof_simplification,[status(thm)],[c_0_19]) ).
fof(c_0_21,plain,
! [X1,X3,X4,X6,X7] : vabs(X1,X3,X4) != vapp(X6,X7),
inference(fof_simplification,[status(thm)],['DIFF-abs-app']) ).
fof(c_0_22,plain,
! [X1,X4,X6] : vvar(X1) != vapp(X4,X6),
inference(fof_simplification,[status(thm)],['DIFF-var-app']) ).
fof(c_0_23,plain,
! [X132,X133,X134] :
( ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| vtcheck(vbind(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),X134),esk13_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk17_3(X132,X133,X134),esk18_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| vtcheck(vbind(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),X134),esk13_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk16_3(X132,X133,X134),varrow(esk18_3(X132,X133,X134),X133)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| vtcheck(vbind(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),X134),esk13_3(X132,X133,X134),esk15_3(X132,X133,X134))
| X132 = vapp(esk16_3(X132,X133,X134),esk17_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| X133 = varrow(esk14_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk17_3(X132,X133,X134),esk18_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| X133 = varrow(esk14_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk16_3(X132,X133,X134),varrow(esk18_3(X132,X133,X134),X133)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| X133 = varrow(esk14_3(X132,X133,X134),esk15_3(X132,X133,X134))
| X132 = vapp(esk16_3(X132,X133,X134),esk17_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| X132 = vabs(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),esk13_3(X132,X133,X134))
| vtcheck(X134,esk17_3(X132,X133,X134),esk18_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| X132 = vabs(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),esk13_3(X132,X133,X134))
| vtcheck(X134,esk16_3(X132,X133,X134),varrow(esk18_3(X132,X133,X134),X133)) )
& ( ~ vtcheck(X134,X132,X133)
| vlookup(esk11_3(X132,X133,X134),X134) = vsomeType(X133)
| X132 = vabs(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),esk13_3(X132,X133,X134))
| X132 = vapp(esk16_3(X132,X133,X134),esk17_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| vtcheck(vbind(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),X134),esk13_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk17_3(X132,X133,X134),esk18_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| vtcheck(vbind(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),X134),esk13_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk16_3(X132,X133,X134),varrow(esk18_3(X132,X133,X134),X133)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| vtcheck(vbind(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),X134),esk13_3(X132,X133,X134),esk15_3(X132,X133,X134))
| X132 = vapp(esk16_3(X132,X133,X134),esk17_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| X133 = varrow(esk14_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk17_3(X132,X133,X134),esk18_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| X133 = varrow(esk14_3(X132,X133,X134),esk15_3(X132,X133,X134))
| vtcheck(X134,esk16_3(X132,X133,X134),varrow(esk18_3(X132,X133,X134),X133)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| X133 = varrow(esk14_3(X132,X133,X134),esk15_3(X132,X133,X134))
| X132 = vapp(esk16_3(X132,X133,X134),esk17_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| X132 = vabs(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),esk13_3(X132,X133,X134))
| vtcheck(X134,esk17_3(X132,X133,X134),esk18_3(X132,X133,X134)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| X132 = vabs(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),esk13_3(X132,X133,X134))
| vtcheck(X134,esk16_3(X132,X133,X134),varrow(esk18_3(X132,X133,X134),X133)) )
& ( ~ vtcheck(X134,X132,X133)
| X132 = vvar(esk11_3(X132,X133,X134))
| X132 = vabs(esk12_3(X132,X133,X134),esk14_3(X132,X133,X134),esk13_3(X132,X133,X134))
| X132 = vapp(esk16_3(X132,X133,X134),esk17_3(X132,X133,X134)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['T-inv'])])])])]) ).
fof(c_0_24,negated_conjecture,
! [X37] :
( vreduce(vapp(ve1,ve2)) != vsomeExp(X37)
& ~ visValue(vapp(ve1,ve2))
& vtcheck(vempty,vapp(ve1,ve2),esk1_0) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])])]) ).
fof(c_0_25,plain,
! [X106,X107,X108,X109,X110] : vabs(X106,X107,X108) != vapp(X109,X110),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_21])]) ).
fof(c_0_26,plain,
! [X103,X104,X105] : vvar(X103) != vapp(X104,X105),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_22])]) ).
fof(c_0_27,plain,
! [X99,X100,X101,X102] :
( ( vapp(X99,X100) = vapp(X101,X102)
| X100 != X102
| X99 != X101 )
& ( vapp(X99,X100) != vapp(X101,X102)
| X100 = X102 )
& ( vapp(X99,X100) != vapp(X101,X102)
| X99 = X101 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-app'])])])]) ).
cnf(c_0_28,plain,
( ~ vtcheck(X3,X1,X2)
| X1 = vvar(esk11_3(X1,X2,X3))
| X1 = vabs(esk12_3(X1,X2,X3),esk14_3(X1,X2,X3),esk13_3(X1,X2,X3))
| X1 = vapp(esk16_3(X1,X2,X3),esk17_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_29,negated_conjecture,
vtcheck(vempty,vapp(ve1,ve2),esk1_0),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_30,plain,
vabs(X1,X2,X3) != vapp(X4,X5),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_31,plain,
vvar(X1) != vapp(X2,X3),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_32,plain,
( vapp(X3,X1) != vapp(X4,X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_33,negated_conjecture,
vapp(esk16_3(vapp(ve1,ve2),esk1_0,vempty),esk17_3(vapp(ve1,ve2),esk1_0,vempty)) = vapp(ve1,ve2),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_30]),c_0_31]) ).
cnf(c_0_34,negated_conjecture,
( vapp(ve1,ve2) != vapp(X2,X1)
| esk17_3(vapp(ve1,ve2),esk1_0,vempty) = X1 ),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_35,negated_conjecture,
esk17_3(vapp(ve1,ve2),esk1_0,vempty) = ve2,
inference(er,[status(thm)],[c_0_34]) ).
fof(c_0_36,plain,
! [X4,X19] :
( epred2_2(X19,X4)
<=> ( ? [X12,X27,X13] :
( X19 = vsomeExp(vapp(vgetSomeExp(X27),X13))
& visSomeExp(X27)
& X27 = vreduce(X12)
& ! [X28,X29,X30] : X12 != vabs(X28,X29,X30)
& X4 = vapp(X12,X13) )
| ? [X9,X10,X12,X26,X13] :
( X19 = vnoExp
& ~ visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X10,X26,X9,X13,X12] :
( X19 = vsomeExp(vsubst(X9,X13,X12))
& visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X13,X9,X10,X12,X26] :
( X19 = vsomeExp(vapp(vabs(X9,X10,X12),vgetSomeExp(X26)))
& visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X9,X10,X11] :
( X19 = vnoExp
& X4 = vabs(X9,X10,X11) )
| ? [X9] :
( X19 = vnoExp
& X4 = vvar(X9) ) ) ),
introduced(definition) ).
cnf(c_0_37,plain,
( vapp(X1,X3) != vapp(X2,X4)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_38,negated_conjecture,
vapp(esk16_3(vapp(ve1,ve2),esk1_0,vempty),ve2) = vapp(ve1,ve2),
inference(rw,[status(thm)],[c_0_33,c_0_35]) ).
fof(c_0_39,plain,
! [X4,X19] :
( epred1_2(X19,X4)
<=> ( ? [X10,X26,X9,X13,X12] :
( X19 = vsomeExp(vsubst(X9,X13,X12))
& visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X13,X9,X10,X12,X26] :
( X19 = vsomeExp(vapp(vabs(X9,X10,X12),vgetSomeExp(X26)))
& visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X9,X10,X11] :
( X19 = vnoExp
& X4 = vabs(X9,X10,X11) )
| ? [X9] :
( X19 = vnoExp
& X4 = vvar(X9) ) ) ),
introduced(definition) ).
fof(c_0_40,plain,
! [X4,X19] :
( vreduce(X4) = X19
=> ( ? [X13,X12,X27] :
( X19 = vnoExp
& ~ visSomeExp(X27)
& X27 = vreduce(X12)
& ! [X28,X29,X30] : X12 != vabs(X28,X29,X30)
& X4 = vapp(X12,X13) )
| epred2_2(X19,X4) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],['reduce-INV']),c_0_36]) ).
fof(c_0_41,plain,
! [X15] :
( ( ~ visValue(ve1)
& vtcheck(vempty,ve1,X15) )
=> ? [X35] : vreduce(ve1) = vsomeExp(X35) ),
inference(fof_simplification,[status(thm)],['T-Progress-T-app-IH1']) ).
cnf(c_0_42,negated_conjecture,
( vapp(X1,X2) != vapp(ve1,ve2)
| X1 = esk16_3(vapp(ve1,ve2),esk1_0,vempty) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
fof(c_0_43,plain,
! [X4,X19] :
( epred2_2(X19,X4)
=> ( ? [X12,X27,X13] :
( X19 = vsomeExp(vapp(vgetSomeExp(X27),X13))
& visSomeExp(X27)
& X27 = vreduce(X12)
& ! [X28,X29,X30] : X12 != vabs(X28,X29,X30)
& X4 = vapp(X12,X13) )
| ? [X9,X10,X12,X26,X13] :
( X19 = vnoExp
& ~ visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| epred1_2(X19,X4) ) ),
inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_36]),c_0_39]) ).
fof(c_0_44,plain,
! [X68,X69,X73,X74,X75] :
( ( vreduce(X68) != X69
| epred2_2(X69,X68)
| X69 = vnoExp )
& ( vreduce(X68) != X69
| epred2_2(X69,X68)
| ~ visSomeExp(esk7_2(X68,X69)) )
& ( vreduce(X68) != X69
| epred2_2(X69,X68)
| esk7_2(X68,X69) = vreduce(esk6_2(X68,X69)) )
& ( vreduce(X68) != X69
| epred2_2(X69,X68)
| esk6_2(X68,X69) != vabs(X73,X74,X75) )
& ( vreduce(X68) != X69
| epred2_2(X69,X68)
| X68 = vapp(esk6_2(X68,X69),esk5_2(X68,X69)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_40])])])])])])]) ).
fof(c_0_45,plain,
! [X12,X4,X19,X27,X13] :
( ( ! [X28,X29,X30] : X12 != vabs(X28,X29,X30)
& X4 = vapp(X12,X13) )
=> ( ( visSomeExp(X27)
& X27 = vreduce(X12) )
=> ( X19 = vreduce(X4)
=> X19 = vsomeExp(vapp(vgetSomeExp(X27),X13)) ) ) ),
inference(fof_simplification,[status(thm)],[reduce5]) ).
fof(c_0_46,plain,
! [X145] :
( vreduce(ve1) = vsomeExp(esk20_0)
| visValue(ve1)
| ~ vtcheck(vempty,ve1,X145) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_41])])])])])]) ).
cnf(c_0_47,plain,
( ~ vtcheck(X1,X2,X3)
| X2 = vvar(esk11_3(X2,X3,X1))
| X2 = vabs(esk12_3(X2,X3,X1),esk14_3(X2,X3,X1),esk13_3(X2,X3,X1))
| vtcheck(X1,esk16_3(X2,X3,X1),varrow(esk18_3(X2,X3,X1),X3)) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_48,negated_conjecture,
esk16_3(vapp(ve1,ve2),esk1_0,vempty) = ve1,
inference(er,[status(thm)],[c_0_42]) ).
fof(c_0_49,plain,
! [X12,X13,X4] :
( X4 = vapp(X12,X13)
=> ~ visValue(X4) ),
inference(fof_simplification,[status(thm)],[isValue2]) ).
fof(c_0_50,plain,
! [X9,X4] :
( X4 = vvar(X9)
=> ~ visValue(X4) ),
inference(fof_simplification,[status(thm)],[isValue1]) ).
fof(c_0_51,plain,
! [X326,X327,X336,X337,X338] :
( ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X327 = vnoExp
| X327 = vsomeExp(vapp(vgetSomeExp(esk55_2(X326,X327)),esk56_2(X326,X327))) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X327 = vnoExp
| visSomeExp(esk55_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X327 = vnoExp
| esk55_2(X326,X327) = vreduce(esk54_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X327 = vnoExp
| esk54_2(X326,X327) != vabs(X336,X337,X338) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X327 = vnoExp
| X326 = vapp(esk54_2(X326,X327),esk56_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visValue(esk53_2(X326,X327))
| X327 = vsomeExp(vapp(vgetSomeExp(esk55_2(X326,X327)),esk56_2(X326,X327))) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visValue(esk53_2(X326,X327))
| visSomeExp(esk55_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visValue(esk53_2(X326,X327))
| esk55_2(X326,X327) = vreduce(esk54_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visValue(esk53_2(X326,X327))
| esk54_2(X326,X327) != vabs(X336,X337,X338) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visValue(esk53_2(X326,X327))
| X326 = vapp(esk54_2(X326,X327),esk56_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visSomeExp(esk52_2(X326,X327))
| X327 = vsomeExp(vapp(vgetSomeExp(esk55_2(X326,X327)),esk56_2(X326,X327))) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visSomeExp(esk52_2(X326,X327))
| visSomeExp(esk55_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visSomeExp(esk52_2(X326,X327))
| esk55_2(X326,X327) = vreduce(esk54_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visSomeExp(esk52_2(X326,X327))
| esk54_2(X326,X327) != vabs(X336,X337,X338) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| ~ visSomeExp(esk52_2(X326,X327))
| X326 = vapp(esk54_2(X326,X327),esk56_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| esk52_2(X326,X327) = vreduce(esk53_2(X326,X327))
| X327 = vsomeExp(vapp(vgetSomeExp(esk55_2(X326,X327)),esk56_2(X326,X327))) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| esk52_2(X326,X327) = vreduce(esk53_2(X326,X327))
| visSomeExp(esk55_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| esk52_2(X326,X327) = vreduce(esk53_2(X326,X327))
| esk55_2(X326,X327) = vreduce(esk54_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| esk52_2(X326,X327) = vreduce(esk53_2(X326,X327))
| esk54_2(X326,X327) != vabs(X336,X337,X338) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| esk52_2(X326,X327) = vreduce(esk53_2(X326,X327))
| X326 = vapp(esk54_2(X326,X327),esk56_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X326 = vapp(vabs(esk49_2(X326,X327),esk50_2(X326,X327),esk51_2(X326,X327)),esk53_2(X326,X327))
| X327 = vsomeExp(vapp(vgetSomeExp(esk55_2(X326,X327)),esk56_2(X326,X327))) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X326 = vapp(vabs(esk49_2(X326,X327),esk50_2(X326,X327),esk51_2(X326,X327)),esk53_2(X326,X327))
| visSomeExp(esk55_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X326 = vapp(vabs(esk49_2(X326,X327),esk50_2(X326,X327),esk51_2(X326,X327)),esk53_2(X326,X327))
| esk55_2(X326,X327) = vreduce(esk54_2(X326,X327)) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X326 = vapp(vabs(esk49_2(X326,X327),esk50_2(X326,X327),esk51_2(X326,X327)),esk53_2(X326,X327))
| esk54_2(X326,X327) != vabs(X336,X337,X338) )
& ( ~ epred2_2(X327,X326)
| epred1_2(X327,X326)
| X326 = vapp(vabs(esk49_2(X326,X327),esk50_2(X326,X327),esk51_2(X326,X327)),esk53_2(X326,X327))
| X326 = vapp(esk54_2(X326,X327),esk56_2(X326,X327)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])])])])])])]) ).
cnf(c_0_52,plain,
( vreduce(X2) != X1
| epred2_2(X1,X2)
| X1 = vnoExp ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
fof(c_0_53,plain,
! [X60,X61,X62,X63,X64] :
( X62 = vsomeExp(vapp(vgetSomeExp(X63),X64))
| X62 != vreduce(X61)
| ~ visSomeExp(X63)
| X63 != vreduce(X60)
| X60 = vabs(esk2_5(X60,X61,X62,X63,X64),esk3_5(X60,X61,X62,X63,X64),esk4_5(X60,X61,X62,X63,X64))
| X61 != vapp(X60,X64) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_45])])])]) ).
cnf(c_0_54,plain,
( ~ vtcheck(vempty,ve1,X1)
| vreduce(ve1) = vsomeExp(esk20_0)
| visValue(ve1) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
cnf(c_0_55,negated_conjecture,
vtcheck(vempty,ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0)),
inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_47,c_0_29]),c_0_30]),c_0_31]),c_0_48]) ).
fof(c_0_56,plain,
! [X41,X42] :
( visSomeExp(X42)
| X42 != vsomeExp(X41) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[isSomeExp1])])]) ).
fof(c_0_57,plain,
! [X147,X148,X149,X150] :
( visValue(X150)
| X150 != vabs(X147,X148,X149) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[isValue0])])]) ).
fof(c_0_58,plain,
! [X43,X44,X45] :
( X44 = X45
| X44 != vgetSomeExp(X43)
| X43 != vsomeExp(X45) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[getSomeExp0])])]) ).
fof(c_0_59,plain,
! [X111,X112,X113] :
( ~ visValue(X113)
| X113 != vapp(X111,X112) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_49])])]) ).
fof(c_0_60,plain,
! [X76,X77,X78] :
( X78 = vnoExp
| X78 != vreduce(X77)
| X77 != vvar(X76) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reduce0])])]) ).
fof(c_0_61,plain,
! [X151,X152] :
( ~ visValue(X152)
| X152 != vvar(X151) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_50])])]) ).
fof(c_0_62,plain,
! [X4] : vnoExp != vsomeExp(X4),
inference(fof_simplification,[status(thm)],['DIFF-noExp-someExp']) ).
fof(c_0_63,plain,
! [X4,X19] :
( epred1_2(X19,X4)
=> ( ? [X10,X26,X9,X13,X12] :
( X19 = vsomeExp(vsubst(X9,X13,X12))
& visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X13,X9,X10,X12,X26] :
( X19 = vsomeExp(vapp(vabs(X9,X10,X12),vgetSomeExp(X26)))
& visSomeExp(X26)
& X26 = vreduce(X13)
& X4 = vapp(vabs(X9,X10,X12),X13) )
| ? [X9,X10,X11] :
( X19 = vnoExp
& X4 = vabs(X9,X10,X11) )
| ? [X9] :
( X19 = vnoExp
& X4 = vvar(X9) ) ) ),
inference(split_equiv,[status(thm)],[c_0_39]) ).
cnf(c_0_64,plain,
( ~ epred2_2(X1,X2)
| epred1_2(X1,X2)
| X1 = vnoExp
| X1 = vsomeExp(vapp(vgetSomeExp(esk55_2(X2,X1)),esk56_2(X2,X1))) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_65,plain,
( epred2_2(vreduce(X1),X1)
| vreduce(X1) = vnoExp ),
inference(er,[status(thm)],[c_0_52]) ).
cnf(c_0_66,plain,
( X4 != vreduce(X1)
| ~ visSomeExp(X5)
| X5 != vreduce(X2)
| X1 != vapp(X2,X3)
| X4 = vsomeExp(vapp(vgetSomeExp(X5),X3))
| X2 = vabs(esk2_5(X2,X1,X4,X5,X3),esk3_5(X2,X1,X4,X5,X3),esk4_5(X2,X1,X4,X5,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
cnf(c_0_67,negated_conjecture,
( visValue(ve1)
| vreduce(ve1) = vsomeExp(esk20_0) ),
inference(spm,[status(thm)],[c_0_54,c_0_55]) ).
cnf(c_0_68,plain,
( X1 != vsomeExp(X2)
| visSomeExp(X1) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_69,plain,
( X1 != vabs(X2,X3,X4)
| visValue(X1) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
cnf(c_0_70,plain,
( X3 != vgetSomeExp(X1)
| X1 != vsomeExp(X2)
| X3 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_71,plain,
( ~ visValue(X1)
| X1 != vapp(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
cnf(c_0_72,plain,
( vreduce(X1) != X2
| epred2_2(X2,X1)
| X1 = vapp(esk6_2(X1,X2),esk5_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
fof(c_0_73,plain,
! [X79,X80,X81,X82,X83] :
( X83 = vnoExp
| X83 != vreduce(X82)
| X82 != vabs(X79,X80,X81) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reduce1])])]) ).
cnf(c_0_74,plain,
( X3 != vreduce(X1)
| X1 != vvar(X2)
| X3 = vnoExp ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_75,plain,
( ~ visValue(X1)
| X1 != vvar(X2) ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
fof(c_0_76,plain,
! [X40] : vnoExp != vsomeExp(X40),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_62])]) ).
fof(c_0_77,plain,
! [X310,X311] :
( ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X311 = vnoExp
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| visSomeExp(esk43_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X311 = vnoExp
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X311 = vsomeExp(vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),vgetSomeExp(esk43_2(X310,X311))))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| visSomeExp(esk43_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| esk43_2(X310,X311) = vreduce(esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X311 = vsomeExp(vsubst(esk46_2(X310,X311),esk47_2(X310,X311),esk48_2(X310,X311))) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| visValue(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| ~ visSomeExp(esk45_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| esk45_2(X310,X311) = vreduce(esk47_2(X310,X311)) )
& ( ~ epred1_2(X311,X310)
| X310 = vvar(esk35_2(X310,X311))
| X310 = vabs(esk36_2(X310,X311),esk37_2(X310,X311),esk38_2(X310,X311))
| X310 = vapp(vabs(esk40_2(X310,X311),esk41_2(X310,X311),esk42_2(X310,X311)),esk39_2(X310,X311))
| X310 = vapp(vabs(esk46_2(X310,X311),esk44_2(X310,X311),esk48_2(X310,X311)),esk47_2(X310,X311)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_63])])])])])]) ).
cnf(c_0_78,negated_conjecture,
vreduce(vapp(ve1,ve2)) != vsomeExp(X1),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_79,plain,
( epred1_2(vreduce(X1),X1)
| vreduce(X1) = vnoExp
| vsomeExp(vapp(vgetSomeExp(esk55_2(X1,vreduce(X1))),esk56_2(X1,vreduce(X1)))) = vreduce(X1) ),
inference(spm,[status(thm)],[c_0_64,c_0_65]) ).
cnf(c_0_80,negated_conjecture,
( X1 != vreduce(X4)
| X2 != vsomeExp(esk20_0)
| X4 != vapp(ve1,X3)
| visValue(ve1)
| X1 = vsomeExp(vapp(vgetSomeExp(X2),X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_67]),c_0_68]),c_0_69]) ).
cnf(c_0_81,plain,
( X2 != vsomeExp(X1)
| X1 = vgetSomeExp(X2) ),
inference(er,[status(thm)],[c_0_70]) ).
cnf(c_0_82,plain,
~ visValue(vapp(X1,X2)),
inference(er,[status(thm)],[c_0_71]) ).
cnf(c_0_83,plain,
( epred2_2(vreduce(X1),X1)
| vapp(esk6_2(X1,vreduce(X1)),esk5_2(X1,vreduce(X1))) = X1 ),
inference(er,[status(thm)],[c_0_72]) ).
cnf(c_0_84,plain,
( X5 != vreduce(X1)
| X1 != vabs(X2,X3,X4)
| X5 = vnoExp ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_85,negated_conjecture,
( vvar(X2) != ve1
| X1 != vsomeExp(esk20_0)
| X1 = vnoExp ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_67]),c_0_75]) ).
cnf(c_0_86,plain,
vnoExp != vsomeExp(X1),
inference(split_conjunct,[status(thm)],[c_0_76]) ).
cnf(c_0_87,plain,
( ~ epred1_2(X1,X2)
| X1 = vnoExp
| X1 = vnoExp
| X1 = vsomeExp(vapp(vabs(esk40_2(X2,X1),esk41_2(X2,X1),esk42_2(X2,X1)),vgetSomeExp(esk43_2(X2,X1))))
| X1 = vsomeExp(vsubst(esk46_2(X2,X1),esk47_2(X2,X1),esk48_2(X2,X1))) ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_88,negated_conjecture,
( vreduce(vapp(ve1,ve2)) != vreduce(X1)
| epred1_2(vreduce(X1),X1)
| vreduce(X1) = vnoExp ),
inference(spm,[status(thm)],[c_0_78,c_0_79]) ).
cnf(c_0_89,negated_conjecture,
( X2 != vsomeExp(esk20_0)
| X1 != vapp(ve1,X3)
| visValue(ve1)
| vreduce(X1) = vsomeExp(vapp(vgetSomeExp(X2),X3)) ),
inference(er,[status(thm)],[c_0_80]) ).
cnf(c_0_90,plain,
vgetSomeExp(vsomeExp(X1)) = X1,
inference(er,[status(thm)],[c_0_81]) ).
cnf(c_0_91,plain,
( ~ epred2_2(X1,X2)
| epred1_2(X1,X2)
| X2 = vapp(vabs(esk49_2(X2,X1),esk50_2(X2,X1),esk51_2(X2,X1)),esk53_2(X2,X1))
| X1 = vsomeExp(vapp(vgetSomeExp(esk55_2(X2,X1)),esk56_2(X2,X1))) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_92,plain,
( ~ visValue(X1)
| epred2_2(vreduce(X1),X1) ),
inference(spm,[status(thm)],[c_0_82,c_0_83]) ).
cnf(c_0_93,plain,
( ~ epred2_2(X2,X1)
| epred1_2(X2,X1)
| X2 = vnoExp
| X1 = vapp(esk54_2(X1,X2),esk56_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_94,plain,
( X1 != vabs(X2,X3,X4)
| vreduce(X1) = vnoExp ),
inference(er,[status(thm)],[c_0_84]) ).
cnf(c_0_95,negated_conjecture,
vvar(X1) != ve1,
inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_85]),c_0_86]) ).
cnf(c_0_96,plain,
( ~ epred1_2(X1,X2)
| X1 = vsomeExp(vapp(vabs(esk40_2(X2,X1),esk41_2(X2,X1),esk42_2(X2,X1)),vgetSomeExp(esk43_2(X2,X1))))
| X1 = vsomeExp(vsubst(esk46_2(X2,X1),esk47_2(X2,X1),esk48_2(X2,X1)))
| X1 = vnoExp ),
inference(cn,[status(thm)],[c_0_87]) ).
cnf(c_0_97,negated_conjecture,
( epred1_2(vreduce(vapp(ve1,ve2)),vapp(ve1,ve2))
| vreduce(vapp(ve1,ve2)) = vnoExp ),
inference(er,[status(thm)],[c_0_88]) ).
cnf(c_0_98,negated_conjecture,
( X1 != vapp(ve1,X2)
| visValue(ve1)
| vreduce(X1) = vsomeExp(vapp(esk20_0,X2)) ),
inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_89]),c_0_90]) ).
fof(c_0_99,plain,
! [X10,X26,X4,X19,X9,X13,X12] :
( X4 = vapp(vabs(X9,X10,X12),X13)
=> ( ( visValue(X13)
& ~ visSomeExp(X26)
& X26 = vreduce(X13) )
=> ( X19 = vreduce(X4)
=> X19 = vsomeExp(vsubst(X9,X13,X12)) ) ) ),
inference(fof_simplification,[status(thm)],[reduce3]) ).
fof(c_0_100,plain,
! [X46,X47,X48,X49,X50,X51,X52] :
( X48 = vsomeExp(vapp(vabs(X49,X50,X51),vgetSomeExp(X52)))
| X48 != vreduce(X47)
| ~ visSomeExp(X52)
| X52 != vreduce(X46)
| X47 != vapp(vabs(X49,X50,X51),X46) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[reduce2])])]) ).
cnf(c_0_101,plain,
( ~ visValue(X1)
| epred1_2(vreduce(X1),X1)
| vsomeExp(vapp(vgetSomeExp(esk55_2(X1,vreduce(X1))),esk56_2(X1,vreduce(X1)))) = vreduce(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_92]),c_0_71]) ).
cnf(c_0_102,plain,
( ~ visValue(X1)
| epred1_2(vreduce(X1),X1)
| vreduce(X1) = vnoExp ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_93,c_0_92]),c_0_71]) ).
cnf(c_0_103,plain,
vreduce(vabs(X1,X2,X3)) = vnoExp,
inference(er,[status(thm)],[c_0_94]) ).
cnf(c_0_104,negated_conjecture,
( vapp(esk16_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty),esk17_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty)) = ve1
| vabs(esk12_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty),esk14_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty),esk13_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty)) = ve1 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_55]),c_0_95]) ).
cnf(c_0_105,plain,
vreduce(vapp(ve1,ve2)) = vnoExp,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_97]),c_0_78]),c_0_78]) ).
cnf(c_0_106,negated_conjecture,
( visValue(ve1)
| vreduce(vapp(ve1,X1)) = vsomeExp(vapp(esk20_0,X1)) ),
inference(er,[status(thm)],[c_0_98]) ).
fof(c_0_107,plain,
! [X15] :
( ( ~ visValue(ve2)
& vtcheck(vempty,ve2,X15) )
=> ? [X35] : vreduce(ve2) = vsomeExp(X35) ),
inference(fof_simplification,[status(thm)],['T-Progress-T-app-IH2']) ).
cnf(c_0_108,plain,
( ~ vtcheck(X1,X2,X3)
| X2 = vvar(esk11_3(X2,X3,X1))
| X2 = vabs(esk12_3(X2,X3,X1),esk14_3(X2,X3,X1),esk13_3(X2,X3,X1))
| vtcheck(X1,esk17_3(X2,X3,X1),esk18_3(X2,X3,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
fof(c_0_109,plain,
! [X53,X54,X55,X56,X57,X58,X59] :
( X56 = vsomeExp(vsubst(X57,X58,X59))
| X56 != vreduce(X55)
| ~ visValue(X58)
| visSomeExp(X54)
| X54 != vreduce(X58)
| X55 != vapp(vabs(X57,X53,X59),X58) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_99])])]) ).
cnf(c_0_110,plain,
( X7 != vreduce(X1)
| ~ visSomeExp(X6)
| X6 != vreduce(X5)
| X1 != vapp(vabs(X2,X3,X4),X5)
| X7 = vsomeExp(vapp(vabs(X2,X3,X4),vgetSomeExp(X6))) ),
inference(split_conjunct,[status(thm)],[c_0_100]) ).
cnf(c_0_111,plain,
( ~ visValue(X1)
| epred1_2(vreduce(X1),X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_101]),c_0_102]) ).
cnf(c_0_112,negated_conjecture,
( vreduce(ve1) = vnoExp
| vapp(esk16_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty),esk17_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty)) = ve1 ),
inference(spm,[status(thm)],[c_0_103,c_0_104]) ).
cnf(c_0_113,plain,
visValue(ve1),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_105,c_0_106]),c_0_86]) ).
fof(c_0_114,plain,
! [X143] :
( vreduce(ve2) = vsomeExp(esk19_0)
| visValue(ve2)
| ~ vtcheck(vempty,ve2,X143) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_107])])])])])]) ).
cnf(c_0_115,negated_conjecture,
vtcheck(vempty,esk17_3(vapp(ve1,ve2),esk1_0,vempty),esk18_3(vapp(ve1,ve2),esk1_0,vempty)),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_108,c_0_29]),c_0_30]),c_0_31]) ).
cnf(c_0_116,plain,
( X7 != vreduce(X1)
| ~ visValue(X5)
| X6 != vreduce(X5)
| X1 != vapp(vabs(X2,X3,X4),X5)
| X7 = vsomeExp(vsubst(X2,X5,X4))
| visSomeExp(X6) ),
inference(split_conjunct,[status(thm)],[c_0_109]) ).
cnf(c_0_117,plain,
( ~ visSomeExp(X5)
| X1 != vnoExp
| X5 != vreduce(X6)
| vapp(vabs(X2,X3,X4),X6) != vapp(ve1,ve2)
| X1 = vsomeExp(vapp(vabs(X2,X3,X4),vgetSomeExp(X5))) ),
inference(spm,[status(thm)],[c_0_110,c_0_105]) ).
cnf(c_0_118,plain,
( epred1_2(vnoExp,ve1)
| vapp(esk16_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty),esk17_3(ve1,varrow(esk18_3(vapp(ve1,ve2),esk1_0,vempty),esk1_0),vempty)) = ve1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111,c_0_112]),c_0_113])]) ).
cnf(c_0_119,plain,
( ~ vtcheck(vempty,ve2,X1)
| vreduce(ve2) = vsomeExp(esk19_0)
| visValue(ve2) ),
inference(split_conjunct,[status(thm)],[c_0_114]) ).
cnf(c_0_120,negated_conjecture,
vtcheck(vempty,ve2,esk18_3(vapp(ve1,ve2),esk1_0,vempty)),
inference(rw,[status(thm)],[c_0_115,c_0_35]) ).
cnf(c_0_121,plain,
( ~ visValue(X3)
| X1 != vnoExp
| X5 != vreduce(X3)
| vapp(vabs(X2,X6,X4),X3) != vapp(ve1,ve2)
| visSomeExp(X5)
| X1 = vsomeExp(vsubst(X2,X3,X4)) ),
inference(spm,[status(thm)],[c_0_116,c_0_105]) ).
cnf(c_0_122,plain,
( ~ visSomeExp(X5)
| X5 != vreduce(X4)
| vapp(vabs(X1,X2,X3),X4) != vapp(ve1,ve2) ),
inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_117]),c_0_86]) ).
cnf(c_0_123,plain,
( ~ epred1_2(X1,X2)
| X2 = vvar(esk35_2(X2,X1))
| X2 = vabs(esk36_2(X2,X1),esk37_2(X2,X1),esk38_2(X2,X1))
| X1 = vsomeExp(vapp(vabs(esk40_2(X2,X1),esk41_2(X2,X1),esk42_2(X2,X1)),vgetSomeExp(esk43_2(X2,X1))))
| X1 = vsomeExp(vsubst(esk46_2(X2,X1),esk47_2(X2,X1),esk48_2(X2,X1))) ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_124,plain,
epred1_2(vnoExp,ve1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_118]),c_0_113])]) ).
cnf(c_0_125,negated_conjecture,
( visValue(ve2)
| vreduce(ve2) = vsomeExp(esk19_0) ),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_126,plain,
( ~ visValue(X5)
| X1 != vreduce(X5)
| vapp(vabs(X2,X3,X4),X5) != vapp(ve1,ve2)
| visSomeExp(X1) ),
inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_121]),c_0_86]) ).
cnf(c_0_127,plain,
( ~ visSomeExp(vreduce(X4))
| vapp(vabs(X1,X2,X3),X4) != vapp(ve1,ve2) ),
inference(er,[status(thm)],[c_0_122]) ).
cnf(c_0_128,plain,
vabs(esk36_2(ve1,vnoExp),esk37_2(ve1,vnoExp),esk38_2(ve1,vnoExp)) = ve1,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_124]),c_0_86]),c_0_86]),c_0_95]) ).
cnf(c_0_129,negated_conjecture,
( X4 != vsomeExp(esk19_0)
| vapp(vabs(X1,X2,X3),ve2) != vapp(ve1,ve2)
| visValue(ve2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_122,c_0_125]),c_0_68]) ).
cnf(c_0_130,plain,
( ~ visValue(X1)
| vapp(vabs(X2,X3,X4),X1) != vapp(ve1,ve2)
| visSomeExp(vreduce(X1)) ),
inference(er,[status(thm)],[c_0_126]) ).
cnf(c_0_131,plain,
( ~ visSomeExp(vreduce(X1))
| vapp(ve1,X1) != vapp(ve1,ve2) ),
inference(spm,[status(thm)],[c_0_127,c_0_128]) ).
cnf(c_0_132,negated_conjecture,
( vapp(vabs(X1,X2,X3),ve2) != vapp(ve1,ve2)
| visValue(ve2) ),
inference(er,[status(thm)],[c_0_129]) ).
cnf(c_0_133,plain,
( ~ visValue(X1)
| vapp(ve1,X1) != vapp(ve1,ve2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_128]),c_0_131]) ).
cnf(c_0_134,negated_conjecture,
visValue(ve2),
inference(spm,[status(thm)],[c_0_132,c_0_128]) ).
cnf(c_0_135,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_133]),c_0_134])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM148+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n014.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:18:34 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 249.34/36.78 % Version: 3.5.1
% 249.34/36.78 % Preprocessing class: FSLSSMSSSSSNFFN.
% 249.34/36.78 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 249.34/36.78 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 249.34/36.78 % Starting new_bool_3 with 300s (1) cores
% 249.34/36.78 % Starting new_bool_1 with 300s (1) cores
% 249.34/36.78 % Starting sh5l with 300s (1) cores
% 249.34/36.78 % sh5l with pid 92326 completed with status 0
% 249.34/36.78 % Result found by sh5l
% 249.34/36.78 % Preprocessing class: FSLSSMSSSSSNFFN.
% 249.34/36.78 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 249.34/36.78 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 249.34/36.78 % Starting new_bool_3 with 300s (1) cores
% 249.34/36.78 % Starting new_bool_1 with 300s (1) cores
% 249.34/36.78 % Starting sh5l with 300s (1) cores
% 249.34/36.78 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 249.34/36.78 % SinE strategy is gf500_gu_R04_F100_L20000
% 249.34/36.78 % Search class: FGHSF-FSLF32-MFFFFFNN
% 249.34/36.78 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 249.34/36.78 % Starting SubtermCWHack with 31s (1) cores
% 249.34/36.78 % SubtermCWHack with pid 92340 completed with status 8
% 249.34/36.78 % Starting G-E--_107_B00_00_F1_PI_AE_Q4_CS_SP_PS_S08BN with 181s (1) cores
% 249.34/36.78 % G-E--_107_B00_00_F1_PI_AE_Q4_CS_SP_PS_S08BN with pid 92346 completed with status 0
% 249.34/36.78 % Result found by G-E--_107_B00_00_F1_PI_AE_Q4_CS_SP_PS_S08BN
% 249.34/36.78 % Preprocessing class: FSLSSMSSSSSNFFN.
% 249.34/36.78 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 249.34/36.78 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 249.34/36.78 % Starting new_bool_3 with 300s (1) cores
% 249.34/36.78 % Starting new_bool_1 with 300s (1) cores
% 249.34/36.78 % Starting sh5l with 300s (1) cores
% 249.34/36.78 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 249.34/36.78 % SinE strategy is gf500_gu_R04_F100_L20000
% 249.34/36.78 % Search class: FGHSF-FSLF32-MFFFFFNN
% 249.34/36.78 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 249.34/36.78 % Starting SubtermCWHack with 31s (1) cores
% 249.34/36.78 % SubtermCWHack with pid 92340 completed with status 8
% 249.34/36.78 % Starting G-E--_107_B00_00_F1_PI_AE_Q4_CS_SP_PS_S08BN with 181s (1) cores
% 249.34/36.78 % Preprocessing time : 0.008 s
% 249.34/36.78 % Presaturation interreduction done
% 249.34/36.78
% 249.34/36.78 % Proof found!
% 249.34/36.79 % SZS status Theorem
% 249.34/36.79 % SZS output start CNFRefutation
% See solution above
% 249.34/36.79 % Parsed axioms : 59
% 249.34/36.79 % Removed by relevancy pruning/SinE : 1
% 249.34/36.79 % Initial clauses : 424
% 249.34/36.79 % Removed in clause preprocessing : 13
% 249.34/36.79 % Initial clauses in saturation : 411
% 249.34/36.79 % Processed clauses : 10303
% 249.34/36.79 % ...of these trivial : 382
% 249.34/36.79 % ...subsumed : 5352
% 249.34/36.79 % ...remaining for further processing : 4569
% 249.34/36.79 % Other redundant clauses eliminated : 666
% 249.34/36.79 % Clauses deleted for lack of memory : 0
% 249.34/36.79 % Backward-subsumed : 708
% 249.34/36.79 % Backward-rewritten : 812
% 249.34/36.79 % Generated clauses : 152471
% 249.34/36.79 % ...of the previous two non-redundant : 135148
% 249.34/36.79 % ...aggressively subsumed : 0
% 249.34/36.79 % Contextual simplify-reflections : 288
% 249.34/36.79 % Paramodulations : 150672
% 249.34/36.79 % Factorizations : 0
% 249.34/36.79 % NegExts : 0
% 249.34/36.79 % Equation resolutions : 1798
% 249.34/36.79 % Disequality decompositions : 0
% 249.34/36.79 % Total rewrite steps : 26899
% 249.34/36.79 % ...of those cached : 21356
% 249.34/36.79 % Propositional unsat checks : 0
% 249.34/36.79 % Propositional check models : 0
% 249.34/36.79 % Propositional check unsatisfiable : 0
% 249.34/36.79 % Propositional clauses : 0
% 249.34/36.79 % Propositional clauses after purity: 0
% 249.34/36.79 % Propositional unsat core size : 0
% 249.34/36.79 % Propositional preprocessing time : 0.000
% 249.34/36.79 % Propositional encoding time : 0.000
% 249.34/36.79 % Propositional solver time : 0.000
% 249.34/36.79 % Success case prop preproc time : 0.000
% 249.34/36.79 % Success case prop encoding time : 0.000
% 249.34/36.79 % Success case prop solver time : 0.000
% 249.34/36.79 % Current number of processed clauses : 2652
% 249.34/36.79 % Positive orientable unit clauses : 534
% 249.34/36.79 % Positive unorientable unit clauses: 2
% 249.34/36.79 % Negative unit clauses : 340
% 249.34/36.79 % Non-unit-clauses : 1776
% 249.34/36.79 % Current number of unprocessed clauses: 123584
% 249.34/36.79 % ...number of literals in the above : 539135
% 249.34/36.79 % Current number of archived formulas : 0
% 249.34/36.79 % Current number of archived clauses : 1896
% 249.34/36.79 % Clause-clause subsumption calls (NU) : 872404
% 249.34/36.79 % Rec. Clause-clause subsumption calls : 442135
% 249.34/36.79 % Non-unit clause-clause subsumptions : 4000
% 249.34/36.79 % Unit Clause-clause subsumption calls : 65027
% 249.34/36.79 % Rewrite failures with RHS unbound : 330
% 249.34/36.79 % BW rewrite match attempts : 20134
% 249.34/36.79 % BW rewrite match successes : 110
% 249.34/36.79 % Condensation attempts : 0
% 249.34/36.79 % Condensation successes : 0
% 249.34/36.79 % Termbank termtop insertions : 4819365
% 249.34/36.79 % Search garbage collected termcells : 4020
% 249.34/36.79
% 249.34/36.79 % -------------------------------------------------
% 249.34/36.79 % User time : 34.400 s
% 249.34/36.79 % System time : 1.431 s
% 249.34/36.79 % Total time : 35.831 s
% 249.34/36.79 % Maximum resident set size: 4776 pages
% 249.34/36.79
% 249.34/36.79 % -------------------------------------------------
% 249.34/36.79 % User time : 34.402 s
% 249.34/36.79 % System time : 1.437 s
% 249.34/36.79 % Total time : 35.839 s
% 249.34/36.79 % Maximum resident set size: 4864 pages
% 249.34/36.79 % E exiting
%------------------------------------------------------------------------------