%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP133^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 : n009.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:37 AM UTC 2026
% Result : Theorem 0.91s 0.47s
% Output : CNFRefutation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP133^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n009.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:58:30 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p
% 0.91/0.47 % Version: 3.5.1-ho
% 0.91/0.47 % Preprocessing class: HSLSSMSSSSLNHSA.
% 0.91/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.91/0.47 % Starting pre_casc_6 with 1200s (4) cores
% 0.91/0.47 % Starting sh4 with 600s (2) cores
% 0.91/0.47 % Starting pre_casc_4 with 300s (1) cores
% 0.91/0.47 % Starting full_lambda_7 with 300s (1) cores
% 0.91/0.47 % pre_casc_6 with pid 277541 completed with status 0
% 0.91/0.47 % Result found by pre_casc_6
% 0.91/0.47 % Preprocessing class: HSLSSMSSSSLNHSA.
% 0.91/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.91/0.47 % Starting pre_casc_6 with 1200s (4) cores
% 0.91/0.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 0.91/0.47 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 0.91/0.47 % Search class: HGHSM-FSLS32-MHSFFSBC
% 0.91/0.47 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.91/0.47 % Starting SubtermCWHack with 109s (1) cores
% 0.91/0.47 % Starting pre_casc_6 with 121s (1) cores
% 0.91/0.47 % Starting new_bool_3 with 109s (1) cores
% 0.91/0.47 % Starting new_bool_1 with 109s (1) cores
% 0.91/0.47 % SubtermCWHack with pid 277549 completed with status 0
% 0.91/0.47 % Result found by SubtermCWHack
% 0.91/0.47 % Preprocessing class: HSLSSMSSSSLNHSA.
% 0.91/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.91/0.47 % Starting pre_casc_6 with 1200s (4) cores
% 0.91/0.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 0.91/0.47 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 0.91/0.47 % Search class: HGHSM-FSLS32-MHSFFSBC
% 0.91/0.47 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.91/0.47 % Starting SubtermCWHack with 109s (1) cores
% 0.91/0.47 % Preprocessing time : 0.007 s
% 0.91/0.47
% 0.91/0.47 % Proof found!
% 0.91/0.47 % SZS status Theorem
% 0.91/0.47 % SZS output start CNFRefutation
% 0.91/0.47 thf(decl_sort1, type, nat: $tType).
% 0.91/0.47 thf(decl_sort2, type, set_nat: $tType).
% 0.91/0.47 thf(decl_23, type, one_one_nat: nat).
% 0.91/0.47 thf(decl_24, type, times_times_nat: nat > nat > nat).
% 0.91/0.47 thf(decl_25, type, zero_zero_nat: nat).
% 0.91/0.47 thf(decl_26, type, groups1842438620at_nat: (nat > nat) > set_nat > nat).
% 0.91/0.47 thf(decl_28, type, ord_less_nat: nat > nat > $o).
% 0.91/0.47 thf(decl_31, type, ord_less_eq_nat: nat > nat > $o).
% 0.91/0.47 thf(decl_36, type, set_ord_atMost_nat: nat > set_nat).
% 0.91/0.47 thf(decl_38, type, member_nat: nat > set_nat > $o).
% 0.91/0.47 thf(decl_40, type, p: nat > nat).
% 0.91/0.47 thf(decl_41, type, esk1_0: nat).
% 0.91/0.47 thf(decl_42, type, esk2_0: nat).
% 0.91/0.47 thf(decl_55, type, esk15_2: (nat > nat) > set_nat > nat).
% 0.91/0.47 thf(decl_130, type, esk90_0: nat > nat).
% 0.91/0.47 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/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', conj_0)).
% 0.91/0.47 thf(fact_143_mult_Ocommute, axiom, ((times_times_nat)=(^[X176:nat, X177:nat]:(times_times_nat @ X177 @ X176))), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_143_mult_Ocommute)).
% 0.91/0.47 thf(fact_14_mult__zero__right, axiom, ![X21:nat]:(((times_times_nat @ X21 @ zero_zero_nat)=(zero_zero_nat))), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_14_mult__zero__right)).
% 0.91/0.47 thf(fact_170_less__nat__zero__code, axiom, ![X4:nat]:(~((ord_less_nat @ X4 @ zero_zero_nat))), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_170_less__nat__zero__code)).
% 0.91/0.47 thf(fact_174_nat__0__less__mult__iff, axiom, ![X10:nat, X4:nat]:(((ord_less_nat @ zero_zero_nat @ (times_times_nat @ X10 @ X4))<=>((ord_less_nat @ zero_zero_nat @ X10)&(ord_less_nat @ zero_zero_nat @ X4)))), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_174_nat__0__less__mult__iff)).
% 0.91/0.47 thf(fact_169_neq0__conv, axiom, ![X4:nat]:((((X4)!=(zero_zero_nat))<=>(ord_less_nat @ zero_zero_nat @ X4))), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_169_neq0__conv)).
% 0.91/0.47 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/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_252_dual__order_Ostrict__trans1)).
% 0.91/0.47 thf(fact_40_sum_Onot__neutral__contains__not__neutral, axiom, ![X43:nat > nat, X1:set_nat]:((((groups1842438620at_nat @ X43 @ X1)!=(zero_zero_nat))=>~(![X44:nat]:(((member_nat @ X44 @ X1)=>((X43 @ X44)=(zero_zero_nat))))))), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_40_sum_Onot__neutral__contains__not__neutral)).
% 0.91/0.47 thf(fact_13_mult__eq__0__iff, axiom, ![X21:nat, X23:nat]:((((times_times_nat @ X21 @ X23)=(zero_zero_nat))<=>(((X21)=(zero_zero_nat))|((X23)=(zero_zero_nat))))), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_13_mult__eq__0__iff)).
% 0.91/0.47 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/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_25_le__antisym)).
% 0.91/0.47 thf(fact_16_bot__nat__0_Oextremum, axiom, ![X21:nat]:((ord_less_eq_nat @ zero_zero_nat @ X21)), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_16_bot__nat__0_Oextremum)).
% 0.91/0.47 thf(fact_75_not__one__le__zero, axiom, ~((ord_less_eq_nat @ one_one_nat @ zero_zero_nat)), file('/export/starexec/sandbox/tmp/tmp.rUM4MWRm2K/E---3.1_277528.p', fact_75_not__one__le__zero)).
% 0.91/0.47 thf(c_0_12, 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])).
% 0.91/0.47 thf(c_0_13, 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])])).
% 0.91/0.47 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_12])])])).
% 0.91/0.47 thf(c_0_15, plain, ![X1560:nat]:(((esk90_0 @ X1560)=(times_times_nat @ (p @ X1560) @ X1560))), inference(variable_rename,[status(thm)],[])).
% 0.91/0.47 thf(c_0_16, plain, ![X1106:nat, X1107:nat]:(((times_times_nat @ X1106 @ X1107)=(times_times_nat @ X1107 @ X1106))), inference(variable_rename,[status(thm)],[c_0_13])).
% 0.91/0.47 thf(c_0_17, 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])])])])])])).
% 0.91/0.47 thf(c_0_18, plain, ![X2:nat]:(((esk90_0 @ X2)=(times_times_nat @ (p @ X2) @ X2))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.91/0.47 thf(c_0_19, plain, ![X4:nat, X2:nat]:(((times_times_nat @ X2 @ X4)=(times_times_nat @ X4 @ X2))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.91/0.47 thf(c_0_20, 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_17])).
% 0.91/0.47 thf(c_0_21, plain, ![X891:nat]:(((times_times_nat @ X891 @ zero_zero_nat)=(zero_zero_nat))), inference(variable_rename,[status(thm)],[fact_14_mult__zero__right])).
% 0.91/0.47 thf(c_0_22, plain, ![X4:nat]:(~(ord_less_nat @ X4 @ zero_zero_nat)), inference(fof_simplification,[status(thm)],[fact_170_less__nat__zero__code])).
% 0.91/0.47 thf(c_0_23, plain, ![X959:nat, X960:nat]:(((((ord_less_nat @ zero_zero_nat @ X959)|~(ord_less_nat @ zero_zero_nat @ (times_times_nat @ X959 @ X960)))&((ord_less_nat @ zero_zero_nat @ X960)|~(ord_less_nat @ zero_zero_nat @ (times_times_nat @ X959 @ X960))))&(~(ord_less_nat @ zero_zero_nat @ X959)|~(ord_less_nat @ zero_zero_nat @ X960)|(ord_less_nat @ zero_zero_nat @ (times_times_nat @ X959 @ X960))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_174_nat__0__less__mult__iff])])])])).
% 0.91/0.47 thf(c_0_24, plain, ![X4:nat]:((((X4)!=(zero_zero_nat))<=>(ord_less_nat @ zero_zero_nat @ X4))), inference(fof_simplification,[status(thm)],[fact_169_neq0__conv])).
% 0.91/0.47 thf(c_0_25, 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])])])).
% 0.91/0.47 thf(c_0_26, plain, ![X2:nat]:(((times_times_nat @ X2 @ (p @ X2))=(esk90_0 @ X2))), inference(rw,[status(thm)],[c_0_18, c_0_19])).
% 0.91/0.47 thf(c_0_27, negated_conjecture, ![X2:nat]:((((p @ X2)=(zero_zero_nat))|(ord_less_eq_nat @ X2 @ zero_zero_nat))), inference(ef,[status(thm)],[c_0_20])).
% 0.91/0.47 thf(c_0_28, plain, ![X2:nat]:(((times_times_nat @ X2 @ zero_zero_nat)=(zero_zero_nat))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.91/0.47 thf(c_0_29, plain, ![X956:nat]:(~(ord_less_nat @ X956 @ zero_zero_nat)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_22])])).
% 0.91/0.47 thf(c_0_30, plain, ![X2:nat, X4:nat]:(((ord_less_nat @ zero_zero_nat @ X2)|~((ord_less_nat @ zero_zero_nat @ (times_times_nat @ X2 @ X4))))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.91/0.47 thf(c_0_31, plain, ![X955:nat]:(((((X955)=(zero_zero_nat))|(ord_less_nat @ zero_zero_nat @ X955))&(~(ord_less_nat @ zero_zero_nat @ X955)|((X955)!=(zero_zero_nat))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])])).
% 0.91/0.47 thf(c_0_32, plain, ![X43:nat > nat, X1:set_nat]:((((groups1842438620at_nat @ X43 @ X1)!=(zero_zero_nat))=>~(![X44:nat]:(((member_nat @ X44 @ X1)=>((X43 @ X44)=(zero_zero_nat))))))), inference(fof_simplification,[status(thm)],[fact_40_sum_Onot__neutral__contains__not__neutral])).
% 0.91/0.47 thf(c_0_33, 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_25])).
% 0.91/0.47 thf(c_0_34, negated_conjecture, ![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_26, c_0_27]), c_0_28])).
% 0.91/0.47 thf(c_0_35, plain, ![X2:nat]:(~((ord_less_nat @ X2 @ zero_zero_nat))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.91/0.47 thf(c_0_36, plain, ![X2:nat]:(((ord_less_nat @ zero_zero_nat @ X2)|~((ord_less_nat @ zero_zero_nat @ (esk90_0 @ X2))))), inference(spm,[status(thm)],[c_0_30, c_0_26])).
% 0.91/0.47 thf(c_0_37, plain, ![X2:nat]:((((X2)=(zero_zero_nat))|(ord_less_nat @ zero_zero_nat @ X2))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.91/0.47 thf(c_0_38, plain, ![X1026:nat > nat, X1027:set_nat]:((((member_nat @ (esk15_2 @ X1026 @ X1027) @ X1027)|((groups1842438620at_nat @ X1026 @ X1027)=(zero_zero_nat)))&(((X1026 @ (esk15_2 @ X1026 @ X1027))!=(zero_zero_nat))|((groups1842438620at_nat @ X1026 @ X1027)=(zero_zero_nat))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_32])])])])])).
% 0.91/0.47 thf(c_0_39, negated_conjecture, ![X4:nat, X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|~((ord_less_nat @ X4 @ X2)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_34]), c_0_35])).
% 0.91/0.47 thf(c_0_40, plain, ![X2:nat]:((((esk90_0 @ X2)=(zero_zero_nat))|(ord_less_nat @ zero_zero_nat @ X2))), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.91/0.47 thf(c_0_41, plain, ![X1524:nat]:(((esk90_0 @ X1524)=(times_times_nat @ (p @ X1524) @ X1524))), introduced(definition)).
% 0.91/0.47 thf(c_0_42, plain, ![X3:nat > nat, X1:set_nat]:((((groups1842438620at_nat @ X3 @ X1)=(zero_zero_nat))|((X3 @ (esk15_2 @ X3 @ X1))!=(zero_zero_nat)))), inference(split_conjunct,[status(thm)],[c_0_38])).
% 0.91/0.47 thf(c_0_43, plain, ![X2:nat]:(((esk90_0 @ X2)=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 0.91/0.47 thf(c_0_44, 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_17]), c_0_41])).
% 0.91/0.47 thf(c_0_45, plain, ![X1:set_nat]:(((groups1842438620at_nat @ esk90_0 @ X1)=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 0.91/0.47 thf(c_0_46, plain, ![X889:nat, X890:nat]:(((((times_times_nat @ X889 @ X890)!=(zero_zero_nat))|(((X889)=(zero_zero_nat))|((X890)=(zero_zero_nat))))&((((X889)!=(zero_zero_nat))|((times_times_nat @ X889 @ X890)=(zero_zero_nat)))&(((X890)!=(zero_zero_nat))|((times_times_nat @ X889 @ X890)=(zero_zero_nat)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_13_mult__eq__0__iff])])])])).
% 0.91/0.47 thf(c_0_47, 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_17])).
% 0.91/0.47 thf(c_0_48, negated_conjecture, (((p @ esk1_0)!=(zero_zero_nat))|((p @ esk2_0)!=(zero_zero_nat))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_45])])).
% 0.91/0.47 thf(c_0_49, plain, ![X2:nat, X4:nat]:((((X2)=(zero_zero_nat))|((X4)=(zero_zero_nat))|((times_times_nat @ X2 @ X4)!=(zero_zero_nat)))), inference(split_conjunct,[status(thm)],[c_0_46])).
% 0.91/0.47 thf(c_0_50, plain, ![X2:nat]:(((times_times_nat @ X2 @ (p @ X2))=(zero_zero_nat))), inference(rw,[status(thm)],[c_0_26, c_0_43])).
% 0.91/0.47 thf(c_0_51, negated_conjecture, ![X2:nat]:((((p @ X2)=(zero_zero_nat))|(ord_less_eq_nat @ one_one_nat @ X2))), inference(ef,[status(thm)],[c_0_47])).
% 0.91/0.47 thf(c_0_52, 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])])])).
% 0.91/0.47 thf(c_0_53, negated_conjecture, ((ord_less_eq_nat @ esk2_0 @ zero_zero_nat)|((p @ esk1_0)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_48, c_0_27])).
% 0.91/0.47 thf(c_0_54, plain, ![X2:nat]:((((p @ X2)=(zero_zero_nat))|((X2)=(zero_zero_nat)))), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 0.91/0.47 thf(c_0_55, plain, ![X893:nat]:((ord_less_eq_nat @ zero_zero_nat @ X893)), inference(variable_rename,[status(thm)],[fact_16_bot__nat__0_Oextremum])).
% 0.91/0.47 thf(c_0_56, plain, ~(ord_less_eq_nat @ one_one_nat @ zero_zero_nat), inference(fof_simplification,[status(thm)],[fact_75_not__one__le__zero])).
% 0.91/0.47 thf(c_0_57, negated_conjecture, ((ord_less_eq_nat @ one_one_nat @ esk2_0)|((p @ esk1_0)!=(zero_zero_nat))), inference(spm,[status(thm)],[c_0_48, c_0_51])).
% 0.91/0.47 thf(c_0_58, 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_52])).
% 0.91/0.47 thf(c_0_59, plain, (((esk1_0)=(zero_zero_nat))|(ord_less_eq_nat @ esk2_0 @ zero_zero_nat)), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 0.91/0.47 thf(c_0_60, plain, ![X2:nat]:((ord_less_eq_nat @ zero_zero_nat @ X2)), inference(split_conjunct,[status(thm)],[c_0_55])).
% 0.91/0.47 thf(c_0_61, plain, ~(ord_less_eq_nat @ one_one_nat @ zero_zero_nat), inference(fof_nnf,[status(thm)],[c_0_56])).
% 0.91/0.47 thf(c_0_62, plain, (((esk1_0)=(zero_zero_nat))|(ord_less_eq_nat @ one_one_nat @ esk2_0)), inference(spm,[status(thm)],[c_0_57, c_0_54])).
% 0.91/0.47 thf(c_0_63, plain, (((esk1_0)=(zero_zero_nat))|((esk2_0)=(zero_zero_nat))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60])])).
% 0.91/0.47 thf(c_0_64, plain, ~((ord_less_eq_nat @ one_one_nat @ zero_zero_nat)), inference(split_conjunct,[status(thm)],[c_0_61])).
% 0.91/0.47 thf(c_0_65, negated_conjecture, ((ord_less_eq_nat @ one_one_nat @ esk1_0)|(ord_less_eq_nat @ esk2_0 @ zero_zero_nat)), inference(spm,[status(thm)],[c_0_53, c_0_51])).
% 0.91/0.47 thf(c_0_66, negated_conjecture, ((ord_less_eq_nat @ one_one_nat @ esk1_0)|(ord_less_eq_nat @ one_one_nat @ esk2_0)), inference(spm,[status(thm)],[c_0_57, c_0_51])).
% 0.91/0.47 thf(c_0_67, plain, ((esk1_0)=(zero_zero_nat)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_64])).
% 0.91/0.47 thf(c_0_68, negated_conjecture, (((esk2_0)=(zero_zero_nat))|(ord_less_eq_nat @ one_one_nat @ esk1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_65]), c_0_60])])).
% 0.91/0.47 thf(c_0_69, negated_conjecture, (ord_less_eq_nat @ one_one_nat @ esk2_0), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67]), c_0_64])).
% 0.91/0.47 thf(c_0_70, negated_conjecture, ((esk2_0)=(zero_zero_nat)), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_67]), c_0_64])).
% 0.91/0.47 thf(c_0_71, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70]), c_0_64]), ['proof']).
% 0.91/0.47 % SZS output end CNFRefutation
% 0.91/0.47 % Parsed axioms : 283
% 0.91/0.47 % Removed by relevancy pruning/SinE : 45
% 0.91/0.47 % Initial clauses : 513
% 0.91/0.47 % Removed in clause preprocessing : 21
% 0.91/0.47 % Initial clauses in saturation : 492
% 0.91/0.47 % Processed clauses : 1912
% 0.91/0.47 % ...of these trivial : 78
% 0.91/0.47 % ...subsumed : 1201
% 0.91/0.47 % ...remaining for further processing : 633
% 0.91/0.47 % Other redundant clauses eliminated : 63
% 0.91/0.47 % Clauses deleted for lack of memory : 0
% 0.91/0.47 % Backward-subsumed : 38
% 0.91/0.47 % Backward-rewritten : 92
% 0.91/0.47 % Generated clauses : 8034
% 0.91/0.47 % ...of the previous two non-redundant : 6241
% 0.91/0.47 % ...aggressively subsumed : 0
% 0.91/0.47 % Contextual simplify-reflections : 0
% 0.91/0.47 % Paramodulations : 7958
% 0.91/0.47 % Factorizations : 12
% 0.91/0.47 % NegExts : 0
% 0.91/0.47 % Equation resolutions : 66
% 0.91/0.47 % Disequality decompositions : 0
% 0.91/0.47 % Total rewrite steps : 2651
% 0.91/0.47 % ...of those cached : 2030
% 0.91/0.47 % Propositional unsat checks : 0
% 0.91/0.47 % Propositional check models : 0
% 0.91/0.47 % Propositional check unsatisfiable : 0
% 0.91/0.47 % Propositional clauses : 0
% 0.91/0.47 % Propositional clauses after purity: 0
% 0.91/0.47 % Propositional unsat core size : 0
% 0.91/0.47 % Propositional preprocessing time : 0.000
% 0.91/0.47 % Propositional encoding time : 0.000
% 0.91/0.47 % Propositional solver time : 0.000
% 0.91/0.47 % Success case prop preproc time : 0.000
% 0.91/0.47 % Success case prop encoding time : 0.000
% 0.91/0.47 % Success case prop solver time : 0.000
% 0.91/0.47 % Current number of processed clauses : 443
% 0.91/0.47 % Positive orientable unit clauses : 173
% 0.91/0.47 % Positive unorientable unit clauses: 4
% 0.91/0.47 % Negative unit clauses : 78
% 0.91/0.47 % Non-unit-clauses : 188
% 0.91/0.47 % Current number of unprocessed clauses: 4705
% 0.91/0.47 % ...number of literals in the above : 9879
% 0.91/0.47 % Current number of archived formulas : 0
% 0.91/0.47 % Current number of archived clauses : 130
% 0.91/0.47 % Clause-clause subsumption calls (NU) : 10928
% 0.91/0.47 % Rec. Clause-clause subsumption calls : 9219
% 0.91/0.47 % Non-unit clause-clause subsumptions : 570
% 0.91/0.47 % Unit Clause-clause subsumption calls : 2181
% 0.91/0.47 % Rewrite failures with RHS unbound : 0
% 0.91/0.47 % BW rewrite match attempts : 716
% 0.91/0.47 % BW rewrite match successes : 62
% 0.91/0.47 % Condensation attempts : 0
% 0.91/0.47 % Condensation successes : 0
% 0.91/0.47 % Termbank termtop insertions : 122316
% 0.91/0.47 % Search garbage collected termcells : 10441
% 0.91/0.47
% 0.91/0.47 % -------------------------------------------------
% 0.91/0.47 % User time : 0.167 s
% 0.91/0.47 % System time : 0.017 s
% 0.91/0.47 % Total time : 0.184 s
% 0.91/0.47 % Maximum resident set size: 5932 pages
% 0.91/0.47
% 0.91/0.47 % -------------------------------------------------
% 0.91/0.47 % User time : 0.509 s
% 0.91/0.47 % System time : 0.055 s
% 0.91/0.47 % Total time : 0.565 s
% 0.91/0.47 % Maximum resident set size: 5376 pages
% 0.91/0.47 % E exiting
%------------------------------------------------------------------------------