%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM253_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.GRpWoapFuY true
% Computer : n006.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:22 PM UTC 2026
% Result : Theorem 0.56s 0.86s
% Output : Refutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM253_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.GRpWoapFuY true
% 0.15/0.34 % Computer : n006.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 19:45:31 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 % Running portfolio for 300 s
% 0.15/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Number of cores: 8
% 0.15/0.35 % Python version: Python 3.6.8
% 0.15/0.35 % Running in FO mode
% 0.55/0.64 % Total configuration time : 435
% 0.55/0.64 % Estimated wc time : 1092
% 0.55/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.70 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.73 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.86 % Solved by fo/fo4.sh.
% 0.56/0.86 % done 82 iterations in 0.077s
% 0.56/0.86 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.56/0.86 % SZS output start Refutation
% 0.56/0.86 thf(vOptAType_type, type, vOptAType: $tType).
% 0.56/0.86 thf(vQID_type, type, vQID: $tType).
% 0.56/0.86 thf(vATMap_type, type, vATMap: $tType).
% 0.56/0.86 thf(vAnsMap_type, type, vAnsMap: $tType).
% 0.56/0.86 thf(vAval_type, type, vAval: $tType).
% 0.56/0.86 thf(vAType_type, type, vAType: $tType).
% 0.56/0.86 thf(vOptAval_type, type, vOptAval: $tType).
% 0.56/0.86 thf('#_fresh_sk2_type', type, '#_fresh_sk2': vOptAval > vAval).
% 0.56/0.86 thf(sk__6_type, type, sk__6: vQID).
% 0.56/0.86 thf(vlookupAnsMap_type, type, vlookupAnsMap: vQID > vAnsMap > vOptAval).
% 0.56/0.86 thf(vam1_type, type, vam1: vAnsMap).
% 0.56/0.86 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 0.56/0.86 thf(vsomeAval_type, type, vsomeAval: vAval > vOptAval).
% 0.56/0.86 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 0.56/0.86 thf(sk__10_type, type, sk__10: vQID).
% 0.56/0.86 thf(vabind_type, type, vabind: vQID > vAval > vAnsMap > vAnsMap).
% 0.56/0.86 thf(vtypeOf_type, type, vtypeOf: vAval > vAType).
% 0.56/0.86 thf(sk__8_type, type, sk__8: vAType).
% 0.56/0.86 thf(sk__9_type, type, sk__9: vAval).
% 0.56/0.86 thf(vlookupATMap_type, type, vlookupATMap: vQID > vATMap > vOptAType).
% 0.56/0.86 thf(sk__7_type, type, sk__7: vAval).
% 0.56/0.86 thf('lookupAnsMapPreservation-abind', conjecture,
% 0.56/0.86 (![Vqid1:vQID,Va:vAval,Vat:vAType,Vavr:vAval,Vqid:vQID]:
% 0.56/0.86 ( ( ( ( vlookupATMap @ Vqid @ ( vtypeAM @ ( vabind @ Vqid1 @ Va @ vam1 ) ) ) =
% 0.56/0.86 ( vsomeAType @ Vat ) ) &
% 0.56/0.86 ( ( vlookupAnsMap @ Vqid @ ( vabind @ Vqid1 @ Va @ vam1 ) ) =
% 0.56/0.86 ( vsomeAval @ Vavr ) ) ) =>
% 0.56/0.86 ( ( vtypeOf @ Vavr ) = ( Vat ) ) ))).
% 0.56/0.86 thf(zf_stmt_0, negated_conjecture,
% 0.56/0.86 (~( ![Vqid1:vQID,Va:vAval,Vat:vAType,Vavr:vAval,Vqid:vQID]:
% 0.56/0.86 ( ( ( ( vlookupATMap @
% 0.56/0.86 Vqid @ ( vtypeAM @ ( vabind @ Vqid1 @ Va @ vam1 ) ) ) =
% 0.56/0.86 ( vsomeAType @ Vat ) ) &
% 0.56/0.86 ( ( vlookupAnsMap @ Vqid @ ( vabind @ Vqid1 @ Va @ vam1 ) ) =
% 0.56/0.86 ( vsomeAval @ Vavr ) ) ) =>
% 0.56/0.86 ( ( vtypeOf @ Vavr ) = ( Vat ) ) ) )),
% 0.56/0.86 inference('cnf.neg', [status(esa)], [lookupAnsMapPreservation-abind])).
% 0.56/0.86 thf(zip_derived_cl31, plain,
% 0.56/0.86 (((vlookupATMap @ sk__10 @ (vtypeAM @ (vabind @ sk__6 @ sk__7 @ vam1)))
% 0.56/0.86 = (vsomeAType @ sk__8))),
% 0.56/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.56/0.86 thf(zip_derived_cl31, plain,
% 0.56/0.86 (((vlookupATMap @ sk__10 @ (vtypeAM @ (vabind @ sk__6 @ sk__7 @ vam1)))
% 0.56/0.86 = (vsomeAType @ sk__8))),
% 0.56/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.56/0.86 thf('lookupAnsMapPreservation-abind-qid-qid1-False', axiom,
% 0.56/0.86 (![Vqid1:vQID,Va:vAval,Vat:vAType,Vavr:vAval,Vqid:vQID]:
% 0.56/0.86 ( ( ( ( Vqid ) != ( Vqid1 ) ) &
% 0.56/0.86 ( ( vlookupATMap @ Vqid @ ( vtypeAM @ ( vabind @ Vqid1 @ Va @ vam1 ) ) ) =
% 0.56/0.86 ( vsomeAType @ Vat ) ) &
% 0.56/0.86 ( ( vlookupAnsMap @ Vqid @ ( vabind @ Vqid1 @ Va @ vam1 ) ) =
% 0.56/0.86 ( vsomeAval @ Vavr ) ) ) =>
% 0.56/0.86 ( ( vtypeOf @ Vavr ) = ( Vat ) ) ))).
% 0.56/0.86 thf(zip_derived_cl29, plain,
% 0.56/0.86 (![X0 : vAType, X1 : vAval, X2 : vQID, X3 : vQID, X4 : vAval]:
% 0.56/0.86 (((vtypeOf @ X1) = (X0))
% 0.56/0.86 | ((X3) = (X2))
% 0.56/0.86 | ((vlookupATMap @ X3 @ (vtypeAM @ (vabind @ X2 @ X4 @ vam1)))
% 0.56/0.86 != (vsomeAType @ X0))
% 0.56/0.86 | ((vlookupAnsMap @ X3 @ (vabind @ X2 @ X4 @ vam1))
% 0.56/0.86 != (vsomeAval @ X1)))),
% 0.56/0.86 inference('cnf', [status(esa)],
% 0.56/0.86 [lookupAnsMapPreservation-abind-qid-qid1-False])).
% 0.56/0.86 thf(zip_derived_cl126, plain,
% 0.56/0.86 (![X0 : vAType, X1 : vAval]:
% 0.56/0.86 (((vsomeAType @ sk__8) != (vsomeAType @ X0))
% 0.56/0.86 | ((vlookupAnsMap @ sk__10 @ (vabind @ sk__6 @ sk__7 @ vam1))
% 0.56/0.86 != (vsomeAval @ X1))
% 0.56/0.86 | ((sk__10) = (sk__6))
% 0.56/0.86 | ((vtypeOf @ X1) = (X0)))),
% 0.56/0.86 inference('sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl29])).
% 0.56/0.86 thf(zip_derived_cl30, plain,
% 0.56/0.86 (((vlookupAnsMap @ sk__10 @ (vabind @ sk__6 @ sk__7 @ vam1))
% 0.56/0.86 = (vsomeAval @ sk__9))),
% 0.56/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.56/0.86 thf(zip_derived_cl129, plain,
% 0.56/0.86 (![X0 : vAType, X1 : vAval]:
% 0.56/0.86 (((vsomeAType @ sk__8) != (vsomeAType @ X0))
% 0.56/0.86 | ((vsomeAval @ sk__9) != (vsomeAval @ X1))
% 0.56/0.86 | ((sk__10) = (sk__6))
% 0.56/0.86 | ((vtypeOf @ X1) = (X0)))),
% 0.56/0.86 inference('demod', [status(thm)], [zip_derived_cl126, zip_derived_cl30])).
% 0.56/0.86 thf(zip_derived_cl132, plain,
% 0.56/0.86 (![X0 : vAval]:
% 0.56/0.86 (((vtypeOf @ X0) = (sk__8))
% 0.56/0.86 | ((sk__10) = (sk__6))
% 0.56/0.86 | ((vsomeAval @ sk__9) != (vsomeAval @ X0)))),
% 0.56/0.86 inference('eq_res', [status(thm)], [zip_derived_cl129])).
% 0.56/0.86 thf(zip_derived_cl133, plain,
% 0.56/0.86 ((((sk__10) = (sk__6)) | ((vtypeOf @ sk__9) = (sk__8)))),
% 0.56/0.86 inference('eq_res', [status(thm)], [zip_derived_cl132])).
% 0.56/0.86 thf(zip_derived_cl32, plain, (((vtypeOf @ sk__9) != (sk__8))),
% 0.56/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.56/0.86 thf(zip_derived_cl134, plain, (((sk__10) = (sk__6))),
% 0.56/0.86 inference('simplify_reflect-', [status(thm)],
% 0.56/0.86 [zip_derived_cl133, zip_derived_cl32])).
% 0.56/0.86 thf(zip_derived_cl136, plain,
% 0.56/0.86 (((vlookupATMap @ sk__6 @ (vtypeAM @ (vabind @ sk__6 @ sk__7 @ vam1)))
% 0.56/0.86 = (vsomeAType @ sk__8))),
% 0.56/0.86 inference('demod', [status(thm)], [zip_derived_cl31, zip_derived_cl134])).
% 0.56/0.86 thf('lookupAnsMapPreservation-abind-qid-qid1-True', axiom,
% 0.56/0.86 (![Vqid1:vQID,Va:vAval,Vat:vAType,Vavr:vAval]:
% 0.56/0.86 ( ( ( ( vlookupATMap @
% 0.56/0.86 Vqid1 @ ( vtypeAM @ ( vabind @ Vqid1 @ Va @ vam1 ) ) ) =
% 0.56/0.86 ( vsomeAType @ Vat ) ) &
% 0.56/0.86 ( ( vlookupAnsMap @ Vqid1 @ ( vabind @ Vqid1 @ Va @ vam1 ) ) =
% 0.56/0.86 ( vsomeAval @ Vavr ) ) ) =>
% 0.56/0.86 ( ( vtypeOf @ Vavr ) = ( Vat ) ) ))).
% 0.56/0.86 thf(zip_derived_cl28, plain,
% 0.56/0.86 (![X0 : vAType, X1 : vQID, X2 : vAval, X3 : vAval]:
% 0.56/0.86 (((vlookupATMap @ X1 @ (vtypeAM @ (vabind @ X1 @ X2 @ vam1)))
% 0.56/0.86 != (vsomeAType @ X0))
% 0.56/0.86 | ((vlookupAnsMap @ X1 @ (vabind @ X1 @ X2 @ vam1))
% 0.56/0.86 != (vsomeAval @ X3))
% 0.56/0.86 | ((vtypeOf @ X3) = (X0)))),
% 0.56/0.86 inference('cnf', [status(esa)],
% 0.56/0.86 [lookupAnsMapPreservation-abind-qid-qid1-True])).
% 0.56/0.86 thf('lookupAnsMap-1', axiom,
% 0.56/0.86 (![Vqid1:vQID,Vaval:vAval,Vaml:vAnsMap]:
% 0.56/0.86 ( ( vlookupAnsMap @ Vqid1 @ ( vabind @ Vqid1 @ Vaval @ Vaml ) ) =
% 0.56/0.86 ( vsomeAval @ Vaval ) ))).
% 0.56/0.86 thf(zip_derived_cl15, plain,
% 0.56/0.86 (![X0 : vAval, X1 : vQID, X2 : vAnsMap]:
% 0.56/0.86 ((vlookupAnsMap @ X1 @ (vabind @ X1 @ X0 @ X2)) = (vsomeAval @ X0))),
% 0.56/0.86 inference('cnf', [status(esa)], [lookupAnsMap-1])).
% 0.56/0.86 thf(zip_derived_cl119, plain,
% 0.56/0.86 (![X0 : vAType, X1 : vQID, X2 : vAval, X3 : vAval]:
% 0.56/0.86 (((vlookupATMap @ X1 @ (vtypeAM @ (vabind @ X1 @ X2 @ vam1)))
% 0.56/0.86 != (vsomeAType @ X0))
% 0.56/0.86 | ((vsomeAval @ X2) != (vsomeAval @ X3))
% 0.56/0.86 | ((vtypeOf @ X3) = (X0)))),
% 0.56/0.86 inference('demod', [status(thm)], [zip_derived_cl28, zip_derived_cl15])).
% 0.56/0.86 thf(zip_derived_cl150, plain,
% 0.56/0.86 (![X0 : vAType, X1 : vAval]:
% 0.56/0.86 (((vsomeAType @ sk__8) != (vsomeAType @ X0))
% 0.56/0.86 | ((vtypeOf @ X1) = (X0))
% 0.56/0.86 | ((vsomeAval @ sk__7) != (vsomeAval @ X1)))),
% 0.56/0.86 inference('sup-', [status(thm)], [zip_derived_cl136, zip_derived_cl119])).
% 0.56/0.86 thf(zip_derived_cl240, plain,
% 0.56/0.86 (![X0 : vAType]:
% 0.56/0.86 (((vtypeOf @ sk__7) = (X0))
% 0.56/0.86 | ((vsomeAType @ sk__8) != (vsomeAType @ X0)))),
% 0.56/0.86 inference('eq_res', [status(thm)], [zip_derived_cl150])).
% 0.56/0.86 thf('EQ-someAType', axiom,
% 0.56/0.86 (![VAType0:vAType,VAType1:vAType]:
% 0.56/0.86 ( ( ( vsomeAType @ VAType0 ) = ( vsomeAType @ VAType1 ) ) =>
% 0.56/0.86 ( ( VAType0 ) = ( VAType1 ) ) ))).
% 0.56/0.86 thf(zip_derived_cl0, plain,
% 0.56/0.86 (![X0 : vAType, X1 : vAType]:
% 0.56/0.86 (((X1) = (X0)) | ((vsomeAType @ X1) != (vsomeAType @ X0)))),
% 0.56/0.86 inference('cnf', [status(esa)], [EQ-someAType])).
% 0.56/0.86 thf(zip_derived_cl32, plain, (((vtypeOf @ sk__9) != (sk__8))),
% 0.56/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.56/0.86 thf(zip_derived_cl33, plain,
% 0.56/0.86 (![X0 : vAType]:
% 0.56/0.86 (((vtypeOf @ sk__9) != (X0))
% 0.56/0.86 | ((vsomeAType @ X0) != (vsomeAType @ sk__8)))),
% 0.56/0.86 inference('sup-', [status(thm)], [zip_derived_cl0, zip_derived_cl32])).
% 0.56/0.86 thf(zip_derived_cl30, plain,
% 0.56/0.86 (((vlookupAnsMap @ sk__10 @ (vabind @ sk__6 @ sk__7 @ vam1))
% 0.56/0.86 = (vsomeAval @ sk__9))),
% 0.56/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.56/0.86 thf(zip_derived_cl134, plain, (((sk__10) = (sk__6))),
% 0.56/0.86 inference('simplify_reflect-', [status(thm)],
% 0.56/0.86 [zip_derived_cl133, zip_derived_cl32])).
% 0.56/0.86 thf(zip_derived_cl15, plain,
% 0.56/0.86 (![X0 : vAval, X1 : vQID, X2 : vAnsMap]:
% 0.56/0.86 ((vlookupAnsMap @ X1 @ (vabind @ X1 @ X0 @ X2)) = (vsomeAval @ X0))),
% 0.56/0.86 inference('cnf', [status(esa)], [lookupAnsMap-1])).
% 0.56/0.86 thf(zip_derived_cl135, plain, (((vsomeAval @ sk__7) = (vsomeAval @ sk__9))),
% 0.56/0.86 inference('demod', [status(thm)],
% 0.56/0.86 [zip_derived_cl30, zip_derived_cl134, zip_derived_cl15])).
% 0.56/0.86 thf('EQ-someAval', axiom,
% 0.56/0.86 (![VAval0:vAval,VAval1:vAval]:
% 0.56/0.86 ( ( ( vsomeAval @ VAval0 ) = ( vsomeAval @ VAval1 ) ) =>
% 0.56/0.86 ( ( VAval0 ) = ( VAval1 ) ) ))).
% 0.56/0.86 thf(zip_derived_cl4, plain,
% 0.56/0.86 (![X0 : vAval, X1 : vAval]:
% 0.56/0.86 (((X1) = (X0)) | ((vsomeAval @ X1) != (vsomeAval @ X0)))),
% 0.56/0.86 inference('cnf', [status(esa)], [EQ-someAval])).
% 0.56/0.86 thf(zip_derived_cl38, plain,
% 0.56/0.86 (![X1 : vAval]: (('#_fresh_sk2' @ (vsomeAval @ X1)) = (X1))),
% 0.56/0.86 inference('inj_rec', [status(thm)], [zip_derived_cl4])).
% 0.56/0.86 thf(zip_derived_cl139, plain,
% 0.56/0.86 ((('#_fresh_sk2' @ (vsomeAval @ sk__7)) = (sk__9))),
% 0.56/0.86 inference('sup+', [status(thm)], [zip_derived_cl135, zip_derived_cl38])).
% 0.56/0.86 thf(zip_derived_cl38, plain,
% 0.56/0.86 (![X1 : vAval]: (('#_fresh_sk2' @ (vsomeAval @ X1)) = (X1))),
% 0.56/0.86 inference('inj_rec', [status(thm)], [zip_derived_cl4])).
% 0.56/0.86 thf(zip_derived_cl140, plain, (((sk__7) = (sk__9))),
% 0.56/0.86 inference('demod', [status(thm)], [zip_derived_cl139, zip_derived_cl38])).
% 0.56/0.86 thf(zip_derived_cl146, plain,
% 0.56/0.86 (![X0 : vAType]:
% 0.56/0.86 (((vtypeOf @ sk__7) != (X0))
% 0.56/0.86 | ((vsomeAType @ X0) != (vsomeAType @ sk__8)))),
% 0.56/0.86 inference('demod', [status(thm)], [zip_derived_cl33, zip_derived_cl140])).
% 0.56/0.86 thf(zip_derived_cl267, plain,
% 0.56/0.86 (![X0 : vAType]: ((vsomeAType @ sk__8) != (vsomeAType @ X0))),
% 0.56/0.86 inference('clc', [status(thm)], [zip_derived_cl240, zip_derived_cl146])).
% 0.56/0.86 thf(zip_derived_cl270, plain, ($false),
% 0.56/0.86 inference('eq_res', [status(thm)], [zip_derived_cl267])).
% 0.56/0.86
% 0.56/0.86 % SZS output end Refutation
% 0.56/0.86
% 0.56/0.86
% 0.56/0.86 % Terminating...
% 0.60/0.96 % Runner terminated.
% 0.60/0.97 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------