%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN010-1.005.005 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n001.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:14 EDT 2024 % Result : Unsatisfiable 0.51s 0.62s % Output : CNFRefutation 0.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYN010-1.005.005 : TPTP v8.2.0. Released v1.0.0. % 0.06/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n001.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Sun Jun 23 19:29:38 EDT 2024 % 0.12/0.32 % CPUTime : % 0.51/0.58 start to proof:theBenchmark % 0.51/0.61 %------------------------------------------- % 0.51/0.61 % File :CSE---1.7 % 0.51/0.61 % Problem :theBenchmark % 0.51/0.61 % Transform :cnf % 0.51/0.61 % Format :tptp:raw % 0.51/0.61 % Command :java -jar mcs_scs.jar %d %s % 0.51/0.61 % 0.51/0.61 % Result :Theorem 0.000000s % 0.51/0.61 % Output :CNFRefutation 0.000000s % 0.51/0.61 %------------------------------------------- % 0.51/0.62 %-------------------------------------------------------------------------- % 0.51/0.62 % File : SYN010-1.005.005 : TPTP v8.2.0. Released v1.0.0. % 0.51/0.62 % Domain : Syntactic % 0.51/0.62 % Problem : Example for Proposition 5.2 in [LMG94] % 0.51/0.62 % Version : Biased. % 0.51/0.62 % English : Example to show that connection tableaux with factorization % 0.51/0.62 % cannot polynomially simulate simulate connection tableaux with % 0.51/0.62 % folding up. % 0.51/0.62 % 0.51/0.62 % Refs : [LMG94] Letz et al. (1994), Controlled Integration of the Cut % 0.51/0.62 % Source : [LMG94] % 0.51/0.62 % Names : Example 5.1 [LMG94] % 0.51/0.62 % 0.51/0.62 % Status : Unsatisfiable % 0.51/0.62 % Rating : 0.00 v2.1.0 % 0.51/0.62 % Syntax : Number of clauses : 27 ( 6 unt; 0 nHn; 27 RR) % 0.51/0.62 % Number of literals : 132 ( 0 equ; 106 neg) % 0.51/0.62 % Maximal clause size : 6 ( 4 avg) % 0.51/0.62 % Maximal term depth : 0 ( 0 avg) % 0.51/0.62 % Number of predicates : 26 ( 26 usr; 26 prp; 0-0 aty) % 0.51/0.62 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 0.51/0.62 % Number of variables : 0 ( 0 sgn) % 0.51/0.62 % SPC : CNF_UNS_PRP % 0.51/0.62 % 0.51/0.62 % Comments : Biased towards folding up. % 0.51/0.62 % : tptp2X: -f tptp -s5:5 SYN010-1.g % 0.51/0.62 %-------------------------------------------------------------------------- % 0.51/0.62 cnf(clause_1,negated_conjecture, % 0.51/0.62 ~ p_0 ). % 0.51/0.62 % 0.51/0.62 cnf(clause_2,negated_conjecture, % 0.51/0.62 ( p_0 % 0.51/0.62 | ~ p_1_1 % 0.51/0.62 | ~ p_1_2 % 0.51/0.62 | ~ p_1_3 % 0.51/0.62 | ~ p_1_4 % 0.51/0.62 | ~ p_1_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_3,negated_conjecture, % 0.51/0.62 ( p_1_1 % 0.51/0.62 | ~ p_2_1 % 0.51/0.62 | ~ p_2_2 % 0.51/0.62 | ~ p_2_3 % 0.51/0.62 | ~ p_2_4 % 0.51/0.62 | ~ p_2_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_4,negated_conjecture, % 0.51/0.62 ( p_1_2 % 0.51/0.62 | ~ p_2_1 % 0.51/0.62 | ~ p_2_2 % 0.51/0.62 | ~ p_2_3 % 0.51/0.62 | ~ p_2_4 % 0.51/0.62 | ~ p_2_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_5,negated_conjecture, % 0.51/0.62 ( p_1_3 % 0.51/0.62 | ~ p_2_1 % 0.51/0.62 | ~ p_2_2 % 0.51/0.62 | ~ p_2_3 % 0.51/0.62 | ~ p_2_4 % 0.51/0.62 | ~ p_2_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_6,negated_conjecture, % 0.51/0.62 ( p_1_4 % 0.51/0.62 | ~ p_2_1 % 0.51/0.62 | ~ p_2_2 % 0.51/0.62 | ~ p_2_3 % 0.51/0.62 | ~ p_2_4 % 0.51/0.62 | ~ p_2_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_7,negated_conjecture, % 0.51/0.62 ( p_1_5 % 0.51/0.62 | ~ p_2_1 % 0.51/0.62 | ~ p_2_2 % 0.51/0.62 | ~ p_2_3 % 0.51/0.62 | ~ p_2_4 % 0.51/0.62 | ~ p_2_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_8,negated_conjecture, % 0.51/0.62 ( p_2_1 % 0.51/0.62 | ~ p_3_1 % 0.51/0.62 | ~ p_3_2 % 0.51/0.62 | ~ p_3_3 % 0.51/0.62 | ~ p_3_4 % 0.51/0.62 | ~ p_3_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_9,negated_conjecture, % 0.51/0.62 ( p_2_2 % 0.51/0.62 | ~ p_3_1 % 0.51/0.62 | ~ p_3_2 % 0.51/0.62 | ~ p_3_3 % 0.51/0.62 | ~ p_3_4 % 0.51/0.62 | ~ p_3_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_10,negated_conjecture, % 0.51/0.62 ( p_2_3 % 0.51/0.62 | ~ p_3_1 % 0.51/0.62 | ~ p_3_2 % 0.51/0.62 | ~ p_3_3 % 0.51/0.62 | ~ p_3_4 % 0.51/0.62 | ~ p_3_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_11,negated_conjecture, % 0.51/0.62 ( p_2_4 % 0.51/0.62 | ~ p_3_1 % 0.51/0.62 | ~ p_3_2 % 0.51/0.62 | ~ p_3_3 % 0.51/0.62 | ~ p_3_4 % 0.51/0.62 | ~ p_3_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_12,negated_conjecture, % 0.51/0.62 ( p_2_5 % 0.51/0.62 | ~ p_3_1 % 0.51/0.62 | ~ p_3_2 % 0.51/0.62 | ~ p_3_3 % 0.51/0.62 | ~ p_3_4 % 0.51/0.62 | ~ p_3_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_13,negated_conjecture, % 0.51/0.62 ( p_3_1 % 0.51/0.62 | ~ p_4_1 % 0.51/0.62 | ~ p_4_2 % 0.51/0.62 | ~ p_4_3 % 0.51/0.62 | ~ p_4_4 % 0.51/0.62 | ~ p_4_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_14,negated_conjecture, % 0.51/0.62 ( p_3_2 % 0.51/0.62 | ~ p_4_1 % 0.51/0.62 | ~ p_4_2 % 0.51/0.62 | ~ p_4_3 % 0.51/0.62 | ~ p_4_4 % 0.51/0.62 | ~ p_4_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_15,negated_conjecture, % 0.51/0.62 ( p_3_3 % 0.51/0.62 | ~ p_4_1 % 0.51/0.62 | ~ p_4_2 % 0.51/0.62 | ~ p_4_3 % 0.51/0.62 | ~ p_4_4 % 0.51/0.62 | ~ p_4_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_16,negated_conjecture, % 0.51/0.62 ( p_3_4 % 0.51/0.62 | ~ p_4_1 % 0.51/0.62 | ~ p_4_2 % 0.51/0.62 | ~ p_4_3 % 0.51/0.62 | ~ p_4_4 % 0.51/0.62 | ~ p_4_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_17,negated_conjecture, % 0.51/0.62 ( p_3_5 % 0.51/0.62 | ~ p_4_1 % 0.51/0.62 | ~ p_4_2 % 0.51/0.62 | ~ p_4_3 % 0.51/0.62 | ~ p_4_4 % 0.51/0.62 | ~ p_4_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_18,negated_conjecture, % 0.51/0.62 ( p_4_1 % 0.51/0.62 | ~ p_5_1 % 0.51/0.62 | ~ p_5_2 % 0.51/0.62 | ~ p_5_3 % 0.51/0.62 | ~ p_5_4 % 0.51/0.62 | ~ p_5_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_19,negated_conjecture, % 0.51/0.62 ( p_4_2 % 0.51/0.62 | ~ p_5_1 % 0.51/0.62 | ~ p_5_2 % 0.51/0.62 | ~ p_5_3 % 0.51/0.62 | ~ p_5_4 % 0.51/0.62 | ~ p_5_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_20,negated_conjecture, % 0.51/0.62 ( p_4_3 % 0.51/0.62 | ~ p_5_1 % 0.51/0.62 | ~ p_5_2 % 0.51/0.62 | ~ p_5_3 % 0.51/0.62 | ~ p_5_4 % 0.51/0.62 | ~ p_5_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_21,negated_conjecture, % 0.51/0.62 ( p_4_4 % 0.51/0.62 | ~ p_5_1 % 0.51/0.62 | ~ p_5_2 % 0.51/0.62 | ~ p_5_3 % 0.51/0.62 | ~ p_5_4 % 0.51/0.62 | ~ p_5_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_22,negated_conjecture, % 0.51/0.62 ( p_4_5 % 0.51/0.62 | ~ p_5_1 % 0.51/0.62 | ~ p_5_2 % 0.51/0.62 | ~ p_5_3 % 0.51/0.62 | ~ p_5_4 % 0.51/0.62 | ~ p_5_5 ) ). % 0.51/0.62 % 0.51/0.62 cnf(clause_23,negated_conjecture, % 0.51/0.62 p_5_1 ). % 0.51/0.62 % 0.51/0.62 cnf(clause_24,negated_conjecture, % 0.51/0.62 p_5_2 ). % 0.51/0.62 % 0.51/0.62 cnf(clause_25,negated_conjecture, % 0.51/0.62 p_5_3 ). % 0.51/0.62 % 0.51/0.62 cnf(clause_26,negated_conjecture, % 0.51/0.62 p_5_4 ). % 0.51/0.62 % 0.51/0.62 cnf(clause_27,negated_conjecture, % 0.51/0.62 p_5_5 ). % 0.51/0.62 % 0.51/0.62 %-------------------------------------------------------------------------- % 0.51/0.62 %------------------------------------------- % 0.51/0.62 % Proof found % 0.51/0.62 % SZS status Theorem for theBenchmark % 0.51/0.62 % SZS output start Proof % 0.51/0.62 %ClaNum:27(EqnAxiom:0) % 0.51/0.62 %VarNum:0(SingletonVarNum:0) % 0.51/0.62 %MaxLitNum:6 % 0.51/0.62 %MaxfuncDepth:0 % 0.51/0.62 %SharedTerms:53 % 0.51/0.62 %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 25 26 27 % 0.51/0.62 %singleGoalClaCount:6 % 0.51/0.62 [1]P1(a5000) % 0.51/0.62 [2]P23(a5000) % 0.51/0.62 [3]P24(a5000) % 0.51/0.62 [4]P25(a5000) % 0.51/0.62 [5]P26(a5000) % 0.51/0.62 [6]~P2(a5000) % 0.51/0.62 [7]P2(a5000)+~P3(a5000)+~P4(a5000)+~P5(a5000)+~P6(a5000)+~P7(a5000) % 0.51/0.62 [8]P3(a5000)+~P8(a5000)+~P9(a5000)+~P10(a5000)+~P11(a5000)+~P12(a5000) % 0.51/0.62 [9]P4(a5000)+~P8(a5000)+~P9(a5000)+~P10(a5000)+~P11(a5000)+~P12(a5000) % 0.51/0.62 [10]P5(a5000)+~P8(a5000)+~P9(a5000)+~P10(a5000)+~P11(a5000)+~P12(a5000) % 0.51/0.62 [11]P6(a5000)+~P8(a5000)+~P9(a5000)+~P10(a5000)+~P11(a5000)+~P12(a5000) % 0.51/0.62 [12]P7(a5000)+~P8(a5000)+~P9(a5000)+~P10(a5000)+~P11(a5000)+~P12(a5000) % 0.51/0.62 [13]P8(a5000)+~P13(a5000)+~P14(a5000)+~P15(a5000)+~P16(a5000)+~P17(a5000) % 0.51/0.62 [14]P9(a5000)+~P13(a5000)+~P14(a5000)+~P15(a5000)+~P16(a5000)+~P17(a5000) % 0.51/0.62 [15]P10(a5000)+~P13(a5000)+~P14(a5000)+~P15(a5000)+~P16(a5000)+~P17(a5000) % 0.51/0.62 [16]P11(a5000)+~P13(a5000)+~P14(a5000)+~P15(a5000)+~P16(a5000)+~P17(a5000) % 0.51/0.62 [17]P12(a5000)+~P13(a5000)+~P14(a5000)+~P15(a5000)+~P16(a5000)+~P17(a5000) % 0.51/0.62 [18]P13(a5000)+~P18(a5000)+~P19(a5000)+~P20(a5000)+~P21(a5000)+~P22(a5000) % 0.51/0.62 [19]P14(a5000)+~P18(a5000)+~P19(a5000)+~P20(a5000)+~P21(a5000)+~P22(a5000) % 0.51/0.62 [20]P15(a5000)+~P18(a5000)+~P19(a5000)+~P20(a5000)+~P21(a5000)+~P22(a5000) % 0.51/0.62 [21]P16(a5000)+~P18(a5000)+~P19(a5000)+~P20(a5000)+~P21(a5000)+~P22(a5000) % 0.51/0.62 [22]P17(a5000)+~P18(a5000)+~P19(a5000)+~P20(a5000)+~P21(a5000)+~P22(a5000) % 0.51/0.62 [23]P18(a5000)+~P1(a5000)+~P23(a5000)+~P24(a5000)+~P25(a5000)+~P26(a5000) % 0.51/0.62 [24]P19(a5000)+~P1(a5000)+~P23(a5000)+~P24(a5000)+~P25(a5000)+~P26(a5000) % 0.51/0.62 [25]P20(a5000)+~P1(a5000)+~P23(a5000)+~P24(a5000)+~P25(a5000)+~P26(a5000) % 0.51/0.62 [26]P21(a5000)+~P1(a5000)+~P23(a5000)+~P24(a5000)+~P25(a5000)+~P26(a5000) % 0.51/0.62 [27]P22(a5000)+~P1(a5000)+~P23(a5000)+~P24(a5000)+~P25(a5000)+~P26(a5000) % 0.51/0.62 %EqnAxiom % 0.51/0.62 % 0.51/0.62 %------------------------------------------- % 0.51/0.62 cnf(28,plain, % 0.51/0.62 (~P4(a5000)+~P5(a5000)+~P6(a5000)+~P7(a5000)+~P9(a5000)+~P10(a5000)+~P11(a5000)+~P12(a5000)+~P8(a5000)), % 0.51/0.62 inference(scs_inference,[],[6,7,8])). % 0.51/0.62 cnf(30,plain, % 0.51/0.62 (P18(a5000)), % 0.51/0.62 inference(scs_inference,[],[1,2,3,4,5,23])). % 0.51/0.62 cnf(31,plain, % 0.51/0.62 (P19(a5000)), % 0.51/0.62 inference(scs_inference,[],[1,2,3,4,5,24])). % 0.51/0.62 cnf(32,plain, % 0.51/0.63 (P20(a5000)), % 0.51/0.63 inference(scs_inference,[],[1,2,3,4,5,25])). % 0.51/0.63 cnf(33,plain, % 0.51/0.63 (P21(a5000)), % 0.51/0.63 inference(scs_inference,[],[1,2,3,4,5,26])). % 0.51/0.63 cnf(34,plain, % 0.51/0.63 (P22(a5000)), % 0.51/0.63 inference(scs_inference,[],[1,2,3,4,5,27])). % 0.51/0.63 cnf(35,plain, % 0.51/0.63 (P13(a5000)), % 0.51/0.63 inference(scs_inference,[],[30,31,32,33,34,18])). % 0.51/0.63 cnf(36,plain, % 0.51/0.63 (P14(a5000)), % 0.51/0.63 inference(scs_inference,[],[30,31,32,33,34,19])). % 0.51/0.63 cnf(37,plain, % 0.51/0.63 (P15(a5000)), % 0.51/0.63 inference(scs_inference,[],[30,31,32,33,34,20])). % 0.51/0.63 cnf(38,plain, % 0.51/0.63 (P16(a5000)), % 0.51/0.63 inference(scs_inference,[],[30,31,32,33,34,21])). % 0.51/0.63 cnf(39,plain, % 0.51/0.63 (P17(a5000)), % 0.51/0.63 inference(scs_inference,[],[30,31,32,33,34,22])). % 0.51/0.63 cnf(40,plain, % 0.51/0.63 (P8(a5000)), % 0.51/0.63 inference(scs_inference,[],[35,36,37,38,39,13])). % 0.51/0.63 cnf(41,plain, % 0.51/0.63 (P9(a5000)), % 0.51/0.63 inference(scs_inference,[],[35,36,37,38,39,14])). % 0.51/0.63 cnf(42,plain, % 0.51/0.63 (P10(a5000)), % 0.51/0.63 inference(scs_inference,[],[35,36,37,38,39,15])). % 0.51/0.63 cnf(43,plain, % 0.51/0.63 (P11(a5000)), % 0.51/0.63 inference(scs_inference,[],[35,36,37,38,39,16])). % 0.51/0.63 cnf(44,plain, % 0.51/0.63 (P12(a5000)), % 0.51/0.63 inference(scs_inference,[],[35,36,37,38,39,17])). % 0.51/0.63 cnf(46,plain, % 0.51/0.63 (P4(a5000)), % 0.51/0.63 inference(scs_inference,[],[40,41,42,43,44,9])). % 0.51/0.63 cnf(47,plain, % 0.51/0.63 (P5(a5000)), % 0.51/0.63 inference(scs_inference,[],[40,41,42,43,44,10])). % 0.51/0.63 cnf(48,plain, % 0.51/0.63 (P6(a5000)), % 0.51/0.63 inference(scs_inference,[],[40,41,42,43,44,11])). % 0.51/0.63 cnf(49,plain, % 0.51/0.63 (P7(a5000)), % 0.51/0.63 inference(scs_inference,[],[40,41,42,43,44,12])). % 0.51/0.63 cnf(50,plain, % 0.51/0.63 (~P4(a5000)+~P5(a5000)+~P6(a5000)+~P7(a5000)), % 0.51/0.63 inference(scs_inference,[],[41,42,43,44,40,28])). % 0.51/0.63 cnf(52,plain, % 0.51/0.63 ($false), % 0.51/0.63 inference(scs_inference,[],[46,47,48,49,50]), % 0.51/0.63 ['proof']). % 0.51/0.63 % SZS output end Proof % 0.51/0.63 % Total time :0.000000s %------------------------------------------------------------------------------