%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM273_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.BGyMgoZy6h true
% Computer : n004.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:23 PM UTC 2026
% Result : Theorem 13.56s 2.54s
% Output : Refutation 13.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM273_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.BGyMgoZy6h true
% 0.16/0.35 % Computer : n004.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Mon May 4 20:07:17 EDT 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 % Running portfolio for 300 s
% 0.16/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.35 % Number of cores: 8
% 0.16/0.35 % Python version: Python 3.6.8
% 0.16/0.36 % Running in FO mode
% 0.54/0.64 % Total configuration time : 435
% 0.54/0.64 % Estimated wc time : 1092
% 0.54/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.69 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.71 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.73 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 13.56/2.54 % Solved by fo/fo1_av.sh.
% 13.56/2.54 % done 2256 iterations in 1.789s
% 13.56/2.54 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 13.56/2.54 % SZS output start Refutation
% 13.56/2.54 thf(vUnOpT_type, type, vUnOpT: $tType).
% 13.56/2.54 thf(vExp_type, type, vExp: $tType).
% 13.56/2.54 thf(vOptAType_type, type, vOptAType: $tType).
% 13.56/2.54 thf(vATMap_type, type, vATMap: $tType).
% 13.56/2.54 thf(vAnsMap_type, type, vAnsMap: $tType).
% 13.56/2.54 thf(vAType_type, type, vAType: $tType).
% 13.56/2.54 thf(vOptExp_type, type, vOptExp: $tType).
% 13.56/2.54 thf(vAval_type, type, vAval: $tType).
% 13.56/2.54 thf(vBinOpT_type, type, vBinOpT: $tType).
% 13.56/2.54 thf(vQID_type, type, vQID: $tType).
% 13.56/2.54 thf(sk__394_type, type, sk__394: vAType).
% 13.56/2.54 thf(vbinop_type, type, vbinop: vExp > vBinOpT > vExp > vExp).
% 13.56/2.54 thf(vunop_type, type, vunop: vUnOpT > vExp > vExp).
% 13.56/2.54 thf(sk__16_type, type, sk__16: vExp > vUnOpT).
% 13.56/2.54 thf(sk__137_type, type, sk__137: vExp > vExp).
% 13.56/2.54 thf(sk__135_type, type, sk__135: vExp > vAval).
% 13.56/2.54 thf(vgetExpValue_type, type, vgetExpValue: vExp > vAval).
% 13.56/2.54 thf(sk__19_type, type, sk__19: vExp > vBinOpT).
% 13.56/2.54 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 13.56/2.54 thf(sk__392_type, type, sk__392: vAnsMap).
% 13.56/2.54 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 13.56/2.54 thf(sk__21_type, type, sk__21: vExp > vQID).
% 13.56/2.54 thf(sk__17_type, type, sk__17: vExp > vExp).
% 13.56/2.54 thf(sk__393_type, type, sk__393: vUnOpT).
% 13.56/2.54 thf(vsomeExp_type, type, vsomeExp: vExp > vOptExp).
% 13.56/2.54 thf(sk__22_type, type, sk__22: vExp > vAval).
% 13.56/2.54 thf(sk__20_type, type, sk__20: vExp > vExp).
% 13.56/2.54 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 13.56/2.54 thf(sk__395_type, type, sk__395: vExp).
% 13.56/2.54 thf(vevalUnOp_type, type, vevalUnOp: vUnOpT > vAval > vOptExp).
% 13.56/2.54 thf(vconstant_type, type, vconstant: vAval > vExp).
% 13.56/2.54 thf(ve1_type, type, ve1: vExp).
% 13.56/2.54 thf(vqvar_type, type, vqvar: vQID > vExp).
% 13.56/2.54 thf(vnotop_type, type, vnotop: vUnOpT).
% 13.56/2.54 thf(vexpIsValue_type, type, vexpIsValue: vExp > $o).
% 13.56/2.54 thf(vreduceExp_type, type, vreduceExp: vExp > vAnsMap > vOptExp).
% 13.56/2.54 thf(sk__18_type, type, sk__18: vExp > vExp).
% 13.56/2.54 thf('dom-UnOpT', axiom, (![VX:vUnOpT]: ( ( VX ) = ( vnotop ) ))).
% 13.56/2.54 thf(zip_derived_cl85, plain, (![X0 : vUnOpT]: ((X0) = (vnotop))),
% 13.56/2.54 inference('cnf', [status(esa)], [dom-UnOpT])).
% 13.56/2.54 thf(zip_derived_cl85, plain, (![X0 : vUnOpT]: ((X0) = (vnotop))),
% 13.56/2.54 inference('cnf', [status(esa)], [dom-UnOpT])).
% 13.56/2.54 thf(zip_derived_cl927, plain, (![X0 : vUnOpT, X1 : vUnOpT]: ((X1) = (X0))),
% 13.56/2.54 inference('s_sup+', [status(thm)], [zip_derived_cl85, zip_derived_cl85])).
% 13.56/2.54 thf('reduceExpPreservation-unop-expIsValue-True', conjecture,
% 13.56/2.54 (![Vam:vAnsMap,Vuot:vUnOpT,Vat:vAType,Ver:vExp]:
% 13.56/2.54 ( ( ( vexpIsValue @ ve1 ) &
% 13.56/2.54 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vunop @ Vuot @ ve1 ) ) =
% 13.56/2.54 ( vsomeAType @ Vat ) ) &
% 13.56/2.54 ( ( vreduceExp @ ( vunop @ Vuot @ ve1 ) @ Vam ) = ( vsomeExp @ Ver ) ) ) =>
% 13.56/2.54 ( ( vecheck @ ( vtypeAM @ Vam ) @ Ver ) = ( vsomeAType @ Vat ) ) ))).
% 13.56/2.54 thf(zf_stmt_0, negated_conjecture,
% 13.56/2.54 (~( ![Vam:vAnsMap,Vuot:vUnOpT,Vat:vAType,Ver:vExp]:
% 13.56/2.54 ( ( ( vexpIsValue @ ve1 ) &
% 13.56/2.54 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vunop @ Vuot @ ve1 ) ) =
% 13.56/2.54 ( vsomeAType @ Vat ) ) &
% 13.56/2.54 ( ( vreduceExp @ ( vunop @ Vuot @ ve1 ) @ Vam ) =
% 13.56/2.54 ( vsomeExp @ Ver ) ) ) =>
% 13.56/2.54 ( ( vecheck @ ( vtypeAM @ Vam ) @ Ver ) = ( vsomeAType @ Vat ) ) ) )),
% 13.56/2.54 inference('cnf.neg', [status(esa)],
% 13.56/2.54 [reduceExpPreservation-unop-expIsValue-True])).
% 13.56/2.54 thf(zip_derived_cl924, plain,
% 13.56/2.54 (((vreduceExp @ (vunop @ sk__393 @ ve1) @ sk__392) = (vsomeExp @ sk__395))),
% 13.56/2.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.56/2.54 thf(zip_derived_cl995, plain,
% 13.56/2.54 (![X0 : vUnOpT]:
% 13.56/2.54 ((vreduceExp @ (vunop @ X0 @ ve1) @ sk__392) = (vsomeExp @ sk__395))),
% 13.56/2.54 inference('s_sup+', [status(thm)], [zip_derived_cl927, zip_derived_cl924])).
% 13.56/2.54 thf('reduceExp-8', axiom,
% 13.56/2.54 (![Ve1:vExp,Vop:vUnOpT,Vam:vAnsMap]:
% 13.56/2.54 ( ( vexpIsValue @ Ve1 ) =>
% 13.56/2.54 ( ( vreduceExp @ ( vunop @ Vop @ Ve1 ) @ Vam ) =
% 13.56/2.54 ( vevalUnOp @ Vop @ ( vgetExpValue @ Ve1 ) ) ) ))).
% 13.56/2.54 thf(zip_derived_cl496, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vUnOpT, X2 : vAnsMap]:
% 13.56/2.54 (~ (vexpIsValue @ X0)
% 13.56/2.54 | ((vreduceExp @ (vunop @ X1 @ X0) @ X2)
% 13.56/2.54 = (vevalUnOp @ X1 @ (vgetExpValue @ X0))))),
% 13.56/2.54 inference('cnf', [status(esa)], [reduceExp-8])).
% 13.56/2.54 thf('dom-Exp', axiom,
% 13.56/2.54 (![VX:vExp]:
% 13.56/2.54 ( ( ?[VUnOpT0:vUnOpT,VExp0:vExp]: ( ( VX ) = ( vunop @ VUnOpT0 @ VExp0 ) ) ) |
% 13.56/2.54 ( ?[VExp0:vExp,VBinOpT0:vBinOpT,VExp1:vExp]:
% 13.56/2.54 ( ( VX ) = ( vbinop @ VExp0 @ VBinOpT0 @ VExp1 ) ) ) |
% 13.56/2.54 ( ?[VQID0:vQID]: ( ( VX ) = ( vqvar @ VQID0 ) ) ) |
% 13.56/2.54 ( ?[VAval0:vAval]: ( ( VX ) = ( vconstant @ VAval0 ) ) ) ))).
% 13.56/2.54 thf(zip_derived_cl34, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (((X0) = (vunop @ (sk__16 @ X0) @ (sk__17 @ X0)))
% 13.56/2.54 | ((X0) = (vbinop @ (sk__18 @ X0) @ (sk__19 @ X0) @ (sk__20 @ X0)))
% 13.56/2.54 | ((X0) = (vqvar @ (sk__21 @ X0)))
% 13.56/2.54 | ((X0) = (vconstant @ (sk__22 @ X0))))),
% 13.56/2.54 inference('cnf', [status(esa)], [dom-Exp])).
% 13.56/2.54 thf('expIsValue-false-INV', axiom,
% 13.56/2.54 (![VExp0:vExp]:
% 13.56/2.54 ( ( ~( vexpIsValue @ VExp0 ) ) =>
% 13.56/2.54 ( ?[Ve:vExp]:
% 13.56/2.54 ( ( ( VExp0 ) = ( Ve ) ) &
% 13.56/2.54 ( ![VwildcardName00:vAval]:
% 13.56/2.54 ( ( Ve ) != ( vconstant @ VwildcardName00 ) ) ) ) ) ))).
% 13.56/2.54 thf(zip_derived_cl371, plain,
% 13.56/2.54 (![X0 : vExp]: (((X0) = (sk__137 @ X0)) | (vexpIsValue @ X0))),
% 13.56/2.54 inference('cnf', [status(esa)], [expIsValue-false-INV])).
% 13.56/2.54 thf(zip_derived_cl925, plain, ( (vexpIsValue @ ve1)),
% 13.56/2.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.56/2.54 thf('expIsValue-1', axiom,
% 13.56/2.54 (![Ve:vExp]:
% 13.56/2.54 ( ( ![VwildcardName00:vAval]:
% 13.56/2.54 ( ( Ve ) != ( vconstant @ VwildcardName00 ) ) ) =>
% 13.56/2.54 ( ~( vexpIsValue @ Ve ) ) ))).
% 13.56/2.54 thf(zip_derived_cl369, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__135 @ X0))))),
% 13.56/2.54 inference('cnf', [status(esa)], [expIsValue-1])).
% 13.56/2.54 thf(zip_derived_cl372, plain,
% 13.56/2.54 (![X0 : vAval, X1 : vExp]:
% 13.56/2.54 (((sk__137 @ X1) != (vconstant @ X0)) | (vexpIsValue @ X1))),
% 13.56/2.54 inference('cnf', [status(esa)], [expIsValue-false-INV])).
% 13.56/2.54 thf(zip_derived_cl2303, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vExp]:
% 13.56/2.54 (~ (vexpIsValue @ X0) | ((sk__137 @ X1) != (X0)) | (vexpIsValue @ X1))),
% 13.56/2.54 inference('s_sup-', [status(thm)], [zip_derived_cl369, zip_derived_cl372])).
% 13.56/2.54 thf(zip_derived_cl2353, plain,
% 13.56/2.54 (![X0 : vExp]: (((sk__137 @ X0) != (ve1)) | (vexpIsValue @ X0))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl925, zip_derived_cl2303])).
% 13.56/2.54 thf(zip_derived_cl2354, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 ( (vexpIsValue @ X0) | ((X0) != (ve1)) | (vexpIsValue @ X0))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl371, zip_derived_cl2353])).
% 13.56/2.54 thf(zip_derived_cl2355, plain,
% 13.56/2.54 (![X0 : vExp]: (((X0) != (ve1)) | (vexpIsValue @ X0))),
% 13.56/2.54 inference('simplify', [status(thm)], [zip_derived_cl2354])).
% 13.56/2.54 thf(zip_derived_cl369, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__135 @ X0))))),
% 13.56/2.54 inference('cnf', [status(esa)], [expIsValue-1])).
% 13.56/2.54 thf('DIFF-constant-binop', axiom,
% 13.56/2.54 (![VAval0:vAval,VExp0:vExp,VBinOpT0:vBinOpT,VExp1:vExp]:
% 13.56/2.54 ( ( vconstant @ VAval0 ) != ( vbinop @ VExp0 @ VBinOpT0 @ VExp1 ) ))).
% 13.56/2.54 thf(zip_derived_cl43, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vBinOpT, X2 : vExp, X3 : vAval]:
% 13.56/2.54 ((vconstant @ X3) != (vbinop @ X0 @ X1 @ X2))),
% 13.56/2.54 inference('cnf', [status(esa)], [DIFF-constant-binop])).
% 13.56/2.54 thf(zip_derived_cl2308, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vExp, X2 : vBinOpT, X3 : vExp]:
% 13.56/2.54 (~ (vexpIsValue @ X0) | ((X0) != (vbinop @ X3 @ X2 @ X1)))),
% 13.56/2.54 inference('s_sup-', [status(thm)], [zip_derived_cl369, zip_derived_cl43])).
% 13.56/2.54 thf(zip_derived_cl2350, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vBinOpT, X2 : vExp]:
% 13.56/2.54 ~ (vexpIsValue @ (vbinop @ X2 @ X1 @ X0))),
% 13.56/2.54 inference('eq_res', [status(thm)], [zip_derived_cl2308])).
% 13.56/2.54 thf(zip_derived_cl2359, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vBinOpT, X2 : vExp]:
% 13.56/2.54 ((vbinop @ X2 @ X1 @ X0) != (ve1))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl2355, zip_derived_cl2350])).
% 13.56/2.54 thf(zip_derived_cl2361, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (((X0) = (vconstant @ (sk__22 @ X0)))
% 13.56/2.54 | ((X0) = (vqvar @ (sk__21 @ X0)))
% 13.56/2.54 | ((X0) = (vunop @ (sk__16 @ X0) @ (sk__17 @ X0)))
% 13.56/2.54 | ((X0) != (ve1)))),
% 13.56/2.54 inference('s_sup-', [status(thm)], [zip_derived_cl34, zip_derived_cl2359])).
% 13.56/2.54 thf(zip_derived_cl2355, plain,
% 13.56/2.54 (![X0 : vExp]: (((X0) != (ve1)) | (vexpIsValue @ X0))),
% 13.56/2.54 inference('simplify', [status(thm)], [zip_derived_cl2354])).
% 13.56/2.54 thf(zip_derived_cl369, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__135 @ X0))))),
% 13.56/2.54 inference('cnf', [status(esa)], [expIsValue-1])).
% 13.56/2.54 thf('DIFF-constant-unop', axiom,
% 13.56/2.54 (![VAval0:vAval,VUnOpT0:vUnOpT,VExp0:vExp]:
% 13.56/2.54 ( ( vconstant @ VAval0 ) != ( vunop @ VUnOpT0 @ VExp0 ) ))).
% 13.56/2.54 thf(zip_derived_cl44, plain,
% 13.56/2.54 (![X0 : vUnOpT, X1 : vExp, X2 : vAval]:
% 13.56/2.54 ((vconstant @ X2) != (vunop @ X0 @ X1))),
% 13.56/2.54 inference('cnf', [status(esa)], [DIFF-constant-unop])).
% 13.56/2.54 thf(zip_derived_cl2309, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vExp, X2 : vUnOpT]:
% 13.56/2.54 (~ (vexpIsValue @ X0) | ((X0) != (vunop @ X2 @ X1)))),
% 13.56/2.54 inference('s_sup-', [status(thm)], [zip_derived_cl369, zip_derived_cl44])).
% 13.56/2.54 thf(zip_derived_cl2312, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vUnOpT]: ~ (vexpIsValue @ (vunop @ X1 @ X0))),
% 13.56/2.54 inference('eq_res', [status(thm)], [zip_derived_cl2309])).
% 13.56/2.54 thf(zip_derived_cl2358, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vUnOpT]: ((vunop @ X1 @ X0) != (ve1))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl2355, zip_derived_cl2312])).
% 13.56/2.54 thf(zip_derived_cl8594, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (((X0) != (ve1))
% 13.56/2.54 | ((X0) = (vqvar @ (sk__21 @ X0)))
% 13.56/2.54 | ((X0) = (vconstant @ (sk__22 @ X0)))
% 13.56/2.54 | ((X0) != (ve1)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl2361, zip_derived_cl2358])).
% 13.56/2.54 thf(zip_derived_cl8599, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (((X0) = (vconstant @ (sk__22 @ X0)))
% 13.56/2.54 | ((X0) = (vqvar @ (sk__21 @ X0)))
% 13.56/2.54 | ((X0) != (ve1)))),
% 13.56/2.54 inference('simplify', [status(thm)], [zip_derived_cl8594])).
% 13.56/2.54 thf(zip_derived_cl2355, plain,
% 13.56/2.54 (![X0 : vExp]: (((X0) != (ve1)) | (vexpIsValue @ X0))),
% 13.56/2.54 inference('simplify', [status(thm)], [zip_derived_cl2354])).
% 13.56/2.54 thf(zip_derived_cl369, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (~ (vexpIsValue @ X0) | ((X0) = (vconstant @ (sk__135 @ X0))))),
% 13.56/2.54 inference('cnf', [status(esa)], [expIsValue-1])).
% 13.56/2.54 thf('DIFF-constant-qvar', axiom,
% 13.56/2.54 (![VAval0:vAval,VQID0:vQID]:
% 13.56/2.54 ( ( vconstant @ VAval0 ) != ( vqvar @ VQID0 ) ))).
% 13.56/2.54 thf(zip_derived_cl42, plain,
% 13.56/2.54 (![X0 : vQID, X1 : vAval]: ((vconstant @ X1) != (vqvar @ X0))),
% 13.56/2.54 inference('cnf', [status(esa)], [DIFF-constant-qvar])).
% 13.56/2.54 thf(zip_derived_cl2306, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vQID]: (~ (vexpIsValue @ X0) | ((X0) != (vqvar @ X1)))),
% 13.56/2.54 inference('s_sup-', [status(thm)], [zip_derived_cl369, zip_derived_cl42])).
% 13.56/2.54 thf(zip_derived_cl2357, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vQID]: (((X0) != (ve1)) | ((X0) != (vqvar @ X1)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl2355, zip_derived_cl2306])).
% 13.56/2.54 thf(zip_derived_cl8600, plain,
% 13.56/2.54 (![X0 : vExp]: (((X0) != (ve1)) | ((X0) = (vconstant @ (sk__22 @ X0))))),
% 13.56/2.54 inference('clc', [status(thm)], [zip_derived_cl8599, zip_derived_cl2357])).
% 13.56/2.54 thf('getExpValue-0', axiom,
% 13.56/2.54 (![Vav:vAval]: ( ( vgetExpValue @ ( vconstant @ Vav ) ) = ( Vav ) ))).
% 13.56/2.54 thf(zip_derived_cl170, plain,
% 13.56/2.54 (![X0 : vAval]: ((vgetExpValue @ (vconstant @ X0)) = (X0))),
% 13.56/2.54 inference('cnf', [status(esa)], [getExpValue-0])).
% 13.56/2.54 thf(zip_derived_cl8602, plain,
% 13.56/2.54 (![X0 : vExp]: (((X0) != (ve1)) | ((vgetExpValue @ X0) = (sk__22 @ X0)))),
% 13.56/2.54 inference('s_sup+', [status(thm)],
% 13.56/2.54 [zip_derived_cl8600, zip_derived_cl170])).
% 13.56/2.54 thf(zip_derived_cl927, plain, (![X0 : vUnOpT, X1 : vUnOpT]: ((X1) = (X0))),
% 13.56/2.54 inference('s_sup+', [status(thm)], [zip_derived_cl85, zip_derived_cl85])).
% 13.56/2.54 thf(zip_derived_cl926, plain,
% 13.56/2.54 (((vecheck @ (vtypeAM @ sk__392) @ (vunop @ sk__393 @ ve1))
% 13.56/2.54 = (vsomeAType @ sk__394))),
% 13.56/2.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.56/2.54 thf(zip_derived_cl997, plain,
% 13.56/2.54 (![X0 : vUnOpT]:
% 13.56/2.54 ((vecheck @ (vtypeAM @ sk__392) @ (vunop @ X0 @ ve1))
% 13.56/2.54 = (vsomeAType @ sk__394))),
% 13.56/2.54 inference('s_sup+', [status(thm)], [zip_derived_cl927, zip_derived_cl926])).
% 13.56/2.54 thf(zip_derived_cl8600, plain,
% 13.56/2.54 (![X0 : vExp]: (((X0) != (ve1)) | ((X0) = (vconstant @ (sk__22 @ X0))))),
% 13.56/2.54 inference('clc', [status(thm)], [zip_derived_cl8599, zip_derived_cl2357])).
% 13.56/2.54 thf(evalUnOpPreservation, axiom,
% 13.56/2.54 (![Veres:vExp,Vatm:vATMap,Vat:vAType,Vav:vAval,Vuot:vUnOpT]:
% 13.56/2.54 ( ( ( ( vecheck @ Vatm @ ( vunop @ Vuot @ ( vconstant @ Vav ) ) ) =
% 13.56/2.54 ( vsomeAType @ Vat ) ) &
% 13.56/2.54 ( ( vevalUnOp @ Vuot @ Vav ) = ( vsomeExp @ Veres ) ) ) =>
% 13.56/2.54 ( ( vecheck @ Vatm @ Veres ) = ( vsomeAType @ Vat ) ) ))).
% 13.56/2.54 thf(zip_derived_cl922, plain,
% 13.56/2.54 (![X0 : vAType, X1 : vATMap, X2 : vExp, X3 : vUnOpT, X4 : vAval]:
% 13.56/2.54 (((vecheck @ X1 @ X2) = (vsomeAType @ X0))
% 13.56/2.54 | ((vecheck @ X1 @ (vunop @ X3 @ (vconstant @ X4)))
% 13.56/2.54 != (vsomeAType @ X0))
% 13.56/2.54 | ((vevalUnOp @ X3 @ X4) != (vsomeExp @ X2)))),
% 13.56/2.54 inference('cnf', [status(esa)], [evalUnOpPreservation])).
% 13.56/2.54 thf(zip_derived_cl8617, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vAType, X2 : vUnOpT, X3 : vATMap, X4 : vExp]:
% 13.56/2.54 (((X0) != (ve1))
% 13.56/2.54 | ((vecheck @ X3 @ X4) = (vsomeAType @ X1))
% 13.56/2.54 | ((vecheck @ X3 @ (vunop @ X2 @ X0)) != (vsomeAType @ X1))
% 13.56/2.54 | ((vevalUnOp @ X2 @ (sk__22 @ X0)) != (vsomeExp @ X4)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl8600, zip_derived_cl922])).
% 13.56/2.54 thf(zip_derived_cl9465, plain,
% 13.56/2.54 (![X0 : vAType, X1 : vUnOpT, X2 : vExp]:
% 13.56/2.54 (((ve1) != (ve1))
% 13.56/2.54 | ((vecheck @ (vtypeAM @ sk__392) @ X2) = (vsomeAType @ X0))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ X0))
% 13.56/2.54 | ((vevalUnOp @ X1 @ (sk__22 @ ve1)) != (vsomeExp @ X2)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl997, zip_derived_cl8617])).
% 13.56/2.54 thf(zip_derived_cl9471, plain,
% 13.56/2.54 (![X0 : vAType, X1 : vUnOpT, X2 : vExp]:
% 13.56/2.54 (((vevalUnOp @ X1 @ (sk__22 @ ve1)) != (vsomeExp @ X2))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ X0))
% 13.56/2.54 | ((vecheck @ (vtypeAM @ sk__392) @ X2) = (vsomeAType @ X0)))),
% 13.56/2.54 inference('simplify', [status(thm)], [zip_derived_cl9465])).
% 13.56/2.54 thf(zip_derived_cl9473, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vUnOpT, X2 : vAType]:
% 13.56/2.54 (((ve1) != (ve1))
% 13.56/2.54 | ((vevalUnOp @ X1 @ (vgetExpValue @ ve1)) != (vsomeExp @ X0))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ X2))
% 13.56/2.54 | ((vecheck @ (vtypeAM @ sk__392) @ X0) = (vsomeAType @ X2)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl8602, zip_derived_cl9471])).
% 13.56/2.54 thf(zip_derived_cl9492, plain,
% 13.56/2.54 (![X0 : vExp, X1 : vUnOpT, X2 : vAType]:
% 13.56/2.54 (((vecheck @ (vtypeAM @ sk__392) @ X0) = (vsomeAType @ X2))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ X2))
% 13.56/2.54 | ((vevalUnOp @ X1 @ (vgetExpValue @ ve1)) != (vsomeExp @ X0)))),
% 13.56/2.54 inference('simplify', [status(thm)], [zip_derived_cl9473])).
% 13.56/2.54 thf(zip_derived_cl9494, plain,
% 13.56/2.54 (![X0 : vAnsMap, X1 : vUnOpT, X2 : vExp, X3 : vAType]:
% 13.56/2.54 (~ (vexpIsValue @ ve1)
% 13.56/2.54 | ((vecheck @ (vtypeAM @ sk__392) @ X2) = (vsomeAType @ X3))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ X3))
% 13.56/2.54 | ((vreduceExp @ (vunop @ X1 @ ve1) @ X0) != (vsomeExp @ X2)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl496, zip_derived_cl9492])).
% 13.56/2.54 thf(zip_derived_cl925, plain, ( (vexpIsValue @ ve1)),
% 13.56/2.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.56/2.54 thf(zip_derived_cl9513, plain,
% 13.56/2.54 (![X0 : vAnsMap, X1 : vUnOpT, X2 : vExp, X3 : vAType]:
% 13.56/2.54 (((vecheck @ (vtypeAM @ sk__392) @ X2) = (vsomeAType @ X3))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ X3))
% 13.56/2.54 | ((vreduceExp @ (vunop @ X1 @ ve1) @ X0) != (vsomeExp @ X2)))),
% 13.56/2.54 inference('demod', [status(thm)], [zip_derived_cl9494, zip_derived_cl925])).
% 13.56/2.54 thf(zip_derived_cl9517, plain,
% 13.56/2.54 (![X0 : vExp, X2 : vAType]:
% 13.56/2.54 (((vecheck @ (vtypeAM @ sk__392) @ X0) = (vsomeAType @ X2))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ X2))
% 13.56/2.54 | ((vsomeExp @ sk__395) != (vsomeExp @ X0)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl995, zip_derived_cl9513])).
% 13.56/2.54 thf(zip_derived_cl9569, plain,
% 13.56/2.54 (![X0 : vExp]:
% 13.56/2.54 (((vsomeExp @ sk__395) != (vsomeExp @ X0))
% 13.56/2.54 | ((vecheck @ (vtypeAM @ sk__392) @ X0) = (vsomeAType @ sk__394)))),
% 13.56/2.54 inference('eq_res', [status(thm)], [zip_derived_cl9517])).
% 13.56/2.54 thf(zip_derived_cl923, plain,
% 13.56/2.54 (((vecheck @ (vtypeAM @ sk__392) @ sk__395) != (vsomeAType @ sk__394))),
% 13.56/2.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.56/2.54 thf(zip_derived_cl9585, plain,
% 13.56/2.54 ((((vsomeExp @ sk__395) != (vsomeExp @ sk__395))
% 13.56/2.54 | ((vsomeAType @ sk__394) != (vsomeAType @ sk__394)))),
% 13.56/2.54 inference('s_sup-', [status(thm)],
% 13.56/2.54 [zip_derived_cl9569, zip_derived_cl923])).
% 13.56/2.54 thf(zip_derived_cl9592, plain, ($false),
% 13.56/2.54 inference('simplify', [status(thm)], [zip_derived_cl9585])).
% 13.56/2.54
% 13.56/2.54 % SZS output end Refutation
% 13.56/2.54
% 13.56/2.54
% 13.56/2.54 % Terminating...
% 14.30/2.64 % Runner terminated.
% 14.30/2.66 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------