%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYN986+1.002 : TPTP v7.5.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n029.cluster.edu---x86_64 x86_64--- ------Linux 3.10.0-693.el7.x86_64 % Model : Unavailable % CPU : Unavailable % Memory : Unavailable % OS : Unavailable % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Mar 28 15:04:48 EDT 2022 % Result : Theorem 280.68s 282.59s % Output : CNFRefutation 280.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN986+1.002 : TPTP v7.5.0. Released v4.0.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % RAMPerCPU : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Thu Mar 10 19:44:14 EST 2022 % 0.12/0.34 % CPUTime : % 0.20/0.45 openjdk version "1.8.0_171" % 0.20/0.45 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.20/0.45 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.20/0.45 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.62/0.64 start to proof:theBenchmark % 252.77/253.96 TMO-Non % 253.85/255.07 CSE is exited by timeout % 254.69/255.87 start to proof:theBenchmark % 280.68/282.59 % Version : CSE-F---1.0 % 280.68/282.59 % Problem : theBenchmark.p % 280.68/282.59 % Proof found % 280.68/282.59 % SZS status Theorem for theBenchmark.p % 280.68/282.59 % SZS output start Proof % 280.68/282.59 [1]P1(x11,a1,f2(x11)) % 280.68/282.59 [3]~P1(a1,x31,x32)+~P1(a1,x33,x31)+~P1(a1,a1,x33) % 280.68/282.59 [2]~P1(x21,x22,x24)+~P1(x24,x22,x23)+P1(x21,f2(x22),x23) % 280.83/282.70 cnf(4,plain, % 280.83/282.70 (~P1(a1,f2(a1),a1)), % 280.83/282.70 inference(scs_inference,[],[1,3])). % 280.83/282.70 cnf(284,plain, % 280.83/282.70 (~P1(f2(a1),a1,x2841)+~P1(a1,f2(a1),f2(a1))), % 280.83/282.70 inference(scs_inference,[],[1,3,2])). % 280.83/282.70 cnf(288,plain, % 280.83/282.70 (P1(x2881,f2(x2882),x2883)+~P1(x2881,x2882,x2884)+~P1(x2884,x2882,x2883)), % 280.83/282.70 inference(rename_variables,[],[2])). % 280.83/282.70 cnf(289,plain, % 280.83/282.70 (P1(x2891,f2(a1),f2(f2(a1)))+~P1(x2891,a1,f2(a1))), % 280.83/282.70 inference(scs_inference,[],[1,4,284,2,288])). % 280.83/282.70 cnf(290,plain, % 280.83/282.70 (P1(x2901,f2(x2902),x2903)+~P1(x2901,x2902,x2904)+~P1(x2904,x2902,x2903)), % 280.83/282.70 inference(rename_variables,[],[2])). % 280.83/282.70 cnf(291,plain, % 280.83/282.70 (~P1(x2911,a1,f2(a1))+~P1(a1,a1,x2911)), % 280.83/282.70 inference(scs_inference,[],[1,4,284,2,288,290])). % 280.83/282.70 cnf(292,plain, % 280.83/282.70 (P1(x2921,f2(x2922),x2923)+~P1(x2921,x2922,x2924)+~P1(x2924,x2922,x2923)), % 280.83/282.70 inference(rename_variables,[],[2])). % 280.83/282.70 cnf(293,plain, % 280.83/282.70 (~P1(f2(f2(a1)),a1,x2931)+P1(f2(a1),f2(a1),x2931)), % 280.83/282.70 inference(scs_inference,[],[1,4,284,2,288,290,292])). % 280.83/282.70 cnf(294,plain, % 280.83/282.70 (P1(a1,f2(a1),f2(f2(a1)))), % 280.83/282.70 inference(scs_inference,[],[1,289])). % 280.83/282.70 cnf(297,plain, % 280.83/282.70 (~P1(a1,a1,x2971)+~P1(x2971,a1,f2(a1))), % 280.83/282.70 inference(rename_variables,[],[291])). % 280.83/282.70 cnf(303,plain, % 280.83/282.70 (P1(x3031,f2(x3032),x3033)+~P1(x3031,x3032,x3034)+~P1(x3034,x3032,x3033)), % 280.83/282.70 inference(rename_variables,[],[2])). % 280.83/282.70 cnf(304,plain, % 280.83/282.70 (~P1(f2(f2(a1)),f2(a1),x3041)), % 280.83/282.70 inference(scs_inference,[],[1,4,289,291,297,3,2,303])). % 280.83/282.70 cnf(77712,plain, % 280.83/282.70 (~P1(a1,x777121,f2(a1))+~P1(a1,a1,x777121)), % 280.83/282.70 inference(scs_inference,[],[294,304,1,293,289,2,3])). % 280.83/282.70 cnf(77723,plain, % 280.83/282.70 (~P1(x777231,x777232,x777233)+~P1(x777234,x777232,x777231)+P1(x777234,f2(x777232),x777233)), % 280.83/282.70 inference(rename_variables,[],[2])). % 280.83/282.70 cnf(77724,plain, % 280.83/282.70 (~P1(x777241,a1,f2(f2(a1)))+~P1(f2(f2(a1)),a1,x777241)), % 280.83/282.70 inference(scs_inference,[],[4,304,1,77712,289,291,2,77723])). % 280.83/282.70 cnf(77732,plain, % 280.83/282.70 (~P1(x777321,a1,f2(f2(a1)))+P1(x777321,f2(a1),f2(f2(f2(a1))))), % 280.83/282.70 inference(scs_inference,[],[304,1,77724,289,2])). % 280.83/282.70 cnf(77741,plain, % 280.83/282.70 (~P1(x777411,x777412,x777413)+~P1(x777414,x777412,x777411)+P1(x777414,f2(x777412),x777413)), % 280.83/282.70 inference(rename_variables,[],[2])). % 280.83/282.70 cnf(77742,plain, % 280.83/282.70 (~P1(x777421,a1,f2(f2(f2(a1))))+~P1(f2(f2(a1)),a1,x777421)), % 280.83/282.70 inference(scs_inference,[],[4,304,1,77732,77724,2,77741])). % 280.83/282.70 cnf(187534,plain, % 280.83/282.70 (~P1(f2(f2(a1)),f2(a1),x1875341)), % 280.83/282.70 inference(rename_variables,[],[304])). % 280.83/282.70 cnf(187537,plain, % 280.83/282.70 (P1(x1875371,a1,f2(x1875371))), % 280.83/282.70 inference(rename_variables,[],[1])). % 280.83/282.70 cnf(187538,plain, % 280.83/282.70 (~P1(x1875381,a1,f2(f2(f2(a1))))+~P1(f2(f2(a1)),a1,x1875381)), % 280.83/282.70 inference(rename_variables,[],[77742])). % 280.83/282.70 cnf(187540,plain, % 280.83/282.70 (P1(x1875401,a1,f2(x1875401))), % 280.83/282.70 inference(rename_variables,[],[1])). % 280.83/282.70 cnf(187543,plain, % 280.83/282.70 (P1(x1875431,a1,f2(x1875431))), % 280.83/282.70 inference(rename_variables,[],[1])). % 280.83/282.70 cnf(187546,plain, % 280.83/282.70 (P1(x1875461,a1,f2(x1875461))), % 280.83/282.70 inference(rename_variables,[],[1])). % 280.83/282.70 cnf(187549,plain, % 280.83/282.70 (P1(x1875491,a1,f2(x1875491))), % 280.83/282.70 inference(rename_variables,[],[1])). % 280.83/282.70 cnf(187552,plain, % 280.83/282.70 (P1(x1875521,a1,f2(x1875521))), % 280.83/282.70 inference(rename_variables,[],[1])). % 280.83/282.70 cnf(187553,plain, % 280.83/282.70 (~P1(x1875531,x1875532,x1875533)+~P1(x1875534,x1875532,x1875531)+P1(x1875534,f2(x1875532),x1875533)), % 280.83/282.70 inference(rename_variables,[],[2])). % 280.83/282.70 cnf(187554,plain, % 280.83/282.70 (~P1(f2(f2(a1)),a1,x1875541)), % 280.83/282.70 inference(scs_inference,[],[4,1,187537,187540,187543,187546,187549,187552,304,187534,289,77742,187538,77724,77712,291,2,187553])). % 280.83/282.70 cnf(187557,plain, % 280.83/282.70 ($false), % 280.83/282.70 inference(scs_inference,[],[187554,1]), % 280.83/282.70 ['proof']). % 280.90/282.79 % SZS output end Proof % 280.90/282.79 % Total time : 30.383333 s %------------------------------------------------------------------------------