%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP133-1.003 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n023.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:58 EDT 2024 % Result : Unsatisfiable 104.30s 104.65s % Output : CNFRefutation 104.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : GRP133-1.003 : TPTP v8.2.0. Released v1.2.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n023.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Thu Jun 20 13:10:24 EDT 2024 % 0.12/0.32 % CPUTime : % 0.52/0.59 start to proof:theBenchmark % 104.30/104.64 %------------------------------------------- % 104.30/104.64 % File :CSE---1.7 % 104.30/104.64 % Problem :theBenchmark % 104.30/104.64 % Transform :cnf % 104.30/104.64 % Format :tptp:raw % 104.30/104.64 % Command :java -jar mcs_scs.jar %d %s % 104.30/104.64 % 104.30/104.64 % Result :Theorem 103.670000s % 104.30/104.64 % Output :CNFRefutation 103.670000s % 104.30/104.64 %------------------------------------------- % 104.30/104.65 %-------------------------------------------------------------------------- % 104.30/104.65 % File : GRP133-1.003 : TPTP v8.2.0. Released v1.2.0. % 104.30/104.65 % Domain : Group Theory (Quasigroups) % 104.30/104.65 % Problem : (a.b).(b.a) = a, no idempotence % 104.30/104.65 % Version : [Sla93] axioms. % 104.30/104.65 % English : Generate the multiplication table for the specified quasi- % 104.30/104.65 % group with 3 elements. % 104.30/104.65 % 104.30/104.65 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 104.30/104.65 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 104.30/104.65 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 104.30/104.65 % Source : [Sla93] % 104.30/104.65 % Names : QG3-ni [Sla93] % 104.30/104.65 % 104.30/104.65 % Status : Unsatisfiable % 104.30/104.65 % Rating : 0.00 v2.1.0 % 104.30/104.65 % Syntax : Number of clauses : 14 ( 9 unt; 1 nHn; 14 RR) % 104.30/104.65 % Number of literals : 26 ( 0 equ; 16 neg) % 104.30/104.65 % Maximal clause size : 5 ( 1 avg) % 104.30/104.65 % Maximal term depth : 1 ( 1 avg) % 104.30/104.65 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 104.30/104.65 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 104.30/104.65 % Number of variables : 18 ( 0 sgn) % 104.30/104.65 % SPC : CNF_UNS_EPR_NEQ_NHN % 104.30/104.65 % 104.30/104.65 % Comments : Slaney's [1993] axiomatization has been modified for this. % 104.30/104.65 % : Substitution axioms are not needed, as any positive equality % 104.30/104.65 % literals should resolve on negative ones directly. % 104.30/104.65 % : tptp2X: -f tptp -s3 GRP133-1.g % 104.30/104.65 %-------------------------------------------------------------------------- % 104.30/104.65 cnf(element_1,axiom, % 104.30/104.65 group_element(e_1) ). % 104.30/104.65 % 104.30/104.65 cnf(element_2,axiom, % 104.30/104.65 group_element(e_2) ). % 104.30/104.65 % 104.30/104.65 cnf(element_3,axiom, % 104.30/104.65 group_element(e_3) ). % 104.30/104.65 % 104.30/104.65 cnf(e_1_is_not_e_2,axiom, % 104.30/104.65 ~ equalish(e_1,e_2) ). % 104.30/104.65 % 104.30/104.65 cnf(e_1_is_not_e_3,axiom, % 104.30/104.65 ~ equalish(e_1,e_3) ). % 104.30/104.65 % 104.30/104.65 cnf(e_2_is_not_e_1,axiom, % 104.30/104.65 ~ equalish(e_2,e_1) ). % 104.30/104.65 % 104.30/104.65 cnf(e_2_is_not_e_3,axiom, % 104.30/104.65 ~ equalish(e_2,e_3) ). % 104.30/104.65 % 104.30/104.65 cnf(e_3_is_not_e_1,axiom, % 104.30/104.65 ~ equalish(e_3,e_1) ). % 104.30/104.65 % 104.30/104.65 cnf(e_3_is_not_e_2,axiom, % 104.30/104.65 ~ equalish(e_3,e_2) ). % 104.30/104.65 % 104.30/104.65 cnf(product_total_function1,axiom, % 104.30/104.65 ( ~ group_element(X) % 104.30/104.65 | ~ group_element(Y) % 104.30/104.65 | product(X,Y,e_1) % 104.30/104.65 | product(X,Y,e_2) % 104.30/104.65 | product(X,Y,e_3) ) ). % 104.30/104.65 % 104.30/104.65 cnf(product_total_function2,axiom, % 104.30/104.65 ( ~ product(X,Y,W) % 104.30/104.65 | ~ product(X,Y,Z) % 104.30/104.65 | equalish(W,Z) ) ). % 104.30/104.65 % 104.30/104.65 cnf(product_right_cancellation,axiom, % 104.30/104.65 ( ~ product(X,W,Y) % 104.30/104.65 | ~ product(X,Z,Y) % 104.30/104.65 | equalish(W,Z) ) ). % 104.30/104.65 % 104.30/104.65 cnf(product_left_cancellation,axiom, % 104.30/104.65 ( ~ product(W,Y,X) % 104.30/104.65 | ~ product(Z,Y,X) % 104.30/104.65 | equalish(W,Z) ) ). % 104.30/104.65 % 104.30/104.65 cnf(qg3,negated_conjecture, % 104.30/104.65 ( ~ product(X,Y,Z1) % 104.30/104.65 | ~ product(Y,X,Z2) % 104.30/104.65 | product(Z1,Z2,X) ) ). % 104.30/104.65 % 104.30/104.65 %-------------------------------------------------------------------------- % 104.30/104.65 %------------------------------------------- % 104.30/104.65 % Proof found % 104.30/104.65 % SZS status Theorem for theBenchmark % 104.30/104.65 % SZS output start Proof % 104.30/104.65 %ClaNum:14(EqnAxiom:0) % 104.30/104.65 %VarNum:41(SingletonVarNum:18) % 104.30/104.65 %MaxLitNum:5 % 104.30/104.65 %MaxfuncDepth:0 % 104.30/104.65 %SharedTerms:12 % 104.30/104.65 %goalClause: 14 % 104.30/104.65 [1]P1(a1) % 104.30/104.65 [2]P1(a2) % 104.30/104.65 [3]P1(a3) % 104.30/104.65 [4]~P2(a1,a2) % 104.30/104.65 [5]~P2(a1,a3) % 104.30/104.65 [6]~P2(a2,a1) % 104.30/104.65 [7]~P2(a2,a3) % 104.30/104.65 [8]~P2(a3,a1) % 104.30/104.65 [9]~P2(a3,a2) % 104.30/104.65 [11]~P3(x113,x114,x111)+P2(x111,x112)+~P3(x113,x114,x112) % 104.30/104.65 [12]~P3(x123,x121,x124)+P2(x121,x122)+~P3(x123,x122,x124) % 104.30/104.65 [13]~P3(x131,x133,x134)+P2(x131,x132)+~P3(x132,x133,x134) % 104.30/104.65 [14]~P3(x143,x144,x141)+P3(x141,x142,x143)+~P3(x144,x143,x142) % 104.30/104.65 [10]~P1(x102)+~P1(x101)+P3(x101,x102,a2)+P3(x101,x102,a3)+P3(x101,x102,a1) % 104.30/104.65 %EqnAxiom % 104.30/104.65 % 104.30/104.65 %------------------------------------------- % 104.30/104.67 cnf(15,plain, % 104.30/104.67 (~P3(x151,a2,x152)+~P3(x153,x152,a1)+~P3(a2,x151,x153)), % 104.30/104.67 inference(scs_inference,[],[4,11,14])). % 104.30/104.67 cnf(16,plain, % 104.30/104.67 (~P3(x161,x162,a3)+~P3(x163,a1,x162)+~P3(x162,x161,x163)), % 104.30/104.67 inference(scs_inference,[],[5,12,14])). % 104.30/104.67 cnf(17,plain, % 104.30/104.67 (~P3(x171,x172,x173)+~P3(a1,x173,x172)+~P3(x172,x171,a2)), % 104.30/104.67 inference(scs_inference,[],[4,13,14])). % 104.30/104.67 cnf(18,plain, % 104.30/104.67 (~P3(x181,x182,a1)+~P3(x183,a3,x182)+~P3(a3,x183,x181)), % 104.30/104.67 inference(scs_inference,[],[8,11,14])). % 104.30/104.67 cnf(20,plain, % 104.30/104.67 (~P3(x201,x202,a3)+~P3(x203,a2,x202)+~P3(a2,x203,x201)), % 104.30/104.67 inference(scs_inference,[],[7,11,14])). % 104.30/104.67 cnf(24,plain, % 104.30/104.67 (~P3(x241,x242,a3)+~P3(x243,a1,x242)+~P3(a1,x243,x241)), % 104.30/104.67 inference(scs_inference,[],[5,11,14])). % 104.30/104.67 cnf(27,plain, % 104.30/104.67 (~P3(x271,a3,x272)+~P3(x273,x272,a2)+~P3(a3,x271,x273)), % 104.30/104.67 inference(scs_inference,[],[7,11,14])). % 104.30/104.67 cnf(37,plain, % 104.30/104.67 (~P3(x371,a2,x372)+~P3(x373,x372,a3)+~P3(x372,x373,x371)), % 104.30/104.67 inference(scs_inference,[],[9,12,14])). % 104.30/104.67 cnf(38,plain, % 104.30/104.67 (~P3(x381,x382,a1)+~P3(x383,a2,x382)+~P3(x382,x381,x383)), % 104.30/104.67 inference(scs_inference,[],[6,12,14])). % 104.30/104.67 cnf(39,plain, % 104.30/104.67 (~P3(x391,a3,x392)+~P3(x393,x392,a1)+~P3(x392,x393,x391)), % 104.30/104.67 inference(scs_inference,[],[5,12,14])). % 104.30/104.67 cnf(46,plain, % 104.30/104.67 (~P3(x461,x462,a2)+~P3(x463,a1,x462)+~P3(x462,x461,x463)), % 104.30/104.67 inference(scs_inference,[],[4,12,14])). % 104.30/104.67 cnf(47,plain, % 104.30/104.67 (~P3(x471,a3,x472)+~P3(x473,x472,a2)+~P3(x472,x473,x471)), % 104.30/104.67 inference(scs_inference,[],[7,12,14])). % 104.30/104.67 cnf(75,plain, % 104.30/104.67 (~P3(a1,a2,a3)+P3(a1,a1,a2)+P3(a1,a1,a1)), % 104.30/104.67 inference(scs_inference,[],[4,1,12,10])). % 104.30/104.67 cnf(84,plain, % 104.30/104.67 (~P3(a1,a3,a2)+~P3(a1,a2,a3)+P3(a1,a1,a1)), % 104.30/104.67 inference(scs_inference,[],[8,12,75])). % 104.30/104.67 cnf(106,plain, % 104.30/104.67 (~P3(a3,a2,a2)+P3(a3,a3,a3)+P3(a3,a3,a1)), % 104.30/104.67 inference(scs_inference,[],[9,3,12,10])). % 104.30/104.67 cnf(116,plain, % 104.30/104.67 (~P3(a3,a3,a2)+P3(a3,a2,a3)+P3(a3,a2,a1)), % 104.30/104.67 inference(scs_inference,[],[7,2,3,12,10])). % 104.30/104.67 cnf(119,plain, % 104.30/104.67 (~P3(a3,a1,a3)+~P3(a3,a3,a2)+P3(a3,a2,a1)), % 104.30/104.67 inference(scs_inference,[],[4,12,116])). % 104.30/104.67 cnf(126,plain, % 104.30/104.67 (~P3(a3,a3,a3)+P3(a3,a1,a2)+P3(a3,a1,a1)), % 104.30/104.67 inference(scs_inference,[],[8,1,3,12,10])). % 104.30/104.67 cnf(127,plain, % 104.30/104.67 (~P3(a1,a3,a3)+P3(a1,a2,a2)+P3(a1,a2,a1)), % 104.30/104.67 inference(scs_inference,[],[7,2,1,12,10])). % 104.30/104.67 cnf(132,plain, % 104.30/104.67 (~P3(a1,a1,a2)+P3(a1,a2,a1)+~P3(a1,a3,a3)), % 104.30/104.67 inference(scs_inference,[],[6,12,127])). % 104.30/104.67 cnf(175,plain, % 104.30/104.67 (~P3(a3,a3,a1)+P3(a3,a2,a2)+P3(a3,a2,a3)), % 104.30/104.67 inference(scs_inference,[],[7,2,3,12,10])). % 104.30/104.67 cnf(178,plain, % 104.30/104.67 (~P3(a3,a1,a3)+~P3(a3,a3,a1)+P3(a3,a2,a2)), % 104.30/104.67 inference(scs_inference,[],[4,12,175])). % 104.30/104.67 cnf(185,plain, % 104.30/104.67 (~P3(a1,a2,a1)+P3(a1,a3,a2)+P3(a1,a3,a3)), % 104.30/104.67 inference(scs_inference,[],[7,3,1,12,10])). % 104.30/104.67 cnf(187,plain, % 104.30/104.67 (~P3(a1,a1,a3)+~P3(a1,a2,a1)+P3(a1,a3,a2)), % 104.30/104.67 inference(scs_inference,[],[5,12,185])). % 104.30/104.67 cnf(188,plain, % 104.30/104.67 (~P3(a1,a2,a1)+P3(a1,a1,a2)+P3(a1,a1,a3)), % 104.30/104.67 inference(scs_inference,[],[4,1,12,10])). % 104.30/104.67 cnf(189,plain, % 104.30/104.67 (P3(a1,a1,a3)+~P3(a1,a2,a1)), % 104.30/104.67 inference(scs_inference,[],[188,17])). % 104.30/104.67 cnf(200,plain, % 104.30/104.67 (~P3(a1,a1,a2)+P3(a1,a1,a3)+~P3(a1,a3,a3)), % 104.30/104.67 inference(scs_inference,[],[189,132])). % 104.30/104.67 cnf(201,plain, % 104.30/104.67 (P3(a1,a1,a3)+P3(a1,a1,a1)+~P3(a1,a3,a3)), % 104.30/104.67 inference(scs_inference,[],[1,200,10])). % 104.30/104.67 cnf(202,plain, % 104.30/104.67 (P3(a1,a1,a1)+~P3(a3,a1,a1)+~P3(a1,a3,a3)), % 104.30/104.67 inference(scs_inference,[],[201,16])). % 104.30/104.67 cnf(206,plain, % 104.30/104.67 (P3(a1,a1,a3)+P3(a1,a2,a2)+P3(a1,a2,a3)), % 104.30/104.67 inference(scs_inference,[],[2,1,189,10])). % 104.30/104.67 cnf(207,plain, % 104.30/104.67 (P3(a1,a1,a3)+P3(a1,a2,a3)+~P3(a2,a1,a2)), % 104.30/104.67 inference(scs_inference,[],[206,17])). % 104.30/104.67 cnf(211,plain, % 104.30/104.67 (P3(a3,a3,a1)+~P3(a1,a2,a1)), % 104.30/104.67 inference(scs_inference,[],[189,14])). % 104.30/104.67 cnf(216,plain, % 104.30/104.67 (~P3(a1,a2,a1)+~P3(a3,a1,a1)), % 104.30/104.67 inference(scs_inference,[],[189,16])). % 104.30/104.67 cnf(230,plain, % 104.30/104.67 (~P3(a1,a2,a1)+~P3(a3,a3,a3)), % 104.30/104.67 inference(scs_inference,[],[189,24])). % 104.30/104.67 cnf(16084,plain, % 104.30/104.67 (~P3(x160841,x160842,a1)+~P3(x160841,x160842,a3)), % 104.30/104.67 inference(scs_inference,[],[8,11])). % 104.30/104.67 cnf(16088,plain, % 104.30/104.67 (~P3(x160881,a2,x160882)+~P3(x160881,a3,x160882)), % 104.30/104.67 inference(scs_inference,[],[9,12])). % 104.30/104.67 cnf(16090,plain, % 104.30/104.67 (~P3(a2,x160901,x160902)+~P3(a3,x160901,x160902)), % 104.30/104.67 inference(scs_inference,[],[9,12,13])). % 104.30/104.68 cnf(16092,plain, % 104.30/104.68 (P3(a2,a2,a2)+P3(a2,a2,a1)+P3(a2,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[2,10])). % 104.30/104.68 cnf(16093,plain, % 104.30/104.68 (~P3(x160931,x160932,a2)+~P3(x160931,x160932,a3)), % 104.30/104.68 inference(scs_inference,[],[9,11])). % 104.30/104.68 cnf(16096,plain, % 104.30/104.68 (~P3(x160961,a1,x160962)+~P3(x160961,a3,x160962)), % 104.30/104.68 inference(scs_inference,[],[8,12])). % 104.30/104.68 cnf(16099,plain, % 104.30/104.68 (~P3(a1,x160991,x160992)+~P3(a3,x160991,x160992)), % 104.30/104.68 inference(scs_inference,[],[8,13])). % 104.30/104.68 cnf(16103,plain, % 104.30/104.68 (~P3(x161031,x161032,a1)+~P3(x161031,x161032,a2)), % 104.30/104.68 inference(scs_inference,[],[6,11])). % 104.30/104.68 cnf(16106,plain, % 104.30/104.68 (~P3(a2,x161061,x161062)+~P3(a1,x161061,x161062)), % 104.30/104.68 inference(scs_inference,[],[4,13])). % 104.30/104.68 cnf(16108,plain, % 104.30/104.68 (~P3(a2,a2,a2)+P3(a1,a2,a1)+P3(a1,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[2,4,1,13,10])). % 104.30/104.68 cnf(16109,plain, % 104.30/104.68 (~P3(x161091,a2,x161092)+~P3(x161091,a1,x161092)), % 104.30/104.68 inference(scs_inference,[],[4,12])). % 104.30/104.68 cnf(16114,plain, % 104.30/104.68 (~P3(a1,a2,a1)+~P3(a1,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[16093,189])). % 104.30/104.68 cnf(16116,plain, % 104.30/104.68 (~P3(x161161,x161162,x161163)+~P3(x161162,x161161,a3)+~P3(a1,x161163,x161162)), % 104.30/104.68 inference(scs_inference,[],[16099,14])). % 104.30/104.68 cnf(16117,plain, % 104.30/104.68 (P3(a1,a1,a2)+P3(a1,a1,a1)+P3(a1,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[1,10])). % 104.30/104.68 cnf(16120,plain, % 104.30/104.68 (~P3(a1,a2,a1)+~P3(a2,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[16106,189])). % 104.30/104.68 cnf(16121,plain, % 104.30/104.68 (~P3(a3,a3,a3)+P3(a3,a1,a1)+~P3(a3,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[16109,126])). % 104.30/104.68 cnf(16123,plain, % 104.30/104.68 (~P3(a1,a1,a2)+~P3(a1,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[16114,132])). % 104.30/104.68 cnf(16129,plain, % 104.30/104.68 (~P3(a2,a1,a2)+P3(a1,a1,a3)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[46,207])). % 104.30/104.68 cnf(16142,plain, % 104.30/104.68 (~P3(a1,a2,a1)+P3(a1,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[187,189])). % 104.30/104.68 cnf(16143,plain, % 104.30/104.68 (~P3(x161431,a1,a2)+~P3(a1,x161431,a1)+P3(a1,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[16142,14])). % 104.30/104.68 cnf(16147,plain, % 104.30/104.68 (~P3(a1,a3,a3)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[202,16099])). % 104.30/104.68 cnf(16148,plain, % 104.30/104.68 (~P3(x161481,a1,a1)+~P3(a1,x161481,a3)+~P3(a1,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[16147,14])). % 104.30/104.68 cnf(16153,plain, % 104.30/104.68 (P3(a1,a1,a1)+P3(a1,a1,a2)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[16117,16])). % 104.30/104.68 cnf(16155,plain, % 104.30/104.68 (P3(a3,a3,a1)+~P3(a3,a2,a2)+P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[16121,106])). % 104.30/104.68 cnf(16158,plain, % 104.30/104.68 (~P3(a2,a1,a2)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[16129,16])). % 104.30/104.68 cnf(16169,plain, % 104.30/104.68 (P3(a1,a1,a2)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[16153,16099])). % 104.30/104.68 cnf(16188,plain, % 104.30/104.68 (~P3(a1,a2,a1)+~P3(a1,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[189,16096])). % 104.30/104.68 cnf(16189,plain, % 104.30/104.68 (P3(a1,a2,a2)+~P3(a1,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[16188,127])). % 104.30/104.68 cnf(16192,plain, % 104.30/104.68 (~P3(a1,a2,a1)+~P3(a3,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[189,16099])). % 104.30/104.68 cnf(20198,plain, % 104.30/104.68 (~P3(a1,a2,a1)+P3(a3,a1,a3)+P3(a3,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[3,1,216,10])). % 104.30/104.68 cnf(20199,plain, % 104.30/104.68 (~P3(a1,a2,a1)+P3(a3,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[20198,16192])). % 104.30/104.68 cnf(20209,plain, % 104.30/104.68 (~P3(a3,a1,a1)+P3(a1,a2,a3)+P3(a1,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[2,1,216,10])). % 104.30/104.68 cnf(20210,plain, % 104.30/104.68 (P3(a1,a2,a3)+~P3(a3,a1,a1)+~P3(a2,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20209,16116])). % 104.30/104.68 cnf(20212,plain, % 104.30/104.68 (~P3(a2,a1,a3)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20210,16])). % 104.30/104.68 cnf(20223,plain, % 104.30/104.68 (~P3(a3,a3,a3)+P3(a1,a2,a3)+~P3(a2,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[230,16108])). % 104.30/104.68 cnf(20236,plain, % 104.30/104.68 (~P3(a1,a3,a2)+P3(a1,a2,a3)+P3(a1,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[2,1,16088,10])). % 104.30/104.68 cnf(20237,plain, % 104.30/104.68 (P3(a1,a1,a1)+~P3(a1,a3,a2)+P3(a1,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[20236,84])). % 104.30/104.68 cnf(20245,plain, % 104.30/104.68 (P3(a3,a3,a3)+P3(a3,a3,a2)+~P3(a3,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[3,16088,10])). % 104.30/104.68 cnf(20256,plain, % 104.30/104.68 (~P3(a3,a3,a3)+~P3(a3,a2,a2)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[16090,16121])). % 104.30/104.68 cnf(20263,plain, % 104.30/104.68 (P3(a3,a3,a2)+~P3(a3,a2,a1)+~P3(a2,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[16090,20245])). % 104.30/104.68 cnf(20264,plain, % 104.30/104.68 (~P3(a3,a2,a1)+~P3(a2,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20263,47])). % 104.30/104.68 cnf(20265,plain, % 104.30/104.68 (~P3(a3,a2,a1)+P3(a2,a3,a2)+P3(a2,a3,a1)), % 104.30/104.68 inference(scs_inference,[],[2,3,20264,10])). % 104.30/104.68 cnf(20267,plain, % 104.30/104.68 (P3(a2,a3,a1)+~P3(a3,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[20265,39])). % 104.30/104.68 cnf(20279,plain, % 104.30/104.68 (P3(a3,a1,a2)+P3(a3,a1,a3)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[3,1,16090,10])). % 104.30/104.68 cnf(20280,plain, % 104.30/104.68 (~P3(a3,a2,a1)+P3(a2,a2,a2)+P3(a2,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[2,16090,10])). % 104.30/104.68 cnf(20281,plain, % 104.30/104.68 (P3(a2,a2,a2)+~P3(a3,a2,a1)+~P3(a3,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20280,20])). % 104.30/104.68 cnf(20285,plain, % 104.30/104.68 (P3(a3,a1,a2)+P3(a3,a1,a1)+~P3(a2,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[3,1,16090,10])). % 104.30/104.68 cnf(20286,plain, % 104.30/104.68 (~P3(a2,a1,a3)+P3(a3,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[20285,20212])). % 104.30/104.68 cnf(20291,plain, % 104.30/104.68 (~P3(a3,a1,a2)+P3(a2,a1,a3)+P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[2,1,16090,10])). % 104.30/104.68 cnf(20292,plain, % 104.30/104.68 (~P3(a1,a2,a1)+P3(a2,a1,a1)+P3(a2,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20291,20199])). % 104.30/104.68 cnf(20293,plain, % 104.30/104.68 (~P3(a1,a2,a1)+P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20292,16120])). % 104.30/104.68 cnf(20301,plain, % 104.30/104.68 (P3(a3,a1,a3)+P3(a3,a1,a1)+~P3(a2,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[3,1,16090,10])). % 104.30/104.68 cnf(20303,plain, % 104.30/104.68 (~P3(a2,a1,a2)+P3(a3,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20301,16158])). % 104.30/104.68 cnf(20304,plain, % 104.30/104.68 (P3(a3,a1,a3)+P3(a2,a1,a3)+P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[2,1,20303,10])). % 104.30/104.68 cnf(20306,plain, % 104.30/104.68 (P3(a3,a1,a2)+P3(a2,a1,a3)+P3(a3,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20304,20279])). % 104.30/104.68 cnf(20307,plain, % 104.30/104.68 (P3(a3,a1,a2)+P3(a3,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20306,20286])). % 104.30/104.68 cnf(20317,plain, % 104.30/104.68 (P3(a3,a2,a2)+P3(a3,a2,a3)+~P3(a2,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[2,3,16090,10])). % 104.30/104.68 cnf(20322,plain, % 104.30/104.68 (~P3(a3,a1,a3)+P3(a2,a1,a2)+P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[2,1,16090,10])). % 104.30/104.68 cnf(20323,plain, % 104.30/104.68 (P3(a2,a1,a3)+P3(a2,a1,a1)+P3(a2,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[20322,20304])). % 104.30/104.68 cnf(20328,plain, % 104.30/104.68 (~P3(a3,a2,a2)+P3(a2,a2,a3)+P3(a2,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[2,16090,10])). % 104.30/104.68 cnf(20329,plain, % 104.30/104.68 (P3(a2,a2,a3)+~P3(a3,a2,a2)+~P3(a1,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20328,15])). % 104.30/104.68 cnf(20330,plain, % 104.30/104.68 (~P3(a1,a1,a1)+~P3(a3,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[20329,37])). % 104.30/104.68 cnf(20332,plain, % 104.30/104.68 (~P3(x203321,a1,a1)+~P3(a1,x203321,a1)+~P3(a3,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[20330,14])). % 104.30/104.68 cnf(20334,plain, % 104.30/104.68 (~P3(a1,a2,a1)+~P3(a3,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[20332,20293])). % 104.30/104.68 cnf(20338,plain, % 104.30/104.68 (~P3(a3,a1,a1)+~P3(a1,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[16093,16169])). % 104.30/104.68 cnf(20340,plain, % 104.30/104.68 (~P3(x203401,a1,a1)+~P3(a1,x203401,a3)+~P3(a1,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20338,14])). % 104.30/104.68 cnf(20342,plain, % 104.30/104.68 (P3(a1,a2,a3)+P3(a1,a2,a2)+~P3(a1,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20340,206])). % 104.30/104.68 cnf(20349,plain, % 104.30/104.68 (~P3(a3,a1,a1)+~P3(a1,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[16096,16169])). % 104.30/104.68 cnf(20350,plain, % 104.30/104.68 (~P3(a3,a3,a3)+~P3(a3,a2,a2)+~P3(a1,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[20349,16121])). % 104.30/104.68 cnf(20351,plain, % 104.30/104.68 (P3(a3,a3,a1)+~P3(a3,a2,a2)+~P3(a1,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[20350,106])). % 104.30/104.68 cnf(20352,plain, % 104.30/104.68 (~P3(a3,a2,a2)+~P3(a1,a3,a2)+~P3(a1,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[20351,38])). % 104.30/104.68 cnf(20353,plain, % 104.30/104.68 (~P3(a3,a2,a2)+~P3(a1,a3,a2)+P3(a1,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[20352,20236])). % 104.30/104.68 cnf(20354,plain, % 104.30/104.68 (~P3(a3,a2,a2)+~P3(a1,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[20353,20334])). % 104.30/104.68 cnf(20356,plain, % 104.30/104.68 (~P3(a1,a3,a2)+P3(a3,a2,a3)+P3(a3,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[3,2,20354,10])). % 104.30/104.68 cnf(20361,plain, % 104.30/104.68 (~P3(a3,a2,a1)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[16096,20267])). % 104.30/104.68 cnf(20377,plain, % 104.30/104.68 (P3(a3,a1,a3)+~P3(a3,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[16096,20307])). % 104.30/104.68 cnf(20381,plain, % 104.30/104.68 (P3(a1,a3,a2)+P3(a1,a3,a3)+~P3(a1,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[1,3,16096,10])). % 104.30/104.68 cnf(20382,plain, % 104.30/104.68 (P3(a3,a1,a2)+~P3(a3,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[16096,20307])). % 104.30/104.68 cnf(20391,plain, % 104.30/104.68 (P3(a1,a3,a3)+P3(a1,a3,a1)+~P3(a1,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[3,1,16096,10])). % 104.30/104.68 cnf(20393,plain, % 104.30/104.68 (~P3(a3,a1,a1)+P3(a1,a3,a1)+P3(a1,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20391,16169])). % 104.30/104.68 cnf(20394,plain, % 104.30/104.68 (P3(a1,a3,a3)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20393,39])). % 104.30/104.68 cnf(20395,plain, % 104.30/104.68 (~P3(x203951,a1,a1)+~P3(a1,x203951,a3)+P3(a1,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20394,14])). % 104.30/104.68 cnf(20396,plain, % 104.30/104.68 (~P3(a1,x203961,a3)+~P3(x203961,a1,a1)+~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20395,16148])). % 104.30/104.68 cnf(20397,plain, % 104.30/104.68 (~P3(a3,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20396,20394])). % 104.30/104.68 cnf(20398,plain, % 104.30/104.68 (~P3(a3,a3,a3)+~P3(a3,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[20397,16121])). % 104.30/104.68 cnf(20399,plain, % 104.30/104.68 (P3(a3,a3,a1)+~P3(a3,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[20397,16155])). % 104.30/104.68 cnf(20402,plain, % 104.30/104.68 (~P3(x204021,a1,a1)+~P3(a1,x204021,a3)), % 104.30/104.68 inference(scs_inference,[],[20397,14])). % 104.30/104.68 cnf(20405,plain, % 104.30/104.68 (~P3(a3,a3,a3)+~P3(a2,a2,a1)+P3(a3,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[20398,20317])). % 104.30/104.68 cnf(20407,plain, % 104.30/104.68 (~P3(a3,a2,a2)+~P3(a1,a3,a1)), % 104.30/104.68 inference(scs_inference,[],[20399,16099])). % 104.30/104.68 cnf(20409,plain, % 104.30/104.68 (~P3(a1,a3,a2)+P3(a1,a2,a1)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20402,20236])). % 104.30/104.68 cnf(20411,plain, % 104.30/104.68 (~P3(a2,a2,a1)+~P3(a3,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20405,16088])). % 104.30/104.68 cnf(20414,plain, % 104.30/104.68 (~P3(a1,a3,a2)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20409,38])). % 104.30/104.68 cnf(20415,plain, % 104.30/104.68 (~P3(a1,a2,a1)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20414,16142])). % 104.30/104.68 cnf(20416,plain, % 104.30/104.68 (~P3(a2,a1,a1)+P3(a1,a2,a2)+P3(a1,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[1,2,20415,10])). % 104.30/104.68 cnf(20418,plain, % 104.30/104.68 (P3(a1,a2,a2)+~P3(a3,a3,a1)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20416,39])). % 104.30/104.68 cnf(20426,plain, % 104.30/104.68 (P3(a2,a3,a2)+P3(a2,a3,a3)+~P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[2,3,16096,10])). % 104.30/104.68 cnf(20427,plain, % 104.30/104.68 (~P3(a1,a2,a1)+P3(a2,a3,a2)+P3(a2,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20426,20293])). % 104.30/104.68 cnf(20473,plain, % 104.30/104.68 (~P3(a2,a1,a2)+~P3(a1,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[16099,20303])). % 104.30/104.68 cnf(20474,plain, % 104.30/104.68 (~P3(a1,a1,a3)+P3(a2,a1,a3)+P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20473,20323])). % 104.30/104.68 cnf(20475,plain, % 104.30/104.68 (P3(a2,a1,a1)+~P3(a1,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20474,16106])). % 104.30/104.68 cnf(20498,plain, % 104.30/104.68 (~P3(a3,a3,a2)+~P3(a1,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[16099,20377])). % 104.30/104.68 cnf(20499,plain, % 104.30/104.68 (~P3(a3,a3,a2)+~P3(x204991,a3,a1)+~P3(a3,x204991,a1)), % 104.30/104.68 inference(scs_inference,[],[20498,14])). % 104.30/104.68 cnf(20500,plain, % 104.30/104.68 (~P3(a3,a3,a2)+~P3(a3,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[20499,20267])). % 104.30/104.68 cnf(20501,plain, % 104.30/104.68 (~P3(a3,a3,a2)+P3(a3,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[20500,116])). % 104.30/104.68 cnf(20502,plain, % 104.30/104.68 (P3(a3,a2,a3)+P3(a3,a3,a3)+P3(a3,a3,a1)), % 104.30/104.68 inference(scs_inference,[],[3,20501,10])). % 104.30/104.68 cnf(20503,plain, % 104.30/104.68 (P3(a3,a3,a3)+P3(a3,a2,a3)+~P3(a1,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20502,18])). % 104.30/104.68 cnf(20509,plain, % 104.30/104.68 (~P3(a3,a3,a3)+~P3(a1,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[16099,20382])). % 104.30/104.68 cnf(20510,plain, % 104.30/104.68 (~P3(a3,a3,a3)+P3(a1,a1,a1)+~P3(a1,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[20509,75])). % 104.30/104.68 cnf(20511,plain, % 104.30/104.68 (P3(a1,a1,a1)+~P3(a3,a3,a3)+~P3(a2,a2,a2)), % 104.30/104.68 inference(scs_inference,[],[20510,20223])). % 104.30/104.68 cnf(20512,plain, % 104.30/104.68 (P3(a1,a1,a1)+~P3(a3,a2,a1)+~P3(a3,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20511,20281])). % 104.30/104.68 cnf(20514,plain, % 104.30/104.68 (P3(a1,a1,a1)+~P3(a3,a2,a1)+P3(a3,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[20512,20245])). % 104.30/104.68 cnf(20516,plain, % 104.30/104.68 (~P3(a3,a2,a1)+P3(a1,a1,a1)+~P3(a1,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[20514,17])). % 104.30/104.68 cnf(20519,plain, % 104.30/104.68 (~P3(a1,a1,a1)+P3(a1,a2,a2)+~P3(a3,a2,a3)), % 104.30/104.68 inference(scs_inference,[],[16099,20342])). % 104.30/104.68 cnf(20520,plain, % 104.30/104.68 (~P3(a1,a1,a1)+~P3(a3,a2,a3)+~P3(a2,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[20519,17])). % 104.30/104.68 cnf(20522,plain, % 104.30/104.68 (~P3(a2,a1,a2)+~P3(a1,a1,a1)+P3(a3,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[20520,20503])). % 104.30/104.68 cnf(20524,plain, % 104.30/104.68 (~P3(a1,a1,a1)+~P3(a2,a1,a2)+~P3(a3,a1,a3)), % 104.30/104.68 inference(scs_inference,[],[20522,16])). % 104.30/104.68 cnf(20525,plain, % 104.30/104.68 (~P3(a2,a1,a2)+~P3(a1,a1,a1)+P3(a3,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[3,1,20397,20524,10])). % 104.30/104.68 cnf(20526,plain, % 104.30/104.68 (~P3(a1,a1,a1)+~P3(a2,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[20525,16090])). % 104.30/104.68 cnf(20527,plain, % 104.30/104.68 (~P3(a1,a1,a1)+~P3(a3,a1,a3)+P3(a2,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20526,20322])). % 104.30/104.68 cnf(20529,plain, % 104.30/104.68 (~P3(a1,a1,a1)+P3(a2,a1,a1)+P3(a3,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[3,1,20397,20527,10])). % 104.30/104.68 cnf(20530,plain, % 104.30/104.68 (P3(a3,a1,a2)+~P3(a1,a1,a1)), % 104.30/104.68 inference(scs_inference,[],[20529,16106])). % 104.30/104.68 cnf(20539,plain, % 104.30/104.68 (~P3(a3,a2,a1)+P3(a3,a3,a2)+~P3(a1,a3,a3)), % 104.30/104.68 inference(scs_inference,[],[16099,20245])). % 104.30/104.68 cnf(20540,plain, % 104.30/104.68 (~P3(a1,a3,a3)+~P3(a3,a2,a1)), % 104.30/104.68 inference(scs_inference,[],[20539,20500])). % 104.30/104.68 cnf(20541,plain, % 104.30/104.68 (~P3(a1,a3,a3)+~P3(x205411,a1,a2)+~P3(a1,x205411,a3)), % 104.30/104.68 inference(scs_inference,[],[20540,14])). % 104.30/104.68 cnf(20542,plain, % 104.30/104.68 (~P3(a1,a1,a1)+P3(a1,a3,a2)+~P3(a3,a1,a2)), % 104.30/104.68 inference(scs_inference,[],[20541,20381])). % 104.30/104.68 cnf(20543,plain, % 104.30/104.68 (~P3(a1,a1,a1)+P3(a1,a3,a2)), % 104.30/104.68 inference(scs_inference,[],[20542,20530])). % 104.30/104.68 cnf(20549,plain, % 104.30/104.69 (~P3(a1,a3,a2)+P3(a3,a2,a1)+~P3(a1,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[16099,20356])). % 104.30/104.69 cnf(20550,plain, % 104.30/104.69 (~P3(a1,a3,a2)+P3(a1,a2,a1)+P3(a3,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20549,20236])). % 104.30/104.69 cnf(20551,plain, % 104.30/104.69 (~P3(a1,a1,a1)+P3(a1,a2,a1)+P3(a3,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20550,20543])). % 104.30/104.69 cnf(20552,plain, % 104.30/104.69 (P3(a3,a2,a1)+~P3(a1,a1,a1)), % 104.30/104.69 inference(scs_inference,[],[20551,16109])). % 104.30/104.69 cnf(20567,plain, % 104.30/104.69 (P3(a3,a2,a3)+P3(a3,a2,a1)+~P3(a1,a2,a2)), % 104.30/104.69 inference(scs_inference,[],[3,2,16099,10])). % 104.30/104.69 cnf(20568,plain, % 104.30/104.69 (~P3(a1,a3,a3)+P3(a3,a2,a1)+P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20567,16189])). % 104.30/104.69 cnf(20569,plain, % 104.30/104.69 (~P3(a1,a3,a3)+P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20568,20540])). % 104.30/104.69 cnf(20571,plain, % 104.30/104.69 (~P3(a1,a1,a2)+P3(a1,a3,a1)+P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20569,20391])). % 104.30/104.69 cnf(20577,plain, % 104.30/104.69 (P3(a3,a2,a2)+P3(a3,a2,a1)+~P3(a1,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[2,3,16099,10])). % 104.30/104.69 cnf(20589,plain, % 104.30/104.69 (~P3(a3,a3,a1)+~P3(a2,a1,a1)+~P3(a3,a2,a2)), % 104.30/104.69 inference(scs_inference,[],[16099,20418])). % 104.30/104.69 cnf(20590,plain, % 104.30/104.69 (P3(a3,a3,a3)+~P3(a3,a2,a2)+~P3(a2,a1,a1)), % 104.30/104.69 inference(scs_inference,[],[20589,106])). % 104.30/104.69 cnf(20591,plain, % 104.30/104.69 (~P3(a3,a2,a2)+~P3(a2,a1,a1)), % 104.30/104.69 inference(scs_inference,[],[20590,20256])). % 104.30/104.69 cnf(20593,plain, % 104.30/104.69 (~P3(a2,a1,a1)+P3(a3,a2,a3)+P3(a3,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[3,2,20591,10])). % 104.30/104.69 cnf(20594,plain, % 104.30/104.69 (~P3(a2,a1,a1)+P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20593,20361])). % 104.30/104.69 cnf(20595,plain, % 104.30/104.69 (~P3(a1,a1,a3)+P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20594,20475])). % 104.30/104.69 cnf(20596,plain, % 104.30/104.69 (~P3(x205961,a3,a1)+~P3(a3,x205961,a1)+P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20595,14])). % 104.30/104.69 cnf(20597,plain, % 104.30/104.69 (~P3(a2,a3,a3)+~P3(a3,x205971,a1)+~P3(x205971,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[20596,37])). % 104.30/104.69 cnf(20598,plain, % 104.30/104.69 (~P3(a2,a3,a3)+~P3(a1,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20597,211])). % 104.30/104.69 cnf(20599,plain, % 104.30/104.69 (~P3(a1,a2,a1)+P3(a2,a3,a2)), % 104.30/104.69 inference(scs_inference,[],[20598,20427])). % 104.30/104.69 cnf(20600,plain, % 104.30/104.69 (P3(a1,a2,a3)+~P3(a2,a2,a2)+P3(a2,a3,a2)), % 104.30/104.69 inference(scs_inference,[],[20599,16108])). % 104.30/104.69 cnf(20601,plain, % 104.30/104.69 (P3(a1,a2,a3)+~P3(a2,a2,a2)), % 104.30/104.69 inference(scs_inference,[],[20600,16088])). % 104.30/104.69 cnf(20602,plain, % 104.30/104.69 (P3(a1,a2,a3)+P3(a2,a2,a1)+P3(a2,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20601,16092])). % 104.30/104.69 cnf(20604,plain, % 104.30/104.69 (P3(a2,a2,a1)+P3(a1,a2,a3)+~P3(a3,a3,a3)), % 104.30/104.69 inference(scs_inference,[],[20602,20])). % 104.30/104.69 cnf(20606,plain, % 104.30/104.69 (P3(a1,a2,a3)+~P3(a3,a3,a3)), % 104.30/104.69 inference(scs_inference,[],[20604,20411])). % 104.30/104.69 cnf(20607,plain, % 104.30/104.69 (P3(a1,a2,a3)+P3(a3,a3,a2)+P3(a3,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[3,20606,10])). % 104.30/104.69 cnf(20608,plain, % 104.30/104.69 (P3(a3,a3,a2)+P3(a1,a2,a3)+~P3(a1,a1,a1)), % 104.30/104.69 inference(scs_inference,[],[20607,18])). % 104.30/104.69 cnf(20609,plain, % 104.30/104.69 (P3(a1,a2,a3)+P3(a3,a3,a2)+~P3(a3,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20608,20514])). % 104.30/104.69 cnf(20611,plain, % 104.30/104.69 (P3(a1,a2,a3)+~P3(a3,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20609,20500])). % 104.30/104.69 cnf(20613,plain, % 104.30/104.69 (P3(a1,a2,a3)+~P3(a1,a1,a1)), % 104.30/104.69 inference(scs_inference,[],[20611,20552])). % 104.30/104.69 cnf(20622,plain, % 104.30/104.69 (~P3(a1,a1,a1)+~P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[16099,20613])). % 104.30/104.69 cnf(20623,plain, % 104.30/104.69 (P3(a1,a1,a3)+~P3(a1,a3,a3)+~P3(a3,a2,a3)), % 104.30/104.69 inference(scs_inference,[],[20622,201])). % 104.30/104.69 cnf(20624,plain, % 104.30/104.69 (~P3(a3,a2,a3)+~P3(a1,a3,a3)), % 104.30/104.69 inference(scs_inference,[],[20623,16096])). % 104.30/104.69 cnf(20625,plain, % 104.30/104.69 (~P3(a1,a1,a2)+~P3(a3,a2,a3)+P3(a1,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[20624,20391])). % 104.30/104.69 cnf(20626,plain, % 104.30/104.69 (~P3(a1,a1,a2)+P3(a1,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[20625,20571])). % 104.30/104.69 cnf(20627,plain, % 104.30/104.69 (~P3(x206271,a2,a1)+~P3(a2,x206271,a1)+P3(a1,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[20626,14])). % 104.30/104.69 cnf(20628,plain, % 104.30/104.69 (~P3(a3,a1,a2)+~P3(a2,x206281,a1)+~P3(x206281,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20627,47])). % 104.30/104.69 cnf(20630,plain, % 104.30/104.69 (P3(a3,a1,a3)+~P3(x206301,a2,a1)+~P3(a2,x206301,a1)), % 104.30/104.69 inference(scs_inference,[],[3,1,20397,20628,10])). % 104.30/104.69 cnf(20631,plain, % 104.30/104.69 (~P3(a3,a2,a1)+P3(a3,a1,a3)), % 104.30/104.69 inference(scs_inference,[],[20630,20267])). % 104.30/104.69 cnf(20650,plain, % 104.30/104.69 (~P3(a3,a2,a1)+~P3(a1,a1,a3)), % 104.30/104.69 inference(scs_inference,[],[16099,20631])). % 104.30/104.69 cnf(20651,plain, % 104.30/104.69 (~P3(a3,a2,a1)+~P3(x206511,a3,a1)+~P3(a3,x206511,a1)), % 104.30/104.69 inference(scs_inference,[],[20650,14])). % 104.30/104.69 cnf(20652,plain, % 104.30/104.69 (~P3(a1,a1,a1)+~P3(a2,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[20651,20552])). % 104.30/104.69 cnf(20653,plain, % 104.30/104.69 (~P3(a1,a1,a1)+~P3(a3,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20652,20267])). % 104.30/104.69 cnf(20654,plain, % 104.30/104.69 (~P3(a1,a1,a1)), % 104.30/104.69 inference(scs_inference,[],[20653,20552])). % 104.30/104.69 cnf(20658,plain, % 104.30/104.69 (P3(a1,a1,a2)+P3(a1,a1,a3)), % 104.30/104.69 inference(scs_inference,[],[20654,16117])). % 104.30/104.69 cnf(20659,plain, % 104.30/104.69 (~P3(a1,a3,a2)+P3(a1,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20654,20237])). % 104.30/104.69 cnf(20668,plain, % 104.30/104.69 (~P3(a1,a2,a3)+~P3(a3,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20654,20516])). % 104.30/104.69 cnf(20677,plain, % 104.30/104.69 (P3(a1,a1,a2)+~P3(a1,a3,a3)), % 104.30/104.69 inference(scs_inference,[],[20658,16096])). % 104.30/104.69 cnf(20689,plain, % 104.30/104.69 (~P3(a1,a2,a3)+P3(a3,a2,a2)), % 104.30/104.69 inference(scs_inference,[],[20668,20577])). % 104.30/104.69 cnf(20696,plain, % 104.30/104.69 (~P3(a1,a3,a3)), % 104.30/104.69 inference(scs_inference,[],[20677,16123])). % 104.30/104.69 cnf(20702,plain, % 104.30/104.69 (P3(a1,a3,a2)+P3(a1,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[1,20696,3,10])). % 104.30/104.69 cnf(20712,plain, % 104.30/104.69 (~P3(a1,a2,a1)+P3(a1,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[1,20696,3,10,16099,16103,16106,20414,20475,20599])). % 104.30/104.69 cnf(20718,plain, % 104.30/104.69 (~P3(a3,a3,a3)+P3(a3,a2,a2)), % 104.30/104.69 inference(scs_inference,[],[20689,20606])). % 104.30/104.69 cnf(20729,plain, % 104.30/104.69 (P3(a1,a3,a1)+~P3(a1,a3,a2)), % 104.30/104.69 inference(scs_inference,[],[20712,20659])). % 104.30/104.69 cnf(20731,plain, % 104.30/104.69 (P3(a3,a2,a2)+P3(a3,a3,a2)+P3(a3,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[3,20718,10])). % 104.30/104.69 cnf(20738,plain, % 104.30/104.69 (~P3(a1,a3,a2)+~P3(a1,a2,a1)), % 104.30/104.69 inference(scs_inference,[],[20729,16088])). % 104.30/104.69 cnf(20741,plain, % 104.30/104.69 (~P3(a1,a3,a2)), % 104.30/104.69 inference(scs_inference,[],[20738,20659])). % 104.30/104.69 cnf(20744,plain, % 104.30/104.69 (~P3(a1,x207441,a1)+~P3(x207441,a1,a2)), % 104.30/104.69 inference(scs_inference,[],[20741,16143])). % 104.30/104.69 cnf(20750,plain, % 104.30/104.69 (P3(a1,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[20741,20702])). % 104.30/104.69 cnf(20759,plain, % 104.30/104.69 (~P3(a3,a2,a2)), % 104.30/104.69 inference(scs_inference,[],[20750,20407])). % 104.30/104.69 cnf(20773,plain, % 104.30/104.69 (~P3(a3,a1,a3)+~P3(a3,a3,a1)), % 104.30/104.69 inference(scs_inference,[],[20759,178])). % 104.30/104.69 cnf(20792,plain, % 104.30/104.69 (P3(a3,a3,a1)+P3(a3,a3,a2)), % 104.30/104.69 inference(scs_inference,[],[20759,20731])). % 104.30/104.69 cnf(20813,plain, % 104.30/104.69 ($false), % 104.30/104.69 inference(scs_inference,[],[20750,5,4,20744,20307,20773,20792,16099,47,27,119,20280,11,13,16084,20267]), % 104.30/104.69 ['proof']). % 104.30/104.69 % SZS output end Proof % 104.30/104.69 % Total time :103.670000s %------------------------------------------------------------------------------