%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ030-2 : 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 : n022.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 13:42:08 EDT 2024 % Result : Unsatisfiable 0.58s 0.77s % Output : CNFRefutation 0.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : PUZ030-2 : TPTP v8.2.0. Released v1.0.0. % 0.10/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n022.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Tue Jun 18 10:38:53 EDT 2024 % 0.11/0.33 % CPUTime : % 0.17/0.51 start to proof:theBenchmark % 0.58/0.76 %------------------------------------------- % 0.58/0.76 % File :CSE---1.7 % 0.58/0.76 % Problem :theBenchmark % 0.58/0.76 % Transform :cnf % 0.58/0.76 % Format :tptp:raw % 0.58/0.76 % Command :java -jar mcs_scs.jar %d %s % 0.58/0.76 % 0.58/0.76 % Result :Theorem 0.200000s % 0.58/0.76 % Output :CNFRefutation 0.200000s % 0.58/0.76 %------------------------------------------- % 0.58/0.77 %-------------------------------------------------------------------------- % 0.58/0.77 % File : PUZ030-2 : TPTP v8.2.0. Released v1.0.0. % 0.58/0.77 % Domain : Puzzles % 0.58/0.77 % Problem : Salt and Mustard Problem % 0.58/0.77 % Version : Especial. % 0.58/0.77 % Theorem formulation : Propositional. % 0.58/0.77 % English : % 0.58/0.77 % 0.58/0.77 % Refs : [Car86] Carroll (1986), Lewis Carroll's Symbolic Logic % 0.58/0.77 % Source : [TPTP] % 0.58/0.77 % Names : salt.in [OTTER] % 0.58/0.77 % 0.58/0.77 % Status : Unsatisfiable % 0.58/0.77 % Rating : 0.00 v4.1.0, 0.20 v4.0.1, 0.00 v2.1.0 % 0.58/0.77 % Syntax : Number of clauses : 63 ( 0 unt; 36 nHn; 63 RR) % 0.58/0.77 % Number of literals : 214 ( 0 equ; 115 neg) % 0.58/0.77 % Maximal clause size : 10 ( 3 avg) % 0.58/0.77 % Maximal term depth : 0 ( 0 avg) % 0.58/0.77 % Number of predicates : 10 ( 10 usr; 10 prp; 0-0 aty) % 0.58/0.77 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 0.58/0.77 % Number of variables : 0 ( 0 sgn) % 0.58/0.77 % SPC : CNF_UNS_PRP % 0.58/0.77 % 0.58/0.77 % Comments : % 0.58/0.77 % Bugfixes : v1.1.2 - Renamed from PUZ030-0. % 0.58/0.77 %-------------------------------------------------------------------------- % 0.58/0.77 cnf(c1,hypothesis, % 0.58/0.77 ( ~ salt_mill % 0.58/0.77 | mustard_barry % 0.58/0.77 | mustard_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c2,hypothesis, % 0.58/0.77 ( ~ salt_mill % 0.58/0.77 | mustard_barry % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c3,hypothesis, % 0.58/0.77 ( ~ salt_mill % 0.58/0.77 | salt_barry % 0.58/0.77 | mustard_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c4,hypothesis, % 0.58/0.77 ( ~ salt_mill % 0.58/0.77 | salt_barry % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c5,hypothesis, % 0.58/0.77 ( ~ mustard_lang % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | ~ mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c6,hypothesis, % 0.58/0.77 ( ~ mustard_lang % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | ~ salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c7,hypothesis, % 0.58/0.77 ( ~ mustard_lang % 0.58/0.77 | ~ salt_cole % 0.58/0.77 | ~ mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c8,hypothesis, % 0.58/0.77 ( ~ mustard_lang % 0.58/0.77 | ~ salt_cole % 0.58/0.77 | ~ salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c9,hypothesis, % 0.58/0.77 ( ~ mustard_dix % 0.58/0.77 | ~ mustard_lang % 0.58/0.77 | ~ mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c10,hypothesis, % 0.58/0.77 ( ~ mustard_dix % 0.58/0.77 | ~ mustard_lang % 0.58/0.77 | ~ salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c11,hypothesis, % 0.58/0.77 ( ~ mustard_dix % 0.58/0.77 | ~ salt_lang % 0.58/0.77 | ~ mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c12,hypothesis, % 0.58/0.77 ( ~ mustard_dix % 0.58/0.77 | ~ salt_lang % 0.58/0.77 | ~ salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c13,hypothesis, % 0.58/0.77 ( ~ salt_dix % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | mustard_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c14,hypothesis, % 0.58/0.77 ( ~ salt_dix % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | salt_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c15,hypothesis, % 0.58/0.77 ( ~ salt_dix % 0.58/0.77 | ~ salt_barry % 0.58/0.77 | mustard_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c16,hypothesis, % 0.58/0.77 ( ~ salt_dix % 0.58/0.77 | ~ salt_barry % 0.58/0.77 | salt_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c17,hypothesis, % 0.58/0.77 ( ~ mustard_cole % 0.58/0.77 | mustard_dix % 0.58/0.77 | mustard_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c18,hypothesis, % 0.58/0.77 ( ~ mustard_cole % 0.58/0.77 | mustard_dix % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c19,hypothesis, % 0.58/0.77 ( ~ mustard_cole % 0.58/0.77 | salt_dix % 0.58/0.77 | mustard_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c20,hypothesis, % 0.58/0.77 ( ~ mustard_cole % 0.58/0.77 | salt_dix % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c21,hypothesis, % 0.58/0.77 ( ~ mustard_barry % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c22,hypothesis, % 0.58/0.77 ( ~ mustard_barry % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c23,hypothesis, % 0.58/0.77 ( ~ mustard_barry % 0.58/0.77 | ~ salt_dix % 0.58/0.77 | mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c24,hypothesis, % 0.58/0.77 ( ~ mustard_barry % 0.58/0.77 | ~ salt_dix % 0.58/0.77 | salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c25,hypothesis, % 0.58/0.77 ( salt_dix % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c26,hypothesis, % 0.58/0.77 ( ~ salt_dix % 0.58/0.77 | mustard_dix % 0.58/0.77 | mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c27,hypothesis, % 0.58/0.77 ( salt_cole % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c28,hypothesis, % 0.58/0.77 ( ~ salt_cole % 0.58/0.77 | mustard_cole % 0.58/0.77 | mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c29,hypothesis, % 0.58/0.77 ( ~ salt_lang % 0.58/0.77 | ~ mustard_lang % 0.58/0.77 | salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c30,hypothesis, % 0.58/0.77 ( ~ salt_barry % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c31,hypothesis, % 0.58/0.77 ( salt_dix % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c32,hypothesis, % 0.58/0.77 ( ~ salt_dix % 0.58/0.77 | mustard_dix % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c33,hypothesis, % 0.58/0.77 ( salt_barry % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c34,hypothesis, % 0.58/0.77 ( ~ salt_barry % 0.58/0.77 | mustard_barry % 0.58/0.77 | salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c35,hypothesis, % 0.58/0.77 ( ~ salt_cole % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | salt_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c36,hypothesis, % 0.58/0.77 ( ~ salt_lang % 0.58/0.77 | ~ mustard_lang % 0.58/0.77 | mustard_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c37,hypothesis, % 0.58/0.77 ( ~ salt_dix % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | mustard_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c38,hypothesis, % 0.58/0.77 ( salt_barry % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | salt_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c39,hypothesis, % 0.58/0.77 ( ~ salt_barry % 0.58/0.77 | mustard_barry % 0.58/0.77 | salt_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c40,hypothesis, % 0.58/0.77 ( ~ salt_mill % 0.58/0.77 | ~ mustard_mill % 0.58/0.77 | mustard_barry ) ). % 0.58/0.77 % 0.58/0.77 cnf(c41,hypothesis, % 0.58/0.77 ( salt_lang % 0.58/0.77 | ~ mustard_lang % 0.58/0.77 | salt_barry ) ). % 0.58/0.77 % 0.58/0.77 cnf(c42,hypothesis, % 0.58/0.77 ( ~ salt_lang % 0.58/0.77 | mustard_lang % 0.58/0.77 | salt_barry ) ). % 0.58/0.77 % 0.58/0.77 cnf(c43,hypothesis, % 0.58/0.77 ( salt_cole % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | salt_barry ) ). % 0.58/0.77 % 0.58/0.77 cnf(c44,hypothesis, % 0.58/0.77 ( ~ salt_cole % 0.58/0.77 | mustard_cole % 0.58/0.77 | salt_barry ) ). % 0.58/0.77 % 0.58/0.77 cnf(c45,hypothesis, % 0.58/0.77 ( ~ salt_cole % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | ~ salt_barry % 0.58/0.77 | ~ mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c46,hypothesis, % 0.58/0.77 ( ~ salt_cole % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | ~ salt_barry % 0.58/0.77 | ~ salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c47,hypothesis, % 0.58/0.77 ( ~ salt_cole % 0.58/0.77 | salt_barry % 0.58/0.77 | mustard_barry % 0.58/0.77 | ~ mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c48,hypothesis, % 0.58/0.77 ( ~ salt_cole % 0.58/0.77 | salt_barry % 0.58/0.77 | mustard_barry % 0.58/0.77 | ~ salt_mill ) ). % 0.58/0.77 % 0.58/0.77 cnf(c49,hypothesis, % 0.58/0.77 ( ~ mustard_mill % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | ~ salt_cole % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | ~ salt_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c50,hypothesis, % 0.58/0.77 ( ~ mustard_mill % 0.58/0.77 | salt_cole % 0.58/0.77 | mustard_cole % 0.58/0.77 | salt_dix % 0.58/0.77 | mustard_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c51,hypothesis, % 0.58/0.77 ( ~ salt_lang % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | ~ salt_barry % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | ~ salt_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c52,hypothesis, % 0.58/0.77 ( ~ salt_lang % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | ~ salt_barry % 0.58/0.77 | salt_dix % 0.58/0.77 | mustard_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c53,hypothesis, % 0.58/0.77 ( ~ salt_lang % 0.58/0.77 | salt_barry % 0.58/0.77 | mustard_barry % 0.58/0.77 | ~ mustard_dix % 0.58/0.77 | ~ salt_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c54,hypothesis, % 0.58/0.77 ( ~ salt_barry % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | ~ salt_cole % 0.58/0.77 | ~ mustard_lang % 0.58/0.77 | ~ salt_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c55,hypothesis, % 0.58/0.77 ( ~ salt_barry % 0.58/0.77 | ~ mustard_cole % 0.58/0.77 | ~ salt_cole % 0.58/0.77 | salt_lang % 0.58/0.77 | mustard_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c56,hypothesis, % 0.58/0.77 ( salt_mill % 0.58/0.77 | mustard_mill % 0.58/0.77 | mustard_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c57,hypothesis, % 0.58/0.77 ( salt_cole % 0.58/0.77 | mustard_cole % 0.58/0.77 | mustard_lang ) ). % 0.58/0.77 % 0.58/0.77 cnf(c58,hypothesis, % 0.58/0.77 ( salt_mill % 0.58/0.77 | mustard_mill % 0.58/0.77 | mustard_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c59,hypothesis, % 0.58/0.77 ( salt_lang % 0.58/0.77 | mustard_lang % 0.58/0.77 | mustard_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c60,hypothesis, % 0.58/0.77 ( salt_barry % 0.58/0.77 | mustard_barry % 0.58/0.77 | salt_dix ) ). % 0.58/0.77 % 0.58/0.77 cnf(c61,hypothesis, % 0.58/0.77 ( salt_mill % 0.58/0.77 | mustard_mill % 0.58/0.77 | salt_cole ) ). % 0.58/0.77 % 0.58/0.77 cnf(c62,hypothesis, % 0.58/0.77 ( salt_dix % 0.58/0.77 | mustard_dix % 0.58/0.77 | mustard_barry ) ). % 0.58/0.77 % 0.58/0.77 cnf(prove_who_takes_what,negated_conjecture, % 0.58/0.77 ( salt_lang % 0.58/0.77 | ~ mustard_barry % 0.58/0.77 | ~ salt_barry % 0.58/0.77 | ~ salt_mill % 0.58/0.77 | ~ mustard_lang % 0.58/0.77 | salt_cole % 0.58/0.77 | mustard_cole % 0.58/0.77 | salt_dix % 0.58/0.77 | mustard_dix % 0.58/0.77 | mustard_mill ) ). % 0.58/0.77 % 0.58/0.77 %-------------------------------------------------------------------------- % 0.58/0.77 %------------------------------------------- % 0.58/0.77 % Proof found % 0.58/0.77 % SZS status Theorem for theBenchmark % 0.58/0.77 % SZS output start Proof % 0.58/0.77 %ClaNum:63(EqnAxiom:0) % 0.58/0.77 %VarNum:0(SingletonVarNum:0) % 0.58/0.77 %MaxLitNum:10 % 0.58/0.77 %MaxfuncDepth:0 % 0.58/0.77 %SharedTerms:21 % 0.58/0.77 %goalClause: 63 % 0.58/0.77 [1]P1(a5000)+P2(a5000)+P6(a5000) % 0.58/0.77 [2]P1(a5000)+P6(a5000)+P7(a5000) % 0.58/0.77 [3]P1(a5000)+P6(a5000)+P3(a5000) % 0.58/0.77 [4]P4(a5000)+P8(a5000)+P9(a5000) % 0.58/0.77 [5]P4(a5000)+P3(a5000)+P9(a5000) % 0.58/0.77 [6]P2(a5000)+P10(a5000)+P3(a5000) % 0.58/0.77 [7]P2(a5000)+P5(a5000)+P7(a5000) % 0.58/0.77 [8]P4(a5000)+P2(a5000)+~P1(a5000) % 0.58/0.77 [9]P4(a5000)+P10(a5000)+~P1(a5000) % 0.58/0.77 [10]P4(a5000)+P10(a5000)+~P8(a5000) % 0.58/0.77 [11]P4(a5000)+P7(a5000)+~P8(a5000) % 0.58/0.77 [12]P2(a5000)+P8(a5000)+~P1(a5000) % 0.58/0.77 [13]P2(a5000)+P8(a5000)+~P10(a5000) % 0.58/0.77 [14]P2(a5000)+P3(a5000)+~P5(a5000) % 0.58/0.77 [15]P2(a5000)+P9(a5000)+~P5(a5000) % 0.58/0.77 [16]P10(a5000)+P8(a5000)+~P1(a5000) % 0.58/0.77 [17]P10(a5000)+P8(a5000)+~P4(a5000) % 0.58/0.77 [18]P10(a5000)+P8(a5000)+~P2(a5000) % 0.58/0.77 [19]P10(a5000)+P3(a5000)+~P5(a5000) % 0.58/0.77 [20]P10(a5000)+P3(a5000)+~P9(a5000) % 0.58/0.77 [21]P10(a5000)+P9(a5000)+~P5(a5000) % 0.58/0.77 [22]P10(a5000)+P9(a5000)+~P3(a5000) % 0.58/0.77 [23]P8(a5000)+P5(a5000)+~P7(a5000) % 0.58/0.77 [24]P8(a5000)+P7(a5000)+~P4(a5000) % 0.58/0.77 [25]P8(a5000)+P7(a5000)+~P5(a5000) % 0.58/0.77 [26]P5(a5000)+P6(a5000)+~P7(a5000) % 0.58/0.77 [27]P6(a5000)+P7(a5000)+~P5(a5000) % 0.58/0.77 [28]P6(a5000)+P3(a5000)+~P9(a5000) % 0.58/0.77 [29]P6(a5000)+P9(a5000)+~P3(a5000) % 0.58/0.77 [30]P1(a5000)+~P4(a5000)+~P8(a5000) % 0.58/0.77 [31]P1(a5000)+~P4(a5000)+~P3(a5000) % 0.58/0.77 [32]P1(a5000)+~P4(a5000)+~P9(a5000) % 0.58/0.77 [33]P1(a5000)+~P2(a5000)+~P10(a5000) % 0.58/0.77 [34]P4(a5000)+~P1(a5000)+~P6(a5000) % 0.58/0.77 [35]P5(a5000)+~P4(a5000)+~P9(a5000) % 0.58/0.77 [36]P5(a5000)+~P2(a5000)+~P10(a5000) % 0.58/0.77 [37]P5(a5000)+~P8(a5000)+~P9(a5000) % 0.58/0.77 [38]P5(a5000)+~P3(a5000)+~P9(a5000) % 0.58/0.77 [39]P6(a5000)+~P4(a5000)+~P3(a5000) % 0.58/0.77 [40]P6(a5000)+~P4(a5000)+~P9(a5000) % 0.58/0.77 [41]P7(a5000)+~P4(a5000)+~P9(a5000) % 0.58/0.77 [42]P7(a5000)+~P8(a5000)+~P9(a5000) % 0.58/0.77 [43]P9(a5000)+~P5(a5000)+~P7(a5000) % 0.58/0.77 [44]~P1(a5000)+~P2(a5000)+~P5(a5000) % 0.58/0.77 [45]~P1(a5000)+~P2(a5000)+~P7(a5000) % 0.58/0.77 [46]~P1(a5000)+~P2(a5000)+~P3(a5000) % 0.58/0.77 [47]~P1(a5000)+~P10(a5000)+~P3(a5000) % 0.58/0.77 [48]~P2(a5000)+~P5(a5000)+~P6(a5000) % 0.58/0.77 [49]~P2(a5000)+~P6(a5000)+~P7(a5000) % 0.58/0.77 [50]~P2(a5000)+~P6(a5000)+~P3(a5000) % 0.58/0.77 [51]~P10(a5000)+~P6(a5000)+~P3(a5000) % 0.58/0.77 [52]P4(a5000)+P8(a5000)+~P1(a5000)+~P7(a5000) % 0.58/0.77 [53]P4(a5000)+P8(a5000)+~P6(a5000)+~P7(a5000) % 0.58/0.77 [55]~P1(a5000)+~P4(a5000)+~P8(a5000)+~P7(a5000) % 0.58/0.77 [56]~P4(a5000)+~P8(a5000)+~P6(a5000)+~P7(a5000) % 0.58/0.77 [54]P5(a5000)+P7(a5000)+P3(a5000)+P9(a5000)+~P6(a5000) % 0.58/0.77 [57]P4(a5000)+P8(a5000)+~P10(a5000)+~P3(a5000)+~P9(a5000) % 0.58/0.77 [58]P2(a5000)+P10(a5000)+~P8(a5000)+~P5(a5000)+~P7(a5000) % 0.58/0.77 [59]P3(a5000)+P9(a5000)+~P4(a5000)+~P10(a5000)+~P8(a5000) % 0.58/0.77 [60]~P4(a5000)+~P10(a5000)+~P8(a5000)+~P3(a5000)+~P9(a5000) % 0.58/0.77 [61]~P2(a5000)+~P10(a5000)+~P8(a5000)+~P5(a5000)+~P7(a5000) % 0.58/0.77 [62]~P5(a5000)+~P6(a5000)+~P7(a5000)+~P3(a5000)+~P9(a5000) % 0.58/0.77 [63]P10(a5000)+P5(a5000)+P6(a5000)+P7(a5000)+P3(a5000)+P9(a5000)+~P1(a5000)+~P4(a5000)+~P2(a5000)+~P8(a5000) % 0.58/0.77 %EqnAxiom % 0.58/0.77 % 0.58/0.77 %------------------------------------------- % 0.58/0.77 cnf(64,plain, % 0.58/0.77 (P6(a5000)+P2(a5000)+P8(a5000)), % 0.58/0.77 inference(scs_inference,[],[1,12])). % 0.58/0.77 cnf(66,plain, % 0.58/0.77 (P4(a5000)+P10(a5000)+P9(a5000)), % 0.58/0.77 inference(scs_inference,[],[5,22])). % 0.58/0.77 cnf(67,plain, % 0.58/0.77 (P3(a5000)+P10(a5000)+P8(a5000)), % 0.58/0.77 inference(scs_inference,[],[6,18])). % 0.58/0.77 cnf(68,plain, % 0.58/0.77 (P7(a5000)+P5(a5000)+~P10(a5000)), % 0.58/0.77 inference(scs_inference,[],[7,36])). % 0.58/0.77 cnf(69,plain, % 0.58/0.77 (P4(a5000)+P2(a5000)+P6(a5000)), % 0.58/0.77 inference(scs_inference,[],[8,1])). % 0.58/0.77 cnf(70,plain, % 0.58/0.77 (P4(a5000)+~P1(a5000)+~P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[9,47])). % 0.58/0.77 cnf(71,plain, % 0.58/0.77 (P10(a5000)+P1(a5000)+~P8(a5000)), % 0.58/0.77 inference(scs_inference,[],[10,30])). % 0.58/0.77 cnf(74,plain, % 0.58/0.77 (P3(a5000)+~P1(a5000)+~P5(a5000)), % 0.58/0.77 inference(scs_inference,[],[14,44])). % 0.58/0.77 cnf(75,plain, % 0.58/0.77 (P9(a5000)+~P5(a5000)+~P6(a5000)), % 0.58/0.77 inference(scs_inference,[],[15,48])). % 0.58/0.77 cnf(76,plain, % 0.58/0.77 (P8(a5000)+~P1(a5000)+~P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[16,47])). % 0.58/0.77 cnf(78,plain, % 0.58/0.77 (~P7(a5000)+P5(a5000)+~P9(a5000)), % 0.58/0.77 inference(scs_inference,[],[23,37])). % 0.58/0.77 cnf(80,plain, % 0.58/0.77 (~P5(a5000)+P7(a5000)+~P9(a5000)), % 0.58/0.77 inference(scs_inference,[],[25,42])). % 0.58/0.77 cnf(82,plain, % 0.58/0.77 (P6(a5000)+P4(a5000)+P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[28,5])). % 0.58/0.77 cnf(83,plain, % 0.58/0.77 (P9(a5000)+~P2(a5000)+~P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[29,50])). % 0.58/0.77 cnf(84,plain, % 0.58/0.77 (~P4(a5000)+~P2(a5000)+~P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[31,46])). % 0.58/0.77 cnf(85,plain, % 0.58/0.77 (~P10(a5000)+~P2(a5000)+~P5(a5000)), % 0.58/0.77 inference(scs_inference,[],[33,44])). % 0.58/0.77 cnf(89,plain, % 0.58/0.77 (~P7(a5000)+~P2(a5000)+~P10(a5000)), % 0.58/0.77 inference(scs_inference,[],[45,33])). % 0.58/0.77 cnf(90,plain, % 0.58/0.77 (~P10(a5000)+~P9(a5000)+P5(a5000)), % 0.58/0.77 inference(scs_inference,[],[68,78])). % 0.58/0.77 cnf(93,plain, % 0.58/0.77 (~P8(a5000)+P1(a5000)+~P2(a5000)), % 0.58/0.77 inference(scs_inference,[],[71,33])). % 0.58/0.77 cnf(95,plain, % 0.58/0.77 (~P5(a5000)+P4(a5000)+~P1(a5000)), % 0.58/0.77 inference(scs_inference,[],[74,70])). % 0.58/0.77 cnf(96,plain, % 0.58/0.77 (~P6(a5000)+~P5(a5000)+P7(a5000)), % 0.58/0.77 inference(scs_inference,[],[75,80])). % 0.58/0.77 cnf(97,plain, % 0.58/0.77 (P8(a5000)+~P4(a5000)+~P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[76,31])). % 0.58/0.77 cnf(98,plain, % 0.58/0.77 (P3(a5000)+P4(a5000)+~P1(a5000)), % 0.58/0.77 inference(scs_inference,[],[82,34])). % 0.58/0.77 cnf(99,plain, % 0.58/0.77 (~P2(a5000)+P5(a5000)+~P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[83,38])). % 0.58/0.77 cnf(100,plain, % 0.58/0.77 (~P5(a5000)+~P2(a5000)+P8(a5000)), % 0.58/0.77 inference(scs_inference,[],[85,18])). % 0.58/0.77 cnf(103,plain, % 0.58/0.77 (~P7(a5000)+P8(a5000)+~P10(a5000)), % 0.58/0.77 inference(scs_inference,[],[89,13])). % 0.58/0.77 cnf(104,plain, % 0.58/0.77 (P5(a5000)+P3(a5000)+~P9(a5000)), % 0.58/0.77 inference(scs_inference,[],[90,20])). % 0.58/0.77 cnf(106,plain, % 0.58/0.77 (P1(a5000)+~P2(a5000)+P10(a5000)), % 0.58/0.77 inference(scs_inference,[],[93,18])). % 0.58/0.77 cnf(107,plain, % 0.58/0.77 (~P5(a5000)+P1(a5000)+P7(a5000)), % 0.58/0.77 inference(scs_inference,[],[96,2])). % 0.58/0.77 cnf(108,plain, % 0.58/0.77 (P4(a5000)+~P1(a5000)+~P2(a5000)), % 0.58/0.77 inference(scs_inference,[],[98,46])). % 0.58/0.77 cnf(109,plain, % 0.58/0.77 (~P3(a5000)+P5(a5000)+P7(a5000)), % 0.58/0.77 inference(scs_inference,[],[99,7])). % 0.58/0.77 cnf(113,plain, % 0.58/0.77 (~P10(a5000)+P8(a5000)+~P4(a5000)), % 0.58/0.77 inference(scs_inference,[],[103,24])). % 0.58/0.77 cnf(115,plain, % 0.58/0.77 (~P2(a5000)+P4(a5000)+P10(a5000)), % 0.58/0.77 inference(scs_inference,[],[106,9])). % 0.58/0.77 cnf(117,plain, % 0.58/0.77 (P4(a5000)+~P10(a5000)+~P2(a5000)), % 0.58/0.77 inference(scs_inference,[],[108,33])). % 0.58/0.77 cnf(118,plain, % 0.58/0.77 (P7(a5000)+P5(a5000)+~P9(a5000)), % 0.58/0.77 inference(scs_inference,[],[109,104])). % 0.58/0.77 cnf(122,plain, % 0.58/0.77 (~P4(a5000)+P8(a5000)+~P1(a5000)), % 0.58/0.77 inference(scs_inference,[],[113,16])). % 0.58/0.77 cnf(124,plain, % 0.58/0.77 (P10(a5000)+P4(a5000)+P6(a5000)), % 0.58/0.77 inference(scs_inference,[],[115,69])). % 0.58/0.77 cnf(126,plain, % 0.58/0.77 (~P10(a5000)+~P2(a5000)+~P3(a5000)), % 0.58/0.77 inference(scs_inference,[],[117,84])). % 0.58/0.77 cnf(127,plain, % 0.58/0.77 (~P9(a5000)+P5(a5000)), % 0.58/0.77 inference(scs_inference,[],[118,78])). % 0.58/0.77 cnf(128,plain, % 0.58/0.77 (P5(a5000)+P4(a5000)+P8(a5000)), % 0.58/0.77 inference(scs_inference,[],[127,4])). % 0.58/0.78 cnf(131,plain, % 0.58/0.78 (P8(a5000)+~P6(a5000)+~P1(a5000)), % 0.58/0.78 inference(scs_inference,[],[122,34])). % 0.58/0.78 cnf(132,plain, % 0.58/0.78 (P6(a5000)+P4(a5000)+~P2(a5000)), % 0.58/0.78 inference(scs_inference,[],[124,117])). % 0.58/0.78 cnf(134,plain, % 0.58/0.78 (~P3(a5000)+~P2(a5000)+P8(a5000)), % 0.58/0.78 inference(scs_inference,[],[126,18])). % 0.58/0.78 cnf(135,plain, % 0.58/0.78 (P4(a5000)+P8(a5000)+P7(a5000)), % 0.58/0.78 inference(scs_inference,[],[128,25])). % 0.58/0.78 cnf(136,plain, % 0.58/0.78 (P4(a5000)+~P2(a5000)+~P5(a5000)), % 0.58/0.78 inference(scs_inference,[],[132,48])). % 0.58/0.78 cnf(137,plain, % 0.58/0.78 (~P3(a5000)+P6(a5000)+P8(a5000)), % 0.58/0.78 inference(scs_inference,[],[134,64])). % 0.58/0.78 cnf(138,plain, % 0.58/0.78 (P8(a5000)+P7(a5000)+~P9(a5000)), % 0.58/0.78 inference(scs_inference,[],[135,41])). % 0.58/0.78 cnf(139,plain, % 0.70/0.78 (~P5(a5000)+~P2(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[136,84])). % 0.70/0.78 cnf(140,plain, % 0.70/0.78 (P8(a5000)+P6(a5000)+~P9(a5000)), % 0.70/0.78 inference(scs_inference,[],[137,28])). % 0.70/0.78 cnf(141,plain, % 0.70/0.78 (~P9(a5000)+P4(a5000)+P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[138,11])). % 0.70/0.78 cnf(142,plain, % 0.70/0.78 (~P2(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[139,99])). % 0.70/0.78 cnf(144,plain, % 0.70/0.78 (P6(a5000)+P7(a5000)+~P9(a5000)), % 0.70/0.78 inference(scs_inference,[],[140,42])). % 0.70/0.78 cnf(145,plain, % 0.70/0.78 (P7(a5000)+P4(a5000)+P10(a5000)), % 0.70/0.78 inference(scs_inference,[],[141,66])). % 0.70/0.78 cnf(147,plain, % 0.70/0.78 (P7(a5000)+P6(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[144,29])). % 0.70/0.78 cnf(148,plain, % 0.70/0.78 (P4(a5000)+P5(a5000)+P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[145,68])). % 0.70/0.78 cnf(150,plain, % 0.70/0.78 (~P3(a5000)+P5(a5000)+P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[147,26])). % 0.70/0.78 cnf(151,plain, % 0.70/0.78 (P5(a5000)+P8(a5000)+P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[148,24])). % 0.70/0.78 cnf(152,plain, % 0.70/0.78 (P5(a5000)+P6(a5000)+P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[150,82])). % 0.70/0.78 cnf(153,plain, % 0.70/0.78 (P8(a5000)+P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[151,25])). % 0.70/0.78 cnf(156,plain, % 0.70/0.78 (P6(a5000)+P4(a5000)+~P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[152,95])). % 0.70/0.78 cnf(157,plain, % 0.70/0.78 (P4(a5000)+P8(a5000)+~P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[156,131])). % 0.70/0.78 cnf(158,plain, % 0.70/0.78 (P8(a5000)+~P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[157,122])). % 0.70/0.78 cnf(160,plain, % 0.70/0.78 (~P9(a5000)+P4(a5000)+~P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[127,95])). % 0.70/0.78 cnf(162,plain, % 0.70/0.78 (~P9(a5000)+~P6(a5000)+P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[127,96])). % 0.70/0.78 cnf(163,plain, % 0.70/0.78 (P7(a5000)+~P9(a5000)), % 0.70/0.78 inference(scs_inference,[],[162,144])). % 0.70/0.78 cnf(172,plain, % 0.70/0.78 (~P9(a5000)+~P2(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[127,100])). % 0.70/0.78 cnf(173,plain, % 0.70/0.78 (~P9(a5000)+P8(a5000)+~P10(a5000)), % 0.70/0.78 inference(scs_inference,[],[172,13])). % 0.70/0.78 cnf(174,plain, % 0.70/0.78 (~P9(a5000)+P4(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[127,136])). % 0.70/0.78 cnf(175,plain, % 0.70/0.78 (~P9(a5000)+P4(a5000)+P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[174,69])). % 0.70/0.78 cnf(176,plain, % 0.70/0.78 (P4(a5000)+P6(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[175,29])). % 0.70/0.78 cnf(177,plain, % 0.70/0.78 (P6(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[176,39])). % 0.70/0.78 cnf(178,plain, % 0.70/0.78 (~P10(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[177,51])). % 0.70/0.78 cnf(188,plain, % 0.70/0.78 (~P2(a5000)+P1(a5000)+P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[142,3])). % 0.70/0.78 cnf(189,plain, % 0.70/0.78 (P1(a5000)+P6(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[188,64])). % 0.70/0.78 cnf(190,plain, % 0.70/0.78 (P8(a5000)+P6(a5000)+P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[189,156])). % 0.70/0.78 cnf(191,plain, % 0.70/0.78 (P4(a5000)+P8(a5000)+~P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[190,53])). % 0.70/0.78 cnf(194,plain, % 0.70/0.78 (~P2(a5000)+P9(a5000)+P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[142,5])). % 0.70/0.78 cnf(195,plain, % 0.70/0.78 (P9(a5000)+P4(a5000)+~P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[194,8])). % 0.70/0.78 cnf(196,plain, % 0.70/0.78 (P4(a5000)+~P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[195,160])). % 0.70/0.78 cnf(210,plain, % 0.70/0.78 (P8(a5000)+P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[153,23])). % 0.70/0.78 cnf(211,plain, % 0.70/0.78 (P5(a5000)+~P4(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[210,30])). % 0.70/0.78 cnf(212,plain, % 0.70/0.78 (P8(a5000)+P9(a5000)+~P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[153,43])). % 0.70/0.78 cnf(213,plain, % 0.70/0.78 (~P5(a5000)+P8(a5000)+P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[212,140])). % 0.70/0.78 cnf(214,plain, % 0.70/0.78 (P8(a5000)+~P7(a5000)+P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[213,26])). % 0.70/0.78 cnf(215,plain, % 0.70/0.78 (P6(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[214,153])). % 0.70/0.78 cnf(216,plain, % 0.70/0.78 (P8(a5000)+~P2(a5000)+~P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[215,49])). % 0.70/0.78 cnf(217,plain, % 0.70/0.78 (~P7(a5000)+P1(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[216,93])). % 0.70/0.78 cnf(218,plain, % 0.70/0.78 (~P2(a5000)+~P5(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[217,107])). % 0.70/0.78 cnf(219,plain, % 0.70/0.78 (P1(a5000)+P3(a5000)+~P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[218,14])). % 0.70/0.78 cnf(220,plain, % 0.70/0.78 (~P5(a5000)+P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[219,74])). % 0.70/0.78 cnf(231,plain, % 0.70/0.78 (P8(a5000)+~P6(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[153,49])). % 0.70/0.78 cnf(232,plain, % 0.70/0.78 (~P6(a5000)+P1(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[231,93])). % 0.70/0.78 cnf(233,plain, % 0.70/0.78 (~P2(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[232,188])). % 0.70/0.78 cnf(234,plain, % 0.70/0.78 (P1(a5000)+P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[233,1])). % 0.70/0.78 cnf(235,plain, % 0.70/0.78 (P6(a5000)+P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[234,196])). % 0.70/0.78 cnf(236,plain, % 0.70/0.78 (~P9(a5000)+P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[235,40])). % 0.70/0.78 cnf(237,plain, % 0.70/0.78 (P6(a5000)+P2(a5000)+~P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[236,15])). % 0.70/0.78 cnf(238,plain, % 0.70/0.78 (P2(a5000)+~P5(a5000)+P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[237,96])). % 0.70/0.78 cnf(239,plain, % 0.70/0.78 (~P5(a5000)+P7(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[238,142])). % 0.70/0.78 cnf(240,plain, % 0.70/0.78 (P7(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[239,109])). % 0.70/0.78 cnf(241,plain, % 0.70/0.78 (~P3(a5000)+P4(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[240,191])). % 0.70/0.78 cnf(242,plain, % 0.70/0.78 (P4(a5000)+P10(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[241,67])). % 0.70/0.78 cnf(243,plain, % 0.70/0.78 (P10(a5000)+P8(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[242,97])). % 0.70/0.78 cnf(244,plain, % 0.70/0.78 (~P3(a5000)+~P9(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[243,173])). % 0.70/0.78 cnf(245,plain, % 0.70/0.78 (~P9(a5000)+P10(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[244,67])). % 0.70/0.78 cnf(246,plain, % 0.70/0.78 (P8(a5000)+P10(a5000)+~P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[245,21])). % 0.70/0.78 cnf(247,plain, % 0.70/0.78 (~P5(a5000)+P10(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[246,71])). % 0.70/0.78 cnf(248,plain, % 0.70/0.78 (P10(a5000)+~P4(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[247,211])). % 0.70/0.78 cnf(249,plain, % 0.70/0.78 (P1(a5000)+P8(a5000)+~P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[248,113])). % 0.70/0.78 cnf(250,plain, % 0.70/0.78 (~P4(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[249,158])). % 0.70/0.78 cnf(254,plain, % 0.70/0.78 (P4(a5000)+P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[153,191])). % 0.70/0.78 cnf(255,plain, % 0.70/0.78 (P8(a5000)), % 0.70/0.78 inference(scs_inference,[],[254,250])). % 0.70/0.78 cnf(257,plain, % 0.70/0.78 (~P4(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[255,30])). % 0.70/0.78 cnf(258,plain, % 0.70/0.78 (~P1(a5000)+~P4(a5000)+~P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[255,55])). % 0.70/0.78 cnf(261,plain, % 0.70/0.78 (P3(a5000)+P9(a5000)+~P4(a5000)+~P10(a5000)), % 0.70/0.78 inference(scs_inference,[],[255,59])). % 0.70/0.78 cnf(262,plain, % 0.70/0.78 (P10(a5000)+P5(a5000)+P6(a5000)+P7(a5000)+P3(a5000)+P9(a5000)+~P1(a5000)+~P4(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[255,63])). % 0.70/0.78 cnf(263,plain, % 0.70/0.78 (P10(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[255,71])). % 0.70/0.78 cnf(265,plain, % 0.70/0.78 (P1(a5000)+P9(a5000)+P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[257,5])). % 0.70/0.78 cnf(266,plain, % 0.70/0.78 (P1(a5000)+~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[263,178])). % 0.70/0.78 cnf(267,plain, % 0.70/0.78 (~P3(a5000)+P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[266,196])). % 0.70/0.78 cnf(268,plain, % 0.70/0.78 (P4(a5000)+~P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[267,220])). % 0.70/0.78 cnf(269,plain, % 0.70/0.78 (~P5(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[268,257])). % 0.70/0.78 cnf(270,plain, % 0.70/0.78 (P1(a5000)+~P9(a5000)), % 0.70/0.78 inference(scs_inference,[],[269,127])). % 0.70/0.78 cnf(271,plain, % 0.70/0.78 (~P9(a5000)+P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[270,196])). % 0.70/0.78 cnf(272,plain, % 0.70/0.78 (P4(a5000)+P1(a5000)+P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[271,265])). % 0.70/0.78 cnf(278,plain, % 0.70/0.78 (P3(a5000)+P5(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[272,211])). % 0.70/0.78 cnf(281,plain, % 0.70/0.78 (P1(a5000)+P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[278,220])). % 0.70/0.78 cnf(282,plain, % 0.70/0.78 (P3(a5000)+P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[281,196])). % 0.70/0.78 cnf(283,plain, % 0.70/0.78 (P4(a5000)+P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[282,266])). % 0.70/0.78 cnf(284,plain, % 0.70/0.78 (P1(a5000)), % 0.70/0.78 inference(scs_inference,[],[283,257])). % 0.70/0.78 cnf(289,plain, % 0.70/0.78 (P4(a5000)), % 0.70/0.78 inference(scs_inference,[],[284,196])). % 0.70/0.78 cnf(291,plain, % 0.70/0.78 (~P4(a5000)+~P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[284,258])). % 0.70/0.78 cnf(292,plain, % 0.70/0.78 (P10(a5000)+P5(a5000)+P6(a5000)+P7(a5000)+P3(a5000)+P9(a5000)+~P4(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[284,262])). % 0.70/0.78 cnf(296,plain, % 0.70/0.78 (P3(a5000)+P9(a5000)+~P10(a5000)), % 0.70/0.78 inference(scs_inference,[],[289,261])). % 0.70/0.78 cnf(298,plain, % 0.70/0.78 (~P7(a5000)), % 0.70/0.78 inference(scs_inference,[],[289,291])). % 0.70/0.78 cnf(299,plain, % 0.70/0.78 (P10(a5000)+P5(a5000)+P6(a5000)+P7(a5000)+P3(a5000)+P9(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[289,292])). % 0.70/0.78 cnf(300,plain, % 0.70/0.78 (P2(a5000)+P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[298,7])). % 0.70/0.78 cnf(302,plain, % 0.70/0.78 (P5(a5000)+P3(a5000)+P9(a5000)+~P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[298,54])). % 0.70/0.78 cnf(307,plain, % 0.70/0.78 (~P9(a5000)), % 0.70/0.78 inference(scs_inference,[],[298,163])). % 0.70/0.78 cnf(310,plain, % 0.70/0.78 (~P3(a5000)), % 0.70/0.78 inference(scs_inference,[],[298,240])). % 0.70/0.78 cnf(319,plain, % 0.70/0.78 (~P5(a5000)), % 0.70/0.78 inference(scs_inference,[],[310,220])). % 0.70/0.78 cnf(325,plain, % 0.70/0.78 (~P10(a5000)), % 0.70/0.78 inference(scs_inference,[],[310,307,296])). % 0.70/0.78 cnf(326,plain, % 0.70/0.78 (P10(a5000)+P5(a5000)+P6(a5000)+~P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[298,310,307,299])). % 0.70/0.78 cnf(345,plain, % 0.70/0.78 (P2(a5000)), % 0.70/0.78 inference(scs_inference,[],[319,300])). % 0.70/0.78 cnf(346,plain, % 0.70/0.78 (~P6(a5000)), % 0.70/0.78 inference(scs_inference,[],[319,310,307,302])). % 0.70/0.78 cnf(369,plain, % 0.70/0.78 ($false), % 0.70/0.78 inference(scs_inference,[],[319,325,345,346,326]), % 0.70/0.78 ['proof']). % 0.70/0.78 % SZS output end Proof % 0.70/0.78 % Total time :0.200000s %------------------------------------------------------------------------------