%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP202^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:05:49 AM UTC 2026
% Result : Theorem 0.23s 0.33s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP202^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.17 % Computer : n014.cluster.edu
% 0.12/0.17 % Model : x86_64 x86_64
% 0.12/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.17 % Memory : 8046.5625MB
% 0.12/0.17 % OS : Linux 6.8.0-71-generic
% 0.12/0.17 % CPULimit : 300
% 0.12/0.17 % WCLimit : 300
% 0.12/0.17 % DateTime : Tue Sep 29 20:10:59 UTC 2026
% 0.12/0.17 % CPUTime :
% 0.12/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.22 Running higher-order theorem proving
% 0.12/0.25 Running: /export/starexec/sandbox/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/sandbox/tmp/tmp.0F76mw9qkP/E---3.1_3157661.p
% 0.23/0.33 % Version: 3.5.1-ho
% 0.23/0.33 % Preprocessing class: HSLMSMSMSSLNHHA.
% 0.23/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.33 % Starting new_bool_8 with 1500s (5) cores
% 0.23/0.33 % Starting full_lambda_4 with 300s (1) cores
% 0.23/0.33 % Starting sh5l with 300s (1) cores
% 0.23/0.33 % Starting ehoh_best8_lambda with 300s (1) cores
% 0.23/0.33 % new_bool_8 with pid 3157675 completed with status 0
% 0.23/0.33 % Result found by new_bool_8
% 0.23/0.33 % Preprocessing class: HSLMSMSMSSLNHHA.
% 0.23/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.33 % Starting new_bool_8 with 1500s (5) cores
% 0.23/0.33 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 0.23/0.33 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 0.23/0.33 % Search class: HGHSM-FFMS31-MHHFFSBN
% 0.23/0.33 % partial match(3): HGHSM-FSLS31-MHSFFSBN
% 0.23/0.33 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.23/0.33 % Starting SubtermCWHack with 136s (1) cores
% 0.23/0.33 % Starting new_bool_8 with 151s (1) cores
% 0.23/0.33 % Starting new_bool_1 with 136s (1) cores
% 0.23/0.33 % Starting new_bool_2 with 136s (1) cores
% 0.23/0.33 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 0.23/0.33 % new_bool_8 with pid 3157680 completed with status 0
% 0.23/0.33 % Result found by new_bool_8
% 0.23/0.33 % Preprocessing class: HSLMSMSMSSLNHHA.
% 0.23/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.33 % Starting new_bool_8 with 1500s (5) cores
% 0.23/0.33 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 0.23/0.33 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 0.23/0.33 % Search class: HGHSM-FFMS31-MHHFFSBN
% 0.23/0.33 % partial match(3): HGHSM-FSLS31-MHSFFSBN
% 0.23/0.33 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.23/0.33 % Starting SubtermCWHack with 136s (1) cores
% 0.23/0.33 % Starting new_bool_8 with 151s (1) cores
% 0.23/0.33 % Preprocessing time : 0.004 s
% 0.23/0.33 % Presaturation interreduction done
% 0.23/0.33
% 0.23/0.33 % Proof found!
% 0.23/0.33 % SZS status Theorem
% 0.23/0.33 % SZS output start CNFRefutation
% 0.23/0.33 thf(decl_sort1, type, option_trm: $tType).
% 0.23/0.33 thf(decl_sort2, type, char: $tType).
% 0.23/0.33 thf(decl_sort3, type, option_fml: $tType).
% 0.23/0.33 thf(decl_sort4, type, option_game: $tType).
% 0.23/0.33 thf(decl_sort5, type, produc799602994n_game: $tType).
% 0.23/0.33 thf(decl_sort6, type, produc62062515n_game: $tType).
% 0.23/0.33 thf(decl_sort7, type, set_variable: $tType).
% 0.23/0.33 thf(decl_sort8, type, trm: $tType).
% 0.23/0.33 thf(decl_sort9, type, produc1418842292n_game: $tType).
% 0.23/0.33 thf(decl_37, type, inf_inf_set_variable: set_variable > set_variable > set_variable).
% 0.23/0.33 thf(decl_43, type, none_trm: option_trm).
% 0.23/0.33 thf(decl_46, type, some_trm: trm > option_trm).
% 0.23/0.33 thf(decl_55, type, the_trm: option_trm > trm).
% 0.23/0.33 thf(decl_63, type, bot_bot_set_variable: set_variable).
% 0.23/0.33 thf(decl_83, type, produc1036610745on_trm: ((char > option_fml) > (char > option_game) > char > option_trm) > produc799602994n_game > char > option_trm).
% 0.23/0.33 thf(decl_89, type, produc1231571704on_trm: ((char > option_trm) > produc799602994n_game > char > option_trm) > produc62062515n_game > char > option_trm).
% 0.23/0.33 thf(decl_95, type, produc866613687on_trm: ((char > option_trm) > produc62062515n_game > char > option_trm) > produc1418842292n_game > char > option_trm).
% 0.23/0.33 thf(decl_107, type, static_FVT: trm > set_variable).
% 0.23/0.33 thf(decl_111, type, const: char > trm).
% 0.23/0.33 thf(decl_127, type, uSubst1559070963pconst: produc1418842292n_game > set_variable > char > option_trm).
% 0.23/0.33 thf(decl_129, type, uSubst516392818stappt: produc1418842292n_game > set_variable > trm > option_trm).
% 0.23/0.33 thf(decl_140, type, u: set_variable).
% 0.23/0.33 thf(decl_141, type, v: set_variable).
% 0.23/0.33 thf(decl_142, type, sigma: produc1418842292n_game).
% 0.23/0.33 thf(decl_143, type, f: char).
% 0.23/0.33 thf(decl_170, type, esk27_0: (char > option_trm) > (char > option_fml) > (char > option_game) > char > option_trm).
% 0.23/0.33 thf(decl_171, type, esk28_0: (char > option_trm) > (char > option_trm) > produc799602994n_game > char > option_trm).
% 0.23/0.33 thf(decl_172, type, esk29_0: (char > option_trm) > produc62062515n_game > char > option_trm).
% 0.23/0.33 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/sandbox/tmp/tmp.0F76mw9qkP/E---3.1_3157661.p', conj_0)).
% 0.23/0.33 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/sandbox/tmp/tmp.0F76mw9qkP/E---3.1_3157661.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.23/0.33 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/sandbox/tmp/tmp.0F76mw9qkP/E---3.1_3157661.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.23/0.33 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/sandbox/tmp/tmp.0F76mw9qkP/E---3.1_3157661.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.23/0.33 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/sandbox/tmp/tmp.0F76mw9qkP/E---3.1_3157661.p', fact_3_f3)).
% 0.23/0.33 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/sandbox/tmp/tmp.0F76mw9qkP/E---3.1_3157661.p', fact_7_usubstappt_Osimps_I3_J)).
% 0.23/0.33 thf(c_0_6, 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.23/0.33 thf(c_0_7, 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.23/0.33 thf(c_0_8, 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_6])).
% 0.23/0.33 thf(c_0_9, 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.23/0.33 thf(c_0_10, 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_7])])])).
% 0.23/0.33 thf(c_0_11, plain, ![X1203:char > option_trm]:(((esk29_0 @ X1203)=(produc1231571704on_trm @ (esk28_0 @ X1203)))), introduced(definition)).
% 0.23/0.33 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.23/0.33 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.23/0.33 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_8])])).
% 0.23/0.33 thf(c_0_15, 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_9])).
% 0.23/0.33 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))) @ 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.23/0.33 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))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_3_f3])])).
% 0.23/0.33 thf(c_0_18, 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_10]), 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.23/0.33 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.23/0.33 thf(c_0_20, 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_15]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13])).
% 0.23/0.33 thf(c_0_21, 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_16])])])).
% 0.23/0.33 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))) @ u)=(bot_bot_set_variable))), inference(fof_nnf,[status(thm)],[c_0_17])).
% 0.23/0.33 thf(c_0_23, plain, (((uSubst1559070963pconst @ sigma @ v @ f)=(some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))))|((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_18, c_0_19])).
% 0.23/0.33 thf(c_0_24, 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_20, c_0_19])).
% 0.23/0.33 thf(c_0_25, 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_21]), 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.23/0.33 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))) @ 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_22]), c_0_11]), c_0_12]), c_0_13]), c_0_11]), c_0_12]), c_0_13])).
% 0.23/0.33 thf(c_0_27, negated_conjecture, ((uSubst516392818stappt @ sigma @ u @ (const @ f))!=(uSubst1559070963pconst @ sigma @ v @ f)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.23/0.33 thf(c_0_28, plain, ((uSubst1559070963pconst @ sigma @ v @ f)=(some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 0.23/0.33 thf(c_0_29, 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.23/0.33 thf(c_0_30, plain, (((uSubst1559070963pconst @ sigma @ u @ f)=(some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f))))|((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_25, c_0_19])).
% 0.23/0.33 thf(c_0_31, 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_26, c_0_19])).
% 0.23/0.33 thf(c_0_32, negated_conjecture, ((uSubst516392818stappt @ sigma @ u @ (const @ f))!=(some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f)))), inference(rw,[status(thm)],[c_0_27, c_0_28])).
% 0.23/0.33 thf(c_0_33, 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_29])).
% 0.23/0.33 thf(c_0_34, plain, ((uSubst1559070963pconst @ sigma @ u @ f)=(some_trm @ (the_trm @ (produc866613687on_trm @ esk29_0 @ sigma @ f)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 0.23/0.33 thf(c_0_35, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_33]), c_0_34])]), ['proof']).
% 0.23/0.33 % SZS output end CNFRefutation
% 0.23/0.33 % Parsed axioms : 507
% 0.23/0.33 % Removed by relevancy pruning/SinE : 430
% 0.23/0.33 % Initial clauses : 132
% 0.23/0.33 % Removed in clause preprocessing : 20
% 0.23/0.33 % Initial clauses in saturation : 112
% 0.23/0.33 % Processed clauses : 71
% 0.23/0.33 % ...of these trivial : 6
% 0.23/0.33 % ...subsumed : 9
% 0.23/0.33 % ...remaining for further processing : 56
% 0.23/0.33 % Other redundant clauses eliminated : 7
% 0.23/0.33 % Clauses deleted for lack of memory : 0
% 0.23/0.33 % Backward-subsumed : 0
% 0.23/0.33 % Backward-rewritten : 9
% 0.23/0.33 % Generated clauses : 7
% 0.23/0.33 % ...of the previous two non-redundant : 10
% 0.23/0.33 % ...aggressively subsumed : 0
% 0.23/0.33 % Contextual simplify-reflections : 0
% 0.23/0.33 % Paramodulations : 0
% 0.23/0.33 % Factorizations : 0
% 0.23/0.33 % NegExts : 0
% 0.23/0.33 % Equation resolutions : 7
% 0.23/0.33 % Disequality decompositions : 0
% 0.23/0.33 % Total rewrite steps : 22
% 0.23/0.33 % ...of those cached : 6
% 0.23/0.33 % Propositional unsat checks : 0
% 0.23/0.33 % Propositional check models : 0
% 0.23/0.33 % Propositional check unsatisfiable : 0
% 0.23/0.33 % Propositional clauses : 0
% 0.23/0.33 % Propositional clauses after purity: 0
% 0.23/0.33 % Propositional unsat core size : 0
% 0.23/0.33 % Propositional preprocessing time : 0.000
% 0.23/0.33 % Propositional encoding time : 0.000
% 0.23/0.33 % Propositional solver time : 0.000
% 0.23/0.33 % Success case prop preproc time : 0.000
% 0.23/0.33 % Success case prop encoding time : 0.000
% 0.23/0.33 % Success case prop solver time : 0.000
% 0.23/0.33 % Current number of processed clauses : 40
% 0.23/0.33 % Positive orientable unit clauses : 19
% 0.23/0.33 % Positive unorientable unit clauses: 2
% 0.23/0.33 % Negative unit clauses : 2
% 0.23/0.33 % Non-unit-clauses : 17
% 0.23/0.33 % Current number of unprocessed clauses: 50
% 0.23/0.33 % ...number of literals in the above : 101
% 0.23/0.33 % Current number of archived formulas : 0
% 0.23/0.33 % Current number of archived clauses : 11
% 0.23/0.33 % Clause-clause subsumption calls (NU) : 26
% 0.23/0.33 % Rec. Clause-clause subsumption calls : 26
% 0.23/0.33 % Non-unit clause-clause subsumptions : 3
% 0.23/0.33 % Unit Clause-clause subsumption calls : 20
% 0.23/0.33 % Rewrite failures with RHS unbound : 0
% 0.23/0.33 % BW rewrite match attempts : 18
% 0.23/0.33 % BW rewrite match successes : 15
% 0.23/0.33 % Condensation attempts : 0
% 0.23/0.33 % Condensation successes : 0
% 0.23/0.33 % Termbank termtop insertions : 16982
% 0.23/0.33 % Search garbage collected termcells : 6146
% 0.23/0.33
% 0.23/0.33 % -------------------------------------------------
% 0.23/0.33 % User time : 0.021 s
% 0.23/0.33 % System time : 0.007 s
% 0.23/0.33 % Total time : 0.028 s
% 0.23/0.33 % Maximum resident set size: 5912 pages
% 0.23/0.33
% 0.23/0.33 % -------------------------------------------------
% 0.23/0.33 % User time : 0.067 s
% 0.23/0.33 % System time : 0.024 s
% 0.23/0.33 % Total time : 0.090 s
% 0.23/0.33 % Maximum resident set size: 6144 pages
% 0.23/0.33 % E exiting
%------------------------------------------------------------------------------