%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWW319+1 : TPTP v9.2.1. Released v5.2.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:31:37 PM UTC 2026
% Result : Theorem 15.82s 10.38s
% Output : CNFRefutation 15.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 10
% Syntax : Number of formulae : 39 ( 26 unt; 0 def)
% Number of atoms : 55 ( 13 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 32 ( 16 ~; 11 |; 2 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% Number of variables : 75 ( 6 sgn 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_cut,axiom,
! [X4,X7,X8,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X5,X8,X7)
=> ( c_Hoare__Mirabelle_Ohoare__derivs(X5,X4,X8)
=> c_Hoare__Mirabelle_Ohoare__derivs(X5,X4,X7) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_cut) ).
fof(conj_0,hypothesis,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(fact_asm,axiom,
! [X4,X7,X5] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(X5),tc_HOL_Obool)),X7),X4))
=> c_Hoare__Mirabelle_Ohoare__derivs(X5,X4,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_asm) ).
fof(conj_1,conjecture,
( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,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_Ohoare__derivs(t_a,v_G,v_ts) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(fact_singleton__conv2,axiom,
! [X6,X5] : hAPP(c_Set_OCollect(X5),hAPP(c_fequal,X6)) = hAPP(hAPP(c_Set_Oinsert(X5),X6),c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_singleton__conv2) ).
fof(fact_Collect__def,axiom,
! [X18,X5] : hAPP(c_Set_OCollect(X5),X18) = X18,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Collect__def) ).
fof(fact_Int__lower1,axiom,
! [X39,X10,X5] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X10),X39)),X10)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Int__lower1) ).
fof(fact_subset__insertI,axiom,
! [X6,X39,X5] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool)),X39),hAPP(hAPP(c_Set_Oinsert(X5),X6),X39))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_subset__insertI) ).
fof(fact_insert__inter__insert,axiom,
! [X39,X10,X6,X5] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X5),X6),X10)),hAPP(hAPP(c_Set_Oinsert(X5),X6),X39)) = hAPP(hAPP(c_Set_Oinsert(X5),X6),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X10),X39)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_insert__inter__insert) ).
fof(fact_Int__empty__right,axiom,
! [X10,X5] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X10),c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool))) = c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Int__empty__right) ).
fof(c_0_10,plain,
! [X16940,X16941,X16942,X16943] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X16943,X16942,X16941)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X16943,X16940,X16942)
| c_Hoare__Mirabelle_Ohoare__derivs(X16943,X16940,X16941) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_cut])]) ).
cnf(c_0_11,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X3)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X1,X4,X2) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_12,hypothesis,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)),
inference(split_conjunct,[status(thm)],[conj_0]) ).
fof(c_0_13,plain,
! [X17263,X17264,X17265] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(X17265),tc_HOL_Obool)),X17264),X17263))
| c_Hoare__Mirabelle_Ohoare__derivs(X17265,X17263,X17264) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_asm])]) ).
fof(c_0_14,negated_conjecture,
~ ( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,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_Ohoare__derivs(t_a,v_G,v_ts) ),
inference(assume_negation,[status(cth)],[conj_1]) ).
fof(c_0_15,plain,
! [X27612,X27613] : hAPP(c_Set_OCollect(X27613),hAPP(c_fequal,X27612)) = hAPP(hAPP(c_Set_Oinsert(X27613),X27612),c_Orderings_Obot__class_Obot(tc_fun(X27613,tc_HOL_Obool))),
inference(variable_rename,[status(thm)],[fact_singleton__conv2]) ).
fof(c_0_16,plain,
! [X27582,X27583] : hAPP(c_Set_OCollect(X27583),X27582) = X27582,
inference(variable_rename,[status(thm)],[fact_Collect__def]) ).
cnf(c_0_17,hypothesis,
( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,X1)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts),X1) ),
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
cnf(c_0_18,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(X1,X3,X2)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_HOL_Obool)),X2),X3)) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
fof(c_0_19,plain,
! [X24145,X24146,X24147] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X24147,tc_HOL_Obool)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X24147,tc_HOL_Obool)),X24146),X24145)),X24146)),
inference(variable_rename,[status(thm)],[fact_Int__lower1]) ).
fof(c_0_20,negated_conjecture,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,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_Ohoare__derivs(t_a,v_G,v_ts) ),
inference(fof_nnf,[status(thm)],[c_0_14]) ).
cnf(c_0_21,plain,
hAPP(c_Set_OCollect(X1),hAPP(c_fequal,X2)) = hAPP(hAPP(c_Set_Oinsert(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_22,plain,
hAPP(c_Set_OCollect(X1),X2) = X2,
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_23,plain,
! [X17252,X17253,X17254] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X17254,tc_HOL_Obool)),X17253),hAPP(hAPP(c_Set_Oinsert(X17254),X17252),X17253))),
inference(variable_rename,[status(thm)],[fact_subset__insertI]) ).
cnf(c_0_24,hypothesis,
( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,X1)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)),X1),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts))) ),
inference(spm,[status(thm)],[c_0_17,c_0_18]) ).
cnf(c_0_25,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X3)),X2)),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_26,plain,
! [X23986,X23987,X23988,X23989] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X23989,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X23989),X23988),X23987)),hAPP(hAPP(c_Set_Oinsert(X23989),X23988),X23986)) = hAPP(hAPP(c_Set_Oinsert(X23989),X23988),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X23989,tc_HOL_Obool)),X23987),X23986)),
inference(variable_rename,[status(thm)],[fact_insert__inter__insert]) ).
cnf(c_0_27,negated_conjecture,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,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_Ohoare__derivs(t_a,v_G,v_ts) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_28,plain,
hAPP(c_fequal,X1) = hAPP(hAPP(c_Set_Oinsert(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))),
inference(rw,[status(thm)],[c_0_21,c_0_22]) ).
cnf(c_0_29,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool)),X2),hAPP(hAPP(c_Set_Oinsert(X1),X3),X2))),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_30,hypothesis,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)),X1)),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_31,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X1),X2),X3)),hAPP(hAPP(c_Set_Oinsert(X1),X2),X4)) = hAPP(hAPP(c_Set_Oinsert(X1),X2),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X3),X4)),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
fof(c_0_32,plain,
! [X24004,X24005] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X24005,tc_HOL_Obool)),X24004),c_Orderings_Obot__class_Obot(tc_fun(X24005,tc_HOL_Obool))) = c_Orderings_Obot__class_Obot(tc_fun(X24005,tc_HOL_Obool)),
inference(variable_rename,[status(thm)],[fact_Int__empty__right]) ).
cnf(c_0_33,negated_conjecture,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(c_fequal,v_t))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,v_ts) ),
inference(rw,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_34,hypothesis,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,v_ts),
inference(spm,[status(thm)],[c_0_24,c_0_29]) ).
cnf(c_0_35,hypothesis,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)),v_ts),X1))),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_36,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_37,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(c_fequal,v_t)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33,c_0_34])]) ).
cnf(c_0_38,hypothesis,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_28]),c_0_37]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWW319+1 : TPTP v9.2.1. Released v5.2.0.
% 0.00/0.11 % 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.14/0.32 % Computer : n017.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 06:35:27 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 15.82/10.38 % Version : CSE_E---1.7
% 15.82/10.38 % Problem : theBenchmark.p
% 15.82/10.38 % SZS status Theorem for theBenchmark.p
% 15.82/10.38 % SZS output start CNFRefutation
% See solution above
% 15.93/10.40 % Total time : 9.029s
%------------------------------------------------------------------------------