%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : GEO299+1 : TPTP v9.2.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n012.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 06:59:12 PM UTC 2026 % Result : Theorem 2.08s 3.30s % Output : Proof 2.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : GEO299+1 : TPTP v9.2.1. Released v4.1.0. % 0.00/0.06 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.07/0.25 % Computer : n012.cluster.edu % 0.07/0.25 % Model : x86_64 x86_64 % 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.25 % Memory : 8042.1875MB % 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.25 % CPULimit : 300 % 0.07/0.25 % WCLimit : 300 % 0.07/0.25 % DateTime : Mon May 11 11:45:31 EDT 2026 % 0.07/0.25 % CPUTime : % 2.08/3.30 % SZS status Theorem % 2.08/3.31 % SZS output start Proof % 2.08/3.31 % 2.08/3.31 =============================================================== % 2.08/3.31 TPTP Problem: holds(324, 1255, 0) (conjecture with 159 axiom(s)) % 2.08/3.31 Axioms: [holds(323, 1254, 0),dis(321),holds(320, 1251, 0),neg(neg(319)),neg(316),qu(cond(axiom(180), 0), imp(cond(axiom(180), 0))),qu(cond(axiom(91), 0), imp(cond(axiom(91), 0))),holds(comma_conjunct2(comma_conjunct2(plural(271))), 1214, 0),pred(s3(plural(315)), 0),ass(cond(conseq(271), 9), 0),ass(cond(conseq(271), 9), 1),ass(cond(conseq(271), 9), 2),pred(s2(plural(294)), 0),pred(s1(plural(294)), 0),pred(294, 0),pred(s2(plural(293)), 0),pred(s1(plural(293)), 0),pred(293, 0),pred(s3(plural(274)), 0),qe(s3(plural(271))),qe(s1(plural(271))),neg(neg(270)),pred(269, 0),and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268))))))))))))))),qu(cond(axiom(190), 0), imp(cond(axiom(190), 0))),qu(cond(axiom(188), 0), imp(cond(axiom(188), 0))),qu(cond(axiom(186), 0), imp(cond(axiom(186), 0))),qu(cond(axiom(184), 0), imp(cond(axiom(184), 0))),qu(cond(axiom(162), 0), imp(cond(axiom(162), 0))),qu(cond(axiom(160), 0), imp(cond(axiom(160), 0))),qu(cond(axiom(149), 0), imp(cond(axiom(149), 0))),qu(cond(axiom(147), 0), imp(cond(axiom(147), 0))),qu(cond(axiom(109), 0), imp(cond(axiom(109), 0))),qu(cond(axiom(99), 0), imp(cond(axiom(99), 0))),qu(cond(axiom(73), 0), imp(cond(axiom(73), 0))),pred(s2(plural(315)), 0),ass(cond(conseq(271), 3), 0),ass(cond(conseq(271), 3), 1),ass(cond(conseq(271), 3), 2),ass(cond(conseq(271), 3), 3),pred(s2(plural(274)), 0),holds(273, 1215, 0),neg(neg(conjunct2(conjunct2(comma_conjunct2(plural(271)))))),pred(conjunct1(conjunct2(comma_conjunct2(plural(271)))), 0),holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0),holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(plural(271)))))), 1211, 0),holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(plural(271)))))), 1210, 0),holds(conjunct1(conjunct2(conjunct2(conjunct2(plural(271))))), 1209, 0),holds(conjunct1(conjunct2(conjunct2(plural(271)))), 1208, 0),holds(conjunct1(conjunct2(plural(271))), 1207, 0),holds(conjunct1(plural(271)), 1206, 0),qe(s2(plural(271))),pred(s2(plural(269)), 0),pred(s1(plural(269)), 0),qu(cond(axiom(178), 0), imp(cond(axiom(178), 0))),qu(cond(axiom(166), 0), imp(cond(axiom(166), 0))),ass(cond(156, 0), 0),qu(cond(axiom(143), 0), imp(cond(axiom(143), 0))),qu(cond(axiom(141), 0), imp(cond(axiom(141), 0))),pred(axiom(137), 2),pred(axiom(137), 1),qu(cond(axiom(61), 0), imp(cond(axiom(61), 0))),pred(s1(plural(315)), 0),pred(313, 0),holds(292, 1231, 0),holds(291, 1230, 0),pred(s1(plural(274)), 0),pred(272, 0),ass(cond(goal(238), 0), 0),ass(cond(goal(238), 0), 1),ass(cond(goal(238), 0), 2),ass(cond(goal(219), 0), 0),ass(cond(goal(219), 0), 1),qu(cond(axiom(194), 0), imp(cond(axiom(194), 0))),qu(cond(axiom(89), 0), imp(cond(axiom(89), 0))),qu(cond(axiom(81), 0), imp(cond(axiom(81), 0))),qu(cond(axiom(53), 0), imp(cond(axiom(53), 0))),qu(cond(axiom(51), 0), imp(cond(axiom(51), 0))),qu(cond(axiom(1), 0), imp(cond(axiom(1), 0))),holds(314, 1247, 0),holds(295, 1236, 0),qu(cond(axiom(176), 0), imp(cond(axiom(176), 0))),qu(cond(axiom(153), 0), imp(cond(axiom(153), 0))),qu(cond(axiom(151), 0), imp(cond(axiom(151), 0))),qu(cond(axiom(145), 0), imp(cond(axiom(145), 0))),qu(cond(axiom(139), 0), imp(cond(axiom(139), 0))),qu(cond(axiom(135), 0), imp(cond(axiom(135), 0))),qu(cond(axiom(133), 0), imp(cond(axiom(133), 0))),qu(cond(axiom(131), 0), imp(cond(axiom(131), 0))),qu(cond(axiom(129), 0), imp(cond(axiom(129), 0))),qu(cond(axiom(127), 0), imp(cond(axiom(127), 0))),qu(cond(axiom(125), 0), imp(cond(axiom(125), 0))),qu(cond(axiom(123), 0), imp(cond(axiom(123), 0))),qu(cond(axiom(121), 0), imp(cond(axiom(121), 0))),qu(cond(axiom(119), 0), imp(cond(axiom(119), 0))),qu(cond(axiom(117), 0), imp(cond(axiom(117), 0))),qu(cond(axiom(115), 0), imp(cond(axiom(115), 0))),qu(cond(axiom(113), 0), imp(cond(axiom(113), 0))),qu(cond(axiom(111), 0), imp(cond(axiom(111), 0))),qu(cond(axiom(107), 0), imp(cond(axiom(107), 0))),qu(cond(axiom(105), 0), imp(cond(axiom(105), 0))),qu(cond(axiom(103), 0), imp(cond(axiom(103), 0))),qu(cond(axiom(101), 0), imp(cond(axiom(101), 0))),qu(cond(axiom(97), 0), imp(cond(axiom(97), 0))),qu(cond(axiom(95), 0), imp(cond(axiom(95), 0))),qu(cond(axiom(93), 0), imp(cond(axiom(93), 0))),qu(cond(axiom(87), 0), imp(cond(axiom(87), 0))),qu(cond(axiom(85), 0), imp(cond(axiom(85), 0))),qu(cond(axiom(83), 0), imp(cond(axiom(83), 0))),qu(cond(axiom(79), 0), imp(cond(axiom(79), 0))),qu(cond(axiom(77), 0), imp(cond(axiom(77), 0))),qu(cond(axiom(75), 0), imp(cond(axiom(75), 0))),qu(cond(axiom(71), 0), imp(cond(axiom(71), 0))),qu(cond(axiom(69), 0), imp(cond(axiom(69), 0))),qu(cond(axiom(67), 0), imp(cond(axiom(67), 0))),qu(cond(axiom(65), 0), imp(cond(axiom(65), 0))),qu(cond(axiom(63), 0), imp(cond(axiom(63), 0))),qu(cond(axiom(59), 0), imp(cond(axiom(59), 0))),qu(cond(axiom(57), 0), imp(cond(axiom(57), 0))),qu(cond(axiom(55), 0), imp(cond(axiom(55), 0))),qu(cond(axiom(49), 0), imp(cond(axiom(49), 0))),qu(cond(axiom(47), 0), imp(cond(axiom(47), 0))),qu(cond(axiom(45), 0), imp(cond(axiom(45), 0))),qu(cond(axiom(43), 0), imp(cond(axiom(43), 0))),qu(cond(axiom(41), 0), imp(cond(axiom(41), 0))),qu(cond(axiom(39), 0), imp(cond(axiom(39), 0))),qu(cond(axiom(37), 0), imp(cond(axiom(37), 0))),qu(cond(axiom(35), 0), imp(cond(axiom(35), 0))),qu(cond(axiom(33), 0), imp(cond(axiom(33), 0))),qu(cond(axiom(31), 0), imp(cond(axiom(31), 0))),qu(cond(axiom(29), 0), imp(cond(axiom(29), 0))),qu(cond(axiom(27), 0), imp(cond(axiom(27), 0))),qu(cond(axiom(25), 0), imp(cond(axiom(25), 0))),qu(cond(axiom(23), 0), imp(cond(axiom(23), 0))),qu(cond(axiom(21), 0), imp(cond(axiom(21), 0))),qu(cond(axiom(19), 0), imp(cond(axiom(19), 0))),qu(cond(axiom(17), 0), imp(cond(axiom(17), 0))),qu(cond(axiom(15), 0), imp(cond(axiom(15), 0))),qu(cond(axiom(13), 0), imp(cond(axiom(13), 0))),qu(cond(axiom(11), 0), imp(cond(axiom(11), 0))),qu(cond(axiom(9), 0), imp(cond(axiom(9), 0))),qu(cond(axiom(7), 0), imp(cond(axiom(7), 0))),pred(axiom(5), 0),qu(cond(axiom(3), 0), imp(cond(axiom(3), 0))),ass(cond(goal(206), 0), 0),ass(cond(goal(206), 0), 1),ass(cond(goal(206), 0), 2),qu(cond(axiom(174), 0), imp(cond(axiom(174), 0))),qu(cond(axiom(192), 0), imp(cond(axiom(192), 0))),qu(cond(axiom(182), 0), imp(cond(axiom(182), 0))),qu(cond(axiom(204), 0), imp(cond(axiom(204), 0))),qu(cond(axiom(172), 0), imp(cond(axiom(172), 0))),qu(cond(axiom(164), 0), imp(cond(axiom(164), 0))),qu(cond(axiom(202), 0), imp(cond(axiom(202), 0))),qu(cond(axiom(170), 0), imp(cond(axiom(170), 0))),qu(cond(axiom(200), 0), imp(cond(axiom(200), 0))),qu(cond(axiom(168), 0), imp(cond(axiom(168), 0))),qu(cond(axiom(198), 0), imp(cond(axiom(198), 0))),qu(cond(axiom(196), 0), imp(cond(axiom(196), 0)))] % 2.08/3.31 =============================================================== % 2.08/3.31 % 2.08/3.31 Combined formula: 159 axiom(s) => conjecture % 2.08/3.31 % 2.08/3.31 % Equality/functions detected -> nanoCoP oracle mode % 2.08/3.31 nanoCoP : % 2.08/3.31 % 1,595,232 inferences, 1.711 CPU in 1.711 seconds (100% CPU, 932607 Lips) % 2.08/3.31 % 2.08/3.31 % nanoCoP proof (equality/functions) % 2.08/3.31 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 2.08/3.31 % 2.08/3.31 % SZS output end Proof %------------------------------------------------------------------------------