%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM274_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.tUdBLP35pK true
% Computer : n002.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 14.82s 2.73s
% Output : Refutation 14.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM274_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.tUdBLP35pK true
% 0.17/0.35 % Computer : n002.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Mon May 4 20:08:16 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 % Running portfolio for 300 s
% 0.17/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.35 % Number of cores: 8
% 0.20/0.35 % Python version: Python 3.6.8
% 0.20/0.36 % 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.54/0.72 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.73 % /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.75 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.54/0.75 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 14.82/2.73 % Solved by fo/fo13.sh.
% 14.82/2.73 % done 1900 iterations in 1.956s
% 14.82/2.73 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 14.82/2.73 % SZS output start Refutation
% 14.82/2.73 thf(vOptExp_type, type, vOptExp: $tType).
% 14.82/2.73 thf(vExp_type, type, vExp: $tType).
% 14.82/2.73 thf(vAnsMap_type, type, vAnsMap: $tType).
% 14.82/2.73 thf(vBinOpT_type, type, vBinOpT: $tType).
% 14.82/2.73 thf(vOptAType_type, type, vOptAType: $tType).
% 14.82/2.73 thf(vATMap_type, type, vATMap: $tType).
% 14.82/2.73 thf(vAType_type, type, vAType: $tType).
% 14.82/2.73 thf(vbinop_type, type, vbinop: vExp > vBinOpT > vExp > vExp).
% 14.82/2.73 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 14.82/2.73 thf(ve2_type, type, ve2: vExp).
% 14.82/2.73 thf(sk__391_type, type, sk__391: vAnsMap > vExp).
% 14.82/2.73 thf(vreduceExp_type, type, vreduceExp: vExp > vAnsMap > vOptExp).
% 14.82/2.73 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 14.82/2.73 thf(sk__33_type, type, sk__33: vOptAType > vAType).
% 14.82/2.73 thf(visSomeAType_type, type, visSomeAType: vOptAType > $o).
% 14.82/2.73 thf(vnoExp_type, type, vnoExp: vOptExp).
% 14.82/2.73 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 14.82/2.73 thf(vnoAType_type, type, vnoAType: vOptAType).
% 14.82/2.73 thf(sk__393_type, type, sk__393: vAnsMap).
% 14.82/2.73 thf(sk__395_type, type, sk__395: vAType).
% 14.82/2.73 thf(visSomeExp_type, type, visSomeExp: vOptExp > $o).
% 14.82/2.73 thf(vsomeExp_type, type, vsomeExp: vExp > vOptExp).
% 14.82/2.73 thf(vexpIsValue_type, type, vexpIsValue: vExp > $o).
% 14.82/2.73 thf(sk__394_type, type, sk__394: vBinOpT).
% 14.82/2.73 thf(ve1_type, type, ve1: vExp).
% 14.82/2.73 thf('reduceExpProgress-binop-expIsValue-False-isSomeExp-False', conjecture,
% 14.82/2.73 (![Vam:vAnsMap,Vbot:vBinOpT,Vat:vAType]:
% 14.82/2.73 ( ( ( ~( visSomeExp @ ( vreduceExp @ ve1 @ Vam ) ) ) &
% 14.82/2.73 ( ~( vexpIsValue @ ve1 ) ) &
% 14.82/2.73 ( ~( vexpIsValue @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) ) &
% 14.82/2.73 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) =
% 14.82/2.73 ( vsomeAType @ Vat ) ) ) =>
% 14.82/2.73 ( ?[Veres000:vExp]:
% 14.82/2.73 ( ( vreduceExp @ ( vbinop @ ve1 @ Vbot @ ve2 ) @ Vam ) =
% 14.82/2.73 ( vsomeExp @ Veres000 ) ) ) ))).
% 14.82/2.73 thf(zf_stmt_0, negated_conjecture,
% 14.82/2.73 (~( ![Vam:vAnsMap,Vbot:vBinOpT,Vat:vAType]:
% 14.82/2.73 ( ( ( ~( visSomeExp @ ( vreduceExp @ ve1 @ Vam ) ) ) &
% 14.82/2.73 ( ~( vexpIsValue @ ve1 ) ) &
% 14.82/2.73 ( ~( vexpIsValue @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) ) &
% 14.82/2.73 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) =
% 14.82/2.73 ( vsomeAType @ Vat ) ) ) =>
% 14.82/2.73 ( ?[Veres000:vExp]:
% 14.82/2.73 ( ( vreduceExp @ ( vbinop @ ve1 @ Vbot @ ve2 ) @ Vam ) =
% 14.82/2.73 ( vsomeExp @ Veres000 ) ) ) ) )),
% 14.82/2.73 inference('cnf.neg', [status(esa)],
% 14.82/2.73 [reduceExpProgress-binop-expIsValue-False-isSomeExp-False])).
% 14.82/2.73 thf(zip_derived_cl922, plain,
% 14.82/2.73 (((vecheck @ (vtypeAM @ sk__393) @ (vbinop @ ve1 @ sk__394 @ ve2))
% 14.82/2.73 = (vsomeAType @ sk__395))),
% 14.82/2.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.82/2.73 thf('isSomeExp-false-INV', axiom,
% 14.82/2.73 (![VOptExp0:vOptExp]:
% 14.82/2.73 ( ( ~( visSomeExp @ VOptExp0 ) ) => ( ( VOptExp0 ) = ( vnoExp ) ) ))).
% 14.82/2.73 thf(zip_derived_cl367, plain,
% 14.82/2.73 (![X0 : vOptExp]: (((X0) = (vnoExp)) | (visSomeExp @ X0))),
% 14.82/2.73 inference('cnf', [status(esa)], [isSomeExp-false-INV])).
% 14.82/2.73 thf(zip_derived_cl923, plain,
% 14.82/2.73 (~ (visSomeExp @ (vreduceExp @ ve1 @ sk__393))),
% 14.82/2.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.82/2.73 thf(zip_derived_cl978, plain, (((vreduceExp @ ve1 @ sk__393) = (vnoExp))),
% 14.82/2.73 inference('s_sup-', [status(thm)], [zip_derived_cl367, zip_derived_cl923])).
% 14.82/2.73 thf('dom-OptAType', axiom,
% 14.82/2.73 (![VX:vOptAType]:
% 14.82/2.73 ( ( ?[VAType0:vAType]: ( ( VX ) = ( vsomeAType @ VAType0 ) ) ) |
% 14.82/2.73 ( ( VX ) = ( vnoAType ) ) ))).
% 14.82/2.73 thf(zip_derived_cl75, plain,
% 14.82/2.73 (![X0 : vOptAType]:
% 14.82/2.73 (((X0) = (vsomeAType @ (sk__33 @ X0))) | ((X0) = (vnoAType)))),
% 14.82/2.73 inference('cnf', [status(esa)], [dom-OptAType])).
% 14.82/2.73 thf('reduceExpProgress-binop-IH0', axiom,
% 14.82/2.73 (![Vam:vAnsMap,Vat:vAType]:
% 14.82/2.73 ( ( ( ~( vexpIsValue @ ve1 ) ) &
% 14.82/2.73 ( ( vecheck @ ( vtypeAM @ Vam ) @ ve1 ) = ( vsomeAType @ Vat ) ) ) =>
% 14.82/2.73 ( ?[Veres00:vExp]:
% 14.82/2.73 ( ( vreduceExp @ ve1 @ Vam ) = ( vsomeExp @ Veres00 ) ) ) ))).
% 14.82/2.73 thf(zip_derived_cl920, plain,
% 14.82/2.73 (![X0 : vAnsMap, X1 : vAType]:
% 14.82/2.73 (((vreduceExp @ ve1 @ X0) = (vsomeExp @ (sk__391 @ X0)))
% 14.82/2.73 | (vexpIsValue @ ve1)
% 14.82/2.73 | ((vecheck @ (vtypeAM @ X0) @ ve1) != (vsomeAType @ X1)))),
% 14.82/2.73 inference('cnf', [status(esa)], [reduceExpProgress-binop-IH0])).
% 14.82/2.73 thf(zip_derived_cl924, plain, (~ (vexpIsValue @ ve1)),
% 14.82/2.73 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.82/2.73 thf(zip_derived_cl934, plain,
% 14.82/2.73 (![X0 : vAnsMap, X1 : vAType]:
% 14.82/2.73 (((vreduceExp @ ve1 @ X0) = (vsomeExp @ (sk__391 @ X0)))
% 14.82/2.73 | ((vecheck @ (vtypeAM @ X0) @ ve1) != (vsomeAType @ X1)))),
% 14.82/2.73 inference('demod', [status(thm)], [zip_derived_cl920, zip_derived_cl924])).
% 14.82/2.73 thf(zip_derived_cl2861, plain,
% 14.82/2.73 (![X0 : vOptAType, X1 : vAnsMap]:
% 14.82/2.73 (((X0) = (vnoAType))
% 14.82/2.73 | ((vreduceExp @ ve1 @ X1) = (vsomeExp @ (sk__391 @ X1)))
% 14.82/2.73 | ((vecheck @ (vtypeAM @ X1) @ ve1) != (X0)))),
% 14.82/2.73 inference('s_sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl934])).
% 14.82/2.73 thf(zip_derived_cl4785, plain,
% 14.82/2.73 (![X0 : vAnsMap]:
% 14.82/2.73 (((vreduceExp @ ve1 @ X0) = (vsomeExp @ (sk__391 @ X0)))
% 14.82/2.73 | ((vecheck @ (vtypeAM @ X0) @ ve1) = (vnoAType)))),
% 14.82/2.73 inference('eq_res', [status(thm)], [zip_derived_cl2861])).
% 14.82/2.73 thf('DIFF-noExp-someExp', axiom,
% 14.82/2.73 (![VExp0:vExp]: ( ( vnoExp ) != ( vsomeExp @ VExp0 ) ))).
% 14.82/2.73 thf(zip_derived_cl88, plain, (![X0 : vExp]: ((vnoExp) != (vsomeExp @ X0))),
% 14.82/2.73 inference('cnf', [status(esa)], [DIFF-noExp-someExp])).
% 14.82/2.73 thf(zip_derived_cl4788, plain,
% 14.82/2.73 (![X0 : vAnsMap]:
% 14.82/2.73 (((vecheck @ (vtypeAM @ X0) @ ve1) = (vnoAType))
% 14.82/2.73 | ((vnoExp) != (vreduceExp @ ve1 @ X0)))),
% 14.82/2.73 inference('s_sup-', [status(thm)], [zip_derived_cl4785, zip_derived_cl88])).
% 14.82/2.73 thf(zip_derived_cl4803, plain,
% 14.82/2.73 ((((vecheck @ (vtypeAM @ sk__393) @ ve1) = (vnoAType))
% 14.82/2.73 | ((vnoExp) != (vnoExp)))),
% 14.82/2.73 inference('s_sup-', [status(thm)],
% 14.82/2.73 [zip_derived_cl978, zip_derived_cl4788])).
% 14.82/2.73 thf(zip_derived_cl4806, plain,
% 14.82/2.73 (((vecheck @ (vtypeAM @ sk__393) @ ve1) = (vnoAType))),
% 14.82/2.73 inference('simplify', [status(thm)], [zip_derived_cl4803])).
% 14.82/2.73 thf('echeck-5', axiom,
% 14.82/2.73 (![Vatm:vATMap,Ve1:vExp,Ve2:vExp,Vop:vBinOpT]:
% 14.82/2.73 ( ( ~( ( visSomeAType @ ( vecheck @ Vatm @ Ve1 ) ) &
% 14.82/2.73 ( visSomeAType @ ( vecheck @ Vatm @ Ve2 ) ) ) ) =>
% 14.82/2.73 ( ( vecheck @ Vatm @ ( vbinop @ Ve1 @ Vop @ Ve2 ) ) = ( vnoAType ) ) ))).
% 14.82/2.73 thf(zip_derived_cl844, plain,
% 14.82/2.73 (![X0 : vATMap, X1 : vExp, X2 : vBinOpT, X3 : vExp]:
% 14.82/2.73 ( (visSomeAType @ (vecheck @ X0 @ X1))
% 14.82/2.73 | ((vecheck @ X0 @ (vbinop @ X1 @ X2 @ X3)) = (vnoAType)))),
% 14.82/2.73 inference('cnf', [status(esa)], [echeck-5])).
% 14.82/2.73 thf(zip_derived_cl10428, plain,
% 14.82/2.73 (![X0 : vExp, X1 : vBinOpT]:
% 14.82/2.73 ( (visSomeAType @ vnoAType)
% 14.82/2.73 | ((vecheck @ (vtypeAM @ sk__393) @ (vbinop @ ve1 @ X1 @ X0))
% 14.82/2.73 = (vnoAType)))),
% 14.82/2.73 inference('s_sup+', [status(thm)],
% 14.82/2.73 [zip_derived_cl4806, zip_derived_cl844])).
% 14.82/2.73 thf('isSomeAType-0', axiom, (~( visSomeAType @ vnoAType ))).
% 14.82/2.73 thf(zip_derived_cl276, plain, (~ (visSomeAType @ vnoAType)),
% 14.82/2.73 inference('cnf', [status(esa)], [isSomeAType-0])).
% 14.82/2.73 thf(zip_derived_cl10437, plain,
% 14.82/2.73 (![X0 : vExp, X1 : vBinOpT]:
% 14.82/2.73 ((vecheck @ (vtypeAM @ sk__393) @ (vbinop @ ve1 @ X1 @ X0))
% 14.82/2.73 = (vnoAType))),
% 14.82/2.73 inference('demod', [status(thm)],
% 14.82/2.73 [zip_derived_cl10428, zip_derived_cl276])).
% 14.82/2.73 thf(zip_derived_cl10440, plain, (((vnoAType) = (vsomeAType @ sk__395))),
% 14.82/2.73 inference('demod', [status(thm)],
% 14.82/2.73 [zip_derived_cl922, zip_derived_cl10437])).
% 14.82/2.73 thf('DIFF-noAType-someAType', axiom,
% 14.82/2.73 (![VAType0:vAType]: ( ( vnoAType ) != ( vsomeAType @ VAType0 ) ))).
% 14.82/2.73 thf(zip_derived_cl77, plain,
% 14.82/2.73 (![X0 : vAType]: ((vnoAType) != (vsomeAType @ X0))),
% 14.82/2.73 inference('cnf', [status(esa)], [DIFF-noAType-someAType])).
% 14.82/2.73 thf(zip_derived_cl10441, plain, ($false),
% 14.82/2.73 inference('simplify_reflect-', [status(thm)],
% 14.82/2.73 [zip_derived_cl10440, zip_derived_cl77])).
% 14.82/2.73
% 14.82/2.73 % SZS output end Refutation
% 14.82/2.73
% 14.82/2.73
% 14.82/2.73 % Terminating...
% 14.82/2.77 % Runner terminated.
% 14.82/2.78 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------