%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP109^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 : n007.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:33 AM UTC 2026
% Result : Theorem 14.99s 2.28s
% Output : CNFRefutation 14.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP109^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 19:52:41 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.23/0.27 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.pYAsRfaiFZ/E---3.1_3844260.p
% 14.99/2.28 % Version: 3.5.1-ho
% 14.99/2.28 % Preprocessing class: HSLSSMSSSSLNSSA.
% 14.99/2.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 14.99/2.28 % Starting sh3 with 1500s (5) cores
% 14.99/2.28 % Starting new_bool_9 with 300s (1) cores
% 14.99/2.28 % Starting ehoh_best8_lambda with 300s (1) cores
% 14.99/2.28 % Starting sh4l with 300s (1) cores
% 14.99/2.28 % sh3 with pid 3844273 completed with status 0
% 14.99/2.28 % Result found by sh3
% 14.99/2.28 % Preprocessing class: HSLSSMSSSSLNSSA.
% 14.99/2.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 14.99/2.28 % Starting sh3 with 1500s (5) cores
% 14.99/2.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 14.99/2.28 % No SInE strategy applied
% 14.99/2.28 % Search class: HGHSM-FSLM32-DSSFFSBN
% 14.99/2.28 % partial match(1): HGHSM-FSLM32-DHSFFSBN
% 14.99/2.28 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 14.99/2.28 % Starting SubtermCWHack with 136s (1) cores
% 14.99/2.28 % Starting sh3 with 151s (1) cores
% 14.99/2.28 % Starting sh4l with 214s (1) cores
% 14.99/2.28 % Starting pre_casc_4 with 204s (1) cores
% 14.99/2.28 % Starting lpo5_fix with 136s (1) cores
% 14.99/2.28 % sh4l with pid 3844282 completed with status 0
% 14.99/2.28 % Result found by sh4l
% 14.99/2.28 % Preprocessing class: HSLSSMSSSSLNSSA.
% 14.99/2.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 14.99/2.28 % Starting sh3 with 1500s (5) cores
% 14.99/2.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 14.99/2.28 % No SInE strategy applied
% 14.99/2.28 % Search class: HGHSM-FSLM32-DSSFFSBN
% 14.99/2.28 % partial match(1): HGHSM-FSLM32-DHSFFSBN
% 14.99/2.28 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 14.99/2.28 % Starting SubtermCWHack with 136s (1) cores
% 14.99/2.28 % Starting sh3 with 151s (1) cores
% 14.99/2.28 % Starting sh4l with 214s (1) cores
% 14.99/2.28 % Preprocessing time : 0.028 s
% 14.99/2.28
% 14.99/2.28 % Proof found!
% 14.99/2.28 % SZS status Theorem
% 14.99/2.28 % SZS output start CNFRefutation
% 14.99/2.28 thf(decl_sort1, type, real: $tType).
% 14.99/2.28 thf(decl_sort2, type, set_a: $tType).
% 14.99/2.28 thf(decl_sort3, type, a: $tType).
% 14.99/2.28 thf(decl_sort4, type, b: $tType).
% 14.99/2.28 thf(decl_sort5, type, extended_ereal: $tType).
% 14.99/2.28 thf(decl_24, type, inverse_inverse_real: real > real).
% 14.99/2.28 thf(decl_31, type, minus_minus_real: real > real > real).
% 14.99/2.28 thf(decl_35, type, one_one_real: real).
% 14.99/2.28 thf(decl_39, type, plus_plus_b: b > b > b).
% 14.99/2.28 thf(decl_40, type, times_times_real: real > real > real).
% 14.99/2.28 thf(decl_43, type, groups1862963056a_real: (a > real) > set_a > real).
% 14.99/2.28 thf(decl_45, type, groups1199149371um_a_b: (a > b) > set_a > b).
% 14.99/2.28 thf(decl_57, type, real_V1035702896aleR_b: real > b > b).
% 14.99/2.28 thf(decl_58, type, divide_divide_real: real > real > real).
% 14.99/2.28 thf(decl_62, type, insert_a: a > set_a > set_a).
% 14.99/2.28 thf(decl_68, type, aa: a > real).
% 14.99/2.28 thf(decl_69, type, f: b > extended_ereal).
% 14.99/2.28 thf(decl_70, type, i: a).
% 14.99/2.28 thf(decl_72, type, sa: set_a).
% 14.99/2.28 thf(decl_73, type, y: a > b).
% 14.99/2.28 thf(decl_191, type, esk118_0: a > b).
% 14.99/2.28 thf(decl_192, type, esk119_2: (a > b) > real > a > b).
% 14.99/2.28 thf(decl_198, type, esk123_0: a > b).
% 14.99/2.28 thf(decl_203, type, esk128_0: a > real).
% 14.99/2.28 thf(decl_266, type, esk168_0: a > b).
% 14.99/2.28 thf(decl_340, type, esk114_0: a).
% 14.99/2.28 thf(conj_0, conjecture, ((f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (aa @ X2) @ (y @ X2))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (times_times_real @ (aa @ X2) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (y @ X2))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', conj_0)).
% 14.99/2.28 thf(fact_147_field__class_Ofield__divide__inverse, axiom, ((divide_divide_real)=(^[X222:real, X223:real]:(times_times_real @ X222 @ (inverse_inverse_real @ X223)))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_147_field__class_Ofield__divide__inverse)).
% 14.99/2.28 thf(fact_17__092_060open_062sum_Aa_As_A_061_A1_A_N_Aa_Ai_092_060close_062, axiom, ((groups1862963056a_real @ aa @ sa)=(minus_minus_real @ one_one_real @ (aa @ i))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_17__092_060open_062sum_Aa_As_A_061_A1_A_N_Aa_Ai_092_060close_062)).
% 14.99/2.28 thf(fact_5__092_060open_062f_A_I_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_A_061_Af_A_I_I_I1_A_N_Aa_Ai_J_A_K_Ainverse_A_I1_A_N_Aa_Ai_J_J_A_K_092_060_094sub_062R_A_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_092_060close_062, axiom, ((f @ (plus_plus_b @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (aa @ X2) @ (y @ X2))) @ sa) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (aa @ X2) @ (y @ X2))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_5__092_060open_062f_A_I_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_A_061_Af_A_I_I_I1_A_N_Aa_Ai_J_A_K_Ainverse_A_I1_A_N_Aa_Ai_J_J_A_K_092_060_094sub_062R_A_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_092_060close_062)).
% 14.99/2.28 thf(fact_7__092_060open_062f_A_I_092_060Sum_062j_092_060in_062insert_Ai_As_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_061_Af_A_I_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_092_060close_062, axiom, ((f @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (aa @ X2) @ (y @ X2))) @ (insert_a @ i @ sa)))=(f @ (plus_plus_b @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (aa @ X2) @ (y @ X2))) @ sa) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_7__092_060open_062f_A_I_092_060Sum_062j_092_060in_062insert_Ai_As_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_061_Af_A_I_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_092_060close_062)).
% 14.99/2.28 thf(fact_297_add_Ocommute, axiom, ((plus_plus_b)=(^[X582:b, X583:b]:(plus_plus_b @ X583 @ X582))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_297_add_Ocommute)).
% 14.99/2.28 thf(fact_47_scale__sum__right, axiom, ![X53:real, X54:a > b, X55:set_a]:(((real_V1035702896aleR_b @ X53 @ (groups1199149371um_a_b @ X54 @ X55))=(groups1199149371um_a_b @ (^[X1:a]:(real_V1035702896aleR_b @ X53 @ (X54 @ X1))) @ X55))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_47_scale__sum__right)).
% 14.99/2.28 thf(fact_348_lambda__one, axiom, ((^[X690:real]:(X690))=(times_times_real @ one_one_real)), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_348_lambda__one)).
% 14.99/2.28 thf(fact_102_times__divide__eq__right, axiom, ![X145:real, X146:real, X147:real]:(((times_times_real @ X145 @ (divide_divide_real @ X146 @ X147))=(divide_divide_real @ (times_times_real @ X145 @ X146) @ X147))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_102_times__divide__eq__right)).
% 14.99/2.28 thf(fact_99_times__divide__eq__left, axiom, ![X136:real, X137:real, X138:real]:(((times_times_real @ (divide_divide_real @ X136 @ X137) @ X138)=(divide_divide_real @ (times_times_real @ X136 @ X138) @ X137))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_99_times__divide__eq__left)).
% 14.99/2.28 thf(fact_73__092_060open_062sum_Aa_As_A_P_A_I1_A_N_Aa_Ai_J_A_061_A1_092_060close_062, axiom, ((divide_divide_real @ (groups1862963056a_real @ aa @ sa) @ (minus_minus_real @ one_one_real @ (aa @ i)))=(one_one_real)), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_73__092_060open_062sum_Aa_As_A_P_A_I1_A_N_Aa_Ai_J_A_061_A1_092_060close_062)).
% 14.99/2.28 thf(fact_13_scaleR__scaleR, axiom, ![X9:real, X10:real, X11:b]:(((real_V1035702896aleR_b @ X9 @ (real_V1035702896aleR_b @ X10 @ X11))=(real_V1035702896aleR_b @ (times_times_real @ X9 @ X10) @ X11))), file('/export/starexec/sandbox2/tmp/tmp.pYAsRfaiFZ/E---3.1_3844260.p', fact_13_scaleR__scaleR)).
% 14.99/2.28 thf(c_0_12, negated_conjecture, ~(((f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (aa @ X2) @ (y @ X2))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (groups1199149371um_a_b @ (^[X2:a]:(real_V1035702896aleR_b @ (times_times_real @ (aa @ X2) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (y @ X2))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i)))))), inference(assume_negation,[status(cth)],[conj_0])).
% 14.99/2.28 thf(c_0_13, plain, ![X3004:a]:(((esk128_0 @ X3004)=(divide_divide_real @ (aa @ X3004) @ (minus_minus_real @ one_one_real @ (aa @ i))))), inference(variable_rename,[status(thm)],[])).
% 14.99/2.28 thf(c_0_14, negated_conjecture, ((f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (aa @ Z0) @ (y @ Z0))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))!=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (times_times_real @ (aa @ Z0) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (y @ Z0))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_12])])).
% 14.99/2.28 thf(c_0_15, plain, ![X3221:a]:(((esk168_0 @ X3221)=(real_V1035702896aleR_b @ (times_times_real @ (aa @ X3221) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (y @ X3221)))), inference(variable_rename,[status(thm)],[])).
% 14.99/2.28 thf(c_0_16, plain, ![X1731:real, X1732:real]:(((divide_divide_real @ X1731 @ X1732)=(times_times_real @ X1731 @ (inverse_inverse_real @ X1732)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_147_field__class_Ofield__divide__inverse])])).
% 14.99/2.28 thf(c_0_17, plain, ![X2989:a]:(((esk123_0 @ X2989)=(real_V1035702896aleR_b @ (divide_divide_real @ (aa @ X2989) @ (minus_minus_real @ one_one_real @ (aa @ i))) @ (y @ X2989)))), inference(variable_rename,[status(thm)],[])).
% 14.99/2.28 thf(c_0_18, plain, ![X1:a]:(((esk128_0 @ X1)=(divide_divide_real @ (aa @ X1) @ (minus_minus_real @ one_one_real @ (aa @ i))))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 14.99/2.28 thf(c_0_19, plain, ((groups1862963056a_real @ aa @ sa)=(minus_minus_real @ one_one_real @ (aa @ i))), inference(split_conjunct,[status(thm)],[fact_17__092_060open_062sum_Aa_As_A_061_A1_A_N_Aa_Ai_092_060close_062])).
% 14.99/2.28 thf(c_0_20, negated_conjecture, ((f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (aa @ Z0) @ (y @ Z0))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))!=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (times_times_real @ (aa @ Z0) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (y @ Z0))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(fof_nnf,[status(thm)],[c_0_14])).
% 14.99/2.28 thf(c_0_21, plain, ![X2970:a]:(((esk168_0 @ X2970)=(real_V1035702896aleR_b @ (times_times_real @ (aa @ X2970) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (y @ X2970)))), introduced(definition)).
% 14.99/2.28 thf(c_0_22, plain, ![X2825:a]:(((esk118_0 @ X2825)=(real_V1035702896aleR_b @ (aa @ X2825) @ (y @ X2825)))), introduced(definition)).
% 14.99/2.28 thf(c_0_23, plain, ((f @ (plus_plus_b @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (aa @ Z0) @ (y @ Z0))) @ sa) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (aa @ Z0) @ (y @ Z0))) @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(fof_simplification,[status(thm)],[fact_5__092_060open_062f_A_I_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_A_061_Af_A_I_I_I1_A_N_Aa_Ai_J_A_K_Ainverse_A_I1_A_N_Aa_Ai_J_J_A_K_092_060_094sub_062R_A_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_092_060close_062])).
% 14.99/2.28 thf(c_0_24, plain, ((f @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (aa @ Z0) @ (y @ Z0))) @ (insert_a @ i @ sa)))=(f @ (plus_plus_b @ (groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ (aa @ Z0) @ (y @ Z0))) @ sa) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(fof_simplification,[status(thm)],[fact_7__092_060open_062f_A_I_092_060Sum_062j_092_060in_062insert_Ai_As_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_061_Af_A_I_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_L_Aa_Ai_A_K_092_060_094sub_062R_Ay_Ai_J_092_060close_062])).
% 14.99/2.28 thf(c_0_25, plain, ![X1744:b, X1745:b]:(((plus_plus_b @ X1744 @ X1745)=(plus_plus_b @ X1745 @ X1744))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_297_add_Ocommute])])).
% 14.99/2.28 thf(c_0_26, plain, ![X53:real, X54:a > b, X55:set_a]:(((real_V1035702896aleR_b @ X53 @ (groups1199149371um_a_b @ X54 @ X55))=(groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ X53 @ (X54 @ Z0))) @ X55))), inference(fof_simplification,[status(thm)],[fact_47_scale__sum__right])).
% 14.99/2.28 thf(c_0_27, plain, ![X1:a]:(((esk168_0 @ X1)=(real_V1035702896aleR_b @ (times_times_real @ (aa @ X1) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (y @ X1)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 14.99/2.28 thf(c_0_28, plain, ![X2091:real, X2092:real]:(((divide_divide_real @ X2091 @ X2092)=(times_times_real @ X2091 @ (inverse_inverse_real @ X2092)))), inference(variable_rename,[status(thm)],[c_0_16])).
% 14.99/2.28 thf(c_0_29, plain, ![X1:a]:(((esk123_0 @ X1)=(real_V1035702896aleR_b @ (divide_divide_real @ (aa @ X1) @ (minus_minus_real @ one_one_real @ (aa @ i))) @ (y @ X1)))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 14.99/2.28 thf(c_0_30, plain, ![X1:a]:(((divide_divide_real @ (aa @ X1) @ (groups1862963056a_real @ aa @ sa))=(esk128_0 @ X1))), inference(rw,[status(thm)],[c_0_18, c_0_19])).
% 14.99/2.28 thf(c_0_31, plain, ![X1748:real]:(((X1748)=(times_times_real @ one_one_real @ X1748))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_348_lambda__one])])).
% 14.99/2.28 thf(c_0_32, negated_conjecture, ((f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ esk118_0 @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))!=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (groups1199149371um_a_b @ esk168_0 @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_20]), c_0_21]), c_0_22])).
% 14.99/2.28 thf(c_0_33, plain, ((f @ (plus_plus_b @ (groups1199149371um_a_b @ esk118_0 @ sa) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (minus_minus_real @ one_one_real @ (aa @ i)) @ (inverse_inverse_real @ (minus_minus_real @ one_one_real @ (aa @ i)))) @ (groups1199149371um_a_b @ esk118_0 @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23]), c_0_22]), c_0_22])).
% 14.99/2.28 thf(c_0_34, plain, ((f @ (groups1199149371um_a_b @ esk118_0 @ (insert_a @ i @ sa)))=(f @ (plus_plus_b @ (groups1199149371um_a_b @ esk118_0 @ sa) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_24]), c_0_22]), c_0_22])).
% 14.99/2.28 thf(c_0_35, plain, ![X2972:a]:(((esk118_0 @ X2972)=(real_V1035702896aleR_b @ (aa @ X2972) @ (y @ X2972)))), inference(variable_rename,[status(thm)],[])).
% 14.99/2.28 thf(c_0_36, plain, ![X2649:b, X2650:b]:(((plus_plus_b @ X2649 @ X2650)=(plus_plus_b @ X2650 @ X2649))), inference(variable_rename,[status(thm)],[c_0_25])).
% 14.99/2.28 thf(c_0_37, plain, ![X1815:real, X1816:a > b, X1817:set_a]:(((real_V1035702896aleR_b @ X1815 @ (groups1199149371um_a_b @ X1816 @ X1817))=(groups1199149371um_a_b @ (^[Z0:a]:(real_V1035702896aleR_b @ X1815 @ (X1816 @ Z0))) @ X1817))), inference(variable_rename,[status(thm)],[c_0_26])).
% 14.99/2.28 thf(c_0_38, plain, ![X2832:a, X3:real, X54:a > b]:(((esk119_2 @ X54 @ X3 @ X2832)=(real_V1035702896aleR_b @ X3 @ (X54 @ X2832)))), introduced(definition)).
% 14.99/2.28 thf(c_0_39, plain, ![X1:a]:(((real_V1035702896aleR_b @ (times_times_real @ (aa @ X1) @ (inverse_inverse_real @ (groups1862963056a_real @ aa @ sa))) @ (y @ X1))=(esk168_0 @ X1))), inference(rw,[status(thm)],[c_0_27, c_0_19])).
% 14.99/2.28 thf(c_0_40, plain, ![X3:real, X5:real]:(((divide_divide_real @ X3 @ X5)=(times_times_real @ X3 @ (inverse_inverse_real @ X5)))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 14.99/2.28 thf(c_0_41, plain, ![X1:a]:(((real_V1035702896aleR_b @ (esk128_0 @ X1) @ (y @ X1))=(esk123_0 @ X1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_19]), c_0_30])).
% 14.99/2.28 thf(c_0_42, plain, ![X1971:real, X1972:real, X1973:real]:(((times_times_real @ X1971 @ (divide_divide_real @ X1972 @ X1973))=(divide_divide_real @ (times_times_real @ X1971 @ X1972) @ X1973))), inference(variable_rename,[status(thm)],[fact_102_times__divide__eq__right])).
% 14.99/2.28 thf(c_0_43, plain, ![X1962:real, X1963:real, X1964:real]:(((times_times_real @ (divide_divide_real @ X1962 @ X1963) @ X1964)=(divide_divide_real @ (times_times_real @ X1962 @ X1964) @ X1963))), inference(variable_rename,[status(thm)],[fact_99_times__divide__eq__left])).
% 14.99/2.28 thf(c_0_44, plain, ((divide_divide_real @ (groups1862963056a_real @ aa @ sa) @ (minus_minus_real @ one_one_real @ (aa @ i)))=(one_one_real)), inference(split_conjunct,[status(thm)],[fact_73__092_060open_062sum_Aa_As_A_P_A_I1_A_N_Aa_Ai_J_A_061_A1_092_060close_062])).
% 14.99/2.28 thf(c_0_45, plain, ![X2802:real]:(((X2802)=(times_times_real @ one_one_real @ X2802))), inference(variable_rename,[status(thm)],[c_0_31])).
% 14.99/2.28 thf(c_0_46, negated_conjecture, ((f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (groups1862963056a_real @ aa @ sa) @ (inverse_inverse_real @ (groups1862963056a_real @ aa @ sa))) @ (groups1199149371um_a_b @ esk118_0 @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))!=(f @ (plus_plus_b @ (real_V1035702896aleR_b @ (groups1862963056a_real @ aa @ sa) @ (groups1199149371um_a_b @ esk168_0 @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_19]), c_0_19]), c_0_19])).
% 14.99/2.28 thf(c_0_47, plain, ((f @ (plus_plus_b @ (real_V1035702896aleR_b @ (times_times_real @ (groups1862963056a_real @ aa @ sa) @ (inverse_inverse_real @ (groups1862963056a_real @ aa @ sa))) @ (groups1199149371um_a_b @ esk118_0 @ sa)) @ (real_V1035702896aleR_b @ (aa @ i) @ (y @ i))))=(f @ (groups1199149371um_a_b @ esk118_0 @ (insert_a @ i @ sa)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_19]), c_0_19]), c_0_34])).
% 14.99/2.28 thf(c_0_48, plain, ![X1:a]:(((esk118_0 @ X1)=(real_V1035702896aleR_b @ (aa @ X1) @ (y @ X1)))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 14.99/2.28 thf(c_0_49, plain, ![X6:b, X4:b]:(((plus_plus_b @ X4 @ X6)=(plus_plus_b @ X6 @ X4))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 14.99/2.28 thf(c_0_50, plain, ![X3:real, X54:a > b, X55:set_a]:(((real_V1035702896aleR_b @ X3 @ (groups1199149371um_a_b @ X54 @ X55))=(groups1199149371um_a_b @ (esk119_2 @ X54 @ X3) @ X55))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_37]), c_0_38])).
% 14.99/2.28 thf(c_0_51, plain, ![X1:a]:(((esk168_0 @ X1)=(esk123_0 @ X1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40]), c_0_30]), c_0_41])).
% 14.99/2.28 thf(c_0_52, plain, ![X1759:real, X1760:real, X1761:b]:(((real_V1035702896aleR_b @ X1759 @ (real_V1035702896aleR_b @ X1760 @ X1761))=(real_V1035702896aleR_b @ (times_times_real @ X1759 @ X1760) @ X1761))), inference(variable_rename,[status(thm)],[fact_13_scaleR__scaleR])).
% 14.99/2.28 thf(c_0_53, plain, ![X3:real, X5:real, X7:real]:(((times_times_real @ X3 @ (divide_divide_real @ X5 @ X7))=(divide_divide_real @ (times_times_real @ X3 @ X5) @ X7))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 14.99/2.28 thf(c_0_54, plain, ![X3:real, X7:real, X5:real]:(((times_times_real @ (divide_divide_real @ X3 @ X5) @ X7)=(divide_divide_real @ (times_times_real @ X3 @ X7) @ X5))), inference(split_conjunct,[status(thm)],[c_0_43])).
% 14.99/2.28 thf(c_0_55, plain, ((divide_divide_real @ (groups1862963056a_real @ aa @ sa) @ (groups1862963056a_real @ aa @ sa))=(one_one_real)), inference(rw,[status(thm)],[c_0_44, c_0_19])).
% 14.99/2.28 thf(c_0_56, plain, ![X3:real]:(((X3)=(times_times_real @ one_one_real @ X3))), inference(split_conjunct,[status(thm)],[c_0_45])).
% 14.99/2.28 thf(c_0_57, negated_conjecture, ((f @ (plus_plus_b @ (esk118_0 @ i) @ (real_V1035702896aleR_b @ (groups1862963056a_real @ aa @ sa) @ (groups1199149371um_a_b @ esk168_0 @ sa))))!=(f @ (groups1199149371um_a_b @ esk118_0 @ (insert_a @ i @ sa)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47]), c_0_48]), c_0_49])).
% 14.99/2.28 thf(c_0_58, plain, ![X54:a > b, X3:real]:((((f @ (plus_plus_b @ (esk118_0 @ i) @ (real_V1035702896aleR_b @ X3 @ (groups1199149371um_a_b @ X54 @ sa))))=(f @ (groups1199149371um_a_b @ esk118_0 @ (insert_a @ i @ sa))))|((esk119_2 @ X54 @ X3)!=(esk118_0)))), inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(rw,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_34, c_0_50]), c_0_48])]), c_0_49])).
% 14.99/2.28 thf(c_0_59, plain, ((esk168_0)=(esk123_0)), inference(pos_ext,[status(thm)],[c_0_51])).
% 14.99/2.28 thf(c_0_60, plain, ![X2973:a, X2974:real, X2975:a > b]:(((esk119_2 @ X2975 @ X2974 @ X2973)=(real_V1035702896aleR_b @ X2974 @ (X2975 @ X2973)))), inference(variable_rename,[status(thm)],[])).
% 14.99/2.28 thf(c_0_61, plain, ![X3:real, X5:real, X4:b]:(((real_V1035702896aleR_b @ X3 @ (real_V1035702896aleR_b @ X5 @ X4))=(real_V1035702896aleR_b @ (times_times_real @ X3 @ X5) @ X4))), inference(split_conjunct,[status(thm)],[c_0_52])).
% 14.99/2.28 thf(c_0_62, plain, ![X3:real, X1:a]:(((divide_divide_real @ (times_times_real @ X3 @ (aa @ X1)) @ (groups1862963056a_real @ aa @ sa))=(times_times_real @ X3 @ (esk128_0 @ X1)))), inference(spm,[status(thm)],[c_0_53, c_0_30])).
% 14.99/2.28 thf(c_0_63, plain, ![X3:real]:(((divide_divide_real @ (times_times_real @ (groups1862963056a_real @ aa @ sa) @ X3) @ (groups1862963056a_real @ aa @ sa))=(X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_55]), c_0_56])).
% 14.99/2.28 thf(c_0_64, negated_conjecture, ((esk119_2 @ esk123_0 @ (groups1862963056a_real @ aa @ sa))!=(esk118_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_58]), c_0_59])).
% 14.99/2.28 thf(c_0_65, plain, ![X54:a > b, X3:real, X1:a]:(((esk119_2 @ X54 @ X3 @ X1)=(real_V1035702896aleR_b @ X3 @ (X54 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_60])).
% 14.99/2.28 thf(c_0_66, plain, ![X3:real, X1:a]:(((real_V1035702896aleR_b @ (times_times_real @ X3 @ (esk128_0 @ X1)) @ (y @ X1))=(real_V1035702896aleR_b @ X3 @ (esk123_0 @ X1)))), inference(spm,[status(thm)],[c_0_61, c_0_41])).
% 14.99/2.28 thf(c_0_67, plain, ![X1:a]:(((times_times_real @ (groups1862963056a_real @ aa @ sa) @ (esk128_0 @ X1))=(aa @ X1))), inference(spm,[status(thm)],[c_0_62, c_0_63])).
% 14.99/2.28 thf(c_0_68, negated_conjecture, ((real_V1035702896aleR_b @ (groups1862963056a_real @ aa @ sa) @ (esk123_0 @ esk114_0))!=(esk118_0 @ esk114_0)), inference(rw,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_64]), c_0_65])).
% 14.99/2.28 thf(c_0_69, plain, ![X1:a]:(((real_V1035702896aleR_b @ (groups1862963056a_real @ aa @ sa) @ (esk123_0 @ X1))=(esk118_0 @ X1))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_67]), c_0_48])).
% 14.99/2.28 thf(c_0_70, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69])]), ['proof']).
% 14.99/2.28 % SZS output end CNFRefutation
% 14.99/2.28 % Parsed axioms : 418
% 14.99/2.28 % Removed by relevancy pruning/SinE : 0
% 14.99/2.28 % Initial clauses : 956
% 14.99/2.28 % Removed in clause preprocessing : 87
% 14.99/2.28 % Initial clauses in saturation : 869
% 14.99/2.28 % Processed clauses : 4520
% 14.99/2.28 % ...of these trivial : 165
% 14.99/2.28 % ...subsumed : 2499
% 14.99/2.28 % ...remaining for further processing : 1856
% 14.99/2.28 % Other redundant clauses eliminated : 1354
% 14.99/2.28 % Clauses deleted for lack of memory : 0
% 14.99/2.28 % Backward-subsumed : 266
% 14.99/2.28 % Backward-rewritten : 105
% 14.99/2.28 % Generated clauses : 39638
% 14.99/2.28 % ...of the previous two non-redundant : 35407
% 14.99/2.28 % ...aggressively subsumed : 0
% 14.99/2.28 % Contextual simplify-reflections : 6
% 14.99/2.28 % Paramodulations : 36461
% 14.99/2.28 % Factorizations : 54
% 14.99/2.28 % NegExts : 137
% 14.99/2.28 % Equation resolutions : 1386
% 14.99/2.28 % Disequality decompositions : 0
% 14.99/2.28 % Total rewrite steps : 13543
% 14.99/2.28 % ...of those cached : 10278
% 14.99/2.28 % Propositional unsat checks : 0
% 14.99/2.28 % Propositional check models : 0
% 14.99/2.28 % Propositional check unsatisfiable : 0
% 14.99/2.28 % Propositional clauses : 0
% 14.99/2.28 % Propositional clauses after purity: 0
% 14.99/2.28 % Propositional unsat core size : 0
% 14.99/2.28 % Propositional preprocessing time : 0.000
% 14.99/2.28 % Propositional encoding time : 0.000
% 14.99/2.28 % Propositional solver time : 0.000
% 14.99/2.28 % Success case prop preproc time : 0.000
% 14.99/2.28 % Success case prop encoding time : 0.000
% 14.99/2.28 % Success case prop solver time : 0.000
% 14.99/2.28 % Current number of processed clauses : 1413
% 14.99/2.28 % Positive orientable unit clauses : 259
% 14.99/2.28 % Positive unorientable unit clauses: 66
% 14.99/2.28 % Negative unit clauses : 161
% 14.99/2.28 % Non-unit-clauses : 927
% 14.99/2.28 % Current number of unprocessed clauses: 30990
% 14.99/2.28 % ...number of literals in the above : 101680
% 14.99/2.28 % Current number of archived formulas : 0
% 14.99/2.28 % Current number of archived clauses : 375
% 14.99/2.28 % Clause-clause subsumption calls (NU) : 222252
% 14.99/2.28 % Rec. Clause-clause subsumption calls : 70967
% 14.99/2.28 % Non-unit clause-clause subsumptions : 1039
% 14.99/2.28 % Unit Clause-clause subsumption calls : 79416
% 14.99/2.28 % Rewrite failures with RHS unbound : 2695
% 14.99/2.28 % BW rewrite match attempts : 26127
% 14.99/2.28 % BW rewrite match successes : 1544
% 14.99/2.28 % Condensation attempts : 4520
% 14.99/2.28 % Condensation successes : 64
% 14.99/2.28 % Termbank termtop insertions : 1798213
% 14.99/2.28 % Search garbage collected termcells : 16471
% 14.99/2.28
% 14.99/2.28 % -------------------------------------------------
% 14.99/2.28 % User time : 1.890 s
% 14.99/2.28 % System time : 0.060 s
% 14.99/2.28 % Total time : 1.950 s
% 14.99/2.28 % Maximum resident set size: 8752 pages
% 14.99/2.28
% 14.99/2.28 % -------------------------------------------------
% 14.99/2.28 % User time : 9.109 s
% 14.99/2.28 % System time : 0.277 s
% 14.99/2.28 % Total time : 9.386 s
% 14.99/2.28 % Maximum resident set size: 5888 pages
% 14.99/2.28 % E exiting
%------------------------------------------------------------------------------