%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM276_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.hWjMCFFDgL true
% 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 06:23:24 PM UTC 2026
% Result : Theorem 31.87s 5.13s
% Output : Refutation 31.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM276_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.hWjMCFFDgL true
% 0.15/0.34 % Computer : n009.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 20:10:11 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 % Running portfolio for 300 s
% 0.15/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Number of cores: 8
% 0.15/0.35 % Python version: Python 3.6.8
% 0.15/0.35 % Running in FO mode
% 0.53/0.64 % Total configuration time : 435
% 0.53/0.64 % Estimated wc time : 1092
% 0.53/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.53/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 31.87/5.13 % Solved by fo/fo3_bce.sh.
% 31.87/5.13 % BCE start: 693
% 31.87/5.13 % BCE eliminated: 0
% 31.87/5.13 % PE start: 693
% 31.87/5.13 logic: eq
% 31.87/5.13 % PE eliminated: -286
% 31.87/5.13 % done 2026 iterations in 4.388s
% 31.87/5.13 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 31.87/5.13 % SZS output start Refutation
% 31.87/5.13 thf(vOptExp_type, type, vOptExp: $tType).
% 31.87/5.13 thf(vExp_type, type, vExp: $tType).
% 31.87/5.13 thf(vBinOpT_type, type, vBinOpT: $tType).
% 31.87/5.13 thf(vOptAType_type, type, vOptAType: $tType).
% 31.87/5.13 thf(vATMap_type, type, vATMap: $tType).
% 31.87/5.13 thf(vAnsMap_type, type, vAnsMap: $tType).
% 31.87/5.13 thf(vAType_type, type, vAType: $tType).
% 31.87/5.13 thf(vAval_type, type, vAval: $tType).
% 31.87/5.13 thf(vUnOpT_type, type, vUnOpT: $tType).
% 31.87/5.13 thf(vQID_type, type, vQID: $tType).
% 31.87/5.13 thf(sk__312_type, type, sk__312: vBinOpT).
% 31.87/5.13 thf(vgetExpValue_type, type, vgetExpValue: vExp > vAval).
% 31.87/5.13 thf(vbinop_type, type, vbinop: vExp > vBinOpT > vExp > vExp).
% 31.87/5.13 thf(vunop_type, type, vunop: vUnOpT > vExp > vExp).
% 31.87/5.13 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 31.87/5.13 thf(ve2_type, type, ve2: vExp).
% 31.87/5.13 thf(vreduceExp_type, type, vreduceExp: vExp > vAnsMap > vOptExp).
% 31.87/5.13 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 31.87/5.13 thf(visSomeAType_type, type, visSomeAType: vOptAType > $o).
% 31.87/5.13 thf(vnoExp_type, type, vnoExp: vOptExp).
% 31.87/5.13 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 31.87/5.13 thf(vsomeExp_type, type, vsomeExp: vExp > vOptExp).
% 31.87/5.13 thf(vgetAType_type, type, vgetAType: vOptAType > vAType).
% 31.87/5.13 thf(sk__18_type, type, sk__18: vExp > vAval).
% 31.87/5.13 thf(sk__14_type, type, sk__14: vExp > vExp).
% 31.87/5.13 thf(vexpIsValue_type, type, vexpIsValue: vExp > $o).
% 31.87/5.13 thf(sk__313_type, type, sk__313: vAnsMap).
% 31.87/5.13 thf(vconstant_type, type, vconstant: vAval > vExp).
% 31.87/5.13 thf(sk__15_type, type, sk__15: vExp > vBinOpT).
% 31.87/5.13 thf(sk__13_type, type, sk__13: vExp > vExp).
% 31.87/5.13 thf(sk__49_type, type, sk__49: vOptAType > vAType).
% 31.87/5.13 thf(vevalBinOp_type, type, vevalBinOp: vBinOpT > vAval > vAval > vOptExp).
% 31.87/5.13 thf(sk__33_type, type, sk__33: vOptExp > vExp).
% 31.87/5.13 thf(sk__69_type, type, sk__69: vExp > vAval).
% 31.87/5.13 thf(ve1_type, type, ve1: vExp).
% 31.87/5.13 thf(vqvar_type, type, vqvar: vQID > vExp).
% 31.87/5.13 thf(sk__16_type, type, sk__16: vExp > vExp).
% 31.87/5.13 thf(sk__12_type, type, sk__12: vExp > vUnOpT).
% 31.87/5.13 thf(sk__314_type, type, sk__314: vAType).
% 31.87/5.13 thf(sk__311_type, type, sk__311: vAval > vAval > vBinOpT > vExp).
% 31.87/5.13 thf(sk__17_type, type, sk__17: vExp > vQID).
% 31.87/5.13 thf(sk__71_type, type, sk__71: vExp > vExp).
% 31.87/5.13 thf('dom-OptExp', axiom,
% 31.87/5.13 (![VX:vOptExp]:
% 31.87/5.13 ( ( ?[VExp0:vExp]: ( ( VX ) = ( vsomeExp @ VExp0 ) ) ) |
% 31.87/5.13 ( ( VX ) = ( vnoExp ) ) ))).
% 31.87/5.13 thf(zip_derived_cl61, plain,
% 31.87/5.13 (![X0 : vOptExp]:
% 31.87/5.13 (((X0) = (vsomeExp @ (sk__33 @ X0))) | ((X0) = (vnoExp)))),
% 31.87/5.13 inference('cnf', [status(esa)], [dom-OptExp])).
% 31.87/5.13 thf('reduceExpProgress-binop-expIsValue-True-expIsValue-True', conjecture,
% 31.87/5.13 (![Vbot:vBinOpT,Vam:vAnsMap,Vat:vAType]:
% 31.87/5.13 ( ( ( vexpIsValue @ ve2 ) & ( vexpIsValue @ ve1 ) &
% 31.87/5.13 ( ~( vexpIsValue @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) ) &
% 31.87/5.13 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) =
% 31.87/5.13 ( vsomeAType @ Vat ) ) ) =>
% 31.87/5.13 ( ?[Veres00:vExp]:
% 31.87/5.13 ( ( vreduceExp @ ( vbinop @ ve1 @ Vbot @ ve2 ) @ Vam ) =
% 31.87/5.13 ( vsomeExp @ Veres00 ) ) ) ))).
% 31.87/5.13 thf(zf_stmt_0, negated_conjecture,
% 31.87/5.13 (~( ![Vbot:vBinOpT,Vam:vAnsMap,Vat:vAType]:
% 31.87/5.13 ( ( ( vexpIsValue @ ve2 ) & ( vexpIsValue @ ve1 ) &
% 31.87/5.13 ( ~( vexpIsValue @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) ) &
% 31.87/5.13 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) =
% 31.87/5.13 ( vsomeAType @ Vat ) ) ) =>
% 31.87/5.13 ( ?[Veres00:vExp]:
% 31.87/5.13 ( ( vreduceExp @ ( vbinop @ ve1 @ Vbot @ ve2 ) @ Vam ) =
% 31.87/5.13 ( vsomeExp @ Veres00 ) ) ) ) )),
% 31.87/5.13 inference('cnf.neg', [status(esa)],
% 31.87/5.13 [reduceExpProgress-binop-expIsValue-True-expIsValue-True])).
% 31.87/5.13 thf(zip_derived_cl692, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 ((vreduceExp @ (vbinop @ ve1 @ sk__312 @ ve2) @ sk__313)
% 31.87/5.13 != (vsomeExp @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.87/5.13 thf(zip_derived_cl10256, plain,
% 31.87/5.13 (![X0 : vOptExp]:
% 31.87/5.13 (((vreduceExp @ (vbinop @ ve1 @ sk__312 @ ve2) @ sk__313) != (X0))
% 31.87/5.13 | ((X0) = (vnoExp)))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl692])).
% 31.87/5.13 thf(zip_derived_cl10258, plain,
% 31.87/5.13 (((vreduceExp @ (vbinop @ ve1 @ sk__312 @ ve2) @ sk__313) = (vnoExp))),
% 31.87/5.13 inference('eq_res', [status(thm)], [zip_derived_cl10256])).
% 31.87/5.13 thf('reduceExp-3', axiom,
% 31.87/5.13 (![Ve1:vExp,Ve2:vExp,Vop:vBinOpT,Vam:vAnsMap]:
% 31.87/5.13 ( ( ( vexpIsValue @ Ve1 ) & ( vexpIsValue @ Ve2 ) ) =>
% 31.87/5.13 ( ( vreduceExp @ ( vbinop @ Ve1 @ Vop @ Ve2 ) @ Vam ) =
% 31.87/5.13 ( vevalBinOp @ Vop @ ( vgetExpValue @ Ve1 ) @ ( vgetExpValue @ Ve2 ) ) ) ))).
% 31.87/5.13 thf(zip_derived_cl291, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vExp, X2 : vBinOpT, X3 : vAnsMap]:
% 31.87/5.13 (~ (vexpIsValue @ X0)
% 31.87/5.13 | ~ (vexpIsValue @ X1)
% 31.87/5.13 | ((vreduceExp @ (vbinop @ X1 @ X2 @ X0) @ X3)
% 31.87/5.13 = (vevalBinOp @ X2 @ (vgetExpValue @ X1) @ (vgetExpValue @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [reduceExp-3])).
% 31.87/5.13 thf(zip_derived_cl688, plain,
% 31.87/5.13 (((vecheck @ (vtypeAM @ sk__313) @ (vbinop @ ve1 @ sk__312 @ ve2))
% 31.87/5.13 = (vsomeAType @ sk__314))),
% 31.87/5.13 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.87/5.13 thf('expIsValue-1', axiom,
% 31.87/5.13 (![Ve:vExp]:
% 31.87/5.13 ( ( ![VwildcardName00:vAval]:
% 31.87/5.13 ( ( Ve ) != ( vconstant @ VwildcardName00 ) ) ) =>
% 31.87/5.13 ( ~( vexpIsValue @ Ve ) ) ))).
% 31.87/5.13 thf(zip_derived_cl183, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__69 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-1])).
% 31.87/5.13 thf('getExpValue-0', axiom,
% 31.87/5.13 (![Vav:vAval]: ( ( vgetExpValue @ ( vconstant @ Vav ) ) = ( Vav ) ))).
% 31.87/5.13 thf(zip_derived_cl120, plain,
% 31.87/5.13 (![X0 : vAval]: ((vgetExpValue @ (vconstant @ X0)) = (X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [getExpValue-0])).
% 31.87/5.13 thf(zip_derived_cl10870, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((vgetExpValue @ X0) = (sk__69 @ X0)) | ~ (vexpIsValue @ X0))),
% 31.87/5.13 inference('sup+', [status(thm)], [zip_derived_cl183, zip_derived_cl120])).
% 31.87/5.13 thf(zip_derived_cl183, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__69 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-1])).
% 31.87/5.13 thf(zip_derived_cl11015, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) = (vconstant @ (vgetExpValue @ X0)))
% 31.87/5.13 | ~ (vexpIsValue @ X0)
% 31.87/5.13 | ~ (vexpIsValue @ X0))),
% 31.87/5.13 inference('sup+', [status(thm)], [zip_derived_cl10870, zip_derived_cl183])).
% 31.87/5.13 thf(zip_derived_cl11018, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (vgetExpValue @ X0))))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl11015])).
% 31.87/5.13 thf('isSomeAType-true-INV', axiom,
% 31.87/5.13 (![VOptAType0:vOptAType]:
% 31.87/5.13 ( ( visSomeAType @ VOptAType0 ) =>
% 31.87/5.13 ( ?[VwildcardName0:vAType]:
% 31.87/5.13 ( ( VOptAType0 ) = ( vsomeAType @ VwildcardName0 ) ) ) ))).
% 31.87/5.13 thf(zip_derived_cl139, plain,
% 31.87/5.13 (![X0 : vOptAType]:
% 31.87/5.13 (((X0) = (vsomeAType @ (sk__49 @ X0))) | ~ (visSomeAType @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [isSomeAType-true-INV])).
% 31.87/5.13 thf('getAType-0', axiom,
% 31.87/5.13 (![Vatype:vAType]: ( ( vgetAType @ ( vsomeAType @ Vatype ) ) = ( Vatype ) ))).
% 31.87/5.13 thf(zip_derived_cl118, plain,
% 31.87/5.13 (![X0 : vAType]: ((vgetAType @ (vsomeAType @ X0)) = (X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [getAType-0])).
% 31.87/5.13 thf(zip_derived_cl10281, plain,
% 31.87/5.13 (![X0 : vOptAType]:
% 31.87/5.13 (((vgetAType @ X0) = (sk__49 @ X0)) | ~ (visSomeAType @ X0))),
% 31.87/5.13 inference('sup+', [status(thm)], [zip_derived_cl139, zip_derived_cl118])).
% 31.87/5.13 thf(zip_derived_cl139, plain,
% 31.87/5.13 (![X0 : vOptAType]:
% 31.87/5.13 (((X0) = (vsomeAType @ (sk__49 @ X0))) | ~ (visSomeAType @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [isSomeAType-true-INV])).
% 31.87/5.13 thf(zip_derived_cl11137, plain,
% 31.87/5.13 (![X0 : vOptAType]:
% 31.87/5.13 (((X0) = (vsomeAType @ (vgetAType @ X0)))
% 31.87/5.13 | ~ (visSomeAType @ X0)
% 31.87/5.13 | ~ (visSomeAType @ X0))),
% 31.87/5.13 inference('sup+', [status(thm)], [zip_derived_cl10281, zip_derived_cl139])).
% 31.87/5.13 thf(zip_derived_cl11141, plain,
% 31.87/5.13 (![X0 : vOptAType]:
% 31.87/5.13 (~ (visSomeAType @ X0) | ((X0) = (vsomeAType @ (vgetAType @ X0))))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl11137])).
% 31.87/5.13 thf('dom-Exp', axiom,
% 31.87/5.13 (![VX:vExp]:
% 31.87/5.13 ( ( ?[VUnOpT0:vUnOpT,VExp0:vExp]: ( ( VX ) = ( vunop @ VUnOpT0 @ VExp0 ) ) ) |
% 31.87/5.13 ( ?[VExp0:vExp,VBinOpT0:vBinOpT,VExp1:vExp]:
% 31.87/5.13 ( ( VX ) = ( vbinop @ VExp0 @ VBinOpT0 @ VExp1 ) ) ) |
% 31.87/5.13 ( ?[VQID0:vQID]: ( ( VX ) = ( vqvar @ VQID0 ) ) ) |
% 31.87/5.13 ( ?[VAval0:vAval]: ( ( VX ) = ( vconstant @ VAval0 ) ) ) ))).
% 31.87/5.13 thf(zip_derived_cl19, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) = (vunop @ (sk__12 @ X0) @ (sk__13 @ X0)))
% 31.87/5.13 | ((X0) = (vbinop @ (sk__14 @ X0) @ (sk__15 @ X0) @ (sk__16 @ X0)))
% 31.87/5.13 | ((X0) = (vqvar @ (sk__17 @ X0)))
% 31.87/5.13 | ((X0) = (vconstant @ (sk__18 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [dom-Exp])).
% 31.87/5.13 thf('expIsValue-false-INV', axiom,
% 31.87/5.13 (![VExp0:vExp]:
% 31.87/5.13 ( ( ~( vexpIsValue @ VExp0 ) ) =>
% 31.87/5.13 ( ?[Ve:vExp]:
% 31.87/5.13 ( ( ( VExp0 ) = ( Ve ) ) &
% 31.87/5.13 ( ![VwildcardName00:vAval]:
% 31.87/5.13 ( ( Ve ) != ( vconstant @ VwildcardName00 ) ) ) ) ) ))).
% 31.87/5.13 thf(zip_derived_cl185, plain,
% 31.87/5.13 (![X0 : vExp]: (((X0) = (sk__71 @ X0)) | (vexpIsValue @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-false-INV])).
% 31.87/5.13 thf(zip_derived_cl690, plain, ( (vexpIsValue @ ve1)),
% 31.87/5.13 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.87/5.13 thf(zip_derived_cl183, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__69 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-1])).
% 31.87/5.13 thf(zip_derived_cl186, plain,
% 31.87/5.13 (![X0 : vAval, X1 : vExp]:
% 31.87/5.13 (((sk__71 @ X1) != (vconstant @ X0)) | (vexpIsValue @ X1))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-false-INV])).
% 31.87/5.13 thf(zip_derived_cl10872, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vExp]:
% 31.87/5.13 (((sk__71 @ X1) != (X0)) | ~ (vexpIsValue @ X0) | (vexpIsValue @ X1))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl183, zip_derived_cl186])).
% 31.87/5.13 thf(zip_derived_cl10928, plain,
% 31.87/5.13 (![X0 : vExp]: ( (vexpIsValue @ X0) | ((sk__71 @ X0) != (ve1)))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl690, zip_derived_cl10872])).
% 31.87/5.13 thf(zip_derived_cl10930, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) != (ve1)) | (vexpIsValue @ X0) | (vexpIsValue @ X0))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl185, zip_derived_cl10928])).
% 31.87/5.13 thf(zip_derived_cl10931, plain,
% 31.87/5.13 (![X0 : vExp]: ( (vexpIsValue @ X0) | ((X0) != (ve1)))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl10930])).
% 31.87/5.13 thf(zip_derived_cl183, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__69 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-1])).
% 31.87/5.13 thf('DIFF-constant-binop', axiom,
% 31.87/5.13 (![VAval0:vAval,VExp0:vExp,VBinOpT0:vBinOpT,VExp1:vExp]:
% 31.87/5.13 ( ( vconstant @ VAval0 ) != ( vbinop @ VExp0 @ VBinOpT0 @ VExp1 ) ))).
% 31.87/5.13 thf(zip_derived_cl28, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vBinOpT, X2 : vExp, X3 : vAval]:
% 31.87/5.13 ((vconstant @ X3) != (vbinop @ X0 @ X1 @ X2))),
% 31.87/5.13 inference('cnf', [status(esa)], [DIFF-constant-binop])).
% 31.87/5.13 thf(zip_derived_cl10877, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vExp, X2 : vBinOpT, X3 : vExp]:
% 31.87/5.13 (((X0) != (vbinop @ X3 @ X2 @ X1)) | ~ (vexpIsValue @ X0))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl183, zip_derived_cl28])).
% 31.87/5.13 thf(zip_derived_cl10914, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vBinOpT, X2 : vExp]:
% 31.87/5.13 ~ (vexpIsValue @ (vbinop @ X2 @ X1 @ X0))),
% 31.87/5.13 inference('eq_res', [status(thm)], [zip_derived_cl10877])).
% 31.87/5.13 thf(zip_derived_cl10935, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vBinOpT, X2 : vExp]:
% 31.87/5.13 ((vbinop @ X2 @ X1 @ X0) != (ve1))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl10931, zip_derived_cl10914])).
% 31.87/5.13 thf(zip_derived_cl10941, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) != (ve1))
% 31.87/5.13 | ((X0) = (vconstant @ (sk__18 @ X0)))
% 31.87/5.13 | ((X0) = (vqvar @ (sk__17 @ X0)))
% 31.87/5.13 | ((X0) = (vunop @ (sk__12 @ X0) @ (sk__13 @ X0))))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl19, zip_derived_cl10935])).
% 31.87/5.13 thf(zip_derived_cl10931, plain,
% 31.87/5.13 (![X0 : vExp]: ( (vexpIsValue @ X0) | ((X0) != (ve1)))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl10930])).
% 31.87/5.13 thf(zip_derived_cl183, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__69 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-1])).
% 31.87/5.13 thf('DIFF-constant-unop', axiom,
% 31.87/5.13 (![VAval0:vAval,VUnOpT0:vUnOpT,VExp0:vExp]:
% 31.87/5.13 ( ( vconstant @ VAval0 ) != ( vunop @ VUnOpT0 @ VExp0 ) ))).
% 31.87/5.13 thf(zip_derived_cl29, plain,
% 31.87/5.13 (![X0 : vUnOpT, X1 : vExp, X2 : vAval]:
% 31.87/5.13 ((vconstant @ X2) != (vunop @ X0 @ X1))),
% 31.87/5.13 inference('cnf', [status(esa)], [DIFF-constant-unop])).
% 31.87/5.13 thf(zip_derived_cl10878, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vExp, X2 : vUnOpT]:
% 31.87/5.13 (((X0) != (vunop @ X2 @ X1)) | ~ (vexpIsValue @ X0))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl183, zip_derived_cl29])).
% 31.87/5.13 thf(zip_derived_cl10895, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vUnOpT]: ~ (vexpIsValue @ (vunop @ X1 @ X0))),
% 31.87/5.13 inference('eq_res', [status(thm)], [zip_derived_cl10878])).
% 31.87/5.13 thf(zip_derived_cl10934, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vUnOpT]: ((vunop @ X1 @ X0) != (ve1))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl10931, zip_derived_cl10895])).
% 31.87/5.13 thf(zip_derived_cl12788, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) != (ve1))
% 31.87/5.13 | ((X0) = (vqvar @ (sk__17 @ X0)))
% 31.87/5.13 | ((X0) = (vconstant @ (sk__18 @ X0)))
% 31.87/5.13 | ((X0) != (ve1)))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl10941, zip_derived_cl10934])).
% 31.87/5.13 thf(zip_derived_cl12794, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) = (vconstant @ (sk__18 @ X0)))
% 31.87/5.13 | ((X0) = (vqvar @ (sk__17 @ X0)))
% 31.87/5.13 | ((X0) != (ve1)))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl12788])).
% 31.87/5.13 thf(zip_derived_cl10931, plain,
% 31.87/5.13 (![X0 : vExp]: ( (vexpIsValue @ X0) | ((X0) != (ve1)))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl10930])).
% 31.87/5.13 thf(zip_derived_cl183, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__69 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-1])).
% 31.87/5.13 thf('DIFF-constant-qvar', axiom,
% 31.87/5.13 (![VAval0:vAval,VQID0:vQID]:
% 31.87/5.13 ( ( vconstant @ VAval0 ) != ( vqvar @ VQID0 ) ))).
% 31.87/5.13 thf(zip_derived_cl27, plain,
% 31.87/5.13 (![X0 : vQID, X1 : vAval]: ((vconstant @ X1) != (vqvar @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [DIFF-constant-qvar])).
% 31.87/5.13 thf(zip_derived_cl10875, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vQID]: (((X0) != (vqvar @ X1)) | ~ (vexpIsValue @ X0))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl183, zip_derived_cl27])).
% 31.87/5.13 thf(zip_derived_cl10933, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vQID]: (((X0) != (ve1)) | ((X0) != (vqvar @ X1)))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl10931, zip_derived_cl10875])).
% 31.87/5.13 thf(zip_derived_cl12817, plain,
% 31.87/5.13 (![X0 : vExp]: (((X0) != (ve1)) | ((X0) = (vconstant @ (sk__18 @ X0))))),
% 31.87/5.13 inference('clc', [status(thm)],
% 31.87/5.13 [zip_derived_cl12794, zip_derived_cl10933])).
% 31.87/5.13 thf(zip_derived_cl120, plain,
% 31.87/5.13 (![X0 : vAval]: ((vgetExpValue @ (vconstant @ X0)) = (X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [getExpValue-0])).
% 31.87/5.13 thf(zip_derived_cl12819, plain,
% 31.87/5.13 (![X0 : vExp]: (((vgetExpValue @ X0) = (sk__18 @ X0)) | ((X0) != (ve1)))),
% 31.87/5.13 inference('sup+', [status(thm)], [zip_derived_cl12817, zip_derived_cl120])).
% 31.87/5.13 thf(zip_derived_cl12819, plain,
% 31.87/5.13 (![X0 : vExp]: (((vgetExpValue @ X0) = (sk__18 @ X0)) | ((X0) != (ve1)))),
% 31.87/5.13 inference('sup+', [status(thm)], [zip_derived_cl12817, zip_derived_cl120])).
% 31.87/5.13 thf(zip_derived_cl12817, plain,
% 31.87/5.13 (![X0 : vExp]: (((X0) != (ve1)) | ((X0) = (vconstant @ (sk__18 @ X0))))),
% 31.87/5.13 inference('clc', [status(thm)],
% 31.87/5.13 [zip_derived_cl12794, zip_derived_cl10933])).
% 31.87/5.13 thf(zip_derived_cl12844, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) = (vconstant @ (vgetExpValue @ X0)))
% 31.87/5.13 | ((X0) != (ve1))
% 31.87/5.13 | ((X0) != (ve1)))),
% 31.87/5.13 inference('sup+', [status(thm)],
% 31.87/5.13 [zip_derived_cl12819, zip_derived_cl12817])).
% 31.87/5.13 thf(zip_derived_cl12845, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) != (ve1)) | ((X0) = (vconstant @ (vgetExpValue @ X0))))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl12844])).
% 31.87/5.13 thf(zip_derived_cl12817, plain,
% 31.87/5.13 (![X0 : vExp]: (((X0) != (ve1)) | ((X0) = (vconstant @ (sk__18 @ X0))))),
% 31.87/5.13 inference('clc', [status(thm)],
% 31.87/5.13 [zip_derived_cl12794, zip_derived_cl10933])).
% 31.87/5.13 thf(zip_derived_cl183, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__69 @ X0))))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-1])).
% 31.87/5.13 thf('EQ-constant', axiom,
% 31.87/5.13 (![VAval0:vAval,VAval1:vAval]:
% 31.87/5.13 ( ( ( vconstant @ VAval0 ) = ( vconstant @ VAval1 ) ) =>
% 31.87/5.13 ( ( VAval0 ) = ( VAval1 ) ) ))).
% 31.87/5.13 thf(zip_derived_cl20, plain,
% 31.87/5.13 (![X0 : vAval, X1 : vAval]:
% 31.87/5.13 (((X1) = (X0)) | ((vconstant @ X1) != (vconstant @ X0)))),
% 31.87/5.13 inference('cnf', [status(esa)], [EQ-constant])).
% 31.87/5.13 thf(zip_derived_cl10869, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vAval]:
% 31.87/5.13 (((vconstant @ X1) != (X0))
% 31.87/5.13 | ~ (vexpIsValue @ X0)
% 31.87/5.13 | ((X1) = (sk__69 @ X0)))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl183, zip_derived_cl20])).
% 31.87/5.13 thf(zip_derived_cl185, plain,
% 31.87/5.13 (![X0 : vExp]: (((X0) = (sk__71 @ X0)) | (vexpIsValue @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-false-INV])).
% 31.87/5.13 thf(zip_derived_cl186, plain,
% 31.87/5.13 (![X0 : vAval, X1 : vExp]:
% 31.87/5.13 (((sk__71 @ X1) != (vconstant @ X0)) | (vexpIsValue @ X1))),
% 31.87/5.13 inference('cnf', [status(esa)], [expIsValue-false-INV])).
% 31.87/5.13 thf(zip_derived_cl10264, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vAval]:
% 31.87/5.13 (((X0) != (vconstant @ X1))
% 31.87/5.13 | (vexpIsValue @ X0)
% 31.87/5.13 | (vexpIsValue @ X0))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl185, zip_derived_cl186])).
% 31.87/5.13 thf(zip_derived_cl10265, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vAval]:
% 31.87/5.13 ( (vexpIsValue @ X0) | ((X0) != (vconstant @ X1)))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl10264])).
% 31.87/5.13 thf(zip_derived_cl10967, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vAval]:
% 31.87/5.13 (((X1) = (sk__69 @ X0)) | ((vconstant @ X1) != (X0)))),
% 31.87/5.13 inference('clc', [status(thm)],
% 31.87/5.13 [zip_derived_cl10869, zip_derived_cl10265])).
% 31.87/5.13 thf(zip_derived_cl10970, plain,
% 31.87/5.13 (![X0 : vAval]: ((X0) = (sk__69 @ (vconstant @ X0)))),
% 31.87/5.13 inference('eq_res', [status(thm)], [zip_derived_cl10967])).
% 31.87/5.13 thf(zip_derived_cl12824, plain,
% 31.87/5.13 (![X0 : vExp]: (((sk__18 @ X0) = (sk__69 @ X0)) | ((X0) != (ve1)))),
% 31.87/5.13 inference('sup+', [status(thm)],
% 31.87/5.13 [zip_derived_cl12817, zip_derived_cl10970])).
% 31.87/5.13 thf(zip_derived_cl10970, plain,
% 31.87/5.13 (![X0 : vAval]: ((X0) = (sk__69 @ (vconstant @ X0)))),
% 31.87/5.13 inference('eq_res', [status(thm)], [zip_derived_cl10967])).
% 31.87/5.13 thf(zip_derived_cl12848, plain,
% 31.87/5.13 (![X0 : vAval]:
% 31.87/5.13 (((X0) = (sk__18 @ (vconstant @ X0))) | ((vconstant @ X0) != (ve1)))),
% 31.87/5.13 inference('sup+', [status(thm)],
% 31.87/5.13 [zip_derived_cl12824, zip_derived_cl10970])).
% 31.87/5.13 thf(zip_derived_cl12849, plain,
% 31.87/5.13 (![X0 : vAval]: (((X0) = (sk__18 @ ve1)) | ((vconstant @ X0) != (ve1)))),
% 31.87/5.13 inference('local_rewriting', [status(thm)], [zip_derived_cl12848])).
% 31.87/5.13 thf(zip_derived_cl12887, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) != (ve1))
% 31.87/5.13 | ((X0) != (ve1))
% 31.87/5.13 | ((vgetExpValue @ X0) = (sk__18 @ ve1)))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl12845, zip_derived_cl12849])).
% 31.87/5.13 thf(zip_derived_cl12902, plain,
% 31.87/5.13 (![X0 : vExp]: (((vgetExpValue @ X0) = (sk__18 @ ve1)) | ((X0) != (ve1)))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl12887])).
% 31.87/5.13 thf(zip_derived_cl12845, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) != (ve1)) | ((X0) = (vconstant @ (vgetExpValue @ X0))))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl12844])).
% 31.87/5.13 thf(zip_derived_cl12914, plain,
% 31.87/5.13 (![X0 : vExp]:
% 31.87/5.13 (((X0) = (vconstant @ (sk__18 @ ve1)))
% 31.87/5.13 | ((X0) != (ve1))
% 31.87/5.13 | ((X0) != (ve1)))),
% 31.87/5.13 inference('sup+', [status(thm)],
% 31.87/5.13 [zip_derived_cl12902, zip_derived_cl12845])).
% 31.87/5.13 thf(zip_derived_cl12919, plain,
% 31.87/5.13 (![X0 : vExp]: (((X0) != (ve1)) | ((X0) = (vconstant @ (sk__18 @ ve1))))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl12914])).
% 31.87/5.13 thf(zip_derived_cl12925, plain, (((ve1) = (vconstant @ (sk__18 @ ve1)))),
% 31.87/5.13 inference('eq_res', [status(thm)], [zip_derived_cl12919])).
% 31.87/5.13 thf(zip_derived_cl12944, plain,
% 31.87/5.13 ((((ve1) = (vconstant @ (vgetExpValue @ ve1))) | ((ve1) != (ve1)))),
% 31.87/5.13 inference('sup+', [status(thm)],
% 31.87/5.13 [zip_derived_cl12819, zip_derived_cl12925])).
% 31.87/5.13 thf(zip_derived_cl12946, plain,
% 31.87/5.13 (((ve1) = (vconstant @ (vgetExpValue @ ve1)))),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl12944])).
% 31.87/5.13 thf(evalBinOpProgress, axiom,
% 31.87/5.13 (![Vbot:vBinOpT,Va:vAval,Vatm:vATMap,Va1:vAval,Vat:vAType]:
% 31.87/5.13 ( ( ( vecheck @
% 31.87/5.13 Vatm @ ( vbinop @ ( vconstant @ Va ) @ Vbot @ ( vconstant @ Va1 ) ) ) =
% 31.87/5.13 ( vsomeAType @ Vat ) ) =>
% 31.87/5.13 ( ?[Veres:vExp]:
% 31.87/5.13 ( ( vevalBinOp @ Vbot @ Va @ Va1 ) = ( vsomeExp @ Veres ) ) ) ))).
% 31.87/5.13 thf(zip_derived_cl686, plain,
% 31.87/5.13 (![X0 : vAval, X1 : vAval, X2 : vBinOpT, X3 : vAType, X4 : vATMap]:
% 31.87/5.13 (((vevalBinOp @ X2 @ X1 @ X0) = (vsomeExp @ (sk__311 @ X0 @ X1 @ X2)))
% 31.87/5.13 | ((vecheck @ X4 @
% 31.87/5.13 (vbinop @ (vconstant @ X1) @ X2 @ (vconstant @ X0)))
% 31.87/5.13 != (vsomeAType @ X3)))),
% 31.87/5.13 inference('cnf', [status(esa)], [evalBinOpProgress])).
% 31.87/5.13 thf(zip_derived_cl12976, plain,
% 31.87/5.13 (![X0 : vAType, X1 : vAval, X2 : vBinOpT, X3 : vATMap]:
% 31.87/5.13 (((vecheck @ X3 @ (vbinop @ ve1 @ X2 @ (vconstant @ X1)))
% 31.87/5.13 != (vsomeAType @ X0))
% 31.87/5.13 | ((vevalBinOp @ X2 @ (vgetExpValue @ ve1) @ X1)
% 31.87/5.13 = (vsomeExp @ (sk__311 @ X1 @ (vgetExpValue @ ve1) @ X2))))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl12946, zip_derived_cl686])).
% 31.87/5.13 thf(zip_derived_cl14351, plain,
% 31.87/5.13 (![X0 : vOptAType, X1 : vAval, X2 : vBinOpT, X3 : vATMap]:
% 31.87/5.13 (((vecheck @ X3 @ (vbinop @ ve1 @ X2 @ (vconstant @ X1))) != (X0))
% 31.87/5.13 | ~ (visSomeAType @ X0)
% 31.87/5.13 | ((vevalBinOp @ X2 @ (vgetExpValue @ ve1) @ X1)
% 31.87/5.13 = (vsomeExp @ (sk__311 @ X1 @ (vgetExpValue @ ve1) @ X2))))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl11141, zip_derived_cl12976])).
% 31.87/5.13 thf(zip_derived_cl14470, plain,
% 31.87/5.13 (![X0 : vAval, X1 : vBinOpT, X2 : vATMap]:
% 31.87/5.13 (((vevalBinOp @ X1 @ (vgetExpValue @ ve1) @ X0)
% 31.87/5.13 = (vsomeExp @ (sk__311 @ X0 @ (vgetExpValue @ ve1) @ X1)))
% 31.87/5.13 | ~ (visSomeAType @
% 31.87/5.13 (vecheck @ X2 @ (vbinop @ ve1 @ X1 @ (vconstant @ X0)))))),
% 31.87/5.13 inference('eq_res', [status(thm)], [zip_derived_cl14351])).
% 31.87/5.13 thf(zip_derived_cl14474, plain,
% 31.87/5.13 (![X0 : vExp, X1 : vBinOpT, X2 : vATMap]:
% 31.87/5.13 (~ (visSomeAType @ (vecheck @ X2 @ (vbinop @ ve1 @ X1 @ X0)))
% 31.87/5.13 | ~ (vexpIsValue @ X0)
% 31.87/5.13 | ((vevalBinOp @ X1 @ (vgetExpValue @ ve1) @ (vgetExpValue @ X0))
% 31.87/5.13 = (vsomeExp @
% 31.87/5.13 (sk__311 @ (vgetExpValue @ X0) @ (vgetExpValue @ ve1) @ X1))))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl11018, zip_derived_cl14470])).
% 31.87/5.13 thf(zip_derived_cl17592, plain,
% 31.87/5.13 ((~ (visSomeAType @ (vsomeAType @ sk__314))
% 31.87/5.13 | ((vevalBinOp @ sk__312 @ (vgetExpValue @ ve1) @ (vgetExpValue @ ve2))
% 31.87/5.13 = (vsomeExp @
% 31.87/5.13 (sk__311 @ (vgetExpValue @ ve2) @ (vgetExpValue @ ve1) @ sk__312)))
% 31.87/5.13 | ~ (vexpIsValue @ ve2))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl688, zip_derived_cl14474])).
% 31.87/5.13 thf('isSomeAType-1', axiom,
% 31.87/5.13 (![VwildcardName0:vAType]:
% 31.87/5.13 ( visSomeAType @ ( vsomeAType @ VwildcardName0 ) ))).
% 31.87/5.13 thf(zip_derived_cl138, plain,
% 31.87/5.13 (![X0 : vAType]: (visSomeAType @ (vsomeAType @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [isSomeAType-1])).
% 31.87/5.13 thf(zip_derived_cl689, plain, ( (vexpIsValue @ ve2)),
% 31.87/5.13 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.87/5.13 thf(zip_derived_cl17596, plain,
% 31.87/5.13 (((vevalBinOp @ sk__312 @ (vgetExpValue @ ve1) @ (vgetExpValue @ ve2))
% 31.87/5.13 = (vsomeExp @
% 31.87/5.13 (sk__311 @ (vgetExpValue @ ve2) @ (vgetExpValue @ ve1) @ sk__312)))),
% 31.87/5.13 inference('demod', [status(thm)],
% 31.87/5.13 [zip_derived_cl17592, zip_derived_cl138, zip_derived_cl689])).
% 31.87/5.13 thf('DIFF-noExp-someExp', axiom,
% 31.87/5.13 (![VExp0:vExp]: ( ( vnoExp ) != ( vsomeExp @ VExp0 ) ))).
% 31.87/5.13 thf(zip_derived_cl63, plain, (![X0 : vExp]: ((vnoExp) != (vsomeExp @ X0))),
% 31.87/5.13 inference('cnf', [status(esa)], [DIFF-noExp-someExp])).
% 31.87/5.13 thf(zip_derived_cl17598, plain,
% 31.87/5.13 (((vnoExp)
% 31.87/5.13 != (vevalBinOp @ sk__312 @ (vgetExpValue @ ve1) @ (vgetExpValue @ ve2)))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl17596, zip_derived_cl63])).
% 31.87/5.13 thf(zip_derived_cl17634, plain,
% 31.87/5.13 (![X0 : vAnsMap]:
% 31.87/5.13 (((vnoExp) != (vreduceExp @ (vbinop @ ve1 @ sk__312 @ ve2) @ X0))
% 31.87/5.13 | ~ (vexpIsValue @ ve1)
% 31.87/5.13 | ~ (vexpIsValue @ ve2))),
% 31.87/5.13 inference('sup-', [status(thm)], [zip_derived_cl291, zip_derived_cl17598])).
% 31.87/5.13 thf(zip_derived_cl690, plain, ( (vexpIsValue @ ve1)),
% 31.87/5.13 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.87/5.13 thf(zip_derived_cl689, plain, ( (vexpIsValue @ ve2)),
% 31.87/5.13 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.87/5.13 thf(zip_derived_cl17636, plain,
% 31.87/5.13 (![X0 : vAnsMap]:
% 31.87/5.13 ((vnoExp) != (vreduceExp @ (vbinop @ ve1 @ sk__312 @ ve2) @ X0))),
% 31.87/5.13 inference('demod', [status(thm)],
% 31.87/5.13 [zip_derived_cl17634, zip_derived_cl690, zip_derived_cl689])).
% 31.87/5.13 thf(zip_derived_cl17642, plain, (((vnoExp) != (vnoExp))),
% 31.87/5.13 inference('sup-', [status(thm)],
% 31.87/5.13 [zip_derived_cl10258, zip_derived_cl17636])).
% 31.87/5.13 thf(zip_derived_cl17651, plain, ($false),
% 31.87/5.13 inference('simplify', [status(thm)], [zip_derived_cl17642])).
% 31.87/5.13
% 31.87/5.13 % SZS output end Refutation
% 31.87/5.13
% 31.87/5.13
% 31.87/5.13 % Terminating...
% 31.87/5.16 % Runner terminated.
% 31.87/5.18 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------