%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU824^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/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:25:47 AM UTC 2026
% Result : Theorem 3.43s 0.70s
% Output : CNFRefutation 3.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU824^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n006.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 14:34:54 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.07/0.24 Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.OBEHWuQTt3/E---3.1_811975.p
% 3.43/0.70 % Version: 3.5.1-ho
% 3.43/0.70 % Preprocessing class: HSSSSMSSSLSNSFN.
% 3.43/0.70 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.43/0.70 % Starting ho_unfolding_3 with 1500s (5) cores
% 3.43/0.70 % Starting post_as_ho5 with 300s (1) cores
% 3.43/0.70 % Starting sh4l with 300s (1) cores
% 3.43/0.70 % Starting ho_unfolding_2 with 300s (1) cores
% 3.43/0.70 % ho_unfolding_3 with pid 811988 completed with status 0
% 3.43/0.70 % Result found by ho_unfolding_3
% 3.43/0.70 % Preprocessing class: HSSSSMSSSLSNSFN.
% 3.43/0.70 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.43/0.70 % Starting ho_unfolding_3 with 1500s (5) cores
% 3.43/0.70 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 3.43/0.70 % No SInE strategy applied
% 3.43/0.70 % Search class: HGHSF-FFMS21-SSFFMFNN
% 3.43/0.70 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 3.43/0.70 % Starting SubtermCWHack with 136s (1) cores
% 3.43/0.70 % Starting ho_unfolding_3 with 151s (1) cores
% 3.43/0.70 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 3.43/0.70 % Starting lpo1_def_fix with 136s (1) cores
% 3.43/0.70 % Starting sh4l with 136s (1) cores
% 3.43/0.70 % ho_unfolding_3 with pid 811995 completed with status 0
% 3.43/0.70 % Result found by ho_unfolding_3
% 3.43/0.70 % Preprocessing class: HSSSSMSSSLSNSFN.
% 3.43/0.70 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.43/0.70 % Starting ho_unfolding_3 with 1500s (5) cores
% 3.43/0.70 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 3.43/0.70 % No SInE strategy applied
% 3.43/0.70 % Search class: HGHSF-FFMS21-SSFFMFNN
% 3.43/0.70 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 3.43/0.70 % Starting SubtermCWHack with 136s (1) cores
% 3.43/0.70 % Starting ho_unfolding_3 with 151s (1) cores
% 3.43/0.70 % Preprocessing time : 0.002 s
% 3.43/0.70 % Presaturation interreduction done
% 3.43/0.70
% 3.43/0.70 % Proof found!
% 3.43/0.70 % SZS status Theorem
% 3.43/0.70 % SZS output start CNFRefutation
% 3.43/0.70 thf(decl_23, type, in: $i > $i > $o).
% 3.43/0.70 thf(decl_24, type, powerset: $i > $i).
% 3.43/0.70 thf(decl_25, type, nonempty: $i > $o).
% 3.43/0.70 thf(decl_26, type, transitiveset: $i > $o).
% 3.43/0.70 thf(decl_27, type, stricttotalorderedByIn: $i > $o).
% 3.43/0.70 thf(decl_28, type, wellorderedByIn: $i > $o).
% 3.43/0.70 thf(decl_29, type, ordinal: $i > $o).
% 3.43/0.70 thf(decl_30, type, ordinalTransSet: $o).
% 3.43/0.70 thf(decl_31, type, epred1_1: $i > $o).
% 3.43/0.70 thf(decl_32, type, epred2_1: $i > $o).
% 3.43/0.70 thf(decl_33, type, esk1_1: $i > $i).
% 3.43/0.70 thf(decl_34, type, esk2_1: $i > $i).
% 3.43/0.70 thf(decl_35, type, esk3_2: $i > $i > $i).
% 3.43/0.70 thf(decl_36, type, esk4_0: $i).
% 3.43/0.70 thf(decl_37, type, esk5_0: $i).
% 3.43/0.70 thf(decl_38, type, esk6_0: $i).
% 3.43/0.70 thf(decl_39, type, esk7_0: $i).
% 3.43/0.70 thf(decl_40, type, esk8_1: $i > $i).
% 3.43/0.70 thf(decl_41, type, esk9_1: $i > $i).
% 3.43/0.70 thf(decl_42, type, esk10_1: $i > $i).
% 3.43/0.70 thf(decl_43, type, esk11_1: $i > $i).
% 3.43/0.70 thf(decl_44, type, esk12_1: $i > $i).
% 3.43/0.70 thf(decl_45, type, esk13_2: $i > $i > $i).
% 3.43/0.70 thf(wellorderedByIn, axiom, ((wellorderedByIn)=(^[X1:$i]:((((stricttotalorderedByIn @ X1))&(![X3:$i]:((((in @ X3 @ (powerset @ X1)))=>((((nonempty @ X3))=>(?[X2:$i]:((((in @ X2 @ X3))&(![X4:$i]:((((in @ X4 @ X3))=>(((((X2)=(X4)))|((in @ X2 @ X4))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.OBEHWuQTt3/E---3.1_811975.p', wellorderedByIn)).
% 3.43/0.70 thf(stricttotalorderedByIn, axiom, ((stricttotalorderedByIn)=(^[X1:$i]:(((((![X2:$i]:((((in @ X2 @ X1))=>(![X3:$i]:((((in @ X3 @ X1))=>(![X4:$i]:((((in @ X4 @ X1))=>((((((in @ X2 @ X3))&((in @ X3 @ X4))))=>((in @ X2 @ X4)))))))))))))&(![X3:$i]:((((in @ X3 @ X1))=>(![X4:$i]:((((in @ X4 @ X1))=>(((((((X3)=(X4)))|((in @ X3 @ X4))))|((in @ X4 @ X3))))))))))))&(![X3:$i]:((((in @ X3 @ X1))=>(~((in @ X3 @ X3)))))))))), file('/export/starexec/sandbox2/tmp/tmp.OBEHWuQTt3/E---3.1_811975.p', stricttotalorderedByIn)).
% 3.43/0.70 thf(ordinal, axiom, ((ordinal)=(^[X2:$i]:((((transitiveset @ X2))&((wellorderedByIn @ X2)))))), file('/export/starexec/sandbox2/tmp/tmp.OBEHWuQTt3/E---3.1_811975.p', ordinal)).
% 3.43/0.70 thf(ordinalTransIn, conjecture, ((ordinalTransSet)=>![X3:$i]:(((ordinal @ X3)=>![X2:$i, X1:$i, X5:$i]:(((in @ X2 @ X1)=>((in @ X1 @ X5)=>((in @ X5 @ X3)=>(in @ X2 @ X5)))))))), file('/export/starexec/sandbox2/tmp/tmp.OBEHWuQTt3/E---3.1_811975.p', ordinalTransIn)).
% 3.43/0.70 thf(ordinalTransSet, axiom, ((ordinalTransSet)<=>![X3:$i]:(((ordinal @ X3)=>![X2:$i, X1:$i]:(((in @ X1 @ X3)=>((in @ X2 @ X1)=>(in @ X2 @ X3))))))), file('/export/starexec/sandbox2/tmp/tmp.OBEHWuQTt3/E---3.1_811975.p', ordinalTransSet)).
% 3.43/0.70 thf(c_0_5, plain, ![X3:$i]:(((epred2_1 @ X3)<=>((transitiveset @ X3)&(((![X49:$i]:(((in @ X49 @ X3)=>![X50:$i]:(((in @ X50 @ X3)=>![X51:$i]:(((in @ X51 @ X3)=>(((in @ X49 @ X50)&(in @ X50 @ X51))=>(in @ X49 @ X51))))))))&![X52:$i]:(((in @ X52 @ X3)=>![X53:$i]:(((in @ X53 @ X3)=>(((X52)=(X53))|(in @ X52 @ X53)|(in @ X53 @ X52)))))))&![X54:$i]:(((in @ X54 @ X3)=>~(in @ X54 @ X54))))&![X55:$i]:(((in @ X55 @ (powerset @ X3))=>((nonempty @ X55)=>?[X56:$i]:(((in @ X56 @ X55)&![X57:$i]:(((in @ X57 @ X55)=>(((X56)=(X57))|(in @ X56 @ X57))))))))))))), introduced(definition)).
% 3.43/0.70 thf(c_0_6, plain, ![X37:$i]:(((epred1_1 @ X37)<=>(![X38:$i]:(((in @ X38 @ X37)=>![X39:$i]:(((in @ X39 @ X37)=>![X40:$i]:(((in @ X40 @ X37)=>(((in @ X38 @ X39)&(in @ X39 @ X40))=>(in @ X38 @ X40))))))))&![X41:$i]:(((in @ X41 @ X37)=>![X42:$i]:(((in @ X42 @ X37)=>(((X41)=(X42))|(in @ X41 @ X42)|(in @ X42 @ X41))))))))), introduced(definition)).
% 3.43/0.70 thf(c_0_7, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X13:$i]:((((in @ X13 @ Z0))=>(![X14:$i]:((((in @ X14 @ Z0))=>(![X15:$i]:((((in @ X15 @ Z0))=>((((((in @ X13 @ X14))&((in @ X14 @ X15))))=>((in @ X13 @ X15)))))))))))))&(![X16:$i]:((((in @ X16 @ Z0))=>(![X17:$i]:((((in @ X17 @ Z0))=>(((((((X16)=(X17)))|((in @ X16 @ X17))))|((in @ X17 @ X16))))))))))))&(![X18:$i]:((((in @ X18 @ Z0))=>(~((in @ X18 @ X18)))))))))&(![X3:$i]:((((in @ X3 @ (powerset @ Z0)))=>((((nonempty @ X3))=>(?[X2:$i]:((((in @ X2 @ X3))&(![X4:$i]:((((in @ X4 @ X3))=>(((((X2)=(X4)))|((in @ X2 @ X4))))))))))))))))))), inference(fof_simplification,[status(thm)],[wellorderedByIn])).
% 3.43/0.70 thf(c_0_8, plain, ((stricttotalorderedByIn)=(^[Z0:$i]:(((((![X2:$i]:((((in @ X2 @ Z0))=>(![X3:$i]:((((in @ X3 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>((((((in @ X2 @ X3))&((in @ X3 @ X4))))=>((in @ X2 @ X4)))))))))))))&(![X3:$i]:((((in @ X3 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>(((((((X3)=(X4)))|((in @ X3 @ X4))))|((in @ X4 @ X3))))))))))))&(![X3:$i]:((((in @ X3 @ Z0))=>(~((in @ X3 @ X3)))))))))), inference(fof_simplification,[status(thm)],[stricttotalorderedByIn])).
% 3.43/0.70 thf(c_0_9, plain, ![X3:$i]:(((epred2_1 @ X3)=>((transitiveset @ X3)&(((![X49:$i]:(((in @ X49 @ X3)=>![X50:$i]:(((in @ X50 @ X3)=>![X51:$i]:(((in @ X51 @ X3)=>(((in @ X49 @ X50)&(in @ X50 @ X51))=>(in @ X49 @ X51))))))))&![X52:$i]:(((in @ X52 @ X3)=>![X53:$i]:(((in @ X53 @ X3)=>(((X52)=(X53))|(in @ X52 @ X53)|(in @ X53 @ X52)))))))&![X54:$i]:(((in @ X54 @ X3)=>~(in @ X54 @ X54))))&![X55:$i]:(((in @ X55 @ (powerset @ X3))=>((nonempty @ X55)=>?[X56:$i]:(((in @ X56 @ X55)&![X57:$i]:(((in @ X57 @ X55)=>(((X56)=(X57))|(in @ X56 @ X57))))))))))))), inference(split_equiv,[status(thm)],[c_0_5])).
% 3.43/0.70 thf(c_0_10, plain, ![X37:$i]:(((![X38:$i]:(((in @ X38 @ X37)=>![X39:$i]:(((in @ X39 @ X37)=>![X40:$i]:(((in @ X40 @ X37)=>(((in @ X38 @ X39)&(in @ X39 @ X40))=>(in @ X38 @ X40))))))))&![X41:$i]:(((in @ X41 @ X37)=>![X42:$i]:(((in @ X42 @ X37)=>(((X41)=(X42))|(in @ X41 @ X42)|(in @ X42 @ X41)))))))=>(epred1_1 @ X37))), inference(split_equiv,[status(thm)],[c_0_6])).
% 3.43/0.70 thf(c_0_11, plain, ((ordinal)=(^[Z0:$i]:((((transitiveset @ Z0))&(((((((((![X19:$i]:((((in @ X19 @ Z0))=>(![X20:$i]:((((in @ X20 @ Z0))=>(![X21:$i]:((((in @ X21 @ Z0))=>((((((in @ X19 @ X20))&((in @ X20 @ X21))))=>((in @ X19 @ X21)))))))))))))&(![X22:$i]:((((in @ X22 @ Z0))=>(![X23:$i]:((((in @ X23 @ Z0))=>(((((((X22)=(X23)))|((in @ X22 @ X23))))|((in @ X23 @ X22))))))))))))&(![X24:$i]:((((in @ X24 @ Z0))=>(~((in @ X24 @ X24)))))))))&(![X25:$i]:((((in @ X25 @ (powerset @ Z0)))=>((((nonempty @ X25))=>(?[X26:$i]:((((in @ X26 @ X25))&(![X27:$i]:((((in @ X27 @ X25))=>(((((X26)=(X27)))|((in @ X26 @ X27)))))))))))))))))))))), inference(fof_simplification,[status(thm)],[ordinal])).
% 3.43/0.70 thf(c_0_12, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X13:$i]:((((in @ X13 @ Z0))=>(![X14:$i]:((((in @ X14 @ Z0))=>(![X15:$i]:((((in @ X15 @ Z0))=>((((((in @ X13 @ X14))&((in @ X14 @ X15))))=>((in @ X13 @ X15)))))))))))))&(![X16:$i]:((((in @ X16 @ Z0))=>(![X17:$i]:((((in @ X17 @ Z0))=>(((((((X16)=(X17)))|((in @ X16 @ X17))))|((in @ X17 @ X16))))))))))))&(![X18:$i]:((((in @ X18 @ Z0))=>(~((in @ X18 @ X18)))))))))&(![X3:$i]:((((in @ X3 @ (powerset @ Z0)))=>((((nonempty @ X3))=>(?[X2:$i]:((((in @ X2 @ X3))&(![X4:$i]:((((in @ X4 @ X3))=>(((((X2)=(X4)))|((in @ X2 @ X4))))))))))))))))))), inference(apply_def,[status(thm)],[c_0_7, c_0_8])).
% 3.43/0.70 thf(c_0_13, plain, ![X75:$i, X76:$i, X77:$i, X78:$i, X79:$i, X80:$i, X81:$i, X82:$i, X84:$i]:((((transitiveset @ X75)|~(epred2_1 @ X75))&((((~(in @ X76 @ X75)|(~(in @ X77 @ X75)|(~(in @ X78 @ X75)|(~(in @ X76 @ X77)|~(in @ X77 @ X78)|(in @ X76 @ X78))))|~(epred2_1 @ X75))&(~(in @ X79 @ X75)|(~(in @ X80 @ X75)|(((X79)=(X80))|(in @ X79 @ X80)|(in @ X80 @ X79)))|~(epred2_1 @ X75)))&(~(in @ X81 @ X75)|~(in @ X81 @ X81)|~(epred2_1 @ X75)))&(((in @ (esk13_2 @ X75 @ X82) @ X82)|~(nonempty @ X82)|~(in @ X82 @ (powerset @ X75))|~(epred2_1 @ X75))&(~(in @ X84 @ X82)|(((esk13_2 @ X75 @ X82)=(X84))|(in @ (esk13_2 @ X75 @ X82) @ X84))|~(nonempty @ X82)|~(in @ X82 @ (powerset @ X75))|~(epred2_1 @ X75)))))), 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_9])])])])])])).
% 3.43/0.70 thf(c_0_14, plain, ![X69:$i]:(((((in @ (esk11_1 @ X69) @ X69)|(in @ (esk8_1 @ X69) @ X69)|(epred1_1 @ X69))&(((in @ (esk12_1 @ X69) @ X69)|(in @ (esk8_1 @ X69) @ X69)|(epred1_1 @ X69))&(((((esk11_1 @ X69)!=(esk12_1 @ X69))|(in @ (esk8_1 @ X69) @ X69)|(epred1_1 @ X69))&(~(in @ (esk11_1 @ X69) @ (esk12_1 @ X69))|(in @ (esk8_1 @ X69) @ X69)|(epred1_1 @ X69)))&(~(in @ (esk12_1 @ X69) @ (esk11_1 @ X69))|(in @ (esk8_1 @ X69) @ X69)|(epred1_1 @ X69)))))&((((in @ (esk11_1 @ X69) @ X69)|(in @ (esk9_1 @ X69) @ X69)|(epred1_1 @ X69))&(((in @ (esk12_1 @ X69) @ X69)|(in @ (esk9_1 @ X69) @ X69)|(epred1_1 @ X69))&(((((esk11_1 @ X69)!=(esk12_1 @ X69))|(in @ (esk9_1 @ X69) @ X69)|(epred1_1 @ X69))&(~(in @ (esk11_1 @ X69) @ (esk12_1 @ X69))|(in @ (esk9_1 @ X69) @ X69)|(epred1_1 @ X69)))&(~(in @ (esk12_1 @ X69) @ (esk11_1 @ X69))|(in @ (esk9_1 @ X69) @ X69)|(epred1_1 @ X69)))))&((((in @ (esk11_1 @ X69) @ X69)|(in @ (esk10_1 @ X69) @ X69)|(epred1_1 @ X69))&(((in @ (esk12_1 @ X69) @ X69)|(in @ (esk10_1 @ X69) @ X69)|(epred1_1 @ X69))&(((((esk11_1 @ X69)!=(esk12_1 @ X69))|(in @ (esk10_1 @ X69) @ X69)|(epred1_1 @ X69))&(~(in @ (esk11_1 @ X69) @ (esk12_1 @ X69))|(in @ (esk10_1 @ X69) @ X69)|(epred1_1 @ X69)))&(~(in @ (esk12_1 @ X69) @ (esk11_1 @ X69))|(in @ (esk10_1 @ X69) @ X69)|(epred1_1 @ X69)))))&(((((in @ (esk11_1 @ X69) @ X69)|(in @ (esk8_1 @ X69) @ (esk9_1 @ X69))|(epred1_1 @ X69))&(((in @ (esk12_1 @ X69) @ X69)|(in @ (esk8_1 @ X69) @ (esk9_1 @ X69))|(epred1_1 @ X69))&(((((esk11_1 @ X69)!=(esk12_1 @ X69))|(in @ (esk8_1 @ X69) @ (esk9_1 @ X69))|(epred1_1 @ X69))&(~(in @ (esk11_1 @ X69) @ (esk12_1 @ X69))|(in @ (esk8_1 @ X69) @ (esk9_1 @ X69))|(epred1_1 @ X69)))&(~(in @ (esk12_1 @ X69) @ (esk11_1 @ X69))|(in @ (esk8_1 @ X69) @ (esk9_1 @ X69))|(epred1_1 @ X69)))))&(((in @ (esk11_1 @ X69) @ X69)|(in @ (esk9_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69))&(((in @ (esk12_1 @ X69) @ X69)|(in @ (esk9_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69))&(((((esk11_1 @ X69)!=(esk12_1 @ X69))|(in @ (esk9_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69))&(~(in @ (esk11_1 @ X69) @ (esk12_1 @ X69))|(in @ (esk9_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69)))&(~(in @ (esk12_1 @ X69) @ (esk11_1 @ X69))|(in @ (esk9_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69))))))&(((in @ (esk11_1 @ X69) @ X69)|~(in @ (esk8_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69))&(((in @ (esk12_1 @ X69) @ X69)|~(in @ (esk8_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69))&(((((esk11_1 @ X69)!=(esk12_1 @ X69))|~(in @ (esk8_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69))&(~(in @ (esk11_1 @ X69) @ (esk12_1 @ X69))|~(in @ (esk8_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69)))&(~(in @ (esk12_1 @ X69) @ (esk11_1 @ X69))|~(in @ (esk8_1 @ X69) @ (esk10_1 @ X69))|(epred1_1 @ X69)))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])])])).
% 3.43/0.70 thf(c_0_15, plain, ((ordinal)=(^[Z0:$i]:((((transitiveset @ Z0))&(((((((((![X19:$i]:((((in @ X19 @ Z0))=>(![X20:$i]:((((in @ X20 @ Z0))=>(![X21:$i]:((((in @ X21 @ Z0))=>((((((in @ X19 @ X20))&((in @ X20 @ X21))))=>((in @ X19 @ X21)))))))))))))&(![X22:$i]:((((in @ X22 @ Z0))=>(![X23:$i]:((((in @ X23 @ Z0))=>(((((((X22)=(X23)))|((in @ X22 @ X23))))|((in @ X23 @ X22))))))))))))&(![X24:$i]:((((in @ X24 @ Z0))=>(~((in @ X24 @ X24)))))))))&(![X25:$i]:((((in @ X25 @ (powerset @ Z0)))=>((((nonempty @ X25))=>(?[X26:$i]:((((in @ X26 @ X25))&(![X27:$i]:((((in @ X27 @ X25))=>(((((X26)=(X27)))|((in @ X26 @ X27)))))))))))))))))))))), inference(apply_def,[status(thm)],[c_0_11, c_0_12])).
% 3.43/0.70 thf(c_0_16, plain, ![X1:$i, X4:$i, X3:$i, X2:$i]:(((in @ X1 @ X4)|~((in @ X1 @ X2))|~((in @ X3 @ X2))|~((in @ X4 @ X2))|~((in @ X1 @ X3))|~((in @ X3 @ X4))|~((epred2_1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.43/0.70 thf(c_0_17, plain, ![X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(in @ (esk10_1 @ X1) @ X1)|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_18, negated_conjecture, ~(((ordinalTransSet)=>![X3:$i]:(((ordinal @ X3)=>![X2:$i, X1:$i, X5:$i]:(((in @ X2 @ X1)=>((in @ X1 @ X5)=>((in @ X5 @ X3)=>(in @ X2 @ X5))))))))), inference(assume_negation,[status(cth)],[ordinalTransIn])).
% 3.43/0.70 thf(c_0_19, axiom, ((ordinalTransSet)=(![X3:$i]:(((((((transitiveset @ X3))&(((((((((![X28:$i]:((((in @ X28 @ X3))=>(![X29:$i]:((((in @ X29 @ X3))=>(![X30:$i]:((((in @ X30 @ X3))=>((((((in @ X28 @ X29))&((in @ X29 @ X30))))=>((in @ X28 @ X30)))))))))))))&(![X31:$i]:((((in @ X31 @ X3))=>(![X32:$i]:((((in @ X32 @ X3))=>(((((((X31)=(X32)))|((in @ X31 @ X32))))|((in @ X32 @ X31))))))))))))&(![X33:$i]:((((in @ X33 @ X3))=>(~((in @ X33 @ X33)))))))))&(![X34:$i]:((((in @ X34 @ (powerset @ X3)))=>((((nonempty @ X34))=>(?[X35:$i]:((((in @ X35 @ X34))&(![X36:$i]:((((in @ X36 @ X34))=>(((((X35)=(X36)))|((in @ X35 @ X36)))))))))))))))))))))=>(![X2:$i, X1:$i]:((((in @ X1 @ X3))=>((((in @ X2 @ X1))=>((in @ X2 @ X3))))))))))), inference(apply_def,[status(thm)],[ordinalTransSet, c_0_15])).
% 3.43/0.70 thf(c_0_20, plain, ![X3:$i, X2:$i, X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(in @ X2 @ (esk10_1 @ X1))|(epred1_1 @ X1)|~((in @ X3 @ (esk10_1 @ X1)))|~((in @ X3 @ X1))|~((in @ X2 @ X3))|~((in @ X2 @ X1))|~((epred2_1 @ X1)))), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 3.43/0.70 thf(c_0_21, plain, ![X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(in @ (esk9_1 @ X1) @ (esk10_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_22, plain, ![X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(in @ (esk9_1 @ X1) @ X1)|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_23, negated_conjecture, ~((![X37:$i]:((((transitiveset @ X37)&(((epred1_1 @ X37)&![X43:$i]:(((in @ X43 @ X37)=>~(in @ X43 @ X43))))&![X44:$i]:(((in @ X44 @ (powerset @ X37))=>((nonempty @ X44)=>?[X45:$i]:(((in @ X45 @ X44)&![X46:$i]:(((in @ X46 @ X44)=>(((X45)=(X46))|(in @ X45 @ X46)))))))))))=>![X47:$i, X48:$i]:(((in @ X48 @ X37)=>((in @ X47 @ X48)=>(in @ X47 @ X37))))))=>![X3:$i]:(((epred2_1 @ X3)=>![X2:$i, X1:$i, X5:$i]:(((in @ X2 @ X1)=>((in @ X1 @ X5)=>((in @ X5 @ X3)=>(in @ X2 @ X5))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_18, c_0_15]), c_0_19])]), c_0_6]), c_0_5])).
% 3.43/0.70 thf(c_0_24, plain, ![X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(in @ (esk10_1 @ X1) @ X1)|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_25, plain, ![X1:$i, X2:$i]:(((in @ X1 @ (esk10_1 @ X2))|(in @ (esk11_1 @ X2) @ X2)|(epred1_1 @ X2)|~((in @ X1 @ (esk9_1 @ X2)))|~((in @ X1 @ X2))|~((epred2_1 @ X2)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_22])).
% 3.43/0.70 thf(c_0_26, plain, ![X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(in @ (esk8_1 @ X1) @ (esk9_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_27, plain, ![X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(in @ (esk8_1 @ X1) @ X1)|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_28, plain, ![X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk8_1 @ X1) @ (esk10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_29, negated_conjecture, ![X58:$i, X61:$i, X63:$i, X64:$i]:((((((in @ (esk2_1 @ X58) @ (powerset @ X58))|((in @ (esk1_1 @ X58) @ X58)|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&(((nonempty @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ X58)|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&(((in @ (esk3_2 @ X58 @ X61) @ (esk2_1 @ X58))|~(in @ X61 @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ X58)|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&((((X61)!=(esk3_2 @ X58 @ X61))|~(in @ X61 @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ X58)|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&(~(in @ X61 @ (esk3_2 @ X58 @ X61))|~(in @ X61 @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ X58)|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))))))&(((in @ (esk2_1 @ X58) @ (powerset @ X58))|((in @ (esk1_1 @ X58) @ (esk1_1 @ X58))|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&(((nonempty @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ (esk1_1 @ X58))|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&(((in @ (esk3_2 @ X58 @ X61) @ (esk2_1 @ X58))|~(in @ X61 @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ (esk1_1 @ X58))|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&((((X61)!=(esk3_2 @ X58 @ X61))|~(in @ X61 @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ (esk1_1 @ X58))|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58))))&(~(in @ X61 @ (esk3_2 @ X58 @ X61))|~(in @ X61 @ (esk2_1 @ X58))|((in @ (esk1_1 @ X58) @ (esk1_1 @ X58))|~(epred1_1 @ X58))|~(transitiveset @ X58)|(~(in @ X64 @ X58)|(~(in @ X63 @ X64)|(in @ X63 @ X58)))))))))&((epred2_1 @ esk4_0)&((in @ esk5_0 @ esk6_0)&((in @ esk6_0 @ esk7_0)&((in @ esk7_0 @ esk4_0)&~(in @ esk5_0 @ esk7_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_23])])])])])])).
% 3.43/0.70 thf(c_0_30, plain, ![X3:$i, X2:$i, X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(in @ X2 @ (esk10_1 @ X1))|(epred1_1 @ X1)|~((in @ X3 @ (esk10_1 @ X1)))|~((in @ X3 @ X1))|~((in @ X2 @ X3))|~((in @ X2 @ X1))|~((epred2_1 @ X1)))), inference(spm,[status(thm)],[c_0_16, c_0_24])).
% 3.43/0.70 thf(c_0_31, plain, ![X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(in @ (esk9_1 @ X1) @ (esk10_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_32, plain, ![X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(in @ (esk9_1 @ X1) @ X1)|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_33, plain, ![X1:$i]:(((in @ (esk11_1 @ X1) @ X1)|(epred1_1 @ X1)|~((epred2_1 @ X1)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_26]), c_0_27]), c_0_28])).
% 3.43/0.70 thf(c_0_34, negated_conjecture, (epred2_1 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_35, plain, ![X1:$i, X2:$i]:(((in @ X1 @ (esk10_1 @ X2))|(in @ (esk12_1 @ X2) @ X2)|(epred1_1 @ X2)|~((in @ X1 @ (esk9_1 @ X2)))|~((in @ X1 @ X2))|~((epred2_1 @ X2)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_32])).
% 3.43/0.70 thf(c_0_36, plain, ![X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(in @ (esk8_1 @ X1) @ (esk9_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_37, plain, ![X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(in @ (esk8_1 @ X1) @ X1)|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_38, plain, ![X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk8_1 @ X1) @ (esk10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_39, plain, ![X1:$i, X3:$i, X2:$i]:((((X1)=(X3))|(in @ X1 @ X3)|(in @ X3 @ X1)|~((in @ X1 @ X2))|~((in @ X3 @ X2))|~((epred2_1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.43/0.70 thf(c_0_40, negated_conjecture, ((in @ (esk11_1 @ esk4_0) @ esk4_0)|(epred1_1 @ esk4_0)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 3.43/0.70 thf(c_0_41, plain, ![X1:$i]:(((in @ (esk12_1 @ X1) @ X1)|(epred1_1 @ X1)|~((epred2_1 @ X1)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_37]), c_0_38])).
% 3.43/0.70 thf(c_0_42, plain, ![X1:$i]:((((X1)=(esk11_1 @ esk4_0))|(in @ X1 @ (esk11_1 @ esk4_0))|(in @ (esk11_1 @ esk4_0) @ X1)|(epred1_1 @ esk4_0)|~((in @ X1 @ esk4_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_34])])).
% 3.43/0.70 thf(c_0_43, negated_conjecture, ((in @ (esk12_1 @ esk4_0) @ esk4_0)|(epred1_1 @ esk4_0)), inference(spm,[status(thm)],[c_0_41, c_0_34])).
% 3.43/0.70 thf(c_0_44, plain, ![X1:$i]:(((in @ (esk10_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk12_1 @ X1) @ (esk11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_45, plain, (((esk12_1 @ esk4_0)=(esk11_1 @ esk4_0))|(in @ (esk11_1 @ esk4_0) @ (esk12_1 @ esk4_0))|(in @ (esk12_1 @ esk4_0) @ (esk11_1 @ esk4_0))|(epred1_1 @ esk4_0)), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 3.43/0.70 thf(c_0_46, plain, ![X1:$i]:(((in @ (esk10_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk11_1 @ X1) @ (esk12_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_47, plain, ![X1:$i]:(((in @ (esk10_1 @ X1) @ X1)|(epred1_1 @ X1)|((esk11_1 @ X1)!=(esk12_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_48, plain, ((in @ (esk10_1 @ esk4_0) @ esk4_0)|(epred1_1 @ esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_45]), c_0_46]), c_0_47])).
% 3.43/0.70 thf(c_0_49, plain, ![X1:$i]:(((in @ (esk9_1 @ X1) @ (esk10_1 @ X1))|(epred1_1 @ X1)|~((in @ (esk12_1 @ X1) @ (esk11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_50, plain, ![X1:$i]:(((in @ (esk9_1 @ X1) @ (esk10_1 @ X1))|(epred1_1 @ X1)|~((in @ (esk11_1 @ X1) @ (esk12_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_51, plain, ![X1:$i]:(((in @ (esk9_1 @ X1) @ (esk10_1 @ X1))|(epred1_1 @ X1)|((esk11_1 @ X1)!=(esk12_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_52, plain, ![X1:$i]:(((in @ (esk9_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk12_1 @ X1) @ (esk11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_53, plain, ![X1:$i]:(((in @ (esk9_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk11_1 @ X1) @ (esk12_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_54, plain, ![X1:$i]:(((in @ (esk9_1 @ X1) @ X1)|(epred1_1 @ X1)|((esk11_1 @ X1)!=(esk12_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_55, plain, ![X1:$i, X2:$i]:(((in @ X1 @ (esk10_1 @ esk4_0))|(epred1_1 @ esk4_0)|~((in @ X2 @ (esk10_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_48]), c_0_34])])).
% 3.43/0.70 thf(c_0_56, plain, ((in @ (esk9_1 @ esk4_0) @ (esk10_1 @ esk4_0))|(epred1_1 @ esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_45]), c_0_50]), c_0_51])).
% 3.43/0.70 thf(c_0_57, plain, ((in @ (esk9_1 @ esk4_0) @ esk4_0)|(epred1_1 @ esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_45]), c_0_53]), c_0_54])).
% 3.43/0.70 thf(c_0_58, plain, ![X1:$i]:(((in @ (esk8_1 @ X1) @ (esk9_1 @ X1))|(epred1_1 @ X1)|~((in @ (esk12_1 @ X1) @ (esk11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_59, plain, ![X1:$i]:(((in @ (esk8_1 @ X1) @ (esk9_1 @ X1))|(epred1_1 @ X1)|~((in @ (esk11_1 @ X1) @ (esk12_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_60, plain, ![X1:$i]:(((in @ (esk8_1 @ X1) @ (esk9_1 @ X1))|(epred1_1 @ X1)|((esk11_1 @ X1)!=(esk12_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_61, plain, ![X1:$i]:(((in @ (esk8_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk12_1 @ X1) @ (esk11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_62, plain, ![X1:$i]:(((in @ (esk8_1 @ X1) @ X1)|(epred1_1 @ X1)|~((in @ (esk11_1 @ X1) @ (esk12_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_63, plain, ![X1:$i]:(((in @ (esk8_1 @ X1) @ X1)|(epred1_1 @ X1)|((esk11_1 @ X1)!=(esk12_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_64, plain, ![X1:$i]:(((in @ X1 @ (esk10_1 @ esk4_0))|(epred1_1 @ esk4_0)|~((in @ X1 @ (esk9_1 @ esk4_0)))|~((in @ X1 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_57])).
% 3.43/0.70 thf(c_0_65, plain, ((in @ (esk8_1 @ esk4_0) @ (esk9_1 @ esk4_0))|(epred1_1 @ esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_45]), c_0_59]), c_0_60])).
% 3.43/0.70 thf(c_0_66, plain, ((in @ (esk8_1 @ esk4_0) @ esk4_0)|(epred1_1 @ esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_45]), c_0_62]), c_0_63])).
% 3.43/0.70 thf(c_0_67, negated_conjecture, ![X1:$i, X3:$i, X2:$i]:(((in @ (esk2_1 @ X1) @ (powerset @ X1))|(in @ (esk1_1 @ X1) @ X1)|(in @ X3 @ X1)|~((epred1_1 @ X1))|~((transitiveset @ X1))|~((in @ X2 @ X1))|~((in @ X3 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_68, negated_conjecture, (in @ esk6_0 @ esk7_0), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_69, plain, ![X1:$i]:(((transitiveset @ X1)|~((epred2_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.43/0.70 thf(c_0_70, plain, ![X1:$i]:(((epred1_1 @ X1)|~((in @ (esk12_1 @ X1) @ (esk11_1 @ X1)))|~((in @ (esk8_1 @ X1) @ (esk10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_71, plain, ((in @ (esk8_1 @ esk4_0) @ (esk10_1 @ esk4_0))|(epred1_1 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_65]), c_0_66])).
% 3.43/0.70 thf(c_0_72, plain, ![X1:$i]:(((epred1_1 @ X1)|~((in @ (esk11_1 @ X1) @ (esk12_1 @ X1)))|~((in @ (esk8_1 @ X1) @ (esk10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_73, plain, ![X1:$i]:(((epred1_1 @ X1)|((esk11_1 @ X1)!=(esk12_1 @ X1))|~((in @ (esk8_1 @ X1) @ (esk10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.43/0.70 thf(c_0_74, negated_conjecture, ![X1:$i]:(((in @ (esk2_1 @ X1) @ (powerset @ X1))|(in @ (esk1_1 @ X1) @ X1)|(in @ esk6_0 @ X1)|~((in @ esk7_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_67, c_0_68])).
% 3.43/0.70 thf(c_0_75, negated_conjecture, (in @ esk7_0 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_76, plain, (transitiveset @ esk4_0), inference(spm,[status(thm)],[c_0_69, c_0_34])).
% 3.43/0.70 thf(c_0_77, plain, ((epred1_1 @ esk4_0)|~((in @ (esk12_1 @ esk4_0) @ (esk11_1 @ esk4_0)))), inference(spm,[status(thm)],[c_0_70, c_0_71])).
% 3.43/0.70 thf(c_0_78, plain, ((epred1_1 @ esk4_0)|~((in @ (esk11_1 @ esk4_0) @ (esk12_1 @ esk4_0)))), inference(spm,[status(thm)],[c_0_72, c_0_71])).
% 3.43/0.70 thf(c_0_79, plain, ((epred1_1 @ esk4_0)|((esk12_1 @ esk4_0)!=(esk11_1 @ esk4_0))), inference(spm,[status(thm)],[c_0_73, c_0_71])).
% 3.43/0.70 thf(c_0_80, negated_conjecture, ![X1:$i, X3:$i, X2:$i]:(((nonempty @ (esk2_1 @ X1))|(in @ (esk1_1 @ X1) @ X1)|(in @ X3 @ X1)|~((epred1_1 @ X1))|~((transitiveset @ X1))|~((in @ X2 @ X1))|~((in @ X3 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_81, negated_conjecture, ![X1:$i, X2:$i, X4:$i, X3:$i]:(((in @ (esk3_2 @ X1 @ X2) @ (esk2_1 @ X1))|(in @ (esk1_1 @ X1) @ X1)|(in @ X4 @ X1)|~((in @ X2 @ (esk2_1 @ X1)))|~((epred1_1 @ X1))|~((transitiveset @ X1))|~((in @ X3 @ X1))|~((in @ X4 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_82, plain, ![X2:$i, X1:$i]:(((in @ (esk13_2 @ X1 @ X2) @ X2)|~((nonempty @ X2))|~((in @ X2 @ (powerset @ X1)))|~((epred2_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.43/0.70 thf(c_0_83, negated_conjecture, ((in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|~((epred1_1 @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_75]), c_0_76])])).
% 3.43/0.70 thf(c_0_84, plain, (epred1_1 @ esk4_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_45]), c_0_78]), c_0_79])).
% 3.43/0.70 thf(c_0_85, negated_conjecture, ![X1:$i]:(((in @ (esk1_1 @ X1) @ X1)|(in @ esk6_0 @ X1)|(nonempty @ (esk2_1 @ X1))|~((in @ esk7_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_80, c_0_68])).
% 3.43/0.70 thf(c_0_86, plain, ![X1:$i, X4:$i, X3:$i, X2:$i]:(((in @ (esk3_2 @ X1 @ (esk13_2 @ X2 @ (esk2_1 @ X1))) @ (esk2_1 @ X1))|(in @ (esk1_1 @ X1) @ X1)|(in @ X3 @ X1)|~((in @ (esk2_1 @ X1) @ (powerset @ X2)))|~((in @ X3 @ X4))|~((in @ X4 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1))|~((epred2_1 @ X2)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_82]), c_0_80])).
% 3.43/0.70 thf(c_0_87, negated_conjecture, ((in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83, c_0_84])])).
% 3.43/0.70 thf(c_0_88, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ esk4_0)|(nonempty @ (esk2_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)|~((epred1_1 @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_75]), c_0_76])])).
% 3.43/0.70 thf(c_0_89, negated_conjecture, ![X1:$i, X2:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_87]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_90, negated_conjecture, ![X1:$i, X3:$i, X2:$i]:(((in @ (esk2_1 @ X1) @ (powerset @ X1))|(in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ X3 @ X1)|~((epred1_1 @ X1))|~((transitiveset @ X1))|~((in @ X2 @ X1))|~((in @ X3 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_91, plain, ![X1:$i, X2:$i, X3:$i]:((((esk13_2 @ X3 @ X2)=(X1))|(in @ (esk13_2 @ X3 @ X2) @ X1)|~((in @ X1 @ X2))|~((nonempty @ X2))|~((in @ X2 @ (powerset @ X3)))|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.43/0.70 thf(c_0_92, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|(nonempty @ (esk2_1 @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_84])])).
% 3.43/0.70 thf(c_0_93, negated_conjecture, ![X1:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk7_0)))), inference(spm,[status(thm)],[c_0_89, c_0_75])).
% 3.43/0.70 thf(c_0_94, negated_conjecture, ![X1:$i, X2:$i, X4:$i, X3:$i]:(((in @ (esk1_1 @ X2) @ X2)|(in @ X4 @ X2)|((X1)!=(esk3_2 @ X2 @ X1))|~((in @ X1 @ (esk2_1 @ X2)))|~((epred1_1 @ X2))|~((transitiveset @ X2))|~((in @ X3 @ X2))|~((in @ X4 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_95, negated_conjecture, ![X1:$i]:(((in @ (esk2_1 @ X1) @ (powerset @ X1))|(in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ esk6_0 @ X1)|~((in @ esk7_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_90, c_0_68])).
% 3.43/0.70 thf(c_0_96, plain, ![X1:$i]:((((esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))=(X1))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ X1)|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|~((in @ X1 @ (esk2_1 @ esk4_0))))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_87]), c_0_34])]), c_0_92])).
% 3.43/0.70 thf(c_0_97, negated_conjecture, ((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_93, c_0_68])).
% 3.43/0.70 thf(c_0_98, plain, ![X2:$i, X1:$i, X4:$i, X3:$i]:(((in @ (esk1_1 @ X1) @ X1)|(in @ X2 @ X1)|((esk3_2 @ X1 @ (esk13_2 @ X3 @ (esk2_1 @ X1)))!=(esk13_2 @ X3 @ (esk2_1 @ X1)))|~((in @ (esk2_1 @ X1) @ (powerset @ X3)))|~((in @ X2 @ X4))|~((in @ X4 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_82]), c_0_80])).
% 3.43/0.70 thf(c_0_99, negated_conjecture, ![X1:$i, X3:$i, X2:$i]:(((nonempty @ (esk2_1 @ X1))|(in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ X3 @ X1)|~((epred1_1 @ X1))|~((transitiveset @ X1))|~((in @ X2 @ X1))|~((in @ X3 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_100, negated_conjecture, ![X1:$i, X2:$i, X4:$i, X3:$i]:(((in @ (esk3_2 @ X1 @ X2) @ (esk2_1 @ X1))|(in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ X4 @ X1)|~((in @ X2 @ (esk2_1 @ X1)))|~((epred1_1 @ X1))|~((transitiveset @ X1))|~((in @ X3 @ X1))|~((in @ X4 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_101, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0))|(in @ esk6_0 @ esk4_0)|~((epred1_1 @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95, c_0_75]), c_0_76])])).
% 3.43/0.70 thf(c_0_102, negated_conjecture, ![X1:$i, X2:$i, X4:$i, X3:$i]:(((in @ (esk1_1 @ X2) @ X2)|(in @ X4 @ X2)|~((in @ X1 @ (esk3_2 @ X2 @ X1)))|~((in @ X1 @ (esk2_1 @ X2)))|~((epred1_1 @ X2))|~((transitiveset @ X2))|~((in @ X3 @ X2))|~((in @ X4 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_103, plain, (((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_96, c_0_97])).
% 3.43/0.70 thf(c_0_104, negated_conjecture, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))!=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_87]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_105, negated_conjecture, ![X1:$i]:(((in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ esk6_0 @ X1)|(nonempty @ (esk2_1 @ X1))|~((in @ esk7_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_99, c_0_68])).
% 3.43/0.70 thf(c_0_106, plain, ![X1:$i, X4:$i, X3:$i, X2:$i]:(((in @ (esk3_2 @ X1 @ (esk13_2 @ X2 @ (esk2_1 @ X1))) @ (esk2_1 @ X1))|(in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ X3 @ X1)|~((in @ (esk2_1 @ X1) @ (powerset @ X2)))|~((in @ X3 @ X4))|~((in @ X4 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1))|~((epred2_1 @ X2)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_82]), c_0_99])).
% 3.43/0.70 thf(c_0_107, negated_conjecture, ((in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_101, c_0_84])])).
% 3.43/0.70 thf(c_0_108, negated_conjecture, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_103]), c_0_76]), c_0_84])]), c_0_104])).
% 3.43/0.70 thf(c_0_109, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(nonempty @ (esk2_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)|~((epred1_1 @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_75]), c_0_76])])).
% 3.43/0.70 thf(c_0_110, negated_conjecture, ![X1:$i, X2:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_107]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_111, plain, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_82]), c_0_34])]), c_0_92]), c_0_87])).
% 3.43/0.70 thf(c_0_112, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)|(nonempty @ (esk2_1 @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_109, c_0_84])])).
% 3.43/0.70 thf(c_0_113, negated_conjecture, ![X1:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk7_0)))), inference(spm,[status(thm)],[c_0_110, c_0_75])).
% 3.43/0.70 thf(c_0_114, negated_conjecture, ![X1:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk7_0)))), inference(spm,[status(thm)],[c_0_111, c_0_75])).
% 3.43/0.70 thf(c_0_115, plain, ![X1:$i]:((((esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))=(X1))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ X1)|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)|~((in @ X1 @ (esk2_1 @ esk4_0))))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_107]), c_0_34])]), c_0_112])).
% 3.43/0.70 thf(c_0_116, negated_conjecture, ((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_113, c_0_68])).
% 3.43/0.70 thf(c_0_117, plain, ![X1:$i, X2:$i]:((~((in @ X1 @ X2))|~((in @ X1 @ X1))|~((epred2_1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.43/0.70 thf(c_0_118, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk6_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_114, c_0_68])).
% 3.43/0.70 thf(c_0_119, negated_conjecture, ![X1:$i, X2:$i, X4:$i, X3:$i]:(((in @ (esk1_1 @ X2) @ (esk1_1 @ X2))|(in @ X4 @ X2)|~((in @ X1 @ (esk3_2 @ X2 @ X1)))|~((in @ X1 @ (esk2_1 @ X2)))|~((epred1_1 @ X2))|~((transitiveset @ X2))|~((in @ X3 @ X2))|~((in @ X4 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_120, plain, (((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_115, c_0_116])).
% 3.43/0.70 thf(c_0_121, plain, ((in @ esk6_0 @ esk4_0)|~((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_117, c_0_118]), c_0_34])])).
% 3.43/0.70 thf(c_0_122, negated_conjecture, ![X1:$i, X2:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_120]), c_0_76]), c_0_84])]), c_0_121])).
% 3.43/0.70 thf(c_0_123, plain, ![X1:$i, X2:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0)))|~((nonempty @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_82]), c_0_34])])).
% 3.43/0.70 thf(c_0_124, negated_conjecture, ![X1:$i, X2:$i, X4:$i, X3:$i]:(((in @ (esk1_1 @ X2) @ (esk1_1 @ X2))|(in @ X4 @ X2)|((X1)!=(esk3_2 @ X2 @ X1))|~((in @ X1 @ (esk2_1 @ X2)))|~((epred1_1 @ X2))|~((transitiveset @ X2))|~((in @ X3 @ X2))|~((in @ X4 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_125, negated_conjecture, ![X1:$i, X2:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_112]), c_0_107]), c_0_121])).
% 3.43/0.70 thf(c_0_126, plain, ![X2:$i, X1:$i, X4:$i, X3:$i]:(((in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ X2 @ X1)|((esk3_2 @ X1 @ (esk13_2 @ X3 @ (esk2_1 @ X1)))!=(esk13_2 @ X3 @ (esk2_1 @ X1)))|~((in @ (esk2_1 @ X1) @ (powerset @ X3)))|~((in @ X2 @ X4))|~((in @ X4 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_82]), c_0_99])).
% 3.43/0.70 thf(c_0_127, negated_conjecture, ![X1:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk7_0)))), inference(spm,[status(thm)],[c_0_125, c_0_75])).
% 3.43/0.70 thf(c_0_128, negated_conjecture, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))!=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_107]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_129, negated_conjecture, (((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk6_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_127, c_0_68])).
% 3.43/0.70 thf(c_0_130, negated_conjecture, ![X1:$i, X2:$i]:(((in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_128, c_0_129]), c_0_121])).
% 3.43/0.70 thf(c_0_131, negated_conjecture, (in @ esk5_0 @ esk6_0), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_132, negated_conjecture, ![X1:$i]:(((in @ esk6_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk7_0)))), inference(spm,[status(thm)],[c_0_130, c_0_75])).
% 3.43/0.70 thf(c_0_133, negated_conjecture, ![X1:$i]:(((in @ (esk2_1 @ X1) @ (powerset @ X1))|(in @ (esk1_1 @ X1) @ X1)|(in @ esk5_0 @ X1)|~((in @ esk6_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_67, c_0_131])).
% 3.43/0.70 thf(c_0_134, negated_conjecture, (in @ esk6_0 @ esk4_0), inference(spm,[status(thm)],[c_0_132, c_0_68])).
% 3.43/0.70 thf(c_0_135, negated_conjecture, ((in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_133, c_0_134]), c_0_76]), c_0_84])])).
% 3.43/0.70 thf(c_0_136, negated_conjecture, ![X1:$i]:(((in @ (esk1_1 @ X1) @ X1)|(in @ esk5_0 @ X1)|(nonempty @ (esk2_1 @ X1))|~((in @ esk6_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_80, c_0_131])).
% 3.43/0.70 thf(c_0_137, plain, ![X1:$i, X2:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_135]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_138, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ esk4_0)|(nonempty @ (esk2_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_136, c_0_134]), c_0_76]), c_0_84])])).
% 3.43/0.70 thf(c_0_139, negated_conjecture, ![X1:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk6_0)))), inference(spm,[status(thm)],[c_0_137, c_0_134])).
% 3.43/0.70 thf(c_0_140, plain, ![X1:$i]:((((esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))=(X1))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ X1)|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)|~((in @ X1 @ (esk2_1 @ esk4_0))))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_135]), c_0_34])]), c_0_138])).
% 3.43/0.70 thf(c_0_141, negated_conjecture, ((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_139, c_0_131])).
% 3.43/0.70 thf(c_0_142, negated_conjecture, ![X1:$i]:(((in @ (esk2_1 @ X1) @ (powerset @ X1))|(in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ esk5_0 @ X1)|~((in @ esk6_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_90, c_0_131])).
% 3.43/0.70 thf(c_0_143, negated_conjecture, (((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))))|(in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_140, c_0_141])).
% 3.43/0.70 thf(c_0_144, plain, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))!=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_135]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_145, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0))|(in @ esk5_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_142, c_0_134]), c_0_76]), c_0_84])])).
% 3.43/0.70 thf(c_0_146, negated_conjecture, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_143]), c_0_76]), c_0_84])]), c_0_144])).
% 3.43/0.70 thf(c_0_147, negated_conjecture, ![X1:$i]:(((in @ (esk1_1 @ X1) @ (esk1_1 @ X1))|(in @ esk5_0 @ X1)|(nonempty @ (esk2_1 @ X1))|~((in @ esk6_0 @ X1))|~((transitiveset @ X1))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_99, c_0_131])).
% 3.43/0.70 thf(c_0_148, plain, ![X1:$i, X2:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_145]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_149, plain, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_146, c_0_82]), c_0_34])]), c_0_138]), c_0_135])).
% 3.43/0.70 thf(c_0_150, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(nonempty @ (esk2_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_147, c_0_134]), c_0_76]), c_0_84])])).
% 3.43/0.70 thf(c_0_151, negated_conjecture, ![X1:$i]:(((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk6_0)))), inference(spm,[status(thm)],[c_0_148, c_0_134])).
% 3.43/0.70 thf(c_0_152, negated_conjecture, ![X1:$i]:(((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk6_0)))), inference(spm,[status(thm)],[c_0_149, c_0_134])).
% 3.43/0.70 thf(c_0_153, plain, ![X1:$i]:((((esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))=(X1))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ X1)|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)|~((in @ X1 @ (esk2_1 @ esk4_0))))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_145]), c_0_34])]), c_0_150])).
% 3.43/0.70 thf(c_0_154, negated_conjecture, ((in @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))) @ (esk2_1 @ esk4_0))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_151, c_0_131])).
% 3.43/0.70 thf(c_0_155, negated_conjecture, ((in @ (esk1_1 @ esk4_0) @ esk4_0)|(in @ esk5_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_152, c_0_131])).
% 3.43/0.70 thf(c_0_156, negated_conjecture, (((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0))))|(in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_153, c_0_154])).
% 3.43/0.70 thf(c_0_157, plain, ((in @ esk5_0 @ esk4_0)|~((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_117, c_0_155]), c_0_34])])).
% 3.43/0.70 thf(c_0_158, negated_conjecture, ![X1:$i, X2:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)) @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_156]), c_0_76]), c_0_84])]), c_0_157])).
% 3.43/0.70 thf(c_0_159, plain, ![X1:$i, X2:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ (esk2_1 @ esk4_0) @ (powerset @ esk4_0)))|~((nonempty @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_158, c_0_82]), c_0_34])])).
% 3.43/0.70 thf(c_0_160, negated_conjecture, ![X1:$i, X2:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_159, c_0_150]), c_0_145]), c_0_157])).
% 3.43/0.70 thf(c_0_161, negated_conjecture, ![X1:$i]:((((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk6_0)))), inference(spm,[status(thm)],[c_0_160, c_0_134])).
% 3.43/0.70 thf(c_0_162, plain, ![X1:$i, X2:$i]:(((in @ (esk1_1 @ esk4_0) @ (esk1_1 @ esk4_0))|(in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))!=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_145]), c_0_76]), c_0_84]), c_0_34])])).
% 3.43/0.70 thf(c_0_163, negated_conjecture, (((esk3_2 @ esk4_0 @ (esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))=(esk13_2 @ esk4_0 @ (esk2_1 @ esk4_0)))|(in @ esk5_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_161, c_0_131])).
% 3.43/0.70 thf(c_0_164, negated_conjecture, ![X1:$i, X2:$i]:(((in @ X1 @ esk7_0)|~((in @ X2 @ esk7_0))|~((in @ X2 @ esk4_0))|~((in @ X1 @ esk4_0))|~((in @ X1 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_75]), c_0_34])])).
% 3.43/0.70 thf(c_0_165, plain, ![X1:$i, X2:$i]:(((in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X2 @ esk4_0))|~((in @ X1 @ X2)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_163]), c_0_157])).
% 3.43/0.70 thf(c_0_166, negated_conjecture, ![X1:$i]:(((in @ X1 @ esk7_0)|~((in @ esk6_0 @ esk4_0))|~((in @ X1 @ esk4_0))|~((in @ X1 @ esk6_0)))), inference(spm,[status(thm)],[c_0_164, c_0_68])).
% 3.43/0.70 thf(c_0_167, negated_conjecture, ![X1:$i]:(((in @ esk5_0 @ esk4_0)|(in @ X1 @ esk4_0)|~((in @ X1 @ esk6_0)))), inference(spm,[status(thm)],[c_0_165, c_0_134])).
% 3.43/0.70 thf(c_0_168, negated_conjecture, ![X1:$i]:(((in @ X1 @ esk7_0)|~((in @ X1 @ esk4_0))|~((in @ X1 @ esk6_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_166, c_0_134])])).
% 3.43/0.70 thf(c_0_169, negated_conjecture, (in @ esk5_0 @ esk4_0), inference(spm,[status(thm)],[c_0_167, c_0_131])).
% 3.43/0.70 thf(c_0_170, negated_conjecture, ~((in @ esk5_0 @ esk7_0)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.43/0.70 thf(c_0_171, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_168, c_0_169]), c_0_131])]), c_0_170]), ['proof']).
% 3.43/0.70 % SZS output end CNFRefutation
% 3.43/0.70 % Parsed axioms : 13
% 3.43/0.70 % Removed by relevancy pruning/SinE : 0
% 3.43/0.70 % Initial clauses : 59
% 3.43/0.70 % Removed in clause preprocessing : 8
% 3.43/0.70 % Initial clauses in saturation : 51
% 3.43/0.70 % Processed clauses : 1495
% 3.43/0.70 % ...of these trivial : 0
% 3.43/0.70 % ...subsumed : 349
% 3.43/0.70 % ...remaining for further processing : 1146
% 3.43/0.70 % Other redundant clauses eliminated : 0
% 3.43/0.70 % Clauses deleted for lack of memory : 0
% 3.43/0.70 % Backward-subsumed : 268
% 3.43/0.70 % Backward-rewritten : 323
% 3.43/0.70 % Generated clauses : 9250
% 3.43/0.70 % ...of the previous two non-redundant : 8225
% 3.43/0.70 % ...aggressively subsumed : 0
% 3.43/0.70 % Contextual simplify-reflections : 129
% 3.43/0.70 % Paramodulations : 9250
% 3.43/0.70 % Factorizations : 0
% 3.43/0.70 % NegExts : 0
% 3.43/0.70 % Equation resolutions : 0
% 3.43/0.70 % Disequality decompositions : 0
% 3.43/0.70 % Total rewrite steps : 2069
% 3.43/0.70 % ...of those cached : 2061
% 3.43/0.70 % Propositional unsat checks : 0
% 3.43/0.70 % Propositional check models : 0
% 3.43/0.70 % Propositional check unsatisfiable : 0
% 3.43/0.70 % Propositional clauses : 0
% 3.43/0.70 % Propositional clauses after purity: 0
% 3.43/0.70 % Propositional unsat core size : 0
% 3.43/0.70 % Propositional preprocessing time : 0.000
% 3.43/0.70 % Propositional encoding time : 0.000
% 3.43/0.70 % Propositional solver time : 0.000
% 3.43/0.70 % Success case prop preproc time : 0.000
% 3.43/0.70 % Success case prop encoding time : 0.000
% 3.43/0.70 % Success case prop solver time : 0.000
% 3.43/0.70 % Current number of processed clauses : 504
% 3.43/0.70 % Positive orientable unit clauses : 8
% 3.43/0.70 % Positive unorientable unit clauses: 0
% 3.43/0.70 % Negative unit clauses : 4
% 3.43/0.70 % Non-unit-clauses : 492
% 3.43/0.70 % Current number of unprocessed clauses: 6081
% 3.43/0.70 % ...number of literals in the above : 60241
% 3.43/0.70 % Current number of archived formulas : 0
% 3.43/0.70 % Current number of archived clauses : 642
% 3.43/0.70 % Clause-clause subsumption calls (NU) : 172780
% 3.43/0.70 % Rec. Clause-clause subsumption calls : 4741
% 3.43/0.70 % Non-unit clause-clause subsumptions : 744
% 3.43/0.70 % Unit Clause-clause subsumption calls : 1492
% 3.43/0.70 % Rewrite failures with RHS unbound : 0
% 3.43/0.70 % BW rewrite match attempts : 3
% 3.43/0.70 % BW rewrite match successes : 3
% 3.43/0.70 % Condensation attempts : 1495
% 3.43/0.70 % Condensation successes : 0
% 3.43/0.70 % Termbank termtop insertions : 456109
% 3.43/0.70 % Search garbage collected termcells : 1059
% 3.43/0.70
% 3.43/0.70 % -------------------------------------------------
% 3.43/0.70 % User time : 0.408 s
% 3.43/0.70 % System time : 0.010 s
% 3.43/0.70 % Total time : 0.418 s
% 3.43/0.70 % Maximum resident set size: 3640 pages
% 3.43/0.70
% 3.43/0.70 % -------------------------------------------------
% 3.43/0.70 % User time : 1.995 s
% 3.43/0.70 % System time : 0.055 s
% 3.43/0.70 % Total time : 2.050 s
% 3.43/0.70 % Maximum resident set size: 4864 pages
% 3.43/0.70 % E exiting
%------------------------------------------------------------------------------