%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP126-4.004 : TPTP v8.2.0. Bugfixed v1.2.1. % 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:52 EDT 2024 % Result : Unsatisfiable 4.38s 4.43s % Output : CNFRefutation 4.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP126-4.004 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n023.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Jun 20 13:08:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.45/0.61 start to proof:theBenchmark % 4.38/4.42 %------------------------------------------- % 4.38/4.42 % File :CSE---1.7 % 4.38/4.42 % Problem :theBenchmark % 4.38/4.42 % Transform :cnf % 4.38/4.42 % Format :tptp:raw % 4.38/4.42 % Command :java -jar mcs_scs.jar %d %s % 4.38/4.42 % 4.38/4.42 % Result :Theorem 3.780000s % 4.38/4.42 % Output :CNFRefutation 3.780000s % 4.38/4.42 %------------------------------------------- % 4.38/4.43 %-------------------------------------------------------------------------- % 4.38/4.43 % File : GRP126-4.004 : TPTP v8.2.0. Bugfixed v1.2.1. % 4.38/4.43 % Domain : Group Theory (Quasigroups) % 4.38/4.43 % Problem : (a.b).(b.a) = b % 4.38/4.43 % Version : [Sla93] axioms : Augmented. % 4.38/4.43 % English : Generate the multiplication table for the specified quasi- % 4.38/4.43 % group with 4 elements. % 4.38/4.43 % 4.38/4.43 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 4.38/4.43 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 4.38/4.43 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 4.38/4.43 % Source : [TPTP] % 4.38/4.43 % Names : % 4.38/4.43 % 4.38/4.43 % Status : Unsatisfiable % 4.38/4.43 % Rating : 0.00 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.00 v2.1.0 % 4.38/4.43 % Syntax : Number of clauses : 26 ( 17 unt; 3 nHn; 25 RR) % 4.38/4.43 % Number of literals : 53 ( 0 equ; 30 neg) % 4.38/4.43 % Maximal clause size : 6 ( 2 avg) % 4.38/4.43 % Maximal term depth : 1 ( 1 avg) % 4.38/4.43 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 4.38/4.43 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 4.38/4.43 % Number of variables : 31 ( 0 sgn) % 4.38/4.43 % SPC : CNF_UNS_EPR_NEQ_NHN % 4.38/4.43 % 4.38/4.43 % Comments : [SFS93]'s axiomatization has been modified for this. % 4.38/4.43 % : Substitution axioms are not needed, as any positive equality % 4.38/4.43 % literals should resolve on negative ones directly. % 4.38/4.43 % : Version 4 has surjectivity and rotation % 4.38/4.43 % : tptp2X: -f tptp -s4 GRP126-4.g % 4.38/4.43 % Bugfixes : v1.2.1 - Clauses row_surjectivity and column_surjectivity fixed. % 4.38/4.43 %-------------------------------------------------------------------------- % 4.38/4.43 cnf(row_surjectivity,axiom, % 4.38/4.43 ( ~ group_element(X) % 4.38/4.43 | ~ group_element(Y) % 4.38/4.43 | product(e_1,X,Y) % 4.38/4.43 | product(e_2,X,Y) % 4.38/4.43 | product(e_3,X,Y) % 4.38/4.43 | product(e_4,X,Y) ) ). % 4.38/4.43 % 4.38/4.43 cnf(column_surjectivity,axiom, % 4.38/4.43 ( ~ group_element(X) % 4.38/4.43 | ~ group_element(Y) % 4.38/4.43 | product(X,e_1,Y) % 4.38/4.43 | product(X,e_2,Y) % 4.38/4.43 | product(X,e_3,Y) % 4.38/4.43 | product(X,e_4,Y) ) ). % 4.38/4.43 % 4.38/4.43 cnf(qg4_1,negated_conjecture, % 4.38/4.43 ( product(X,Y,Z1) % 4.38/4.43 | ~ product(Z1,Z2,Y) % 4.38/4.43 | ~ product(Y,X,Z2) ) ). % 4.38/4.43 % 4.38/4.43 cnf(qg4_2,negated_conjecture, % 4.38/4.43 ( product(Y,X,Z2) % 4.38/4.43 | ~ product(Z1,Z2,Y) % 4.38/4.43 | ~ product(X,Y,Z1) ) ). % 4.38/4.43 % 4.38/4.43 cnf(element_1,axiom, % 4.38/4.43 group_element(e_1) ). % 4.38/4.43 % 4.38/4.43 cnf(element_2,axiom, % 4.38/4.43 group_element(e_2) ). % 4.38/4.43 % 4.38/4.43 cnf(element_3,axiom, % 4.38/4.43 group_element(e_3) ). % 4.38/4.43 % 4.38/4.43 cnf(element_4,axiom, % 4.38/4.43 group_element(e_4) ). % 4.38/4.43 % 4.38/4.43 cnf(e_1_is_not_e_2,axiom, % 4.38/4.43 ~ equalish(e_1,e_2) ). % 4.38/4.43 % 4.38/4.43 cnf(e_1_is_not_e_3,axiom, % 4.38/4.43 ~ equalish(e_1,e_3) ). % 4.38/4.43 % 4.38/4.43 cnf(e_1_is_not_e_4,axiom, % 4.38/4.43 ~ equalish(e_1,e_4) ). % 4.38/4.43 % 4.38/4.43 cnf(e_2_is_not_e_1,axiom, % 4.38/4.43 ~ equalish(e_2,e_1) ). % 4.38/4.43 % 4.38/4.43 cnf(e_2_is_not_e_3,axiom, % 4.38/4.43 ~ equalish(e_2,e_3) ). % 4.38/4.43 % 4.38/4.43 cnf(e_2_is_not_e_4,axiom, % 4.38/4.43 ~ equalish(e_2,e_4) ). % 4.38/4.43 % 4.38/4.43 cnf(e_3_is_not_e_1,axiom, % 4.38/4.43 ~ equalish(e_3,e_1) ). % 4.38/4.43 % 4.38/4.43 cnf(e_3_is_not_e_2,axiom, % 4.38/4.43 ~ equalish(e_3,e_2) ). % 4.38/4.43 % 4.38/4.43 cnf(e_3_is_not_e_4,axiom, % 4.38/4.43 ~ equalish(e_3,e_4) ). % 4.38/4.43 % 4.38/4.43 cnf(e_4_is_not_e_1,axiom, % 4.38/4.43 ~ equalish(e_4,e_1) ). % 4.38/4.43 % 4.38/4.43 cnf(e_4_is_not_e_2,axiom, % 4.38/4.43 ~ equalish(e_4,e_2) ). % 4.38/4.43 % 4.38/4.43 cnf(e_4_is_not_e_3,axiom, % 4.38/4.43 ~ equalish(e_4,e_3) ). % 4.38/4.43 % 4.38/4.43 cnf(product_total_function1,axiom, % 4.38/4.43 ( ~ group_element(X) % 4.38/4.43 | ~ group_element(Y) % 4.38/4.43 | product(X,Y,e_1) % 4.38/4.43 | product(X,Y,e_2) % 4.38/4.43 | product(X,Y,e_3) % 4.38/4.43 | product(X,Y,e_4) ) ). % 4.38/4.43 % 4.38/4.43 cnf(product_total_function2,axiom, % 4.38/4.43 ( ~ product(X,Y,W) % 4.38/4.43 | ~ product(X,Y,Z) % 4.38/4.43 | equalish(W,Z) ) ). % 4.38/4.43 % 4.38/4.43 cnf(product_right_cancellation,axiom, % 4.38/4.43 ( ~ product(X,W,Y) % 4.38/4.43 | ~ product(X,Z,Y) % 4.38/4.43 | equalish(W,Z) ) ). % 4.38/4.43 % 4.38/4.43 cnf(product_left_cancellation,axiom, % 4.38/4.43 ( ~ product(W,Y,X) % 4.38/4.43 | ~ product(Z,Y,X) % 4.38/4.43 | equalish(W,Z) ) ). % 4.38/4.43 % 4.38/4.43 cnf(product_idempotence,axiom, % 4.38/4.43 product(X,X,X) ). % 4.38/4.43 % 4.38/4.43 cnf(qg4,negated_conjecture, % 4.38/4.43 ( ~ product(X,Y,Z1) % 4.38/4.43 | ~ product(Y,X,Z2) % 4.38/4.43 | product(Z1,Z2,Y) ) ). % 4.38/4.43 % 4.38/4.43 %-------------------------------------------------------------------------- % 4.38/4.43 %------------------------------------------- % 4.38/4.43 % Proof found % 4.38/4.43 % SZS status Theorem for theBenchmark % 4.38/4.43 % SZS output start Proof % 4.38/4.43 %ClaNum:26(EqnAxiom:0) % 4.38/4.43 %VarNum:84(SingletonVarNum:31) % 4.38/4.43 %MaxLitNum:6 % 4.38/4.43 %MaxfuncDepth:0 % 4.38/4.43 %SharedTerms:20 % 4.38/4.43 %goalClause: 21 22 23 % 4.38/4.43 [1]P1(a1) % 4.38/4.43 [2]P1(a2) % 4.38/4.43 [3]P1(a3) % 4.38/4.43 [4]P1(a4) % 4.38/4.43 [6]~P2(a1,a2) % 4.38/4.43 [7]~P2(a1,a3) % 4.38/4.43 [8]~P2(a1,a4) % 4.38/4.43 [9]~P2(a2,a1) % 4.38/4.43 [10]~P2(a2,a3) % 4.38/4.43 [11]~P2(a2,a4) % 4.38/4.43 [12]~P2(a3,a1) % 4.38/4.43 [13]~P2(a3,a2) % 4.38/4.43 [14]~P2(a3,a4) % 4.38/4.43 [15]~P2(a4,a1) % 4.38/4.43 [16]~P2(a4,a2) % 4.38/4.43 [17]~P2(a4,a3) % 4.38/4.43 [5]P3(x51,x51,x51) % 4.38/4.43 [18]~P3(x183,x184,x181)+P2(x181,x182)+~P3(x183,x184,x182) % 4.38/4.43 [19]~P3(x193,x191,x194)+P2(x191,x192)+~P3(x193,x192,x194) % 4.38/4.43 [20]~P3(x201,x203,x204)+P2(x201,x202)+~P3(x202,x203,x204) % 4.38/4.43 [21]~P3(x214,x213,x211)+P3(x211,x212,x213)+~P3(x213,x214,x212) % 4.38/4.43 [22]~P3(x222,x221,x224)+P3(x221,x222,x223)+~P3(x224,x223,x221) % 4.38/4.43 [23]~P3(x232,x231,x234)+P3(x231,x232,x233)+~P3(x233,x234,x232) % 4.38/4.43 [24]~P1(x242)+~P1(x241)+P3(x241,x242,a2)+P3(x241,x242,a3)+P3(x241,x242,a4)+P3(x241,x242,a1) % 4.38/4.43 [25]~P1(x252)+~P1(x251)+P3(x251,a2,x252)+P3(x251,a3,x252)+P3(x251,a4,x252)+P3(x251,a1,x252) % 4.38/4.43 [26]~P1(x262)+~P1(x261)+P3(a2,x261,x262)+P3(a3,x261,x262)+P3(a4,x261,x262)+P3(a1,x261,x262) % 4.38/4.43 %EqnAxiom % 4.38/4.43 % 4.38/4.43 %------------------------------------------- % 4.38/4.44 cnf(152,plain, % 4.38/4.44 (~P3(a1,a2,a1)), % 4.38/4.44 inference(scs_inference,[],[5,6,18,22])). % 4.38/4.44 cnf(153,plain, % 4.38/4.44 (~P3(a2,a1,a1)), % 4.38/4.44 inference(scs_inference,[],[5,152,22])). % 4.38/4.44 cnf(201,plain, % 4.38/4.44 (~P3(a1,a3,a3)), % 4.38/4.44 inference(scs_inference,[],[7,5,18,23])). % 4.38/4.44 cnf(202,plain, % 4.38/4.44 (~P3(a3,a1,a3)), % 4.38/4.44 inference(scs_inference,[],[5,201,23])). % 4.38/4.44 cnf(250,plain, % 4.38/4.44 (~P3(a1,a4,a1)), % 4.38/4.44 inference(scs_inference,[],[8,5,18,22])). % 4.38/4.44 cnf(296,plain, % 4.38/4.44 (~P3(a1,a2,a2)), % 4.38/4.44 inference(scs_inference,[],[9,5,18,23])). % 4.38/4.44 cnf(297,plain, % 4.38/4.44 (~P3(a2,a1,a2)), % 4.38/4.44 inference(scs_inference,[],[5,296,23])). % 4.38/4.44 cnf(298,plain, % 4.38/4.44 (P3(x2981,x2981,x2981)), % 4.38/4.44 inference(rename_variables,[],[5])). % 4.38/4.44 cnf(302,plain, % 4.38/4.44 (P3(a1,a2,a3)+P3(a1,a2,a4)), % 4.38/4.44 inference(scs_inference,[],[1,5,298,152,296,2,23,19,24])). % 4.38/4.44 cnf(308,plain, % 4.38/4.44 (P3(a2,a1,a3)+P3(a2,a1,a4)), % 4.38/4.44 inference(scs_inference,[],[1,5,297,153,2,20,24])). % 4.38/4.44 cnf(313,plain, % 4.38/4.44 (P3(a1,a3,a2)+P3(a1,a1,a2)+P3(a1,a4,a2)), % 4.38/4.44 inference(scs_inference,[],[1,5,296,297,2,18,25])). % 4.38/4.44 cnf(718,plain, % 4.38/4.44 (P3(a1,a2,a3)+~P3(a4,a2,a2)), % 4.38/4.44 inference(scs_inference,[],[297,302,22])). % 4.38/4.44 cnf(764,plain, % 4.38/4.44 (~P3(a2,a3,a1)+~P3(a4,a2,a2)), % 4.38/4.44 inference(scs_inference,[],[297,718,23])). % 4.38/4.44 cnf(810,plain, % 4.38/4.44 (P3(a2,a2,a1)+P3(a2,a4,a1)+~P3(a4,a2,a2)), % 4.38/4.44 inference(scs_inference,[],[153,1,2,764,25])). % 4.38/4.44 cnf(1225,plain, % 4.38/4.44 (~P3(a2,a2,a1)), % 4.38/4.44 inference(scs_inference,[],[5,296,21])). % 4.38/4.44 cnf(1226,plain, % 4.38/4.44 (P3(x12261,x12261,x12261)), % 4.38/4.44 inference(rename_variables,[],[5])). % 4.38/4.44 cnf(1230,plain, % 4.38/4.44 (P3(a2,a4,a1)+~P3(a4,a2,a2)), % 4.38/4.44 inference(scs_inference,[],[5,1226,296,21,19,810])). % 4.38/4.44 cnf(1248,plain, % 4.38/4.44 (P3(a2,a4,a1)+P3(a1,a1,a2)+P3(a4,a1,a2)), % 4.38/4.44 inference(scs_inference,[],[5,152,296,297,1225,201,153,1,2,20,25,23,21,22,24,26])). % 4.38/4.44 cnf(1255,plain, % 4.38/4.44 (~P3(a1,a3,a2)+P3(a4,a2,a1)), % 4.38/4.44 inference(scs_inference,[],[5,152,202,1225,1,2,18,26,21,23])). % 4.38/4.44 cnf(1296,plain, % 4.38/4.44 (~P3(a4,a2,a2)), % 4.38/4.44 inference(scs_inference,[],[297,1230,21])). % 4.38/4.44 cnf(1664,plain, % 4.38/4.44 (~P3(a2,a1,a4)+~P3(a1,a3,a2)), % 4.38/4.44 inference(scs_inference,[],[296,1255,22])). % 4.38/4.44 cnf(1848,plain, % 4.38/4.44 (P3(a2,a1,a3)+~P3(a1,a3,a2)), % 4.38/4.44 inference(scs_inference,[],[1664,308])). % 4.38/4.44 cnf(1940,plain, % 4.38/4.44 (~P3(a1,a3,a2)), % 4.38/4.44 inference(scs_inference,[],[152,1848,23])). % 4.38/4.44 cnf(1941,plain, % 4.38/4.44 (P3(a1,a1,a2)+P3(a1,a4,a2)), % 4.38/4.44 inference(scs_inference,[],[1940,313])). % 4.38/4.44 cnf(1944,plain, % 4.38/4.44 (P3(a1,a3,a4)+P3(a1,a3,a1)), % 4.38/4.44 inference(scs_inference,[],[5,1940,201,3,1,19,24])). % 4.38/4.44 cnf(2312,plain, % 4.38/4.44 (P3(a1,a1,a2)+P3(a4,a1,a2)+~P3(a1,a2,a4)), % 4.38/4.44 inference(scs_inference,[],[1296,1248,22])). % 4.38/4.44 cnf(2496,plain, % 4.38/4.44 (P3(a1,a1,a2)+~P3(a1,a4,a2)+~P3(a1,a2,a4)), % 4.38/4.44 inference(scs_inference,[],[1225,2312,21])). % 4.38/4.44 cnf(2956,plain, % 4.38/4.44 (P3(a1,a1,a2)+P3(a1,a2,a3)+~P3(a1,a4,a2)), % 4.38/4.44 inference(scs_inference,[],[296,152,2,1,2496,24])). % 4.38/4.44 cnf(3830,plain, % 4.38/4.44 (P3(a1,a2,a4)+~P3(a3,a1,a2)), % 4.38/4.44 inference(scs_inference,[],[153,302,22])). % 4.38/4.44 cnf(4518,plain, % 4.38/4.44 (P3(a1,a2,a3)+~P3(a2,a4,a1)), % 4.38/4.44 inference(scs_inference,[],[1296,302,22])). % 4.38/4.44 cnf(4564,plain, % 4.38/4.44 (~P3(a1,a3,a1)+~P3(a2,a4,a1)), % 4.38/4.44 inference(scs_inference,[],[153,4518,23])). % 4.38/4.44 cnf(4610,plain, % 4.38/4.44 (P3(a1,a3,a4)+~P3(a2,a4,a1)), % 4.38/4.44 inference(scs_inference,[],[4564,1944])). % 4.38/4.44 cnf(7225,plain, % 4.38/4.44 (~P3(a4,a1,a1)), % 4.38/4.44 inference(scs_inference,[],[250,5,20,22])). % 4.38/4.44 cnf(10178,plain, % 4.38/4.44 (~P3(a1,a1,a2)), % 4.38/4.44 inference(scs_inference,[],[5,152,19,21])). % 4.38/4.44 cnf(10181,plain, % 4.38/4.44 (~P3(x101811,a1,a4)+~P3(a1,a4,x101811)), % 4.38/4.44 inference(scs_inference,[],[7225,5,152,19,21,22])). % 4.38/4.44 cnf(10186,plain, % 4.38/4.44 (P3(a1,a4,a2)), % 4.38/4.44 inference(scs_inference,[],[10178,1941])). % 4.38/4.44 cnf(10188,plain, % 4.38/4.44 (~P3(a1,a2,a4)+~P3(a1,a4,a2)), % 4.38/4.44 inference(scs_inference,[],[10178,2496])). % 4.38/4.44 cnf(10189,plain, % 4.38/4.44 (P3(a1,a2,a3)+~P3(a1,a4,a2)), % 4.38/4.44 inference(scs_inference,[],[10178,2956])). % 4.38/4.44 cnf(10191,plain, % 4.38/4.44 (~P3(a2,a1,a4)), % 4.38/4.44 inference(scs_inference,[],[296,1940,10178,2,1,10181,25])). % 4.38/4.44 cnf(10193,plain, % 4.38/4.44 (~P3(a1,a2,a4)), % 4.38/4.44 inference(scs_inference,[],[10186,10188])). % 4.38/4.44 cnf(10201,plain, % 4.38/4.44 (P3(a2,a4,a1)), % 4.38/4.44 inference(scs_inference,[],[5,1225,297,10186,10191,153,2,1,10188,10189,23,22,20,25])). % 4.38/4.44 cnf(10203,plain, % 4.38/4.44 (P3(a1,a3,a4)), % 4.38/4.44 inference(scs_inference,[],[5,1225,297,10186,10191,153,2,1,10188,10189,23,22,20,25,4610])). % 4.38/4.44 cnf(10216,plain, % 4.38/4.44 (~P3(a3,a1,a2)), % 4.38/4.44 inference(scs_inference,[],[10193,3830])). % 4.38/4.44 cnf(10244,plain, % 4.38/4.44 ($false), % 4.38/4.44 inference(scs_inference,[],[10201,10216,10203,23]), % 4.38/4.44 ['proof']). % 4.38/4.44 % SZS output end Proof % 4.38/4.44 % Total time :3.780000s %------------------------------------------------------------------------------