%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN098-1.002 : TPTP v8.2.0. Bugfixed v1.2.1. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:33 EDT 2024 % Result : Unsatisfiable 0.47s 0.57s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.09 % Problem : SYN098-1.002 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.03/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Sun Jun 23 21:11:23 EDT 2024 % 0.08/0.28 % CPUTime : % 0.14/0.45 start to proof:theBenchmark % 0.14/0.55 %------------------------------------------- % 0.14/0.55 % File :CSE---1.7 % 0.14/0.55 % Problem :theBenchmark % 0.14/0.55 % Transform :cnf % 0.14/0.55 % Format :tptp:raw % 0.14/0.55 % Command :java -jar mcs_scs.jar %d %s % 0.14/0.55 % 0.14/0.55 % Result :Theorem 0.070000s % 0.14/0.55 % Output :CNFRefutation 0.070000s % 0.14/0.55 %------------------------------------------- % 0.47/0.56 %-------------------------------------------------------------------------- % 0.47/0.56 % File : SYN098-1.002 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.47/0.56 % Domain : Syntactic % 0.47/0.56 % Problem : Plaisted problem sym(u(t(3,2))) % 0.47/0.56 % Version : Biased. % 0.47/0.56 % English : % 0.47/0.56 % 0.47/0.56 % Refs : [Pla94] Plaisted (1994), The Search Efficiency of Theorem Prov % 0.47/0.56 % Source : [Pla94] % 0.47/0.56 % Names : Sym(U(T3n)) [Pla94] % 0.47/0.56 % 0.47/0.56 % Status : Unsatisfiable % 0.47/0.56 % Rating : 0.33 v5.5.0, 0.00 v4.1.0, 0.20 v4.0.1, 0.00 v2.1.0 % 0.47/0.56 % Syntax : Number of clauses : 68 ( 2 unt; 25 nHn; 68 RR) % 0.47/0.56 % Number of literals : 176 ( 0 equ; 88 neg) % 0.47/0.56 % Maximal clause size : 4 ( 2 avg) % 0.47/0.56 % Maximal term depth : 0 ( 0 avg) % 0.47/0.56 % Number of predicates : 54 ( 54 usr; 54 prp; 0-0 aty) % 0.47/0.56 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 0.47/0.56 % Number of variables : 0 ( 0 sgn) % 0.47/0.56 % SPC : CNF_UNS_PRP % 0.47/0.56 % 0.47/0.56 % Comments : Biased away from various calculi. % 0.47/0.56 % : tptp2X: -f tptp -s2 SYN098-1.g % 0.47/0.56 % Bugfixes : v1.2.0 - Bugfix in SYN086-1. % 0.47/0.56 % : v1.2.1 - Bugfix in SYN086-1. % 0.47/0.56 %-------------------------------------------------------------------------- % 0.47/0.56 cnf(u_s3_goal_1,negated_conjecture, % 0.47/0.56 ( u_1 % 0.47/0.56 | ~ p_0 % 0.47/0.56 | ~ q_0 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_1_s3_goal_1,axiom, % 0.47/0.56 ~ u_1 ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type11_1,axiom, % 0.47/0.56 ( u_2 % 0.47/0.56 | p_0 % 0.47/0.56 | ~ p_1 % 0.47/0.56 | ~ p_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_2_s3_type11_1,axiom, % 0.47/0.56 ( p_0 % 0.47/0.56 | ~ u_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type11_2,axiom, % 0.47/0.56 ( u_3 % 0.47/0.56 | p_0 % 0.47/0.56 | ~ q_1 % 0.47/0.56 | ~ q_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_3_s3_type11_2,axiom, % 0.47/0.56 ( p_0 % 0.47/0.56 | ~ u_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type11_3,axiom, % 0.47/0.56 ( u_4 % 0.47/0.56 | p_1 % 0.47/0.56 | ~ p_2 % 0.47/0.56 | ~ p_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_4_s3_type11_3,axiom, % 0.47/0.56 ( p_1 % 0.47/0.56 | ~ u_4 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type11_4,axiom, % 0.47/0.56 ( u_5 % 0.47/0.56 | p_1 % 0.47/0.56 | ~ q_2 % 0.47/0.56 | ~ q_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_5_s3_type11_4,axiom, % 0.47/0.56 ( p_1 % 0.47/0.56 | ~ u_5 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type12_1,axiom, % 0.47/0.56 ( u_6 % 0.47/0.56 | q_0 % 0.47/0.56 | ~ p_1 % 0.47/0.56 | ~ q_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_6_s3_type12_1,axiom, % 0.47/0.56 ( q_0 % 0.47/0.56 | ~ u_6 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type12_2,axiom, % 0.47/0.56 ( u_7 % 0.47/0.56 | q_0 % 0.47/0.56 | ~ q_1 % 0.47/0.56 | ~ p_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_7_s3_type12_2,axiom, % 0.47/0.56 ( q_0 % 0.47/0.56 | ~ u_7 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type12_3,axiom, % 0.47/0.56 ( u_8 % 0.47/0.56 | q_1 % 0.47/0.56 | ~ p_2 % 0.47/0.56 | ~ q_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_8_s3_type12_3,axiom, % 0.47/0.56 ( q_1 % 0.47/0.56 | ~ u_8 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type12_4,axiom, % 0.47/0.56 ( u_9 % 0.47/0.56 | q_1 % 0.47/0.56 | ~ q_2 % 0.47/0.56 | ~ p_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_9_s3_type12_4,axiom, % 0.47/0.56 ( q_1 % 0.47/0.56 | ~ u_9 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type2_1,axiom, % 0.47/0.56 ( u_10 % 0.47/0.56 | p_3 % 0.47/0.56 | ~ p_1 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_10_s3_type2_1,axiom, % 0.47/0.56 ( p_3 % 0.47/0.56 | ~ u_10 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type2_2,axiom, % 0.47/0.56 ( u_11 % 0.47/0.56 | p_4 % 0.47/0.56 | ~ p_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_11_s3_type2_2,axiom, % 0.47/0.56 ( p_4 % 0.47/0.56 | ~ u_11 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type2_3,axiom, % 0.47/0.56 ( u_12 % 0.47/0.56 | q_3 % 0.47/0.56 | ~ q_1 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_12_s3_type2_3,axiom, % 0.47/0.56 ( q_3 % 0.47/0.56 | ~ u_12 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_s3_type2_4,axiom, % 0.47/0.56 ( u_13 % 0.47/0.56 | q_4 % 0.47/0.56 | ~ q_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_13_s3_type2_4,axiom, % 0.47/0.56 ( q_4 % 0.47/0.56 | ~ u_13 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_t3_1,axiom, % 0.47/0.56 ( u_14 % 0.47/0.56 | p_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_14_t3_1,axiom, % 0.47/0.56 ( p_2 % 0.47/0.56 | ~ u_14 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_t3_2,axiom, % 0.47/0.56 ( u_15 % 0.47/0.56 | p_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_15_t3_2,axiom, % 0.47/0.56 ( p_3 % 0.47/0.56 | ~ u_15 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_t3_3,axiom, % 0.47/0.56 ( u_16 % 0.47/0.56 | q_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_16_t3_3,axiom, % 0.47/0.56 ( q_2 % 0.47/0.56 | ~ u_16 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_t3_4,axiom, % 0.47/0.56 ( u_17 % 0.47/0.56 | q_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(u_17_t3_4,axiom, % 0.47/0.56 ( q_3 % 0.47/0.56 | ~ u_17 ) ). % 0.47/0.56 % 0.47/0.56 cnf(sym_u_s3_goal_1,axiom, % 0.47/0.56 ( ~ sym_u_1 % 0.47/0.56 | sym_p_0 % 0.47/0.56 | sym_q_0 ) ). % 0.47/0.56 % 0.47/0.56 cnf(sym_u_1_s3_goal_1,axiom, % 0.47/0.56 sym_u_1 ). % 0.47/0.56 % 0.47/0.56 cnf(sym_u_s3_type11_1,axiom, % 0.47/0.56 ( ~ sym_u_2 % 0.47/0.56 | ~ sym_p_0 % 0.47/0.56 | sym_p_1 % 0.47/0.56 | sym_p_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(sym_u_2_s3_type11_1,axiom, % 0.47/0.56 ( ~ sym_p_0 % 0.47/0.56 | sym_u_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(sym_u_s3_type11_2,axiom, % 0.47/0.56 ( ~ sym_u_3 % 0.47/0.56 | ~ sym_p_0 % 0.47/0.56 | sym_q_1 % 0.47/0.56 | sym_q_2 ) ). % 0.47/0.56 % 0.47/0.56 cnf(sym_u_3_s3_type11_2,axiom, % 0.47/0.56 ( ~ sym_p_0 % 0.47/0.56 | sym_u_3 ) ). % 0.47/0.56 % 0.47/0.56 cnf(sym_u_s3_type11_3,axiom, % 0.47/0.56 ( ~ sym_u_4 % 0.47/0.56 | ~ sym_p_1 % 0.47/0.56 | sym_p_2 % 0.47/0.56 | sym_p_3 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_4_s3_type11_3,axiom, % 0.47/0.57 ( ~ sym_p_1 % 0.47/0.57 | sym_u_4 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type11_4,axiom, % 0.47/0.57 ( ~ sym_u_5 % 0.47/0.57 | ~ sym_p_1 % 0.47/0.57 | sym_q_2 % 0.47/0.57 | sym_q_3 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_5_s3_type11_4,axiom, % 0.47/0.57 ( ~ sym_p_1 % 0.47/0.57 | sym_u_5 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type12_1,axiom, % 0.47/0.57 ( ~ sym_u_6 % 0.47/0.57 | ~ sym_q_0 % 0.47/0.57 | sym_p_1 % 0.47/0.57 | sym_q_2 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_6_s3_type12_1,axiom, % 0.47/0.57 ( ~ sym_q_0 % 0.47/0.57 | sym_u_6 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type12_2,axiom, % 0.47/0.57 ( ~ sym_u_7 % 0.47/0.57 | ~ sym_q_0 % 0.47/0.57 | sym_q_1 % 0.47/0.57 | sym_p_2 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_7_s3_type12_2,axiom, % 0.47/0.57 ( ~ sym_q_0 % 0.47/0.57 | sym_u_7 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type12_3,axiom, % 0.47/0.57 ( ~ sym_u_8 % 0.47/0.57 | ~ sym_q_1 % 0.47/0.57 | sym_p_2 % 0.47/0.57 | sym_q_3 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_8_s3_type12_3,axiom, % 0.47/0.57 ( ~ sym_q_1 % 0.47/0.57 | sym_u_8 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type12_4,axiom, % 0.47/0.57 ( ~ sym_u_9 % 0.47/0.57 | ~ sym_q_1 % 0.47/0.57 | sym_q_2 % 0.47/0.57 | sym_p_3 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_9_s3_type12_4,axiom, % 0.47/0.57 ( ~ sym_q_1 % 0.47/0.57 | sym_u_9 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type2_1,axiom, % 0.47/0.57 ( ~ sym_u_10 % 0.47/0.57 | ~ sym_p_3 % 0.47/0.57 | sym_p_1 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_10_s3_type2_1,axiom, % 0.47/0.57 ( ~ sym_p_3 % 0.47/0.57 | sym_u_10 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type2_2,axiom, % 0.47/0.57 ( ~ sym_u_11 % 0.47/0.57 | ~ sym_p_4 % 0.47/0.57 | sym_p_2 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_11_s3_type2_2,axiom, % 0.47/0.57 ( ~ sym_p_4 % 0.47/0.57 | sym_u_11 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type2_3,axiom, % 0.47/0.57 ( ~ sym_u_12 % 0.47/0.57 | ~ sym_q_3 % 0.47/0.57 | sym_q_1 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_12_s3_type2_3,axiom, % 0.47/0.57 ( ~ sym_q_3 % 0.47/0.57 | sym_u_12 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_s3_type2_4,axiom, % 0.47/0.57 ( ~ sym_u_13 % 0.47/0.57 | ~ sym_q_4 % 0.47/0.57 | sym_q_2 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_13_s3_type2_4,axiom, % 0.47/0.57 ( ~ sym_q_4 % 0.47/0.57 | sym_u_13 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_t3_1,axiom, % 0.47/0.57 ( ~ sym_u_14 % 0.47/0.57 | ~ sym_p_2 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_14_t3_1,axiom, % 0.47/0.57 ( ~ sym_p_2 % 0.47/0.57 | sym_u_14 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_t3_2,axiom, % 0.47/0.57 ( ~ sym_u_15 % 0.47/0.57 | ~ sym_p_3 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_15_t3_2,axiom, % 0.47/0.57 ( ~ sym_p_3 % 0.47/0.57 | sym_u_15 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_t3_3,axiom, % 0.47/0.57 ( ~ sym_u_16 % 0.47/0.57 | ~ sym_q_2 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_16_t3_3,axiom, % 0.47/0.57 ( ~ sym_q_2 % 0.47/0.57 | sym_u_16 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_t3_4,axiom, % 0.47/0.57 ( ~ sym_u_17 % 0.47/0.57 | ~ sym_q_3 ) ). % 0.47/0.57 % 0.47/0.57 cnf(sym_u_17_t3_4,axiom, % 0.47/0.57 ( ~ sym_q_3 % 0.47/0.57 | sym_u_17 ) ). % 0.47/0.57 % 0.47/0.57 %-------------------------------------------------------------------------- % 0.47/0.57 %------------------------------------------- % 0.47/0.57 % Proof found % 0.47/0.57 % SZS status Theorem for theBenchmark % 0.47/0.57 % SZS output start Proof % 0.47/0.57 %ClaNum:68(EqnAxiom:0) % 0.47/0.57 %VarNum:0(SingletonVarNum:0) % 0.47/0.57 %MaxLitNum:4 % 0.47/0.57 %MaxfuncDepth:0 % 0.47/0.57 %SharedTerms:105 % 0.47/0.57 %goalClause: 48 % 0.47/0.57 [1]P1(a5000) % 0.47/0.57 [2]~P22(a5000) % 0.47/0.57 [3]P2(a5000)+P39(a5000) % 0.47/0.57 [4]P5(a5000)+P44(a5000) % 0.47/0.57 [5]P6(a5000)+P45(a5000) % 0.47/0.57 [6]P10(a5000)+P46(a5000) % 0.47/0.57 [7]P3(a5000)+~P47(a5000) % 0.47/0.57 [8]P3(a5000)+~P48(a5000) % 0.47/0.57 [9]P7(a5000)+~P49(a5000) % 0.47/0.57 [10]P7(a5000)+~P52(a5000) % 0.47/0.57 [11]P4(a5000)+~P50(a5000) % 0.47/0.57 [12]P4(a5000)+~P51(a5000) % 0.47/0.57 [13]P2(a5000)+~P39(a5000) % 0.47/0.57 [14]P9(a5000)+~P53(a5000) % 0.47/0.57 [15]P9(a5000)+~P54(a5000) % 0.47/0.57 [16]P5(a5000)+~P44(a5000) % 0.47/0.57 [17]P6(a5000)+~P40(a5000) % 0.47/0.57 [18]P6(a5000)+~P45(a5000) % 0.47/0.57 [19]P10(a5000)+~P41(a5000) % 0.47/0.57 [20]P10(a5000)+~P46(a5000) % 0.47/0.57 [21]P8(a5000)+~P42(a5000) % 0.47/0.57 [22]P11(a5000)+~P43(a5000) % 0.47/0.57 [23]P23(a5000)+~P12(a5000) % 0.47/0.57 [24]P32(a5000)+~P12(a5000) % 0.47/0.57 [25]P33(a5000)+~P13(a5000) % 0.47/0.57 [26]P34(a5000)+~P13(a5000) % 0.47/0.57 [27]P35(a5000)+~P14(a5000) % 0.47/0.57 [28]P36(a5000)+~P14(a5000) % 0.47/0.57 [29]P37(a5000)+~P18(a5000) % 0.47/0.57 [30]P38(a5000)+~P18(a5000) % 0.47/0.57 [31]P24(a5000)+~P15(a5000) % 0.47/0.57 [32]P25(a5000)+~P17(a5000) % 0.47/0.57 [33]P26(a5000)+~P19(a5000) % 0.47/0.57 [34]P27(a5000)+~P21(a5000) % 0.47/0.57 [35]P28(a5000)+~P16(a5000) % 0.47/0.57 [36]P29(a5000)+~P15(a5000) % 0.47/0.57 [37]P30(a5000)+~P20(a5000) % 0.47/0.57 [38]P31(a5000)+~P19(a5000) % 0.47/0.57 [39]~P16(a5000)+~P28(a5000) % 0.47/0.57 [40]~P20(a5000)+~P30(a5000) % 0.47/0.57 [41]~P15(a5000)+~P29(a5000) % 0.47/0.57 [42]~P19(a5000)+~P31(a5000) % 0.47/0.57 [43]P6(a5000)+P40(a5000)+~P4(a5000) % 0.47/0.57 [44]P10(a5000)+P41(a5000)+~P9(a5000) % 0.47/0.57 [45]P42(a5000)+P8(a5000)+~P2(a5000) % 0.47/0.57 [46]P43(a5000)+P11(a5000)+~P5(a5000) % 0.47/0.57 [47]P12(a5000)+P14(a5000)+~P1(a5000) % 0.47/0.57 [48]P22(a5000)+~P3(a5000)+~P7(a5000) % 0.47/0.57 [49]P13(a5000)+~P15(a5000)+~P24(a5000) % 0.47/0.57 [50]P16(a5000)+~P25(a5000)+~P17(a5000) % 0.47/0.57 [51]P18(a5000)+~P19(a5000)+~P26(a5000) % 0.47/0.57 [52]P20(a5000)+~P27(a5000)+~P21(a5000) % 0.47/0.57 [53]P3(a5000)+P47(a5000)+~P4(a5000)+~P2(a5000) % 0.47/0.57 [54]P3(a5000)+P48(a5000)+~P9(a5000)+~P5(a5000) % 0.47/0.57 [55]P7(a5000)+P49(a5000)+~P4(a5000)+~P5(a5000) % 0.47/0.57 [56]P7(a5000)+P52(a5000)+~P2(a5000)+~P9(a5000) % 0.47/0.57 [57]P4(a5000)+P50(a5000)+~P2(a5000)+~P6(a5000) % 0.47/0.57 [58]P4(a5000)+P51(a5000)+~P5(a5000)+~P10(a5000) % 0.47/0.57 [59]P9(a5000)+P53(a5000)+~P2(a5000)+~P10(a5000) % 0.47/0.57 [60]P9(a5000)+P54(a5000)+~P5(a5000)+~P6(a5000) % 0.47/0.57 [61]P13(a5000)+P16(a5000)+~P12(a5000)+~P23(a5000) % 0.47/0.57 [62]P13(a5000)+P20(a5000)+~P14(a5000)+~P35(a5000) % 0.47/0.57 [63]P16(a5000)+P18(a5000)+~P14(a5000)+~P36(a5000) % 0.47/0.57 [64]P16(a5000)+P15(a5000)+~P13(a5000)+~P33(a5000) % 0.47/0.57 [65]P16(a5000)+P19(a5000)+~P18(a5000)+~P37(a5000) % 0.47/0.57 [66]P18(a5000)+P20(a5000)+~P12(a5000)+~P32(a5000) % 0.47/0.57 [67]P20(a5000)+P15(a5000)+~P18(a5000)+~P38(a5000) % 0.47/0.57 [68]P20(a5000)+P19(a5000)+~P13(a5000)+~P34(a5000) % 0.47/0.57 %EqnAxiom % 0.47/0.57 % 0.47/0.57 %------------------------------------------- % 0.47/0.57 cnf(69,plain, % 0.47/0.57 (~P3(a5000)+~P7(a5000)), % 0.47/0.57 inference(scs_inference,[],[2,48])). % 0.47/0.57 cnf(70,plain, % 0.47/0.57 (~P47(a5000)+~P7(a5000)), % 0.47/0.57 inference(scs_inference,[],[2,48,7])). % 0.47/0.57 cnf(71,plain, % 0.47/0.57 (~P48(a5000)+~P7(a5000)), % 0.47/0.57 inference(scs_inference,[],[2,48,7,8])). % 0.47/0.57 cnf(72,plain, % 0.47/0.57 (~P7(a5000)+~P2(a5000)+P50(a5000)+~P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[2,48,7,8,53,57])). % 0.47/0.57 cnf(73,plain, % 0.47/0.57 (P2(a5000)), % 0.47/0.57 inference(scs_inference,[],[3,13])). % 0.47/0.57 cnf(74,plain, % 0.47/0.57 (P3(a5000)+P47(a5000)+~P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[73,53])). % 0.47/0.57 cnf(75,plain, % 0.47/0.57 (P7(a5000)+P52(a5000)+~P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[73,56])). % 0.47/0.57 cnf(76,plain, % 0.47/0.57 (P4(a5000)+P50(a5000)+~P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[73,57])). % 0.47/0.57 cnf(77,plain, % 0.47/0.57 (P9(a5000)+P53(a5000)+~P10(a5000)), % 0.47/0.57 inference(scs_inference,[],[73,59])). % 0.47/0.57 cnf(78,plain, % 0.47/0.57 (~P7(a5000)+P50(a5000)+~P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[73,72])). % 0.47/0.57 cnf(79,plain, % 0.47/0.57 (P5(a5000)), % 0.47/0.57 inference(scs_inference,[],[4,16])). % 0.47/0.57 cnf(80,plain, % 0.47/0.57 (P3(a5000)+P48(a5000)+~P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[79,54])). % 0.47/0.57 cnf(81,plain, % 0.47/0.57 (P7(a5000)+P49(a5000)+~P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[79,55])). % 0.47/0.57 cnf(83,plain, % 0.47/0.57 (P9(a5000)+P54(a5000)+~P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[79,60])). % 0.47/0.57 cnf(85,plain, % 0.47/0.57 (P46(a5000)+P9(a5000)+P53(a5000)), % 0.47/0.57 inference(scs_inference,[],[6,77])). % 0.47/0.57 cnf(86,plain, % 0.47/0.57 (~P49(a5000)+~P3(a5000)), % 0.47/0.57 inference(scs_inference,[],[9,69])). % 0.47/0.57 cnf(87,plain, % 0.47/0.57 (~P52(a5000)+~P47(a5000)), % 0.47/0.57 inference(scs_inference,[],[10,70])). % 0.47/0.57 cnf(91,plain, % 0.47/0.57 (~P54(a5000)+P7(a5000)+P52(a5000)), % 0.47/0.57 inference(scs_inference,[],[15,75])). % 0.47/0.57 cnf(93,plain, % 0.47/0.57 (~P45(a5000)+P9(a5000)+P54(a5000)), % 0.47/0.57 inference(scs_inference,[],[18,83])). % 0.47/0.57 cnf(95,plain, % 0.47/0.57 (~P46(a5000)+P9(a5000)+P53(a5000)), % 0.47/0.57 inference(scs_inference,[],[20,77])). % 0.47/0.57 cnf(96,plain, % 0.47/0.57 (~P7(a5000)+P3(a5000)+~P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[71,80])). % 0.47/0.57 cnf(97,plain, % 0.47/0.57 (~P3(a5000)+P7(a5000)+~P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[86,81])). % 0.47/0.57 cnf(98,plain, % 0.47/0.57 (~P47(a5000)+~P54(a5000)+P7(a5000)), % 0.47/0.57 inference(scs_inference,[],[87,91])). % 0.47/0.57 cnf(105,plain, % 0.47/0.57 (P9(a5000)+P54(a5000)+P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[93,5])). % 0.47/0.57 cnf(106,plain, % 0.47/0.57 (P9(a5000)+P53(a5000)), % 0.47/0.57 inference(scs_inference,[],[95,85])). % 0.47/0.57 cnf(108,plain, % 0.47/0.57 (P3(a5000)+~P9(a5000)+~P49(a5000)), % 0.47/0.57 inference(scs_inference,[],[96,9])). % 0.47/0.57 cnf(110,plain, % 0.47/0.57 (~P54(a5000)+~P47(a5000)), % 0.47/0.57 inference(scs_inference,[],[98,70])). % 0.47/0.57 cnf(111,plain, % 0.47/0.57 (~P47(a5000)+P9(a5000)+~P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[110,83])). % 0.47/0.57 cnf(118,plain, % 0.47/0.57 (P6(a5000)+P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[105,15])). % 0.47/0.57 cnf(119,plain, % 0.47/0.57 (P9(a5000)+~P7(a5000)+P50(a5000)), % 0.47/0.57 inference(scs_inference,[],[118,78])). % 0.47/0.57 cnf(122,plain, % 0.47/0.57 (~P9(a5000)+~P49(a5000)), % 0.47/0.57 inference(scs_inference,[],[108,86])). % 0.47/0.57 cnf(123,plain, % 0.47/0.57 (~P49(a5000)+~P53(a5000)), % 0.47/0.57 inference(scs_inference,[],[122,14])). % 0.47/0.57 cnf(124,plain, % 0.47/0.57 (~P53(a5000)+P7(a5000)+~P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[123,81])). % 0.47/0.57 cnf(126,plain, % 0.47/0.57 (~P47(a5000)+P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[111,118])). % 0.47/0.57 cnf(127,plain, % 0.47/0.57 (P9(a5000)+P3(a5000)+~P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[126,74])). % 0.47/0.57 cnf(132,plain, % 0.47/0.57 (P50(a5000)+~P7(a5000)+P3(a5000)), % 0.47/0.57 inference(scs_inference,[],[119,96])). % 0.47/0.57 cnf(134,plain, % 0.47/0.57 (P7(a5000)+~P4(a5000)+P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[124,106])). % 0.47/0.57 cnf(141,plain, % 0.47/0.57 (P50(a5000)+~P7(a5000)), % 0.47/0.57 inference(scs_inference,[],[132,69])). % 0.47/0.57 cnf(142,plain, % 0.47/0.57 (P50(a5000)+~P52(a5000)), % 0.47/0.57 inference(scs_inference,[],[141,10])). % 0.47/0.57 cnf(143,plain, % 0.47/0.57 (~P52(a5000)+P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[142,11])). % 0.47/0.57 cnf(144,plain, % 0.47/0.57 (P4(a5000)+~P54(a5000)+P7(a5000)), % 0.47/0.57 inference(scs_inference,[],[143,91])). % 0.47/0.57 cnf(151,plain, % 0.47/0.57 (~P54(a5000)+~P3(a5000)+P7(a5000)), % 0.47/0.57 inference(scs_inference,[],[144,97])). % 0.47/0.57 cnf(153,plain, % 0.47/0.57 (~P54(a5000)+~P3(a5000)), % 0.47/0.57 inference(scs_inference,[],[151,69])). % 0.47/0.57 cnf(154,plain, % 0.47/0.57 (~P3(a5000)+P9(a5000)+~P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[153,83])). % 0.47/0.57 cnf(156,plain, % 0.47/0.57 (~P6(a5000)+P9(a5000)+~P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[154,127])). % 0.47/0.57 cnf(160,plain, % 0.47/0.57 (P6(a5000)), % 0.47/0.57 inference(scs_inference,[],[5,18])). % 0.47/0.57 cnf(161,plain, % 0.47/0.57 (P4(a5000)+P50(a5000)), % 0.47/0.57 inference(scs_inference,[],[160,76])). % 0.47/0.57 cnf(162,plain, % 0.47/0.57 (P9(a5000)+P54(a5000)), % 0.47/0.57 inference(scs_inference,[],[160,83])). % 0.47/0.57 cnf(163,plain, % 0.47/0.57 (~P3(a5000)+P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[160,154])). % 0.47/0.57 cnf(164,plain, % 0.47/0.57 (P9(a5000)+~P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[160,156])). % 0.47/0.57 cnf(165,plain, % 0.47/0.57 (P50(a5000)+P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[161,164])). % 0.47/0.57 cnf(168,plain, % 0.47/0.57 (P9(a5000)+P4(a5000)), % 0.47/0.57 inference(scs_inference,[],[165,11])). % 0.47/0.57 cnf(171,plain, % 0.47/0.57 (P4(a5000)+P7(a5000)+P52(a5000)), % 0.47/0.57 inference(scs_inference,[],[168,75])). % 0.47/0.57 cnf(179,plain, % 0.47/0.57 (P52(a5000)+P7(a5000)+P9(a5000)), % 0.47/0.57 inference(scs_inference,[],[171,134])). % 0.47/0.58 cnf(181,plain, % 0.47/0.58 (P9(a5000)+P7(a5000)), % 0.47/0.58 inference(scs_inference,[],[179,10])). % 0.47/0.58 cnf(182,plain, % 0.47/0.58 (P7(a5000)+P52(a5000)), % 0.47/0.58 inference(scs_inference,[],[181,75])). % 0.47/0.58 cnf(183,plain, % 0.47/0.58 (P52(a5000)+~P3(a5000)), % 0.47/0.58 inference(scs_inference,[],[182,69])). % 0.47/0.58 cnf(184,plain, % 0.47/0.58 (~P3(a5000)+~P47(a5000)), % 0.47/0.58 inference(scs_inference,[],[183,87])). % 0.53/0.58 cnf(185,plain, % 0.53/0.58 (~P47(a5000)), % 0.53/0.58 inference(scs_inference,[],[184,7])). % 0.53/0.58 cnf(186,plain, % 0.53/0.58 (P3(a5000)+~P4(a5000)), % 0.53/0.58 inference(scs_inference,[],[185,74])). % 0.53/0.58 cnf(187,plain, % 0.53/0.58 (~P4(a5000)+~P54(a5000)), % 0.53/0.58 inference(scs_inference,[],[186,153])). % 0.53/0.58 cnf(188,plain, % 0.53/0.58 (~P54(a5000)+~P50(a5000)), % 0.53/0.58 inference(scs_inference,[],[187,11])). % 0.53/0.58 cnf(189,plain, % 0.53/0.58 (~P50(a5000)+P9(a5000)), % 0.53/0.58 inference(scs_inference,[],[188,162])). % 0.53/0.58 cnf(190,plain, % 0.53/0.58 (P9(a5000)+~P7(a5000)), % 0.53/0.58 inference(scs_inference,[],[189,141])). % 0.53/0.58 cnf(191,plain, % 0.53/0.58 (~P7(a5000)+P3(a5000)+P48(a5000)), % 0.53/0.58 inference(scs_inference,[],[190,80])). % 0.53/0.58 cnf(199,plain, % 0.53/0.58 (P3(a5000)+~P9(a5000)), % 0.53/0.58 inference(scs_inference,[],[8,80])). % 0.53/0.58 cnf(200,plain, % 0.53/0.58 (~P9(a5000)+~P7(a5000)), % 0.53/0.58 inference(scs_inference,[],[199,69])). % 0.53/0.58 cnf(201,plain, % 0.53/0.58 (~P7(a5000)+~P53(a5000)), % 0.53/0.58 inference(scs_inference,[],[200,14])). % 0.53/0.58 cnf(202,plain, % 0.53/0.58 (~P53(a5000)+~P52(a5000)), % 0.53/0.58 inference(scs_inference,[],[201,10])). % 0.53/0.58 cnf(203,plain, % 0.53/0.58 (~P52(a5000)+P9(a5000)), % 0.53/0.58 inference(scs_inference,[],[202,106])). % 0.53/0.58 cnf(204,plain, % 0.53/0.58 (~P52(a5000)+P3(a5000)), % 0.53/0.58 inference(scs_inference,[],[203,199])). % 0.53/0.58 cnf(205,plain, % 0.53/0.58 (P3(a5000)+P7(a5000)), % 0.53/0.58 inference(scs_inference,[],[204,182])). % 0.53/0.58 cnf(206,plain, % 0.53/0.58 (P7(a5000)+~P54(a5000)), % 0.53/0.58 inference(scs_inference,[],[205,153])). % 0.53/0.58 cnf(207,plain, % 0.53/0.58 (~P54(a5000)+~P48(a5000)), % 0.53/0.58 inference(scs_inference,[],[206,71])). % 0.53/0.58 cnf(208,plain, % 0.53/0.58 (~P54(a5000)+~P7(a5000)+P3(a5000)), % 0.53/0.58 inference(scs_inference,[],[207,191])). % 0.53/0.58 cnf(209,plain, % 0.53/0.58 (~P54(a5000)+P3(a5000)), % 0.53/0.58 inference(scs_inference,[],[208,205])). % 0.53/0.58 cnf(210,plain, % 0.53/0.58 (P3(a5000)+P9(a5000)), % 0.53/0.58 inference(scs_inference,[],[209,162])). % 0.53/0.58 cnf(211,plain, % 0.53/0.58 (P9(a5000)), % 0.53/0.58 inference(scs_inference,[],[210,163])). % 0.53/0.58 cnf(213,plain, % 0.53/0.58 (~P7(a5000)), % 0.53/0.58 inference(scs_inference,[],[211,200])). % 0.53/0.58 cnf(214,plain, % 0.53/0.58 (~P52(a5000)), % 0.53/0.58 inference(scs_inference,[],[213,10])). % 0.53/0.58 cnf(222,plain, % 0.53/0.58 (P52(a5000)), % 0.53/0.58 inference(scs_inference,[],[213,182])). % 0.53/0.58 cnf(227,plain, % 0.53/0.58 ($false), % 0.53/0.58 inference(scs_inference,[],[214,222]), % 0.53/0.58 ['proof']). % 0.53/0.58 % SZS output end Proof % 0.53/0.58 % Total time :0.070000s %------------------------------------------------------------------------------