%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO649-1 : TPTP v7.5.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n024.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 51.69s 51.74s % Output : CNFRefutation 51.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYO649-1 : TPTP v7.5.0. Released v7.3.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.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 13:28:18 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.43 openjdk version "1.8.0_171" % 0.18/0.43 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.18/0.43 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.18/0.44 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.65 start to proof:theBenchmark % 51.69/51.74 % Version : CSE-F---1.0 % 51.69/51.74 % Problem : theBenchmark.p % 51.69/51.74 % Proof found % 51.69/51.74 % SZS status Theorem for theBenchmark.p % 51.69/51.74 % SZS output start Proof % 51.69/51.74 [2]~P1(f1(a4),a2) % 51.69/51.74 [1]P1(f1(x11),f3(a2)) % 51.69/51.74 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 51.69/51.74 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41))) % 51.69/51.74 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61)))) % 51.69/51.74 [8]P1(f1(x81),a2)+~P1(f1(f5(f5(f5(x81)))),f3(a2))+P2(a2,f1(f5(f5(f5(x81))))) % 51.69/51.74 [12]P1(f1(x121),a2)+~P1(f1(f5(f5(f5(f5(x121))))),f3(a2))+P2(a2,f1(f5(f5(f5(f5(x121)))))) % 51.69/51.74 [19]P1(f1(x191),a2)+~P1(f1(f5(f5(f5(f5(f5(x191)))))),f3(a2))+P2(a2,f1(f5(f5(f5(f5(f5(x191))))))) % 51.69/51.74 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51))) % 51.69/51.74 [9]P3(f5(x91),f5(x91))+~P2(a2,f1(x91))+~P2(f1(x91),f1(f5(x91)))+P2(f1(x91),f1(f5(f5(x91))))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(f5(x91)))) % 51.69/51.74 [7]~P3(f5(x72),f5(x71))+P2(f1(x71),f1(f5(x71)))+P2(f1(x72),f1(f5(x72)))+~P2(a2,f1(x71))+~P2(a2,f1(x72))+~P2(a2,f1(f5(x71)))+~P2(a2,f1(f5(x72))) % 51.69/51.74 [14]P3(f5(x141),f5(x141))+~P2(a2,f1(x141))+~P2(f1(x141),f1(f5(x141)))+~P2(f1(x141),f1(f5(f5(x141))))+~P2(a2,f1(f5(x141)))+P2(f1(x141),f1(f5(f5(f5(x141)))))+~P2(a2,f1(f5(f5(x141))))+~P2(a2,f1(f5(f5(f5(x141))))) % 51.69/51.75 [10]~P3(f5(x102),f5(x101))+P2(f1(x101),f1(f5(x101)))+~P2(a2,f1(x101))+~P2(f1(x102),f1(f5(x102)))+~P2(a2,f1(x102))+~P2(a2,f1(f5(x101)))+~P2(a2,f1(f5(x102)))+P2(f1(x102),f1(f5(f5(x102))))+~P2(a2,f1(f5(f5(x102)))) % 51.69/51.75 [11]~P3(f5(x111),f5(x112))+P2(f1(x111),f1(f5(x111)))+~P2(a2,f1(x111))+~P2(f1(x112),f1(f5(x112)))+~P2(a2,f1(x112))+~P2(a2,f1(f5(x112)))+~P2(a2,f1(f5(x111)))+P2(f1(x112),f1(f5(f5(x112))))+~P2(a2,f1(f5(f5(x112)))) % 51.69/51.75 [20]P3(f5(x201),f5(x201))+~P2(a2,f1(x201))+~P2(f1(x201),f1(f5(x201)))+~P2(f1(x201),f1(f5(f5(x201))))+~P2(a2,f1(f5(x201)))+~P2(f1(x201),f1(f5(f5(f5(x201)))))+~P2(a2,f1(f5(f5(x201))))+P2(f1(x201),f1(f5(f5(f5(f5(x201))))))+~P2(a2,f1(f5(f5(f5(x201)))))+~P2(a2,f1(f5(f5(f5(f5(x201)))))) % 51.69/51.75 [28]P3(f5(x281),f5(x281))+~P2(a2,f1(x281))+~P2(f1(x281),f1(f5(x281)))+~P2(f1(x281),f1(f5(f5(x281))))+~P2(a2,f1(f5(x281)))+~P2(f1(x281),f1(f5(f5(f5(x281)))))+~P2(a2,f1(f5(f5(x281))))+~P2(f1(x281),f1(f5(f5(f5(f5(x281))))))+~P2(a2,f1(f5(f5(f5(x281)))))+~P2(a2,f1(f5(f5(f5(f5(x281))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x281))))))) % 51.69/51.75 [13]~P3(f5(x132),f5(x131))+~P2(f1(x131),f1(f5(x131)))+~P2(a2,f1(x131))+~P2(f1(x132),f1(f5(x132)))+~P2(a2,f1(x132))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x132)))+P2(f1(x131),f1(f5(f5(x131))))+P2(f1(x132),f1(f5(f5(x132))))+~P2(a2,f1(f5(f5(x131))))+~P2(a2,f1(f5(f5(x132)))) % 51.69/51.75 [15]~P3(f5(x151),f5(x152))+P2(f1(x151),f1(f5(x151)))+~P2(a2,f1(x151))+~P2(f1(x152),f1(f5(x152)))+~P2(a2,f1(x152))+~P2(a2,f1(f5(x151)))+~P2(a2,f1(f5(x152)))+~P2(f1(x152),f1(f5(f5(x152))))+~P2(a2,f1(f5(f5(x152))))+P2(f1(x152),f1(f5(f5(f5(x152)))))+~P2(a2,f1(f5(f5(f5(x152))))) % 51.69/51.75 [16]~P3(f5(x162),f5(x161))+P2(f1(x161),f1(f5(x161)))+~P2(a2,f1(x161))+~P2(f1(x162),f1(f5(x162)))+~P2(a2,f1(x162))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(x162)))+~P2(f1(x162),f1(f5(f5(x162))))+~P2(a2,f1(f5(f5(x162))))+P2(f1(x162),f1(f5(f5(f5(x162)))))+~P2(a2,f1(f5(f5(f5(x162))))) % 51.69/51.75 [17]~P3(f5(x171),f5(x172))+~P2(f1(x171),f1(f5(x171)))+~P2(a2,f1(x171))+~P2(f1(x172),f1(f5(x172)))+~P2(a2,f1(x172))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x172)))+P2(f1(x171),f1(f5(f5(x171))))+~P2(f1(x172),f1(f5(f5(x172))))+~P2(a2,f1(f5(f5(x171))))+~P2(a2,f1(f5(f5(x172))))+P2(f1(x172),f1(f5(f5(f5(x172)))))+~P2(a2,f1(f5(f5(f5(x172))))) % 51.69/51.75 [18]~P3(f5(x182),f5(x181))+~P2(f1(x181),f1(f5(x181)))+~P2(a2,f1(x181))+~P2(f1(x182),f1(f5(x182)))+~P2(a2,f1(x182))+~P2(a2,f1(f5(x181)))+~P2(a2,f1(f5(x182)))+P2(f1(x181),f1(f5(f5(x181))))+~P2(f1(x182),f1(f5(f5(x182))))+~P2(a2,f1(f5(f5(x181))))+~P2(a2,f1(f5(f5(x182))))+P2(f1(x182),f1(f5(f5(f5(x182)))))+~P2(a2,f1(f5(f5(f5(x182))))) % 51.69/51.75 [22]~P3(f5(x221),f5(x222))+P2(f1(x221),f1(f5(x221)))+~P2(a2,f1(x221))+~P2(f1(x222),f1(f5(x222)))+~P2(a2,f1(x222))+~P2(a2,f1(f5(x221)))+~P2(a2,f1(f5(x222)))+~P2(f1(x222),f1(f5(f5(x222))))+~P2(a2,f1(f5(f5(x222))))+~P2(f1(x222),f1(f5(f5(f5(x222)))))+~P2(a2,f1(f5(f5(f5(x222)))))+P2(f1(x222),f1(f5(f5(f5(f5(x222))))))+~P2(a2,f1(f5(f5(f5(f5(x222)))))) % 51.69/51.75 [23]~P3(f5(x232),f5(x231))+P2(f1(x231),f1(f5(x231)))+~P2(a2,f1(x231))+~P2(f1(x232),f1(f5(x232)))+~P2(a2,f1(x232))+~P2(a2,f1(f5(x231)))+~P2(a2,f1(f5(x232)))+~P2(f1(x232),f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x232))))+~P2(f1(x232),f1(f5(f5(f5(x232)))))+~P2(a2,f1(f5(f5(f5(x232)))))+P2(f1(x232),f1(f5(f5(f5(f5(x232))))))+~P2(a2,f1(f5(f5(f5(f5(x232)))))) % 51.69/51.75 [29]~P3(f5(x291),f5(x292))+P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(x291))+~P2(f1(x292),f1(f5(x292)))+~P2(a2,f1(x292))+~P2(a2,f1(f5(x291)))+~P2(a2,f1(f5(x292)))+~P2(f1(x292),f1(f5(f5(x292))))+~P2(a2,f1(f5(f5(x292))))+~P2(f1(x292),f1(f5(f5(f5(x292)))))+~P2(a2,f1(f5(f5(f5(x292)))))+~P2(f1(x292),f1(f5(f5(f5(f5(x292))))))+~P2(a2,f1(f5(f5(f5(f5(x292))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x292))))))) % 51.69/51.75 [30]~P3(f5(x302),f5(x301))+P2(f1(x301),f1(f5(x301)))+~P2(a2,f1(x301))+~P2(f1(x302),f1(f5(x302)))+~P2(a2,f1(x302))+~P2(a2,f1(f5(x301)))+~P2(a2,f1(f5(x302)))+~P2(f1(x302),f1(f5(f5(x302))))+~P2(a2,f1(f5(f5(x302))))+~P2(f1(x302),f1(f5(f5(f5(x302)))))+~P2(a2,f1(f5(f5(f5(x302)))))+~P2(f1(x302),f1(f5(f5(f5(f5(x302))))))+~P2(a2,f1(f5(f5(f5(f5(x302))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x302))))))) % 51.69/51.75 [21]~P3(f5(x212),f5(x211))+~P2(f1(x211),f1(f5(x211)))+~P2(a2,f1(x211))+~P2(f1(x212),f1(f5(x212)))+~P2(a2,f1(x212))+~P2(a2,f1(f5(x211)))+~P2(a2,f1(f5(x212)))+~P2(f1(x211),f1(f5(f5(x211))))+~P2(f1(x212),f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x211))))+~P2(a2,f1(f5(f5(x212))))+P2(f1(x211),f1(f5(f5(f5(x211)))))+P2(f1(x212),f1(f5(f5(f5(x212)))))+~P2(a2,f1(f5(f5(f5(x211)))))+~P2(a2,f1(f5(f5(f5(x212))))) % 51.69/51.75 [24]~P3(f5(x241),f5(x242))+~P2(f1(x241),f1(f5(x241)))+~P2(a2,f1(x241))+~P2(f1(x242),f1(f5(x242)))+~P2(a2,f1(x242))+~P2(a2,f1(f5(x241)))+~P2(a2,f1(f5(x242)))+P2(f1(x241),f1(f5(f5(x241))))+~P2(f1(x242),f1(f5(f5(x242))))+~P2(a2,f1(f5(f5(x241))))+~P2(a2,f1(f5(f5(x242))))+~P2(f1(x242),f1(f5(f5(f5(x242)))))+~P2(a2,f1(f5(f5(f5(x242)))))+P2(f1(x242),f1(f5(f5(f5(f5(x242))))))+~P2(a2,f1(f5(f5(f5(f5(x242)))))) % 51.69/51.75 [25]~P3(f5(x252),f5(x251))+~P2(f1(x251),f1(f5(x251)))+~P2(a2,f1(x251))+~P2(f1(x252),f1(f5(x252)))+~P2(a2,f1(x252))+~P2(a2,f1(f5(x251)))+~P2(a2,f1(f5(x252)))+P2(f1(x251),f1(f5(f5(x251))))+~P2(f1(x252),f1(f5(f5(x252))))+~P2(a2,f1(f5(f5(x251))))+~P2(a2,f1(f5(f5(x252))))+~P2(f1(x252),f1(f5(f5(f5(x252)))))+~P2(a2,f1(f5(f5(f5(x252)))))+P2(f1(x252),f1(f5(f5(f5(f5(x252))))))+~P2(a2,f1(f5(f5(f5(f5(x252)))))) % 51.69/51.75 [31]~P3(f5(x311),f5(x312))+~P2(f1(x311),f1(f5(x311)))+~P2(a2,f1(x311))+~P2(f1(x312),f1(f5(x312)))+~P2(a2,f1(x312))+~P2(a2,f1(f5(x311)))+~P2(a2,f1(f5(x312)))+P2(f1(x311),f1(f5(f5(x311))))+~P2(f1(x312),f1(f5(f5(x312))))+~P2(a2,f1(f5(f5(x311))))+~P2(a2,f1(f5(f5(x312))))+~P2(f1(x312),f1(f5(f5(f5(x312)))))+~P2(a2,f1(f5(f5(f5(x312)))))+~P2(f1(x312),f1(f5(f5(f5(f5(x312))))))+~P2(a2,f1(f5(f5(f5(f5(x312))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x312))))))) % 51.69/51.75 [32]~P3(f5(x322),f5(x321))+~P2(f1(x321),f1(f5(x321)))+~P2(a2,f1(x321))+~P2(f1(x322),f1(f5(x322)))+~P2(a2,f1(x322))+~P2(a2,f1(f5(x321)))+~P2(a2,f1(f5(x322)))+P2(f1(x321),f1(f5(f5(x321))))+~P2(f1(x322),f1(f5(f5(x322))))+~P2(a2,f1(f5(f5(x321))))+~P2(a2,f1(f5(f5(x322))))+~P2(f1(x322),f1(f5(f5(f5(x322)))))+~P2(a2,f1(f5(f5(f5(x322)))))+~P2(f1(x322),f1(f5(f5(f5(f5(x322))))))+~P2(a2,f1(f5(f5(f5(f5(x322))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x322))))))) % 51.69/51.75 [26]~P3(f5(x262),f5(x261))+~P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(a2,f1(x262))+~P2(a2,f1(f5(x261)))+~P2(a2,f1(f5(x262)))+~P2(f1(x261),f1(f5(f5(x261))))+~P2(f1(x262),f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x261))))+~P2(a2,f1(f5(f5(x262))))+P2(f1(x261),f1(f5(f5(f5(x261)))))+~P2(f1(x262),f1(f5(f5(f5(x262)))))+~P2(a2,f1(f5(f5(f5(x261)))))+~P2(a2,f1(f5(f5(f5(x262)))))+P2(f1(x262),f1(f5(f5(f5(f5(x262))))))+~P2(a2,f1(f5(f5(f5(f5(x262)))))) % 51.69/51.75 [27]~P3(f5(x271),f5(x272))+~P2(f1(x271),f1(f5(x271)))+~P2(a2,f1(x271))+~P2(f1(x272),f1(f5(x272)))+~P2(a2,f1(x272))+~P2(a2,f1(f5(x272)))+~P2(a2,f1(f5(x271)))+~P2(f1(x271),f1(f5(f5(x271))))+~P2(f1(x272),f1(f5(f5(x272))))+~P2(a2,f1(f5(f5(x272))))+~P2(a2,f1(f5(f5(x271))))+P2(f1(x271),f1(f5(f5(f5(x271)))))+~P2(f1(x272),f1(f5(f5(f5(x272)))))+~P2(a2,f1(f5(f5(f5(x272)))))+~P2(a2,f1(f5(f5(f5(x271)))))+P2(f1(x272),f1(f5(f5(f5(f5(x272))))))+~P2(a2,f1(f5(f5(f5(f5(x272)))))) % 51.69/51.75 [34]~P3(f5(x342),f5(x341))+~P2(f1(x341),f1(f5(x341)))+~P2(a2,f1(x341))+~P2(f1(x342),f1(f5(x342)))+~P2(a2,f1(x342))+~P2(a2,f1(f5(x341)))+~P2(a2,f1(f5(x342)))+~P2(f1(x341),f1(f5(f5(x341))))+~P2(f1(x342),f1(f5(f5(x342))))+~P2(a2,f1(f5(f5(x342))))+~P2(a2,f1(f5(f5(x341))))+P2(f1(x341),f1(f5(f5(f5(x341)))))+~P2(f1(x342),f1(f5(f5(f5(x342)))))+~P2(a2,f1(f5(f5(f5(x341)))))+~P2(a2,f1(f5(f5(f5(x342)))))+~P2(f1(x342),f1(f5(f5(f5(f5(x342))))))+~P2(a2,f1(f5(f5(f5(f5(x342))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x342))))))) % 51.69/51.75 [35]~P3(f5(x351),f5(x352))+~P2(f1(x351),f1(f5(x351)))+~P2(a2,f1(x351))+~P2(f1(x352),f1(f5(x352)))+~P2(a2,f1(x352))+~P2(a2,f1(f5(x352)))+~P2(a2,f1(f5(x351)))+~P2(f1(x351),f1(f5(f5(x351))))+~P2(f1(x352),f1(f5(f5(x352))))+~P2(a2,f1(f5(f5(x351))))+~P2(a2,f1(f5(f5(x352))))+P2(f1(x351),f1(f5(f5(f5(x351)))))+~P2(f1(x352),f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x351)))))+~P2(f1(x352),f1(f5(f5(f5(f5(x352))))))+~P2(a2,f1(f5(f5(f5(f5(x352))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x352))))))) % 51.69/51.75 [33]~P3(f5(x332),f5(x331))+~P2(f1(x331),f1(f5(x331)))+~P2(a2,f1(x331))+~P2(f1(x332),f1(f5(x332)))+~P2(a2,f1(x332))+~P2(a2,f1(f5(x331)))+~P2(a2,f1(f5(x332)))+~P2(f1(x331),f1(f5(f5(x331))))+~P2(f1(x332),f1(f5(f5(x332))))+~P2(a2,f1(f5(f5(x331))))+~P2(a2,f1(f5(f5(x332))))+~P2(f1(x331),f1(f5(f5(f5(x331)))))+~P2(f1(x332),f1(f5(f5(f5(x332)))))+~P2(a2,f1(f5(f5(f5(x331)))))+~P2(a2,f1(f5(f5(f5(x332)))))+P2(f1(x331),f1(f5(f5(f5(f5(x331))))))+P2(f1(x332),f1(f5(f5(f5(f5(x332))))))+~P2(a2,f1(f5(f5(f5(f5(x331))))))+~P2(a2,f1(f5(f5(f5(f5(x332)))))) % 51.69/51.75 [36]~P3(f5(x362),f5(x361))+~P2(f1(x361),f1(f5(x361)))+~P2(a2,f1(x361))+~P2(f1(x362),f1(f5(x362)))+~P2(a2,f1(x362))+~P2(a2,f1(f5(x361)))+~P2(a2,f1(f5(x362)))+~P2(f1(x361),f1(f5(f5(x361))))+~P2(f1(x362),f1(f5(f5(x362))))+~P2(a2,f1(f5(f5(x361))))+~P2(a2,f1(f5(f5(x362))))+~P2(f1(x361),f1(f5(f5(f5(x361)))))+~P2(f1(x362),f1(f5(f5(f5(x362)))))+~P2(a2,f1(f5(f5(f5(x361)))))+~P2(a2,f1(f5(f5(f5(x362)))))+P2(f1(x361),f1(f5(f5(f5(f5(x361))))))+~P2(f1(x362),f1(f5(f5(f5(f5(x362))))))+~P2(a2,f1(f5(f5(f5(f5(x361))))))+~P2(a2,f1(f5(f5(f5(f5(x362))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x362))))))) % 51.69/51.75 [37]~P3(f5(x371),f5(x372))+~P2(f1(x371),f1(f5(x371)))+~P2(a2,f1(x371))+~P2(f1(x372),f1(f5(x372)))+~P2(a2,f1(x372))+~P2(a2,f1(f5(x372)))+~P2(a2,f1(f5(x371)))+~P2(f1(x371),f1(f5(f5(x371))))+~P2(f1(x372),f1(f5(f5(x372))))+~P2(a2,f1(f5(f5(x371))))+~P2(a2,f1(f5(f5(x372))))+~P2(f1(x371),f1(f5(f5(f5(x371)))))+~P2(f1(x372),f1(f5(f5(f5(x372)))))+~P2(a2,f1(f5(f5(f5(x372)))))+~P2(a2,f1(f5(f5(f5(x371)))))+P2(f1(x371),f1(f5(f5(f5(f5(x371))))))+~P2(f1(x372),f1(f5(f5(f5(f5(x372))))))+~P2(a2,f1(f5(f5(f5(f5(x372))))))+~P2(a2,f1(f5(f5(f5(f5(x371))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x372))))))) % 51.69/51.75 [38]~P3(f5(x382),f5(x381))+~P2(f1(x381),f1(f5(x381)))+~P2(f1(x382),f1(f5(x382)))+~P2(a2,f1(x381))+~P2(a2,f1(x382))+~P2(a2,f1(f5(x381)))+~P2(a2,f1(f5(x382)))+~P2(f1(x381),f1(f5(f5(x381))))+~P2(f1(x382),f1(f5(f5(x382))))+~P2(a2,f1(f5(f5(x382))))+~P2(a2,f1(f5(f5(x381))))+~P2(f1(x381),f1(f5(f5(f5(x381)))))+~P2(f1(x382),f1(f5(f5(f5(x382)))))+~P2(a2,f1(f5(f5(f5(x381)))))+~P2(a2,f1(f5(f5(f5(x382)))))+~P2(f1(x381),f1(f5(f5(f5(f5(x381))))))+~P2(f1(x382),f1(f5(f5(f5(f5(x382))))))+~P2(a2,f1(f5(f5(f5(f5(x381))))))+~P2(a2,f1(f5(f5(f5(f5(x382))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x381)))))))+~P2(a2,f1(f5(f5(f5(f5(f5(x382))))))) % 51.69/51.75 cnf(40,plain, % 51.69/51.75 (~P2(a2,f1(x401))+P2(f1(x401),f1(f5(x401)))+~P2(a2,f1(f5(x401)))), % 51.69/51.75 inference(scs_inference,[],[7,5])). % 51.69/51.75 cnf(41,plain, % 51.69/51.75 (P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(a4))), % 51.69/51.75 inference(scs_inference,[],[1,2,40,4])). % 51.69/51.75 cnf(42,plain, % 51.69/51.75 (P2(f1(a4),f1(f5(a4)))), % 51.69/51.75 inference(scs_inference,[],[2,1,41,3])). % 51.69/51.75 cnf(43,plain, % 51.69/51.75 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(a2,f1(f5(f5(a4))))), % 51.69/51.75 inference(scs_inference,[],[1,2,40,4])). % 51.69/51.75 cnf(44,plain, % 51.69/51.75 (P2(f1(f5(a4)),f1(f5(f5(a4))))), % 51.69/51.75 inference(scs_inference,[],[1,2,43,6])). % 51.69/51.75 cnf(45,plain, % 51.69/51.75 (P2(f1(f5(f5(a4))),f1(f5(f5(f5(a4)))))+~P2(a2,f1(f5(f5(a4))))), % 51.69/51.75 inference(scs_inference,[],[1,2,40,8])). % 51.69/51.75 cnf(46,plain, % 51.69/51.75 (P2(f1(f5(f5(a4))),f1(f5(f5(f5(a4)))))), % 51.69/51.75 inference(scs_inference,[],[1,2,45,6])). % 51.69/51.75 cnf(322,plain, % 51.69/51.75 (P2(a2,f1(a4))), % 51.69/51.75 inference(scs_inference,[],[2,1,3])). % 51.69/51.75 cnf(325,plain, % 51.69/51.75 (P2(f1(a4),f1(f5(f5(a4))))+~P2(a2,f1(f5(a4)))+~P2(a2,f1(f5(f5(a4))))), % 51.69/51.75 inference(scs_inference,[],[322,42,9,13])). % 51.69/51.75 cnf(326,plain, % 51.69/51.75 (~P2(a2,f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(a4))))), % 51.69/51.75 inference(scs_inference,[],[1,2,325,4])). % 51.69/51.75 cnf(327,plain, % 51.69/51.75 (P2(f1(a4),f1(f5(f5(a4))))), % 51.69/51.75 inference(scs_inference,[],[1,2,326,6])). % 51.69/51.75 cnf(376,plain, % 51.69/51.75 (P2(a2,f1(f5(a4)))), % 51.69/51.75 inference(scs_inference,[],[1,2,4])). % 51.69/51.75 cnf(377,plain, % 51.69/51.75 (P1(f1(x3771),f3(a2))), % 51.69/51.75 inference(rename_variables,[],[1])). % 51.69/51.75 cnf(379,plain, % 51.69/51.75 (P2(a2,f1(f5(f5(a4))))), % 51.69/51.75 inference(scs_inference,[],[1,377,2,4,6])). % 51.69/51.75 cnf(380,plain, % 51.69/51.75 (P1(f1(x3801),f3(a2))), % 51.69/51.75 inference(rename_variables,[],[1])). % 51.69/51.75 cnf(382,plain, % 51.69/51.75 (P2(a2,f1(f5(f5(f5(a4)))))), % 51.69/51.75 inference(scs_inference,[],[1,377,380,2,4,6,8])). % 51.69/51.75 cnf(383,plain, % 51.69/51.75 (P1(f1(x3831),f3(a2))), % 51.69/51.75 inference(rename_variables,[],[1])). % 51.69/51.75 cnf(385,plain, % 51.69/51.75 (P2(a2,f1(f5(f5(f5(f5(a4))))))), % 51.69/51.75 inference(scs_inference,[],[1,377,380,383,2,4,6,8,12])). % 51.69/51.75 cnf(386,plain, % 51.69/51.75 (P1(f1(x3861),f3(a2))), % 51.69/51.75 inference(rename_variables,[],[1])). % 51.69/51.75 cnf(388,plain, % 51.69/51.75 (P2(a2,f1(f5(f5(f5(f5(f5(a4)))))))), % 51.69/51.75 inference(scs_inference,[],[1,377,380,383,386,2,4,6,8,12,19])). % 51.69/51.75 cnf(393,plain, % 51.69/51.75 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(a4)))))), % 51.69/51.75 inference(scs_inference,[],[1,377,380,383,386,327,44,322,42,2,4,6,8,12,19,9,14])). % 51.69/51.75 cnf(395,plain, % 51.69/51.75 (P2(f1(a4),f1(f5(f5(f5(a4)))))), % 51.69/51.75 inference(scs_inference,[],[379,327,376,322,42,382,393,21])). % 51.69/51.75 cnf(398,plain, % 51.69/51.75 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(f5(a4))))))), % 51.69/51.75 inference(scs_inference,[],[395,46,385,376,379,382,327,42,322,9,20])). % 51.69/51.75 cnf(400,plain, % 51.69/51.75 (P2(f1(a4),f1(f5(f5(f5(f5(a4))))))), % 51.69/51.75 inference(scs_inference,[],[395,379,327,376,322,42,382,385,398,33])). % 51.69/51.75 cnf(403,plain, % 51.69/51.75 ($false), % 51.69/51.75 inference(scs_inference,[],[400,388,395,376,385,327,379,382,322,42,28,38]), % 51.69/51.75 ['proof']). % 51.69/51.75 % SZS output end Proof % 51.69/51.75 % Total time : 51.010000 s %------------------------------------------------------------------------------