%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SCT105+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 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 12 07:09:48 PM UTC 2026 % Result : Theorem 7.16s 7.57s % Output : Proof 7.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SCT105+1 : TPTP v9.2.1. Released v5.2.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.17/0.34 % Computer : n017.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon May 11 13:33:13 EDT 2026 % 0.17/0.34 % CPUTime : % 7.16/7.57 % SZS status Theorem % 7.16/7.57 % SZS output start Proof % 7.16/7.57 % 7.16/7.57 =============================================================== % 7.16/7.57 TPTP Problem: conj_0 (conjecture with 522 axiom(s)) % 7.16/7.57 Axioms: [fact_ext,fact_trans__def,fact_transD,fact_equalityCE,fact_in__rel__def,fact_same__fstI,fact_Nitpick_Orefl_H__def,fact_notin__Lin__iff,fact_split__paired__All,fact_Pair__eq,fact_Pair__inject,fact_mem__def,fact_eq__mem__trans,fact_eqelem__imp__iff,fact_eqset__imp__iff,fact_prod_Orecs,fact_irrefl__def,fact_in__lex__prod,fact_internal__split__conv,fact_RangeI,fact_Id__on__iff,fact_Id__on__eqI,fact_DomainI,fact_transI,fact_total__on__def,fact_in__inv__image,fact_trans__lex__prod,fact_Range__Id__on,fact_Domain__Id__on,fact_trans__Id__on,fact_trans__inv__image,fact_Domain__iff,fact_Range__iff,fact_strict__linear__order__on__def,fact_Id__onE,fact_RangeE,fact_DomainE,fact_acc_Osimps,fact_acc__downward,fact_refl__onD,fact_refl__onD1,fact_refl__onD2,fact_wfrec__rel_Oequations,fact_refl__on__Id__on,fact_preorder__on__def,fact_not__acc__down,fact_acc_OaccI,fact_wfrec__rel_Ointros,fact_wfrec__rel_Osimps,fact_acc__downwards__aux,fact_acc__downwards,fact_curryI,fact_single__valuedD,fact_single__valued__def,fact_curryD,fact_curryE,fact_single__valued__Id__on,fact_curry__conv,fact_rtrancl_Ortrancl__refl,fact_r__into__rtrancl,fact_Not__Domain__rtrancl,fact_single__valued__confluent,fact_converse__rtrancl__into__rtrancl,fact_rtrancl_Ortrancl__into__rtrancl,fact_rtrancl__trans,fact_trans__rtrancl,fact_single__valuedI,fact_rtrancl__idemp,fact_rtrancl__induct2,fact_converse__rtrancl__induct2,fact_converse__rtranclE2,fact_rtranclE,fact_converse__rtranclE,fact_converse__rtrancl__induct,fact_rtrancl__induct,fact_trancl__into__rtrancl,fact_cut__apply,fact_trancl_Or__into__trancl,fact_r__into__trancl_H,fact_trancl__rtrancl__absorb,fact_rtrancl__trancl__absorb,fact_trancl__domain,fact_trans__trancl,fact_trancl__id,fact_trancl__range,fact_r__r__into__trancl,fact_trancl__into__trancl2,fact_Transitive__Closure_Otrancl__into__trancl,fact_trancl__trans,fact_rtrancl__eq__or__trancl,fact_rtrancl__into__trancl2,fact_rtranclD,fact_rtrancl__into__trancl1,fact_trancl__rtrancl__trancl,fact_rtrancl__trancl__trancl,fact_tfl__cut__apply,fact_cuts__eq,fact_tranclD2,fact_tranclD,fact_acyclic__def,fact_irrefl__trancl__rD,fact_converse__tranclE,fact_tranclE,fact_Nitpick_Owf__wfrec_H__def,fact_IdI,fact_trans__Id,fact_single__valued__Id,fact_pair__in__Id__conv,fact_acyclicI,fact_IdE,fact_acyclic__insert,fact_acyclic__impl__antisym__rtrancl,fact_trancl__reflcl,fact_reflcl__trancl,fact_antisymD,fact_insertE,fact_insertCI,fact_UnE,fact_UnCI,fact_antisym__reflcl,fact_Un__absorb,fact_Un__commute,fact_insert__absorb2,fact_Un__left__absorb,fact_insert__commute,fact_Un__insert__right,fact_Un__left__commute,fact_Un__insert__left,fact_Un__assoc,fact_bex__Un,fact_ball__Un,fact_insert__code,fact_refl__on__Un,fact_Range__Un__eq,fact_Domain__Un__eq,fact_Domain__insert,fact_Range__insert,fact_Un__iff,fact_UnI1,fact_UnI2,fact_insertI1,fact_insert__iff,fact_insert__ident,fact_insertI2,fact_insert__absorb,fact_rtrancl__Un__rtrancl,fact_antisym__Id,fact_in__rtrancl__UnI,fact_antisym__Id__on,fact_rtrancl__reflcl,fact_rtrancl__reflcl__absorb,fact_trans__reflclI,fact_antisym__def,fact_sup1CI,fact_sup1E,fact_sup__apply,fact_partial__order__on__def,fact_rtrancl__Un__separator__converseE,fact_rtrancl__Un__separatorE,fact_wf__insert,fact_wf__inv__image,fact_wf__lex__prod,fact_wf__trancl,fact_wf__acyclic,fact_wf__irrefl,fact_wf__asym,fact_wf__not__sym,fact_wf__not__refl,fact_acc__wfD,fact_wf__acc__iff,fact_eq__mem,fact_sup_Oidem,fact_sup__idem,fact_sup_Ocommute,fact_inf__sup__aci_I5_J,fact_sup__commute,fact_sup_Oleft__idem,fact_inf__sup__aci_I8_J,fact_sup__left__idem,fact_sup_Oleft__commute,fact_inf__sup__aci_I7_J,fact_sup__left__commute,fact_sup_Oassoc,fact_inf__sup__aci_I6_J,fact_sup__assoc,fact_sup1I1,fact_sup1I2,fact_wf__measure,fact_linear__order__on__def,fact_def__wfrec,fact_wfrec,fact_tfl__wfrec,fact_wf__eq__minimal,fact_wf__same__fst,fact_wf__in__rel,fact_strict__linear__order__on__diff__Id,fact_antisymI,fact_acc__wfI,fact_DiffE,fact_DiffI,fact_Diff__iff,fact_DiffD1,fact_DiffD2,fact_Un__Diff__cancel,fact_Un__Diff__cancel2,fact_Un__Diff,fact_Diff__idemp,fact_minus__apply,fact_insert__Diff1,fact_insert__Diff__if,fact_rtrancl__r__diff__Id,fact_total__on__diff__Id,fact_irrefl__diff__Id,fact_trans__diff__Id,fact_well__order__on__def,fact_Field__def,fact_in__measure,fact_measure__def,fact_Range__Diff__subset,fact_equalityI,fact_trans__less__than,fact_wf__less__than,fact_subsetD,fact_Un__mono,fact_Un__least,fact_Un__absorb2,fact_Un__absorb1,fact_subset__Un__eq,fact_Un__upper2,fact_Un__upper1,fact_rev__predicate1D,fact_predicate1D,fact_Domain__mono,fact_acc__subset,fact_subset__refl,fact_set__eq__subset,fact_equalityD1,fact_equalityD2,fact_mono__Field,fact_subset__trans,fact_equalityE,fact_less__than__iff,fact_insert__mono,fact_subset__insertI2,fact_subset__insertI,fact_le__supE,fact_sup__mono,fact_sup__least,fact_le__supI,fact_sup__absorb1,fact_sup__absorb2,fact_le__supI2,fact_le__supI1,fact_le__sup__iff,fact_le__iff__sup,fact_sup__ge2,fact_inf__sup__ord_I4_J,fact_sup__ge1,fact_inf__sup__ord_I3_J,fact_less__supI2,fact_less__supI1,fact_set__mp,fact_set__rev__mp,fact_in__mono,fact_Diff__subset,fact_Diff__mono,fact_double__diff,fact_rtrancl__subset__rtrancl,fact_rtrancl__subset,fact_rtrancl__mono,fact_wf__subset,fact_antisym__subset,fact_acyclic__subset,fact_single__valued__subset,fact_insert__subset,fact_subset__insert,fact_Diff__subset__conv,fact_Diff__partition,fact_trancl__mono,fact_rtrancl__Un__subset,fact_Field__Un,fact_Domain__Diff__subset,fact_order__refl,fact_mlex__less,fact_le__funE,fact_le__funD,fact_psubset__eq,fact_subset__iff__psubset__eq,fact_psubset__imp__subset,fact_termination__basic__simps_I5_J,fact_psubset__subset__trans,fact_subset__psubset__trans,fact_less__fun__def,fact_psubsetD,fact_wfP__subset,fact_mlex__leq,fact_linorder__linear,fact_order__eq__iff,fact_order__eq__refl,fact_order__antisym__conv,fact_ord__eq__le__trans,fact_xt1_I3_J,fact_ord__le__eq__trans,fact_xt1_I4_J,fact_order__antisym,fact_order__trans,fact_xt1_I5_J,fact_xt1_I6_J,fact_linorder__le__cases,fact_order__less__irrefl,fact_linorder__neq__iff,fact_not__less__iff__gr__or__eq,fact_linorder__less__linear,fact_linorder__antisym__conv3,fact_linorder__neqE,fact_less__imp__neq,fact_order__less__not__sym,fact_order__less__imp__not__less,fact_order__less__imp__not__eq,fact_order__less__imp__not__eq2,fact_order__less__asym_H,fact_xt1_I9_J,fact_ord__eq__less__trans,fact_xt1_I1_J,fact_ord__less__eq__trans,fact_xt1_I2_J,fact_order__less__trans,fact_xt1_I10_J,fact_order__less__asym,fact_linorder__cases,fact_wf__mlex,fact_linorder__not__less,fact_linorder__not__le,fact_linorder__le__less__linear,fact_order__less__le,fact_less__le__not__le,fact_order__le__less,fact_leI,fact_not__leE,fact_linorder__antisym__conv1,fact_order__neq__le__trans,fact_xt1_I12_J,fact_leD,fact_order__less__imp__le,fact_linorder__antisym__conv2,fact_order__le__imp__less__or__eq,fact_order__le__neq__trans,fact_xt1_I11_J,fact_order__less__le__trans,fact_xt1_I7_J,fact_order__le__less__trans,fact_xt1_I8_J,fact_le__fun__def,fact_less__eq,fact_pred__nat__trancl__eq__le,fact_diff__eq__diff__less,fact_predicate2D,fact_rev__predicate2D,fact_psubset__trans,fact_diff__eq__diff__eq,fact_less__than__def,fact_wf__pred__nat,fact_diff__eq__diff__less__eq,fact_nat__less__le,fact_le__eq__less__or__eq,fact_less__not__refl,fact_nat__neq__iff,fact_linorder__neqE__nat,fact_less__irrefl__nat,fact_less__not__refl2,fact_less__not__refl3,fact_nat__less__cases,fact_diff__less__mono2,fact_less__imp__diff__less,fact_le__refl,fact_nat__le__linear,fact_eq__imp__le,fact_le__trans,fact_le__antisym,fact_le__diff__iff,fact_Nat_Odiff__diff__eq,fact_eq__diff__iff,fact_diff__diff__cancel,fact_diff__le__mono,fact_diff__le__mono2,fact_diff__le__self,fact_diff__less__mono,fact_less__diff__iff,fact_less__or__eq__imp__le,fact_le__neq__implies__less,fact_less__imp__le__nat,fact_pair__lessI2,fact_Field__insert,fact_wf__empty,fact_emptyE,fact_empty__subsetI,fact_diff__commute,fact_insert__is__Un,fact_insert__Diff__single,fact_Diff__insert2,fact_Diff__insert,fact_wf__pair__less,fact_all__not__in__conv,fact_ex__in__conv,fact_empty__iff,fact_equals0D,fact_bot__apply,fact_antisym__empty,fact_total__on__empty,fact_sup__eq__bot__iff,fact_sup__bot__right,fact_sup__bot__left,fact_partial__order__on__empty,fact_Id__on__empty,fact_preorder__on__empty,fact_Domain__empty__iff,fact_Domain__empty,fact_Range__empty__iff,fact_Range__empty,fact_refl__on__empty,fact_lnear__order__on__empty,fact_Diff__cancel,fact_Diff__empty,fact_empty__Diff,fact_Un__empty,fact_Un__empty__right,fact_Un__empty__left,fact_singleton__inject,fact_doubleton__eq__iff,fact_insert__not__empty,fact_empty__not__insert,fact_Field__empty,fact_well__order__on__empty,fact_subset__singletonD,fact_singletonE,fact_singleton__iff,fact_trancl__empty,fact_bot__least,fact_less__by__empty,fact_subset__empty,fact_not__psubset__empty,fact_rtrancl__empty,fact_pair__less__def,fact_insert__Diff,fact_Diff__insert__absorb,fact_subset__insert__iff,fact_diff__single__insert,fact_pair__lessI1,fact_psubset__insert__iff,fact_smax__insertI,fact_smin__insertI,fact_smin__emptyI,fact_pair__leqI2,fact_pair__leqI1,fact_pair__leq__def,fact_wmax__insertI,fact_wmin__insertI,fact_wmin__emptyI,fact_min__weak__def,fact_max__weak__def,fact_max__ext__wf,fact_min__ext__wf,fact_max__strict__def,fact_max__ext__additive,fact_min__strict__def,fact_the__elem__eq,fact_fold__graph_H_Ointros_I2_J,fact_fold__graph_H_Ointros_I1_J,fact_fold__graph_H_Oequations_I1_J,fact_subset__Image1__Image1__iff,fact_max__rpair__set,fact_wfE__pf,fact_Image__iff,fact_rev__ImageI,fact_Image__Id,fact_Image__mono,fact_Image__closed__trancl,fact_Image__empty,fact_Image__Un,fact_Un__Image,fact_Image__singleton__iff,fact_Partial__order__eq__Image1__Image1__iff,fact_Refl__antisym__eq__Image1__Image1__iff,fact_min__rpair__set,fact_subset__Image__Image__iff,fact_fold__graph_H_Oequations_I2_J,fact_rp__inv__image__rp,fact_ImageE,fact_reduction__pairI,fact_subset__equiv__class,fact_rel__compI,fact_rtrancl__unfold,fact_equiv__class__self,fact_union__comp__emptyR,arity_HOL__Obool__Lattices_Obounded__lattice,arity_fun__Lattices_Obounded__lattice,arity_fun__Lattices_Obounded__lattice__bot,arity_fun__Lattices_Osemilattice__sup,arity_fun__Orderings_Opreorder,arity_fun__Lattices_Olattice,arity_fun__Orderings_Oorder,arity_fun__Orderings_Oord,arity_fun__Orderings_Obot,arity_fun__Groups_Ominus,arity_Nat__Onat__Lattices_Osemilattice__sup,arity_Nat__Onat__Orderings_Opreorder,arity_Nat__Onat__Orderings_Olinorder,arity_Nat__Onat__Lattices_Olattice,arity_Nat__Onat__Orderings_Oorder,arity_Nat__Onat__Orderings_Oord,arity_Nat__Onat__Orderings_Obot,arity_Nat__Onat__Groups_Ominus,arity_HOL__Obool__Lattices_Obounded__lattice__bot,arity_HOL__Obool__Lattices_Osemilattice__sup,arity_HOL__Obool__Orderings_Opreorder,arity_HOL__Obool__Lattices_Olattice,arity_HOL__Obool__Orderings_Oorder,arity_HOL__Obool__Orderings_Oord,arity_HOL__Obool__Orderings_Obot,arity_HOL__Obool__Groups_Ominus,help_c__fequal__1,help_c__fequal__2] % 7.16/7.57 =============================================================== % 7.16/7.57 % 7.16/7.57 Combined formula: 522 axiom(s) => conjecture % 7.16/7.57 % 7.16/7.57 % Equality/functions detected -> nanoCoP oracle mode % 7.16/7.57 nanoCoP : % 7.16/7.57 % 8,796,107 inferences, 6.106 CPU in 6.107 seconds (100% CPU, 1440621 Lips) % 7.16/7.57 % 7.16/7.57 % nanoCoP proof (equality/functions) % 7.16/7.57 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 7.16/7.57 % 7.16/7.58 % SZS output end Proof %------------------------------------------------------------------------------