%-------------------------------------------------------------------------- % File : GRP124-3.005 : TPTP v2.4.1. Released v1.2.0. % Domain : Group Theory (Quasigroups) % Problem : (3,1,2) conjugate orthogonality % Version : [Sla93] axioms : Augmented. % English : If ab=xy and a*b = x*y then a=x and b=y, where c*a=b iff ab=c. % Generate the multiplication table for the specified quasi- % group with 5 elements. % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % : [Sla93] Slaney (1993), Email to G. Sutcliffe % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % Source : [TPTP] % Names : % Status : satisfiable % Rating : 0.60 v2.4.0, 0.67 v2.2.0, 1.00 v2.1.0 % Syntax : Number of clauses : 59 ( 2 non-Horn; 47 unit; 58 RR) % Number of literals : 102 ( 0 equality) % Maximal clause size : 7 ( 1 average) % Number of predicates : 6 ( 0 propositional; 1-3 arity) % Number of functors : 6 ( 6 constant; 0-0 arity) % Number of variables : 47 ( 0 singleton) % Maximal term depth : 1 ( 1 average) % Comments : [SFS93]'s axiomatization has been modified for this. % : Substitution axioms are not needed, as any positive equality % literals should resolve on negative ones directly. % : As in GRP123-1, either one of qg2_1 or qg2_2 may be used, as % each implies the other in this scenario, with the help of % cancellation. The dependence cannot be proved, so both have % been left in here. % : Version 3 has complex isomorphism avoidance (mentioned in % [SFS95] % : tptp2X: -f tptp -s5 GRP124-3.g % : tptp2X -f tptp GRP124-3.005.p %-------------------------------------------------------------------------- input_clause(e_0_then_e_1,axiom, [++ next(e_0, e_1)]). input_clause(e_1_then_e_2,axiom, [++ next(e_1, e_2)]). input_clause(e_2_then_e_3,axiom, [++ next(e_2, e_3)]). input_clause(e_3_then_e_4,axiom, [++ next(e_3, e_4)]). input_clause(e_4_then_e_5,axiom, [++ next(e_4, e_5)]). input_clause(e_1_greater_e_0,axiom, [++ greater(e_1, e_0)]). input_clause(e_2_greater_e_0,axiom, [++ greater(e_2, e_0)]). input_clause(e_3_greater_e_0,axiom, [++ greater(e_3, e_0)]). input_clause(e_4_greater_e_0,axiom, [++ greater(e_4, e_0)]). input_clause(e_5_greater_e_0,axiom, [++ greater(e_5, e_0)]). input_clause(e_2_greater_e_1,axiom, [++ greater(e_2, e_1)]). input_clause(e_3_greater_e_1,axiom, [++ greater(e_3, e_1)]). input_clause(e_4_greater_e_1,axiom, [++ greater(e_4, e_1)]). input_clause(e_5_greater_e_1,axiom, [++ greater(e_5, e_1)]). input_clause(e_3_greater_e_2,axiom, [++ greater(e_3, e_2)]). input_clause(e_4_greater_e_2,axiom, [++ greater(e_4, e_2)]). input_clause(e_5_greater_e_2,axiom, [++ greater(e_5, e_2)]). input_clause(e_4_greater_e_3,axiom, [++ greater(e_4, e_3)]). input_clause(e_5_greater_e_3,axiom, [++ greater(e_5, e_3)]). input_clause(e_5_greater_e_4,axiom, [++ greater(e_5, e_4)]). input_clause(cycle1,axiom, [-- cycle(X, Y), -- cycle(X, Z), ++ equalish(Y, Z)]). input_clause(cycle2,axiom, [-- group_element(X), ++ cycle(X, e_0), ++ cycle(X, e_1), ++ cycle(X, e_2), ++ cycle(X, e_3), ++ cycle(X, e_4)]). input_clause(cycle3,axiom, [++ cycle(e_5, e_0)]). input_clause(cycle4,axiom, [-- cycle(X, Y), -- cycle(W, Z), -- next(X, W), -- greater(Y, e_0), -- next(Z, Z1), ++ equalish(Y, Z1)]). input_clause(cycle5,axiom, [-- cycle(X, Z1), -- cycle(Y, e_0), -- cycle(W, Z2), -- next(Y, W), -- greater(Y, X), -- greater(Z1, Z2)]). input_clause(cycle6,axiom, [-- cycle(X, e_0), -- product(X, e_1, Y), -- greater(Y, X)]). input_clause(cycle7,axiom, [-- cycle(X, Y), -- product(X, e_1, Z), -- greater(Y, e_0), -- next(X, X1), ++ equalish(Z, X1)]). input_clause(element_1,axiom, [++ group_element(e_1)]). input_clause(element_2,axiom, [++ group_element(e_2)]). input_clause(element_3,axiom, [++ group_element(e_3)]). input_clause(element_4,axiom, [++ group_element(e_4)]). input_clause(element_5,axiom, [++ group_element(e_5)]). input_clause(e_1_is_not_e_2,axiom, [-- equalish(e_1, e_2)]). input_clause(e_1_is_not_e_3,axiom, [-- equalish(e_1, e_3)]). input_clause(e_1_is_not_e_4,axiom, [-- equalish(e_1, e_4)]). input_clause(e_1_is_not_e_5,axiom, [-- equalish(e_1, e_5)]). input_clause(e_2_is_not_e_1,axiom, [-- equalish(e_2, e_1)]). input_clause(e_2_is_not_e_3,axiom, [-- equalish(e_2, e_3)]). input_clause(e_2_is_not_e_4,axiom, [-- equalish(e_2, e_4)]). input_clause(e_2_is_not_e_5,axiom, [-- equalish(e_2, e_5)]). input_clause(e_3_is_not_e_1,axiom, [-- equalish(e_3, e_1)]). input_clause(e_3_is_not_e_2,axiom, [-- equalish(e_3, e_2)]). input_clause(e_3_is_not_e_4,axiom, [-- equalish(e_3, e_4)]). input_clause(e_3_is_not_e_5,axiom, [-- equalish(e_3, e_5)]). input_clause(e_4_is_not_e_1,axiom, [-- equalish(e_4, e_1)]). input_clause(e_4_is_not_e_2,axiom, [-- equalish(e_4, e_2)]). input_clause(e_4_is_not_e_3,axiom, [-- equalish(e_4, e_3)]). input_clause(e_4_is_not_e_5,axiom, [-- equalish(e_4, e_5)]). input_clause(e_5_is_not_e_1,axiom, [-- equalish(e_5, e_1)]). input_clause(e_5_is_not_e_2,axiom, [-- equalish(e_5, e_2)]). input_clause(e_5_is_not_e_3,axiom, [-- equalish(e_5, e_3)]). input_clause(e_5_is_not_e_4,axiom, [-- equalish(e_5, e_4)]). input_clause(product_total_function1,axiom, [-- group_element(X), -- group_element(Y), ++ product(X, Y, e_1), ++ product(X, Y, e_2), ++ product(X, Y, e_3), ++ product(X, Y, e_4), ++ product(X, Y, e_5)]). input_clause(product_total_function2,axiom, [-- product(X, Y, W), -- product(X, Y, Z), ++ equalish(W, Z)]). input_clause(product_right_cancellation,axiom, [-- product(X, W, Y), -- product(X, Z, Y), ++ equalish(W, Z)]). input_clause(product_left_cancellation,axiom, [-- product(W, Y, X), -- product(Z, Y, X), ++ equalish(W, Z)]). input_clause(product_idempotence,axiom, [++ product(X, X, X)]). input_clause(qg2_1,conjecture, [-- product(X1, Y1, Z1), -- product(X2, Y2, Z1), -- product(Z2, X1, Y1), -- product(Z2, X2, Y2), ++ equalish(X1, X2)]). input_clause(qg2_2,conjecture, [-- product(X1, Y1, Z1), -- product(X2, Y2, Z1), -- product(Z2, X1, Y1), -- product(Z2, X2, Y2), ++ equalish(Y1, Y2)]). %--------------------------------------------------------------------------