%------------------------------------------------------------------------------
% File : E-SAT---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 : n020.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:33 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.02 % Problem : NUM730^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n020.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 12:47:04 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/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.yTulF15Pza/E---3.1_999738.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 % sh4l with pid 999753 completed with status 0
% 0.20/0.27 % Result found by sh4l
% 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 % (lift_lambdas = 0, lambda_to_forall = 0,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 1 cores with 300 seconds (300 total)
% 0.20/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.20/0.27 % SubtermCWHack with pid 999758 completed with status 0
% 0.20/0.27 % Result found by SubtermCWHack
% 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 % (lift_lambdas = 0, lambda_to_forall = 0,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 1 cores with 300 seconds (300 total)
% 0.20/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.20/0.27 % Preprocessing time : 0.001 s
% 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.yTulF15Pza/E---3.1_999738.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.yTulF15Pza/E---3.1_999738.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]:(((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_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, ((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_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, 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_13, 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_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, ((more @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(less @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)), 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, negated_conjecture, ~(((epred1_0)&(epred2_0))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_12]), c_0_2]), c_0_13])).
% 0.20/0.27 thf(c_0_19, 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_20, 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_21, 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_22, plain, ((less @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)), 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_23, 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_13])).
% 0.20/0.27 thf(c_0_24, negated_conjecture, (~(epred1_0)|~(epred2_0)), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])).
% 0.20/0.27 thf(c_0_25, 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_26, plain, ![X1:nat]:(((orec3 @ (($true)) @ (($true)) @ (($true)))|~((more @ X1 @ X1))|~((less @ X1 @ X1)))), inference(er,[status(thm)],[c_0_19])).
% 0.20/0.27 thf(c_0_27, plain, ((more @ (ts @ (c1y @ y) @ (c2x @ x)) @ (ts @ (c1y @ y) @ (c2x @ x)))|(epred1_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_10]), c_0_21]), c_0_22])).
% 0.20/0.27 thf(c_0_28, 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_23])])])).
% 0.20/0.27 thf(c_0_29, negated_conjecture, (~((epred1_0))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.20/0.27 thf(c_0_30, plain, (epred1_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_10]), c_0_26]), c_0_22]), c_0_27])).
% 0.20/0.27 thf(c_0_31, 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_32, 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_33, plain, ((more @ (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_28])).
% 0.20/0.27 thf(c_0_34, negated_conjecture, ~((epred2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 0.20/0.27 thf(c_0_35, plain, ![X1:nat, X2:nat]:((((X1)=(X2))|(orec3 @ (~($true)) @ (~($true)) @ (($true)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))|~((less @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 0.20/0.27 thf(c_0_36, 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_28])).
% 0.20/0.27 thf(c_0_37, 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_38, 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_39, plain, (((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(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_33]), c_0_34]), c_0_35])).
% 0.20/0.27 thf(c_0_40, 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_36])).
% 0.20/0.27 thf(c_0_41, 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_28])).
% 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_37, c_0_38])).
% 0.20/0.27 thf(c_0_43, plain, ((epred2_0)|((ts @ (c1x @ x) @ (c2y @ y))!=(ts @ (c1y @ y) @ (c2x @ x)))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.20/0.27 thf(c_0_44, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_34])).
% 0.20/0.27 thf(c_0_45, 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_37, c_0_41]), c_0_34]), c_0_42])).
% 0.20/0.27 thf(c_0_46, plain, ((orec3 @ (~($true)) @ (($true)) @ (($true)))|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))|~((orec3 @ (~($true)) @ (($true)) @ (~($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_34])).
% 0.20/0.27 thf(c_0_47, 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_28])).
% 0.20/0.27 thf(c_0_48, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_45]), c_0_46])).
% 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_47, c_0_38]), c_0_34]), c_0_42])).
% 0.20/0.27 thf(c_0_50, plain, ((orec3 @ (~($true)) @ (($true)) @ (($true)))|~((orec3 @ (~($true)) @ (~($true)) @ (~($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_48]), c_0_34])).
% 0.20/0.27 thf(c_0_51, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))|(orec3 @ (~($true)) @ (~($true)) @ (($true)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_49]), c_0_50])).
% 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))))|~((less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.20/0.27 thf(c_0_53, 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_28])).
% 0.20/0.27 thf(c_0_54, plain, ((orec3 @ (~($true)) @ (~($true)) @ (($true)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_51]), c_0_34])).
% 0.20/0.27 thf(c_0_55, 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_52])).
% 0.20/0.27 thf(c_0_56, plain, (((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))))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_53]), c_0_34]), c_0_54])).
% 0.20/0.27 thf(c_0_57, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_49]), c_0_34])).
% 0.20/0.27 thf(c_0_58, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (~($true)))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_45]), c_0_34])).
% 0.20/0.27 thf(c_0_59, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (($true)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_49]), c_0_50])).
% 0.20/0.27 thf(c_0_60, 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_28])).
% 0.20/0.27 thf(c_0_61, plain, ((orec3 @ (~($true)) @ (~($true)) @ (~($true)))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_57]), c_0_34])).
% 0.20/0.27 thf(c_0_62, plain, ((orec3 @ (~($true)) @ (($true)) @ (~($true)))|~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_58]), c_0_34])).
% 0.20/0.27 thf(c_0_63, 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_28])).
% 0.20/0.27 thf(c_0_64, plain, (orec3 @ (~($true)) @ (($true)) @ (($true))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_59]), c_0_34])).
% 0.20/0.27 thf(c_0_65, plain, (~((orec3 @ (~($true)) @ (($true)) @ (($true))))|~((orec3 @ (~($true)) @ (~($true)) @ (($true))))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_34]), c_0_62])).
% 0.20/0.27 thf(c_0_66, 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_63, c_0_64])]), c_0_34])).
% 0.20/0.27 thf(c_0_67, plain, ~((orec3 @ (~($true)) @ (~($true)) @ (($true)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_64])])).
% 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(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_32]), c_0_67])).
% 0.20/0.27 thf(c_0_69, 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_28])).
% 0.20/0.27 thf(c_0_70, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (($true)) @ (~($true)))), inference(spm,[status(thm)],[c_0_68, c_0_45])).
% 0.20/0.27 thf(c_0_71, plain, (((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x)))|(orec3 @ (~($true)) @ (~($true)) @ (~($true)))), inference(spm,[status(thm)],[c_0_68, c_0_49])).
% 0.20/0.27 thf(c_0_72, plain, (~((more @ (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_69, c_0_64])]), c_0_34])).
% 0.20/0.27 thf(c_0_73, plain, (orec3 @ (~($true)) @ (($true)) @ (~($true))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_70]), c_0_34])).
% 0.20/0.27 thf(c_0_74, plain, (orec3 @ (~($true)) @ (~($true)) @ (~($true))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_71]), c_0_34])).
% 0.20/0.27 thf(c_0_75, plain, ~((more @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])])).
% 0.20/0.27 thf(c_0_76, plain, (less @ (ts @ (c1x @ x) @ (c2y @ y)) @ (ts @ (c1y @ y) @ (c2x @ x))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_74])]), c_0_75]), c_0_34])).
% 0.20/0.27 thf(c_0_77, plain, ((ts @ (c1x @ x) @ (c2y @ y))=(ts @ (c1y @ y) @ (c2x @ x))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_76])])).
% 0.20/0.27 thf(c_0_78, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_77])]), c_0_34]), ['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 : 207
% 0.20/0.27 % ...of these trivial : 0
% 0.20/0.27 % ...subsumed : 91
% 0.20/0.27 % ...remaining for further processing : 116
% 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 : 56
% 0.20/0.27 % Backward-rewritten : 40
% 0.20/0.27 % Generated clauses : 695
% 0.20/0.27 % ...of the previous two non-redundant : 502
% 0.20/0.27 % ...aggressively subsumed : 0
% 0.20/0.27 % Contextual simplify-reflections : 26
% 0.20/0.27 % Paramodulations : 688
% 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 : 40
% 0.20/0.27 % ...of those cached : 34
% 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 : 5
% 0.20/0.27 % Positive unorientable unit clauses: 0
% 0.20/0.27 % Negative unit clauses : 2
% 0.20/0.27 % Non-unit-clauses : 8
% 0.20/0.27 % Current number of unprocessed clauses: 11
% 0.20/0.27 % ...number of literals in the above : 31
% 0.20/0.27 % Current number of archived formulas : 0
% 0.20/0.27 % Current number of archived clauses : 97
% 0.20/0.27 % Clause-clause subsumption calls (NU) : 3295
% 0.20/0.27 % Rec. Clause-clause subsumption calls : 577
% 0.20/0.27 % Non-unit clause-clause subsumptions : 170
% 0.20/0.27 % Unit Clause-clause subsumption calls : 67
% 0.20/0.27 % Rewrite failures with RHS unbound : 0
% 0.20/0.27 % BW rewrite match attempts : 9
% 0.20/0.27 % BW rewrite match successes : 6
% 0.20/0.27 % Condensation attempts : 0
% 0.20/0.27 % Condensation successes : 0
% 0.20/0.27 % Termbank termtop insertions : 21178
% 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.001 s
% 0.20/0.27 % Total time : 0.020 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.022 s
% 0.20/0.27 % System time : 0.003 s
% 0.20/0.27 % Total time : 0.025 s
% 0.20/0.27 % Maximum resident set size: 4608 pages
% 0.20/0.27 % E exiting
%------------------------------------------------------------------------------