%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP127-4.004 : TPTP v8.2.0. Bugfixed v1.2.1. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 06:38:53 EDT 2024 % Result : Unsatisfiable 6.79s 7.01s % Output : CNFRefutation 6.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : GRP127-4.004 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n021.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 13:05:53 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 6.79/7.00 %------------------------------------------- % 6.79/7.00 % File :CSE---1.7 % 6.79/7.00 % Problem :theBenchmark % 6.79/7.00 % Transform :cnf % 6.79/7.00 % Format :tptp:raw % 6.79/7.00 % Command :java -jar mcs_scs.jar %d %s % 6.79/7.00 % 6.79/7.00 % Result :Theorem 6.290000s % 6.79/7.00 % Output :CNFRefutation 6.290000s % 6.79/7.00 %------------------------------------------- % 6.79/7.00 %-------------------------------------------------------------------------- % 6.79/7.00 % File : GRP127-4.004 : TPTP v8.2.0. Bugfixed v1.2.1. % 6.79/7.00 % Domain : Group Theory (Quasigroups) % 6.79/7.00 % Problem : ((b.a).b).b) = a % 6.79/7.00 % Version : [Sla93] axioms : Augmented. % 6.79/7.00 % English : Generate the multiplication table for the specified quasi- % 6.79/7.00 % group with 4 elements. % 6.79/7.00 % 6.79/7.00 % Refs : [Ben89] Bennett (1989), Quasigroup Identities and Mendelsohn D % 6.79/7.00 % : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 6.79/7.00 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 6.79/7.00 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 6.79/7.00 % Source : [TPTP] % 6.79/7.00 % Names : % 6.79/7.00 % 6.79/7.00 % Status : Unsatisfiable % 6.79/7.00 % Rating : 0.00 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.00 v2.1.0 % 6.79/7.00 % Syntax : Number of clauses : 26 ( 17 unt; 3 nHn; 25 RR) % 6.79/7.00 % Number of literals : 53 ( 0 equ; 30 neg) % 6.79/7.00 % Maximal clause size : 6 ( 2 avg) % 6.79/7.00 % Maximal term depth : 1 ( 1 avg) % 6.79/7.00 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 6.79/7.00 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 6.79/7.00 % Number of variables : 31 ( 0 sgn) % 6.79/7.00 % SPC : CNF_UNS_EPR_NEQ_NHN % 6.79/7.00 % 6.79/7.00 % Comments : [SFS93]'s axiomatization has been modified for this. % 6.79/7.00 % : Substitution axioms are not needed, as any positive equality % 6.79/7.00 % literals should resolve on negative ones directly. % 6.79/7.00 % : This problem is extensively investigated in [Ben89]. % 6.79/7.00 % : Version 4 has surjectivity and rotation % 6.79/7.00 % : tptp2X: -f tptp -s4 GRP127-4.g % 6.79/7.00 % Bugfixes : v1.2.1 - Clauses row_surjectivity and column_surjectivity fixed. % 6.79/7.00 %-------------------------------------------------------------------------- % 6.79/7.00 cnf(row_surjectivity,axiom, % 6.79/7.01 ( ~ group_element(X) % 6.79/7.01 | ~ group_element(Y) % 6.79/7.01 | product(e_1,X,Y) % 6.79/7.01 | product(e_2,X,Y) % 6.79/7.01 | product(e_3,X,Y) % 6.79/7.01 | product(e_4,X,Y) ) ). % 6.79/7.01 % 6.79/7.01 cnf(column_surjectivity,axiom, % 6.79/7.01 ( ~ group_element(X) % 6.79/7.01 | ~ group_element(Y) % 6.79/7.01 | product(X,e_1,Y) % 6.79/7.01 | product(X,e_2,Y) % 6.79/7.01 | product(X,e_3,Y) % 6.79/7.01 | product(X,e_4,Y) ) ). % 6.79/7.01 % 6.79/7.01 cnf(qg3_1,negated_conjecture, % 6.79/7.01 ( product(Y,X,Z1) % 6.79/7.01 | ~ product(Z2,Y,X) % 6.79/7.01 | ~ product(Z1,Y,Z2) ) ). % 6.79/7.01 % 6.79/7.01 cnf(qg3_2,negated_conjecture, % 6.79/7.01 ( product(Z1,Y,Z2) % 6.79/7.01 | ~ product(Z2,Y,X) % 6.79/7.01 | ~ product(Y,X,Z1) ) ). % 6.79/7.01 % 6.79/7.01 cnf(element_1,axiom, % 6.79/7.01 group_element(e_1) ). % 6.79/7.01 % 6.79/7.01 cnf(element_2,axiom, % 6.79/7.01 group_element(e_2) ). % 6.79/7.01 % 6.79/7.01 cnf(element_3,axiom, % 6.79/7.01 group_element(e_3) ). % 6.79/7.01 % 6.79/7.01 cnf(element_4,axiom, % 6.79/7.01 group_element(e_4) ). % 6.79/7.01 % 6.79/7.01 cnf(e_1_is_not_e_2,axiom, % 6.79/7.01 ~ equalish(e_1,e_2) ). % 6.79/7.01 % 6.79/7.01 cnf(e_1_is_not_e_3,axiom, % 6.79/7.01 ~ equalish(e_1,e_3) ). % 6.79/7.01 % 6.79/7.01 cnf(e_1_is_not_e_4,axiom, % 6.79/7.01 ~ equalish(e_1,e_4) ). % 6.79/7.01 % 6.79/7.01 cnf(e_2_is_not_e_1,axiom, % 6.79/7.01 ~ equalish(e_2,e_1) ). % 6.79/7.01 % 6.79/7.01 cnf(e_2_is_not_e_3,axiom, % 6.79/7.01 ~ equalish(e_2,e_3) ). % 6.79/7.01 % 6.79/7.01 cnf(e_2_is_not_e_4,axiom, % 6.79/7.01 ~ equalish(e_2,e_4) ). % 6.79/7.01 % 6.79/7.01 cnf(e_3_is_not_e_1,axiom, % 6.79/7.01 ~ equalish(e_3,e_1) ). % 6.79/7.01 % 6.79/7.01 cnf(e_3_is_not_e_2,axiom, % 6.79/7.01 ~ equalish(e_3,e_2) ). % 6.79/7.01 % 6.79/7.01 cnf(e_3_is_not_e_4,axiom, % 6.79/7.01 ~ equalish(e_3,e_4) ). % 6.79/7.01 % 6.79/7.01 cnf(e_4_is_not_e_1,axiom, % 6.79/7.01 ~ equalish(e_4,e_1) ). % 6.79/7.01 % 6.79/7.01 cnf(e_4_is_not_e_2,axiom, % 6.79/7.01 ~ equalish(e_4,e_2) ). % 6.79/7.01 % 6.79/7.01 cnf(e_4_is_not_e_3,axiom, % 6.79/7.01 ~ equalish(e_4,e_3) ). % 6.79/7.01 % 6.79/7.01 cnf(product_total_function1,axiom, % 6.79/7.01 ( ~ group_element(X) % 6.79/7.01 | ~ group_element(Y) % 6.79/7.01 | product(X,Y,e_1) % 6.79/7.01 | product(X,Y,e_2) % 6.79/7.01 | product(X,Y,e_3) % 6.79/7.01 | product(X,Y,e_4) ) ). % 6.79/7.01 % 6.79/7.01 cnf(product_total_function2,axiom, % 6.79/7.01 ( ~ product(X,Y,W) % 6.79/7.01 | ~ product(X,Y,Z) % 6.79/7.01 | equalish(W,Z) ) ). % 6.79/7.01 % 6.79/7.01 cnf(product_right_cancellation,axiom, % 6.79/7.01 ( ~ product(X,W,Y) % 6.79/7.01 | ~ product(X,Z,Y) % 6.79/7.01 | equalish(W,Z) ) ). % 6.79/7.01 % 6.79/7.01 cnf(product_left_cancellation,axiom, % 6.79/7.01 ( ~ product(W,Y,X) % 6.79/7.01 | ~ product(Z,Y,X) % 6.79/7.01 | equalish(W,Z) ) ). % 6.79/7.01 % 6.79/7.01 cnf(product_idempotence,axiom, % 6.79/7.01 product(X,X,X) ). % 6.79/7.01 % 6.79/7.01 cnf(qg3,negated_conjecture, % 6.79/7.01 ( ~ product(Y,X,Z1) % 6.79/7.01 | ~ product(Z1,Y,Z2) % 6.79/7.01 | product(Z2,Y,X) ) ). % 6.79/7.01 % 6.79/7.01 %-------------------------------------------------------------------------- % 6.79/7.01 %------------------------------------------- % 6.79/7.01 % Proof found % 6.79/7.01 % SZS status Theorem for theBenchmark % 6.79/7.01 % SZS output start Proof % 6.79/7.01 %ClaNum:26(EqnAxiom:0) % 6.79/7.01 %VarNum:84(SingletonVarNum:31) % 6.79/7.01 %MaxLitNum:6 % 6.79/7.01 %MaxfuncDepth:0 % 6.79/7.01 %SharedTerms:20 % 6.79/7.01 %goalClause: 21 22 23 % 6.79/7.01 [1]P1(a1) % 6.79/7.01 [2]P1(a2) % 6.79/7.01 [3]P1(a3) % 6.79/7.01 [4]P1(a4) % 6.79/7.01 [6]~P2(a1,a2) % 6.79/7.01 [7]~P2(a1,a3) % 6.79/7.01 [8]~P2(a1,a4) % 6.79/7.01 [9]~P2(a2,a1) % 6.79/7.01 [10]~P2(a2,a3) % 6.79/7.01 [11]~P2(a2,a4) % 6.79/7.01 [12]~P2(a3,a1) % 6.79/7.01 [13]~P2(a3,a2) % 6.79/7.01 [14]~P2(a3,a4) % 6.79/7.01 [15]~P2(a4,a1) % 6.79/7.01 [16]~P2(a4,a2) % 6.79/7.01 [17]~P2(a4,a3) % 6.79/7.01 [5]P3(x51,x51,x51) % 6.79/7.01 [18]~P3(x183,x184,x181)+P2(x181,x182)+~P3(x183,x184,x182) % 6.79/7.01 [19]~P3(x193,x191,x194)+P2(x191,x192)+~P3(x193,x192,x194) % 6.79/7.01 [20]~P3(x201,x203,x204)+P2(x201,x202)+~P3(x202,x203,x204) % 6.79/7.01 [21]~P3(x212,x213,x214)+P3(x211,x212,x213)+~P3(x214,x212,x211) % 6.79/7.01 [22]~P3(x223,x221,x224)+P3(x221,x222,x223)+~P3(x224,x221,x222) % 6.79/7.01 [23]~P3(x232,x234,x231)+P3(x231,x232,x233)+~P3(x233,x232,x234) % 6.79/7.01 [24]~P1(x242)+~P1(x241)+P3(x241,x242,a2)+P3(x241,x242,a3)+P3(x241,x242,a4)+P3(x241,x242,a1) % 6.79/7.01 [25]~P1(x252)+~P1(x251)+P3(x251,a2,x252)+P3(x251,a3,x252)+P3(x251,a4,x252)+P3(x251,a1,x252) % 6.79/7.01 [26]~P1(x262)+~P1(x261)+P3(a2,x261,x262)+P3(a3,x261,x262)+P3(a4,x261,x262)+P3(a1,x261,x262) % 6.79/7.01 %EqnAxiom % 6.79/7.01 % 6.79/7.01 %------------------------------------------- % 6.79/7.02 cnf(152,plain, % 6.79/7.02 (~P3(a1,a2,a1)), % 6.79/7.02 inference(scs_inference,[],[5,6,18,21])). % 6.79/7.02 cnf(198,plain, % 6.79/7.02 (~P3(a1,a3,a3)), % 6.79/7.02 inference(scs_inference,[],[7,5,18,22])). % 6.79/7.02 cnf(244,plain, % 6.79/7.02 (~P3(a4,a1,a1)), % 6.79/7.02 inference(scs_inference,[],[8,5,18,23])). % 6.79/7.02 cnf(245,plain, % 6.79/7.02 (~P3(a3,a3,a1)), % 6.79/7.02 inference(scs_inference,[],[5,198,23])). % 6.79/7.02 cnf(246,plain, % 6.79/7.02 (P3(x2461,x2461,x2461)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(248,plain, % 6.79/7.02 (~P3(a3,a1,a3)), % 6.79/7.02 inference(scs_inference,[],[5,246,198,23,21])). % 6.79/7.02 cnf(254,plain, % 6.79/7.02 (~P3(a1,a1,a4)), % 6.79/7.02 inference(scs_inference,[],[5,244,23])). % 6.79/7.02 cnf(299,plain, % 6.79/7.02 (~P3(a2,a1,a1)), % 6.79/7.02 inference(scs_inference,[],[9,5,18,22])). % 6.79/7.02 cnf(300,plain, % 6.79/7.02 (~P3(a1,a1,a2)), % 6.79/7.02 inference(scs_inference,[],[5,299,23])). % 6.79/7.02 cnf(348,plain, % 6.79/7.02 (~P3(a2,a3,a2)), % 6.79/7.02 inference(scs_inference,[],[10,5,18,21])). % 6.79/7.02 cnf(387,plain, % 6.79/7.02 (P3(a3,a3,a2)+P3(a1,a3,a2)+P3(a4,a3,a2)), % 6.79/7.02 inference(scs_inference,[],[2,5,348,152,3,1,20,26])). % 6.79/7.02 cnf(400,plain, % 6.79/7.02 (P3(a2,a3,a3)+P3(a2,a3,a1)+P3(a2,a3,a4)), % 6.79/7.02 inference(scs_inference,[],[2,5,348,152,3,1,19,24])). % 6.79/7.02 cnf(4096,plain, % 6.79/7.02 (P3(a2,a1,a3)+P3(a1,a1,a3)+P3(a4,a1,a3)), % 6.79/7.02 inference(scs_inference,[],[5,248,152,348,3,2,1,19,26])). % 6.79/7.02 cnf(7531,plain, % 6.79/7.02 (~P3(a1,a4,a1)), % 6.79/7.02 inference(scs_inference,[],[254,5,21])). % 6.79/7.02 cnf(10173,plain, % 6.79/7.02 (~P3(a1,a2,x101731)+~P3(a2,x101731,a1)), % 6.79/7.02 inference(scs_inference,[],[5,152,19,23])). % 6.79/7.02 cnf(10178,plain, % 6.79/7.02 (~P3(a1,a4,x101781)+~P3(a4,x101781,a1)), % 6.79/7.02 inference(scs_inference,[],[5,7531,18,23])). % 6.79/7.02 cnf(10183,plain, % 6.79/7.02 (~P3(a3,a1,x101831)+~P3(a1,x101831,a3)), % 6.79/7.02 inference(scs_inference,[],[5,248,20,23])). % 6.79/7.02 cnf(10188,plain, % 6.79/7.02 (~P3(a2,a3,x101881)+~P3(a3,x101881,a2)), % 6.79/7.02 inference(scs_inference,[],[5,348,19,23])). % 6.79/7.02 cnf(10193,plain, % 6.79/7.02 (~P3(x101931,a2,a1)+~P3(a2,a1,x101931)), % 6.79/7.02 inference(scs_inference,[],[5,152,18,21])). % 6.79/7.02 cnf(10199,plain, % 6.79/7.02 (~P3(x101991,a4,a1)+~P3(a4,a1,x101991)), % 6.79/7.02 inference(scs_inference,[],[5,7531,19,21])). % 6.79/7.02 cnf(10202,plain, % 6.79/7.02 (~P3(a2,a2,a3)), % 6.79/7.02 inference(scs_inference,[],[5,348,22])). % 6.79/7.02 cnf(10203,plain, % 6.79/7.02 (P3(x102031,x102031,x102031)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10205,plain, % 6.79/7.02 (~P3(a3,a2,a2)), % 6.79/7.02 inference(scs_inference,[],[5,10203,348,22,23])). % 6.79/7.02 cnf(10206,plain, % 6.79/7.02 (P3(x102061,x102061,x102061)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10210,plain, % 6.79/7.02 (~P3(x102101,a1,a3)+~P3(a1,a3,x102101)), % 6.79/7.02 inference(scs_inference,[],[5,10203,10206,248,348,22,23,18,21])). % 6.79/7.02 cnf(10213,plain, % 6.79/7.02 (~P3(a1,a2,a2)), % 6.79/7.02 inference(scs_inference,[],[5,10173,22])). % 6.79/7.02 cnf(10214,plain, % 6.79/7.02 (~P3(a2,a2,a1)), % 6.79/7.02 inference(scs_inference,[],[5,10213,21])). % 6.79/7.02 cnf(10215,plain, % 6.79/7.02 (P3(x102151,x102151,x102151)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10219,plain, % 6.79/7.02 (~P3(x102191,a2,a1)+~P3(a1,a2,x102191)), % 6.79/7.02 inference(scs_inference,[],[5,10215,299,10213,21,18,22])). % 6.79/7.02 cnf(10226,plain, % 6.79/7.02 (~P3(a2,a1,a2)), % 6.79/7.02 inference(scs_inference,[],[5,10214,21])). % 6.79/7.02 cnf(10245,plain, % 6.79/7.02 (~P3(x102451,a4,a1)+~P3(a1,a4,x102451)), % 6.79/7.02 inference(scs_inference,[],[5,244,19,22])). % 6.79/7.02 cnf(10248,plain, % 6.79/7.02 (P3(x102481,x102481,x102481)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10250,plain, % 6.79/7.02 (~P3(a1,a4,a4)), % 6.79/7.02 inference(scs_inference,[],[5,10248,244,19,22,21,23])). % 6.79/7.02 cnf(10254,plain, % 6.79/7.02 (~P3(a4,a4,a1)), % 6.79/7.02 inference(scs_inference,[],[5,10250,21])). % 6.79/7.02 cnf(10255,plain, % 6.79/7.02 (P3(x102551,x102551,x102551)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10259,plain, % 6.79/7.02 (~P3(x102591,a1,a4)+~P3(a4,a1,x102591)), % 6.79/7.02 inference(scs_inference,[],[5,10255,10250,21,19,22])). % 6.79/7.02 cnf(10268,plain, % 6.79/7.02 (~P3(a4,a1,a4)), % 6.79/7.02 inference(scs_inference,[],[5,10254,21])). % 6.79/7.02 cnf(10269,plain, % 6.79/7.02 (P3(x102691,x102691,x102691)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10275,plain, % 6.79/7.02 (~P3(a3,a1,a1)), % 6.79/7.02 inference(scs_inference,[],[5,10269,198,10254,21,18,22,23])). % 6.79/7.02 cnf(10279,plain, % 6.79/7.02 (~P3(a1,a1,a3)), % 6.79/7.02 inference(scs_inference,[],[5,10275,21])). % 6.79/7.02 cnf(10280,plain, % 6.79/7.02 (P3(x102801,x102801,x102801)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10284,plain, % 6.79/7.02 (~P3(x102841,a3,a1)+~P3(a1,a3,x102841)), % 6.79/7.02 inference(scs_inference,[],[5,10280,10275,21,20,22])). % 6.79/7.02 cnf(10291,plain, % 6.79/7.02 (P3(a2,a1,a3)+P3(a4,a1,a3)), % 6.79/7.02 inference(scs_inference,[],[10279,4096])). % 6.79/7.02 cnf(10295,plain, % 6.79/7.02 (~P3(a1,a3,a1)), % 6.79/7.02 inference(scs_inference,[],[5,10279,21])). % 6.79/7.02 cnf(10296,plain, % 6.79/7.02 (P3(x102961,x102961,x102961)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10300,plain, % 6.79/7.02 (~P3(x103001,a3,a2)+~P3(a2,a3,x103001)), % 6.79/7.02 inference(scs_inference,[],[5,10296,10205,10279,21,19,22])). % 6.79/7.02 cnf(10302,plain, % 6.79/7.02 (~P3(a2,a3,a3)), % 6.79/7.02 inference(scs_inference,[],[5,10296,10205,10279,21,19,22,23])). % 6.79/7.02 cnf(10306,plain, % 6.79/7.02 (P3(a2,a3,a1)+P3(a2,a3,a4)), % 6.79/7.02 inference(scs_inference,[],[10302,400])). % 6.79/7.02 cnf(10310,plain, % 6.79/7.02 (~P3(a3,a3,a2)), % 6.79/7.02 inference(scs_inference,[],[5,10302,21])). % 6.79/7.02 cnf(10311,plain, % 6.79/7.02 (P3(x103111,x103111,x103111)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10331,plain, % 6.79/7.02 (P3(a4,a3,a2)+~P3(a3,a4,a1)), % 6.79/7.02 inference(scs_inference,[],[3,5,10311,10275,10302,299,245,10214,348,10295,1,2,21,18,387,22,23,25,26,24,10210,10291,10300,10199])). % 6.79/7.02 cnf(10335,plain, % 6.79/7.02 (P3(a4,a3,a2)+~P3(a1,a4,a3)), % 6.79/7.02 inference(scs_inference,[],[3,5,10311,10275,10302,299,245,10214,348,10295,1,2,21,18,387,22,23,25,26,24,10210,10291,10300,10199,10173,10178])). % 6.79/7.02 cnf(10339,plain, % 6.79/7.02 (~P3(a3,a2,a3)), % 6.79/7.02 inference(scs_inference,[],[5,10310,21])). % 6.79/7.02 cnf(10340,plain, % 6.79/7.02 (P3(x103401,x103401,x103401)), % 6.79/7.02 inference(rename_variables,[],[5])). % 6.79/7.02 cnf(10344,plain, % 6.79/7.02 (~P3(x103441,a2,a3)+~P3(a3,a2,x103441)), % 6.79/7.02 inference(scs_inference,[],[5,10340,10302,10310,21,20,22])). % 6.79/7.02 cnf(10352,plain, % 6.79/7.02 (~P3(a2,a3,a1)+~P3(a3,a2,a4)), % 6.79/7.02 inference(scs_inference,[],[3,5,10340,10302,152,10202,10310,2,21,20,22,26,10183,10219,23])). % 6.79/7.02 cnf(10362,plain, % 6.79/7.02 (~P3(a2,a1,a3)+P3(a4,a1,a2)), % 6.79/7.02 inference(scs_inference,[],[3,5,300,10205,10213,10310,10226,1,2,19,22,25,26])). % 6.79/7.02 cnf(10366,plain, % 6.79/7.02 (~P3(a2,a1,a3)+~P3(a2,a3,a4)), % 6.79/7.02 inference(scs_inference,[],[3,5,10275,300,10205,10213,248,10310,10226,1,2,19,22,25,26,24,10188])). % 6.79/7.02 cnf(10380,plain, % 6.79/7.02 (~P3(x103801,a3,a2)+~P3(a3,a2,x103801)), % 6.79/7.02 inference(scs_inference,[],[5,348,18,21])). % 6.79/7.02 cnf(10382,plain, % 6.79/7.02 (~P3(a1,a3,a2)+P3(a3,a4,a1)), % 6.79/7.02 inference(scs_inference,[],[3,5,10275,245,348,1,18,21,25])). % 6.79/7.02 cnf(10398,plain, % 6.79/7.02 (~P3(a2,a1,a4)+P3(a1,a3,a2)), % 6.79/7.02 inference(scs_inference,[],[5,300,10213,10268,1,2,19,21,25])). % 6.79/7.02 cnf(10406,plain, % 6.79/7.02 (P3(a2,a3,a4)+~P3(a2,a1,a4)), % 6.79/7.02 inference(scs_inference,[],[5,10250,300,10213,7531,10268,4,1,2,19,21,25,24,10245,10284,10306])). % 6.79/7.02 cnf(10407,plain, % 6.79/7.02 (P3(a4,a3,a2)+~P3(a2,a1,a4)), % 6.79/7.02 inference(scs_inference,[],[5,10250,300,10213,7531,10268,4,1,2,19,21,25,24,10245,10284,10306,10335])). % 6.79/7.02 cnf(10410,plain, % 6.79/7.02 (~P3(a2,a1,a4)+P3(a4,a3,a1)), % 6.79/7.02 inference(scs_inference,[],[3,5,10250,300,152,245,10213,7531,10268,10295,4,1,2,19,21,25,24,10245,10284,10306,10335,10382,10183,10300,22,23,26])). % 6.79/7.02 cnf(10414,plain, % 6.79/7.02 (~P3(x104141,a2,a3)+~P3(a2,a3,x104141)), % 6.79/7.02 inference(scs_inference,[],[5,10339,20,21])). % 6.79/7.02 cnf(10428,plain, % 6.79/7.02 (~P3(a1,a2,a3)+~P3(a4,a3,a2)), % 6.79/7.02 inference(scs_inference,[],[3,5,10302,299,245,10214,348,10339,10295,1,2,20,21,25,26,24,10366,10291,10199,10173,10300])). % 6.79/7.02 cnf(10444,plain, % 6.79/7.02 (~P3(a3,a1,a2)+P3(a4,a2,a3)), % 6.79/7.02 inference(scs_inference,[],[3,5,152,198,10213,10202,10279,10226,10339,1,2,18,21,25,24,26])). % 6.79/7.02 cnf(10462,plain, % 6.79/7.02 (~P3(a2,a3,a1)+P3(a4,a1,a2)), % 6.79/7.02 inference(scs_inference,[],[3,5,300,10205,10310,10226,10295,1,2,19,21,25,26])). % 6.79/7.02 cnf(10485,plain, % 6.79/7.02 (~P3(a1,a2,a4)+~P3(a4,a3,a2)), % 6.79/7.02 inference(scs_inference,[],[5,244,10268,4,1,20,23,24,10362,10462,10259,10306,10300])). % 6.79/7.02 cnf(10492,plain, % 6.79/7.02 (~P3(a3,a2,x104921)+~P3(a2,x104921,a3)), % 6.79/7.02 inference(scs_inference,[],[5,10339,18,23])). % 6.79/7.02 cnf(10506,plain, % 6.79/7.02 (~P3(a2,a1,a3)), % 6.79/7.02 inference(scs_inference,[],[3,5,10275,152,10205,245,10214,10339,1,2,18,23,25,24,26,10352,10380,10344,10306,10331,10366])). % 6.79/7.02 cnf(10535,plain, % 6.79/7.02 ($false), % 6.79/7.02 inference(scs_inference,[],[3,5,10302,299,10202,10226,10506,1,2,19,25,24,10410,10398,10406,10407,10414,10428,10444,10485,10492,10193,10178,10300]), % 6.79/7.02 ['proof']). % 6.79/7.03 % SZS output end Proof % 6.79/7.03 % Total time :6.290000s %------------------------------------------------------------------------------