%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP123-4.003 : 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 : n024.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:47 EDT 2024 % Result : Unsatisfiable 58.54s 58.68s % Output : CNFRefutation 59.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP123-4.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 09:35:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.47/0.54 start to proof:theBenchmark % 58.54/58.65 %------------------------------------------- % 58.54/58.65 % File :CSE---1.7 % 58.54/58.65 % Problem :theBenchmark % 58.54/58.65 % Transform :cnf % 58.54/58.65 % Format :tptp:raw % 58.54/58.65 % Command :java -jar mcs_scs.jar %d %s % 58.54/58.65 % 58.54/58.65 % Result :Theorem 58.000000s % 58.54/58.65 % Output :CNFRefutation 58.000000s % 58.54/58.65 %------------------------------------------- % 58.54/58.68 %-------------------------------------------------------------------------- % 58.54/58.68 % File : GRP123-4.003 : TPTP v8.2.0. Bugfixed v1.2.1. % 58.54/58.68 % Domain : Group Theory (Quasigroups) % 58.54/58.68 % Problem : (3,2,1) conjugate orthogonality % 58.54/58.68 % Version : [Sla93] axioms : Augmented. % 58.54/58.68 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*b=a iff ab=c. % 58.54/58.68 % Generate the multiplication table for the specified quasi- % 58.54/58.68 % group with 3 elements. % 58.54/58.68 % 58.54/58.68 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 58.54/58.68 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 58.54/58.68 % : [Zha94] Zhang (1994), Email to G. Sutcliffe % 58.54/58.68 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 58.54/58.68 % Source : [TPTP] % 58.54/58.68 % Names : % 58.54/58.68 % 58.54/58.68 % Status : Unsatisfiable % 58.54/58.68 % Rating : 0.00 v2.1.0 % 58.54/58.68 % Syntax : Number of clauses : 18 ( 10 unt; 3 nHn; 17 RR) % 58.54/58.68 % Number of literals : 44 ( 0 equ; 26 neg) % 58.54/58.68 % Maximal clause size : 5 ( 2 avg) % 58.54/58.68 % Maximal term depth : 1 ( 1 avg) % 58.54/58.68 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 58.54/58.68 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 58.54/58.68 % Number of variables : 31 ( 0 sgn) % 58.54/58.68 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.54/58.68 % 58.54/58.68 % Comments : [SFS93]'s axiomatization has been modified for this. % 58.54/58.68 % : Substitution axioms are not needed, as any positive equality % 58.54/58.68 % literals should resolve on negative ones directly. % 58.54/58.68 % : [Zha94] has pointed out that either one of qg1_1 % 58.54/58.68 % or qg1_2 may be used, as each implies the other in this % 58.54/58.68 % scenario, with the help of cancellation. The dependence % 58.54/58.68 % cannot be proved, so both have been left in here. % 58.54/58.68 % : Version 4 has surjectivity and rotation % 58.54/58.68 % : tptp2X: -f tptp -s3 GRP123-4.g % 58.54/58.68 % Bugfixes : v1.2.1 - Clauses row_surjectivity and column_surjectivity fixed. % 58.54/58.68 %-------------------------------------------------------------------------- % 58.54/58.68 cnf(row_surjectivity,axiom, % 58.54/58.68 ( ~ group_element(X) % 58.54/58.68 | ~ group_element(Y) % 58.54/58.68 | product(e_1,X,Y) % 58.54/58.68 | product(e_2,X,Y) % 58.54/58.68 | product(e_3,X,Y) ) ). % 58.54/58.68 % 58.54/58.68 cnf(column_surjectivity,axiom, % 58.54/58.68 ( ~ group_element(X) % 58.54/58.68 | ~ group_element(Y) % 58.54/58.68 | product(X,e_1,Y) % 58.54/58.68 | product(X,e_2,Y) % 58.54/58.68 | product(X,e_3,Y) ) ). % 58.54/58.68 % 58.54/58.68 cnf(element_1,axiom, % 58.54/58.68 group_element(e_1) ). % 58.54/58.68 % 58.54/58.68 cnf(element_2,axiom, % 58.54/58.68 group_element(e_2) ). % 58.54/58.68 % 58.54/58.68 cnf(element_3,axiom, % 58.54/58.68 group_element(e_3) ). % 58.54/58.68 % 58.54/58.68 cnf(e_1_is_not_e_2,axiom, % 58.54/58.68 ~ equalish(e_1,e_2) ). % 58.54/58.68 % 58.54/58.68 cnf(e_1_is_not_e_3,axiom, % 58.54/58.68 ~ equalish(e_1,e_3) ). % 58.54/58.68 % 58.54/58.68 cnf(e_2_is_not_e_1,axiom, % 58.54/58.68 ~ equalish(e_2,e_1) ). % 58.54/58.68 % 58.54/58.68 cnf(e_2_is_not_e_3,axiom, % 58.54/58.68 ~ equalish(e_2,e_3) ). % 58.54/58.68 % 58.54/58.68 cnf(e_3_is_not_e_1,axiom, % 58.54/58.68 ~ equalish(e_3,e_1) ). % 58.54/58.68 % 58.54/58.68 cnf(e_3_is_not_e_2,axiom, % 58.54/58.68 ~ equalish(e_3,e_2) ). % 58.54/58.68 % 58.54/58.68 cnf(product_total_function1,axiom, % 58.54/58.68 ( ~ group_element(X) % 58.54/58.68 | ~ group_element(Y) % 58.54/58.68 | product(X,Y,e_1) % 58.54/58.68 | product(X,Y,e_2) % 58.54/58.68 | product(X,Y,e_3) ) ). % 58.54/58.68 % 58.54/58.68 cnf(product_total_function2,axiom, % 58.54/58.68 ( ~ product(X,Y,W) % 58.54/58.68 | ~ product(X,Y,Z) % 58.54/58.68 | equalish(W,Z) ) ). % 58.54/58.68 % 58.54/58.68 cnf(product_right_cancellation,axiom, % 58.54/58.68 ( ~ product(X,W,Y) % 58.54/58.68 | ~ product(X,Z,Y) % 58.54/58.68 | equalish(W,Z) ) ). % 58.54/58.68 % 58.54/58.68 cnf(product_left_cancellation,axiom, % 58.54/58.68 ( ~ product(W,Y,X) % 58.54/58.68 | ~ product(Z,Y,X) % 58.54/58.68 | equalish(W,Z) ) ). % 58.54/58.68 % 58.54/58.68 cnf(product_idempotence,axiom, % 58.54/58.68 product(X,X,X) ). % 58.54/58.68 % 58.54/58.68 cnf(qg1_1,negated_conjecture, % 58.54/58.68 ( ~ product(X1,Y1,Z1) % 58.54/58.68 | ~ product(X2,Y2,Z1) % 58.54/58.68 | ~ product(Z2,Y1,X1) % 58.54/58.68 | ~ product(Z2,Y2,X2) % 58.54/58.68 | equalish(X1,X2) ) ). % 58.54/58.68 % 58.54/58.68 cnf(qg1_2,negated_conjecture, % 58.54/58.68 ( ~ product(X1,Y1,Z1) % 58.54/58.68 | ~ product(X2,Y2,Z1) % 58.54/58.68 | ~ product(Z2,Y1,X1) % 58.54/58.68 | ~ product(Z2,Y2,X2) % 58.54/58.68 | equalish(Y1,Y2) ) ). % 58.54/58.68 % 58.54/58.68 %-------------------------------------------------------------------------- % 58.54/58.68 %------------------------------------------- % 58.54/58.68 % Proof found % 58.54/58.68 % SZS status Theorem for theBenchmark % 58.54/58.68 % SZS output start Proof % 58.61/58.70 %ClaNum:18(EqnAxiom:0) % 58.61/58.70 %VarNum:79(SingletonVarNum:31) % 58.61/58.70 %MaxLitNum:5 % 58.61/58.70 %MaxfuncDepth:0 % 58.61/58.70 %SharedTerms:12 % 58.61/58.70 %goalClause: 17 18 % 58.61/58.70 [1]P1(a1) % 58.61/58.70 [2]P1(a2) % 58.61/58.70 [3]P1(a3) % 58.61/58.70 [5]~P2(a1,a2) % 58.61/58.70 [6]~P2(a1,a3) % 58.61/58.70 [7]~P2(a2,a1) % 58.61/58.70 [8]~P2(a2,a3) % 58.61/58.70 [9]~P2(a3,a1) % 58.61/58.70 [10]~P2(a3,a2) % 58.61/58.70 [4]P3(x41,x41,x41) % 58.61/58.70 [14]~P3(x143,x144,x141)+P2(x141,x142)+~P3(x143,x144,x142) % 58.61/58.70 [15]~P3(x153,x151,x154)+P2(x151,x152)+~P3(x153,x152,x154) % 58.61/58.70 [16]~P3(x161,x163,x164)+P2(x161,x162)+~P3(x162,x163,x164) % 58.61/58.70 [11]~P1(x112)+~P1(x111)+P3(x111,x112,a2)+P3(x111,x112,a3)+P3(x111,x112,a1) % 58.61/58.70 [12]~P1(x122)+~P1(x121)+P3(x121,a2,x122)+P3(x121,a3,x122)+P3(x121,a1,x122) % 58.61/58.70 [13]~P1(x132)+~P1(x131)+P3(a2,x131,x132)+P3(a3,x131,x132)+P3(a1,x131,x132) % 58.61/58.70 [17]~P3(x175,x171,x176)+P2(x171,x172)+~P3(x173,x172,x174)+~P3(x173,x171,x175)+~P3(x174,x172,x176) % 58.61/58.70 [18]~P3(x181,x185,x186)+P2(x181,x182)+~P3(x183,x184,x182)+~P3(x183,x185,x181)+~P3(x182,x184,x186) % 58.61/58.70 %EqnAxiom % 58.61/58.70 % 58.61/58.70 %------------------------------------------- % 58.83/58.92 cnf(346343,plain, % 58.83/58.92 (~P3(a1,a2,a1)), % 58.83/58.92 inference(scs_inference,[],[5,4,15])). % 58.83/58.92 cnf(346344,plain, % 58.83/58.92 (P3(x3463441,x3463441,x3463441)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346346,plain, % 58.83/58.92 (~P3(a2,a1,a1)), % 58.83/58.92 inference(scs_inference,[],[5,4,346344,15,16])). % 58.83/58.92 cnf(346347,plain, % 58.83/58.92 (P3(x3463471,x3463471,x3463471)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346349,plain, % 58.83/58.92 (~P3(a1,a1,a2)), % 58.83/58.92 inference(scs_inference,[],[5,4,346344,346347,15,16,14])). % 58.83/58.92 cnf(346350,plain, % 58.83/58.92 (P3(x3463501,x3463501,x3463501)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346354,plain, % 58.83/58.92 (P3(a1,a2,a3)+P3(a1,a2,a2)), % 58.83/58.92 inference(scs_inference,[],[1,2,5,4,346344,346347,346350,15,16,14,17,11])). % 58.83/58.92 cnf(346361,plain, % 58.83/58.92 (P3(x3463611,x3463611,x3463611)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346364,plain, % 58.83/58.92 (P3(x3463641,x3463641,x3463641)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346367,plain, % 58.83/58.92 (P3(x3463671,x3463671,x3463671)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346371,plain, % 58.83/58.92 (P3(a2,a3,a1)+P3(a2,a2,a1)), % 58.83/58.92 inference(scs_inference,[],[1,6,346346,2,4,346361,346364,346367,15,16,14,18,12])). % 58.83/58.92 cnf(346373,plain, % 58.83/58.92 (~P3(a1,a3,a2)+P3(a2,a2,a1)), % 58.83/58.92 inference(scs_inference,[],[1,6,9,346346,2,4,346361,346364,346367,15,16,14,18,12,17])). % 58.83/58.92 cnf(346377,plain, % 58.83/58.92 (~P3(a1,a2,a2)), % 58.83/58.92 inference(scs_inference,[],[7,4,16])). % 58.83/58.92 cnf(346378,plain, % 58.83/58.92 (P3(x3463781,x3463781,x3463781)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346381,plain, % 58.83/58.92 (P3(x3463811,x3463811,x3463811)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346384,plain, % 58.83/58.92 (P3(x3463841,x3463841,x3463841)), % 58.83/58.92 inference(rename_variables,[],[4])). % 58.83/58.92 cnf(346389,plain, % 58.83/58.92 (~P3(a1,a3,a2)), % 58.83/58.92 inference(scs_inference,[],[7,4,346378,346381,346384,16,15,14,17,346371,346373])). % 58.83/58.92 cnf(346390,plain, % 58.83/58.92 (P3(a3,a2,a1)), % 58.83/58.92 inference(scs_inference,[],[1,7,346343,2,4,346378,346381,346384,16,15,14,17,346371,346373,13])). % 58.83/58.92 cnf(346392,plain, % 58.83/58.92 (P3(a1,a2,a3)), % 58.83/58.92 inference(scs_inference,[],[1,7,346343,2,4,346378,346381,346384,16,15,14,17,346371,346373,13,346354])). % 58.83/58.92 cnf(346402,plain, % 58.83/58.92 ($false), % 58.83/58.92 inference(scs_inference,[],[1,346389,8,346349,346377,346390,346392,6,2,4,15,16,14,12]), % 58.83/58.92 ['proof']). % 59.06/59.15 % SZS output end Proof % 59.06/59.15 % Total time :58.000000s %------------------------------------------------------------------------------