%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN099-1.003 : 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 : n017.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.55s 0.62s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN099-1.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n017.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 21:19:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 0.55/0.61 %------------------------------------------- % 0.55/0.61 % File :CSE---1.7 % 0.55/0.61 % Problem :theBenchmark % 0.55/0.61 % Transform :cnf % 0.55/0.61 % Format :tptp:raw % 0.55/0.61 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.61 % 0.55/0.61 % Result :Theorem 0.000000s % 0.55/0.61 % Output :CNFRefutation 0.000000s % 0.55/0.61 %------------------------------------------- % 0.55/0.61 %-------------------------------------------------------------------------- % 0.55/0.61 % File : SYN099-1.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.55/0.61 % Domain : Syntactic % 0.55/0.61 % Problem : Plaisted problem sym(m(t(2,3))) % 0.55/0.61 % Version : Biased. % 0.55/0.61 % English : % 0.55/0.61 % 0.55/0.61 % Refs : [Pla94] Plaisted (1994), The Search Efficiency of Theorem Prov % 0.55/0.61 % Source : [Pla94] % 0.55/0.61 % Names : Sym(M(T2n)) [Pla94] % 0.55/0.61 % 0.55/0.61 % Status : Unsatisfiable % 0.55/0.61 % Rating : 0.00 v2.1.0 % 0.55/0.61 % Syntax : Number of clauses : 50 ( 14 unt; 12 nHn; 49 RR) % 0.55/0.61 % Number of literals : 110 ( 0 equ; 55 neg) % 0.55/0.61 % Maximal clause size : 3 ( 2 avg) % 0.55/0.61 % Maximal term depth : 1 ( 1 avg) % 0.55/0.61 % Number of predicates : 24 ( 24 usr; 0 prp; 1-1 aty) % 0.55/0.61 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.55/0.61 % Number of variables : 38 ( 2 sgn) % 0.55/0.61 % SPC : CNF_UNS_EPR_NEQ_NHN % 0.55/0.61 % 0.55/0.61 % Comments : Biased away from various calculi. % 0.55/0.61 % : tptp2X: -f tptp -s3 SYN099-1.g % 0.55/0.61 % Bugfixes : v1.2.0 - Bugfix in SYN086-1. % 0.55/0.61 % : v1.2.1 - Bugfix in SYN086-1. % 0.55/0.61 %-------------------------------------------------------------------------- % 0.55/0.61 cnf(m_s2_goal_1,negated_conjecture, % 0.55/0.61 ~ p_1_3(X) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type11_1,axiom, % 0.55/0.61 ( p_1_2(X) % 0.55/0.61 | ~ p_2_2(X) % 0.55/0.61 | ~ p_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type11_2,axiom, % 0.55/0.61 ( p_1_2(X) % 0.55/0.61 | ~ q_2_2(X) % 0.55/0.61 | ~ q_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type11_3,axiom, % 0.55/0.61 ( p_1_3(X) % 0.55/0.61 | ~ p_2_3(X) % 0.55/0.61 | ~ p_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type11_4,axiom, % 0.55/0.61 ( p_1_3(X) % 0.55/0.61 | ~ q_2_3(X) % 0.55/0.61 | ~ q_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type11_5,axiom, % 0.55/0.61 ( p_2_3(X) % 0.55/0.61 | ~ p_3_3(X) % 0.55/0.61 | ~ p_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type11_6,axiom, % 0.55/0.61 ( p_2_3(X) % 0.55/0.61 | ~ q_3_3(X) % 0.55/0.61 | ~ q_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type12_1,axiom, % 0.55/0.61 ( q_1_2(X) % 0.55/0.61 | ~ p_2_2(X) % 0.55/0.61 | ~ q_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type12_2,axiom, % 0.55/0.61 ( q_1_2(X) % 0.55/0.61 | ~ q_2_2(X) % 0.55/0.61 | ~ p_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type12_3,axiom, % 0.55/0.61 ( q_1_3(X) % 0.55/0.61 | ~ p_2_3(X) % 0.55/0.61 | ~ q_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type12_4,axiom, % 0.55/0.61 ( q_1_3(X) % 0.55/0.61 | ~ q_2_3(X) % 0.55/0.61 | ~ p_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type12_5,axiom, % 0.55/0.61 ( q_2_3(X) % 0.55/0.61 | ~ p_3_3(X) % 0.55/0.61 | ~ q_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type12_6,axiom, % 0.55/0.61 ( q_2_3(X) % 0.55/0.61 | ~ q_3_3(X) % 0.55/0.61 | ~ p_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type21_1,axiom, % 0.55/0.61 ( p_1_1(X) % 0.55/0.61 | ~ p_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type21_2,axiom, % 0.55/0.61 ( q_1_1(X) % 0.55/0.61 | ~ q_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type22_1,axiom, % 0.55/0.61 ( p_2_2(X) % 0.55/0.61 | ~ p_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type22_2,axiom, % 0.55/0.61 ( p_3_3(X) % 0.55/0.61 | ~ p_2_3(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type22_3,axiom, % 0.55/0.61 ( q_2_2(X) % 0.55/0.61 | ~ q_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_s2_type22_4,axiom, % 0.55/0.61 ( q_3_3(X) % 0.55/0.61 | ~ q_2_3(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(m_t2_1,axiom, % 0.55/0.61 p_1_1(a) ). % 0.55/0.61 % 0.55/0.61 cnf(m_t2_2,axiom, % 0.55/0.61 q_1_1(a) ). % 0.55/0.61 % 0.55/0.61 cnf(m_t2_3,axiom, % 0.55/0.61 p_2_2(a) ). % 0.55/0.61 % 0.55/0.61 cnf(m_t2_4,axiom, % 0.55/0.61 q_2_2(a) ). % 0.55/0.61 % 0.55/0.61 cnf(m_t2_5,axiom, % 0.55/0.61 p_3_3(a) ). % 0.55/0.61 % 0.55/0.61 cnf(m_t2_6,axiom, % 0.55/0.61 q_3_3(a) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_goal_1,axiom, % 0.55/0.61 sym_p_1_3(X) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type11_1,axiom, % 0.55/0.61 ( ~ sym_p_1_2(X) % 0.55/0.61 | sym_p_2_2(X) % 0.55/0.61 | sym_p_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type11_2,axiom, % 0.55/0.61 ( ~ sym_p_1_2(X) % 0.55/0.61 | sym_q_2_2(X) % 0.55/0.61 | sym_q_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type11_3,axiom, % 0.55/0.61 ( ~ sym_p_1_3(X) % 0.55/0.61 | sym_p_2_3(X) % 0.55/0.61 | sym_p_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type11_4,axiom, % 0.55/0.61 ( ~ sym_p_1_3(X) % 0.55/0.61 | sym_q_2_3(X) % 0.55/0.61 | sym_q_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type11_5,axiom, % 0.55/0.61 ( ~ sym_p_2_3(X) % 0.55/0.61 | sym_p_3_3(X) % 0.55/0.61 | sym_p_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type11_6,axiom, % 0.55/0.61 ( ~ sym_p_2_3(X) % 0.55/0.61 | sym_q_3_3(X) % 0.55/0.61 | sym_q_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type12_1,axiom, % 0.55/0.61 ( ~ sym_q_1_2(X) % 0.55/0.61 | sym_p_2_2(X) % 0.55/0.61 | sym_q_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type12_2,axiom, % 0.55/0.61 ( ~ sym_q_1_2(X) % 0.55/0.61 | sym_q_2_2(X) % 0.55/0.61 | sym_p_1_1(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type12_3,axiom, % 0.55/0.61 ( ~ sym_q_1_3(X) % 0.55/0.61 | sym_p_2_3(X) % 0.55/0.61 | sym_q_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type12_4,axiom, % 0.55/0.61 ( ~ sym_q_1_3(X) % 0.55/0.61 | sym_q_2_3(X) % 0.55/0.61 | sym_p_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type12_5,axiom, % 0.55/0.61 ( ~ sym_q_2_3(X) % 0.55/0.61 | sym_p_3_3(X) % 0.55/0.61 | sym_q_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type12_6,axiom, % 0.55/0.61 ( ~ sym_q_2_3(X) % 0.55/0.61 | sym_q_3_3(X) % 0.55/0.61 | sym_p_2_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type21_1,axiom, % 0.55/0.61 ( ~ sym_p_1_1(X) % 0.55/0.61 | sym_p_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type21_2,axiom, % 0.55/0.61 ( ~ sym_q_1_1(X) % 0.55/0.61 | sym_q_1_2(X) ) ). % 0.55/0.61 % 0.55/0.61 cnf(sym_m_s2_type22_1,axiom, % 0.55/0.61 ( ~ sym_p_2_2(X) % 0.55/0.62 | sym_p_1_2(X) ) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_s2_type22_2,axiom, % 0.55/0.62 ( ~ sym_p_3_3(X) % 0.55/0.62 | sym_p_2_3(X) ) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_s2_type22_3,axiom, % 0.55/0.62 ( ~ sym_q_2_2(X) % 0.55/0.62 | sym_q_1_2(X) ) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_s2_type22_4,axiom, % 0.55/0.62 ( ~ sym_q_3_3(X) % 0.55/0.62 | sym_q_2_3(X) ) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_t2_1,axiom, % 0.55/0.62 ~ sym_p_1_1(a) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_t2_2,axiom, % 0.55/0.62 ~ sym_q_1_1(a) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_t2_3,axiom, % 0.55/0.62 ~ sym_p_2_2(a) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_t2_4,axiom, % 0.55/0.62 ~ sym_q_2_2(a) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_t2_5,axiom, % 0.55/0.62 ~ sym_p_3_3(a) ). % 0.55/0.62 % 0.55/0.62 cnf(sym_m_t2_6,axiom, % 0.55/0.62 ~ sym_q_3_3(a) ). % 0.55/0.62 % 0.55/0.62 %-------------------------------------------------------------------------- % 0.55/0.62 %------------------------------------------- % 0.55/0.62 % Proof found % 0.55/0.62 % SZS status Theorem for theBenchmark % 0.55/0.62 % SZS output start Proof % 0.55/0.62 %ClaNum:49(EqnAxiom:0) % 0.55/0.62 %VarNum:95(SingletonVarNum:37) % 0.55/0.62 %MaxLitNum:3 % 0.55/0.62 %MaxfuncDepth:0 % 0.55/0.62 %SharedTerms:13 % 0.55/0.62 %goalClause: 13 % 0.55/0.62 %singleGoalClaCount:1 % 0.55/0.62 [1]P1(a1) % 0.55/0.62 [2]P2(a1) % 0.55/0.62 [3]P5(a1) % 0.55/0.62 [4]P6(a1) % 0.55/0.62 [5]P7(a1) % 0.55/0.62 [6]P11(a1) % 0.55/0.62 [7]~P13(a1) % 0.55/0.62 [8]~P14(a1) % 0.55/0.62 [9]~P16(a1) % 0.55/0.62 [10]~P17(a1) % 0.55/0.62 [11]~P18(a1) % 0.55/0.62 [12]~P22(a1) % 0.55/0.62 [13]~P3(x131) % 0.55/0.62 [14]P19(x141)+P15(x141) % 0.55/0.62 [15]P20(x151)+P23(x151) % 0.55/0.62 [16]~P4(x161)+P1(x161) % 0.55/0.62 [17]~P4(x171)+P2(x171) % 0.55/0.62 [18]~P9(x181)+P5(x181) % 0.55/0.62 [19]~P9(x191)+P6(x191) % 0.55/0.62 [20]~P8(x201)+P7(x201) % 0.55/0.62 [21]~P12(x211)+P11(x211) % 0.55/0.62 [22]~P13(x221)+P15(x221) % 0.55/0.62 [23]~P14(x231)+P15(x231) % 0.55/0.62 [24]~P18(x241)+P19(x241) % 0.55/0.62 [25]~P22(x251)+P23(x251) % 0.55/0.62 [26]~P16(x261)+P20(x261) % 0.55/0.62 [27]~P17(x271)+P20(x271) % 0.55/0.62 [28]P23(x281)+~P21(x281)+P15(x281) % 0.55/0.62 [29]P14(x291)+~P15(x291)+P13(x291) % 0.55/0.62 [30]P17(x301)+~P20(x301)+P13(x301) % 0.55/0.62 [31]P18(x311)+~P19(x311)+P13(x311) % 0.55/0.62 [32]P22(x321)+~P23(x321)+P13(x321) % 0.55/0.62 [33]P16(x331)+~P20(x331)+P14(x331) % 0.55/0.62 [34]P17(x341)+~P15(x341)+P16(x341) % 0.55/0.62 [35]P18(x351)+~P23(x351)+P16(x351) % 0.55/0.62 [36]P22(x361)+~P19(x361)+P16(x361) % 0.55/0.62 [37]P20(x371)+~P21(x371)+P19(x371) % 0.55/0.62 [38]~P4(x381)+~P8(x381)+P3(x381) % 0.55/0.62 [39]~P12(x391)+~P9(x391)+P3(x391) % 0.55/0.62 [40]~P1(x401)+~P2(x401)+P4(x401) % 0.55/0.62 [41]~P5(x411)+~P6(x411)+P4(x411) % 0.55/0.62 [42]~P1(x421)+~P7(x421)+P8(x421) % 0.55/0.62 [43]~P5(x431)+~P11(x431)+P8(x431) % 0.55/0.62 [44]~P1(x441)+~P11(x441)+P12(x441) % 0.55/0.62 [45]~P5(x451)+~P7(x451)+P12(x451) % 0.55/0.62 [46]~P1(x461)+~P6(x461)+P9(x461) % 0.55/0.62 [47]~P2(x471)+~P5(x471)+P9(x471) % 0.55/0.62 [48]~P4(x481)+~P12(x481)+P10(x481) % 0.55/0.62 [49]~P8(x491)+~P9(x491)+P10(x491) % 0.55/0.62 %EqnAxiom % 0.55/0.62 % 0.55/0.62 %------------------------------------------- % 0.55/0.62 cnf(58,plain, % 0.55/0.62 ($false), % 0.55/0.62 inference(scs_inference,[],[13,1,2,4,5,6,40,42,44,46,38]), % 0.55/0.62 ['proof']). % 0.55/0.62 % SZS output end Proof % 0.55/0.62 % Total time :0.000000s %------------------------------------------------------------------------------