%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO648-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 : n013.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.63s 51.74s % Output : CNFRefutation 51.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SYO648-1 : TPTP v7.5.0. Released v7.3.0. % 0.07/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.35 % Computer : n013.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % RAMPerCPU : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 600 % 0.12/0.35 % DateTime : Mon Mar 14 13:18:37 EDT 2022 % 0.12/0.35 % CPUTime : % 0.19/0.46 openjdk version "1.8.0_171" % 0.19/0.46 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.19/0.46 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.19/0.47 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.49/0.69 start to proof:theBenchmark % 51.63/51.74 % Version : CSE-F---1.0 % 51.63/51.74 % Problem : theBenchmark.p % 51.63/51.74 % Proof found % 51.63/51.74 % SZS status Theorem for theBenchmark.p % 51.63/51.74 % SZS output start Proof % 51.63/51.74 [2]~P1(f1(a4),a2) % 51.63/51.74 [1]P1(f1(x11),f3(a2)) % 51.63/51.74 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 51.63/51.74 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41))) % 51.63/51.74 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61)))) % 51.63/51.74 [8]P1(f1(x81),a2)+~P1(f1(f5(f5(f5(x81)))),f3(a2))+P2(a2,f1(f5(f5(f5(x81))))) % 51.63/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.63/51.74 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51))) % 51.63/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.63/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.63/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.63/51.74 [19]P3(f5(x191),f5(x191))+~P2(a2,f1(x191))+~P2(f1(x191),f1(f5(x191)))+~P2(f1(x191),f1(f5(f5(x191))))+~P2(a2,f1(f5(x191)))+~P2(f1(x191),f1(f5(f5(f5(x191)))))+~P2(a2,f1(f5(f5(x191))))+~P2(a2,f1(f5(f5(f5(x191)))))+~P2(a2,f1(f5(f5(f5(f5(x191)))))) % 51.63/51.74 [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.63/51.74 [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.63/51.74 [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.63/51.74 [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.63/51.74 [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.63/51.74 [20]~P3(f5(x201),f5(x202))+P2(f1(x201),f1(f5(x201)))+~P2(a2,f1(x201))+~P2(f1(x202),f1(f5(x202)))+~P2(a2,f1(x202))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x202)))+~P2(f1(x202),f1(f5(f5(x202))))+~P2(a2,f1(f5(f5(x202))))+~P2(f1(x202),f1(f5(f5(f5(x202)))))+~P2(a2,f1(f5(f5(f5(x202)))))+~P2(a2,f1(f5(f5(f5(f5(x202)))))) % 51.63/51.74 [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(x212),f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x212))))+~P2(f1(x212),f1(f5(f5(f5(x212)))))+~P2(a2,f1(f5(f5(f5(x212)))))+~P2(a2,f1(f5(f5(f5(f5(x212)))))) % 51.63/51.74 [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.63/51.74 [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.63/51.74 [23]~P3(f5(x231),f5(x232))+~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(x231),f1(f5(f5(x231))))+~P2(f1(x232),f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x231))))+~P2(a2,f1(f5(f5(x232))))+~P2(f1(x232),f1(f5(f5(f5(x232)))))+~P2(a2,f1(f5(f5(f5(x232)))))+~P2(a2,f1(f5(f5(f5(f5(x232)))))) % 51.63/51.74 [24]~P3(f5(x242),f5(x241))+~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(a2,f1(f5(f5(f5(f5(x242)))))) % 51.63/51.74 [22]~P3(f5(x222),f5(x221))+~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(x221),f1(f5(f5(x221))))+~P2(f1(x222),f1(f5(f5(x222))))+~P2(a2,f1(f5(f5(x221))))+~P2(a2,f1(f5(f5(x222))))+P2(f1(x221),f1(f5(f5(f5(x221)))))+P2(f1(x222),f1(f5(f5(f5(x222)))))+~P2(a2,f1(f5(f5(f5(x221)))))+~P2(a2,f1(f5(f5(f5(x222))))) % 51.63/51.74 [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(x251),f1(f5(f5(f5(x251)))))+~P2(f1(x252),f1(f5(f5(f5(x252)))))+~P2(a2,f1(f5(f5(f5(x251)))))+~P2(a2,f1(f5(f5(f5(x252)))))+~P2(a2,f1(f5(f5(f5(f5(x252)))))) % 51.63/51.74 [26]~P3(f5(x261),f5(x262))+~P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(a2,f1(x262))+~P2(a2,f1(f5(x262)))+~P2(a2,f1(f5(x261)))+~P2(f1(x261),f1(f5(f5(x261))))+~P2(f1(x262),f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x261))))+P2(f1(x261),f1(f5(f5(f5(x261)))))+~P2(f1(x262),f1(f5(f5(f5(x262)))))+~P2(a2,f1(f5(f5(f5(x262)))))+~P2(a2,f1(f5(f5(f5(x261)))))+~P2(a2,f1(f5(f5(f5(f5(x262)))))) % 51.63/51.74 [27]~P3(f5(x272),f5(x271))+~P2(f1(x271),f1(f5(x271)))+~P2(f1(x272),f1(f5(x272)))+~P2(a2,f1(x271))+~P2(a2,f1(x272))+~P2(a2,f1(f5(x271)))+~P2(a2,f1(f5(x272)))+~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(x271)))))+~P2(a2,f1(f5(f5(f5(x272)))))+~P2(a2,f1(f5(f5(f5(f5(x271))))))+~P2(a2,f1(f5(f5(f5(f5(x272)))))) % 51.63/51.74 cnf(29,plain, % 51.63/51.74 (~P2(a2,f1(x291))+P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(f5(x291)))), % 51.63/51.74 inference(scs_inference,[],[7,5])). % 51.63/51.74 cnf(30,plain, % 51.63/51.74 (P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(a4))), % 51.63/51.74 inference(scs_inference,[],[1,2,29,4])). % 51.63/51.74 cnf(31,plain, % 51.63/51.74 (P2(f1(a4),f1(f5(a4)))), % 51.63/51.74 inference(scs_inference,[],[2,1,30,3])). % 51.63/51.74 cnf(32,plain, % 51.63/51.74 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(a2,f1(f5(f5(a4))))), % 51.63/51.74 inference(scs_inference,[],[1,2,29,4])). % 51.63/51.74 cnf(33,plain, % 51.63/51.74 (P2(f1(f5(a4)),f1(f5(f5(a4))))), % 51.63/51.74 inference(scs_inference,[],[1,2,32,6])). % 51.63/51.74 cnf(328,plain, % 51.63/51.74 (P2(a2,f1(a4))), % 51.63/51.74 inference(scs_inference,[],[2,1,3])). % 51.63/51.74 cnf(331,plain, % 51.63/51.74 (P2(f1(a4),f1(f5(f5(a4))))+~P2(a2,f1(f5(a4)))+~P2(a2,f1(f5(f5(a4))))), % 51.63/51.74 inference(scs_inference,[],[328,31,9,13])). % 51.63/51.74 cnf(332,plain, % 51.63/51.74 (~P2(a2,f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(a4))))), % 51.63/51.74 inference(scs_inference,[],[1,2,331,4])). % 51.63/51.74 cnf(333,plain, % 51.63/51.74 (P2(f1(a4),f1(f5(f5(a4))))), % 51.63/51.74 inference(scs_inference,[],[1,2,332,6])). % 51.63/51.74 cnf(466,plain, % 51.63/51.74 (P2(a2,f1(f5(a4)))), % 51.63/51.74 inference(scs_inference,[],[1,2,4])). % 51.63/51.74 cnf(467,plain, % 51.63/51.74 (P1(f1(x4671),f3(a2))), % 51.63/51.74 inference(rename_variables,[],[1])). % 51.63/51.74 cnf(469,plain, % 51.63/51.74 (P2(a2,f1(f5(f5(a4))))), % 51.63/51.74 inference(scs_inference,[],[1,467,2,4,6])). % 51.63/51.74 cnf(470,plain, % 51.63/51.74 (P1(f1(x4701),f3(a2))), % 51.63/51.74 inference(rename_variables,[],[1])). % 51.63/51.74 cnf(472,plain, % 51.63/51.74 (P2(a2,f1(f5(f5(f5(a4)))))), % 51.63/51.74 inference(scs_inference,[],[1,467,470,2,4,6,8])). % 51.63/51.74 cnf(473,plain, % 51.63/51.74 (P1(f1(x4731),f3(a2))), % 51.63/51.74 inference(rename_variables,[],[1])). % 51.63/51.75 cnf(475,plain, % 51.63/51.75 (P2(a2,f1(f5(f5(f5(f5(a4))))))), % 51.63/51.75 inference(scs_inference,[],[1,467,470,473,2,4,6,8,12])). % 51.63/51.75 cnf(480,plain, % 51.63/51.75 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(a4)))))), % 51.63/51.75 inference(scs_inference,[],[1,467,470,473,333,33,328,31,2,4,6,8,12,9,14])). % 51.63/51.75 cnf(482,plain, % 51.63/51.75 (P2(f1(a4),f1(f5(f5(f5(a4)))))), % 51.63/51.75 inference(scs_inference,[],[469,333,466,328,31,472,480,22])). % 51.63/51.75 cnf(485,plain, % 51.63/51.75 ($false), % 51.63/51.75 inference(scs_inference,[],[482,475,466,469,472,333,31,328,19,27]), % 51.63/51.75 ['proof']). % 51.63/51.75 % SZS output end Proof % 51.63/51.75 % Total time : 51.000000 s %------------------------------------------------------------------------------