%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM233_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.pOHi71bf38 true
% Computer : n019.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:20 PM UTC 2026
% Result : Theorem 3.88s 1.18s
% Output : Refutation 3.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM233_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.pOHi71bf38 true
% 0.18/0.34 % Computer : n019.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Mon May 4 19:15:59 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.18/0.34 % Running portfolio for 300 s
% 0.18/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.35 % Number of cores: 8
% 0.18/0.35 % Python version: Python 3.6.8
% 0.18/0.35 % Running in FO mode
% 0.53/0.63 % Total configuration time : 435
% 0.53/0.63 % Estimated wc time : 1092
% 0.53/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.53/0.69 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.70 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.70 % /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/fo5.sh running for 50s
% 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/fo4.sh running for 50s
% 3.88/1.18 % Solved by fo/fo13.sh.
% 3.88/1.18 % done 739 iterations in 0.413s
% 3.88/1.18 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 3.88/1.18 % SZS output start Refutation
% 3.88/1.18 thf(vOptTerm_type, type, vOptTerm: $tType).
% 3.88/1.18 thf(vTerm_type, type, vTerm: $tType).
% 3.88/1.18 thf(vTy_type, type, vTy: $tType).
% 3.88/1.18 thf(vt2_type, type, vt2: vTerm).
% 3.88/1.18 thf(vgetTerm_type, type, vgetTerm: vOptTerm > vTerm).
% 3.88/1.18 thf(vnoTerm_type, type, vnoTerm: vOptTerm).
% 3.88/1.18 thf(vt1_type, type, vt1: vTerm).
% 3.88/1.18 thf(visNV_type, type, visNV: vTerm > $o).
% 3.88/1.18 thf(vsomeTerm_type, type, vsomeTerm: vTerm > vOptTerm).
% 3.88/1.18 thf(visSomeTerm_type, type, visSomeTerm: vOptTerm > $o).
% 3.88/1.18 thf(vreduce_type, type, vreduce: vTerm > vOptTerm).
% 3.88/1.18 thf(vptchecksimple_type, type, vptchecksimple: vTerm > vTy > $o).
% 3.88/1.18 thf(visValue_type, type, visValue: vTerm > $o).
% 3.88/1.18 thf(vPlus_type, type, vPlus: vTerm > vTerm > vTerm).
% 3.88/1.18 thf('isSomeTerm-0', axiom, (~( visSomeTerm @ vnoTerm ))).
% 3.88/1.18 thf(zip_derived_cl67, plain, (~ (visSomeTerm @ vnoTerm)),
% 3.88/1.18 inference('cnf', [status(esa)], [isSomeTerm-0])).
% 3.88/1.18 thf('Progress-Plus-isNV-False-isSomeTerm-True', conjecture,
% 3.88/1.18 (![VT:vTy]:
% 3.88/1.18 ( ( ( visSomeTerm @ ( vreduce @ vt1 ) ) & ( ~( visNV @ vt1 ) ) &
% 3.88/1.18 ( vptchecksimple @ ( vPlus @ vt1 @ vt2 ) @ VT ) &
% 3.88/1.18 ( ~( visValue @ ( vPlus @ vt1 @ vt2 ) ) ) ) =>
% 3.88/1.18 ( ( vreduce @ ( vPlus @ vt1 @ vt2 ) ) != ( vnoTerm ) ) ))).
% 3.88/1.18 thf(zf_stmt_0, negated_conjecture,
% 3.88/1.18 (~( ![VT:vTy]:
% 3.88/1.18 ( ( ( visSomeTerm @ ( vreduce @ vt1 ) ) & ( ~( visNV @ vt1 ) ) &
% 3.88/1.18 ( vptchecksimple @ ( vPlus @ vt1 @ vt2 ) @ VT ) &
% 3.88/1.18 ( ~( visValue @ ( vPlus @ vt1 @ vt2 ) ) ) ) =>
% 3.88/1.18 ( ( vreduce @ ( vPlus @ vt1 @ vt2 ) ) != ( vnoTerm ) ) ) )),
% 3.88/1.18 inference('cnf.neg', [status(esa)],
% 3.88/1.18 [Progress-Plus-isNV-False-isSomeTerm-True])).
% 3.88/1.18 thf(zip_derived_cl268, plain,
% 3.88/1.18 (((vreduce @ (vPlus @ vt1 @ vt2)) = (vnoTerm))),
% 3.88/1.18 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.88/1.18 thf(zip_derived_cl265, plain, ( (visSomeTerm @ (vreduce @ vt1))),
% 3.88/1.18 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.88/1.18 thf('reduce-21', axiom,
% 3.88/1.18 (![Vt1:vTerm,Vt2:vTerm]:
% 3.88/1.18 ( ( ( ~( visNV @ Vt1 ) ) & ( visSomeTerm @ ( vreduce @ Vt1 ) ) ) =>
% 3.88/1.18 ( ( vreduce @ ( vPlus @ Vt1 @ Vt2 ) ) =
% 3.88/1.18 ( vsomeTerm @ ( vPlus @ ( vgetTerm @ ( vreduce @ Vt1 ) ) @ Vt2 ) ) ) ))).
% 3.88/1.18 thf(zip_derived_cl119, plain,
% 3.88/1.18 (![X0 : vTerm, X1 : vTerm]:
% 3.88/1.18 (~ (visSomeTerm @ (vreduce @ X0))
% 3.88/1.18 | (visNV @ X0)
% 3.88/1.18 | ((vreduce @ (vPlus @ X0 @ X1))
% 3.88/1.18 = (vsomeTerm @ (vPlus @ (vgetTerm @ (vreduce @ X0)) @ X1))))),
% 3.88/1.18 inference('cnf', [status(esa)], [reduce-21])).
% 3.88/1.18 thf(zip_derived_cl2655, plain,
% 3.88/1.18 (![X0 : vTerm]:
% 3.88/1.18 ( (visNV @ vt1)
% 3.88/1.18 | ((vreduce @ (vPlus @ vt1 @ X0))
% 3.88/1.18 = (vsomeTerm @ (vPlus @ (vgetTerm @ (vreduce @ vt1)) @ X0))))),
% 3.88/1.18 inference('s_sup-', [status(thm)], [zip_derived_cl265, zip_derived_cl119])).
% 3.88/1.18 thf(zip_derived_cl266, plain, (~ (visNV @ vt1)),
% 3.88/1.18 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.88/1.18 thf(zip_derived_cl2684, plain,
% 3.88/1.18 (![X0 : vTerm]:
% 3.88/1.18 ((vreduce @ (vPlus @ vt1 @ X0))
% 3.88/1.18 = (vsomeTerm @ (vPlus @ (vgetTerm @ (vreduce @ vt1)) @ X0)))),
% 3.88/1.18 inference('demod', [status(thm)], [zip_derived_cl2655, zip_derived_cl266])).
% 3.88/1.18 thf('isSomeTerm-1', axiom,
% 3.88/1.18 (![VwildcardName0:vTerm]: ( visSomeTerm @ ( vsomeTerm @ VwildcardName0 ) ))).
% 3.88/1.18 thf(zip_derived_cl68, plain,
% 3.88/1.18 (![X0 : vTerm]: (visSomeTerm @ (vsomeTerm @ X0))),
% 3.88/1.18 inference('cnf', [status(esa)], [isSomeTerm-1])).
% 3.88/1.18 thf(zip_derived_cl3499, plain,
% 3.88/1.18 (![X0 : vTerm]: (visSomeTerm @ (vreduce @ (vPlus @ vt1 @ X0)))),
% 3.88/1.18 inference('s_sup+', [status(thm)], [zip_derived_cl2684, zip_derived_cl68])).
% 3.88/1.18 thf(zip_derived_cl3524, plain, ( (visSomeTerm @ vnoTerm)),
% 3.88/1.18 inference('s_sup+', [status(thm)],
% 3.88/1.18 [zip_derived_cl268, zip_derived_cl3499])).
% 3.88/1.18 thf(zip_derived_cl3531, plain, ($false),
% 3.88/1.18 inference('demod', [status(thm)], [zip_derived_cl67, zip_derived_cl3524])).
% 3.88/1.18
% 3.88/1.18 % SZS output end Refutation
% 3.88/1.18
% 3.88/1.18
% 3.88/1.18 % Terminating...
% 4.40/1.24 % Runner terminated.
% 4.40/1.25 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------