%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWW336+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 : Thu Sep 24 03:10:19 PM UTC 2026
% Result : Theorem 27.93s 6.47s
% Output : CNFRefutation 27.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 11
% Syntax : Number of formulae : 66 ( 18 unt; 0 def)
% Number of atoms : 155 ( 35 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 145 ( 56 ~; 56 |; 10 &)
% ( 6 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-2 aty)
% Number of variables : 154 ( 21 sgn 84 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_emptyE,axiom,
! [X6,X5] : ~ hBOOL(hAPP(hAPP(c_member(X5),X6),c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_emptyE) ).
fof(fact_all__not__in__conv,axiom,
! [X12,X5] :
( ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(X5),X3),X12))
<=> X12 = c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_all__not__in__conv) ).
fof(fact_mem__def,axiom,
! [X12,X16,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X16),X12))
<=> hBOOL(hAPP(X12,X16)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mem__def) ).
fof(fact_ex__in__conv,axiom,
! [X12,X5] :
( ? [X3] : hBOOL(hAPP(hAPP(c_member(X5),X3),X12))
<=> X12 != c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ex__in__conv) ).
fof(fact_empty__not__insert,axiom,
! [X12,X6,X5] : c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) != hAPP(hAPP(c_Set_Oinsert(X5),X6),X12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_empty__not__insert) ).
fof(fact_singletonE,axiom,
! [X6,X15,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X15),hAPP(hAPP(c_Set_Oinsert(X5),X6),c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)))))
=> X15 = X6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_singletonE) ).
fof(fact_insertE,axiom,
! [X12,X15,X6,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X6),hAPP(hAPP(c_Set_Oinsert(X5),X15),X12)))
=> ( X6 != X15
=> hBOOL(hAPP(hAPP(c_member(X5),X6),X12)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_insertE) ).
fof(conj_4,conjecture,
! [X10] :
( ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) )
=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_4) ).
fof(fact_bex__UNIV,axiom,
! [X11,X5] :
( ? [X3] :
( hBOOL(hAPP(X11,X3))
& hBOOL(hAPP(hAPP(c_member(X5),X3),c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)))) )
<=> ? [X118] : hBOOL(hAPP(X11,X118)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_bex__UNIV) ).
fof(conj_3,hypothesis,
! [X10] :
( ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) )
=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),v_ts))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_3) ).
fof(conj_1,hypothesis,
! [X10] :
( ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) )
=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(c_0_11,plain,
! [X6,X5] : ~ hBOOL(hAPP(hAPP(c_member(X5),X6),c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)))),
inference(fof_simplification,[status(thm)],[fact_emptyE]) ).
fof(c_0_12,plain,
! [X12,X5] :
( ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(X5),X3),X12))
<=> X12 = c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) ),
inference(fof_simplification,[status(thm)],[fact_all__not__in__conv]) ).
fof(c_0_13,plain,
! [X324,X325] : ~ hBOOL(hAPP(hAPP(c_member(X325),X324),c_Orderings_Obot__class_Obot(tc_fun(X325,tc_HOL_Obool)))),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_11])]) ).
fof(c_0_14,plain,
! [X589,X590,X591] :
( ( hBOOL(hAPP(hAPP(c_member(X591),X590),X589))
| ~ hBOOL(hAPP(X589,X590)) )
& ( hBOOL(hAPP(X589,X590))
| ~ hBOOL(hAPP(hAPP(c_member(X591),X590),X589)) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_mem__def])])]) ).
fof(c_0_15,plain,
! [X334,X335,X337,X338,X339] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X338),X339),X337))
| X337 != c_Orderings_Obot__class_Obot(tc_fun(X338,tc_HOL_Obool)) )
& ( X334 = c_Orderings_Obot__class_Obot(tc_fun(X335,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X335),esk6_2(X334,X335)),X334)) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])])])]) ).
fof(c_0_16,plain,
! [X12,X5] :
( ? [X3] : hBOOL(hAPP(hAPP(c_member(X5),X3),X12))
<=> X12 != c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) ),
inference(fof_simplification,[status(thm)],[fact_ex__in__conv]) ).
fof(c_0_17,plain,
! [X12,X6,X5] : c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) != hAPP(hAPP(c_Set_Oinsert(X5),X6),X12),
inference(fof_simplification,[status(thm)],[fact_empty__not__insert]) ).
cnf(c_0_18,plain,
~ hBOOL(hAPP(hAPP(c_member(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)))),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_19,plain,
( ~ hBOOL(hAPP(X1,X2))
| hBOOL(hAPP(hAPP(c_member(X3),X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_20,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| hBOOL(hAPP(X3,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_21,plain,
( X2 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X1),esk6_2(X2,X1)),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
fof(c_0_22,plain,
! [X402,X403,X404] :
( X403 = X402
| ~ hBOOL(hAPP(hAPP(c_member(X404),X403),hAPP(hAPP(c_Set_Oinsert(X404),X402),c_Orderings_Obot__class_Obot(tc_fun(X404,tc_HOL_Obool))))) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_singletonE])])]) ).
fof(c_0_23,plain,
! [X340,X341,X342,X343,X344] :
( ( hBOOL(hAPP(hAPP(c_member(X344),esk7_2(X343,X344)),X343))
| X343 = c_Orderings_Obot__class_Obot(tc_fun(X344,tc_HOL_Obool)) )
& ( X340 != c_Orderings_Obot__class_Obot(tc_fun(X341,tc_HOL_Obool))
| ~ hBOOL(hAPP(hAPP(c_member(X341),X342),X340)) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])])])]) ).
fof(c_0_24,plain,
! [X374,X375,X376] : c_Orderings_Obot__class_Obot(tc_fun(X376,tc_HOL_Obool)) != hAPP(hAPP(c_Set_Oinsert(X376),X375),X374),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_17])]) ).
cnf(c_0_25,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)),X2)),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_26,plain,
( hBOOL(hAPP(X1,esk6_2(X1,X2)))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
fof(c_0_27,plain,
! [X12,X15,X6,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X6),hAPP(hAPP(c_Set_Oinsert(X5),X15),X12)))
=> ( X6 != X15
=> hBOOL(hAPP(hAPP(c_member(X5),X6),X12)) ) ),
inference(fof_simplification,[status(thm)],[fact_insertE]) ).
fof(c_0_28,negated_conjecture,
~ ! [X10] :
( ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) )
=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X3),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X10,X3) ) ),
inference(assume_negation,[status(cth)],[conj_4]) ).
cnf(c_0_29,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),hAPP(hAPP(c_Set_Oinsert(X1),X3),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)))))
| X2 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_30,plain,
( hBOOL(hAPP(hAPP(c_member(X2),esk7_2(X1,X2)),X1))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_31,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != hAPP(hAPP(c_Set_Oinsert(X1),X2),X3),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_32,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
fof(c_0_33,plain,
! [X2058,X2059,X2060,X2062,X2063,X2064] :
( ( ~ hBOOL(hAPP(X2062,X2063))
| hBOOL(hAPP(X2062,esk44_2(X2062,X2064))) )
& ( ~ hBOOL(hAPP(X2062,X2063))
| hBOOL(hAPP(hAPP(c_member(X2064),esk44_2(X2062,X2064)),c_Orderings_Otop__class_Otop(tc_fun(X2064,tc_HOL_Obool)))) )
& ( hBOOL(hAPP(X2058,esk43_1(X2058)))
| ~ hBOOL(hAPP(X2058,X2060))
| ~ hBOOL(hAPP(hAPP(c_member(X2059),X2060),c_Orderings_Otop__class_Otop(tc_fun(X2059,tc_HOL_Obool)))) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_bex__UNIV])])])])])])]) ).
fof(c_0_34,plain,
! [X414,X415,X416,X417] :
( hBOOL(hAPP(hAPP(c_member(X417),X416),X414))
| X416 = X415
| ~ hBOOL(hAPP(hAPP(c_member(X417),X416),hAPP(hAPP(c_Set_Oinsert(X417),X415),X414))) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])]) ).
fof(c_0_35,negated_conjecture,
! [X289] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,esk3_0,esk4_0)
& hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk4_0),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)))
& ( c_Hoare__Mirabelle_Otriple__valid(t_a,esk3_0,X289)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X289),v_G)) ) ),
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_28])])])])]) ).
cnf(c_0_36,plain,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(X3),X2),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_HOL_Obool))),X1))
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_29,c_0_19]) ).
cnf(c_0_37,plain,
( hBOOL(hAPP(X1,esk7_2(X1,X2)))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_20,c_0_30]) ).
cnf(c_0_38,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != hAPP(hAPP(c_Set_Oinsert(X2),X3),X4),
inference(spm,[status(thm)],[c_0_31,c_0_32]) ).
cnf(c_0_39,plain,
( ~ hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X1,esk44_2(X1,X2))) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
fof(c_0_40,hypothesis,
! [X285,X287] :
( ( c_Hoare__Mirabelle_Otriple__valid(t_a,X285,X287)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X287),v_ts))
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X285,esk2_1(X285)) )
& ( c_Hoare__Mirabelle_Otriple__valid(t_a,X285,X287)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X287),v_ts))
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk2_1(X285)),v_G)) ) ),
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)],[conj_3])])])])])]) ).
cnf(c_0_41,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),hAPP(hAPP(c_Set_Oinsert(X1),X3),X4)))
| hBOOL(hAPP(hAPP(c_member(X1),X2),X4))
| X2 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_42,negated_conjecture,
hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk4_0),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts))),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
fof(c_0_43,hypothesis,
! [X282,X284] :
( ( c_Hoare__Mirabelle_Otriple__valid(t_a,X282,X284)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X284),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))))
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X282,esk1_1(X282)) )
& ( c_Hoare__Mirabelle_Otriple__valid(t_a,X282,X284)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X284),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))))
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk1_1(X282)),v_G)) ) ),
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)],[conj_1])])])])])]) ).
cnf(c_0_44,plain,
esk7_2(hAPP(hAPP(c_Set_Oinsert(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))),X3) = X2,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_37]),c_0_38]) ).
cnf(c_0_45,plain,
( hBOOL(hAPP(X1,esk44_2(X1,X3)))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_39,c_0_26]) ).
cnf(c_0_46,hypothesis,
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X2),v_ts))
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X1,esk2_1(X1))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_47,negated_conjecture,
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk4_0),v_ts))
| esk4_0 = v_t ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_48,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_G))
| c_Hoare__Mirabelle_Otriple__valid(t_a,esk3_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_49,hypothesis,
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X2),v_ts))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,X2)
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk2_1(X1)),v_G)) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_50,hypothesis,
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X2),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))))
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X1,esk1_1(X1))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_51,plain,
esk7_2(hAPP(hAPP(c_Set_Oinsert(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_HOL_Obool))),X4) = X2,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_45]),c_0_25]) ).
cnf(c_0_52,hypothesis,
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X2),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,X2)
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk1_1(X1)),v_G)) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_53,hypothesis,
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X1,esk2_1(X1))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,esk4_0)
| esk4_0 = v_t ),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_54,negated_conjecture,
( ~ hBOOL(hAPP(v_G,X1))
| c_Hoare__Mirabelle_Otriple__valid(t_a,esk3_0,X1) ),
inference(spm,[status(thm)],[c_0_48,c_0_19]) ).
cnf(c_0_55,negated_conjecture,
~ c_Hoare__Mirabelle_Otriple__valid(t_a,esk3_0,esk4_0),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_56,hypothesis,
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk2_1(X1)),v_G))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,esk4_0)
| esk4_0 = v_t ),
inference(spm,[status(thm)],[c_0_49,c_0_47]) ).
cnf(c_0_57,hypothesis,
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X1,esk1_1(X1))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,v_t) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_30]),c_0_51]),c_0_38]) ).
cnf(c_0_58,hypothesis,
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),esk1_1(X1)),v_G))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,v_t) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_30]),c_0_51]),c_0_38]) ).
cnf(c_0_59,negated_conjecture,
( ~ hBOOL(hAPP(v_G,esk2_1(esk3_0)))
| esk4_0 = v_t ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_55]) ).
cnf(c_0_60,hypothesis,
( hBOOL(hAPP(v_G,esk2_1(X1)))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,esk4_0)
| esk4_0 = v_t ),
inference(spm,[status(thm)],[c_0_20,c_0_56]) ).
cnf(c_0_61,negated_conjecture,
( ~ hBOOL(hAPP(v_G,esk1_1(esk3_0)))
| c_Hoare__Mirabelle_Otriple__valid(t_a,esk3_0,v_t) ),
inference(spm,[status(thm)],[c_0_57,c_0_54]) ).
cnf(c_0_62,hypothesis,
( hBOOL(hAPP(v_G,esk1_1(X1)))
| c_Hoare__Mirabelle_Otriple__valid(t_a,X1,v_t) ),
inference(spm,[status(thm)],[c_0_20,c_0_58]) ).
cnf(c_0_63,negated_conjecture,
esk4_0 = v_t,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_60]),c_0_55]) ).
cnf(c_0_64,negated_conjecture,
c_Hoare__Mirabelle_Otriple__valid(t_a,esk3_0,v_t),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
cnf(c_0_65,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_55,c_0_63]),c_0_64])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW336+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.59 % Computer : n014.cluster.edu
% 0.11/0.59 % Model : x86_64 x86_64
% 0.11/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.59 % Memory : 8046.5625MB
% 0.11/0.59 % OS : Linux 6.8.0-71-generic
% 0.11/0.59 % CPULimit : 300
% 0.11/0.59 % WCLimit : 300
% 0.11/0.59 % DateTime : Mon Sep 21 09:48:06 UTC 2026
% 0.11/0.59 % CPUTime :
% 0.11/0.59 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.64 Running first-order theorem proving
% 0.16/0.64 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.93/6.47 % Version: 3.5.1
% 27.93/6.47 % Preprocessing class: FMLMSMSMSSSNFFN.
% 27.93/6.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 27.93/6.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 27.93/6.47 % Starting new_bool_3 with 300s (1) cores
% 27.93/6.47 % Starting new_bool_1 with 300s (1) cores
% 27.93/6.47 % Starting sh5l with 300s (1) cores
% 27.93/6.47 % new_bool_3 with pid 3770399 completed with status 0
% 27.93/6.47 % Result found by new_bool_3
% 27.93/6.47 % Preprocessing class: FMLMSMSMSSSNFFN.
% 27.93/6.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 27.93/6.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 27.93/6.47 % Starting new_bool_3 with 300s (1) cores
% 27.93/6.47 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 27.93/6.47 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 27.93/6.47 % Search class: FGHSM-FSLM32-DFFFFFNN
% 27.93/6.47 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 27.93/6.47 % Starting SubtermCWHack with 28s (1) cores
% 27.93/6.47 % SubtermCWHack with pid 3770402 completed with status 0
% 27.93/6.47 % Result found by SubtermCWHack
% 27.93/6.47 % Preprocessing class: FMLMSMSMSSSNFFN.
% 27.93/6.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 27.93/6.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 27.93/6.47 % Starting new_bool_3 with 300s (1) cores
% 27.93/6.47 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 27.93/6.47 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 27.93/6.47 % Search class: FGHSM-FSLM32-DFFFFFNN
% 27.93/6.47 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 27.93/6.47 % Starting SubtermCWHack with 28s (1) cores
% 27.93/6.47 % Preprocessing time : 0.022 s
% 27.93/6.47
% 27.93/6.47 % Proof found!
% 27.93/6.47 % SZS status Theorem
% 27.93/6.47 % SZS output start CNFRefutation
% See solution above
% 27.93/6.47 % Parsed axioms : 5228
% 27.93/6.47 % Removed by relevancy pruning/SinE : 4611
% 27.93/6.47 % Initial clauses : 905
% 27.93/6.47 % Removed in clause preprocessing : 36
% 27.93/6.47 % Initial clauses in saturation : 869
% 27.93/6.47 % Processed clauses : 10118
% 27.93/6.47 % ...of these trivial : 375
% 27.93/6.47 % ...subsumed : 7679
% 27.93/6.47 % ...remaining for further processing : 2064
% 27.93/6.47 % Other redundant clauses eliminated : 4565
% 27.93/6.47 % Clauses deleted for lack of memory : 0
% 27.93/6.47 % Backward-subsumed : 54
% 27.93/6.47 % Backward-rewritten : 126
% 27.93/6.47 % Generated clauses : 301334
% 27.93/6.47 % ...of the previous two non-redundant : 270801
% 27.93/6.47 % ...aggressively subsumed : 0
% 27.93/6.47 % Contextual simplify-reflections : 14
% 27.93/6.47 % Paramodulations : 296719
% 27.93/6.47 % Factorizations : 38
% 27.93/6.47 % NegExts : 0
% 27.93/6.47 % Equation resolutions : 4589
% 27.93/6.47 % Disequality decompositions : 0
% 27.93/6.47 % Total rewrite steps : 52188
% 27.93/6.47 % ...of those cached : 45836
% 27.93/6.47 % Propositional unsat checks : 0
% 27.93/6.47 % Propositional check models : 0
% 27.93/6.47 % Propositional check unsatisfiable : 0
% 27.93/6.47 % Propositional clauses : 0
% 27.93/6.47 % Propositional clauses after purity: 0
% 27.93/6.47 % Propositional unsat core size : 0
% 27.93/6.47 % Propositional preprocessing time : 0.000
% 27.93/6.47 % Propositional encoding time : 0.000
% 27.93/6.47 % Propositional solver time : 0.000
% 27.93/6.47 % Success case prop preproc time : 0.000
% 27.93/6.47 % Success case prop encoding time : 0.000
% 27.93/6.47 % Success case prop solver time : 0.000
% 27.93/6.47 % Current number of processed clauses : 1806
% 27.93/6.47 % Positive orientable unit clauses : 383
% 27.93/6.47 % Positive unorientable unit clauses: 17
% 27.93/6.47 % Negative unit clauses : 140
% 27.93/6.47 % Non-unit-clauses : 1266
% 27.93/6.47 % Current number of unprocessed clauses: 259161
% 27.93/6.47 % ...number of literals in the above : 833048
% 27.93/6.47 % Current number of archived formulas : 0
% 27.93/6.47 % Current number of archived clauses : 180
% 27.93/6.47 % Clause-clause subsumption calls (NU) : 221222
% 27.93/6.47 % Rec. Clause-clause subsumption calls : 120874
% 27.93/6.47 % Non-unit clause-clause subsumptions : 6243
% 27.93/6.47 % Unit Clause-clause subsumption calls : 5474
% 27.93/6.47 % Rewrite failures with RHS unbound : 199
% 27.93/6.47 % BW rewrite match attempts : 12908
% 27.93/6.47 % BW rewrite match successes : 170
% 27.93/6.47 % Condensation attempts : 0
% 27.93/6.47 % Condensation successes : 0
% 27.93/6.47 % Termbank termtop insertions : 8266022
% 27.93/6.47 % Search garbage collected termcells : 54987
% 27.93/6.47
% 27.93/6.47 % -------------------------------------------------
% 27.93/6.47 % User time : 5.236 s
% 27.93/6.47 % System time : 0.215 s
% 27.93/6.47 % Total time : 5.451 s
% 27.93/6.47 % Maximum resident set size: 13148 pages
% 27.93/6.47
% 27.93/6.47 % -------------------------------------------------
% 27.93/6.47 % User time : 5.493 s
% 27.93/6.47 % System time : 0.233 s
% 27.93/6.47 % Total time : 5.726 s
% 27.93/6.47 % Maximum resident set size: 12288 pages
% 27.93/6.47 % E exiting
%------------------------------------------------------------------------------