%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO652-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 : n006.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:47 EDT 2022 % Result : Unsatisfiable 51.68s 51.75s % Output : CNFRefutation 51.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYO652-1 : TPTP v7.5.0. Released v7.3.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n006.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 14:02:44 EDT 2022 % 0.13/0.33 % CPUTime : % 0.20/0.44 openjdk version "1.8.0_171" % 0.20/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.20/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.20/0.45 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.65 start to proof:theBenchmark % 51.68/51.75 % Version : CSE-F---1.0 % 51.68/51.75 % Problem : theBenchmark.p % 51.68/51.75 % Proof found % 51.68/51.75 % SZS status Theorem for theBenchmark.p % 51.68/51.75 % SZS output start Proof % 51.68/51.75 [2]~P1(f1(a4),a2) % 51.68/51.75 [1]P1(f1(x11),f3(a2)) % 51.68/51.75 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 51.68/51.75 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41))) % 51.68/51.75 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61)))) % 51.68/51.75 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51))) % 51.68/51.75 [7]P3(f5(x71),f5(x71))+~P2(a2,f1(x71))+~P2(f1(x71),f1(f5(x71)))+~P2(a2,f1(f5(x71)))+~P2(a2,f1(f5(f5(x71)))) % 51.68/51.75 [8]~P3(f5(x81),f5(x84))+~P3(f5(x83),f5(x82))+~P3(f5(x84),f5(x83))+P2(f1(x81),f1(f5(x81)))+P2(f1(x82),f1(f5(x82)))+~P2(a2,f1(x81))+P2(f1(x83),f1(f5(x83)))+P2(f1(x84),f1(f5(x84)))+~P2(a2,f1(x82))+~P2(a2,f1(x83))+~P2(a2,f1(x84))+~P2(a2,f1(f5(x81)))+~P2(a2,f1(f5(x82)))+~P2(a2,f1(f5(x83)))+~P2(a2,f1(f5(x84))) % 51.68/51.75 [9]~P3(f5(x91),f5(x94))+~P3(f5(x93),f5(x92))+~P3(f5(x94),f5(x93))+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(f1(x94),f1(f5(x94)))+~P2(a2,f1(x93))+~P2(a2,f1(x94))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(x92)))+~P2(a2,f1(f5(x93)))+~P2(a2,f1(f5(x94)))+~P2(a2,f1(f5(f5(x94)))) % 51.68/51.75 [10]~P3(f5(x101),f5(x103))+~P3(f5(x104),f5(x102))+~P3(f5(x103),f5(x104))+P2(f1(x101),f1(f5(x101)))+P2(f1(x102),f1(f5(x102)))+~P2(a2,f1(x101))+P2(f1(x103),f1(f5(x103)))+~P2(a2,f1(x102))+~P2(f1(x104),f1(f5(x104)))+~P2(a2,f1(x103))+~P2(a2,f1(x104))+~P2(a2,f1(f5(x101)))+~P2(a2,f1(f5(x102)))+~P2(a2,f1(f5(x104)))+~P2(a2,f1(f5(x103)))+~P2(a2,f1(f5(f5(x104)))) % 51.68/51.75 [11]~P3(f5(x111),f5(x113))+~P3(f5(x112),f5(x114))+~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(f1(x114),f1(f5(x114)))+~P2(a2,f1(x113))+~P2(a2,f1(x114))+~P2(a2,f1(f5(x111)))+~P2(a2,f1(f5(x114)))+~P2(a2,f1(f5(x112)))+~P2(a2,f1(f5(x113)))+~P2(a2,f1(f5(f5(x114)))) % 51.68/51.75 [12]~P3(f5(x124),f5(x123))+~P3(f5(x122),f5(x121))+~P3(f5(x123),f5(x122))+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(f1(x124),f1(f5(x124)))+~P2(a2,f1(x123))+~P2(a2,f1(x124))+~P2(a2,f1(f5(x124)))+~P2(a2,f1(f5(x121)))+~P2(a2,f1(f5(x122)))+~P2(a2,f1(f5(x123)))+~P2(a2,f1(f5(f5(x124)))) % 51.68/51.75 [13]~P3(f5(x134),f5(x133))+~P3(f5(x133),f5(x132))+~P3(f5(x131),f5(x134))+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(f1(x134),f1(f5(x134)))+~P2(a2,f1(x133))+~P2(a2,f1(x134))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x132)))+~P2(a2,f1(f5(x133)))+~P2(a2,f1(f5(x134)))+~P2(a2,f1(f5(f5(x133))))+~P2(a2,f1(f5(f5(x134)))) % 51.68/51.75 [14]~P3(f5(x144),f5(x142))+~P3(f5(x142),f5(x143))+~P3(f5(x141),f5(x144))+P2(f1(x141),f1(f5(x141)))+P2(f1(x142),f1(f5(x142)))+~P2(a2,f1(x141))+~P2(f1(x143),f1(f5(x143)))+~P2(a2,f1(x142))+~P2(f1(x144),f1(f5(x144)))+~P2(a2,f1(x143))+~P2(a2,f1(x144))+~P2(a2,f1(f5(x141)))+~P2(a2,f1(f5(x143)))+~P2(a2,f1(f5(x142)))+~P2(a2,f1(f5(x144)))+~P2(a2,f1(f5(f5(x143))))+~P2(a2,f1(f5(f5(x144)))) % 51.68/51.75 [15]~P3(f5(x152),f5(x154))+~P3(f5(x154),f5(x153))+~P3(f5(x151),f5(x152))+P2(f1(x151),f1(f5(x151)))+P2(f1(x152),f1(f5(x152)))+~P2(a2,f1(x151))+~P2(f1(x153),f1(f5(x153)))+~P2(a2,f1(x152))+~P2(f1(x154),f1(f5(x154)))+~P2(a2,f1(x153))+~P2(a2,f1(x154))+~P2(a2,f1(f5(x151)))+~P2(a2,f1(f5(x153)))+~P2(a2,f1(f5(x154)))+~P2(a2,f1(f5(x152)))+~P2(a2,f1(f5(f5(x153))))+~P2(a2,f1(f5(f5(x154)))) % 51.68/51.75 [16]~P3(f5(x164),f5(x162))+~P3(f5(x162),f5(x161))+~P3(f5(x163),f5(x164))+P2(f1(x161),f1(f5(x161)))+P2(f1(x162),f1(f5(x162)))+~P2(a2,f1(x161))+~P2(f1(x163),f1(f5(x163)))+~P2(a2,f1(x162))+~P2(f1(x164),f1(f5(x164)))+~P2(a2,f1(x163))+~P2(a2,f1(x164))+~P2(a2,f1(f5(x163)))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(x162)))+~P2(a2,f1(f5(x164)))+~P2(a2,f1(f5(f5(x163))))+~P2(a2,f1(f5(f5(x164)))) % 51.68/51.75 [17]~P3(f5(x172),f5(x174))+~P3(f5(x174),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(f1(x174),f1(f5(x174)))+~P2(a2,f1(x173))+~P2(a2,f1(x174))+~P2(a2,f1(f5(x173)))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x174)))+~P2(a2,f1(f5(x172)))+~P2(a2,f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(x174)))) % 51.68/51.75 [18]~P3(f5(x182),f5(x181))+~P3(f5(x181),f5(x184))+~P3(f5(x183),f5(x182))+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(f1(x184),f1(f5(x184)))+~P2(a2,f1(x183))+~P2(a2,f1(x184))+~P2(a2,f1(f5(x183)))+~P2(a2,f1(f5(x184)))+~P2(a2,f1(f5(x181)))+~P2(a2,f1(f5(x182)))+~P2(a2,f1(f5(f5(x183))))+~P2(a2,f1(f5(f5(x184)))) % 51.68/51.75 [19]~P3(f5(x191),f5(x194))+~P3(f5(x193),f5(x192))+~P3(f5(x194),f5(x193))+P2(f1(x191),f1(f5(x191)))+~P2(a2,f1(x191))+~P2(f1(x192),f1(f5(x192)))+~P2(f1(x193),f1(f5(x193)))+~P2(a2,f1(x192))+~P2(f1(x194),f1(f5(x194)))+~P2(a2,f1(x193))+~P2(a2,f1(x194))+~P2(a2,f1(f5(x192)))+~P2(a2,f1(f5(x194)))+~P2(a2,f1(f5(x193)))+~P2(a2,f1(f5(x191)))+~P2(a2,f1(f5(f5(x192))))+~P2(a2,f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(x194)))) % 51.68/51.75 [20]~P3(f5(x202),f5(x204))+~P3(f5(x203),f5(x201))+~P3(f5(x204),f5(x203))+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(f1(x204),f1(f5(x204)))+~P2(a2,f1(x203))+~P2(a2,f1(x204))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x204)))+~P2(a2,f1(f5(x203)))+~P2(a2,f1(f5(x202)))+~P2(a2,f1(f5(f5(x202))))+~P2(a2,f1(f5(f5(x203))))+~P2(a2,f1(f5(f5(x204)))) % 51.68/51.75 [21]~P3(f5(x212),f5(x214))+~P3(f5(x211),f5(x213))+~P3(f5(x214),f5(x211))+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(f1(x214),f1(f5(x214)))+~P2(a2,f1(x213))+~P2(a2,f1(x214))+~P2(a2,f1(f5(x213)))+~P2(a2,f1(f5(x214)))+~P2(a2,f1(f5(x211)))+~P2(a2,f1(f5(x212)))+~P2(a2,f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x213))))+~P2(a2,f1(f5(f5(x214)))) % 51.68/51.75 [22]~P3(f5(x222),f5(x221))+~P3(f5(x224),f5(x223))+~P3(f5(x221),f5(x224))+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(f1(x224),f1(f5(x224)))+~P2(a2,f1(x223))+~P2(a2,f1(x224))+~P2(a2,f1(f5(x223)))+~P2(a2,f1(f5(x221)))+~P2(a2,f1(f5(x224)))+~P2(a2,f1(f5(x222)))+~P2(a2,f1(f5(f5(x222))))+~P2(a2,f1(f5(f5(x223))))+~P2(a2,f1(f5(f5(x224)))) % 51.68/51.75 [23]~P3(f5(x231),f5(x234))+~P3(f5(x233),f5(x232))+~P3(f5(x234),f5(x233))+~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(f1(x234),f1(f5(x234)))+~P2(a2,f1(x233))+~P2(a2,f1(x234))+~P2(a2,f1(f5(x233)))+~P2(a2,f1(f5(x234)))+~P2(a2,f1(f5(x232)))+~P2(a2,f1(f5(x231)))+~P2(a2,f1(f5(f5(x231))))+~P2(a2,f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x233))))+~P2(a2,f1(f5(f5(x234)))) % 51.68/51.76 cnf(25,plain, % 51.68/51.76 (P3(f5(f5(a4)),f5(f5(a4)))+~P2(a2,f1(f5(a4)))+P2(f1(f5(a4)),f1(f5(f5(a4))))), % 51.68/51.76 inference(scs_inference,[],[2,1,6,5])). % 51.68/51.76 cnf(27,plain, % 51.68/51.76 (~P3(f5(f5(a4)),f5(f5(a4)))+~P2(a2,f1(f5(a4)))+P2(f1(f5(a4)),f1(f5(f5(a4))))), % 51.68/51.76 inference(scs_inference,[],[2,1,6,8])). % 51.68/51.76 cnf(28,plain, % 51.68/51.76 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P3(f5(f5(a4)),f5(f5(a4)))), % 51.68/51.76 inference(scs_inference,[],[1,2,27,4])). % 51.68/51.76 cnf(29,plain, % 51.68/51.76 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(a2,f1(f5(a4)))), % 51.68/51.76 inference(scs_inference,[],[28,25])). % 51.68/51.76 cnf(30,plain, % 51.68/51.76 (P2(f1(f5(a4)),f1(f5(f5(a4))))), % 51.68/51.76 inference(scs_inference,[],[1,2,29,4])). % 51.68/51.76 cnf(5572,plain, % 51.68/51.76 (P2(a2,f1(a4))), % 51.68/51.76 inference(scs_inference,[],[1,2,3])). % 51.68/51.76 cnf(5573,plain, % 51.68/51.76 (P1(f1(x55731),f3(a2))), % 51.68/51.76 inference(rename_variables,[],[1])). % 51.68/51.76 cnf(5575,plain, % 51.68/51.76 (P2(a2,f1(f5(a4)))), % 51.68/51.76 inference(scs_inference,[],[1,5573,2,3,4])). % 51.68/51.76 cnf(5576,plain, % 51.68/51.76 (P1(f1(x55761),f3(a2))), % 51.68/51.76 inference(rename_variables,[],[1])). % 51.68/51.76 cnf(5578,plain, % 51.68/51.76 (P2(a2,f1(f5(f5(a4))))), % 51.68/51.76 inference(scs_inference,[],[1,5573,5576,2,3,4,6])). % 51.68/51.76 cnf(5583,plain, % 51.68/51.76 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))), % 51.68/51.76 inference(scs_inference,[],[1,5573,5576,30,2,3,4,6,7,5])). % 51.68/51.76 cnf(5586,plain, % 51.68/51.76 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))), % 51.68/51.76 inference(scs_inference,[],[5572,5575,5578,7])). % 51.68/51.76 cnf(5590,plain, % 51.68/51.76 (P3(f5(a4),f5(a4))), % 51.68/51.76 inference(scs_inference,[],[5586,5583])). % 51.68/51.76 cnf(5593,plain, % 51.68/51.76 ($false), % 51.68/51.76 inference(scs_inference,[],[5590,5572,5578,5575,23,8]), % 51.68/51.76 ['proof']). % 51.68/51.76 % SZS output end Proof % 51.68/51.76 % Total time : 51.020000 s %------------------------------------------------------------------------------