%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : CSR037+2 : TPTP v9.2.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n003.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 08:16:00 PM UTC 2026 % Result : Theorem 1.50s 2.44s % Output : Proof 1.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.14 % Problem : CSR037+2 : TPTP v9.2.1. Released v3.4.0. % 0.11/0.15 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.17/0.37 % Computer : n003.cluster.edu % 0.17/0.37 % Model : x86_64 x86_64 % 0.17/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.37 % Memory : 8042.1875MB % 0.17/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.37 % CPULimit : 300 % 0.17/0.37 % WCLimit : 300 % 0.17/0.37 % DateTime : Tue May 12 15:45:57 EDT 2026 % 0.17/0.37 % CPUTime : % 1.50/2.44 % SZS status Theorem % 1.50/2.45 % SZS output start Proof % 1.50/2.45 % 1.50/2.45 =============================================================== % 1.50/2.45 TPTP Problem: query87 (conjecture with 1131 axiom(s)) % 1.50/2.45 Axioms: [ax1_1,ax1_2,ax1_3,ax1_4,ax1_5,ax1_6,ax1_7,ax1_8,ax1_9,ax1_10,ax1_11,ax1_12,ax1_13,ax1_14,ax1_15,ax1_16,ax1_17,ax1_18,ax1_19,ax1_20,ax1_21,ax1_22,ax1_23,ax1_24,ax1_25,ax1_26,ax1_27,ax1_28,ax1_29,ax1_30,ax1_31,ax1_32,ax1_33,ax1_34,ax1_35,ax1_36,ax1_37,ax1_38,ax1_39,ax1_40,ax1_41,ax1_42,ax1_43,ax1_44,ax1_45,ax1_46,ax1_47,ax1_48,ax1_49,ax1_50,ax1_51,ax1_52,ax1_53,ax1_54,ax1_55,ax1_56,ax1_57,ax1_58,ax1_59,ax1_60,ax1_61,ax1_62,ax1_63,ax1_64,ax1_65,ax1_66,ax1_67,ax1_68,ax1_69,ax1_70,ax1_71,ax1_72,ax1_73,ax1_74,ax1_75,ax1_76,ax1_77,ax1_78,ax1_79,ax1_80,ax1_81,ax1_82,ax1_83,ax1_84,ax1_85,ax1_86,ax1_87,ax1_88,ax1_89,ax1_90,ax1_91,ax1_92,ax1_93,ax1_94,ax1_95,ax1_96,ax1_97,ax1_98,ax1_99,ax1_100,ax1_101,ax1_102,ax1_103,ax1_104,ax1_105,ax1_106,ax1_107,ax1_108,ax1_109,ax1_110,ax1_111,ax1_112,ax1_113,ax1_114,ax1_115,ax1_116,ax1_117,ax1_118,ax1_119,ax1_120,ax1_121,ax1_122,ax1_123,ax1_124,ax1_125,ax1_126,ax1_127,ax1_128,ax1_129,ax1_130,ax1_131,ax1_132,ax1_133,ax1_134,ax1_135,ax1_136,ax1_137,ax1_138,ax1_139,ax1_140,ax1_141,ax1_142,ax1_143,ax1_144,ax1_145,ax1_146,ax1_147,ax1_148,ax1_149,ax1_150,ax1_151,ax1_152,ax1_153,ax1_154,ax1_155,ax1_156,ax1_157,ax1_158,ax1_159,ax1_160,ax1_161,ax1_162,ax1_163,ax1_164,ax1_165,ax1_166,ax1_167,ax1_168,ax1_169,ax1_170,ax1_171,ax1_172,ax1_173,ax1_174,ax1_175,ax1_176,ax1_177,ax1_178,ax1_179,ax1_180,ax1_181,ax1_182,ax1_183,ax1_184,ax1_185,ax1_186,ax1_187,ax1_188,ax1_189,ax1_190,ax1_191,ax1_192,ax1_193,ax1_194,ax1_195,ax1_196,ax1_197,ax1_198,ax1_199,ax1_200,ax1_201,ax1_202,ax1_203,ax1_204,ax1_205,ax1_206,ax1_207,ax1_208,ax1_209,ax1_210,ax1_211,ax1_212,ax1_213,ax1_214,ax1_215,ax1_216,ax1_217,ax1_218,ax1_219,ax1_220,ax1_221,ax1_222,ax1_223,ax1_224,ax1_225,ax1_226,ax1_227,ax1_228,ax1_229,ax1_230,ax1_231,ax1_232,ax1_233,ax1_234,ax1_235,ax1_236,ax1_237,ax1_238,ax1_239,ax1_240,ax1_241,ax1_242,ax1_243,ax1_244,ax1_245,ax1_246,ax1_247,ax1_248,ax1_249,ax1_250,ax1_251,ax1_252,ax1_253,ax1_254,ax1_255,ax1_256,ax1_257,ax1_258,ax1_259,ax1_260,ax1_261,ax1_262,ax1_263,ax1_264,ax1_265,ax1_266,ax1_267,ax1_268,ax1_269,ax1_270,ax1_271,ax1_272,ax1_273,ax1_274,ax1_275,ax1_276,ax1_277,ax1_278,ax1_279,ax1_280,ax1_281,ax1_282,ax1_283,ax1_284,ax1_285,ax1_286,ax1_287,ax1_288,ax1_289,ax1_290,ax1_291,ax1_292,ax1_293,ax1_294,ax1_295,ax1_296,ax1_297,ax1_298,ax1_299,ax1_300,ax1_301,ax1_302,ax1_303,ax1_304,ax1_305,ax1_306,ax1_307,ax1_308,ax1_309,ax1_310,ax1_311,ax1_312,ax1_313,ax1_314,ax1_315,ax1_316,ax1_317,ax1_318,ax1_319,ax1_320,ax1_321,ax1_322,ax1_323,ax1_324,ax1_325,ax1_326,ax1_327,ax1_328,ax1_329,ax1_330,ax1_331,ax1_332,ax1_333,ax1_334,ax1_335,ax1_336,ax1_337,ax1_338,ax1_339,ax1_340,ax1_341,ax1_342,ax1_343,ax1_344,ax1_345,ax1_346,ax1_347,ax1_348,ax1_349,ax1_350,ax1_351,ax1_352,ax1_353,ax1_354,ax1_355,ax1_356,ax1_357,ax1_358,ax1_359,ax1_360,ax1_361,ax1_362,ax1_363,ax1_364,ax1_365,ax1_366,ax1_367,ax1_368,ax1_369,ax1_370,ax1_371,ax1_372,ax1_373,ax1_374,ax1_375,ax1_376,ax1_377,ax1_378,ax1_379,ax1_380,ax1_381,ax1_382,ax1_383,ax1_384,ax1_385,ax1_386,ax1_387,ax1_388,ax1_389,ax1_390,ax1_391,ax1_392,ax1_393,ax1_394,ax1_395,ax1_396,ax1_397,ax1_398,ax1_399,ax1_400,ax1_401,ax1_402,ax1_403,ax1_404,ax1_405,ax1_406,ax1_407,ax1_408,ax1_409,ax1_410,ax1_411,ax1_412,ax1_413,ax1_414,ax1_415,ax1_416,ax1_417,ax1_418,ax1_419,ax1_420,ax1_421,ax1_422,ax1_423,ax1_424,ax1_425,ax1_426,ax1_427,ax1_428,ax1_429,ax1_430,ax1_431,ax1_432,ax1_433,ax1_434,ax1_435,ax1_436,ax1_437,ax1_438,ax1_439,ax1_440,ax1_441,ax1_442,ax1_443,ax1_444,ax1_445,ax1_446,ax1_447,ax1_448,ax1_449,ax1_450,ax1_451,ax1_452,ax1_453,ax1_454,ax1_455,ax1_456,ax1_457,ax1_458,ax1_459,ax1_460,ax1_461,ax1_462,ax1_463,ax1_464,ax1_465,ax1_466,ax1_467,ax1_468,ax1_469,ax1_470,ax1_471,ax1_472,ax1_473,ax1_474,ax1_475,ax1_476,ax1_477,ax1_478,ax1_479,ax1_480,ax1_481,ax1_482,ax1_483,ax1_484,ax1_485,ax1_486,ax1_487,ax1_488,ax1_489,ax1_490,ax1_491,ax1_492,ax1_493,ax1_494,ax1_495,ax1_496,ax1_497,ax1_498,ax1_499,ax1_500,ax1_501,ax1_502,ax1_503,ax1_504,ax1_505,ax1_506,ax1_507,ax1_508,ax1_509,ax1_510,ax1_511,ax1_512,ax1_513,ax1_514,ax1_515,ax1_516,ax1_517,ax1_518,ax1_519,ax1_520,ax1_521,ax1_522,ax1_523,ax1_524,ax1_525,ax1_526,ax1_527,ax1_528,ax1_529,ax1_530,ax1_531,ax1_532,ax1_533,ax1_534,ax1_535,ax1_536,ax1_537,ax1_538,ax1_539,ax1_540,ax1_541,ax1_542,ax1_543,ax1_544,ax1_545,ax1_546,ax1_547,ax1_548,ax1_549,ax1_550,ax1_551,ax1_552,ax1_553,ax1_554,ax1_555,ax1_556,ax1_557,ax1_558,ax1_559,ax1_560,ax1_561,ax1_562,ax1_563,ax1_564,ax1_565,ax1_566,ax1_567,ax1_568,ax1_569,ax1_570,ax1_571,ax1_572,ax1_573,ax1_574,ax1_575,ax1_576,ax1_577,ax1_578,ax1_579,ax1_580,ax1_581,ax1_582,ax1_583,ax1_584,ax1_585,ax1_586,ax1_587,ax1_588,ax1_589,ax1_590,ax1_591,ax1_592,ax1_593,ax1_594,ax1_595,ax1_596,ax1_597,ax1_598,ax1_599,ax1_600,ax1_601,ax1_602,ax1_603,ax1_604,ax1_605,ax1_606,ax1_607,ax1_608,ax1_609,ax1_610,ax1_611,ax1_612,ax1_613,ax1_614,ax1_615,ax1_616,ax1_617,ax1_618,ax1_619,ax1_620,ax1_621,ax1_622,ax1_623,ax1_624,ax1_625,ax1_626,ax1_627,ax1_628,ax1_629,ax1_630,ax1_631,ax1_632,ax1_633,ax1_634,ax1_635,ax1_636,ax1_637,ax1_638,ax1_639,ax1_640,ax1_641,ax1_642,ax1_643,ax1_644,ax1_645,ax1_646,ax1_647,ax1_648,ax1_649,ax1_650,ax1_651,ax1_652,ax1_653,ax1_654,ax1_655,ax1_656,ax1_657,ax1_658,ax1_659,ax1_660,ax1_661,ax1_662,ax1_663,ax1_664,ax1_665,ax1_666,ax1_667,ax1_668,ax1_669,ax1_670,ax1_671,ax1_672,ax1_673,ax1_674,ax1_675,ax1_676,ax1_677,ax1_678,ax1_679,ax1_680,ax1_681,ax1_682,ax1_683,ax1_684,ax1_685,ax1_686,ax1_687,ax1_688,ax1_689,ax1_690,ax1_691,ax1_692,ax1_693,ax1_694,ax1_695,ax1_696,ax1_697,ax1_698,ax1_699,ax1_700,ax1_701,ax1_702,ax1_703,ax1_704,ax1_705,ax1_706,ax1_707,ax1_708,ax1_709,ax1_710,ax1_711,ax1_712,ax1_713,ax1_714,ax1_715,ax1_716,ax1_717,ax1_718,ax1_719,ax1_720,ax1_721,ax1_722,ax1_723,ax1_724,ax1_725,ax1_726,ax1_727,ax1_728,ax1_729,ax1_730,ax1_731,ax1_732,ax1_733,ax1_734,ax1_735,ax1_736,ax1_737,ax1_738,ax1_739,ax1_740,ax1_741,ax1_742,ax1_743,ax1_744,ax1_745,ax1_746,ax1_747,ax1_748,ax1_749,ax1_750,ax1_751,ax1_752,ax1_753,ax1_754,ax1_755,ax1_756,ax1_757,ax1_758,ax1_759,ax1_760,ax1_761,ax1_762,ax1_763,ax1_764,ax1_765,ax1_766,ax1_767,ax1_768,ax1_769,ax1_770,ax1_771,ax1_772,ax1_773,ax1_774,ax1_775,ax1_776,ax1_777,ax1_778,ax1_779,ax1_780,ax1_781,ax1_782,ax1_783,ax1_784,ax1_785,ax1_786,ax1_787,ax1_788,ax1_789,ax1_790,ax1_791,ax1_792,ax1_793,ax1_794,ax1_795,ax1_796,ax1_797,ax1_798,ax1_799,ax1_800,ax1_801,ax1_802,ax1_803,ax1_804,ax1_805,ax1_806,ax1_807,ax1_808,ax1_809,ax1_810,ax1_811,ax1_812,ax1_813,ax1_814,ax1_815,ax1_816,ax1_817,ax1_818,ax1_819,ax1_820,ax1_821,ax1_822,ax1_823,ax1_824,ax1_825,ax1_826,ax1_827,ax1_828,ax1_829,ax1_830,ax1_831,ax1_832,ax1_833,ax1_834,ax1_835,ax1_836,ax1_837,ax1_838,ax1_839,ax1_840,ax1_841,ax1_842,ax1_843,ax1_844,ax1_845,ax1_846,ax1_847,ax1_848,ax1_849,ax1_850,ax1_851,ax1_852,ax1_853,ax1_854,ax1_855,ax1_856,ax1_857,ax1_858,ax1_859,ax1_860,ax1_861,ax1_862,ax1_863,ax1_864,ax1_865,ax1_866,ax1_867,ax1_868,ax1_869,ax1_870,ax1_871,ax1_872,ax1_873,ax1_874,ax1_875,ax1_876,ax1_877,ax1_878,ax1_879,ax1_880,ax1_881,ax1_882,ax1_883,ax1_884,ax1_885,ax1_886,ax1_887,ax1_888,ax1_889,ax1_890,ax1_891,ax1_892,ax1_893,ax1_894,ax1_895,ax1_896,ax1_897,ax1_898,ax1_899,ax1_900,ax1_901,ax1_902,ax1_903,ax1_904,ax1_905,ax1_906,ax1_907,ax1_908,ax1_909,ax1_910,ax1_911,ax1_912,ax1_913,ax1_914,ax1_915,ax1_916,ax1_917,ax1_918,ax1_919,ax1_920,ax1_921,ax1_922,ax1_923,ax1_924,ax1_925,ax1_926,ax1_927,ax1_928,ax1_929,ax1_930,ax1_931,ax1_932,ax1_933,ax1_934,ax1_935,ax1_936,ax1_937,ax1_938,ax1_939,ax1_940,ax1_941,ax1_942,ax1_943,ax1_944,ax1_945,ax1_946,ax1_947,ax1_948,ax1_949,ax1_950,ax1_951,ax1_952,ax1_953,ax1_954,ax1_955,ax1_956,ax1_957,ax1_958,ax1_959,ax1_960,ax1_961,ax1_962,ax1_963,ax1_964,ax1_965,ax1_966,ax1_967,ax1_968,ax1_969,ax1_970,ax1_971,ax1_972,ax1_973,ax1_974,ax1_975,ax1_976,ax1_977,ax1_978,ax1_979,ax1_980,ax1_981,ax1_982,ax1_983,ax1_984,ax1_985,ax1_986,ax1_987,ax1_988,ax1_989,ax1_990,ax1_991,ax1_992,ax1_993,ax1_994,ax1_995,ax1_996,ax1_997,ax1_998,ax1_999,ax1_1000,ax1_1001,ax1_1002,ax1_1003,ax1_1004,ax1_1005,ax1_1006,ax1_1007,ax1_1008,ax1_1009,ax1_1010,ax1_1011,ax1_1012,ax1_1013,ax1_1014,ax1_1015,ax1_1016,ax1_1017,ax1_1018,ax1_1019,ax1_1020,ax1_1021,ax1_1022,ax1_1023,ax1_1024,ax1_1025,ax1_1026,ax1_1027,ax1_1028,ax1_1029,ax1_1030,ax1_1031,ax1_1032,ax1_1033,ax1_1034,ax1_1035,ax1_1036,ax1_1037,ax1_1038,ax1_1039,ax1_1040,ax1_1041,ax1_1042,ax1_1043,ax1_1044,ax1_1045,ax1_1046,ax1_1047,ax1_1048,ax1_1049,ax1_1050,ax1_1051,ax1_1052,ax1_1053,ax1_1054,ax1_1055,ax1_1056,ax1_1057,ax1_1058,ax1_1059,ax1_1060,ax1_1061,ax1_1062,ax1_1063,ax1_1064,ax1_1065,ax1_1066,ax1_1067,ax1_1068,ax1_1069,ax1_1070,ax1_1071,ax1_1072,ax1_1073,ax1_1074,ax1_1075,ax1_1076,ax1_1077,ax1_1078,ax1_1079,ax1_1080,ax1_1081,ax1_1082,ax1_1083,ax1_1084,ax1_1085,ax1_1086,ax1_1087,ax1_1088,ax1_1089,ax1_1090,ax1_1091,ax1_1092,ax1_1093,ax1_1094,ax1_1095,ax1_1096,ax1_1097,ax1_1098,ax1_1099,ax1_1100,ax1_1101,ax1_1102,ax1_1103,ax1_1104,ax1_1105,ax1_1106,ax1_1107,ax1_1108,ax1_1109,ax1_1110,ax1_1111,ax1_1112,ax1_1113,ax1_1114,ax1_1115,ax1_1116,ax1_1117,ax1_1118,ax1_1119,ax1_1120,ax1_1121,ax1_1122,ax1_1123,ax1_1124,ax1_1125,ax1_1126,ax1_1127,ax1_1128,ax1_1129,ax1_1130,ax1_1131] % 1.50/2.45 =============================================================== % 1.50/2.45 % 1.50/2.45 Combined formula: 1131 axiom(s) => conjecture % 1.50/2.45 % 1.50/2.45 % Equality/functions detected -> nanoCoP oracle mode % 1.50/2.45 nanoCoP : % 1.50/2.45 % 242,049 inferences, 0.608 CPU in 0.608 seconds (100% CPU, 398296 Lips) % 1.50/2.45 % 1.50/2.45 % nanoCoP proof (equality/functions) % 1.50/2.45 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 1.50/2.45 % 1.50/2.45 % SZS output end Proof %------------------------------------------------------------------------------