%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : TOP001-2 : TPTP v7.5.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n005.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 15:48:09 EDT 2022 % Result : Unsatisfiable 101.67s 102.07s % Output : CNFRefutation 102.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : TOP001-2 : TPTP v7.5.0. Released v1.0.0. % 0.06/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.34 % Computer : n005.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % RAMPerCPU : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Wed Mar 16 05:43:12 EDT 2022 % 0.14/0.34 % 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/sandbox2/benchmark/theBenchmark.p % 0.54/0.67 start to proof:theBenchmark % 101.67/102.07 % Version : CSE-F---1.0 % 101.67/102.07 % Problem : theBenchmark.p % 101.67/102.07 % Proof found % 101.67/102.07 % SZS status Theorem for theBenchmark.p % 101.67/102.07 % SZS output start Proof % 101.67/102.07 [1]P1(a1,a2) % 101.67/102.07 [3]~P2(f7(f3(a2)),a1) % 101.67/102.07 [2]P2(x21,x21) % 101.67/102.07 [4]~P3(x41,x42)+P2(x41,x42) % 101.67/102.07 [5]~P1(x52,x51)+P3(f7(x51),x52) % 101.67/102.07 [6]P2(x61,x62)+P4(f4(x61,x62),x61) % 101.67/102.07 [9]~P4(x91,f7(x92))+P4(x91,f5(x92,x91)) % 101.67/102.07 [10]~P4(x102,f7(x101))+P5(f5(x101,x102),x101) % 101.67/102.07 [11]P2(x111,x112)+~P4(f4(x111,x112),x112) % 101.67/102.07 [7]~P2(x73,x72)+P4(x71,x72)+~P4(x71,x73) % 101.67/102.07 [8]~P5(x83,x82)+~P4(x81,x83)+P4(x81,f7(x82)) % 101.67/102.07 [12]~P4(x121,x123)+~P5(x123,f3(x122))+P4(x121,f6(x122,x123,x121)) % 101.67/102.07 [13]~P4(x133,x132)+~P5(x132,f3(x131))+P5(f6(x131,x132,x133),x131) % 101.87/102.26 cnf(14,plain, % 101.87/102.26 (~P3(f7(f3(a2)),a1)), % 101.87/102.26 inference(scs_inference,[],[3,4])). % 101.87/102.26 cnf(48,plain, % 101.87/102.26 (~P4(x481,x482)+P4(x481,x483)+P4(f4(x482,x483),x482)), % 101.87/102.26 inference(scs_inference,[],[6,7])). % 101.87/102.26 cnf(79,plain, % 101.87/102.26 (~P4(x791,x792)+P4(x791,x793)+~P4(f4(x792,x793),x793)), % 101.87/102.27 inference(scs_inference,[],[11,7])). % 101.87/102.27 cnf(110,plain, % 101.87/102.27 (~P5(f5(x1101,x1102),x1103)+P4(x1102,f7(x1103))+~P4(x1102,f7(x1101))), % 101.87/102.27 inference(scs_inference,[],[9,8])). % 101.87/102.27 cnf(141,plain, % 101.87/102.27 (~P4(x1411,f5(f3(x1412),x1413))+P4(x1411,f6(x1412,f5(f3(x1412),x1413),x1411))+~P4(x1413,f7(f3(x1412)))), % 101.87/102.27 inference(scs_inference,[],[10,12])). % 101.87/102.27 cnf(172,plain, % 101.87/102.27 (~P4(x1721,f7(x1722))+P4(x1721,x1723)+P4(f4(f7(x1722),x1723),f5(x1722,f4(f7(x1722),x1723)))), % 101.87/102.27 inference(scs_inference,[],[48,9])). % 101.87/102.27 cnf(203,plain, % 101.87/102.27 (~P4(f4(f7(f3(a2)),x2031),x2031)+P4(f4(f7(f3(a2)),a1),x2031)), % 101.87/102.27 inference(scs_inference,[],[3,79,6])). % 101.87/102.27 cnf(541,plain, % 101.87/102.27 (~P4(x5411,x5412)+~P3(x5412,x5413)+P4(x5411,x5413)), % 101.87/102.27 inference(scs_inference,[],[4,7])). % 101.87/102.27 cnf(572,plain, % 101.87/102.27 (~P4(f4(f7(f3(a2)),a1),x5721)+~P3(x5721,a1)), % 101.87/102.27 inference(scs_inference,[],[3,541,11])). % 101.87/102.27 cnf(603,plain, % 101.87/102.27 (~P4(f4(f7(f3(a2)),x6031),x6031)+~P3(x6031,a1)), % 101.87/102.27 inference(scs_inference,[],[572,203])). % 101.87/102.27 cnf(281082,plain, % 101.87/102.27 (P3(f7(a2),a1)), % 101.87/102.27 inference(scs_inference,[],[1,5])). % 101.87/102.27 cnf(281086,plain, % 101.87/102.27 (P4(x2810861,a1)+~P4(x2810861,f7(a2))), % 101.87/102.27 inference(scs_inference,[],[1,5,4,541])). % 101.87/102.27 cnf(281090,plain, % 101.87/102.27 (~P4(f4(f7(f3(a2)),a1),f7(a2))), % 101.87/102.27 inference(scs_inference,[],[3,11,281086])). % 101.87/102.27 cnf(281094,plain, % 101.87/102.27 (P4(f4(x2810941,f7(a2)),x2810941)+~P4(f4(f7(f3(a2)),a1),x2810941)), % 101.87/102.27 inference(scs_inference,[],[3,11,281086,79,48])). % 101.87/102.27 cnf(281142,plain, % 101.87/102.27 (~P4(f4(f7(f3(a2)),f7(a2)),f7(a2))), % 101.87/102.27 inference(scs_inference,[],[281082,603])). % 101.87/102.27 cnf(281144,plain, % 101.87/102.27 (~P5(x2811441,a2)+~P4(f4(f7(f3(a2)),f7(a2)),x2811441)), % 101.87/102.27 inference(scs_inference,[],[281082,603,8])). % 101.87/102.27 cnf(281261,plain, % 101.87/102.27 (~P4(f4(f7(f3(a2)),f7(a2)),x2812611)+~P3(x2812611,f7(a2))), % 101.87/102.27 inference(scs_inference,[],[281142,541])). % 101.87/102.27 cnf(322914,plain, % 101.87/102.27 (P4(f4(f7(f3(a2)),a1),f7(f3(a2)))), % 101.87/102.27 inference(scs_inference,[],[3,14,5,6])). % 101.87/102.27 cnf(322916,plain, % 101.87/102.27 (P4(f4(f7(f3(a2)),f7(a2)),f7(f3(a2)))), % 101.87/102.27 inference(scs_inference,[],[3,14,5,6,281094])). % 101.87/102.27 cnf(322922,plain, % 101.87/102.27 (P4(f4(f7(f3(a2)),a1),f5(f3(a2),f4(f7(f3(a2)),a1)))), % 101.87/102.27 inference(scs_inference,[],[3,14,5,6,281094,281261,281144,9])). % 101.87/102.27 cnf(322928,plain, % 101.87/102.27 (P4(f4(f5(f3(a2),f4(f7(f3(a2)),a1)),f7(a2)),f5(f3(a2),f4(f7(f3(a2)),a1)))), % 101.87/102.27 inference(scs_inference,[],[3,14,281090,5,6,281094,281261,281144,9,10,572,48])). % 101.87/102.27 cnf(322932,plain, % 101.87/102.27 (~P4(f4(f5(f3(a2),f4(f7(f3(a2)),a1)),f7(a2)),f7(a2))), % 101.87/102.27 inference(scs_inference,[],[3,14,281090,5,6,281094,281261,281144,9,10,572,48,541,79])). % 101.87/102.27 cnf(322936,plain, % 101.87/102.27 (P4(f4(f7(f3(a2)),f7(a2)),f5(f3(a2),f4(f7(f3(a2)),f7(a2))))), % 101.87/102.27 inference(scs_inference,[],[3,14,281090,5,6,281094,281261,281144,9,10,572,48,541,79,110,172])). % 101.87/102.27 cnf(322938,plain, % 101.87/102.27 (P4(f4(f7(f3(a2)),f7(a2)),f6(a2,f5(f3(a2),f4(f7(f3(a2)),f7(a2))),f4(f7(f3(a2)),f7(a2))))), % 101.87/102.27 inference(scs_inference,[],[3,14,281090,5,6,281094,281261,281144,9,10,572,48,541,79,110,172,141])). % 101.87/102.27 cnf(322975,plain, % 101.87/102.27 ($false), % 101.87/102.27 inference(scs_inference,[],[14,281090,281142,322914,322916,322938,322936,322922,322928,322932,5,281261,281144,10,572,48,8,541,79,110,7,13]), % 101.87/102.27 ['proof']). % 102.08/102.47 % SZS output end Proof % 102.08/102.47 % Total time : 101.010000 s %------------------------------------------------------------------------------