%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : GEO278+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 : n004.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:10 PM UTC 2026 % Result : Theorem 7.01s 7.60s % Output : Proof 7.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : GEO278+1 : TPTP v9.2.1. Released v4.1.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.16/0.34 % Computer : n004.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 11 11:45:03 EDT 2026 % 0.16/0.34 % CPUTime : % 7.01/7.60 % SZS status Theorem % 7.01/7.60 % SZS output start Proof % 7.01/7.60 % 7.01/7.60 =============================================================== % 7.01/7.60 TPTP Problem: qu(theu(the(231), 1), imp(the(231))) (conjecture with 129 axiom(s)) % 7.01/7.60 Axioms: [and(pred(comma_conjunct2(the(231)), 0), and(pred(comma_conjunct1(the(231)), 0), pred(the(231), 0))),replace(pred(230, 2)),replace(qu(theu(the(230), 1), imp(the(230)))),replace(replace(and(pred(s2(plural(the(230))), 0), and(pred(s1(plural(the(230))), 0), pred(the(230), 0))))),holds(conjunct2(comma_conjunct2(229)), 1097, 0),pred(229, 0),pred(226, 0),qe(s1(plural(224))),qu(cond(axiom(81), 0), imp(cond(axiom(81), 0))),qu(cond(axiom(53), 0), imp(cond(axiom(53), 0))),pred(conjunct1(comma_conjunct2(229)), 0),pred(comma_conjunct1(229), 0),holds(226, 1090, 1),holds(226, 1090, 0),pred(224, 5),qe(s2(plural(224))),replace(pred(228, 2)),replace(qu(theu(the(228), 1), imp(the(228)))),replace(replace(and(pred(comma_conjunct2(the(228)), 0), and(pred(comma_conjunct1(the(228)), 0), pred(the(228), 0))))),replace(pred(227, 2)),replace(qu(theu(the(227), 1), imp(the(227)))),replace(replace(and(pred(s2(plural(the(227))), 0), and(pred(s1(plural(the(227))), 0), pred(the(227), 0))))),pred(225, 4),holds(conjunct2(225), 1088, 0),holds(conjunct1(225), 1087, 0),pred(225, 1),ass(cond(goal(206), 0), 0),ass(cond(goal(206), 0), 1),ass(cond(goal(206), 0), 2),qu(cond(axiom(166), 0), imp(cond(axiom(166), 0))),qu(cond(axiom(63), 0), imp(cond(axiom(63), 0))),qu(cond(axiom(162), 0), imp(cond(axiom(162), 0))),qu(cond(axiom(73), 0), imp(cond(axiom(73), 0))),qu(cond(axiom(79), 0), imp(cond(axiom(79), 0))),qu(cond(axiom(51), 0), imp(cond(axiom(51), 0))),ass(cond(156, 0), 0),qu(cond(axiom(61), 0), imp(cond(axiom(61), 0))),qu(cond(axiom(204), 0), imp(cond(axiom(204), 0))),qu(cond(axiom(182), 0), imp(cond(axiom(182), 0))),qu(cond(axiom(77), 0), imp(cond(axiom(77), 0))),qu(cond(axiom(49), 0), imp(cond(axiom(49), 0))),qu(cond(axiom(164), 0), imp(cond(axiom(164), 0))),qu(cond(axiom(153), 0), imp(cond(axiom(153), 0))),qu(cond(axiom(151), 0), imp(cond(axiom(151), 0))),qu(cond(axiom(149), 0), imp(cond(axiom(149), 0))),qu(cond(axiom(147), 0), imp(cond(axiom(147), 0))),qu(cond(axiom(145), 0), imp(cond(axiom(145), 0))),qu(cond(axiom(143), 0), imp(cond(axiom(143), 0))),qu(cond(axiom(141), 0), imp(cond(axiom(141), 0))),qu(cond(axiom(139), 0), imp(cond(axiom(139), 0))),pred(axiom(137), 2),pred(axiom(137), 1),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(109), 0), imp(cond(axiom(109), 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(99), 0), imp(cond(axiom(99), 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(91), 0), imp(cond(axiom(91), 0))),qu(cond(axiom(89), 0), imp(cond(axiom(89), 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(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(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(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))),qu(cond(axiom(1), 0), imp(cond(axiom(1), 0))),qu(cond(axiom(202), 0), imp(cond(axiom(202), 0))),qu(cond(axiom(184), 0), imp(cond(axiom(184), 0))),qu(cond(axiom(160), 0), imp(cond(axiom(160), 0))),qu(cond(axiom(200), 0), imp(cond(axiom(200), 0))),qu(cond(axiom(198), 0), imp(cond(axiom(198), 0))),qu(cond(axiom(196), 0), imp(cond(axiom(196), 0))),qu(cond(axiom(194), 0), imp(cond(axiom(194), 0))),qu(cond(axiom(192), 0), imp(cond(axiom(192), 0))),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(180), 0), imp(cond(axiom(180), 0))),qu(cond(axiom(178), 0), imp(cond(axiom(178), 0))),qu(cond(axiom(176), 0), imp(cond(axiom(176), 0))),qu(cond(axiom(174), 0), imp(cond(axiom(174), 0))),qu(cond(axiom(172), 0), imp(cond(axiom(172), 0))),qu(cond(axiom(170), 0), imp(cond(axiom(170), 0))),qu(cond(axiom(168), 0), imp(cond(axiom(168), 0)))] % 7.01/7.60 =============================================================== % 7.01/7.60 % 7.01/7.60 Combined formula: 129 axiom(s) => conjecture % 7.01/7.60 % 7.01/7.60 % Equality/functions detected -> nanoCoP oracle mode % 7.01/7.60 nanoCoP : % 7.01/7.60 % 5,262,719 inferences, 6.158 CPU in 6.157 seconds (100% CPU, 854634 Lips) % 7.01/7.60 % 7.01/7.60 % nanoCoP proof (equality/functions) % 7.01/7.60 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 7.01/7.60 % 7.01/7.60 % SZS output end Proof %------------------------------------------------------------------------------