%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO650-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 : n011.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:46 EDT 2022 % Result : Unsatisfiable 52.44s 52.47s % Output : CNFRefutation 52.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYO650-1 : TPTP v7.5.0. Released v7.3.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n011.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % RAMPerCPU : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon Mar 14 13:28:27 EDT 2022 % 0.13/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.52/0.68 start to proof:theBenchmark % 52.44/52.47 % Version : CSE-F---1.0 % 52.44/52.47 % Problem : theBenchmark.p % 52.44/52.47 % Proof found % 52.44/52.47 % SZS status Theorem for theBenchmark.p % 52.44/52.47 % SZS output start Proof % 52.44/52.47 [2]~P1(f1(a4),a2) % 52.44/52.47 [1]P1(f1(x11),f3(a2)) % 52.44/52.47 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 52.44/52.47 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41))) % 52.44/52.47 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61)))) % 52.44/52.47 [7]P1(f1(x71),a2)+~P1(f1(f5(f5(f5(x71)))),f3(a2))+P2(a2,f1(f5(f5(f5(x71))))) % 52.44/52.47 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51))) % 52.44/52.47 [8]P3(f5(x81),f5(x81))+~P2(a2,f1(x81))+~P2(f1(x81),f1(f5(x81)))+P2(f1(x81),f1(f5(f5(x81))))+~P2(a2,f1(f5(x81)))+~P2(a2,f1(f5(f5(x81)))) % 52.44/52.47 [10]P3(f5(x101),f5(x101))+~P2(a2,f1(x101))+~P2(f1(x101),f1(f5(x101)))+~P2(f1(x101),f1(f5(f5(x101))))+~P2(a2,f1(f5(x101)))+~P2(a2,f1(f5(f5(x101))))+~P2(a2,f1(f5(f5(f5(x101))))) % 52.44/52.47 [9]~P3(f5(x92),f5(x91))+~P3(f5(x93),f5(x92))+P2(f1(x91),f1(f5(x91)))+P2(f1(x92),f1(f5(x92)))+~P2(a2,f1(x91))+P2(f1(x93),f1(f5(x93)))+~P2(a2,f1(x92))+~P2(a2,f1(x93))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(x92)))+~P2(a2,f1(f5(x93))) % 52.44/52.47 [11]~P3(f5(x112),f5(x111))+~P3(f5(x113),f5(x112))+P2(f1(x111),f1(f5(x111)))+P2(f1(x112),f1(f5(x112)))+~P2(a2,f1(x111))+~P2(f1(x113),f1(f5(x113)))+~P2(a2,f1(x112))+~P2(a2,f1(x113))+~P2(a2,f1(f5(x111)))+~P2(a2,f1(f5(x112)))+~P2(a2,f1(f5(x113)))+P2(f1(x113),f1(f5(f5(x113))))+~P2(a2,f1(f5(f5(x113)))) % 52.44/52.47 [12]~P3(f5(x122),f5(x123))+~P3(f5(x123),f5(x121))+P2(f1(x121),f1(f5(x121)))+P2(f1(x122),f1(f5(x122)))+~P2(a2,f1(x121))+~P2(f1(x123),f1(f5(x123)))+~P2(a2,f1(x122))+~P2(a2,f1(x123))+~P2(a2,f1(f5(x121)))+~P2(a2,f1(f5(x122)))+~P2(a2,f1(f5(x123)))+P2(f1(x123),f1(f5(f5(x123))))+~P2(a2,f1(f5(f5(x123)))) % 52.44/52.47 [13]~P3(f5(x131),f5(x133))+~P3(f5(x132),f5(x131))+P2(f1(x131),f1(f5(x131)))+P2(f1(x132),f1(f5(x132)))+~P2(a2,f1(x131))+~P2(f1(x133),f1(f5(x133)))+~P2(a2,f1(x132))+~P2(a2,f1(x133))+~P2(a2,f1(f5(x133)))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x132)))+P2(f1(x133),f1(f5(f5(x133))))+~P2(a2,f1(f5(f5(x133)))) % 52.44/52.47 [17]~P3(f5(x172),f5(x171))+~P3(f5(x173),f5(x172))+P2(f1(x171),f1(f5(x171)))+P2(f1(x172),f1(f5(x172)))+~P2(a2,f1(x171))+~P2(f1(x173),f1(f5(x173)))+~P2(a2,f1(x172))+~P2(a2,f1(x173))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x172)))+~P2(a2,f1(f5(x173)))+~P2(f1(x173),f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(f5(x173))))) % 52.44/52.47 [18]~P3(f5(x182),f5(x183))+~P3(f5(x183),f5(x181))+P2(f1(x181),f1(f5(x181)))+P2(f1(x182),f1(f5(x182)))+~P2(a2,f1(x181))+~P2(f1(x183),f1(f5(x183)))+~P2(a2,f1(x182))+~P2(a2,f1(x183))+~P2(a2,f1(f5(x181)))+~P2(a2,f1(f5(x182)))+~P2(a2,f1(f5(x183)))+~P2(f1(x183),f1(f5(f5(x183))))+~P2(a2,f1(f5(f5(x183))))+~P2(a2,f1(f5(f5(f5(x183))))) % 52.44/52.47 [19]~P3(f5(x191),f5(x193))+~P3(f5(x192),f5(x191))+P2(f1(x191),f1(f5(x191)))+P2(f1(x192),f1(f5(x192)))+~P2(a2,f1(x191))+~P2(f1(x193),f1(f5(x193)))+~P2(a2,f1(x192))+~P2(a2,f1(x193))+~P2(a2,f1(f5(x193)))+~P2(a2,f1(f5(x191)))+~P2(a2,f1(f5(x192)))+~P2(f1(x193),f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(f5(x193))))) % 52.44/52.47 [14]~P3(f5(x142),f5(x143))+~P3(f5(x143),f5(x141))+P2(f1(x141),f1(f5(x141)))+~P2(a2,f1(x141))+~P2(f1(x142),f1(f5(x142)))+~P2(f1(x143),f1(f5(x143)))+~P2(a2,f1(x142))+~P2(a2,f1(x143))+~P2(a2,f1(f5(x141)))+~P2(a2,f1(f5(x142)))+~P2(a2,f1(f5(x143)))+P2(f1(x142),f1(f5(f5(x142))))+P2(f1(x143),f1(f5(f5(x143))))+~P2(a2,f1(f5(f5(x142))))+~P2(a2,f1(f5(f5(x143)))) % 52.44/52.47 [15]~P3(f5(x151),f5(x152))+~P3(f5(x153),f5(x151))+P2(f1(x151),f1(f5(x151)))+~P2(a2,f1(x151))+~P2(f1(x152),f1(f5(x152)))+~P2(f1(x153),f1(f5(x153)))+~P2(a2,f1(x152))+~P2(a2,f1(x153))+~P2(a2,f1(f5(x152)))+~P2(a2,f1(f5(x151)))+~P2(a2,f1(f5(x153)))+P2(f1(x152),f1(f5(f5(x152))))+P2(f1(x153),f1(f5(f5(x153))))+~P2(a2,f1(f5(f5(x152))))+~P2(a2,f1(f5(f5(x153)))) % 52.44/52.47 [16]~P3(f5(x161),f5(x163))+~P3(f5(x163),f5(x162))+P2(f1(x161),f1(f5(x161)))+~P2(a2,f1(x161))+~P2(f1(x162),f1(f5(x162)))+~P2(f1(x163),f1(f5(x163)))+~P2(a2,f1(x162))+~P2(a2,f1(x163))+~P2(a2,f1(f5(x162)))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(x163)))+P2(f1(x162),f1(f5(f5(x162))))+P2(f1(x163),f1(f5(f5(x163))))+~P2(a2,f1(f5(f5(x162))))+~P2(a2,f1(f5(f5(x163)))) % 52.44/52.47 [21]~P3(f5(x212),f5(x211))+~P3(f5(x213),f5(x212))+P2(f1(x211),f1(f5(x211)))+~P2(a2,f1(x211))+~P2(f1(x212),f1(f5(x212)))+~P2(f1(x213),f1(f5(x213)))+~P2(a2,f1(x212))+~P2(a2,f1(x213))+~P2(a2,f1(f5(x211)))+~P2(a2,f1(f5(x212)))+~P2(a2,f1(f5(x213)))+P2(f1(x212),f1(f5(f5(x212))))+~P2(f1(x213),f1(f5(f5(x213))))+~P2(a2,f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x213))))+~P2(a2,f1(f5(f5(f5(x213))))) % 52.44/52.47 [22]~P3(f5(x222),f5(x223))+~P3(f5(x223),f5(x221))+P2(f1(x221),f1(f5(x221)))+~P2(a2,f1(x221))+~P2(f1(x222),f1(f5(x222)))+~P2(f1(x223),f1(f5(x223)))+~P2(a2,f1(x222))+~P2(a2,f1(x223))+~P2(a2,f1(f5(x221)))+~P2(a2,f1(f5(x222)))+~P2(a2,f1(f5(x223)))+P2(f1(x222),f1(f5(f5(x222))))+~P2(f1(x223),f1(f5(f5(x223))))+~P2(a2,f1(f5(f5(x222))))+~P2(a2,f1(f5(f5(x223))))+~P2(a2,f1(f5(f5(f5(x223))))) % 52.44/52.47 [23]~P3(f5(x231),f5(x232))+~P3(f5(x233),f5(x231))+P2(f1(x231),f1(f5(x231)))+~P2(a2,f1(x231))+~P2(f1(x232),f1(f5(x232)))+~P2(f1(x233),f1(f5(x233)))+~P2(a2,f1(x232))+~P2(a2,f1(x233))+~P2(a2,f1(f5(x232)))+~P2(a2,f1(f5(x231)))+~P2(a2,f1(f5(x233)))+P2(f1(x232),f1(f5(f5(x232))))+~P2(f1(x233),f1(f5(f5(x233))))+~P2(a2,f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x233))))+~P2(a2,f1(f5(f5(f5(x233))))) % 52.44/52.47 [24]~P3(f5(x241),f5(x243))+~P3(f5(x243),f5(x242))+P2(f1(x241),f1(f5(x241)))+~P2(a2,f1(x241))+~P2(f1(x242),f1(f5(x242)))+~P2(f1(x243),f1(f5(x243)))+~P2(a2,f1(x242))+~P2(a2,f1(x243))+~P2(a2,f1(f5(x242)))+~P2(a2,f1(f5(x241)))+~P2(a2,f1(f5(x243)))+P2(f1(x242),f1(f5(f5(x242))))+~P2(f1(x243),f1(f5(f5(x243))))+~P2(a2,f1(f5(f5(x242))))+~P2(a2,f1(f5(f5(x243))))+~P2(a2,f1(f5(f5(f5(x243))))) % 52.44/52.47 [25]~P3(f5(x251),f5(x253))+~P3(f5(x252),f5(x251))+P2(f1(x251),f1(f5(x251)))+~P2(a2,f1(x251))+~P2(f1(x252),f1(f5(x252)))+~P2(f1(x253),f1(f5(x253)))+~P2(a2,f1(x252))+~P2(a2,f1(x253))+~P2(a2,f1(f5(x253)))+~P2(a2,f1(f5(x251)))+~P2(a2,f1(f5(x252)))+P2(f1(x252),f1(f5(f5(x252))))+~P2(f1(x253),f1(f5(f5(x253))))+~P2(a2,f1(f5(f5(x253))))+~P2(a2,f1(f5(f5(x252))))+~P2(a2,f1(f5(f5(f5(x253))))) % 52.44/52.47 [26]~P3(f5(x261),f5(x262))+~P3(f5(x262),f5(x263))+P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(f1(x263),f1(f5(x263)))+~P2(a2,f1(x262))+~P2(a2,f1(x263))+~P2(a2,f1(f5(x263)))+~P2(a2,f1(f5(x261)))+~P2(a2,f1(f5(x262)))+P2(f1(x262),f1(f5(f5(x262))))+~P2(f1(x263),f1(f5(f5(x263))))+~P2(a2,f1(f5(f5(x263))))+~P2(a2,f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(f5(x263))))) % 52.44/52.47 [20]~P3(f5(x202),f5(x203))+~P3(f5(x203),f5(x201))+~P2(f1(x201),f1(f5(x201)))+~P2(a2,f1(x201))+~P2(f1(x202),f1(f5(x202)))+~P2(f1(x203),f1(f5(x203)))+~P2(a2,f1(x202))+~P2(a2,f1(x203))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x202)))+~P2(a2,f1(f5(x203)))+P2(f1(x201),f1(f5(f5(x201))))+P2(f1(x202),f1(f5(f5(x202))))+P2(f1(x203),f1(f5(f5(x203))))+~P2(a2,f1(f5(f5(x201))))+~P2(a2,f1(f5(f5(x202))))+~P2(a2,f1(f5(f5(x203)))) % 52.44/52.47 [30]~P3(f5(x302),f5(x301))+~P3(f5(x303),f5(x302))+P2(f1(x301),f1(f5(x301)))+~P2(a2,f1(x301))+~P2(f1(x302),f1(f5(x302)))+~P2(f1(x303),f1(f5(x303)))+~P2(a2,f1(x302))+~P2(a2,f1(x303))+~P2(a2,f1(f5(x303)))+~P2(a2,f1(f5(x302)))+~P2(a2,f1(f5(x301)))+~P2(f1(x302),f1(f5(f5(x302))))+~P2(f1(x303),f1(f5(f5(x303))))+~P2(a2,f1(f5(f5(x302))))+~P2(a2,f1(f5(f5(x303))))+~P2(a2,f1(f5(f5(f5(x302)))))+~P2(a2,f1(f5(f5(f5(x303))))) % 52.44/52.47 [31]~P3(f5(x311),f5(x312))+~P3(f5(x313),f5(x311))+P2(f1(x311),f1(f5(x311)))+~P2(a2,f1(x311))+~P2(f1(x312),f1(f5(x312)))+~P2(f1(x313),f1(f5(x313)))+~P2(a2,f1(x312))+~P2(a2,f1(x313))+~P2(a2,f1(f5(x313)))+~P2(a2,f1(f5(x311)))+~P2(a2,f1(f5(x312)))+~P2(f1(x312),f1(f5(f5(x312))))+~P2(f1(x313),f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(x312))))+~P2(a2,f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(f5(x312)))))+~P2(a2,f1(f5(f5(f5(x313))))) % 52.44/52.47 [32]~P3(f5(x321),f5(x323))+~P3(f5(x323),f5(x322))+P2(f1(x321),f1(f5(x321)))+~P2(a2,f1(x321))+~P2(f1(x322),f1(f5(x322)))+~P2(f1(x323),f1(f5(x323)))+~P2(a2,f1(x322))+~P2(a2,f1(x323))+~P2(a2,f1(f5(x323)))+~P2(a2,f1(f5(x321)))+~P2(a2,f1(f5(x322)))+~P2(f1(x322),f1(f5(f5(x322))))+~P2(f1(x323),f1(f5(f5(x323))))+~P2(a2,f1(f5(f5(x322))))+~P2(a2,f1(f5(f5(x323))))+~P2(a2,f1(f5(f5(f5(x322)))))+~P2(a2,f1(f5(f5(f5(x323))))) % 52.44/52.47 [27]~P3(f5(x272),f5(x271))+~P3(f5(x273),f5(x272))+~P2(f1(x271),f1(f5(x271)))+~P2(a2,f1(x271))+~P2(f1(x272),f1(f5(x272)))+~P2(f1(x273),f1(f5(x273)))+~P2(a2,f1(x272))+~P2(a2,f1(x273))+~P2(a2,f1(f5(x271)))+~P2(a2,f1(f5(x272)))+~P2(a2,f1(f5(x273)))+P2(f1(x271),f1(f5(f5(x271))))+P2(f1(x272),f1(f5(f5(x272))))+~P2(f1(x273),f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(x271))))+~P2(a2,f1(f5(f5(x272))))+~P2(a2,f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(f5(x273))))) % 52.44/52.47 [28]~P3(f5(x282),f5(x283))+~P3(f5(x283),f5(x281))+~P2(f1(x281),f1(f5(x281)))+~P2(a2,f1(x281))+~P2(f1(x282),f1(f5(x282)))+~P2(f1(x283),f1(f5(x283)))+~P2(a2,f1(x282))+~P2(a2,f1(x283))+~P2(a2,f1(f5(x281)))+~P2(a2,f1(f5(x282)))+~P2(a2,f1(f5(x283)))+P2(f1(x281),f1(f5(f5(x281))))+P2(f1(x282),f1(f5(f5(x282))))+~P2(f1(x283),f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(x281))))+~P2(a2,f1(f5(f5(x282))))+~P2(a2,f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(f5(x283))))) % 52.44/52.47 [29]~P3(f5(x291),f5(x292))+~P3(f5(x292),f5(x293))+~P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(x291))+~P2(f1(x292),f1(f5(x292)))+~P2(f1(x293),f1(f5(x293)))+~P2(a2,f1(x292))+~P2(a2,f1(x293))+~P2(a2,f1(f5(x293)))+~P2(a2,f1(f5(x291)))+~P2(a2,f1(f5(x292)))+P2(f1(x291),f1(f5(f5(x291))))+P2(f1(x292),f1(f5(f5(x292))))+~P2(f1(x293),f1(f5(f5(x293))))+~P2(a2,f1(f5(f5(x293))))+~P2(a2,f1(f5(f5(x291))))+~P2(a2,f1(f5(f5(x292))))+~P2(a2,f1(f5(f5(f5(x293))))) % 52.44/52.47 [33]~P3(f5(x333),f5(x332))+~P3(f5(x332),f5(x331))+~P2(f1(x331),f1(f5(x331)))+~P2(a2,f1(x331))+~P2(f1(x332),f1(f5(x332)))+~P2(f1(x333),f1(f5(x333)))+~P2(a2,f1(x332))+~P2(a2,f1(x333))+~P2(a2,f1(f5(x331)))+~P2(a2,f1(f5(x332)))+~P2(a2,f1(f5(x333)))+P2(f1(x331),f1(f5(f5(x331))))+~P2(f1(x332),f1(f5(f5(x332))))+~P2(f1(x333),f1(f5(f5(x333))))+~P2(a2,f1(f5(f5(x331))))+~P2(a2,f1(f5(f5(x332))))+~P2(a2,f1(f5(f5(x333))))+~P2(a2,f1(f5(f5(f5(x332)))))+~P2(a2,f1(f5(f5(f5(x333))))) % 52.44/52.47 [34]~P3(f5(x341),f5(x342))+~P3(f5(x343),f5(x341))+~P2(f1(x341),f1(f5(x341)))+~P2(a2,f1(x341))+~P2(f1(x342),f1(f5(x342)))+~P2(f1(x343),f1(f5(x343)))+~P2(a2,f1(x342))+~P2(a2,f1(x343))+~P2(a2,f1(f5(x341)))+~P2(a2,f1(f5(x343)))+~P2(a2,f1(f5(x342)))+P2(f1(x341),f1(f5(f5(x341))))+~P2(f1(x342),f1(f5(f5(x342))))+~P2(f1(x343),f1(f5(f5(x343))))+~P2(a2,f1(f5(f5(x342))))+~P2(a2,f1(f5(f5(x341))))+~P2(a2,f1(f5(f5(x343))))+~P2(a2,f1(f5(f5(f5(x342)))))+~P2(a2,f1(f5(f5(f5(x343))))) % 52.44/52.47 [35]~P3(f5(x351),f5(x353))+~P3(f5(x353),f5(x352))+~P2(f1(x351),f1(f5(x351)))+~P2(a2,f1(x351))+~P2(f1(x352),f1(f5(x352)))+~P2(f1(x353),f1(f5(x353)))+~P2(a2,f1(x352))+~P2(a2,f1(x353))+~P2(a2,f1(f5(x351)))+~P2(a2,f1(f5(x353)))+~P2(a2,f1(f5(x352)))+P2(f1(x351),f1(f5(f5(x351))))+~P2(f1(x352),f1(f5(f5(x352))))+~P2(f1(x353),f1(f5(f5(x353))))+~P2(a2,f1(f5(f5(x352))))+~P2(a2,f1(f5(f5(x351))))+~P2(a2,f1(f5(f5(x353))))+~P2(a2,f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x353))))) % 52.44/52.47 [36]~P3(f5(x362),f5(x361))+~P3(f5(x363),f5(x362))+~P2(f1(x361),f1(f5(x361)))+~P2(a2,f1(x361))+~P2(f1(x362),f1(f5(x362)))+~P2(f1(x363),f1(f5(x363)))+~P2(a2,f1(x362))+~P2(a2,f1(x363))+~P2(a2,f1(f5(x363)))+~P2(a2,f1(f5(x362)))+~P2(a2,f1(f5(x361)))+~P2(f1(x361),f1(f5(f5(x361))))+~P2(f1(x362),f1(f5(f5(x362))))+~P2(f1(x363),f1(f5(f5(x363))))+~P2(a2,f1(f5(f5(x361))))+~P2(a2,f1(f5(f5(x362))))+~P2(a2,f1(f5(f5(x363))))+~P2(a2,f1(f5(f5(f5(x361)))))+~P2(a2,f1(f5(f5(f5(x362)))))+~P2(a2,f1(f5(f5(f5(x363))))) % 52.44/52.47 cnf(43,plain, % 52.44/52.47 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))), % 52.44/52.47 inference(scs_inference,[],[2,1,5,3])). % 52.44/52.47 cnf(44,plain, % 52.44/52.47 (P2(f1(a4),f1(f5(a4)))+P3(f5(a4),f5(a4))), % 52.44/52.47 inference(scs_inference,[],[1,2,43,4])). % 52.44/52.47 cnf(70,plain, % 52.44/52.47 (P2(a2,f1(a4))), % 52.44/52.47 inference(scs_inference,[],[1,2,3])). % 52.44/52.47 cnf(71,plain, % 52.44/52.47 (P1(f1(x711),f3(a2))), % 52.44/52.47 inference(rename_variables,[],[1])). % 52.44/52.47 cnf(73,plain, % 52.44/52.47 (P2(a2,f1(f5(a4)))), % 52.44/52.47 inference(scs_inference,[],[1,71,2,3,4])). % 52.44/52.47 cnf(74,plain, % 52.44/52.47 (P1(f1(x741),f3(a2))), % 52.44/52.47 inference(rename_variables,[],[1])). % 52.44/52.47 cnf(76,plain, % 52.44/52.47 (P2(a2,f1(f5(f5(a4))))), % 52.44/52.47 inference(scs_inference,[],[1,71,74,2,3,4,6])). % 52.44/52.47 cnf(77,plain, % 52.44/52.47 (P1(f1(x771),f3(a2))), % 52.44/52.47 inference(rename_variables,[],[1])). % 52.44/52.47 cnf(79,plain, % 52.44/52.47 (P2(a2,f1(f5(f5(f5(a4)))))), % 52.44/52.47 inference(scs_inference,[],[1,71,74,77,2,3,4,6,7])). % 52.44/52.47 cnf(85,plain, % 52.44/52.47 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))), % 52.44/52.47 inference(scs_inference,[],[70,73,76,8])). % 52.44/52.47 cnf(86,plain, % 52.44/52.47 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))), % 52.44/52.47 inference(scs_inference,[],[79,70,73,76,10])). % 52.44/52.47 cnf(122,plain, % 52.44/52.47 (~P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))), % 52.44/52.47 inference(scs_inference,[],[70,73,9])). % 52.44/52.47 cnf(150,plain, % 52.44/52.47 (~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))), % 52.44/52.47 inference(scs_inference,[],[73,76,70,79,86,36])). % 52.44/52.47 cnf(166,plain, % 52.44/52.47 (~P2(f1(a4),f1(f5(f5(a4))))+P3(f5(a4),f5(a4))), % 52.44/52.47 inference(scs_inference,[],[70,73,150,5])). % 52.44/52.47 cnf(182,plain, % 52.44/52.47 (P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))), % 52.44/52.47 inference(scs_inference,[],[166,122])). % 52.44/52.47 cnf(198,plain, % 52.44/52.47 (~P2(f1(a4),f1(f5(f5(a4))))), % 52.44/52.47 inference(scs_inference,[],[182,150])). % 52.44/52.47 cnf(199,plain, % 52.44/52.47 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))), % 52.44/52.47 inference(scs_inference,[],[198,85])). % 52.44/52.47 cnf(204,plain, % 52.44/52.47 (~P2(f1(a4),f1(f5(a4)))), % 52.44/52.47 inference(scs_inference,[],[198,70,73,76,20,199])). % 52.44/52.47 cnf(207,plain, % 52.44/52.47 (P3(f5(a4),f5(a4))), % 52.44/52.47 inference(scs_inference,[],[204,44])). % 52.44/52.47 cnf(208,plain, % 52.44/52.47 (~P3(f5(a4),f5(a4))), % 52.44/52.47 inference(scs_inference,[],[204,122])). % 52.44/52.47 cnf(210,plain, % 52.44/52.47 ($false), % 52.44/52.47 inference(scs_inference,[],[207,208]), % 52.44/52.47 ['proof']). % 52.44/52.47 % SZS output end Proof % 52.44/52.47 % Total time : 51.710000 s %------------------------------------------------------------------------------