%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SYO578+1 : TPTP v9.2.1. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/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:19:56 PM UTC 2026 % Result : Theorem 19.98s 19.96s % Output : Proof 19.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYO578+1 : TPTP v9.2.1. Released v5.5.0. % 0.11/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.17/0.34 % Computer : n002.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 14:50:17 EDT 2026 % 0.17/0.34 % CPUTime : % 19.98/19.96 % SZS status Theorem % 19.98/19.97 % SZS output start Proof % 19.98/19.97 % 19.98/19.97 =============================================================== % 19.98/19.97 TPTP Problem: goals_86 (conjecture with 85 axiom(s)) % 19.98/19.97 Axioms: [sos_01,sos_02,sos_03,sos_04,sos_05,sos_06,sos_07,sos_08,sos_09,sos_10,sos_11,sos_12,sos_13,sos_14,sos_15,sos_16,sos_17,sos_18,sos_19,sos_20,sos_21,sos_22,sos_23,sos_24,sos_25,sos_26,sos_27,sos_28,sos_29,sos_30,sos_31,sos_32,sos_33,sos_34,sos_35,sos_36,sos_37,sos_38,sos_39,sos_40,sos_41,sos_42,sos_43,sos_44,sos_45,sos_46,sos_47,sos_48,sos_49,sos_50,sos_51,sos_52,sos_53,sos_54,sos_55,sos_56,sos_57,sos_58,sos_59,sos_60,sos_61,sos_62,sos_63,sos_64,sos_65,sos_66,sos_67,sos_68,sos_69,sos_70,sos_71,sos_72,sos_73,sos_74,sos_75,sos_76,sos_77,sos_78,sos_79,sos_80,sos_81,sos_82,sos_83,sos_84,sos_85] % 19.98/19.97 =============================================================== % 19.98/19.97 % 19.98/19.97 Combined formula: 85 axiom(s) => conjecture % 19.98/19.97 % 19.98/19.97 nanoCoP : % 19.98/19.97 % 372,477 inferences, 0.279 CPU in 0.279 seconds (100% CPU, 1333549 Lips) % 19.98/19.97 g4mic : % 19.98/19.97 % 100,006,454 inferences, 18.497 CPU in 18.496 seconds (100% CPU, 5406519 Lips) % 19.98/19.97 % 19.98/19.97 % Logic level: not determined (G4+ inference limit exceeded) % 19.98/19.97 % To get proofs (sequent calculus G4 and natural deduction), you can use G4+ at https://g4-mic.vidal-rosset.net/wasm/tinker % 19.98/19.97 % 19.98/19.97 % SZS output end Proof %------------------------------------------------------------------------------