%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ030-1 : 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 13:42:07 EDT 2024 % Result : Unsatisfiable 4.85s 4.90s % Output : CNFRefutation 4.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : PUZ030-1 : TPTP v8.2.0. Released v1.0.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 09:40:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.66/0.64 start to proof:theBenchmark % 4.85/4.89 %------------------------------------------- % 4.85/4.89 % File :CSE---1.7 % 4.85/4.89 % Problem :theBenchmark % 4.85/4.89 % Transform :cnf % 4.85/4.89 % Format :tptp:raw % 4.85/4.89 % Command :java -jar mcs_scs.jar %d %s % 4.85/4.89 % 4.85/4.89 % Result :Theorem 4.190000s % 4.85/4.89 % Output :CNFRefutation 4.190000s % 4.85/4.89 %------------------------------------------- % 4.85/4.89 %-------------------------------------------------------------------------- % 4.85/4.89 % File : PUZ030-1 : TPTP v8.2.0. Released v1.0.0. % 4.85/4.89 % Domain : Puzzles % 4.85/4.89 % Problem : Salt and Mustard Problem % 4.85/4.89 % Version : Especial. % 4.85/4.89 % English : % 4.85/4.89 % 4.85/4.89 % Refs : [LO85] Lusk & Overbeek (1985), Non-Horn Problems % 4.85/4.89 % : [Car86] Carroll (1986), Lewis Carroll's Symbolic Logic % 4.85/4.89 % : [MB88] Manthey & Bry (1988), SATCHMO: A Theorem Prover Implem % 4.85/4.89 % Source : [LO85] % 4.85/4.89 % Names : Salt and Mustard Problem [LO85] % 4.85/4.89 % : Salt-and-Mustard Problem [MB88] % 4.85/4.89 % 4.85/4.89 % Status : Unsatisfiable % 4.85/4.89 % Rating : 0.00 v5.5.0, 0.20 v5.4.0, 0.00 v2.2.0, 0.25 v2.1.0, 0.00 v2.0.0 % 4.85/4.89 % Syntax : Number of clauses : 43 ( 0 unt; 13 nHn; 41 RR) % 4.85/4.89 % Number of literals : 106 ( 0 equ; 55 neg) % 4.85/4.89 % Maximal clause size : 7 ( 2 avg) % 4.85/4.89 % Maximal term depth : 1 ( 1 avg) % 4.85/4.89 % Number of predicates : 5 ( 5 usr; 0 prp; 1-1 aty) % 4.85/4.89 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 4.85/4.89 % Number of variables : 12 ( 0 sgn) % 4.85/4.89 % SPC : CNF_UNS_EPR_NEQ_NHN % 4.85/4.89 % 4.85/4.89 % Comments : % 4.85/4.89 %-------------------------------------------------------------------------- % 4.85/4.89 cnf(both1,axiom, % 4.85/4.89 ( ~ both(X) % 4.85/4.89 | salt(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(both2,axiom, % 4.85/4.89 ( ~ both(X) % 4.85/4.89 | mustard(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(both3,axiom, % 4.85/4.89 ( ~ salt(X) % 4.85/4.89 | ~ mustard(X) % 4.85/4.89 | both(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(oneof1,axiom, % 4.85/4.89 ( ~ oneof(X) % 4.85/4.89 | salt(X) % 4.85/4.89 | mustard(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(oneof2,axiom, % 4.85/4.89 ( ~ oneof(X) % 4.85/4.89 | ~ both(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(oneof3,axiom, % 4.85/4.89 ( ~ oneof(X) % 4.85/4.89 | ~ neither(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(one_condition_holds1,axiom, % 4.85/4.89 ( both(X) % 4.85/4.89 | neither(X) % 4.85/4.89 | oneof(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(oneof4,axiom, % 4.85/4.89 ( ~ oneof(X) % 4.85/4.89 | ~ salt(X) % 4.85/4.89 | ~ mustard(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(neither1,axiom, % 4.85/4.89 ( ~ both(X) % 4.85/4.89 | ~ neither(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(neither2,axiom, % 4.85/4.89 ( ~ neither(X) % 4.85/4.89 | ~ salt(X) ) ). % 4.85/4.89 % 4.85/4.89 cnf(neither3,axiom, % 4.85/4.89 ( ~ neither(X) % 4.85/4.89 | ~ mustard(X) ) ). % 4.85/4.89 % 4.85/4.90 cnf(neither4,axiom, % 4.85/4.90 ( salt(X) % 4.85/4.90 | mustard(X) % 4.85/4.90 | neither(X) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule1_1,hypothesis, % 4.85/4.90 ( ~ salt(barry) % 4.85/4.90 | oneof(cole) % 4.85/4.90 | oneof(lang) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule1_2,hypothesis, % 4.85/4.90 ( ~ oneof(cole) % 4.85/4.90 | salt(barry) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule1_3,hypothesis, % 4.85/4.90 ( ~ oneof(lang) % 4.85/4.90 | salt(barry) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule2_1,hypothesis, % 4.85/4.90 ( ~ mustard(barry) % 4.85/4.90 | neither(dix) % 4.85/4.90 | both(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule2_2,hypothesis, % 4.85/4.90 ( ~ neither(dix) % 4.85/4.90 | mustard(barry) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule2_3,hypothesis, % 4.85/4.90 ( ~ both(mill) % 4.85/4.90 | mustard(barry) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule3_1,hypothesis, % 4.85/4.90 ( ~ salt(cole) % 4.85/4.90 | oneof(barry) % 4.85/4.90 | neither(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule3_2,hypothesis, % 4.85/4.90 ( ~ oneof(barry) % 4.85/4.90 | salt(cole) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule3_3,hypothesis, % 4.85/4.90 ( ~ neither(mill) % 4.85/4.90 | salt(cole) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule4_1,hypothesis, % 4.85/4.90 ( ~ mustard(cole) % 4.85/4.90 | both(dix) % 4.85/4.90 | both(lang) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule4_2,hypothesis, % 4.85/4.90 ( ~ both(dix) % 4.85/4.90 | mustard(cole) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule4_3,hypothesis, % 4.85/4.90 ( ~ both(lang) % 4.85/4.90 | mustard(cole) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule5_1,hypothesis, % 4.85/4.90 ( ~ salt(dix) % 4.85/4.90 | neither(barry) % 4.85/4.90 | both(cole) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule5_2,hypothesis, % 4.85/4.90 ( ~ neither(barry) % 4.85/4.90 | salt(dix) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule5_3,hypothesis, % 4.85/4.90 ( ~ both(cole) % 4.85/4.90 | salt(dix) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule6_1,hypothesis, % 4.85/4.90 ( ~ mustard(dix) % 4.85/4.90 | neither(lang) % 4.85/4.90 | neither(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule6_2,hypothesis, % 4.85/4.90 ( ~ neither(lang) % 4.85/4.90 | mustard(dix) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule6_3,hypothesis, % 4.85/4.90 ( ~ neither(mill) % 4.85/4.90 | mustard(dix) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule7_1,hypothesis, % 4.85/4.90 ( ~ salt(lang) % 4.85/4.90 | oneof(barry) % 4.85/4.90 | oneof(dix) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule7_2,hypothesis, % 4.85/4.90 ( ~ oneof(barry) % 4.85/4.90 | salt(lang) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule7_3,hypothesis, % 4.85/4.90 ( ~ oneof(dix) % 4.85/4.90 | salt(lang) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule8_1,hypothesis, % 4.85/4.90 ( ~ mustard(lang) % 4.85/4.90 | neither(cole) % 4.85/4.90 | neither(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule8_2,hypothesis, % 4.85/4.90 ( ~ neither(cole) % 4.85/4.90 | mustard(lang) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule8_3,hypothesis, % 4.85/4.90 ( ~ neither(mill) % 4.85/4.90 | mustard(lang) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule9_1,hypothesis, % 4.85/4.90 ( ~ salt(mill) % 4.85/4.90 | both(barry) % 4.85/4.90 | both(lang) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule9_2,hypothesis, % 4.85/4.90 ( ~ both(barry) % 4.85/4.90 | salt(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule9_3,hypothesis, % 4.85/4.90 ( ~ both(lang) % 4.85/4.90 | mustard(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule10_1,hypothesis, % 4.85/4.90 ( ~ mustard(mill) % 4.85/4.90 | oneof(cole) % 4.85/4.90 | oneof(dix) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule10_2,hypothesis, % 4.85/4.90 ( ~ oneof(cole) % 4.85/4.90 | mustard(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(rule10_3,hypothesis, % 4.85/4.90 ( ~ oneof(dix) % 4.85/4.90 | mustard(mill) ) ). % 4.85/4.90 % 4.85/4.90 cnf(prove_who_takes_what,negated_conjecture, % 4.85/4.90 ( ~ neither(cole) % 4.85/4.90 | ~ neither(dix) % 4.85/4.90 | ~ both(barry) % 4.85/4.90 | ~ oneof(lang) % 4.85/4.90 | ~ salt(mill) % 4.85/4.90 | ~ mustard(lang) % 4.85/4.90 | ~ oneof(mill) ) ). % 4.85/4.90 % 4.85/4.90 %-------------------------------------------------------------------------- % 4.85/4.90 %------------------------------------------- % 4.85/4.90 % Proof found % 4.85/4.90 % SZS status Theorem for theBenchmark % 4.85/4.90 % SZS output start Proof % 4.85/4.90 %ClaNum:43(EqnAxiom:0) % 4.85/4.90 %VarNum:29(SingletonVarNum:12) % 4.85/4.90 %MaxLitNum:7 % 4.85/4.90 %MaxfuncDepth:0 % 4.85/4.90 %SharedTerms:54 % 4.85/4.90 %goalClause: 43 % 4.85/4.90 [1]P1(a1)+~P2(a2) % 4.85/4.90 [2]P1(a1)+~P2(a3) % 4.85/4.90 [3]P1(a2)+~P2(a1) % 4.85/4.90 [4]P1(a2)+~P3(a5) % 4.85/4.90 [5]P1(a3)+~P2(a1) % 4.85/4.90 [6]P1(a3)+~P2(a4) % 4.85/4.90 [7]P1(a4)+~P4(a2) % 4.85/4.90 [8]P1(a4)+~P3(a1) % 4.85/4.90 [9]P1(a5)+~P4(a1) % 4.85/4.90 [10]P5(a1)+~P4(a5) % 4.85/4.90 [11]P5(a1)+~P3(a4) % 4.85/4.90 [12]P5(a2)+~P4(a3) % 4.85/4.90 [13]P5(a2)+~P4(a4) % 4.85/4.90 [14]P5(a3)+~P3(a2) % 4.85/4.90 [15]P5(a3)+~P3(a5) % 4.85/4.90 [16]P5(a4)+~P3(a3) % 4.85/4.90 [17]P5(a4)+~P3(a5) % 4.85/4.90 [18]P5(a5)+~P4(a3) % 4.85/4.90 [19]P5(a5)+~P2(a2) % 4.85/4.90 [20]P5(a5)+~P2(a4) % 4.85/4.90 [31]~P4(x311)+P1(x311) % 4.85/4.90 [32]~P4(x321)+P5(x321) % 4.85/4.90 [35]~P2(x351)+~P4(x351) % 4.85/4.90 [36]~P3(x361)+~P4(x361) % 4.85/4.90 [37]~P3(x371)+~P1(x371) % 4.85/4.90 [38]~P3(x381)+~P5(x381) % 4.85/4.90 [39]~P3(x391)+~P2(x391) % 4.85/4.90 [21]P4(a1)+P4(a3)+~P1(a5) % 4.85/4.90 [22]P4(a2)+P3(a1)+~P1(a4) % 4.85/4.90 [23]P4(a3)+P4(a4)+~P5(a2) % 4.85/4.90 [24]P4(a5)+P3(a4)+~P5(a1) % 4.85/4.90 [25]P2(a1)+P2(a4)+~P1(a3) % 4.85/4.90 [26]P2(a1)+P3(a5)+~P1(a2) % 4.85/4.90 [27]P2(a2)+P2(a3)+~P1(a1) % 4.85/4.90 [28]P2(a2)+P2(a4)+~P5(a5) % 4.85/4.90 [29]P3(a2)+P3(a5)+~P5(a3) % 4.85/4.90 [30]P3(a3)+P3(a5)+~P5(a4) % 4.85/4.90 [33]P2(x331)+P3(x331)+P4(x331) % 4.85/4.90 [34]P5(x341)+P3(x341)+P1(x341) % 4.85/4.90 [40]P5(x401)+~P2(x401)+P1(x401) % 4.85/4.90 [41]~P1(x411)+~P5(x411)+P4(x411) % 4.85/4.90 [42]~P5(x421)+~P2(x421)+~P1(x421) % 4.85/4.90 [43]~P4(a1)+~P1(a5)+~P5(a3)+~P2(a3)+~P2(a5)+~P3(a2)+~P3(a4) % 4.85/4.90 %EqnAxiom % 4.85/4.90 % 4.85/4.90 %------------------------------------------- % 4.85/4.91 cnf(44,plain, % 4.85/4.91 (~P3(a1)+~P2(a2)), % 4.85/4.91 inference(scs_inference,[],[1,37])). % 4.85/4.91 cnf(45,plain, % 4.85/4.91 (~P3(a1)+~P2(a3)), % 4.85/4.91 inference(scs_inference,[],[2,37])). % 4.85/4.91 cnf(46,plain, % 4.85/4.91 (~P3(a2)+~P2(a1)), % 4.85/4.91 inference(scs_inference,[],[3,37])). % 4.85/4.91 cnf(48,plain, % 4.85/4.91 (~P3(a3)+~P2(a1)), % 4.85/4.91 inference(scs_inference,[],[5,37])). % 4.85/4.91 cnf(49,plain, % 4.85/4.91 (~P3(a3)+~P2(a4)), % 4.85/4.91 inference(scs_inference,[],[6,37])). % 4.85/4.91 cnf(51,plain, % 4.85/4.91 (~P3(a4)+~P3(a1)), % 4.85/4.91 inference(scs_inference,[],[8,37])). % 4.85/4.91 cnf(52,plain, % 4.85/4.91 (~P3(a5)+~P4(a1)), % 4.85/4.91 inference(scs_inference,[],[9,37])). % 4.85/4.91 cnf(55,plain, % 4.85/4.91 (~P3(a2)+~P4(a3)), % 4.85/4.91 inference(scs_inference,[],[12,38])). % 4.85/4.91 cnf(56,plain, % 4.85/4.91 (~P3(a2)+~P4(a4)), % 4.85/4.91 inference(scs_inference,[],[13,38])). % 4.85/4.91 cnf(57,plain, % 4.85/4.91 (~P3(a3)+~P3(a2)), % 4.85/4.91 inference(scs_inference,[],[14,38])). % 4.85/4.91 cnf(59,plain, % 4.85/4.91 (~P3(a4)+~P3(a3)), % 4.85/4.91 inference(scs_inference,[],[16,38])). % 4.85/4.91 cnf(61,plain, % 4.85/4.91 (~P3(a5)+~P4(a3)), % 4.85/4.91 inference(scs_inference,[],[18,38])). % 4.85/4.91 cnf(62,plain, % 4.85/4.91 (~P3(a5)+~P2(a2)), % 4.85/4.91 inference(scs_inference,[],[19,38])). % 4.85/4.91 cnf(63,plain, % 4.85/4.91 (~P3(a5)+~P2(a4)), % 4.85/4.91 inference(scs_inference,[],[20,38])). % 4.85/4.91 cnf(65,plain, % 4.85/4.91 (~P4(a2)+P4(a3)+P4(a4)), % 4.85/4.91 inference(scs_inference,[],[32,23])). % 4.85/4.91 cnf(66,plain, % 4.85/4.91 (~P2(a2)+P3(a1)+~P1(a4)), % 4.85/4.91 inference(scs_inference,[],[35,22])). % 4.85/4.91 cnf(69,plain, % 4.85/4.91 (~P2(a2)+~P1(a4)), % 4.85/4.91 inference(scs_inference,[],[44,66])). % 4.85/4.91 cnf(70,plain, % 4.85/4.91 (~P2(a3)+P4(a2)+~P1(a4)), % 4.93/4.91 inference(scs_inference,[],[45,22])). % 4.93/4.91 cnf(71,plain, % 4.93/4.91 (~P2(a1)+P3(a5)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[46,29])). % 4.93/4.91 cnf(73,plain, % 4.93/4.91 (~P2(a1)+P3(a5)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[48,30])). % 4.93/4.91 cnf(74,plain, % 4.93/4.91 (~P2(a4)+P3(a5)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[49,30])). % 4.93/4.91 cnf(76,plain, % 4.93/4.91 (P4(a4)+P2(a4)+~P3(a1)), % 4.93/4.91 inference(scs_inference,[],[51,33])). % 4.93/4.91 cnf(77,plain, % 4.93/4.91 (~P4(a1)+P2(a1)+~P1(a2)), % 4.93/4.91 inference(scs_inference,[],[52,26])). % 4.93/4.91 cnf(79,plain, % 4.93/4.91 (~P4(a3)+P3(a5)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[55,29])). % 4.93/4.91 cnf(80,plain, % 4.93/4.91 (P4(a2)+P2(a2)+~P4(a4)), % 4.93/4.91 inference(scs_inference,[],[56,33])). % 4.93/4.91 cnf(81,plain, % 4.93/4.91 (~P3(a2)+P3(a5)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[57,30])). % 4.93/4.91 cnf(83,plain, % 4.93/4.91 (~P3(a3)+~P5(a1)+P4(a5)), % 4.93/4.91 inference(scs_inference,[],[59,24])). % 4.93/4.91 cnf(85,plain, % 4.93/4.91 (~P4(a3)+~P2(a1)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[61,71])). % 4.93/4.91 cnf(86,plain, % 4.93/4.91 (~P2(a2)+~P2(a1)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[62,73])). % 4.93/4.91 cnf(87,plain, % 4.93/4.91 (~P2(a4)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[63,74])). % 4.93/4.91 cnf(88,plain, % 4.93/4.91 (~P1(a4)+P2(a3)+~P1(a1)), % 4.93/4.91 inference(scs_inference,[],[69,27])). % 4.93/4.91 cnf(89,plain, % 4.93/4.91 (~P5(a4)+P2(a2)+~P5(a5)), % 4.93/4.91 inference(scs_inference,[],[87,28])). % 4.93/4.91 cnf(91,plain, % 4.93/4.91 (P1(a4)+~P2(a4)), % 4.93/4.91 inference(scs_inference,[],[40,87])). % 4.93/4.91 cnf(92,plain, % 4.93/4.91 (~P2(a4)+~P2(a2)), % 4.93/4.91 inference(scs_inference,[],[91,69])). % 4.93/4.91 cnf(93,plain, % 4.93/4.91 (~P2(a2)+P2(a1)+~P1(a3)), % 4.93/4.91 inference(scs_inference,[],[92,25])). % 4.93/4.91 cnf(96,plain, % 4.93/4.91 (P4(a2)+~P1(a4)+~P1(a1)), % 4.93/4.91 inference(scs_inference,[],[70,88])). % 4.93/4.91 cnf(98,plain, % 4.93/4.91 (P3(a1)+P2(a1)+~P1(a2)), % 4.93/4.91 inference(scs_inference,[],[77,33])). % 4.93/4.91 cnf(99,plain, % 4.93/4.91 (~P5(a3)+~P1(a3)+P3(a5)), % 4.93/4.91 inference(scs_inference,[],[79,41])). % 4.93/4.91 cnf(100,plain, % 4.93/4.91 (P1(a2)+P2(a2)+~P4(a4)), % 4.93/4.91 inference(scs_inference,[],[80,31])). % 4.93/4.91 cnf(101,plain, % 4.93/4.91 (~P5(a4)+P3(a5)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[81,29])). % 4.93/4.91 cnf(103,plain, % 4.93/4.91 (~P5(a3)+~P1(a3)+~P2(a1)), % 4.93/4.91 inference(scs_inference,[],[85,41])). % 4.93/4.91 cnf(108,plain, % 4.93/4.91 (P2(a1)+~P1(a2)+P1(a4)), % 4.93/4.91 inference(scs_inference,[],[98,8])). % 4.93/4.91 cnf(109,plain, % 4.93/4.91 (~P1(a3)+P3(a5)+~P3(a2)), % 4.93/4.91 inference(scs_inference,[],[99,14])). % 4.93/4.91 cnf(112,plain, % 4.93/4.91 (~P1(a3)+~P2(a1)+~P3(a5)), % 4.93/4.91 inference(scs_inference,[],[103,15])). % 4.93/4.91 cnf(114,plain, % 4.93/4.91 (P3(a5)+~P3(a2)+~P2(a4)), % 4.93/4.91 inference(scs_inference,[],[109,6])). % 4.93/4.91 cnf(116,plain, % 4.93/4.91 (~P3(a5)+~P2(a1)), % 4.93/4.91 inference(scs_inference,[],[112,5])). % 4.93/4.91 cnf(118,plain, % 4.93/4.91 (~P3(a2)+~P2(a4)+P1(a2)), % 4.93/4.91 inference(scs_inference,[],[114,4])). % 4.93/4.91 cnf(119,plain, % 4.93/4.91 (P1(a2)+P5(a2)+~P2(a4)), % 4.93/4.91 inference(scs_inference,[],[118,34])). % 4.93/4.91 cnf(120,plain, % 4.93/4.91 (~P3(a2)+P5(a2)+~P2(a4)), % 4.93/4.91 inference(scs_inference,[],[119,37])). % 4.93/4.91 cnf(121,plain, % 4.93/4.91 (~P3(a2)+~P2(a4)), % 4.93/4.91 inference(scs_inference,[],[120,38])). % 4.93/4.91 cnf(122,plain, % 4.93/4.91 (~P2(a4)+P3(a5)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[121,29])). % 4.93/4.91 cnf(123,plain, % 4.93/4.91 (~P5(a3)+~P2(a4)), % 4.93/4.91 inference(scs_inference,[],[122,63])). % 4.93/4.91 cnf(124,plain, % 4.93/4.91 (~P4(a3)+~P2(a4)), % 4.93/4.91 inference(scs_inference,[],[123,32])). % 4.93/4.91 cnf(125,plain, % 4.93/4.91 (~P2(a4)+~P1(a5)+P4(a1)), % 4.93/4.91 inference(scs_inference,[],[124,21])). % 4.93/4.91 cnf(128,plain, % 4.93/4.91 (P1(a1)+P2(a4)+~P5(a5)), % 4.93/4.91 inference(scs_inference,[],[1,28])). % 4.93/4.91 cnf(129,plain, % 4.93/4.91 (~P3(a1)+P2(a4)+~P5(a5)), % 4.93/4.91 inference(scs_inference,[],[128,37])). % 4.93/4.91 cnf(139,plain, % 4.93/4.91 (P1(a1)+P4(a2)+~P4(a4)), % 4.93/4.91 inference(scs_inference,[],[1,80])). % 4.93/4.91 cnf(140,plain, % 4.93/4.91 (~P4(a4)+P4(a2)+~P1(a4)), % 4.93/4.91 inference(scs_inference,[],[139,96])). % 4.93/4.91 cnf(141,plain, % 4.93/4.91 (~P5(a4)+~P1(a4)+P4(a2)), % 4.93/4.91 inference(scs_inference,[],[140,41])). % 4.93/4.91 cnf(142,plain, % 4.93/4.91 (~P1(a4)+P4(a2)+~P3(a3)), % 4.93/4.91 inference(scs_inference,[],[141,16])). % 4.93/4.91 cnf(150,plain, % 4.93/4.91 (P1(a1)+P1(a2)+~P4(a4)), % 4.93/4.91 inference(scs_inference,[],[1,100])). % 4.93/4.91 cnf(151,plain, % 4.93/4.91 (~P3(a1)+P1(a2)+~P4(a4)), % 4.93/4.91 inference(scs_inference,[],[150,37])). % 4.93/4.91 cnf(152,plain, % 4.93/4.91 (P3(a3)+P4(a3)+P1(a1)), % 4.93/4.91 inference(scs_inference,[],[2,33])). % 4.93/4.91 cnf(153,plain, % 4.93/4.91 (P4(a3)+P1(a1)+P5(a4)), % 4.93/4.91 inference(scs_inference,[],[152,16])). % 4.93/4.91 cnf(154,plain, % 4.93/4.91 (P1(a1)+P5(a4)+P5(a2)), % 4.93/4.91 inference(scs_inference,[],[153,12])). % 4.93/4.91 cnf(155,plain, % 4.93/4.91 (~P3(a1)+P5(a4)+P5(a2)), % 4.93/4.91 inference(scs_inference,[],[154,37])). % 4.93/4.91 cnf(157,plain, % 4.93/4.91 (P4(a1)+~P5(a1)+~P2(a3)), % 4.93/4.91 inference(scs_inference,[],[2,41])). % 4.93/4.91 cnf(158,plain, % 4.93/4.91 (~P5(a1)+~P2(a3)+P1(a5)), % 4.93/4.91 inference(scs_inference,[],[157,9])). % 4.93/4.91 cnf(160,plain, % 4.93/4.91 (~P2(a1)+~P5(a1)+~P2(a3)), % 4.93/4.91 inference(scs_inference,[],[2,42])). % 4.93/4.91 cnf(176,plain, % 4.93/4.91 (P3(a1)+P4(a1)+P1(a2)), % 4.93/4.91 inference(scs_inference,[],[3,33])). % 4.93/4.91 cnf(179,plain, % 4.93/4.91 (P1(a2)+~P2(a2)+~P1(a3)), % 4.93/4.91 inference(scs_inference,[],[3,93])). % 4.93/4.91 cnf(180,plain, % 4.93/4.91 (~P2(a2)+~P5(a2)+~P1(a3)), % 4.93/4.91 inference(scs_inference,[],[179,42])). % 4.93/4.91 cnf(184,plain, % 4.93/4.91 (P1(a2)+P3(a2)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[4,29])). % 4.93/4.91 cnf(186,plain, % 4.93/4.91 (P1(a2)+P3(a3)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[4,30])). % 4.93/4.91 cnf(187,plain, % 4.93/4.91 (~P3(a2)+P3(a3)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[186,37])). % 4.93/4.91 cnf(188,plain, % 4.93/4.91 (~P5(a4)+~P3(a2)), % 4.93/4.91 inference(scs_inference,[],[187,57])). % 4.93/4.91 cnf(189,plain, % 4.93/4.91 (P3(a4)+P1(a4)+~P3(a2)), % 4.93/4.91 inference(scs_inference,[],[188,34])). % 4.93/4.91 cnf(203,plain, % 4.93/4.91 (~P3(a5)+P3(a1)+P2(a1)), % 4.93/4.91 inference(scs_inference,[],[4,98])). % 4.93/4.91 cnf(204,plain, % 4.93/4.91 (P3(a1)+~P3(a5)), % 4.93/4.91 inference(scs_inference,[],[203,116])). % 4.93/4.91 cnf(215,plain, % 4.93/4.91 (P1(a3)+P3(a5)+~P1(a2)), % 4.93/4.91 inference(scs_inference,[],[5,26])). % 4.93/4.91 cnf(229,plain, % 4.93/4.91 (P1(a3)+~P4(a1)+~P1(a2)), % 4.93/4.91 inference(scs_inference,[],[5,77])). % 4.93/4.91 cnf(230,plain, % 4.93/4.91 (~P3(a3)+~P4(a1)+~P1(a2)), % 4.93/4.91 inference(scs_inference,[],[229,37])). % 4.93/4.91 cnf(233,plain, % 4.93/4.91 (P1(a3)+~P1(a2)+P3(a1)), % 4.93/4.91 inference(scs_inference,[],[5,98])). % 4.93/4.91 cnf(234,plain, % 4.93/4.91 (~P3(a3)+~P1(a2)+P3(a1)), % 4.93/4.91 inference(scs_inference,[],[233,37])). % 4.93/4.91 cnf(235,plain, % 4.93/4.91 (P1(a3)+~P1(a2)+P1(a4)), % 4.93/4.91 inference(scs_inference,[],[5,108])). % 4.93/4.91 cnf(245,plain, % 4.93/4.91 (P1(a3)+P2(a2)+~P5(a5)), % 4.93/4.91 inference(scs_inference,[],[6,28])). % 4.93/4.91 cnf(246,plain, % 4.93/4.91 (~P3(a3)+P2(a2)+~P5(a5)), % 4.93/4.91 inference(scs_inference,[],[245,37])). % 4.93/4.91 cnf(262,plain, % 4.93/4.91 (P3(a2)+P2(a2)+P1(a4)), % 4.93/4.91 inference(scs_inference,[],[7,33])). % 4.93/4.91 cnf(263,plain, % 4.93/4.91 (P2(a2)+P3(a4)+P1(a4)), % 4.93/4.91 inference(scs_inference,[],[262,189])). % 4.93/4.91 cnf(290,plain, % 4.93/4.91 (P4(a4)+~P5(a4)+~P3(a1)), % 4.93/4.91 inference(scs_inference,[],[8,41])). % 4.93/4.91 cnf(291,plain, % 4.93/4.91 (~P5(a4)+~P3(a1)+P1(a2)), % 4.93/4.91 inference(scs_inference,[],[290,151])). % 4.93/4.91 cnf(292,plain, % 4.93/4.91 (~P5(a4)+P4(a1)+P1(a2)), % 4.93/4.91 inference(scs_inference,[],[291,176])). % 4.93/4.91 cnf(293,plain, % 4.93/4.91 (P4(a1)+P1(a2)+~P3(a3)), % 4.93/4.91 inference(scs_inference,[],[292,16])). % 4.93/4.91 cnf(294,plain, % 4.93/4.91 (~P3(a1)+~P4(a4)+P4(a2)), % 4.93/4.91 inference(scs_inference,[],[8,140])). % 4.93/4.91 cnf(307,plain, % 4.93/4.91 (~P3(a1)+P4(a2)+~P3(a3)), % 4.93/4.91 inference(scs_inference,[],[8,142])). % 4.93/4.91 cnf(308,plain, % 4.93/4.91 (P4(a2)+~P3(a3)+~P1(a2)), % 4.93/4.91 inference(scs_inference,[],[307,234])). % 4.93/4.91 cnf(309,plain, % 4.93/4.91 (~P2(a2)+~P3(a3)+~P1(a2)), % 4.93/4.91 inference(scs_inference,[],[308,35])). % 4.93/4.91 cnf(310,plain, % 4.93/4.91 (~P1(a2)+~P3(a3)+~P5(a5)), % 4.93/4.91 inference(scs_inference,[],[309,246])). % 4.93/4.91 cnf(311,plain, % 4.93/4.91 (~P5(a5)+P4(a1)+~P3(a3)), % 4.93/4.91 inference(scs_inference,[],[310,293])). % 4.93/4.91 cnf(333,plain, % 4.93/4.91 (P1(a5)+~P5(a5)+~P3(a3)), % 4.93/4.91 inference(scs_inference,[],[9,311])). % 4.93/4.91 cnf(334,plain, % 4.93/4.91 (P4(a5)+~P5(a5)+~P3(a3)), % 4.93/4.91 inference(scs_inference,[],[333,41])). % 4.93/4.91 cnf(335,plain, % 4.93/4.91 (~P5(a5)+~P3(a3)+P5(a1)), % 4.93/4.91 inference(scs_inference,[],[334,10])). % 4.93/4.91 cnf(350,plain, % 4.93/4.91 (P4(a4)+P2(a4)+P5(a1)), % 4.93/4.91 inference(scs_inference,[],[11,33])). % 4.93/4.91 cnf(353,plain, % 4.93/4.91 (P1(a4)+P5(a4)+P5(a1)), % 4.93/4.91 inference(scs_inference,[],[11,34])). % 4.93/4.91 cnf(354,plain, % 4.93/4.91 (P5(a4)+P5(a1)+~P2(a2)), % 4.93/4.91 inference(scs_inference,[],[353,69])). % 4.93/4.91 cnf(355,plain, % 4.93/4.91 (P5(a1)+~P2(a1)+~P2(a2)), % 4.93/4.91 inference(scs_inference,[],[354,86])). % 4.93/4.91 cnf(356,plain, % 4.93/4.91 (~P1(a1)+~P2(a1)+~P2(a2)), % 4.93/4.91 inference(scs_inference,[],[355,42])). % 4.93/4.91 cnf(357,plain, % 4.93/4.91 (~P2(a1)+~P2(a2)), % 4.93/4.91 inference(scs_inference,[],[356,1])). % 4.93/4.91 cnf(358,plain, % 4.93/4.91 (~P2(a2)+~P1(a3)+P2(a4)), % 4.93/4.91 inference(scs_inference,[],[357,25])). % 4.93/4.91 cnf(359,plain, % 4.93/4.91 (~P1(a3)+P2(a4)+~P5(a5)), % 4.93/4.91 inference(scs_inference,[],[358,28])). % 4.93/4.91 cnf(392,plain, % 4.93/4.91 (P3(a4)+P2(a4)+P5(a2)), % 4.93/4.91 inference(scs_inference,[],[13,33])). % 4.93/4.91 cnf(393,plain, % 4.93/4.91 (~P3(a2)+P3(a4)+P2(a4)), % 4.93/4.91 inference(scs_inference,[],[392,38])). % 4.93/4.91 cnf(394,plain, % 4.93/4.91 (P3(a4)+~P3(a2)), % 4.93/4.91 inference(scs_inference,[],[393,121])). % 4.93/4.91 cnf(395,plain, % 4.93/4.91 (~P3(a2)+P5(a1)), % 4.93/4.91 inference(scs_inference,[],[394,11])). % 4.93/4.91 cnf(396,plain, % 4.93/4.91 (P4(a2)+P2(a2)+P5(a1)), % 4.93/4.91 inference(scs_inference,[],[395,33])). % 4.93/4.91 cnf(397,plain, % 4.93/4.91 (P1(a2)+P2(a2)+P5(a1)), % 4.93/4.91 inference(scs_inference,[],[396,31])). % 4.93/4.91 cnf(406,plain, % 4.93/4.91 (~P4(a4)+~P2(a2)+~P1(a3)), % 4.93/4.91 inference(scs_inference,[],[13,180])). % 4.93/4.91 cnf(407,plain, % 4.93/4.91 (~P1(a3)+P4(a2)+~P4(a4)), % 4.93/4.91 inference(scs_inference,[],[406,80])). % 4.93/4.91 cnf(409,plain, % 4.93/4.91 (P5(a2)+~P5(a4)+~P3(a1)), % 4.93/4.91 inference(scs_inference,[],[13,290])). % 4.93/4.91 cnf(410,plain, % 4.93/4.91 (~P3(a1)+P5(a2)), % 4.93/4.91 inference(scs_inference,[],[409,155])). % 4.93/4.91 cnf(411,plain, % 4.93/4.91 (P5(a2)+P4(a2)+~P1(a4)), % 4.93/4.91 inference(scs_inference,[],[410,22])). % 4.93/4.91 cnf(412,plain, % 4.93/4.91 (P4(a2)+~P1(a2)+~P1(a4)), % 4.93/4.91 inference(scs_inference,[],[411,41])). % 4.93/4.91 cnf(413,plain, % 4.93/4.91 (P5(a2)+~P1(a2)+~P1(a4)), % 4.93/4.91 inference(scs_inference,[],[412,32])). % 4.93/4.91 cnf(414,plain, % 4.93/4.91 (~P1(a4)+~P2(a4)+P5(a2)), % 4.93/4.91 inference(scs_inference,[],[413,119])). % 4.93/4.91 cnf(415,plain, % 4.93/4.91 (~P2(a4)+P5(a4)+P5(a2)), % 4.93/4.91 inference(scs_inference,[],[414,40])). % 4.93/4.91 cnf(429,plain, % 4.93/4.91 (P4(a3)+~P1(a3)+~P3(a5)), % 4.93/4.91 inference(scs_inference,[],[15,41])). % 4.93/4.91 cnf(440,plain, % 4.93/4.91 (P5(a4)+P3(a5)+~P5(a4)), % 4.93/4.91 inference(scs_inference,[],[16,30])). % 4.93/4.91 cnf(441,plain, % 4.93/4.91 (~P5(a4)+P5(a4)), % 4.93/4.91 inference(scs_inference,[],[440,17])). % 4.93/4.91 cnf(445,plain, % 4.93/4.91 (P4(a4)+~P1(a4)+~P3(a3)), % 4.93/4.91 inference(scs_inference,[],[16,41])). % 4.93/4.91 cnf(446,plain, % 4.93/4.91 (P1(a3)+P5(a3)+P5(a4)), % 4.93/4.91 inference(scs_inference,[],[16,34])). % 4.93/4.91 cnf(455,plain, % 4.93/4.91 (~P3(a3)+~P3(a1)+P1(a2)), % 4.93/4.91 inference(scs_inference,[],[16,291])). % 4.93/4.91 cnf(463,plain, % 4.93/4.91 (P5(a4)+P3(a2)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[17,29])). % 4.93/4.91 cnf(469,plain, % 4.93/4.91 (P5(a4)+~P4(a3)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[17,79])). % 4.93/4.91 cnf(470,plain, % 4.93/4.91 (~P4(a3)+P5(a4)), % 4.93/4.91 inference(scs_inference,[],[469,32])). % 4.93/4.91 cnf(479,plain, % 4.93/4.91 (P5(a5)+~P1(a3)+~P3(a5)), % 4.93/4.91 inference(scs_inference,[],[18,429])). % 4.93/4.91 cnf(480,plain, % 4.93/4.91 (~P3(a5)+~P1(a3)+P2(a4)), % 4.93/4.91 inference(scs_inference,[],[479,359])). % 4.93/4.91 cnf(481,plain, % 4.93/4.91 (P2(a4)+~P1(a3)+~P5(a3)), % 4.93/4.91 inference(scs_inference,[],[480,99])). % 4.93/4.91 cnf(482,plain, % 4.93/4.91 (~P1(a3)+~P5(a3)+P5(a5)), % 4.93/4.91 inference(scs_inference,[],[481,20])). % 4.93/4.91 cnf(502,plain, % 4.93/4.91 (~P4(a3)+P2(a4)+~P3(a1)), % 4.93/4.91 inference(scs_inference,[],[18,129])). % 4.93/4.91 cnf(503,plain, % 4.93/4.91 (~P3(a1)+~P4(a3)), % 4.93/4.91 inference(scs_inference,[],[502,124])). % 4.93/4.91 cnf(504,plain, % 4.93/4.91 (~P4(a3)+P4(a2)+~P1(a4)), % 4.93/4.91 inference(scs_inference,[],[503,22])). % 4.93/4.91 cnf(510,plain, % 4.93/4.91 (P5(a5)+~P4(a2)+P4(a4)), % 4.93/4.91 inference(scs_inference,[],[18,65])). % 4.93/4.91 cnf(511,plain, % 4.93/4.91 (~P4(a3)+~P1(a3)+P2(a4)), % 4.93/4.91 inference(scs_inference,[],[18,359])). % 4.93/4.91 cnf(512,plain, % 4.93/4.91 (~P4(a3)+P2(a4)), % 4.93/4.91 inference(scs_inference,[],[511,31])). % 4.93/4.91 cnf(513,plain, % 4.93/4.92 (P2(a4)+~P1(a5)+P4(a1)), % 4.93/4.92 inference(scs_inference,[],[512,21])). % 4.93/4.92 cnf(514,plain, % 4.93/4.92 (P4(a1)+~P1(a5)), % 4.93/4.92 inference(scs_inference,[],[513,125])). % 4.93/4.92 cnf(516,plain, % 4.93/4.92 (P5(a5)+P3(a3)+P1(a1)), % 4.93/4.92 inference(scs_inference,[],[18,152])). % 4.93/4.92 cnf(517,plain, % 4.93/4.92 (P3(a3)+P2(a4)+P1(a1)), % 4.93/4.92 inference(scs_inference,[],[516,128])). % 4.93/4.92 cnf(518,plain, % 4.93/4.92 (~P3(a1)+P3(a3)+P2(a4)), % 4.93/4.92 inference(scs_inference,[],[517,37])). % 4.93/4.92 cnf(519,plain, % 4.93/4.92 (P3(a3)+P2(a4)+~P3(a5)), % 4.93/4.92 inference(scs_inference,[],[518,204])). % 4.93/4.92 cnf(520,plain, % 4.93/4.92 (~P5(a3)+P2(a4)+~P3(a5)), % 4.93/4.92 inference(scs_inference,[],[519,38])). % 4.93/4.92 cnf(521,plain, % 4.93/4.92 (P2(a4)+~P3(a5)), % 4.93/4.92 inference(scs_inference,[],[520,15])). % 4.93/4.92 cnf(522,plain, % 4.93/4.92 (~P3(a5)+P1(a3)), % 4.93/4.92 inference(scs_inference,[],[521,6])). % 4.93/4.92 cnf(523,plain, % 4.93/4.92 (P1(a3)+~P1(a2)+P2(a1)), % 4.93/4.92 inference(scs_inference,[],[522,26])). % 4.93/4.92 cnf(524,plain, % 4.93/4.92 (~P1(a2)+P2(a1)+~P2(a2)), % 4.93/4.92 inference(scs_inference,[],[523,93])). % 4.93/4.92 cnf(525,plain, % 4.93/4.92 (~P2(a2)+P5(a2)+P2(a1)), % 4.93/4.92 inference(scs_inference,[],[524,40])). % 4.93/4.92 cnf(526,plain, % 4.93/4.92 (P5(a2)+~P2(a2)), % 4.93/4.92 inference(scs_inference,[],[525,357])). % 4.93/4.92 cnf(527,plain, % 4.93/4.92 (~P2(a2)+P4(a4)+P4(a3)), % 4.93/4.92 inference(scs_inference,[],[526,23])). % 4.93/4.92 cnf(536,plain, % 4.93/4.92 (P3(a2)+P4(a2)+P5(a5)), % 4.93/4.92 inference(scs_inference,[],[19,33])). % 4.93/4.92 cnf(537,plain, % 4.93/4.92 (P4(a2)+P5(a5)+P5(a3)), % 4.93/4.92 inference(scs_inference,[],[536,14])). % 4.93/4.92 cnf(538,plain, % 4.93/4.92 (P5(a3)+P5(a5)+P4(a4)), % 4.93/4.92 inference(scs_inference,[],[537,510])). % 4.93/4.92 cnf(539,plain, % 4.93/4.92 (P4(a4)+~P1(a3)+P5(a5)), % 4.93/4.92 inference(scs_inference,[],[538,482])). % 4.93/4.92 cnf(540,plain, % 4.93/4.92 (P5(a5)+~P1(a3)+P4(a2)), % 4.93/4.92 inference(scs_inference,[],[539,407])). % 4.93/4.92 cnf(541,plain, % 4.93/4.92 (P4(a2)+~P1(a3)+P2(a4)), % 4.93/4.92 inference(scs_inference,[],[540,359])). % 4.93/4.92 cnf(542,plain, % 4.93/4.92 (~P1(a3)+P2(a4)+P1(a4)), % 4.93/4.92 inference(scs_inference,[],[541,7])). % 4.93/4.92 cnf(543,plain, % 4.93/4.92 (P2(a4)+~P1(a2)+P1(a4)), % 4.93/4.92 inference(scs_inference,[],[542,235])). % 4.93/4.92 cnf(544,plain, % 4.93/4.92 (~P1(a2)+P1(a4)+P5(a5)), % 4.93/4.92 inference(scs_inference,[],[543,20])). % 4.93/4.92 cnf(546,plain, % 4.93/4.92 (P5(a5)+P4(a2)+~P4(a4)), % 4.93/4.92 inference(scs_inference,[],[19,80])). % 4.93/4.92 cnf(586,plain, % 4.93/4.92 (P5(a5)+P1(a2)+P5(a1)), % 4.93/4.92 inference(scs_inference,[],[19,397])). % 4.93/4.92 cnf(587,plain, % 4.93/4.92 (P1(a2)+~P3(a3)+P5(a1)), % 4.93/4.92 inference(scs_inference,[],[586,335])). % 4.93/4.92 cnf(588,plain, % 4.93/4.92 (P5(a1)+P3(a1)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[587,234])). % 4.93/4.92 cnf(589,plain, % 4.93/4.92 (P3(a1)+~P3(a3)+P4(a5)), % 4.93/4.92 inference(scs_inference,[],[588,83])). % 4.93/4.92 cnf(590,plain, % 4.93/4.92 (P4(a5)+~P3(a3)+P1(a2)), % 4.93/4.92 inference(scs_inference,[],[589,455])). % 4.93/4.92 cnf(591,plain, % 4.93/4.92 (P5(a5)+P1(a2)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[590,32])). % 4.93/4.92 cnf(592,plain, % 4.93/4.92 (P1(a2)+P2(a2)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[591,246])). % 4.93/4.92 cnf(593,plain, % 4.93/4.92 (P2(a2)+~P3(a3)+~P4(a1)), % 4.93/4.92 inference(scs_inference,[],[592,230])). % 4.93/4.92 cnf(604,plain, % 4.93/4.92 (P5(a5)+~P3(a5)), % 4.93/4.92 inference(scs_inference,[],[20,521])). % 4.93/4.92 cnf(605,plain, % 4.93/4.92 (~P3(a5)), % 4.93/4.92 inference(scs_inference,[],[604,38])). % 4.93/4.92 cnf(606,plain, % 4.93/4.92 (~P1(a2)+P2(a1)), % 4.93/4.92 inference(scs_inference,[],[605,26])). % 4.93/4.92 cnf(608,plain, % 4.93/4.92 (P3(a3)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[605,30])). % 4.93/4.92 cnf(609,plain, % 4.93/4.92 (~P2(a1)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[605,73])). % 4.93/4.92 cnf(612,plain, % 4.93/4.92 (~P5(a4)+~P5(a3)), % 4.93/4.92 inference(scs_inference,[],[605,101])). % 4.93/4.92 cnf(615,plain, % 4.93/4.92 (P1(a3)+~P1(a2)), % 4.93/4.92 inference(scs_inference,[],[605,215])). % 4.93/4.92 cnf(624,plain, % 4.93/4.92 (P5(a5)+P2(a5)), % 4.93/4.92 inference(scs_inference,[],[605,33,31,514,32])). % 4.93/4.92 cnf(633,plain, % 4.93/4.92 (P5(a5)+P4(a1)), % 4.93/4.92 inference(scs_inference,[],[605,34,514])). % 4.93/4.92 cnf(641,plain, % 4.93/4.92 (~P4(a2)+P2(a1)), % 4.93/4.92 inference(scs_inference,[],[606,31])). % 4.93/4.92 cnf(643,plain, % 4.93/4.92 (~P1(a3)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[608,37])). % 4.93/4.92 cnf(644,plain, % 4.93/4.92 (~P5(a4)+~P4(a2)), % 4.93/4.92 inference(scs_inference,[],[609,641])). % 4.93/4.92 cnf(649,plain, % 4.93/4.92 (~P3(a3)+~P1(a2)), % 4.93/4.92 inference(scs_inference,[],[615,37])). % 4.93/4.92 cnf(658,plain, % 4.93/4.92 (P4(a1)+P2(a2)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[633,89])). % 4.93/4.92 cnf(663,plain, % 4.93/4.92 (~P4(a3)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[643,31])). % 4.93/4.92 cnf(664,plain, % 4.93/4.92 (~P4(a2)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[644,16])). % 4.93/4.92 cnf(666,plain, % 4.93/4.92 (~P1(a2)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[649,608])). % 4.93/4.92 cnf(669,plain, % 4.93/4.92 (~P5(a4)+~P2(a2)+P4(a4)), % 4.93/4.92 inference(scs_inference,[],[663,527])). % 4.93/4.92 cnf(670,plain, % 4.93/4.92 (~P3(a3)+~P3(a1)+~P4(a4)), % 4.93/4.92 inference(scs_inference,[],[664,294])). % 4.93/4.92 cnf(671,plain, % 4.93/4.92 (P3(a2)+P5(a2)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[666,34])). % 4.93/4.92 cnf(682,plain, % 4.93/4.92 (~P5(a4)+P2(a2)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[658,593])). % 4.93/4.92 cnf(691,plain, % 4.93/4.92 (~P4(a4)+~P3(a1)+P2(a4)), % 4.93/4.92 inference(scs_inference,[],[670,518])). % 4.93/4.92 cnf(692,plain, % 4.93/4.92 (P5(a2)+~P5(a4)+P5(a3)), % 4.93/4.92 inference(scs_inference,[],[671,14])). % 4.93/4.92 cnf(701,plain, % 4.93/4.92 (P2(a2)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[682,16])). % 4.93/4.92 cnf(712,plain, % 4.93/4.92 (P2(a4)+~P3(a1)), % 4.93/4.92 inference(scs_inference,[],[691,76])). % 4.93/4.92 cnf(713,plain, % 4.93/4.92 (~P3(a1)+P1(a3)), % 4.93/4.92 inference(scs_inference,[],[712,6])). % 4.93/4.92 cnf(714,plain, % 4.93/4.92 (P1(a3)+P4(a2)+~P1(a4)), % 4.93/4.92 inference(scs_inference,[],[713,22])). % 4.93/4.92 cnf(715,plain, % 4.93/4.92 (P5(a2)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[692,612])). % 4.93/4.92 cnf(716,plain, % 4.93/4.92 (~P5(a4)+P4(a3)+P4(a4)), % 4.93/4.92 inference(scs_inference,[],[715,23])). % 4.93/4.92 cnf(733,plain, % 4.93/4.92 (~P1(a4)+P5(a5)+P4(a2)), % 4.93/4.92 inference(scs_inference,[],[714,540])). % 4.93/4.92 cnf(734,plain, % 4.93/4.92 (P4(a4)+P4(a3)+P1(a1)), % 4.93/4.92 inference(scs_inference,[],[716,153])). % 4.93/4.92 cnf(742,plain, % 4.93/4.92 (P4(a2)+~P1(a2)+P5(a5)), % 4.93/4.92 inference(scs_inference,[],[733,544])). % 4.93/4.92 cnf(743,plain, % 4.93/4.92 (P4(a3)+P1(a1)+P4(a2)), % 4.93/4.92 inference(scs_inference,[],[734,139])). % 4.93/4.92 cnf(750,plain, % 4.93/4.92 (~P1(a2)+P5(a5)+P4(a4)), % 4.93/4.92 inference(scs_inference,[],[742,510])). % 4.93/4.92 cnf(751,plain, % 4.93/4.92 (P1(a1)+~P1(a4)+P4(a2)), % 4.93/4.92 inference(scs_inference,[],[743,504])). % 4.93/4.92 cnf(758,plain, % 4.93/4.92 (P4(a4)+P5(a5)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[750,591])). % 4.93/4.92 cnf(759,plain, % 4.93/4.92 (P4(a2)+P2(a3)+~P1(a4)), % 4.93/4.92 inference(scs_inference,[],[751,88])). % 4.93/4.92 cnf(766,plain, % 4.93/4.92 (~P3(a3)+P5(a5)+P4(a2)), % 4.93/4.92 inference(scs_inference,[],[758,546])). % 4.93/4.92 cnf(767,plain, % 4.93/4.92 (~P1(a4)+P4(a2)), % 4.93/4.92 inference(scs_inference,[],[759,70])). % 4.93/4.92 cnf(783,plain, % 4.93/4.92 (P5(a5)+P4(a2)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[766,608])). % 4.93/4.92 cnf(786,plain, % 4.93/4.92 (P4(a2)+P2(a2)+~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[783,89])). % 4.93/4.92 cnf(795,plain, % 4.93/4.92 (P2(a2)+~P5(a4)+P1(a4)), % 4.93/4.92 inference(scs_inference,[],[786,7])). % 4.93/4.92 cnf(797,plain, % 4.93/4.92 (P1(a4)+~P5(a4)+P4(a4)), % 4.93/4.92 inference(scs_inference,[],[795,669])). % 4.93/4.92 cnf(799,plain, % 4.93/4.92 (~P5(a4)+P4(a4)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[797,445])). % 4.93/4.92 cnf(800,plain, % 4.93/4.92 (P4(a4)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[799,16])). % 4.93/4.92 cnf(876,plain, % 4.93/4.92 (~P4(a4)+~P2(a2)), % 4.93/4.92 inference(scs_inference,[],[31,69])). % 4.93/4.92 cnf(877,plain, % 4.93/4.92 (~P2(a2)+~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[876,800])). % 4.93/4.92 cnf(878,plain, % 4.93/4.92 (~P3(a3)), % 4.93/4.92 inference(scs_inference,[],[877,701])). % 4.93/4.92 cnf(883,plain, % 4.93/4.92 (~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[878,608])). % 4.93/4.92 cnf(885,plain, % 4.93/4.92 (P4(a3)+P2(a3)), % 4.93/4.92 inference(scs_inference,[],[878,33])). % 4.93/4.92 cnf(905,plain, % 4.93/4.92 (~P2(a4)+P5(a2)), % 4.93/4.92 inference(scs_inference,[],[883,415])). % 4.93/4.92 cnf(907,plain, % 4.93/4.92 (~P5(a4)), % 4.93/4.92 inference(scs_inference,[],[883,441])). % 4.93/4.92 cnf(908,plain, % 4.93/4.92 (P1(a3)+P5(a3)), % 4.93/4.92 inference(scs_inference,[],[883,446])). % 4.93/4.92 cnf(910,plain, % 4.93/4.92 (P3(a2)+~P5(a3)), % 4.93/4.92 inference(scs_inference,[],[883,463])). % 4.93/4.92 cnf(912,plain, % 4.93/4.92 (~P4(a3)), % 4.93/4.92 inference(scs_inference,[],[883,470])). % 4.93/4.92 cnf(920,plain, % 4.93/4.92 (~P5(a2)+P4(a4)), % 4.93/4.92 inference(scs_inference,[],[912,23])). % 4.93/4.92 cnf(934,plain, % 4.93/4.92 (P2(a3)), % 4.93/4.92 inference(scs_inference,[],[912,885])). % 4.93/4.92 cnf(938,plain, % 4.93/4.92 (~P4(a1)+~P1(a5)+~P5(a3)+~P2(a5)+~P3(a2)+~P3(a4)), % 4.93/4.92 inference(scs_inference,[],[934,43])). % 4.93/4.92 cnf(941,plain, % 4.93/4.92 (~P5(a1)+P4(a1)), % 4.93/4.92 inference(scs_inference,[],[934,157])). % 4.93/4.92 cnf(942,plain, % 4.93/4.92 (~P5(a1)+P1(a5)), % 4.93/4.92 inference(scs_inference,[],[934,158])). % 4.93/4.92 cnf(943,plain, % 4.93/4.92 (~P5(a1)+~P2(a1)), % 4.93/4.92 inference(scs_inference,[],[934,160])). % 4.93/4.92 cnf(970,plain, % 4.93/4.92 (~P2(a2)+~P5(a3)), % 4.93/4.92 inference(scs_inference,[],[910,39])). % 4.93/4.92 cnf(975,plain, % 4.93/4.92 (P4(a4)+~P2(a4)), % 4.93/4.92 inference(scs_inference,[],[920,905])). % 4.93/4.92 cnf(994,plain, % 4.93/4.92 (~P5(a3)+~P5(a5)+P2(a4)), % 4.93/4.92 inference(scs_inference,[],[970,28])). % 4.93/4.92 cnf(998,plain, % 4.93/4.92 (~P2(a4)), % 4.93/4.92 inference(scs_inference,[],[883,975,32])). % 4.93/4.92 cnf(999,plain, % 4.93/4.92 (P2(a1)+~P1(a3)), % 4.93/4.92 inference(scs_inference,[],[998,25])). % 4.93/4.92 cnf(1004,plain, % 4.93/4.92 (P4(a4)+P5(a1)), % 4.93/4.92 inference(scs_inference,[],[998,350])). % 4.93/4.92 cnf(1033,plain, % 4.93/4.92 (~P5(a3)+~P5(a5)), % 4.93/4.92 inference(scs_inference,[],[998,994])). % 4.93/4.92 cnf(1046,plain, % 4.93/4.92 (~P1(a3)+~P5(a1)), % 4.93/4.92 inference(scs_inference,[],[999,943])). % 4.93/4.92 cnf(1049,plain, % 4.93/4.92 (P5(a1)), % 4.93/4.92 inference(scs_inference,[],[907,1004,32])). % 4.93/4.92 cnf(1056,plain, % 4.93/4.92 (P4(a1)), % 4.93/4.92 inference(scs_inference,[],[1049,941])). % 4.93/4.92 cnf(1057,plain, % 4.93/4.92 (P1(a5)), % 4.93/4.92 inference(scs_inference,[],[1049,942])). % 4.93/4.92 cnf(1058,plain, % 4.93/4.92 (~P2(a1)), % 4.93/4.92 inference(scs_inference,[],[1049,943])). % 4.93/4.92 cnf(1062,plain, % 4.93/4.92 (~P1(a3)), % 4.93/4.92 inference(scs_inference,[],[1049,1046])). % 4.93/4.92 cnf(1065,plain, % 4.93/4.92 (~P1(a2)), % 4.93/4.92 inference(scs_inference,[],[1058,1056,77])). % 4.93/4.92 cnf(1093,plain, % 4.93/4.92 (~P4(a2)), % 4.93/4.92 inference(scs_inference,[],[1058,641])). % 4.93/4.92 cnf(1108,plain, % 4.93/4.92 (P5(a3)), % 4.93/4.92 inference(scs_inference,[],[1062,908])). % 4.93/4.92 cnf(1111,plain, % 4.93/4.92 (~P5(a3)+~P2(a5)+~P3(a2)+~P3(a4)), % 4.93/4.92 inference(scs_inference,[],[1056,1057,938])). % 4.93/4.92 cnf(1134,plain, % 4.93/4.92 (P3(a2)), % 4.93/4.92 inference(scs_inference,[],[1065,1108,184])). % 4.93/4.92 cnf(1166,plain, % 4.93/4.92 (~P1(a4)), % 4.93/4.92 inference(scs_inference,[],[1093,767])). % 4.93/4.92 cnf(1186,plain, % 4.93/4.92 (~P2(a2)), % 4.93/4.92 inference(scs_inference,[],[1108,970])). % 4.93/4.92 cnf(1192,plain, % 4.93/4.92 (~P5(a5)), % 4.93/4.92 inference(scs_inference,[],[1108,1033])). % 4.93/4.92 cnf(1193,plain, % 4.93/4.92 (~P3(a2)+~P3(a4)+~P2(a5)), % 4.93/4.92 inference(scs_inference,[],[1108,1111])). % 4.93/4.92 cnf(1208,plain, % 4.93/4.92 (P3(a4)), % 4.93/4.92 inference(scs_inference,[],[1186,1166,263])). % 4.93/4.92 cnf(1231,plain, % 4.93/4.92 (P2(a5)), % 4.93/4.92 inference(scs_inference,[],[1192,624])). % 4.93/4.92 cnf(1384,plain, % 4.93/4.92 ($false), % 4.93/4.92 inference(scs_inference,[],[1134,1208,1231,1193]), % 4.93/4.92 ['proof']). % 4.93/4.92 % SZS output end Proof % 4.93/4.92 % Total time :4.190000s %------------------------------------------------------------------------------