%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP130-4.003 : 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 : 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:56 EDT 2024 % Result : Unsatisfiable 0.61s 0.73s % Output : CNFRefutation 0.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : GRP130-4.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.00/0.08 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.07/0.28 % Computer : n023.cluster.edu % 0.07/0.28 % Model : x86_64 x86_64 % 0.07/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.28 % Memory : 8042.1875MB % 0.07/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.28 % CPULimit : 300 % 0.07/0.28 % WCLimit : 300 % 0.07/0.28 % DateTime : Thu Jun 20 11:43:53 EDT 2024 % 0.07/0.28 % CPUTime : % 0.12/0.45 start to proof:theBenchmark % 0.61/0.72 %------------------------------------------- % 0.61/0.72 % File :CSE---1.7 % 0.61/0.72 % Problem :theBenchmark % 0.61/0.72 % Transform :cnf % 0.61/0.72 % Format :tptp:raw % 0.61/0.72 % Command :java -jar mcs_scs.jar %d %s % 0.61/0.72 % 0.61/0.72 % Result :Theorem 0.240000s % 0.61/0.72 % Output :CNFRefutation 0.240000s % 0.61/0.73 %------------------------------------------- % 0.61/0.73 %-------------------------------------------------------------------------- % 0.61/0.73 % File : GRP130-4.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.61/0.73 % Domain : Group Theory (Quasigroups) % 0.61/0.73 % Problem : (a.(a.b)).b = a % 0.61/0.73 % Version : [Sla93] axioms : Augmented. % 0.61/0.73 % English : Generate the multiplication table for the specified quasi- % 0.61/0.73 % group with 3 elements. % 0.61/0.73 % 0.61/0.73 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 0.61/0.73 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 0.61/0.73 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 0.61/0.73 % Source : [TPTP] % 0.61/0.73 % Names : % 0.61/0.73 % 0.61/0.73 % Status : Unsatisfiable % 0.61/0.73 % Rating : 0.00 v2.1.0 % 0.61/0.73 % Syntax : Number of clauses : 18 ( 9 unt; 3 nHn; 18 RR) % 0.61/0.73 % Number of literals : 42 ( 0 equ; 24 neg) % 0.61/0.73 % Maximal clause size : 5 ( 2 avg) % 0.61/0.73 % Maximal term depth : 1 ( 1 avg) % 0.61/0.73 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 0.61/0.73 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 0.61/0.73 % Number of variables : 30 ( 0 sgn) % 0.61/0.73 % SPC : CNF_UNS_EPR_NEQ_NHN % 0.61/0.73 % 0.61/0.73 % Comments : [SFS93]'s axiomatization has been modified for this. % 0.61/0.73 % : Substitution axioms are not needed, as any positive equality % 0.61/0.73 % literals should resolve on negative ones directly. % 0.61/0.73 % : Version 4 has surjectivity and rotation % 0.61/0.73 % : tptp2X: -f tptp -s3 GRP130-4.g % 0.61/0.73 % Bugfixes : v1.2.1 - Clauses row_surjectivity and column_surjectivity fixed. % 0.61/0.73 %-------------------------------------------------------------------------- % 0.61/0.73 cnf(row_surjectivity,axiom, % 0.61/0.73 ( ~ group_element(X) % 0.61/0.73 | ~ group_element(Y) % 0.61/0.73 | product(e_1,X,Y) % 0.61/0.73 | product(e_2,X,Y) % 0.61/0.73 | product(e_3,X,Y) ) ). % 0.61/0.73 % 0.61/0.73 cnf(column_surjectivity,axiom, % 0.61/0.73 ( ~ group_element(X) % 0.61/0.73 | ~ group_element(Y) % 0.61/0.73 | product(X,e_1,Y) % 0.61/0.73 | product(X,e_2,Y) % 0.61/0.73 | product(X,e_3,Y) ) ). % 0.61/0.73 % 0.61/0.73 cnf(qg3_1,negated_conjecture, % 0.61/0.73 ( product(X,Y,Z1) % 0.61/0.73 | ~ product(Z2,Y,X) % 0.61/0.73 | ~ product(X,Z1,Z2) ) ). % 0.61/0.73 % 0.61/0.73 cnf(qg3_2,negated_conjecture, % 0.61/0.73 ( product(X,Z1,Z2) % 0.61/0.73 | ~ product(Z2,Y,X) % 0.61/0.73 | ~ product(X,Y,Z1) ) ). % 0.61/0.73 % 0.61/0.73 cnf(element_1,axiom, % 0.61/0.73 group_element(e_1) ). % 0.61/0.73 % 0.61/0.73 cnf(element_2,axiom, % 0.61/0.73 group_element(e_2) ). % 0.61/0.73 % 0.61/0.73 cnf(element_3,axiom, % 0.61/0.73 group_element(e_3) ). % 0.61/0.73 % 0.61/0.73 cnf(e_1_is_not_e_2,axiom, % 0.61/0.73 ~ equalish(e_1,e_2) ). % 0.61/0.73 % 0.61/0.73 cnf(e_1_is_not_e_3,axiom, % 0.61/0.73 ~ equalish(e_1,e_3) ). % 0.61/0.73 % 0.61/0.73 cnf(e_2_is_not_e_1,axiom, % 0.61/0.73 ~ equalish(e_2,e_1) ). % 0.61/0.73 % 0.61/0.73 cnf(e_2_is_not_e_3,axiom, % 0.61/0.73 ~ equalish(e_2,e_3) ). % 0.61/0.73 % 0.61/0.73 cnf(e_3_is_not_e_1,axiom, % 0.61/0.73 ~ equalish(e_3,e_1) ). % 0.61/0.73 % 0.61/0.73 cnf(e_3_is_not_e_2,axiom, % 0.61/0.73 ~ equalish(e_3,e_2) ). % 0.61/0.73 % 0.61/0.73 cnf(product_total_function1,axiom, % 0.61/0.73 ( ~ group_element(X) % 0.61/0.73 | ~ group_element(Y) % 0.61/0.73 | product(X,Y,e_1) % 0.61/0.73 | product(X,Y,e_2) % 0.61/0.73 | product(X,Y,e_3) ) ). % 0.61/0.73 % 0.61/0.73 cnf(product_total_function2,axiom, % 0.61/0.73 ( ~ product(X,Y,W) % 0.61/0.73 | ~ product(X,Y,Z) % 0.61/0.73 | equalish(W,Z) ) ). % 0.61/0.73 % 0.61/0.73 cnf(product_right_cancellation,axiom, % 0.61/0.73 ( ~ product(X,W,Y) % 0.61/0.73 | ~ product(X,Z,Y) % 0.61/0.73 | equalish(W,Z) ) ). % 0.61/0.73 % 0.61/0.73 cnf(product_left_cancellation,axiom, % 0.61/0.73 ( ~ product(W,Y,X) % 0.61/0.73 | ~ product(Z,Y,X) % 0.61/0.73 | equalish(W,Z) ) ). % 0.61/0.73 % 0.61/0.73 cnf(qg3,negated_conjecture, % 0.61/0.73 ( ~ product(X,Y,Z1) % 0.61/0.73 | ~ product(X,Z1,Z2) % 0.61/0.73 | product(Z2,Y,X) ) ). % 0.61/0.73 % 0.61/0.73 %-------------------------------------------------------------------------- % 0.61/0.73 %------------------------------------------- % 0.61/0.73 % Proof found % 0.61/0.73 % SZS status Theorem for theBenchmark % 0.61/0.73 % SZS output start Proof % 0.61/0.73 %ClaNum:18(EqnAxiom:0) % 0.61/0.73 %VarNum:75(SingletonVarNum:30) % 0.61/0.73 %MaxLitNum:5 % 0.61/0.73 %MaxfuncDepth:0 % 0.61/0.73 %SharedTerms:12 % 0.61/0.73 %goalClause: 16 17 18 % 0.61/0.73 [1]P1(a1) % 0.61/0.73 [2]P1(a2) % 0.61/0.73 [3]P1(a3) % 0.61/0.73 [4]~P2(a1,a2) % 0.61/0.73 [5]~P2(a1,a3) % 0.61/0.73 [6]~P2(a2,a1) % 0.61/0.73 [7]~P2(a2,a3) % 0.61/0.73 [8]~P2(a3,a1) % 0.61/0.73 [9]~P2(a3,a2) % 0.61/0.73 [13]~P3(x133,x134,x131)+P2(x131,x132)+~P3(x133,x134,x132) % 0.61/0.73 [14]~P3(x143,x141,x144)+P2(x141,x142)+~P3(x143,x142,x144) % 0.61/0.73 [15]~P3(x151,x153,x154)+P2(x151,x152)+~P3(x152,x153,x154) % 0.61/0.73 [16]~P3(x163,x162,x164)+P3(x161,x162,x163)+~P3(x163,x164,x161) % 0.61/0.73 [17]~P3(x171,x173,x174)+P3(x171,x172,x173)+~P3(x174,x172,x171) % 0.61/0.73 [18]~P3(x181,x184,x182)+P3(x181,x182,x183)+~P3(x183,x184,x181) % 0.61/0.73 [10]~P1(x102)+~P1(x101)+P3(x101,x102,a2)+P3(x101,x102,a3)+P3(x101,x102,a1) % 0.61/0.73 [11]~P1(x112)+~P1(x111)+P3(x111,a2,x112)+P3(x111,a3,x112)+P3(x111,a1,x112) % 0.61/0.73 [12]~P1(x122)+~P1(x121)+P3(a2,x121,x122)+P3(a3,x121,x122)+P3(a1,x121,x122) % 0.61/0.73 %EqnAxiom % 0.61/0.73 % 0.61/0.73 %------------------------------------------- % 0.61/0.73 cnf(19,plain, % 0.61/0.73 (~P3(a2,x191,x192)+~P3(x192,x193,a1)+~P3(a2,x193,x191)), % 0.61/0.73 inference(scs_inference,[],[4,13,16])). % 0.61/0.73 cnf(20,plain, % 0.61/0.73 (~P3(x201,a3,x202)+~P3(x202,a1,x203)+~P3(x202,x203,x201)), % 0.61/0.73 inference(scs_inference,[],[5,14,17])). % 0.61/0.73 cnf(21,plain, % 0.61/0.73 (~P3(x211,x212,a2)+~P3(a1,x213,x211)+~P3(a2,x212,x213)), % 0.61/0.73 inference(scs_inference,[],[4,15,18])). % 0.61/0.73 cnf(22,plain, % 0.61/0.73 (~P3(x221,x222,a1)+~P3(a3,x223,x221)+~P3(a3,x222,x223)), % 0.61/0.73 inference(scs_inference,[],[8,13,16])). % 0.61/0.73 cnf(25,plain, % 0.61/0.73 (~P3(x251,x252,x253)+~P3(x253,x252,a1)+~P3(x253,a3,x251)), % 0.61/0.73 inference(scs_inference,[],[5,13,17])). % 0.61/0.73 cnf(26,plain, % 0.61/0.73 (~P3(x261,x262,a3)+~P3(x263,x262,x261)+~P3(x261,a2,x263)), % 0.61/0.73 inference(scs_inference,[],[7,13,17])). % 0.61/0.73 cnf(27,plain, % 0.61/0.73 (~P3(a2,x271,x272)+~P3(x272,x273,a3)+~P3(x272,x271,x273)), % 0.61/0.73 inference(scs_inference,[],[9,13,18])). % 0.61/0.73 cnf(28,plain, % 0.61/0.73 (~P3(x281,x282,a1)+~P3(x283,x282,x281)+~P3(x281,a2,x283)), % 0.61/0.73 inference(scs_inference,[],[6,13,17])). % 0.61/0.73 cnf(31,plain, % 0.61/0.73 (~P3(a1,x311,x312)+~P3(x312,x313,a3)+~P3(a1,x313,x311)), % 0.61/0.73 inference(scs_inference,[],[8,13,16])). % 0.61/0.73 cnf(32,plain, % 0.61/0.73 (~P3(x321,x322,a2)+~P3(a3,x323,x321)+~P3(a3,x322,x323)), % 0.61/0.73 inference(scs_inference,[],[9,13,16])). % 0.61/0.73 cnf(33,plain, % 0.61/0.73 (~P3(a3,x331,x332)+~P3(x332,x333,a1)+~P3(x332,x331,x333)), % 0.61/0.73 inference(scs_inference,[],[5,13,18])). % 0.61/0.73 cnf(34,plain, % 0.61/0.73 (~P3(x341,x342,a3)+~P3(x343,x342,x341)+~P3(x341,a1,x343)), % 0.61/0.73 inference(scs_inference,[],[5,13,17])). % 0.61/0.73 cnf(38,plain, % 0.61/0.73 (~P3(x381,x382,a2)+~P3(x383,x382,x381)+~P3(x381,a1,x383)), % 0.61/0.73 inference(scs_inference,[],[4,13,17])). % 0.61/0.73 cnf(39,plain, % 0.61/0.73 (~P3(a1,x391,x392)+~P3(x392,x393,a2)+~P3(x392,x391,x393)), % 0.61/0.73 inference(scs_inference,[],[6,13,18])). % 0.61/0.73 cnf(40,plain, % 0.61/0.73 (~P3(a3,a2,a1)+P3(a3,a3,a3)+P3(a3,a1,a3)), % 0.61/0.73 inference(scs_inference,[],[8,3,13,11])). % 0.61/0.73 cnf(41,plain, % 0.61/0.73 (P3(a3,a3,a3)+~P3(a3,a2,a1)), % 0.61/0.73 inference(scs_inference,[],[40,18])). % 0.61/0.73 cnf(48,plain, % 0.61/0.73 (~P3(x481,a2,a3)+~P3(a3,a1,x481)+P3(a3,a3,a3)), % 0.61/0.73 inference(scs_inference,[],[41,17])). % 0.61/0.73 cnf(50,plain, % 0.61/0.73 (~P3(a3,a2,a3)+~P3(a3,a2,a1)), % 0.61/0.73 inference(scs_inference,[],[41,26])). % 0.61/0.73 cnf(51,plain, % 0.61/0.73 (P3(a2,a2,a3)+P3(a1,a2,a3)+~P3(a3,a2,a1)), % 0.61/0.73 inference(scs_inference,[],[3,2,50,12])). % 0.61/0.73 cnf(52,plain, % 0.61/0.73 (~P3(a2,x521,a2)+P3(a1,a2,a3)+~P3(a3,a2,a1)), % 0.61/0.73 inference(scs_inference,[],[51,27])). % 0.61/0.73 cnf(53,plain, % 0.61/0.73 (~P3(a3,a2,a1)+~P3(a2,x531,a2)), % 0.61/0.73 inference(scs_inference,[],[52,26])). % 0.61/0.73 cnf(59,plain, % 0.61/0.73 (P3(a3,a3,a3)+P3(a3,a2,a2)+P3(a3,a2,a3)), % 0.61/0.73 inference(scs_inference,[],[2,3,41,10])). % 0.61/0.73 cnf(60,plain, % 0.61/0.73 (~P3(a3,a3,a1)+P3(a3,a2,a2)+P3(a3,a2,a3)), % 0.61/0.73 inference(scs_inference,[],[59,25])). % 0.61/0.73 cnf(61,plain, % 0.61/0.73 (P3(a3,a2,a2)+~P3(a3,a3,a1)), % 0.61/0.73 inference(scs_inference,[],[60,17])). % 0.61/0.73 cnf(70,plain, % 0.61/0.73 (P3(a3,a3,a3)+P3(a2,a2,a1)+P3(a1,a2,a1)), % 0.61/0.73 inference(scs_inference,[],[1,2,41,12])). % 0.61/0.73 cnf(71,plain, % 0.61/0.73 (P3(a2,a2,a1)+~P3(a3,a3,a1)+P3(a1,a2,a1)), % 0.61/0.73 inference(scs_inference,[],[70,25])). % 0.61/0.73 cnf(101,plain, % 0.61/0.73 (~P3(a3,a2,a1)+P3(a2,a2,a2)+P3(a2,a3,a2)), % 0.61/0.73 inference(scs_inference,[],[2,53,11])). % 0.61/0.73 cnf(112,plain, % 0.61/0.73 (~P3(a3,a2,a1)+P3(a2,a3,a2)), % 0.61/0.73 inference(scs_inference,[],[53,101])). % 0.61/0.73 cnf(118,plain, % 0.61/0.73 (~P3(a3,a2,a1)), % 0.61/0.73 inference(scs_inference,[],[53,112])). % 0.61/0.73 cnf(119,plain, % 0.61/0.73 (P3(a3,a3,a1)+P3(a3,a1,a1)), % 0.61/0.73 inference(scs_inference,[],[118,1,3,11])). % 0.61/0.73 cnf(127,plain, % 0.61/0.73 (P3(a3,a1,a1)+P3(a3,a2,a2)), % 0.61/0.73 inference(scs_inference,[],[61,119])). % 0.61/0.73 cnf(128,plain, % 0.61/0.73 (P3(a1,a1,a3)+P3(a3,a2,a2)), % 0.61/0.74 inference(scs_inference,[],[127,16])). % 0.61/0.74 cnf(129,plain, % 0.61/0.74 (~P3(a1,a2,a3)+P3(a1,a1,a3)), % 0.61/0.74 inference(scs_inference,[],[118,128,18])). % 0.61/0.74 cnf(130,plain, % 0.61/0.74 (~P3(a1,a2,a3)+~P3(a1,a3,a1)), % 0.61/0.74 inference(scs_inference,[],[129,31])). % 0.61/0.74 cnf(131,plain, % 0.61/0.74 (~P3(x1311,a3,a1)+~P3(a1,a1,x1311)+~P3(a1,a2,a3)), % 0.61/0.74 inference(scs_inference,[],[130,17])). % 0.61/0.74 cnf(147,plain, % 0.61/0.74 (~P3(a3,a3,a1)+~P3(a2,a2,a1)), % 0.61/0.74 inference(scs_inference,[],[61,22])). % 0.61/0.74 cnf(148,plain, % 0.61/0.74 (P3(a3,a1,a1)+~P3(a2,a2,a1)), % 0.61/0.74 inference(scs_inference,[],[147,119])). % 0.61/0.74 cnf(149,plain, % 0.61/0.74 (P3(a1,a1,a3)+~P3(a2,a2,a1)), % 0.61/0.74 inference(scs_inference,[],[148,16])). % 0.61/0.74 cnf(150,plain, % 0.61/0.74 (P3(a1,a1,a3)+P3(a1,a2,a1)), % 0.61/0.74 inference(scs_inference,[],[118,1,2,149,12])). % 0.61/0.74 cnf(151,plain, % 0.61/0.74 (P3(a1,a1,a3)), % 0.61/0.74 inference(scs_inference,[],[150,28])). % 0.61/0.74 cnf(165,plain, % 0.61/0.74 (P3(a3,a3,a1)), % 0.61/0.74 inference(scs_inference,[],[118,151,1,3,34,31,13,18,16,15,11])). % 0.61/0.74 cnf(186,plain, % 0.61/0.74 (~P3(a3,a2,a2)), % 0.61/0.74 inference(scs_inference,[],[118,151,1,3,34,31,13,18,16,15,11,10,38,48,71,131,33,39,17,22,32,20,14,147,148,19,21])). % 0.61/0.74 cnf(218,plain, % 0.61/0.74 ($false), % 0.61/0.74 inference(scs_inference,[],[165,186,61]), % 0.61/0.74 ['proof']). % 0.61/0.74 % SZS output end Proof % 0.61/0.74 % Total time :0.240000s %------------------------------------------------------------------------------