%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP126-1.004 : 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 : n020.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:52 EDT 2024 % Result : Unsatisfiable 61.75s 61.96s % Output : CNFRefutation 62.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP126-1.004 : 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 : n020.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 07:30:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 61.64/61.94 %------------------------------------------- % 61.64/61.94 % File :CSE---1.7 % 61.64/61.94 % Problem :theBenchmark % 61.64/61.94 % Transform :cnf % 61.64/61.94 % Format :tptp:raw % 61.64/61.94 % Command :java -jar mcs_scs.jar %d %s % 61.64/61.94 % 61.64/61.94 % Result :Theorem 61.160000s % 61.64/61.94 % Output :CNFRefutation 61.160000s % 61.64/61.94 %------------------------------------------- % 61.64/61.95 %-------------------------------------------------------------------------- % 61.64/61.95 % File : GRP126-1.004 : TPTP v8.2.0. Released v1.2.0. % 61.64/61.95 % Domain : Group Theory (Quasigroups) % 61.64/61.95 % Problem : (a.b).(b.a) = b % 61.64/61.95 % Version : [Sla93] axioms. % 61.64/61.95 % English : Generate the multiplication table for the specified quasi- % 61.64/61.95 % group with 4 elements. % 61.64/61.95 % 61.64/61.95 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 61.64/61.95 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 61.64/61.95 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 61.64/61.95 % Source : [Sla93] % 61.64/61.95 % Names : QG4 [Sla93] % 61.64/61.95 % : QG4 [FSB93] % 61.64/61.95 % : QG4 [SFS95] % 61.64/61.95 % : Bennett QG4 [TPTP] % 61.64/61.95 % 61.64/61.95 % Status : Unsatisfiable % 61.64/61.95 % Rating : 0.00 v2.4.0, 0.00 v2.1.0 % 61.64/61.95 % Syntax : Number of clauses : 22 ( 17 unt; 1 nHn; 21 RR) % 61.64/61.95 % Number of literals : 35 ( 0 equ; 22 neg) % 61.64/61.95 % Maximal clause size : 6 ( 1 avg) % 61.64/61.95 % Maximal term depth : 1 ( 1 avg) % 61.64/61.95 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 61.64/61.95 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 61.64/61.95 % Number of variables : 19 ( 0 sgn) % 61.64/61.95 % SPC : CNF_UNS_EPR_NEQ_NHN % 61.64/61.95 % 61.64/61.95 % Comments : [SFS93]'s axiomatization has been modified for this. % 61.64/61.95 % : Substitution axioms are not needed, as any positive equality % 61.64/61.95 % literals should resolve on negative ones directly. % 61.64/61.95 % : tptp2X: -f tptp -s4 GRP126-1.g % 61.64/61.95 %-------------------------------------------------------------------------- % 61.64/61.95 cnf(element_1,axiom, % 61.64/61.95 group_element(e_1) ). % 61.64/61.95 % 61.64/61.95 cnf(element_2,axiom, % 61.64/61.95 group_element(e_2) ). % 61.64/61.95 % 61.64/61.95 cnf(element_3,axiom, % 61.64/61.95 group_element(e_3) ). % 61.64/61.95 % 61.64/61.95 cnf(element_4,axiom, % 61.64/61.95 group_element(e_4) ). % 61.64/61.95 % 61.64/61.95 cnf(e_1_is_not_e_2,axiom, % 61.64/61.95 ~ equalish(e_1,e_2) ). % 61.64/61.95 % 61.64/61.95 cnf(e_1_is_not_e_3,axiom, % 61.64/61.95 ~ equalish(e_1,e_3) ). % 61.64/61.95 % 61.64/61.95 cnf(e_1_is_not_e_4,axiom, % 61.64/61.95 ~ equalish(e_1,e_4) ). % 61.64/61.95 % 61.64/61.95 cnf(e_2_is_not_e_1,axiom, % 61.64/61.95 ~ equalish(e_2,e_1) ). % 61.64/61.95 % 61.64/61.95 cnf(e_2_is_not_e_3,axiom, % 61.64/61.95 ~ equalish(e_2,e_3) ). % 61.64/61.95 % 61.64/61.95 cnf(e_2_is_not_e_4,axiom, % 61.64/61.95 ~ equalish(e_2,e_4) ). % 61.64/61.95 % 61.64/61.95 cnf(e_3_is_not_e_1,axiom, % 61.64/61.95 ~ equalish(e_3,e_1) ). % 61.64/61.95 % 61.64/61.95 cnf(e_3_is_not_e_2,axiom, % 61.64/61.95 ~ equalish(e_3,e_2) ). % 61.64/61.95 % 61.64/61.95 cnf(e_3_is_not_e_4,axiom, % 61.64/61.95 ~ equalish(e_3,e_4) ). % 61.64/61.95 % 61.64/61.95 cnf(e_4_is_not_e_1,axiom, % 61.64/61.95 ~ equalish(e_4,e_1) ). % 61.64/61.95 % 61.64/61.95 cnf(e_4_is_not_e_2,axiom, % 61.64/61.95 ~ equalish(e_4,e_2) ). % 61.64/61.95 % 61.64/61.95 cnf(e_4_is_not_e_3,axiom, % 61.64/61.95 ~ equalish(e_4,e_3) ). % 61.64/61.95 % 61.64/61.95 cnf(product_total_function1,axiom, % 61.64/61.95 ( ~ group_element(X) % 61.64/61.95 | ~ group_element(Y) % 61.64/61.95 | product(X,Y,e_1) % 61.75/61.96 | product(X,Y,e_2) % 61.75/61.96 | product(X,Y,e_3) % 61.75/61.96 | product(X,Y,e_4) ) ). % 61.75/61.96 % 61.75/61.96 cnf(product_total_function2,axiom, % 61.75/61.96 ( ~ product(X,Y,W) % 61.75/61.96 | ~ product(X,Y,Z) % 61.75/61.96 | equalish(W,Z) ) ). % 61.75/61.96 % 61.75/61.96 cnf(product_right_cancellation,axiom, % 61.75/61.96 ( ~ product(X,W,Y) % 61.75/61.96 | ~ product(X,Z,Y) % 61.75/61.96 | equalish(W,Z) ) ). % 61.75/61.96 % 61.75/61.96 cnf(product_left_cancellation,axiom, % 61.75/61.96 ( ~ product(W,Y,X) % 61.75/61.96 | ~ product(Z,Y,X) % 61.75/61.96 | equalish(W,Z) ) ). % 61.75/61.96 % 61.75/61.96 cnf(product_idempotence,axiom, % 61.75/61.96 product(X,X,X) ). % 61.75/61.96 % 61.75/61.96 cnf(qg4,negated_conjecture, % 61.75/61.96 ( ~ product(X,Y,Z1) % 61.75/61.96 | ~ product(Y,X,Z2) % 61.75/61.96 | product(Z1,Z2,Y) ) ). % 61.75/61.96 % 61.75/61.96 %-------------------------------------------------------------------------- % 61.75/61.96 %------------------------------------------- % 61.75/61.96 % Proof found % 61.75/61.96 % SZS status Theorem for theBenchmark % 61.75/61.96 % SZS output start Proof % 61.75/61.96 %ClaNum:22(EqnAxiom:0) % 61.75/61.96 %VarNum:46(SingletonVarNum:19) % 61.75/61.96 %MaxLitNum:6 % 61.75/61.96 %MaxfuncDepth:0 % 61.75/61.96 %SharedTerms:20 % 61.75/61.96 %goalClause: 21 % 61.75/61.96 [1]P1(a1) % 61.75/61.96 [2]P1(a2) % 61.75/61.96 [3]P1(a3) % 61.75/61.96 [4]P1(a4) % 61.75/61.96 [6]~P2(a1,a2) % 61.75/61.96 [7]~P2(a1,a3) % 61.75/61.96 [8]~P2(a1,a4) % 61.75/61.96 [9]~P2(a2,a1) % 61.75/61.96 [10]~P2(a2,a3) % 61.75/61.96 [11]~P2(a2,a4) % 61.75/61.96 [12]~P2(a3,a1) % 61.75/61.96 [13]~P2(a3,a2) % 61.75/61.96 [14]~P2(a3,a4) % 61.75/61.96 [15]~P2(a4,a1) % 61.75/61.96 [16]~P2(a4,a2) % 61.75/61.96 [17]~P2(a4,a3) % 61.75/61.96 [5]P3(x51,x51,x51) % 61.75/61.96 [18]~P3(x183,x184,x181)+P2(x181,x182)+~P3(x183,x184,x182) % 61.75/61.96 [19]~P3(x193,x191,x194)+P2(x191,x192)+~P3(x193,x192,x194) % 61.75/61.96 [20]~P3(x201,x203,x204)+P2(x201,x202)+~P3(x202,x203,x204) % 61.75/61.96 [21]~P3(x214,x213,x211)+P3(x211,x212,x213)+~P3(x213,x214,x212) % 61.75/61.96 [22]~P1(x222)+~P1(x221)+P3(x221,x222,a2)+P3(x221,x222,a3)+P3(x221,x222,a4)+P3(x221,x222,a1) % 61.75/61.96 %EqnAxiom % 61.75/61.96 % 61.75/61.96 %------------------------------------------- % 61.87/62.10 cnf(86,plain, % 61.87/62.10 (~P3(a2,x861,a1)+~P3(x861,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[5,6,18,21])). % 61.87/62.10 cnf(147,plain, % 61.87/62.10 (~P3(a1,x1471,a3)+~P3(x1471,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[7,5,18,21])). % 61.87/62.10 cnf(208,plain, % 61.87/62.10 (~P3(a4,x2081,a1)+~P3(x2081,a4,a1)), % 61.87/62.10 inference(scs_inference,[],[8,5,18,21])). % 61.87/62.10 cnf(269,plain, % 61.87/62.10 (~P3(a1,x2691,a2)+~P3(x2691,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[9,5,18,21])). % 61.87/62.10 cnf(330,plain, % 61.87/62.10 (~P3(a2,x3301,a3)+~P3(x3301,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[10,5,18,21])). % 61.87/62.10 cnf(391,plain, % 61.87/62.10 (~P3(a2,x3911,a4)+~P3(x3911,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[11,5,18,21])). % 61.87/62.10 cnf(452,plain, % 61.87/62.10 (~P3(a3,x4521,a1)+~P3(x4521,a3,a1)), % 61.87/62.10 inference(scs_inference,[],[12,5,18,21])). % 61.87/62.10 cnf(513,plain, % 61.87/62.10 (~P3(a3,x5131,a2)+~P3(x5131,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[13,5,18,21])). % 61.87/62.10 cnf(574,plain, % 61.87/62.10 (~P3(a4,x5741,a3)+~P3(x5741,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[14,5,18,21])). % 61.87/62.10 cnf(635,plain, % 61.87/62.10 (~P3(a1,x6351,a4)+~P3(x6351,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[15,5,18,21])). % 61.87/62.10 cnf(696,plain, % 61.87/62.10 (~P3(a4,x6961,a2)+~P3(x6961,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[16,5,18,21])). % 61.87/62.10 cnf(757,plain, % 61.87/62.10 (~P3(a3,x7571,a4)+~P3(x7571,a3,a4)), % 61.87/62.10 inference(scs_inference,[],[17,5,18,21])). % 61.87/62.10 cnf(848,plain, % 61.87/62.10 (~P3(a1,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[5,6,19,21])). % 61.87/62.10 cnf(894,plain, % 61.87/62.10 (~P3(a3,a3,a1)), % 61.87/62.10 inference(scs_inference,[],[7,5,19,21])). % 61.87/62.10 cnf(940,plain, % 61.87/62.10 (~P3(a1,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[8,5,19,21])). % 61.87/62.10 cnf(971,plain, % 61.87/62.10 (~P3(a2,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[9,5,19,21])). % 61.87/62.10 cnf(1002,plain, % 61.87/62.10 (~P3(a3,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[10,5,19,21])). % 61.87/62.10 cnf(1033,plain, % 61.87/62.10 (~P3(a4,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[11,5,19,21])). % 61.87/62.10 cnf(1079,plain, % 61.87/62.10 (~P3(a1,a3,a1)+P3(a1,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[12,848,940,1,19,22])). % 61.87/62.10 cnf(1125,plain, % 61.87/62.10 (~P3(a1,a3,a1)), % 61.87/62.10 inference(scs_inference,[],[1079,147])). % 61.87/62.10 cnf(1171,plain, % 61.87/62.10 (~P3(a2,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[13,5,19,21])). % 61.87/62.10 cnf(1217,plain, % 61.87/62.10 (~P3(a3,a3,a4)), % 61.87/62.10 inference(scs_inference,[],[14,5,19,21])). % 61.87/62.10 cnf(1263,plain, % 61.87/62.10 (~P3(a4,a1,a4)+P3(a4,a4,a1)+P3(a4,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[15,1033,4,19,22])). % 61.87/62.10 cnf(1309,plain, % 61.87/62.10 (P3(a4,a4,a3)+~P3(a4,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[1263,208])). % 61.87/62.10 cnf(1355,plain, % 61.87/62.10 (~P3(a4,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[1309,574])). % 61.87/62.10 cnf(1401,plain, % 61.87/62.10 (~P3(a2,a1,a2)+P3(a2,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[6,971,1171,2,19,22])). % 61.87/62.10 cnf(1447,plain, % 61.87/62.10 (~P3(a2,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[1401,391])). % 61.87/62.10 cnf(1493,plain, % 61.87/62.10 (~P3(a1,a2,a1)+P3(a1,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[6,848,940,1,19,22])). % 61.87/62.10 cnf(1539,plain, % 61.87/62.10 (~P3(a1,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[1493,147])). % 61.87/62.10 cnf(1723,plain, % 61.87/62.10 (~P3(a3,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[7,1002,894,1217,3,19,22])). % 61.87/62.10 cnf(1769,plain, % 61.87/62.10 (P3(a1,a3,a2)+P3(a1,a3,a4)+P3(a1,a3,a3)), % 61.87/62.10 inference(scs_inference,[],[7,5,3,1,19,22])). % 61.87/62.10 cnf(1815,plain, % 61.87/62.10 (~P3(a3,a1,a2)+P3(a1,a3,a4)+P3(a1,a3,a3)), % 61.87/62.10 inference(scs_inference,[],[1769,269])). % 61.87/62.10 cnf(1951,plain, % 61.87/62.10 (P3(a1,a2,a4)+P3(a1,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[5,9,1539,2,1,20,22])). % 61.87/62.10 cnf(1997,plain, % 61.87/62.10 (P3(a1,a2,a3)+~P3(a2,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[1951,391])). % 61.87/62.10 cnf(2043,plain, % 61.87/62.10 (~P3(a2,a1,a4)+~P3(a2,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[1997,147])). % 61.87/62.10 cnf(2089,plain, % 61.87/62.10 (~P3(a4,x20891,a1)+~P3(x20891,a4,a2)+~P3(a2,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[2043,21])). % 61.87/62.10 cnf(2180,plain, % 61.87/62.10 (P3(a1,a2,a4)+~P3(a2,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[1951,147])). % 61.87/62.10 cnf(8830,plain, % 61.87/62.10 (P3(a2,a1,a4)+P3(a2,a1,a3)+P3(a2,a1,a1)), % 61.87/62.10 inference(scs_inference,[],[1447,5,2,1,18,22])). % 61.87/62.10 cnf(8849,plain, % 61.87/62.10 (~P3(a1,a2,a4)+P3(a2,a1,a3)+P3(a2,a1,a1)), % 61.87/62.10 inference(scs_inference,[],[1033,8830,21])). % 61.87/62.10 cnf(8895,plain, % 61.87/62.10 (~P3(a1,a2,a3)+P3(a2,a1,a1)+~P3(a1,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[894,8849,21])). % 61.87/62.10 cnf(8941,plain, % 61.87/62.10 (~P3(a1,a2,a3)+~P3(a1,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[1125,8895,21])). % 61.87/62.10 cnf(118634,plain, % 61.87/62.10 (~P3(a4,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[17,5,18])). % 61.87/62.10 cnf(118635,plain, % 61.87/62.10 (P3(x1186351,x1186351,x1186351)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118637,plain, % 61.87/62.10 (~P3(a4,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[16,17,5,118635,18,19])). % 61.87/62.10 cnf(118638,plain, % 61.87/62.10 (P3(x1186381,x1186381,x1186381)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118640,plain, % 61.87/62.10 (~P3(a2,a4,a4)), % 61.87/62.10 inference(scs_inference,[],[16,17,5,118635,118638,18,19,20])). % 61.87/62.10 cnf(118643,plain, % 61.87/62.10 (P3(a4,a1,a1)+P3(a4,a1,a2)+P3(a4,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[1,16,17,1355,5,118635,118638,4,18,19,20,22])). % 61.87/62.10 cnf(118645,plain, % 61.87/62.10 (P3(x1186451,x1186451,x1186451)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118647,plain, % 61.87/62.10 (~P3(a4,a1,a1)), % 61.87/62.10 inference(scs_inference,[],[8,11,5,118645,18,20])). % 61.87/62.10 cnf(118648,plain, % 61.87/62.10 (P3(x1186481,x1186481,x1186481)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118650,plain, % 61.87/62.10 (~P3(a1,a4,a1)), % 61.87/62.10 inference(scs_inference,[],[8,11,5,118645,118648,18,20,19])). % 61.87/62.10 cnf(118653,plain, % 61.87/62.10 (P3(a3,a1,a4)+P3(a3,a1,a2)+P3(a3,a1,a1)), % 61.87/62.10 inference(scs_inference,[],[1,1723,3,8,11,5,118645,118648,18,20,19,22])). % 61.87/62.10 cnf(118654,plain, % 61.87/62.10 (P3(a4,a1,a3)+P3(a4,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118647,118643])). % 61.87/62.10 cnf(118655,plain, % 61.87/62.10 (~P3(a2,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[10,5,19])). % 61.87/62.10 cnf(118656,plain, % 61.87/62.10 (P3(x1186561,x1186561,x1186561)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118658,plain, % 61.87/62.10 (~P3(a3,a2,a2)), % 61.87/62.10 inference(scs_inference,[],[10,5,118656,19,20])). % 61.87/62.10 cnf(118662,plain, % 61.87/62.10 (~P3(a3,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[13,5,19])). % 61.87/62.10 cnf(118663,plain, % 61.87/62.10 (P3(x1186631,x1186631,x1186631)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118665,plain, % 61.87/62.10 (~P3(a1,a3,a3)), % 61.87/62.10 inference(scs_inference,[],[12,13,5,118663,19,20])). % 61.87/62.10 cnf(118668,plain, % 61.87/62.10 (P3(a1,a3,a4)+P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[12,13,5,118663,19,20,1769])). % 61.87/62.10 cnf(118669,plain, % 61.87/62.10 (~P3(a3,a1,a4)+P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118634,12,13,5,118663,19,20,1769,21])). % 61.87/62.10 cnf(118671,plain, % 61.87/62.10 (P3(a1,a3,a2)+P3(a3,a1,a1)+P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118634,12,13,5,118663,19,20,1769,21,118653])). % 61.87/62.10 cnf(118672,plain, % 61.87/62.10 (P3(a1,a3,a4)+~P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118665,1815])). % 61.87/62.10 cnf(118673,plain, % 61.87/62.10 (~P3(a3,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[14,5,19])). % 61.87/62.10 cnf(118674,plain, % 61.87/62.10 (P3(x1186741,x1186741,x1186741)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118676,plain, % 61.87/62.10 (~P3(a4,a3,a3)), % 61.87/62.10 inference(scs_inference,[],[14,5,118674,19,20])). % 61.87/62.10 cnf(118680,plain, % 61.87/62.10 (~P3(a4,a3,a4)), % 61.87/62.10 inference(scs_inference,[],[17,5,19])). % 61.87/62.10 cnf(118681,plain, % 61.87/62.10 (P3(x1186811,x1186811,x1186811)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118686,plain, % 61.87/62.10 (P3(a1,a4,a3)+P3(a1,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[1,118650,15,17,5,118681,4,19,20,22])). % 61.87/62.10 cnf(118690,plain, % 61.87/62.10 (P3(a4,a1,a2)+P3(a1,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[1,118650,15,17,5,118681,4,19,20,22,147,118654])). % 61.87/62.10 cnf(118694,plain, % 61.87/62.10 (P3(x1186941,x1186941,x1186941)), % 61.87/62.10 inference(rename_variables,[],[5])). % 61.87/62.10 cnf(118696,plain, % 61.87/62.10 (~P3(a1,a2,a2)), % 61.87/62.10 inference(scs_inference,[],[9,11,5,118694,19,20])). % 61.87/62.10 cnf(118699,plain, % 61.87/62.10 (P3(a2,a4,a3)+P3(a2,a4,a1)), % 61.87/62.10 inference(scs_inference,[],[118640,9,11,2,5,118694,4,19,20,22])). % 61.87/62.10 cnf(118703,plain, % 61.87/62.10 (~P3(a2,a3,a3)), % 61.87/62.10 inference(scs_inference,[],[13,5,20])). % 61.87/62.10 cnf(118706,plain, % 61.87/62.10 (P3(a4,a3,a1)+P3(a4,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118680,118676,13,3,5,4,20,22])). % 61.87/62.10 cnf(118708,plain, % 61.87/62.10 (P3(a4,a3,a2)+~P3(a3,a4,a1)), % 61.87/62.10 inference(scs_inference,[],[118680,118676,13,3,5,4,20,22,208])). % 61.87/62.10 cnf(118710,plain, % 61.87/62.10 (~P3(a2,a1,a3)+P3(a4,a3,a2)+~P3(a3,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[118680,118676,13,3,5,4,20,22,208,2089])). % 61.87/62.10 cnf(118711,plain, % 61.87/62.10 (~P3(a3,a4,a4)), % 61.87/62.10 inference(scs_inference,[],[17,5,20])). % 61.87/62.10 cnf(118714,plain, % 61.87/62.10 (P3(a2,a3,a1)+P3(a2,a3,a4)), % 61.87/62.10 inference(scs_inference,[],[118703,118655,17,3,2,5,20,22])). % 61.87/62.10 cnf(118716,plain, % 61.87/62.10 (P3(a2,a3,a4)+~P3(a3,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118703,118655,17,3,2,5,20,22,86])). % 61.87/62.10 cnf(118718,plain, % 61.87/62.10 (~P3(a4,a2,a2)), % 61.87/62.10 inference(scs_inference,[],[11,5,20])). % 61.87/62.10 cnf(118721,plain, % 61.87/62.10 (~P3(a2,a1,a1)), % 61.87/62.10 inference(scs_inference,[],[6,5,20])). % 61.87/62.10 cnf(118724,plain, % 61.87/62.10 (P3(a2,a1,a3)+P3(a2,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[6,5,20,8830])). % 61.87/62.10 cnf(118725,plain, % 61.87/62.10 (~P3(a1,a2,a3)+P3(a2,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[1002,6,5,20,8830,21])). % 61.87/62.10 cnf(118727,plain, % 61.87/62.10 (P3(a2,a1,a4)+P3(a1,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[1,118696,1002,1539,6,2,5,20,8830,21,22])). % 61.87/62.10 cnf(118731,plain, % 61.87/62.10 (P3(a2,a1,a4)+P3(a4,a3,a2)+~P3(a3,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[1,118696,1002,1539,6,2,5,20,8830,21,22,635,118710])). % 61.87/62.10 cnf(118732,plain, % 61.87/62.10 (P3(a2,a1,a3)+~P3(a1,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[118721,8849])). % 61.87/62.10 cnf(118733,plain, % 61.87/62.10 (~P3(a3,a1,a1)), % 61.87/62.10 inference(scs_inference,[],[7,5,20])). % 61.87/62.10 cnf(118736,plain, % 61.87/62.10 (P3(a1,a3,a2)+P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[7,5,20,118671])). % 61.87/62.10 cnf(118737,plain, % 61.87/62.10 (P3(a3,a1,a4)+P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118733,118653])). % 61.87/62.10 cnf(118738,plain, % 61.87/62.10 (P3(a3,a4,a1)+P3(a3,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[118711,118673,3,4,22])). % 61.87/62.10 cnf(118740,plain, % 61.87/62.10 (P3(a3,a4,a2)+~P3(a4,a3,a1)), % 61.87/62.10 inference(scs_inference,[],[118711,118673,3,4,22,452])). % 61.87/62.10 cnf(118742,plain, % 61.87/62.10 (~P3(a4,a3,a2)+P3(a1,a3,a4)), % 61.87/62.10 inference(scs_inference,[],[8,118668,20])). % 61.87/62.10 cnf(118743,plain, % 61.87/62.10 (P3(a3,a2,a1)+P3(a3,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[118662,118658,3,2,22])). % 61.87/62.10 cnf(118745,plain, % 61.87/62.10 (P3(a3,a2,a4)+~P3(a2,a3,a1)), % 61.87/62.10 inference(scs_inference,[],[118662,118658,3,2,22,452])). % 61.87/62.10 cnf(118748,plain, % 61.87/62.10 (~P3(a3,a1,a4)+~P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118669,269])). % 61.87/62.10 cnf(118749,plain, % 61.87/62.10 (~P3(a1,a2,a4)+~P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[10,118672,19])). % 61.87/62.10 cnf(118750,plain, % 61.87/62.10 (P3(a1,a4,a3)+~P3(a4,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118686,696])). % 61.87/62.10 cnf(118753,plain, % 61.87/62.10 (~P3(a4,a2,a1)+P3(a2,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118699,86])). % 61.87/62.10 cnf(118755,plain, % 61.87/62.10 (P3(a4,a3,a1)+~P3(a3,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[118706,513])). % 61.87/62.10 cnf(118756,plain, % 61.87/62.10 (P3(a4,a2,a3)+P3(a4,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118718,118637,2,4,22])). % 61.87/62.10 cnf(118758,plain, % 61.87/62.10 (P3(a4,a2,a1)+~P3(a2,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118718,118637,2,4,22,574])). % 61.87/62.10 cnf(118760,plain, % 61.87/62.10 (P3(a2,a4,a1)+P3(a4,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118718,118637,2,4,22,574,118699])). % 61.87/62.10 cnf(118766,plain, % 61.87/62.10 (~P3(a3,a2,a1)+~P3(a3,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[118716,757])). % 61.87/62.10 cnf(118767,plain, % 61.87/62.10 (P3(a2,a1,a3)+P3(a1,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[118724,1997])). % 61.87/62.10 cnf(118768,plain, % 61.87/62.10 (~P3(a3,a1,a4)+~P3(a1,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[13,118725,20])). % 61.87/62.10 cnf(118769,plain, % 61.87/62.10 (P3(a2,a1,a4)+~P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118727,118749])). % 61.87/62.10 cnf(118770,plain, % 61.87/62.10 (~P3(a2,a4,a3)+~P3(a1,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[8,118732,19])). % 61.87/62.10 cnf(118772,plain, % 61.87/62.10 (P3(a3,a1,a4)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118737,513])). % 61.87/62.10 cnf(118773,plain, % 61.87/62.10 (P3(a3,a4,a1)+~P3(a4,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118738,696])). % 61.87/62.10 cnf(118775,plain, % 61.87/62.10 (~P3(a4,a3,a2)+~P3(a3,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[118742,635])). % 61.87/62.10 cnf(118776,plain, % 61.87/62.10 (P3(a3,a2,a1)+~P3(a2,a3,a4)), % 61.87/62.10 inference(scs_inference,[],[118743,391])). % 61.87/62.10 cnf(118779,plain, % 61.87/62.10 (~P3(a2,a4,a3)+~P3(a4,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[6,118750,20])). % 61.87/62.10 cnf(118782,plain, % 61.87/62.10 (~P3(a2,a4,a3)+~P3(a2,a4,a1)), % 61.87/62.10 inference(scs_inference,[],[118758,86])). % 61.87/62.10 cnf(118787,plain, % 61.87/62.10 (~P3(a4,a1,a3)+P3(a1,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[16,118767,20])). % 61.87/62.10 cnf(118788,plain, % 61.87/62.10 (P3(a3,a1,a2)+~P3(a1,a2,a3)), % 61.87/62.10 inference(scs_inference,[],[118768,118737])). % 61.87/62.10 cnf(118789,plain, % 61.87/62.10 (P3(a1,a2,a3)+~P3(a3,a1,a2)), % 61.87/62.10 inference(scs_inference,[],[118769,1997])). % 61.87/62.10 cnf(118790,plain, % 61.87/62.10 (P3(a1,a2,a3)+~P3(a2,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118770,1951])). % 61.87/62.10 cnf(118791,plain, % 61.87/62.10 (~P3(a1,a3,a4)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118772,635])). % 61.87/62.10 cnf(118793,plain, % 61.87/62.10 (P3(a3,a1,a2)+~P3(a4,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118775,118737])). % 61.87/62.10 cnf(118796,plain, % 61.87/62.10 (P3(a4,a1,a3)+~P3(a2,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118779,118654])). % 61.87/62.10 cnf(118798,plain, % 61.87/62.10 (~P3(a4,a1,a3)+~P3(a2,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[118787,147])). % 61.87/62.10 cnf(118799,plain, % 61.87/62.10 (~P3(a1,a2,a3)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118788,269])). % 61.87/62.10 cnf(118800,plain, % 61.87/62.10 (~P3(a3,a1,a2)+~P3(a2,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[118789,330])). % 61.87/62.10 cnf(118801,plain, % 61.87/62.10 (P3(a2,a1,a4)+~P3(a2,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118790,118725])). % 61.87/62.10 cnf(118804,plain, % 61.87/62.10 (~P3(a4,a3,a2)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118793,513])). % 61.87/62.10 cnf(118805,plain, % 61.87/62.10 (~P3(a2,a4,a3)+~P3(a1,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118796,147])). % 61.87/62.10 cnf(118806,plain, % 61.87/62.10 (P3(a2,a1,a4)+~P3(a4,a1,a3)), % 61.87/62.10 inference(scs_inference,[],[118798,118724])). % 61.87/62.10 cnf(118807,plain, % 61.87/62.10 (P3(a1,a2,a4)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118799,1951])). % 61.87/62.10 cnf(118808,plain, % 61.87/62.10 (~P3(a2,a1,a3)+P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118800,118736])). % 61.87/62.10 cnf(118809,plain, % 61.87/62.10 (~P3(a2,a1,a3)+~P3(a2,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118801,2043])). % 61.87/62.10 cnf(118810,plain, % 61.87/62.10 (~P3(a2,a1,a3)+~P3(a4,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118804,118808])). % 61.87/62.10 cnf(118811,plain, % 61.87/62.10 (P3(a2,a4,a1)+~P3(a1,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118805,118699])). % 61.87/62.10 cnf(118812,plain, % 61.87/62.10 (~P3(a4,a1,a3)+~P3(a1,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[118806,391])). % 61.87/62.10 cnf(118813,plain, % 61.87/62.10 (~P3(a1,a3,a2)+~P3(a2,a1,a4)), % 61.87/62.10 inference(scs_inference,[],[118807,635])). % 61.87/62.10 cnf(118814,plain, % 61.87/62.10 (~P3(a2,a1,a3)+~P3(a4,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118809,118753])). % 61.87/62.10 cnf(118815,plain, % 61.87/62.10 (P3(a2,a1,a4)+~P3(a4,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118810,118724])). % 61.87/62.10 cnf(118816,plain, % 61.87/62.10 (~P3(a4,a2,a1)+~P3(a1,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118811,86])). % 61.87/62.10 cnf(118817,plain, % 61.87/62.10 (~P3(a4,a1,a3)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118812,118807])). % 61.87/62.10 cnf(118818,plain, % 61.87/62.10 (~P3(a1,a3,a2)+~P3(a2,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118813,118801])). % 61.87/62.10 cnf(118819,plain, % 61.87/62.10 (~P3(a1,a2,a4)+~P3(a4,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118814,118732])). % 61.87/62.10 cnf(118820,plain, % 61.87/62.10 (P3(a1,a2,a3)+~P3(a4,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118815,1997])). % 61.87/62.10 cnf(118821,plain, % 61.87/62.10 (P3(a4,a2,a3)+~P3(a1,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118816,118756])). % 61.87/62.10 cnf(118822,plain, % 61.87/62.10 (P3(a4,a1,a2)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118817,118654])). % 61.87/62.10 cnf(118823,plain, % 61.87/62.10 (P3(a2,a4,a1)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118818,118699])). % 61.87/62.10 cnf(118824,plain, % 61.87/62.10 (P3(a1,a2,a3)+~P3(a4,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118819,1951])). % 61.87/62.10 cnf(118825,plain, % 61.87/62.10 (~P3(a1,a2,a4)+~P3(a4,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118820,8941])). % 61.87/62.10 cnf(118826,plain, % 61.87/62.10 (~P3(a1,a2,a3)+~P3(a1,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[15,118821,20])). % 61.87/62.10 cnf(118827,plain, % 61.87/62.10 (~P3(a1,a3,a2)+~P3(a1,a4,a2)), % 61.87/62.10 inference(scs_inference,[],[118822,269])). % 61.87/62.10 cnf(118828,plain, % 61.87/62.10 (~P3(a1,a3,a2)+~P3(a4,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118823,208])). % 61.87/62.10 cnf(118829,plain, % 61.87/62.10 (P3(a2,a1,a4)+~P3(a4,a2,a1)), % 61.87/62.10 inference(scs_inference,[],[118824,118725])). % 61.87/62.10 cnf(118830,plain, % 61.87/62.10 (P3(a4,a3,a1)+~P3(a1,a2,a4)), % 61.87/62.10 inference(scs_inference,[],[118825,118706])). % 61.87/62.10 cnf(118831,plain, % 61.87/62.10 (P3(a2,a1,a3)+~P3(a1,a4,a3)), % 61.87/62.10 inference(scs_inference,[],[118826,118767])). % 61.87/62.10 cnf(118832,plain, % 61.87/62.10 (P3(a1,a4,a3)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118827,118686])). % 61.87/62.10 cnf(118833,plain, % 61.87/62.10 (P3(a4,a2,a3)+~P3(a1,a3,a2)), % 61.87/62.10 inference(scs_inference,[],[118828,118756])). % 61.87/62.10 cnf(118834,plain, % 61.87/62.10 (~P3(a2,a3,a4)+~P3(a4,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[7,118829,19])). % 61.87/62.11 cnf(118835,plain, % 61.87/62.11 (~P3(a1,a2,a4)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118830,452])). % 61.87/62.11 cnf(118836,plain, % 61.87/62.11 (~P3(a2,a1,a4)+~P3(a1,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118831,2043])). % 61.87/62.11 cnf(118837,plain, % 61.87/62.11 (P3(a2,a1,a3)+~P3(a1,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[118832,118831])). % 61.87/62.11 cnf(118838,plain, % 61.87/62.11 (P3(a1,a3,a4)+P3(a4,a2,a3)), % 61.87/62.11 inference(scs_inference,[],[118833,118668])). % 61.87/62.11 cnf(118839,plain, % 61.87/62.11 (~P3(a2,a4,a3)+~P3(a2,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118834,118758])). % 61.87/62.11 cnf(118840,plain, % 61.87/62.11 (~P3(a2,a1,a3)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118835,2180])). % 61.87/62.11 cnf(118841,plain, % 61.87/62.11 (P3(a1,a2,a4)+~P3(a1,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118836,118727])). % 61.87/62.11 cnf(118842,plain, % 61.87/62.11 (~P3(a1,a3,a2)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118837,118840])). % 61.87/62.11 cnf(118843,plain, % 61.87/62.11 (P3(a4,a2,a3)+~P3(a3,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[118838,757])). % 61.87/62.11 cnf(118844,plain, % 61.87/62.11 (P3(a2,a4,a1)+~P3(a2,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118839,118699])). % 61.87/62.11 cnf(118845,plain, % 61.87/62.11 (~P3(a3,a1,a2)+~P3(a1,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118841,118749])). % 61.87/62.11 cnf(118846,plain, % 61.87/62.11 (~P3(a3,a1,a4)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118842,118669])). % 61.87/62.11 cnf(118847,plain, % 61.87/62.11 (~P3(a3,a1,a4)+~P3(a2,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118843,330])). % 61.87/62.11 cnf(118848,plain, % 61.87/62.11 (P3(a2,a4,a1)+P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118844,118714])). % 61.87/62.11 cnf(118849,plain, % 61.87/62.11 (P3(a1,a3,a2)+~P3(a1,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118845,118736])). % 61.87/62.11 cnf(118850,plain, % 61.87/62.11 (P3(a3,a1,a2)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118846,118737])). % 61.87/62.11 cnf(118851,plain, % 61.87/62.11 (P3(a3,a1,a2)+~P3(a2,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118847,118737])). % 61.87/62.11 cnf(118852,plain, % 61.87/62.11 (P3(a2,a3,a1)+~P3(a2,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118848,118782])). % 61.87/62.11 cnf(118853,plain, % 61.87/62.11 (P3(a3,a1,a4)+~P3(a1,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118849,118772])). % 61.87/62.11 cnf(118854,plain, % 61.87/62.11 (P3(a1,a3,a4)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118850,118672])). % 61.87/62.11 cnf(118855,plain, % 61.87/62.11 (P3(a1,a3,a4)+~P3(a2,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118851,118672])). % 61.87/62.11 cnf(118856,plain, % 61.87/62.11 (P3(a3,a2,a4)+~P3(a2,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118852,118745])). % 61.87/62.11 cnf(118858,plain, % 61.87/62.11 (P3(a1,a3,a4)+P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118854,118738])). % 61.87/62.11 cnf(118859,plain, % 61.87/62.11 (P3(a1,a3,a4)+~P3(a4,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[118855,118753])). % 61.87/62.11 cnf(118860,plain, % 61.87/62.11 (~P3(a2,a4,a3)+~P3(a3,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[118856,118766])). % 61.87/62.11 cnf(118862,plain, % 61.87/62.11 (P3(a3,a4,a2)+~P3(a1,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[118858,118791])). % 61.87/62.11 cnf(118863,plain, % 61.87/62.11 (~P3(a4,a2,a1)+~P3(a3,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[118859,635])). % 61.87/62.11 cnf(118864,plain, % 61.87/62.11 (~P3(a4,a2,a1)+~P3(a3,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[118860,118753])). % 61.87/62.11 cnf(118866,plain, % 61.87/62.11 (P3(a4,a3,a1)+~P3(a1,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[118862,118755])). % 61.87/62.11 cnf(118867,plain, % 61.87/62.11 (P3(a3,a1,a2)+~P3(a4,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[118863,118737])). % 61.87/62.11 cnf(118868,plain, % 61.87/62.11 (P3(a2,a4,a1)+~P3(a3,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[118864,118760])). % 61.87/62.11 cnf(118870,plain, % 61.87/62.11 (P3(a4,a3,a1)+P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118866,118668])). % 61.87/62.11 cnf(118871,plain, % 61.87/62.11 (~P3(a3,a4,a2)+~P3(a4,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[8,118867,19])). % 61.87/62.11 cnf(118872,plain, % 61.87/62.11 (P3(a3,a2,a4)+P3(a2,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118868,118743])). % 61.87/62.11 cnf(118874,plain, % 61.87/62.11 (P3(a4,a3,a1)+~P3(a3,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[118870,757])). % 61.87/62.11 cnf(118875,plain, % 61.87/62.11 (~P3(a2,a4,a3)+~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118871,118758])). % 61.87/62.11 cnf(118876,plain, % 61.87/62.11 (~P3(a1,a2,a4)+P3(a2,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[12,118872,20])). % 61.87/62.11 cnf(118878,plain, % 61.87/62.11 (P3(a3,a4,a2)+~P3(a3,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[118874,118740])). % 61.87/62.11 cnf(118880,plain, % 61.87/62.11 (~P3(a2,a3,a1)+~P3(a1,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[14,118876,19])). % 61.87/62.11 cnf(118883,plain, % 61.87/62.11 (P3(a1,a2,a3)+~P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118880,1951])). % 61.87/62.11 cnf(118886,plain, % 61.87/62.11 (~P3(a2,a3,a1)+~P3(a2,a1,a3)), % 61.87/62.11 inference(scs_inference,[],[118883,147])). % 61.87/62.11 cnf(118889,plain, % 61.87/62.11 (P3(a2,a1,a4)+~P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118886,118724])). % 61.87/62.11 cnf(118892,plain, % 61.87/62.11 (~P3(a1,a3,a2)+~P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118889,118813])). % 61.87/62.11 cnf(118895,plain, % 61.87/62.11 (~P3(a3,a1,a4)+~P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118892,118669])). % 61.87/62.11 cnf(118897,plain, % 61.87/62.11 (P3(a3,a1,a2)+~P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118895,118737])). % 61.87/62.11 cnf(118899,plain, % 61.87/62.11 (P3(a1,a3,a4)+~P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118897,118672])). % 61.87/62.11 cnf(118901,plain, % 61.87/62.11 (P3(a1,a3,a4)+P3(a2,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118899,118714])). % 61.87/62.11 cnf(118903,plain, % 61.87/62.11 (P3(a1,a3,a4)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118901,391])). % 61.87/62.11 cnf(118905,plain, % 61.87/62.11 (~P3(a3,a2,a4)+~P3(a3,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[118903,635])). % 61.87/62.11 cnf(118907,plain, % 61.87/62.11 (~P3(a1,a3,a2)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118905,118772])). % 61.87/62.11 cnf(118909,plain, % 61.87/62.11 (P3(a3,a1,a2)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118907,118736])). % 61.87/62.11 cnf(118911,plain, % 61.87/62.11 (~P3(a1,a2,a4)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118909,118749])). % 61.87/62.11 cnf(118912,plain, % 61.87/62.11 (P3(a1,a2,a3)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118911,1951])). % 61.87/62.11 cnf(118913,plain, % 61.87/62.11 (~P3(a3,a2,a4)+~P3(a2,a1,a3)), % 61.87/62.11 inference(scs_inference,[],[118912,147])). % 61.87/62.11 cnf(118914,plain, % 61.87/62.11 (P3(a2,a1,a4)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118913,118724])). % 61.87/62.11 cnf(118915,plain, % 61.87/62.11 (~P3(a3,a2,a4)+~P3(a1,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[118914,118836])). % 61.87/62.11 cnf(118916,plain, % 61.87/62.11 (P3(a1,a4,a2)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118915,118686])). % 61.87/62.11 cnf(118917,plain, % 61.87/62.11 (~P3(a3,a2,a4)+~P3(a4,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[118916,269])). % 61.87/62.11 cnf(118918,plain, % 61.87/62.11 (P3(a4,a1,a3)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118917,118654])). % 61.87/62.11 cnf(118919,plain, % 61.87/62.11 (~P3(a4,a2,a3)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[6,118918,19])). % 61.87/62.11 cnf(118920,plain, % 61.87/62.11 (P3(a4,a2,a1)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118919,118756])). % 61.87/62.11 cnf(118921,plain, % 61.87/62.11 (~P3(a3,a2,a4)+~P3(a2,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118920,86])). % 61.87/62.11 cnf(118922,plain, % 61.87/62.11 (P3(a2,a4,a3)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118921,118699])). % 61.87/62.11 cnf(118923,plain, % 61.87/62.11 (~P3(a3,a4,a2)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118922,118875])). % 61.87/62.11 cnf(118924,plain, % 61.87/62.11 (P3(a3,a4,a1)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118923,118738])). % 61.87/62.11 cnf(118925,plain, % 61.87/62.11 (~P3(a3,a2,a4)+~P3(a4,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118924,208])). % 61.87/62.11 cnf(118926,plain, % 61.87/62.11 (P3(a4,a3,a2)+~P3(a3,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118925,118706])). % 61.87/62.11 cnf(118927,plain, % 61.87/62.11 (P3(a4,a3,a2)+P3(a3,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[118926,118743])). % 61.87/62.11 cnf(118928,plain, % 61.87/62.11 (P3(a3,a2,a1)+~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118927,513])). % 61.87/62.11 cnf(118929,plain, % 61.87/62.11 (~P3(a3,a4,a2)+~P3(a2,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[118928,452])). % 61.87/62.11 cnf(118930,plain, % 61.87/62.11 (P3(a2,a3,a4)+~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118929,118714])). % 61.87/62.11 cnf(118931,plain, % 61.87/62.11 (~P3(a1,a3,a4)+~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[9,118930,20])). % 61.87/62.11 cnf(118932,plain, % 61.87/62.11 (~P3(a4,a3,a1)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118931,118740])). % 61.87/62.11 cnf(118933,plain, % 61.87/62.11 (~P3(a1,a2,a4)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118932,118830])). % 61.87/62.11 cnf(118934,plain, % 61.87/62.11 (~P3(a2,a1,a3)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118933,2180])). % 61.87/62.11 cnf(118935,plain, % 61.87/62.11 (P3(a1,a2,a3)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118934,118767])). % 61.87/62.11 cnf(118936,plain, % 61.87/62.11 (P3(a2,a1,a4)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118935,118725])). % 61.87/62.11 cnf(118937,plain, % 61.87/62.11 (~P3(a1,a4,a3)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118936,118836])). % 61.87/62.11 cnf(118938,plain, % 61.87/62.11 (~P3(a4,a1,a2)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118937,118750])). % 61.87/62.11 cnf(118939,plain, % 61.87/62.11 (P3(a1,a4,a2)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118938,118690])). % 61.87/62.11 cnf(118940,plain, % 61.87/62.11 (P3(a1,a4,a2)+P3(a1,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[118939,118668])). % 61.87/62.11 cnf(118941,plain, % 61.87/62.11 (P3(a1,a4,a2)+P3(a3,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[118940,118772])). % 61.87/62.11 cnf(118942,plain, % 61.87/62.11 (P3(a1,a4,a2)+~P3(a3,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[118941,118748])). % 61.87/62.11 cnf(118943,plain, % 61.87/62.11 (~P3(a3,a1,a2)+~P3(a4,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[118942,696])). % 61.87/62.11 cnf(118944,plain, % 61.87/62.11 (P3(a4,a1,a3)+~P3(a3,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[118943,118654])). % 61.87/62.11 cnf(118945,plain, % 61.87/62.11 (P3(a4,a1,a3)+P3(a1,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[118944,118736])). % 61.87/62.11 cnf(118946,plain, % 61.87/62.11 (P3(a4,a1,a3)+~P3(a1,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118945,118791])). % 61.87/62.11 cnf(118947,plain, % 61.87/62.11 (P3(a4,a1,a3)+~P3(a4,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[118946,118742])). % 61.87/62.11 cnf(118948,plain, % 61.87/62.11 (P3(a4,a1,a3)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118947,118708])). % 61.87/62.11 cnf(118949,plain, % 61.87/62.11 (P3(a1,a2,a3)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118948,118787])). % 61.87/62.11 cnf(118950,plain, % 61.87/62.11 (P3(a2,a1,a4)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[118949,118725])). % 61.87/62.11 cnf(118951,plain, % 61.87/62.11 (~P3(a2,a3,a4)+~P3(a3,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[7,118950,19])). % 61.87/62.11 cnf(118952,plain, % 61.87/62.11 (~P3(a4,a3,a2)+~P3(a2,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118951,118773])). % 61.87/62.11 cnf(118953,plain, % 61.87/62.11 (P3(a4,a3,a1)+~P3(a2,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118952,118706])). % 61.87/62.11 cnf(118954,plain, % 61.87/62.11 (P3(a3,a4,a2)+~P3(a2,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[118953,118740])). % 61.87/62.11 cnf(118965,plain, % 61.87/62.11 (P3(a4,a3,a2)+~P3(a3,a4,a2)+~P3(a1,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[118731,391])). % 61.87/62.11 cnf(118966,plain, % 61.87/62.11 (~P3(a1,a2,a4)+~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118965,513])). % 61.87/62.11 cnf(118993,plain, % 61.87/62.11 (P3(a1,a2,a4)+P3(a3,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[1951,118788])). % 61.87/62.11 cnf(118994,plain, % 61.87/62.11 (P3(a1,a2,a4)+P3(a1,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118993,118942])). % 61.87/62.11 cnf(118995,plain, % 61.87/62.11 (P3(a1,a2,a4)+~P3(a4,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[118994,696])). % 61.87/62.11 cnf(118996,plain, % 61.87/62.11 (~P3(a4,a1,a2)+~P3(a1,a2,a3)), % 61.87/62.11 inference(scs_inference,[],[118995,8941])). % 61.87/62.11 cnf(118997,plain, % 61.87/62.11 (P3(a1,a4,a2)+~P3(a1,a2,a3)), % 61.87/62.11 inference(scs_inference,[],[118996,118690])). % 61.87/62.11 cnf(118998,plain, % 61.87/62.11 (~P3(a3,a4,a2)+~P3(a1,a2,a3)), % 61.87/62.11 inference(scs_inference,[],[12,118997,20])). % 61.87/62.11 cnf(118999,plain, % 61.87/62.11 (~P3(a2,a1,a4)+~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118998,1997])). % 61.87/62.11 cnf(119000,plain, % 61.87/62.11 (P3(a1,a2,a4)+~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[118999,118727])). % 61.87/62.11 cnf(119001,plain, % 61.87/62.11 (~P3(a3,a4,a2)+~P3(a3,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[119000,118749])). % 61.87/62.11 cnf(119002,plain, % 61.87/62.11 (~P3(a3,a1,a2)+~P3(a4,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[119001,118740])). % 61.87/62.11 cnf(119003,plain, % 61.87/62.11 (P3(a1,a3,a2)+~P3(a4,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[119002,118736])). % 61.87/62.11 cnf(119041,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a4,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[1951,118830])). % 61.87/62.11 cnf(119042,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a1,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[119041,119003])). % 61.87/62.11 cnf(119043,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a4,a1,a2)), % 61.87/62.11 inference(scs_inference,[],[119042,118822])). % 61.87/62.11 cnf(119044,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a1,a4,a3)), % 61.87/62.11 inference(scs_inference,[],[119043,118750])). % 61.87/62.11 cnf(119045,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a3,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[119044,118853])). % 61.87/62.11 cnf(119046,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[119045,118878])). % 61.87/62.11 cnf(119047,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a2,a3,a4)), % 61.87/62.11 inference(scs_inference,[],[119046,118930])). % 61.87/62.11 cnf(119048,plain, % 61.87/62.11 (P3(a1,a2,a3)+P3(a3,a2,a1)), % 61.87/62.11 inference(scs_inference,[],[119047,118776])). % 61.87/62.11 cnf(119049,plain, % 61.87/62.11 (P3(a3,a2,a1)+P3(a2,a1,a4)), % 61.87/62.11 inference(scs_inference,[],[119048,118725])). % 61.87/62.11 cnf(119050,plain, % 61.87/62.11 (P3(a3,a2,a1)+~P3(a1,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[119049,391])). % 61.87/62.11 cnf(119051,plain, % 61.87/62.11 (P3(a2,a3,a4)+~P3(a1,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[119050,118716])). % 61.87/62.11 cnf(119052,plain, % 61.87/62.11 (P3(a3,a4,a2)+~P3(a1,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[119051,118954])). % 61.87/62.11 cnf(119053,plain, % 61.87/62.11 (~P3(a1,a2,a4)), % 61.87/62.11 inference(scs_inference,[],[119052,118966])). % 61.87/62.11 cnf(119063,plain, % 61.87/62.11 (~P3(a3,a4,a2)), % 61.87/62.11 inference(scs_inference,[],[119053,119000])). % 61.87/62.11 cnf(119066,plain, % 61.87/62.11 (~P3(a4,x1190661,a2)+~P3(x1190661,a4,a1)), % 61.87/62.11 inference(scs_inference,[],[119053,21])). % 61.87/62.11 cnf(119088,plain, % 61.87/62.11 (~P3(a4,a3,a1)), % 61.87/62.11 inference(scs_inference,[],[119063,118740])). % 61.87/62.11 cnf(119178,plain, % 61.87/62.11 (~P3(a4,a3,a2)), % 61.87/62.11 inference(scs_inference,[],[3,118711,118673,4,119063,119066,22])). % 61.87/62.11 cnf(119341,plain, % 61.87/62.11 ($false), % 61.87/62.11 inference(scs_inference,[],[119178,119088,118706]), % 61.87/62.11 ['proof']). % 62.03/62.19 % SZS output end Proof % 62.03/62.19 % Total time :61.160000s %------------------------------------------------------------------------------