%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SYO868^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:44:53 AM UTC 2026
% Result : Theorem 1.55s 0.65s
% Output : CNFRefutation 1.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO868^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 17:26:34 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.26 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.FPj7hqhtWB/E---3.1_647319.p
% 1.55/0.65 % Version: 3.5.1-ho
% 1.55/0.65 % partial match(1): HSLMSMSSSSLCHFA
% 1.55/0.65 % Preprocessing class: HSLMSLSSSSLCHFA.
% 1.55/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.55/0.65 % Starting new_ho_10 with 1500s (5) cores
% 1.55/0.65 % Starting sh5l with 300s (1) cores
% 1.55/0.65 % Starting lpo8_s with 300s (1) cores
% 1.55/0.65 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 1.55/0.65 % ehoh_best_nonlift_rwall with pid 647336 completed with status 0
% 1.55/0.65 % Result found by ehoh_best_nonlift_rwall
% 1.55/0.65 % partial match(1): HSLMSMSSSSLCHFA
% 1.55/0.65 % Preprocessing class: HSLMSLSSSSLCHFA.
% 1.55/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.55/0.65 % Starting new_ho_10 with 1500s (5) cores
% 1.55/0.65 % Starting sh5l with 300s (1) cores
% 1.55/0.65 % Starting lpo8_s with 300s (1) cores
% 1.55/0.65 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 1.55/0.65 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = Auto)
% 1.55/0.65 % No SInE strategy applied
% 1.55/0.65 % Search class: HGHSM-SMLM33-DHFFFSBC
% 1.55/0.65 % partial match(1): HGHSM-SMLM33-MHFFFSBC
% 1.55/0.65 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 1.55/0.65 % Starting SubtermCWHack with 28s (1) cores
% 1.55/0.65 % SubtermCWHack with pid 647349 completed with status 0
% 1.55/0.65 % Result found by SubtermCWHack
% 1.55/0.65 % partial match(1): HSLMSMSSSSLCHFA
% 1.55/0.65 % Preprocessing class: HSLMSLSSSSLCHFA.
% 1.55/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.55/0.65 % Starting new_ho_10 with 1500s (5) cores
% 1.55/0.65 % Starting sh5l with 300s (1) cores
% 1.55/0.65 % Starting lpo8_s with 300s (1) cores
% 1.55/0.65 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 1.55/0.65 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = Auto)
% 1.55/0.65 % No SInE strategy applied
% 1.55/0.65 % Search class: HGHSM-SMLM33-DHFFFSBC
% 1.55/0.65 % partial match(1): HGHSM-SMLM33-MHFFFSBC
% 1.55/0.65 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 1.55/0.65 % Starting SubtermCWHack with 28s (1) cores
% 1.55/0.65 % Preprocessing time : 0.063 s
% 1.55/0.65
% 1.55/0.65 % Proof found!
% 1.55/0.65 % SZS status Theorem
% 1.55/0.65 % SZS output start CNFRefutation
% 1.55/0.65 thf(decl_24, type, c_False: $o).
% 1.55/0.65 thf(decl_26, type, c_not: $o > $o).
% 1.55/0.65 thf(decl_27, type, c_and: $o > $o > $o).
% 1.55/0.65 thf(decl_30, type, c_In: $i > $i > $o).
% 1.55/0.65 thf(decl_32, type, c_Empty: $i).
% 1.55/0.65 thf(decl_34, type, c_Power: $i > $i).
% 1.55/0.65 thf(decl_36, type, c_TransSet: $i > $o).
% 1.55/0.65 thf(decl_37, type, c_atleast2: $i > $o).
% 1.55/0.65 thf(decl_38, type, c_atleast3: $i > $o).
% 1.55/0.65 thf(decl_40, type, c_atleast5: $i > $o).
% 1.55/0.65 thf(decl_42, type, c_exactly2: $i > $o).
% 1.55/0.65 thf(decl_45, type, c_exactly5: $i > $o).
% 1.55/0.65 thf(decl_61, type, c_exactly1of2: $o > $o > $o).
% 1.55/0.65 thf(decl_81, type, c_nat_p: $i > $o).
% 1.55/0.65 thf(decl_85, type, c_ordinal: $i > $o).
% 1.55/0.65 thf(decl_94, type, c_binrep: $i > $i > $i).
% 1.55/0.65 thf(decl_117, type, c_SNoLt: $i > $i > $o).
% 1.55/0.65 thf(decl_269, type, epred143_2: $i > $i > $o).
% 1.55/0.65 thf(decl_270, type, epred144_2: $i > $i > $o).
% 1.55/0.65 thf(decl_271, type, esk1_0: $i).
% 1.55/0.65 thf(decl_283, type, epred145_0: $o).
% 1.55/0.65 thf(decl_329, type, esk52_0: $i).
% 1.55/0.65 thf(decl_330, type, esk53_0: $i).
% 1.55/0.65 thf(decl_331, type, esk54_0: $i).
% 1.55/0.65 thf(decl_332, type, esk55_1: $i > $i).
% 1.55/0.65 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox2/tmp/tmp.FPj7hqhtWB/E---3.1_647319.p', ax13)).
% 1.55/0.65 thf(conj, conjecture, ![X201:$i]:(((c_In @ X201 @ c_Empty)=>![X2:$i]:(((c_In @ X2 @ X201)=>![X9:$i]:(((c_In @ X9 @ X2)=>?[X13:$i]:(![X66:$i]:((((c_ordinal @ X13)=>(c_and @ ((c_exactly2 @ X13)) @ ((c_not @ ((c_exactly5 @ X66))))))=>((((c_ordinal @ X13)=>(c_exactly2 @ X13))=>((c_atleast2 @ X13)=>((((c_not @ ((c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))))=>((X13)=(X66)))=>(c_atleast3 @ X13))=>(c_and @ ((c_atleast5 @ X9)) @ ((c_not @ ((c_exactly1of2 @ ((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))) @ ((c_TransSet @ X66))))))))))=>(c_nat_p @ X13))))))))))), file('/export/starexec/sandbox2/tmp/tmp.FPj7hqhtWB/E---3.1_647319.p', conj)).
% 1.55/0.65 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox2/tmp/tmp.FPj7hqhtWB/E---3.1_647319.p', ax5)).
% 1.55/0.65 thf(ax11, axiom, ((c_False)<=>![X15:$o]:((X15))), file('/export/starexec/sandbox2/tmp/tmp.FPj7hqhtWB/E---3.1_647319.p', ax11)).
% 1.55/0.65 thf(c_0_4, plain, ![X236:$o]:(((c_not @ ((X236)))<=>((X236)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 1.55/0.65 thf(c_0_5, negated_conjecture, ~(![X201:$i]:(((c_In @ X201 @ c_Empty)=>![X2:$i]:(((c_In @ X2 @ X201)=>![X9:$i]:(((c_In @ X9 @ X2)=>?[X13:$i]:(![X66:$i]:((((c_ordinal @ X13)=>(c_and @ ((c_exactly2 @ X13)) @ ((c_not @ ((c_exactly5 @ X66))))))=>((((c_ordinal @ X13)=>(c_exactly2 @ X13))=>((c_atleast2 @ X13)=>((((c_not @ ((c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))))=>((X13)=(X66)))=>(c_atleast3 @ X13))=>(c_and @ ((c_atleast5 @ X9)) @ ((c_not @ ((c_exactly1of2 @ ((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))) @ ((c_TransSet @ X66))))))))))=>(c_nat_p @ X13)))))))))))), inference(assume_negation,[status(cth)],[conj])).
% 1.55/0.65 thf(c_0_6, plain, ![X13:$i, X66:$i]:(((epred143_2 @ X66 @ X13)<=>((~(c_exactly2 @ X13)|((((~(c_exactly5 @ X66)|~(c_not @ $true))&((c_exactly5 @ X66)|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(c_exactly5 @ X66)|(c_not @ $true))&((c_exactly5 @ X66)|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_exactly2 @ X13)|((((~(c_exactly5 @ X66)|~(c_not @ $true))&((c_exactly5 @ X66)|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(c_exactly5 @ X66)|(c_not @ $true))&((c_exactly5 @ X66)|(c_not @ $false)))|(c_and @ $false @ $false))))))), introduced(definition)).
% 1.55/0.65 thf(c_0_7, plain, ![X9:$i, X66:$i]:(((epred144_2 @ X66 @ X9)<=>((~(c_atleast5 @ X9)|((((((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $false)))))|~(c_not @ $true))&(((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $false @ $false)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $false)))))|(c_not @ $true))&(((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $false @ $false)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_atleast5 @ X9)|((((((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $false)))))|~(c_not @ $true))&(((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $false @ $false)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|~(c_exactly1of2 @ $false @ $false)))))|(c_not @ $true))&(((~(c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $true @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $true @ $false))))&((c_SNoLt @ X9 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty))|((~(c_TransSet @ X66)|(c_exactly1of2 @ $false @ $true))&((c_TransSet @ X66)|(c_exactly1of2 @ $false @ $false)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))), introduced(definition)).
% 1.55/0.65 thf(c_0_8, axiom, ((~(?[X7:$i]:((c_In @ X7 @ c_Empty)))|(c_not @ $true))&(?[X7:$i]:((c_In @ X7 @ c_Empty))|(c_not @ $false))), inference(fool_unroll,[status(thm)],[ax5])).
% 1.55/0.65 thf(c_0_9, plain, ![X484:$o]:(((~(c_not @ ((X484)))|(~(X484)|(c_False)))&(((X484)|(c_not @ ((X484))))&(~(c_False)|(c_not @ ((X484))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])).
% 1.55/0.65 thf(c_0_10, plain, ![X482:$o]:(((~(c_False)|(X482))&(~(epred145_0)|(c_False)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax11])])])])])).
% 1.55/0.65 thf(c_0_11, negated_conjecture, ~(![X201:$i]:(((c_In @ X201 @ c_Empty)=>![X2:$i]:(((c_In @ X2 @ X201)=>![X9:$i]:(((c_In @ X9 @ X2)=>?[X13:$i]:(![X66:$i]:((((c_ordinal @ X13)=>(epred143_2 @ X66 @ X13))=>((((c_ordinal @ X13)=>(c_exactly2 @ X13))=>((c_atleast2 @ X13)=>(((((~(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|(c_not @ $true))&((c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|(c_not @ $false)))=>((X13)=(X66)))=>(c_atleast3 @ X13))=>(epred144_2 @ X66 @ X9))))=>(c_nat_p @ X13)))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_5]), c_0_6]), c_0_7])).
% 1.55/0.65 thf(c_0_12, plain, ![X451:$i]:(((~(c_In @ X451 @ c_Empty)|(c_not @ $true))&((c_In @ esk1_0 @ c_Empty)|(c_not @ $false)))), 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_8])])])])])).
% 1.55/0.65 thf(c_0_13, plain, ((c_False)|~((c_not @ (($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_9])])])).
% 1.55/0.65 thf(c_0_14, plain, ~((c_False)), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_10])])])).
% 1.55/0.65 thf(c_0_15, negated_conjecture, ![X818:$i]:(((c_In @ esk52_0 @ c_Empty)&((c_In @ esk53_0 @ esk52_0)&((c_In @ esk54_0 @ esk53_0)&((~(c_ordinal @ X818)|(epred143_2 @ (esk55_1 @ X818) @ X818))&((((((~(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|(c_ordinal @ X818))&(~(c_not @ $false)|(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|(c_ordinal @ X818)))&((~(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|~(c_not @ $true)|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|(c_ordinal @ X818))&(~(c_not @ $false)|~(c_not @ $true)|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|(c_ordinal @ X818))))&(~(c_atleast3 @ X818)|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|(c_ordinal @ X818)))&((((~(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|~(c_exactly2 @ X818))&(~(c_not @ $false)|(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|~(c_exactly2 @ X818)))&((~(c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))|~(c_not @ $true)|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|~(c_exactly2 @ X818))&(~(c_not @ $false)|~(c_not @ $true)|((X818)=(esk55_1 @ X818))|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|~(c_exactly2 @ X818))))&(~(c_atleast3 @ X818)|(epred144_2 @ (esk55_1 @ X818) @ esk54_0)|~(c_atleast2 @ X818)|~(c_exactly2 @ X818))))&~(c_nat_p @ X818))))))), 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_11])])])])])])).
% 1.55/0.65 thf(c_0_16, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.55/0.65 thf(c_0_17, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_13, c_0_14])).
% 1.55/0.65 thf(c_0_18, negated_conjecture, (c_In @ esk52_0 @ c_Empty), inference(split_conjunct,[status(thm)],[c_0_15])).
% 1.55/0.65 thf(c_0_19, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_16, c_0_17])).
% 1.55/0.65 thf(c_0_20, negated_conjecture, ($false), inference(sr,[status(thm)],[c_0_18, c_0_19]), ['proof']).
% 1.55/0.65 % SZS output end CNFRefutation
% 1.55/0.65 % Parsed axioms : 213
% 1.55/0.65 % Removed by relevancy pruning/SinE : 0
% 1.55/0.65 % Initial clauses : 6208
% 1.55/0.65 % Removed in clause preprocessing : 1864
% 1.55/0.65 % Initial clauses in saturation : 4344
% 1.55/0.65 % Processed clauses : 50
% 1.55/0.65 % ...of these trivial : 1
% 1.55/0.65 % ...subsumed : 3
% 1.55/0.65 % ...remaining for further processing : 46
% 1.55/0.65 % Other redundant clauses eliminated : 0
% 1.55/0.65 % Clauses deleted for lack of memory : 0
% 1.55/0.65 % Backward-subsumed : 0
% 1.55/0.65 % Backward-rewritten : 0
% 1.55/0.65 % Generated clauses : 16
% 1.55/0.65 % ...of the previous two non-redundant : 0
% 1.55/0.65 % ...aggressively subsumed : 0
% 1.55/0.65 % Contextual simplify-reflections : 0
% 1.55/0.65 % Paramodulations : 15
% 1.55/0.65 % Factorizations : 0
% 1.55/0.65 % NegExts : 0
% 1.55/0.65 % Equation resolutions : 0
% 1.55/0.65 % Disequality decompositions : 0
% 1.55/0.65 % Total rewrite steps : 3
% 1.55/0.65 % ...of those cached : 2
% 1.55/0.65 % Propositional unsat checks : 0
% 1.55/0.65 % Propositional check models : 0
% 1.55/0.65 % Propositional check unsatisfiable : 0
% 1.55/0.65 % Propositional clauses : 0
% 1.55/0.65 % Propositional clauses after purity: 0
% 1.55/0.65 % Propositional unsat core size : 0
% 1.55/0.65 % Propositional preprocessing time : 0.000
% 1.55/0.65 % Propositional encoding time : 0.000
% 1.55/0.65 % Propositional solver time : 0.000
% 1.55/0.65 % Success case prop preproc time : 0.000
% 1.55/0.65 % Success case prop encoding time : 0.000
% 1.55/0.65 % Success case prop solver time : 0.000
% 1.55/0.65 % Current number of processed clauses : 45
% 1.55/0.65 % Positive orientable unit clauses : 5
% 1.55/0.65 % Positive unorientable unit clauses: 0
% 1.55/0.65 % Negative unit clauses : 10
% 1.55/0.65 % Non-unit-clauses : 30
% 1.55/0.65 % Current number of unprocessed clauses: 4294
% 1.55/0.65 % ...number of literals in the above : 22419
% 1.55/0.65 % Current number of archived formulas : 0
% 1.55/0.65 % Current number of archived clauses : 1
% 1.55/0.65 % Clause-clause subsumption calls (NU) : 356
% 1.55/0.65 % Rec. Clause-clause subsumption calls : 356
% 1.55/0.65 % Non-unit clause-clause subsumptions : 0
% 1.55/0.65 % Unit Clause-clause subsumption calls : 4
% 1.55/0.65 % Rewrite failures with RHS unbound : 0
% 1.55/0.65 % BW rewrite match attempts : 0
% 1.55/0.65 % BW rewrite match successes : 0
% 1.55/0.65 % Condensation attempts : 0
% 1.55/0.65 % Condensation successes : 0
% 1.55/0.65 % Termbank termtop insertions : 481638
% 1.55/0.65 % Search garbage collected termcells : 52280
% 1.55/0.65
% 1.55/0.65 % -------------------------------------------------
% 1.55/0.65 % User time : 0.330 s
% 1.55/0.65 % System time : 0.033 s
% 1.55/0.65 % Total time : 0.363 s
% 1.55/0.65 % Maximum resident set size: 15284 pages
% 1.55/0.65
% 1.55/0.65 % -------------------------------------------------
% 1.55/0.65 % User time : 0.336 s
% 1.55/0.65 % System time : 0.040 s
% 1.55/0.65 % Total time : 0.377 s
% 1.55/0.65 % Maximum resident set size: 5120 pages
% 1.55/0.65 % E exiting
%------------------------------------------------------------------------------