%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWW474+2 : TPTP v9.2.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:32:38 PM UTC 2026
% Result : Theorem 2.21s 2.08s
% Output : CNFRefutation 2.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 12
% Syntax : Number of formulae : 44 ( 25 unt; 0 def)
% Number of atoms : 78 ( 19 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 59 ( 25 ~; 26 |; 0 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 13 con; 0-2 aty)
% Number of variables : 40 ( 8 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(help_fFalse_1_1_T,axiom,
! [X33] :
( is_bool(X33)
=> ( X33 = fTrue
| X33 = fFalse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
fof(gsy_c_hAPP_000tc__fun_Itc__Hoare____Mirabelle____ddpglwnxwg__Otriple_Itc__Com__O_004,hypothesis,
! [X1,X2] : is_bool(hAPP_f1760790145l_bool(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__fun_Itc__Hoare____Mirabelle____ddpglwnxwg__Otriple_Itc__Com__O_004) ).
fof(fact_4_cut,axiom,
! [X3,X6,X4] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X6),X4))
=> ( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X3),X6))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X3),X4)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_cut) ).
fof(fact_0_empty,axiom,
! [X3] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X3),bot_bo1055319631e_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_empty) ).
fof(fact_29_finite_OemptyI,axiom,
hBOOL(hAPP_f1760790145l_bool(finite784854244_state,bot_bo1055319631e_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_finite_OemptyI) ).
fof(help_fFalse_1_1_U,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(fact_215_WT__bodiesD,axiom,
! [X29,X30] :
( hBOOL(wT_bodies)
=> ( hAPP_p799580910on_com(body,X29) = some_com(X30)
=> hBOOL(hAPP_com_bool(wt,X30)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_WT__bodiesD) ).
fof(conj_7,conjecture,
hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_7) ).
fof(conj_1,hypothesis,
hBOOL(wT_bodies),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(fact_53_MGF,axiom,
! [X15] :
( hBOOL(hoare_298929751gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP_com_bool(wt,X15))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X15)),bot_bo1055319631e_bool))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_MGF) ).
fof(conj_5,hypothesis,
hAPP_p799580910on_com(body,pn) = some_com(y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_5) ).
fof(conj_0,hypothesis,
hBOOL(hoare_298929751gleton),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(c_0_12,plain,
! [X4360] :
( ~ is_bool(X4360)
| X4360 = fTrue
| X4360 = fFalse ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[help_fFalse_1_1_T])]) ).
fof(c_0_13,hypothesis,
! [X2383,X2384] : is_bool(hAPP_f1760790145l_bool(X2383,X2384)),
inference(variable_rename,[status(thm)],[gsy_c_hAPP_000tc__fun_Itc__Hoare____Mirabelle____ddpglwnxwg__Otriple_Itc__Com__O_004]) ).
cnf(c_0_14,plain,
( X1 = fTrue
| X1 = fFalse
| ~ is_bool(X1) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_15,hypothesis,
is_bool(hAPP_f1760790145l_bool(X1,X2)),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
fof(c_0_16,plain,
! [X2412,X2413,X2414] :
( ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X2413),X2414))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X2412),X2413))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X2412),X2414)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_4_cut])]) ).
fof(c_0_17,plain,
! [X2403] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X2403),bot_bo1055319631e_bool)),
inference(variable_rename,[status(thm)],[fact_0_empty]) ).
cnf(c_0_18,plain,
hBOOL(hAPP_f1760790145l_bool(finite784854244_state,bot_bo1055319631e_bool)),
inference(split_conjunct,[status(thm)],[fact_29_finite_OemptyI]) ).
cnf(c_0_19,hypothesis,
( hAPP_f1760790145l_bool(X1,X2) = fTrue
| hAPP_f1760790145l_bool(X1,X2) = fFalse ),
inference(spm,[status(thm)],[c_0_14,c_0_15]) ).
fof(c_0_20,plain,
~ hBOOL(fFalse),
inference(fof_simplification,[status(thm)],[help_fFalse_1_1_U]) ).
fof(c_0_21,plain,
! [X2899,X2900] :
( ~ hBOOL(wT_bodies)
| hAPP_p799580910on_com(body,X2899) != some_com(X2900)
| hBOOL(hAPP_com_bool(wt,X2900)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_215_WT__bodiesD])]) ).
cnf(c_0_22,plain,
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X3),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X3),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_23,plain,
hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),bot_bo1055319631e_bool)),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_24,hypothesis,
( hAPP_f1760790145l_bool(finite784854244_state,bot_bo1055319631e_bool) = fFalse
| hBOOL(fTrue) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_25,plain,
~ hBOOL(fFalse),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
fof(c_0_26,negated_conjecture,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj_7])]) ).
cnf(c_0_27,plain,
( hBOOL(hAPP_com_bool(wt,X2))
| ~ hBOOL(wT_bodies)
| hAPP_p799580910on_com(body,X1) != some_com(X2) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_28,hypothesis,
hBOOL(wT_bodies),
inference(split_conjunct,[status(thm)],[conj_1]) ).
fof(c_0_29,plain,
! [X2513] :
( ~ hBOOL(hoare_298929751gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP_com_bool(wt,X2513))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X2513)),bot_bo1055319631e_bool))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_53_MGF])]) ).
cnf(c_0_30,plain,
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),X2)) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_31,hypothesis,
hBOOL(fTrue),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_18,c_0_24]),c_0_25]) ).
cnf(c_0_32,negated_conjecture,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_33,plain,
( hBOOL(hAPP_com_bool(wt,X1))
| hAPP_p799580910on_com(body,X2) != some_com(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_28])]) ).
cnf(c_0_34,hypothesis,
hAPP_p799580910on_com(body,pn) = some_com(y),
inference(split_conjunct,[status(thm)],[conj_5]) ).
cnf(c_0_35,plain,
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X1)),bot_bo1055319631e_bool)))
| ~ hBOOL(hoare_298929751gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP_com_bool(wt,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_36,hypothesis,
hBOOL(hoare_298929751gleton),
inference(split_conjunct,[status(thm)],[conj_0]) ).
cnf(c_0_37,hypothesis,
( hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),X1) = fFalse
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X2),X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_19]),c_0_31])]) ).
cnf(c_0_38,negated_conjecture,
hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool)) = fFalse,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_19]),c_0_31])]) ).
cnf(c_0_39,hypothesis,
( hBOOL(hAPP_com_bool(wt,y))
| hAPP_p799580910on_com(body,X1) != hAPP_p799580910on_com(body,pn) ),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
cnf(c_0_40,plain,
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X1)),bot_bo1055319631e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_35,c_0_28]),c_0_36])]) ).
cnf(c_0_41,negated_conjecture,
hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool)) = fFalse,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_38]),c_0_25]) ).
cnf(c_0_42,hypothesis,
hBOOL(hAPP_com_bool(wt,y)),
inference(er,[status(thm)],[c_0_39]) ).
cnf(c_0_43,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_42])]),c_0_25]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWW474+2 : TPTP v9.2.1. Released v5.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n017.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 06:55:42 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 2.21/2.08 % Version : CSE_E---1.7
% 2.21/2.08 % Problem : theBenchmark.p
% 2.21/2.08 % SZS status Theorem for theBenchmark.p
% 2.21/2.08 % SZS output start CNFRefutation
% See solution above
% 2.21/2.08 % Total time : 1.535s
%------------------------------------------------------------------------------