%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP129-1.003 : TPTP v8.2.0. Released v1.2.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 06:38:55 EDT 2024 % Result : Unsatisfiable 64.88s 65.76s % Output : CNFRefutation 65.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP129-1.003 : TPTP v8.2.0. Released v1.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n022.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 : Thu Jun 20 12:13:38 EDT 2024 % 0.11/0.33 % CPUTime : % 0.52/0.58 start to proof:theBenchmark % 64.88/65.75 %------------------------------------------- % 64.88/65.75 % File :CSE---1.7 % 64.88/65.75 % Problem :theBenchmark % 64.88/65.75 % Transform :cnf % 64.88/65.75 % Format :tptp:raw % 64.88/65.75 % Command :java -jar mcs_scs.jar %d %s % 64.88/65.75 % 64.88/65.75 % Result :Theorem 64.300000s % 64.88/65.75 % Output :CNFRefutation 64.300000s % 64.88/65.75 %------------------------------------------- % 64.88/65.76 %-------------------------------------------------------------------------- % 64.88/65.76 % File : GRP129-1.003 : TPTP v8.2.0. Released v1.2.0. % 64.88/65.76 % Domain : Group Theory (Quasigroups) % 64.88/65.76 % Problem : a.(b.a) = (b.a).b % 64.88/65.76 % Version : [Sla93] axioms. % 64.88/65.76 % English : Generate the multiplication table for the specified quasi- % 64.88/65.76 % group with 3 elements. % 64.88/65.76 % 64.88/65.76 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 64.88/65.76 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 64.88/65.76 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 64.88/65.76 % Source : [Sla93] % 64.88/65.76 % Names : QG7 [Sla93] % 64.88/65.76 % : QG7 [FSB93] % 64.88/65.76 % : QG7 [SFS95] % 64.88/65.76 % : Bennett QG7 [TPTP] % 64.88/65.76 % 64.88/65.76 % Status : Unsatisfiable % 64.88/65.76 % Rating : 0.00 v2.1.0 % 64.88/65.76 % Syntax : Number of clauses : 14 ( 9 unt; 1 nHn; 14 RR) % 64.88/65.76 % Number of literals : 26 ( 0 equ; 16 neg) % 64.88/65.76 % Maximal clause size : 5 ( 1 avg) % 64.88/65.76 % Maximal term depth : 1 ( 1 avg) % 64.88/65.76 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 64.88/65.76 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 64.88/65.76 % Number of variables : 18 ( 0 sgn) % 64.88/65.76 % SPC : CNF_UNS_EPR_NEQ_NHN % 64.88/65.76 % 64.88/65.76 % Comments : [SFS93]'s axiomatization has been modified for this. % 64.88/65.76 % : Substitution axioms are not needed, as any positive equality % 64.88/65.76 % literals should resolve on negative ones directly. % 64.88/65.76 % : tptp2X: -f tptp -s3 GRP129-1.g % 64.88/65.76 %-------------------------------------------------------------------------- % 64.88/65.76 cnf(element_1,axiom, % 64.88/65.76 group_element(e_1) ). % 64.88/65.76 % 64.88/65.76 cnf(element_2,axiom, % 64.88/65.76 group_element(e_2) ). % 64.88/65.76 % 64.88/65.76 cnf(element_3,axiom, % 64.88/65.76 group_element(e_3) ). % 64.88/65.76 % 64.88/65.76 cnf(e_1_is_not_e_2,axiom, % 64.88/65.76 ~ equalish(e_1,e_2) ). % 64.88/65.76 % 64.88/65.76 cnf(e_1_is_not_e_3,axiom, % 64.88/65.76 ~ equalish(e_1,e_3) ). % 64.88/65.76 % 64.88/65.76 cnf(e_2_is_not_e_1,axiom, % 64.88/65.76 ~ equalish(e_2,e_1) ). % 64.88/65.76 % 64.88/65.76 cnf(e_2_is_not_e_3,axiom, % 64.88/65.76 ~ equalish(e_2,e_3) ). % 64.88/65.76 % 64.88/65.76 cnf(e_3_is_not_e_1,axiom, % 64.88/65.76 ~ equalish(e_3,e_1) ). % 64.88/65.76 % 64.88/65.76 cnf(e_3_is_not_e_2,axiom, % 64.88/65.76 ~ equalish(e_3,e_2) ). % 64.88/65.76 % 64.88/65.76 cnf(product_total_function1,axiom, % 64.88/65.76 ( ~ group_element(X) % 64.88/65.76 | ~ group_element(Y) % 64.88/65.76 | product(X,Y,e_1) % 64.88/65.76 | product(X,Y,e_2) % 64.88/65.76 | product(X,Y,e_3) ) ). % 64.88/65.76 % 64.88/65.76 cnf(product_total_function2,axiom, % 64.88/65.76 ( ~ product(X,Y,W) % 64.88/65.76 | ~ product(X,Y,Z) % 64.88/65.76 | equalish(W,Z) ) ). % 64.88/65.76 % 64.88/65.76 cnf(product_right_cancellation,axiom, % 64.88/65.76 ( ~ product(X,W,Y) % 64.88/65.76 | ~ product(X,Z,Y) % 64.88/65.76 | equalish(W,Z) ) ). % 64.88/65.76 % 64.88/65.76 cnf(product_left_cancellation,axiom, % 64.88/65.76 ( ~ product(W,Y,X) % 64.88/65.76 | ~ product(Z,Y,X) % 64.88/65.76 | equalish(W,Z) ) ). % 64.88/65.76 % 64.88/65.76 cnf(qg3,negated_conjecture, % 64.88/65.76 ( ~ product(Y,X,Z1) % 64.88/65.76 | ~ product(X,Z1,Z2) % 64.88/65.76 | product(Z1,Y,Z2) ) ). % 64.88/65.76 % 64.88/65.76 %-------------------------------------------------------------------------- % 64.88/65.76 %------------------------------------------- % 64.88/65.76 % Proof found % 64.88/65.76 % SZS status Theorem for theBenchmark % 64.88/65.76 % SZS output start Proof % 64.88/65.77 %ClaNum:14(EqnAxiom:0) % 64.88/65.77 %VarNum:41(SingletonVarNum:18) % 64.88/65.77 %MaxLitNum:5 % 64.88/65.77 %MaxfuncDepth:0 % 64.88/65.77 %SharedTerms:12 % 64.88/65.77 %goalClause: 14 % 64.88/65.77 [1]P1(a1) % 64.88/65.77 [2]P1(a2) % 64.88/65.77 [3]P1(a3) % 64.88/65.77 [4]~P2(a1,a2) % 64.88/65.77 [5]~P2(a1,a3) % 64.88/65.77 [6]~P2(a2,a1) % 64.88/65.77 [7]~P2(a2,a3) % 64.88/65.77 [8]~P2(a3,a1) % 64.88/65.77 [9]~P2(a3,a2) % 64.88/65.77 [11]~P3(x113,x114,x111)+P2(x111,x112)+~P3(x113,x114,x112) % 64.88/65.77 [12]~P3(x123,x121,x124)+P2(x121,x122)+~P3(x123,x122,x124) % 64.88/65.77 [13]~P3(x131,x133,x134)+P2(x131,x132)+~P3(x132,x133,x134) % 64.88/65.77 [14]~P3(x142,x144,x141)+P3(x141,x142,x143)+~P3(x144,x141,x143) % 64.88/65.77 [10]~P1(x102)+~P1(x101)+P3(x101,x102,a2)+P3(x101,x102,a3)+P3(x101,x102,a1) % 64.88/65.77 %EqnAxiom % 64.88/65.77 % 64.88/65.77 %------------------------------------------- % 64.88/65.79 cnf(16,plain, % 64.88/65.79 (~P3(x161,x162,x163)+~P3(x162,a1,x163)+~P3(a3,x161,x162)), % 64.88/65.79 inference(scs_inference,[],[5,12,14])). % 64.88/65.79 cnf(17,plain, % 64.88/65.79 (~P3(x171,a2,x172)+~P3(a1,x173,x172)+~P3(x173,x171,a2)), % 64.88/65.79 inference(scs_inference,[],[4,13,14])). % 64.88/65.79 cnf(19,plain, % 64.88/65.79 (~P3(x191,x192,a1)+~P3(x192,x193,a2)+~P3(x193,x191,x192)), % 64.88/65.79 inference(scs_inference,[],[6,11,14])). % 64.88/65.79 cnf(20,plain, % 64.88/65.79 (~P3(x201,x202,a3)+~P3(x203,x201,a2)+~P3(x202,x203,x201)), % 64.88/65.79 inference(scs_inference,[],[7,11,14])). % 64.88/65.79 cnf(37,plain, % 64.88/65.79 (~P3(x371,a3,x372)+~P3(x373,x371,x372)+~P3(a1,x373,x371)), % 64.88/65.79 inference(scs_inference,[],[5,12,14])). % 64.88/65.79 cnf(38,plain, % 64.88/65.79 (~P3(x381,x382,x383)+~P3(x382,a2,x383)+~P3(a3,x381,x382)), % 64.88/65.79 inference(scs_inference,[],[7,12,14])). % 64.88/65.79 cnf(39,plain, % 64.88/65.79 (~P3(a2,a2,a1)+P3(a2,a3,a2)+P3(a2,a3,a3)), % 64.88/65.79 inference(scs_inference,[],[9,3,2,12,10])). % 64.88/65.79 cnf(41,plain, % 64.88/65.79 (~P3(x411,a2,x412)+~P3(x413,x411,x412)+~P3(a1,x413,x411)), % 64.88/65.79 inference(scs_inference,[],[4,12,14])). % 64.88/65.79 cnf(45,plain, % 64.88/65.79 (~P3(x451,a1,x452)+~P3(x453,x451,x452)+~P3(a2,x453,x451)), % 64.88/65.79 inference(scs_inference,[],[6,12,14])). % 64.88/65.79 cnf(48,plain, % 64.88/65.79 (~P3(a2,a1,a1)+P3(a2,a3,a2)+P3(a2,a3,a3)), % 64.88/65.79 inference(scs_inference,[],[8,3,2,12,10])). % 64.88/65.79 cnf(53,plain, % 64.88/65.79 (~P3(x531,a3,x532)+~P3(x533,x531,x532)+~P3(a2,x533,x531)), % 64.88/65.79 inference(scs_inference,[],[7,12,14])). % 64.88/65.79 cnf(57,plain, % 64.88/65.79 (~P3(a2,a1,a3)+P3(a2,a3,a2)+P3(a2,a3,a1)), % 64.88/65.79 inference(scs_inference,[],[5,3,2,12,10])). % 64.88/65.79 cnf(63,plain, % 64.88/65.79 (~P3(a3,a3,a1)+P3(a3,a1,a2)+P3(a3,a1,a3)), % 64.88/65.79 inference(scs_inference,[],[8,1,3,12,10])). % 64.88/65.79 cnf(67,plain, % 64.88/65.79 (~P3(a2,a2,a3)+P3(a2,a3,a2)+P3(a2,a3,a1)), % 64.88/65.79 inference(scs_inference,[],[7,3,2,12,10])). % 64.88/65.79 cnf(68,plain, % 64.88/65.79 (~P3(a1,a2,a1)+P3(a1,a3,a2)+P3(a1,a3,a3)), % 64.88/65.79 inference(scs_inference,[],[9,3,1,12,10])). % 64.88/65.79 cnf(77,plain, % 64.88/65.79 (~P3(a2,a3,a1)+P3(a2,a2,a2)+P3(a2,a2,a3)), % 64.88/65.79 inference(scs_inference,[],[9,2,12,10])). % 64.88/65.79 cnf(78,plain, % 64.88/65.79 (~P3(a2,a3,a1)+P3(a2,a2,a2)+~P3(a3,a2,a2)), % 64.88/65.79 inference(scs_inference,[],[77,38])). % 64.88/65.79 cnf(79,plain, % 64.88/65.79 (~P3(a2,a3,a1)+~P3(a3,a2,a2)), % 64.88/65.79 inference(scs_inference,[],[78,38])). % 64.88/65.79 cnf(84,plain, % 64.88/65.79 (~P3(a2,a1,a3)+P3(a2,a3,a2)+~P3(a3,a2,a2)), % 64.88/65.79 inference(scs_inference,[],[79,57])). % 64.88/65.79 cnf(85,plain, % 64.88/65.79 (~P3(a3,a2,a2)+~P3(a2,a1,a3)), % 64.88/65.79 inference(scs_inference,[],[84,53])). % 64.88/65.79 cnf(94,plain, % 64.88/65.79 (~P3(x941,a3,a2)+~P3(a2,x941,a3)+~P3(a2,a1,a3)), % 64.88/65.79 inference(scs_inference,[],[85,14])). % 64.88/65.79 cnf(95,plain, % 64.88/65.79 (~P3(x951,a2,a3)+~P3(a1,x951,a2)+~P3(a1,a3,a2)), % 64.88/65.79 inference(scs_inference,[],[94,14])). % 64.88/65.79 cnf(19008,plain, % 64.88/65.79 (~P3(x190081,a2,x190082)+~P3(x190081,a1,x190082)), % 64.88/65.79 inference(scs_inference,[],[4,12])). % 64.88/65.79 cnf(19010,plain, % 64.88/65.79 (~P3(a2,x190101,x190102)+~P3(a1,x190101,x190102)), % 64.88/65.79 inference(scs_inference,[],[4,12,13])). % 64.88/65.79 cnf(19012,plain, % 64.88/65.79 (P3(a2,a2,a2)+P3(a2,a2,a3)+P3(a2,a2,a1)), % 64.88/65.79 inference(scs_inference,[],[2,10])). % 64.88/65.79 cnf(19013,plain, % 64.88/65.79 (P3(a2,a1,a2)+P3(a2,a1,a3)+~P3(a2,a2,a1)), % 64.88/65.79 inference(scs_inference,[],[1,2,19008,10])). % 64.88/65.79 cnf(19015,plain, % 64.88/65.79 (~P3(x190151,x190152,a1)+~P3(x190151,x190152,a3)), % 64.88/65.79 inference(scs_inference,[],[8,11])). % 64.88/65.79 cnf(19018,plain, % 64.88/65.79 (~P3(a2,x190181,x190182)+~P3(a3,x190181,x190182)), % 64.88/65.79 inference(scs_inference,[],[9,13])). % 64.88/65.79 cnf(19021,plain, % 64.88/65.79 (~P3(x190211,a3,x190212)+~P3(x190211,a2,x190212)), % 64.88/65.79 inference(scs_inference,[],[7,12])). % 64.88/65.79 cnf(19025,plain, % 64.88/65.79 (~P3(a1,x190251,x190252)+~P3(a3,x190251,x190252)), % 64.88/65.79 inference(scs_inference,[],[8,13])). % 64.88/65.79 cnf(19027,plain, % 64.88/65.79 (~P3(x190271,x190272,a2)+~P3(x190271,x190272,a3)), % 64.88/65.79 inference(scs_inference,[],[8,9,13,11])). % 64.88/65.79 cnf(19029,plain, % 64.88/65.79 (~P3(a1,a3,a2)+P3(a3,a3,a1)+P3(a3,a3,a3)), % 64.88/65.79 inference(scs_inference,[],[3,8,9,13,10])). % 64.88/65.79 cnf(19031,plain, % 64.88/65.79 (~P3(x190311,a3,x190312)+~P3(x190311,a1,x190312)), % 64.88/65.79 inference(scs_inference,[],[5,12])). % 64.88/65.79 cnf(19034,plain, % 64.88/65.79 (P3(a3,a3,a1)+P3(a3,a3,a3)+P3(a3,a3,a2)), % 64.88/65.79 inference(scs_inference,[],[3,10])). % 64.88/65.80 cnf(19037,plain, % 64.88/65.80 (~P3(a3,a3,a1)+~P3(a2,a1,a2)+P3(a3,a1,a3)), % 64.88/65.80 inference(scs_inference,[],[19018,63])). % 64.88/65.80 cnf(19041,plain, % 64.88/65.80 (~P3(a2,a2,a1)+P3(a2,a1,a2)+~P3(a2,a3,a3)), % 64.88/65.80 inference(scs_inference,[],[19031,19013])). % 64.88/65.80 cnf(19043,plain, % 64.88/65.80 (P3(a2,a2,a1)+P3(a2,a2,a2)+~P3(a3,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19012,38])). % 64.88/65.80 cnf(19048,plain, % 64.88/65.80 (P3(a3,a3,a3)+P3(a3,a3,a2)+~P3(a1,a3,a3)), % 64.88/65.80 inference(scs_inference,[],[19034,37])). % 64.88/65.80 cnf(19050,plain, % 64.88/65.80 (P3(a1,a1,a1)+P3(a1,a1,a3)+P3(a1,a1,a2)), % 64.88/65.80 inference(scs_inference,[],[1,10])). % 64.88/65.80 cnf(19053,plain, % 64.88/65.80 (P3(a2,a2,a2)+~P3(a3,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19043,38])). % 64.88/65.80 cnf(19054,plain, % 64.88/65.80 (~P3(a3,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19053,38])). % 64.88/65.80 cnf(19055,plain, % 64.88/65.80 (P3(a3,a2,a1)+P3(a3,a2,a3)), % 64.88/65.80 inference(scs_inference,[],[2,19054,3,10])). % 64.88/65.80 cnf(19057,plain, % 64.88/65.80 (~P3(a3,a1,a1)+P3(a3,a2,a3)), % 64.88/65.80 inference(scs_inference,[],[2,19054,3,10,19008])). % 64.88/65.80 cnf(19063,plain, % 64.88/65.80 (~P3(x190631,a3,a2)+~P3(a2,x190631,a3)), % 64.88/65.80 inference(scs_inference,[],[19054,14])). % 64.88/65.80 cnf(19065,plain, % 64.88/65.80 (~P3(a3,a1,a1)+~P3(a2,a2,a3)), % 64.88/65.80 inference(scs_inference,[],[19057,19018])). % 64.88/65.80 cnf(19067,plain, % 64.88/65.80 (P3(a2,a2,a1)+P3(a2,a2,a2)+~P3(a2,a3,a2)), % 64.88/65.80 inference(scs_inference,[],[19063,19012])). % 64.88/65.80 cnf(19073,plain, % 64.88/65.80 (P3(a3,a3,a3)+~P3(a1,a3,a3)), % 64.88/65.80 inference(scs_inference,[],[19048,37])). % 64.88/65.80 cnf(19074,plain, % 64.88/65.80 (~P3(a1,a3,a3)+~P3(a3,a3,a1)), % 64.88/65.80 inference(scs_inference,[],[19073,19015])). % 64.88/65.80 cnf(19075,plain, % 64.88/65.80 (~P3(x190751,a1,a3)+~P3(a3,x190751,a1)+~P3(a3,a3,a1)), % 64.88/65.80 inference(scs_inference,[],[19074,14])). % 64.88/65.80 cnf(19076,plain, % 64.88/65.80 (P3(a1,a1,a1)+P3(a1,a1,a2)+~P3(a3,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19050,16])). % 64.88/65.80 cnf(19079,plain, % 64.88/65.80 (P3(a2,a2,a2)+~P3(a2,a3,a2)+~P3(a1,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19067,41])). % 64.88/65.80 cnf(19082,plain, % 64.88/65.80 (P3(a3,a3,a3)+P3(a3,a3,a2)+~P3(a3,a1,a3)), % 64.88/65.80 inference(scs_inference,[],[19075,19034])). % 64.88/65.80 cnf(19083,plain, % 64.88/65.80 (P3(a1,a1,a1)+~P3(a3,a1,a1)+~P3(a1,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19076,17])). % 64.88/65.80 cnf(19084,plain, % 64.88/65.80 (~P3(a2,a3,a2)+~P3(a1,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19079,19010])). % 64.88/65.80 cnf(19088,plain, % 64.88/65.80 (P3(a3,a3,a2)+~P3(a3,a1,a3)), % 64.88/65.80 inference(scs_inference,[],[19082,16])). % 64.88/65.80 cnf(19090,plain, % 64.88/65.80 (~P3(a1,a2,a2)+~P3(a3,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19083,19025])). % 64.88/65.80 cnf(19097,plain, % 64.88/65.80 (P3(a3,a2,a1)+~P3(a3,a1,a3)), % 64.88/65.80 inference(scs_inference,[],[19008,19055])). % 64.88/65.80 cnf(19106,plain, % 64.88/65.80 (P3(a2,a2,a2)+~P3(a2,a3,a2)+~P3(a2,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19008,19067])). % 64.88/65.80 cnf(19107,plain, % 64.88/65.80 (~P3(a2,a1,a1)+~P3(a2,a3,a2)), % 64.88/65.80 inference(scs_inference,[],[19106,19021])). % 64.88/65.80 cnf(19128,plain, % 64.88/65.80 (P3(a3,a1,a2)+P3(a3,a1,a1)+~P3(a3,a2,a3)), % 64.88/65.80 inference(scs_inference,[],[3,1,19008,10])). % 64.88/65.80 cnf(19129,plain, % 64.88/65.80 (P3(a3,a1,a2)+P3(a3,a2,a1)+P3(a3,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19054,3,2,19128,10])). % 64.88/65.80 cnf(19130,plain, % 64.88/65.80 (P3(a3,a1,a2)+~P3(a2,a2,a1)+P3(a3,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19129,19018])). % 64.88/65.80 cnf(19133,plain, % 64.88/65.80 (P3(a3,a1,a2)+P3(a3,a1,a3)+~P3(a3,a2,a1)), % 64.88/65.80 inference(scs_inference,[],[1,3,19008,10])). % 64.88/65.80 cnf(19134,plain, % 64.88/65.80 (P3(a3,a1,a2)+P3(a3,a1,a3)+P3(a3,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19133,19129])). % 64.88/65.80 cnf(19136,plain, % 64.88/65.80 (P3(a2,a1,a1)+P3(a2,a1,a2)+~P3(a2,a2,a3)), % 64.88/65.80 inference(scs_inference,[],[1,2,19008,10])). % 64.88/65.80 cnf(19141,plain, % 64.88/65.80 (~P3(a2,a2,a3)+P3(a2,a1,a1)+~P3(a1,a1,a2)), % 64.88/65.80 inference(scs_inference,[],[19010,19136])). % 64.88/65.80 cnf(19143,plain, % 64.88/65.80 (~P3(a1,a3,a3)+P3(a2,a3,a2)+P3(a2,a3,a1)), % 64.88/65.80 inference(scs_inference,[],[3,2,19010,10])). % 64.88/65.80 cnf(19153,plain, % 64.88/65.80 (P3(a1,a1,a1)+P3(a1,a1,a2)+~P3(a2,a1,a3)), % 64.88/65.80 inference(scs_inference,[],[19010,19050])). % 64.88/65.80 cnf(19161,plain, % 64.88/65.80 (~P3(a2,a2,a3)+P3(a2,a3,a2)+~P3(a1,a3,a1)), % 64.88/65.80 inference(scs_inference,[],[19010,67])). % 64.88/65.80 cnf(19162,plain, % 64.88/65.80 (~P3(a1,a3,a1)+~P3(a2,a2,a3)), % 64.88/65.80 inference(scs_inference,[],[19161,19063])). % 64.88/65.80 cnf(19163,plain, % 64.88/65.80 (P3(a2,a2,a1)+P3(a2,a2,a2)+~P3(a1,a3,a1)), % 64.88/65.80 inference(scs_inference,[],[19162,19012])). % 64.88/65.80 cnf(19164,plain, % 64.88/65.80 (P3(a2,a2,a2)+~P3(a1,a3,a1)+~P3(a1,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19163,41])). % 64.88/65.80 cnf(19165,plain, % 64.88/65.80 (~P3(a1,a3,a1)+~P3(a1,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19164,19010])). % 64.88/65.80 cnf(19169,plain, % 64.88/65.80 (P3(a1,a1,a2)+P3(a1,a1,a3)+~P3(a2,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19010,19050])). % 64.88/65.80 cnf(19170,plain, % 64.88/65.80 (P3(a1,a1,a2)+~P3(a2,a1,a1)), % 64.88/65.80 inference(scs_inference,[],[19169,45])). % 64.88/65.80 cnf(19173,plain, % 64.88/65.80 (P3(a2,a2,a3)+~P3(a2,a3,a1)+~P3(a1,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19010,77])). % 64.88/65.80 cnf(19174,plain, % 64.88/65.80 (~P3(a2,a3,a1)+~P3(a1,a2,a2)), % 64.88/65.80 inference(scs_inference,[],[19173,41])). % 65.00/65.80 cnf(19176,plain, % 65.00/65.80 (~P3(x191761,a1,a2)+~P3(a2,x191761,a1)+~P3(a2,a3,a1)), % 65.00/65.80 inference(scs_inference,[],[19174,14])). % 65.00/65.80 cnf(19186,plain, % 65.00/65.80 (P3(a2,a2,a3)+P3(a2,a2,a1)+~P3(a1,a2,a2)), % 65.00/65.80 inference(scs_inference,[],[19010,19012])). % 65.00/65.80 cnf(19187,plain, % 65.00/65.80 (P3(a2,a2,a1)+~P3(a1,a2,a2)), % 65.00/65.80 inference(scs_inference,[],[19186,41])). % 65.00/65.80 cnf(19188,plain, % 65.00/65.80 (~P3(x191881,a1,a2)+~P3(a2,x191881,a1)+P3(a2,a2,a1)), % 65.00/65.80 inference(scs_inference,[],[19187,14])). % 65.00/65.80 cnf(19189,plain, % 65.00/65.80 (~P3(a2,a2,a3)+P3(a2,a2,a1)+~P3(a1,a1,a2)), % 65.00/65.80 inference(scs_inference,[],[19188,19141])). % 65.00/65.80 cnf(19190,plain, % 65.00/65.80 (~P3(a1,a1,a2)+P3(a2,a2,a1)+P3(a2,a2,a2)), % 65.00/65.80 inference(scs_inference,[],[19189,19012])). % 65.00/65.80 cnf(19192,plain, % 65.00/65.80 (~P3(a2,a1,a1)+P3(a2,a2,a1)+P3(a2,a2,a2)), % 65.00/65.80 inference(scs_inference,[],[19190,19170])). % 65.00/65.80 cnf(19194,plain, % 65.00/65.80 (P3(a2,a2,a2)+~P3(a2,a1,a1)), % 65.00/65.80 inference(scs_inference,[],[19192,19008])). % 65.00/65.80 cnf(19195,plain, % 65.00/65.80 (~P3(a2,a2,a3)+P3(a2,a2,a2)+P3(a2,a1,a2)), % 65.00/65.80 inference(scs_inference,[],[19194,19136])). % 65.00/65.80 cnf(19196,plain, % 65.00/65.80 (P3(a2,a2,a2)+~P3(a2,a3,a1)+P3(a2,a1,a2)), % 65.00/65.80 inference(scs_inference,[],[19195,77])). % 65.00/65.80 cnf(19204,plain, % 65.00/65.80 (P3(a2,a2,a3)+P3(a2,a2,a2)+~P3(a1,a2,a1)), % 65.00/65.80 inference(scs_inference,[],[19010,19012])). % 65.00/65.80 cnf(19207,plain, % 65.00/65.80 (P3(a1,a3,a2)+P3(a1,a3,a3)+~P3(a2,a3,a1)), % 65.00/65.80 inference(scs_inference,[],[1,3,19010,10])). % 65.00/65.80 cnf(19208,plain, % 65.00/65.80 (~P3(a2,a2,a1)+P3(a2,a1,a2)+~P3(a1,a1,a3)), % 65.00/65.80 inference(scs_inference,[],[19010,19013])). % 65.00/65.80 cnf(19209,plain, % 65.00/65.80 (~P3(a1,a2,a2)+~P3(a1,a1,a3)+P3(a2,a1,a2)), % 65.00/65.80 inference(scs_inference,[],[19208,19187])). % 65.00/65.80 cnf(19210,plain, % 65.00/65.80 (~P3(a1,a2,a2)+~P3(a1,a1,a3)), % 65.00/65.80 inference(scs_inference,[],[19209,45])). % 65.00/65.80 cnf(19222,plain, % 65.00/65.80 (~P3(a2,a3,a3)+~P3(a2,a2,a1)+~P3(a1,a1,a2)), % 65.00/65.80 inference(scs_inference,[],[19010,19041])). % 65.00/65.80 cnf(19223,plain, % 65.00/65.80 (~P3(a2,a2,a1)+~P3(a1,a1,a2)+P3(a2,a3,a2)), % 65.00/65.80 inference(scs_inference,[],[19222,39])). % 65.00/65.80 cnf(19224,plain, % 65.00/65.80 (P3(a2,a2,a2)+~P3(a1,a1,a2)+P3(a2,a3,a2)), % 65.00/65.80 inference(scs_inference,[],[19223,19190])). % 65.00/65.80 cnf(19233,plain, % 65.00/65.80 (P3(a1,a2,a1)+P3(a1,a2,a2)+~P3(a2,a2,a3)), % 65.00/65.80 inference(scs_inference,[],[1,2,19010,10])). % 65.00/65.80 cnf(19234,plain, % 65.00/65.80 (P3(a1,a3,a1)+P3(a1,a3,a2)+~P3(a2,a3,a3)), % 65.00/65.80 inference(scs_inference,[],[3,1,19010,10])). % 65.00/65.80 cnf(19237,plain, % 65.00/65.80 (P3(a1,a2,a1)+P3(a1,a2,a3)+~P3(a2,a2,a2)), % 65.00/65.80 inference(scs_inference,[],[2,1,19010,10])). % 65.00/65.80 cnf(19261,plain, % 65.00/65.80 (~P3(a1,a1,a2)+P3(a2,a1,a1)+P3(a2,a1,a3)), % 65.00/65.80 inference(scs_inference,[],[1,2,19010,10])). % 65.00/65.80 cnf(19274,plain, % 65.00/65.80 (~P3(a1,a2,a2)+~P3(a3,a2,a1)), % 65.00/65.80 inference(scs_inference,[],[19018,19187])). % 65.00/65.80 cnf(19275,plain, % 65.00/65.80 (~P3(x192751,a1,a2)+~P3(a2,x192751,a1)+~P3(a3,a2,a1)), % 65.00/65.80 inference(scs_inference,[],[19274,14])). % 65.00/65.80 cnf(19276,plain, % 65.00/65.80 (P3(a3,a2,a3)+~P3(a2,x192761,a1)+~P3(x192761,a1,a2)), % 65.00/65.80 inference(scs_inference,[],[19054,3,2,19275,10])). % 65.00/65.80 cnf(19278,plain, % 65.00/65.80 (~P3(a2,a3,a3)+~P3(x192781,a1,a2)+~P3(a2,x192781,a1)), % 65.00/65.80 inference(scs_inference,[],[19276,38])). % 65.00/65.80 cnf(19279,plain, % 65.00/65.80 (~P3(a2,a3,a3)+~P3(a2,a1,a1)), % 65.00/65.80 inference(scs_inference,[],[19278,19170])). % 65.00/65.80 cnf(19280,plain, % 65.00/65.80 (~P3(a2,a3,a3)+~P3(a1,a1,a2)+P3(a2,a1,a3)), % 65.00/65.80 inference(scs_inference,[],[19279,19261])). % 65.00/65.80 cnf(19281,plain, % 65.00/65.80 (~P3(a1,a1,a2)+~P3(a2,a3,a3)), % 65.00/65.80 inference(scs_inference,[],[19280,19031])). % 65.00/65.80 cnf(19291,plain, % 65.00/65.80 (~P3(x192911,a2,x192912)+~P3(x192913,x192911,a2)+~P3(a3,x192913,x192912)), % 65.00/65.80 inference(scs_inference,[],[19018,14])). % 65.00/65.80 cnf(19343,plain, % 65.00/65.80 (~P3(a1,a3,a2)+P3(a3,a3,a3)+~P3(a2,a3,a1)), % 65.00/65.80 inference(scs_inference,[],[19018,19029])). % 65.00/65.80 cnf(19344,plain, % 65.00/65.81 (~P3(a2,a3,a1)+P3(a3,a3,a3)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19343,19207])). % 65.00/65.81 cnf(19346,plain, % 65.00/65.81 (~P3(a2,a3,a1)+P3(a3,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19344,19073])). % 65.00/65.81 cnf(19348,plain, % 65.00/65.81 (~P3(x193481,a2,a1)+~P3(a3,x193481,a2)+P3(a3,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19346,14])). % 65.00/65.81 cnf(19349,plain, % 65.00/65.81 (~P3(a3,a1,a3)+~P3(a3,x193491,a2)+~P3(x193491,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19348,16])). % 65.00/65.81 cnf(19350,plain, % 65.00/65.81 (~P3(a3,a1,a3)+~P3(a3,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19349,19097])). % 65.00/65.81 cnf(19351,plain, % 65.00/65.81 (~P3(a3,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19350,19088])). % 65.00/65.81 cnf(19352,plain, % 65.00/65.81 (~P3(a3,a3,a1)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19351,63])). % 65.00/65.81 cnf(19353,plain, % 65.00/65.81 (~P3(a2,a1,a2)+~P3(a3,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19351,19037])). % 65.00/65.81 cnf(19354,plain, % 65.00/65.81 (~P3(a3,a2,a1)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19351,19133])). % 65.00/65.81 cnf(19355,plain, % 65.00/65.81 (P3(a3,a1,a2)+P3(a3,a1,a1)), % 65.00/65.81 inference(scs_inference,[],[19351,19134])). % 65.00/65.81 cnf(19360,plain, % 65.00/65.81 (P3(a3,a3,a3)+P3(a3,a3,a2)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19352,19034])). % 65.00/65.81 cnf(19364,plain, % 65.00/65.81 (P3(a3,a2,a3)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19354,19055])). % 65.00/65.81 cnf(19365,plain, % 65.00/65.81 (P3(a3,a1,a1)+~P3(a1,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19355,19025])). % 65.00/65.81 cnf(19367,plain, % 65.00/65.81 (P3(a3,a1,a2)+~P3(a2,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19364,19018])). % 65.00/65.81 cnf(19368,plain, % 65.00/65.81 (~P3(a2,a1,a1)+P3(a3,a1,a1)), % 65.00/65.81 inference(scs_inference,[],[19365,19170])). % 65.00/65.81 cnf(19369,plain, % 65.00/65.81 (~P3(x193691,a2,a3)+~P3(a2,x193691,a2)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19367,14])). % 65.00/65.81 cnf(19371,plain, % 65.00/65.81 (~P3(a2,a2,a3)+P3(a3,a1,a1)+P3(a2,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19368,19136])). % 65.00/65.81 cnf(19373,plain, % 65.00/65.81 (P3(a3,a3,a2)+P3(a3,a1,a2)+~P3(a2,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19360,53])). % 65.00/65.81 cnf(19376,plain, % 65.00/65.81 (~P3(a2,x193761,a2)+~P3(a2,a3,a1)+~P3(x193761,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19369,19176])). % 65.00/65.81 cnf(19377,plain, % 65.00/65.81 (~P3(a2,a2,a3)+P3(a2,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19371,19065])). % 65.00/65.81 cnf(19379,plain, % 65.00/65.81 (P3(a3,a1,a2)+~P3(a2,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19373,19063])). % 65.00/65.81 cnf(19381,plain, % 65.00/65.81 (~P3(a2,a2,a1)+P3(a2,a3,a2)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19379,39])). % 65.00/65.81 cnf(19386,plain, % 65.00/65.81 (~P3(a1,a2,a2)+P3(a2,a3,a2)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19381,19187])). % 65.00/65.81 cnf(19389,plain, % 65.00/65.81 (~P3(a1,a2,a2)+P3(a3,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19386,19084])). % 65.00/65.81 cnf(19401,plain, % 65.00/65.81 (P3(a3,a1,a1)+~P3(a2,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19018,19355])). % 65.00/65.81 cnf(19408,plain, % 65.00/65.81 (P3(a3,a2,a3)+~P3(a2,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19018,19364])). % 65.00/65.81 cnf(19409,plain, % 65.00/65.81 (P3(a3,a2,a3)+~P3(a2,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19408,19377])). % 65.00/65.81 cnf(19410,plain, % 65.00/65.81 (P3(a3,a2,a3)+P3(a2,a2,a2)+~P3(a2,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19409,77])). % 65.00/65.81 cnf(19428,plain, % 65.00/65.81 (~P3(a1,a1,a2)+~P3(a2,a1,a1)), % 65.00/65.81 inference(scs_inference,[],[19018,19365])). % 65.00/65.81 cnf(19430,plain, % 65.00/65.81 (~P3(x194301,a2,a1)+~P3(a1,x194301,a2)+~P3(a1,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19428,14])). % 65.00/65.81 cnf(19432,plain, % 65.00/65.81 (P3(a1,a1,a3)+P3(a1,a1,a1)+~P3(a1,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19430,19050])). % 65.00/65.81 cnf(19433,plain, % 65.00/65.81 (P3(a1,a1,a3)+~P3(a1,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19432,19008])). % 65.00/65.81 cnf(19442,plain, % 65.00/65.81 (P3(a2,a2,a2)+P3(a2,a2,a1)+~P3(a3,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19018,19012])). % 65.00/65.81 cnf(19443,plain, % 65.00/65.81 (P3(a2,a2,a2)+P3(a2,a2,a1)+~P3(a2,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19442,19410])). % 65.00/65.81 cnf(19444,plain, % 65.00/65.81 (P3(a2,a2,a1)+~P3(a2,a3,a1)+~P3(a2,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19443,19376])). % 65.00/65.81 cnf(19445,plain, % 65.00/65.81 (~P3(a2,a2,a3)+~P3(a2,a3,a1)+~P3(a2,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19444,19176])). % 65.00/65.81 cnf(19446,plain, % 65.00/65.81 (~P3(a2,a2,a3)+P3(a2,a2,a2)+~P3(a2,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19445,19196])). % 65.00/65.81 cnf(19447,plain, % 65.00/65.81 (P3(a2,a2,a2)+~P3(a2,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19446,77])). % 65.00/65.81 cnf(19449,plain, % 65.00/65.81 (~P3(a2,a3,a1)+~P3(a2,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19447,20])). % 65.00/65.81 cnf(19451,plain, % 65.00/65.81 (~P3(a2,a2,a3)+~P3(x194511,a2,a1)+~P3(a3,x194511,a2)), % 65.00/65.81 inference(scs_inference,[],[19449,14])). % 65.00/65.81 cnf(19452,plain, % 65.00/65.81 (~P3(a2,a2,a3)+~P3(a1,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19451,19367])). % 65.00/65.81 cnf(19453,plain, % 65.00/65.81 (~P3(a1,a2,a1)+P3(a2,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19452,19204])). % 65.00/65.81 cnf(19454,plain, % 65.00/65.81 (~P3(a2,a2,a3)+P3(a2,a2,a2)+P3(a1,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19453,19233])). % 65.00/65.81 cnf(19455,plain, % 65.00/65.81 (P3(a2,a2,a2)+P3(a2,a2,a1)+P3(a1,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19454,19012])). % 65.00/65.81 cnf(19456,plain, % 65.00/65.81 (P3(a2,a2,a1)+P3(a1,a2,a2)+~P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19455,53])). % 65.00/65.81 cnf(19457,plain, % 65.00/65.81 (~P3(a2,a3,a2)+P3(a2,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19456,19084])). % 65.00/65.81 cnf(19459,plain, % 65.00/65.81 (~P3(a2,a1,a1)+P3(a2,a2,a1)+P3(a2,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19457,48])). % 65.00/65.81 cnf(19461,plain, % 65.00/65.81 (P3(a2,a3,a3)+~P3(a2,a1,a1)), % 65.00/65.81 inference(scs_inference,[],[19459,19008])). % 65.00/65.81 cnf(19462,plain, % 65.00/65.81 (~P3(a1,a1,a2)+P3(a2,a3,a3)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19461,19261])). % 65.00/65.81 cnf(19463,plain, % 65.00/65.81 (~P3(a1,a1,a2)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19462,19281])). % 65.00/65.81 cnf(19464,plain, % 65.00/65.81 (~P3(a2,a1,a1)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19463,19170])). % 65.00/65.81 cnf(19465,plain, % 65.00/65.81 (~P3(x194651,a2,a1)+~P3(a1,x194651,a2)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19464,14])). % 65.00/65.81 cnf(19466,plain, % 65.00/65.81 (~P3(a1,a3,a2)+~P3(a1,x194661,a2)+~P3(x194661,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19054,19465,14])). % 65.00/65.81 cnf(19467,plain, % 65.00/65.81 (~P3(a2,a3,a1)+P3(a1,a3,a3)+~P3(a3,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19466,19207])). % 65.00/65.81 cnf(19468,plain, % 65.00/65.81 (~P3(a2,a3,a1)+P3(a1,a3,a3)+P3(a3,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19054,2,3,19467,10])). % 65.00/65.81 cnf(19469,plain, % 65.00/65.81 (~P3(a1,a3,a2)+~P3(a2,a3,a1)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19468,95])). % 65.00/65.81 cnf(19471,plain, % 65.00/65.81 (~P3(a2,a3,a1)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19469,19207])). % 65.00/65.81 cnf(19473,plain, % 65.00/65.81 (~P3(a2,a1,a3)+P3(a1,a3,a3)+P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19471,57])). % 65.00/65.81 cnf(19474,plain, % 65.00/65.81 (~P3(a1,a1,a2)+P3(a2,a3,a2)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19473,19463])). % 65.00/65.81 cnf(19475,plain, % 65.00/65.81 (~P3(a2,a1,a1)+P3(a1,a3,a3)+P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19474,19170])). % 65.00/65.81 cnf(19476,plain, % 65.00/65.81 (~P3(a2,a1,a1)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19475,19107])). % 65.00/65.81 cnf(19477,plain, % 65.00/65.81 (~P3(x194771,a2,a1)+~P3(a1,x194771,a2)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19476,14])). % 65.00/65.81 cnf(19478,plain, % 65.00/65.81 (~P3(a3,a3,x194781)+~P3(a1,x194782,a2)+~P3(x194782,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19477,37])). % 65.00/65.81 cnf(19479,plain, % 65.00/65.81 (P3(a3,a2,a3)+~P3(a3,a3,x194791)+~P3(a1,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19054,2,3,19478,10])). % 65.00/65.81 cnf(19481,plain, % 65.00/65.81 (~P3(a1,a3,a2)+~P3(a3,a3,x194811)), % 65.00/65.81 inference(scs_inference,[],[19479,95])). % 65.00/65.81 cnf(19483,plain, % 65.00/65.81 (~P3(a2,a2,a3)+~P3(a2,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19018,19367])). % 65.00/65.81 cnf(19484,plain, % 65.00/65.81 (~P3(a2,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19483,19377])). % 65.00/65.81 cnf(19485,plain, % 65.00/65.81 (P3(a2,a2,a2)+P3(a2,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19484,19012])). % 65.00/65.81 cnf(19486,plain, % 65.00/65.81 (~P3(x194861,a2,a3)+~P3(a2,x194861,a2)), % 65.00/65.81 inference(scs_inference,[],[19484,14])). % 65.00/65.81 cnf(19491,plain, % 65.00/65.81 (P3(a3,a2,a1)+~P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19486,19055])). % 65.00/65.81 cnf(19493,plain, % 65.00/65.81 (P3(a3,a2,a1)+~P3(a2,a2,a1)+P3(a2,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19491,39])). % 65.00/65.81 cnf(19495,plain, % 65.00/65.81 (~P3(a2,a2,a1)+P3(a2,a3,a3)+~P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19493,19291])). % 65.00/65.81 cnf(19497,plain, % 65.00/65.81 (~P3(a2,a3,a2)+P3(a2,a3,a3)+P3(a2,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[2,19484,19495,10])). % 65.00/65.81 cnf(19501,plain, % 65.00/65.81 (~P3(a1,a1,a2)+P3(a2,a2,a2)+P3(a2,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19497,19224])). % 65.00/65.81 cnf(19502,plain, % 65.00/65.81 (~P3(a1,a1,a2)+P3(a2,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19501,19281])). % 65.00/65.81 cnf(19503,plain, % 65.00/65.81 (~P3(x195031,a1,a2)+~P3(a1,x195031,a1)+P3(a2,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19502,14])). % 65.00/65.81 cnf(19504,plain, % 65.00/65.81 (~P3(a2,a2,a1)+~P3(a1,x195041,a1)+~P3(x195041,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19503,19])). % 65.00/65.81 cnf(19505,plain, % 65.00/65.81 (~P3(a2,a2,a1)+P3(a3,a1,a1)+~P3(a1,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19504,19130])). % 65.00/65.81 cnf(19506,plain, % 65.00/65.81 (~P3(a1,a3,a1)+P3(a3,a1,a1)+P3(a2,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[2,19484,19505,10])). % 65.00/65.81 cnf(19507,plain, % 65.00/65.81 (P3(a2,a2,a2)+~P3(a1,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19506,37])). % 65.00/65.81 cnf(19509,plain, % 65.00/65.81 (~P3(a2,a3,a3)+P3(a2,a2,a2)+P3(a1,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19507,19234])). % 65.00/65.81 cnf(19511,plain, % 65.00/65.81 (~P3(a2,a3,a2)+P3(a2,a2,a2)+P3(a1,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19509,19497])). % 65.00/65.81 cnf(19512,plain, % 65.00/65.81 (P3(a1,a3,a2)+~P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19511,19021])). % 65.00/65.81 cnf(19513,plain, % 65.00/65.81 (~P3(a2,a2,a1)+P3(a1,a3,a2)+P3(a2,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19512,39])). % 65.00/65.81 cnf(19514,plain, % 65.00/65.81 (P3(a1,a3,a2)+P3(a2,a3,a3)+P3(a2,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[2,19484,19513,10])). % 65.00/65.81 cnf(19516,plain, % 65.00/65.81 (P3(a1,a3,a2)+P3(a2,a3,a3)+~P3(a1,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19514,17])). % 65.00/65.81 cnf(19518,plain, % 65.00/65.81 (P3(a2,a3,a3)+~P3(a1,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19516,19021])). % 65.00/65.81 cnf(19525,plain, % 65.00/65.81 (~P3(a2,a1,a1)), % 65.00/65.81 inference(scs_inference,[],[19018,19368])). % 65.00/65.81 cnf(19526,plain, % 65.00/65.81 (~P3(x195261,a2,a1)+~P3(a1,x195261,a2)), % 65.00/65.81 inference(scs_inference,[],[19525,14])). % 65.00/65.81 cnf(19528,plain, % 65.00/65.81 (~P3(a3,a2,a1)+P3(a1,a3,a3)+P3(a1,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19525,3,1,14,10])). % 65.00/65.81 cnf(19529,plain, % 65.00/65.81 (P3(a2,a1,a2)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19525,2,1,10])). % 65.00/65.81 cnf(19533,plain, % 65.00/65.81 (P3(a2,a1,a3)+~P3(a1,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19525,2,1,10,19027,19486])). % 65.00/65.81 cnf(19535,plain, % 65.00/65.81 (~P3(a3,a3,a1)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19525,2,1,10,19027,19486,19353])). % 65.00/65.81 cnf(19537,plain, % 65.00/65.81 (P3(a2,a1,a3)+~P3(a2,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19525,2,1,10,19027,19486,19353,19408,19008])). % 65.00/65.81 cnf(19540,plain, % 65.00/65.81 (~P3(a2,a1,a3)+P3(a1,a1,a1)+~P3(a1,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19526,19153])). % 65.00/65.81 cnf(19542,plain, % 65.00/65.81 (P3(a2,a1,a2)+~P3(a1,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19529,19010])). % 65.00/65.81 cnf(19544,plain, % 65.00/65.81 (~P3(a1,a3,a2)+P3(a3,a3,a3)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19535,19029])). % 65.00/65.81 cnf(19546,plain, % 65.00/65.81 (~P3(a2,a3,a1)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19537,19447])). % 65.00/65.81 cnf(19547,plain, % 65.00/65.81 (~P3(a1,a2,a1)+P3(a2,a1,a2)), % 65.00/65.81 inference(scs_inference,[],[19542,19433])). % 65.00/65.81 cnf(19549,plain, % 65.00/65.81 (~P3(a1,a3,a3)+P3(a2,a1,a3)+P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19546,19143])). % 65.00/65.81 cnf(19551,plain, % 65.00/65.81 (~P3(a2,a2,a2)+P3(a2,a1,a2)+P3(a1,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19547,19237])). % 65.00/65.81 cnf(19554,plain, % 65.00/65.81 (P3(a1,a3,a3)+P3(a1,a3,a1)+P3(a3,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19054,3,2,19528,10])). % 65.00/65.81 cnf(19555,plain, % 65.00/65.81 (~P3(a2,a1,a3)+~P3(a1,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19540,19008])). % 65.00/65.81 cnf(19562,plain, % 65.00/65.81 (~P3(a1,a3,a2)+P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19544,19481])). % 65.00/65.81 cnf(19563,plain, % 65.00/65.81 (~P3(a1,a2,a1)+P3(a2,a1,a3)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19562,68])). % 65.00/65.81 cnf(19564,plain, % 65.00/65.81 (~P3(a1,a2,a1)+P3(a2,a1,a3)+P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19549,19563])). % 65.00/65.81 cnf(19565,plain, % 65.00/65.81 (P3(a2,a1,a2)+P3(a1,a2,a3)+P3(a2,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[2,19484,19551,10])). % 65.00/65.81 cnf(19567,plain, % 65.00/65.81 (~P3(a2,a3,a3)+P3(a1,a3,a1)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19554,38])). % 65.00/65.81 cnf(19572,plain, % 65.00/65.81 (~P3(a1,a2,a1)+P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19564,19555])). % 65.00/65.81 cnf(19574,plain, % 65.00/65.81 (P3(a2,a1,a2)+P3(a1,a2,a3)+~P3(a1,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19565,41])). % 65.00/65.81 cnf(19576,plain, % 65.00/65.81 (~P3(a1,a2,a2)+P3(a1,a3,a3)+P3(a1,a3,a1)), % 65.00/65.81 inference(scs_inference,[],[19567,19518])). % 65.00/65.81 cnf(19584,plain, % 65.00/65.81 (P3(a2,a1,a2)+P3(a1,a2,a1)+P3(a1,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[1,2,19574,10])). % 65.00/65.81 cnf(19591,plain, % 65.00/65.81 (~P3(a1,a2,a2)+P3(a1,a3,a3)), % 65.00/65.81 inference(scs_inference,[],[19576,19165])). % 65.00/65.81 cnf(19616,plain, % 65.00/65.81 (P3(a2,a2,a2)+~P3(a3,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19018,19485])). % 65.00/65.81 cnf(19646,plain, % 65.00/65.81 (~P3(a2,a3,a2)+~P3(a2,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19018,19491])). % 65.00/65.81 cnf(19647,plain, % 65.00/65.81 (~P3(a2,a3,a2)), % 65.00/65.81 inference(scs_inference,[],[19646,19457])). % 65.00/65.81 cnf(19661,plain, % 65.00/65.81 (~P3(a1,a2,a1)), % 65.00/65.81 inference(scs_inference,[],[19647,19572])). % 65.00/65.81 cnf(19665,plain, % 65.00/65.81 (~P3(x196651,a2,a2)+~P3(a3,x196651,a2)), % 65.00/65.81 inference(scs_inference,[],[19647,14])). % 65.00/65.81 cnf(19667,plain, % 65.00/65.81 (~P3(a1,a2,a2)+P3(a3,a1,a1)), % 65.00/65.81 inference(scs_inference,[],[19647,14,19355])). % 65.00/65.81 cnf(19668,plain, % 65.00/65.81 (P3(a3,a2,a3)+~P3(a1,a2,a2)), % 65.00/65.81 inference(scs_inference,[],[19647,14,19355,19364])). % 65.00/65.81 cnf(19672,plain, % 65.00/65.81 (P3(a2,a1,a2)+P3(a1,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19661,19584])). % 65.00/65.81 cnf(19694,plain, % 65.00/65.81 (P3(a1,a2,a3)), % 65.00/65.81 inference(scs_inference,[],[19661,2,1,10,19526,19665,19090,19165,19187,19210,19274,19379,19389,19401,19518,19591,19667,19668,19672])). % 65.00/65.81 cnf(19701,plain, % 65.00/65.81 (P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19694,19533])). % 65.00/65.81 cnf(19724,plain, % 65.00/65.81 (~P3(a2,a1,a3)), % 65.00/65.81 inference(scs_inference,[],[19694,19647,19351,8,3,2,19008,19027,17,13,14,10,19010,19055,19616,19526,19364,37,38])). % 65.00/65.81 cnf(19741,plain, % 65.00/65.81 ($false), % 65.00/65.81 inference(scs_inference,[],[19701,19724]), % 65.00/65.81 ['proof']). % 65.00/65.81 % SZS output end Proof % 65.00/65.81 % Total time :64.300000s %------------------------------------------------------------------------------