%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO666-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:49 EDT 2022 % Result : Unsatisfiable 51.65s 51.73s % Output : CNFRefutation 51.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYO666-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.12/0.33 % Computer : n011.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 15:51:27 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.44 openjdk version "1.8.0_171" % 0.19/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.19/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.19/0.45 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.57/0.64 start to proof:theBenchmark % 51.65/51.73 % Version : CSE-F---1.0 % 51.65/51.73 % Problem : theBenchmark.p % 51.65/51.73 % Proof found % 51.65/51.73 % SZS status Theorem for theBenchmark.p % 51.65/51.73 % SZS output start Proof % 51.65/51.73 [2]~P1(f1(a4),a2) % 51.65/51.73 [1]P1(f1(x11),f3(f3(a2))) % 51.65/51.73 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 51.65/51.73 [4]P1(f1(x41),f3(a2))+P2(f3(a2),f1(x41))+~P1(f1(x41),f3(f3(a2))) % 51.65/51.73 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+~P2(a2,f1(f5(x51))) % 51.65/51.73 [6]P1(f1(x61),a2)+~P1(f1(f5(x61)),f3(a2))+P2(a2,f1(f5(x61))) % 51.65/51.73 [7]P3(f5(x71),f5(x71))+~P2(f3(a2),f1(x71))+~P2(f3(a2),f1(f5(x71))) % 51.65/51.73 [8]P1(f1(x81),f3(a2))+~P1(f1(f5(x81)),f3(f3(a2)))+P2(f3(a2),f1(f5(x81))) % 51.65/51.73 [9]~P3(f5(x96),f5(x95))+~P3(f5(x95),f5(x93))+~P3(f5(x94),f5(x92))+~P3(f5(x92),f5(x91))+~P3(f5(x91),f5(x96))+~P2(a2,f1(x91))+~P2(a2,f1(x92))+~P2(a2,f1(x93))+~P2(a2,f1(x94))+~P2(a2,f1(x95))+~P2(a2,f1(x96))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(x92)))+~P2(a2,f1(f5(x93)))+~P2(a2,f1(f5(x94)))+~P2(a2,f1(f5(x95)))+~P2(a2,f1(f5(x96))) % 51.65/51.73 [10]~P3(f5(x101),f5(x102))+~P3(f5(x103),f5(x104))+~P3(f5(x104),f5(x101))+~P3(f5(x102),f5(x105))+~P3(f5(x105),f5(x106))+~P2(f3(a2),f1(x105))+~P2(f3(a2),f1(x104))+~P2(f3(a2),f1(x102))+~P2(f3(a2),f1(x103))+~P2(f3(a2),f1(x101))+~P2(f3(a2),f1(x106))+~P2(f3(a2),f1(f5(x101)))+~P2(f3(a2),f1(f5(x102)))+~P2(f3(a2),f1(f5(x103)))+~P2(f3(a2),f1(f5(x104)))+~P2(f3(a2),f1(f5(x105)))+~P2(f3(a2),f1(f5(x106))) % 51.65/51.75 cnf(11,plain, % 51.65/51.75 (P1(f1(x111),f3(a2))+P2(f3(a2),f1(x111))), % 51.65/51.75 inference(scs_inference,[],[1,4])). % 51.65/51.75 cnf(14,plain, % 51.65/51.75 (P2(f3(a2),f1(a4))+P2(a2,f1(a4))), % 51.65/51.75 inference(scs_inference,[],[2,11,3])). % 51.65/51.75 cnf(16,plain, % 51.65/51.75 (P2(f3(a2),f1(f5(a4)))+P2(a2,f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[2,6,11])). % 51.65/51.75 cnf(17,plain, % 51.65/51.75 (~P3(f5(a4),f5(a4))+P2(a2,f1(f5(a4)))+~P2(f3(a2),f1(a4))), % 51.65/51.75 inference(scs_inference,[],[16,10])). % 51.65/51.75 cnf(24,plain, % 51.65/51.75 (P2(a2,f1(a4))+P2(f3(a2),f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[1,2,8,3])). % 51.65/51.75 cnf(25,plain, % 51.65/51.75 (P2(a2,f1(a4))+~P3(f5(a4),f5(a4))+~P2(f3(a2),f1(a4))), % 51.65/51.75 inference(scs_inference,[],[24,10])). % 51.65/51.75 cnf(32,plain, % 51.65/51.75 (P2(f3(a2),f1(a4))+P3(f5(a4),f5(a4))+~P2(a2,f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[14,5])). % 51.65/51.75 cnf(33,plain, % 51.65/51.75 (~P3(f5(a4),f5(a4))+P2(a2,f1(a4))), % 51.65/51.75 inference(scs_inference,[],[14,25])). % 51.65/51.75 cnf(39,plain, % 51.65/51.75 (P1(f1(x391),f3(a2))+P3(f5(x391),f5(x391))+~P2(f3(a2),f1(f5(x391)))), % 51.65/51.75 inference(scs_inference,[],[11,7])). % 51.65/51.75 cnf(47,plain, % 51.65/51.75 (P1(f1(f5(x471)),f3(a2))+P3(f5(x471),f5(x471))+~P2(f3(a2),f1(x471))), % 51.65/51.75 inference(scs_inference,[],[11,7])). % 51.65/51.75 cnf(48,plain, % 51.65/51.75 (P2(a2,f1(f5(a4)))+~P2(f3(a2),f1(a4))+P1(f1(f5(a4)),f3(a2))), % 51.65/51.75 inference(scs_inference,[],[47,17])). % 51.65/51.75 cnf(49,plain, % 51.65/51.75 (~P2(f3(a2),f1(a4))+P2(a2,f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[2,48,6])). % 51.65/51.75 cnf(50,plain, % 51.65/51.75 (~P2(f3(a2),f1(a4))+~P3(f5(a4),f5(a4))+~P2(a2,f1(a4))), % 51.65/51.75 inference(scs_inference,[],[49,9])). % 51.65/51.75 cnf(51,plain, % 51.65/51.75 (~P2(f3(a2),f1(a4))+~P3(f5(a4),f5(a4))), % 51.65/51.75 inference(scs_inference,[],[50,33])). % 51.65/51.75 cnf(52,plain, % 51.65/51.75 (~P3(f5(a4),f5(a4))+P1(f1(a4),f3(a2))), % 51.65/51.75 inference(scs_inference,[],[51,11])). % 51.65/51.75 cnf(53,plain, % 51.65/51.75 (~P2(f3(a2),f1(f5(a4)))+P1(f1(a4),f3(a2))), % 51.65/51.75 inference(scs_inference,[],[52,39])). % 51.65/51.75 cnf(54,plain, % 51.65/51.75 (P1(f1(a4),f3(a2))+P2(a2,f1(a4))), % 51.65/51.75 inference(scs_inference,[],[53,24])). % 51.65/51.75 cnf(55,plain, % 51.65/51.75 (P2(a2,f1(a4))), % 51.65/51.75 inference(scs_inference,[],[2,54,3])). % 51.65/51.75 cnf(58,plain, % 51.65/51.75 (~P2(f3(a2),f1(a4))+~P2(a2,f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[55,51,5])). % 51.65/51.75 cnf(62,plain, % 51.65/51.75 (~P2(a2,f1(f5(a4)))+P3(f5(a4),f5(a4))), % 51.65/51.75 inference(scs_inference,[],[58,32])). % 51.65/51.75 cnf(66,plain, % 51.65/51.75 (P3(f5(a4),f5(a4))+~P1(f1(f5(a4)),f3(a2))), % 51.65/51.75 inference(scs_inference,[],[2,62,6])). % 51.65/51.75 cnf(67,plain, % 51.65/51.75 (P3(f5(a4),f5(a4))+P2(f3(a2),f1(f5(f5(a4))))), % 51.65/51.75 inference(scs_inference,[],[1,66,8])). % 51.65/51.75 cnf(68,plain, % 51.65/51.75 (P2(f3(a2),f1(f5(a4)))+~P3(f5(a4),f5(a4))), % 51.65/51.75 inference(scs_inference,[],[55,16,9])). % 51.65/51.75 cnf(69,plain, % 51.65/51.75 (~P2(a2,f1(f5(a4)))+P2(f3(a2),f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[68,62])). % 51.65/51.75 cnf(70,plain, % 51.65/51.75 (P2(f3(a2),f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[69,16])). % 51.65/51.75 cnf(23326,plain, % 51.65/51.75 (P2(f3(a2),f1(f5(f5(a4))))+P2(a2,f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[2,1,6,8])). % 51.65/51.75 cnf(23342,plain, % 51.65/51.75 (~P2(f3(a2),f1(f5(f5(a4))))), % 51.65/51.75 inference(scs_inference,[],[70,7,10])). % 51.65/51.75 cnf(23345,plain, % 51.65/51.75 (P3(f5(a4),f5(a4))), % 51.65/51.75 inference(scs_inference,[],[23342,67])). % 51.65/51.75 cnf(23346,plain, % 51.65/51.75 (P2(a2,f1(f5(a4)))), % 51.65/51.75 inference(scs_inference,[],[23342,23326])). % 51.65/51.75 cnf(23359,plain, % 51.65/51.75 ($false), % 51.65/51.75 inference(scs_inference,[],[23345,23346,55,9]), % 51.65/51.75 ['proof']). % 51.65/51.78 % SZS output end Proof % 51.65/51.78 % Total time : 51.010000 s %------------------------------------------------------------------------------