%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM275_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.cCObVZXGTM 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:24 PM UTC 2026
% Result : Theorem 23.23s 3.92s
% Output : Refutation 23.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM275_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.cCObVZXGTM 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.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Mon May 4 20:09:36 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 % Running portfolio for 300 s
% 0.17/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.35 % Number of cores: 8
% 0.17/0.35 % Python version: Python 3.6.8
% 0.19/0.35 % Running in FO mode
% 0.54/0.65 % Total configuration time : 435
% 0.54/0.65 % Estimated wc time : 1092
% 0.54/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 23.23/3.92 % Solved by fo/fo6_bce.sh.
% 23.23/3.92 % BCE start: 928
% 23.23/3.92 % BCE eliminated: 1
% 23.23/3.92 % PE start: 927
% 23.23/3.92 logic: eq
% 23.23/3.92 % PE eliminated: -317
% 23.23/3.92 % done 877 iterations in 3.177s
% 23.23/3.92 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 23.23/3.92 % SZS output start Refutation
% 23.23/3.92 thf(vOptExp_type, type, vOptExp: $tType).
% 23.23/3.92 thf(vExp_type, type, vExp: $tType).
% 23.23/3.92 thf(vAnsMap_type, type, vAnsMap: $tType).
% 23.23/3.92 thf(vBinOpT_type, type, vBinOpT: $tType).
% 23.23/3.92 thf(vOptAType_type, type, vOptAType: $tType).
% 23.23/3.92 thf(vATMap_type, type, vATMap: $tType).
% 23.23/3.92 thf(vAType_type, type, vAType: $tType).
% 23.23/3.92 thf(vbinop_type, type, vbinop: vExp > vBinOpT > vExp > vExp).
% 23.23/3.92 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 23.23/3.92 thf(ve2_type, type, ve2: vExp).
% 23.23/3.92 thf(vreduceExp_type, type, vreduceExp: vExp > vAnsMap > vOptExp).
% 23.23/3.92 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 23.23/3.92 thf(vnoExp_type, type, vnoExp: vOptExp).
% 23.23/3.92 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 23.23/3.92 thf(sk__393_type, type, sk__393: vAnsMap).
% 23.23/3.92 thf(visSomeExp_type, type, visSomeExp: vOptExp > $o).
% 23.23/3.92 thf(vsomeExp_type, type, vsomeExp: vExp > vOptExp).
% 23.23/3.92 thf(vgetExp_type, type, vgetExp: vOptExp > vExp).
% 23.23/3.92 thf(vexpIsValue_type, type, vexpIsValue: vExp > $o).
% 23.23/3.92 thf(sk__394_type, type, sk__394: vBinOpT).
% 23.23/3.92 thf(ve1_type, type, ve1: vExp).
% 23.23/3.92 thf(sk__134_type, type, sk__134: vOptExp > vExp).
% 23.23/3.92 thf('isSomeExp-false-INV', axiom,
% 23.23/3.92 (![VOptExp0:vOptExp]:
% 23.23/3.92 ( ( ~( visSomeExp @ VOptExp0 ) ) => ( ( VOptExp0 ) = ( vnoExp ) ) ))).
% 23.23/3.92 thf(zip_derived_cl367, plain,
% 23.23/3.92 (![X0 : vOptExp]: (((X0) = (vnoExp)) | (visSomeExp @ X0))),
% 23.23/3.92 inference('cnf', [status(esa)], [isSomeExp-false-INV])).
% 23.23/3.92 thf('isSomeExp-true-INV', axiom,
% 23.23/3.92 (![VOptExp0:vOptExp]:
% 23.23/3.92 ( ( visSomeExp @ VOptExp0 ) =>
% 23.23/3.92 ( ?[VwildcardName0:vExp]:
% 23.23/3.92 ( ( VOptExp0 ) = ( vsomeExp @ VwildcardName0 ) ) ) ))).
% 23.23/3.92 thf(zip_derived_cl366, plain,
% 23.23/3.92 (![X0 : vOptExp]:
% 23.23/3.92 (((X0) = (vsomeExp @ (sk__134 @ X0))) | ~ (visSomeExp @ X0))),
% 23.23/3.92 inference('cnf', [status(esa)], [isSomeExp-true-INV])).
% 23.23/3.92 thf('reduceExpProgress-binop-expIsValue-True-expIsValue-False-isSomeExp-True', conjecture,
% 23.23/3.92 (![Vam:vAnsMap,Vbot:vBinOpT,Vat:vAType]:
% 23.23/3.92 ( ( ( visSomeExp @ ( vreduceExp @ ve2 @ Vam ) ) &
% 23.23/3.92 ( ~( vexpIsValue @ ve2 ) ) & ( vexpIsValue @ ve1 ) &
% 23.23/3.92 ( ~( vexpIsValue @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) ) &
% 23.23/3.92 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) =
% 23.23/3.92 ( vsomeAType @ Vat ) ) ) =>
% 23.23/3.92 ( ?[Veres000:vExp]:
% 23.23/3.92 ( ( vreduceExp @ ( vbinop @ ve1 @ Vbot @ ve2 ) @ Vam ) =
% 23.23/3.92 ( vsomeExp @ Veres000 ) ) ) ))).
% 23.23/3.92 thf(zf_stmt_0, negated_conjecture,
% 23.23/3.92 (~( ![Vam:vAnsMap,Vbot:vBinOpT,Vat:vAType]:
% 23.23/3.92 ( ( ( visSomeExp @ ( vreduceExp @ ve2 @ Vam ) ) &
% 23.23/3.92 ( ~( vexpIsValue @ ve2 ) ) & ( vexpIsValue @ ve1 ) &
% 23.23/3.92 ( ~( vexpIsValue @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) ) &
% 23.23/3.92 ( ( vecheck @ ( vtypeAM @ Vam ) @ ( vbinop @ ve1 @ Vbot @ ve2 ) ) =
% 23.23/3.92 ( vsomeAType @ Vat ) ) ) =>
% 23.23/3.92 ( ?[Veres000:vExp]:
% 23.23/3.92 ( ( vreduceExp @ ( vbinop @ ve1 @ Vbot @ ve2 ) @ Vam ) =
% 23.23/3.92 ( vsomeExp @ Veres000 ) ) ) ) )),
% 23.23/3.92 inference('cnf.neg', [status(esa)],
% 23.23/3.92 [reduceExpProgress-binop-expIsValue-True-expIsValue-False-isSomeExp-True])).
% 23.23/3.92 thf(zip_derived_cl927, plain,
% 23.23/3.92 (![X0 : vExp]:
% 23.23/3.92 ((vreduceExp @ (vbinop @ ve1 @ sk__394 @ ve2) @ sk__393)
% 23.23/3.92 != (vsomeExp @ X0))),
% 23.23/3.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.23/3.92 thf(zip_derived_cl12774, plain,
% 23.23/3.92 (![X0 : vOptExp]:
% 23.23/3.92 (~ (visSomeExp @ X0)
% 23.23/3.92 | ((vreduceExp @ (vbinop @ ve1 @ sk__394 @ ve2) @ sk__393) != (X0)))),
% 23.23/3.92 inference('s_sup-', [status(thm)], [zip_derived_cl366, zip_derived_cl927])).
% 23.23/3.92 thf(zip_derived_cl12788, plain,
% 23.23/3.92 (~ (visSomeExp @ (vreduceExp @ (vbinop @ ve1 @ sk__394 @ ve2) @ sk__393))),
% 23.23/3.92 inference('eq_res', [status(thm)], [zip_derived_cl12774])).
% 23.23/3.92 thf(zip_derived_cl12789, plain,
% 23.23/3.92 (((vreduceExp @ (vbinop @ ve1 @ sk__394 @ ve2) @ sk__393) = (vnoExp))),
% 23.23/3.92 inference('s_sup-', [status(thm)],
% 23.23/3.92 [zip_derived_cl367, zip_derived_cl12788])).
% 23.23/3.92 thf(zip_derived_cl923, plain, ( (visSomeExp @ (vreduceExp @ ve2 @ sk__393))),
% 23.23/3.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.23/3.92 thf('reduceExp-4', axiom,
% 23.23/3.92 (![Ve1:vExp,Ve2:vExp,Vam:vAnsMap,Vop:vBinOpT]:
% 23.23/3.92 ( ( ( vexpIsValue @ Ve1 ) & ( ~( vexpIsValue @ Ve2 ) ) &
% 23.23/3.92 ( visSomeExp @ ( vreduceExp @ Ve2 @ Vam ) ) ) =>
% 23.23/3.92 ( ( vreduceExp @ ( vbinop @ Ve1 @ Vop @ Ve2 ) @ Vam ) =
% 23.23/3.92 ( vsomeExp @
% 23.23/3.92 ( vbinop @ Ve1 @ Vop @ ( vgetExp @ ( vreduceExp @ Ve2 @ Vam ) ) ) ) ) ))).
% 23.23/3.92 thf(zip_derived_cl492, plain,
% 23.23/3.92 (![X0 : vExp, X1 : vAnsMap, X2 : vExp, X3 : vBinOpT]:
% 23.23/3.92 (~ (visSomeExp @ (vreduceExp @ X0 @ X1))
% 23.23/3.92 | (vexpIsValue @ X0)
% 23.23/3.92 | ~ (vexpIsValue @ X2)
% 23.23/3.92 | ((vreduceExp @ (vbinop @ X2 @ X3 @ X0) @ X1)
% 23.23/3.92 = (vsomeExp @
% 23.23/3.92 (vbinop @ X2 @ X3 @ (vgetExp @ (vreduceExp @ X0 @ X1))))))),
% 23.23/3.92 inference('cnf', [status(esa)], [reduceExp-4])).
% 23.23/3.92 thf('DIFF-noExp-someExp', axiom,
% 23.23/3.92 (![VExp0:vExp]: ( ( vnoExp ) != ( vsomeExp @ VExp0 ) ))).
% 23.23/3.92 thf(zip_derived_cl88, plain, (![X0 : vExp]: ((vnoExp) != (vsomeExp @ X0))),
% 23.23/3.92 inference('cnf', [status(esa)], [DIFF-noExp-someExp])).
% 23.23/3.92 thf(zip_derived_cl16018, plain,
% 23.23/3.92 (![X0 : vAnsMap, X1 : vExp, X2 : vBinOpT, X3 : vExp]:
% 23.23/3.92 (~ (vexpIsValue @ X3)
% 23.23/3.92 | (vexpIsValue @ X1)
% 23.23/3.92 | ~ (visSomeExp @ (vreduceExp @ X1 @ X0))
% 23.23/3.92 | ((vnoExp) != (vreduceExp @ (vbinop @ X3 @ X2 @ X1) @ X0)))),
% 23.23/3.92 inference('s_sup-', [status(thm)], [zip_derived_cl492, zip_derived_cl88])).
% 23.23/3.92 thf(zip_derived_cl16046, plain,
% 23.23/3.92 (![X0 : vExp, X1 : vBinOpT]:
% 23.23/3.92 (~ (vexpIsValue @ X0)
% 23.23/3.92 | (vexpIsValue @ ve2)
% 23.23/3.92 | ((vnoExp) != (vreduceExp @ (vbinop @ X0 @ X1 @ ve2) @ sk__393)))),
% 23.23/3.92 inference('s_sup-', [status(thm)],
% 23.23/3.92 [zip_derived_cl923, zip_derived_cl16018])).
% 23.23/3.92 thf(zip_derived_cl924, plain, (~ (vexpIsValue @ ve2)),
% 23.23/3.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.23/3.92 thf(zip_derived_cl16054, plain,
% 23.23/3.92 (![X0 : vExp, X1 : vBinOpT]:
% 23.23/3.92 (~ (vexpIsValue @ X0)
% 23.23/3.92 | ((vnoExp) != (vreduceExp @ (vbinop @ X0 @ X1 @ ve2) @ sk__393)))),
% 23.23/3.92 inference('demod', [status(thm)],
% 23.23/3.92 [zip_derived_cl16046, zip_derived_cl924])).
% 23.23/3.92 thf(zip_derived_cl16090, plain,
% 23.23/3.92 ((~ (vexpIsValue @ ve1) | ((vnoExp) != (vnoExp)))),
% 23.23/3.92 inference('s_sup-', [status(thm)],
% 23.23/3.92 [zip_derived_cl12789, zip_derived_cl16054])).
% 23.23/3.92 thf(zip_derived_cl925, plain, ( (vexpIsValue @ ve1)),
% 23.23/3.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.23/3.92 thf(zip_derived_cl16095, plain, (((vnoExp) != (vnoExp))),
% 23.23/3.92 inference('demod', [status(thm)],
% 23.23/3.92 [zip_derived_cl16090, zip_derived_cl925])).
% 23.23/3.92 thf(zip_derived_cl16096, plain, ($false),
% 23.23/3.92 inference('simplify', [status(thm)], [zip_derived_cl16095])).
% 23.23/3.92
% 23.23/3.92 % SZS output end Refutation
% 23.23/3.92
% 23.23/3.92
% 23.23/3.92 % Terminating...
% 23.23/3.97 % Runner terminated.
% 23.23/3.98 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------