%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM251_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.h7pc9YpZSv true
% Computer : n008.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 5.84s 1.45s
% Output : Refutation 5.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM251_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.h7pc9YpZSv true
% 0.16/0.34 % Computer : n008.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Mon May 4 19:42:58 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 % Running portfolio for 300 s
% 0.16/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Number of cores: 8
% 0.16/0.35 % Python version: Python 3.6.8
% 0.16/0.35 % Running in FO mode
% 0.57/0.65 % Total configuration time : 435
% 0.57/0.65 % Estimated wc time : 1092
% 0.57/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.58/0.71 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.58/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.58/0.75 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.58/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.58/0.75 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.58/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.58/0.76 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 5.84/1.45 % Solved by fo/fo7.sh.
% 5.84/1.45 % done 1483 iterations in 0.683s
% 5.84/1.45 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 5.84/1.45 % SZS output start Refutation
% 5.84/1.45 thf(vBinOpT_type, type, vBinOpT: $tType).
% 5.84/1.45 thf(vAval_type, type, vAval: $tType).
% 5.84/1.45 thf(vnat_type, type, vnat: $tType).
% 5.84/1.45 thf(vOptAType_type, type, vOptAType: $tType).
% 5.84/1.45 thf(vATMap_type, type, vATMap: $tType).
% 5.84/1.45 thf(vExp_type, type, vExp: $tType).
% 5.84/1.45 thf(vAType_type, type, vAType: $tType).
% 5.84/1.45 thf(vOptExp_type, type, vOptExp: $tType).
% 5.84/1.45 thf(vnoExp_type, type, vnoExp: vOptExp).
% 5.84/1.45 thf(sk__313_type, type, sk__313: vnat).
% 5.84/1.45 thf(vplus_type, type, vplus: vnat > vnat > vnat).
% 5.84/1.45 thf(vbinop_type, type, vbinop: vExp > vBinOpT > vExp > vExp).
% 5.84/1.45 thf(sk__33_type, type, sk__33: vOptExp > vExp).
% 5.84/1.45 thf(vsomeExp_type, type, vsomeExp: vExp > vOptExp).
% 5.84/1.45 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 5.84/1.45 thf(vaddop_type, type, vaddop: vBinOpT).
% 5.84/1.45 thf(sk__314_type, type, sk__314: vnat).
% 5.84/1.45 thf(vconstant_type, type, vconstant: vAval > vExp).
% 5.84/1.45 thf(sk__316_type, type, sk__316: vAval).
% 5.84/1.45 thf(vevalBinOp_type, type, vevalBinOp: vBinOpT > vAval > vAval > vOptExp).
% 5.84/1.45 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 5.84/1.45 thf(sk__315_type, type, sk__315: vBinOpT).
% 5.84/1.45 thf(sk__318_type, type, sk__318: vAval).
% 5.84/1.45 thf(vNum_type, type, vNum: vnat > vAval).
% 5.84/1.45 thf('evalBinOpProgress-addop-Num-Num', conjecture,
% 5.84/1.45 (![Vn1:vnat,Vn2:vnat,Vbot:vBinOpT,Va:vAval,Vatm:vATMap,Va1:vAval,Vat:vAType]:
% 5.84/1.45 ( ( ( ( Vbot ) = ( vaddop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 5.84/1.45 ( ( Va1 ) = ( vNum @ Vn2 ) ) &
% 5.84/1.45 ( ( vecheck @
% 5.84/1.45 Vatm @
% 5.84/1.45 ( vbinop @ ( vconstant @ Va ) @ Vbot @ ( vconstant @ Va1 ) ) ) =
% 5.84/1.45 ( vsomeAType @ Vat ) ) ) =>
% 5.84/1.45 ( ?[Veres:vExp]:
% 5.84/1.45 ( ( vevalBinOp @ Vbot @ Va @ Va1 ) = ( vsomeExp @ Veres ) ) ) ))).
% 5.84/1.45 thf(zf_stmt_0, negated_conjecture,
% 5.84/1.45 (~( ![Vn1:vnat,Vn2:vnat,Vbot:vBinOpT,Va:vAval,Vatm:vATMap,Va1:vAval,
% 5.84/1.45 Vat:vAType]:
% 5.84/1.45 ( ( ( ( Vbot ) = ( vaddop ) ) & ( ( Va ) = ( vNum @ Vn1 ) ) &
% 5.84/1.45 ( ( Va1 ) = ( vNum @ Vn2 ) ) &
% 5.84/1.45 ( ( vecheck @
% 5.84/1.45 Vatm @
% 5.84/1.45 ( vbinop @ ( vconstant @ Va ) @ Vbot @ ( vconstant @ Va1 ) ) ) =
% 5.84/1.45 ( vsomeAType @ Vat ) ) ) =>
% 5.84/1.45 ( ?[Veres:vExp]:
% 5.84/1.45 ( ( vevalBinOp @ Vbot @ Va @ Va1 ) = ( vsomeExp @ Veres ) ) ) ) )),
% 5.84/1.45 inference('cnf.neg', [status(esa)], [evalBinOpProgress-addop-Num-Num])).
% 5.84/1.45 thf(zip_derived_cl732, plain, (((sk__316) = (vNum @ sk__313))),
% 5.84/1.45 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.84/1.45 thf(zip_derived_cl733, plain, (((sk__318) = (vNum @ sk__314))),
% 5.84/1.45 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.84/1.45 thf('evalBinOp-0', axiom,
% 5.84/1.45 (![Vn1:vnat,Vn2:vnat]:
% 5.84/1.45 ( ( vevalBinOp @ vaddop @ ( vNum @ Vn1 ) @ ( vNum @ Vn2 ) ) =
% 5.84/1.45 ( vsomeExp @ ( vconstant @ ( vNum @ ( vplus @ Vn1 @ Vn2 ) ) ) ) ))).
% 5.84/1.45 thf(zip_derived_cl224, plain,
% 5.84/1.45 (![X0 : vnat, X1 : vnat]:
% 5.84/1.45 ((vevalBinOp @ vaddop @ (vNum @ X0) @ (vNum @ X1))
% 5.84/1.45 = (vsomeExp @ (vconstant @ (vNum @ (vplus @ X0 @ X1)))))),
% 5.84/1.45 inference('cnf', [status(esa)], [evalBinOp-0])).
% 5.84/1.45 thf(zip_derived_cl731, plain, (((sk__315) = (vaddop))),
% 5.84/1.45 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.84/1.45 thf(zip_derived_cl3998, plain,
% 5.84/1.45 (![X0 : vnat, X1 : vnat]:
% 5.84/1.45 ((vevalBinOp @ sk__315 @ (vNum @ X0) @ (vNum @ X1))
% 5.84/1.45 = (vsomeExp @ (vconstant @ (vNum @ (vplus @ X0 @ X1)))))),
% 5.84/1.45 inference('demod', [status(thm)], [zip_derived_cl224, zip_derived_cl731])).
% 5.84/1.45 thf(zip_derived_cl4000, plain,
% 5.84/1.45 (![X0 : vnat]:
% 5.84/1.45 ((vevalBinOp @ sk__315 @ (vNum @ X0) @ sk__318)
% 5.84/1.45 = (vsomeExp @ (vconstant @ (vNum @ (vplus @ X0 @ sk__314)))))),
% 5.84/1.45 inference('sup+', [status(thm)], [zip_derived_cl733, zip_derived_cl3998])).
% 5.84/1.45 thf(zip_derived_cl4005, plain,
% 5.84/1.45 (((vevalBinOp @ sk__315 @ sk__316 @ sk__318)
% 5.84/1.45 = (vsomeExp @ (vconstant @ (vNum @ (vplus @ sk__313 @ sk__314)))))),
% 5.84/1.45 inference('sup+', [status(thm)], [zip_derived_cl732, zip_derived_cl4000])).
% 5.84/1.45 thf('dom-OptExp', axiom,
% 5.84/1.45 (![VX:vOptExp]:
% 5.84/1.45 ( ( ?[VExp0:vExp]: ( ( VX ) = ( vsomeExp @ VExp0 ) ) ) |
% 5.84/1.45 ( ( VX ) = ( vnoExp ) ) ))).
% 5.84/1.45 thf(zip_derived_cl61, plain,
% 5.84/1.45 (![X0 : vOptExp]:
% 5.84/1.45 (((X0) = (vsomeExp @ (sk__33 @ X0))) | ((X0) = (vnoExp)))),
% 5.84/1.46 inference('cnf', [status(esa)], [dom-OptExp])).
% 5.84/1.46 thf(zip_derived_cl734, plain,
% 5.84/1.46 (![X0 : vExp]:
% 5.84/1.46 ((vevalBinOp @ sk__315 @ sk__316 @ sk__318) != (vsomeExp @ X0))),
% 5.84/1.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.84/1.46 thf(zip_derived_cl932, plain,
% 5.84/1.46 (![X0 : vOptExp]:
% 5.84/1.46 (((vevalBinOp @ sk__315 @ sk__316 @ sk__318) != (X0))
% 5.84/1.46 | ((X0) = (vnoExp)))),
% 5.84/1.46 inference('sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl734])).
% 5.84/1.46 thf(zip_derived_cl943, plain,
% 5.84/1.46 (((vevalBinOp @ sk__315 @ sk__316 @ sk__318) = (vnoExp))),
% 5.84/1.46 inference('eq_res', [status(thm)], [zip_derived_cl932])).
% 5.84/1.46 thf(zip_derived_cl4007, plain,
% 5.84/1.46 (((vnoExp)
% 5.84/1.46 = (vsomeExp @ (vconstant @ (vNum @ (vplus @ sk__313 @ sk__314)))))),
% 5.84/1.46 inference('demod', [status(thm)], [zip_derived_cl4005, zip_derived_cl943])).
% 5.84/1.46 thf('DIFF-noExp-someExp', axiom,
% 5.84/1.46 (![VExp0:vExp]: ( ( vnoExp ) != ( vsomeExp @ VExp0 ) ))).
% 5.84/1.46 thf(zip_derived_cl63, plain, (![X0 : vExp]: ((vnoExp) != (vsomeExp @ X0))),
% 5.84/1.46 inference('cnf', [status(esa)], [DIFF-noExp-someExp])).
% 5.84/1.46 thf(zip_derived_cl4008, plain, ($false),
% 5.84/1.46 inference('simplify_reflect-', [status(thm)],
% 5.84/1.46 [zip_derived_cl4007, zip_derived_cl63])).
% 5.84/1.46
% 5.84/1.46 % SZS output end Refutation
% 5.84/1.46
% 5.84/1.46
% 5.84/1.46 % Terminating...
% 6.49/1.57 % Runner terminated.
% 6.49/1.59 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------