%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM258_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.hqdOPvKAvb true
% Computer : n009.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 7.96s 1.74s
% Output : Refutation 7.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM258_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.hqdOPvKAvb true
% 0.16/0.33 % Computer : n009.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 19:52:11 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 % Running portfolio for 300 s
% 0.16/0.33 % 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.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.52/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.52/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.52/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.52/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 7.96/1.74 % Solved by fo/fo4.sh.
% 7.96/1.74 % done 1288 iterations in 0.949s
% 7.96/1.74 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 7.96/1.74 % SZS output start Refutation
% 7.96/1.74 thf(vMapConf_type, type, vMapConf: $tType).
% 7.96/1.74 thf(vATMap_type, type, vATMap: $tType).
% 7.96/1.74 thf(vQuestionnaire_type, type, vQuestionnaire: $tType).
% 7.96/1.74 thf(vAnsMap_type, type, vAnsMap: $tType).
% 7.96/1.74 thf(vQMap_type, type, vQMap: $tType).
% 7.96/1.74 thf(vOptQConf_type, type, vOptQConf: $tType).
% 7.96/1.74 thf(vQConf_type, type, vQConf: $tType).
% 7.96/1.74 thf(vsomeQConf_type, type, vsomeQConf: vQConf > vOptQConf).
% 7.96/1.74 thf('#_fresh_sk6_type', type, '#_fresh_sk6': vQConf > vAnsMap).
% 7.96/1.74 thf(sk__1_type, type, sk__1: vMapConf > vATMap).
% 7.96/1.74 thf(sk__14_type, type, sk__14: vQuestionnaire > vATMap > vATMap > vATMap).
% 7.96/1.74 thf(vq1_type, type, vq1: vQuestionnaire).
% 7.96/1.74 thf(sk__17_type, type, sk__17: vQuestionnaire).
% 7.96/1.74 thf(vtypeAM_type, type, vtypeAM: vAnsMap > vATMap).
% 7.96/1.74 thf(vtypeQM_type, type, vtypeQM: vQMap > vATMap).
% 7.96/1.74 thf(vptcheck_type, type, vptcheck: vMapConf > vQuestionnaire > vMapConf > $o).
% 7.96/1.74 thf(vqseq_type, type, vqseq: vQuestionnaire > vQuestionnaire > vQuestionnaire).
% 7.96/1.74 thf(sk__15_type, type, sk__15: vQuestionnaire > vATMap > vATMap > vATMap).
% 7.96/1.74 thf(vMC_type, type, vMC: vATMap > vATMap > vMapConf).
% 7.96/1.74 thf('#_fresh_sk7_type', type, '#_fresh_sk7': vQConf > vQMap).
% 7.96/1.74 thf('#_fresh_sk2_type', type, '#_fresh_sk2': vMapConf > vATMap).
% 7.96/1.74 thf(vqempty_type, type, vqempty: vQuestionnaire).
% 7.96/1.74 thf(sk__20_type, type, sk__20: vATMap).
% 7.96/1.74 thf(sk__16_type, type, sk__16: vATMap).
% 7.96/1.74 thf(sk__21_type, type, sk__21: vAnsMap).
% 7.96/1.74 thf(vreduce_type, type, vreduce: vQuestionnaire > vAnsMap > vQMap > vOptQConf).
% 7.96/1.74 thf(vq2_type, type, vq2: vQuestionnaire).
% 7.96/1.74 thf(sk__19_type, type, sk__19: vAnsMap).
% 7.96/1.74 thf(vQC_type, type, vQC: vAnsMap > vQMap > vQuestionnaire > vQConf).
% 7.96/1.74 thf('#_fresh_sk3_type', type, '#_fresh_sk3': vMapConf > vATMap).
% 7.96/1.74 thf(sk__22_type, type, sk__22: vQMap).
% 7.96/1.74 thf(sk__18_type, type, sk__18: vQMap).
% 7.96/1.74 thf(sk__type, type, sk_: vMapConf > vATMap).
% 7.96/1.74 thf('#_fresh_sk1_type', type, '#_fresh_sk1': vOptQConf > vQConf).
% 7.96/1.74 thf('#_fresh_sk8_type', type, '#_fresh_sk8': vQConf > vQuestionnaire).
% 7.96/1.74 thf('dom-MapConf', axiom,
% 7.96/1.74 (![VX:vMapConf]:
% 7.96/1.74 ( ?[VATMap0:vATMap,VATMap1:vATMap]:
% 7.96/1.74 ( ( VX ) = ( vMC @ VATMap0 @ VATMap1 ) ) ))).
% 7.96/1.74 thf(zip_derived_cl0, plain,
% 7.96/1.74 (![X0 : vMapConf]: ((X0) = (vMC @ (sk_ @ X0) @ (sk__1 @ X0)))),
% 7.96/1.74 inference('cnf', [status(esa)], [dom-MapConf])).
% 7.96/1.74 thf(zip_derived_cl0, plain,
% 7.96/1.74 (![X0 : vMapConf]: ((X0) = (vMC @ (sk_ @ X0) @ (sk__1 @ X0)))),
% 7.96/1.74 inference('cnf', [status(esa)], [dom-MapConf])).
% 7.96/1.74 thf('EQ-MC', axiom,
% 7.96/1.74 (![VATMap0:vATMap,VATMap1:vATMap,VATMap2:vATMap,VATMap3:vATMap]:
% 7.96/1.74 ( ( ( vMC @ VATMap0 @ VATMap1 ) = ( vMC @ VATMap2 @ VATMap3 ) ) =>
% 7.96/1.74 ( ( ( VATMap0 ) = ( VATMap2 ) ) & ( ( VATMap1 ) = ( VATMap3 ) ) ) ))).
% 7.96/1.74 thf(zip_derived_cl1, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 7.96/1.74 (((X1) = (X0)) | ((vMC @ X1 @ X3) != (vMC @ X0 @ X2)))),
% 7.96/1.74 inference('cnf', [status(esa)], [EQ-MC])).
% 7.96/1.74 thf(zip_derived_cl65, plain,
% 7.96/1.74 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk2' @ (vMC @ X1 @ X3)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl1])).
% 7.96/1.74 thf(zip_derived_cl115, plain,
% 7.96/1.74 (![X0 : vMapConf]: (('#_fresh_sk2' @ X0) = (sk_ @ X0))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl65])).
% 7.96/1.74 thf(zip_derived_cl116, plain,
% 7.96/1.74 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk2' @ X0) @ (sk__1 @ X0)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl0, zip_derived_cl115])).
% 7.96/1.74 thf(zip_derived_cl116, plain,
% 7.96/1.74 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk2' @ X0) @ (sk__1 @ X0)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl0, zip_derived_cl115])).
% 7.96/1.74 thf(zip_derived_cl2, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 7.96/1.74 (((X1) = (X0)) | ((vMC @ X3 @ X1) != (vMC @ X2 @ X0)))),
% 7.96/1.74 inference('cnf', [status(esa)], [EQ-MC])).
% 7.96/1.74 thf(zip_derived_cl69, plain,
% 7.96/1.74 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk3' @ (vMC @ X3 @ X1)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl2])).
% 7.96/1.74 thf(zip_derived_cl246, plain,
% 7.96/1.74 (![X0 : vMapConf]: (('#_fresh_sk3' @ X0) = (sk__1 @ X0))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl116, zip_derived_cl69])).
% 7.96/1.74 thf(zip_derived_cl270, plain,
% 7.96/1.74 (![X0 : vMapConf]:
% 7.96/1.74 ((X0) = (vMC @ ('#_fresh_sk2' @ X0) @ ('#_fresh_sk3' @ X0)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl116, zip_derived_cl246])).
% 7.96/1.74 thf(Tqempty, axiom,
% 7.96/1.74 (![Vatm:vATMap,Vqm:vATMap]:
% 7.96/1.74 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ vqempty @ ( vMC @ Vatm @ Vqm ) ))).
% 7.96/1.74 thf(zip_derived_cl32, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (vptcheck @ (vMC @ X0 @ X1) @ vqempty @ (vMC @ X0 @ X1))),
% 7.96/1.74 inference('cnf', [status(esa)], [Tqempty])).
% 7.96/1.74 thf('Preservation-qseq-qempty', conjecture,
% 7.96/1.74 (![Vqtm1:vATMap,Vqr:vQuestionnaire,Vqm:vQMap,Vamr:vAnsMap,Vatm1:vATMap,
% 7.96/1.74 Vam:vAnsMap,Vqmr:vQMap]:
% 7.96/1.74 ( ( ( ( vq1 ) = ( vqempty ) ) &
% 7.96/1.74 ( vptcheck @
% 7.96/1.74 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 7.96/1.74 ( vqseq @ vq1 @ vq2 ) @ ( vMC @ Vatm1 @ Vqtm1 ) ) &
% 7.96/1.74 ( ( vreduce @ ( vqseq @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 7.96/1.74 ( vsomeQConf @ ( vQC @ Vamr @ Vqmr @ Vqr ) ) ) ) =>
% 7.96/1.74 ( vptcheck @
% 7.96/1.74 ( vMC @ ( vtypeAM @ Vamr ) @ ( vtypeQM @ Vqmr ) ) @ Vqr @
% 7.96/1.74 ( vMC @ Vatm1 @ Vqtm1 ) ) ))).
% 7.96/1.74 thf(zf_stmt_0, negated_conjecture,
% 7.96/1.74 (~( ![Vqtm1:vATMap,Vqr:vQuestionnaire,Vqm:vQMap,Vamr:vAnsMap,Vatm1:vATMap,
% 7.96/1.74 Vam:vAnsMap,Vqmr:vQMap]:
% 7.96/1.74 ( ( ( ( vq1 ) = ( vqempty ) ) &
% 7.96/1.74 ( vptcheck @
% 7.96/1.74 ( vMC @ ( vtypeAM @ Vam ) @ ( vtypeQM @ Vqm ) ) @
% 7.96/1.74 ( vqseq @ vq1 @ vq2 ) @ ( vMC @ Vatm1 @ Vqtm1 ) ) &
% 7.96/1.74 ( ( vreduce @ ( vqseq @ vq1 @ vq2 ) @ Vam @ Vqm ) =
% 7.96/1.74 ( vsomeQConf @ ( vQC @ Vamr @ Vqmr @ Vqr ) ) ) ) =>
% 7.96/1.74 ( vptcheck @
% 7.96/1.74 ( vMC @ ( vtypeAM @ Vamr ) @ ( vtypeQM @ Vqmr ) ) @ Vqr @
% 7.96/1.74 ( vMC @ Vatm1 @ Vqtm1 ) ) ) )),
% 7.96/1.74 inference('cnf.neg', [status(esa)], [Preservation-qseq-qempty])).
% 7.96/1.74 thf(zip_derived_cl44, plain, (((vq1) = (vqempty))),
% 7.96/1.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.96/1.74 thf(zip_derived_cl189, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (vptcheck @ (vMC @ X0 @ X1) @ vq1 @ (vMC @ X0 @ X1))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl32, zip_derived_cl44])).
% 7.96/1.74 thf(zip_derived_cl45, plain,
% 7.96/1.74 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 7.96/1.74 (vqseq @ vq1 @ vq2) @ (vMC @ sk__20 @ sk__16))),
% 7.96/1.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.96/1.74 thf(Tqseq_inv4, axiom,
% 7.96/1.74 (![Vqm:vATMap,Vatm2:vATMap,Vqm2:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,
% 7.96/1.74 Vqm1:vATMap,Vatmr:vATMap,Vatm1:vATMap,Vqmr:vATMap,Vq2:vQuestionnaire]:
% 7.96/1.74 ( ( ( vptcheck @
% 7.96/1.74 ( vMC @ Vatm @ Vqm ) @ ( vqseq @ Vq1 @ Vq2 ) @
% 7.96/1.74 ( vMC @ Vatmr @ Vqmr ) ) &
% 7.96/1.74 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) &
% 7.96/1.74 ( vptcheck @ ( vMC @ Vatm1 @ Vqm1 ) @ Vq2 @ ( vMC @ Vatm2 @ Vqm2 ) ) ) =>
% 7.96/1.74 ( ( Vqmr ) = ( Vqm2 ) ) ))).
% 7.96/1.74 thf(zip_derived_cl39, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap,
% 7.96/1.74 X4 : vQuestionnaire, X5 : vATMap, X6 : vATMap, X7 : vQuestionnaire,
% 7.96/1.74 X8 : vATMap, X9 : vATMap]:
% 7.96/1.74 (((X1) = (X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X4 @ (vMC @ X5 @ X6))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ X2 @ X3) @ (vqseq @ X4 @ X7) @ (vMC @ X8 @ X1))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ X5 @ X6) @ X7 @ (vMC @ X9 @ X0)))),
% 7.96/1.74 inference('cnf', [status(esa)], [Tqseq_inv4])).
% 7.96/1.74 thf(zip_derived_cl136, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 7.96/1.74 (~ (vptcheck @ (vMC @ X3 @ X2) @ vq2 @ (vMC @ X1 @ X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 7.96/1.74 vq1 @ (vMC @ X3 @ X2))
% 7.96/1.74 | ((sk__16) = (X0)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl45, zip_derived_cl39])).
% 7.96/1.74 thf(zip_derived_cl193, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (((sk__16) = (X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 7.96/1.74 vq2 @ (vMC @ X1 @ X0)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl189, zip_derived_cl136])).
% 7.96/1.74 thf('reduce-8', axiom,
% 7.96/1.74 (![Vqs:vQuestionnaire,Vam:vAnsMap,Vqm:vQMap]:
% 7.96/1.74 ( ( vreduce @ ( vqseq @ vqempty @ Vqs ) @ Vam @ Vqm ) =
% 7.96/1.74 ( vsomeQConf @ ( vQC @ Vam @ Vqm @ Vqs ) ) ))).
% 7.96/1.74 thf(zip_derived_cl15, plain,
% 7.96/1.74 (![X0 : vAnsMap, X1 : vQMap, X2 : vQuestionnaire]:
% 7.96/1.74 ((vreduce @ (vqseq @ vqempty @ X2) @ X0 @ X1)
% 7.96/1.74 = (vsomeQConf @ (vQC @ X0 @ X1 @ X2)))),
% 7.96/1.74 inference('cnf', [status(esa)], [reduce-8])).
% 7.96/1.74 thf(zip_derived_cl44, plain, (((vq1) = (vqempty))),
% 7.96/1.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.96/1.74 thf(zip_derived_cl138, plain,
% 7.96/1.74 (![X0 : vAnsMap, X1 : vQMap, X2 : vQuestionnaire]:
% 7.96/1.74 ((vreduce @ (vqseq @ vq1 @ X2) @ X0 @ X1)
% 7.96/1.74 = (vsomeQConf @ (vQC @ X0 @ X1 @ X2)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl15, zip_derived_cl44])).
% 7.96/1.74 thf(zip_derived_cl43, plain,
% 7.96/1.74 (((vreduce @ (vqseq @ vq1 @ vq2) @ sk__21 @ sk__18)
% 7.96/1.74 = (vsomeQConf @ (vQC @ sk__19 @ sk__22 @ sk__17)))),
% 7.96/1.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.96/1.74 thf(zip_derived_cl139, plain,
% 7.96/1.74 (((vsomeQConf @ (vQC @ sk__21 @ sk__18 @ vq2))
% 7.96/1.74 = (vsomeQConf @ (vQC @ sk__19 @ sk__22 @ sk__17)))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl138, zip_derived_cl43])).
% 7.96/1.74 thf('EQ-someQConf', axiom,
% 7.96/1.74 (![VQConf0:vQConf,VQConf1:vQConf]:
% 7.96/1.74 ( ( ( vsomeQConf @ VQConf0 ) = ( vsomeQConf @ VQConf1 ) ) =>
% 7.96/1.74 ( ( VQConf0 ) = ( VQConf1 ) ) ))).
% 7.96/1.74 thf(zip_derived_cl10, plain,
% 7.96/1.74 (![X0 : vQConf, X1 : vQConf]:
% 7.96/1.74 (((X1) = (X0)) | ((vsomeQConf @ X1) != (vsomeQConf @ X0)))),
% 7.96/1.74 inference('cnf', [status(esa)], [EQ-someQConf])).
% 7.96/1.74 thf(zip_derived_cl50, plain,
% 7.96/1.74 (![X1 : vQConf]: (('#_fresh_sk1' @ (vsomeQConf @ X1)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl10])).
% 7.96/1.74 thf(zip_derived_cl142, plain,
% 7.96/1.74 ((('#_fresh_sk1' @ (vsomeQConf @ (vQC @ sk__19 @ sk__22 @ sk__17)))
% 7.96/1.74 = (vQC @ sk__21 @ sk__18 @ vq2))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl139, zip_derived_cl50])).
% 7.96/1.74 thf(zip_derived_cl50, plain,
% 7.96/1.74 (![X1 : vQConf]: (('#_fresh_sk1' @ (vsomeQConf @ X1)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl10])).
% 7.96/1.74 thf(zip_derived_cl147, plain,
% 7.96/1.74 (((vQC @ sk__19 @ sk__22 @ sk__17) = (vQC @ sk__21 @ sk__18 @ vq2))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl142, zip_derived_cl50])).
% 7.96/1.74 thf(zip_derived_cl147, plain,
% 7.96/1.74 (((vQC @ sk__19 @ sk__22 @ sk__17) = (vQC @ sk__21 @ sk__18 @ vq2))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl142, zip_derived_cl50])).
% 7.96/1.74 thf('EQ-QC', axiom,
% 7.96/1.74 (![VQMap0:vQMap,VAnsMap1:vAnsMap,VQuestionnaire1:vQuestionnaire,
% 7.96/1.74 VAnsMap0:vAnsMap,VQuestionnaire0:vQuestionnaire,VQMap1:vQMap]:
% 7.96/1.74 ( ( ( vQC @ VAnsMap0 @ VQMap0 @ VQuestionnaire0 ) =
% 7.96/1.74 ( vQC @ VAnsMap1 @ VQMap1 @ VQuestionnaire1 ) ) =>
% 7.96/1.74 ( ( ( VAnsMap0 ) = ( VAnsMap1 ) ) & ( ( VQMap0 ) = ( VQMap1 ) ) &
% 7.96/1.74 ( ( VQuestionnaire0 ) = ( VQuestionnaire1 ) ) ) ))).
% 7.96/1.74 thf(zip_derived_cl12, plain,
% 7.96/1.74 (![X0 : vAnsMap, X1 : vAnsMap, X2 : vQMap, X3 : vQuestionnaire,
% 7.96/1.74 X4 : vQMap, X5 : vQuestionnaire]:
% 7.96/1.74 (((X1) = (X0)) | ((vQC @ X1 @ X4 @ X5) != (vQC @ X0 @ X2 @ X3)))),
% 7.96/1.74 inference('cnf', [status(esa)], [EQ-QC])).
% 7.96/1.74 thf(zip_derived_cl82, plain,
% 7.96/1.74 (![X1 : vAnsMap, X4 : vQMap, X5 : vQuestionnaire]:
% 7.96/1.74 (('#_fresh_sk6' @ (vQC @ X1 @ X4 @ X5)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl12])).
% 7.96/1.74 thf(zip_derived_cl160, plain,
% 7.96/1.74 ((('#_fresh_sk6' @ (vQC @ sk__19 @ sk__22 @ sk__17)) = (sk__21))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl147, zip_derived_cl82])).
% 7.96/1.74 thf(zip_derived_cl82, plain,
% 7.96/1.74 (![X1 : vAnsMap, X4 : vQMap, X5 : vQuestionnaire]:
% 7.96/1.74 (('#_fresh_sk6' @ (vQC @ X1 @ X4 @ X5)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl12])).
% 7.96/1.74 thf(zip_derived_cl161, plain, (((sk__21) = (sk__19))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl160, zip_derived_cl82])).
% 7.96/1.74 thf(zip_derived_cl166, plain,
% 7.96/1.74 (((vQC @ sk__21 @ sk__22 @ sk__17) = (vQC @ sk__21 @ sk__18 @ vq2))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl147, zip_derived_cl161])).
% 7.96/1.74 thf(zip_derived_cl13, plain,
% 7.96/1.74 (![X0 : vQMap, X1 : vQMap, X2 : vAnsMap, X3 : vQuestionnaire,
% 7.96/1.74 X4 : vAnsMap, X5 : vQuestionnaire]:
% 7.96/1.74 (((X1) = (X0)) | ((vQC @ X4 @ X1 @ X5) != (vQC @ X2 @ X0 @ X3)))),
% 7.96/1.74 inference('cnf', [status(esa)], [EQ-QC])).
% 7.96/1.74 thf(zip_derived_cl88, plain,
% 7.96/1.74 (![X1 : vQMap, X4 : vAnsMap, X5 : vQuestionnaire]:
% 7.96/1.74 (('#_fresh_sk7' @ (vQC @ X4 @ X1 @ X5)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl13])).
% 7.96/1.74 thf(zip_derived_cl199, plain,
% 7.96/1.74 ((('#_fresh_sk7' @ (vQC @ sk__21 @ sk__22 @ sk__17)) = (sk__18))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl166, zip_derived_cl88])).
% 7.96/1.74 thf(zip_derived_cl88, plain,
% 7.96/1.74 (![X1 : vQMap, X4 : vAnsMap, X5 : vQuestionnaire]:
% 7.96/1.74 (('#_fresh_sk7' @ (vQC @ X4 @ X1 @ X5)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl13])).
% 7.96/1.74 thf(zip_derived_cl209, plain, (((sk__22) = (sk__18))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl199, zip_derived_cl88])).
% 7.96/1.74 thf(zip_derived_cl216, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (((sk__16) = (X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq2 @ (vMC @ X1 @ X0)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl193, zip_derived_cl209])).
% 7.96/1.74 thf(zip_derived_cl294, plain,
% 7.96/1.74 (![X0 : vMapConf]:
% 7.96/1.74 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq2 @ X0)
% 7.96/1.74 | ((sk__16) = ('#_fresh_sk3' @ X0)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl270, zip_derived_cl216])).
% 7.96/1.74 thf(zip_derived_cl45, plain,
% 7.96/1.74 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 7.96/1.74 (vqseq @ vq1 @ vq2) @ (vMC @ sk__20 @ sk__16))),
% 7.96/1.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.96/1.74 thf(zip_derived_cl209, plain, (((sk__22) = (sk__18))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl199, zip_derived_cl88])).
% 7.96/1.74 thf(zip_derived_cl211, plain,
% 7.96/1.74 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 (vqseq @ vq1 @ vq2) @ (vMC @ sk__20 @ sk__16))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl45, zip_derived_cl209])).
% 7.96/1.74 thf(Tqseq_inv2, axiom,
% 7.96/1.74 (![Vqm:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,Vqm1:vATMap,Vatmr:vATMap,
% 7.96/1.74 Vatm1:vATMap,Vqmr:vATMap,Vq2:vQuestionnaire]:
% 7.96/1.74 ( ( ( vptcheck @
% 7.96/1.74 ( vMC @ Vatm @ Vqm ) @ ( vqseq @ Vq1 @ Vq2 ) @
% 7.96/1.74 ( vMC @ Vatmr @ Vqmr ) ) &
% 7.96/1.74 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) ) =>
% 7.96/1.74 ( ?[Vatm2:vATMap,Vqm2:vATMap]:
% 7.96/1.74 ( vptcheck @ ( vMC @ Vatm1 @ Vqm1 ) @ Vq2 @ ( vMC @ Vatm2 @ Vqm2 ) ) ) ))).
% 7.96/1.74 thf(zip_derived_cl37, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap, X2 : vQuestionnaire, X3 : vATMap,
% 7.96/1.74 X4 : vATMap, X5 : vQuestionnaire, X6 : vATMap, X7 : vATMap]:
% 7.96/1.74 (~ (vptcheck @ (vMC @ X0 @ X1) @ X2 @ (vMC @ X3 @ X4))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ X0 @ X1) @ (vqseq @ X2 @ X5) @ (vMC @ X6 @ X7))
% 7.96/1.74 | (vptcheck @ (vMC @ X3 @ X4) @ X5 @
% 7.96/1.74 (vMC @ (sk__14 @ X5 @ X3 @ X4) @ (sk__15 @ X5 @ X3 @ X4))))),
% 7.96/1.74 inference('cnf', [status(esa)], [Tqseq_inv2])).
% 7.96/1.74 thf(zip_derived_cl555, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 ( (vptcheck @ (vMC @ X1 @ X0) @ vq2 @
% 7.96/1.74 (vMC @ (sk__14 @ vq2 @ X1 @ X0) @ (sk__15 @ vq2 @ X1 @ X0)))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq1 @ (vMC @ X1 @ X0)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl37])).
% 7.96/1.74 thf(zip_derived_cl3441, plain,
% 7.96/1.74 ((((sk__16)
% 7.96/1.74 = ('#_fresh_sk3' @
% 7.96/1.74 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq1 @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl294, zip_derived_cl555])).
% 7.96/1.74 thf(zip_derived_cl69, plain,
% 7.96/1.74 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk3' @ (vMC @ X3 @ X1)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl2])).
% 7.96/1.74 thf(zip_derived_cl116, plain,
% 7.96/1.74 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk2' @ X0) @ (sk__1 @ X0)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl0, zip_derived_cl115])).
% 7.96/1.74 thf(zip_derived_cl189, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (vptcheck @ (vMC @ X0 @ X1) @ vq1 @ (vMC @ X0 @ X1))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl32, zip_derived_cl44])).
% 7.96/1.74 thf(zip_derived_cl248, plain,
% 7.96/1.74 (![X0 : vMapConf]:
% 7.96/1.74 (vptcheck @ (vMC @ ('#_fresh_sk2' @ X0) @ (sk__1 @ X0)) @ vq1 @ X0)),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl116, zip_derived_cl189])).
% 7.96/1.74 thf(zip_derived_cl116, plain,
% 7.96/1.74 (![X0 : vMapConf]: ((X0) = (vMC @ ('#_fresh_sk2' @ X0) @ (sk__1 @ X0)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl0, zip_derived_cl115])).
% 7.96/1.74 thf(zip_derived_cl262, plain,
% 7.96/1.74 (![X0 : vMapConf]: (vptcheck @ X0 @ vq1 @ X0)),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl248, zip_derived_cl116])).
% 7.96/1.74 thf(zip_derived_cl3450, plain,
% 7.96/1.74 (((sk__16) = (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 7.96/1.74 inference('demod', [status(thm)],
% 7.96/1.74 [zip_derived_cl3441, zip_derived_cl69, zip_derived_cl262])).
% 7.96/1.74 thf(zip_derived_cl555, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 ( (vptcheck @ (vMC @ X1 @ X0) @ vq2 @
% 7.96/1.74 (vMC @ (sk__14 @ vq2 @ X1 @ X0) @ (sk__15 @ vq2 @ X1 @ X0)))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq1 @ (vMC @ X1 @ X0)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl37])).
% 7.96/1.74 thf(zip_derived_cl3465, plain,
% 7.96/1.74 (( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 7.96/1.74 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 sk__16))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq1 @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl3450, zip_derived_cl555])).
% 7.96/1.74 thf(zip_derived_cl270, plain,
% 7.96/1.74 (![X0 : vMapConf]:
% 7.96/1.74 ((X0) = (vMC @ ('#_fresh_sk2' @ X0) @ ('#_fresh_sk3' @ X0)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl116, zip_derived_cl246])).
% 7.96/1.74 thf(zip_derived_cl189, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (vptcheck @ (vMC @ X0 @ X1) @ vq1 @ (vMC @ X0 @ X1))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl32, zip_derived_cl44])).
% 7.96/1.74 thf(zip_derived_cl45, plain,
% 7.96/1.74 ( (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 7.96/1.74 (vqseq @ vq1 @ vq2) @ (vMC @ sk__20 @ sk__16))),
% 7.96/1.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.96/1.74 thf(Tqseq_inv3, axiom,
% 7.96/1.74 (![Vqm:vATMap,Vatm2:vATMap,Vqm2:vATMap,Vq1:vQuestionnaire,Vatm:vATMap,
% 7.96/1.74 Vqm1:vATMap,Vatmr:vATMap,Vatm1:vATMap,Vqmr:vATMap,Vq2:vQuestionnaire]:
% 7.96/1.74 ( ( ( vptcheck @
% 7.96/1.74 ( vMC @ Vatm @ Vqm ) @ ( vqseq @ Vq1 @ Vq2 ) @
% 7.96/1.74 ( vMC @ Vatmr @ Vqmr ) ) &
% 7.96/1.74 ( vptcheck @ ( vMC @ Vatm @ Vqm ) @ Vq1 @ ( vMC @ Vatm1 @ Vqm1 ) ) &
% 7.96/1.74 ( vptcheck @ ( vMC @ Vatm1 @ Vqm1 ) @ Vq2 @ ( vMC @ Vatm2 @ Vqm2 ) ) ) =>
% 7.96/1.74 ( ( Vatmr ) = ( Vatm2 ) ) ))).
% 7.96/1.74 thf(zip_derived_cl38, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap,
% 7.96/1.74 X4 : vQuestionnaire, X5 : vATMap, X6 : vATMap, X7 : vQuestionnaire,
% 7.96/1.74 X8 : vATMap, X9 : vATMap]:
% 7.96/1.74 (((X1) = (X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ X2 @ X3) @ X4 @ (vMC @ X5 @ X6))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ X2 @ X3) @ (vqseq @ X4 @ X7) @ (vMC @ X1 @ X8))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ X5 @ X6) @ X7 @ (vMC @ X0 @ X9)))),
% 7.96/1.74 inference('cnf', [status(esa)], [Tqseq_inv3])).
% 7.96/1.74 thf(zip_derived_cl135, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap, X2 : vATMap, X3 : vATMap]:
% 7.96/1.74 (~ (vptcheck @ (vMC @ X3 @ X2) @ vq2 @ (vMC @ X1 @ X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 7.96/1.74 vq1 @ (vMC @ X3 @ X2))
% 7.96/1.74 | ((sk__20) = (X1)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl45, zip_derived_cl38])).
% 7.96/1.74 thf(zip_derived_cl192, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (((sk__20) = (X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__18)) @
% 7.96/1.74 vq2 @ (vMC @ X0 @ X1)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl189, zip_derived_cl135])).
% 7.96/1.74 thf(zip_derived_cl209, plain, (((sk__22) = (sk__18))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl199, zip_derived_cl88])).
% 7.96/1.74 thf(zip_derived_cl215, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 (((sk__20) = (X0))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq2 @ (vMC @ X0 @ X1)))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl192, zip_derived_cl209])).
% 7.96/1.74 thf(zip_derived_cl284, plain,
% 7.96/1.74 (![X0 : vMapConf]:
% 7.96/1.74 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq2 @ X0)
% 7.96/1.74 | ((sk__20) = ('#_fresh_sk2' @ X0)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl270, zip_derived_cl215])).
% 7.96/1.74 thf(zip_derived_cl555, plain,
% 7.96/1.74 (![X0 : vATMap, X1 : vATMap]:
% 7.96/1.74 ( (vptcheck @ (vMC @ X1 @ X0) @ vq2 @
% 7.96/1.74 (vMC @ (sk__14 @ vq2 @ X1 @ X0) @ (sk__15 @ vq2 @ X1 @ X0)))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq1 @ (vMC @ X1 @ X0)))),
% 7.96/1.74 inference('sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl37])).
% 7.96/1.74 thf(zip_derived_cl3440, plain,
% 7.96/1.74 ((((sk__20)
% 7.96/1.74 = ('#_fresh_sk2' @
% 7.96/1.74 (vMC @ (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 (sk__15 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))))
% 7.96/1.74 | ~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 vq1 @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22))))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl284, zip_derived_cl555])).
% 7.96/1.74 thf(zip_derived_cl65, plain,
% 7.96/1.74 (![X1 : vATMap, X3 : vATMap]: (('#_fresh_sk2' @ (vMC @ X1 @ X3)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl1])).
% 7.96/1.74 thf(zip_derived_cl262, plain,
% 7.96/1.74 (![X0 : vMapConf]: (vptcheck @ X0 @ vq1 @ X0)),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl248, zip_derived_cl116])).
% 7.96/1.74 thf(zip_derived_cl3449, plain,
% 7.96/1.74 (((sk__20) = (sk__14 @ vq2 @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)))),
% 7.96/1.74 inference('demod', [status(thm)],
% 7.96/1.74 [zip_derived_cl3440, zip_derived_cl65, zip_derived_cl262])).
% 7.96/1.74 thf(zip_derived_cl42, plain,
% 7.96/1.74 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__19) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 sk__17 @ (vMC @ sk__20 @ sk__16))),
% 7.96/1.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.96/1.74 thf(zip_derived_cl161, plain, (((sk__21) = (sk__19))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl160, zip_derived_cl82])).
% 7.96/1.74 thf(zip_derived_cl164, plain,
% 7.96/1.74 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @
% 7.96/1.74 sk__17 @ (vMC @ sk__20 @ sk__16))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl161])).
% 7.96/1.74 thf(zip_derived_cl166, plain,
% 7.96/1.74 (((vQC @ sk__21 @ sk__22 @ sk__17) = (vQC @ sk__21 @ sk__18 @ vq2))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl147, zip_derived_cl161])).
% 7.96/1.74 thf(zip_derived_cl209, plain, (((sk__22) = (sk__18))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl199, zip_derived_cl88])).
% 7.96/1.74 thf(zip_derived_cl214, plain,
% 7.96/1.74 (((vQC @ sk__21 @ sk__22 @ sk__17) = (vQC @ sk__21 @ sk__22 @ vq2))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl166, zip_derived_cl209])).
% 7.96/1.74 thf(zip_derived_cl14, plain,
% 7.96/1.74 (![X0 : vQuestionnaire, X1 : vQuestionnaire, X2 : vAnsMap, X3 : vQMap,
% 7.96/1.74 X4 : vAnsMap, X5 : vQMap]:
% 7.96/1.74 (((X1) = (X0)) | ((vQC @ X4 @ X5 @ X1) != (vQC @ X2 @ X3 @ X0)))),
% 7.96/1.74 inference('cnf', [status(esa)], [EQ-QC])).
% 7.96/1.74 thf(zip_derived_cl100, plain,
% 7.96/1.74 (![X1 : vQuestionnaire, X4 : vAnsMap, X5 : vQMap]:
% 7.96/1.74 (('#_fresh_sk8' @ (vQC @ X4 @ X5 @ X1)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl14])).
% 7.96/1.74 thf(zip_derived_cl225, plain,
% 7.96/1.74 ((('#_fresh_sk8' @ (vQC @ sk__21 @ sk__22 @ vq2)) = (sk__17))),
% 7.96/1.74 inference('sup+', [status(thm)], [zip_derived_cl214, zip_derived_cl100])).
% 7.96/1.74 thf(zip_derived_cl100, plain,
% 7.96/1.74 (![X1 : vQuestionnaire, X4 : vAnsMap, X5 : vQMap]:
% 7.96/1.74 (('#_fresh_sk8' @ (vQC @ X4 @ X5 @ X1)) = (X1))),
% 7.96/1.74 inference('inj_rec', [status(thm)], [zip_derived_cl14])).
% 7.96/1.74 thf(zip_derived_cl232, plain, (((vq2) = (sk__17))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl225, zip_derived_cl100])).
% 7.96/1.74 thf(zip_derived_cl234, plain,
% 7.96/1.74 (~ (vptcheck @ (vMC @ (vtypeAM @ sk__21) @ (vtypeQM @ sk__22)) @ vq2 @
% 7.96/1.74 (vMC @ sk__20 @ sk__16))),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl164, zip_derived_cl232])).
% 7.96/1.74 thf(zip_derived_cl262, plain,
% 7.96/1.74 (![X0 : vMapConf]: (vptcheck @ X0 @ vq1 @ X0)),
% 7.96/1.74 inference('demod', [status(thm)], [zip_derived_cl248, zip_derived_cl116])).
% 7.96/1.74 thf(zip_derived_cl3466, plain, ($false),
% 7.96/1.74 inference('demod', [status(thm)],
% 7.96/1.74 [zip_derived_cl3465, zip_derived_cl3449, zip_derived_cl234,
% 7.96/1.74 zip_derived_cl262])).
% 7.96/1.74
% 7.96/1.74 % SZS output end Refutation
% 7.96/1.74
% 7.96/1.74
% 7.96/1.74 % Terminating...
% 8.65/1.84 % Runner terminated.
% 8.65/1.85 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------