%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : NUM730^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:16:57 AM UTC 2026
% Result : Theorem 0.20s 0.27s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM730^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n026.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 12:48:57 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.23 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.u2C3CTKsSB/E---3.1_542001.p
% 0.20/0.27 % Version: 3.5.1-ho
% 0.20/0.27 % Preprocessing class: HSSSSMSSSSSNFFN.
% 0.20/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.20/0.27 % Starting ho_unfolding_6 with 300s (1) cores
% 0.20/0.27 % Starting sh4l with 300s (1) cores
% 0.20/0.27 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 0.20/0.27 % new_ho_10 with pid 542014 completed with status 0
% 0.20/0.27 % Result found by new_ho_10
% 0.20/0.27 % Preprocessing class: HSSSSMSSSSSNFFN.
% 0.20/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.20/0.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/0.27 % No SInE strategy applied
% 0.20/0.27 % Search class: HGHSF-FFMF21-SFFFFFNN
% 0.20/0.27 % partial match(1): FGHSF-FFMF21-SFFFFFNN
% 0.20/0.27 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.20/0.27 % Starting SubtermCWHack with 136s (1) cores
% 0.20/0.27 % Starting new_ho_10 with 151s (1) cores
% 0.20/0.27 % Starting G-E--_208_B07----S_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 0.20/0.27 % Starting new_bool_3 with 136s (1) cores
% 0.20/0.27 % Starting G-E--_208_B00_00_F1_SE_CS_SP_PS_S033N with 136s (1) cores
% 0.20/0.27 % new_ho_10 with pid 542019 completed with status 0
% 0.20/0.27 % Result found by new_ho_10
% 0.20/0.27 % Preprocessing class: HSSSSMSSSSSNFFN.
% 0.20/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.20/0.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/0.27 % No SInE strategy applied
% 0.20/0.27 % Search class: HGHSF-FFMF21-SFFFFFNN
% 0.20/0.27 % partial match(1): FGHSF-FFMF21-SFFFFFNN
% 0.20/0.27 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.20/0.27 % Starting SubtermCWHack with 136s (1) cores
% 0.20/0.27 % Starting new_ho_10 with 151s (1) cores
% 0.20/0.27 % Preprocessing time : 0.002 s
% 0.20/0.27 % Presaturation interreduction done
% 0.20/0.27
% 0.20/0.27 % Proof found!
% 0.20/0.27 % SZS status Theorem
% 0.20/0.27 % SZS output start CNFRefutation
% 0.20/0.27 thf(decl_sort1, type, frac: $tType).
% 0.20/0.27 thf(decl_sort2, type, nat: $tType).
% 0.20/0.27 thf(decl_23, type, x: frac).
% 0.20/0.27 thf(decl_24, type, y: frac).
% 0.20/0.27 thf(decl_25, type, orec3: $o > $o > $o > $o).
% 0.20/0.27 thf(decl_26, type, ts: nat > nat > nat).
% 0.20/0.27 thf(decl_27, type, c1x: frac > nat).
% 0.20/0.27 thf(decl_28, type, c2y: frac > nat).
% 0.20/0.27 thf(decl_29, type, c1y: frac > nat).
% 0.20/0.27 thf(decl_30, type, c2x: frac > nat).
% 0.20/0.27 thf(decl_31, type, more: nat > nat > $o).
% 0.20/0.27 thf(decl_32, type, less: nat > nat > $o).
% 0.20/0.27 thf(decl_33, type, epred1_0: $o).
% 0.20/0.27 thf(decl_34, type, epred2_0: $o).
% 0.20/0.27 thf(satz10, axiom, ![X1:nat, X2:nat]:((orec3 @ (((X1)=(X2))) @ ((more @ X1 @ X2)) @ ((less @ X1 @ X2)))), file('/export/starexec/sandbox/tmp/tmp.u2C3CTKsSB/E---3.1_542001.p', satz10)).
% 0.20/0.27 thf(satz41, conjecture, (orec3 @ (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))) @ ((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))) @ ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))), file('/export/starexec/sandbox/tmp/tmp.u2C3CTKsSB/E---3.1_542001.p', satz41)).
% 0.20/0.27 thf(c_0_2, plain, ((epred1_0)<=>(((ts @ (c1x @ x) @ (c2y @ y))!=(ts @ (c1y @ y) @ (c2x @ x)))|((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $true @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $true @ $false))))&((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $false @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $false @ $false))))))), introduced(definition)).
% 0.20/0.27 thf(c_0_3, axiom, ![X1:nat, X2:nat]:(((((X1)!=(X2))|((~(more @ X1 @ X2)|((~(less @ X1 @ X2)|(orec3 @ $true @ $true @ $true))&((less @ X1 @ X2)|(orec3 @ $true @ $true @ $false))))&((more @ X1 @ X2)|((~(less @ X1 @ X2)|(orec3 @ $true @ $false @ $true))&((less @ X1 @ X2)|(orec3 @ $true @ $false @ $false))))))&(((X1)=(X2))|((~(more @ X1 @ X2)|((~(less @ X1 @ X2)|(orec3 @ $false @ $true @ $true))&((less @ X1 @ X2)|(orec3 @ $false @ $true @ $false))))&((more @ X1 @ X2)|((~(less @ X1 @ X2)|(orec3 @ $false @ $false @ $true))&((less @ X1 @ X2)|(orec3 @ $false @ $false @ $false)))))))), inference(fool_unroll,[status(thm)],[satz10])).
% 0.20/0.27 thf(c_0_4, plain, ((((ts @ (c1x @ x) @ (c2y @ y))!=(ts @ (c1y @ y) @ (c2x @ x)))|((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $true @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $true @ $false))))&((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $false @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $true @ $false @ $false))))))=>(epred1_0)), inference(split_equiv,[status(thm)],[c_0_2])).
% 0.20/0.27 thf(c_0_5, plain, ![X5:nat, X6:nat]:(((((~(less @ X5 @ X6)|(orec3 @ $true @ $true @ $true)|~(more @ X5 @ X6)|((X5)!=(X6)))&((less @ X5 @ X6)|(orec3 @ $true @ $true @ $false)|~(more @ X5 @ X6)|((X5)!=(X6))))&((~(less @ X5 @ X6)|(orec3 @ $true @ $false @ $true)|(more @ X5 @ X6)|((X5)!=(X6)))&((less @ X5 @ X6)|(orec3 @ $true @ $false @ $false)|(more @ X5 @ X6)|((X5)!=(X6)))))&(((~(less @ X5 @ X6)|(orec3 @ $false @ $true @ $true)|~(more @ X5 @ X6)|((X5)=(X6)))&((less @ X5 @ X6)|(orec3 @ $false @ $true @ $false)|~(more @ X5 @ X6)|((X5)=(X6))))&((~(less @ X5 @ X6)|(orec3 @ $false @ $false @ $true)|(more @ X5 @ X6)|((X5)=(X6)))&((less @ X5 @ X6)|(orec3 @ $false @ $false @ $false)|(more @ X5 @ X6)|((X5)=(X6))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_3])])])).
% 0.20/0.27 thf(c_0_6, plain, ((((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0))&(((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $false @ $true)|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|~(orec3 @ $true @ $false @ $true)|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)))))&((((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|~(orec3 @ $true @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0)))))&((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $true @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $true @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $true @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $false @ $true)|(~(orec3 @ $true @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|~(orec3 @ $true @ $false @ $true)|(~(orec3 @ $true @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred1_0))))))&(((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $true @ $true))|(epred1_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $true @ $true))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $true @ $true))|(epred1_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $true @ $true))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|~(orec3 @ $true @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $true @ $true))|(epred1_0)))))&((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $true @ $true @ $false)|~(orec3 @ $true @ $true @ $true))|(epred1_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $true @ $true @ $false)|~(orec3 @ $true @ $true @ $true))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $true @ $true @ $false)|~(orec3 @ $true @ $true @ $true))|(epred1_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $true @ $false @ $true)|(~(orec3 @ $true @ $true @ $false)|~(orec3 @ $true @ $true @ $true))|(epred1_0))&(~(orec3 @ $true @ $false @ $false)|~(orec3 @ $true @ $false @ $true)|(~(orec3 @ $true @ $true @ $false)|~(orec3 @ $true @ $true @ $true))|(epred1_0))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])).
% 0.20/0.27 thf(c_0_7, plain, ![X1:nat, X2:nat]:(((orec3 @ (($true)) @ (($true)) @ (($true)))|~((less @ X1 @ X2))|~((more @ X1 @ X2))|((X1)!=(X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_8, plain, ![X1:nat, X2:nat]:(((less @ X1 @ X2)|(orec3 @ (($true)) @ (($true)) @ (~($true)))|~((more @ X1 @ X2))|((X1)!=(X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_9, plain, ((epred1_0)|~((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (($true)) @ (($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.20/0.27 thf(c_0_10, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.20/0.27 thf(c_0_11, plain, ![X1:nat]:(((orec3 @ (($true)) @ (($true)) @ (($true)))|~((more @ X1 @ X1))|~((less @ X1 @ X1)))), inference(er,[status(thm)],[c_0_7])).
% 0.20/0.27 thf(c_0_12, plain, ((epred2_0)<=>(((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $true @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $true @ $false))))&((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $false @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $false @ $false))))))), introduced(definition)).
% 0.20/0.27 thf(c_0_13, negated_conjecture, ~((orec3 @ (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))) @ ((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))) @ ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))))), inference(assume_negation,[status(cth)],[satz41])).
% 0.20/0.27 thf(c_0_14, plain, ![X1:nat, X2:nat]:(((orec3 @ (($true)) @ (~($true)) @ (($true)))|(more @ X1 @ X2)|~((less @ X1 @ X2))|((X1)!=(X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_15, plain, ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)|~((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (($true)) @ (($true)) @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.20/0.27 thf(c_0_16, plain, ![X1:nat]:(((orec3 @ (($true)) @ (($true)) @ (~($true)))|(less @ X1 @ X1)|~((more @ X1 @ X1)))), inference(er,[status(thm)],[c_0_8])).
% 0.20/0.27 thf(c_0_17, plain, ((epred1_0)|~((more @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((less @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_9, c_0_10]), c_0_11])).
% 0.20/0.27 thf(c_0_18, plain, ((((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $true @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $true @ $false))))&((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $false @ $true))&((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ $false @ $false @ $false))))))=>(epred2_0)), inference(split_equiv,[status(thm)],[c_0_12])).
% 0.20/0.27 thf(c_0_19, negated_conjecture, ~(((epred1_0)&(epred2_0))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_13]), c_0_2]), c_0_12])).
% 0.20/0.27 thf(c_0_20, plain, ![X1:nat, X2:nat]:(((less @ X1 @ X2)|(orec3 @ (($true)) @ (~($true)) @ (~($true)))|(more @ X1 @ X2)|((X1)!=(X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_21, plain, ((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (($true)) @ (~($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.20/0.27 thf(c_0_22, plain, ![X1:nat]:(((orec3 @ (($true)) @ (~($true)) @ (($true)))|(more @ X1 @ X1)|~((less @ X1 @ X1)))), inference(er,[status(thm)],[c_0_14])).
% 0.20/0.27 thf(c_0_23, plain, ((epred1_0)|~((more @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_10]), c_0_16]), c_0_17])).
% 0.20/0.27 thf(c_0_24, plain, ((((ts @ (c1x @ x) @ (c2y @ y))!=(ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0))&(((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $false @ $true)|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|~(orec3 @ $false @ $false @ $true)|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0)))))&((((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|~(orec3 @ $false @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0)))))&((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $false @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $false @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $false @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $false @ $true)|(~(orec3 @ $false @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|~(orec3 @ $false @ $false @ $true)|(~(orec3 @ $false @ $true @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|(epred2_0))))))&(((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $true @ $true))|(epred2_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $true @ $true))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $true @ $true))|(epred2_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $true @ $true))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|~(orec3 @ $false @ $false @ $true)|(~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $true @ $true))|(epred2_0)))))&((~(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $false @ $true @ $false)|~(orec3 @ $false @ $true @ $true))|(epred2_0))&(((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $false @ $true @ $false)|~(orec3 @ $false @ $true @ $true))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(~(orec3 @ $false @ $true @ $false)|~(orec3 @ $false @ $true @ $true))|(epred2_0)))&((~(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~(orec3 @ $false @ $false @ $true)|(~(orec3 @ $false @ $true @ $false)|~(orec3 @ $false @ $true @ $true))|(epred2_0))&(~(orec3 @ $false @ $false @ $false)|~(orec3 @ $false @ $false @ $true)|(~(orec3 @ $false @ $true @ $false)|~(orec3 @ $false @ $true @ $true))|(epred2_0))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])).
% 0.20/0.27 thf(c_0_25, plain, ![X1:nat, X2:nat]:(((orec3 @ (~($true)) @ (($true)) @ (($true)))|((X1)=(X2))|~((less @ X1 @ X2))|~((more @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_26, plain, ![X1:nat, X2:nat]:(((orec3 @ (~($true)) @ (~($true)) @ (($true)))|(more @ X1 @ X2)|((X1)=(X2))|~((less @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_27, negated_conjecture, (~(epred1_0)|~(epred2_0)), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])).
% 0.20/0.27 thf(c_0_28, plain, ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)|~((orec3 @ (($true)) @ (~($true)) @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.20/0.27 thf(c_0_29, plain, ![X1:nat]:(((orec3 @ (($true)) @ (~($true)) @ (~($true)))|(more @ X1 @ X1)|(less @ X1 @ X1))), inference(er,[status(thm)],[c_0_20])).
% 0.20/0.27 thf(c_0_30, plain, ((epred1_0)|~((less @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_10]), c_0_22]), c_0_23])).
% 0.20/0.27 thf(c_0_31, plain, ((epred2_0)|~((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_32, plain, ![X1:nat, X2:nat]:((((X1)=(X2))|(orec3 @ (~($true)) @ (~($true)) @ (($true)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))|~((less @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 0.20/0.27 thf(c_0_33, plain, ((epred2_0)|((ts @ (c1x @ x) @ (c2y @ y))!=(ts @ (c1y @ y) @ (c2x @ x)))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_34, negated_conjecture, (~((epred1_0))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.20/0.27 thf(c_0_35, plain, (epred1_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_10]), c_0_29]), c_0_30]), c_0_23])).
% 0.20/0.27 thf(c_0_36, plain, ![X1:nat, X2:nat]:(((less @ X1 @ X2)|(orec3 @ (~($true)) @ (($true)) @ (~($true)))|((X1)=(X2))|~((more @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_37, plain, ![X1:nat, X2:nat]:(((less @ X1 @ X2)|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))|(more @ X1 @ X2)|((X1)=(X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.20/0.27 thf(c_0_38, plain, ((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0)|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_39, plain, ((orec3 @ (~($true)) @ (~($true)) @ (($true)))|(epred2_0)|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_26]), c_0_32]), c_0_33])).
% 0.20/0.27 thf(c_0_40, plain, ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0)|~((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_41, negated_conjecture, ~((epred2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 0.20/0.27 thf(c_0_42, plain, ![X1:nat, X2:nat]:((((X1)=(X2))|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))|(orec3 @ (~($true)) @ (($true)) @ (~($true)))|(less @ X1 @ X2))), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.20/0.27 thf(c_0_43, plain, ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0)|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_44, plain, ((epred2_0)|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_45, plain, ((epred2_0)|~((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_46, plain, ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred2_0)|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_47, plain, ((orec3 @ (~($true)) @ (($true)) @ (($true)))|(epred2_0)|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_38]), c_0_39]), c_0_33])).
% 0.20/0.27 thf(c_0_48, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_37]), c_0_41]), c_0_42])).
% 0.20/0.27 thf(c_0_49, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (~($true)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_43]), c_0_41]), c_0_42])).
% 0.20/0.27 thf(c_0_50, plain, ((epred2_0)|~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(cn,[status(thm)],[c_0_44])).
% 0.20/0.27 thf(c_0_51, plain, ((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))|(epred2_0)|~((orec3 @ (~($true)) @ (($true)) @ (($true))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_37]), c_0_42]), c_0_33])).
% 0.20/0.27 thf(c_0_52, plain, ((epred2_0)|(less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))), inference(cn,[status(thm)],[c_0_46])).
% 0.20/0.27 thf(c_0_53, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_41])).
% 0.20/0.27 thf(c_0_54, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (~($true)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_49]), c_0_41])).
% 0.20/0.27 thf(c_0_55, plain, ((orec3 @ (~($true)) @ (~($true)) @ (($true)))|(epred2_0)|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_26]), c_0_32]), c_0_33])).
% 0.20/0.27 thf(c_0_56, plain, ((epred2_0)|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_57, plain, ((orec3 @ (~($true)) @ (~($true)) @ (~($true)))|(epred2_0)|~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 0.20/0.27 thf(c_0_58, plain, ((orec3 @ (~($true)) @ (($true)) @ (($true)))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_52]), c_0_41])).
% 0.20/0.27 thf(c_0_59, plain, ((orec3 @ (~($true)) @ (($true)) @ (($true)))|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_53]), c_0_41])).
% 0.20/0.27 thf(c_0_60, plain, ((orec3 @ (~($true)) @ (($true)) @ (($true)))|(orec3 @ (~($true)) @ (($true)) @ (~($true)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_54]), c_0_41])).
% 0.20/0.27 thf(c_0_61, plain, ((orec3 @ (~($true)) @ (~($true)) @ (($true)))|(epred2_0)|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))), inference(spm,[status(thm)],[c_0_55, c_0_52])).
% 0.20/0.27 thf(c_0_62, plain, ((epred2_0)|~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 0.20/0.27 thf(c_0_63, plain, (orec3 @ (~($true)) @ (($true)) @ (($true))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60])).
% 0.20/0.27 thf(c_0_64, plain, ((epred2_0)|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_51]), c_0_61]), c_0_62])).
% 0.20/0.27 thf(c_0_65, plain, (~((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_63])]), c_0_41])).
% 0.20/0.27 thf(c_0_66, plain, (~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_63])]), c_0_41])).
% 0.20/0.27 thf(c_0_67, plain, ~((orec3 @ (~($true)) @ (($true)) @ (~($true)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_63])]), c_0_41])).
% 0.20/0.27 thf(c_0_68, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_26]), c_0_66])).
% 0.20/0.27 thf(c_0_69, plain, ((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_49, c_0_67]), c_0_68])).
% 0.20/0.27 thf(c_0_70, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_69])]), c_0_41]), ['proof']).
% 0.20/0.27 % SZS output end CNFRefutation
% 0.20/0.27 % Parsed axioms : 14
% 0.20/0.27 % Removed by relevancy pruning/SinE : 0
% 0.20/0.27 % Initial clauses : 73
% 0.20/0.27 % Removed in clause preprocessing : 36
% 0.20/0.27 % Initial clauses in saturation : 37
% 0.20/0.27 % Processed clauses : 176
% 0.20/0.27 % ...of these trivial : 0
% 0.20/0.27 % ...subsumed : 61
% 0.20/0.27 % ...remaining for further processing : 115
% 0.20/0.27 % Other redundant clauses eliminated : 6
% 0.20/0.27 % Clauses deleted for lack of memory : 0
% 0.20/0.27 % Backward-subsumed : 32
% 0.20/0.27 % Backward-rewritten : 32
% 0.20/0.27 % Generated clauses : 338
% 0.20/0.27 % ...of the previous two non-redundant : 192
% 0.20/0.27 % ...aggressively subsumed : 0
% 0.20/0.27 % Contextual simplify-reflections : 25
% 0.20/0.27 % Paramodulations : 329
% 0.20/0.27 % Factorizations : 0
% 0.20/0.27 % NegExts : 0
% 0.20/0.27 % Equation resolutions : 6
% 0.20/0.27 % Disequality decompositions : 0
% 0.20/0.27 % Total rewrite steps : 35
% 0.20/0.27 % ...of those cached : 32
% 0.20/0.27 % Propositional unsat checks : 0
% 0.20/0.27 % Propositional check models : 0
% 0.20/0.27 % Propositional check unsatisfiable : 0
% 0.20/0.27 % Propositional clauses : 0
% 0.20/0.27 % Propositional clauses after purity: 0
% 0.20/0.27 % Propositional unsat core size : 0
% 0.20/0.27 % Propositional preprocessing time : 0.000
% 0.20/0.27 % Propositional encoding time : 0.000
% 0.20/0.27 % Propositional solver time : 0.000
% 0.20/0.27 % Success case prop preproc time : 0.000
% 0.20/0.27 % Success case prop encoding time : 0.000
% 0.20/0.27 % Success case prop solver time : 0.000
% 0.20/0.27 % Current number of processed clauses : 15
% 0.20/0.27 % Positive orientable unit clauses : 3
% 0.20/0.27 % Positive unorientable unit clauses: 0
% 0.20/0.27 % Negative unit clauses : 2
% 0.20/0.27 % Non-unit-clauses : 10
% 0.20/0.27 % Current number of unprocessed clauses: 61
% 0.20/0.27 % ...number of literals in the above : 273
% 0.20/0.27 % Current number of archived formulas : 0
% 0.20/0.27 % Current number of archived clauses : 96
% 0.20/0.27 % Clause-clause subsumption calls (NU) : 1791
% 0.20/0.27 % Rec. Clause-clause subsumption calls : 644
% 0.20/0.27 % Non-unit clause-clause subsumptions : 115
% 0.20/0.27 % Unit Clause-clause subsumption calls : 65
% 0.20/0.27 % Rewrite failures with RHS unbound : 0
% 0.20/0.27 % BW rewrite match attempts : 4
% 0.20/0.27 % BW rewrite match successes : 3
% 0.20/0.27 % Condensation attempts : 176
% 0.20/0.27 % Condensation successes : 0
% 0.20/0.27 % Termbank termtop insertions : 12242
% 0.20/0.27 % Search garbage collected termcells : 443
% 0.20/0.27
% 0.20/0.27 % -------------------------------------------------
% 0.20/0.27 % User time : 0.019 s
% 0.20/0.27 % System time : 0.004 s
% 0.20/0.27 % Total time : 0.023 s
% 0.20/0.27 % Maximum resident set size: 3632 pages
% 0.20/0.27
% 0.20/0.27 % -------------------------------------------------
% 0.20/0.27 % User time : 0.079 s
% 0.20/0.27 % System time : 0.012 s
% 0.20/0.27 % Total time : 0.091 s
% 0.20/0.27 % Maximum resident set size: 4864 pages
% 0.20/0.27 % E exiting
%------------------------------------------------------------------------------