%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP202^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:04:40 AM UTC 2026
% Result : Theorem 0.33s 0.47s
% Output : CNFRefutation 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP202^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.24 % Computer : n013.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.24 % DateTime : Tue Sep 29 20:10:36 UTC 2026
% 0.11/0.24 % CPUTime :
% 0.11/0.24 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.31 Running higher-order theorem proving
% 0.33/0.39 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p
% 0.33/0.47 % Version: 3.5.1-ho
% 0.33/0.47 % Preprocessing class: HSLMSMSMSSLNHHA.
% 0.33/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.33/0.47 % Starting new_bool_8 with 1500s (5) cores
% 0.33/0.47 % Starting full_lambda_4 with 300s (1) cores
% 0.33/0.47 % Starting sh5l with 300s (1) cores
% 0.33/0.47 % Starting ehoh_best8_lambda with 300s (1) cores
% 0.33/0.47 % new_bool_8 with pid 2601118 completed with status 0
% 0.33/0.47 % Result found by new_bool_8
% 0.33/0.47 % Preprocessing class: HSLMSMSMSSLNHHA.
% 0.33/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.33/0.47 % Starting new_bool_8 with 1500s (5) cores
% 0.33/0.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 0.33/0.47 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 0.33/0.47 % Search class: HGHSM-FFMS31-MHHFFSBN
% 0.33/0.47 % partial match(3): HGHSM-FSLS31-MHSFFSBN
% 0.33/0.47 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.33/0.47 % Starting SubtermCWHack with 136s (1) cores
% 0.33/0.47 % Starting new_bool_8 with 151s (1) cores
% 0.33/0.47 % Starting new_bool_1 with 136s (1) cores
% 0.33/0.47 % Starting new_bool_2 with 136s (1) cores
% 0.33/0.47 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 0.33/0.47 % new_bool_1 with pid 2601124 completed with status 0
% 0.33/0.47 % Result found by new_bool_1
% 0.33/0.47 % Preprocessing class: HSLMSMSMSSLNHHA.
% 0.33/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.33/0.47 % Starting new_bool_8 with 1500s (5) cores
% 0.33/0.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 0.33/0.47 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 0.33/0.47 % Search class: HGHSM-FFMS31-MHHFFSBN
% 0.33/0.47 % partial match(3): HGHSM-FSLS31-MHSFFSBN
% 0.33/0.47 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.33/0.47 % Starting SubtermCWHack with 136s (1) cores
% 0.33/0.47 % Starting new_bool_8 with 151s (1) cores
% 0.33/0.47 % Starting new_bool_1 with 136s (1) cores
% 0.33/0.47 % Preprocessing time : 0.006 s
% 0.33/0.47 % Presaturation interreduction done
% 0.33/0.47
% 0.33/0.47 % Proof found!
% 0.33/0.47 % SZS status Theorem
% 0.33/0.47 % SZS output start CNFRefutation
% 0.33/0.47 thf(decl_sort1, type, option_trm: $tType).
% 0.33/0.47 thf(decl_sort2, type, char: $tType).
% 0.33/0.47 thf(decl_sort3, type, option_fml: $tType).
% 0.33/0.47 thf(decl_sort4, type, option_game: $tType).
% 0.33/0.47 thf(decl_sort5, type, produc799602994n_game: $tType).
% 0.33/0.47 thf(decl_sort6, type, produc62062515n_game: $tType).
% 0.33/0.47 thf(decl_sort7, type, set_variable: $tType).
% 0.33/0.47 thf(decl_sort8, type, trm: $tType).
% 0.33/0.47 thf(decl_sort9, type, produc1418842292n_game: $tType).
% 0.33/0.47 thf(decl_37, type, inf_inf_set_variable: set_variable > set_variable > set_variable).
% 0.33/0.47 thf(decl_43, type, none_trm: option_trm).
% 0.33/0.47 thf(decl_46, type, some_trm: trm > option_trm).
% 0.33/0.47 thf(decl_55, type, the_trm: option_trm > trm).
% 0.33/0.47 thf(decl_63, type, bot_bot_set_variable: set_variable).
% 0.33/0.47 thf(decl_83, type, produc1036610745on_trm: ((char > option_fml) > (char > option_game) > char > option_trm) > produc799602994n_game > char > option_trm).
% 0.33/0.47 thf(decl_89, type, produc1231571704on_trm: ((char > option_trm) > produc799602994n_game > char > option_trm) > produc62062515n_game > char > option_trm).
% 0.33/0.47 thf(decl_95, type, produc866613687on_trm: ((char > option_trm) > produc62062515n_game > char > option_trm) > produc1418842292n_game > char > option_trm).
% 0.33/0.47 thf(decl_107, type, static_FVT: trm > set_variable).
% 0.33/0.47 thf(decl_111, type, const: char > trm).
% 0.33/0.47 thf(decl_127, type, uSubst1559070963pconst: produc1418842292n_game > set_variable > char > option_trm).
% 0.33/0.47 thf(decl_129, type, uSubst516392818stappt: produc1418842292n_game > set_variable > trm > option_trm).
% 0.33/0.47 thf(decl_140, type, u: set_variable).
% 0.33/0.47 thf(decl_141, type, v: set_variable).
% 0.33/0.47 thf(decl_142, type, sigma: produc1418842292n_game).
% 0.33/0.47 thf(decl_143, type, f: char).
% 0.33/0.47 thf(decl_170, type, esk27_0: (char > option_trm) > (char > option_fml) > (char > option_game) > char > option_trm).
% 0.33/0.47 thf(decl_171, type, esk28_0: (char > option_trm) > (char > option_trm) > produc799602994n_game > char > option_trm).
% 0.33/0.47 thf(decl_172, type, esk29_0: (char > option_trm) > produc62062515n_game > char > option_trm).
% 0.33/0.47 thf(conj_0, conjecture, (((produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)=(none_trm))|((uSubst516392818stappt @ sigma @ u @ (const @ f))=(uSubst1559070963pconst @ sigma @ v @ f))), file('/export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p', conj_0)).
% 0.33/0.47 thf(fact_3_f3, axiom, (((produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)!=(none_trm))=>((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f))) @ u)=(bot_bot_set_variable))), file('/export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p', fact_3_f3)).
% 0.33/0.47 thf(fact_72_inf__commute, axiom, ((inf_inf_set_variable)=(^[X135:set_variable, X136:set_variable]:(inf_inf_set_variable @ X136 @ X135))), file('/export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p', fact_72_inf__commute)).
% 0.33/0.47 thf(fact_4__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AV_A_061_A_123_125_092_060close_062, axiom, (((produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)!=(none_trm))=>((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f))) @ v)=(bot_bot_set_variable))), file('/export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p', fact_4__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AV_A_061_A_123_125_092_060close_062)).
% 0.33/0.47 thf(fact_10__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_A_Iif_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AU_A_061_A_123_125_Athen_AAterm_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_Aelse_Aundeft_J_A_061_Ausappconst_A_092_060sigma_062_AU_Af_092_060close_062, axiom, (((produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)!=(none_trm))=>((((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f))) @ u)=(bot_bot_set_variable))=>((some_trm @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ u @ f)))&(((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f))) @ u)!=(bot_bot_set_variable))=>((none_trm)=(uSubst1559070963pconst @ sigma @ u @ f))))), file('/export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p', fact_10__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_A_Iif_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AU_A_061_A_123_125_Athen_AAterm_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_Aelse_Aundeft_J_A_061_Ausappconst_A_092_060sigma_062_AU_Af_092_060close_062)).
% 0.33/0.47 thf(fact_9__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_A_Iif_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AV_A_061_A_123_125_Athen_AAterm_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_Aelse_Aundeft_J_A_061_Ausappconst_A_092_060sigma_062_AV_Af_092_060close_062, axiom, (((produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)!=(none_trm))=>((((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f))) @ v)=(bot_bot_set_variable))=>((some_trm @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ v @ f)))&(((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f))) @ v)!=(bot_bot_set_variable))=>((none_trm)=(uSubst1559070963pconst @ sigma @ v @ f))))), file('/export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p', fact_9__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_A_Iif_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AV_A_061_A_123_125_Athen_AAterm_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_Aelse_Aundeft_J_A_061_Ausappconst_A_092_060sigma_062_AV_Af_092_060close_062)).
% 0.33/0.47 thf(fact_7_usubstappt_Osimps_I3_J, axiom, ![X13:produc1418842292n_game, X14:set_variable, X15:char]:(((uSubst516392818stappt @ X13 @ X14 @ (const @ X15))=(uSubst1559070963pconst @ X13 @ X14 @ X15))), file('/export/starexec/sandbox2/tmp/tmp.toimJv0E0g/E---3.1_2601105.p', fact_7_usubstappt_Osimps_I3_J)).
% 0.33/0.47 thf(c_0_7, negated_conjecture, ~((((produc866613687on_trm @ (^[X4:char > option_trm]:(produc1231571704on_trm @ (^[X5:char > option_trm]:(produc1036610745on_trm @ (^[X6:char > option_fml, X7:char > option_game]:(X4)))))) @ sigma @ f)=(none_trm))|((uSubst516392818stappt @ sigma @ u @ (const @ f))=(uSubst1559070963pconst @ sigma @ v @ f)))), inference(assume_negation,[status(cth)],[conj_0])).
% 0.33/0.47 thf(c_0_8, plain, (((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)!=(none_trm))=>((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ u)=(bot_bot_set_variable))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_3_f3])])).
% 0.33/0.47 thf(c_0_9, negated_conjecture, ~((((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)=(none_trm))|((uSubst516392818stappt @ sigma @ u @ (const @ f))=(uSubst1559070963pconst @ sigma @ v @ f)))), inference(fof_simplification,[status(thm)],[c_0_7])).
% 0.33/0.47 thf(c_0_10, plain, (((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)=(none_trm))|((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ u)=(bot_bot_set_variable))), inference(fof_nnf,[status(thm)],[c_0_8])).
% 0.33/0.47 thf(c_0_11, plain, ![X1203:char > option_trm]:(((esk29_0 @ X1203)=(produc1231571704on_trm @ (esk28_0 @ X1203)))), introduced(definition)).
% 0.33/0.47 thf(c_0_12, plain, ![X1201:char > option_trm, X1202:char > option_trm]:(((esk28_0 @ X1202 @ X1201)=(produc1036610745on_trm @ (esk27_0 @ X1202)))), introduced(definition)).
% 0.33/0.47 thf(c_0_13, plain, ![X1199:char > option_game, X1198:char > option_fml, X1200:char > option_trm]:(((esk27_0 @ X1200 @ X1198 @ X1199)=(X1200))), introduced(definition)).
% 0.33/0.47 thf(c_0_14, negated_conjecture, (((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)!=(none_trm))&((uSubst516392818stappt @ sigma @ u @ (const @ f))!=(uSubst1559070963pconst @ sigma @ v @ f))), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])).
% 0.33/0.47 thf(c_0_15, plain, ![X996:set_variable, X997:set_variable]:(((inf_inf_set_variable @ X996 @ X997)=(inf_inf_set_variable @ X997 @ X996))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_72_inf__commute])])).
% 0.33/0.47 thf(c_0_16, plain, (((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)!=(none_trm))=>((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ v)=(bot_bot_set_variable))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_4__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AV_A_061_A_123_125_092_060close_062])])).
% 0.33/0.47 thf(c_0_17, plain, (((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)!=(none_trm))=>((((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ u)=(bot_bot_set_variable))=>((some_trm @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ u @ f)))&(((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ u)!=(bot_bot_set_variable))=>((none_trm)=(uSubst1559070963pconst @ sigma @ u @ f))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_10__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_A_Iif_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AU_A_061_A_123_125_Athen_AAterm_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_Aelse_Aundeft_J_A_061_Ausappconst_A_092_060sigma_062_AU_Af_092_060close_062])])).
% 0.33/0.47 thf(c_0_18, plain, (((produc866613687on_trm @ esk29_0 @ sigma @ f)=(none_trm))|((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))) @ u)=(bot_bot_set_variable))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_10]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13])).
% 0.33/0.47 thf(c_0_19, negated_conjecture, ((produc866613687on_trm @ esk29_0 @ sigma @ f)!=(none_trm)), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_14]), c_0_11]), c_0_12]), c_0_13])).
% 0.33/0.47 thf(c_0_20, plain, ![X1125:set_variable, X1126:set_variable]:(((inf_inf_set_variable @ X1125 @ X1126)=(inf_inf_set_variable @ X1126 @ X1125))), inference(variable_rename,[status(thm)],[c_0_15])).
% 0.33/0.47 thf(c_0_21, plain, (((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)=(none_trm))|((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ v)=(bot_bot_set_variable))), inference(fof_nnf,[status(thm)],[c_0_16])).
% 0.33/0.47 thf(c_0_22, plain, (((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)!=(none_trm))=>((((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ v)=(bot_bot_set_variable))=>((some_trm @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ v @ f)))&(((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ v)!=(bot_bot_set_variable))=>((none_trm)=(uSubst1559070963pconst @ sigma @ v @ f))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_9__092_060open_062SConst_A_092_060sigma_062_Af_A_092_060noteq_062_Aundeft_A_092_060longrightarrow_062_A_Iif_AFVT_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_A_092_060inter_062_AV_A_061_A_123_125_Athen_AAterm_A_Ithe_A_ISConst_A_092_060sigma_062_Af_J_J_Aelse_Aundeft_J_A_061_Ausappconst_A_092_060sigma_062_AV_Af_092_060close_062])])).
% 0.33/0.47 thf(c_0_23, plain, ((((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ u)!=(bot_bot_set_variable))|((some_trm @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ u @ f))|((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)=(none_trm)))&(((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ u)=(bot_bot_set_variable))|((none_trm)=(uSubst1559070963pconst @ sigma @ u @ f))|((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)=(none_trm)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_17])])])).
% 0.33/0.47 thf(c_0_24, plain, ((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))) @ u)=(bot_bot_set_variable)), inference(sr,[status(thm)],[c_0_18, c_0_19])).
% 0.33/0.47 thf(c_0_25, plain, ![X14:set_variable, X9:set_variable]:(((inf_inf_set_variable @ X9 @ X14)=(inf_inf_set_variable @ X14 @ X9))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.33/0.47 thf(c_0_26, plain, (((produc866613687on_trm @ esk29_0 @ sigma @ f)=(none_trm))|((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))) @ v)=(bot_bot_set_variable))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_21]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13])).
% 0.33/0.47 thf(c_0_27, plain, ((((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ v)!=(bot_bot_set_variable))|((some_trm @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ v @ f))|((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)=(none_trm)))&(((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f))) @ v)=(bot_bot_set_variable))|((none_trm)=(uSubst1559070963pconst @ sigma @ v @ f))|((produc866613687on_trm @ (^[Z0:char > option_trm]:(produc1231571704on_trm @ (^[Z1:char > option_trm]:(produc1036610745on_trm @ (^[Z2:char > option_fml, Z3:char > option_game]:(Z0)))))) @ sigma @ f)=(none_trm)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_22])])])).
% 0.33/0.47 thf(c_0_28, plain, (((some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ u @ f))|((produc866613687on_trm @ esk29_0 @ sigma @ f)=(none_trm))|((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))) @ u)!=(bot_bot_set_variable))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13])).
% 0.33/0.47 thf(c_0_29, plain, ((inf_inf_set_variable @ u @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))))=(bot_bot_set_variable)), inference(rw,[status(thm)],[c_0_24, c_0_25])).
% 0.33/0.47 thf(c_0_30, plain, ((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))) @ v)=(bot_bot_set_variable)), inference(sr,[status(thm)],[c_0_26, c_0_19])).
% 0.33/0.47 thf(c_0_31, plain, (((some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ v @ f))|((produc866613687on_trm @ esk29_0 @ sigma @ f)=(none_trm))|((inf_inf_set_variable @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))) @ v)!=(bot_bot_set_variable))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_27]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13])).
% 0.33/0.47 thf(c_0_32, plain, ((some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f)))=(uSubst1559070963pconst @ sigma @ u @ f)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_25]), c_0_29])]), c_0_19])).
% 0.33/0.47 thf(c_0_33, plain, ((inf_inf_set_variable @ v @ (static_FVT @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))))=(bot_bot_set_variable)), inference(rw,[status(thm)],[c_0_30, c_0_25])).
% 0.33/0.47 thf(c_0_34, negated_conjecture, ((uSubst516392818stappt @ sigma @ u @ (const @ f))!=(uSubst1559070963pconst @ sigma @ v @ f)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.33/0.47 thf(c_0_35, plain, ((uSubst1559070963pconst @ sigma @ v @ f)=(uSubst1559070963pconst @ sigma @ u @ f)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32]), c_0_25]), c_0_33])]), c_0_19])).
% 0.33/0.47 thf(c_0_36, plain, ![X1007:produc1418842292n_game, X1008:set_variable, X1009:char]:(((uSubst516392818stappt @ X1007 @ X1008 @ (const @ X1009))=(uSubst1559070963pconst @ X1007 @ X1008 @ X1009))), inference(variable_rename,[status(thm)],[fact_7_usubstappt_Osimps_I3_J])).
% 0.33/0.47 thf(c_0_37, negated_conjecture, ((uSubst516392818stappt @ sigma @ u @ (const @ f))!=(uSubst1559070963pconst @ sigma @ u @ f)), inference(rw,[status(thm)],[c_0_34, c_0_35])).
% 0.33/0.47 thf(c_0_38, plain, ![X8:produc1418842292n_game, X9:set_variable, X10:char]:(((uSubst516392818stappt @ X8 @ X9 @ (const @ X10))=(uSubst1559070963pconst @ X8 @ X9 @ X10))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 0.33/0.47 thf(c_0_39, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])]), ['proof']).
% 0.33/0.47 % SZS output end CNFRefutation
% 0.33/0.47 % Parsed axioms : 507
% 0.33/0.47 % Removed by relevancy pruning/SinE : 430
% 0.33/0.47 % Initial clauses : 132
% 0.33/0.47 % Removed in clause preprocessing : 20
% 0.33/0.47 % Initial clauses in saturation : 112
% 0.33/0.47 % Processed clauses : 67
% 0.33/0.47 % ...of these trivial : 7
% 0.33/0.47 % ...subsumed : 8
% 0.33/0.47 % ...remaining for further processing : 52
% 0.33/0.47 % Other redundant clauses eliminated : 7
% 0.33/0.47 % Clauses deleted for lack of memory : 0
% 0.33/0.47 % Backward-subsumed : 0
% 0.33/0.47 % Backward-rewritten : 7
% 0.33/0.47 % Generated clauses : 7
% 0.33/0.47 % ...of the previous two non-redundant : 7
% 0.33/0.47 % ...aggressively subsumed : 0
% 0.33/0.47 % Contextual simplify-reflections : 0
% 0.33/0.47 % Paramodulations : 0
% 0.33/0.47 % Factorizations : 0
% 0.33/0.47 % NegExts : 0
% 0.33/0.47 % Equation resolutions : 7
% 0.33/0.47 % Disequality decompositions : 0
% 0.33/0.47 % Total rewrite steps : 20
% 0.33/0.47 % ...of those cached : 2
% 0.33/0.47 % Propositional unsat checks : 0
% 0.33/0.47 % Propositional check models : 0
% 0.33/0.47 % Propositional check unsatisfiable : 0
% 0.33/0.47 % Propositional clauses : 0
% 0.33/0.47 % Propositional clauses after purity: 0
% 0.33/0.47 % Propositional unsat core size : 0
% 0.33/0.47 % Propositional preprocessing time : 0.000
% 0.33/0.47 % Propositional encoding time : 0.000
% 0.33/0.47 % Propositional solver time : 0.000
% 0.33/0.47 % Success case prop preproc time : 0.000
% 0.33/0.47 % Success case prop encoding time : 0.000
% 0.33/0.47 % Success case prop solver time : 0.000
% 0.33/0.47 % Current number of processed clauses : 38
% 0.33/0.47 % Positive orientable unit clauses : 19
% 0.33/0.47 % Positive unorientable unit clauses: 3
% 0.33/0.47 % Negative unit clauses : 2
% 0.33/0.47 % Non-unit-clauses : 14
% 0.33/0.47 % Current number of unprocessed clauses: 52
% 0.33/0.47 % ...number of literals in the above : 113
% 0.33/0.47 % Current number of archived formulas : 0
% 0.33/0.47 % Current number of archived clauses : 9
% 0.33/0.47 % Clause-clause subsumption calls (NU) : 16
% 0.33/0.47 % Rec. Clause-clause subsumption calls : 16
% 0.33/0.47 % Non-unit clause-clause subsumptions : 1
% 0.33/0.47 % Unit Clause-clause subsumption calls : 17
% 0.33/0.47 % Rewrite failures with RHS unbound : 0
% 0.33/0.47 % BW rewrite match attempts : 89
% 0.33/0.47 % BW rewrite match successes : 13
% 0.33/0.47 % Condensation attempts : 0
% 0.33/0.47 % Condensation successes : 0
% 0.33/0.47 % Termbank termtop insertions : 18008
% 0.33/0.47 % Search garbage collected termcells : 6146
% 0.33/0.47
% 0.33/0.47 % -------------------------------------------------
% 0.33/0.47 % User time : 0.026 s
% 0.33/0.47 % System time : 0.014 s
% 0.33/0.47 % Total time : 0.040 s
% 0.33/0.47 % Maximum resident set size: 5912 pages
% 0.33/0.47
% 0.33/0.47 % -------------------------------------------------
% 0.33/0.47 % User time : 0.084 s
% 0.33/0.47 % System time : 0.044 s
% 0.33/0.47 % Total time : 0.128 s
% 0.33/0.47 % Maximum resident set size: 6144 pages
% 0.33/0.47 % E exiting
%------------------------------------------------------------------------------