%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:23 AM UTC 2026
% Result : Theorem 0.09s 0.25s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n011.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 17:14:46 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running higher-order theorem proving
% 0.09/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.e51fcHPygA/E---3.1_383941.p
% 0.09/0.25 % Version: 3.5.1-ho
% 0.09/0.25 % Preprocessing class: HSSSSMSSSSMCHSA.
% 0.09/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.09/0.25 % Starting lpo8_s with 1500s (5) cores
% 0.09/0.25 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 0.09/0.25 % Starting ehoh_best_sine_rwall with 300s (1) cores
% 0.09/0.25 % Starting sh1 with 300s (1) cores
% 0.09/0.25 % lpo8_s with pid 383954 completed with status 0
% 0.09/0.25 % Result found by lpo8_s
% 0.09/0.25 % Preprocessing class: HSSSSMSSSSMCHSA.
% 0.09/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.09/0.25 % Starting lpo8_s with 1500s (5) cores
% 0.09/0.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 0.09/0.25 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 0.09/0.25 % Search class: HGUSF-FFMF11-SHSFFFBC
% 0.09/0.25 % partial match(3): HGUSF-FFMF33-SHSFFMBC
% 0.09/0.25 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.09/0.25 % Starting SubtermCWHack with 151s (1) cores
% 0.09/0.25 % Starting lpo8_s with 901s (1) cores
% 0.09/0.25 % Starting ehoh_best_nonlift_rwall with 151s (1) cores
% 0.09/0.25 % Starting ehoh_best_sine_rwall with 151s (1) cores
% 0.09/0.25 % Starting sh1 with 146s (1) cores
% 0.09/0.25 % SubtermCWHack with pid 383958 completed with status 10
% 0.09/0.25 % lpo8_s with pid 383960 completed with status 0
% 0.09/0.25 % Result found by lpo8_s
% 0.09/0.25 % Preprocessing class: HSSSSMSSSSMCHSA.
% 0.09/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.09/0.25 % Starting lpo8_s with 1500s (5) cores
% 0.09/0.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 0.09/0.25 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 0.09/0.25 % Search class: HGUSF-FFMF11-SHSFFFBC
% 0.09/0.25 % partial match(3): HGUSF-FFMF33-SHSFFMBC
% 0.09/0.25 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.09/0.25 % Starting SubtermCWHack with 151s (1) cores
% 0.09/0.25 % Starting lpo8_s with 901s (1) cores
% 0.09/0.25 % Preprocessing time : 0.002 s
% 0.09/0.25 % Presaturation interreduction done
% 0.09/0.25
% 0.09/0.25 % Proof found!
% 0.09/0.25 % SZS status Theorem
% 0.09/0.25 % SZS output start CNFRefutation
% 0.09/0.25 thf(decl_23, type, eps: ($i > $o) > $i).
% 0.09/0.25 thf(decl_24, type, case: ($o > $o) > $i > $i > $i > $i > $i).
% 0.09/0.25 thf(decl_25, type, f: $o > $o).
% 0.09/0.25 thf(decl_26, type, esk1_0: $i).
% 0.09/0.25 thf(decl_27, type, epred1_0: $i > $o).
% 0.09/0.25 thf(decl_28, type, epred2_1: $i > $o).
% 0.09/0.25 thf(decl_29, type, epred3_1: $i > $o).
% 0.09/0.25 thf(decl_30, type, epred4_1: $i > $o).
% 0.09/0.25 thf(decl_31, type, esk5_0: $o).
% 0.09/0.25 thf(conj, conjecture, ![X2:$i]:(((case @ f @ X2 @ X2 @ X2 @ X2)=(X2))), file('/export/starexec/sandbox/tmp/tmp.e51fcHPygA/E---3.1_383941.p', conj)).
% 0.09/0.25 thf(caseood, axiom, ((case)=(^[X3:$o > $o, X2:$i, X4:$i, X5:$i, X6:$i]:(eps @ (^[X7:$i]:(((((((((((X3)=(^[X8:$o]:(~($true)))))&(((X7)=(X2)))))|(((((X3)=($not)))&(((X7)=(X4)))))))|(((((X3)=(^[X8:$o]:((X8)))))&(((X7)=(X5)))))))|(((((X3)=(^[X8:$o]:(($true)))))&(((X7)=(X6))))))))))), file('/export/starexec/sandbox/tmp/tmp.e51fcHPygA/E---3.1_383941.p', caseood)).
% 0.09/0.25 thf(choiceax, axiom, ![X1:$i > $o]:((?[X2:$i]:((X1 @ X2))=>(X1 @ (eps @ X1)))), file('/export/starexec/sandbox/tmp/tmp.e51fcHPygA/E---3.1_383941.p', choiceax)).
% 0.09/0.25 thf(c_0_3, plain, ![X22:$i, X23:$o, X24:$o, X25:$o]:((((((((((~(f @ ((X25)))|($true)|(~(f @ ((X24)))|(X24)|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(f @ ((X24)))|(X24)|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(f @ ((X24)))|(X24)|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((~(f @ ((X25)))|($true)|(~(X24)|(f @ ((X24)))|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(X24)|(f @ ((X24)))|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(X24)|(f @ ((X24)))|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))))&(((~(f @ ((X25)))|($true)|(((X22)=(esk1_0))|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(((X22)=(esk1_0))|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(((X22)=(esk1_0))|(((f)=($not))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))))&(((((~(f @ ((X25)))|($true)|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((~(f @ ((X25)))|($true)|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))))&(((~(f @ ((X25)))|($true)|(((X22)=(esk1_0))|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(((X22)=(esk1_0))|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(((X22)=(esk1_0))|(((X22)=(esk1_0))|(~(f @ ((X23)))|~($true))))|~(epred1_0 @ X22)))))&((((((~(f @ ((X25)))|($true)|(~(f @ ((X24)))|(X24)|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(f @ ((X24)))|(X24)|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(f @ ((X24)))|(X24)|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((~(f @ ((X25)))|($true)|(~(X24)|(f @ ((X24)))|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(X24)|(f @ ((X24)))|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(X24)|(f @ ((X24)))|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))))&(((~(f @ ((X25)))|($true)|(((X22)=(esk1_0))|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(((X22)=(esk1_0))|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(((X22)=(esk1_0))|(((f)=($not))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))))&(((((~(f @ ((X25)))|($true)|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((~(f @ ((X25)))|($true)|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))))&(((~(f @ ((X25)))|($true)|(((X22)=(esk1_0))|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(((X22)=(esk1_0))|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(((X22)=(esk1_0))|(((X22)=(esk1_0))|(($true)|(f @ ((X23))))))|~(epred1_0 @ X22))))))&((((((~(f @ ((X25)))|($true)|(~(f @ ((X24)))|(X24)|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(f @ ((X24)))|(X24)|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(f @ ((X24)))|(X24)|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((~(f @ ((X25)))|($true)|(~(X24)|(f @ ((X24)))|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(X24)|(f @ ((X24)))|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(X24)|(f @ ((X24)))|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22))))&(((~(f @ ((X25)))|($true)|(((X22)=(esk1_0))|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(((X22)=(esk1_0))|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(((X22)=(esk1_0))|(((f)=($not))|((X22)=(esk1_0))))|~(epred1_0 @ X22))))&(((((~(f @ ((X25)))|($true)|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(f @ ((X24)))|(X24)|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((~(f @ ((X25)))|($true)|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(~(X24)|(f @ ((X24)))|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22))))&(((~(f @ ((X25)))|($true)|(((X22)=(esk1_0))|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22))&(~($true)|(f @ ((X25)))|(((X22)=(esk1_0))|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22)))&(((X22)=(esk1_0))|(((X22)=(esk1_0))|(((X22)=(esk1_0))|((X22)=(esk1_0))))|~(epred1_0 @ X22))))))&(((((((~(epred2_1 @ X22)|(epred2_1 @ X22)|($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))&(~(f @ $false)|(epred2_1 @ X22)|($true)|((X22)!=(esk1_0))|(epred1_0 @ X22)))&((~(epred2_1 @ X22)|~(f @ $true)|($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))&(~(f @ $false)|~(f @ $true)|($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))))&((~(epred2_1 @ X22)|(f @ $true)|~($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))&((epred2_1 @ X22)|(f @ $false)|~($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))))&(((f)!=($not))|((X22)!=(esk1_0))|(epred1_0 @ X22)))&((((~(epred3_1 @ X22)|(epred3_1 @ X22)|~(epred3_1 @ X22)|((X22)!=(esk1_0))|(epred1_0 @ X22))&(~(f @ $false)|(epred3_1 @ X22)|~(epred3_1 @ X22)|((X22)!=(esk1_0))|(epred1_0 @ X22)))&((~(epred3_1 @ X22)|~(f @ $true)|~(epred3_1 @ X22)|((X22)!=(esk1_0))|(epred1_0 @ X22))&(~(f @ $false)|~(f @ $true)|~(epred3_1 @ X22)|((X22)!=(esk1_0))|(epred1_0 @ X22))))&((~(epred3_1 @ X22)|(f @ $true)|(epred3_1 @ X22)|((X22)!=(esk1_0))|(epred1_0 @ X22))&((epred3_1 @ X22)|(f @ $false)|(epred3_1 @ X22)|((X22)!=(esk1_0))|(epred1_0 @ X22)))))&((((~(epred4_1 @ X22)|(epred4_1 @ X22)|~($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))&(~(f @ $false)|(epred4_1 @ X22)|~($true)|((X22)!=(esk1_0))|(epred1_0 @ X22)))&((~(epred4_1 @ X22)|~(f @ $true)|~($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))&(~(f @ $false)|~(f @ $true)|~($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))))&((~(epred4_1 @ X22)|(f @ $true)|($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))&((epred4_1 @ X22)|(f @ $false)|($true)|((X22)!=(esk1_0))|(epred1_0 @ X22))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fool_unroll,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])])])])])).
% 0.09/0.25 thf(c_0_4, plain, ![X2:$i]:(((epred1_0 @ X2)|((f)!=($not))|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.09/0.25 thf(c_0_5, plain, ![X2:$i]:(((f @ (($true)))|(epred1_0 @ X2)|~((epred2_1 @ X2))|~(($true))|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.09/0.25 thf(c_0_6, plain, ![X2:$i]:(((epred2_1 @ X2)|(f @ (~($true)))|(epred1_0 @ X2)|~(($true))|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.09/0.25 thf(c_0_7, plain, ((epred1_0 @ esk1_0)|(($not)!=(f))), inference(er,[status(thm)],[c_0_4])).
% 0.09/0.25 thf(c_0_8, plain, ![X2:$i]:(((epred1_0 @ X2)|(f @ (($true)))|((X2)!=(esk1_0))|~((epred2_1 @ X2)))), inference(cn,[status(thm)],[c_0_5])).
% 0.09/0.25 thf(c_0_9, plain, ![X2:$i]:(((epred1_0 @ X2)|(epred2_1 @ X2)|(f @ (~($true)))|((X2)!=(esk1_0)))), inference(cn,[status(thm)],[c_0_6])).
% 0.09/0.25 thf(c_0_10, plain, ((epred1_0 @ esk1_0)|(~((esk5_0))<~>(f @ ((esk5_0))))), inference(neg_ext,[status(thm)],[c_0_7])).
% 0.09/0.25 thf(c_0_11, plain, ((epred1_0 @ esk1_0)|(f @ (($true)))|~((epred2_1 @ esk1_0))), inference(er,[status(thm)],[c_0_8])).
% 0.09/0.25 thf(c_0_12, plain, ((epred1_0 @ esk1_0)|(epred2_1 @ esk1_0)|(f @ (~($true)))), inference(er,[status(thm)],[c_0_9])).
% 0.09/0.25 thf(c_0_13, negated_conjecture, ~(![X2:$i]:(((case @ f @ X2 @ X2 @ X2 @ X2)=(X2)))), inference(assume_negation,[status(cth)],[conj])).
% 0.09/0.25 thf(c_0_14, plain, ((case)=(^[Z0:$o > $o, Z1:$i, Z2:$i, Z3:$i, Z4:$i]:(eps @ (^[Z5:$i]:(((((((((((Z0)=(^[Z6:$o]:(~($true)))))&(((Z5)=(Z1)))))|(((((Z0)=($not)))&(((Z5)=(Z2)))))))|(((((Z0)=(^[Z6:$o]:((Z6)))))&(((Z5)=(Z3)))))))|(((((Z0)=(^[Z6:$o]:(($true)))))&((Z5)))))))))), inference(fof_simplification,[status(thm)],[caseood])).
% 0.09/0.25 thf(c_0_15, plain, ![X16:$i > $o, X17:$i]:((~(X16 @ X17)|(X16 @ (eps @ X16)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[choiceax])])])])).
% 0.09/0.25 thf(c_0_16, plain, ((epred1_0 @ esk1_0)|(esk5_0)|~((f @ (~($true))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_10])])).
% 0.09/0.25 thf(c_0_17, plain, ((f @ (~($true)))|(epred1_0 @ esk1_0)|(f @ (($true)))), inference(spm,[status(thm)],[c_0_11, c_0_12])).
% 0.09/0.25 thf(c_0_18, plain, ((epred1_0 @ esk1_0)|(f @ (($true)))|~((esk5_0))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_10])])).
% 0.09/0.25 thf(c_0_19, negated_conjecture, ~(![X2:$i]:(((eps @ (^[Z0:$i]:(((((((((![X12:$o]:((((f @ ((X12))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f)=($not)))&(((Z0)=(X2)))))))|(((![X13:$o]:((((f @ ((X13))))<=>((X13)))))&(((Z0)=(X2)))))))|(((![X14:$o]:((((f @ ((X14))))<=>($true))))&(((Z0)=(X2)))))))))=(X2)))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[c_0_13, c_0_14])])).
% 0.09/0.25 thf(c_0_20, plain, ![X2:$i]:(((epred1_0 @ X2)|~((epred3_1 @ X2))|~((f @ (($true))))|~((epred3_1 @ X2))|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.09/0.25 thf(c_0_21, plain, ![X2:$i]:((((X2)=(esk1_0))|((X2)=(esk1_0))|((X2)=(esk1_0))|((X2)=(esk1_0))|~((epred1_0 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.09/0.25 thf(c_0_22, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (eps @ X1))|~((X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_23, plain, ((f @ (($true)))|(epred1_0 @ esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18])).
% 0.09/0.25 thf(c_0_24, negated_conjecture, ((eps @ (^[Z0:$i]:(((((((((![X12:$o]:((((f @ ((X12))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f)=($not)))&(((Z0)=(esk1_0)))))))|(((![X13:$o]:((((f @ ((X13))))<=>((X13)))))&(((Z0)=(esk1_0)))))))|(((![X14:$o]:((((f @ ((X14))))<=>($true))))&(((Z0)=(esk1_0)))))))))!=(esk1_0)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])])).
% 0.09/0.25 thf(c_0_25, plain, ![X21:$i]:(((epred1_0 @ X21)<=>((![X18:$o]:(((f @ ((X18)))<=>~(($true))))&((X21)=(esk1_0)))|(((f)=($not))&((X21)=(esk1_0)))|(![X19:$o]:(((f @ ((X19)))<=>(X19)))&((X21)=(esk1_0)))|(![X20:$o]:(((f @ ((X20)))<=>($true)))&((X21)=(esk1_0)))))), introduced(definition)).
% 0.09/0.25 thf(c_0_26, plain, ![X2:$i]:(((epred1_0 @ X2)|~((f @ (~($true))))|~((f @ (($true))))|~(($true))|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.09/0.25 thf(c_0_27, plain, ![X2:$i]:(((epred1_0 @ X2)|((X2)!=(esk1_0))|~((epred3_1 @ X2))|~((f @ (($true)))))), inference(cn,[status(thm)],[c_0_20])).
% 0.09/0.25 thf(c_0_28, plain, ![X2:$i]:((((X2)=(esk1_0))|~((epred1_0 @ X2)))), inference(cn,[status(thm)],[c_0_21])).
% 0.09/0.25 thf(c_0_29, plain, ((epred1_0 @ (eps @ epred1_0))|(f @ (($true)))), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 0.09/0.25 thf(c_0_30, negated_conjecture, ((eps @ epred1_0)!=(esk1_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_24]), c_0_25])).
% 0.09/0.25 thf(c_0_31, plain, ![X2:$i]:(((epred3_1 @ X2)|(f @ (~($true)))|(epred3_1 @ X2)|(epred1_0 @ X2)|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.09/0.25 thf(c_0_32, plain, ![X2:$i]:(((epred1_0 @ X2)|((X2)!=(esk1_0))|~((f @ (($true))))|~((f @ (~($true)))))), inference(cn,[status(thm)],[c_0_26])).
% 0.09/0.25 thf(c_0_33, plain, ((epred1_0 @ esk1_0)|~((f @ (($true))))|~((epred3_1 @ esk1_0))), inference(er,[status(thm)],[c_0_27])).
% 0.09/0.25 thf(c_0_34, plain, (f @ (($true))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_30])).
% 0.09/0.25 thf(c_0_35, plain, ![X2:$i]:(((epred1_0 @ X2)|(epred3_1 @ X2)|(f @ (~($true)))|((X2)!=(esk1_0)))), inference(cn,[status(thm)],[c_0_31])).
% 0.09/0.25 thf(c_0_36, plain, ((epred1_0 @ esk1_0)|~((f @ (($true))))|~((f @ (~($true))))), inference(er,[status(thm)],[c_0_32])).
% 0.09/0.25 thf(c_0_37, plain, ((epred1_0 @ esk1_0)|~((epred3_1 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 0.09/0.25 thf(c_0_38, plain, ((epred1_0 @ esk1_0)|(epred3_1 @ esk1_0)|(f @ (~($true)))), inference(er,[status(thm)],[c_0_35])).
% 0.09/0.25 thf(c_0_39, plain, ((epred1_0 @ esk1_0)|~((f @ (~($true))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_34])])).
% 0.09/0.25 thf(c_0_40, plain, (epred1_0 @ esk1_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39])).
% 0.09/0.25 thf(c_0_41, plain, (epred1_0 @ (eps @ epred1_0)), inference(spm,[status(thm)],[c_0_22, c_0_40])).
% 0.09/0.25 thf(c_0_42, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_41]), c_0_30]), ['proof']).
% 0.09/0.25 % SZS output end CNFRefutation
% 0.09/0.25 % Parsed axioms : 6
% 0.09/0.25 % Removed by relevancy pruning/SinE : 3
% 0.09/0.25 % Initial clauses : 75
% 0.09/0.25 % Removed in clause preprocessing : 40
% 0.09/0.25 % Initial clauses in saturation : 35
% 0.09/0.25 % Processed clauses : 77
% 0.09/0.25 % ...of these trivial : 1
% 0.09/0.25 % ...subsumed : 24
% 0.09/0.25 % ...remaining for further processing : 52
% 0.09/0.25 % Other redundant clauses eliminated : 9
% 0.09/0.25 % Clauses deleted for lack of memory : 0
% 0.09/0.25 % Backward-subsumed : 7
% 0.09/0.25 % Backward-rewritten : 13
% 0.09/0.25 % Generated clauses : 69
% 0.09/0.25 % ...of the previous two non-redundant : 37
% 0.09/0.25 % ...aggressively subsumed : 0
% 0.09/0.25 % Contextual simplify-reflections : 2
% 0.09/0.25 % Paramodulations : 17
% 0.09/0.25 % Factorizations : 0
% 0.09/0.25 % NegExts : 1
% 0.09/0.25 % Equation resolutions : 9
% 0.09/0.25 % Disequality decompositions : 0
% 0.09/0.25 % Total rewrite steps : 15
% 0.09/0.25 % ...of those cached : 12
% 0.09/0.25 % Propositional unsat checks : 0
% 0.09/0.25 % Propositional check models : 0
% 0.09/0.25 % Propositional check unsatisfiable : 0
% 0.09/0.25 % Propositional clauses : 0
% 0.09/0.25 % Propositional clauses after purity: 0
% 0.09/0.25 % Propositional unsat core size : 0
% 0.09/0.25 % Propositional preprocessing time : 0.000
% 0.09/0.25 % Propositional encoding time : 0.000
% 0.09/0.25 % Propositional solver time : 0.000
% 0.09/0.25 % Success case prop preproc time : 0.000
% 0.09/0.25 % Success case prop encoding time : 0.000
% 0.09/0.25 % Success case prop solver time : 0.000
% 0.09/0.25 % Current number of processed clauses : 8
% 0.09/0.25 % Positive orientable unit clauses : 3
% 0.09/0.25 % Positive unorientable unit clauses: 0
% 0.09/0.25 % Negative unit clauses : 1
% 0.09/0.25 % Non-unit-clauses : 4
% 0.09/0.25 % Current number of unprocessed clauses: 8
% 0.09/0.25 % ...number of literals in the above : 24
% 0.09/0.25 % Current number of archived formulas : 0
% 0.09/0.25 % Current number of archived clauses : 35
% 0.09/0.25 % Clause-clause subsumption calls (NU) : 110
% 0.09/0.25 % Rec. Clause-clause subsumption calls : 104
% 0.09/0.25 % Non-unit clause-clause subsumptions : 41
% 0.09/0.25 % Unit Clause-clause subsumption calls : 2
% 0.09/0.25 % Rewrite failures with RHS unbound : 0
% 0.09/0.25 % BW rewrite match attempts : 2
% 0.09/0.25 % BW rewrite match successes : 2
% 0.09/0.25 % Condensation attempts : 77
% 0.09/0.25 % Condensation successes : 8
% 0.09/0.25 % Termbank termtop insertions : 5104
% 0.09/0.25 % Search garbage collected termcells : 907
% 0.09/0.25
% 0.09/0.25 % -------------------------------------------------
% 0.09/0.25 % User time : 0.009 s
% 0.09/0.25 % System time : 0.007 s
% 0.09/0.25 % Total time : 0.016 s
% 0.09/0.25 % Maximum resident set size: 4152 pages
% 0.09/0.25
% 0.09/0.25 % -------------------------------------------------
% 0.09/0.25 % User time : 0.018 s
% 0.09/0.25 % System time : 0.020 s
% 0.09/0.25 % Total time : 0.038 s
% 0.09/0.25 % Maximum resident set size: 4864 pages
% 0.09/0.25 % E exiting
%------------------------------------------------------------------------------