%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO657-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 : n029.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:48 EDT 2022 % Result : Unsatisfiable 227.81s 228.03s % Output : CNFRefutation 227.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYO657-1 : TPTP v7.5.0. Released v7.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.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 14:38:32 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.44 openjdk version "1.8.0_171" % 0.18/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.18/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.18/0.45 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.62/0.67 start to proof:theBenchmark % 227.81/228.03 % Version : CSE-F---1.0 % 227.81/228.03 % Problem : theBenchmark.p % 227.81/228.03 % Proof found % 227.81/228.03 % SZS status Theorem for theBenchmark.p % 227.81/228.03 % SZS output start Proof % 227.81/228.03 [2]~P1(f1(a4),a2) % 227.81/228.03 [1]P1(f1(x11),f3(f3(a2))) % 227.81/228.03 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 227.81/228.03 [4]P1(f1(x41),f3(a2))+P2(f3(a2),f1(x41))+~P1(f1(x41),f3(f3(a2))) % 227.81/228.03 [5]P1(f1(x51),a2)+~P1(f1(f5(x51)),f3(a2))+P2(a2,f1(f5(x51))) % 227.81/228.03 [6]P1(f1(x61),f3(a2))+~P1(f1(f5(x61)),f3(f3(a2)))+P2(f3(a2),f1(f5(x61))) % 227.81/228.03 [9]P1(f1(x91),a2)+~P1(f1(f5(f5(x91))),f3(a2))+P2(a2,f1(f5(f5(x91)))) % 227.81/228.03 [10]P1(f1(x101),f3(a2))+~P1(f1(f5(f5(x101))),f3(f3(a2)))+P2(f3(a2),f1(f5(f5(x101)))) % 227.81/228.03 [7]P3(f5(x71),f5(x71))+~P2(a2,f1(x71))+P2(f1(x71),f1(f5(x71)))+~P2(a2,f1(f5(x71))) % 227.81/228.03 [8]P3(f5(x81),f5(x81))+~P2(f3(a2),f1(x81))+P2(f1(x81),f1(f5(x81)))+~P2(f3(a2),f1(f5(x81))) % 227.81/228.03 [11]P3(f5(x111),f5(x111))+~P2(a2,f1(x111))+~P2(f1(x111),f1(f5(x111)))+~P2(a2,f1(f5(x111)))+~P2(a2,f1(f5(f5(x111)))) % 227.81/228.03 [12]P3(f5(x121),f5(x121))+~P2(f3(a2),f1(x121))+~P2(f1(x121),f1(f5(x121)))+~P2(f3(a2),f1(f5(x121)))+~P2(f3(a2),f1(f5(f5(x121)))) % 227.81/228.03 [13]~P3(f5(x132),f5(x131))+P2(f1(x131),f1(f5(x131)))+P2(f1(x132),f1(f5(x132)))+~P2(a2,f1(x131))+~P2(a2,f1(x132))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x132))) % 227.81/228.03 [14]~P3(f5(x142),f5(x141))+~P2(f3(a2),f1(x141))+~P2(f3(a2),f1(x142))+P2(f1(x141),f1(f5(x141)))+P2(f1(x142),f1(f5(x142)))+~P2(f3(a2),f1(f5(x141)))+~P2(f3(a2),f1(f5(x142))) % 227.81/228.03 [15]~P3(f5(x152),f5(x151))+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(a2,f1(f5(f5(x152)))) % 227.81/228.03 [16]~P3(f5(x161),f5(x162))+P2(f1(x161),f1(f5(x161)))+~P2(a2,f1(x161))+~P2(f1(x162),f1(f5(x162)))+~P2(a2,f1(x162))+~P2(a2,f1(f5(x162)))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(f5(x162)))) % 227.81/228.03 [17]~P3(f5(x172),f5(x171))+~P2(f3(a2),f1(x172))+~P2(f3(a2),f1(x171))+P2(f1(x171),f1(f5(x171)))+~P2(f1(x172),f1(f5(x172)))+~P2(f3(a2),f1(f5(x171)))+~P2(f3(a2),f1(f5(x172)))+~P2(f3(a2),f1(f5(f5(x172)))) % 227.81/228.03 [18]~P3(f5(x181),f5(x182))+~P2(f3(a2),f1(x182))+~P2(f3(a2),f1(x181))+P2(f1(x181),f1(f5(x181)))+~P2(f1(x182),f1(f5(x182)))+~P2(f3(a2),f1(f5(x181)))+~P2(f3(a2),f1(f5(x182)))+~P2(f3(a2),f1(f5(f5(x182)))) % 227.81/228.03 [19]~P3(f5(x192),f5(x191))+~P2(f1(x191),f1(f5(x191)))+~P2(a2,f1(x191))+~P2(f1(x192),f1(f5(x192)))+~P2(a2,f1(x192))+~P2(a2,f1(f5(x191)))+~P2(a2,f1(f5(x192)))+~P2(a2,f1(f5(f5(x191))))+~P2(a2,f1(f5(f5(x192)))) % 227.81/228.03 [20]~P3(f5(x201),f5(x202))+~P2(f3(a2),f1(x202))+~P2(f3(a2),f1(x201))+~P2(f1(x201),f1(f5(x201)))+~P2(f1(x202),f1(f5(x202)))+~P2(f3(a2),f1(f5(x201)))+~P2(f3(a2),f1(f5(x202)))+~P2(f3(a2),f1(f5(f5(x201))))+~P2(f3(a2),f1(f5(f5(x202)))) % 227.88/228.07 cnf(21,plain, % 227.88/228.07 (P1(f1(x211),f3(a2))+P2(f3(a2),f1(x211))), % 227.88/228.07 inference(scs_inference,[],[1,4])). % 227.88/228.07 cnf(25,plain, % 227.88/228.07 (P2(f3(a2),f1(f5(a4)))+P2(a2,f1(f5(a4)))), % 227.88/228.07 inference(scs_inference,[],[2,5,21])). % 227.88/228.07 cnf(26,plain, % 227.88/228.07 (P2(f3(a2),f1(f5(f5(a4))))+P2(a2,f1(f5(f5(a4))))), % 227.88/228.07 inference(scs_inference,[],[2,9,21])). % 227.88/228.07 cnf(29,plain, % 227.88/228.07 (~P2(a2,f1(x291))+P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(f5(x291)))), % 227.88/228.07 inference(scs_inference,[],[7,13])). % 227.88/228.07 cnf(30,plain, % 227.88/228.07 (~P2(f3(a2),f1(x301))+P2(f1(x301),f1(f5(x301)))+~P2(f3(a2),f1(f5(x301)))), % 227.88/228.07 inference(scs_inference,[],[8,14])). % 227.88/228.07 cnf(31,plain, % 227.88/228.07 (P2(f1(x311),f1(f5(x311)))+~P2(f3(a2),f1(x311))+P1(f1(f5(x311)),f3(a2))), % 227.88/228.07 inference(scs_inference,[],[30,21])). % 227.88/228.07 cnf(32,plain, % 227.88/228.07 (P2(f1(x321),f1(f5(x321)))+~P2(f3(a2),f1(f5(x321)))+P1(f1(x321),f3(a2))), % 227.88/228.07 inference(scs_inference,[],[21,30])). % 227.88/228.07 cnf(45,plain, % 227.88/228.07 (P2(f3(a2),f1(f5(f5(f5(f5(a4))))))+P2(a2,f1(f5(f5(a4))))), % 227.88/228.07 inference(scs_inference,[],[2,1,9,10])). % 227.88/228.08 cnf(32123,plain, % 227.88/228.08 (~P1(f1(a4),f3(a2))+P2(a2,f1(a4))), % 227.88/228.08 inference(scs_inference,[],[2,3])). % 227.88/228.08 cnf(32126,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+~P1(f1(a4),f3(a2))+~P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32123,29])). % 227.88/228.08 cnf(32127,plain, % 227.88/228.08 (~P1(f1(f5(f5(a4))),f3(a2))+P2(a2,f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[2,9])). % 227.88/228.08 cnf(32129,plain, % 227.88/228.08 (~P1(f1(f5(a4)),f3(a2))+P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[2,9,5])). % 227.88/228.08 cnf(32131,plain, % 227.88/228.08 (P1(f1(x321311),f3(a2))+P2(f3(a2),f1(f5(x321311)))), % 227.88/228.08 inference(scs_inference,[],[1,6])). % 227.88/228.08 cnf(32133,plain, % 227.88/228.08 (P2(f3(a2),f1(f5(f5(a4))))+P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[1,2,6,5])). % 227.88/228.08 cnf(32136,plain, % 227.88/228.08 (P1(f1(x321361),f3(a2))+P2(f3(a2),f1(f5(f5(x321361))))), % 227.88/228.08 inference(scs_inference,[],[1,10])). % 227.88/228.08 cnf(32145,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P1(f1(f5(f5(a4))),f3(a2))+~P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32127,29])). % 227.88/228.08 cnf(32148,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))+~P2(f3(a2),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32126,32])). % 227.88/228.08 cnf(32159,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+P2(a2,f1(f5(a4)))+~P2(f3(a2),f1(a4))), % 227.88/228.08 inference(scs_inference,[],[32129,31])). % 227.88/228.08 cnf(32160,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+~P2(f3(a2),f1(a4))+~P2(a2,f1(a4))), % 227.88/228.08 inference(scs_inference,[],[32159,29])). % 227.88/228.08 cnf(32162,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+P2(a2,f1(f5(a4)))+~P2(f3(a2),f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32129,32])). % 227.88/228.08 cnf(32163,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32162,32133])). % 227.88/228.08 cnf(32164,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(a2,f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32163,29])). % 227.88/228.08 cnf(32165,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+P2(f3(a2),f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32164,26])). % 227.88/228.08 cnf(32166,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(f3(a2),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32165,30])). % 227.88/228.08 cnf(32167,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32166,21])). % 227.88/228.08 cnf(32172,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P1(f1(f5(a4)),f3(a2))+~P1(f1(f5(f5(a4))),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32129,32145])). % 227.88/228.08 cnf(32173,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+~P1(f1(f5(f5(a4))),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32172,32167])). % 227.88/228.08 cnf(32174,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.08 inference(scs_inference,[],[32173,32136])). % 227.88/228.08 cnf(32178,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))+P2(f3(a2),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32131,32126])). % 227.88/228.08 cnf(32179,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32178,32148])). % 227.88/228.08 cnf(32180,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+P2(f3(a2),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32179,25])). % 227.88/228.08 cnf(32181,plain, % 227.88/228.08 (P2(f1(f5(a4)),f1(f5(f5(a4))))+P2(f1(a4),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32180,32166])). % 227.88/228.08 cnf(32187,plain, % 227.88/228.08 (P2(f1(x321871),f1(f5(x321871)))+P1(f1(x321871),f3(a2))+~P2(f3(a2),f1(x321871))), % 227.88/228.08 inference(scs_inference,[],[32131,30])). % 227.88/228.08 cnf(32188,plain, % 227.88/228.08 (P2(f1(x321881),f1(f5(x321881)))+P1(f1(x321881),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32187,21])). % 227.88/228.08 cnf(32189,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+P2(a2,f1(a4))), % 227.88/228.08 inference(scs_inference,[],[32188,32123])). % 227.88/228.08 cnf(32190,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+~P2(f3(a2),f1(a4))), % 227.88/228.08 inference(scs_inference,[],[32189,32160])). % 227.88/228.08 cnf(32200,plain, % 227.88/228.08 (P2(f1(f5(x322001)),f1(f5(f5(x322001))))+P1(f1(x322001),f3(a2))+~P2(f3(a2),f1(f5(x322001)))), % 227.88/228.08 inference(scs_inference,[],[32136,30])). % 227.88/228.08 cnf(32201,plain, % 227.88/228.08 (P2(f1(f5(x322011)),f1(f5(f5(x322011))))+P1(f1(x322011),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32200,32131])). % 227.88/228.08 cnf(32211,plain, % 227.88/228.08 (~P3(f5(f5(a4)),f5(f5(a4)))+~P2(f3(a2),f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+P2(a2,f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[2,9,32188,32201,21,32131,32136,20])). % 227.88/228.08 cnf(32214,plain, % 227.88/228.08 (P2(a2,f1(a4))), % 227.88/228.08 inference(scs_inference,[],[2,3,32188,32201,21,32131,32136,30,12,20])). % 227.88/228.08 cnf(32405,plain, % 227.88/228.08 (~P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))+~P2(a2,f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32214,19])). % 227.88/228.08 cnf(32406,plain, % 227.88/228.08 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))+~P2(a2,f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32214,11])). % 227.88/228.08 cnf(32896,plain, % 227.88/228.08 (~P2(f3(a2),f1(f5(a4)))+P2(a2,f1(f5(f5(a4))))+~P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32166,32211])). % 227.88/228.08 cnf(32899,plain, % 227.88/228.08 (~P2(a2,f1(f5(f5(a4))))+~P2(a2,f1(f5(a4)))+~P3(f5(a4),f5(a4))), % 227.88/228.08 inference(scs_inference,[],[32214,29,32405])). % 227.88/228.08 cnf(32901,plain, % 227.88/228.08 (~P2(a2,f1(f5(f5(a4))))+~P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32899,32406])). % 227.88/228.08 cnf(32909,plain, % 227.88/228.08 (~P2(a2,f1(f5(a4)))+~P2(a2,f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32214,29,32901])). % 227.88/228.08 cnf(32910,plain, % 227.88/228.08 (~P2(a2,f1(f5(a4)))+P2(f3(a2),f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32909,26])). % 227.88/228.08 cnf(32916,plain, % 227.88/228.08 (~P2(a2,f1(f5(f5(a4))))+~P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32909,32129])). % 227.88/228.08 cnf(32924,plain, % 227.88/228.08 (~P2(a2,f1(f5(a4)))+~P1(f1(f5(f5(a4))),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32909,32127])). % 227.88/228.08 cnf(32926,plain, % 227.88/228.08 (~P2(a2,f1(f5(a4)))+~P2(f3(a2),f1(f5(a4)))+~P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32909,32896])). % 227.88/228.08 cnf(32927,plain, % 227.88/228.08 (~P2(a2,f1(f5(a4)))+~P3(f5(f5(a4)),f5(f5(a4)))+P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32926,21])). % 227.88/228.08 cnf(32932,plain, % 227.88/228.08 (P2(f3(a2),f1(f5(f5(a4))))+~P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32910,32129])). % 227.88/228.08 cnf(32933,plain, % 227.88/228.08 (P2(f3(a2),f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32932,32131])). % 227.88/228.08 cnf(32937,plain, % 227.88/228.08 (P3(f5(f5(a4)),f5(f5(a4)))+~P2(f3(a2),f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(f3(a2),f1(f5(f5(f5(a4)))))), % 227.88/228.08 inference(scs_inference,[],[32933,12])). % 227.88/228.08 cnf(32956,plain, % 227.88/228.08 (~P3(f5(f5(f5(a4))),f5(f5(f5(a4))))+~P2(f1(f5(f5(a4))),f1(f5(f5(f5(a4)))))+~P2(f3(a2),f1(f5(f5(f5(a4)))))+~P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.08 inference(scs_inference,[],[32933,20])). % 227.88/228.08 cnf(32966,plain, % 227.88/228.08 (~P1(f1(f5(a4)),f3(a2))+~P1(f1(f5(f5(a4))),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32916,32127])). % 227.88/228.08 cnf(32970,plain, % 227.88/228.08 (~P1(f1(f5(f5(a4))),f3(a2))+P2(f3(a2),f1(f5(f5(f5(a4)))))), % 227.88/228.08 inference(scs_inference,[],[32966,32136])). % 227.88/228.08 cnf(32972,plain, % 227.88/228.08 (~P3(f5(f5(a4)),f5(f5(a4)))+~P2(f3(a2),f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(f3(a2),f1(f5(f5(f5(a4)))))), % 227.88/228.08 inference(scs_inference,[],[32933,20])). % 227.88/228.08 cnf(32973,plain, % 227.88/228.08 (P2(f3(a2),f1(f5(f5(f5(a4)))))), % 227.88/228.08 inference(scs_inference,[],[32970,32131])). % 227.88/228.08 cnf(32977,plain, % 227.88/228.08 (~P2(f3(a2),f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32973,32937])). % 227.88/228.08 cnf(32979,plain, % 227.88/228.08 (~P2(f3(a2),f1(f5(f5(f5(f5(a4))))))+~P2(f1(f5(f5(a4))),f1(f5(f5(f5(a4)))))+~P3(f5(f5(f5(a4))),f5(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32973,32956])). % 227.88/228.08 cnf(32980,plain, % 227.88/228.08 (~P2(f3(a2),f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+~P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32973,32972])). % 227.88/228.08 cnf(32987,plain, % 227.88/228.08 (P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))+~P2(f3(a2),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32933,32190,12])). % 227.88/228.08 cnf(33009,plain, % 227.88/228.08 (~P2(f3(a2),f1(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f3(a2),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32933,32987,20])). % 227.88/228.08 cnf(33013,plain, % 227.88/228.08 (~P2(f1(a4),f1(f5(a4)))+~P2(f3(a2),f1(a4))+P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[33009,21])). % 227.88/228.08 cnf(33036,plain, % 227.88/228.08 (~P2(f1(f5(a4)),f1(f5(f5(a4))))+P3(f5(f5(a4)),f5(f5(a4)))+P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[32977,21])). % 227.88/228.08 cnf(33037,plain, % 227.88/228.08 (P2(a2,f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+~P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32980,25])). % 227.88/228.08 cnf(33038,plain, % 227.88/228.08 (P1(f1(f5(a4)),f3(a2))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+~P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[33037,32927])). % 227.88/228.08 cnf(33042,plain, % 227.88/228.08 (~P2(f1(f5(a4)),f1(f5(f5(a4))))+P3(f5(f5(a4)),f5(f5(a4)))+P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[2,33036,5])). % 227.88/228.08 cnf(33043,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[33042,32179])). % 227.88/228.08 cnf(33044,plain, % 227.88/228.08 (P1(f1(f5(a4)),f3(a2))+~P3(f5(f5(a4)),f5(f5(a4)))+~P2(f3(a2),f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[32933,33038,30])). % 227.88/228.08 cnf(33046,plain, % 227.88/228.08 (~P3(f5(f5(a4)),f5(f5(a4)))+P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[33044,21])). % 227.88/228.08 cnf(33055,plain, % 227.88/228.08 (~P3(f5(f5(a4)),f5(f5(a4)))+P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[2,33046,5])). % 227.88/228.08 cnf(33056,plain, % 227.88/228.08 (~P2(a2,f1(f5(f5(a4))))+~P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[33055,32909])). % 227.88/228.08 cnf(33057,plain, % 227.88/228.08 (~P1(f1(f5(f5(a4))),f3(a2))+~P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[33056,32127])). % 227.88/228.08 cnf(33059,plain, % 227.88/228.08 (~P3(f5(f5(a4)),f5(f5(a4)))+P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.08 inference(scs_inference,[],[33057,32136])). % 227.88/228.08 cnf(33065,plain, % 227.88/228.08 (P2(f1(a4),f1(f5(a4)))+P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[33043,32181])). % 227.88/228.08 cnf(33066,plain, % 227.88/228.08 (~P2(f3(a2),f1(a4))+P1(f1(f5(a4)),f3(a2))+P3(f5(f5(a4)),f5(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[33065,33013])). % 227.88/228.08 cnf(33067,plain, % 227.88/228.08 (~P2(f3(a2),f1(a4))+P3(f5(f5(a4)),f5(f5(a4)))+P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[2,33066,5])). % 227.88/228.08 cnf(33068,plain, % 227.88/228.08 (~P2(f3(a2),f1(a4))+P2(a2,f1(f5(a4)))), % 227.88/228.08 inference(scs_inference,[],[33067,33055])). % 227.88/228.08 cnf(33125,plain, % 227.88/228.08 (~P2(f3(a2),f1(a4))+~P1(f1(f5(f5(a4))),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[33068,32924])). % 227.88/228.08 cnf(33131,plain, % 227.88/228.08 (~P2(f3(a2),f1(a4))+P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.08 inference(scs_inference,[],[33125,32136])). % 227.88/228.08 cnf(33169,plain, % 227.88/228.08 (~P1(f1(f5(a4)),f3(a2))+P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.08 inference(scs_inference,[],[32136,32966])). % 227.88/228.08 cnf(33309,plain, % 227.88/228.08 (P2(a2,f1(f5(a4)))+~P2(f3(a2),f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[32933,32973,33055,12])). % 227.88/228.08 cnf(33325,plain, % 227.88/228.08 (P2(a2,f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))+P1(f1(f5(a4)),f3(a2))), % 227.88/228.08 inference(scs_inference,[],[33309,21])). % 227.88/228.08 cnf(33341,plain, % 227.88/228.08 (P2(a2,f1(f5(a4)))+~P2(f1(f5(a4)),f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[33325,32129])). % 227.88/228.08 cnf(33357,plain, % 227.88/228.08 (~P2(a2,f1(f5(f5(a4))))+~P2(f1(f5(a4)),f1(f5(f5(a4))))), % 227.88/228.08 inference(scs_inference,[],[33341,32909])). % 227.88/228.08 cnf(33371,plain, % 227.88/228.08 (P2(f1(f5(f5(a4))),f1(f5(f5(f5(a4)))))), % 227.88/228.08 inference(scs_inference,[],[32973,32933,30])). % 227.88/228.08 cnf(33373,plain, % 227.88/228.08 (P3(f5(f5(f5(a4))),f5(f5(f5(a4))))+~P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.09 inference(scs_inference,[],[32973,32933,30,12])). % 227.88/228.09 cnf(33378,plain, % 227.88/228.09 (~P1(f1(f5(a4)),f3(a2))+P3(f5(f5(f5(a4))),f5(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[32973,32933,30,12,32174,33059,33131,33169])). % 227.88/228.09 cnf(33379,plain, % 227.88/228.09 (P2(a2,f1(f5(a4)))+P3(f5(f5(f5(a4))),f5(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[32973,32933,30,12,32174,33059,33131,33169,33341])). % 227.88/228.09 cnf(33387,plain, % 227.88/228.09 (~P2(f3(a2),f1(f5(f5(f5(f5(a4))))))+~P3(f5(f5(f5(a4))),f5(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[33371,32979])). % 227.88/228.09 cnf(33410,plain, % 227.88/228.09 (P2(f3(a2),f1(f5(f5(f5(f5(a4))))))+~P2(f1(f5(a4)),f1(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[33357,45])). % 227.88/228.09 cnf(33855,plain, % 227.88/228.09 (~P2(f1(f5(a4)),f1(f5(f5(a4))))+P3(f5(f5(f5(a4))),f5(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[33410,33373])). % 227.88/228.09 cnf(33967,plain, % 227.88/228.09 (~P2(f1(f5(a4)),f1(f5(f5(a4))))+~P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.09 inference(scs_inference,[],[32933,33371,32973,33855,20])). % 227.88/228.09 cnf(33983,plain, % 227.88/228.09 (~P2(f3(a2),f1(f5(f5(f5(f5(a4))))))+~P2(f3(a2),f1(f5(a4)))), % 227.88/228.09 inference(scs_inference,[],[33967,32166])). % 227.88/228.09 cnf(33999,plain, % 227.88/228.09 (~P2(f3(a2),f1(f5(a4)))+P2(a2,f1(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[33983,45])). % 227.88/228.09 cnf(34358,plain, % 227.88/228.09 (~P2(f3(a2),f1(f5(a4)))+~P2(a2,f1(f5(a4)))), % 227.88/228.09 inference(scs_inference,[],[33999,32909])). % 227.88/228.09 cnf(34365,plain, % 227.88/228.09 (~P2(a2,f1(f5(a4)))+P1(f1(f5(a4)),f3(a2))), % 227.88/228.09 inference(scs_inference,[],[34358,21])). % 227.88/228.09 cnf(34366,plain, % 227.88/228.09 (~P2(a2,f1(f5(a4)))+P3(f5(f5(f5(a4))),f5(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[34365,33378])). % 227.88/228.09 cnf(34368,plain, % 227.88/228.09 (P3(f5(f5(f5(a4))),f5(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[34366,33379])). % 227.88/228.09 cnf(34369,plain, % 227.88/228.09 (~P2(f3(a2),f1(f5(f5(f5(f5(a4))))))), % 227.88/228.09 inference(scs_inference,[],[34368,33387])). % 227.88/228.09 cnf(34374,plain, % 227.88/228.09 (P2(f1(f5(a4)),f1(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[34369,32174])). % 227.88/228.09 cnf(34380,plain, % 227.88/228.09 (~P2(f1(f5(a4)),f1(f5(f5(a4))))), % 227.88/228.09 inference(scs_inference,[],[34369,33410])). % 227.88/228.09 cnf(34385,plain, % 227.88/228.09 ($false), % 227.88/228.09 inference(scs_inference,[],[34374,34380]), % 227.88/228.09 ['proof']). % 227.88/228.11 % SZS output end Proof % 227.88/228.11 % Total time : 227.030000 s %------------------------------------------------------------------------------