%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP109^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 : 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:23 AM UTC 2026
% Result : Theorem 15.02s 2.28s
% Output : CNFRefutation 15.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP109^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n013.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 19:54:06 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.22/0.27 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.Uq2Y79S69B/E---3.1_2581232.p
% 15.02/2.28 % Version: 3.5.1-ho
% 15.02/2.28 % Preprocessing class: HSLSSMSSSSLNSSA.
% 15.02/2.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 15.02/2.28 % Starting sh3 with 1500s (5) cores
% 15.02/2.28 % Starting new_bool_9 with 300s (1) cores
% 15.02/2.28 % Starting ehoh_best8_lambda with 300s (1) cores
% 15.02/2.28 % Starting sh4l with 300s (1) cores
% 15.02/2.28 % sh3 with pid 2581245 completed with status 0
% 15.02/2.28 % Result found by sh3
% 15.02/2.28 % Preprocessing class: HSLSSMSSSSLNSSA.
% 15.02/2.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 15.02/2.28 % Starting sh3 with 1500s (5) cores
% 15.02/2.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 15.02/2.28 % No SInE strategy applied
% 15.02/2.28 % Search class: HGHSM-FSLM32-DSSFFSBN
% 15.02/2.28 % partial match(1): HGHSM-FSLM32-DHSFFSBN
% 15.02/2.28 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 15.02/2.28 % Starting SubtermCWHack with 136s (1) cores
% 15.02/2.28 % Starting sh3 with 151s (1) cores
% 15.02/2.28 % Starting sh4l with 214s (1) cores
% 15.02/2.28 % Starting pre_casc_4 with 204s (1) cores
% 15.02/2.28 % Starting lpo5_fix with 136s (1) cores
% 15.02/2.28 % sh4l with pid 2581254 completed with status 0
% 15.02/2.28 % Result found by sh4l
% 15.02/2.28 % Preprocessing class: HSLSSMSSSSLNSSA.
% 15.02/2.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 15.02/2.28 % Starting sh3 with 1500s (5) cores
% 15.02/2.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 15.02/2.28 % No SInE strategy applied
% 15.02/2.28 % Search class: HGHSM-FSLM32-DSSFFSBN
% 15.02/2.28 % partial match(1): HGHSM-FSLM32-DHSFFSBN
% 15.02/2.28 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 15.02/2.28 % Starting SubtermCWHack with 136s (1) cores
% 15.02/2.28 % Starting sh3 with 151s (1) cores
% 15.02/2.28 % Starting sh4l with 214s (1) cores
% 15.02/2.28 % Preprocessing time : 0.028 s
% 15.02/2.28
% 15.02/2.28 % Proof found!
% 15.02/2.28 % SZS status Theorem
% 15.02/2.28 % SZS output start CNFRefutation
% 15.02/2.28 thf(decl_sort1, type, real: $tType).
% 15.02/2.28 thf(decl_sort2, type, set_a: $tType).
% 15.02/2.28 thf(decl_sort3, type, a: $tType).
% 15.02/2.28 thf(decl_sort4, type, b: $tType).
% 15.02/2.28 thf(decl_sort5, type, extended_ereal: $tType).
% 15.02/2.28 thf(decl_24, type, inverse_inverse_real: real > real).
% 15.02/2.28 thf(decl_31, type, minus_minus_real: real > real > real).
% 15.02/2.28 thf(decl_35, type, one_one_real: real).
% 15.02/2.28 thf(decl_39, type, plus_plus_b: b > b > b).
% 15.02/2.28 thf(decl_40, type, times_times_real: real > real > real).
% 15.02/2.28 thf(decl_43, type, groups1862963056a_real: (a > real) > set_a > real).
% 15.02/2.28 thf(decl_45, type, groups1199149371um_a_b: (a > b) > set_a > b).
% 15.02/2.28 thf(decl_57, type, real_V1035702896aleR_b: real > b > b).
% 15.02/2.28 thf(decl_58, type, divide_divide_real: real > real > real).
% 15.02/2.28 thf(decl_62, type, insert_a: a > set_a > set_a).
% 15.02/2.28 thf(decl_68, type, aa: a > real).
% 15.02/2.28 thf(decl_69, type, f: b > extended_ereal).
% 15.02/2.28 thf(decl_70, type, i: a).
% 15.02/2.28 thf(decl_72, type, sa: set_a).
% 15.02/2.28 thf(decl_73, type, y: a > b).
% 15.02/2.28 thf(decl_191, type, esk118_0: a > b).
% 15.02/2.28 thf(decl_192, type, esk119_2: (a > b) > real > a > b).
% 15.02/2.28 thf(decl_198, type, esk123_0: a > b).
% 15.02/2.28 thf(decl_203, type, esk128_0: a > real).
% 15.02/2.28 thf(decl_266, type, esk168_0: a > b).
% 15.02/2.28 thf(decl_337, type, esk112_0: a).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', conj_0)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_147_field__class_Ofield__divide__inverse)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_17__092_060open_062sum_Aa_As_A_061_A1_A_N_Aa_Ai_092_060close_062)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.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)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.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)).
% 15.02/2.28 thf(fact_297_add_Ocommute, axiom, ((plus_plus_b)=(^[X582:b, X583:b]:(plus_plus_b @ X583 @ X582))), file('/export/starexec/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_297_add_Ocommute)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_47_scale__sum__right)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_102_times__divide__eq__right)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_73__092_060open_062sum_Aa_As_A_P_A_I1_A_N_Aa_Ai_J_A_061_A1_092_060close_062)).
% 15.02/2.28 thf(fact_277_mult_Oright__neutral, axiom, ![X551:real]:(((times_times_real @ X551 @ one_one_real)=(X551))), file('/export/starexec/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_277_mult_Oright__neutral)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_99_times__divide__eq__left)).
% 15.02/2.28 thf(fact_288_mult_Ocommute, axiom, ((times_times_real)=(^[X566:real, X223:real]:(times_times_real @ X223 @ X566))), file('/export/starexec/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_288_mult_Ocommute)).
% 15.02/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/sandbox/tmp/tmp.Uq2Y79S69B/E---3.1_2581232.p', fact_13_scaleR__scaleR)).
% 15.02/2.28 thf(c_0_13, 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])).
% 15.02/2.28 thf(c_0_14, plain, ![X3004:a]:(((esk128_0 @ X3004)=(divide_divide_real @ (aa @ X3004) @ (minus_minus_real @ one_one_real @ (aa @ i))))), inference(variable_rename,[status(thm)],[])).
% 15.02/2.28 thf(c_0_15, 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_13])])).
% 15.02/2.28 thf(c_0_16, 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)],[])).
% 15.02/2.28 thf(c_0_17, 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])])).
% 15.02/2.28 thf(c_0_18, 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)],[])).
% 15.02/2.28 thf(c_0_19, 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_14])).
% 15.02/2.28 thf(c_0_20, 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])).
% 15.02/2.28 thf(c_0_21, 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_15])).
% 15.02/2.28 thf(c_0_22, 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)).
% 15.02/2.28 thf(c_0_23, plain, ![X2825:a]:(((esk118_0 @ X2825)=(real_V1035702896aleR_b @ (aa @ X2825) @ (y @ X2825)))), introduced(definition)).
% 15.02/2.28 thf(c_0_24, 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])).
% 15.02/2.28 thf(c_0_25, 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])).
% 15.02/2.28 thf(c_0_26, 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])])).
% 15.02/2.28 thf(c_0_27, 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])).
% 15.02/2.28 thf(c_0_28, 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_16])).
% 15.02/2.28 thf(c_0_29, 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_17])).
% 15.02/2.28 thf(c_0_30, 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_18])).
% 15.02/2.28 thf(c_0_31, plain, ![X1:a]:(((divide_divide_real @ (aa @ X1) @ (groups1862963056a_real @ aa @ sa))=(esk128_0 @ X1))), inference(rw,[status(thm)],[c_0_19, c_0_20])).
% 15.02/2.28 thf(c_0_32, 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])).
% 15.02/2.28 thf(c_0_33, 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])).
% 15.02/2.28 thf(c_0_34, plain, ![X2598:real]:(((times_times_real @ X2598 @ one_one_real)=(X2598))), inference(variable_rename,[status(thm)],[fact_277_mult_Oright__neutral])).
% 15.02/2.28 thf(c_0_35, 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])).
% 15.02/2.28 thf(c_0_36, 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_21]), c_0_22]), c_0_23])).
% 15.02/2.28 thf(c_0_37, 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_24]), c_0_23]), c_0_23])).
% 15.02/2.28 thf(c_0_38, 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_25]), c_0_23]), c_0_23])).
% 15.02/2.28 thf(c_0_39, plain, ![X2972:a]:(((esk118_0 @ X2972)=(real_V1035702896aleR_b @ (aa @ X2972) @ (y @ X2972)))), inference(variable_rename,[status(thm)],[])).
% 15.02/2.28 thf(c_0_40, plain, ![X2649:b, X2650:b]:(((plus_plus_b @ X2649 @ X2650)=(plus_plus_b @ X2650 @ X2649))), inference(variable_rename,[status(thm)],[c_0_26])).
% 15.02/2.28 thf(c_0_41, 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_27])).
% 15.02/2.28 thf(c_0_42, plain, ![X2832:a, X3:real, X54:a > b]:(((esk119_2 @ X54 @ X3 @ X2832)=(real_V1035702896aleR_b @ X3 @ (X54 @ X2832)))), introduced(definition)).
% 15.02/2.28 thf(c_0_43, 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_28, c_0_20])).
% 15.02/2.28 thf(c_0_44, 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_29])).
% 15.02/2.28 thf(c_0_45, plain, ![X1:a]:(((real_V1035702896aleR_b @ (esk128_0 @ X1) @ (y @ X1))=(esk123_0 @ X1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_20]), c_0_31])).
% 15.02/2.28 thf(c_0_46, plain, ![X1742:real, X1743:real]:(((times_times_real @ X1742 @ X1743)=(times_times_real @ X1743 @ X1742))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_288_mult_Ocommute])])).
% 15.02/2.28 thf(c_0_47, 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_32])).
% 15.02/2.28 thf(c_0_48, plain, ((divide_divide_real @ (groups1862963056a_real @ aa @ sa) @ (groups1862963056a_real @ aa @ sa))=(one_one_real)), inference(rw,[status(thm)],[c_0_33, c_0_20])).
% 15.02/2.28 thf(c_0_49, plain, ![X3:real]:(((times_times_real @ X3 @ one_one_real)=(X3))), inference(split_conjunct,[status(thm)],[c_0_34])).
% 15.02/2.28 thf(c_0_50, 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_35])).
% 15.02/2.28 thf(c_0_51, 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_36, c_0_20]), c_0_20]), c_0_20])).
% 15.02/2.28 thf(c_0_52, 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_37, c_0_20]), c_0_20]), c_0_38])).
% 15.02/2.28 thf(c_0_53, plain, ![X1:a]:(((esk118_0 @ X1)=(real_V1035702896aleR_b @ (aa @ X1) @ (y @ X1)))), inference(split_conjunct,[status(thm)],[c_0_39])).
% 15.02/2.28 thf(c_0_54, plain, ![X6:b, X4:b]:(((plus_plus_b @ X4 @ X6)=(plus_plus_b @ X6 @ X4))), inference(split_conjunct,[status(thm)],[c_0_40])).
% 15.02/2.28 thf(c_0_55, 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_41]), c_0_42])).
% 15.02/2.28 thf(c_0_56, plain, ![X1:a]:(((esk168_0 @ X1)=(esk123_0 @ X1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44]), c_0_31]), c_0_45])).
% 15.02/2.28 thf(c_0_57, 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])).
% 15.02/2.28 thf(c_0_58, plain, ![X2623:real, X2624:real]:(((times_times_real @ X2623 @ X2624)=(times_times_real @ X2624 @ X2623))), inference(variable_rename,[status(thm)],[c_0_46])).
% 15.02/2.28 thf(c_0_59, plain, ![X3:real]:(((divide_divide_real @ (times_times_real @ X3 @ (groups1862963056a_real @ aa @ sa)) @ (groups1862963056a_real @ aa @ sa))=(X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_49])).
% 15.02/2.28 thf(c_0_60, plain, ![X1:a, X3:real]:(((divide_divide_real @ (times_times_real @ (aa @ X1) @ X3) @ (groups1862963056a_real @ aa @ sa))=(times_times_real @ (esk128_0 @ X1) @ X3))), inference(spm,[status(thm)],[c_0_50, c_0_31])).
% 15.02/2.28 thf(c_0_61, 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_51, c_0_52]), c_0_53]), c_0_54])).
% 15.02/2.28 thf(c_0_62, 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_38, c_0_55]), c_0_53])]), c_0_54])).
% 15.02/2.28 thf(c_0_63, plain, ((esk168_0)=(esk123_0)), inference(pos_ext,[status(thm)],[c_0_56])).
% 15.02/2.28 thf(c_0_64, plain, ![X2973:a, X2974:real, X2975:a > b]:(((esk119_2 @ X2975 @ X2974 @ X2973)=(real_V1035702896aleR_b @ X2974 @ (X2975 @ X2973)))), inference(variable_rename,[status(thm)],[])).
% 15.02/2.28 thf(c_0_65, 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_57])).
% 15.02/2.28 thf(c_0_66, plain, ![X5:real, X3:real]:(((times_times_real @ X3 @ X5)=(times_times_real @ X5 @ X3))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 15.02/2.28 thf(c_0_67, plain, ![X1:a]:(((times_times_real @ (esk128_0 @ X1) @ (groups1862963056a_real @ aa @ sa))=(aa @ X1))), inference(spm,[status(thm)],[c_0_59, c_0_60])).
% 15.02/2.28 thf(c_0_68, negated_conjecture, ((esk119_2 @ esk123_0 @ (groups1862963056a_real @ aa @ sa))!=(esk118_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_63])).
% 15.02/2.28 thf(c_0_69, 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_64])).
% 15.02/2.28 thf(c_0_70, 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_65, c_0_45])).
% 15.02/2.28 thf(c_0_71, plain, ![X1:a]:(((times_times_real @ (groups1862963056a_real @ aa @ sa) @ (esk128_0 @ X1))=(aa @ X1))), inference(spm,[status(thm)],[c_0_66, c_0_67])).
% 15.02/2.28 thf(c_0_72, negated_conjecture, ((real_V1035702896aleR_b @ (groups1862963056a_real @ aa @ sa) @ (esk123_0 @ esk112_0))!=(esk118_0 @ esk112_0)), inference(rw,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_68]), c_0_69])).
% 15.02/2.28 thf(c_0_73, 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_70, c_0_71]), c_0_53])).
% 15.02/2.28 thf(c_0_74, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])]), ['proof']).
% 15.02/2.28 % SZS output end CNFRefutation
% 15.02/2.28 % Parsed axioms : 418
% 15.02/2.28 % Removed by relevancy pruning/SinE : 0
% 15.02/2.28 % Initial clauses : 956
% 15.02/2.28 % Removed in clause preprocessing : 87
% 15.02/2.28 % Initial clauses in saturation : 869
% 15.02/2.28 % Processed clauses : 4532
% 15.02/2.28 % ...of these trivial : 171
% 15.02/2.28 % ...subsumed : 2498
% 15.02/2.28 % ...remaining for further processing : 1863
% 15.02/2.28 % Other redundant clauses eliminated : 1341
% 15.02/2.28 % Clauses deleted for lack of memory : 0
% 15.02/2.28 % Backward-subsumed : 142
% 15.02/2.28 % Backward-rewritten : 105
% 15.02/2.28 % Generated clauses : 39413
% 15.02/2.28 % ...of the previous two non-redundant : 35225
% 15.02/2.28 % ...aggressively subsumed : 0
% 15.02/2.28 % Contextual simplify-reflections : 5
% 15.02/2.28 % Paramodulations : 36256
% 15.02/2.28 % Factorizations : 54
% 15.02/2.28 % NegExts : 134
% 15.02/2.28 % Equation resolutions : 1373
% 15.02/2.28 % Disequality decompositions : 0
% 15.02/2.28 % Total rewrite steps : 13577
% 15.02/2.28 % ...of those cached : 10170
% 15.02/2.28 % Propositional unsat checks : 0
% 15.02/2.28 % Propositional check models : 0
% 15.02/2.28 % Propositional check unsatisfiable : 0
% 15.02/2.28 % Propositional clauses : 0
% 15.02/2.28 % Propositional clauses after purity: 0
% 15.02/2.28 % Propositional unsat core size : 0
% 15.02/2.28 % Propositional preprocessing time : 0.000
% 15.02/2.28 % Propositional encoding time : 0.000
% 15.02/2.28 % Propositional solver time : 0.000
% 15.02/2.28 % Success case prop preproc time : 0.000
% 15.02/2.28 % Success case prop encoding time : 0.000
% 15.02/2.28 % Success case prop solver time : 0.000
% 15.02/2.28 % Current number of processed clauses : 1544
% 15.02/2.28 % Positive orientable unit clauses : 257
% 15.02/2.28 % Positive unorientable unit clauses: 66
% 15.02/2.28 % Negative unit clauses : 173
% 15.02/2.28 % Non-unit-clauses : 1048
% 15.02/2.28 % Current number of unprocessed clauses: 31054
% 15.02/2.28 % ...number of literals in the above : 101795
% 15.02/2.28 % Current number of archived formulas : 0
% 15.02/2.28 % Current number of archived clauses : 251
% 15.02/2.28 % Clause-clause subsumption calls (NU) : 225912
% 15.02/2.28 % Rec. Clause-clause subsumption calls : 74534
% 15.02/2.28 % Non-unit clause-clause subsumptions : 1044
% 15.02/2.28 % Unit Clause-clause subsumption calls : 80959
% 15.02/2.28 % Rewrite failures with RHS unbound : 2665
% 15.02/2.28 % BW rewrite match attempts : 26095
% 15.02/2.28 % BW rewrite match successes : 1530
% 15.02/2.28 % Condensation attempts : 4532
% 15.02/2.28 % Condensation successes : 60
% 15.02/2.28 % Termbank termtop insertions : 1790673
% 15.02/2.28 % Search garbage collected termcells : 16471
% 15.02/2.28
% 15.02/2.28 % -------------------------------------------------
% 15.02/2.28 % User time : 1.885 s
% 15.02/2.28 % System time : 0.066 s
% 15.02/2.28 % Total time : 1.951 s
% 15.02/2.28 % Maximum resident set size: 8752 pages
% 15.02/2.28
% 15.02/2.28 % -------------------------------------------------
% 15.02/2.28 % User time : 9.178 s
% 15.02/2.28 % System time : 0.279 s
% 15.02/2.28 % Total time : 9.457 s
% 15.02/2.28 % Maximum resident set size: 5888 pages
% 15.02/2.28 % E exiting
%------------------------------------------------------------------------------