%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM265_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.mWcabs2oyU true
% Computer : n013.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:23 PM UTC 2026
% Result : Theorem 40.82s 6.45s
% Output : Refutation 40.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM265_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.mWcabs2oyU true
% 0.16/0.34 % Computer : n013.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:56 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.35 % Running in FO mode
% 0.44/0.62 % Total configuration time : 435
% 0.44/0.62 % Estimated wc time : 1092
% 0.44/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 40.82/6.45 % Solved by fo/fo3_bce.sh.
% 40.82/6.45 % BCE start: 705
% 40.82/6.45 % BCE eliminated: 0
% 40.82/6.45 % PE start: 705
% 40.82/6.45 logic: eq
% 40.82/6.45 % PE eliminated: -336
% 40.82/6.45 % done 2428 iterations in 5.699s
% 40.82/6.45 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 40.82/6.45 % SZS output start Refutation
% 40.82/6.45 thf(vAval_type, type, vAval: $tType).
% 40.82/6.45 thf(vYN_type, type, vYN: $tType).
% 40.82/6.45 thf(vAType_type, type, vAType: $tType).
% 40.82/6.45 thf(vnat_type, type, vnat: $tType).
% 40.82/6.45 thf(vstring_type, type, vstring: $tType).
% 40.82/6.45 thf(vQuestionnaire_type, type, vQuestionnaire: $tType).
% 40.82/6.45 thf(vExp_type, type, vExp: $tType).
% 40.82/6.45 thf(vMapConf_type, type, vMapConf: $tType).
% 40.82/6.45 thf(vATMap_type, type, vATMap: $tType).
% 40.82/6.45 thf(vAnsMap_type, type, vAnsMap: $tType).
% 40.82/6.45 thf(vQMap_type, type, vQMap: $tType).
% 40.82/6.45 thf(vOptQConf_type, type, vOptQConf: $tType).
% 40.82/6.45 thf(vQConf_type, type, vQConf: $tType).
% 40.82/6.45 thf(vOptAType_type, type, vOptAType: $tType).
% 40.82/6.45 thf(vsomeQConf_type, type, vsomeQConf: vQConf > vOptQConf).
% 40.82/6.45 thf(sk__57_type, type, sk__57: vAval > vYN).
% 40.82/6.45 thf(vnoQConf_type, type, vnoQConf: vOptQConf).
% 40.82/6.45 thf(sk__47_type, type, sk__47: vQConf > vAnsMap).
% 40.82/6.45 thf(vB_type, type, vB: vYN > vAval).
% 40.82/6.45 thf(zip_tseitin_3_type, type, zip_tseitin_3: vYN > vAval > $o).
% 40.82/6.45 thf(sk__347_type, type, sk__347: vAnsMap).
% 40.82/6.45 thf(vqcond_type, type, vqcond: vExp > vQuestionnaire > vQuestionnaire > vQuestionnaire).
% 40.82/6.45 thf(zip_tseitin_5_type, type, zip_tseitin_5: vstring > vAval > $o).
% 40.82/6.45 thf(sk__32_type, type, sk__32: vOptQConf > vQConf).
% 40.82/6.45 thf(sk__340_type, type, sk__340: vAnsMap > vYN > vQMap > vAnsMap).
% 40.82/6.45 thf(sk__56_type, type, sk__56: vAval > vnat).
% 40.82/6.45 thf(vecheck_type, type, vecheck: vATMap > vExp > vOptAType).
% 40.82/6.45 thf(sk__343_type, type, sk__343: vQMap).
% 40.82/6.45 thf(vq1_type, type, vq1: vQuestionnaire).
% 40.82/6.45 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 40.82/6.45 thf(sk__344_type, type, sk__344: vATMap).
% 40.82/6.45 thf(visValue_type, type, visValue: vQuestionnaire > $o).
% 40.82/6.45 thf(sk__345_type, type, sk__345: vATMap).
% 40.82/6.45 thf(vtypeQM_type, type, vtypeQM: vQMap > vATMap).
% 40.82/6.45 thf(vptcheck_type, type, vptcheck: vMapConf > vQuestionnaire > vMapConf > $o).
% 40.82/6.45 thf(vnoAType_type, type, vnoAType: vOptAType).
% 40.82/6.45 thf(sk__55_type, type, sk__55: vAval > vstring).
% 40.82/6.45 thf(zip_tseitin_4_type, type, zip_tseitin_4: vnat > vAval > $o).
% 40.82/6.45 thf(sk__346_type, type, sk__346: vAval).
% 40.82/6.45 thf(vMC_type, type, vMC: vATMap > vATMap > vMapConf).
% 40.82/6.45 thf(sk__49_type, type, sk__49: vQConf > vQuestionnaire).
% 40.82/6.45 thf(vsomeAType_type, type, vsomeAType: vAType > vOptAType).
% 40.82/6.45 thf(vtypeOf_type, type, vtypeOf: vAval > vAType).
% 40.82/6.45 thf(vYesNo_type, type, vYesNo: vAType).
% 40.82/6.45 thf(sk__48_type, type, sk__48: vQConf > vQMap).
% 40.82/6.45 thf(vconstant_type, type, vconstant: vAval > vExp).
% 40.82/6.45 thf(vreduce_type, type, vreduce: vQuestionnaire > vAnsMap > vQMap > vOptQConf).
% 40.82/6.45 thf(vText_type, type, vText: vAType).
% 40.82/6.45 thf(vq2_type, type, vq2: vQuestionnaire).
% 40.82/6.45 thf(vQC_type, type, vQC: vAnsMap > vQMap > vQuestionnaire > vQConf).
% 40.82/6.45 thf(vT_type, type, vT: vstring > vAval).
% 40.82/6.45 thf(sk__342_type, type, sk__342: vAnsMap > vYN > vQMap > vQuestionnaire).
% 40.82/6.45 thf(sk__33_type, type, sk__33: vOptAType > vAType).
% 40.82/6.45 thf(sk__341_type, type, sk__341: vAnsMap > vYN > vQMap > vQMap).
% 40.82/6.45 thf(vNum_type, type, vNum: vnat > vAval).
% 40.82/6.45 thf(vNumber_type, type, vNumber: vAType).
% 40.82/6.45 thf('typeOf-INV', axiom,
% 40.82/6.45 (![VAval0:vAval]:
% 40.82/6.45 ( ( ?[VwildcardName00:vYN]:
% 40.82/6.45 ( ( ( VAval0 ) = ( vB @ VwildcardName00 ) ) &
% 40.82/6.45 ( ( vtypeOf @ VAval0 ) = ( vYesNo ) ) ) ) |
% 40.82/6.45 ( ?[VwildcardName01:vnat]:
% 40.82/6.45 ( ( ( VAval0 ) = ( vNum @ VwildcardName01 ) ) &
% 40.82/6.45 ( ( vtypeOf @ VAval0 ) = ( vNumber ) ) ) ) |
% 40.82/6.45 ( ?[VwildcardName02:vstring]:
% 40.82/6.45 ( ( ( VAval0 ) = ( vT @ VwildcardName02 ) ) &
% 40.82/6.45 ( ( vtypeOf @ VAval0 ) = ( vText ) ) ) ) ))).
% 40.82/6.45 thf(zf_stmt_0, type, zip_tseitin_5 : vstring > vAval > $o).
% 40.82/6.45 thf(zf_stmt_1, axiom,
% 40.82/6.45 (![VwildcardName02:vstring,VAval0:vAval]:
% 40.82/6.45 ( ( zip_tseitin_5 @ VwildcardName02 @ VAval0 ) =>
% 40.82/6.45 ( ( ( vtypeOf @ VAval0 ) = ( vText ) ) &
% 40.82/6.45 ( ( VAval0 ) = ( vT @ VwildcardName02 ) ) ) ))).
% 40.82/6.45 thf(zf_stmt_2, type, zip_tseitin_4 : vnat > vAval > $o).
% 40.82/6.45 thf(zf_stmt_3, axiom,
% 40.82/6.45 (![VwildcardName01:vnat,VAval0:vAval]:
% 40.82/6.45 ( ( zip_tseitin_4 @ VwildcardName01 @ VAval0 ) =>
% 40.82/6.45 ( ( ( vtypeOf @ VAval0 ) = ( vNumber ) ) &
% 40.82/6.45 ( ( VAval0 ) = ( vNum @ VwildcardName01 ) ) ) ))).
% 40.82/6.45 thf(zf_stmt_4, type, zip_tseitin_3 : vYN > vAval > $o).
% 40.82/6.45 thf(zf_stmt_5, axiom,
% 40.82/6.45 (![VwildcardName00:vYN,VAval0:vAval]:
% 40.82/6.45 ( ( zip_tseitin_3 @ VwildcardName00 @ VAval0 ) =>
% 40.82/6.45 ( ( ( vtypeOf @ VAval0 ) = ( vYesNo ) ) &
% 40.82/6.45 ( ( VAval0 ) = ( vB @ VwildcardName00 ) ) ) ))).
% 40.82/6.45 thf(zf_stmt_6, axiom,
% 40.82/6.45 (![VAval0:vAval]:
% 40.82/6.45 ( ( ?[VwildcardName02:vstring]:
% 40.82/6.45 ( zip_tseitin_5 @ VwildcardName02 @ VAval0 ) ) |
% 40.82/6.45 ( ?[VwildcardName01:vnat]: ( zip_tseitin_4 @ VwildcardName01 @ VAval0 ) ) |
% 40.82/6.45 ( ?[VwildcardName00:vYN]: ( zip_tseitin_3 @ VwildcardName00 @ VAval0 ) ) ))).
% 40.82/6.45 thf(zip_derived_cl133, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 ( (zip_tseitin_5 @ (sk__55 @ X0) @ X0)
% 40.82/6.45 | (zip_tseitin_4 @ (sk__56 @ X0) @ X0)
% 40.82/6.45 | (zip_tseitin_3 @ (sk__57 @ X0) @ X0))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_6])).
% 40.82/6.45 thf(zip_derived_cl128, plain,
% 40.82/6.45 (![X0 : vYN, X1 : vAval]:
% 40.82/6.45 (((X1) = (vB @ X0)) | ~ (zip_tseitin_3 @ X0 @ X1))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_5])).
% 40.82/6.45 thf(zip_derived_cl2136, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 ( (zip_tseitin_4 @ (sk__56 @ X0) @ X0)
% 40.82/6.45 | (zip_tseitin_5 @ (sk__55 @ X0) @ X0)
% 40.82/6.45 | ((X0) = (vB @ (sk__57 @ X0))))),
% 40.82/6.45 inference('dp-resolution', [status(thm)],
% 40.82/6.45 [zip_derived_cl133, zip_derived_cl128])).
% 40.82/6.45 thf(zip_derived_cl130, plain,
% 40.82/6.45 (![X0 : vnat, X1 : vAval]:
% 40.82/6.45 (((X1) = (vNum @ X0)) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_3])).
% 40.82/6.45 thf(zip_derived_cl2169, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 (((X0) = (vB @ (sk__57 @ X0)))
% 40.82/6.45 | (zip_tseitin_5 @ (sk__55 @ X0) @ X0)
% 40.82/6.45 | ((X0) = (vNum @ (sk__56 @ X0))))),
% 40.82/6.45 inference('dp-resolution', [status(thm)],
% 40.82/6.45 [zip_derived_cl2136, zip_derived_cl130])).
% 40.82/6.45 thf(zip_derived_cl131, plain,
% 40.82/6.45 (![X0 : vAval, X1 : vstring]:
% 40.82/6.45 (((vtypeOf @ X0) = (vText)) | ~ (zip_tseitin_5 @ X1 @ X0))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_1])).
% 40.82/6.45 thf(zip_derived_cl2224, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 (((X0) = (vNum @ (sk__56 @ X0)))
% 40.82/6.45 | ((X0) = (vB @ (sk__57 @ X0)))
% 40.82/6.45 | ((vtypeOf @ X0) = (vText)))),
% 40.82/6.45 inference('dp-resolution', [status(thm)],
% 40.82/6.45 [zip_derived_cl2169, zip_derived_cl131])).
% 40.82/6.45 thf('Progress-qcond-constant', conjecture,
% 40.82/6.45 (![Vqm:vQMap,Vatm2:vATMap,Vqtm2:vATMap,Va:vAval,Vam:vAnsMap]:
% 40.82/6.45 ( ( ( ~( visValue @ ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) ) ) &
% 40.82/6.45 ( vptcheck @
% 40.82/6.45 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 40.82/6.45 ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) @
% 40.82/6.45 ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 40.82/6.45 ( ?[Vam00000:vAnsMap,Vqm00000:vQMap,Vq00000:vQuestionnaire]:
% 40.82/6.45 ( ( vreduce @ ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 40.82/6.45 ( vsomeQConf @ ( vQC @ Vam00000 @ Vqm00000 @ Vq00000 ) ) ) ) ))).
% 40.82/6.45 thf(zf_stmt_7, negated_conjecture,
% 40.82/6.45 (~( ![Vqm:vQMap,Vatm2:vATMap,Vqtm2:vATMap,Va:vAval,Vam:vAnsMap]:
% 40.82/6.45 ( ( ( ~( visValue @ ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) ) ) &
% 40.82/6.45 ( vptcheck @
% 40.82/6.45 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 40.82/6.45 ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) @
% 40.82/6.45 ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 40.82/6.45 ( ?[Vam00000:vAnsMap,Vqm00000:vQMap,Vq00000:vQuestionnaire]:
% 40.82/6.45 ( ( vreduce @
% 40.82/6.45 ( vqcond @ ( vconstant @ Va ) @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 40.82/6.45 ( vsomeQConf @ ( vQC @ Vam00000 @ Vqm00000 @ Vq00000 ) ) ) ) ) )),
% 40.82/6.45 inference('cnf.neg', [status(esa)], [Progress-qcond-constant])).
% 40.82/6.45 thf(zip_derived_cl703, plain,
% 40.82/6.45 ( (vptcheck @ (vMC @ (vtypeAM @ sk__347) @ (vtypeQM @ sk__343)) @
% 40.82/6.45 (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @
% 40.82/6.45 (vMC @ sk__344 @ sk__345))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_7])).
% 40.82/6.45 thf('Progress-qcond-constant-B', axiom,
% 40.82/6.45 (![Vqm:vQMap,Vyn:vYN,Vatm2:vATMap,Vqtm2:vATMap,Vam:vAnsMap]:
% 40.82/6.45 ( ( ( ~( visValue @ ( vqcond @ ( vconstant @ ( vB @ Vyn ) ) @ vq1 @ vq2 ) ) ) &
% 40.82/6.45 ( vptcheck @
% 40.82/6.45 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 40.82/6.45 ( vqcond @ ( vconstant @ ( vB @ Vyn ) ) @ vq1 @ vq2 ) @
% 40.82/6.45 ( vMC @ Vatm2 @ Vqtm2 ) ) ) =>
% 40.82/6.45 ( ?[Vam000000:vAnsMap,Vqm000000:vQMap,Vq000000:vQuestionnaire]:
% 40.82/6.45 ( ( vreduce @
% 40.82/6.45 ( vqcond @ ( vconstant @ ( vB @ Vyn ) ) @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 40.82/6.45 ( vsomeQConf @ ( vQC @ Vam000000 @ Vqm000000 @ Vq000000 ) ) ) ) ))).
% 40.82/6.45 thf(zip_derived_cl701, plain,
% 40.82/6.45 (![X0 : vYN, X1 : vAnsMap, X2 : vQMap, X3 : vATMap, X4 : vATMap]:
% 40.82/6.45 ( (visValue @ (vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2))
% 40.82/6.45 | ~ (vptcheck @ (vMC @ (vtypeAM @ X1) @ (vtypeQM @ X2)) @
% 40.82/6.45 (vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2) @ (vMC @ X3 @ X4))
% 40.82/6.45 | ((vreduce @ (vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2) @ X1 @
% 40.82/6.45 X2)
% 40.82/6.45 = (vsomeQConf @
% 40.82/6.45 (vQC @ (sk__340 @ X1 @ X0 @ X2) @ (sk__341 @ X1 @ X0 @ X2) @
% 40.82/6.45 (sk__342 @ X1 @ X0 @ X2)))))),
% 40.82/6.45 inference('cnf', [status(esa)], [Progress-qcond-constant-B])).
% 40.82/6.45 thf(zip_derived_cl704, plain,
% 40.82/6.45 (~ (visValue @ (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_7])).
% 40.82/6.45 thf(zip_derived_cl2428, plain,
% 40.82/6.45 (![X0 : vYN, X1 : vATMap, X2 : vATMap, X3 : vQMap, X4 : vAnsMap]:
% 40.82/6.45 (((vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2))
% 40.82/6.45 | ((vreduce @ (vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2) @ X4 @
% 40.82/6.45 X3)
% 40.82/6.45 = (vsomeQConf @
% 40.82/6.45 (vQC @ (sk__340 @ X4 @ X0 @ X3) @ (sk__341 @ X4 @ X0 @ X3) @
% 40.82/6.45 (sk__342 @ X4 @ X0 @ X3))))
% 40.82/6.45 | ~ (vptcheck @ (vMC @ (vtypeAM @ X4) @ (vtypeQM @ X3)) @
% 40.82/6.45 (vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2) @ (vMC @ X2 @ X1)))),
% 40.82/6.45 inference('dp-resolution', [status(thm)],
% 40.82/6.45 [zip_derived_cl701, zip_derived_cl704])).
% 40.82/6.45 thf(zip_derived_cl20000, plain,
% 40.82/6.45 (![X0 : vYN, X1 : vATMap, X2 : vATMap, X3 : vQMap, X4 : vAnsMap]:
% 40.82/6.45 (((vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2))
% 40.82/6.45 | ((vreduce @ (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @ X4 @ X3)
% 40.82/6.45 = (vsomeQConf @
% 40.82/6.45 (vQC @ (sk__340 @ X4 @ X0 @ X3) @ (sk__341 @ X4 @ X0 @ X3) @
% 40.82/6.45 (sk__342 @ X4 @ X0 @ X3))))
% 40.82/6.45 | ~ (vptcheck @ (vMC @ (vtypeAM @ X4) @ (vtypeQM @ X3)) @
% 40.82/6.45 (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @ (vMC @ X2 @ X1)))),
% 40.82/6.45 inference('local_rewriting', [status(thm)], [zip_derived_cl2428])).
% 40.82/6.45 thf(zip_derived_cl20002, plain,
% 40.82/6.45 (![X0 : vYN]:
% 40.82/6.45 (((vreduce @ (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @ sk__347 @
% 40.82/6.45 sk__343)
% 40.82/6.45 = (vsomeQConf @
% 40.82/6.45 (vQC @ (sk__340 @ sk__347 @ X0 @ sk__343) @
% 40.82/6.45 (sk__341 @ sk__347 @ X0 @ sk__343) @
% 40.82/6.45 (sk__342 @ sk__347 @ X0 @ sk__343))))
% 40.82/6.45 | ((vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2)))),
% 40.82/6.45 inference('sup-', [status(thm)], [zip_derived_cl703, zip_derived_cl20000])).
% 40.82/6.45 thf('dom-OptQConf', axiom,
% 40.82/6.45 (![VX:vOptQConf]:
% 40.82/6.45 ( ( ?[VQConf0:vQConf]: ( ( VX ) = ( vsomeQConf @ VQConf0 ) ) ) |
% 40.82/6.45 ( ( VX ) = ( vnoQConf ) ) ))).
% 40.82/6.45 thf(zip_derived_cl63, plain,
% 40.82/6.45 (![X0 : vOptQConf]:
% 40.82/6.45 (((X0) = (vsomeQConf @ (sk__32 @ X0))) | ((X0) = (vnoQConf)))),
% 40.82/6.45 inference('cnf', [status(esa)], [dom-OptQConf])).
% 40.82/6.45 thf('dom-QConf', axiom,
% 40.82/6.45 (![VX:vQConf]:
% 40.82/6.45 ( ?[VAnsMap0:vAnsMap,VQMap0:vQMap,VQuestionnaire0:vQuestionnaire]:
% 40.82/6.45 ( ( VX ) = ( vQC @ VAnsMap0 @ VQMap0 @ VQuestionnaire0 ) ) ))).
% 40.82/6.45 thf(zip_derived_cl103, plain,
% 40.82/6.45 (![X0 : vQConf]:
% 40.82/6.45 ((X0) = (vQC @ (sk__47 @ X0) @ (sk__48 @ X0) @ (sk__49 @ X0)))),
% 40.82/6.45 inference('cnf', [status(esa)], [dom-QConf])).
% 40.82/6.45 thf(zip_derived_cl702, plain,
% 40.82/6.45 (![X0 : vAnsMap, X1 : vQMap, X2 : vQuestionnaire]:
% 40.82/6.45 ((vreduce @ (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @ sk__347 @
% 40.82/6.45 sk__343) != (vsomeQConf @ (vQC @ X0 @ X1 @ X2)))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_7])).
% 40.82/6.45 thf(zip_derived_cl12491, plain,
% 40.82/6.45 (![X0 : vQConf]:
% 40.82/6.45 ((vreduce @ (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @ sk__347 @
% 40.82/6.45 sk__343) != (vsomeQConf @ X0))),
% 40.82/6.45 inference('sup-', [status(thm)], [zip_derived_cl103, zip_derived_cl702])).
% 40.82/6.45 thf(zip_derived_cl12492, plain,
% 40.82/6.45 (![X0 : vOptQConf]:
% 40.82/6.45 (((vreduce @ (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @ sk__347 @
% 40.82/6.45 sk__343) != (X0))
% 40.82/6.45 | ((X0) = (vnoQConf)))),
% 40.82/6.45 inference('sup-', [status(thm)], [zip_derived_cl63, zip_derived_cl12491])).
% 40.82/6.45 thf(zip_derived_cl12494, plain,
% 40.82/6.45 (((vreduce @ (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @ sk__347 @
% 40.82/6.45 sk__343) = (vnoQConf))),
% 40.82/6.45 inference('eq_res', [status(thm)], [zip_derived_cl12492])).
% 40.82/6.45 thf(zip_derived_cl20013, plain,
% 40.82/6.45 (![X0 : vYN]:
% 40.82/6.45 (((vnoQConf)
% 40.82/6.45 = (vsomeQConf @
% 40.82/6.45 (vQC @ (sk__340 @ sk__347 @ X0 @ sk__343) @
% 40.82/6.45 (sk__341 @ sk__347 @ X0 @ sk__343) @
% 40.82/6.45 (sk__342 @ sk__347 @ X0 @ sk__343))))
% 40.82/6.45 | ((vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2)))),
% 40.82/6.45 inference('demod', [status(thm)],
% 40.82/6.45 [zip_derived_cl20002, zip_derived_cl12494])).
% 40.82/6.45 thf('DIFF-noQConf-someQConf', axiom,
% 40.82/6.45 (![VQConf0:vQConf]: ( ( vnoQConf ) != ( vsomeQConf @ VQConf0 ) ))).
% 40.82/6.45 thf(zip_derived_cl65, plain,
% 40.82/6.45 (![X0 : vQConf]: ((vnoQConf) != (vsomeQConf @ X0))),
% 40.82/6.45 inference('cnf', [status(esa)], [DIFF-noQConf-someQConf])).
% 40.82/6.45 thf(zip_derived_cl20014, plain,
% 40.82/6.45 (![X0 : vYN]:
% 40.82/6.45 ((vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl20013, zip_derived_cl65])).
% 40.82/6.45 thf(zip_derived_cl20019, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 (((vqcond @ (vconstant @ X0) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2))
% 40.82/6.45 | ((vtypeOf @ X0) = (vText))
% 40.82/6.45 | ((X0) = (vNum @ (sk__56 @ X0))))),
% 40.82/6.45 inference('sup-', [status(thm)],
% 40.82/6.45 [zip_derived_cl2224, zip_derived_cl20014])).
% 40.82/6.45 thf(zip_derived_cl20525, plain,
% 40.82/6.45 ((((sk__346) = (vNum @ (sk__56 @ sk__346)))
% 40.82/6.45 | ((vtypeOf @ sk__346) = (vText)))),
% 40.82/6.45 inference('eq_res', [status(thm)], [zip_derived_cl20019])).
% 40.82/6.45 thf('echeck-1', axiom,
% 40.82/6.45 (![VwildcardName0:vATMap,Vn:vnat]:
% 40.82/6.45 ( ( vecheck @ VwildcardName0 @ ( vconstant @ ( vNum @ Vn ) ) ) =
% 40.82/6.45 ( vsomeAType @ vNumber ) ))).
% 40.82/6.45 thf(zip_derived_cl619, plain,
% 40.82/6.45 (![X0 : vATMap, X1 : vnat]:
% 40.82/6.45 ((vecheck @ X0 @ (vconstant @ (vNum @ X1))) = (vsomeAType @ vNumber))),
% 40.82/6.45 inference('cnf', [status(esa)], [echeck-1])).
% 40.82/6.45 thf(zip_derived_cl20547, plain,
% 40.82/6.45 (![X0 : vATMap]:
% 40.82/6.45 (((vecheck @ X0 @ (vconstant @ sk__346)) = (vsomeAType @ vNumber))
% 40.82/6.45 | ((vtypeOf @ sk__346) = (vText)))),
% 40.82/6.45 inference('sup+', [status(thm)], [zip_derived_cl20525, zip_derived_cl619])).
% 40.82/6.45 thf(zip_derived_cl703, plain,
% 40.82/6.45 ( (vptcheck @ (vMC @ (vtypeAM @ sk__347) @ (vtypeQM @ sk__343)) @
% 40.82/6.45 (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2) @
% 40.82/6.45 (vMC @ sk__344 @ sk__345))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_7])).
% 40.82/6.45 thf(Tqcond_inv1, axiom,
% 40.82/6.45 (![Vqm:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,Vatmr:vATMap,Vqmr:vATMap,
% 40.82/6.45 Vexp:vExp,Vq2:vQuestionnaire]:
% 40.82/6.45 ( ( vptcheck @
% 40.82/6.45 ( vMC @ Vatm @ Vqm ) @ ( vqcond @ Vexp @ Vq1 @ Vq2 ) @
% 40.82/6.45 ( vMC @ Vatmr @ Vqmr ) ) =>
% 40.82/6.45 ( ( vecheck @ Vatm @ Vexp ) = ( vsomeAType @ vYesNo ) ) ))).
% 40.82/6.45 thf(zip_derived_cl691, plain,
% 40.82/6.45 (![X0 : vATMap, X1 : vExp, X2 : vATMap, X3 : vQuestionnaire,
% 40.82/6.45 X4 : vQuestionnaire, X5 : vATMap, X6 : vATMap]:
% 40.82/6.45 (((vecheck @ X0 @ X1) = (vsomeAType @ vYesNo))
% 40.82/6.45 | ~ (vptcheck @ (vMC @ X0 @ X2) @ (vqcond @ X1 @ X3 @ X4) @
% 40.82/6.45 (vMC @ X5 @ X6)))),
% 40.82/6.45 inference('cnf', [status(esa)], [Tqcond_inv1])).
% 40.82/6.45 thf(zip_derived_cl13899, plain,
% 40.82/6.45 (((vecheck @ (vtypeAM @ sk__347) @ (vconstant @ sk__346))
% 40.82/6.45 = (vsomeAType @ vYesNo))),
% 40.82/6.45 inference('sup-', [status(thm)], [zip_derived_cl703, zip_derived_cl691])).
% 40.82/6.45 thf(zip_derived_cl20963, plain,
% 40.82/6.45 ((((vsomeAType @ vNumber) = (vsomeAType @ vYesNo))
% 40.82/6.45 | ((vtypeOf @ sk__346) = (vText)))),
% 40.82/6.45 inference('sup+', [status(thm)],
% 40.82/6.45 [zip_derived_cl20547, zip_derived_cl13899])).
% 40.82/6.45 thf(zip_derived_cl2136, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 ( (zip_tseitin_4 @ (sk__56 @ X0) @ X0)
% 40.82/6.45 | (zip_tseitin_5 @ (sk__55 @ X0) @ X0)
% 40.82/6.45 | ((X0) = (vB @ (sk__57 @ X0))))),
% 40.82/6.45 inference('dp-resolution', [status(thm)],
% 40.82/6.45 [zip_derived_cl133, zip_derived_cl128])).
% 40.82/6.45 thf(zip_derived_cl129, plain,
% 40.82/6.45 (![X0 : vAval, X1 : vnat]:
% 40.82/6.45 (((vtypeOf @ X0) = (vNumber)) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_3])).
% 40.82/6.45 thf(zip_derived_cl2168, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 (((X0) = (vB @ (sk__57 @ X0)))
% 40.82/6.45 | (zip_tseitin_5 @ (sk__55 @ X0) @ X0)
% 40.82/6.45 | ((vtypeOf @ X0) = (vNumber)))),
% 40.82/6.45 inference('dp-resolution', [status(thm)],
% 40.82/6.45 [zip_derived_cl2136, zip_derived_cl129])).
% 40.82/6.45 thf(zip_derived_cl132, plain,
% 40.82/6.45 (![X0 : vstring, X1 : vAval]:
% 40.82/6.45 (((X1) = (vT @ X0)) | ~ (zip_tseitin_5 @ X0 @ X1))),
% 40.82/6.45 inference('cnf', [status(esa)], [zf_stmt_1])).
% 40.82/6.45 thf(zip_derived_cl2223, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 (((vtypeOf @ X0) = (vNumber))
% 40.82/6.45 | ((X0) = (vB @ (sk__57 @ X0)))
% 40.82/6.45 | ((X0) = (vT @ (sk__55 @ X0))))),
% 40.82/6.45 inference('dp-resolution', [status(thm)],
% 40.82/6.45 [zip_derived_cl2168, zip_derived_cl132])).
% 40.82/6.45 thf(zip_derived_cl20014, plain,
% 40.82/6.45 (![X0 : vYN]:
% 40.82/6.45 ((vqcond @ (vconstant @ (vB @ X0)) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl20013, zip_derived_cl65])).
% 40.82/6.45 thf(zip_derived_cl20018, plain,
% 40.82/6.45 (![X0 : vAval]:
% 40.82/6.45 (((vqcond @ (vconstant @ X0) @ vq1 @ vq2)
% 40.82/6.45 != (vqcond @ (vconstant @ sk__346) @ vq1 @ vq2))
% 40.82/6.45 | ((X0) = (vT @ (sk__55 @ X0)))
% 40.82/6.45 | ((vtypeOf @ X0) = (vNumber)))),
% 40.82/6.45 inference('sup-', [status(thm)],
% 40.82/6.45 [zip_derived_cl2223, zip_derived_cl20014])).
% 40.82/6.45 thf(zip_derived_cl20492, plain,
% 40.82/6.45 ((((vtypeOf @ sk__346) = (vNumber))
% 40.82/6.45 | ((sk__346) = (vT @ (sk__55 @ sk__346))))),
% 40.82/6.45 inference('eq_res', [status(thm)], [zip_derived_cl20018])).
% 40.82/6.45 thf('echeck-2', axiom,
% 40.82/6.45 (![VwildcardName0:vATMap,Vn:vstring]:
% 40.82/6.45 ( ( vecheck @ VwildcardName0 @ ( vconstant @ ( vT @ Vn ) ) ) =
% 40.82/6.45 ( vsomeAType @ vText ) ))).
% 40.82/6.45 thf(zip_derived_cl620, plain,
% 40.82/6.45 (![X0 : vATMap, X1 : vstring]:
% 40.82/6.45 ((vecheck @ X0 @ (vconstant @ (vT @ X1))) = (vsomeAType @ vText))),
% 40.82/6.45 inference('cnf', [status(esa)], [echeck-2])).
% 40.82/6.45 thf(zip_derived_cl20499, plain,
% 40.82/6.45 (![X0 : vATMap]:
% 40.82/6.45 (((vecheck @ X0 @ (vconstant @ sk__346)) = (vsomeAType @ vText))
% 40.82/6.45 | ((vtypeOf @ sk__346) = (vNumber)))),
% 40.82/6.45 inference('sup+', [status(thm)], [zip_derived_cl20492, zip_derived_cl620])).
% 40.82/6.45 thf(zip_derived_cl13899, plain,
% 40.82/6.45 (((vecheck @ (vtypeAM @ sk__347) @ (vconstant @ sk__346))
% 40.82/6.45 = (vsomeAType @ vYesNo))),
% 40.82/6.45 inference('sup-', [status(thm)], [zip_derived_cl703, zip_derived_cl691])).
% 40.82/6.45 thf(zip_derived_cl20623, plain,
% 40.82/6.45 ((((vsomeAType @ vText) = (vsomeAType @ vYesNo))
% 40.82/6.45 | ((vtypeOf @ sk__346) = (vNumber)))),
% 40.82/6.45 inference('sup+', [status(thm)],
% 40.82/6.45 [zip_derived_cl20499, zip_derived_cl13899])).
% 40.82/6.45 thf(zip_derived_cl20965, plain,
% 40.82/6.45 ((((vText) = (vNumber))
% 40.82/6.45 | ((vsomeAType @ vNumber) = (vsomeAType @ vYesNo))
% 40.82/6.45 | ((vsomeAType @ vText) = (vsomeAType @ vYesNo)))),
% 40.82/6.45 inference('sup+', [status(thm)],
% 40.82/6.45 [zip_derived_cl20963, zip_derived_cl20623])).
% 40.82/6.45 thf('DIFF-Number-Text', axiom, (( vNumber ) != ( vText ))).
% 40.82/6.45 thf(zip_derived_cl28, plain, (((vNumber) != (vText))),
% 40.82/6.45 inference('cnf', [status(esa)], [DIFF-Number-Text])).
% 40.82/6.45 thf(zip_derived_cl20966, plain,
% 40.82/6.45 ((((vsomeAType @ vNumber) = (vsomeAType @ vYesNo))
% 40.82/6.45 | ((vsomeAType @ vText) = (vsomeAType @ vYesNo)))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl20965, zip_derived_cl28])).
% 40.82/6.45 thf('dom-OptAType', axiom,
% 40.82/6.45 (![VX:vOptAType]:
% 40.82/6.45 ( ( ?[VAType0:vAType]: ( ( VX ) = ( vsomeAType @ VAType0 ) ) ) |
% 40.82/6.45 ( ( VX ) = ( vnoAType ) ) ))).
% 40.82/6.45 thf(zip_derived_cl66, plain,
% 40.82/6.45 (![X0 : vOptAType]:
% 40.82/6.45 (((X0) = (vsomeAType @ (sk__33 @ X0))) | ((X0) = (vnoAType)))),
% 40.82/6.45 inference('cnf', [status(esa)], [dom-OptAType])).
% 40.82/6.45 thf('EQ-someAType', axiom,
% 40.82/6.45 (![VAType0:vAType,VAType1:vAType]:
% 40.82/6.45 ( ( ( vsomeAType @ VAType0 ) = ( vsomeAType @ VAType1 ) ) =>
% 40.82/6.45 ( ( VAType0 ) = ( VAType1 ) ) ))).
% 40.82/6.45 thf(zip_derived_cl67, plain,
% 40.82/6.45 (![X0 : vAType, X1 : vAType]:
% 40.82/6.45 (((X1) = (X0)) | ((vsomeAType @ X1) != (vsomeAType @ X0)))),
% 40.82/6.45 inference('cnf', [status(esa)], [EQ-someAType])).
% 40.82/6.45 thf(zip_derived_cl12104, plain,
% 40.82/6.45 (![X0 : vOptAType, X1 : vAType]:
% 40.82/6.45 (((vsomeAType @ X1) != (X0))
% 40.82/6.45 | ((X0) = (vnoAType))
% 40.82/6.45 | ((X1) = (sk__33 @ X0)))),
% 40.82/6.45 inference('sup-', [status(thm)], [zip_derived_cl66, zip_derived_cl67])).
% 40.82/6.45 thf(zip_derived_cl12111, plain,
% 40.82/6.45 (![X0 : vAType]:
% 40.82/6.45 (((X0) = (sk__33 @ (vsomeAType @ X0)))
% 40.82/6.45 | ((vsomeAType @ X0) = (vnoAType)))),
% 40.82/6.45 inference('eq_res', [status(thm)], [zip_derived_cl12104])).
% 40.82/6.45 thf('DIFF-noAType-someAType', axiom,
% 40.82/6.45 (![VAType0:vAType]: ( ( vnoAType ) != ( vsomeAType @ VAType0 ) ))).
% 40.82/6.45 thf(zip_derived_cl68, plain,
% 40.82/6.45 (![X0 : vAType]: ((vnoAType) != (vsomeAType @ X0))),
% 40.82/6.45 inference('cnf', [status(esa)], [DIFF-noAType-someAType])).
% 40.82/6.45 thf(zip_derived_cl12112, plain,
% 40.82/6.45 (![X0 : vAType]: ((X0) = (sk__33 @ (vsomeAType @ X0)))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl12111, zip_derived_cl68])).
% 40.82/6.45 thf(zip_derived_cl20983, plain,
% 40.82/6.45 ((((vText) = (sk__33 @ (vsomeAType @ vYesNo)))
% 40.82/6.45 | ((vsomeAType @ vNumber) = (vsomeAType @ vYesNo)))),
% 40.82/6.45 inference('sup+', [status(thm)],
% 40.82/6.45 [zip_derived_cl20966, zip_derived_cl12112])).
% 40.82/6.45 thf(zip_derived_cl12112, plain,
% 40.82/6.45 (![X0 : vAType]: ((X0) = (sk__33 @ (vsomeAType @ X0)))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl12111, zip_derived_cl68])).
% 40.82/6.45 thf(zip_derived_cl20994, plain,
% 40.82/6.45 ((((vText) = (vYesNo)) | ((vsomeAType @ vNumber) = (vsomeAType @ vYesNo)))),
% 40.82/6.45 inference('demod', [status(thm)],
% 40.82/6.45 [zip_derived_cl20983, zip_derived_cl12112])).
% 40.82/6.45 thf('DIFF-YesNo-Text', axiom, (( vYesNo ) != ( vText ))).
% 40.82/6.45 thf(zip_derived_cl27, plain, (((vYesNo) != (vText))),
% 40.82/6.45 inference('cnf', [status(esa)], [DIFF-YesNo-Text])).
% 40.82/6.45 thf(zip_derived_cl20995, plain,
% 40.82/6.45 (((vsomeAType @ vNumber) = (vsomeAType @ vYesNo))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl20994, zip_derived_cl27])).
% 40.82/6.45 thf(zip_derived_cl12112, plain,
% 40.82/6.45 (![X0 : vAType]: ((X0) = (sk__33 @ (vsomeAType @ X0)))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl12111, zip_derived_cl68])).
% 40.82/6.45 thf(zip_derived_cl21033, plain,
% 40.82/6.45 (((vYesNo) = (sk__33 @ (vsomeAType @ vNumber)))),
% 40.82/6.45 inference('sup+', [status(thm)],
% 40.82/6.45 [zip_derived_cl20995, zip_derived_cl12112])).
% 40.82/6.45 thf(zip_derived_cl12112, plain,
% 40.82/6.45 (![X0 : vAType]: ((X0) = (sk__33 @ (vsomeAType @ X0)))),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl12111, zip_derived_cl68])).
% 40.82/6.45 thf(zip_derived_cl21041, plain, (((vYesNo) = (vNumber))),
% 40.82/6.45 inference('demod', [status(thm)],
% 40.82/6.45 [zip_derived_cl21033, zip_derived_cl12112])).
% 40.82/6.45 thf('DIFF-YesNo-Number', axiom, (( vYesNo ) != ( vNumber ))).
% 40.82/6.45 thf(zip_derived_cl26, plain, (((vYesNo) != (vNumber))),
% 40.82/6.45 inference('cnf', [status(esa)], [DIFF-YesNo-Number])).
% 40.82/6.45 thf(zip_derived_cl21042, plain, ($false),
% 40.82/6.45 inference('simplify_reflect-', [status(thm)],
% 40.82/6.45 [zip_derived_cl21041, zip_derived_cl26])).
% 40.82/6.45
% 40.82/6.45 % SZS output end Refutation
% 40.82/6.45
% 40.82/6.45
% 40.82/6.45 % Terminating...
% 41.50/6.55 % Runner terminated.
% 41.50/6.55 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------