%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM277_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.3HUV7MhLth true
% Computer : n012.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 9.96s 1.87s
% Output : Refutation 9.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : COM277_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.06 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.3HUV7MhLth true
% 0.07/0.25 % Computer : n012.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Mon May 4 20:11:30 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 % Running portfolio for 300 s
% 0.07/0.25 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.25 % Number of cores: 8
% 0.07/0.25 % Python version: Python 3.6.8
% 0.07/0.25 % Running in FO mode
% 0.13/0.40 % Total configuration time : 435
% 0.13/0.40 % Estimated wc time : 1092
% 0.13/0.40 % Estimated cpu time (7 cpus) : 156.0
% 0.49/0.46 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.46 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.46 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.46 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.46 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.46 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.49/0.47 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 9.96/1.87 % Solved by fo/fo5.sh.
% 9.96/1.87 % done 1567 iterations in 1.378s
% 9.96/1.87 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 9.96/1.87 % SZS output start Refutation
% 9.96/1.87 thf(vOptAType_type, type, vOptAType: $tType).
% 9.96/1.87 thf(vAType_type, type, vAType: $tType).
% 9.96/1.87 thf(vExp_type, type, vExp: $tType).
% 9.96/1.87 thf(vATMap_type, type, vATMap: $tType).
% 9.96/1.87 thf(vAnsMap_type, type, vAnsMap: $tType).
% 9.96/1.87 thf(vOptExp_type, type, vOptExp: $tType).
% 9.96/1.87 thf(vUnOpT_type, type, vUnOpT: $tType).
% 9.96/1.87 thf(vunop_type, type, vunop: vUnOpT > vExp > vExp).
% 9.96/1.87 thf(sk__392_type, type, sk__392: vAnsMap).
% 9.96/1.87 thf(sk__393_type, type, sk__393: vUnOpT).
% 9.96/1.87 thf(visSomeAType_type, type, visSomeAType: vOptAType > $o).
% 9.96/1.87 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 9.96/1.87 thf(visSomeExp_type, type, visSomeExp: vOptExp > $o).
% 9.96/1.87 thf(vnoExp_type, type, vnoExp: vOptExp).
% 9.96/1.87 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 9.96/1.87 thf(vnoAType_type, type, vnoAType: vOptAType).
% 9.96/1.87 thf(vsomeExp_type, type, vsomeExp: vExp > vOptExp).
% 9.96/1.87 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 9.96/1.87 thf(sk__83_type, type, sk__83: vOptAType > vAType).
% 9.96/1.87 thf(sk__394_type, type, sk__394: vAType).
% 9.96/1.87 thf(ve1_type, type, ve1: vExp).
% 9.96/1.87 thf(sk__391_type, type, sk__391: vAnsMap > vExp).
% 9.96/1.87 thf(vexpIsValue_type, type, vexpIsValue: vExp > $o).
% 9.96/1.87 thf(vreduceExp_type, type, vreduceExp: vExp > vAnsMap > vOptExp).
% 9.96/1.87 thf('isSomeAType-false-INV', axiom,
% 9.96/1.87 (![VOptAType0:vOptAType]:
% 9.96/1.87 ( ( ~( visSomeAType @ VOptAType0 ) ) => ( ( VOptAType0 ) = ( vnoAType ) ) ))).
% 9.96/1.87 thf(zip_derived_cl279, plain,
% 9.96/1.87 (![X0 : vOptAType]: (((X0) = (vnoAType)) | (visSomeAType @ X0))),
% 9.96/1.87 inference('cnf', [status(esa)], [isSomeAType-false-INV])).
% 9.96/1.87 thf('isSomeAType-true-INV', axiom,
% 9.96/1.87 (![VOptAType0:vOptAType]:
% 9.96/1.87 ( ( visSomeAType @ VOptAType0 ) =>
% 9.96/1.87 ( ?[VwildcardName0:vAType]:
% 9.96/1.87 ( ( VOptAType0 ) = ( vsomeAType @ VwildcardName0 ) ) ) ))).
% 9.96/1.87 thf(zip_derived_cl278, plain,
% 9.96/1.87 (![X0 : vOptAType]:
% 9.96/1.87 (((X0) = (vsomeAType @ (sk__83 @ X0))) | ~ (visSomeAType @ X0))),
% 9.96/1.87 inference('cnf', [status(esa)], [isSomeAType-true-INV])).
% 9.96/1.87 thf('reduceExpProgress-unop-IH0', axiom,
% 9.96/1.87 (![Vam:vAnsMap,Vat:vAType]:
% 9.96/1.87 ( ( ( ~( vexpIsValue @ ve1 ) ) &
% 9.96/1.87 ( ( vecheck @ ( vtypeAM @ Vam ) @ ve1 ) = ( vsomeAType @ Vat ) ) ) =>
% 9.96/1.87 ( ?[Veres00:vExp]:
% 9.96/1.87 ( ( vreduceExp @ ve1 @ Vam ) = ( vsomeExp @ Veres00 ) ) ) ))).
% 9.96/1.87 thf(zip_derived_cl920, plain,
% 9.96/1.87 (![X0 : vAnsMap, X1 : vAType]:
% 9.96/1.87 (((vreduceExp @ ve1 @ X0) = (vsomeExp @ (sk__391 @ X0)))
% 9.96/1.87 | (vexpIsValue @ ve1)
% 9.96/1.87 | ((vecheck @ (vtypeAM @ X0) @ ve1) != (vsomeAType @ X1)))),
% 9.96/1.87 inference('cnf', [status(esa)], [reduceExpProgress-unop-IH0])).
% 9.96/1.87 thf('reduceExpProgress-unop-expIsValue-False-isSomeExp-False', conjecture,
% 9.96/1.87 (![Vam:vAnsMap,Vuot:vUnOpT,Vat:vAType]:
% 9.96/1.87 ( ( ( ~( visSomeExp @ ( vreduceExp @ ve1 @ Vam ) ) ) &
% 9.96/1.87 ( ~( vexpIsValue @ ve1 ) ) &
% 9.96/1.87 ( ~( vexpIsValue @ ( vunop @ Vuot @ ve1 ) ) ) &
% 9.96/1.87 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vunop @ Vuot @ ve1 ) ) =
% 9.96/1.87 ( vsomeAType @ Vat ) ) ) =>
% 9.96/1.87 ( ?[Veres000:vExp]:
% 9.96/1.87 ( ( vreduceExp @ ( vunop @ Vuot @ ve1 ) @ Vam ) =
% 9.96/1.87 ( vsomeExp @ Veres000 ) ) ) ))).
% 9.96/1.87 thf(zf_stmt_0, negated_conjecture,
% 9.96/1.87 (~( ![Vam:vAnsMap,Vuot:vUnOpT,Vat:vAType]:
% 9.96/1.87 ( ( ( ~( visSomeExp @ ( vreduceExp @ ve1 @ Vam ) ) ) &
% 9.96/1.87 ( ~( vexpIsValue @ ve1 ) ) &
% 9.96/1.87 ( ~( vexpIsValue @ ( vunop @ Vuot @ ve1 ) ) ) &
% 9.96/1.87 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vunop @ Vuot @ ve1 ) ) =
% 9.96/1.87 ( vsomeAType @ Vat ) ) ) =>
% 9.96/1.87 ( ?[Veres000:vExp]:
% 9.96/1.87 ( ( vreduceExp @ ( vunop @ Vuot @ ve1 ) @ Vam ) =
% 9.96/1.87 ( vsomeExp @ Veres000 ) ) ) ) )),
% 9.96/1.87 inference('cnf.neg', [status(esa)],
% 9.96/1.87 [reduceExpProgress-unop-expIsValue-False-isSomeExp-False])).
% 9.96/1.87 thf(zip_derived_cl923, plain, (~ (vexpIsValue @ ve1)),
% 9.96/1.87 inference('cnf', [status(esa)], [zf_stmt_0])).
% 9.96/1.87 thf(zip_derived_cl5185, plain,
% 9.96/1.87 (![X0 : vAnsMap, X1 : vAType]:
% 9.96/1.87 (((vreduceExp @ ve1 @ X0) = (vsomeExp @ (sk__391 @ X0)))
% 9.96/1.87 | ((vecheck @ (vtypeAM @ X0) @ ve1) != (vsomeAType @ X1)))),
% 9.96/1.87 inference('demod', [status(thm)], [zip_derived_cl920, zip_derived_cl923])).
% 9.96/1.87 thf(zip_derived_cl5191, plain,
% 9.96/1.87 (![X0 : vOptAType, X1 : vAnsMap]:
% 9.96/1.87 (((vecheck @ (vtypeAM @ X1) @ ve1) != (X0))
% 9.96/1.87 | ~ (visSomeAType @ X0)
% 9.96/1.87 | ((vreduceExp @ ve1 @ X1) = (vsomeExp @ (sk__391 @ X1))))),
% 9.96/1.87 inference('sup-', [status(thm)], [zip_derived_cl278, zip_derived_cl5185])).
% 9.96/1.87 thf(zip_derived_cl5361, plain,
% 9.96/1.87 (![X0 : vAnsMap]:
% 9.96/1.87 (((vreduceExp @ ve1 @ X0) = (vsomeExp @ (sk__391 @ X0)))
% 9.96/1.87 | ~ (visSomeAType @ (vecheck @ (vtypeAM @ X0) @ ve1)))),
% 9.96/1.87 inference('eq_res', [status(thm)], [zip_derived_cl5191])).
% 9.96/1.87 thf(zip_derived_cl5362, plain,
% 9.96/1.87 (![X0 : vAnsMap]:
% 9.96/1.87 (((vecheck @ (vtypeAM @ X0) @ ve1) = (vnoAType))
% 9.96/1.87 | ((vreduceExp @ ve1 @ X0) = (vsomeExp @ (sk__391 @ X0))))),
% 9.96/1.87 inference('sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl5361])).
% 9.96/1.87 thf(zip_derived_cl921, plain,
% 9.96/1.87 (((vecheck @ (vtypeAM @ sk__392) @ (vunop @ sk__393 @ ve1))
% 9.96/1.87 = (vsomeAType @ sk__394))),
% 9.96/1.87 inference('cnf', [status(esa)], [zf_stmt_0])).
% 9.96/1.87 thf('echeck-7', axiom,
% 9.96/1.87 (![Vatm:vATMap,Ve:vExp,Vop:vUnOpT]:
% 9.96/1.87 ( ( ~( visSomeAType @ ( vecheck @ Vatm @ Ve ) ) ) =>
% 9.96/1.87 ( ( vecheck @ Vatm @ ( vunop @ Vop @ Ve ) ) = ( vnoAType ) ) ))).
% 9.96/1.87 thf(zip_derived_cl847, plain,
% 9.96/1.87 (![X0 : vATMap, X1 : vExp, X2 : vUnOpT]:
% 9.96/1.87 ( (visSomeAType @ (vecheck @ X0 @ X1))
% 9.96/1.87 | ((vecheck @ X0 @ (vunop @ X2 @ X1)) = (vnoAType)))),
% 9.96/1.87 inference('cnf', [status(esa)], [echeck-7])).
% 9.96/1.87 thf(zip_derived_cl6928, plain,
% 9.96/1.87 ((((vsomeAType @ sk__394) = (vnoAType))
% 9.96/1.87 | (visSomeAType @ (vecheck @ (vtypeAM @ sk__392) @ ve1)))),
% 9.96/1.87 inference('sup+', [status(thm)], [zip_derived_cl921, zip_derived_cl847])).
% 9.96/1.87 thf('DIFF-noAType-someAType', axiom,
% 9.96/1.87 (![VAType0:vAType]: ( ( vnoAType ) != ( vsomeAType @ VAType0 ) ))).
% 9.96/1.87 thf(zip_derived_cl77, plain,
% 9.96/1.87 (![X0 : vAType]: ((vnoAType) != (vsomeAType @ X0))),
% 9.96/1.87 inference('cnf', [status(esa)], [DIFF-noAType-someAType])).
% 9.96/1.87 thf(zip_derived_cl6929, plain,
% 9.96/1.87 ( (visSomeAType @ (vecheck @ (vtypeAM @ sk__392) @ ve1))),
% 9.96/1.87 inference('simplify_reflect-', [status(thm)],
% 9.96/1.87 [zip_derived_cl6928, zip_derived_cl77])).
% 9.96/1.87 thf(zip_derived_cl6935, plain,
% 9.96/1.87 (( (visSomeAType @ vnoAType)
% 9.96/1.87 | ((vreduceExp @ ve1 @ sk__392) = (vsomeExp @ (sk__391 @ sk__392))))),
% 9.96/1.87 inference('sup+', [status(thm)], [zip_derived_cl5362, zip_derived_cl6929])).
% 9.96/1.87 thf('isSomeAType-0', axiom, (~( visSomeAType @ vnoAType ))).
% 9.96/1.87 thf(zip_derived_cl276, plain, (~ (visSomeAType @ vnoAType)),
% 9.96/1.87 inference('cnf', [status(esa)], [isSomeAType-0])).
% 9.96/1.87 thf('isSomeExp-false-INV', axiom,
% 9.96/1.87 (![VOptExp0:vOptExp]:
% 9.96/1.87 ( ( ~( visSomeExp @ VOptExp0 ) ) => ( ( VOptExp0 ) = ( vnoExp ) ) ))).
% 9.96/1.87 thf(zip_derived_cl367, plain,
% 9.96/1.87 (![X0 : vOptExp]: (((X0) = (vnoExp)) | (visSomeExp @ X0))),
% 9.96/1.87 inference('cnf', [status(esa)], [isSomeExp-false-INV])).
% 9.96/1.87 thf(zip_derived_cl922, plain,
% 9.96/1.87 (~ (visSomeExp @ (vreduceExp @ ve1 @ sk__392))),
% 9.96/1.87 inference('cnf', [status(esa)], [zf_stmt_0])).
% 9.96/1.87 thf(zip_derived_cl941, plain, (((vreduceExp @ ve1 @ sk__392) = (vnoExp))),
% 9.96/1.87 inference('sup-', [status(thm)], [zip_derived_cl367, zip_derived_cl922])).
% 9.96/1.87 thf(zip_derived_cl6940, plain,
% 9.96/1.87 (((vnoExp) = (vsomeExp @ (sk__391 @ sk__392)))),
% 9.96/1.87 inference('demod', [status(thm)],
% 9.96/1.87 [zip_derived_cl6935, zip_derived_cl276, zip_derived_cl941])).
% 9.96/1.87 thf('DIFF-noExp-someExp', axiom,
% 9.96/1.87 (![VExp0:vExp]: ( ( vnoExp ) != ( vsomeExp @ VExp0 ) ))).
% 9.96/1.87 thf(zip_derived_cl88, plain, (![X0 : vExp]: ((vnoExp) != (vsomeExp @ X0))),
% 9.96/1.87 inference('cnf', [status(esa)], [DIFF-noExp-someExp])).
% 9.96/1.87 thf(zip_derived_cl6941, plain, ($false),
% 9.96/1.87 inference('simplify_reflect-', [status(thm)],
% 9.96/1.87 [zip_derived_cl6940, zip_derived_cl88])).
% 9.96/1.87
% 9.96/1.87 % SZS output end Refutation
% 9.96/1.87
% 9.96/1.87
% 9.96/1.87 % Terminating...
% 2.21/1.91 % Runner terminated.
% 2.21/1.91 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------