%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO674-1 : TPTP v7.5.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n026.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 : 600s % DateTime : Tue Mar 29 01:05:50 EDT 2022 % Result : Unsatisfiable 1.60s 1.67s % Output : CNFRefutation 1.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYO674-1 : TPTP v7.5.0. Released v7.3.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Mar 14 17:16:08 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.43 openjdk version "1.8.0_171" % 0.19/0.43 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.19/0.43 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.19/0.44 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.51/0.71 start to proof:theBenchmark % 1.60/1.67 % Version : CSE-F---1.0 % 1.60/1.67 % Problem : theBenchmark.p % 1.60/1.67 % Proof found % 1.60/1.67 % SZS status Theorem for theBenchmark.p % 1.60/1.67 % SZS output start Proof % 1.60/1.67 [2]~P1(f1(a4),a2) % 1.60/1.67 [1]P1(f1(x11),f3(f3(f3(a2)))) % 1.60/1.67 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 1.60/1.67 [4]P1(f1(x41),f3(a2))+P2(f3(a2),f1(x41))+~P1(f1(x41),f3(f3(a2))) % 1.60/1.67 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+~P2(a2,f1(f5(x51))) % 1.60/1.67 [6]P1(f1(x61),a2)+~P1(f1(f5(x61)),f3(a2))+P2(a2,f1(f5(x61))) % 1.60/1.67 [7]P3(f5(x71),f5(x71))+~P2(f3(a2),f1(x71))+~P2(f3(a2),f1(f5(x71))) % 1.60/1.67 [8]P1(f1(x81),f3(a2))+~P1(f1(f5(x81)),f3(f3(a2)))+P2(f3(a2),f1(f5(x81))) % 1.60/1.67 [10]P3(f5(x101),f5(x101))+~P2(f3(f3(a2)),f1(x101))+~P2(f3(f3(a2)),f1(f5(x101))) % 1.60/1.67 [9]P1(f1(x91),f3(f3(a2)))+P2(f3(f3(a2)),f1(x91))+~P1(f1(x91),f3(f3(f3(a2)))) % 1.60/1.67 [11]P2(f3(f3(a2)),f1(f5(x111)))+P1(f1(x111),f3(f3(a2)))+~P1(f1(f5(x111)),f3(f3(f3(a2)))) % 1.60/1.67 [12]~P3(f5(x126),f5(x125))+~P3(f5(x125),f5(x123))+~P3(f5(x124),f5(x121))+~P3(f5(x123),f5(x122))+~P3(f5(x122),f5(x124))+~P2(a2,f1(x121))+~P2(a2,f1(x122))+~P2(a2,f1(x123))+~P2(a2,f1(x124))+~P2(a2,f1(x125))+~P2(a2,f1(x126))+~P2(a2,f1(f5(x121)))+~P2(a2,f1(f5(x122)))+~P2(a2,f1(f5(x123)))+~P2(a2,f1(f5(x124)))+~P2(a2,f1(f5(x125)))+~P2(a2,f1(f5(x126))) % 1.60/1.67 [13]~P3(f5(x131),f5(x132))+~P3(f5(x132),f5(x133))+~P3(f5(x133),f5(x134))+~P3(f5(x134),f5(x135))+~P3(f5(x135),f5(x136))+~P2(f3(a2),f1(x133))+~P2(f3(a2),f1(x136))+~P2(f3(a2),f1(x135))+~P2(f3(a2),f1(x134))+~P2(f3(a2),f1(x132))+~P2(f3(a2),f1(x131))+~P2(f3(a2),f1(f5(x131)))+~P2(f3(a2),f1(f5(x132)))+~P2(f3(a2),f1(f5(x133)))+~P2(f3(a2),f1(f5(x134)))+~P2(f3(a2),f1(f5(x135)))+~P2(f3(a2),f1(f5(x136))) % 1.60/1.67 [14]~P3(f5(x141),f5(x142))+~P3(f5(x143),f5(x141))+~P3(f5(x144),f5(x143))+~P3(f5(x145),f5(x144))+~P3(f5(x146),f5(x145))+~P2(f3(f3(a2)),f1(x145))+~P2(f3(f3(a2)),f1(x146))+~P2(f3(f3(a2)),f1(x142))+~P2(f3(f3(a2)),f1(x144))+~P2(f3(f3(a2)),f1(x143))+~P2(f3(f3(a2)),f1(x141))+~P2(f3(f3(a2)),f1(f5(x141)))+~P2(f3(f3(a2)),f1(f5(x142)))+~P2(f3(f3(a2)),f1(f5(x143)))+~P2(f3(f3(a2)),f1(f5(x144)))+~P2(f3(f3(a2)),f1(f5(x145)))+~P2(f3(f3(a2)),f1(f5(x146))) % 1.60/1.67 cnf(15,plain, % 1.60/1.67 (P1(f1(x151),f3(f3(a2)))+P2(f3(f3(a2)),f1(x151))), % 1.60/1.67 inference(scs_inference,[],[1,9])). % 1.60/1.67 cnf(17,plain, % 1.60/1.67 (P1(f1(x171),f3(f3(a2)))+P2(f3(f3(a2)),f1(f5(x171)))), % 1.60/1.67 inference(scs_inference,[],[1,9,4,11])). % 1.60/1.67 cnf(19,plain, % 1.60/1.67 (P2(f3(f3(a2)),f1(x191))+P1(f1(x191),f3(a2))+P2(f3(a2),f1(x191))), % 1.60/1.67 inference(scs_inference,[],[15,4])). % 1.60/1.67 cnf(21,plain, % 1.60/1.67 (P2(a2,f1(a4))+~P1(f1(f5(a4)),f3(f3(a2)))+P2(f3(a2),f1(f5(a4)))), % 1.60/1.67 inference(scs_inference,[],[2,3,8])). % 1.60/1.67 cnf(23,plain, % 1.60/1.67 (P2(f3(f3(a2)),f1(f5(a4)))+P2(f3(a2),f1(f5(a4)))+P2(a2,f1(a4))), % 1.60/1.67 inference(scs_inference,[],[21,15])). % 1.60/1.67 cnf(26,plain, % 1.60/1.67 (P1(f1(x261),f3(f3(a2)))+P3(f5(x261),f5(x261))+~P2(f3(f3(a2)),f1(f5(x261)))), % 1.60/1.67 inference(scs_inference,[],[15,10])). % 1.60/1.67 cnf(27,plain, % 1.60/1.67 (P3(f5(x271),f5(x271))+P1(f1(x271),f3(f3(a2)))), % 1.60/1.67 inference(scs_inference,[],[26,17])). % 1.60/1.67 cnf(28,plain, % 1.60/1.67 (P2(f3(f3(a2)),f1(f5(x281)))+P1(f1(x281),f3(a2))+P2(f3(a2),f1(f5(x281)))), % 1.60/1.67 inference(scs_inference,[],[15,8])). % 1.60/1.67 cnf(30,plain, % 1.60/1.67 (P2(f3(f3(a2)),f1(f5(x301)))+P1(f1(x301),f3(a2))+P2(f3(a2),f1(x301))), % 1.60/1.67 inference(scs_inference,[],[17,4])). % 1.60/1.67 cnf(31,plain, % 1.60/1.67 (P1(f1(x311),f3(f3(a2)))+~P3(f5(f5(x311)),f5(f5(x311)))+~P2(f3(f3(a2)),f1(f5(f5(x311))))), % 1.60/1.67 inference(scs_inference,[],[17,14])). % 1.60/1.67 cnf(32,plain, % 1.60/1.67 (P1(f1(x321),f3(f3(a2)))+~P2(f3(f3(a2)),f1(f5(x321)))+~P2(f3(f3(a2)),f1(f5(f5(x321))))), % 1.60/1.67 inference(scs_inference,[],[31,10])). % 1.60/1.67 cnf(37,plain, % 1.60/1.67 (~P2(f3(f3(a2)),f1(f5(f5(x371))))+P1(f1(x371),f3(f3(a2)))), % 1.60/1.67 inference(scs_inference,[],[17,32])). % 1.60/1.67 cnf(40,plain, % 1.60/1.67 (P2(f3(f3(a2)),f1(f5(f5(a4))))+P2(f3(a2),f1(f5(a4)))+P2(a2,f1(a4))), % 1.60/1.67 inference(scs_inference,[],[17,21])). % 1.60/1.67 cnf(52,plain, % 1.60/1.67 (P1(f1(x521),f3(f3(a2)))+P1(f1(f5(x521)),f3(a2))+P2(f3(a2),f1(f5(f5(x521))))), % 1.60/1.67 inference(scs_inference,[],[37,28])). % 1.60/1.67 cnf(58,plain, % 1.60/1.67 (~P3(f5(a4),f5(a4))+~P2(a2,f1(a4))+~P1(f1(f5(a4)),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[2,6,12])). % 1.60/1.68 cnf(59,plain, % 1.60/1.68 (P2(f3(a2),f1(a4))+P2(a2,f1(a4))+~P1(f1(a4),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[2,4,3])). % 1.60/1.68 cnf(65,plain, % 1.60/1.68 (~P1(f1(f5(a4)),f3(a2))+~P2(a2,f1(a4))+~P2(a2,f1(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[5,58])). % 1.60/1.68 cnf(66,plain, % 1.60/1.68 (~P2(a2,f1(a4))+~P1(f1(f5(a4)),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[2,65,6])). % 1.60/1.68 cnf(67,plain, % 1.60/1.68 (~P2(a2,f1(a4))+P2(f3(a2),f1(f5(a4)))+~P1(f1(f5(a4)),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[66,4])). % 1.60/1.68 cnf(70,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(a4)))+~P1(f1(f5(a4)),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[67,21])). % 1.60/1.68 cnf(77,plain, % 1.60/1.68 (~P1(f1(f5(a4)),f3(a2))+~P1(f1(a4),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[2,66,3])). % 1.60/1.68 cnf(79,plain, % 1.60/1.68 (~P2(a2,f1(a4))+~P1(f1(f5(f5(a4))),f3(f3(a2)))+P2(f3(a2),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[66,8])). % 1.60/1.68 cnf(80,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(a4)))+P2(f3(f3(a2)),f1(f5(a4)))+~P1(f1(f5(a4)),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[66,23])). % 1.60/1.68 cnf(81,plain, % 1.60/1.68 (P2(f3(f3(a2)),f1(f5(a4)))+P2(f3(a2),f1(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[80,19])). % 1.60/1.68 cnf(82,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(a4)))+~P3(f5(f5(a4)),f5(f5(a4)))+~P2(f3(f3(a2)),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[81,14])). % 1.60/1.68 cnf(86,plain, % 1.60/1.68 (P2(f3(f3(a2)),f1(f5(f5(a4))))+P2(f3(a2),f1(f5(a4)))+~P2(a2,f1(a4))), % 1.60/1.68 inference(scs_inference,[],[66,30])). % 1.60/1.68 cnf(87,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(a4)))+P2(f3(f3(a2)),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[86,40])). % 1.60/1.68 cnf(126,plain, % 1.60/1.68 (P1(f1(a4),f3(f3(a2)))+P2(f3(a2),f1(f5(f5(a4))))+~P2(a2,f1(a4))), % 1.60/1.68 inference(scs_inference,[],[66,52])). % 1.60/1.68 cnf(131,plain, % 1.60/1.68 (~P1(f1(a4),f3(a2))+P2(f3(f3(a2)),f1(f5(f5(a4))))+P2(f3(a2),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[77,28])). % 1.60/1.68 cnf(144,plain, % 1.60/1.68 (~P1(f1(a4),f3(a2))+P1(f1(a4),f3(f3(a2)))+P2(f3(a2),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[77,52])). % 1.60/1.68 cnf(147,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(a4)))+P3(f5(f5(a4)),f5(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[70,27])). % 1.60/1.68 cnf(153,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(a4)))+~P2(f3(f3(a2)),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[147,82])). % 1.60/1.68 cnf(156,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[87,153])). % 1.60/1.68 cnf(157,plain, % 1.60/1.68 (P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))), % 1.60/1.68 inference(scs_inference,[],[156,7])). % 1.60/1.68 cnf(172,plain, % 1.60/1.68 (~P2(f3(a2),f1(a4))), % 1.60/1.68 inference(scs_inference,[],[156,157,13])). % 1.60/1.68 cnf(173,plain, % 1.60/1.68 (~P1(f1(a4),f3(f3(a2)))+P2(a2,f1(a4))), % 1.60/1.68 inference(scs_inference,[],[172,59])). % 1.60/1.68 cnf(179,plain, % 1.60/1.68 (P2(a2,f1(a4))+P2(f3(f3(a2)),f1(a4))), % 1.60/1.68 inference(scs_inference,[],[173,15])). % 1.60/1.68 cnf(232,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(f5(a4))))+~P1(f1(a4),f3(a2))+P2(a2,f1(a4))), % 1.60/1.68 inference(scs_inference,[],[173,144])). % 1.60/1.68 cnf(238,plain, % 1.60/1.68 (P2(a2,f1(a4))+~P3(f5(a4),f5(a4))+~P2(f3(f3(a2)),f1(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[179,14])). % 1.60/1.68 cnf(239,plain, % 1.60/1.68 (P2(a2,f1(a4))+~P2(f3(f3(a2)),f1(a4))+~P2(f3(f3(a2)),f1(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[238,10])). % 1.60/1.68 cnf(240,plain, % 1.60/1.68 (P2(a2,f1(a4))+~P2(f3(f3(a2)),f1(a4))+P1(f1(a4),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[172,239,30])). % 1.60/1.68 cnf(241,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(f5(a4))))+P2(a2,f1(a4))+~P2(f3(f3(a2)),f1(a4))), % 1.60/1.68 inference(scs_inference,[],[240,232])). % 1.60/1.68 cnf(242,plain, % 1.60/1.68 (P2(a2,f1(a4))+~P2(f3(f3(a2)),f1(a4))+P3(f5(f5(a4)),f5(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[156,241,7])). % 1.60/1.68 cnf(243,plain, % 1.60/1.68 (P3(f5(f5(a4)),f5(f5(a4)))+P2(a2,f1(a4))), % 1.60/1.68 inference(scs_inference,[],[242,179])). % 1.60/1.68 cnf(244,plain, % 1.60/1.68 (P3(f5(f5(a4)),f5(f5(a4)))+~P1(f1(f5(a4)),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[243,66])). % 1.60/1.68 cnf(245,plain, % 1.60/1.68 (P3(f5(f5(a4)),f5(f5(a4)))+~P1(f1(f5(f5(a4))),f3(f3(a2)))+P2(f3(a2),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[244,8])). % 1.60/1.68 cnf(246,plain, % 1.60/1.68 (~P1(f1(f5(f5(a4))),f3(f3(a2)))+P3(f5(f5(a4)),f5(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[156,245,7])). % 1.60/1.68 cnf(270,plain, % 1.60/1.68 (~P2(f3(f3(a2)),f1(f5(a4)))+P2(a2,f1(a4))), % 1.60/1.68 inference(scs_inference,[],[179,239])). % 1.60/1.68 cnf(271,plain, % 1.60/1.68 (P2(a2,f1(a4))+P1(f1(a4),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[270,17])). % 1.60/1.68 cnf(272,plain, % 1.60/1.68 (P2(a2,f1(a4))), % 1.60/1.68 inference(scs_inference,[],[271,173])). % 1.60/1.68 cnf(274,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(f5(a4))))+~P1(f1(f5(f5(a4))),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[272,79])). % 1.60/1.68 cnf(280,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(f5(a4))))+P1(f1(a4),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[272,126])). % 1.60/1.68 cnf(282,plain, % 1.60/1.68 (P1(f1(a4),f3(f3(a2)))+~P3(f5(f5(a4)),f5(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[156,280,13])). % 1.60/1.68 cnf(283,plain, % 1.60/1.68 (~P3(f5(f5(a4)),f5(f5(a4)))+P1(f1(a4),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[172,282,4])). % 1.60/1.68 cnf(284,plain, % 1.60/1.68 (P1(f1(a4),f3(a2))+~P1(f1(f5(f5(a4))),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[283,246])). % 1.60/1.68 cnf(285,plain, % 1.60/1.68 (P1(f1(a4),f3(a2))+P2(f3(f3(a2)),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[284,15])). % 1.60/1.68 cnf(286,plain, % 1.60/1.68 (P1(f1(a4),f3(a2))+P1(f1(a4),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[285,37])). % 1.60/1.68 cnf(287,plain, % 1.60/1.68 (P1(f1(a4),f3(a2))), % 1.60/1.68 inference(scs_inference,[],[172,286,4])). % 1.60/1.68 cnf(290,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(f5(a4))))+P2(f3(f3(a2)),f1(f5(f5(a4))))), % 1.60/1.68 inference(scs_inference,[],[287,131])). % 1.60/1.68 cnf(296,plain, % 1.60/1.68 (~P1(f1(f5(f5(a4))),f3(f3(a2)))+~P3(f5(f5(a4)),f5(f5(a4)))), % 1.60/1.68 inference(scs_inference,[],[156,274,13])). % 1.60/1.68 cnf(299,plain, % 1.60/1.68 (P2(f3(a2),f1(f5(f5(a4))))+~P3(f5(f5(f5(a4))),f5(f5(f5(a4))))+~P2(f3(f3(a2)),f1(f5(f5(f5(a4)))))), % 1.60/1.68 inference(scs_inference,[],[290,14])). % 1.60/1.68 cnf(300,plain, % 1.60/1.68 (~P1(f1(f5(f5(a4))),f3(f3(a2)))), % 1.60/1.68 inference(scs_inference,[],[296,246])). % 1.60/1.68 cnf(309,plain, % 1.60/1.68 ($false), % 1.60/1.68 inference(scs_inference,[],[156,300,17,27,299,7,13]), % 1.60/1.68 ['proof']). % 1.60/1.68 % SZS output end Proof % 1.60/1.68 % Total time : 0.900000 s %------------------------------------------------------------------------------