%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO614-1 : TPTP v7.5.0. Released v7.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n021.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:42 EDT 2022 % Result : Unsatisfiable 111.73s 111.72s % Output : CNFRefutation 111.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYO614-1 : TPTP v7.5.0. Released v7.1.0. % 0.10/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n021.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 : Mon Mar 14 07:28:26 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.71/0.72 start to proof:theBenchmark % 111.73/111.72 % Version : CSE-F---1.0 % 111.73/111.72 % Problem : theBenchmark.p % 111.73/111.72 % Proof found % 111.73/111.72 % SZS status Theorem for theBenchmark.p % 111.73/111.72 % SZS output start Proof % 111.73/111.72 [1]P1(x11,x11) % 111.73/111.72 [2]P2(f1(x21),a2)+P2(f1(x21),a3) % 111.73/111.72 [3]P1(x31,x32)+~P1(f4(x33,x31),x32) % 111.73/111.72 [4]P1(x41,x42)+~P1(f4(x41,x43),x42) % 111.73/111.72 [5]~P1(f5(x51),x52)+~P2(f1(x52),a2)+~P2(f1(x51),a2) % 111.73/111.72 [6]~P1(f5(x61),x62)+~P2(f1(x62),a3)+~P2(f1(x61),a3) % 111.73/111.73 cnf(7,plain, % 111.73/111.73 (P1(x71,f4(x72,x71))), % 111.73/111.73 inference(scs_inference,[],[1,3])). % 111.73/111.73 cnf(8,plain, % 111.73/111.73 (P1(x81,x81)), % 111.73/111.73 inference(rename_variables,[],[1])). % 111.73/111.73 cnf(10,plain, % 111.73/111.73 (P1(x101,f4(x101,x102))), % 111.73/111.73 inference(scs_inference,[],[1,8,3,4])). % 111.73/111.73 cnf(13,plain, % 111.73/111.73 (P1(x131,f4(x132,f4(x133,x131)))), % 111.73/111.73 inference(scs_inference,[],[7,3])). % 111.73/111.73 cnf(26,plain, % 111.73/111.73 (~P2(f1(f4(x261,f4(x262,f4(x263,f5(x264))))),a3)+~P2(f1(x264),a3)), % 111.73/111.73 inference(scs_inference,[],[13,6,3])). % 111.73/111.73 cnf(28,plain, % 111.73/111.73 (~P2(f1(x281),a2)+P2(f1(f5(x281)),a3)), % 111.73/111.73 inference(scs_inference,[],[1,2,5])). % 111.73/111.73 cnf(32,plain, % 111.73/111.73 (P2(f1(f5(x321)),a3)+P2(f1(x321),a3)), % 111.73/111.73 inference(scs_inference,[],[2,28])). % 111.73/111.73 cnf(33,plain, % 111.73/111.73 (P2(f1(f5(f5(x331))),a3)+~P2(f1(x331),a3)), % 111.73/111.73 inference(scs_inference,[],[1,32,6])). % 111.73/111.73 cnf(37,plain, % 111.73/111.73 (~P2(f1(x371),a3)+P2(f1(f5(x371)),a2)), % 111.73/111.73 inference(scs_inference,[],[1,2,6])). % 111.73/111.73 cnf(49,plain, % 111.73/111.73 (~P2(f1(f5(x491)),a2)+P2(f1(x491),a3)), % 111.73/111.73 inference(scs_inference,[],[1,2,5])). % 111.73/111.73 cnf(124,plain, % 111.73/111.73 (~P2(f1(f5(x1241)),a2)+~P2(f1(f5(x1241)),a3)), % 111.73/111.73 inference(scs_inference,[],[1,49,6])). % 111.73/111.73 cnf(125,plain, % 111.73/111.73 (~P2(f1(f5(x1251)),a3)+~P2(f1(x1251),a3)), % 111.73/111.73 inference(scs_inference,[],[124,37])). % 111.73/111.73 cnf(169,plain, % 111.73/111.73 (~P2(f1(f4(f5(x1691),x1692)),a2)+P2(f1(x1691),a3)), % 111.73/111.73 inference(scs_inference,[],[10,5,2])). % 111.73/111.73 cnf(314,plain, % 111.73/111.73 (~P2(f1(x3141),a3)+~P2(f1(f5(f5(f5(x3141)))),a3)), % 111.73/111.73 inference(scs_inference,[],[125,33])). % 111.73/111.73 cnf(626,plain, % 111.73/111.73 (~P2(f1(f5(f5(f5(x6261)))),a3)+~P2(f1(f4(f5(x6261),x6262)),a2)), % 111.73/111.73 inference(scs_inference,[],[314,169])). % 111.73/111.73 cnf(627,plain, % 111.73/111.73 (~P2(f1(f4(f5(x6271),x6272)),a2)+~P2(f1(f5(f5(x6271))),a2)), % 111.73/111.73 inference(scs_inference,[],[626,28])). % 111.73/111.73 cnf(628,plain, % 111.73/111.73 (~P2(f1(f5(f5(x6281))),a2)+P2(f1(f4(f5(x6281),x6282)),a3)), % 111.73/111.73 inference(scs_inference,[],[627,2])). % 111.73/111.73 cnf(629,plain, % 111.73/111.73 (P2(f1(f4(f5(x6291),x6292)),a3)+~P2(f1(f5(x6291)),a3)), % 111.73/111.73 inference(scs_inference,[],[628,37])). % 111.73/111.73 cnf(630,plain, % 111.73/111.73 (~P2(f1(x6301),a3)+~P2(f1(f5(x6302)),a3)), % 111.73/111.73 inference(scs_inference,[],[629,26])). % 111.73/111.73 cnf(631,plain, % 111.73/111.73 (P2(f1(x6311),a3)), % 111.73/111.73 inference(scs_inference,[],[630,32])). % 111.73/111.73 cnf(633,plain, % 111.73/111.73 ($false), % 111.73/111.73 inference(scs_inference,[],[631,630]), % 111.73/111.73 ['proof']). % 111.73/111.73 % SZS output end Proof % 111.73/111.73 % Total time : 110.940000 s %------------------------------------------------------------------------------