%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM246_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.EUCFUHe9qm true
% Computer : n016.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:21 PM UTC 2026
% Result : Theorem 251.86s 36.73s
% Output : Refutation 251.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM246_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.EUCFUHe9qm true
% 0.17/0.34 % Computer : n016.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Mon May 4 19:37:06 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 % Running portfolio for 300 s
% 0.17/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Number of cores: 8
% 0.17/0.34 % Python version: Python 3.6.8
% 0.17/0.34 % Running in FO mode
% 0.54/0.63 % Total configuration time : 435
% 0.54/0.63 % Estimated wc time : 1092
% 0.54/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.70 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.71 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.73 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 251.86/36.73 % Solved by fo/fo6_bce.sh.
% 251.86/36.73 % BCE start: 932
% 251.86/36.73 % BCE eliminated: 1
% 251.86/36.73 % PE start: 931
% 251.86/36.73 logic: eq
% 251.86/36.73 % PE eliminated: -317
% 251.86/36.73 % done 8289 iterations in 36.002s
% 251.86/36.73 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 251.86/36.73 % SZS output start Refutation
% 251.86/36.73 thf(vBinOpT_type, type, vBinOpT: $tType).
% 251.86/36.73 thf(vAval_type, type, vAval: $tType).
% 251.86/36.73 thf(vnat_type, type, vnat: $tType).
% 251.86/36.73 thf(vYN_type, type, vYN: $tType).
% 251.86/36.73 thf(vOptAType_type, type, vOptAType: $tType).
% 251.86/36.73 thf(vATMap_type, type, vATMap: $tType).
% 251.86/36.73 thf(vExp_type, type, vExp: $tType).
% 251.86/36.73 thf(vAType_type, type, vAType: $tType).
% 251.86/36.73 thf(vOptExp_type, type, vOptExp: $tType).
% 251.86/36.73 thf(vB_type, type, vB: vYN > vAval).
% 251.86/36.73 thf(sk__396_type, type, sk__396: vYN).
% 251.86/36.73 thf(vand_type, type, vand: vYN > vYN > vYN).
% 251.86/36.73 thf(vandop_type, type, vandop: vBinOpT).
% 251.86/36.73 thf(sk__395_type, type, sk__395: vAval).
% 251.86/36.73 thf(vbinop_type, type, vbinop: vExp > vBinOpT > vExp > vExp).
% 251.86/36.73 thf(sk__393_type, type, sk__393: vAval).
% 251.86/36.73 thf(sk__392_type, type, sk__392: vBinOpT).
% 251.86/36.73 thf(sk__398_type, type, sk__398: vAType).
% 251.86/36.73 thf(vsomeExp_type, type, vsomeExp: vExp > vOptExp).
% 251.86/36.73 thf(vgetAType_type, type, vgetAType: vOptAType > vAType).
% 251.86/36.73 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 251.86/36.73 thf(vaddop_type, type, vaddop: vBinOpT).
% 251.86/36.73 thf(vYesNo_type, type, vYesNo: vAType).
% 251.86/36.73 thf(vdivop_type, type, vdivop: vBinOpT).
% 251.86/36.73 thf(vltop_type, type, vltop: vBinOpT).
% 251.86/36.73 thf(vcheckBinOp_type, type, vcheckBinOp: vBinOpT > vAType > vAType > vOptAType).
% 251.86/36.73 thf(vconstant_type, type, vconstant: vAval > vExp).
% 251.86/36.73 thf(vevalBinOp_type, type, vevalBinOp: vBinOpT > vAval > vAval > vOptExp).
% 251.86/36.73 thf(vgtop_type, type, vgtop: vBinOpT).
% 251.86/36.73 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 251.86/36.73 thf(sk__394_type, type, sk__394: vATMap).
% 251.86/36.73 thf(sk__391_type, type, sk__391: vExp).
% 251.86/36.73 thf(sk__397_type, type, sk__397: vYN).
% 251.86/36.73 thf(vmulop_type, type, vmulop: vBinOpT).
% 251.86/36.73 thf(vNum_type, type, vNum: vnat > vAval).
% 251.86/36.73 thf(vsubop_type, type, vsubop: vBinOpT).
% 251.86/36.73 thf(visSomeAType_type, type, visSomeAType: vOptAType > $o).
% 251.86/36.73 thf('evalBinOpPreservation-andop-B-B', conjecture,
% 251.86/36.73 (![Veres:vExp,Vbot:vBinOpT,Va:vAval,Vatm:vATMap,Va1:vAval,Vb1:vYN,Vb2:vYN,
% 251.86/36.73 Vat:vAType]:
% 251.86/36.73 ( ( ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vaddop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vsubop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vmulop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vdivop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vgtop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vltop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ( Vbot ) = ( vandop ) ) & ( ( Va ) = ( vB @ Vb1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vB @ Vb2 ) ) &
% 251.86/36.73 ( ( vecheck @
% 251.86/36.73 Vatm @
% 251.86/36.73 ( vbinop @ ( vconstant @ Va ) @ Vbot @ ( vconstant @ Va1 ) ) ) =
% 251.86/36.73 ( vsomeAType @ Vat ) ) &
% 251.86/36.73 ( ( vevalBinOp @ Vbot @ Va @ Va1 ) = ( vsomeExp @ Veres ) ) ) =>
% 251.86/36.73 ( ( vecheck @ Vatm @ Veres ) = ( vsomeAType @ Vat ) ) ))).
% 251.86/36.73 thf(zf_stmt_0, negated_conjecture,
% 251.86/36.73 (~( ![Veres:vExp,Vbot:vBinOpT,Va:vAval,Vatm:vATMap,Va1:vAval,Vb1:vYN,
% 251.86/36.73 Vb2:vYN,Vat:vAType]:
% 251.86/36.73 ( ( ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vaddop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vsubop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vmulop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vdivop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vgtop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ![Vn1:vnat,Vn2:vnat]:
% 251.86/36.73 ( ~( ( ( Vbot ) = ( vltop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vNum @ Vn2 ) ) ) ) ) &
% 251.86/36.73 ( ( Vbot ) = ( vandop ) ) & ( ( Va ) = ( vB @ Vb1 ) ) &
% 251.86/36.73 ( ( Va1 ) = ( vB @ Vb2 ) ) &
% 251.86/36.73 ( ( vecheck @
% 251.86/36.73 Vatm @
% 251.86/36.73 ( vbinop @ ( vconstant @ Va ) @ Vbot @ ( vconstant @ Va1 ) ) ) =
% 251.86/36.73 ( vsomeAType @ Vat ) ) &
% 251.86/36.73 ( ( vevalBinOp @ Vbot @ Va @ Va1 ) = ( vsomeExp @ Veres ) ) ) =>
% 251.86/36.73 ( ( vecheck @ Vatm @ Veres ) = ( vsomeAType @ Vat ) ) ) )),
% 251.86/36.73 inference('cnf.neg', [status(esa)], [evalBinOpPreservation-andop-B-B])).
% 251.86/36.73 thf(zip_derived_cl929, plain, (((sk__393) = (vB @ sk__396))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf('echeck-0', axiom,
% 251.86/36.73 (![VwildcardName0:vATMap,Vn:vYN]:
% 251.86/36.73 ( ( vecheck @ VwildcardName0 @ ( vconstant @ ( vB @ Vn ) ) ) =
% 251.86/36.73 ( vsomeAType @ vYesNo ) ))).
% 251.86/36.73 thf(zip_derived_cl839, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vYN]:
% 251.86/36.73 ((vecheck @ X0 @ (vconstant @ (vB @ X1))) = (vsomeAType @ vYesNo))),
% 251.86/36.73 inference('cnf', [status(esa)], [echeck-0])).
% 251.86/36.73 thf(zip_derived_cl12964, plain,
% 251.86/36.73 (![X0 : vATMap]:
% 251.86/36.73 ((vecheck @ X0 @ (vconstant @ sk__393)) = (vsomeAType @ vYesNo))),
% 251.86/36.73 inference('s_sup+', [status(thm)], [zip_derived_cl929, zip_derived_cl839])).
% 251.86/36.73 thf(zip_derived_cl930, plain, (((sk__395) = (vB @ sk__397))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf(zip_derived_cl839, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vYN]:
% 251.86/36.73 ((vecheck @ X0 @ (vconstant @ (vB @ X1))) = (vsomeAType @ vYesNo))),
% 251.86/36.73 inference('cnf', [status(esa)], [echeck-0])).
% 251.86/36.73 thf(zip_derived_cl12965, plain,
% 251.86/36.73 (![X0 : vATMap]:
% 251.86/36.73 ((vecheck @ X0 @ (vconstant @ sk__395)) = (vsomeAType @ vYesNo))),
% 251.86/36.73 inference('s_sup+', [status(thm)], [zip_derived_cl930, zip_derived_cl839])).
% 251.86/36.73 thf('echeck-4', axiom,
% 251.86/36.73 (![Vatm:vATMap,Ve1:vExp,Ve2:vExp,Vop:vBinOpT]:
% 251.86/36.73 ( ( ( visSomeAType @ ( vecheck @ Vatm @ Ve1 ) ) &
% 251.86/36.73 ( visSomeAType @ ( vecheck @ Vatm @ Ve2 ) ) ) =>
% 251.86/36.73 ( ( vecheck @ Vatm @ ( vbinop @ Ve1 @ Vop @ Ve2 ) ) =
% 251.86/36.73 ( vcheckBinOp @
% 251.86/36.73 Vop @ ( vgetAType @ ( vecheck @ Vatm @ Ve1 ) ) @
% 251.86/36.73 ( vgetAType @ ( vecheck @ Vatm @ Ve2 ) ) ) ) ))).
% 251.86/36.73 thf(zip_derived_cl843, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vExp, X2 : vExp, X3 : vBinOpT]:
% 251.86/36.73 (~ (visSomeAType @ (vecheck @ X0 @ X1))
% 251.86/36.73 | ~ (visSomeAType @ (vecheck @ X0 @ X2))
% 251.86/36.73 | ((vecheck @ X0 @ (vbinop @ X2 @ X3 @ X1))
% 251.86/36.73 = (vcheckBinOp @ X3 @ (vgetAType @ (vecheck @ X0 @ X2)) @
% 251.86/36.73 (vgetAType @ (vecheck @ X0 @ X1)))))),
% 251.86/36.73 inference('cnf', [status(esa)], [echeck-4])).
% 251.86/36.73 thf(zip_derived_cl18354, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vExp, X2 : vBinOpT]:
% 251.86/36.73 (~ (visSomeAType @ (vsomeAType @ vYesNo))
% 251.86/36.73 | ~ (visSomeAType @ (vecheck @ X0 @ X1))
% 251.86/36.73 | ((vecheck @ X0 @ (vbinop @ X1 @ X2 @ (vconstant @ sk__395)))
% 251.86/36.73 = (vcheckBinOp @ X2 @ (vgetAType @ (vecheck @ X0 @ X1)) @
% 251.86/36.73 (vgetAType @ (vsomeAType @ vYesNo)))))),
% 251.86/36.73 inference('s_sup+', [status(thm)],
% 251.86/36.73 [zip_derived_cl12965, zip_derived_cl843])).
% 251.86/36.73 thf('isSomeAType-1', axiom,
% 251.86/36.73 (![VwildcardName0:vAType]:
% 251.86/36.73 ( visSomeAType @ ( vsomeAType @ VwildcardName0 ) ))).
% 251.86/36.73 thf(zip_derived_cl277, plain,
% 251.86/36.73 (![X0 : vAType]: (visSomeAType @ (vsomeAType @ X0))),
% 251.86/36.73 inference('cnf', [status(esa)], [isSomeAType-1])).
% 251.86/36.73 thf('getAType-0', axiom,
% 251.86/36.73 (![Vatype:vAType]: ( ( vgetAType @ ( vsomeAType @ Vatype ) ) = ( Vatype ) ))).
% 251.86/36.73 thf(zip_derived_cl164, plain,
% 251.86/36.73 (![X0 : vAType]: ((vgetAType @ (vsomeAType @ X0)) = (X0))),
% 251.86/36.73 inference('cnf', [status(esa)], [getAType-0])).
% 251.86/36.73 thf(zip_derived_cl18371, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vExp, X2 : vBinOpT]:
% 251.86/36.73 (~ (visSomeAType @ (vecheck @ X0 @ X1))
% 251.86/36.73 | ((vecheck @ X0 @ (vbinop @ X1 @ X2 @ (vconstant @ sk__395)))
% 251.86/36.73 = (vcheckBinOp @ X2 @ (vgetAType @ (vecheck @ X0 @ X1)) @ vYesNo)))),
% 251.86/36.73 inference('demod', [status(thm)],
% 251.86/36.73 [zip_derived_cl18354, zip_derived_cl277, zip_derived_cl164])).
% 251.86/36.73 thf(zip_derived_cl127981, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vBinOpT]:
% 251.86/36.73 (~ (visSomeAType @ (vsomeAType @ vYesNo))
% 251.86/36.73 | ((vecheck @ X0 @
% 251.86/36.73 (vbinop @ (vconstant @ sk__393) @ X1 @ (vconstant @ sk__395)))
% 251.86/36.73 = (vcheckBinOp @ X1 @ (vgetAType @ (vsomeAType @ vYesNo)) @
% 251.86/36.73 vYesNo)))),
% 251.86/36.73 inference('s_sup+', [status(thm)],
% 251.86/36.73 [zip_derived_cl12964, zip_derived_cl18371])).
% 251.86/36.73 thf(zip_derived_cl277, plain,
% 251.86/36.73 (![X0 : vAType]: (visSomeAType @ (vsomeAType @ X0))),
% 251.86/36.73 inference('cnf', [status(esa)], [isSomeAType-1])).
% 251.86/36.73 thf(zip_derived_cl164, plain,
% 251.86/36.73 (![X0 : vAType]: ((vgetAType @ (vsomeAType @ X0)) = (X0))),
% 251.86/36.73 inference('cnf', [status(esa)], [getAType-0])).
% 251.86/36.73 thf(zip_derived_cl128001, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vBinOpT]:
% 251.86/36.73 ((vecheck @ X0 @
% 251.86/36.73 (vbinop @ (vconstant @ sk__393) @ X1 @ (vconstant @ sk__395)))
% 251.86/36.73 = (vcheckBinOp @ X1 @ vYesNo @ vYesNo))),
% 251.86/36.73 inference('demod', [status(thm)],
% 251.86/36.73 [zip_derived_cl127981, zip_derived_cl277, zip_derived_cl164])).
% 251.86/36.73 thf(zip_derived_cl921, plain,
% 251.86/36.73 (((vecheck @ sk__394 @
% 251.86/36.73 (vbinop @ (vconstant @ sk__393) @ sk__392 @ (vconstant @ sk__395)))
% 251.86/36.73 = (vsomeAType @ sk__398))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf(zip_derived_cl928, plain, (((sk__392) = (vandop))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf(zip_derived_cl13564, plain,
% 251.86/36.73 (((vecheck @ sk__394 @
% 251.86/36.73 (vbinop @ (vconstant @ sk__393) @ vandop @ (vconstant @ sk__395)))
% 251.86/36.73 = (vsomeAType @ sk__398))),
% 251.86/36.73 inference('demod', [status(thm)], [zip_derived_cl921, zip_derived_cl928])).
% 251.86/36.73 thf(zip_derived_cl128069, plain,
% 251.86/36.73 (((vcheckBinOp @ vandop @ vYesNo @ vYesNo) = (vsomeAType @ sk__398))),
% 251.86/36.73 inference('s_sup+', [status(thm)],
% 251.86/36.73 [zip_derived_cl128001, zip_derived_cl13564])).
% 251.86/36.73 thf('checkBinOp-6', axiom,
% 251.86/36.73 (( vcheckBinOp @ vandop @ vYesNo @ vYesNo ) = ( vsomeAType @ vYesNo ))).
% 251.86/36.73 thf(zip_derived_cl750, plain,
% 251.86/36.73 (((vcheckBinOp @ vandop @ vYesNo @ vYesNo) = (vsomeAType @ vYesNo))),
% 251.86/36.73 inference('cnf', [status(esa)], [checkBinOp-6])).
% 251.86/36.73 thf(zip_derived_cl128078, plain,
% 251.86/36.73 (((vsomeAType @ vYesNo) = (vsomeAType @ sk__398))),
% 251.86/36.73 inference('demod', [status(thm)],
% 251.86/36.73 [zip_derived_cl128069, zip_derived_cl750])).
% 251.86/36.73 thf(zip_derived_cl920, plain,
% 251.86/36.73 (((vecheck @ sk__394 @ sk__391) != (vsomeAType @ sk__398))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf(zip_derived_cl929, plain, (((sk__393) = (vB @ sk__396))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf(zip_derived_cl930, plain, (((sk__395) = (vB @ sk__397))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf('evalBinOp-6', axiom,
% 251.86/36.73 (![Vb1:vYN,Vb2:vYN]:
% 251.86/36.73 ( ( vevalBinOp @ vandop @ ( vB @ Vb1 ) @ ( vB @ Vb2 ) ) =
% 251.86/36.73 ( vsomeExp @ ( vconstant @ ( vB @ ( vand @ Vb1 @ Vb2 ) ) ) ) ))).
% 251.86/36.73 thf(zip_derived_cl392, plain,
% 251.86/36.73 (![X0 : vYN, X1 : vYN]:
% 251.86/36.73 ((vevalBinOp @ vandop @ (vB @ X0) @ (vB @ X1))
% 251.86/36.73 = (vsomeExp @ (vconstant @ (vB @ (vand @ X0 @ X1)))))),
% 251.86/36.73 inference('cnf', [status(esa)], [evalBinOp-6])).
% 251.86/36.73 thf('EQ-someExp', axiom,
% 251.86/36.73 (![VExp0:vExp,VExp1:vExp]:
% 251.86/36.73 ( ( ( vsomeExp @ VExp0 ) = ( vsomeExp @ VExp1 ) ) =>
% 251.86/36.73 ( ( VExp0 ) = ( VExp1 ) ) ))).
% 251.86/36.73 thf(zip_derived_cl87, plain,
% 251.86/36.73 (![X0 : vExp, X1 : vExp]:
% 251.86/36.73 (((X1) = (X0)) | ((vsomeExp @ X1) != (vsomeExp @ X0)))),
% 251.86/36.73 inference('cnf', [status(esa)], [EQ-someExp])).
% 251.86/36.73 thf(zip_derived_cl13808, plain,
% 251.86/36.73 (![X0 : vYN, X1 : vYN, X2 : vExp]:
% 251.86/36.73 (((X2) = (vconstant @ (vB @ (vand @ X1 @ X0))))
% 251.86/36.73 | ((vsomeExp @ X2) != (vevalBinOp @ vandop @ (vB @ X1) @ (vB @ X0))))),
% 251.86/36.73 inference('s_sup-', [status(thm)], [zip_derived_cl392, zip_derived_cl87])).
% 251.86/36.73 thf(zip_derived_cl15178, plain,
% 251.86/36.73 (![X0 : vYN, X1 : vExp]:
% 251.86/36.73 (((X1) = (vconstant @ (vB @ (vand @ X0 @ sk__397))))
% 251.86/36.73 | ((vsomeExp @ X1) != (vevalBinOp @ vandop @ (vB @ X0) @ sk__395)))),
% 251.86/36.73 inference('s_sup-', [status(thm)],
% 251.86/36.73 [zip_derived_cl930, zip_derived_cl13808])).
% 251.86/36.73 thf(zip_derived_cl15302, plain,
% 251.86/36.73 (![X0 : vExp]:
% 251.86/36.73 (((X0) = (vconstant @ (vB @ (vand @ sk__396 @ sk__397))))
% 251.86/36.73 | ((vsomeExp @ X0) != (vevalBinOp @ vandop @ sk__393 @ sk__395)))),
% 251.86/36.73 inference('s_sup-', [status(thm)],
% 251.86/36.73 [zip_derived_cl929, zip_derived_cl15178])).
% 251.86/36.73 thf(zip_derived_cl931, plain,
% 251.86/36.73 (((vevalBinOp @ sk__392 @ sk__393 @ sk__395) = (vsomeExp @ sk__391))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf(zip_derived_cl928, plain, (((sk__392) = (vandop))),
% 251.86/36.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 251.86/36.73 thf(zip_derived_cl13478, plain,
% 251.86/36.73 (((vevalBinOp @ vandop @ sk__393 @ sk__395) = (vsomeExp @ sk__391))),
% 251.86/36.73 inference('demod', [status(thm)], [zip_derived_cl931, zip_derived_cl928])).
% 251.86/36.73 thf(zip_derived_cl15307, plain,
% 251.86/36.73 (![X0 : vExp]:
% 251.86/36.73 (((X0) = (vconstant @ (vB @ (vand @ sk__396 @ sk__397))))
% 251.86/36.73 | ((vsomeExp @ X0) != (vsomeExp @ sk__391)))),
% 251.86/36.73 inference('demod', [status(thm)],
% 251.86/36.73 [zip_derived_cl15302, zip_derived_cl13478])).
% 251.86/36.73 thf(zip_derived_cl15318, plain,
% 251.86/36.73 (((sk__391) = (vconstant @ (vB @ (vand @ sk__396 @ sk__397))))),
% 251.86/36.73 inference('eq_res', [status(thm)], [zip_derived_cl15307])).
% 251.86/36.73 thf(zip_derived_cl839, plain,
% 251.86/36.73 (![X0 : vATMap, X1 : vYN]:
% 251.86/36.73 ((vecheck @ X0 @ (vconstant @ (vB @ X1))) = (vsomeAType @ vYesNo))),
% 251.86/36.73 inference('cnf', [status(esa)], [echeck-0])).
% 251.86/36.73 thf(zip_derived_cl17472, plain,
% 251.86/36.73 (![X0 : vATMap]: ((vecheck @ X0 @ sk__391) = (vsomeAType @ vYesNo))),
% 251.86/36.73 inference('s_sup+', [status(thm)],
% 251.86/36.73 [zip_derived_cl15318, zip_derived_cl839])).
% 251.86/36.73 thf(zip_derived_cl17499, plain,
% 251.86/36.73 (((vsomeAType @ vYesNo) != (vsomeAType @ sk__398))),
% 251.86/36.73 inference('demod', [status(thm)],
% 251.86/36.73 [zip_derived_cl920, zip_derived_cl17472])).
% 251.86/36.73 thf(zip_derived_cl128079, plain, ($false),
% 251.86/36.73 inference('simplify_reflect-', [status(thm)],
% 251.86/36.73 [zip_derived_cl128078, zip_derived_cl17499])).
% 251.86/36.73
% 251.86/36.73 % SZS output end Refutation
% 251.86/36.73
% 251.86/36.73
% 251.86/36.73 % Terminating...
% 0.64/36.82 % Runner terminated.
% 0.64/36.82 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------