%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP125-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 : n032.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:51 EDT 2024 % Result : Unsatisfiable 0.77s 0.88s % Output : CNFRefutation 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : GRP125-4.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Thu Jun 20 08:07:23 EDT 2024 % 0.09/0.29 % CPUTime : % 0.13/0.46 start to proof:theBenchmark % 0.77/0.87 %------------------------------------------- % 0.77/0.87 % File :CSE---1.7 % 0.77/0.87 % Problem :theBenchmark % 0.77/0.87 % Transform :cnf % 0.77/0.87 % Format :tptp:raw % 0.77/0.87 % Command :java -jar mcs_scs.jar %d %s % 0.77/0.87 % 0.77/0.87 % Result :Theorem 0.380000s % 0.77/0.87 % Output :CNFRefutation 0.380000s % 0.77/0.87 %------------------------------------------- % 0.77/0.88 %-------------------------------------------------------------------------- % 0.77/0.88 % File : GRP125-4.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.77/0.88 % Domain : Group Theory (Quasigroups) % 0.77/0.88 % Problem : (a.b).(b.a) = a % 0.77/0.88 % Version : [Sla93] axioms : Augmented. % 0.77/0.88 % English : Generate the multiplication table for the specified quasi- % 0.77/0.88 % group with 3 elements. % 0.77/0.88 % 0.77/0.88 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 0.77/0.88 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 0.77/0.88 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 0.77/0.88 % Source : [TPTP] % 0.77/0.88 % Names : % 0.77/0.88 % 0.77/0.88 % Status : Unsatisfiable % 0.77/0.88 % Rating : 0.00 v2.1.0 % 0.77/0.88 % Syntax : Number of clauses : 19 ( 10 unt; 3 nHn; 18 RR) % 0.77/0.88 % Number of literals : 43 ( 0 equ; 24 neg) % 0.77/0.88 % Maximal clause size : 5 ( 2 avg) % 0.77/0.88 % Maximal term depth : 1 ( 1 avg) % 0.77/0.88 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 0.77/0.88 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 0.77/0.88 % Number of variables : 31 ( 0 sgn) % 0.77/0.88 % SPC : CNF_UNS_EPR_NEQ_NHN % 0.77/0.88 % 0.77/0.88 % Comments : [SFS93]'s axiomatization has been modified for this. % 0.77/0.88 % : Substitution axioms are not needed, as any positive equality % 0.77/0.88 % literals should resolve on negative ones directly. % 0.77/0.88 % : Version 4 has surjectivity and rotation % 0.77/0.88 % : tptp2X: -f tptp -s3 GRP125-4.g % 0.77/0.88 % Bugfixes : v1.2.1 - Clauses row_surjectivity and column_surjectivity fixed. % 0.77/0.88 %-------------------------------------------------------------------------- % 0.77/0.88 cnf(row_surjectivity,axiom, % 0.77/0.88 ( ~ group_element(X) % 0.77/0.88 | ~ group_element(Y) % 0.77/0.88 | product(e_1,X,Y) % 0.77/0.88 | product(e_2,X,Y) % 0.77/0.88 | product(e_3,X,Y) ) ). % 0.77/0.88 % 0.77/0.88 cnf(column_surjectivity,axiom, % 0.77/0.88 ( ~ group_element(X) % 0.77/0.88 | ~ group_element(Y) % 0.77/0.88 | product(X,e_1,Y) % 0.77/0.88 | product(X,e_2,Y) % 0.77/0.88 | product(X,e_3,Y) ) ). % 0.77/0.88 % 0.77/0.88 cnf(qg3_1,negated_conjecture, % 0.77/0.88 ( product(X,Y,Z1) % 0.77/0.88 | ~ product(Z1,Z2,X) % 0.77/0.88 | ~ product(Y,X,Z2) ) ). % 0.77/0.88 % 0.77/0.88 cnf(qg3_2,negated_conjecture, % 0.77/0.88 ( product(Y,X,Z2) % 0.77/0.88 | ~ product(Z1,Z2,X) % 0.77/0.88 | ~ product(X,Y,Z1) ) ). % 0.77/0.88 % 0.77/0.88 cnf(element_1,axiom, % 0.77/0.88 group_element(e_1) ). % 0.77/0.88 % 0.77/0.88 cnf(element_2,axiom, % 0.77/0.88 group_element(e_2) ). % 0.77/0.88 % 0.77/0.88 cnf(element_3,axiom, % 0.77/0.88 group_element(e_3) ). % 0.77/0.88 % 0.77/0.88 cnf(e_1_is_not_e_2,axiom, % 0.77/0.88 ~ equalish(e_1,e_2) ). % 0.77/0.88 % 0.77/0.88 cnf(e_1_is_not_e_3,axiom, % 0.77/0.88 ~ equalish(e_1,e_3) ). % 0.77/0.88 % 0.77/0.88 cnf(e_2_is_not_e_1,axiom, % 0.77/0.88 ~ equalish(e_2,e_1) ). % 0.77/0.88 % 0.77/0.88 cnf(e_2_is_not_e_3,axiom, % 0.77/0.88 ~ equalish(e_2,e_3) ). % 0.77/0.88 % 0.77/0.88 cnf(e_3_is_not_e_1,axiom, % 0.77/0.88 ~ equalish(e_3,e_1) ). % 0.77/0.88 % 0.77/0.88 cnf(e_3_is_not_e_2,axiom, % 0.77/0.88 ~ equalish(e_3,e_2) ). % 0.77/0.88 % 0.77/0.88 cnf(product_total_function1,axiom, % 0.77/0.88 ( ~ group_element(X) % 0.77/0.88 | ~ group_element(Y) % 0.77/0.88 | product(X,Y,e_1) % 0.77/0.88 | product(X,Y,e_2) % 0.77/0.88 | product(X,Y,e_3) ) ). % 0.77/0.88 % 0.77/0.88 cnf(product_total_function2,axiom, % 0.77/0.88 ( ~ product(X,Y,W) % 0.77/0.88 | ~ product(X,Y,Z) % 0.77/0.88 | equalish(W,Z) ) ). % 0.77/0.88 % 0.77/0.88 cnf(product_right_cancellation,axiom, % 0.77/0.88 ( ~ product(X,W,Y) % 0.77/0.88 | ~ product(X,Z,Y) % 0.77/0.88 | equalish(W,Z) ) ). % 0.77/0.88 % 0.77/0.88 cnf(product_left_cancellation,axiom, % 0.77/0.88 ( ~ product(W,Y,X) % 0.77/0.88 | ~ product(Z,Y,X) % 0.77/0.88 | equalish(W,Z) ) ). % 0.77/0.88 % 0.77/0.88 cnf(product_idempotence,axiom, % 0.77/0.88 product(X,X,X) ). % 0.77/0.88 % 0.77/0.88 cnf(qg3,negated_conjecture, % 0.77/0.88 ( ~ product(X,Y,Z1) % 0.77/0.88 | ~ product(Y,X,Z2) % 0.77/0.88 | product(Z1,Z2,X) ) ). % 0.77/0.88 % 0.77/0.88 %-------------------------------------------------------------------------- % 0.77/0.88 %------------------------------------------- % 0.77/0.88 % Proof found % 0.77/0.88 % SZS status Theorem for theBenchmark % 0.77/0.88 % SZS output start Proof % 0.77/0.88 %ClaNum:19(EqnAxiom:0) % 0.77/0.88 %VarNum:78(SingletonVarNum:31) % 0.77/0.88 %MaxLitNum:5 % 0.77/0.88 %MaxfuncDepth:0 % 0.77/0.88 %SharedTerms:12 % 0.77/0.88 %goalClause: 17 18 19 % 0.77/0.88 [1]P1(a1) % 0.77/0.88 [2]P1(a2) % 0.77/0.88 [3]P1(a3) % 0.77/0.88 [5]~P2(a1,a2) % 0.77/0.88 [6]~P2(a1,a3) % 0.77/0.88 [7]~P2(a2,a1) % 0.77/0.88 [8]~P2(a2,a3) % 0.77/0.88 [9]~P2(a3,a1) % 0.77/0.88 [10]~P2(a3,a2) % 0.77/0.88 [4]P3(x41,x41,x41) % 0.77/0.88 [14]~P3(x143,x144,x141)+P2(x141,x142)+~P3(x143,x144,x142) % 0.77/0.88 [15]~P3(x153,x151,x154)+P2(x151,x152)+~P3(x153,x152,x154) % 0.77/0.88 [16]~P3(x161,x163,x164)+P2(x161,x162)+~P3(x162,x163,x164) % 0.77/0.88 [17]~P3(x173,x174,x171)+P3(x171,x172,x173)+~P3(x174,x173,x172) % 0.77/0.88 [18]~P3(x182,x181,x184)+P3(x181,x182,x183)+~P3(x184,x183,x182) % 0.77/0.88 [19]~P3(x192,x191,x194)+P3(x191,x192,x193)+~P3(x193,x194,x191) % 0.77/0.88 [11]~P1(x112)+~P1(x111)+P3(x111,x112,a2)+P3(x111,x112,a3)+P3(x111,x112,a1) % 0.77/0.88 [12]~P1(x122)+~P1(x121)+P3(x121,a2,x122)+P3(x121,a3,x122)+P3(x121,a1,x122) % 0.77/0.88 [13]~P1(x132)+~P1(x131)+P3(a2,x131,x132)+P3(a3,x131,x132)+P3(a1,x131,x132) % 0.77/0.88 %EqnAxiom % 0.77/0.88 % 0.77/0.88 %------------------------------------------- % 0.77/0.88 cnf(52,plain, % 0.77/0.88 (P3(a2,a1,a2)+P3(a2,a3,a1)+P3(a2,a1,a1)), % 0.77/0.88 inference(scs_inference,[],[4,1,2,17,12])). % 0.77/0.88 cnf(238,plain, % 0.77/0.88 (~P3(a2,a1,a1)), % 0.77/0.88 inference(scs_inference,[],[4,5,14,19])). % 0.77/0.88 cnf(239,plain, % 0.77/0.88 (P3(a2,a1,a2)+P3(a2,a3,a1)), % 0.77/0.88 inference(scs_inference,[],[238,52])). % 0.77/0.88 cnf(454,plain, % 0.77/0.88 (P3(a1,a2,a1)+P3(a2,a3,a1)), % 0.77/0.88 inference(scs_inference,[],[239,18])). % 0.77/0.88 cnf(485,plain, % 0.77/0.88 (~P3(a1,a1,a2)+P3(a2,a3,a1)), % 0.77/0.88 inference(scs_inference,[],[238,454,19])). % 0.77/0.88 cnf(516,plain, % 0.77/0.88 (~P3(a1,a2,a1)+P3(a2,a3,a1)), % 0.77/0.88 inference(scs_inference,[],[4,485,18])). % 0.77/0.88 cnf(547,plain, % 0.77/0.88 (P3(a2,a3,a1)), % 0.77/0.88 inference(scs_inference,[],[516,454])). % 0.77/0.88 cnf(550,plain, % 0.77/0.88 (~P3(a3,a2,x5501)+P3(x5501,a1,a3)), % 0.77/0.88 inference(scs_inference,[],[4,547,14,17])). % 0.77/0.88 cnf(552,plain, % 0.77/0.88 (~P3(a1,x5521,a2)+P3(x5521,a1,a3)), % 0.77/0.88 inference(scs_inference,[],[4,547,14,17,18])). % 0.77/0.88 cnf(559,plain, % 0.77/0.88 (~P3(x5591,a1,a3)+P3(a1,x5591,a2)), % 0.77/0.88 inference(scs_inference,[],[4,547,15,19])). % 0.77/0.88 cnf(592,plain, % 0.77/0.88 (~P3(a1,a3,a2)), % 0.77/0.88 inference(scs_inference,[],[4,6,552,15])). % 0.77/0.88 cnf(593,plain, % 0.77/0.88 (~P3(a3,a1,a3)), % 0.77/0.88 inference(scs_inference,[],[592,559])). % 0.77/0.88 cnf(692,plain, % 0.77/0.88 (P3(x6921,x6921,x6921)), % 0.77/0.88 inference(rename_variables,[],[4])). % 0.77/0.88 cnf(696,plain, % 0.77/0.88 (~P3(a1,a1,a3)), % 0.77/0.88 inference(scs_inference,[],[4,692,238,17,16,559])). % 0.77/0.88 cnf(700,plain, % 0.77/0.88 (P3(a3,a3,a1)+P3(a3,a1,a1)), % 0.77/0.88 inference(scs_inference,[],[3,4,692,238,1,17,16,559,550,12])). % 0.77/0.88 cnf(766,plain, % 0.77/0.88 (P3(a3,a1,a1)), % 0.77/0.88 inference(scs_inference,[],[696,700,17])). % 0.77/0.88 cnf(767,plain, % 0.77/0.88 (P3(a1,a3,a3)), % 0.77/0.88 inference(scs_inference,[],[766,19])). % 0.77/0.88 cnf(800,plain, % 0.77/0.88 ($false), % 0.77/0.88 inference(scs_inference,[],[4,593,767,19]), % 0.77/0.88 ['proof']). % 0.77/0.88 % SZS output end Proof % 0.77/0.88 % Total time :0.380000s %------------------------------------------------------------------------------