%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : ITP001+5 : TPTP v9.2.1. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n002.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:01:32 PM UTC 2026 % Result : Theorem 0.66s 1.54s % Output : Proof 0.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.22 % Problem : ITP001+5 : TPTP v9.2.1. Bugfixed v7.5.0. % 0.08/0.23 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.18/0.50 % Computer : n002.cluster.edu % 0.18/0.50 % Model : x86_64 x86_64 % 0.18/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.50 % Memory : 8042.1875MB % 0.18/0.50 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.50 % CPULimit : 300 % 0.18/0.50 % WCLimit : 300 % 0.18/0.50 % DateTime : Mon May 11 12:11:17 EDT 2026 % 0.18/0.50 % CPUTime : % 0.66/1.54 % SZS status Theorem % 0.66/1.54 % SZS output start Proof % 0.66/1.54 % 0.66/1.54 =============================================================== % 0.66/1.54 TPTP Problem: conj_thm_2Ebool_2ETRUTH (conjecture with 117 axiom(s)) % 0.66/1.54 Axioms: [bool_ne,ind_ne,arr_ne,ap_tp,boolext,funcext,kbeta,ibeta,mem_c_2Emin_2E_3D,ax_eq_p,mem_c_2Emin_2E_3D_3D_3E,ax_imp_p,mem_c_2Emin_2E_40,ne_ty_2Ebool_2Eitself,mem_c_2Ebool_2E_21,ax_all_p,mem_c_2Ebool_2E_2F_5C,ax_and_p,mem_c_2Ebool_2E_3F,ax_ex_p,mem_c_2Ebool_2E_3F_21,mem_c_2Ebool_2EARB,mem_c_2Ebool_2EBOUNDED,mem_c_2Ebool_2ECOND,mem_c_2Ebool_2EDATATYPE,mem_c_2Ebool_2EF,ax_false_p,mem_c_2Ebool_2EIN,mem_c_2Ebool_2ELET,mem_c_2Ebool_2EONE__ONE,mem_c_2Ebool_2EONTO,mem_c_2Ebool_2ERES__ABSTRACT,mem_c_2Ebool_2ERES__EXISTS,mem_c_2Ebool_2ERES__EXISTS__UNIQUE,mem_c_2Ebool_2ERES__FORALL,mem_c_2Ebool_2ERES__SELECT,mem_c_2Ebool_2ET,ax_true_p,mem_c_2Ebool_2ETYPE__DEFINITION,mem_c_2Ebool_2E_5C_2F,ax_or_p,mem_c_2Ebool_2Eitself__case,mem_c_2Ebool_2Eliteral__case,mem_c_2Ebool_2Ethe__value,mem_c_2Ebool_2E_7E,ax_neg_p,ax_thm_2Ebool_2ET__DEF,lameq_f1,ax_thm_2Ebool_2EFORALL__DEF,lameq_f2,ax_thm_2Ebool_2EEXISTS__DEF,lameq_f3,lameq_f4,lameq_f5,ax_thm_2Ebool_2EAND__DEF,lameq_f6,lameq_f7,lameq_f8,ax_thm_2Ebool_2EOR__DEF,ax_thm_2Ebool_2EF__DEF,lameq_f9,ax_thm_2Ebool_2ENOT__DEF,lameq_f10,lameq_f11,lameq_f12,ax_thm_2Ebool_2EEXISTS__UNIQUE__DEF,lameq_f13,lameq_f14,ax_thm_2Ebool_2ELET__DEF,lameq_f15,lameq_f16,lameq_f17,lameq_f18,ax_thm_2Ebool_2ECOND__DEF,lameq_f19,lameq_f20,lameq_f21,ax_thm_2Ebool_2EONE__ONE__DEF,lameq_f22,lameq_f23,lameq_f24,ax_thm_2Ebool_2EONTO__DEF,lameq_f25,lameq_f26,lameq_f27,lameq_f28,lameq_f29,lameq_f30,ax_thm_2Ebool_2ETYPE__DEFINITION,ax_thm_2Ebool_2EBOOL__CASES__AX,lameq_f31,ax_thm_2Ebool_2EETA__AX,ax_thm_2Ebool_2ESELECT__AX,ax_thm_2Ebool_2EINFINITY__AX,ax_thm_2Ebool_2Eliteral__case__DEF,lameq_f32,lameq_f33,ax_thm_2Ebool_2EIN__DEF,lameq_f34,lameq_f35,lameq_f36,ax_thm_2Ebool_2ERES__FORALL__DEF,lameq_f37,lameq_f38,lameq_f39,ax_thm_2Ebool_2ERES__EXISTS__DEF,lameq_f40,lameq_f41,lameq_f42,lameq_f43,lameq_f44,ax_thm_2Ebool_2ERES__EXISTS__UNIQUE__DEF,lameq_f45,lameq_f46,ax_thm_2Ebool_2ERES__SELECT__DEF,ax_thm_2Ebool_2EBOUNDED__DEF,ax_thm_2Ebool_2EDATATYPE__TAG__DEF] % 0.66/1.54 =============================================================== % 0.66/1.54 % 0.66/1.54 Combined formula: 117 axiom(s) => conjecture % 0.66/1.54 % 0.66/1.54 % Equality/functions detected -> nanoCoP oracle mode % 0.66/1.54 nanoCoP : % 0.66/1.54 % 143,092 inferences, 0.090 CPU in 0.090 seconds (100% CPU, 1593222 Lips) % 0.66/1.54 % 0.66/1.54 % nanoCoP proof (equality/functions) % 0.66/1.54 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 0.66/1.54 % 0.66/1.54 % SZS output end Proof %------------------------------------------------------------------------------