%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM254_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.tNdj974xBf 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:22 PM UTC 2026
% Result : Theorem 0.55s 0.98s
% Output : Refutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : COM254_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.tNdj974xBf true
% 0.17/0.35 % Computer : n008.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Mon May 4 19:47:13 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 % Running portfolio for 300 s
% 0.17/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.35 % Number of cores: 8
% 0.21/0.36 % Python version: Python 3.6.8
% 0.21/0.36 % Running in FO mode
% 0.52/0.64 % Total configuration time : 435
% 0.52/0.64 % Estimated wc time : 1092
% 0.52/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.53/0.70 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.53/0.71 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.53/0.71 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.53/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.53/0.75 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.53/0.75 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.53/0.75 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.55/0.98 % Solved by fo/fo4.sh.
% 0.55/0.98 % done 242 iterations in 0.207s
% 0.55/0.98 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.55/0.98 % SZS output start Refutation
% 0.55/0.98 thf(vMapConf_type, type, vMapConf: $tType).
% 0.55/0.98 thf(vATMap_type, type, vATMap: $tType).
% 0.55/0.98 thf(vAnsMap_type, type, vAnsMap: $tType).
% 0.55/0.98 thf(vQMap_type, type, vQMap: $tType).
% 0.55/0.98 thf(vQuestionnaire_type, type, vQuestionnaire: $tType).
% 0.55/0.98 thf(vExp_type, type, vExp: $tType).
% 0.55/0.98 thf(vAval_type, type, vAval: $tType).
% 0.55/0.98 thf(vYN_type, type, vYN: $tType).
% 0.55/0.98 thf(vOptQConf_type, type, vOptQConf: $tType).
% 0.55/0.98 thf(vQConf_type, type, vQConf: $tType).
% 0.55/0.98 thf(vsomeQConf_type, type, vsomeQConf: vQConf > vOptQConf).
% 0.55/0.98 thf(vB_type, type, vB: vYN > vAval).
% 0.55/0.98 thf(vqcond_type, type, vqcond: vExp > vQuestionnaire > vQuestionnaire > vQuestionnaire).
% 0.55/0.98 thf('#_fresh_sk11_type', type, '#_fresh_sk11': vQConf > vQuestionnaire).
% 0.55/0.98 thf(sk__12_type, type, sk__12: vATMap > vQuestionnaire > vATMap > vATMap).
% 0.55/0.98 thf(sk__type, type, sk_: vMapConf > vATMap).
% 0.55/0.98 thf(sk__14_type, type, sk__14: vQuestionnaire > vATMap > vATMap > vATMap).
% 0.55/0.98 thf(vq1_type, type, vq1: vQuestionnaire).
% 0.55/0.98 thf(sk__21_type, type, sk__21: vAnsMap).
% 0.55/0.98 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 0.55/0.98 thf(sk__1_type, type, sk__1: vMapConf > vATMap).
% 0.55/0.98 thf(sk__15_type, type, sk__15: vQuestionnaire > vATMap > vATMap > vATMap).
% 0.55/0.98 thf(vtypeQM_type, type, vtypeQM: vQMap > vATMap).
% 0.55/0.98 thf(vptcheck_type, type, vptcheck: vMapConf > vQuestionnaire > vMapConf > $o).
% 0.55/0.98 thf(sk__18_type, type, sk__18: vQMap).
% 0.55/0.98 thf('#_fresh_sk2_type', type, '#_fresh_sk2': vOptQConf > vQConf).
% 0.55/0.98 thf(vMC_type, type, vMC: vATMap > vATMap > vMapConf).
% 0.55/0.98 thf('#_fresh_sk9_type', type, '#_fresh_sk9': vQConf > vAnsMap).
% 0.55/0.98 thf(sk__13_type, type, sk__13: vATMap > vQuestionnaire > vATMap > vATMap).
% 0.55/0.98 thf(sk__16_type, type, sk__16: vATMap).
% 0.55/0.98 thf('#_fresh_sk3_type', type, '#_fresh_sk3': vMapConf > vATMap).
% 0.55/0.98 thf(vconstant_type, type, vconstant: vAval > vExp).
% 0.55/0.98 thf(vreduce_type, type, vreduce: vQuestionnaire > vAnsMap > vQMap > vOptQConf).
% 0.55/0.98 thf(vq2_type, type, vq2: vQuestionnaire).
% 0.55/0.98 thf(vQC_type, type, vQC: vAnsMap > vQMap > vQuestionnaire > vQConf).
% 0.55/0.98 thf(sk__22_type, type, sk__22: vQMap).
% 0.55/0.98 thf(sk__17_type, type, sk__17: vQuestionnaire).
% 0.55/0.98 thf(sk__20_type, type, sk__20: vATMap).
% 0.55/0.98 thf(vno_type, type, vno: vYN).
% 0.55/0.98 thf('#_fresh_sk10_type', type, '#_fresh_sk10': vQConf > vQMap).
% 0.55/0.98 thf(sk__19_type, type, sk__19: vAnsMap).
% 0.55/0.98 thf('#_fresh_sk4_type', type, '#_fresh_sk4': vMapConf > vATMap).
% 0.55/0.98 thf('Preservation-qcond-constant-B-no', conjecture,
% 0.55/0.98 (![Vqtm1:vATMap,Vqr:vQuestionnaire,Vqm:vQMap,Vamr:vAnsMap,Vatm1:vATMap,
% 0.55/0.98 Vam:vAnsMap,Vqmr:vQMap]:
% 0.55/0.98 ( ( ( vptcheck @
% 0.55/0.98 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 0.55/0.98 ( vqcond @ ( vconstant @ ( vB @ vno ) ) @ vq1 @ vq2 ) @
% 0.55/0.98 ( vMC @ Vatm1 @ Vqtm1 ) ) &
% 0.55/0.98 ( ( vreduce @
% 0.55/0.98 ( vqcond @ ( vconstant @ ( vB @ vno ) ) @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 0.55/0.98 ( vsomeQConf @ ( vQC @ Vamr @ Vqmr @ Vqr ) ) ) ) =>
% 0.55/0.98 ( vptcheck @
% 0.55/0.98 ( vMC @ ( vtypeAM @ Vamr ) @ ( vtypeQM @ Vqmr ) ) @ Vqr @
% 0.55/0.98 ( vMC @ Vatm1 @ Vqtm1 ) ) ))).
% 0.55/0.98 thf(zf_stmt_0, negated_conjecture,
% 0.55/0.98 (~( ![Vqtm1:vATMap,Vqr:vQuestionnaire,Vqm:vQMap,Vamr:vAnsMap,Vatm1:vATMap,
% 0.55/0.98 Vam:vAnsMap,Vqmr:vQMap]:
% 0.55/0.98 ( ( ( vptcheck @
% 0.55/0.98 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 0.55/0.98 ( vqcond @ ( vconstant @ ( vB @ vno ) ) @ vq1 @ vq2 ) @
% 0.55/0.98 ( vMC @ Vatm1 @ Vqtm1 ) ) &
% 0.55/0.98 ( ( vreduce @
% 0.55/0.98 ( vqcond @ ( vconstant @ ( vB @ vno ) ) @ vq1 @ vq2 ) @ Vam @
% 0.55/0.98 Vqm ) =
% 0.55/0.98 ( vsomeQConf @ ( vQC @ Vamr @ Vqmr @ Vqr ) ) ) ) =>
% 0.55/0.98 ( vptcheck @
% 0.55/0.98 ( vMC @ ( vtypeAM @ Vamr ) @ ( vtypeQM @ Vqmr ) ) @ Vqr @
% 0.55/0.98 ( vMC @ Vatm1 @ Vqtm1 ) ) ) )),
% 0.55/0.98 inference('cnf.neg', [status(esa)], [Preservation-qcond-constant-B-no])).
% 0.55/0.98 thf(zip_derived_cl49, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @
% 0.55/0.98 (vMC @ sk__20 @ sk__16))),
% 0.55/0.98 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.55/0.98 thf(zip_derived_cl48, plain,
% 0.55/0.98 (((vreduce @ (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @ sk__21 @
% 0.55/0.98 sk__18) = (vsomeQConf @ (vQC @ sk__19 @ sk__22 @ sk__17)))),
% 0.55/0.98 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.55/0.98 thf('reduce-12', axiom,
% 0.55/0.98 (![Vqs1:vQuestionnaire,Vqs2:vQuestionnaire,Vam:vAnsMap,Vqm:vQMap]:
% 0.55/0.98 ( ( vreduce @
% 0.55/0.98 ( vqcond @ ( vconstant @ ( vB @ vno ) ) @ Vqs1 @ Vqs2 ) @ Vam @ Vqm ) =
% 0.55/0.98 ( vsomeQConf @ ( vQC @ Vam @ Vqm @ Vqs2 ) ) ))).
% 0.55/0.98 thf(zip_derived_cl22, plain,
% 0.55/0.98 (![X0 : vAnsMap, X1 : vQMap, X2 : vQuestionnaire, X3 : vQuestionnaire]:
% 0.55/0.98 ((vreduce @ (vqcond @ (vconstant @ (vB @ vno)) @ X3 @ X2) @ X0 @ X1)
% 0.55/0.98 = (vsomeQConf @ (vQC @ X0 @ X1 @ X2)))),
% 0.55/0.98 inference('cnf', [status(esa)], [reduce-12])).
% 0.55/0.98 thf(zip_derived_cl648, plain,
% 0.55/0.98 (((vsomeQConf @ (vQC @ sk__21 @ sk__18 @ vq2))
% 0.55/0.98 = (vsomeQConf @ (vQC @ sk__19 @ sk__22 @ sk__17)))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl48, zip_derived_cl22])).
% 0.55/0.98 thf('EQ-someQConf', axiom,
% 0.55/0.98 (![VQConf0:vQConf,VQConf1:vQConf]:
% 0.55/0.98 ( ( ( vsomeQConf @ VQConf0 ) = ( vsomeQConf @ VQConf1 ) ) =>
% 0.55/0.98 ( ( VQConf0 ) = ( VQConf1 ) ) ))).
% 0.55/0.98 thf(zip_derived_cl12, plain,
% 0.55/0.98 (![X0 : vQConf, X1 : vQConf]:
% 0.55/0.98 (((X1) = (X0)) | ((vsomeQConf @ X1) != (vsomeQConf @ X0)))),
% 0.55/0.98 inference('cnf', [status(esa)], [EQ-someQConf])).
% 0.55/0.98 thf(zip_derived_cl57, plain,
% 0.55/0.98 (![X1 : vQConf]: (('#_fresh_sk2' @ (vsomeQConf @ X1)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl12])).
% 0.55/0.98 thf(zip_derived_cl666, plain,
% 0.55/0.98 ((('#_fresh_sk2' @ (vsomeQConf @ (vQC @ sk__21 @ sk__18 @ vq2)))
% 0.55/0.98 = (vQC @ sk__19 @ sk__22 @ sk__17))),
% 0.55/0.98 inference('sup+', [status(thm)], [zip_derived_cl648, zip_derived_cl57])).
% 0.55/0.98 thf(zip_derived_cl57, plain,
% 0.55/0.98 (![X1 : vQConf]: (('#_fresh_sk2' @ (vsomeQConf @ X1)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl12])).
% 0.55/0.98 thf(zip_derived_cl671, plain,
% 0.55/0.98 (((vQC @ sk__21 @ sk__18 @ vq2) = (vQC @ sk__19 @ sk__22 @ sk__17))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl666, zip_derived_cl57])).
% 0.55/0.98 thf(zip_derived_cl671, plain,
% 0.55/0.98 (((vQC @ sk__21 @ sk__18 @ vq2) = (vQC @ sk__19 @ sk__22 @ sk__17))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl666, zip_derived_cl57])).
% 0.55/0.98 thf('EQ-QC', axiom,
% 0.55/0.98 (![VQMap0:vQMap,VAnsMap1:vAnsMap,VQuestionnaire1:vQuestionnaire,
% 0.55/0.98 VAnsMap0:vAnsMap,VQuestionnaire0:vQuestionnaire,VQMap1:vQMap]:
% 0.55/0.98 ( ( ( vQC @ VAnsMap0 @ VQMap0 @ VQuestionnaire0 ) =
% 0.55/0.98 ( vQC @ VAnsMap1 @ VQMap1 @ VQuestionnaire1 ) ) =>
% 0.55/0.98 ( ( ( VAnsMap0 ) = ( VAnsMap1 ) ) & ( ( VQMap0 ) = ( VQMap1 ) ) &
% 0.55/0.98 ( ( VQuestionnaire0 ) = ( VQuestionnaire1 ) ) ) ))).
% 0.55/0.98 thf(zip_derived_cl18, plain,
% 0.55/0.98 (![X0 : vQuestionnaire, X1 : vQuestionnaire, X2 : vAnsMap, X3 : vQMap,
% 0.55/0.98 X4 : vAnsMap, X5 : vQMap]:
% 0.55/0.98 (((X1) = (X0)) | ((vQC @ X4 @ X5 @ X1) != (vQC @ X2 @ X3 @ X0)))),
% 0.55/0.98 inference('cnf', [status(esa)], [EQ-QC])).
% 0.55/0.98 thf(zip_derived_cl272, plain,
% 0.55/0.98 (![X1 : vQuestionnaire, X4 : vAnsMap, X5 : vQMap]:
% 0.55/0.98 (('#_fresh_sk11' @ (vQC @ X4 @ X5 @ X1)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl18])).
% 0.55/0.98 thf(zip_derived_cl680, plain,
% 0.55/0.98 ((('#_fresh_sk11' @ (vQC @ sk__21 @ sk__18 @ vq2)) = (sk__17))),
% 0.55/0.98 inference('sup+', [status(thm)], [zip_derived_cl671, zip_derived_cl272])).
% 0.55/0.98 thf(zip_derived_cl272, plain,
% 0.55/0.98 (![X1 : vQuestionnaire, X4 : vAnsMap, X5 : vQMap]:
% 0.55/0.98 (('#_fresh_sk11' @ (vQC @ X4 @ X5 @ X1)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl18])).
% 0.55/0.98 thf(zip_derived_cl687, plain, (((vq2) = (sk__17))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl680, zip_derived_cl272])).
% 0.55/0.98 thf(zip_derived_cl690, plain,
% 0.55/0.98 (((vQC @ sk__21 @ sk__18 @ vq2) = (vQC @ sk__19 @ sk__22 @ vq2))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl671, zip_derived_cl687])).
% 0.55/0.98 thf(zip_derived_cl671, plain,
% 0.55/0.98 (((vQC @ sk__21 @ sk__18 @ vq2) = (vQC @ sk__19 @ sk__22 @ sk__17))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl666, zip_derived_cl57])).
% 0.55/0.98 thf(zip_derived_cl16, plain,
% 0.55/0.98 (![X0 : vAnsMap, X1 : vAnsMap, X2 : vQMap, X3 : vQuestionnaire,
% 0.55/0.98 X4 : vQMap, X5 : vQuestionnaire]:
% 0.55/0.98 (((X1) = (X0)) | ((vQC @ X1 @ X4 @ X5) != (vQC @ X0 @ X2 @ X3)))),
% 0.55/0.98 inference('cnf', [status(esa)], [EQ-QC])).
% 0.55/0.98 thf(zip_derived_cl260, plain,
% 0.55/0.98 (![X1 : vAnsMap, X4 : vQMap, X5 : vQuestionnaire]:
% 0.55/0.98 (('#_fresh_sk9' @ (vQC @ X1 @ X4 @ X5)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl16])).
% 0.55/0.98 thf(zip_derived_cl674, plain,
% 0.55/0.98 ((('#_fresh_sk9' @ (vQC @ sk__21 @ sk__18 @ vq2)) = (sk__19))),
% 0.55/0.98 inference('sup+', [status(thm)], [zip_derived_cl671, zip_derived_cl260])).
% 0.55/0.98 thf(zip_derived_cl260, plain,
% 0.55/0.98 (![X1 : vAnsMap, X4 : vQMap, X5 : vQuestionnaire]:
% 0.55/0.98 (('#_fresh_sk9' @ (vQC @ X1 @ X4 @ X5)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl16])).
% 0.55/0.98 thf(zip_derived_cl686, plain, (((sk__21) = (sk__19))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl674, zip_derived_cl260])).
% 0.55/0.98 thf(zip_derived_cl692, plain,
% 0.55/0.98 (((vQC @ sk__21 @ sk__18 @ vq2) = (vQC @ sk__21 @ sk__22 @ vq2))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl690, zip_derived_cl686])).
% 0.55/0.98 thf(zip_derived_cl17, plain,
% 0.55/0.98 (![X0 : vQMap, X1 : vQMap, X2 : vAnsMap, X3 : vQuestionnaire,
% 0.55/0.98 X4 : vAnsMap, X5 : vQuestionnaire]:
% 0.55/0.98 (((X1) = (X0)) | ((vQC @ X4 @ X1 @ X5) != (vQC @ X2 @ X0 @ X3)))),
% 0.55/0.98 inference('cnf', [status(esa)], [EQ-QC])).
% 0.55/0.98 thf(zip_derived_cl266, plain,
% 0.55/0.98 (![X1 : vQMap, X4 : vAnsMap, X5 : vQuestionnaire]:
% 0.55/0.98 (('#_fresh_sk10' @ (vQC @ X4 @ X1 @ X5)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl17])).
% 0.55/0.98 thf(zip_derived_cl698, plain,
% 0.55/0.98 ((('#_fresh_sk10' @ (vQC @ sk__21 @ sk__22 @ vq2)) = (sk__18))),
% 0.55/0.98 inference('sup+', [status(thm)], [zip_derived_cl692, zip_derived_cl266])).
% 0.55/0.98 thf(zip_derived_cl266, plain,
% 0.55/0.98 (![X1 : vQMap, X4 : vAnsMap, X5 : vQuestionnaire]:
% 0.55/0.98 (('#_fresh_sk10' @ (vQC @ X4 @ X1 @ X5)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl17])).
% 0.55/0.98 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.98 thf(zip_derived_cl715, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @
% 0.55/0.98 (vMC @ sk__20 @ sk__16))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl49, zip_derived_cl707])).
% 0.55/0.98 thf(Tqcond_inv3, axiom,
% 0.55/0.98 (![Vqm:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,Vatmr:vATMap,Vqmr:vATMap,
% 0.55/0.98 Vexp:vExp,Vq2:vQuestionnaire]:
% 0.55/0.98 ( ( vptcheck @
% 0.55/0.98 ( vMC @ Vatm @ Vqm ) @ ( vqcond @ Vexp @ Vq1 @ Vq2 ) @
% 0.55/0.98 ( vMC @ Vatmr @ Vqmr ) ) =>
% 0.55/0.98 ( ?[Vatm1:vATMap,Vqm1:vATMap]:
% 0.55/0.98 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq2 @ ( vMC @ Vatm1 @ Vqm1 ) ) ) ))).
% 0.55/0.98 thf(zip_derived_cl40, plain,
% 0.55/0.98 (![X0 : vATMap, X1 : vATMap, X2 : vQuestionnaire, X3 : vExp,
% 0.55/0.98 X4 : vQuestionnaire, X5 : vATMap, X6 : vATMap]:
% 0.55/0.98 ( (vptcheck @ (vMC @ X0 @ X1) @ X2 @
% 0.55/0.98 (vMC @ (sk__14 @ X2 @ X0 @ X1) @ (sk__15 @ X2 @ X0 @ X1)))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ X0 @ X1) @ (vqcond @ X3 @ X4 @ X2) @
% 0.55/0.98 (vMC @ X5 @ X6)))),
% 0.55/0.98 inference('cnf', [status(esa)], [Tqcond_inv3])).
% 0.55/0.98 thf(zip_derived_cl949, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.98 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 0.55/0.98 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl40])).
% 0.55/0.98 thf('dom-MapConf', axiom,
% 0.55/0.98 (![VX:vMapConf]:
% 0.55/0.98 ( ?[VATMap0:vATMap,VATMap1:vATMap]:
% 0.55/0.98 ( ( VX ) = ( vMC @ VATMap0 @ VATMap1 ) ) ))).
% 0.55/0.98 thf(zip_derived_cl2, plain,
% 0.55/0.98 (![X0 : vMapConf]: ((X0) = (vMC @ (sk_ @ X0) @ (sk__1 @ X0)))),
% 0.55/0.98 inference('cnf', [status(esa)], [dom-MapConf])).
% 0.55/0.98 thf(zip_derived_cl2, plain,
% 0.55/0.98 (![X0 : vMapConf]: ((X0) = (vMC @ (sk_ @ X0) @ (sk__1 @ X0)))),
% 0.55/0.98 inference('cnf', [status(esa)], [dom-MapConf])).
% 0.55/0.98 thf('EQ-MC', axiom,
% 0.55/0.98 (![VATMap0:vATMap,VATMap1:vATMap,VATMap2:vATMap,VATMap3:vATMap]:
% 0.55/0.98 ( ( ( vMC @ VATMap0 @ VATMap1 ) = ( vMC @ VATMap2 @ VATMap3 ) ) =>
% 0.55/0.98 ( ( ( VATMap0 ) = ( VATMap2 ) ) & ( ( VATMap1 ) = ( VATMap3 ) ) ) ))).
% 0.55/0.98 thf(zip_derived_cl3, plain,
% 0.55/0.98 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 0.55/0.98 (((X1) = (X0)) | ((vMC @ X1 @ X3) != (vMC @ X0 @ X2)))),
% 0.55/0.98 inference('cnf', [status(esa)], [EQ-MC])).
% 0.55/0.98 thf(zip_derived_cl198, plain,
% 0.55/0.98 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk3' @ (vMC @ X1 @ X3)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl3])).
% 0.55/0.98 thf(zip_derived_cl246, plain,
% 0.55/0.98 (![X0 : vMapConf]: (('#_fresh_sk3' @ X0) = (sk_ @ X0))),
% 0.55/0.98 inference('sup+', [status(thm)], [zip_derived_cl2, zip_derived_cl198])).
% 0.55/0.98 thf(zip_derived_cl247, plain,
% 0.55/0.98 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ (sk__1 @ X0)))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl2, zip_derived_cl246])).
% 0.55/0.98 thf(zip_derived_cl49, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @
% 0.55/0.98 (vMC @ sk__20 @ sk__16))),
% 0.55/0.98 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.55/0.98 thf(Tqcond_inv6, axiom,
% 0.55/0.98 (![Vqm:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,Vqm1:vATMap,Vatmr:vATMap,
% 0.55/0.98 Vatm1:vATMap,Vqmr:vATMap,Vexp:vExp,Vq2:vQuestionnaire]:
% 0.55/0.98 ( ( ( vptcheck @
% 0.55/0.98 ( vMC @ Vatm @ Vqm ) @ ( vqcond @ Vexp @ Vq1 @ Vq2 ) @
% 0.55/0.98 ( vMC @ Vatmr @ Vqmr ) ) &
% 0.55/0.98 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) &
% 0.55/0.98 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq2 @ ( vMC @ Vatm1 @ Vqm1 ) ) ) =>
% 0.55/0.98 ( ( Vatmr ) = ( Vatm1 ) ) ))).
% 0.55/0.98 thf(zip_derived_cl43, plain,
% 0.55/0.98 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap,
% 0.55/0.98 X4 : vQuestionnaire, X5 : vATMap, X6 : vExp, X7 : vQuestionnaire,
% 0.55/0.98 X8 : vATMap]:
% 0.55/0.98 (((X1) = (X0))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X4 @ (vMC @ X0 @ X5))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ X2 @ X3) @ (vqcond @ X6 @ X4 @ X7) @
% 0.55/0.98 (vMC @ X1 @ X8))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X7 @ (vMC @ X0 @ X5)))),
% 0.55/0.98 inference('cnf', [status(esa)], [Tqcond_inv6])).
% 0.55/0.98 thf(zip_derived_cl458, plain,
% 0.55/0.98 (![X0 : vATMap, X1 : vATMap]:
% 0.55/0.98 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 vq2 @ (vMC @ X1 @ X0))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 vq1 @ (vMC @ X1 @ X0))
% 0.55/0.98 | ((sk__20) = (X1)))),
% 0.55/0.98 inference('sup-', [status(thm)], [zip_derived_cl49, zip_derived_cl43])).
% 0.55/0.98 thf(zip_derived_cl501, plain,
% 0.55/0.98 (![X0 : vMapConf]:
% 0.55/0.98 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 vq2 @ X0)
% 0.55/0.98 | ((sk__20) = ('#_fresh_sk3' @ X0))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 vq1 @ (vMC @ ('#_fresh_sk3' @ X0) @ (sk__1 @ X0))))),
% 0.55/0.98 inference('sup-', [status(thm)], [zip_derived_cl247, zip_derived_cl458])).
% 0.55/0.98 thf(zip_derived_cl247, plain,
% 0.55/0.98 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ (sk__1 @ X0)))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl2, zip_derived_cl246])).
% 0.55/0.98 thf(zip_derived_cl510, plain,
% 0.55/0.98 (![X0 : vMapConf]:
% 0.55/0.98 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 vq2 @ X0)
% 0.55/0.98 | ((sk__20) = ('#_fresh_sk3' @ X0))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.98 vq1 @ X0))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl501, zip_derived_cl247])).
% 0.55/0.98 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.98 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.98 thf(zip_derived_cl720, plain,
% 0.55/0.98 (![X0 : vMapConf]:
% 0.55/0.98 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 vq2 @ X0)
% 0.55/0.98 | ((sk__20) = ('#_fresh_sk3' @ X0))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 vq1 @ X0))),
% 0.55/0.98 inference('demod', [status(thm)],
% 0.55/0.98 [zip_derived_cl510, zip_derived_cl707, zip_derived_cl707])).
% 0.55/0.98 thf(zip_derived_cl715, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @
% 0.55/0.98 (vMC @ sk__20 @ sk__16))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl49, zip_derived_cl707])).
% 0.55/0.98 thf(Tqcond_inv2, axiom,
% 0.55/0.98 (![Vqm:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,Vatmr:vATMap,Vqmr:vATMap,
% 0.55/0.98 Vexp:vExp,Vq2:vQuestionnaire]:
% 0.55/0.98 ( ( vptcheck @
% 0.55/0.98 ( vMC @ Vatm @ Vqm ) @ ( vqcond @ Vexp @ Vq1 @ Vq2 ) @
% 0.55/0.98 ( vMC @ Vatmr @ Vqmr ) ) =>
% 0.55/0.98 ( ?[Vatm1:vATMap,Vqm1:vATMap]:
% 0.55/0.98 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) ) ))).
% 0.55/0.98 thf(zip_derived_cl39, plain,
% 0.55/0.98 (![X0 : vATMap, X1 : vATMap, X2 : vQuestionnaire, X3 : vExp,
% 0.55/0.98 X4 : vQuestionnaire, X5 : vATMap, X6 : vATMap]:
% 0.55/0.98 ( (vptcheck @ (vMC @ X0 @ X1) @ X2 @
% 0.55/0.98 (vMC @ (sk__12 @ X0 @ X2 @ X1) @ (sk__13 @ X0 @ X2 @ X1)))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ X0 @ X1) @ (vqcond @ X3 @ X2 @ X4) @
% 0.55/0.98 (vMC @ X5 @ X6)))),
% 0.55/0.98 inference('cnf', [status(esa)], [Tqcond_inv2])).
% 0.55/0.98 thf(zip_derived_cl948, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq1 @
% 0.55/0.98 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))))),
% 0.55/0.98 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl39])).
% 0.55/0.98 thf(zip_derived_cl979, plain,
% 0.55/0.98 ((((sk__20)
% 0.55/0.98 = ('#_fresh_sk3' @
% 0.55/0.98 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 vq2 @
% 0.55/0.98 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))),
% 0.55/0.98 inference('sup+', [status(thm)], [zip_derived_cl720, zip_derived_cl948])).
% 0.55/0.98 thf(zip_derived_cl198, plain,
% 0.55/0.98 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk3' @ (vMC @ X1 @ X3)) = (X1))),
% 0.55/0.98 inference('inj_rec', [status(thm)], [zip_derived_cl3])).
% 0.55/0.98 thf(zip_derived_cl981, plain,
% 0.55/0.98 ((((sk__20) = (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))
% 0.55/0.98 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 vq2 @
% 0.55/0.98 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl979, zip_derived_cl198])).
% 0.55/0.98 thf(zip_derived_cl949, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.98 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 0.55/0.98 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl40])).
% 0.55/0.98 thf(zip_derived_cl948, plain,
% 0.55/0.98 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq1 @
% 0.55/0.98 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.98 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))))),
% 0.55/0.98 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl39])).
% 0.55/0.98 thf(zip_derived_cl247, plain,
% 0.55/0.98 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ (sk__1 @ X0)))),
% 0.55/0.98 inference('demod', [status(thm)], [zip_derived_cl2, zip_derived_cl246])).
% 0.55/0.99 thf(zip_derived_cl247, plain,
% 0.55/0.99 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ (sk__1 @ X0)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl2, zip_derived_cl246])).
% 0.55/0.99 thf(zip_derived_cl4, plain,
% 0.55/0.99 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 0.55/0.99 (((X1) = (X0)) | ((vMC @ X3 @ X1) != (vMC @ X2 @ X0)))),
% 0.55/0.99 inference('cnf', [status(esa)], [EQ-MC])).
% 0.55/0.99 thf(zip_derived_cl200, plain,
% 0.55/0.99 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk4' @ (vMC @ X3 @ X1)) = (X1))),
% 0.55/0.99 inference('inj_rec', [status(thm)], [zip_derived_cl4])).
% 0.55/0.99 thf(zip_derived_cl485, plain,
% 0.55/0.99 (![X0 : vMapConf]: (('#_fresh_sk4' @ X0) = (sk__1 @ X0))),
% 0.55/0.99 inference('sup+', [status(thm)], [zip_derived_cl247, zip_derived_cl200])).
% 0.55/0.99 thf(zip_derived_cl511, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ ('#_fresh_sk4' @ X0)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl247, zip_derived_cl485])).
% 0.55/0.99 thf(zip_derived_cl49, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @
% 0.55/0.99 (vMC @ sk__20 @ sk__16))),
% 0.55/0.99 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.55/0.99 thf(Tqcond_inv4, axiom,
% 0.55/0.99 (![Vqm:vATMap,Vatm2:vATMap,Vqm2:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,
% 0.55/0.99 Vqm1:vATMap,Vatmr:vATMap,Vatm1:vATMap,Vqmr:vATMap,Vexp:vExp,
% 0.55/0.99 Vq2:vQuestionnaire]:
% 0.55/0.99 ( ( ( vptcheck @
% 0.55/0.99 ( vMC @ Vatm @ Vqm ) @ ( vqcond @ Vexp @ Vq1 @ Vq2 ) @
% 0.55/0.99 ( vMC @ Vatmr @ Vqmr ) ) &
% 0.55/0.99 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) &
% 0.55/0.99 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq2 @ ( vMC @ Vatm2 @ Vqm2 ) ) ) =>
% 0.55/0.99 ( ( Vatm1 ) = ( Vatm2 ) ) ))).
% 0.55/0.99 thf(zip_derived_cl41, plain,
% 0.55/0.99 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap,
% 0.55/0.99 X4 : vQuestionnaire, X5 : vATMap, X6 : vExp, X7 : vQuestionnaire,
% 0.55/0.99 X8 : vATMap, X9 : vATMap, X10 : vATMap]:
% 0.55/0.99 (((X1) = (X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X4 @ (vMC @ X1 @ X5))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ (vqcond @ X6 @ X4 @ X7) @
% 0.55/0.99 (vMC @ X8 @ X9))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X7 @ (vMC @ X0 @ X10)))),
% 0.55/0.99 inference('cnf', [status(esa)], [Tqcond_inv4])).
% 0.55/0.99 thf(zip_derived_cl456, plain,
% 0.55/0.99 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq2 @ (vMC @ X1 @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq1 @ (vMC @ X3 @ X2))
% 0.55/0.99 | ((X3) = (X1)))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl49, zip_derived_cl41])).
% 0.55/0.99 thf(zip_derived_cl563, plain,
% 0.55/0.99 (![X0 : vMapConf, X1 : vATMap, X2 : vATMap]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq2 @ X0)
% 0.55/0.99 | ((X1) = ('#_fresh_sk3' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq1 @ (vMC @ X1 @ X2)))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl511, zip_derived_cl456])).
% 0.55/0.99 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.99 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.99 thf(zip_derived_cl721, plain,
% 0.55/0.99 (![X0 : vMapConf, X1 : vATMap, X2 : vATMap]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @ X0)
% 0.55/0.99 | ((X1) = ('#_fresh_sk3' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq1 @ (vMC @ X1 @ X2)))),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl563, zip_derived_cl707, zip_derived_cl707])).
% 0.55/0.99 thf(zip_derived_cl1016, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 (((sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = ('#_fresh_sk3' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @ X0))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl948, zip_derived_cl721])).
% 0.55/0.99 thf(zip_derived_cl1056, plain,
% 0.55/0.99 (((sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = ('#_fresh_sk3' @
% 0.55/0.99 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl949, zip_derived_cl1016])).
% 0.55/0.99 thf(zip_derived_cl198, plain,
% 0.55/0.99 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk3' @ (vMC @ X1 @ X3)) = (X1))),
% 0.55/0.99 inference('inj_rec', [status(thm)], [zip_derived_cl3])).
% 0.55/0.99 thf(zip_derived_cl1057, plain,
% 0.55/0.99 (((sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl1056, zip_derived_cl198])).
% 0.55/0.99 thf(zip_derived_cl1057, plain,
% 0.55/0.99 (((sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl1056, zip_derived_cl198])).
% 0.55/0.99 thf(zip_derived_cl1069, plain,
% 0.55/0.99 ((((sk__20) = (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @
% 0.55/0.99 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl981, zip_derived_cl1057, zip_derived_cl1057])).
% 0.55/0.99 thf(zip_derived_cl949, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.99 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl40])).
% 0.55/0.99 thf(zip_derived_cl948, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq1 @
% 0.55/0.99 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl39])).
% 0.55/0.99 thf(zip_derived_cl511, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ ('#_fresh_sk4' @ X0)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl247, zip_derived_cl485])).
% 0.55/0.99 thf(zip_derived_cl49, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @
% 0.55/0.99 (vMC @ sk__20 @ sk__16))),
% 0.55/0.99 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.55/0.99 thf(Tqcond_inv5, axiom,
% 0.55/0.99 (![Vqm:vATMap,Vatm2:vATMap,Vqm2:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,
% 0.55/0.99 Vqm1:vATMap,Vatmr:vATMap,Vatm1:vATMap,Vqmr:vATMap,Vexp:vExp,
% 0.55/0.99 Vq2:vQuestionnaire]:
% 0.55/0.99 ( ( ( vptcheck @
% 0.55/0.99 ( vMC @ Vatm @ Vqm ) @ ( vqcond @ Vexp @ Vq1 @ Vq2 ) @
% 0.55/0.99 ( vMC @ Vatmr @ Vqmr ) ) &
% 0.55/0.99 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) &
% 0.55/0.99 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq2 @ ( vMC @ Vatm2 @ Vqm2 ) ) ) =>
% 0.55/0.99 ( ( Vqm1 ) = ( Vqm2 ) ) ))).
% 0.55/0.99 thf(zip_derived_cl42, plain,
% 0.55/0.99 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap,
% 0.55/0.99 X4 : vQuestionnaire, X5 : vATMap, X6 : vExp, X7 : vQuestionnaire,
% 0.55/0.99 X8 : vATMap, X9 : vATMap, X10 : vATMap]:
% 0.55/0.99 (((X1) = (X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X4 @ (vMC @ X5 @ X1))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ (vqcond @ X6 @ X4 @ X7) @
% 0.55/0.99 (vMC @ X8 @ X9))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X7 @ (vMC @ X10 @ X0)))),
% 0.55/0.99 inference('cnf', [status(esa)], [Tqcond_inv5])).
% 0.55/0.99 thf(zip_derived_cl457, plain,
% 0.55/0.99 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq2 @ (vMC @ X1 @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq1 @ (vMC @ X3 @ X2))
% 0.55/0.99 | ((X2) = (X0)))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl49, zip_derived_cl42])).
% 0.55/0.99 thf(zip_derived_cl564, plain,
% 0.55/0.99 (![X0 : vMapConf, X1 : vATMap, X2 : vATMap]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq2 @ X0)
% 0.55/0.99 | ((X1) = ('#_fresh_sk4' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq1 @ (vMC @ X2 @ X1)))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl511, zip_derived_cl457])).
% 0.55/0.99 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.99 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.99 thf(zip_derived_cl722, plain,
% 0.55/0.99 (![X0 : vMapConf, X1 : vATMap, X2 : vATMap]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @ X0)
% 0.55/0.99 | ((X1) = ('#_fresh_sk4' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq1 @ (vMC @ X2 @ X1)))),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl564, zip_derived_cl707, zip_derived_cl707])).
% 0.55/0.99 thf(zip_derived_cl1018, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 (((sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = ('#_fresh_sk4' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @ X0))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl948, zip_derived_cl722])).
% 0.55/0.99 thf(zip_derived_cl1060, plain,
% 0.55/0.99 (((sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = ('#_fresh_sk4' @
% 0.55/0.99 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl949, zip_derived_cl1018])).
% 0.55/0.99 thf(zip_derived_cl200, plain,
% 0.55/0.99 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk4' @ (vMC @ X3 @ X1)) = (X1))),
% 0.55/0.99 inference('inj_rec', [status(thm)], [zip_derived_cl4])).
% 0.55/0.99 thf(zip_derived_cl1061, plain,
% 0.55/0.99 (((sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl1060, zip_derived_cl200])).
% 0.55/0.99 thf(zip_derived_cl949, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.99 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl40])).
% 0.55/0.99 thf(zip_derived_cl1084, plain,
% 0.55/0.99 (((sk__20) = (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl1069, zip_derived_cl1061, zip_derived_cl949])).
% 0.55/0.99 thf(zip_derived_cl1085, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.99 (vMC @ sk__20 @
% 0.55/0.99 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl949, zip_derived_cl1084])).
% 0.55/0.99 thf(zip_derived_cl511, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ ('#_fresh_sk4' @ X0)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl247, zip_derived_cl485])).
% 0.55/0.99 thf(zip_derived_cl49, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 (vqcond @ (vconstant @ (vB @ vno)) @ vq1 @ vq2) @
% 0.55/0.99 (vMC @ sk__20 @ sk__16))),
% 0.55/0.99 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.55/0.99 thf(Tqcond_inv7, axiom,
% 0.55/0.99 (![Vqm:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,Vqm1:vATMap,Vatmr:vATMap,
% 0.55/0.99 Vatm1:vATMap,Vqmr:vATMap,Vexp:vExp,Vq2:vQuestionnaire]:
% 0.55/0.99 ( ( ( vptcheck @
% 0.55/0.99 ( vMC @ Vatm @ Vqm ) @ ( vqcond @ Vexp @ Vq1 @ Vq2 ) @
% 0.55/0.99 ( vMC @ Vatmr @ Vqmr ) ) &
% 0.55/0.99 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) &
% 0.55/0.99 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq2 @ ( vMC @ Vatm1 @ Vqm1 ) ) ) =>
% 0.55/0.99 ( ( Vqmr ) = ( Vqm1 ) ) ))).
% 0.55/0.99 thf(zip_derived_cl44, plain,
% 0.55/0.99 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap,
% 0.55/0.99 X4 : vQuestionnaire, X5 : vATMap, X6 : vExp, X7 : vQuestionnaire,
% 0.55/0.99 X8 : vATMap]:
% 0.55/0.99 (((X1) = (X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X4 @ (vMC @ X5 @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ (vqcond @ X6 @ X4 @ X7) @
% 0.55/0.99 (vMC @ X8 @ X1))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X7 @ (vMC @ X5 @ X0)))),
% 0.55/0.99 inference('cnf', [status(esa)], [Tqcond_inv7])).
% 0.55/0.99 thf(zip_derived_cl459, plain,
% 0.55/0.99 (![X0 : vATMap, X1 : vATMap]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq2 @ (vMC @ X1 @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq1 @ (vMC @ X1 @ X0))
% 0.55/0.99 | ((sk__16) = (X0)))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl49, zip_derived_cl44])).
% 0.55/0.99 thf(zip_derived_cl566, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq2 @ X0)
% 0.55/0.99 | ((sk__16) = ('#_fresh_sk4' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq1 @ (vMC @ ('#_fresh_sk3' @ X0) @ ('#_fresh_sk4' @ X0))))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl511, zip_derived_cl459])).
% 0.55/0.99 thf(zip_derived_cl511, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 ((X0) = (vMC @ ('#_fresh_sk3' @ X0) @ ('#_fresh_sk4' @ X0)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl247, zip_derived_cl485])).
% 0.55/0.99 thf(zip_derived_cl577, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq2 @ X0)
% 0.55/0.99 | ((sk__16) = ('#_fresh_sk4' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 0.55/0.99 vq1 @ X0))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl566, zip_derived_cl511])).
% 0.55/0.99 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.99 thf(zip_derived_cl707, plain, (((sk__22) = (sk__18))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl698, zip_derived_cl266])).
% 0.55/0.99 thf(zip_derived_cl723, plain,
% 0.55/0.99 (![X0 : vMapConf]:
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @ X0)
% 0.55/0.99 | ((sk__16) = ('#_fresh_sk4' @ X0))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq1 @ X0))),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl577, zip_derived_cl707, zip_derived_cl707])).
% 0.55/0.99 thf(zip_derived_cl948, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq1 @
% 0.55/0.99 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))))),
% 0.55/0.99 inference('sup-', [status(thm)], [zip_derived_cl715, zip_derived_cl39])).
% 0.55/0.99 thf(zip_derived_cl980, plain,
% 0.55/0.99 ((((sk__16)
% 0.55/0.99 = ('#_fresh_sk4' @
% 0.55/0.99 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @
% 0.55/0.99 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))),
% 0.55/0.99 inference('sup+', [status(thm)], [zip_derived_cl723, zip_derived_cl948])).
% 0.55/0.99 thf(zip_derived_cl200, plain,
% 0.55/0.99 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk4' @ (vMC @ X3 @ X1)) = (X1))),
% 0.55/0.99 inference('inj_rec', [status(thm)], [zip_derived_cl4])).
% 0.55/0.99 thf(zip_derived_cl982, plain,
% 0.55/0.99 ((((sk__16) = (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @
% 0.55/0.99 (vMC @ (sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl980, zip_derived_cl200])).
% 0.55/0.99 thf(zip_derived_cl1057, plain,
% 0.55/0.99 (((sk__12 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl1056, zip_derived_cl198])).
% 0.55/0.99 thf(zip_derived_cl1070, plain,
% 0.55/0.99 ((((sk__16) = (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))
% 0.55/0.99 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 vq2 @
% 0.55/0.99 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 (sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22)))))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl982, zip_derived_cl1057])).
% 0.55/0.99 thf(zip_derived_cl1061, plain,
% 0.55/0.99 (((sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl1060, zip_derived_cl200])).
% 0.55/0.99 thf(zip_derived_cl1084, plain,
% 0.55/0.99 (((sk__20) = (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl1069, zip_derived_cl1061, zip_derived_cl949])).
% 0.55/0.99 thf(zip_derived_cl1061, plain,
% 0.55/0.99 (((sk__13 @ (vtypeAM @ sk__21) @ vq1 @ (vtypeQM @ sk__22))
% 0.55/0.99 = (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl1060, zip_derived_cl200])).
% 0.55/0.99 thf(zip_derived_cl1085, plain,
% 0.55/0.99 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.99 (vMC @ sk__20 @
% 0.55/0.99 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl949, zip_derived_cl1084])).
% 0.55/0.99 thf(zip_derived_cl1463, plain,
% 0.55/0.99 (((sk__16) = (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl1070, zip_derived_cl1061, zip_derived_cl1084,
% 0.55/0.99 zip_derived_cl1061, zip_derived_cl1085])).
% 0.55/0.99 thf(zip_derived_cl47, plain,
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__19) @ (vtypeQM @ sk__22)) @
% 0.55/0.99 sk__17 @ (vMC @ sk__20 @ sk__16))),
% 0.55/0.99 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.55/0.99 thf(zip_derived_cl687, plain, (((vq2) = (sk__17))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl680, zip_derived_cl272])).
% 0.55/0.99 thf(zip_derived_cl689, plain,
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__19) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.99 (vMC @ sk__20 @ sk__16))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl47, zip_derived_cl687])).
% 0.55/0.99 thf(zip_derived_cl686, plain, (((sk__21) = (sk__19))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl674, zip_derived_cl260])).
% 0.55/0.99 thf(zip_derived_cl691, plain,
% 0.55/0.99 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 0.55/0.99 (vMC @ sk__20 @ sk__16))),
% 0.55/0.99 inference('demod', [status(thm)], [zip_derived_cl689, zip_derived_cl686])).
% 0.55/0.99 thf(zip_derived_cl1466, plain, ($false),
% 0.55/0.99 inference('demod', [status(thm)],
% 0.55/0.99 [zip_derived_cl1085, zip_derived_cl1463, zip_derived_cl691])).
% 0.55/0.99
% 0.55/0.99 % SZS output end Refutation
% 0.55/0.99
% 0.55/0.99
% 0.55/0.99 % Terminating...
% 3.03/1.06 % Runner terminated.
% 3.03/1.07 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------