%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEV046^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:34:46 AM UTC 2026
% Result : Theorem 81.32s 12.07s
% Output : CNFRefutation 81.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV046^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.28 % Computer : n015.cluster.edu
% 0.12/0.28 % Model : x86_64 x86_64
% 0.12/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.28 % Memory : 8046.5625MB
% 0.12/0.28 % OS : Linux 6.8.0-71-generic
% 0.12/0.28 % CPULimit : 300
% 0.12/0.29 % WCLimit : 300
% 0.12/0.29 % DateTime : Tue Sep 29 15:08:32 UTC 2026
% 0.12/0.29 % CPUTime :
% 0.12/0.29 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.30/0.36 Running higher-order theorem proving
% 0.30/0.38 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.VilktDF3TZ/E---3.1_3638816.p
% 81.32/12.07 % Version: 3.5.1-ho
% 81.32/12.07 % Preprocessing class: HSMSSMSSSSSNSSA.
% 81.32/12.07 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 81.32/12.07 % Starting post_as_ho1 with 1500s (5) cores
% 81.32/12.07 % Starting post_as_ho12 with 300s (1) cores
% 81.32/12.07 % Starting new_ho_3 with 300s (1) cores
% 81.32/12.07 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 81.32/12.07 % new_ho_3 with pid 3638831 completed with status 0
% 81.32/12.07 % Result found by new_ho_3
% 81.32/12.07 % Preprocessing class: HSMSSMSSSSSNSSA.
% 81.32/12.07 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 81.32/12.07 % Starting post_as_ho1 with 1500s (5) cores
% 81.32/12.07 % Starting post_as_ho12 with 300s (1) cores
% 81.32/12.07 % Starting new_ho_3 with 300s (1) cores
% 81.32/12.07 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 81.32/12.07 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 81.32/12.07 % Search class: HGHSF-FFMF00-SSSFFSBN
% 81.32/12.07 % partial match(1): HGHSF-FFSF00-SSSFFSBN
% 81.32/12.07 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 81.32/12.07 % Starting SubtermCWHack with 28s (1) cores
% 81.32/12.07 % SubtermCWHack with pid 3638836 completed with status 0
% 81.32/12.07 % Result found by SubtermCWHack
% 81.32/12.07 % Preprocessing class: HSMSSMSSSSSNSSA.
% 81.32/12.07 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 81.32/12.07 % Starting post_as_ho1 with 1500s (5) cores
% 81.32/12.07 % Starting post_as_ho12 with 300s (1) cores
% 81.32/12.07 % Starting new_ho_3 with 300s (1) cores
% 81.32/12.07 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 81.32/12.07 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 81.32/12.07 % Search class: HGHSF-FFMF00-SSSFFSBN
% 81.32/12.07 % partial match(1): HGHSF-FFSF00-SSSFFSBN
% 81.32/12.07 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 81.32/12.07 % Starting SubtermCWHack with 28s (1) cores
% 81.32/12.07 % Preprocessing time : 0.001 s
% 81.32/12.07
% 81.32/12.07 % Proof found!
% 81.32/12.07 % SZS status Theorem
% 81.32/12.07 % SZS output start CNFRefutation
% 81.32/12.07 thf(decl_sort1, type, a: $tType).
% 81.32/12.07 thf(decl_sort2, type, b: $tType).
% 81.32/12.07 thf(decl_23, type, epred1_2: (a > b > b > $o) > (a > a > $o) > $o).
% 81.32/12.07 thf(decl_24, type, epred2_0: a > a > $o).
% 81.32/12.07 thf(decl_25, type, epred3_0: a > b > b > $o).
% 81.32/12.07 thf(decl_26, type, esk1_0: a > b).
% 81.32/12.07 thf(decl_27, type, esk2_0: a > b).
% 81.32/12.07 thf(decl_28, type, esk3_0: a).
% 81.32/12.07 thf(decl_29, type, esk4_0: a).
% 81.32/12.07 thf(decl_30, type, esk5_0: a > b).
% 81.32/12.07 thf(decl_31, type, esk6_0: a > b).
% 81.32/12.07 thf(decl_32, type, esk7_0: a > b).
% 81.32/12.07 thf(decl_33, type, esk8_0: a).
% 81.32/12.07 thf(decl_34, type, esk9_0: a).
% 81.32/12.07 thf(cTHM507_pme, conjecture, ![X1:a > a > $o, X2:a > b > b > $o]:(((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&![X3:a]:(((X1 @ X3 @ X3)=>(![X6:b, X7:b]:(((X2 @ X3 @ X6 @ X7)=>(X2 @ X3 @ X7 @ X6)))&![X6:b, X8:b, X9:b]:((((X2 @ X3 @ X6 @ X8)&(X2 @ X3 @ X8 @ X9))=>(X2 @ X3 @ X6 @ X9)))))))&![X3:a, X4:a]:(((X1 @ X3 @ X4)=>((X2 @ X3)=(X2 @ X4)))))=>(![X10:a > b, X11:a > b]:((![X12:a, X13:a]:(((X1 @ X12 @ X13)=>(X2 @ X12 @ (X10 @ X12) @ (X11 @ X13))))=>![X14:a, X13:a]:(((X1 @ X14 @ X13)=>(X2 @ X14 @ (X11 @ X14) @ (X10 @ X13))))))&![X15:a > b, X16:a > b, X17:a > b]:(((![X18:a, X13:a]:(((X1 @ X18 @ X13)=>(X2 @ X18 @ (X15 @ X18) @ (X16 @ X13))))&![X19:a, X13:a]:(((X1 @ X19 @ X13)=>(X2 @ X19 @ (X16 @ X19) @ (X17 @ X13)))))=>![X20:a, X13:a]:(((X1 @ X20 @ X13)=>(X2 @ X20 @ (X15 @ X20) @ (X17 @ X13))))))))), file('/export/starexec/sandbox/tmp/tmp.VilktDF3TZ/E---3.1_3638816.p', cTHM507_pme)).
% 81.32/12.07 thf(c_0_1, plain, ![X1:a > a > $o, X2:a > b > b > $o]:(((epred1_2 @ X2 @ X1)<=>(((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&![X3:a]:(((X1 @ X3 @ X3)=>(![X6:b, X7:b]:(((X2 @ X3 @ X6 @ X7)=>(X2 @ X3 @ X7 @ X6)))&![X6:b, X8:b, X9:b]:((((X2 @ X3 @ X6 @ X8)&(X2 @ X3 @ X8 @ X9))=>(X2 @ X3 @ X6 @ X9)))))))&![X3:a, X4:a]:(((X1 @ X3 @ X4)=>((X2 @ X3)=(X2 @ X4))))))), introduced(definition)).
% 81.32/12.07 thf(c_0_2, negated_conjecture, ~(![X1:a > a > $o, X2:a > b > b > $o]:(((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&![X3:a]:(((X1 @ X3 @ X3)=>(![X6:b, X7:b]:(((X2 @ X3 @ X6 @ X7)=>(X2 @ X3 @ X7 @ X6)))&![X6:b, X8:b, X9:b]:((((X2 @ X3 @ X6 @ X8)&(X2 @ X3 @ X8 @ X9))=>(X2 @ X3 @ X6 @ X9)))))))&![X3:a, X4:a]:(((X1 @ X3 @ X4)=>((X2 @ X3)=(X2 @ X4)))))=>(![X10:a > b, X11:a > b]:((![X12:a, X13:a]:(((X1 @ X12 @ X13)=>(X2 @ X12 @ (X10 @ X12) @ (X11 @ X13))))=>![X14:a, X13:a]:(((X1 @ X14 @ X13)=>(X2 @ X14 @ (X11 @ X14) @ (X10 @ X13))))))&![X15:a > b, X16:a > b, X17:a > b]:(((![X18:a, X13:a]:(((X1 @ X18 @ X13)=>(X2 @ X18 @ (X15 @ X18) @ (X16 @ X13))))&![X19:a, X13:a]:(((X1 @ X19 @ X13)=>(X2 @ X19 @ (X16 @ X19) @ (X17 @ X13)))))=>![X20:a, X13:a]:(((X1 @ X20 @ X13)=>(X2 @ X20 @ (X15 @ X20) @ (X17 @ X13)))))))))), inference(assume_negation,[status(cth)],[cTHM507_pme])).
% 81.32/12.07 thf(c_0_3, plain, ![X1:a > a > $o, X2:a > b > b > $o]:(((epred1_2 @ X2 @ X1)=>(((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&![X3:a]:(((X1 @ X3 @ X3)=>(![X6:b, X7:b]:(((X2 @ X3 @ X6 @ X7)=>(X2 @ X3 @ X7 @ X6)))&![X6:b, X8:b, X9:b]:((((X2 @ X3 @ X6 @ X8)&(X2 @ X3 @ X8 @ X9))=>(X2 @ X3 @ X6 @ X9)))))))&![X3:a, X4:a]:(((X1 @ X3 @ X4)=>((X2 @ X3)=(X2 @ X4))))))), inference(split_equiv,[status(thm)],[c_0_1])).
% 81.32/12.07 thf(c_0_4, negated_conjecture, ~(![X1:a > a > $o, X2:a > b > b > $o]:(((epred1_2 @ X2 @ X1)=>(![X10:a > b, X11:a > b]:((![X12:a, X13:a]:(((X1 @ X12 @ X13)=>(X2 @ X12 @ (X10 @ X12) @ (X11 @ X13))))=>![X14:a, X13:a]:(((X1 @ X14 @ X13)=>(X2 @ X14 @ (X11 @ X14) @ (X10 @ X13))))))&![X15:a > b, X16:a > b, X17:a > b]:(((![X18:a, X13:a]:(((X1 @ X18 @ X13)=>(X2 @ X18 @ (X15 @ X18) @ (X16 @ X13))))&![X19:a, X13:a]:(((X1 @ X19 @ X13)=>(X2 @ X19 @ (X16 @ X19) @ (X17 @ X13)))))=>![X20:a, X13:a]:(((X1 @ X20 @ X13)=>(X2 @ X20 @ (X15 @ X20) @ (X17 @ X13)))))))))), inference(apply_def,[status(thm)],[c_0_2, c_0_1])).
% 81.32/12.07 thf(c_0_5, plain, ![X68:a > a > $o, X69:a > b > b > $o, X70:a, X71:a, X72:a, X73:a, X74:a, X75:a, X76:b, X77:b, X78:b, X79:b, X80:b, X81:a, X82:a]:(((((~(X68 @ X70 @ X71)|(X68 @ X71 @ X70)|~(epred1_2 @ X69 @ X68))&(~(X68 @ X72 @ X73)|~(X68 @ X73 @ X74)|(X68 @ X72 @ X74)|~(epred1_2 @ X69 @ X68)))&((~(X69 @ X75 @ X76 @ X77)|(X69 @ X75 @ X77 @ X76)|~(X68 @ X75 @ X75)|~(epred1_2 @ X69 @ X68))&(~(X69 @ X75 @ X78 @ X79)|~(X69 @ X75 @ X79 @ X80)|(X69 @ X75 @ X78 @ X80)|~(X68 @ X75 @ X75)|~(epred1_2 @ X69 @ X68))))&(~(X68 @ X81 @ X82)|((X69 @ X81)=(X69 @ X82))|~(epred1_2 @ X69 @ X68)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])).
% 81.32/12.07 thf(c_0_6, negated_conjecture, ![X55:a, X56:a, X62:a, X63:a, X64:a, X65:a]:(((epred1_2 @ epred3_0 @ epred2_0)&((((~(epred2_0 @ X62 @ X63)|(epred3_0 @ X62 @ (esk5_0 @ X62) @ (esk6_0 @ X63))|(~(epred2_0 @ X55 @ X56)|(epred3_0 @ X55 @ (esk1_0 @ X55) @ (esk2_0 @ X56))))&(~(epred2_0 @ X64 @ X65)|(epred3_0 @ X64 @ (esk6_0 @ X64) @ (esk7_0 @ X65))|(~(epred2_0 @ X55 @ X56)|(epred3_0 @ X55 @ (esk1_0 @ X55) @ (esk2_0 @ X56)))))&(((epred2_0 @ esk8_0 @ esk9_0)|(~(epred2_0 @ X55 @ X56)|(epred3_0 @ X55 @ (esk1_0 @ X55) @ (esk2_0 @ X56))))&(~(epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0))|(~(epred2_0 @ X55 @ X56)|(epred3_0 @ X55 @ (esk1_0 @ X55) @ (esk2_0 @ X56))))))&((((~(epred2_0 @ X62 @ X63)|(epred3_0 @ X62 @ (esk5_0 @ X62) @ (esk6_0 @ X63))|(epred2_0 @ esk3_0 @ esk4_0))&(~(epred2_0 @ X64 @ X65)|(epred3_0 @ X64 @ (esk6_0 @ X64) @ (esk7_0 @ X65))|(epred2_0 @ esk3_0 @ esk4_0)))&(((epred2_0 @ esk8_0 @ esk9_0)|(epred2_0 @ esk3_0 @ esk4_0))&(~(epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0))|(epred2_0 @ esk3_0 @ esk4_0))))&(((~(epred2_0 @ X62 @ X63)|(epred3_0 @ X62 @ (esk5_0 @ X62) @ (esk6_0 @ X63))|~(epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0)))&(~(epred2_0 @ X64 @ X65)|(epred3_0 @ X64 @ (esk6_0 @ X64) @ (esk7_0 @ X65))|~(epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0))))&(((epred2_0 @ esk8_0 @ esk9_0)|~(epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0)))&(~(epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0))|~(epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])])])).
% 81.32/12.07 thf(c_0_7, plain, ![X3:a, X2:a > b > b > $o, X4:a, X1:a > a > $o]:(((X1 @ X4 @ X3)|~((X1 @ X3 @ X4))|~((epred1_2 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 81.32/12.07 thf(c_0_8, negated_conjecture, (epred1_2 @ epred3_0 @ epred2_0), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_9, plain, ![X3:a, X2:a > b > b > $o, X4:a, X1:a > a > $o]:((((X2 @ X3)=(X2 @ X4))|~((X1 @ X3 @ X4))|~((epred1_2 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 81.32/12.07 thf(c_0_10, negated_conjecture, ![X4:a, X3:a]:(((epred2_0 @ X3 @ X4)|~((epred2_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 81.32/12.07 thf(c_0_11, negated_conjecture, ((epred2_0 @ esk8_0 @ esk9_0)|(epred2_0 @ esk3_0 @ esk4_0)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_12, negated_conjecture, ![X3:a, X4:a]:((((epred3_0 @ X3)=(epred3_0 @ X4))|~((epred2_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_9, c_0_8])).
% 81.32/12.07 thf(c_0_13, negated_conjecture, ((epred2_0 @ esk3_0 @ esk4_0)|(epred2_0 @ esk9_0 @ esk8_0)), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 81.32/12.07 thf(c_0_14, plain, ![X3:a, X2:a > b > b > $o, X5:a, X4:a, X1:a > a > $o]:(((X1 @ X3 @ X5)|~((X1 @ X3 @ X4))|~((X1 @ X4 @ X5))|~((epred1_2 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 81.32/12.07 thf(c_0_15, negated_conjecture, (((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred2_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_12, c_0_13])).
% 81.32/12.07 thf(c_0_16, negated_conjecture, ![X3:a, X4:a, X5:a]:(((epred2_0 @ X3 @ X4)|~((epred2_0 @ X5 @ X4))|~((epred2_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_14, c_0_8])).
% 81.32/12.07 thf(c_0_17, plain, ![X3:a, X2:a > b > b > $o, X7:b, X6:b, X1:a > a > $o]:(((X2 @ X3 @ X7 @ X6)|~((X2 @ X3 @ X6 @ X7))|~((X1 @ X3 @ X3))|~((epred1_2 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 81.32/12.07 thf(c_0_18, negated_conjecture, ![X87:b, X88:b]:((((epred3_0 @ esk9_0 @ X87 @ X88)<=>(epred3_0 @ esk8_0 @ X87 @ X88))|(epred2_0 @ esk3_0 @ esk4_0))), inference(arg_cong,[status(thm)],[c_0_15])).
% 81.32/12.07 thf(c_0_19, negated_conjecture, ![X3:a]:(((epred2_0 @ esk3_0 @ esk4_0)|(epred2_0 @ X3 @ esk9_0)|~((epred2_0 @ X3 @ esk8_0)))), inference(spm,[status(thm)],[c_0_16, c_0_11])).
% 81.32/12.07 thf(c_0_20, negated_conjecture, ![X7:b, X6:b, X3:a]:(((epred3_0 @ X3 @ X6 @ X7)|~((epred3_0 @ X3 @ X7 @ X6))|~((epred2_0 @ X3 @ X3)))), inference(spm,[status(thm)],[c_0_17, c_0_8])).
% 81.32/12.07 thf(c_0_21, negated_conjecture, ![X6:b, X7:b]:(((epred2_0 @ esk3_0 @ esk4_0)|(epred3_0 @ esk9_0 @ X6 @ X7)|~((epred3_0 @ esk8_0 @ X6 @ X7)))), inference(dynamic_cnf,[status(thm)],[c_0_18])).
% 81.32/12.07 thf(c_0_22, negated_conjecture, ((epred2_0 @ esk9_0 @ esk9_0)|(epred2_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_19, c_0_13])).
% 81.32/12.07 thf(c_0_23, negated_conjecture, ![X6:b, X7:b]:(((epred2_0 @ esk3_0 @ esk4_0)|(epred3_0 @ esk8_0 @ X6 @ X7)|~((epred3_0 @ esk9_0 @ X6 @ X7)))), inference(dynamic_cnf,[status(thm)],[c_0_18])).
% 81.32/12.07 thf(c_0_24, negated_conjecture, ![X7:b, X6:b]:(((epred2_0 @ esk3_0 @ esk4_0)|(epred3_0 @ esk9_0 @ X6 @ X7)|~((epred3_0 @ esk8_0 @ X7 @ X6)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_22])).
% 81.32/12.07 thf(c_0_25, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk6_0 @ X3) @ (esk7_0 @ X4))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred2_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_26, plain, ![X3:a, X2:a > b > b > $o, X8:b, X7:b, X6:b, X1:a > a > $o]:(((X2 @ X3 @ X6 @ X8)|~((X2 @ X3 @ X6 @ X7))|~((X2 @ X3 @ X7 @ X8))|~((X1 @ X3 @ X3))|~((epred1_2 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 81.32/12.07 thf(c_0_27, negated_conjecture, ![X7:b, X6:b]:(((epred3_0 @ esk8_0 @ X6 @ X7)|(epred2_0 @ esk3_0 @ esk4_0)|~((epred3_0 @ esk8_0 @ X7 @ X6)))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 81.32/12.07 thf(c_0_28, negated_conjecture, ![X3:a]:(((epred3_0 @ esk8_0 @ (esk6_0 @ esk9_0) @ (esk7_0 @ X3))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred2_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_23, c_0_25])).
% 81.32/12.07 thf(c_0_29, negated_conjecture, ![X3:a]:(((epred2_0 @ esk3_0 @ esk4_0)|(epred2_0 @ X3 @ esk8_0)|~((epred2_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_16, c_0_13])).
% 81.32/12.07 thf(c_0_30, negated_conjecture, ![X6:b, X8:b, X7:b, X3:a]:(((epred3_0 @ X3 @ X6 @ X7)|~((epred3_0 @ X3 @ X8 @ X7))|~((epred3_0 @ X3 @ X6 @ X8))|~((epred2_0 @ X3 @ X3)))), inference(spm,[status(thm)],[c_0_26, c_0_8])).
% 81.32/12.07 thf(c_0_31, negated_conjecture, ![X3:a]:(((epred3_0 @ esk8_0 @ (esk7_0 @ X3) @ (esk6_0 @ esk9_0))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred2_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 81.32/12.07 thf(c_0_32, negated_conjecture, ((epred2_0 @ esk8_0 @ esk8_0)|(epred2_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_29, c_0_11])).
% 81.32/12.07 thf(c_0_33, negated_conjecture, ![X6:b, X3:a]:(((epred3_0 @ esk8_0 @ X6 @ (esk6_0 @ esk9_0))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred3_0 @ esk8_0 @ X6 @ (esk7_0 @ X3)))|~((epred2_0 @ esk9_0 @ X3)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_32])).
% 81.32/12.07 thf(c_0_34, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk5_0 @ X3) @ (esk6_0 @ X4))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred2_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_35, negated_conjecture, ![X3:a]:(((epred3_0 @ esk8_0 @ (esk6_0 @ esk8_0) @ (esk6_0 @ esk9_0))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred2_0 @ esk9_0 @ X3))|~((epred2_0 @ esk8_0 @ X3)))), inference(spm,[status(thm)],[c_0_33, c_0_25])).
% 81.32/12.07 thf(c_0_36, negated_conjecture, ![X3:a]:(((epred3_0 @ esk8_0 @ (esk6_0 @ X3) @ (esk5_0 @ esk8_0))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred2_0 @ esk8_0 @ X3)))), inference(spm,[status(thm)],[c_0_27, c_0_34])).
% 81.32/12.07 thf(c_0_37, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk6_0 @ esk8_0) @ (esk6_0 @ esk9_0))|(epred2_0 @ esk3_0 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_22]), c_0_11])).
% 81.32/12.07 thf(c_0_38, negated_conjecture, ![X6:b, X3:a]:(((epred3_0 @ esk8_0 @ X6 @ (esk5_0 @ esk8_0))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred3_0 @ esk8_0 @ X6 @ (esk6_0 @ X3)))|~((epred2_0 @ esk8_0 @ X3)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_36]), c_0_32])).
% 81.32/12.07 thf(c_0_39, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk6_0 @ esk9_0) @ (esk6_0 @ esk8_0))|(epred2_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_27, c_0_37])).
% 81.32/12.07 thf(c_0_40, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk6_0 @ esk9_0) @ (esk5_0 @ esk8_0))|(epred2_0 @ esk3_0 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_32])).
% 81.32/12.07 thf(c_0_41, negated_conjecture, ![X6:b, X3:a]:(((epred3_0 @ esk8_0 @ X6 @ (esk7_0 @ X3))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred3_0 @ esk8_0 @ X6 @ (esk6_0 @ esk9_0)))|~((epred2_0 @ esk9_0 @ X3)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_28]), c_0_32])).
% 81.32/12.07 thf(c_0_42, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk6_0 @ esk9_0))|(epred2_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_27, c_0_40])).
% 81.32/12.07 thf(c_0_43, negated_conjecture, ((epred2_0 @ esk3_0 @ esk4_0)|~((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_44, negated_conjecture, ![X3:a]:(((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ X3))|(epred2_0 @ esk3_0 @ esk4_0)|~((epred2_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 81.32/12.07 thf(c_0_45, negated_conjecture, (epred2_0 @ esk3_0 @ esk4_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_22])).
% 81.32/12.07 thf(c_0_46, negated_conjecture, ((epred3_0 @ esk4_0)=(epred3_0 @ esk3_0)), inference(spm,[status(thm)],[c_0_12, c_0_45])).
% 81.32/12.07 thf(c_0_47, negated_conjecture, ![X3:a]:(((epred2_0 @ X3 @ esk4_0)|~((epred2_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_16, c_0_45])).
% 81.32/12.07 thf(c_0_48, negated_conjecture, ![X364:b, X365:b]:(((epred3_0 @ esk4_0 @ X364 @ X365)<=>(epred3_0 @ esk3_0 @ X364 @ X365))), inference(arg_cong,[status(thm)],[c_0_46])).
% 81.32/12.07 thf(c_0_49, negated_conjecture, ![X3:a, X4:a]:(((epred2_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ (esk1_0 @ X3) @ (esk2_0 @ X4))|~((epred2_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_50, negated_conjecture, ![X3:a]:(((epred2_0 @ esk4_0 @ X3)|~((epred2_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_10, c_0_47])).
% 81.32/12.07 thf(c_0_51, negated_conjecture, (epred2_0 @ esk4_0 @ esk3_0), inference(spm,[status(thm)],[c_0_10, c_0_45])).
% 81.32/12.07 thf(c_0_52, negated_conjecture, ![X6:b, X7:b]:(((epred3_0 @ esk3_0 @ X6 @ X7)|~((epred3_0 @ esk4_0 @ X6 @ X7)))), inference(dynamic_cnf,[status(thm)],[c_0_48])).
% 81.32/12.07 thf(c_0_53, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk2_0 @ X4) @ (esk1_0 @ X3))|(epred2_0 @ esk8_0 @ esk9_0)|~((epred2_0 @ X3 @ X3))|~((epred2_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_20, c_0_49])).
% 81.32/12.07 thf(c_0_54, negated_conjecture, (epred2_0 @ esk4_0 @ esk4_0), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 81.32/12.07 thf(c_0_55, negated_conjecture, ((epred2_0 @ esk8_0 @ esk9_0)|~((epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_56, negated_conjecture, ![X3:a]:(((epred3_0 @ esk3_0 @ (esk2_0 @ X3) @ (esk1_0 @ esk4_0))|(epred2_0 @ esk8_0 @ esk9_0)|~((epred2_0 @ esk4_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_53]), c_0_54])])).
% 81.32/12.07 thf(c_0_57, negated_conjecture, (((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|((epred3_0 @ esk4_0)=(epred3_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_12, c_0_15])).
% 81.32/12.07 thf(c_0_58, negated_conjecture, ![X3:a]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred2_0 @ X3 @ esk4_0)|~((epred2_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_16, c_0_15])).
% 81.32/12.07 thf(c_0_59, negated_conjecture, (epred2_0 @ esk8_0 @ esk9_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_51])])).
% 81.32/12.07 thf(c_0_60, negated_conjecture, ![X95:b, X96:b]:((((epred3_0 @ esk4_0 @ X95 @ X96)<=>(epred3_0 @ esk3_0 @ X95 @ X96))|((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0)))), inference(arg_cong,[status(thm)],[c_0_57])).
% 81.32/12.07 thf(c_0_61, negated_conjecture, ![X3:a]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred2_0 @ esk4_0 @ X3)|~((epred2_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_10, c_0_58])).
% 81.32/12.07 thf(c_0_62, negated_conjecture, (((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred2_0 @ esk4_0 @ esk3_0)), inference(spm,[status(thm)],[c_0_10, c_0_15])).
% 81.32/12.07 thf(c_0_63, negated_conjecture, ![X3:a, X4:a, X5:a, X12:a]:(((epred3_0 @ X3 @ (esk6_0 @ X3) @ (esk7_0 @ X4))|(epred3_0 @ X5 @ (esk1_0 @ X5) @ (esk2_0 @ X12))|~((epred2_0 @ X3 @ X4))|~((epred2_0 @ X5 @ X12)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_64, negated_conjecture, (epred2_0 @ esk9_0 @ esk8_0), inference(spm,[status(thm)],[c_0_10, c_0_59])).
% 81.32/12.07 thf(c_0_65, negated_conjecture, ![X6:b, X7:b]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred3_0 @ esk4_0 @ X6 @ X7)|~((epred3_0 @ esk3_0 @ X6 @ X7)))), inference(dynamic_cnf,[status(thm)],[c_0_60])).
% 81.32/12.07 thf(c_0_66, negated_conjecture, (((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred2_0 @ esk4_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 81.32/12.07 thf(c_0_67, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ esk4_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))|(epred3_0 @ X3 @ (esk6_0 @ X3) @ (esk7_0 @ X4))|~((epred2_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_63, c_0_51])).
% 81.32/12.07 thf(c_0_68, negated_conjecture, ![X3:a, X4:a, X5:a, X12:a]:(((epred3_0 @ X3 @ (esk5_0 @ X3) @ (esk6_0 @ X4))|(epred3_0 @ X5 @ (esk1_0 @ X5) @ (esk2_0 @ X12))|~((epred2_0 @ X3 @ X4))|~((epred2_0 @ X5 @ X12)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_69, negated_conjecture, ![X3:a]:(((epred2_0 @ X3 @ esk8_0)|~((epred2_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_16, c_0_64])).
% 81.32/12.07 thf(c_0_70, negated_conjecture, ![X6:b, X7:b]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred3_0 @ esk3_0 @ X6 @ X7)|~((epred3_0 @ esk4_0 @ X6 @ X7)))), inference(dynamic_cnf,[status(thm)],[c_0_60])).
% 81.32/12.07 thf(c_0_71, negated_conjecture, ![X7:b, X6:b]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred3_0 @ esk4_0 @ X6 @ X7)|~((epred3_0 @ esk3_0 @ X7 @ X6)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_65]), c_0_66])).
% 81.32/12.07 thf(c_0_72, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk6_0 @ esk8_0) @ (esk7_0 @ esk9_0))|(epred3_0 @ esk4_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_67, c_0_59])).
% 81.32/12.07 thf(c_0_73, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ esk4_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))|(epred3_0 @ X3 @ (esk5_0 @ X3) @ (esk6_0 @ X4))|~((epred2_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_68, c_0_51])).
% 81.32/12.07 thf(c_0_74, negated_conjecture, (epred2_0 @ esk8_0 @ esk8_0), inference(spm,[status(thm)],[c_0_69, c_0_59])).
% 81.32/12.07 thf(c_0_75, negated_conjecture, ![X7:b, X6:b]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred3_0 @ esk3_0 @ X6 @ X7)|~((epred3_0 @ esk3_0 @ X7 @ X6)))), inference(spm,[status(thm)],[c_0_70, c_0_71])).
% 81.32/12.07 thf(c_0_76, negated_conjecture, ![X3:a]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred3_0 @ esk3_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ X3))|~((epred2_0 @ esk4_0 @ X3)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_49]), c_0_12])).
% 81.32/12.07 thf(c_0_77, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk6_0 @ esk8_0) @ (esk7_0 @ esk9_0))|(epred3_0 @ esk3_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_52, c_0_72])).
% 81.32/12.07 thf(c_0_78, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk6_0 @ esk8_0))|(epred3_0 @ esk4_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_73, c_0_74])).
% 81.32/12.07 thf(c_0_79, negated_conjecture, ![X3:a]:((((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0))|(epred3_0 @ esk3_0 @ (esk2_0 @ X3) @ (esk1_0 @ esk4_0))|~((epred2_0 @ esk4_0 @ X3)))), inference(spm,[status(thm)],[c_0_75, c_0_76])).
% 81.32/12.07 thf(c_0_80, negated_conjecture, ![X6:b]:(((epred3_0 @ esk3_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))|(epred3_0 @ esk8_0 @ X6 @ (esk7_0 @ esk9_0))|~((epred3_0 @ esk8_0 @ X6 @ (esk6_0 @ esk8_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_77]), c_0_74])])).
% 81.32/12.07 thf(c_0_81, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk6_0 @ esk8_0))|(epred3_0 @ esk3_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_52, c_0_78])).
% 81.32/12.07 thf(c_0_82, negated_conjecture, ((epred3_0 @ esk9_0)=(epred3_0 @ esk8_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_79]), c_0_62]), c_0_12])).
% 81.32/12.07 thf(c_0_83, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk1_0 @ X3) @ (esk2_0 @ X4))|~((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0)))|~((epred2_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_84, negated_conjecture, ((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0))|(epred3_0 @ esk3_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 81.32/12.07 thf(c_0_85, negated_conjecture, ![X301:b, X302:b]:(((epred3_0 @ esk9_0 @ X301 @ X302)<=>(epred3_0 @ esk8_0 @ X301 @ X302))), inference(arg_cong,[status(thm)],[c_0_82])).
% 81.32/12.07 thf(c_0_86, negated_conjecture, ![X3:a]:(((epred2_0 @ X3 @ esk9_0)|~((epred2_0 @ X3 @ esk8_0)))), inference(spm,[status(thm)],[c_0_16, c_0_59])).
% 81.32/12.07 thf(c_0_87, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ esk3_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0))|(epred3_0 @ X3 @ (esk1_0 @ X3) @ (esk2_0 @ X4))|~((epred2_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_83, c_0_84])).
% 81.32/12.07 thf(c_0_88, negated_conjecture, ![X3:a]:(((epred2_0 @ X3 @ esk3_0)|~((epred2_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_16, c_0_51])).
% 81.32/12.07 thf(c_0_89, negated_conjecture, ![X6:b, X7:b]:(((epred3_0 @ esk9_0 @ X6 @ X7)|~((epred3_0 @ esk8_0 @ X6 @ X7)))), inference(dynamic_cnf,[status(thm)],[c_0_85])).
% 81.32/12.07 thf(c_0_90, negated_conjecture, ![X3:a]:(((epred2_0 @ esk9_0 @ X3)|~((epred2_0 @ X3 @ esk8_0)))), inference(spm,[status(thm)],[c_0_10, c_0_86])).
% 81.32/12.07 thf(c_0_91, negated_conjecture, (epred3_0 @ esk3_0 @ (esk1_0 @ esk4_0) @ (esk2_0 @ esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_51]), c_0_52])).
% 81.32/12.07 thf(c_0_92, negated_conjecture, (epred2_0 @ esk3_0 @ esk3_0), inference(spm,[status(thm)],[c_0_88, c_0_45])).
% 81.32/12.07 thf(c_0_93, negated_conjecture, ![X6:b, X8:b, X7:b]:(((epred3_0 @ esk9_0 @ X6 @ X7)|~((epred3_0 @ esk9_0 @ X6 @ X8))|~((epred2_0 @ esk9_0 @ esk9_0))|~((epred3_0 @ esk8_0 @ X8 @ X7)))), inference(spm,[status(thm)],[c_0_30, c_0_89])).
% 81.32/12.07 thf(c_0_94, negated_conjecture, (epred2_0 @ esk9_0 @ esk9_0), inference(spm,[status(thm)],[c_0_90, c_0_64])).
% 81.32/12.07 thf(c_0_95, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk5_0 @ X3) @ (esk6_0 @ X4))|~((epred2_0 @ X3 @ X4))|~((epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0))))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_96, negated_conjecture, (epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_91]), c_0_92])])).
% 81.32/12.07 thf(c_0_97, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk6_0 @ X3) @ (esk7_0 @ X4))|~((epred2_0 @ X3 @ X4))|~((epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0))))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_98, negated_conjecture, ![X6:b, X8:b, X7:b]:(((epred3_0 @ esk9_0 @ X6 @ X7)|~((epred3_0 @ esk9_0 @ X6 @ X8))|~((epred3_0 @ esk8_0 @ X8 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_93, c_0_94])])).
% 81.32/12.07 thf(c_0_99, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk5_0 @ X3) @ (esk6_0 @ X4))|~((epred2_0 @ X3 @ X4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_96])])).
% 81.32/12.07 thf(c_0_100, negated_conjecture, ![X3:a, X86:b, X85:b, X4:a]:((((epred3_0 @ X3 @ X85 @ X86)<=>(epred3_0 @ X4 @ X85 @ X86))|~((epred2_0 @ X3 @ X4)))), inference(arg_cong,[status(thm)],[c_0_12])).
% 81.32/12.07 thf(c_0_101, negated_conjecture, ![X6:b, X7:b]:(((epred3_0 @ esk8_0 @ X6 @ X7)|~((epred3_0 @ esk9_0 @ X6 @ X7)))), inference(dynamic_cnf,[status(thm)],[c_0_85])).
% 81.32/12.07 thf(c_0_102, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk6_0 @ X3) @ (esk7_0 @ X4))|~((epred2_0 @ X3 @ X4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_97, c_0_96])])).
% 81.32/12.07 thf(c_0_103, negated_conjecture, ![X6:b, X3:a]:(((epred3_0 @ esk9_0 @ (esk5_0 @ esk9_0) @ X6)|~((epred3_0 @ esk8_0 @ (esk6_0 @ X3) @ X6))|~((epred2_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_98, c_0_99])).
% 81.32/12.07 thf(c_0_104, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk6_0 @ X4) @ (esk5_0 @ X3))|~((epred2_0 @ X3 @ X3))|~((epred2_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_20, c_0_99])).
% 81.32/12.07 thf(c_0_105, negated_conjecture, ![X7:b, X6:b, X4:a, X3:a]:(((epred3_0 @ X3 @ X6 @ X7)|~((epred3_0 @ X4 @ X6 @ X7))|~((epred2_0 @ X4 @ X3)))), inference(dynamic_cnf,[status(thm)],[c_0_100])).
% 81.32/12.07 thf(c_0_106, negated_conjecture, ![X3:a]:(((epred3_0 @ esk8_0 @ (esk6_0 @ esk9_0) @ (esk7_0 @ X3))|~((epred2_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_101, c_0_102])).
% 81.32/12.07 thf(c_0_107, negated_conjecture, ![X3:a]:(((epred3_0 @ esk9_0 @ (esk5_0 @ esk9_0) @ (esk5_0 @ esk8_0))|~((epred2_0 @ esk9_0 @ X3))|~((epred2_0 @ esk8_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_104]), c_0_74])])).
% 81.32/12.07 thf(c_0_108, negated_conjecture, ![X3:a, X4:a]:(((epred3_0 @ X3 @ (esk6_0 @ esk9_0) @ (esk7_0 @ X4))|~((epred2_0 @ esk8_0 @ X3))|~((epred2_0 @ esk9_0 @ X4)))), inference(spm,[status(thm)],[c_0_105, c_0_106])).
% 81.32/12.07 thf(c_0_109, negated_conjecture, (epred3_0 @ esk9_0 @ (esk5_0 @ esk9_0) @ (esk5_0 @ esk8_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_86]), c_0_59]), c_0_64])])).
% 81.32/12.07 thf(c_0_110, negated_conjecture, ![X3:a]:(((epred3_0 @ esk9_0 @ (esk5_0 @ esk9_0) @ (esk7_0 @ X3))|~((epred2_0 @ esk9_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_108]), c_0_94]), c_0_74])])).
% 81.32/12.07 thf(c_0_111, negated_conjecture, ![X6:b]:(((epred3_0 @ esk9_0 @ X6 @ (esk5_0 @ esk8_0))|~((epred3_0 @ esk9_0 @ X6 @ (esk5_0 @ esk9_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_109]), c_0_94])])).
% 81.32/12.07 thf(c_0_112, negated_conjecture, ![X3:a]:(((epred3_0 @ esk9_0 @ (esk7_0 @ X3) @ (esk5_0 @ esk9_0))|~((epred2_0 @ esk9_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_110]), c_0_94])])).
% 81.32/12.07 thf(c_0_113, negated_conjecture, ![X3:a]:(((epred3_0 @ esk9_0 @ (esk7_0 @ X3) @ (esk5_0 @ esk8_0))|~((epred2_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_111, c_0_112])).
% 81.32/12.07 thf(c_0_114, negated_conjecture, (~((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0)))|~((epred3_0 @ esk3_0 @ (esk2_0 @ esk3_0) @ (esk1_0 @ esk4_0)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.32/12.07 thf(c_0_115, negated_conjecture, ![X3:a]:(((epred3_0 @ esk9_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ X3))|~((epred2_0 @ esk9_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_113]), c_0_94])])).
% 81.32/12.07 thf(c_0_116, negated_conjecture, ~((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ esk9_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_114, c_0_96])])).
% 81.32/12.07 thf(c_0_117, negated_conjecture, ![X3:a]:(((epred3_0 @ esk8_0 @ (esk5_0 @ esk8_0) @ (esk7_0 @ X3))|~((epred2_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_101, c_0_115])).
% 81.32/12.07 thf(c_0_118, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116, c_0_117]), c_0_94])]), ['proof']).
% 81.32/12.07 % SZS output end CNFRefutation
% 81.32/12.07 % Parsed axioms : 3
% 81.32/12.07 % Removed by relevancy pruning/SinE : 2
% 81.32/12.07 % Initial clauses : 18
% 81.32/12.07 % Removed in clause preprocessing : 0
% 81.32/12.07 % Initial clauses in saturation : 18
% 81.32/12.07 % Processed clauses : 52838
% 81.32/12.07 % ...of these trivial : 490
% 81.32/12.07 % ...subsumed : 41600
% 81.32/12.07 % ...remaining for further processing : 10748
% 81.32/12.07 % Other redundant clauses eliminated : 0
% 81.32/12.07 % Clauses deleted for lack of memory : 0
% 81.32/12.07 % Backward-subsumed : 3183
% 81.32/12.07 % Backward-rewritten : 5586
% 81.32/12.07 % Generated clauses : 350204
% 81.32/12.07 % ...of the previous two non-redundant : 331310
% 81.32/12.07 % ...aggressively subsumed : 0
% 81.32/12.07 % Contextual simplify-reflections : 19
% 81.32/12.07 % Paramodulations : 349956
% 81.32/12.07 % Factorizations : 0
% 81.32/12.07 % NegExts : 0
% 81.32/12.07 % Equation resolutions : 0
% 81.32/12.07 % Disequality decompositions : 0
% 81.32/12.07 % Total rewrite steps : 74026
% 81.32/12.07 % ...of those cached : 73913
% 81.32/12.07 % Propositional unsat checks : 0
% 81.32/12.07 % Propositional check models : 0
% 81.32/12.07 % Propositional check unsatisfiable : 0
% 81.32/12.07 % Propositional clauses : 0
% 81.32/12.07 % Propositional clauses after purity: 0
% 81.32/12.07 % Propositional unsat core size : 0
% 81.32/12.07 % Propositional preprocessing time : 0.000
% 81.32/12.07 % Propositional encoding time : 0.000
% 81.32/12.07 % Propositional solver time : 0.000
% 81.32/12.07 % Success case prop preproc time : 0.000
% 81.32/12.07 % Success case prop encoding time : 0.000
% 81.32/12.07 % Success case prop solver time : 0.000
% 81.32/12.07 % Current number of processed clauses : 1919
% 81.32/12.07 % Positive orientable unit clauses : 85
% 81.32/12.07 % Positive unorientable unit clauses: 0
% 81.32/12.07 % Negative unit clauses : 1
% 81.32/12.07 % Non-unit-clauses : 1833
% 81.32/12.07 % Current number of unprocessed clauses: 184409
% 81.32/12.07 % ...number of literals in the above : 600509
% 81.32/12.07 % Current number of archived formulas : 0
% 81.32/12.07 % Current number of archived clauses : 8829
% 81.32/12.07 % Clause-clause subsumption calls (NU) : 18334340
% 81.32/12.07 % Rec. Clause-clause subsumption calls : 15556873
% 81.32/12.07 % Non-unit clause-clause subsumptions : 43482
% 81.32/12.07 % Unit Clause-clause subsumption calls : 70070
% 81.32/12.07 % Rewrite failures with RHS unbound : 0
% 81.32/12.07 % BW rewrite match attempts : 342
% 81.32/12.07 % BW rewrite match successes : 70
% 81.32/12.07 % Condensation attempts : 0
% 81.32/12.07 % Condensation successes : 0
% 81.32/12.07 % Termbank termtop insertions : 5442222
% 81.32/12.07 % Search garbage collected termcells : 623
% 81.32/12.07
% 81.32/12.07 % -------------------------------------------------
% 81.32/12.07 % User time : 11.390 s
% 81.32/12.07 % System time : 0.141 s
% 81.32/12.07 % Total time : 11.532 s
% 81.32/12.07 % Maximum resident set size: 3604 pages
% 81.32/12.07
% 81.32/12.07 % -------------------------------------------------
% 81.32/12.07 % User time : 11.392 s
% 81.32/12.07 % System time : 0.150 s
% 81.32/12.07 % Total time : 11.542 s
% 81.32/12.07 % Maximum resident set size: 4608 pages
% 81.32/12.07 % E exiting
%------------------------------------------------------------------------------