%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN003-1.006 : TPTP v8.2.0. Released v1.0.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 : 300s % DateTime : Mon Jun 24 19:04:12 EDT 2024 % Result : Unsatisfiable 0.51s 0.61s % Output : CNFRefutation 0.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYN003-1.006 : TPTP v8.2.0. Released v1.0.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n021.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 18:33:38 EDT 2024 % 0.11/0.33 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 0.51/0.60 %------------------------------------------- % 0.51/0.60 % File :CSE---1.7 % 0.51/0.60 % Problem :theBenchmark % 0.51/0.60 % Transform :cnf % 0.51/0.60 % Format :tptp:raw % 0.51/0.60 % Command :java -jar mcs_scs.jar %d %s % 0.51/0.60 % 0.51/0.60 % Result :Theorem 0.000000s % 0.51/0.60 % Output :CNFRefutation 0.000000s % 0.51/0.60 %------------------------------------------- % 0.51/0.61 %-------------------------------------------------------------------------- % 0.51/0.61 % File : SYN003-1.006 : TPTP v8.2.0. Released v1.0.0. % 0.51/0.61 % Domain : Syntactic % 0.51/0.61 % Problem : Implications that form a contradiction % 0.51/0.61 % Version : Biased. % 0.51/0.61 % English : P1 & Q1 -> P2 P1 & R1 -> P2 Q -> Q1 R -> R1 : % 0.51/0.61 % P2 & Q2 -> P3 P2 & R2 -> P3 Q -> Q2 R -> R2 : % 0.51/0.61 % ...... ...... .... .... : % 0.51/0.61 % Pk-1 & Qk-1 ->Pk Pk-1 & Rk-1 -> Pk Q -> Qk-1 R -> Rk-1 : % 0.51/0.61 % P1 ~Pk Q R : % 0.51/0.61 % : The size is k, in the above. % 0.51/0.61 % 0.51/0.61 % Refs : [Pla82] Plaisted (1982), A Simplified Problem Reduction Format % 0.51/0.61 % Source : [Pla82] % 0.51/0.61 % Names : Problem 5.2 [Pla82] % 0.51/0.61 % 0.51/0.61 % Status : Unsatisfiable % 0.51/0.61 % Rating : 0.00 v2.1.0 % 0.51/0.61 % Syntax : Number of clauses : 24 ( 4 unt; 0 nHn; 24 RR) % 0.51/0.61 % Number of literals : 54 ( 0 equ; 31 neg) % 0.51/0.61 % Maximal clause size : 3 ( 2 avg) % 0.51/0.61 % Maximal term depth : 0 ( 0 avg) % 0.51/0.61 % Number of predicates : 18 ( 18 usr; 18 prp; 0-0 aty) % 0.51/0.61 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 0.51/0.61 % Number of variables : 0 ( 0 sgn) % 0.51/0.61 % SPC : CNF_UNS_PRP % 0.51/0.61 % 0.51/0.61 % Comments : "This set of clauses can cause the following strategies to % 0.51/0.61 % generate a search space which is exponential in k: All-negative % 0.51/0.61 % resolution, set-of-support with ~Pk as the support set, input % 0.51/0.61 % resolution, SL-resolution, locking resolution with a bad choice % 0.51/0.61 % of indices, and ancestor-filter form (linear resolution)." % 0.51/0.61 % [Pla82] p.243. % 0.51/0.61 % : tptp2X: -f tptp -s6 SYN003-1.g % 0.51/0.61 %-------------------------------------------------------------------------- % 0.51/0.61 cnf(pqp_1,negated_conjecture, % 0.51/0.61 ( ~ p_1 % 0.51/0.61 | ~ q_1 % 0.51/0.61 | p_2 ) ). % 0.51/0.61 % 0.51/0.61 cnf(pqp_2,negated_conjecture, % 0.51/0.61 ( ~ p_2 % 0.51/0.61 | ~ q_2 % 0.51/0.61 | p_3 ) ). % 0.51/0.61 % 0.51/0.61 cnf(pqp_3,negated_conjecture, % 0.51/0.61 ( ~ p_3 % 0.51/0.61 | ~ q_3 % 0.51/0.61 | p_4 ) ). % 0.51/0.61 % 0.51/0.61 cnf(pqp_4,negated_conjecture, % 0.51/0.61 ( ~ p_4 % 0.51/0.61 | ~ q_4 % 0.51/0.61 | p_5 ) ). % 0.51/0.61 % 0.51/0.61 cnf(pqp_5,negated_conjecture, % 0.51/0.61 ( ~ p_5 % 0.51/0.61 | ~ q_5 % 0.51/0.61 | p_6 ) ). % 0.51/0.61 % 0.51/0.61 cnf(prp_1,negated_conjecture, % 0.51/0.61 ( ~ p_1 % 0.51/0.61 | ~ r_1 % 0.51/0.61 | p_2 ) ). % 0.51/0.61 % 0.51/0.61 cnf(prp_2,negated_conjecture, % 0.51/0.61 ( ~ p_2 % 0.51/0.61 | ~ r_2 % 0.51/0.61 | p_3 ) ). % 0.51/0.61 % 0.51/0.61 cnf(prp_3,negated_conjecture, % 0.51/0.61 ( ~ p_3 % 0.51/0.61 | ~ r_3 % 0.51/0.61 | p_4 ) ). % 0.51/0.61 % 0.51/0.61 cnf(prp_4,negated_conjecture, % 0.51/0.61 ( ~ p_4 % 0.51/0.61 | ~ r_4 % 0.51/0.61 | p_5 ) ). % 0.51/0.61 % 0.51/0.61 cnf(prp_5,negated_conjecture, % 0.51/0.61 ( ~ p_5 % 0.51/0.61 | ~ r_5 % 0.51/0.61 | p_6 ) ). % 0.51/0.61 % 0.51/0.61 cnf(qq_1,negated_conjecture, % 0.51/0.61 ( ~ q % 0.51/0.61 | q_1 ) ). % 0.51/0.61 % 0.51/0.61 cnf(qq_2,negated_conjecture, % 0.51/0.61 ( ~ q % 0.51/0.61 | q_2 ) ). % 0.51/0.61 % 0.51/0.61 cnf(qq_3,negated_conjecture, % 0.51/0.61 ( ~ q % 0.51/0.61 | q_3 ) ). % 0.51/0.61 % 0.51/0.61 cnf(qq_4,negated_conjecture, % 0.51/0.61 ( ~ q % 0.51/0.61 | q_4 ) ). % 0.51/0.61 % 0.51/0.61 cnf(qq_5,negated_conjecture, % 0.51/0.61 ( ~ q % 0.51/0.61 | q_5 ) ). % 0.51/0.61 % 0.51/0.61 cnf(rr_1,negated_conjecture, % 0.51/0.61 ( ~ r % 0.51/0.61 | r_1 ) ). % 0.51/0.61 % 0.51/0.61 cnf(rr_2,negated_conjecture, % 0.51/0.61 ( ~ r % 0.51/0.61 | r_2 ) ). % 0.51/0.61 % 0.51/0.61 cnf(rr_3,negated_conjecture, % 0.51/0.61 ( ~ r % 0.51/0.61 | r_3 ) ). % 0.51/0.61 % 0.51/0.61 cnf(rr_4,negated_conjecture, % 0.51/0.61 ( ~ r % 0.51/0.61 | r_4 ) ). % 0.51/0.61 % 0.51/0.61 cnf(rr_5,negated_conjecture, % 0.51/0.61 ( ~ r % 0.51/0.61 | r_5 ) ). % 0.51/0.61 % 0.51/0.61 cnf(base_1,negated_conjecture, % 0.51/0.61 p_1 ). % 0.51/0.61 % 0.51/0.61 cnf(base_2,negated_conjecture, % 0.51/0.61 ~ p_6 ). % 0.51/0.61 % 0.51/0.61 cnf(base_3,negated_conjecture, % 0.51/0.61 q ). % 0.51/0.61 % 0.51/0.61 cnf(base_4,negated_conjecture, % 0.51/0.61 r ). % 0.51/0.61 % 0.51/0.61 %-------------------------------------------------------------------------- % 0.51/0.61 %------------------------------------------- % 0.51/0.61 % Proof found % 0.51/0.61 % SZS status Theorem for theBenchmark % 0.51/0.61 % SZS output start Proof % 0.51/0.61 %ClaNum:24(EqnAxiom:0) % 0.51/0.61 %VarNum:0(SingletonVarNum:0) % 0.51/0.61 %MaxLitNum:3 % 0.51/0.61 %MaxfuncDepth:0 % 0.51/0.61 %SharedTerms:37 % 0.51/0.61 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 % 0.51/0.61 %singleGoalClaCount:4 % 0.51/0.61 [1]P1(a5000) % 0.51/0.61 [2]P2(a5000) % 0.51/0.61 [3]P8(a5000) % 0.51/0.61 [4]~P3(a5000) % 0.51/0.61 [5]P9(a5000)+~P2(a5000) % 0.51/0.61 [6]P10(a5000)+~P2(a5000) % 0.51/0.61 [7]P11(a5000)+~P2(a5000) % 0.51/0.61 [8]P12(a5000)+~P2(a5000) % 0.51/0.61 [9]P13(a5000)+~P2(a5000) % 0.51/0.61 [10]P14(a5000)+~P8(a5000) % 0.51/0.61 [11]P15(a5000)+~P8(a5000) % 0.51/0.61 [12]P16(a5000)+~P8(a5000) % 0.51/0.61 [13]P17(a5000)+~P8(a5000) % 0.51/0.61 [14]P18(a5000)+~P8(a5000) % 0.51/0.61 [15]P4(a5000)+~P1(a5000)+~P9(a5000) % 0.51/0.61 [16]P4(a5000)+~P1(a5000)+~P14(a5000) % 0.51/0.61 [17]P5(a5000)+~P4(a5000)+~P10(a5000) % 0.51/0.61 [18]P5(a5000)+~P4(a5000)+~P15(a5000) % 0.51/0.61 [19]P6(a5000)+~P5(a5000)+~P11(a5000) % 0.51/0.61 [20]P6(a5000)+~P5(a5000)+~P16(a5000) % 0.51/0.61 [21]P7(a5000)+~P6(a5000)+~P12(a5000) % 0.51/0.61 [22]P7(a5000)+~P6(a5000)+~P17(a5000) % 0.51/0.61 [23]P3(a5000)+~P7(a5000)+~P13(a5000) % 0.51/0.61 [24]P3(a5000)+~P7(a5000)+~P18(a5000) % 0.51/0.61 %EqnAxiom % 0.51/0.61 % 0.51/0.61 %------------------------------------------- % 0.51/0.61 cnf(25,plain, % 0.51/0.61 (~P7(a5000)+~P13(a5000)), % 0.51/0.61 inference(scs_inference,[],[4,23])). % 0.51/0.61 cnf(27,plain, % 0.51/0.61 (P9(a5000)), % 0.51/0.61 inference(scs_inference,[],[2,5])). % 0.51/0.61 cnf(28,plain, % 0.51/0.61 (P10(a5000)), % 0.51/0.61 inference(scs_inference,[],[2,6])). % 0.51/0.61 cnf(29,plain, % 0.51/0.61 (P11(a5000)), % 0.51/0.61 inference(scs_inference,[],[2,7])). % 0.51/0.61 cnf(30,plain, % 0.51/0.61 (P12(a5000)), % 0.51/0.61 inference(scs_inference,[],[2,8])). % 0.51/0.61 cnf(31,plain, % 0.51/0.61 (P13(a5000)), % 0.51/0.61 inference(scs_inference,[],[2,9])). % 0.51/0.61 cnf(37,plain, % 0.51/0.61 (P4(a5000)+~P9(a5000)), % 0.51/0.61 inference(scs_inference,[],[1,15])). % 0.51/0.61 cnf(40,plain, % 0.51/0.61 (P5(a5000)+~P4(a5000)), % 0.51/0.61 inference(scs_inference,[],[28,17])). % 0.51/0.61 cnf(42,plain, % 0.51/0.61 (P6(a5000)+~P5(a5000)), % 0.51/0.61 inference(scs_inference,[],[29,19])). % 0.51/0.61 cnf(44,plain, % 0.51/0.61 (P7(a5000)+~P6(a5000)), % 0.51/0.61 inference(scs_inference,[],[30,21])). % 0.51/0.61 cnf(46,plain, % 0.51/0.61 (~P7(a5000)), % 0.51/0.61 inference(scs_inference,[],[31,25])). % 0.51/0.61 cnf(47,plain, % 0.51/0.61 (P4(a5000)), % 0.51/0.61 inference(scs_inference,[],[27,37])). % 0.51/0.61 cnf(50,plain, % 0.51/0.61 (~P4(a5000)+P6(a5000)), % 0.51/0.61 inference(scs_inference,[],[40,42])). % 0.51/0.61 cnf(53,plain, % 0.51/0.61 (~P6(a5000)), % 0.51/0.61 inference(scs_inference,[],[46,44])). % 0.51/0.61 cnf(55,plain, % 0.51/0.61 (P6(a5000)), % 0.51/0.61 inference(scs_inference,[],[47,50])). % 0.51/0.61 cnf(56,plain, % 0.51/0.61 ($false), % 0.51/0.61 inference(scs_inference,[],[53,55]), % 0.51/0.61 ['proof']). % 0.51/0.61 % SZS output end Proof % 0.51/0.61 % Total time :0.000000s %------------------------------------------------------------------------------