%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : NUM768^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:17:04 AM UTC 2026
% Result : Theorem 1.78s 0.58s
% Output : CNFRefutation 1.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM768^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.23 % Computer : n018.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Tue Sep 29 12:56:26 UTC 2026
% 0.11/0.23 % CPUTime :
% 0.11/0.24 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.29 Running higher-order theorem proving
% 0.24/0.30 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.NfIvEGhApS/E---3.1_28596.p
% 1.78/0.58 % Version: 3.5.1-ho
% 1.78/0.58 % partial match(1): HSSSSMSSSSMCSSA
% 1.78/0.58 % Preprocessing class: HSMSSMSSSSMCSSA.
% 1.78/0.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.78/0.58 % Starting ho_unfolding_3 with 1500s (5) cores
% 1.78/0.58 % Starting ehoh_best_sine_rwall with 300s (1) cores
% 1.78/0.58 % Starting new_bool_3 with 300s (1) cores
% 1.78/0.58 % Starting new_bool_1 with 300s (1) cores
% 1.78/0.58 % ho_unfolding_3 with pid 28609 completed with status 0
% 1.78/0.58 % Result found by ho_unfolding_3
% 1.78/0.58 % partial match(1): HSSSSMSSSSMCSSA
% 1.78/0.58 % Preprocessing class: HSMSSMSSSSMCSSA.
% 1.78/0.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.78/0.58 % Starting ho_unfolding_3 with 1500s (5) cores
% 1.78/0.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.78/0.58 % No SInE strategy applied
% 1.78/0.58 % Search class: HHUSM-FFSF21-DSSFFFBN
% 1.78/0.58 % partial match(4): FHUSM-FFSF21-DFFFFFNN
% 1.78/0.58 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 1.78/0.58 % Starting SubtermCWHack with 136s (1) cores
% 1.78/0.58 % Starting ho_unfolding_3 with 151s (1) cores
% 1.78/0.58 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S04AN with 271s (1) cores
% 1.78/0.58 % Starting new_bool_3 with 271s (1) cores
% 1.78/0.58 % Starting U----_206d_02_B11_00_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 1.78/0.58 % new_bool_3 with pid 28617 completed with status 0
% 1.78/0.58 % Result found by new_bool_3
% 1.78/0.58 % partial match(1): HSSSSMSSSSMCSSA
% 1.78/0.58 % Preprocessing class: HSMSSMSSSSMCSSA.
% 1.78/0.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.78/0.58 % Starting ho_unfolding_3 with 1500s (5) cores
% 1.78/0.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.78/0.58 % No SInE strategy applied
% 1.78/0.58 % Search class: HHUSM-FFSF21-DSSFFFBN
% 1.78/0.58 % partial match(4): FHUSM-FFSF21-DFFFFFNN
% 1.78/0.58 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 1.78/0.58 % Starting SubtermCWHack with 136s (1) cores
% 1.78/0.58 % Starting ho_unfolding_3 with 151s (1) cores
% 1.78/0.58 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S04AN with 271s (1) cores
% 1.78/0.58 % Starting new_bool_3 with 271s (1) cores
% 1.78/0.58 % Preprocessing time : 0.002 s
% 1.78/0.58 % Presaturation interreduction done
% 1.78/0.58
% 1.78/0.58 % Proof found!
% 1.78/0.58 % SZS status Theorem
% 1.78/0.58 % SZS output start CNFRefutation
% 1.78/0.58 thf(decl_sort1, type, frac: $tType).
% 1.78/0.58 thf(decl_sort2, type, nat: $tType).
% 1.78/0.58 thf(decl_23, type, x: frac).
% 1.78/0.58 thf(decl_24, type, y: frac).
% 1.78/0.58 thf(decl_25, type, some: (nat > $o) > $o).
% 1.78/0.58 thf(decl_26, type, ts: nat > nat > nat).
% 1.78/0.58 thf(decl_27, type, num: frac > nat).
% 1.78/0.58 thf(decl_28, type, den: frac > nat).
% 1.78/0.58 thf(decl_29, type, pl: nat > nat > nat).
% 1.78/0.58 thf(decl_30, type, eq: frac > frac > $o).
% 1.78/0.58 thf(decl_31, type, pf: frac > frac > frac).
% 1.78/0.58 thf(decl_32, type, fr: nat > nat > frac).
% 1.78/0.58 thf(decl_33, type, ind: (nat > $o) > nat).
% 1.78/0.58 thf(decl_34, type, amone: (nat > $o) > $o).
% 1.78/0.58 thf(decl_35, type, epred1_0: nat > $o).
% 1.78/0.58 thf(decl_36, type, epred2_2: nat > nat > nat > $o).
% 1.78/0.58 thf(decl_41, type, esk7_2: nat > nat > nat).
% 1.78/0.58 thf(satz8b, axiom, ![X2:nat, X3:nat]:((amone @ (^[X4:nat]:(((X2)=(pl @ X3 @ X4)))))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz8b)).
% 1.78/0.58 thf(satz29, axiom, ![X2:nat, X3:nat]:(((ts @ X2 @ X3)=(ts @ X3 @ X2))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz29)).
% 1.78/0.58 thf(oneax, axiom, ![X17:nat > $o]:((~(((amone @ X17)=>~((some @ X17))))=>(X17 @ (ind @ X17)))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', oneax)).
% 1.78/0.58 thf(satz67c, conjecture, (eq @ (pf @ y @ (fr @ (ind @ (^[X19:nat]:(((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ X19))))) @ (ts @ (den @ x) @ (den @ y)))) @ x), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz67c)).
% 1.78/0.58 thf(satz57, axiom, ![X15:nat, X16:nat, X13:nat]:((eq @ (pf @ (fr @ X15 @ X13) @ (fr @ X16 @ X13)) @ (fr @ (pl @ X15 @ X16) @ X13))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz57)).
% 1.78/0.58 thf(satz56, axiom, ![X8:frac, X9:frac, X10:frac, X11:frac]:(((eq @ X8 @ X9)=>((eq @ X10 @ X11)=>(eq @ (pf @ X8 @ X10) @ (pf @ X9 @ X11))))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz56)).
% 1.78/0.58 thf(satz37, axiom, ![X14:frac]:((eq @ X14 @ X14)), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz37)).
% 1.78/0.58 thf(satz40, axiom, ![X12:frac, X13:nat]:((eq @ X12 @ (fr @ (ts @ (num @ X12) @ X13) @ (ts @ (den @ X12) @ X13)))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz40)).
% 1.78/0.58 thf(m, axiom, (some @ (^[X1:nat]:(((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ X1))))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', m)).
% 1.78/0.58 thf(satz39, axiom, ![X5:frac, X6:frac, X7:frac]:(((eq @ X5 @ X6)=>((eq @ X6 @ X7)=>(eq @ X5 @ X7)))), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz39)).
% 1.78/0.58 thf(satz40a, axiom, ![X18:frac, X13:nat]:((eq @ (fr @ (ts @ (num @ X18) @ X13) @ (ts @ (den @ X18) @ X13)) @ X18)), file('/export/starexec/sandbox2/tmp/tmp.NfIvEGhApS/E---3.1_28596.p', satz40a)).
% 1.78/0.58 thf(c_0_11, plain, ![X2:nat, X3:nat]:((amone @ (^[Z0:nat]:(((X2)=(pl @ X3 @ Z0)))))), inference(fof_simplification,[status(thm)],[satz8b])).
% 1.78/0.58 thf(c_0_12, plain, ![X63:nat]:(((~(epred1_0 @ X63)|((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ X63)))&(((ts @ (num @ x) @ (den @ y))!=(pl @ (ts @ (num @ y) @ (den @ x)) @ X63))|(epred1_0 @ X63)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 1.78/0.58 thf(c_0_13, plain, ![X52:nat, X53:nat]:(((ts @ X52 @ X53)=(ts @ X53 @ X52))), inference(variable_rename,[status(thm)],[satz29])).
% 1.78/0.58 thf(c_0_14, plain, ![X17:nat > $o]:((~(((amone @ X17)=>~(some @ X17)))=>(X17 @ (ind @ X17)))), inference(fof_simplification,[status(thm)],[oneax])).
% 1.78/0.58 thf(c_0_15, plain, ![X40:nat, X41:nat]:((amone @ (^[Z0:nat]:(((X40)=(pl @ X41 @ Z0)))))), inference(variable_rename,[status(thm)],[c_0_11])).
% 1.78/0.58 thf(c_0_16, plain, ![X61:nat, X1:nat, X2:nat]:(((epred2_2 @ X2 @ X1 @ X61)<=>((X1)=(pl @ X2 @ X61)))), introduced(definition)).
% 1.78/0.58 thf(c_0_17, negated_conjecture, ~((eq @ (pf @ y @ (fr @ (ind @ (^[X19:nat]:(((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ X19))))) @ (ts @ (den @ x) @ (den @ y)))) @ x)), inference(assume_negation,[status(cth)],[satz67c])).
% 1.78/0.58 thf(c_0_18, plain, ![X54:nat, X55:nat, X56:nat]:((eq @ (pf @ (fr @ X54 @ X56) @ (fr @ X55 @ X56)) @ (fr @ (pl @ X54 @ X55) @ X56))), inference(variable_rename,[status(thm)],[satz57])).
% 1.78/0.58 thf(c_0_19, plain, ![X1:nat]:((((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ X1))|~((epred1_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.78/0.58 thf(c_0_20, plain, ![X2:nat, X1:nat]:(((ts @ X1 @ X2)=(ts @ X2 @ X1))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.78/0.58 thf(c_0_21, plain, ![X45:frac, X46:frac, X47:frac, X48:frac]:((~(eq @ X45 @ X46)|(~(eq @ X47 @ X48)|(eq @ (pf @ X45 @ X47) @ (pf @ X46 @ X48))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[satz56])])])).
% 1.78/0.58 thf(c_0_22, plain, ![X51:frac]:((eq @ X51 @ X51)), inference(variable_rename,[status(thm)],[satz37])).
% 1.78/0.58 thf(c_0_23, plain, ![X49:frac, X50:nat]:((eq @ X49 @ (fr @ (ts @ (num @ X49) @ X50) @ (ts @ (den @ X49) @ X50)))), inference(variable_rename,[status(thm)],[satz40])).
% 1.78/0.58 thf(c_0_24, plain, ![X64:nat, X65:nat, X66:nat]:(((~(epred2_2 @ X66 @ X65 @ X64)|((X65)=(pl @ X66 @ X64)))&(((X65)!=(pl @ X66 @ X64))|(epred2_2 @ X66 @ X65 @ X64)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 1.78/0.58 thf(c_0_25, plain, ![X57:nat > $o]:((~(amone @ X57)|~(some @ X57)|(X57 @ (ind @ X57)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])).
% 1.78/0.58 thf(c_0_26, plain, ![X2:nat, X1:nat]:((((amone @ (epred2_2 @ X2 @ X1)))=(($true)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_15]), c_0_16])).
% 1.78/0.58 thf(c_0_27, plain, (some @ (^[Z0:nat]:(((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ Z0))))), inference(fof_simplification,[status(thm)],[m])).
% 1.78/0.58 thf(c_0_28, plain, ![X60:nat]:(((epred1_0 @ X60)<=>((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ X60)))), introduced(definition)).
% 1.78/0.58 thf(c_0_29, negated_conjecture, ~(eq @ (pf @ y @ (fr @ (ind @ (^[Z0:nat]:(((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ Z0))))) @ (ts @ (den @ x) @ (den @ y)))) @ x), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_17])])).
% 1.78/0.58 thf(c_0_30, plain, ![X42:frac, X43:frac, X44:frac]:((~(eq @ X42 @ X43)|(~(eq @ X43 @ X44)|(eq @ X42 @ X44)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[satz39])])])).
% 1.78/0.58 thf(c_0_31, plain, ![X58:frac, X59:nat]:((eq @ (fr @ (ts @ (num @ X58) @ X59) @ (ts @ (den @ X58) @ X59)) @ X58)), inference(variable_rename,[status(thm)],[satz40a])).
% 1.78/0.58 thf(c_0_32, plain, ![X1:nat, X3:nat, X2:nat]:((eq @ (pf @ (fr @ X1 @ X2) @ (fr @ X3 @ X2)) @ (fr @ (pl @ X1 @ X3) @ X2))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.78/0.58 thf(c_0_33, plain, ![X1:nat]:((((pl @ (ts @ (den @ x) @ (num @ y)) @ X1)=(ts @ (den @ y) @ (num @ x)))|~((epred1_0 @ X1)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20]), c_0_20])).
% 1.78/0.58 thf(c_0_34, plain, ![X5:frac, X6:frac, X7:frac, X8:frac]:(((eq @ (pf @ X5 @ X7) @ (pf @ X6 @ X8))|~((eq @ X5 @ X6))|~((eq @ X7 @ X8)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.78/0.58 thf(c_0_35, plain, ![X5:frac]:((eq @ X5 @ X5)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 1.78/0.58 thf(c_0_36, plain, ![X5:frac, X1:nat]:((eq @ X5 @ (fr @ (ts @ (num @ X5) @ X1) @ (ts @ (den @ X5) @ X1)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 1.78/0.58 thf(c_0_37, plain, ![X1:nat, X2:nat, X3:nat]:((((X2)=(pl @ X1 @ X3))|~((epred2_2 @ X1 @ X2 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.78/0.58 thf(c_0_38, plain, ![X17:nat > $o]:(((X17 @ (ind @ X17))|~((amone @ X17))|~((some @ X17)))), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.78/0.58 thf(c_0_39, plain, ![X1:nat, X2:nat]:((amone @ (epred2_2 @ X1 @ X2))), inference(cn,[status(thm)],[c_0_26])).
% 1.78/0.58 thf(c_0_40, plain, (((some @ epred1_0))=(($true))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_27]), c_0_28])).
% 1.78/0.58 thf(c_0_41, negated_conjecture, ~(eq @ (pf @ y @ (fr @ (ind @ (^[Z0:nat]:(((ts @ (num @ x) @ (den @ y))=(pl @ (ts @ (num @ y) @ (den @ x)) @ Z0))))) @ (ts @ (den @ x) @ (den @ y)))) @ x), inference(fof_nnf,[status(thm)],[c_0_29])).
% 1.78/0.58 thf(c_0_42, plain, ![X5:frac, X6:frac, X7:frac]:(((eq @ X5 @ X7)|~((eq @ X5 @ X6))|~((eq @ X6 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 1.78/0.58 thf(c_0_43, plain, ![X1:nat, X5:frac]:((eq @ (fr @ (ts @ (num @ X5) @ X1) @ (ts @ (den @ X5) @ X1)) @ X5)), inference(split_conjunct,[status(thm)],[c_0_31])).
% 1.78/0.58 thf(c_0_44, plain, ![X1:nat, X2:nat]:(((eq @ (pf @ (fr @ (ts @ (den @ x) @ (num @ y)) @ X1) @ (fr @ X2 @ X1)) @ (fr @ (ts @ (den @ y) @ (num @ x)) @ X1))|~((epred1_0 @ X2)))), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 1.78/0.58 thf(c_0_45, plain, ![X5:frac, X6:frac, X7:frac]:(((eq @ (pf @ X5 @ X6) @ (pf @ X7 @ X6))|~((eq @ X5 @ X7)))), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 1.78/0.58 thf(c_0_46, plain, ![X5:frac, X1:nat]:((eq @ X5 @ (fr @ (ts @ X1 @ (num @ X5)) @ (ts @ (den @ X5) @ X1)))), inference(spm,[status(thm)],[c_0_36, c_0_20])).
% 1.78/0.58 thf(c_0_47, plain, ![X1:nat, X2:nat]:((((pl @ X1 @ (ind @ (epred2_2 @ X1 @ X2)))=(X2))|~((some @ (epred2_2 @ X1 @ X2))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39])])).
% 1.78/0.58 thf(c_0_48, plain, (some @ epred1_0), inference(cn,[status(thm)],[c_0_40])).
% 1.78/0.58 thf(c_0_49, negated_conjecture, ~((((eq @ (pf @ y @ (fr @ (ind @ (epred2_2 @ (ts @ (num @ y) @ (den @ x)) @ (ts @ (num @ x) @ (den @ y)))) @ (ts @ (den @ x) @ (den @ y)))) @ x))=(($true)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_41]), c_0_16])).
% 1.78/0.58 thf(c_0_50, plain, ![X6:frac, X5:frac, X1:nat]:(((eq @ X5 @ X6)|~((eq @ X5 @ (fr @ (ts @ (num @ X6) @ X1) @ (ts @ (den @ X6) @ X1)))))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 1.78/0.58 thf(c_0_51, plain, ![X1:nat, X5:frac, X2:nat]:(((eq @ X5 @ (fr @ (ts @ (den @ y) @ (num @ x)) @ X1))|~((eq @ X5 @ (pf @ (fr @ (ts @ (den @ x) @ (num @ y)) @ X1) @ (fr @ X2 @ X1))))|~((epred1_0 @ X2)))), inference(spm,[status(thm)],[c_0_42, c_0_44])).
% 1.78/0.58 thf(c_0_52, plain, ![X1:nat, X5:frac, X6:frac]:((eq @ (pf @ X5 @ X6) @ (pf @ (fr @ (ts @ X1 @ (num @ X5)) @ (ts @ (den @ X5) @ X1)) @ X6))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 1.78/0.58 thf(c_0_53, plain, ![X1:nat, X2:nat]:((((pl @ X1 @ (ind @ (epred2_2 @ X1 @ X2)))=(X2))|((epred2_2 @ X1 @ X2)!=(epred1_0)))), inference(ext_sup,[status(thm)],[c_0_47, c_0_48])).
% 1.78/0.58 thf(c_0_54, negated_conjecture, ~((eq @ (pf @ y @ (fr @ (ind @ (epred2_2 @ (ts @ (num @ y) @ (den @ x)) @ (ts @ (num @ x) @ (den @ y)))) @ (ts @ (den @ x) @ (den @ y)))) @ x)), inference(cn,[status(thm)],[c_0_49])).
% 1.78/0.58 thf(c_0_55, plain, ![X6:frac, X5:frac, X1:nat]:(((eq @ X5 @ X6)|~((eq @ X5 @ (fr @ (ts @ X1 @ (num @ X6)) @ (ts @ (den @ X6) @ X1)))))), inference(spm,[status(thm)],[c_0_50, c_0_20])).
% 1.78/0.58 thf(c_0_56, plain, ![X1:nat]:(((eq @ (pf @ y @ (fr @ X1 @ (ts @ (den @ x) @ (den @ y)))) @ (fr @ (ts @ (den @ y) @ (num @ x)) @ (ts @ (den @ x) @ (den @ y))))|~((epred1_0 @ X1)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_20]), c_0_20])).
% 1.78/0.58 thf(c_0_57, plain, ![X1:nat, X2:nat, X3:nat]:(((epred2_2 @ X2 @ X1 @ X3)|((X1)!=(pl @ X2 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.78/0.58 thf(c_0_58, plain, ![X1:nat]:(((epred1_0 @ X1)|((ts @ (num @ x) @ (den @ y))!=(pl @ (ts @ (num @ y) @ (den @ x)) @ X1)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.78/0.58 thf(c_0_59, plain, ![X1:nat, X2:nat]:((((pl @ X1 @ (ind @ (epred2_2 @ X1 @ X2)))=(X2))|((epred2_2 @ X1 @ X2 @ (esk7_2 @ X1 @ X2))<~>(epred1_0 @ (esk7_2 @ X1 @ X2))))), inference(neg_ext,[status(thm)],[c_0_53])).
% 1.78/0.58 thf(c_0_60, negated_conjecture, ~((eq @ (pf @ y @ (fr @ (ind @ (epred2_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x)))) @ (ts @ (den @ x) @ (den @ y)))) @ x)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_20]), c_0_20])).
% 1.78/0.58 thf(c_0_61, plain, ![X1:nat]:(((eq @ (pf @ y @ (fr @ X1 @ (ts @ (den @ x) @ (den @ y)))) @ x)|~((epred1_0 @ X1)))), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 1.78/0.58 thf(c_0_62, plain, ![X1:nat, X2:nat]:((epred2_2 @ X1 @ (pl @ X1 @ X2) @ X2)), inference(er,[status(thm)],[c_0_57])).
% 1.78/0.58 thf(c_0_63, plain, ![X1:nat]:(((epred1_0 @ X1)|((pl @ (ts @ (den @ x) @ (num @ y)) @ X1)!=(ts @ (den @ y) @ (num @ x))))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_20]), c_0_20])).
% 1.78/0.58 thf(c_0_64, plain, ![X1:nat, X2:nat]:((((pl @ X1 @ (ind @ (epred2_2 @ X1 @ X2)))=(X2))|(epred2_2 @ X1 @ X2 @ (esk7_2 @ X1 @ X2))|(epred1_0 @ (esk7_2 @ X1 @ X2)))), inference(dynamic_cnf,[status(thm)],[c_0_59])).
% 1.78/0.58 thf(c_0_65, negated_conjecture, ~((epred1_0 @ (ind @ (epred2_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x)))))), inference(spm,[status(thm)],[c_0_60, c_0_61])).
% 1.78/0.58 thf(c_0_66, plain, ![X1:nat]:(((epred2_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x)) @ X1)|~((epred1_0 @ X1)))), inference(spm,[status(thm)],[c_0_62, c_0_33])).
% 1.78/0.58 thf(c_0_67, plain, (epred2_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x)) @ (esk7_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64])]), c_0_65]), c_0_66])).
% 1.78/0.58 thf(c_0_68, plain, ((pl @ (ts @ (den @ x) @ (num @ y)) @ (esk7_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x))))=(ts @ (den @ y) @ (num @ x))), inference(spm,[status(thm)],[c_0_37, c_0_67])).
% 1.78/0.58 thf(c_0_69, plain, ![X1:nat, X2:nat]:((((pl @ X1 @ (ind @ (epred2_2 @ X1 @ X2)))=(X2))|~((epred2_2 @ X1 @ X2 @ (esk7_2 @ X1 @ X2)))|~((epred1_0 @ (esk7_2 @ X1 @ X2))))), inference(dynamic_cnf,[status(thm)],[c_0_59])).
% 1.78/0.58 thf(c_0_70, plain, (epred1_0 @ (esk7_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x)))), inference(spm,[status(thm)],[c_0_63, c_0_68])).
% 1.78/0.58 thf(c_0_71, plain, ((pl @ (ts @ (den @ x) @ (num @ y)) @ (ind @ (epred2_2 @ (ts @ (den @ x) @ (num @ y)) @ (ts @ (den @ y) @ (num @ x)))))=(ts @ (den @ y) @ (num @ x))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_70]), c_0_67])])).
% 1.78/0.58 thf(c_0_72, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_71]), c_0_65]), ['proof']).
% 1.78/0.58 % SZS output end CNFRefutation
% 1.78/0.58 % Parsed axioms : 25
% 1.78/0.58 % Removed by relevancy pruning/SinE : 0
% 1.78/0.58 % Initial clauses : 29
% 1.78/0.58 % Removed in clause preprocessing : 14
% 1.78/0.58 % Initial clauses in saturation : 15
% 1.78/0.58 % Processed clauses : 574
% 1.78/0.58 % ...of these trivial : 51
% 1.78/0.58 % ...subsumed : 238
% 1.78/0.58 % ...remaining for further processing : 285
% 1.78/0.58 % Other redundant clauses eliminated : 2
% 1.78/0.58 % Clauses deleted for lack of memory : 0
% 1.78/0.58 % Backward-subsumed : 6
% 1.78/0.58 % Backward-rewritten : 1
% 1.78/0.58 % Generated clauses : 5391
% 1.78/0.58 % ...of the previous two non-redundant : 4909
% 1.78/0.58 % ...aggressively subsumed : 0
% 1.78/0.58 % Contextual simplify-reflections : 1
% 1.78/0.58 % Paramodulations : 5327
% 1.78/0.58 % Factorizations : 0
% 1.78/0.58 % NegExts : 13
% 1.78/0.58 % Equation resolutions : 3
% 1.78/0.58 % Disequality decompositions : 0
% 1.78/0.58 % Total rewrite steps : 597
% 1.78/0.58 % ...of those cached : 524
% 1.78/0.58 % Propositional unsat checks : 0
% 1.78/0.58 % Propositional check models : 0
% 1.78/0.58 % Propositional check unsatisfiable : 0
% 1.78/0.58 % Propositional clauses : 0
% 1.78/0.58 % Propositional clauses after purity: 0
% 1.78/0.58 % Propositional unsat core size : 0
% 1.78/0.58 % Propositional preprocessing time : 0.000
% 1.78/0.58 % Propositional encoding time : 0.000
% 1.78/0.58 % Propositional solver time : 0.000
% 1.78/0.58 % Success case prop preproc time : 0.000
% 1.78/0.58 % Success case prop encoding time : 0.000
% 1.78/0.58 % Success case prop solver time : 0.000
% 1.78/0.58 % Current number of processed clauses : 250
% 1.78/0.58 % Positive orientable unit clauses : 71
% 1.78/0.58 % Positive unorientable unit clauses: 1
% 1.78/0.58 % Negative unit clauses : 2
% 1.78/0.58 % Non-unit-clauses : 176
% 1.78/0.58 % Current number of unprocessed clauses: 4357
% 1.78/0.58 % ...number of literals in the above : 5781
% 1.78/0.58 % Current number of archived formulas : 0
% 1.78/0.58 % Current number of archived clauses : 34
% 1.78/0.58 % Clause-clause subsumption calls (NU) : 8252
% 1.78/0.58 % Rec. Clause-clause subsumption calls : 7054
% 1.78/0.58 % Non-unit clause-clause subsumptions : 245
% 1.78/0.58 % Unit Clause-clause subsumption calls : 235
% 1.78/0.58 % Rewrite failures with RHS unbound : 0
% 1.78/0.58 % BW rewrite match attempts : 591
% 1.78/0.58 % BW rewrite match successes : 4
% 1.78/0.58 % Condensation attempts : 0
% 1.78/0.58 % Condensation successes : 0
% 1.78/0.58 % Termbank termtop insertions : 210656
% 1.78/0.58 % Search garbage collected termcells : 203
% 1.78/0.58
% 1.78/0.58 % -------------------------------------------------
% 1.78/0.58 % User time : 0.240 s
% 1.78/0.58 % System time : 0.014 s
% 1.78/0.58 % Total time : 0.254 s
% 1.78/0.58 % Maximum resident set size: 3612 pages
% 1.78/0.58
% 1.78/0.58 % -------------------------------------------------
% 1.78/0.58 % User time : 1.189 s
% 1.78/0.58 % System time : 0.075 s
% 1.78/0.58 % Total time : 1.265 s
% 1.78/0.58 % Maximum resident set size: 4608 pages
% 1.78/0.58 % E exiting
%------------------------------------------------------------------------------