%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO500^1.002 : TPTP v9.3.1. Released v4.1.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:43:15 AM UTC 2026
% Result : Theorem 0.22s 0.28s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500^1.002 : TPTP v9.3.1. Released v4.1.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 17:13:42 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.23 Running higher-order theorem proving
% 0.07/0.24 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.GJC4J6K1kU/E---3.1_885978.p
% 0.22/0.28 % Version: 3.5.1-ho
% 0.22/0.28 % Preprocessing class: HSSSSMSSSSSNFFN.
% 0.22/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.28 % Starting new_ho_10 with 1500s (5) cores
% 0.22/0.28 % Starting ho_unfolding_6 with 300s (1) cores
% 0.22/0.28 % Starting sh4l with 300s (1) cores
% 0.22/0.28 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 0.22/0.28 % new_ho_10 with pid 886007 completed with status 0
% 0.22/0.28 % Result found by new_ho_10
% 0.22/0.28 % Preprocessing class: HSSSSMSSSSSNFFN.
% 0.22/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.28 % Starting new_ho_10 with 1500s (5) cores
% 0.22/0.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.28 % No SInE strategy applied
% 0.22/0.28 % Search class: HGHNF-FFMM00-SFFFFFNN
% 0.22/0.28 % partial match(1): FGHNF-FFMM00-SFFFFFNN
% 0.22/0.28 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.22/0.28 % Starting SubtermCWHack with 136s (1) cores
% 0.22/0.28 % Starting new_ho_10 with 151s (1) cores
% 0.22/0.28 % Starting H----_011_C07_F1_PI_AE_OS_R8_SP_S1U with 136s (1) cores
% 0.22/0.28 % Starting G----_425_C05_02_F1_SE_CS_SP_PS_RG_S04AI with 136s (1) cores
% 0.22/0.28 % Starting G-E--_208_B07--C_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 0.22/0.28 % SubtermCWHack with pid 886013 completed with status 0
% 0.22/0.28 % Result found by SubtermCWHack
% 0.22/0.28 % Preprocessing class: HSSSSMSSSSSNFFN.
% 0.22/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.28 % Starting new_ho_10 with 1500s (5) cores
% 0.22/0.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.28 % No SInE strategy applied
% 0.22/0.28 % Search class: HGHNF-FFMM00-SFFFFFNN
% 0.22/0.28 % partial match(1): FGHNF-FFMM00-SFFFFFNN
% 0.22/0.28 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.22/0.28 % Starting SubtermCWHack with 136s (1) cores
% 0.22/0.28 % Preprocessing time : 0.001 s
% 0.22/0.28
% 0.22/0.28 % Proof found!
% 0.22/0.28 % SZS status Theorem
% 0.22/0.28 % SZS output start CNFRefutation
% 0.22/0.28 thf(decl_23, type, x: $o).
% 0.22/0.28 thf(decl_24, type, f0: $o > $o).
% 0.22/0.28 thf(decl_25, type, f1: $o > $o).
% 0.22/0.28 thf(decl_26, type, epred1_0: $o).
% 0.22/0.28 thf(decl_27, type, epred2_0: $o).
% 0.22/0.28 thf(decl_28, type, epred3_0: $o).
% 0.22/0.28 thf(decl_29, type, epred4_0: $o).
% 0.22/0.28 thf(decl_30, type, epred5_0: $o).
% 0.22/0.28 thf(decl_31, type, epred6_0: $o).
% 0.22/0.28 thf(kaminski2, conjecture, ((f0 @ ((f0 @ ((f0 @ ((f1 @ ((x)))))))))<=>(f0 @ ((f1 @ ((f1 @ ((f1 @ ((x)))))))))), file('/export/starexec/sandbox/tmp/tmp.GJC4J6K1kU/E---3.1_885978.p', kaminski2)).
% 0.22/0.28 thf(c_0_1, plain, ((epred3_0)<=>((((((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|~(f0 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|~(f0 @ $false)))|~(f0 @ $true))&(((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|(f0 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|(f0 @ $false)))|~(f0 @ $false)))|(f0 @ $true))&(((((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|~(f0 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|~(f0 @ $false)))|(f0 @ $true))&(((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|(f0 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|(f0 @ $false)))|(f0 @ $false)))|(f0 @ $false)))), introduced(definition)).
% 0.22/0.28 thf(c_0_2, plain, ((epred1_0)<=>((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|~(f0 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|~(f0 @ $false)))), introduced(definition)).
% 0.22/0.28 thf(c_0_3, plain, ((epred2_0)<=>((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|(f0 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|(f0 @ $false)))), introduced(definition)).
% 0.22/0.28 thf(c_0_4, plain, ((epred3_0)<=>(((((epred1_0)|~(f0 @ $true))&((epred2_0)|~(f0 @ $false)))|(f0 @ $true))&((((epred1_0)|(f0 @ $true))&((epred2_0)|(f0 @ $false)))|(f0 @ $false)))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1, c_0_2]), c_0_3]), c_0_2]), c_0_3])).
% 0.22/0.28 thf(c_0_5, plain, (((((epred1_0)|~(f0 @ $true)|(f0 @ $true)|~(epred3_0))&((epred2_0)|~(f0 @ $false)|(f0 @ $true)|~(epred3_0)))&(((epred1_0)|(f0 @ $true)|(f0 @ $false)|~(epred3_0))&((epred2_0)|(f0 @ $false)|(f0 @ $false)|~(epred3_0))))&(((((((~(epred2_0)|~(epred1_0)|(~(epred2_0)|~(epred1_0))|(epred3_0))&(~(f0 @ $false)|~(epred1_0)|(~(epred2_0)|~(epred1_0))|(epred3_0)))&((~(epred2_0)|~(f0 @ $true)|(~(epred2_0)|~(epred1_0))|(epred3_0))&(~(f0 @ $false)|~(f0 @ $true)|(~(epred2_0)|~(epred1_0))|(epred3_0))))&(~(f0 @ $false)|(~(epred2_0)|~(epred1_0))|(epred3_0)))&((((~(epred2_0)|~(epred1_0)|((f0 @ $false)|~(epred1_0))|(epred3_0))&(~(f0 @ $false)|~(epred1_0)|((f0 @ $false)|~(epred1_0))|(epred3_0)))&((~(epred2_0)|~(f0 @ $true)|((f0 @ $false)|~(epred1_0))|(epred3_0))&(~(f0 @ $false)|~(f0 @ $true)|((f0 @ $false)|~(epred1_0))|(epred3_0))))&(~(f0 @ $false)|((f0 @ $false)|~(epred1_0))|(epred3_0))))&(((((~(epred2_0)|~(epred1_0)|(~(epred2_0)|(f0 @ $true))|(epred3_0))&(~(f0 @ $false)|~(epred1_0)|(~(epred2_0)|(f0 @ $true))|(epred3_0)))&((~(epred2_0)|~(f0 @ $true)|(~(epred2_0)|(f0 @ $true))|(epred3_0))&(~(f0 @ $false)|~(f0 @ $true)|(~(epred2_0)|(f0 @ $true))|(epred3_0))))&(~(f0 @ $false)|(~(epred2_0)|(f0 @ $true))|(epred3_0)))&((((~(epred2_0)|~(epred1_0)|((f0 @ $false)|(f0 @ $true))|(epred3_0))&(~(f0 @ $false)|~(epred1_0)|((f0 @ $false)|(f0 @ $true))|(epred3_0)))&((~(epred2_0)|~(f0 @ $true)|((f0 @ $false)|(f0 @ $true))|(epred3_0))&(~(f0 @ $false)|~(f0 @ $true)|((f0 @ $false)|(f0 @ $true))|(epred3_0))))&(~(f0 @ $false)|((f0 @ $false)|(f0 @ $true))|(epred3_0)))))&((((~(epred2_0)|~(epred1_0)|~(f0 @ $true)|(epred3_0))&(~(f0 @ $false)|~(epred1_0)|~(f0 @ $true)|(epred3_0)))&((~(epred2_0)|~(f0 @ $true)|~(f0 @ $true)|(epred3_0))&(~(f0 @ $false)|~(f0 @ $true)|~(f0 @ $true)|(epred3_0))))&(~(f0 @ $false)|~(f0 @ $true)|(epred3_0))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])).
% 0.22/0.28 thf(c_0_6, plain, ((epred5_0)<=>((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|(f1 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|(f1 @ $false)))), introduced(definition)).
% 0.22/0.28 thf(c_0_7, plain, ((((~(x)|~(f1 @ $true)|(f0 @ $true)|~(epred2_0))&((x)|~(f1 @ $false)|(f0 @ $true)|~(epred2_0)))&((~(x)|(f1 @ $true)|(f0 @ $false)|~(epred2_0))&((x)|(f1 @ $false)|(f0 @ $false)|~(epred2_0))))&(((((((~(x)|(x)|(~(x)|(x))|(epred2_0))&(~(f1 @ $false)|(x)|(~(x)|(x))|(epred2_0)))&((~(x)|~(f1 @ $true)|(~(x)|(x))|(epred2_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(x))|(epred2_0))))&(~(f0 @ $false)|(~(x)|(x))|(epred2_0)))&((((~(x)|(x)|((f1 @ $false)|(x))|(epred2_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(x))|(epred2_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred2_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred2_0))))&(~(f0 @ $false)|((f1 @ $false)|(x))|(epred2_0))))&(((((~(x)|(x)|(~(x)|(f1 @ $true))|(epred2_0))&(~(f1 @ $false)|(x)|(~(x)|(f1 @ $true))|(epred2_0)))&((~(x)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred2_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred2_0))))&(~(f0 @ $false)|(~(x)|(f1 @ $true))|(epred2_0)))&((((~(x)|(x)|((f1 @ $false)|(f1 @ $true))|(epred2_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(f1 @ $true))|(epred2_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred2_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred2_0))))&(~(f0 @ $false)|((f1 @ $false)|(f1 @ $true))|(epred2_0)))))&((((~(x)|(x)|~(f0 @ $true)|(epred2_0))&(~(f1 @ $false)|(x)|~(f0 @ $true)|(epred2_0)))&((~(x)|~(f1 @ $true)|~(f0 @ $true)|(epred2_0))&(~(f1 @ $false)|~(f1 @ $true)|~(f0 @ $true)|(epred2_0))))&(~(f0 @ $false)|~(f0 @ $true)|(epred2_0))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])).
% 0.22/0.28 thf(c_0_8, plain, ((epred2_0)|(f0 @ (~($true)))|(f0 @ (~($true)))|~((epred3_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.22/0.28 thf(c_0_9, negated_conjecture, ~(((f0 @ ((f0 @ ((f0 @ ((f1 @ ((x)))))))))<=>(f0 @ ((f1 @ ((f1 @ ((f1 @ ((x))))))))))), inference(assume_negation,[status(cth)],[kaminski2])).
% 0.22/0.28 thf(c_0_10, plain, ((epred6_0)<=>((((((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|~(f1 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|~(f1 @ $false)))|~(f1 @ $true))&(((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|(f1 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|(f1 @ $false)))|~(f1 @ $false)))|(f0 @ $true))&(((((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|~(f1 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|~(f1 @ $false)))|(f1 @ $true))&(((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|(f1 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|(f1 @ $false)))|(f1 @ $false)))|(f0 @ $false)))), introduced(definition)).
% 0.22/0.28 thf(c_0_11, plain, ((((~(x)|~(f1 @ $true)|(f1 @ $true)|~(epred5_0))&((x)|~(f1 @ $false)|(f1 @ $true)|~(epred5_0)))&((~(x)|(f1 @ $true)|(f1 @ $false)|~(epred5_0))&((x)|(f1 @ $false)|(f1 @ $false)|~(epred5_0))))&(((((((~(x)|(x)|(~(x)|(x))|(epred5_0))&(~(f1 @ $false)|(x)|(~(x)|(x))|(epred5_0)))&((~(x)|~(f1 @ $true)|(~(x)|(x))|(epred5_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(x))|(epred5_0))))&(~(f1 @ $false)|(~(x)|(x))|(epred5_0)))&((((~(x)|(x)|((f1 @ $false)|(x))|(epred5_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(x))|(epred5_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred5_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred5_0))))&(~(f1 @ $false)|((f1 @ $false)|(x))|(epred5_0))))&(((((~(x)|(x)|(~(x)|(f1 @ $true))|(epred5_0))&(~(f1 @ $false)|(x)|(~(x)|(f1 @ $true))|(epred5_0)))&((~(x)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred5_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred5_0))))&(~(f1 @ $false)|(~(x)|(f1 @ $true))|(epred5_0)))&((((~(x)|(x)|((f1 @ $false)|(f1 @ $true))|(epred5_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(f1 @ $true))|(epred5_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred5_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred5_0))))&(~(f1 @ $false)|((f1 @ $false)|(f1 @ $true))|(epred5_0)))))&((((~(x)|(x)|~(f1 @ $true)|(epred5_0))&(~(f1 @ $false)|(x)|~(f1 @ $true)|(epred5_0)))&((~(x)|~(f1 @ $true)|~(f1 @ $true)|(epred5_0))&(~(f1 @ $false)|~(f1 @ $true)|~(f1 @ $true)|(epred5_0))))&(~(f1 @ $false)|~(f1 @ $true)|(epred5_0))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])])).
% 0.22/0.28 thf(c_0_12, plain, ((epred4_0)<=>((((~(x)|~(f1 @ $true))&((x)|~(f1 @ $false)))|~(f1 @ $true))&(((~(x)|(f1 @ $true))&((x)|(f1 @ $false)))|~(f1 @ $false)))), introduced(definition)).
% 0.22/0.28 thf(c_0_13, plain, ((epred2_0)|~((f0 @ (~($true))))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_14, plain, ((epred2_0)|(f0 @ (~($true)))|~((epred3_0))), inference(cn,[status(thm)],[c_0_8])).
% 0.22/0.28 thf(c_0_15, negated_conjecture, ~(((epred3_0)<=>(epred6_0))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_9]), c_0_1]), c_0_10])).
% 0.22/0.28 thf(c_0_16, plain, ((x)|(f1 @ (~($true)))|(f1 @ (~($true)))|~((epred5_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.22/0.28 thf(c_0_17, plain, ((((~(x)|~(f1 @ $true)|~(f1 @ $true)|~(epred4_0))&((x)|~(f1 @ $false)|~(f1 @ $true)|~(epred4_0)))&((~(x)|(f1 @ $true)|~(f1 @ $false)|~(epred4_0))&((x)|(f1 @ $false)|~(f1 @ $false)|~(epred4_0))))&(((((((~(x)|(x)|(~(x)|(x))|(epred4_0))&(~(f1 @ $false)|(x)|(~(x)|(x))|(epred4_0)))&((~(x)|~(f1 @ $true)|(~(x)|(x))|(epred4_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(x))|(epred4_0))))&((f1 @ $false)|(~(x)|(x))|(epred4_0)))&((((~(x)|(x)|((f1 @ $false)|(x))|(epred4_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(x))|(epred4_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred4_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred4_0))))&((f1 @ $false)|((f1 @ $false)|(x))|(epred4_0))))&(((((~(x)|(x)|(~(x)|(f1 @ $true))|(epred4_0))&(~(f1 @ $false)|(x)|(~(x)|(f1 @ $true))|(epred4_0)))&((~(x)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred4_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred4_0))))&((f1 @ $false)|(~(x)|(f1 @ $true))|(epred4_0)))&((((~(x)|(x)|((f1 @ $false)|(f1 @ $true))|(epred4_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(f1 @ $true))|(epred4_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred4_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred4_0))))&((f1 @ $false)|((f1 @ $false)|(f1 @ $true))|(epred4_0)))))&((((~(x)|(x)|(f1 @ $true)|(epred4_0))&(~(f1 @ $false)|(x)|(f1 @ $true)|(epred4_0)))&((~(x)|~(f1 @ $true)|(f1 @ $true)|(epred4_0))&(~(f1 @ $false)|~(f1 @ $true)|(f1 @ $true)|(epred4_0))))&((f1 @ $false)|(f1 @ $true)|(epred4_0))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])).
% 0.22/0.28 thf(c_0_18, plain, ((epred6_0)<=>(((((epred4_0)|~(f1 @ $true))&((epred5_0)|~(f1 @ $false)))|(f0 @ $true))&((((epred4_0)|(f1 @ $true))&((epred5_0)|(f1 @ $false)))|(f0 @ $false)))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_10, c_0_12]), c_0_6]), c_0_12]), c_0_6])).
% 0.22/0.28 thf(c_0_19, plain, ((epred2_0)|(f0 @ (($true)))|~((f0 @ (~($true))))|~((epred3_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.22/0.28 thf(c_0_20, plain, ((epred2_0)|~((f0 @ (($true))))|~((epred3_0))), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 0.22/0.28 thf(c_0_21, negated_conjecture, ((~(epred3_0)|~(epred6_0))&((epred3_0)|(epred6_0))), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_15])])).
% 0.22/0.28 thf(c_0_22, plain, ((f1 @ (($true)))|(f1 @ (~($true)))|~((x))|~((epred5_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.22/0.28 thf(c_0_23, plain, ((x)|(f1 @ (~($true)))|~((epred5_0))), inference(cn,[status(thm)],[c_0_16])).
% 0.22/0.28 thf(c_0_24, plain, ((f1 @ (~($true)))|(f1 @ (~($true)))|(x)|(epred4_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.28 thf(c_0_25, plain, ((epred5_0)|~((x))|~((f1 @ (($true))))|~((f1 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.22/0.28 thf(c_0_26, plain, ((((~(x)|~(f1 @ $true)|~(f0 @ $true)|~(epred1_0))&((x)|~(f1 @ $false)|~(f0 @ $true)|~(epred1_0)))&((~(x)|(f1 @ $true)|~(f0 @ $false)|~(epred1_0))&((x)|(f1 @ $false)|~(f0 @ $false)|~(epred1_0))))&(((((((~(x)|(x)|(~(x)|(x))|(epred1_0))&(~(f1 @ $false)|(x)|(~(x)|(x))|(epred1_0)))&((~(x)|~(f1 @ $true)|(~(x)|(x))|(epred1_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(x))|(epred1_0))))&((f0 @ $false)|(~(x)|(x))|(epred1_0)))&((((~(x)|(x)|((f1 @ $false)|(x))|(epred1_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(x))|(epred1_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred1_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(x))|(epred1_0))))&((f0 @ $false)|((f1 @ $false)|(x))|(epred1_0))))&(((((~(x)|(x)|(~(x)|(f1 @ $true))|(epred1_0))&(~(f1 @ $false)|(x)|(~(x)|(f1 @ $true))|(epred1_0)))&((~(x)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred1_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(x)|(f1 @ $true))|(epred1_0))))&((f0 @ $false)|(~(x)|(f1 @ $true))|(epred1_0)))&((((~(x)|(x)|((f1 @ $false)|(f1 @ $true))|(epred1_0))&(~(f1 @ $false)|(x)|((f1 @ $false)|(f1 @ $true))|(epred1_0)))&((~(x)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred1_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred1_0))))&((f0 @ $false)|((f1 @ $false)|(f1 @ $true))|(epred1_0)))))&((((~(x)|(x)|(f0 @ $true)|(epred1_0))&(~(f1 @ $false)|(x)|(f0 @ $true)|(epred1_0)))&((~(x)|~(f1 @ $true)|(f0 @ $true)|(epred1_0))&(~(f1 @ $false)|~(f1 @ $true)|(f0 @ $true)|(epred1_0))))&((f0 @ $false)|(f0 @ $true)|(epred1_0))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])).
% 0.22/0.28 thf(c_0_27, plain, (((((epred4_0)|~(f1 @ $true)|(f0 @ $true)|~(epred6_0))&((epred5_0)|~(f1 @ $false)|(f0 @ $true)|~(epred6_0)))&(((epred4_0)|(f1 @ $true)|(f0 @ $false)|~(epred6_0))&((epred5_0)|(f1 @ $false)|(f0 @ $false)|~(epred6_0))))&(((((((~(epred5_0)|~(epred4_0)|(~(epred5_0)|~(epred4_0))|(epred6_0))&(~(f1 @ $false)|~(epred4_0)|(~(epred5_0)|~(epred4_0))|(epred6_0)))&((~(epred5_0)|~(f1 @ $true)|(~(epred5_0)|~(epred4_0))|(epred6_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(epred5_0)|~(epred4_0))|(epred6_0))))&(~(f0 @ $false)|(~(epred5_0)|~(epred4_0))|(epred6_0)))&((((~(epred5_0)|~(epred4_0)|((f1 @ $false)|~(epred4_0))|(epred6_0))&(~(f1 @ $false)|~(epred4_0)|((f1 @ $false)|~(epred4_0))|(epred6_0)))&((~(epred5_0)|~(f1 @ $true)|((f1 @ $false)|~(epred4_0))|(epred6_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|~(epred4_0))|(epred6_0))))&(~(f0 @ $false)|((f1 @ $false)|~(epred4_0))|(epred6_0))))&(((((~(epred5_0)|~(epred4_0)|(~(epred5_0)|(f1 @ $true))|(epred6_0))&(~(f1 @ $false)|~(epred4_0)|(~(epred5_0)|(f1 @ $true))|(epred6_0)))&((~(epred5_0)|~(f1 @ $true)|(~(epred5_0)|(f1 @ $true))|(epred6_0))&(~(f1 @ $false)|~(f1 @ $true)|(~(epred5_0)|(f1 @ $true))|(epred6_0))))&(~(f0 @ $false)|(~(epred5_0)|(f1 @ $true))|(epred6_0)))&((((~(epred5_0)|~(epred4_0)|((f1 @ $false)|(f1 @ $true))|(epred6_0))&(~(f1 @ $false)|~(epred4_0)|((f1 @ $false)|(f1 @ $true))|(epred6_0)))&((~(epred5_0)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred6_0))&(~(f1 @ $false)|~(f1 @ $true)|((f1 @ $false)|(f1 @ $true))|(epred6_0))))&(~(f0 @ $false)|((f1 @ $false)|(f1 @ $true))|(epred6_0)))))&((((~(epred5_0)|~(epred4_0)|~(f0 @ $true)|(epred6_0))&(~(f1 @ $false)|~(epred4_0)|~(f0 @ $true)|(epred6_0)))&((~(epred5_0)|~(f1 @ $true)|~(f0 @ $true)|(epred6_0))&(~(f1 @ $false)|~(f1 @ $true)|~(f0 @ $true)|(epred6_0))))&(~(f0 @ $false)|~(f0 @ $true)|(epred6_0))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])).
% 0.22/0.28 thf(c_0_28, plain, ((epred2_0)|~((epred3_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_19, c_0_14]), c_0_20])).
% 0.22/0.28 thf(c_0_29, negated_conjecture, ((epred3_0)|(epred6_0)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.28 thf(c_0_30, plain, ((x)|(f1 @ (($true)))|~((f1 @ (~($true))))|~((epred5_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.22/0.28 thf(c_0_31, plain, ((f1 @ (~($true)))|(f1 @ (($true)))|~((epred5_0))), inference(csr,[status(thm)],[c_0_22, c_0_23])).
% 0.22/0.28 thf(c_0_32, plain, ((epred5_0)|~((f1 @ (~($true))))|~((f1 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.22/0.28 thf(c_0_33, plain, ((x)|(epred4_0)|(f1 @ (~($true)))), inference(cn,[status(thm)],[c_0_24])).
% 0.22/0.28 thf(c_0_34, plain, ((epred5_0)|~((x))|~((f1 @ (($true))))), inference(cn,[status(thm)],[c_0_25])).
% 0.22/0.28 thf(c_0_35, plain, ((x)|(f1 @ (($true)))|(epred4_0)|~((f1 @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.28 thf(c_0_36, plain, ((f1 @ (~($true)))|(f1 @ (($true)))|(epred4_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.28 thf(c_0_37, plain, ((x)|(f1 @ (~($true)))|~((f0 @ (~($true))))|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_38, plain, ((x)|(f1 @ (~($true)))|(f0 @ (~($true)))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_39, plain, ((epred6_0)|~((epred5_0))|~((f1 @ (($true))))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_40, plain, ((f0 @ (($true)))|~((x))|~((f1 @ (($true))))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_41, negated_conjecture, ((epred6_0)|(epred2_0)), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 0.22/0.28 thf(c_0_42, plain, ((f1 @ (($true)))|(epred6_0)|~((f0 @ (~($true))))|~((epred5_0))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_43, plain, ((f1 @ (($true)))|(f0 @ (~($true)))|~((x))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_44, plain, ((f1 @ (($true)))|(x)|~((epred5_0))), inference(csr,[status(thm)],[c_0_30, c_0_31])).
% 0.22/0.28 thf(c_0_45, plain, ((f1 @ (($true)))|(epred5_0)|~((f1 @ (~($true))))|~((x))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.22/0.28 thf(c_0_46, plain, ((epred4_0)|(epred5_0)|~((f1 @ (($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_34])).
% 0.22/0.28 thf(c_0_47, plain, ((f1 @ (($true)))|(epred4_0)|(x)), inference(csr,[status(thm)],[c_0_35, c_0_36])).
% 0.22/0.28 thf(c_0_48, plain, ((x)|~((f1 @ (~($true))))|~((f0 @ (($true))))|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_49, plain, ((x)|(f0 @ (($true)))|~((f1 @ (~($true))))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_50, plain, ((f1 @ (~($true)))|(x)|~((epred1_0))|~((epred2_0))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 0.22/0.28 thf(c_0_51, plain, (~((x))|~((f1 @ (($true))))|~((f1 @ (($true))))|~((epred4_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.28 thf(c_0_52, plain, ((epred6_0)|~((f1 @ (($true))))|~((x))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_41]), c_0_34])).
% 0.22/0.28 thf(c_0_53, plain, ((f1 @ (($true)))|(epred6_0)|~((epred5_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_41]), c_0_44])).
% 0.22/0.28 thf(c_0_54, plain, ((epred5_0)|~((f1 @ (~($true))))|~((x))), inference(csr,[status(thm)],[c_0_45, c_0_34])).
% 0.22/0.28 thf(c_0_55, plain, ((x)|(epred5_0)|(epred4_0)), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 0.22/0.28 thf(c_0_56, plain, (~((x))|~((f1 @ (($true))))|~((f0 @ (($true))))|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_57, plain, ((x)|~((epred1_0))|~((epred2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_49]), c_0_50])).
% 0.22/0.28 thf(c_0_58, plain, ((f1 @ (($true)))|~((x))|~((f0 @ (~($true))))|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_59, plain, ((f1 @ (($true)))|~((x))|~((f1 @ (~($true))))|~((epred4_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.28 thf(c_0_60, plain, (~((x))|~((epred4_0))|~((f1 @ (($true))))), inference(cn,[status(thm)],[c_0_51])).
% 0.22/0.28 thf(c_0_61, plain, ((f1 @ (~($true)))|(f1 @ (($true)))|(epred6_0)|~((f0 @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_62, plain, ((f0 @ (~($true)))|(f1 @ (~($true)))|(f1 @ (($true)))|(epred1_0)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_63, plain, ((epred6_0)|~((x))|~((epred5_0))), inference(spm,[status(thm)],[c_0_52, c_0_53])).
% 0.22/0.28 thf(c_0_64, plain, ((epred4_0)|(epred5_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_36]), c_0_55]), c_0_46])).
% 0.22/0.28 thf(c_0_65, plain, (~((f1 @ (($true))))|~((epred1_0))|~((epred2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_40]), c_0_57])).
% 0.22/0.28 thf(c_0_66, plain, ((f1 @ (($true)))|~((x))|~((epred1_0))|~((epred2_0))), inference(spm,[status(thm)],[c_0_58, c_0_43])).
% 0.22/0.28 thf(c_0_67, plain, (~((f1 @ (~($true))))|~((x))|~((epred4_0))), inference(csr,[status(thm)],[c_0_59, c_0_60])).
% 0.22/0.28 thf(c_0_68, plain, ((f1 @ (($true)))|(f1 @ (~($true)))|(epred1_0)|(epred6_0)), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 0.22/0.28 thf(c_0_69, plain, ((epred4_0)|(epred6_0)|~((x))), inference(spm,[status(thm)],[c_0_63, c_0_64])).
% 0.22/0.28 thf(c_0_70, plain, ((epred6_0)|~((f1 @ (~($true))))|~((f1 @ (($true))))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_71, plain, ((f0 @ (($true)))|(epred1_0)|~((f1 @ (~($true))))|~((f1 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_72, plain, ((f1 @ (~($true)))|(epred6_0)|~((f0 @ (~($true))))|~((epred4_0))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_73, plain, (~((epred1_0))|~((epred2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_66]), c_0_57])).
% 0.22/0.28 thf(c_0_74, plain, ((epred6_0)|(epred1_0)|~((x))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_69]), c_0_52])).
% 0.22/0.28 thf(c_0_75, plain, ((epred1_0)|(epred6_0)|~((f1 @ (($true))))|~((f1 @ (~($true))))), inference(spm,[status(thm)],[c_0_70, c_0_71])).
% 0.22/0.28 thf(c_0_76, plain, ((f1 @ (~($true)))|(x)|(epred6_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_38]), c_0_41]), c_0_33])).
% 0.22/0.28 thf(c_0_77, plain, ((epred6_0)|~((x))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_74]), c_0_41])).
% 0.22/0.28 thf(c_0_78, plain, ((epred6_0)|(epred1_0)|~((f1 @ (($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_77])).
% 0.22/0.28 thf(c_0_79, plain, ((f1 @ (~($true)))|(x)|(epred2_0)|~((f0 @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_80, plain, ((f0 @ (~($true)))|(f1 @ (~($true)))|(x)|(epred1_0)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_81, plain, ((f0 @ (($true)))|(epred3_0)|~((f0 @ (~($true))))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.22/0.28 thf(c_0_82, plain, ((epred3_0)|~((f0 @ (~($true))))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.22/0.28 thf(c_0_83, plain, ((epred3_0)|~((epred2_0))|~((epred1_0))|~((epred2_0))|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.22/0.28 thf(c_0_84, plain, ((epred3_0)|~((epred2_0))|~((f0 @ (($true))))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.22/0.28 thf(c_0_85, plain, ((epred6_0)|~((f1 @ (~($true))))|~((epred4_0))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_86, plain, ((epred1_0)|(epred6_0)|~((epred5_0))), inference(spm,[status(thm)],[c_0_78, c_0_53])).
% 0.22/0.28 thf(c_0_87, plain, ((x)|(epred2_0)|~((f1 @ (~($true))))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_88, plain, ((x)|(f0 @ (($true)))|(epred1_0)|~((f1 @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_89, plain, ((f1 @ (~($true)))|(epred1_0)|(x)|(epred2_0)), inference(spm,[status(thm)],[c_0_79, c_0_80])).
% 0.22/0.28 thf(c_0_90, plain, ((epred3_0)|~((f0 @ (~($true))))|~((epred2_0))), inference(csr,[status(thm)],[c_0_81, c_0_82])).
% 0.22/0.28 thf(c_0_91, plain, ((f0 @ (~($true)))|(f0 @ (($true)))|(epred1_0)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_92, plain, ((epred3_0)|~((epred1_0))|~((epred2_0))), inference(cn,[status(thm)],[c_0_83])).
% 0.22/0.28 thf(c_0_93, plain, ((epred3_0)|~((epred2_0))|~((f0 @ (($true))))), inference(cn,[status(thm)],[c_0_84])).
% 0.22/0.28 thf(c_0_94, plain, ((x)|(epred6_0)|~((epred4_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_49]), c_0_41]), c_0_76])).
% 0.22/0.28 thf(c_0_95, plain, ((epred4_0)|(epred6_0)|(epred1_0)), inference(spm,[status(thm)],[c_0_86, c_0_64])).
% 0.22/0.28 thf(c_0_96, plain, ((epred2_0)|~((x))|~((f1 @ (($true))))|~((f0 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_97, plain, ((f0 @ (($true)))|(epred1_0)|~((x))|~((f1 @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_98, plain, ((epred1_0)|(x)|(epred2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_88]), c_0_89])).
% 0.22/0.28 thf(c_0_99, plain, ((f1 @ (($true)))|(epred2_0)|~((f0 @ (~($true))))|~((x))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.22/0.28 thf(c_0_100, plain, ((f0 @ (~($true)))|(f1 @ (($true)))|(epred1_0)|~((x))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.28 thf(c_0_101, negated_conjecture, (~((epred3_0))|~((epred6_0))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.28 thf(c_0_102, plain, ((epred3_0)|~((epred2_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_91]), c_0_92]), c_0_93])).
% 0.22/0.28 thf(c_0_103, plain, ((epred1_0)|(epred6_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_77])).
% 0.22/0.28 thf(c_0_104, plain, ((epred1_0)|(epred2_0)|~((f1 @ (($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_97]), c_0_98])).
% 0.22/0.28 thf(c_0_105, plain, ((f1 @ (($true)))|(epred1_0)|(epred2_0)|~((x))), inference(spm,[status(thm)],[c_0_99, c_0_100])).
% 0.22/0.28 thf(c_0_106, negated_conjecture, (~((epred6_0))|~((epred2_0))), inference(spm,[status(thm)],[c_0_101, c_0_102])).
% 0.22/0.28 thf(c_0_107, plain, (epred6_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_103]), c_0_41])).
% 0.22/0.28 thf(c_0_108, plain, ((epred5_0)|(f1 @ (~($true)))|(f0 @ (~($true)))|~((epred6_0))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_109, plain, ((epred4_0)|(f1 @ (($true)))|(f0 @ (~($true)))|~((epred6_0))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_110, plain, ((epred2_0)|(epred1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_105]), c_0_98])).
% 0.22/0.28 thf(c_0_111, negated_conjecture, ~((epred2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_106, c_0_107])])).
% 0.22/0.28 thf(c_0_112, plain, ((x)|~((f1 @ (~($true))))|~((f1 @ (($true))))|~((epred4_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.28 thf(c_0_113, plain, ((f1 @ (($true)))|~((epred4_0))|~((epred5_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_31]), c_0_44])).
% 0.22/0.28 thf(c_0_114, plain, ((epred5_0)|(f0 @ (($true)))|~((f1 @ (~($true))))|~((epred6_0))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_115, plain, ((f1 @ (~($true)))|(x)|(epred2_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_108]), c_0_41]), c_0_23])).
% 0.22/0.28 thf(c_0_116, plain, ((epred4_0)|(f0 @ (($true)))|~((f1 @ (($true))))|~((epred6_0))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.28 thf(c_0_117, plain, ((f1 @ (($true)))|(epred4_0)|~((epred1_0))|~((epred6_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_109]), c_0_47])).
% 0.22/0.28 thf(c_0_118, plain, (epred1_0), inference(sr,[status(thm)],[c_0_110, c_0_111])).
% 0.22/0.28 thf(c_0_119, plain, (~((f1 @ (($true))))|~((f1 @ (~($true))))|~((epred4_0))), inference(csr,[status(thm)],[c_0_112, c_0_60])).
% 0.22/0.28 thf(c_0_120, plain, (~((x))|~((epred4_0))|~((epred5_0))), inference(spm,[status(thm)],[c_0_60, c_0_113])).
% 0.22/0.28 thf(c_0_121, plain, ((epred5_0)|(x)|(epred2_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_114]), c_0_41]), c_0_115])).
% 0.22/0.28 thf(c_0_122, plain, (~((f1 @ (($true))))|~((x))|~((epred1_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_116]), c_0_69]), c_0_60])).
% 0.22/0.28 thf(c_0_123, plain, ((f1 @ (($true)))|(epred4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_117, c_0_107])]), c_0_118])])).
% 0.22/0.28 thf(c_0_124, plain, (~((epred4_0))|~((epred5_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_23]), c_0_113]), c_0_120])).
% 0.22/0.28 thf(c_0_125, plain, ((x)|(epred5_0)), inference(sr,[status(thm)],[c_0_121, c_0_111])).
% 0.22/0.28 thf(c_0_126, plain, ((epred4_0)|~((x))|~((epred1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_117]), c_0_69])).
% 0.22/0.28 thf(c_0_127, plain, ((f0 @ (($true)))|(epred4_0)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_116, c_0_107])]), c_0_123])).
% 0.22/0.28 thf(c_0_128, plain, ((f1 @ (~($true)))|(x)), inference(sr,[status(thm)],[c_0_115, c_0_111])).
% 0.22/0.28 thf(c_0_129, plain, ((x)|~((epred4_0))), inference(spm,[status(thm)],[c_0_124, c_0_125])).
% 0.22/0.28 thf(c_0_130, plain, ((epred4_0)|~((x))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_126, c_0_118])])).
% 0.22/0.28 thf(c_0_131, plain, (x), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_127]), c_0_111]), c_0_128]), c_0_129])).
% 0.22/0.28 thf(c_0_132, plain, (~((f1 @ (($true))))|~((x))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_122, c_0_118])])).
% 0.22/0.28 thf(c_0_133, plain, (epred4_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_130, c_0_131])])).
% 0.22/0.28 thf(c_0_134, plain, ~((f1 @ (($true)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_132, c_0_131])])).
% 0.22/0.28 thf(c_0_135, plain, ~((epred5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_124, c_0_133])])).
% 0.22/0.28 thf(c_0_136, plain, ((f0 @ (~($true)))|(f1 @ (~($true)))|(epred5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_108, c_0_107])])).
% 0.22/0.28 thf(c_0_137, plain, ~((f0 @ (~($true)))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_99, c_0_131])]), c_0_111]), c_0_134])).
% 0.22/0.28 thf(c_0_138, plain, ~((f1 @ (~($true)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_131])]), c_0_135])).
% 0.22/0.28 thf(c_0_139, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_136, c_0_135]), c_0_137]), c_0_138]), ['proof']).
% 0.22/0.28 % SZS output end CNFRefutation
% 0.22/0.28 % Parsed axioms : 4
% 0.22/0.28 % Removed by relevancy pruning/SinE : 0
% 0.22/0.28 % Initial clauses : 179
% 0.22/0.28 % Removed in clause preprocessing : 98
% 0.22/0.28 % Initial clauses in saturation : 81
% 0.22/0.28 % Processed clauses : 213
% 0.22/0.28 % ...of these trivial : 0
% 0.22/0.28 % ...subsumed : 72
% 0.22/0.28 % ...remaining for further processing : 140
% 0.22/0.28 % Other redundant clauses eliminated : 0
% 0.22/0.28 % Clauses deleted for lack of memory : 0
% 0.22/0.28 % Backward-subsumed : 74
% 0.22/0.28 % Backward-rewritten : 51
% 0.22/0.28 % Generated clauses : 361
% 0.22/0.28 % ...of the previous two non-redundant : 233
% 0.22/0.28 % ...aggressively subsumed : 0
% 0.22/0.28 % Contextual simplify-reflections : 59
% 0.22/0.28 % Paramodulations : 356
% 0.22/0.28 % Factorizations : 0
% 0.22/0.28 % NegExts : 0
% 0.22/0.28 % Equation resolutions : 0
% 0.22/0.28 % Disequality decompositions : 0
% 0.22/0.28 % Total rewrite steps : 56
% 0.22/0.28 % ...of those cached : 52
% 0.22/0.28 % Propositional unsat checks : 0
% 0.22/0.28 % Propositional check models : 0
% 0.22/0.28 % Propositional check unsatisfiable : 0
% 0.22/0.28 % Propositional clauses : 0
% 0.22/0.28 % Propositional clauses after purity: 0
% 0.22/0.28 % Propositional unsat core size : 0
% 0.22/0.28 % Propositional preprocessing time : 0.000
% 0.22/0.28 % Propositional encoding time : 0.000
% 0.22/0.28 % Propositional solver time : 0.000
% 0.22/0.28 % Success case prop preproc time : 0.000
% 0.22/0.28 % Success case prop encoding time : 0.000
% 0.22/0.28 % Success case prop solver time : 0.000
% 0.22/0.28 % Current number of processed clauses : 10
% 0.22/0.28 % Positive orientable unit clauses : 4
% 0.22/0.28 % Positive unorientable unit clauses: 0
% 0.22/0.28 % Negative unit clauses : 6
% 0.22/0.28 % Non-unit-clauses : 0
% 0.22/0.28 % Current number of unprocessed clauses: 8
% 0.22/0.28 % ...number of literals in the above : 25
% 0.22/0.28 % Current number of archived formulas : 0
% 0.22/0.28 % Current number of archived clauses : 130
% 0.22/0.28 % Clause-clause subsumption calls (NU) : 2519
% 0.22/0.28 % Rec. Clause-clause subsumption calls : 1291
% 0.22/0.28 % Non-unit clause-clause subsumptions : 186
% 0.22/0.28 % Unit Clause-clause subsumption calls : 75
% 0.22/0.28 % Rewrite failures with RHS unbound : 0
% 0.22/0.28 % BW rewrite match attempts : 4
% 0.22/0.28 % BW rewrite match successes : 4
% 0.22/0.28 % Condensation attempts : 0
% 0.22/0.28 % Condensation successes : 0
% 0.22/0.28 % Termbank termtop insertions : 9647
% 0.22/0.28 % Search garbage collected termcells : 1133
% 0.22/0.28
% 0.22/0.28 % -------------------------------------------------
% 0.22/0.28 % User time : 0.016 s
% 0.22/0.28 % System time : 0.003 s
% 0.22/0.28 % Total time : 0.019 s
% 0.22/0.28 % Maximum resident set size: 3828 pages
% 0.22/0.28
% 0.22/0.28 % -------------------------------------------------
% 0.22/0.28 % User time : 0.043 s
% 0.22/0.28 % System time : 0.011 s
% 0.22/0.28 % Total time : 0.054 s
% 0.22/0.28 % Maximum resident set size: 4864 pages
% 0.22/0.28 % E exiting
%------------------------------------------------------------------------------