%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : CSR044-10 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.KVKoGGbVu5 true
% Computer : n027.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 : Thu Oct 2 04:31:05 PM UTC 2025
% Result : Unsatisfiable 7.12s 2.01s
% Output : Refutation 7.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : CSR044-10 : TPTP v9.2.0. Released v7.5.0.
% 0.10/0.11 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.KVKoGGbVu5 true
% 0.10/0.31 % Computer : n027.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.31 % CPULimit : 300
% 0.16/0.31 % WCLimit : 300
% 0.16/0.31 % DateTime : Wed Oct 1 14:51:08 EDT 2025
% 0.16/0.31 % CPUTime :
% 0.16/0.31 % Running portfolio for 300 s
% 0.16/0.31 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.31 % Number of cores: 8
% 0.16/0.32 % Python version: Python 3.6.8
% 0.16/0.32 % Running in FO mode
% 0.57/0.61 % Total configuration time : 435
% 0.57/0.61 % Estimated wc time : 1092
% 0.57/0.61 % Estimated cpu time (7 cpus) : 156.0
% 0.99/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.99/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.99/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.99/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 1.24/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 1.27/0.86 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 1.27/0.87 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 4.36/1.49 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 7.12/2.01 % Solved by fo/fo7.sh.
% 7.12/2.01 % done 476 iterations in 1.163s
% 7.12/2.01 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 7.12/2.01 % SZS output start Refutation
% 7.12/2.01 thf(c_tptp_9_720_type, type, c_tptp_9_720: $i).
% 7.12/2.01 thf(c_cyclistsmt_type, type, c_cyclistsmt: $i).
% 7.12/2.01 thf(ifeq2_type, type, ifeq2: $i > $i > $i > $i > $i).
% 7.12/2.01 thf(tptp_9_720_type, type, tptp_9_720: $i > $i > $i).
% 7.12/2.01 thf(f_relationallexistsfn_type, type, f_relationallexistsfn: $i > $i > $i >
% 7.12/2.01 $i > $i).
% 7.12/2.01 thf(c_basekb_type, type, c_basekb: $i).
% 7.12/2.01 thf(relationallexists_type, type, relationallexists: $i > $i > $i > $i).
% 7.12/2.01 thf(c_tptpcol_16_29490_type, type, c_tptpcol_16_29490: $i).
% 7.12/2.01 thf(executionbyfiringsquad_type, type, executionbyfiringsquad: $i > $i).
% 7.12/2.01 thf(c_tptp_spindleheadmt_type, type, c_tptp_spindleheadmt: $i).
% 7.12/2.01 thf(true_type, type, true: $i).
% 7.12/2.01 thf(mtvisible_type, type, mtvisible: $i > $i).
% 7.12/2.01 thf(genlmt_type, type, genlmt: $i > $i > $i).
% 7.12/2.01 thf(b_type, type, b: $i).
% 7.12/2.01 thf(c_worldgeographymt_type, type, c_worldgeographymt: $i).
% 7.12/2.01 thf(isa_type, type, isa: $i > $i > $i).
% 7.12/2.01 thf(genls_type, type, genls: $i > $i > $i).
% 7.12/2.01 thf(c_tptp_member3633_mt_type, type, c_tptp_member3633_mt: $i).
% 7.12/2.01 thf(ifeq4_type, type, ifeq4: $i > $i > $i > $i > $i).
% 7.12/2.01 thf(c_tptpexecutionbyfiringsquad_90_type, type, c_tptpexecutionbyfiringsquad_90:
% 7.12/2.01 $i).
% 7.12/2.01 thf(collection_type, type, collection: $i > $i).
% 7.12/2.01 thf(tuple2_type, type, tuple2: $i > $i > $i).
% 7.12/2.01 thf(a_type, type, a: $i).
% 7.12/2.01 thf(c_executionbyfiringsquad_type, type, c_executionbyfiringsquad: $i).
% 7.12/2.01 thf(tptpcol_16_29490_type, type, tptpcol_16_29490: $i > $i).
% 7.12/2.01 thf(c_collection_type, type, c_collection: $i).
% 7.12/2.01 thf(ax2_3768, axiom,
% 7.12/2.01 (( executionbyfiringsquad @ c_tptpexecutionbyfiringsquad_90 ) = ( true ))).
% 7.12/2.01 thf(zip_derived_cl22, plain,
% 7.12/2.01 (((executionbyfiringsquad @ c_tptpexecutionbyfiringsquad_90) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_3768])).
% 7.12/2.01 thf(ax2_1411, axiom, (( genlmt @ c_worldgeographymt @ c_basekb ) = ( true ))).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl87, plain,
% 7.12/2.01 (((executionbyfiringsquad @ c_tptpexecutionbyfiringsquad_90)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl22, zip_derived_cl9])).
% 7.12/2.01 thf(ax2_2496, axiom,
% 7.12/2.01 (( ifeq4 @
% 7.12/2.01 ( mtvisible @ c_cyclistsmt ) @ true @
% 7.12/2.01 ( relationallexists @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490 ) @
% 7.12/2.01 true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl13, plain,
% 7.12/2.01 (((ifeq4 @ (mtvisible @ c_cyclistsmt) @ true @
% 7.12/2.01 (relationallexists @ c_tptp_9_720 @ c_executionbyfiringsquad @
% 7.12/2.01 c_tptpcol_16_29490) @
% 7.12/2.01 true) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_2496])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl97, plain,
% 7.12/2.01 (((ifeq4 @ (mtvisible @ c_cyclistsmt) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (relationallexists @ c_tptp_9_720 @ c_executionbyfiringsquad @
% 7.12/2.01 c_tptpcol_16_29490) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl13, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9])).
% 7.12/2.01 thf(ax2_4288, axiom,
% 7.12/2.01 (( genlmt @ c_tptp_spindleheadmt @ c_cyclistsmt ) = ( true ))).
% 7.12/2.01 thf(zip_derived_cl25, plain,
% 7.12/2.01 (((genlmt @ c_tptp_spindleheadmt @ c_cyclistsmt) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_4288])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl88, plain,
% 7.12/2.01 (((genlmt @ c_tptp_spindleheadmt @ c_cyclistsmt)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl25, zip_derived_cl9])).
% 7.12/2.01 thf(ax2_142, axiom,
% 7.12/2.01 (( genlmt @ c_tptp_member3633_mt @ c_tptp_spindleheadmt ) = ( true ))).
% 7.12/2.01 thf(zip_derived_cl4, plain,
% 7.12/2.01 (((genlmt @ c_tptp_member3633_mt @ c_tptp_spindleheadmt) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_142])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl92, plain,
% 7.12/2.01 (((genlmt @ c_tptp_member3633_mt @ c_tptp_spindleheadmt)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl4, zip_derived_cl9])).
% 7.12/2.01 thf(ax2_7997, axiom,
% 7.12/2.01 (( ifeq4 @
% 7.12/2.01 ( genlmt @ SPECMT @ GENLMT ) @ true @
% 7.12/2.01 ( ifeq4 @ ( mtvisible @ SPECMT ) @ true @ ( mtvisible @ GENLMT ) @ true ) @
% 7.12/2.01 true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl72, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i]:
% 7.12/2.01 ((ifeq4 @ (genlmt @ X0 @ X1) @ true @
% 7.12/2.01 (ifeq4 @ (mtvisible @ X0) @ true @ (mtvisible @ X1) @ true) @ true)
% 7.12/2.01 = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_7997])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl201, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i]:
% 7.12/2.01 ((ifeq4 @ (genlmt @ X0 @ X1) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (ifeq4 @ (mtvisible @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @ (mtvisible @ X1) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb)) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl72, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9, zip_derived_cl9, zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl214, plain,
% 7.12/2.01 (((ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (ifeq4 @ (mtvisible @ c_tptp_member3633_mt) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (mtvisible @ c_tptp_spindleheadmt) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb)) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl92, zip_derived_cl201])).
% 7.12/2.01 thf(query144, conjecture, (( mtvisible @ c_tptp_member3633_mt ) != ( true ))).
% 7.12/2.01 thf(zf_stmt_0, negated_conjecture,
% 7.12/2.01 (( mtvisible @ c_tptp_member3633_mt ) = ( true )),
% 7.12/2.01 inference('cnf.neg', [status(esa)], [query144])).
% 7.12/2.01 thf(zip_derived_cl81, plain, (((mtvisible @ c_tptp_member3633_mt) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [zf_stmt_0])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl91, plain,
% 7.12/2.01 (((mtvisible @ c_tptp_member3633_mt)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl81, zip_derived_cl9])).
% 7.12/2.01 thf(ifeq_axiom, axiom, (( ifeq4 @ A @ A @ B @ C ) = ( B ))).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl222, plain,
% 7.12/2.01 (((mtvisible @ c_tptp_spindleheadmt)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl214, zip_derived_cl91, zip_derived_cl0,
% 7.12/2.01 zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl201, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i]:
% 7.12/2.01 ((ifeq4 @ (genlmt @ X0 @ X1) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (ifeq4 @ (mtvisible @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @ (mtvisible @ X1) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb)) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl72, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9, zip_derived_cl9, zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl224, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (genlmt @ c_tptp_spindleheadmt @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @ (mtvisible @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb)) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl222, zip_derived_cl201])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl226, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (genlmt @ c_tptp_spindleheadmt @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @ (mtvisible @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl224, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl279, plain,
% 7.12/2.01 (((ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (mtvisible @ c_cyclistsmt) @ (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl88, zip_derived_cl226])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl283, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (mtvisible @ c_cyclistsmt))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl279, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl284, plain,
% 7.12/2.01 (((relationallexists @ c_tptp_9_720 @ c_executionbyfiringsquad @
% 7.12/2.01 c_tptpcol_16_29490) = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl97, zip_derived_cl283, zip_derived_cl0])).
% 7.12/2.01 thf(ax2_7685, axiom,
% 7.12/2.01 (( ifeq4 @
% 7.12/2.01 ( relationallexists @ ARG1 @ ARG2 @ INS ) @ true @
% 7.12/2.01 ( collection @ INS ) @ true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl49, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 7.12/2.01 ((ifeq4 @ (relationallexists @ X0 @ X1 @ X2) @ true @
% 7.12/2.01 (collection @ X2) @ true) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_7685])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl185, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 7.12/2.01 ((ifeq4 @ (relationallexists @ X0 @ X1 @ X2) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @ (collection @ X2) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl49, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl294, plain,
% 7.12/2.01 (((ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (collection @ c_tptpcol_16_29490) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl284, zip_derived_cl185])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl315, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb)
% 7.12/2.01 = (collection @ c_tptpcol_16_29490))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl294, zip_derived_cl0])).
% 7.12/2.01 thf(ax2_7957, axiom,
% 7.12/2.01 (( ifeq4 @ ( collection @ X ) @ true @ ( isa @ X @ c_collection ) @ true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl58, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (collection @ X0) @ true @ (isa @ X0 @ c_collection) @ true)
% 7.12/2.01 = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_7957])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl163, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (collection @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (isa @ X0 @ c_collection) @ (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl58, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl319, plain,
% 7.12/2.01 (((ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (isa @ c_tptpcol_16_29490 @ c_collection) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl315, zip_derived_cl163])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl388, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb)
% 7.12/2.01 = (isa @ c_tptpcol_16_29490 @ c_collection))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl319, zip_derived_cl0])).
% 7.12/2.01 thf(ax2_7978, axiom,
% 7.12/2.01 (( ifeq4 @ ( isa @ ARG1 @ INS ) @ true @ ( collection @ INS ) @ true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl62, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i]:
% 7.12/2.01 ((ifeq4 @ (isa @ X0 @ X1) @ true @ (collection @ X1) @ true) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_7978])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl149, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i]:
% 7.12/2.01 ((ifeq4 @ (isa @ X0 @ X1) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @ (collection @ X1) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl62, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl391, plain,
% 7.12/2.01 (((ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (collection @ c_collection) @ (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl388, zip_derived_cl149])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl399, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (collection @ c_collection))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl391, zip_derived_cl0])).
% 7.12/2.01 thf(ax2_7992, axiom,
% 7.12/2.01 (( ifeq4 @ ( collection @ X ) @ true @ ( genls @ X @ X ) @ true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl69, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (collection @ X0) @ true @ (genls @ X0 @ X0) @ true)
% 7.12/2.01 = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_7992])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl170, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (collection @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @ (genls @ X0 @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl69, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl404, plain,
% 7.12/2.01 (((ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl399, zip_derived_cl170])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl417, plain,
% 7.12/2.01 (((executionbyfiringsquad @ c_tptpexecutionbyfiringsquad_90)
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl87, zip_derived_cl412])).
% 7.12/2.01 thf(ax2_2495, axiom,
% 7.12/2.01 (( ifeq4 @
% 7.12/2.01 ( executionbyfiringsquad @ TERM ) @ true @
% 7.12/2.01 ( ifeq4 @
% 7.12/2.01 ( mtvisible @ c_cyclistsmt ) @ true @
% 7.12/2.01 ( tptp_9_720 @
% 7.12/2.01 TERM @
% 7.12/2.01 ( f_relationallexistsfn @
% 7.12/2.01 TERM @ c_tptp_9_720 @ c_executionbyfiringsquad @
% 7.12/2.01 c_tptpcol_16_29490 ) ) @
% 7.12/2.01 true ) @
% 7.12/2.01 true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl12, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (executionbyfiringsquad @ X0) @ true @
% 7.12/2.01 (ifeq4 @ (mtvisible @ c_cyclistsmt) @ true @
% 7.12/2.01 (tptp_9_720 @ X0 @
% 7.12/2.01 (f_relationallexistsfn @ X0 @ c_tptp_9_720 @
% 7.12/2.01 c_executionbyfiringsquad @ c_tptpcol_16_29490)) @
% 7.12/2.01 true) @
% 7.12/2.01 true) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_2495])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl283, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (mtvisible @ c_cyclistsmt))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl279, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl495, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (mtvisible @ c_cyclistsmt))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl283, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl798, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (executionbyfiringsquad @ X0) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (tptp_9_720 @ X0 @
% 7.12/2.01 (f_relationallexistsfn @ X0 @ c_tptp_9_720 @
% 7.12/2.01 c_executionbyfiringsquad @ c_tptpcol_16_29490)) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl12, zip_derived_cl413, zip_derived_cl495,
% 7.12/2.01 zip_derived_cl413, zip_derived_cl413, zip_derived_cl0,
% 7.12/2.01 zip_derived_cl413, zip_derived_cl413])).
% 7.12/2.01 thf(zip_derived_cl799, plain,
% 7.12/2.01 (((ifeq4 @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (tptp_9_720 @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490)) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl417, zip_derived_cl798])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl801, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (tptp_9_720 @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490)))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl799, zip_derived_cl0])).
% 7.12/2.01 thf(query144_1, conjecture,
% 7.12/2.01 (( ifeq2 @
% 7.12/2.01 ( tuple2 @
% 7.12/2.01 ( tptp_9_720 @ c_tptpexecutionbyfiringsquad_90 @ X ) @
% 7.12/2.01 ( tptpcol_16_29490 @ X ) ) @
% 7.12/2.01 ( tuple2 @ true @ true ) @ a @ b ) !=
% 7.12/2.01 ( b ))).
% 7.12/2.01 thf(zf_stmt_1, negated_conjecture,
% 7.12/2.01 (( ifeq2 @
% 7.12/2.01 ( tuple2 @
% 7.12/2.01 ( tptp_9_720 @ c_tptpexecutionbyfiringsquad_90 @ X ) @
% 7.12/2.01 ( tptpcol_16_29490 @ X ) ) @
% 7.12/2.01 ( tuple2 @ true @ true ) @ a @ b ) =
% 7.12/2.01 ( b )),
% 7.12/2.01 inference('cnf.neg', [status(esa)], [query144_1])).
% 7.12/2.01 thf(zip_derived_cl80, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq2 @
% 7.12/2.01 (tuple2 @ (tptp_9_720 @ c_tptpexecutionbyfiringsquad_90 @ X0) @
% 7.12/2.01 (tptpcol_16_29490 @ X0)) @
% 7.12/2.01 (tuple2 @ true @ true) @ a @ b) = (b))),
% 7.12/2.01 inference('cnf', [status(esa)], [zf_stmt_1])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl200, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq2 @
% 7.12/2.01 (tuple2 @ (tptp_9_720 @ c_tptpexecutionbyfiringsquad_90 @ X0) @
% 7.12/2.01 (tptpcol_16_29490 @ X0)) @
% 7.12/2.01 (tuple2 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb)) @
% 7.12/2.01 a @ b) = (b))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl80, zip_derived_cl9, zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl469, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq2 @
% 7.12/2.01 (tuple2 @ (tptp_9_720 @ c_tptpexecutionbyfiringsquad_90 @ X0) @
% 7.12/2.01 (tptpcol_16_29490 @ X0)) @
% 7.12/2.01 (tuple2 @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (genls @ c_collection @ c_collection)) @
% 7.12/2.01 a @ b) = (b))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl200, zip_derived_cl412, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl807, plain,
% 7.12/2.01 (((ifeq2 @
% 7.12/2.01 (tuple2 @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (tptpcol_16_29490 @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490))) @
% 7.12/2.01 (tuple2 @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (genls @ c_collection @ c_collection)) @
% 7.12/2.01 a @ b) = (b))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl801, zip_derived_cl469])).
% 7.12/2.01 thf(zip_derived_cl284, plain,
% 7.12/2.01 (((relationallexists @ c_tptp_9_720 @ c_executionbyfiringsquad @
% 7.12/2.01 c_tptpcol_16_29490) = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl97, zip_derived_cl283, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl496, plain,
% 7.12/2.01 (((relationallexists @ c_tptp_9_720 @ c_executionbyfiringsquad @
% 7.12/2.01 c_tptpcol_16_29490) = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl284, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl87, plain,
% 7.12/2.01 (((executionbyfiringsquad @ c_tptpexecutionbyfiringsquad_90)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl22, zip_derived_cl9])).
% 7.12/2.01 thf(ax2_7920, axiom,
% 7.12/2.01 (( ifeq4 @
% 7.12/2.01 ( executionbyfiringsquad @ X ) @ true @
% 7.12/2.01 ( isa @ X @ c_executionbyfiringsquad ) @ true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl55, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (executionbyfiringsquad @ X0) @ true @
% 7.12/2.01 (isa @ X0 @ c_executionbyfiringsquad) @ true) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_7920])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl128, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (executionbyfiringsquad @ X0) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (isa @ X0 @ c_executionbyfiringsquad) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl55, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl129, plain,
% 7.12/2.01 (((ifeq4 @ (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (isa @ c_tptpexecutionbyfiringsquad_90 @ c_executionbyfiringsquad) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl87, zip_derived_cl128])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl296, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb)
% 7.12/2.01 = (isa @ c_tptpexecutionbyfiringsquad_90 @ c_executionbyfiringsquad))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl129, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl500, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (isa @ c_tptpexecutionbyfiringsquad_90 @ c_executionbyfiringsquad))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl296, zip_derived_cl412])).
% 7.12/2.01 thf(ax2_2981, axiom,
% 7.12/2.01 (( ifeq4 @
% 7.12/2.01 ( relationallexists @ PRED @ INDEPCOL @ DEPCOL ) @ true @
% 7.12/2.01 ( ifeq4 @
% 7.12/2.01 ( isa @ TERM @ INDEPCOL ) @ true @
% 7.12/2.01 ( isa @
% 7.12/2.01 ( f_relationallexistsfn @ TERM @ PRED @ INDEPCOL @ DEPCOL ) @ DEPCOL ) @
% 7.12/2.01 true ) @
% 7.12/2.01 true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl19, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 7.12/2.01 ((ifeq4 @ (relationallexists @ X0 @ X1 @ X2) @ true @
% 7.12/2.01 (ifeq4 @ (isa @ X3 @ X1) @ true @
% 7.12/2.01 (isa @ (f_relationallexistsfn @ X3 @ X0 @ X1 @ X2) @ X2) @ true) @
% 7.12/2.01 true) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_2981])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl413, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection) = (true))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl787, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 7.12/2.01 ((ifeq4 @ (relationallexists @ X0 @ X1 @ X2) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (ifeq4 @ (isa @ X3 @ X1) @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (isa @ (f_relationallexistsfn @ X3 @ X0 @ X1 @ X2) @ X2) @
% 7.12/2.01 (genls @ c_collection @ c_collection)) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl19, zip_derived_cl413, zip_derived_cl413,
% 7.12/2.01 zip_derived_cl413, zip_derived_cl413, zip_derived_cl413])).
% 7.12/2.01 thf(zip_derived_cl789, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i]:
% 7.12/2.01 ((ifeq4 @ (relationallexists @ X1 @ c_executionbyfiringsquad @ X0) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (ifeq4 @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (isa @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @ X1 @
% 7.12/2.01 c_executionbyfiringsquad @ X0) @
% 7.12/2.01 X0) @
% 7.12/2.01 (genls @ c_collection @ c_collection)) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl500, zip_derived_cl787])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl794, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i]:
% 7.12/2.01 ((ifeq4 @ (relationallexists @ X1 @ c_executionbyfiringsquad @ X0) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (isa @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @ X1 @
% 7.12/2.01 c_executionbyfiringsquad @ X0) @
% 7.12/2.01 X0) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl789, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl912, plain,
% 7.12/2.01 (((ifeq4 @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (isa @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490) @
% 7.12/2.01 c_tptpcol_16_29490) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl496, zip_derived_cl794])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl913, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (isa @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490) @
% 7.12/2.01 c_tptpcol_16_29490))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl912, zip_derived_cl0])).
% 7.12/2.01 thf(ax2_5730, axiom,
% 7.12/2.01 (( ifeq4 @
% 7.12/2.01 ( isa @ X @ c_tptpcol_16_29490 ) @ true @ ( tptpcol_16_29490 @ X ) @
% 7.12/2.01 true ) =
% 7.12/2.01 ( true ))).
% 7.12/2.01 thf(zip_derived_cl35, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (isa @ X0 @ c_tptpcol_16_29490) @ true @
% 7.12/2.01 (tptpcol_16_29490 @ X0) @ true) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_5730])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl9, plain,
% 7.12/2.01 (((genlmt @ c_worldgeographymt @ c_basekb) = (true))),
% 7.12/2.01 inference('cnf', [status(esa)], [ax2_1411])).
% 7.12/2.01 thf(zip_derived_cl122, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (isa @ X0 @ c_tptpcol_16_29490) @
% 7.12/2.01 (genlmt @ c_worldgeographymt @ c_basekb) @
% 7.12/2.01 (tptpcol_16_29490 @ X0) @ (genlmt @ c_worldgeographymt @ c_basekb))
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl35, zip_derived_cl9, zip_derived_cl9,
% 7.12/2.01 zip_derived_cl9])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl412, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (genlmt @ c_worldgeographymt @ c_basekb))),
% 7.12/2.01 inference('demod', [status(thm)], [zip_derived_cl404, zip_derived_cl0])).
% 7.12/2.01 thf(zip_derived_cl440, plain,
% 7.12/2.01 (![X0 : $i]:
% 7.12/2.01 ((ifeq4 @ (isa @ X0 @ c_tptpcol_16_29490) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @ (tptpcol_16_29490 @ X0) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl122, zip_derived_cl412, zip_derived_cl412,
% 7.12/2.01 zip_derived_cl412])).
% 7.12/2.01 thf(zip_derived_cl917, plain,
% 7.12/2.01 (((ifeq4 @ (genls @ c_collection @ c_collection) @
% 7.12/2.01 (genls @ c_collection @ c_collection) @
% 7.12/2.01 (tptpcol_16_29490 @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490)) @
% 7.12/2.01 (genls @ c_collection @ c_collection))
% 7.12/2.01 = (genls @ c_collection @ c_collection))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl913, zip_derived_cl440])).
% 7.12/2.01 thf(zip_derived_cl0, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq4 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom])).
% 7.12/2.01 thf(zip_derived_cl926, plain,
% 7.12/2.01 (((genls @ c_collection @ c_collection)
% 7.12/2.01 = (tptpcol_16_29490 @
% 7.12/2.01 (f_relationallexistsfn @ c_tptpexecutionbyfiringsquad_90 @
% 7.12/2.01 c_tptp_9_720 @ c_executionbyfiringsquad @ c_tptpcol_16_29490)))),
% 7.12/2.01 inference('sup+', [status(thm)], [zip_derived_cl917, zip_derived_cl0])).
% 7.12/2.01 thf(ifeq_axiom_002, axiom, (( ifeq2 @ A @ A @ B @ C ) = ( B ))).
% 7.12/2.01 thf(zip_derived_cl2, plain,
% 7.12/2.01 (![X0 : $i, X1 : $i, X2 : $i]: ((ifeq2 @ X1 @ X1 @ X0 @ X2) = (X0))),
% 7.12/2.01 inference('cnf', [status(esa)], [ifeq_axiom_002])).
% 7.12/2.01 thf(zip_derived_cl927, plain, (((a) = (b))),
% 7.12/2.01 inference('demod', [status(thm)],
% 7.12/2.01 [zip_derived_cl807, zip_derived_cl926, zip_derived_cl2])).
% 7.12/2.01 thf(goal, conjecture, (( a ) = ( b ))).
% 7.12/2.01 thf(zf_stmt_2, negated_conjecture, (( a ) != ( b )),
% 7.12/2.01 inference('cnf.neg', [status(esa)], [goal])).
% 7.12/2.01 thf(zip_derived_cl79, plain, (((a) != (b))),
% 7.12/2.01 inference('cnf', [status(esa)], [zf_stmt_2])).
% 7.12/2.01 thf(zip_derived_cl928, plain, ($false),
% 7.12/2.01 inference('simplify_reflect-', [status(thm)],
% 7.12/2.01 [zip_derived_cl927, zip_derived_cl79])).
% 7.12/2.01
% 7.12/2.01 % SZS output end Refutation
% 7.12/2.01
% 7.12/2.01
% 7.12/2.01 % Terminating...
% 8.07/2.22 % Runner terminated.
% 8.07/2.25 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------