%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SYO544^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 : n006.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:44:49 AM UTC 2026
% Result : Theorem 1.01s 0.42s
% Output : CNFRefutation 1.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO544^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.08/0.16 % Computer : n006.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Tue Sep 29 17:13:54 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running higher-order theorem proving
% 0.08/0.22 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.PhSxIy9Fjp/E---3.1_1040300.p
% 1.01/0.42 % Version: 3.5.1-ho
% 1.01/0.42 % partial match(1): HSLSSMSSSSMCHSA
% 1.01/0.42 % Preprocessing class: HSMSSMSSSSMCHSA.
% 1.01/0.42 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.01/0.42 % Starting post_as_ho6 with 1500s (5) cores
% 1.01/0.42 % Starting post_as_ho7 with 300s (1) cores
% 1.01/0.42 % Starting post_as_ho8 with 300s (1) cores
% 1.01/0.42 % Starting lpo8_s with 300s (1) cores
% 1.01/0.42 % lpo8_s with pid 1040316 completed with status 0
% 1.01/0.42 % Result found by lpo8_s
% 1.01/0.42 % partial match(1): HSLSSMSSSSMCHSA
% 1.01/0.42 % Preprocessing class: HSMSSMSSSSMCHSA.
% 1.01/0.42 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.01/0.42 % Starting post_as_ho6 with 1500s (5) cores
% 1.01/0.42 % Starting post_as_ho7 with 300s (1) cores
% 1.01/0.42 % Starting post_as_ho8 with 300s (1) cores
% 1.01/0.42 % Starting lpo8_s with 300s (1) cores
% 1.01/0.42 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 1.01/0.42 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 1.01/0.42 % Search class: HGHSF-FSLS11-SHSFFFBC
% 1.01/0.42 % partial match(4): HGHSM-FSLM32-SHSFFFBC
% 1.01/0.42 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 1.01/0.42 % Starting SubtermCWHack with 28s (1) cores
% 1.01/0.42 % SubtermCWHack with pid 1040325 completed with status 10
% 1.01/0.42 % Starting lpo8_s with 31s (1) cores
% 1.01/0.42 % lpo8_s with pid 1040328 completed with status 0
% 1.01/0.42 % Result found by lpo8_s
% 1.01/0.42 % partial match(1): HSLSSMSSSSMCHSA
% 1.01/0.42 % Preprocessing class: HSMSSMSSSSMCHSA.
% 1.01/0.42 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.01/0.42 % Starting post_as_ho6 with 1500s (5) cores
% 1.01/0.42 % Starting post_as_ho7 with 300s (1) cores
% 1.01/0.42 % Starting post_as_ho8 with 300s (1) cores
% 1.01/0.42 % Starting lpo8_s with 300s (1) cores
% 1.01/0.42 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,4.0,,6,20000,1.0))
% 1.01/0.42 % SinE strategy is GSinE(CountFormulas,hypos,4.0,,6,20000,1.0)
% 1.01/0.42 % Search class: HGHSF-FSLS11-SHSFFFBC
% 1.01/0.42 % partial match(4): HGHSM-FSLM32-SHSFFFBC
% 1.01/0.42 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 1.01/0.42 % Starting SubtermCWHack with 28s (1) cores
% 1.01/0.42 % SubtermCWHack with pid 1040325 completed with status 10
% 1.01/0.42 % Starting lpo8_s with 31s (1) cores
% 1.01/0.42 % Preprocessing time : 0.003 s
% 1.01/0.42 % Presaturation interreduction done
% 1.01/0.42
% 1.01/0.42 % Proof found!
% 1.01/0.42 % SZS status Theorem
% 1.01/0.42 % SZS output start CNFRefutation
% 1.01/0.42 thf(decl_23, type, eps: ($i > $o) > $i).
% 1.01/0.42 thf(decl_24, type, case: ($o > $o) > $i > $i > $i > $i > $i).
% 1.01/0.42 thf(decl_25, type, f0: $o > $o).
% 1.01/0.42 thf(decl_26, type, f1: $o > $o).
% 1.01/0.42 thf(decl_27, type, f2: $o > $o).
% 1.01/0.42 thf(decl_28, type, f3: $o > $o).
% 1.01/0.42 thf(decl_29, type, esk1_0: $i).
% 1.01/0.42 thf(decl_30, type, esk2_0: $i).
% 1.01/0.42 thf(decl_31, type, esk3_0: $i).
% 1.01/0.42 thf(decl_32, type, esk4_0: $i).
% 1.01/0.42 thf(decl_33, type, epred1_0: $i > $o).
% 1.01/0.42 thf(decl_34, type, epred2_0: $i > $o).
% 1.01/0.42 thf(decl_35, type, epred3_0: $i > $o).
% 1.01/0.42 thf(decl_36, type, epred4_0: $i > $o).
% 1.01/0.42 thf(decl_37, type, epred5_1: $i > $o).
% 1.01/0.42 thf(decl_38, type, epred6_1: $i > $o).
% 1.01/0.42 thf(decl_39, type, epred7_1: $i > $o).
% 1.01/0.42 thf(decl_40, type, epred8_1: $i > $o).
% 1.01/0.42 thf(decl_41, type, epred9_1: $i > $o).
% 1.01/0.42 thf(decl_42, type, epred10_1: $i > $o).
% 1.01/0.42 thf(decl_43, type, epred11_1: $i > $o).
% 1.01/0.42 thf(decl_44, type, epred12_1: $i > $o).
% 1.01/0.42 thf(decl_45, type, epred13_1: $i > $o).
% 1.01/0.42 thf(decl_46, type, epred14_1: $i > $o).
% 1.01/0.42 thf(decl_47, type, epred15_1: $i > $o).
% 1.01/0.42 thf(decl_48, type, epred16_1: $i > $o).
% 1.01/0.42 thf(decl_50, type, esk18_0: $o).
% 1.01/0.42 thf(decl_54, type, esk22_0: $o).
% 1.01/0.42 thf(decl_91, type, esk59_0: $i).
% 1.01/0.42 thf(f0f, axiom, ((f0 @ (~($true)))<=>~($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f0f)).
% 1.01/0.42 thf(f0t, axiom, ((f0 @ (($true)))<=>~($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f0t)).
% 1.01/0.42 thf(f1t, axiom, ((f1 @ (($true)))<=>~($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f1t)).
% 1.01/0.42 thf(f1f, axiom, ((f1 @ (~($true)))<=>($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f1f)).
% 1.01/0.42 thf(choiceax, axiom, ![X1:$i > $o]:((?[X2:$i]:((X1 @ X2))=>(X1 @ (eps @ X1)))), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', choiceax)).
% 1.01/0.42 thf(f3f, axiom, ((f3 @ (~($true)))<=>($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f3f)).
% 1.01/0.42 thf(conj, conjecture, ![X2:$i, X4:$i, X5:$i, X6:$i]:((((((case @ f0 @ X2 @ X4 @ X5 @ X6)=(X2))&((case @ f1 @ X2 @ X4 @ X5 @ X6)=(X4)))&((case @ f2 @ X2 @ X4 @ X5 @ X6)=(X5)))&((case @ f3 @ X2 @ X4 @ X5 @ X6)=(X6)))), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', conj)).
% 1.01/0.42 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.PhSxIy9Fjp/E---3.1_1040300.p', caseood)).
% 1.01/0.42 thf(f3t, axiom, ((f3 @ (($true)))<=>($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f3t)).
% 1.01/0.42 thf(f2f, axiom, ((f2 @ (~($true)))<=>~($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f2f)).
% 1.01/0.42 thf(f2t, axiom, ((f2 @ (($true)))<=>($true)), file('/export/starexec/sandbox/tmp/tmp.PhSxIy9Fjp/E---3.1_1040300.p', f2t)).
% 1.01/0.42 thf(c_0_11, axiom, (((~(~($true))|(f0 @ $true))&(~($true)|(f0 @ $false)))<=>~($true)), inference(fool_unroll,[status(thm)],[f0f])).
% 1.01/0.42 thf(c_0_12, plain, ![X49:$i, X50:$o, X51:$o, X52:$o]:((((((((((~(f0 @ ((X52)))|($true)|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((~(f0 @ ((X52)))|($true)|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))))&(((~(f0 @ ((X52)))|($true)|(((X49)=(esk3_0))|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(((X49)=(esk3_0))|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((f0)=($not))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))))&(((((~(f0 @ ((X52)))|($true)|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((~(f0 @ ((X52)))|($true)|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))))&(((~(f0 @ ((X52)))|($true)|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(~(f0 @ ((X50)))|~($true))))|~(epred1_0 @ X49)))))&((((((~(f0 @ ((X52)))|($true)|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((~(f0 @ ((X52)))|($true)|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))))&(((~(f0 @ ((X52)))|($true)|(((X49)=(esk3_0))|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(((X49)=(esk3_0))|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((f0)=($not))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))))&(((((~(f0 @ ((X52)))|($true)|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((~(f0 @ ((X52)))|($true)|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))))&(((~(f0 @ ((X52)))|($true)|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((X49)=(esk2_0))|(($true)|(f0 @ ((X50))))))|~(epred1_0 @ X49))))))&((((((~(f0 @ ((X52)))|($true)|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f0 @ ((X51)))|(X51)|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((~(f0 @ ((X52)))|($true)|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f0 @ ((X51)))|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))))&(((~(f0 @ ((X52)))|($true)|(((X49)=(esk3_0))|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(((X49)=(esk3_0))|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(((X49)=(esk3_0))|(((f0)=($not))|((X49)=(esk1_0))))|~(epred1_0 @ X49))))&(((((~(f0 @ ((X52)))|($true)|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(f0 @ ((X51)))|(X51)|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((~(f0 @ ((X52)))|($true)|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((X52)))|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49)))&(((X49)=(esk4_0))|(~(X51)|(f0 @ ((X51)))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))))&(((~(f0 @ ((X52)))|($true)|(((X49)=(esk3_0))|(((X49)=(esk2_0))|((X49)=(esk1_0))))|~(epred1_0 @ X49))&(~($true)|(f0 @ ((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))))))&(((((((~(epred5_1 @ X49)|(epred5_1 @ X49)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))&(~(f0 @ $false)|(epred5_1 @ X49)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49)))&((~(epred5_1 @ X49)|~(f0 @ $true)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))&(~(f0 @ $false)|~(f0 @ $true)|($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))))&((~(epred5_1 @ X49)|(f0 @ $true)|~($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))&((epred5_1 @ X49)|(f0 @ $false)|~($true)|((X49)!=(esk1_0))|(epred1_0 @ X49))))&(((f0)!=($not))|((X49)!=(esk2_0))|(epred1_0 @ X49)))&((((~(epred6_1 @ X49)|(epred6_1 @ X49)|~(epred6_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))&(~(f0 @ $false)|(epred6_1 @ X49)|~(epred6_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49)))&((~(epred6_1 @ X49)|~(f0 @ $true)|~(epred6_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))&(~(f0 @ $false)|~(f0 @ $true)|~(epred6_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))))&((~(epred6_1 @ X49)|(f0 @ $true)|(epred6_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49))&((epred6_1 @ X49)|(f0 @ $false)|(epred6_1 @ X49)|((X49)!=(esk3_0))|(epred1_0 @ X49)))))&((((~(epred7_1 @ X49)|(epred7_1 @ X49)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))&(~(f0 @ $false)|(epred7_1 @ X49)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49)))&((~(epred7_1 @ X49)|~(f0 @ $true)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))&(~(f0 @ $false)|~(f0 @ $true)|~($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))))&((~(epred7_1 @ X49)|(f0 @ $true)|($true)|((X49)!=(esk4_0))|(epred1_0 @ X49))&((epred7_1 @ X49)|(f0 @ $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)],[])])])])])])])).
% 1.01/0.42 thf(c_0_13, plain, ((((($true)|~($true)|~($true))&(~(f0 @ $false)|~($true)|~($true)))&((($true)|~(f0 @ $true)|~($true))&(~(f0 @ $false)|~(f0 @ $true)|~($true))))&((($true)|(f0 @ $true)|($true))&(~($true)|(f0 @ $false)|($true)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])).
% 1.01/0.42 thf(c_0_14, plain, ((~(f0 @ $true)|~($true))&(($true)|(f0 @ $true))), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[f0t])])).
% 1.01/0.42 thf(c_0_15, plain, ![X2:$i]:(((epred5_1 @ X2)|(f0 @ (~($true)))|(epred1_0 @ X2)|~(($true))|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.01/0.42 thf(c_0_16, plain, (~((f0 @ (~($true))))|~(($true))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.01/0.42 thf(c_0_17, plain, ((~(f1 @ $true)|~($true))&(($true)|(f1 @ $true))), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[f1t])])).
% 1.01/0.42 thf(c_0_18, axiom, (((~(~($true))|(f1 @ $true))&(~($true)|(f1 @ $false)))<=>$true), inference(fool_unroll,[status(thm)],[f1f])).
% 1.01/0.42 thf(c_0_19, plain, ![X2:$i]:(((f0 @ (($true)))|(epred1_0 @ X2)|~((epred5_1 @ X2))|~(($true))|((X2)!=(esk1_0)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.01/0.42 thf(c_0_20, plain, (~((f0 @ (($true))))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.01/0.42 thf(c_0_21, plain, ![X2:$i]:(((epred1_0 @ X2)|(epred5_1 @ X2)|(f0 @ (~($true)))|((X2)!=(esk1_0)))), inference(cn,[status(thm)],[c_0_15])).
% 1.01/0.42 thf(c_0_22, plain, ~((f0 @ (~($true)))), inference(cn,[status(thm)],[c_0_16])).
% 1.01/0.42 thf(c_0_23, plain, ![X56:$i, X57:$o, X58:$o, X59:$o]:((((((((((~(f1 @ ((X59)))|($true)|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((~(f1 @ ((X59)))|($true)|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))))&(((~(f1 @ ((X59)))|($true)|(((X56)=(esk3_0))|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(((X56)=(esk3_0))|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(((X56)=(esk3_0))|(((f1)=($not))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))))&(((((~(f1 @ ((X59)))|($true)|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((~(f1 @ ((X59)))|($true)|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))))&(((~(f1 @ ((X59)))|($true)|(((X56)=(esk3_0))|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(((X56)=(esk3_0))|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(((X56)=(esk3_0))|(((X56)=(esk2_0))|(~(f1 @ ((X57)))|~($true))))|~(epred2_0 @ X56)))))&((((((~(f1 @ ((X59)))|($true)|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((~(f1 @ ((X59)))|($true)|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))))&(((~(f1 @ ((X59)))|($true)|(((X56)=(esk3_0))|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(((X56)=(esk3_0))|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(((X56)=(esk3_0))|(((f1)=($not))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))))&(((((~(f1 @ ((X59)))|($true)|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((~(f1 @ ((X59)))|($true)|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))))&(((~(f1 @ ((X59)))|($true)|(((X56)=(esk3_0))|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(((X56)=(esk3_0))|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(((X56)=(esk3_0))|(((X56)=(esk2_0))|(($true)|(f1 @ ((X57))))))|~(epred2_0 @ X56))))))&((((((~(f1 @ ((X59)))|($true)|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(f1 @ ((X58)))|(X58)|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((~(f1 @ ((X59)))|($true)|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(X58)|(f1 @ ((X58)))|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56))))&(((~(f1 @ ((X59)))|($true)|(((X56)=(esk3_0))|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(((X56)=(esk3_0))|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(((X56)=(esk3_0))|(((f1)=($not))|((X56)=(esk1_0))))|~(epred2_0 @ X56))))&(((((~(f1 @ ((X59)))|($true)|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(f1 @ ((X58)))|(X58)|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((~(f1 @ ((X59)))|($true)|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(~(X58)|(f1 @ ((X58)))|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56))))&(((~(f1 @ ((X59)))|($true)|(((X56)=(esk3_0))|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56))&(~($true)|(f1 @ ((X59)))|(((X56)=(esk3_0))|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56)))&(((X56)=(esk4_0))|(((X56)=(esk3_0))|(((X56)=(esk2_0))|((X56)=(esk1_0))))|~(epred2_0 @ X56))))))&(((((((~(epred8_1 @ X56)|(epred8_1 @ X56)|($true)|((X56)!=(esk1_0))|(epred2_0 @ X56))&(~(f1 @ $false)|(epred8_1 @ X56)|($true)|((X56)!=(esk1_0))|(epred2_0 @ X56)))&((~(epred8_1 @ X56)|~(f1 @ $true)|($true)|((X56)!=(esk1_0))|(epred2_0 @ X56))&(~(f1 @ $false)|~(f1 @ $true)|($true)|((X56)!=(esk1_0))|(epred2_0 @ X56))))&((~(epred8_1 @ X56)|(f1 @ $true)|~($true)|((X56)!=(esk1_0))|(epred2_0 @ X56))&((epred8_1 @ X56)|(f1 @ $false)|~($true)|((X56)!=(esk1_0))|(epred2_0 @ X56))))&(((f1)!=($not))|((X56)!=(esk2_0))|(epred2_0 @ X56)))&((((~(epred9_1 @ X56)|(epred9_1 @ X56)|~(epred9_1 @ X56)|((X56)!=(esk3_0))|(epred2_0 @ X56))&(~(f1 @ $false)|(epred9_1 @ X56)|~(epred9_1 @ X56)|((X56)!=(esk3_0))|(epred2_0 @ X56)))&((~(epred9_1 @ X56)|~(f1 @ $true)|~(epred9_1 @ X56)|((X56)!=(esk3_0))|(epred2_0 @ X56))&(~(f1 @ $false)|~(f1 @ $true)|~(epred9_1 @ X56)|((X56)!=(esk3_0))|(epred2_0 @ X56))))&((~(epred9_1 @ X56)|(f1 @ $true)|(epred9_1 @ X56)|((X56)!=(esk3_0))|(epred2_0 @ X56))&((epred9_1 @ X56)|(f1 @ $false)|(epred9_1 @ X56)|((X56)!=(esk3_0))|(epred2_0 @ X56)))))&((((~(epred10_1 @ X56)|(epred10_1 @ X56)|~($true)|((X56)!=(esk4_0))|(epred2_0 @ X56))&(~(f1 @ $false)|(epred10_1 @ X56)|~($true)|((X56)!=(esk4_0))|(epred2_0 @ X56)))&((~(epred10_1 @ X56)|~(f1 @ $true)|~($true)|((X56)!=(esk4_0))|(epred2_0 @ X56))&(~(f1 @ $false)|~(f1 @ $true)|~($true)|((X56)!=(esk4_0))|(epred2_0 @ X56))))&((~(epred10_1 @ X56)|(f1 @ $true)|($true)|((X56)!=(esk4_0))|(epred2_0 @ X56))&((epred10_1 @ X56)|(f1 @ $false)|($true)|((X56)!=(esk4_0))|(epred2_0 @ X56))))))), 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)],[])])])])])])])).
% 1.01/0.42 thf(c_0_24, plain, (~((f1 @ (($true))))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.01/0.42 thf(c_0_25, plain, ((((($true)|~($true)|($true))&(~(f1 @ $false)|~($true)|($true)))&((($true)|~(f1 @ $true)|($true))&(~(f1 @ $false)|~(f1 @ $true)|($true))))&((($true)|(f1 @ $true)|~($true))&(~($true)|(f1 @ $false)|~($true)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])).
% 1.01/0.42 thf(c_0_26, 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])])])])).
% 1.01/0.43 thf(c_0_27, plain, ![X2:$i]:(((epred1_0 @ X2)|(f0 @ (($true)))|((X2)!=(esk1_0))|~((epred5_1 @ X2)))), inference(cn,[status(thm)],[c_0_19])).
% 1.01/0.43 thf(c_0_28, plain, ~((f0 @ (($true)))), inference(cn,[status(thm)],[c_0_20])).
% 1.01/0.43 thf(c_0_29, plain, ((epred1_0 @ esk1_0)|(epred5_1 @ esk1_0)), inference(er,[status(thm)],[inference(sr,[status(thm)],[c_0_21, c_0_22])])).
% 1.01/0.43 thf(c_0_30, plain, ![X16:$o, X8:$o, X2:$i]:(((f1 @ ((X8)))|(f1 @ (($true)))|((X2)=(esk2_0))|~((f1 @ ((X16))))|~((epred2_0 @ X2)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23])])])).
% 1.01/0.43 thf(c_0_31, plain, ~((f1 @ (($true)))), inference(cn,[status(thm)],[c_0_24])).
% 1.01/0.43 thf(c_0_32, plain, ((f1 @ (~($true)))|~(($true))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.01/0.43 thf(c_0_33, plain, ![X2:$i]:(((epred2_0 @ X2)|((f1)!=($not))|((X2)!=(esk2_0)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 1.01/0.43 thf(c_0_34, axiom, (((~(~($true))|(f3 @ $true))&(~($true)|(f3 @ $false)))<=>$true), inference(fool_unroll,[status(thm)],[f3f])).
% 1.01/0.43 thf(c_0_35, plain, ![X8:$o, X2:$i]:(((f0 @ ((X8)))|(f0 @ (($true)))|((f0)=($not))|((X2)=(esk1_0))|~((epred1_0 @ X2)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_12])])])).
% 1.01/0.43 thf(c_0_36, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (eps @ X1))|~((X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 1.01/0.43 thf(c_0_37, plain, (epred1_0 @ esk1_0), inference(csr,[status(thm)],[inference(er,[status(thm)],[inference(sr,[status(thm)],[c_0_27, c_0_28])]), c_0_29])).
% 1.01/0.43 thf(c_0_38, plain, ![X8:$o, X2:$i]:((((X2)=(esk2_0))|~((f1 @ ((X8))))|~((epred2_0 @ X2)))), inference(sr,[status(thm)],[inference(condense,[status(thm)],[c_0_30]), c_0_31])).
% 1.01/0.43 thf(c_0_39, plain, (f1 @ (~($true))), inference(cn,[status(thm)],[c_0_32])).
% 1.01/0.43 thf(c_0_40, plain, ((epred2_0 @ esk2_0)|(($not)!=(f1))), inference(er,[status(thm)],[c_0_33])).
% 1.01/0.43 thf(c_0_41, plain, ((((($true)|~($true)|($true))&(~(f3 @ $false)|~($true)|($true)))&((($true)|~(f3 @ $true)|($true))&(~(f3 @ $false)|~(f3 @ $true)|($true))))&((($true)|(f3 @ $true)|~($true))&(~($true)|(f3 @ $false)|~($true)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_34])])])).
% 1.01/0.43 thf(c_0_42, negated_conjecture, ~(![X2:$i, X4:$i, X5:$i, X6:$i]:((((((case @ f0 @ X2 @ X4 @ X5 @ X6)=(X2))&((case @ f1 @ X2 @ X4 @ X5 @ X6)=(X4)))&((case @ f2 @ X2 @ X4 @ X5 @ X6)=(X5)))&((case @ f3 @ X2 @ X4 @ X5 @ X6)=(X6))))), inference(assume_negation,[status(cth)],[conj])).
% 1.01/0.43 thf(c_0_43, 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])).
% 1.01/0.43 thf(c_0_44, plain, ![X2:$i]:(((($not)=(f0))|((X2)=(esk1_0))|~((epred1_0 @ X2)))), inference(sr,[status(thm)],[inference(condense,[status(thm)],[c_0_35]), c_0_28])).
% 1.01/0.43 thf(c_0_45, plain, (epred1_0 @ (eps @ epred1_0)), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 1.01/0.43 thf(c_0_46, plain, ![X2:$i]:((((X2)=(esk2_0))|~((epred2_0 @ X2)))), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 1.01/0.43 thf(c_0_47, plain, ((epred2_0 @ (eps @ epred2_0))|(($not)!=(f1))), inference(spm,[status(thm)],[c_0_36, c_0_40])).
% 1.01/0.43 thf(c_0_48, plain, ![X70:$i, X71:$o, X72:$o, X73:$o]:((((((((((~(f3 @ ((X73)))|($true)|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((~(f3 @ ((X73)))|($true)|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))))&(((~(f3 @ ((X73)))|($true)|(((X70)=(esk3_0))|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(((X70)=(esk3_0))|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(((X70)=(esk3_0))|(((f3)=($not))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))))&(((((~(f3 @ ((X73)))|($true)|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((~(f3 @ ((X73)))|($true)|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))))&(((~(f3 @ ((X73)))|($true)|(((X70)=(esk3_0))|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(((X70)=(esk3_0))|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(((X70)=(esk3_0))|(((X70)=(esk2_0))|(~(f3 @ ((X71)))|~($true))))|~(epred4_0 @ X70)))))&((((((~(f3 @ ((X73)))|($true)|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((~(f3 @ ((X73)))|($true)|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))))&(((~(f3 @ ((X73)))|($true)|(((X70)=(esk3_0))|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(((X70)=(esk3_0))|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(((X70)=(esk3_0))|(((f3)=($not))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))))&(((((~(f3 @ ((X73)))|($true)|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((~(f3 @ ((X73)))|($true)|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))))&(((~(f3 @ ((X73)))|($true)|(((X70)=(esk3_0))|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(((X70)=(esk3_0))|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(((X70)=(esk3_0))|(((X70)=(esk2_0))|(($true)|(f3 @ ((X71))))))|~(epred4_0 @ X70))))))&((((((~(f3 @ ((X73)))|($true)|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(f3 @ ((X72)))|(X72)|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((~(f3 @ ((X73)))|($true)|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(X72)|(f3 @ ((X72)))|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70))))&(((~(f3 @ ((X73)))|($true)|(((X70)=(esk3_0))|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(((X70)=(esk3_0))|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(((X70)=(esk3_0))|(((f3)=($not))|((X70)=(esk1_0))))|~(epred4_0 @ X70))))&(((((~(f3 @ ((X73)))|($true)|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(f3 @ ((X72)))|(X72)|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((~(f3 @ ((X73)))|($true)|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(~(X72)|(f3 @ ((X72)))|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70))))&(((~(f3 @ ((X73)))|($true)|(((X70)=(esk3_0))|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70))&(~($true)|(f3 @ ((X73)))|(((X70)=(esk3_0))|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70)))&(((X70)=(esk4_0))|(((X70)=(esk3_0))|(((X70)=(esk2_0))|((X70)=(esk1_0))))|~(epred4_0 @ X70))))))&(((((((~(epred14_1 @ X70)|(epred14_1 @ X70)|($true)|((X70)!=(esk1_0))|(epred4_0 @ X70))&(~(f3 @ $false)|(epred14_1 @ X70)|($true)|((X70)!=(esk1_0))|(epred4_0 @ X70)))&((~(epred14_1 @ X70)|~(f3 @ $true)|($true)|((X70)!=(esk1_0))|(epred4_0 @ X70))&(~(f3 @ $false)|~(f3 @ $true)|($true)|((X70)!=(esk1_0))|(epred4_0 @ X70))))&((~(epred14_1 @ X70)|(f3 @ $true)|~($true)|((X70)!=(esk1_0))|(epred4_0 @ X70))&((epred14_1 @ X70)|(f3 @ $false)|~($true)|((X70)!=(esk1_0))|(epred4_0 @ X70))))&(((f3)!=($not))|((X70)!=(esk2_0))|(epred4_0 @ X70)))&((((~(epred15_1 @ X70)|(epred15_1 @ X70)|~(epred15_1 @ X70)|((X70)!=(esk3_0))|(epred4_0 @ X70))&(~(f3 @ $false)|(epred15_1 @ X70)|~(epred15_1 @ X70)|((X70)!=(esk3_0))|(epred4_0 @ X70)))&((~(epred15_1 @ X70)|~(f3 @ $true)|~(epred15_1 @ X70)|((X70)!=(esk3_0))|(epred4_0 @ X70))&(~(f3 @ $false)|~(f3 @ $true)|~(epred15_1 @ X70)|((X70)!=(esk3_0))|(epred4_0 @ X70))))&((~(epred15_1 @ X70)|(f3 @ $true)|(epred15_1 @ X70)|((X70)!=(esk3_0))|(epred4_0 @ X70))&((epred15_1 @ X70)|(f3 @ $false)|(epred15_1 @ X70)|((X70)!=(esk3_0))|(epred4_0 @ X70)))))&((((~(epred16_1 @ X70)|(epred16_1 @ X70)|~($true)|((X70)!=(esk4_0))|(epred4_0 @ X70))&(~(f3 @ $false)|(epred16_1 @ X70)|~($true)|((X70)!=(esk4_0))|(epred4_0 @ X70)))&((~(epred16_1 @ X70)|~(f3 @ $true)|~($true)|((X70)!=(esk4_0))|(epred4_0 @ X70))&(~(f3 @ $false)|~(f3 @ $true)|~($true)|((X70)!=(esk4_0))|(epred4_0 @ X70))))&((~(epred16_1 @ X70)|(f3 @ $true)|($true)|((X70)!=(esk4_0))|(epred4_0 @ X70))&((epred16_1 @ X70)|(f3 @ $false)|($true)|((X70)!=(esk4_0))|(epred4_0 @ X70))))))), 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)],[])])])])])])])).
% 1.01/0.43 thf(c_0_49, plain, ((f3 @ (~($true)))|~(($true))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.01/0.43 thf(c_0_50, negated_conjecture, ~(![X2:$i, X4:$i, X5:$i, X6:$i]:((((((eps @ (^[Z0:$i]:(((((((((![X15:$o]:((((f0 @ ((X15))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f0)=($not)))&(((Z0)=(X4)))))))|(((![X16:$o]:((((f0 @ ((X16))))<=>((X16)))))&(((Z0)=(X5)))))))|(((![X17:$o]:((((f0 @ ((X17))))<=>($true))))&(((Z0)=(X6)))))))))=(X2))&((eps @ (^[Z0:$i]:(((((((((![X18:$o]:((((f1 @ ((X18))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f1)=($not)))&(((Z0)=(X4)))))))|(((![X19:$o]:((((f1 @ ((X19))))<=>((X19)))))&(((Z0)=(X5)))))))|(((![X20:$o]:((((f1 @ ((X20))))<=>($true))))&(((Z0)=(X6)))))))))=(X4)))&((eps @ (^[Z0:$i]:(((((((((![X21:$o]:((((f2 @ ((X21))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f2)=($not)))&(((Z0)=(X4)))))))|(((![X22:$o]:((((f2 @ ((X22))))<=>((X22)))))&(((Z0)=(X5)))))))|(((![X23:$o]:((((f2 @ ((X23))))<=>($true))))&(((Z0)=(X6)))))))))=(X5)))&((eps @ (^[Z0:$i]:(((((((((![X24:$o]:((((f3 @ ((X24))))<=>(~($true)))))&(((Z0)=(X2)))))|(((((f3)=($not)))&(((Z0)=(X4)))))))|(((![X25:$o]:((((f3 @ ((X25))))<=>((X25)))))&(((Z0)=(X5)))))))|(((![X26:$o]:((((f3 @ ((X26))))<=>($true))))&(((Z0)=(X6)))))))))=(X6))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[c_0_42, c_0_43])])).
% 1.01/0.43 thf(c_0_51, plain, (((eps @ epred1_0)=(esk1_0))|(($not)=(f0))), inference(spm,[status(thm)],[c_0_44, c_0_45])).
% 1.01/0.43 thf(c_0_52, plain, (((eps @ epred2_0)=(esk2_0))|(($not)!=(f1))), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 1.01/0.43 thf(c_0_53, plain, ![X15:$o, X2:$i]:((((X2)=(esk4_0))|((f3)=($not))|~((f3 @ (~($true))))|~((f3 @ ((X15))))|~((epred4_0 @ X2)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_48])])])).
% 1.01/0.43 thf(c_0_54, plain, (f3 @ (~($true))), inference(cn,[status(thm)],[c_0_49])).
% 1.01/0.43 thf(c_0_55, plain, ((~(f3 @ $true)|($true))&(~($true)|(f3 @ $true))), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[f3t])])).
% 1.01/0.43 thf(c_0_56, negated_conjecture, (((eps @ (^[Z0:$i]:(((((((((![X15:$o]:((((f0 @ ((X15))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f0)=($not)))&(((Z0)=(esk2_0)))))))|(((![X16:$o]:((((f0 @ ((X16))))<=>((X16)))))&(((Z0)=(esk3_0)))))))|(((![X17:$o]:((((f0 @ ((X17))))<=>($true))))&(((Z0)=(esk4_0)))))))))!=(esk1_0))|((eps @ (^[Z0:$i]:(((((((((![X18:$o]:((((f1 @ ((X18))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f1)=($not)))&(((Z0)=(esk2_0)))))))|(((![X19:$o]:((((f1 @ ((X19))))<=>((X19)))))&(((Z0)=(esk3_0)))))))|(((![X20:$o]:((((f1 @ ((X20))))<=>($true))))&(((Z0)=(esk4_0)))))))))!=(esk2_0))|((eps @ (^[Z0:$i]:(((((((((![X21:$o]:((((f2 @ ((X21))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f2)=($not)))&(((Z0)=(esk2_0)))))))|(((![X22:$o]:((((f2 @ ((X22))))<=>((X22)))))&(((Z0)=(esk3_0)))))))|(((![X23:$o]:((((f2 @ ((X23))))<=>($true))))&(((Z0)=(esk4_0)))))))))!=(esk3_0))|((eps @ (^[Z0:$i]:(((((((((![X24:$o]:((((f3 @ ((X24))))<=>(~($true)))))&(((Z0)=(esk1_0)))))|(((((f3)=($not)))&(((Z0)=(esk2_0)))))))|(((![X25:$o]:((((f3 @ ((X25))))<=>((X25)))))&(((Z0)=(esk3_0)))))))|(((![X26:$o]:((((f3 @ ((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_50])])])])).
% 1.01/0.43 thf(c_0_57, plain, ![X48:$i]:(((epred4_0 @ X48)<=>((![X45:$o]:(((f3 @ ((X45)))<=>~(($true))))&((X48)=(esk1_0)))|(((f3)=($not))&((X48)=(esk2_0)))|(![X46:$o]:(((f3 @ ((X46)))<=>(X46)))&((X48)=(esk3_0)))|(![X47:$o]:(((f3 @ ((X47)))<=>($true)))&((X48)=(esk4_0)))))), introduced(definition)).
% 1.01/0.43 thf(c_0_58, plain, ![X44:$i]:(((epred3_0 @ X44)<=>((![X41:$o]:(((f2 @ ((X41)))<=>~(($true))))&((X44)=(esk1_0)))|(((f2)=($not))&((X44)=(esk2_0)))|(![X42:$o]:(((f2 @ ((X42)))<=>(X42)))&((X44)=(esk3_0)))|(![X43:$o]:(((f2 @ ((X43)))<=>($true)))&((X44)=(esk4_0)))))), introduced(definition)).
% 1.01/0.43 thf(c_0_59, plain, ![X40:$i]:(((epred2_0 @ X40)<=>((![X37:$o]:(((f1 @ ((X37)))<=>~(($true))))&((X40)=(esk1_0)))|(((f1)=($not))&((X40)=(esk2_0)))|(![X38:$o]:(((f1 @ ((X38)))<=>(X38)))&((X40)=(esk3_0)))|(![X39:$o]:(((f1 @ ((X39)))<=>($true)))&((X40)=(esk4_0)))))), introduced(definition)).
% 1.01/0.43 thf(c_0_60, plain, ![X36:$i]:(((epred1_0 @ X36)<=>((![X33:$o]:(((f0 @ ((X33)))<=>~(($true))))&((X36)=(esk1_0)))|(((f0)=($not))&((X36)=(esk2_0)))|(![X34:$o]:(((f0 @ ((X34)))<=>(X34)))&((X36)=(esk3_0)))|(![X35:$o]:(((f0 @ ((X35)))<=>($true)))&((X36)=(esk4_0)))))), introduced(definition)).
% 1.01/0.43 thf(c_0_61, plain, ![X91:$o]:((((eps @ epred1_0)=(esk1_0))|(~((X91))<=>(f0 @ ((X91)))))), inference(arg_cong,[status(thm)],[c_0_51])).
% 1.01/0.43 thf(c_0_62, plain, (((eps @ epred2_0)=(esk2_0))|(~((esk22_0))<~>(f1 @ ((esk22_0))))), inference(neg_ext,[status(thm)],[c_0_52])).
% 1.01/0.43 thf(c_0_63, plain, ![X8:$o, X2:$i]:(((($not)=(f3))|((X2)=(esk4_0))|~((f3 @ ((X8))))|~((epred4_0 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 1.01/0.43 thf(c_0_64, plain, ((f3 @ (($true)))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 1.01/0.43 thf(c_0_65, plain, ![X2:$i]:(((epred4_0 @ X2)|~((f3 @ (~($true))))|~((f3 @ (($true))))|~(($true))|((X2)!=(esk4_0)))), inference(split_conjunct,[status(thm)],[c_0_48])).
% 1.01/0.43 thf(c_0_66, negated_conjecture, (((eps @ epred1_0)!=(esk1_0))|((eps @ epred2_0)!=(esk2_0))|((eps @ epred3_0)!=(esk3_0))|((eps @ epred4_0)!=(esk4_0))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_56]), c_0_57]), c_0_58]), c_0_59]), c_0_60])).
% 1.01/0.43 thf(c_0_67, plain, ((eps @ epred1_0)=(esk1_0)), inference(sr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_61]), c_0_22])).
% 1.01/0.43 thf(c_0_68, plain, (((eps @ epred2_0)=(esk2_0))|~((esk22_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_62])]), c_0_31])).
% 1.01/0.43 thf(c_0_69, plain, ![X102:$o, X8:$o, X2:$i]:(((~((X102))<=>(f3 @ ((X102))))|((X2)=(esk4_0))|~((f3 @ ((X8))))|~((epred4_0 @ X2)))), inference(arg_cong,[status(thm)],[c_0_63])).
% 1.01/0.43 thf(c_0_70, plain, (f3 @ (($true))), inference(cn,[status(thm)],[c_0_64])).
% 1.01/0.43 thf(c_0_71, plain, ![X2:$i]:(((epred4_0 @ X2)|((X2)!=(esk4_0))|~((f3 @ (($true))))|~((f3 @ (~($true)))))), inference(cn,[status(thm)],[c_0_65])).
% 1.01/0.43 thf(c_0_72, plain, ![X63:$i, X64:$o, X65:$o, X66:$o]:((((((((((~(f2 @ ((X66)))|($true)|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((~(f2 @ ((X66)))|($true)|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))))&(((~(f2 @ ((X66)))|($true)|(((X63)=(esk3_0))|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(((X63)=(esk3_0))|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(((X63)=(esk3_0))|(((f2)=($not))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))))&(((((~(f2 @ ((X66)))|($true)|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((~(f2 @ ((X66)))|($true)|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))))&(((~(f2 @ ((X66)))|($true)|(((X63)=(esk3_0))|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(((X63)=(esk3_0))|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(((X63)=(esk3_0))|(((X63)=(esk2_0))|(~(f2 @ ((X64)))|~($true))))|~(epred3_0 @ X63)))))&((((((~(f2 @ ((X66)))|($true)|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((~(f2 @ ((X66)))|($true)|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))))&(((~(f2 @ ((X66)))|($true)|(((X63)=(esk3_0))|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(((X63)=(esk3_0))|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(((X63)=(esk3_0))|(((f2)=($not))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))))&(((((~(f2 @ ((X66)))|($true)|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((~(f2 @ ((X66)))|($true)|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))))&(((~(f2 @ ((X66)))|($true)|(((X63)=(esk3_0))|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(((X63)=(esk3_0))|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(((X63)=(esk3_0))|(((X63)=(esk2_0))|(($true)|(f2 @ ((X64))))))|~(epred3_0 @ X63))))))&((((((~(f2 @ ((X66)))|($true)|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(f2 @ ((X65)))|(X65)|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((~(f2 @ ((X66)))|($true)|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(X65)|(f2 @ ((X65)))|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63))))&(((~(f2 @ ((X66)))|($true)|(((X63)=(esk3_0))|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(((X63)=(esk3_0))|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(((X63)=(esk3_0))|(((f2)=($not))|((X63)=(esk1_0))))|~(epred3_0 @ X63))))&(((((~(f2 @ ((X66)))|($true)|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(f2 @ ((X65)))|(X65)|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((~(f2 @ ((X66)))|($true)|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(~(X65)|(f2 @ ((X65)))|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63))))&(((~(f2 @ ((X66)))|($true)|(((X63)=(esk3_0))|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63))&(~($true)|(f2 @ ((X66)))|(((X63)=(esk3_0))|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63)))&(((X63)=(esk4_0))|(((X63)=(esk3_0))|(((X63)=(esk2_0))|((X63)=(esk1_0))))|~(epred3_0 @ X63))))))&(((((((~(epred11_1 @ X63)|(epred11_1 @ X63)|($true)|((X63)!=(esk1_0))|(epred3_0 @ X63))&(~(f2 @ $false)|(epred11_1 @ X63)|($true)|((X63)!=(esk1_0))|(epred3_0 @ X63)))&((~(epred11_1 @ X63)|~(f2 @ $true)|($true)|((X63)!=(esk1_0))|(epred3_0 @ X63))&(~(f2 @ $false)|~(f2 @ $true)|($true)|((X63)!=(esk1_0))|(epred3_0 @ X63))))&((~(epred11_1 @ X63)|(f2 @ $true)|~($true)|((X63)!=(esk1_0))|(epred3_0 @ X63))&((epred11_1 @ X63)|(f2 @ $false)|~($true)|((X63)!=(esk1_0))|(epred3_0 @ X63))))&(((f2)!=($not))|((X63)!=(esk2_0))|(epred3_0 @ X63)))&((((~(epred12_1 @ X63)|(epred12_1 @ X63)|~(epred12_1 @ X63)|((X63)!=(esk3_0))|(epred3_0 @ X63))&(~(f2 @ $false)|(epred12_1 @ X63)|~(epred12_1 @ X63)|((X63)!=(esk3_0))|(epred3_0 @ X63)))&((~(epred12_1 @ X63)|~(f2 @ $true)|~(epred12_1 @ X63)|((X63)!=(esk3_0))|(epred3_0 @ X63))&(~(f2 @ $false)|~(f2 @ $true)|~(epred12_1 @ X63)|((X63)!=(esk3_0))|(epred3_0 @ X63))))&((~(epred12_1 @ X63)|(f2 @ $true)|(epred12_1 @ X63)|((X63)!=(esk3_0))|(epred3_0 @ X63))&((epred12_1 @ X63)|(f2 @ $false)|(epred12_1 @ X63)|((X63)!=(esk3_0))|(epred3_0 @ X63)))))&((((~(epred13_1 @ X63)|(epred13_1 @ X63)|~($true)|((X63)!=(esk4_0))|(epred3_0 @ X63))&(~(f2 @ $false)|(epred13_1 @ X63)|~($true)|((X63)!=(esk4_0))|(epred3_0 @ X63)))&((~(epred13_1 @ X63)|~(f2 @ $true)|~($true)|((X63)!=(esk4_0))|(epred3_0 @ X63))&(~(f2 @ $false)|~(f2 @ $true)|~($true)|((X63)!=(esk4_0))|(epred3_0 @ X63))))&((~(epred13_1 @ X63)|(f2 @ $true)|($true)|((X63)!=(esk4_0))|(epred3_0 @ X63))&((epred13_1 @ X63)|(f2 @ $false)|($true)|((X63)!=(esk4_0))|(epred3_0 @ X63))))))), 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)],[])])])])])])])).
% 1.01/0.43 thf(c_0_73, negated_conjecture, (((eps @ epred2_0)!=(esk2_0))|((eps @ epred3_0)!=(esk3_0))|((eps @ epred4_0)!=(esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67])])).
% 1.01/0.43 thf(c_0_74, plain, ((eps @ epred2_0)=(esk2_0)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_62]), c_0_39])]), c_0_68])).
% 1.01/0.43 thf(c_0_75, plain, ![X8:$o, X2:$i]:((((X2)=(esk4_0))|~((f3 @ ((X8))))|~((epred4_0 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_69]), c_0_70])])).
% 1.01/0.43 thf(c_0_76, plain, (epred4_0 @ esk4_0), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_70]), c_0_54])])])).
% 1.01/0.43 thf(c_0_77, axiom, (((~(~($true))|(f2 @ $true))&(~($true)|(f2 @ $false)))<=>~($true)), inference(fool_unroll,[status(thm)],[f2f])).
% 1.01/0.43 thf(c_0_78, plain, ((~(f2 @ $true)|($true))&(~($true)|(f2 @ $true))), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[f2t])])).
% 1.01/0.43 thf(c_0_79, plain, ![X8:$o, X2:$i]:((((X2)=(esk4_0))|((X2)=(esk3_0))|((f2)=($not))|~((f2 @ ((X8))))|~(($true))|~((epred3_0 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_72])).
% 1.01/0.43 thf(c_0_80, negated_conjecture, (((eps @ epred3_0)!=(esk3_0))|((eps @ epred4_0)!=(esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74])])).
% 1.01/0.43 thf(c_0_81, plain, ![X2:$i]:(((eps @ (^[Z0:$i]:(((Z0)=(X2)))))=(X2))), inference(eliminate_leibniz_eq,[status(thm)],[inference(cn,[status(thm)],[]), c_0_36])).
% 1.01/0.43 thf(c_0_82, plain, ![X2:$i]:((((X2)=(esk4_0))|~((epred4_0 @ X2)))), inference(spm,[status(thm)],[c_0_75, c_0_54])).
% 1.01/0.43 thf(c_0_83, plain, (epred4_0 @ (eps @ epred4_0)), inference(spm,[status(thm)],[c_0_36, c_0_76])).
% 1.01/0.43 thf(c_0_84, plain, ((((($true)|~($true)|~($true))&(~(f2 @ $false)|~($true)|~($true)))&((($true)|~(f2 @ $true)|~($true))&(~(f2 @ $false)|~(f2 @ $true)|~($true))))&((($true)|(f2 @ $true)|($true))&(~($true)|(f2 @ $false)|($true)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_77])])])).
% 1.01/0.43 thf(c_0_85, plain, ![X2:$i]:(((epred3_0 @ X2)|~((epred12_1 @ X2))|~((f2 @ (($true))))|~((epred12_1 @ X2))|((X2)!=(esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_72])).
% 1.01/0.43 thf(c_0_86, plain, ((f2 @ (($true)))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_78])).
% 1.01/0.43 thf(c_0_87, plain, ![X8:$o, X2:$i]:((((X2)=(esk3_0))|((X2)=(esk4_0))|((f2)=($not))|~((f2 @ ((X8))))|~((epred3_0 @ X2)))), inference(cn,[status(thm)],[c_0_79])).
% 1.01/0.43 thf(c_0_88, plain, (((^[Z0:$i]:(((Z0)=(esk3_0))))!=(epred3_0))|((eps @ epred4_0)!=(esk4_0))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_80, c_0_81])])).
% 1.01/0.43 thf(c_0_89, plain, ((eps @ epred4_0)=(esk4_0)), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 1.01/0.43 thf(c_0_90, plain, ![X2:$i]:(((epred12_1 @ X2)|(f2 @ (~($true)))|(epred12_1 @ X2)|(epred3_0 @ X2)|((X2)!=(esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_72])).
% 1.01/0.43 thf(c_0_91, plain, (~((f2 @ (~($true))))|~(($true))|~(($true))), inference(split_conjunct,[status(thm)],[c_0_84])).
% 1.01/0.43 thf(c_0_92, plain, ![X2:$i]:(((epred3_0 @ X2)|((X2)!=(esk3_0))|~((epred12_1 @ X2))|~((f2 @ (($true)))))), inference(cn,[status(thm)],[c_0_85])).
% 1.01/0.43 thf(c_0_93, plain, (f2 @ (($true))), inference(cn,[status(thm)],[c_0_86])).
% 1.01/0.43 thf(c_0_94, plain, ![X104:$o, X8:$o, X2:$i]:(((~((X104))<=>(f2 @ ((X104))))|((X2)=(esk4_0))|((X2)=(esk3_0))|~((f2 @ ((X8))))|~((epred3_0 @ X2)))), inference(arg_cong,[status(thm)],[c_0_87])).
% 1.01/0.43 thf(c_0_95, plain, ((^[Z0:$i]:(((Z0)=(esk3_0))))!=(epred3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_89])])).
% 1.01/0.43 thf(c_0_96, plain, ![X16:$o, X8:$o, X2:$i]:(((f1 @ ((X8)))|(f1 @ (($true)))|((f1)=($not))|~((f1 @ ((X16))))|~((epred2_0 @ X2)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23])])])).
% 1.01/0.43 thf(c_0_97, plain, ((epred2_0 @ esk2_0)|(~((esk18_0))<~>(f1 @ ((esk18_0))))), inference(neg_ext,[status(thm)],[c_0_40])).
% 1.01/0.43 thf(c_0_98, plain, ![X2:$i]:(((epred3_0 @ X2)|(epred12_1 @ X2)|(f2 @ (~($true)))|((X2)!=(esk3_0)))), inference(cn,[status(thm)],[c_0_90])).
% 1.01/0.43 thf(c_0_99, plain, ~((f2 @ (~($true)))), inference(cn,[status(thm)],[c_0_91])).
% 1.01/0.43 thf(c_0_100, plain, ((epred3_0 @ esk3_0)|~((epred12_1 @ esk3_0))), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_92, c_0_93])])])).
% 1.01/0.43 thf(c_0_101, plain, ![X8:$o, X2:$i]:((((X2)=(esk3_0))|((X2)=(esk4_0))|~((f2 @ ((X8))))|~((epred3_0 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_94]), c_0_93])])).
% 1.01/0.43 thf(c_0_102, plain, (((esk59_0)=(esk3_0))<~>(epred3_0 @ esk59_0)), inference(neg_ext,[status(thm)],[c_0_95])).
% 1.01/0.43 thf(c_0_103, plain, ![X8:$o, X2:$i]:(((($not)=(f1))|~((f1 @ ((X8))))|~((epred2_0 @ X2)))), inference(sr,[status(thm)],[inference(condense,[status(thm)],[c_0_96]), c_0_31])).
% 1.01/0.43 thf(c_0_104, plain, ((epred2_0 @ esk2_0)|~((esk18_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_97])]), c_0_31])).
% 1.01/0.43 thf(c_0_105, plain, (epred3_0 @ esk3_0), inference(csr,[status(thm)],[inference(er,[status(thm)],[inference(sr,[status(thm)],[c_0_98, c_0_99])]), c_0_100])).
% 1.01/0.43 thf(c_0_106, plain, ![X2:$i]:((((X2)=(esk4_0))|((X2)=(esk3_0))|~((epred3_0 @ X2)))), inference(spm,[status(thm)],[c_0_101, c_0_93])).
% 1.01/0.43 thf(c_0_107, plain, (((esk3_0)=(esk59_0))|(epred3_0 @ esk59_0)), inference(dynamic_cnf,[status(thm)],[c_0_102])).
% 1.01/0.43 thf(c_0_108, plain, ![X15:$o, X8:$o, X2:$i]:(((f2 @ ((X8)))|((X2)=(esk3_0))|((f2)=($not))|~(($true))|~((f2 @ ((X15))))|~(($true))|~((epred3_0 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_72])).
% 1.01/0.43 thf(c_0_109, plain, ![X2:$i]:(((($not)=(f1))|~((epred2_0 @ X2)))), inference(spm,[status(thm)],[c_0_103, c_0_39])).
% 1.01/0.43 thf(c_0_110, plain, (epred2_0 @ esk2_0), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_97]), c_0_39])]), c_0_104])).
% 1.01/0.43 thf(c_0_111, plain, (epred3_0 @ (eps @ epred3_0)), inference(spm,[status(thm)],[c_0_36, c_0_105])).
% 1.01/0.43 thf(c_0_112, negated_conjecture, ((eps @ epred3_0)!=(esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_80, c_0_89])])).
% 1.01/0.43 thf(c_0_113, plain, (((esk3_0)=(esk59_0))|((esk4_0)=(esk59_0))), inference(spm,[status(thm)],[c_0_106, c_0_107])).
% 1.01/0.43 thf(c_0_114, plain, ![X15:$o, X8:$o, X2:$i]:((((X2)=(esk3_0))|((f2)=($not))|(f2 @ ((X8)))|~((f2 @ ((X15))))|~((epred3_0 @ X2)))), inference(cn,[status(thm)],[c_0_108])).
% 1.01/0.43 thf(c_0_115, plain, (($not)=(f1)), inference(spm,[status(thm)],[c_0_109, c_0_110])).
% 1.01/0.43 thf(c_0_116, plain, ((eps @ epred3_0)=(esk4_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_111]), c_0_112])).
% 1.01/0.43 thf(c_0_117, plain, (((esk3_0)!=(esk59_0))|~((epred3_0 @ esk59_0))), inference(dynamic_cnf,[status(thm)],[c_0_102])).
% 1.01/0.43 thf(c_0_118, plain, (((esk4_0)=(esk59_0))|(epred3_0 @ esk59_0)), inference(spm,[status(thm)],[c_0_105, c_0_113])).
% 1.01/0.43 thf(c_0_119, plain, ![X15:$o, X8:$o, X2:$i]:((((f1)=(f2))|((X2)=(esk3_0))|(f2 @ ((X8)))|~((f2 @ ((X15))))|~((epred3_0 @ X2)))), inference(rw,[status(thm)],[c_0_114, c_0_115])).
% 1.01/0.43 thf(c_0_120, plain, (epred3_0 @ esk4_0), inference(rw,[status(thm)],[c_0_111, c_0_116])).
% 1.01/0.43 thf(c_0_121, plain, ((esk4_0)=(esk59_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_117, c_0_118]), c_0_113])).
% 1.01/0.43 thf(c_0_122, negated_conjecture, ((esk3_0)!=(esk4_0)), inference(rw,[status(thm)],[c_0_112, c_0_116])).
% 1.01/0.43 thf(c_0_123, plain, ![X8:$o, X2:$i]:((((f1)=(f2))|((X2)=(esk3_0))|(f2 @ ((X8)))|~((epred3_0 @ X2)))), inference(spm,[status(thm)],[c_0_119, c_0_93])).
% 1.01/0.43 thf(c_0_124, plain, (epred3_0 @ esk59_0), inference(rw,[status(thm)],[c_0_120, c_0_121])).
% 1.01/0.43 thf(c_0_125, negated_conjecture, ((esk3_0)!=(esk59_0)), inference(rw,[status(thm)],[c_0_122, c_0_121])).
% 1.01/0.43 thf(c_0_126, plain, ![X8:$o]:((((f1)=(f2))|(f2 @ ((X8))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_124]), c_0_125])).
% 1.01/0.43 thf(c_0_127, plain, ((f1)=(f2)), inference(spm,[status(thm)],[c_0_99, c_0_126])).
% 1.01/0.43 thf(c_0_128, plain, ![X185:$o]:(((f1 @ ((X185)))<=>(f2 @ ((X185))))), inference(arg_cong,[status(thm)],[c_0_127])).
% 1.01/0.43 thf(c_0_129, plain, ![X8:$o]:(((f2 @ ((X8)))|~((f1 @ ((X8)))))), inference(dynamic_cnf,[status(thm)],[c_0_128])).
% 1.01/0.43 thf(c_0_130, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_129, c_0_39]), c_0_99]), ['proof']).
% 1.01/0.43 % SZS output end CNFRefutation
% 1.01/0.43 % Parsed axioms : 17
% 1.01/0.43 % Removed by relevancy pruning/SinE : 6
% 1.01/0.43 % Initial clauses : 326
% 1.01/0.43 % Removed in clause preprocessing : 182
% 1.01/0.43 % Initial clauses in saturation : 144
% 1.01/0.43 % Processed clauses : 1691
% 1.01/0.43 % ...of these trivial : 36
% 1.01/0.43 % ...subsumed : 760
% 1.01/0.43 % ...remaining for further processing : 895
% 1.01/0.43 % Other redundant clauses eliminated : 21
% 1.01/0.43 % Clauses deleted for lack of memory : 0
% 1.01/0.43 % Backward-subsumed : 246
% 1.01/0.43 % Backward-rewritten : 328
% 1.01/0.43 % Generated clauses : 4557
% 1.01/0.43 % ...of the previous two non-redundant : 3546
% 1.01/0.43 % ...aggressively subsumed : 0
% 1.01/0.43 % Contextual simplify-reflections : 19
% 1.01/0.43 % Paramodulations : 3311
% 1.01/0.43 % Factorizations : 32
% 1.01/0.43 % NegExts : 159
% 1.01/0.43 % Equation resolutions : 21
% 1.01/0.43 % Disequality decompositions : 0
% 1.01/0.43 % Total rewrite steps : 2150
% 1.01/0.43 % ...of those cached : 2121
% 1.01/0.43 % Propositional unsat checks : 0
% 1.01/0.43 % Propositional check models : 0
% 1.01/0.43 % Propositional check unsatisfiable : 0
% 1.01/0.43 % Propositional clauses : 0
% 1.01/0.43 % Propositional clauses after purity: 0
% 1.01/0.43 % Propositional unsat core size : 0
% 1.01/0.43 % Propositional preprocessing time : 0.000
% 1.01/0.43 % Propositional encoding time : 0.000
% 1.01/0.43 % Propositional solver time : 0.000
% 1.01/0.43 % Success case prop preproc time : 0.000
% 1.01/0.43 % Success case prop encoding time : 0.000
% 1.01/0.43 % Success case prop solver time : 0.000
% 1.01/0.43 % Current number of processed clauses : 162
% 1.01/0.43 % Positive orientable unit clauses : 18
% 1.01/0.43 % Positive unorientable unit clauses: 0
% 1.01/0.43 % Negative unit clauses : 6
% 1.01/0.43 % Non-unit-clauses : 138
% 1.01/0.43 % Current number of unprocessed clauses: 1509
% 1.01/0.43 % ...number of literals in the above : 5905
% 1.01/0.43 % Current number of archived formulas : 0
% 1.01/0.43 % Current number of archived clauses : 715
% 1.01/0.43 % Clause-clause subsumption calls (NU) : 67877
% 1.01/0.43 % Rec. Clause-clause subsumption calls : 54408
% 1.01/0.43 % Non-unit clause-clause subsumptions : 783
% 1.01/0.43 % Unit Clause-clause subsumption calls : 1590
% 1.01/0.43 % Rewrite failures with RHS unbound : 0
% 1.01/0.43 % BW rewrite match attempts : 16
% 1.01/0.43 % BW rewrite match successes : 15
% 1.01/0.43 % Condensation attempts : 1691
% 1.01/0.43 % Condensation successes : 23
% 1.01/0.43 % Termbank termtop insertions : 86868
% 1.01/0.43 % Search garbage collected termcells : 3767
% 1.01/0.43
% 1.01/0.43 % -------------------------------------------------
% 1.01/0.43 % User time : 0.171 s
% 1.01/0.43 % System time : 0.013 s
% 1.01/0.43 % Total time : 0.184 s
% 1.01/0.43 % Maximum resident set size: 4928 pages
% 1.01/0.43
% 1.01/0.43 % -------------------------------------------------
% 1.01/0.43 % User time : 0.172 s
% 1.01/0.43 % System time : 0.022 s
% 1.01/0.43 % Total time : 0.194 s
% 1.01/0.43 % Maximum resident set size: 4864 pages
% 1.01/0.43 % E exiting
%------------------------------------------------------------------------------