%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP133^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 : n015.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:27 AM UTC 2026
% Result : Theorem 1.89s 0.68s
% Output : CNFRefutation 1.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP133^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.26 % Computer : n015.cluster.edu
% 0.08/0.26 % Model : x86_64 x86_64
% 0.08/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.26 % Memory : 8046.5625MB
% 0.08/0.26 % OS : Linux 6.8.0-71-generic
% 0.08/0.26 % CPULimit : 300
% 0.08/0.26 % WCLimit : 300
% 0.08/0.26 % DateTime : Tue Sep 29 20:01:48 UTC 2026
% 0.08/0.27 % CPUTime :
% 0.08/0.27 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.33 Running higher-order theorem proving
% 0.33/0.40 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.9d6Sdw7RxX/E---3.1_4040511.p
% 1.89/0.68 % Version: 3.5.1-ho
% 1.89/0.68 % Preprocessing class: HSLSSMSSSSLNHSA.
% 1.89/0.68 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.89/0.68 % Starting pre_casc_6 with 1200s (4) cores
% 1.89/0.68 % Starting sh4 with 600s (2) cores
% 1.89/0.68 % Starting pre_casc_4 with 300s (1) cores
% 1.89/0.68 % Starting full_lambda_7 with 300s (1) cores
% 1.89/0.68 % pre_casc_6 with pid 4040530 completed with status 0
% 1.89/0.68 % Result found by pre_casc_6
% 1.89/0.68 % Preprocessing class: HSLSSMSSSSLNHSA.
% 1.89/0.68 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.89/0.68 % Starting pre_casc_6 with 1200s (4) cores
% 1.89/0.68 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 1.89/0.68 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 1.89/0.68 % Search class: HGHSM-FSLS32-MHSFFSBC
% 1.89/0.68 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 1.89/0.68 % Starting SubtermCWHack with 109s (1) cores
% 1.89/0.68 % Starting pre_casc_6 with 121s (1) cores
% 1.89/0.68 % Starting new_bool_3 with 109s (1) cores
% 1.89/0.68 % Starting new_bool_1 with 109s (1) cores
% 1.89/0.68 % new_bool_1 with pid 4040539 completed with status 0
% 1.89/0.68 % Result found by new_bool_1
% 1.89/0.68 % Preprocessing class: HSLSSMSSSSLNHSA.
% 1.89/0.68 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.89/0.68 % Starting pre_casc_6 with 1200s (4) cores
% 1.89/0.68 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 1.89/0.68 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 1.89/0.68 % Search class: HGHSM-FSLS32-MHSFFSBC
% 1.89/0.68 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 1.89/0.68 % Starting SubtermCWHack with 109s (1) cores
% 1.89/0.68 % Starting pre_casc_6 with 121s (1) cores
% 1.89/0.68 % Starting new_bool_3 with 109s (1) cores
% 1.89/0.68 % Starting new_bool_1 with 109s (1) cores
% 1.89/0.68 % Preprocessing time : 0.020 s
% 1.89/0.68 % Presaturation interreduction done
% 1.89/0.68
% 1.89/0.68 % Proof found!
% 1.89/0.68 % SZS status Theorem
% 1.89/0.68 % SZS output start CNFRefutation
% 1.89/0.68 thf(decl_sort1, type, nat: $tType).
% 1.89/0.68 thf(decl_sort2, type, set_nat: $tType).
% 1.89/0.68 thf(decl_23, type, one_one_nat: nat).
% 1.89/0.68 thf(decl_24, type, times_times_nat: nat > nat > nat).
% 1.89/0.68 thf(decl_25, type, zero_zero_nat: nat).
% 1.89/0.68 thf(decl_26, type, groups1842438620at_nat: (nat > nat) > set_nat > nat).
% 1.89/0.68 thf(decl_28, type, ord_less_nat: nat > nat > $o).
% 1.89/0.68 thf(decl_31, type, ord_less_eq_nat: nat > nat > $o).
% 1.89/0.68 thf(decl_36, type, set_ord_atMost_nat: nat > set_nat).
% 1.89/0.68 thf(decl_40, type, p: nat > nat).
% 1.89/0.68 thf(decl_41, type, esk1_0: nat).
% 1.89/0.68 thf(decl_42, type, esk2_0: nat).
% 1.89/0.68 thf(decl_130, type, esk90_0: nat > nat).
% 1.89/0.68 thf(decl_131, type, esk91_0: nat > nat).
% 1.89/0.68 thf(decl_142, type, esk5_0: nat).
% 1.89/0.68 thf(conj_0, conjecture, ((![X6:nat]:((((p @ X6)!=(zero_zero_nat))=>((ord_less_eq_nat @ one_one_nat @ X6)&(ord_less_eq_nat @ X6 @ zero_zero_nat))))&((groups1842438620at_nat @ (^[X6:nat]:(times_times_nat @ (p @ X6) @ X6)) @ (set_ord_atMost_nat @ zero_zero_nat))=(zero_zero_nat)))<=>((p)=(^[X6:nat]:(zero_zero_nat)))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', conj_0)).
% 1.89/0.68 thf(fact_143_mult_Ocommute, axiom, ((times_times_nat)=(^[X176:nat, X177:nat]:(times_times_nat @ X177 @ X176))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_143_mult_Ocommute)).
% 1.89/0.69 thf(fact_14_mult__zero__right, axiom, ![X21:nat]:(((times_times_nat @ X21 @ zero_zero_nat)=(zero_zero_nat))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_14_mult__zero__right)).
% 1.89/0.69 thf(fact_0_sum_Oneutral__const, axiom, ![X1:set_nat]:(((groups1842438620at_nat @ (^[X2:nat]:(zero_zero_nat)) @ X1)=(zero_zero_nat))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_0_sum_Oneutral__const)).
% 1.89/0.69 thf(fact_25_le__antisym, axiom, ![X10:nat, X4:nat]:(((ord_less_eq_nat @ X10 @ X4)=>((ord_less_eq_nat @ X4 @ X10)=>((X10)=(X4))))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_25_le__antisym)).
% 1.89/0.69 thf(fact_16_bot__nat__0_Oextremum, axiom, ![X21:nat]:((ord_less_eq_nat @ zero_zero_nat @ X21)), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_16_bot__nat__0_Oextremum)).
% 1.89/0.69 thf(fact_45_bot__nat__0_Oextremum__uniqueI, axiom, ![X21:nat]:(((ord_less_eq_nat @ X21 @ zero_zero_nat)=>((X21)=(zero_zero_nat)))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_45_bot__nat__0_Oextremum__uniqueI)).
% 1.89/0.69 thf(fact_75_not__one__le__zero, axiom, ~((ord_less_eq_nat @ one_one_nat @ zero_zero_nat)), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_75_not__one__le__zero)).
% 1.89/0.69 thf(fact_57_lambda__zero, axiom, ((^[X62:nat]:(zero_zero_nat))=(times_times_nat @ zero_zero_nat)), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_57_lambda__zero)).
% 1.89/0.69 thf(fact_177_less__one, axiom, ![X4:nat]:(((ord_less_nat @ X4 @ one_one_nat)<=>((X4)=(zero_zero_nat)))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_177_less__one)).
% 1.89/0.69 thf(fact_252_dual__order_Ostrict__trans1, axiom, ![X23:nat, X21:nat, X22:nat]:(((ord_less_eq_nat @ X23 @ X21)=>((ord_less_nat @ X22 @ X23)=>(ord_less_nat @ X22 @ X21)))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_252_dual__order_Ostrict__trans1)).
% 1.89/0.69 thf(fact_250_dual__order_Ostrict__trans2, axiom, ![X23:nat, X21:nat, X22:nat]:(((ord_less_nat @ X23 @ X21)=>((ord_less_eq_nat @ X22 @ X23)=>(ord_less_nat @ X22 @ X21)))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_250_dual__order_Ostrict__trans2)).
% 1.89/0.69 thf(fact_188_dual__order_Oirrefl, axiom, ![X21:nat]:(~((ord_less_nat @ X21 @ X21))), file('/export/starexec/sandbox2/tmp/tmp.9d6Sdw7RxX/E---3.1_4040511.p', fact_188_dual__order_Oirrefl)).
% 1.89/0.69 thf(c_0_13, negated_conjecture, ~(((![X6:nat]:((((p @ X6)!=(zero_zero_nat))=>((ord_less_eq_nat @ one_one_nat @ X6)&(ord_less_eq_nat @ X6 @ zero_zero_nat))))&((groups1842438620at_nat @ (^[X6:nat]:(times_times_nat @ (p @ X6) @ X6)) @ (set_ord_atMost_nat @ zero_zero_nat))=(zero_zero_nat)))<=>((p)=(^[X6:nat]:(zero_zero_nat))))), inference(assume_negation,[status(cth)],[conj_0])).
% 1.89/0.69 thf(c_0_14, negated_conjecture, ~(((![X6:nat]:((((p @ X6)!=(zero_zero_nat))=>((ord_less_eq_nat @ one_one_nat @ X6)&(ord_less_eq_nat @ X6 @ zero_zero_nat))))&((groups1842438620at_nat @ (^[Z0:nat]:(times_times_nat @ (p @ Z0) @ Z0)) @ (set_ord_atMost_nat @ zero_zero_nat))=(zero_zero_nat)))<=>![X840:nat]:(((p @ X840)=(zero_zero_nat))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_13])])])).
% 1.89/0.69 thf(c_0_15, negated_conjecture, ![X881:nat, X882:nat]:((((((p @ esk1_0)!=(zero_zero_nat))|((groups1842438620at_nat @ (^[Z0:nat]:(times_times_nat @ (p @ Z0) @ Z0)) @ (set_ord_atMost_nat @ zero_zero_nat))!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat)))&(~(ord_less_eq_nat @ one_one_nat @ esk1_0)|~(ord_less_eq_nat @ esk1_0 @ zero_zero_nat)|((groups1842438620at_nat @ (^[Z0:nat]:(times_times_nat @ (p @ Z0) @ Z0)) @ (set_ord_atMost_nat @ zero_zero_nat))!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))))&((((ord_less_eq_nat @ one_one_nat @ X881)|((p @ X881)=(zero_zero_nat))|((p @ X882)=(zero_zero_nat)))&((ord_less_eq_nat @ X881 @ zero_zero_nat)|((p @ X881)=(zero_zero_nat))|((p @ X882)=(zero_zero_nat))))&(((groups1842438620at_nat @ (^[Z0:nat]:(times_times_nat @ (p @ Z0) @ Z0)) @ (set_ord_atMost_nat @ zero_zero_nat))=(zero_zero_nat))|((p @ X882)=(zero_zero_nat)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])])])])).
% 1.89/0.69 thf(c_0_16, plain, ![X846:nat, X847:nat]:(((times_times_nat @ X846 @ X847)=(times_times_nat @ X847 @ X846))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_143_mult_Ocommute])])).
% 1.89/0.69 thf(c_0_17, plain, ![X1524:nat]:(((esk90_0 @ X1524)=(times_times_nat @ (p @ X1524) @ X1524))), introduced(definition)).
% 1.89/0.69 thf(c_0_18, negated_conjecture, ![X2:nat, X4:nat]:(((ord_less_eq_nat @ X2 @ zero_zero_nat)|((p @ X2)=(zero_zero_nat))|((p @ X4)=(zero_zero_nat)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 1.89/0.69 thf(c_0_19, plain, ![X1560:nat]:(((esk90_0 @ X1560)=(times_times_nat @ (p @ X1560) @ X1560))), inference(variable_rename,[status(thm)],[])).
% 1.89/0.69 thf(c_0_20, plain, ![X1106:nat, X1107:nat]:(((times_times_nat @ X1106 @ X1107)=(times_times_nat @ X1107 @ X1106))), inference(variable_rename,[status(thm)],[c_0_16])).
% 1.89/0.69 thf(c_0_21, negated_conjecture, (((p @ esk1_0)!=(zero_zero_nat))|((groups1842438620at_nat @ esk90_0 @ (set_ord_atMost_nat @ zero_zero_nat))!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_15]), c_0_17])).
% 1.89/0.69 thf(c_0_22, negated_conjecture, ![X2:nat]:((((p @ X2)=(zero_zero_nat))|(ord_less_eq_nat @ X2 @ zero_zero_nat))), inference(ef,[status(thm)],[c_0_18])).
% 1.89/0.69 thf(c_0_23, plain, ![X2:nat]:(((esk90_0 @ X2)=(times_times_nat @ (p @ X2) @ X2))), inference(split_conjunct,[status(thm)],[c_0_19])).
% 1.89/0.69 thf(c_0_24, plain, ![X4:nat, X2:nat]:(((times_times_nat @ X2 @ X4)=(times_times_nat @ X4 @ X2))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 1.89/0.69 thf(c_0_25, plain, ![X891:nat]:(((times_times_nat @ X891 @ zero_zero_nat)=(zero_zero_nat))), inference(variable_rename,[status(thm)],[fact_14_mult__zero__right])).
% 1.89/0.69 thf(c_0_26, plain, ![X1:set_nat]:(((groups1842438620at_nat @ (^[Z0:nat]:(zero_zero_nat)) @ X1)=(zero_zero_nat))), inference(fof_simplification,[status(thm)],[fact_0_sum_Oneutral__const])).
% 1.89/0.69 thf(c_0_27, negated_conjecture, ((ord_less_eq_nat @ esk1_0 @ zero_zero_nat)|((groups1842438620at_nat @ esk90_0 @ (set_ord_atMost_nat @ zero_zero_nat))!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 1.89/0.69 thf(c_0_28, plain, ![X2:nat]:(((times_times_nat @ X2 @ (p @ X2))=(esk90_0 @ X2))), inference(rw,[status(thm)],[c_0_23, c_0_24])).
% 1.89/0.69 thf(c_0_29, negated_conjecture, ![X2:nat]:((((groups1842438620at_nat @ esk90_0 @ (set_ord_atMost_nat @ zero_zero_nat))=(zero_zero_nat))|((p @ X2)=(zero_zero_nat)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_15]), c_0_17])).
% 1.89/0.69 thf(c_0_30, plain, ![X2:nat]:(((times_times_nat @ X2 @ zero_zero_nat)=(zero_zero_nat))), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.89/0.69 thf(c_0_31, plain, ![X989:set_nat]:(((groups1842438620at_nat @ (^[Z0:nat]:(zero_zero_nat)) @ X989)=(zero_zero_nat))), inference(variable_rename,[status(thm)],[c_0_26])).
% 1.89/0.69 thf(c_0_32, plain, ![X1527:nat]:(((esk91_0 @ X1527)=(zero_zero_nat))), introduced(definition)).
% 1.89/0.69 thf(c_0_33, plain, ![X1125:nat, X1126:nat]:((~(ord_less_eq_nat @ X1125 @ X1126)|(~(ord_less_eq_nat @ X1126 @ X1125)|((X1125)=(X1126))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_25_le__antisym])])])).
% 1.89/0.69 thf(c_0_34, negated_conjecture, ((ord_less_eq_nat @ esk2_0 @ zero_zero_nat)|(ord_less_eq_nat @ esk1_0 @ zero_zero_nat)|((groups1842438620at_nat @ esk90_0 @ (set_ord_atMost_nat @ zero_zero_nat))!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_27, c_0_22])).
% 1.89/0.69 thf(c_0_35, negated_conjecture, ![X2:nat]:((((groups1842438620at_nat @ esk90_0 @ (set_ord_atMost_nat @ zero_zero_nat))=(zero_zero_nat))|((esk90_0 @ X2)=(zero_zero_nat)))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_30])).
% 1.89/0.69 thf(c_0_36, plain, ![X893:nat]:((ord_less_eq_nat @ zero_zero_nat @ X893)), inference(variable_rename,[status(thm)],[fact_16_bot__nat__0_Oextremum])).
% 1.89/0.69 thf(c_0_37, plain, ![X1:set_nat]:(((groups1842438620at_nat @ esk91_0 @ X1)=(zero_zero_nat))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_31]), c_0_32])).
% 1.89/0.69 thf(c_0_38, plain, ![X1561:nat]:(((esk91_0 @ X1561)=(zero_zero_nat))), inference(variable_rename,[status(thm)],[])).
% 1.89/0.69 thf(c_0_39, plain, ![X4:nat, X2:nat]:((((X2)=(X4))|~((ord_less_eq_nat @ X2 @ X4))|~((ord_less_eq_nat @ X4 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 1.89/0.69 thf(c_0_40, negated_conjecture, ![X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|(ord_less_eq_nat @ esk1_0 @ zero_zero_nat)|(ord_less_eq_nat @ esk2_0 @ zero_zero_nat))), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 1.89/0.69 thf(c_0_41, plain, ![X2:nat]:((ord_less_eq_nat @ zero_zero_nat @ X2)), inference(split_conjunct,[status(thm)],[c_0_36])).
% 1.89/0.69 thf(c_0_42, plain, (((p @ esk1_0)!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))|((esk91_0)!=(esk90_0))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_21, c_0_37])])).
% 1.89/0.69 thf(c_0_43, plain, ![X2:nat]:(((esk91_0 @ X2)=(zero_zero_nat))), inference(split_conjunct,[status(thm)],[c_0_38])).
% 1.89/0.69 thf(c_0_44, negated_conjecture, ![X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|((esk2_0)=(zero_zero_nat))|(ord_less_eq_nat @ esk1_0 @ zero_zero_nat))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_41])])).
% 1.89/0.69 thf(c_0_45, plain, ![X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|(ord_less_eq_nat @ X2 @ zero_zero_nat))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_22]), c_0_30])).
% 1.89/0.69 thf(c_0_46, plain, (((esk90_0 @ esk5_0)!=(zero_zero_nat))|((p @ esk1_0)!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(rw,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_42]), c_0_43])).
% 1.89/0.69 thf(c_0_47, negated_conjecture, ![X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|((esk2_0)=(zero_zero_nat))|((esk1_0)=(zero_zero_nat)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_44]), c_0_41])])).
% 1.89/0.69 thf(c_0_48, plain, ![X916:nat]:((~(ord_less_eq_nat @ X916 @ zero_zero_nat)|((X916)=(zero_zero_nat)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_45_bot__nat__0_Oextremum__uniqueI])])])).
% 1.89/0.69 thf(c_0_49, plain, ![X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|((zero_zero_nat)=(X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_45]), c_0_41])])).
% 1.89/0.69 thf(c_0_50, plain, (((esk1_0)=(zero_zero_nat))|((esk2_0)=(zero_zero_nat))|((p @ esk1_0)!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 1.89/0.69 thf(c_0_51, plain, ![X2:nat]:((((X2)=(zero_zero_nat))|~((ord_less_eq_nat @ X2 @ zero_zero_nat)))), inference(split_conjunct,[status(thm)],[c_0_48])).
% 1.89/0.69 thf(c_0_52, plain, (((zero_zero_nat)=(esk5_0))|((p @ esk1_0)!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_46, c_0_49])).
% 1.89/0.69 thf(c_0_53, negated_conjecture, (((esk2_0)=(zero_zero_nat))|((esk1_0)=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_22]), c_0_51])).
% 1.89/0.69 thf(c_0_54, plain, ~(ord_less_eq_nat @ one_one_nat @ zero_zero_nat), inference(fof_simplification,[status(thm)],[fact_75_not__one__le__zero])).
% 1.89/0.69 thf(c_0_55, negated_conjecture, (((zero_zero_nat)=(esk5_0))|(ord_less_eq_nat @ esk1_0 @ zero_zero_nat)|((p @ esk2_0)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_52, c_0_22])).
% 1.89/0.69 thf(c_0_56, negated_conjecture, (((esk1_0)=(zero_zero_nat))|((esk2_0)=(zero_zero_nat))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_22]), c_0_51])).
% 1.89/0.69 thf(c_0_57, plain, ~(ord_less_eq_nat @ one_one_nat @ zero_zero_nat), inference(fof_nnf,[status(thm)],[c_0_54])).
% 1.89/0.69 thf(c_0_58, negated_conjecture, (((esk1_0)=(zero_zero_nat))|((zero_zero_nat)=(esk5_0))|((p @ zero_zero_nat)!=(zero_zero_nat))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_51])).
% 1.89/0.69 thf(c_0_59, negated_conjecture, ![X2:nat, X4:nat]:(((ord_less_eq_nat @ one_one_nat @ X2)|((p @ X2)=(zero_zero_nat))|((p @ X4)=(zero_zero_nat)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 1.89/0.69 thf(c_0_60, plain, ~((ord_less_eq_nat @ one_one_nat @ zero_zero_nat)), inference(split_conjunct,[status(thm)],[c_0_57])).
% 1.89/0.69 thf(c_0_61, negated_conjecture, ![X2:nat]:((((p @ X2)=(zero_zero_nat))|((zero_zero_nat)=(esk5_0))|((esk1_0)=(zero_zero_nat)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60])).
% 1.89/0.69 thf(c_0_62, negated_conjecture, (((zero_zero_nat)=(esk5_0))|((esk1_0)=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_58, c_0_61])).
% 1.89/0.69 thf(c_0_63, plain, (((zero_zero_nat)=(esk5_0))|((p @ zero_zero_nat)!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_52, c_0_62])).
% 1.89/0.69 thf(c_0_64, negated_conjecture, ![X2:nat]:((((p @ X2)=(zero_zero_nat))|(ord_less_eq_nat @ one_one_nat @ X2))), inference(ef,[status(thm)],[c_0_59])).
% 1.89/0.69 thf(c_0_65, plain, (((zero_zero_nat)=(esk5_0))|((p @ esk2_0)!=(zero_zero_nat))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_60])).
% 1.89/0.69 thf(c_0_66, plain, ![X841:nat]:(((zero_zero_nat)=(times_times_nat @ zero_zero_nat @ X841))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_57_lambda__zero])])).
% 1.89/0.69 thf(c_0_67, negated_conjecture, (((zero_zero_nat)=(esk5_0))|(ord_less_eq_nat @ esk2_0 @ zero_zero_nat)), inference(spm,[status(thm)],[c_0_65, c_0_22])).
% 1.89/0.69 thf(c_0_68, negated_conjecture, (((esk1_0)=(zero_zero_nat))|((groups1842438620at_nat @ esk90_0 @ (set_ord_atMost_nat @ zero_zero_nat))!=(zero_zero_nat))|((p @ zero_zero_nat)!=(zero_zero_nat))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_56]), c_0_51])).
% 1.89/0.69 thf(c_0_69, plain, ![X921:nat]:(((zero_zero_nat)=(times_times_nat @ zero_zero_nat @ X921))), inference(variable_rename,[status(thm)],[c_0_66])).
% 1.89/0.69 thf(c_0_70, negated_conjecture, (((zero_zero_nat)=(esk5_0))|((esk2_0)=(zero_zero_nat))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_67]), c_0_41])])).
% 1.89/0.69 thf(c_0_71, negated_conjecture, ![X2:nat]:((((p @ X2)=(zero_zero_nat))|((esk1_0)=(zero_zero_nat)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_59]), c_0_60]), c_0_29])).
% 1.89/0.69 thf(c_0_72, plain, ![X2:nat]:(((zero_zero_nat)=(times_times_nat @ zero_zero_nat @ X2))), inference(split_conjunct,[status(thm)],[c_0_69])).
% 1.89/0.69 thf(c_0_73, plain, (((zero_zero_nat)=(esk5_0))|((p @ zero_zero_nat)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_65, c_0_70])).
% 1.89/0.69 thf(c_0_74, plain, ![X1294:nat]:(((~(ord_less_nat @ X1294 @ one_one_nat)|((X1294)=(zero_zero_nat)))&(((X1294)!=(zero_zero_nat))|(ord_less_nat @ X1294 @ one_one_nat)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_177_less__one])])])).
% 1.89/0.69 thf(c_0_75, plain, ![X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|((esk1_0)=(zero_zero_nat)))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_71]), c_0_30])).
% 1.89/0.69 thf(c_0_76, plain, ((esk90_0 @ zero_zero_nat)=(zero_zero_nat)), inference(spm,[status(thm)],[c_0_72, c_0_28])).
% 1.89/0.69 thf(c_0_77, negated_conjecture, ((zero_zero_nat)=(esk5_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_64]), c_0_60])).
% 1.89/0.69 thf(c_0_78, plain, ![X2:nat]:(((ord_less_nat @ X2 @ one_one_nat)|((X2)!=(zero_zero_nat)))), inference(split_conjunct,[status(thm)],[c_0_74])).
% 1.89/0.69 thf(c_0_79, plain, ((esk1_0)=(zero_zero_nat)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_75]), c_0_71]), c_0_71])).
% 1.89/0.69 thf(c_0_80, plain, ((esk90_0 @ esk5_0)=(esk5_0)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_76, c_0_77]), c_0_77])).
% 1.89/0.69 thf(c_0_81, plain, ![X1280:nat, X1281:nat, X1282:nat]:((~(ord_less_eq_nat @ X1280 @ X1281)|(~(ord_less_nat @ X1282 @ X1280)|(ord_less_nat @ X1282 @ X1281)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_252_dual__order_Ostrict__trans1])])])).
% 1.89/0.69 thf(c_0_82, plain, (ord_less_nat @ zero_zero_nat @ one_one_nat), inference(er,[status(thm)],[c_0_78])).
% 1.89/0.69 thf(c_0_83, plain, (((p @ esk5_0)!=(esk5_0))|((p @ esk2_0)!=(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_79]), c_0_80]), c_0_77]), c_0_77]), c_0_77]), c_0_77])])).
% 1.89/0.69 thf(c_0_84, negated_conjecture, ![X2:nat]:((((p @ X2)=(esk5_0))|(ord_less_eq_nat @ one_one_nat @ X2))), inference(rw,[status(thm)],[c_0_64, c_0_77])).
% 1.89/0.69 thf(c_0_85, plain, ~((ord_less_eq_nat @ one_one_nat @ esk5_0)), inference(rw,[status(thm)],[c_0_60, c_0_77])).
% 1.89/0.69 thf(c_0_86, plain, ![X5:nat, X4:nat, X2:nat]:(((ord_less_nat @ X5 @ X4)|~((ord_less_eq_nat @ X2 @ X4))|~((ord_less_nat @ X5 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_81])).
% 1.89/0.69 thf(c_0_87, plain, (ord_less_nat @ esk5_0 @ one_one_nat), inference(rw,[status(thm)],[c_0_82, c_0_77])).
% 1.89/0.69 thf(c_0_88, plain, ((p @ esk2_0)!=(esk5_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_83, c_0_84]), c_0_85])).
% 1.89/0.69 thf(c_0_89, plain, ![X1277:nat, X1278:nat, X1279:nat]:((~(ord_less_nat @ X1277 @ X1278)|(~(ord_less_eq_nat @ X1279 @ X1277)|(ord_less_nat @ X1279 @ X1278)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_250_dual__order_Ostrict__trans2])])])).
% 1.89/0.69 thf(c_0_90, plain, ![X2:nat]:(((ord_less_nat @ esk5_0 @ X2)|~((ord_less_eq_nat @ one_one_nat @ X2)))), inference(spm,[status(thm)],[c_0_86, c_0_87])).
% 1.89/0.69 thf(c_0_91, negated_conjecture, (ord_less_eq_nat @ one_one_nat @ esk2_0), inference(spm,[status(thm)],[c_0_88, c_0_84])).
% 1.89/0.69 thf(c_0_92, plain, ![X21:nat]:(~(ord_less_nat @ X21 @ X21)), inference(fof_simplification,[status(thm)],[fact_188_dual__order_Oirrefl])).
% 1.89/0.69 thf(c_0_93, plain, ![X5:nat, X4:nat, X2:nat]:(((ord_less_nat @ X5 @ X4)|~((ord_less_nat @ X2 @ X4))|~((ord_less_eq_nat @ X5 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_89])).
% 1.89/0.69 thf(c_0_94, negated_conjecture, (ord_less_nat @ esk5_0 @ esk2_0), inference(spm,[status(thm)],[c_0_90, c_0_91])).
% 1.89/0.69 thf(c_0_95, negated_conjecture, ![X2:nat]:((((p @ X2)=(esk5_0))|(ord_less_eq_nat @ X2 @ esk5_0))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_77]), c_0_77])).
% 1.89/0.69 thf(c_0_96, plain, ![X1325:nat]:(~(ord_less_nat @ X1325 @ X1325)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_92])])).
% 1.89/0.69 thf(c_0_97, negated_conjecture, ![X2:nat]:(((ord_less_nat @ X2 @ esk2_0)|~((ord_less_eq_nat @ X2 @ esk5_0)))), inference(spm,[status(thm)],[c_0_93, c_0_94])).
% 1.89/0.69 thf(c_0_98, plain, (ord_less_eq_nat @ esk2_0 @ esk5_0), inference(spm,[status(thm)],[c_0_88, c_0_95])).
% 1.89/0.69 thf(c_0_99, plain, ![X2:nat]:(~((ord_less_nat @ X2 @ X2))), inference(split_conjunct,[status(thm)],[c_0_96])).
% 1.89/0.69 thf(c_0_100, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_98]), c_0_99]), ['proof']).
% 1.89/0.69 % SZS output end CNFRefutation
% 1.89/0.69 % Parsed axioms : 283
% 1.89/0.69 % Removed by relevancy pruning/SinE : 45
% 1.89/0.69 % Initial clauses : 513
% 1.89/0.69 % Removed in clause preprocessing : 21
% 1.89/0.69 % Initial clauses in saturation : 492
% 1.89/0.69 % Processed clauses : 981
% 1.89/0.69 % ...of these trivial : 42
% 1.89/0.69 % ...subsumed : 302
% 1.89/0.69 % ...remaining for further processing : 637
% 1.89/0.69 % Other redundant clauses eliminated : 139
% 1.89/0.69 % Clauses deleted for lack of memory : 0
% 1.89/0.69 % Backward-subsumed : 16
% 1.89/0.69 % Backward-rewritten : 97
% 1.89/0.69 % Generated clauses : 2163
% 1.89/0.69 % ...of the previous two non-redundant : 1793
% 1.89/0.69 % ...aggressively subsumed : 0
% 1.89/0.69 % Contextual simplify-reflections : 8
% 1.89/0.69 % Paramodulations : 1803
% 1.89/0.69 % Factorizations : 10
% 1.89/0.69 % NegExts : 4
% 1.89/0.69 % Equation resolutions : 142
% 1.89/0.69 % Disequality decompositions : 0
% 1.89/0.69 % Total rewrite steps : 833
% 1.89/0.69 % ...of those cached : 668
% 1.89/0.69 % Propositional unsat checks : 0
% 1.89/0.69 % Propositional check models : 0
% 1.89/0.69 % Propositional check unsatisfiable : 0
% 1.89/0.69 % Propositional clauses : 0
% 1.89/0.69 % Propositional clauses after purity: 0
% 1.89/0.69 % Propositional unsat core size : 0
% 1.89/0.69 % Propositional preprocessing time : 0.000
% 1.89/0.69 % Propositional encoding time : 0.000
% 1.89/0.69 % Propositional solver time : 0.000
% 1.89/0.69 % Success case prop preproc time : 0.000
% 1.89/0.69 % Success case prop encoding time : 0.000
% 1.89/0.69 % Success case prop solver time : 0.000
% 1.89/0.69 % Current number of processed clauses : 192
% 1.89/0.69 % Positive orientable unit clauses : 66
% 1.89/0.69 % Positive unorientable unit clauses: 9
% 1.89/0.69 % Negative unit clauses : 6
% 1.89/0.69 % Non-unit-clauses : 111
% 1.89/0.69 % Current number of unprocessed clauses: 1435
% 1.89/0.69 % ...number of literals in the above : 3538
% 1.89/0.69 % Current number of archived formulas : 0
% 1.89/0.69 % Current number of archived clauses : 363
% 1.89/0.69 % Clause-clause subsumption calls (NU) : 17924
% 1.89/0.69 % Rec. Clause-clause subsumption calls : 9036
% 1.89/0.69 % Non-unit clause-clause subsumptions : 236
% 1.89/0.69 % Unit Clause-clause subsumption calls : 607
% 1.89/0.69 % Rewrite failures with RHS unbound : 0
% 1.89/0.69 % BW rewrite match attempts : 758
% 1.89/0.69 % BW rewrite match successes : 115
% 1.89/0.69 % Condensation attempts : 0
% 1.89/0.69 % Condensation successes : 0
% 1.89/0.69 % Termbank termtop insertions : 115081
% 1.89/0.69 % Search garbage collected termcells : 10441
% 1.89/0.69
% 1.89/0.69 % -------------------------------------------------
% 1.89/0.69 % User time : 0.234 s
% 1.89/0.69 % System time : 0.018 s
% 1.89/0.69 % Total time : 0.252 s
% 1.89/0.69 % Maximum resident set size: 5932 pages
% 1.89/0.69
% 1.89/0.69 % -------------------------------------------------
% 1.89/0.69 % User time : 0.765 s
% 1.89/0.69 % System time : 0.056 s
% 1.89/0.69 % Total time : 0.821 s
% 1.89/0.69 % Maximum resident set size: 5376 pages
% 1.89/0.69 % E exiting
%------------------------------------------------------------------------------