%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO545^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 : 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:43:23 AM UTC 2026
% Result : Theorem 0.31s 0.26s
% Output : CNFRefutation 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO545^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n020.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 17:15: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.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.j9TCevGGfQ/E---3.1_1340373.p
% 0.31/0.26 % Version: 3.5.1-ho
% 0.31/0.26 % Preprocessing class: HSSSSMSSSSMCHSA.
% 0.31/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.31/0.26 % Starting lpo8_s with 1500s (5) cores
% 0.31/0.26 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 0.31/0.26 % Starting ehoh_best_sine_rwall with 300s (1) cores
% 0.31/0.26 % Starting sh1 with 300s (1) cores
% 0.31/0.26 % lpo8_s with pid 1340408 completed with status 0
% 0.31/0.26 % Result found by lpo8_s
% 0.31/0.26 % Preprocessing class: HSSSSMSSSSMCHSA.
% 0.31/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.31/0.26 % Starting lpo8_s with 1500s (5) cores
% 0.31/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 0.31/0.26 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 0.31/0.26 % Search class: HGUSF-FFMF11-SHSFFFBC
% 0.31/0.26 % partial match(3): HGUSF-FFMF33-SHSFFMBC
% 0.31/0.26 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.31/0.26 % Starting SubtermCWHack with 151s (1) cores
% 0.31/0.26 % Starting lpo8_s with 901s (1) cores
% 0.31/0.26 % Starting ehoh_best_nonlift_rwall with 151s (1) cores
% 0.31/0.26 % Starting ehoh_best_sine_rwall with 151s (1) cores
% 0.31/0.26 % Starting sh1 with 146s (1) cores
% 0.31/0.26 % SubtermCWHack with pid 1340413 completed with status 10
% 0.31/0.26 % lpo8_s with pid 1340415 completed with status 0
% 0.31/0.26 % Result found by lpo8_s
% 0.31/0.26 % Preprocessing class: HSSSSMSSSSMCHSA.
% 0.31/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.31/0.26 % Starting lpo8_s with 1500s (5) cores
% 0.31/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 0.31/0.26 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 0.31/0.26 % Search class: HGUSF-FFMF11-SHSFFFBC
% 0.31/0.26 % partial match(3): HGUSF-FFMF33-SHSFFMBC
% 0.31/0.26 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.31/0.26 % Starting SubtermCWHack with 151s (1) cores
% 0.31/0.26 % Starting lpo8_s with 901s (1) cores
% 0.31/0.26 % Preprocessing time : 0.002 s
% 0.31/0.26 % Presaturation interreduction done
% 0.31/0.26
% 0.31/0.26 % Proof found!
% 0.31/0.26 % SZS status Theorem
% 0.31/0.26 % SZS output start CNFRefutation
% 0.31/0.26 thf(decl_23, type, eps: ($i > $o) > $i).
% 0.31/0.26 thf(decl_24, type, case: ($o > $o) > $i > $i > $i > $i > $i).
% 0.31/0.26 thf(decl_25, type, f: $o > $o).
% 0.31/0.26 thf(decl_26, type, esk1_0: $i).
% 0.31/0.26 thf(decl_27, type, esk2_0: $i).
% 0.31/0.26 thf(decl_28, type, esk3_0: $i).
% 0.31/0.26 thf(decl_29, type, esk4_0: $i).
% 0.31/0.26 thf(decl_30, type, epred1_0: $i > $o).
% 0.31/0.26 thf(decl_31, type, epred2_1: $i > $o).
% 0.31/0.26 thf(decl_32, type, epred3_1: $i > $o).
% 0.31/0.26 thf(decl_33, type, epred4_1: $i > $o).
% 0.31/0.26 thf(decl_34, type, esk5_0: $o).
% 0.31/0.26 thf(conj, conjecture, ![X2:$i, X4:$i, X5:$i, X6:$i]:((((case @ f @ X2 @ X4 @ X5 @ X6)=(X2))|((case @ f @ X2 @ X4 @ X5 @ X6)=(X4))|((case @ f @ X2 @ X4 @ X5 @ X6)=(X5))|((case @ f @ X2 @ X4 @ X5 @ X6)=(X6)))), file('/export/starexec/sandbox/tmp/tmp.j9TCevGGfQ/E---3.1_1340373.p', conj)).
% 0.31/0.26 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.j9TCevGGfQ/E---3.1_1340373.p', caseood)).
% 0.31/0.26 thf(choiceax, axiom, ![X1:$i > $o]:((?[X2:$i]:((X1 @ X2))=>(X1 @ (eps @ X1)))), file('/export/starexec/sandbox/tmp/tmp.j9TCevGGfQ/E---3.1_1340373.p', choiceax)).
% 0.31/0.27 thf(c_0_3, plain, ![X49:$i, X50:$o, X51:$o, X52:$o]:((((((((((~(f @ ((X52)))|($true)|(~(f @ ((X51)))|(X51)|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(f @ ((X51)))|(X51)|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f @ ((X51)))|(X51)|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((~(f @ ((X52)))|($true)|(~(X51)|(f @ ((X51)))|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(X51)|(f @ ((X51)))|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f @ ((X51)))|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))))&(((~(f @ ((X52)))|($true)|(((X49)=(esk3_0))|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(((X49)=(esk3_0))|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((f)=($not))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))))&(((((~(f @ ((X52)))|($true)|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((~(f @ ((X52)))|($true)|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))))&(((~(f @ ((X52)))|($true)|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(~(f @ ((X50)))|~($true))))|~(epred1_0 @ X49)))))&((((((~(f @ ((X52)))|($true)|(~(f @ ((X51)))|(X51)|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(f @ ((X51)))|(X51)|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f @ ((X51)))|(X51)|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((~(f @ ((X52)))|($true)|(~(X51)|(f @ ((X51)))|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(X51)|(f @ ((X51)))|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f @ ((X51)))|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))))&(((~(f @ ((X52)))|($true)|(((X49)=(esk3_0))|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(((X49)=(esk3_0))|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((f)=($not))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))))&(((((~(f @ ((X52)))|($true)|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((~(f @ ((X52)))|($true)|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))))&(((~(f @ ((X52)))|($true)|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(($true)|(f @ ((X50))))))|~(epred1_0 @ X49))))))&((((((~(f @ ((X52)))|($true)|(~(f @ ((X51)))|(X51)|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(f @ ((X51)))|(X51)|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f @ ((X51)))|(X51)|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((~(f @ ((X52)))|($true)|(~(X51)|(f @ ((X51)))|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(X51)|(f @ ((X51)))|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f @ ((X51)))|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))))&(((~(f @ ((X52)))|($true)|(((X49)=(esk3_0))|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(((X49)=(esk3_0))|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((f)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))))&(((((~(f @ ((X52)))|($true)|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f @ ((X51)))|(X51)|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((~(f @ ((X52)))|($true)|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f @ ((X51)))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))))&(((~(f @ ((X52)))|($true)|(((X49)=(esk3_0))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f @ ((X52)))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))))))&(((((((~(epred2_1 @ X49)|(epred2_1 @ X49)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))&(~(f @ $false)|(epred2_1 @ X49)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49)))&((~(epred2_1 @ X49)|~(f @ $true)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))&(~(f @ $false)|~(f @ $true)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))))&((~(epred2_1 @ X49)|(f @ $true)|~($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))&((epred2_1 @ X49)|(f @ $false)|~($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))))&(((f)!=($not))|((X49)!=(esk2_0))|(epred1_0 @ X49)))&((((~(epred3_1 @ X49)|(epred3_1 @ X49)|~(epred3_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))&(~(f @ $false)|(epred3_1 @ X49)|~(epred3_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49)))&((~(epred3_1 @ X49)|~(f @ $true)|~(epred3_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))&(~(f @ $false)|~(f @ $true)|~(epred3_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))))&((~(epred3_1 @ X49)|(f @ $true)|(epred3_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))&((epred3_1 @ X49)|(f @ $false)|(epred3_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49)))))&((((~(epred4_1 @ X49)|(epred4_1 @ X49)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))&(~(f @ $false)|(epred4_1 @ X49)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49)))&((~(epred4_1 @ X49)|~(f @ $true)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))&(~(f @ $false)|~(f @ $true)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))))&((~(epred4_1 @ X49)|(f @ $true)|($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))&((epred4_1 @ X49)|(f @ $false)|($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))))))), 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.31/0.27 thf(c_0_4, plain, ![X2:$i]:(((epred1_0 @ X2)|((f)!=($not))|((X2)!=(esk2_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.31/0.27 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.31/0.27 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.31/0.27 thf(c_0_7, plain, ((epred1_0 @ esk2_0)|(($not)!=(f))), inference(er,[status(thm)],[c_0_4])).
% 0.31/0.27 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.31/0.27 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.31/0.27 thf(c_0_10, plain, ((epred1_0 @ esk2_0)|(~((esk5_0))<~>(f @ ((esk5_0))))), inference(neg_ext,[status(thm)],[c_0_7])).
% 0.31/0.27 thf(c_0_11, plain, ((epred1_0 @ esk1_0)|(f @ (($true)))|~((epred2_1 @ esk1_0))), inference(er,[status(thm)],[c_0_8])).
% 0.31/0.27 thf(c_0_12, plain, ((epred1_0 @ esk1_0)|(epred2_1 @ esk1_0)|(f @ (~($true)))), inference(er,[status(thm)],[c_0_9])).
% 0.31/0.27 thf(c_0_13, negated_conjecture, ~(![X2:$i, X4:$i, X5:$i, X6:$i]:((((case @ f @ X2 @ X4 @ X5 @ X6)=(X2))|((case @ f @ X2 @ X4 @ X5 @ X6)=(X4))|((case @ f @ X2 @ X4 @ X5 @ X6)=(X5))|((case @ f @ X2 @ X4 @ X5 @ X6)=(X6))))), inference(assume_negation,[status(cth)],[conj])).
% 0.31/0.27 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.31/0.27 thf(c_0_15, plain, ![X2:$i]:(((epred1_0 @ X2)|~((epred3_1 @ X2))|~((f @ (($true))))|~((epred3_1 @ X2))|((X2)!=(esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.31/0.27 thf(c_0_16, plain, ![X2:$i]:(((epred3_1 @ X2)|(f @ (~($true)))|(epred3_1 @ X2)|(epred1_0 @ X2)|((X2)!=(esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.31/0.27 thf(c_0_17, plain, ![X31:$i > $o, X32:$i]:((~(X31 @ X32)|(X31 @ (eps @ X31)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[choiceax])])])])).
% 0.31/0.27 thf(c_0_18, plain, ((epred1_0 @ esk2_0)|(esk5_0)|~((f @ (~($true))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_10])])).
% 0.31/0.27 thf(c_0_19, plain, ((f @ (~($true)))|(epred1_0 @ esk1_0)|(f @ (($true)))), inference(spm,[status(thm)],[c_0_11, c_0_12])).
% 0.31/0.27 thf(c_0_20, plain, ((epred1_0 @ esk2_0)|(f @ (($true)))|~((esk5_0))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_10])])).
% 0.31/0.27 thf(c_0_21, negated_conjecture, ~(![X2:$i, X4:$i, X5:$i, X6:$i]:((((eps @ (^[Z0:$i]:(((((((((![X15:$o]:((((f @ ((X15))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f)=($not)))&(((Z0)=(X4)))))))|(((![X16:$o]:((((f @ ((X16))))<=>((X16)))))&(((Z0)=(X5)))))))|(((![X17:$o]:((((f @ ((X17))))<=>($true))))&(((Z0)=(X6)))))))))=(X2))|((eps @ (^[Z0:$i]:(((((((((![X18:$o]:((((f @ ((X18))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f)=($not)))&(((Z0)=(X4)))))))|(((![X19:$o]:((((f @ ((X19))))<=>((X19)))))&(((Z0)=(X5)))))))|(((![X20:$o]:((((f @ ((X20))))<=>($true))))&(((Z0)=(X6)))))))))=(X4))|((eps @ (^[Z0:$i]:(((((((((![X21:$o]:((((f @ ((X21))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f)=($not)))&(((Z0)=(X4)))))))|(((![X22:$o]:((((f @ ((X22))))<=>((X22)))))&(((Z0)=(X5)))))))|(((![X23:$o]:((((f @ ((X23))))<=>($true))))&(((Z0)=(X6)))))))))=(X5))|((eps @ (^[Z0:$i]:(((((((((![X24:$o]:((((f @ ((X24))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f)=($not)))&(((Z0)=(X4)))))))|(((![X25:$o]:((((f @ ((X25))))<=>((X25)))))&(((Z0)=(X5)))))))|(((![X26:$o]:((((f @ ((X26))))<=>($true))))&(((Z0)=(X6)))))))))=(X6))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[c_0_13, c_0_14])])).
% 0.31/0.27 thf(c_0_22, plain, ![X2:$i]:(((epred1_0 @ X2)|((X2)!=(esk3_0))|~((epred3_1 @ X2))|~((f @ (($true)))))), inference(cn,[status(thm)],[c_0_15])).
% 0.31/0.27 thf(c_0_23, plain, ![X2:$i]:(((epred1_0 @ X2)|(epred3_1 @ X2)|(f @ (~($true)))|((X2)!=(esk3_0)))), inference(cn,[status(thm)],[c_0_16])).
% 0.31/0.27 thf(c_0_24, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (eps @ X1))|~((X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.31/0.27 thf(c_0_25, plain, ((f @ (($true)))|(epred1_0 @ esk1_0)|(epred1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_19]), c_0_20])).
% 0.31/0.27 thf(c_0_26, negated_conjecture, (((((eps @ (^[Z0:$i]:(((((((((![X15:$o]:((((f @ ((X15))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f)=($not)))&(((Z0)=(esk2_0)))))))|(((![X16:$o]:((((f @ ((X16))))<=>((X16)))))&(((Z0)=(esk3_0)))))))|(((![X17:$o]:((((f @ ((X17))))<=>($true))))&(((Z0)=(esk4_0)))))))))!=(esk1_0))&((eps @ (^[Z0:$i]:(((((((((![X18:$o]:((((f @ ((X18))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f)=($not)))&(((Z0)=(esk2_0)))))))|(((![X19:$o]:((((f @ ((X19))))<=>((X19)))))&(((Z0)=(esk3_0)))))))|(((![X20:$o]:((((f @ ((X20))))<=>($true))))&(((Z0)=(esk4_0)))))))))!=(esk2_0)))&((eps @ (^[Z0:$i]:(((((((((![X21:$o]:((((f @ ((X21))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f)=($not)))&(((Z0)=(esk2_0)))))))|(((![X22:$o]:((((f @ ((X22))))<=>((X22)))))&(((Z0)=(esk3_0)))))))|(((![X23:$o]:((((f @ ((X23))))<=>($true))))&(((Z0)=(esk4_0)))))))))!=(esk3_0)))&((eps @ (^[Z0:$i]:(((((((((![X24:$o]:((((f @ ((X24))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f)=($not)))&(((Z0)=(esk2_0)))))))|(((![X25:$o]:((((f @ ((X25))))<=>((X25)))))&(((Z0)=(esk3_0)))))))|(((![X26:$o]:((((f @ ((X26))))<=>($true))))&(((Z0)=(esk4_0)))))))))!=(esk4_0))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])])).
% 0.31/0.27 thf(c_0_27, plain, ![X36:$i]:(((epred1_0 @ X36)<=>((![X33:$o]:(((f @ ((X33)))<=>~(($true))))&((X36)=(esk1_0)))|(((f)=($not))&((X36)=(esk2_0)))|(![X34:$o]:(((f @ ((X34)))<=>(X34)))&((X36)=(esk3_0)))|(![X35:$o]:(((f @ ((X35)))<=>($true)))&((X36)=(esk4_0)))))), introduced(definition)).
% 0.31/0.27 thf(c_0_28, plain, ((epred1_0 @ esk3_0)|~((f @ (($true))))|~((epred3_1 @ esk3_0))), inference(er,[status(thm)],[c_0_22])).
% 0.31/0.27 thf(c_0_29, plain, ((epred1_0 @ esk3_0)|(epred3_1 @ esk3_0)|(f @ (~($true)))), inference(er,[status(thm)],[c_0_23])).
% 0.31/0.27 thf(c_0_30, plain, ![X2:$i]:((((X2)=(esk4_0))|((X2)=(esk3_0))|((X2)=(esk2_0))|((X2)=(esk1_0))|~((epred1_0 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.31/0.27 thf(c_0_31, plain, ((epred1_0 @ (eps @ epred1_0))|(f @ (($true)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_24])).
% 0.31/0.27 thf(c_0_32, negated_conjecture, ((eps @ epred1_0)!=(esk1_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_26]), c_0_27])).
% 0.31/0.27 thf(c_0_33, negated_conjecture, ((eps @ epred1_0)!=(esk2_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_26]), c_0_27])).
% 0.31/0.27 thf(c_0_34, negated_conjecture, ((eps @ epred1_0)!=(esk3_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_26]), c_0_27])).
% 0.31/0.27 thf(c_0_35, negated_conjecture, ((eps @ epred1_0)!=(esk4_0)), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_26]), c_0_27])).
% 0.31/0.27 thf(c_0_36, plain, ![X2:$i]:(((epred1_0 @ X2)|~((f @ (~($true))))|~((f @ (($true))))|~(($true))|((X2)!=(esk4_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.31/0.27 thf(c_0_37, plain, ((f @ (~($true)))|(epred1_0 @ esk3_0)|~((f @ (($true))))), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 0.31/0.27 thf(c_0_38, plain, (f @ (($true))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_32]), c_0_33]), c_0_34]), c_0_35])).
% 0.31/0.27 thf(c_0_39, plain, ![X2:$i]:(((epred1_0 @ X2)|((X2)!=(esk4_0))|~((f @ (($true))))|~((f @ (~($true)))))), inference(cn,[status(thm)],[c_0_36])).
% 0.31/0.27 thf(c_0_40, plain, ((epred1_0 @ esk3_0)|(f @ (~($true)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 0.31/0.27 thf(c_0_41, plain, ((epred1_0 @ esk4_0)|~((f @ (($true))))|~((f @ (~($true))))), inference(er,[status(thm)],[c_0_39])).
% 0.31/0.27 thf(c_0_42, plain, ((epred1_0 @ (eps @ epred1_0))|(f @ (~($true)))), inference(spm,[status(thm)],[c_0_24, c_0_40])).
% 0.31/0.27 thf(c_0_43, plain, ((epred1_0 @ esk4_0)|~((f @ (~($true))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_38])])).
% 0.31/0.27 thf(c_0_44, plain, (f @ (~($true))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_42]), c_0_32]), c_0_33]), c_0_34]), c_0_35])).
% 0.31/0.27 thf(c_0_45, plain, (epred1_0 @ esk4_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 0.31/0.27 thf(c_0_46, plain, (epred1_0 @ (eps @ epred1_0)), inference(spm,[status(thm)],[c_0_24, c_0_45])).
% 0.31/0.27 thf(c_0_47, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_46]), c_0_32]), c_0_33]), c_0_34]), c_0_35]), ['proof']).
% 0.31/0.27 % SZS output end CNFRefutation
% 0.31/0.27 % Parsed axioms : 6
% 0.31/0.27 % Removed by relevancy pruning/SinE : 3
% 0.31/0.27 % Initial clauses : 78
% 0.31/0.27 % Removed in clause preprocessing : 40
% 0.31/0.27 % Initial clauses in saturation : 38
% 0.31/0.27 % Processed clauses : 93
% 0.31/0.27 % ...of these trivial : 0
% 0.31/0.27 % ...subsumed : 10
% 0.31/0.27 % ...remaining for further processing : 83
% 0.31/0.27 % Other redundant clauses eliminated : 9
% 0.31/0.27 % Clauses deleted for lack of memory : 0
% 0.31/0.27 % Backward-subsumed : 12
% 0.31/0.27 % Backward-rewritten : 17
% 0.31/0.27 % Generated clauses : 82
% 0.31/0.27 % ...of the previous two non-redundant : 56
% 0.31/0.27 % ...aggressively subsumed : 0
% 0.31/0.27 % Contextual simplify-reflections : 2
% 0.31/0.27 % Paramodulations : 26
% 0.31/0.27 % Factorizations : 0
% 0.31/0.27 % NegExts : 1
% 0.31/0.27 % Equation resolutions : 9
% 0.31/0.27 % Disequality decompositions : 0
% 0.31/0.27 % Total rewrite steps : 18
% 0.31/0.27 % ...of those cached : 14
% 0.31/0.27 % Propositional unsat checks : 0
% 0.31/0.27 % Propositional check models : 0
% 0.31/0.27 % Propositional check unsatisfiable : 0
% 0.31/0.27 % Propositional clauses : 0
% 0.31/0.27 % Propositional clauses after purity: 0
% 0.31/0.27 % Propositional unsat core size : 0
% 0.31/0.27 % Propositional preprocessing time : 0.000
% 0.31/0.27 % Propositional encoding time : 0.000
% 0.31/0.27 % Propositional solver time : 0.000
% 0.31/0.27 % Success case prop preproc time : 0.000
% 0.31/0.27 % Success case prop encoding time : 0.000
% 0.31/0.27 % Success case prop solver time : 0.000
% 0.31/0.27 % Current number of processed clauses : 14
% 0.31/0.27 % Positive orientable unit clauses : 4
% 0.31/0.27 % Positive unorientable unit clauses: 0
% 0.31/0.27 % Negative unit clauses : 4
% 0.31/0.27 % Non-unit-clauses : 6
% 0.31/0.27 % Current number of unprocessed clauses: 25
% 0.31/0.27 % ...number of literals in the above : 97
% 0.31/0.27 % Current number of archived formulas : 0
% 0.31/0.27 % Current number of archived clauses : 60
% 0.31/0.27 % Clause-clause subsumption calls (NU) : 244
% 0.31/0.27 % Rec. Clause-clause subsumption calls : 141
% 0.31/0.27 % Non-unit clause-clause subsumptions : 32
% 0.31/0.27 % Unit Clause-clause subsumption calls : 4
% 0.31/0.27 % Rewrite failures with RHS unbound : 0
% 0.31/0.27 % BW rewrite match attempts : 3
% 0.31/0.27 % BW rewrite match successes : 3
% 0.31/0.27 % Condensation attempts : 93
% 0.31/0.27 % Condensation successes : 8
% 0.31/0.27 % Termbank termtop insertions : 6355
% 0.31/0.27 % Search garbage collected termcells : 1165
% 0.31/0.27
% 0.31/0.27 % -------------------------------------------------
% 0.31/0.27 % User time : 0.015 s
% 0.31/0.27 % System time : 0.007 s
% 0.31/0.27 % Total time : 0.022 s
% 0.31/0.27 % Maximum resident set size: 3896 pages
% 0.31/0.27
% 0.31/0.27 % -------------------------------------------------
% 0.31/0.27 % User time : 0.031 s
% 0.31/0.27 % System time : 0.016 s
% 0.31/0.27 % Total time : 0.048 s
% 0.31/0.27 % Maximum resident set size: 4864 pages
% 0.31/0.27 % E exiting
%------------------------------------------------------------------------------