%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO611-1 : TPTP v7.5.0. Released v7.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n014.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 0.63s 0.72s % Output : CNFRefutation 0.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYO611-1 : TPTP v7.5.0. Released v7.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n014.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 07:14:02 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.43 openjdk version "1.8.0_171" % 0.18/0.43 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.18/0.43 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.18/0.44 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.55/0.66 start to proof:theBenchmark % 0.63/0.72 % Version : CSE-F---1.0 % 0.63/0.72 % Problem : theBenchmark.p % 0.63/0.72 % Proof found % 0.63/0.72 % SZS status Theorem for theBenchmark.p % 0.63/0.72 % SZS output start Proof % 0.63/0.72 [1]P1(x11,x11) % 0.63/0.72 [2]P2(f1(x21),a2) % 0.63/0.72 [3]P1(x31,x32)+~P1(f3(x33,x31),x32) % 0.63/0.72 [4]P1(x41,x42)+~P1(f3(x41,x43),x42) % 0.63/0.72 [5]~P1(f4(x51),x52)+~P2(f1(x52),a2)+~P2(f1(x51),a2) % 0.63/0.72 cnf(6,plain, % 0.63/0.72 (P1(x61,f3(x62,x61))), % 0.63/0.72 inference(scs_inference,[],[1,3])). % 0.63/0.72 cnf(14,plain, % 0.63/0.72 (P1(x141,f3(x142,f3(x143,x141)))), % 0.63/0.72 inference(scs_inference,[],[6,3])). % 0.63/0.72 cnf(30,plain, % 0.63/0.72 (~P2(f1(x301),a2)), % 0.63/0.72 inference(scs_inference,[],[14,2,3,5])). % 0.63/0.72 cnf(31,plain, % 0.63/0.72 ($false), % 0.63/0.72 inference(scs_inference,[],[30,2]), % 0.63/0.72 ['proof']). % 0.63/0.72 % SZS output end Proof % 0.63/0.72 % Total time : 0.010000 s %------------------------------------------------------------------------------