%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM264_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.9KGl1iSGaq 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 17.26s 3.09s
% Output : Refutation 17.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM264_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.9KGl1iSGaq true
% 0.16/0.34 % Computer : n006.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:58:45 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 % Running portfolio for 300 s
% 0.16/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Number of cores: 8
% 0.16/0.34 % Python version: Python 3.6.8
% 0.16/0.34 % Running in FO mode
% 0.44/0.60 % Total configuration time : 435
% 0.44/0.60 % Estimated wc time : 1092
% 0.44/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.51/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.51/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.51/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.52/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 17.26/3.09 % Solved by fo/fo4.sh.
% 17.26/3.09 % done 2386 iterations in 2.327s
% 17.26/3.09 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 17.26/3.09 % SZS output start Refutation
% 17.26/3.09 thf(vQuestionnaire_type, type, vQuestionnaire: $tType).
% 17.26/3.09 thf(vExp_type, type, vExp: $tType).
% 17.26/3.09 thf(vMapConf_type, type, vMapConf: $tType).
% 17.26/3.09 thf(vATMap_type, type, vATMap: $tType).
% 17.26/3.09 thf(vAnsMap_type, type, vAnsMap: $tType).
% 17.26/3.09 thf(vQMap_type, type, vQMap: $tType).
% 17.26/3.09 thf(vOptQConf_type, type, vOptQConf: $tType).
% 17.26/3.09 thf(vQConf_type, type, vQConf: $tType).
% 17.26/3.09 thf(vAval_type, type, vAval: $tType).
% 17.26/3.09 thf(vsomeQConf_type, type, vsomeQConf: vQConf > vOptQConf).
% 17.26/3.09 thf(sk__3_type, type, sk__3: vQConf > vQMap).
% 17.26/3.09 thf(sk__2_type, type, sk__2: vQConf > vAnsMap).
% 17.26/3.09 thf(vqcond_type, type, vqcond: vExp > vQuestionnaire > vQuestionnaire > vQuestionnaire).
% 17.26/3.09 thf(sk__32_type, type, sk__32: vATMap).
% 17.26/3.09 thf(sk__34_type, type, sk__34: vAnsMap).
% 17.26/3.09 thf(sk__31_type, type, sk__31: vATMap).
% 17.26/3.09 thf(vq1_type, type, vq1: vQuestionnaire).
% 17.26/3.09 thf(sk__24_type, type, sk__24: vAnsMap > vAval > vQMap > vQMap).
% 17.26/3.09 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 17.26/3.09 thf(visValue_type, type, visValue: vQuestionnaire > $o).
% 17.26/3.09 thf(sk__28_type, type, sk__28: vAnsMap > vExp > vQMap > vQMap).
% 17.26/3.09 thf(vtypeQM_type, type, vtypeQM: vQMap > vATMap).
% 17.26/3.09 thf(vptcheck_type, type, vptcheck: vMapConf > vQuestionnaire > vMapConf > $o).
% 17.26/3.09 thf(vMC_type, type, vMC: vATMap > vATMap > vMapConf).
% 17.26/3.09 thf(sk__29_type, type, sk__29: vAnsMap > vExp > vQMap > vQuestionnaire).
% 17.26/3.09 thf(vqempty_type, type, vqempty: vQuestionnaire).
% 17.26/3.09 thf(sk__33_type, type, sk__33: vExp).
% 17.26/3.09 thf(sk__4_type, type, sk__4: vQConf > vQuestionnaire).
% 17.26/3.09 thf(vconstant_type, type, vconstant: vAval > vExp).
% 17.26/3.09 thf(vreduce_type, type, vreduce: vQuestionnaire > vAnsMap > vQMap > vOptQConf).
% 17.26/3.09 thf(vq2_type, type, vq2: vQuestionnaire).
% 17.26/3.09 thf(vQC_type, type, vQC: vAnsMap > vQMap > vQuestionnaire > vQConf).
% 17.26/3.09 thf(sk__25_type, type, sk__25: vAnsMap > vAval > vQMap > vQuestionnaire).
% 17.26/3.09 thf(sk__27_type, type, sk__27: vAnsMap > vExp > vQMap > vAnsMap).
% 17.26/3.09 thf(sk__23_type, type, sk__23: vAnsMap > vAval > vQMap > vAnsMap).
% 17.26/3.09 thf(sk__30_type, type, sk__30: vQMap).
% 17.26/3.09 thf(sk__26_type, type, sk__26: vExp > vAval).
% 17.26/3.09 thf('Progress-qcond', conjecture,
% 17.26/3.09 (![Vqm:vQMap,Vatm2:vATMap,Vqtm2:vATMap,Ve:vExp,Vam:vAnsMap]:
% 17.26/3.09 ( ( ( ~( visValue @ ( vqcond @ Ve @ vq1 @ vq2 ) ) ) &
% 17.26/3.09 ( vptcheck @
% 17.26/3.09 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 17.26/3.09 ( vqcond @ Ve @ vq1 @ vq2 ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 17.26/3.09 ( ?[Vam0000:vAnsMap,Vqm0000:vQMap,Vq0000:vQuestionnaire]:
% 17.26/3.09 ( ( vreduce @ ( vqcond @ Ve @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 17.26/3.09 ( vsomeQConf @ ( vQC @ Vam0000 @ Vqm0000 @ Vq0000 ) ) ) ) ))).
% 17.26/3.09 thf(zf_stmt_0, negated_conjecture,
% 17.26/3.09 (~( ![Vqm:vQMap,Vatm2:vATMap,Vqtm2:vATMap,Ve:vExp,Vam:vAnsMap]:
% 17.26/3.09 ( ( ( ~( visValue @ ( vqcond @ Ve @ vq1 @ vq2 ) ) ) &
% 17.26/3.09 ( vptcheck @
% 17.26/3.09 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 17.26/3.09 ( vqcond @ Ve @ vq1 @ vq2 ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 17.26/3.09 ( ?[Vam0000:vAnsMap,Vqm0000:vQMap,Vq0000:vQuestionnaire]:
% 17.26/3.09 ( ( vreduce @ ( vqcond @ Ve @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 17.26/3.09 ( vsomeQConf @ ( vQC @ Vam0000 @ Vqm0000 @ Vq0000 ) ) ) ) ) )),
% 17.26/3.09 inference('cnf.neg', [status(esa)], [Progress-qcond])).
% 17.26/3.09 thf(zip_derived_cl47, plain,
% 17.26/3.09 ( (vptcheck @ (vMC @ (vtypeAM @ sk__34) @ (vtypeQM @ sk__30)) @
% 17.26/3.09 (vqcond @ sk__33 @ vq1 @ vq2) @ (vMC @ sk__31 @ sk__32))),
% 17.26/3.09 inference('cnf', [status(esa)], [zf_stmt_0])).
% 17.26/3.09 thf(zip_derived_cl47, plain,
% 17.26/3.09 ( (vptcheck @ (vMC @ (vtypeAM @ sk__34) @ (vtypeQM @ sk__30)) @
% 17.26/3.09 (vqcond @ sk__33 @ vq1 @ vq2) @ (vMC @ sk__31 @ sk__32))),
% 17.26/3.09 inference('cnf', [status(esa)], [zf_stmt_0])).
% 17.26/3.09 thf('Progress-qcond-e', axiom,
% 17.26/3.09 (![Vqm:vQMap,Vatm2:vATMap,Vqtm2:vATMap,Ve:vExp,Vam:vAnsMap]:
% 17.26/3.09 ( ( ( ![Va000:vAval]: ( ( Ve ) != ( vconstant @ Va000 ) ) ) &
% 17.26/3.09 ( ~( visValue @ ( vqcond @ Ve @ vq1 @ vq2 ) ) ) &
% 17.26/3.09 ( vptcheck @
% 17.26/3.09 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 17.26/3.09 ( vqcond @ Ve @ vq1 @ vq2 ) @ ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 17.26/3.09 ( ?[Vam0000:vAnsMap,Vqm0000:vQMap,Vq0000:vQuestionnaire]:
% 17.26/3.09 ( ( vreduce @ ( vqcond @ Ve @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 17.26/3.09 ( vsomeQConf @ ( vQC @ Vam0000 @ Vqm0000 @ Vq0000 ) ) ) ) ))).
% 17.26/3.09 thf(zip_derived_cl45, plain,
% 17.26/3.09 (![X0 : vExp, X1 : vAnsMap, X2 : vQMap, X3 : vATMap, X4 : vATMap]:
% 17.26/3.09 ( (visValue @ (vqcond @ X0 @ vq1 @ vq2))
% 17.26/3.09 | ((X0) = (vconstant @ (sk__26 @ X0)))
% 17.26/3.09 | ~ (vptcheck @ (vMC @ (vtypeAM @ X1) @ (vtypeQM @ X2)) @
% 17.26/3.09 (vqcond @ X0 @ vq1 @ vq2) @ (vMC @ X3 @ X4))
% 17.26/3.09 | ((vreduce @ (vqcond @ X0 @ vq1 @ vq2) @ X1 @ X2)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__27 @ X1 @ X0 @ X2) @ (sk__28 @ X1 @ X0 @ X2) @
% 17.26/3.09 (sk__29 @ X1 @ X0 @ X2)))))),
% 17.26/3.09 inference('cnf', [status(esa)], [Progress-qcond-e])).
% 17.26/3.09 thf('isValue-1', axiom,
% 17.26/3.09 (![VwildcardName0:vQuestionnaire]:
% 17.26/3.09 ( ( ( VwildcardName0 ) != ( vqempty ) ) =>
% 17.26/3.09 ( ~( visValue @ VwildcardName0 ) ) ))).
% 17.26/3.09 thf(zip_derived_cl15, plain,
% 17.26/3.09 (![X0 : vQuestionnaire]: (~ (visValue @ X0) | ((X0) = (vqempty)))),
% 17.26/3.09 inference('cnf', [status(esa)], [isValue-1])).
% 17.26/3.09 thf('DIFF-qempty-qcond', axiom,
% 17.26/3.09 (![VExp0:vExp,VQuestionnaire0:vQuestionnaire,VQuestionnaire1:vQuestionnaire]:
% 17.26/3.09 ( ( vqempty ) != ( vqcond @ VExp0 @ VQuestionnaire0 @ VQuestionnaire1 ) ))).
% 17.26/3.09 thf(zip_derived_cl6, plain,
% 17.26/3.09 (![X0 : vExp, X1 : vQuestionnaire, X2 : vQuestionnaire]:
% 17.26/3.09 ((vqempty) != (vqcond @ X0 @ X1 @ X2))),
% 17.26/3.09 inference('cnf', [status(esa)], [DIFF-qempty-qcond])).
% 17.26/3.09 thf(zip_derived_cl52, plain,
% 17.26/3.09 (![X0 : vQuestionnaire, X1 : vQuestionnaire, X2 : vQuestionnaire,
% 17.26/3.09 X3 : vExp]: (((X0) != (vqcond @ X3 @ X2 @ X1)) | ~ (visValue @ X0))),
% 17.26/3.09 inference('sup-', [status(thm)], [zip_derived_cl15, zip_derived_cl6])).
% 17.26/3.09 thf(zip_derived_cl63, plain,
% 17.26/3.09 (![X0 : vQuestionnaire, X1 : vQuestionnaire, X2 : vExp]:
% 17.26/3.09 ~ (visValue @ (vqcond @ X2 @ X1 @ X0))),
% 17.26/3.09 inference('eq_res', [status(thm)], [zip_derived_cl52])).
% 17.26/3.09 thf(zip_derived_cl975, plain,
% 17.26/3.09 (![X0 : vExp, X1 : vAnsMap, X2 : vQMap, X3 : vATMap, X4 : vATMap]:
% 17.26/3.09 (((X0) = (vconstant @ (sk__26 @ X0)))
% 17.26/3.09 | ~ (vptcheck @ (vMC @ (vtypeAM @ X1) @ (vtypeQM @ X2)) @
% 17.26/3.09 (vqcond @ X0 @ vq1 @ vq2) @ (vMC @ X3 @ X4))
% 17.26/3.09 | ((vreduce @ (vqcond @ X0 @ vq1 @ vq2) @ X1 @ X2)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__27 @ X1 @ X0 @ X2) @ (sk__28 @ X1 @ X0 @ X2) @
% 17.26/3.09 (sk__29 @ X1 @ X0 @ X2)))))),
% 17.26/3.09 inference('demod', [status(thm)], [zip_derived_cl45, zip_derived_cl63])).
% 17.26/3.09 thf(zip_derived_cl976, plain,
% 17.26/3.09 ((((vreduce @ (vqcond @ sk__33 @ vq1 @ vq2) @ sk__34 @ sk__30)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__27 @ sk__34 @ sk__33 @ sk__30) @
% 17.26/3.09 (sk__28 @ sk__34 @ sk__33 @ sk__30) @
% 17.26/3.09 (sk__29 @ sk__34 @ sk__33 @ sk__30))))
% 17.26/3.09 | ((sk__33) = (vconstant @ (sk__26 @ sk__33))))),
% 17.26/3.09 inference('sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl975])).
% 17.26/3.09 thf('dom-QConf', axiom,
% 17.26/3.09 (![VX:vQConf]:
% 17.26/3.09 ( ?[VAnsMap0:vAnsMap,VQMap0:vQMap,VQuestionnaire0:vQuestionnaire]:
% 17.26/3.09 ( ( VX ) = ( vQC @ VAnsMap0 @ VQMap0 @ VQuestionnaire0 ) ) ))).
% 17.26/3.09 thf(zip_derived_cl10, plain,
% 17.26/3.09 (![X0 : vQConf]:
% 17.26/3.09 ((X0) = (vQC @ (sk__2 @ X0) @ (sk__3 @ X0) @ (sk__4 @ X0)))),
% 17.26/3.09 inference('cnf', [status(esa)], [dom-QConf])).
% 17.26/3.09 thf(zip_derived_cl46, plain,
% 17.26/3.09 (![X0 : vAnsMap, X1 : vQMap, X2 : vQuestionnaire]:
% 17.26/3.09 ((vreduce @ (vqcond @ sk__33 @ vq1 @ vq2) @ sk__34 @ sk__30)
% 17.26/3.09 != (vsomeQConf @ (vQC @ X0 @ X1 @ X2)))),
% 17.26/3.09 inference('cnf', [status(esa)], [zf_stmt_0])).
% 17.26/3.09 thf(zip_derived_cl150, plain,
% 17.26/3.09 (![X0 : vQConf]:
% 17.26/3.09 ((vreduce @ (vqcond @ sk__33 @ vq1 @ vq2) @ sk__34 @ sk__30)
% 17.26/3.09 != (vsomeQConf @ X0))),
% 17.26/3.09 inference('sup-', [status(thm)], [zip_derived_cl10, zip_derived_cl46])).
% 17.26/3.09 thf(zip_derived_cl994, plain, (((sk__33) = (vconstant @ (sk__26 @ sk__33)))),
% 17.26/3.09 inference('simplify_reflect-', [status(thm)],
% 17.26/3.09 [zip_derived_cl976, zip_derived_cl150])).
% 17.26/3.09 thf('Progress-qcond-constant', axiom,
% 17.26/3.09 (![Vqm:vQMap,Vatm2:vATMap,Vqtm2:vATMap,Va:vAval,Vam:vAnsMap]:
% 17.26/3.09 ( ( ( ~( visValue @ ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) ) ) &
% 17.26/3.09 ( vptcheck @
% 17.26/3.09 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 17.26/3.09 ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) @
% 17.26/3.09 ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 17.26/3.09 ( ?[Vam00000:vAnsMap,Vqm00000:vQMap,Vq00000:vQuestionnaire]:
% 17.26/3.09 ( ( vreduce @ ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 17.26/3.09 ( vsomeQConf @ ( vQC @ Vam00000 @ Vqm00000 @ Vq00000 ) ) ) ) ))).
% 17.26/3.09 thf(zip_derived_cl44, plain,
% 17.26/3.09 (![X0 : vAval, X1 : vAnsMap, X2 : vQMap, X3 : vATMap, X4 : vATMap]:
% 17.26/3.09 ( (visValue @ (vqcond @ (vconstant @ X0) @ vq1 @ vq2))
% 17.26/3.09 | ~ (vptcheck @ (vMC @ (vtypeAM @ X1) @ (vtypeQM @ X2)) @
% 17.26/3.09 (vqcond @ (vconstant @ X0) @ vq1 @ vq2) @ (vMC @ X3 @ X4))
% 17.26/3.09 | ((vreduce @ (vqcond @ (vconstant @ X0) @ vq1 @ vq2) @ X1 @ X2)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__23 @ X1 @ X0 @ X2) @ (sk__24 @ X1 @ X0 @ X2) @
% 17.26/3.09 (sk__25 @ X1 @ X0 @ X2)))))),
% 17.26/3.09 inference('cnf', [status(esa)], [Progress-qcond-constant])).
% 17.26/3.09 thf(zip_derived_cl63, plain,
% 17.26/3.09 (![X0 : vQuestionnaire, X1 : vQuestionnaire, X2 : vExp]:
% 17.26/3.09 ~ (visValue @ (vqcond @ X2 @ X1 @ X0))),
% 17.26/3.09 inference('eq_res', [status(thm)], [zip_derived_cl52])).
% 17.26/3.09 thf(zip_derived_cl919, plain,
% 17.26/3.09 (![X0 : vAval, X1 : vAnsMap, X2 : vQMap, X3 : vATMap, X4 : vATMap]:
% 17.26/3.09 (~ (vptcheck @ (vMC @ (vtypeAM @ X1) @ (vtypeQM @ X2)) @
% 17.26/3.09 (vqcond @ (vconstant @ X0) @ vq1 @ vq2) @ (vMC @ X3 @ X4))
% 17.26/3.09 | ((vreduce @ (vqcond @ (vconstant @ X0) @ vq1 @ vq2) @ X1 @ X2)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__23 @ X1 @ X0 @ X2) @ (sk__24 @ X1 @ X0 @ X2) @
% 17.26/3.09 (sk__25 @ X1 @ X0 @ X2)))))),
% 17.26/3.09 inference('demod', [status(thm)], [zip_derived_cl44, zip_derived_cl63])).
% 17.26/3.09 thf(zip_derived_cl999, plain,
% 17.26/3.09 (![X0 : vATMap, X1 : vATMap, X2 : vQMap, X3 : vAnsMap]:
% 17.26/3.09 (~ (vptcheck @ (vMC @ (vtypeAM @ X3) @ (vtypeQM @ X2)) @
% 17.26/3.09 (vqcond @ sk__33 @ vq1 @ vq2) @ (vMC @ X1 @ X0))
% 17.26/3.09 | ((vreduce @
% 17.26/3.09 (vqcond @ (vconstant @ (sk__26 @ sk__33)) @ vq1 @ vq2) @ X3 @ X2)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__23 @ X3 @ (sk__26 @ sk__33) @ X2) @
% 17.26/3.09 (sk__24 @ X3 @ (sk__26 @ sk__33) @ X2) @
% 17.26/3.09 (sk__25 @ X3 @ (sk__26 @ sk__33) @ X2)))))),
% 17.26/3.09 inference('sup-', [status(thm)], [zip_derived_cl994, zip_derived_cl919])).
% 17.26/3.09 thf(zip_derived_cl994, plain, (((sk__33) = (vconstant @ (sk__26 @ sk__33)))),
% 17.26/3.09 inference('simplify_reflect-', [status(thm)],
% 17.26/3.09 [zip_derived_cl976, zip_derived_cl150])).
% 17.26/3.09 thf(zip_derived_cl1000, plain,
% 17.26/3.09 (![X0 : vATMap, X1 : vATMap, X2 : vQMap, X3 : vAnsMap]:
% 17.26/3.09 (~ (vptcheck @ (vMC @ (vtypeAM @ X3) @ (vtypeQM @ X2)) @
% 17.26/3.09 (vqcond @ sk__33 @ vq1 @ vq2) @ (vMC @ X1 @ X0))
% 17.26/3.09 | ((vreduce @ (vqcond @ sk__33 @ vq1 @ vq2) @ X3 @ X2)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__23 @ X3 @ (sk__26 @ sk__33) @ X2) @
% 17.26/3.09 (sk__24 @ X3 @ (sk__26 @ sk__33) @ X2) @
% 17.26/3.09 (sk__25 @ X3 @ (sk__26 @ sk__33) @ X2)))))),
% 17.26/3.09 inference('demod', [status(thm)], [zip_derived_cl999, zip_derived_cl994])).
% 17.26/3.09 thf(zip_derived_cl9815, plain,
% 17.26/3.09 (((vreduce @ (vqcond @ sk__33 @ vq1 @ vq2) @ sk__34 @ sk__30)
% 17.26/3.09 = (vsomeQConf @
% 17.26/3.09 (vQC @ (sk__23 @ sk__34 @ (sk__26 @ sk__33) @ sk__30) @
% 17.26/3.09 (sk__24 @ sk__34 @ (sk__26 @ sk__33) @ sk__30) @
% 17.26/3.09 (sk__25 @ sk__34 @ (sk__26 @ sk__33) @ sk__30))))),
% 17.26/3.09 inference('sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl1000])).
% 17.26/3.09 thf(zip_derived_cl150, plain,
% 17.26/3.09 (![X0 : vQConf]:
% 17.26/3.09 ((vreduce @ (vqcond @ sk__33 @ vq1 @ vq2) @ sk__34 @ sk__30)
% 17.26/3.09 != (vsomeQConf @ X0))),
% 17.26/3.09 inference('sup-', [status(thm)], [zip_derived_cl10, zip_derived_cl46])).
% 17.26/3.09 thf(zip_derived_cl9871, plain, ($false),
% 17.26/3.09 inference('simplify_reflect-', [status(thm)],
% 17.26/3.09 [zip_derived_cl9815, zip_derived_cl150])).
% 17.26/3.09
% 17.26/3.09 % SZS output end Refutation
% 17.26/3.09
% 17.26/3.09
% 17.26/3.09 % Terminating...
% 3.67/3.15 % Runner terminated.
% 3.67/3.15 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------