%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP123-2.003 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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:46 EDT 2024 % Result : Unsatisfiable 58.58s 58.74s % Output : CNFRefutation 58.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP123-2.003 : TPTP v8.2.0. Released v1.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.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 07:19:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 58.58/58.71 %------------------------------------------- % 58.58/58.71 % File :CSE---1.7 % 58.58/58.71 % Problem :theBenchmark % 58.58/58.71 % Transform :cnf % 58.58/58.71 % Format :tptp:raw % 58.58/58.71 % Command :java -jar mcs_scs.jar %d %s % 58.58/58.71 % 58.58/58.71 % Result :Theorem 58.010000s % 58.58/58.71 % Output :CNFRefutation 58.010000s % 58.58/58.71 %------------------------------------------- % 58.58/58.73 %-------------------------------------------------------------------------- % 58.58/58.73 % File : GRP123-2.003 : TPTP v8.2.0. Released v1.2.0. % 58.58/58.73 % Domain : Group Theory (Quasigroups) % 58.58/58.73 % Problem : (3,2,1) conjugate orthogonality % 58.58/58.73 % Version : [Sla93] axioms : Augmented. % 58.58/58.73 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*b=a iff ab=c. % 58.58/58.73 % Generate the multiplication table for the specified quasi- % 58.58/58.73 % group with 3 elements. % 58.58/58.73 % 58.58/58.73 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 58.58/58.73 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 58.58/58.73 % : [Zha94] Zhang (1994), Email to G. Sutcliffe % 58.58/58.73 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 58.58/58.73 % Source : [TPTP] % 58.58/58.73 % Names : % 58.58/58.73 % 58.58/58.73 % Status : Unsatisfiable % 58.58/58.73 % Rating : 0.00 v2.1.0 % 58.58/58.73 % Syntax : Number of clauses : 22 ( 15 unt; 1 nHn; 21 RR) % 58.58/58.73 % Number of literals : 42 ( 0 equ; 25 neg) % 58.58/58.73 % Maximal clause size : 5 ( 1 avg) % 58.58/58.73 % Maximal term depth : 1 ( 1 avg) % 58.58/58.73 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty) % 58.58/58.73 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 58.58/58.73 % Number of variables : 30 ( 0 sgn) % 58.58/58.73 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.58/58.73 % 58.58/58.73 % Comments : [SFS93]'s axiomatization has been modified for this. % 58.58/58.73 % : Substitution axioms are not needed, as any positive equality % 58.58/58.73 % literals should resolve on negative ones directly. % 58.58/58.73 % : [Zha94] has pointed out that either one of qg1_1 % 58.58/58.73 % or qg1_2 may be used, as each implies the other in this % 58.58/58.73 % scenario, with the help of cancellation. The dependence % 58.58/58.73 % cannot be proved, so both have been left in here. % 58.58/58.73 % : Version 2 has simple isomorphism avoidance (as mentioned in % 58.58/58.73 % [FSB93]) % 58.58/58.73 % : tptp2X: -f tptp -s3 GRP123-2.g % 58.58/58.73 %-------------------------------------------------------------------------- % 58.58/58.73 cnf(e_1_then_e_2,axiom, % 58.58/58.73 next(e_1,e_2) ). % 58.58/58.73 % 58.58/58.73 cnf(e_2_then_e_3,axiom, % 58.58/58.73 next(e_2,e_3) ). % 58.58/58.73 % 58.58/58.73 cnf(e_2_greater_e_1,axiom, % 58.58/58.73 greater(e_2,e_1) ). % 58.58/58.73 % 58.58/58.73 cnf(e_3_greater_e_1,axiom, % 58.58/58.73 greater(e_3,e_1) ). % 58.58/58.73 % 58.58/58.73 cnf(e_3_greater_e_2,axiom, % 58.58/58.73 greater(e_3,e_2) ). % 58.58/58.73 % 58.58/58.73 cnf(no_redundancy,axiom, % 58.58/58.73 ( ~ product(X,e_1,Y) % 58.58/58.73 | ~ next(X,X1) % 58.58/58.73 | ~ greater(Y,X1) ) ). % 58.58/58.73 % 58.58/58.73 cnf(element_1,axiom, % 58.58/58.73 group_element(e_1) ). % 58.58/58.73 % 58.58/58.73 cnf(element_2,axiom, % 58.58/58.73 group_element(e_2) ). % 58.58/58.73 % 58.58/58.73 cnf(element_3,axiom, % 58.58/58.73 group_element(e_3) ). % 58.58/58.73 % 58.58/58.73 cnf(e_1_is_not_e_2,axiom, % 58.58/58.73 ~ equalish(e_1,e_2) ). % 58.58/58.73 % 58.58/58.73 cnf(e_1_is_not_e_3,axiom, % 58.58/58.73 ~ equalish(e_1,e_3) ). % 58.58/58.73 % 58.58/58.73 cnf(e_2_is_not_e_1,axiom, % 58.58/58.73 ~ equalish(e_2,e_1) ). % 58.58/58.73 % 58.58/58.73 cnf(e_2_is_not_e_3,axiom, % 58.58/58.73 ~ equalish(e_2,e_3) ). % 58.58/58.73 % 58.58/58.73 cnf(e_3_is_not_e_1,axiom, % 58.58/58.73 ~ equalish(e_3,e_1) ). % 58.58/58.73 % 58.58/58.73 cnf(e_3_is_not_e_2,axiom, % 58.58/58.73 ~ equalish(e_3,e_2) ). % 58.58/58.73 % 58.58/58.73 cnf(product_total_function1,axiom, % 58.58/58.73 ( ~ group_element(X) % 58.58/58.73 | ~ group_element(Y) % 58.58/58.73 | product(X,Y,e_1) % 58.58/58.73 | product(X,Y,e_2) % 58.58/58.73 | product(X,Y,e_3) ) ). % 58.58/58.73 % 58.58/58.73 cnf(product_total_function2,axiom, % 58.58/58.73 ( ~ product(X,Y,W) % 58.58/58.73 | ~ product(X,Y,Z) % 58.58/58.73 | equalish(W,Z) ) ). % 58.58/58.73 % 58.58/58.73 cnf(product_right_cancellation,axiom, % 58.58/58.73 ( ~ product(X,W,Y) % 58.58/58.73 | ~ product(X,Z,Y) % 58.58/58.73 | equalish(W,Z) ) ). % 58.58/58.73 % 58.58/58.74 cnf(product_left_cancellation,axiom, % 58.58/58.74 ( ~ product(W,Y,X) % 58.58/58.74 | ~ product(Z,Y,X) % 58.58/58.74 | equalish(W,Z) ) ). % 58.58/58.74 % 58.58/58.74 cnf(product_idempotence,axiom, % 58.58/58.74 product(X,X,X) ). % 58.58/58.74 % 58.58/58.74 cnf(qg1_1,negated_conjecture, % 58.58/58.74 ( ~ product(X1,Y1,Z1) % 58.58/58.74 | ~ product(X2,Y2,Z1) % 58.58/58.74 | ~ product(Z2,Y1,X1) % 58.58/58.74 | ~ product(Z2,Y2,X2) % 58.58/58.74 | equalish(X1,X2) ) ). % 58.58/58.74 % 58.58/58.74 cnf(qg1_2,negated_conjecture, % 58.58/58.74 ( ~ product(X1,Y1,Z1) % 58.58/58.74 | ~ product(X2,Y2,Z1) % 58.58/58.74 | ~ product(Z2,Y1,X1) % 58.58/58.74 | ~ product(Z2,Y2,X2) % 58.58/58.74 | equalish(Y1,Y2) ) ). % 58.58/58.74 % 58.58/58.74 %-------------------------------------------------------------------------- % 58.58/58.74 %------------------------------------------- % 58.58/58.74 % Proof found % 58.58/58.74 % SZS status Theorem for theBenchmark % 58.58/58.74 % SZS output start Proof % 58.58/58.74 %ClaNum:22(EqnAxiom:0) % 58.58/58.74 %VarNum:69(SingletonVarNum:30) % 58.58/58.74 %MaxLitNum:5 % 58.58/58.74 %MaxfuncDepth:0 % 58.58/58.74 %SharedTerms:17 % 58.58/58.74 %goalClause: 21 22 % 58.58/58.74 [1]P1(a1) % 58.58/58.74 [2]P1(a2) % 58.58/58.74 [3]P1(a3) % 58.58/58.74 [4]P4(a1,a2) % 58.58/58.74 [5]P4(a2,a3) % 58.58/58.74 [6]P2(a2,a1) % 58.58/58.74 [7]P2(a3,a1) % 58.58/58.74 [8]P2(a3,a2) % 58.58/58.74 [10]~P3(a1,a2) % 58.58/58.74 [11]~P3(a1,a3) % 58.58/58.74 [12]~P3(a2,a1) % 58.58/58.74 [13]~P3(a2,a3) % 58.58/58.74 [14]~P3(a3,a1) % 58.58/58.74 [15]~P3(a3,a2) % 58.58/58.74 [9]P5(x91,x91,x91) % 58.58/58.74 [16]~P4(x161,x162)+~P2(x163,x162)+~P5(x161,a1,x163) % 58.58/58.74 [18]~P5(x183,x184,x181)+P3(x181,x182)+~P5(x183,x184,x182) % 58.58/58.74 [19]~P5(x193,x191,x194)+P3(x191,x192)+~P5(x193,x192,x194) % 58.58/58.74 [20]~P5(x201,x203,x204)+P3(x201,x202)+~P5(x202,x203,x204) % 58.58/58.74 [17]~P1(x172)+~P1(x171)+P5(x171,x172,a2)+P5(x171,x172,a3)+P5(x171,x172,a1) % 58.58/58.74 [21]~P5(x215,x211,x216)+P3(x211,x212)+~P5(x213,x212,x214)+~P5(x213,x211,x215)+~P5(x214,x212,x216) % 58.58/58.74 [22]~P5(x221,x225,x226)+P3(x221,x222)+~P5(x223,x224,x222)+~P5(x223,x225,x221)+~P5(x222,x224,x226) % 58.58/58.74 %EqnAxiom % 58.58/58.74 % 58.58/58.74 %------------------------------------------- % 58.82/58.94 cnf(344269,plain, % 58.82/58.94 (P5(x3442691,x3442691,x3442691)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344272,plain, % 58.82/58.94 (P5(x3442721,x3442721,x3442721)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344275,plain, % 58.82/58.94 (P5(x3442751,x3442751,x3442751)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344281,plain, % 58.82/58.94 (P5(a1,a2,a3)+P5(a1,a2,a2)), % 58.82/58.94 inference(scs_inference,[],[1,2,8,10,4,9,344269,344272,344275,19,18,20,16,21,17])). % 58.82/58.94 cnf(344301,plain, % 58.82/58.94 (P5(x3443011,x3443011,x3443011)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344304,plain, % 58.82/58.94 (P5(x3443041,x3443041,x3443041)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344306,plain, % 58.82/58.94 (~P5(a3,a2,a2)), % 58.82/58.94 inference(scs_inference,[],[13,9,344301,344304,19,18,20])). % 58.82/58.94 cnf(344333,plain, % 58.82/58.94 (P5(x3443331,x3443331,x3443331)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344335,plain, % 58.82/58.94 (~P5(a3,a2,a3)), % 58.82/58.94 inference(scs_inference,[],[15,9,344333,18,19])). % 58.82/58.94 cnf(344350,plain, % 58.82/58.94 (P5(x3443501,x3443501,x3443501)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344353,plain, % 58.82/58.94 (P5(x3443531,x3443531,x3443531)), % 58.82/58.94 inference(rename_variables,[],[9])). % 58.82/58.94 cnf(344360,plain, % 58.82/58.94 (~P5(a3,a2,a1)), % 58.82/58.94 inference(scs_inference,[],[6,12,11,9,344350,344353,19,20,21,344281,16,22])). % 58.82/58.94 cnf(344371,plain, % 58.82/58.94 ($false), % 58.82/58.94 inference(scs_inference,[],[344360,344335,344306,3,2,17]), % 58.82/58.94 ['proof']). % 58.93/59.08 % SZS output end Proof % 58.93/59.08 % Total time :58.010000s %------------------------------------------------------------------------------