%------------------------------------------------------------------------------ % File : PUZ005+0 : TPTP v7.2.0. Released v3.2.0. % Domain : Puzzles (Sudoku) % Axioms : Sudoku axioms % Version : [Hil06] axioms : Especial. % English : % Refs : [Hil06] Hillenbrand (2006), Email to G. Sutcliffe % Source : [Hil06] % Names : % Status : Satisfiable % Syntax : Number of formulae : 353 ( 1 unit) % Number of atoms : 3925 (3924 equality) % Maximal formula depth : 37 ( 11 average) % Number of connectives : 4580 (1008 ~ ;2592 |; 980 &) % ( 0 <=>; 0 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 2 ( 0 propositional; 2-81 arity) % Number of functors : 10 ( 9 constant; 0-2 arity) % Number of variables : 0 ( 0 singleton; 0 !; 0 ?) % Maximal term depth : 2 ( 2 average) % SPC : % Comments : %------------------------------------------------------------------------------ %----Lower cardinality bound fof(ax1,axiom, ( n1 != n2 & n1 != n3 & n1 != n4 & n1 != n5 & n1 != n6 & n1 != n7 & n1 != n8 & n1 != n9 & n2 != n3 & n2 != n4 & n2 != n5 & n2 != n6 & n2 != n7 & n2 != n8 & n2 != n9 & n3 != n4 & n3 != n5 & n3 != n6 & n3 != n7 & n3 != n8 & n3 != n9 & n4 != n5 & n4 != n6 & n4 != n7 & n4 != n8 & n4 != n9 & n5 != n6 & n5 != n7 & n5 != n8 & n5 != n9 & n6 != n7 & n6 != n8 & n6 != n9 & n7 != n8 & n7 != n9 & n8 != n9 )). %----Row constraints fof(ax2,axiom, ( ssA(n1,n1) = n1 | ssA(n1,n2) = n1 | ssA(n1,n3) = n1 | ssA(n1,n4) = n1 | ssA(n1,n5) = n1 | ssA(n1,n6) = n1 | ssA(n1,n7) = n1 | ssA(n1,n8) = n1 | ssA(n1,n9) = n1 )). fof(ax3,axiom, ( ssA(n1,n1) = n2 | ssA(n1,n2) = n2 | ssA(n1,n3) = n2 | ssA(n1,n4) = n2 | ssA(n1,n5) = n2 | ssA(n1,n6) = n2 | ssA(n1,n7) = n2 | ssA(n1,n8) = n2 | ssA(n1,n9) = n2 )). fof(ax4,axiom, ( ssA(n1,n1) = n3 | ssA(n1,n2) = n3 | ssA(n1,n3) = n3 | ssA(n1,n4) = n3 | ssA(n1,n5) = n3 | ssA(n1,n6) = n3 | ssA(n1,n7) = n3 | ssA(n1,n8) = n3 | ssA(n1,n9) = n3 )). fof(ax5,axiom, ( ssA(n1,n1) = n4 | ssA(n1,n2) = n4 | ssA(n1,n3) = n4 | ssA(n1,n4) = n4 | ssA(n1,n5) = n4 | ssA(n1,n6) = n4 | ssA(n1,n7) = n4 | ssA(n1,n8) = n4 | ssA(n1,n9) = n4 )). fof(ax6,axiom, ( ssA(n1,n1) = n5 | ssA(n1,n2) = n5 | ssA(n1,n3) = n5 | ssA(n1,n4) = n5 | ssA(n1,n5) = n5 | ssA(n1,n6) = n5 | ssA(n1,n7) = n5 | ssA(n1,n8) = n5 | ssA(n1,n9) = n5 )). fof(ax7,axiom, ( ssA(n1,n1) = n6 | ssA(n1,n2) = n6 | ssA(n1,n3) = n6 | ssA(n1,n4) = n6 | ssA(n1,n5) = n6 | ssA(n1,n6) = n6 | ssA(n1,n7) = n6 | ssA(n1,n8) = n6 | ssA(n1,n9) = n6 )). fof(ax8,axiom, ( ssA(n1,n1) = n7 | ssA(n1,n2) = n7 | ssA(n1,n3) = n7 | ssA(n1,n4) = n7 | ssA(n1,n5) = n7 | ssA(n1,n6) = n7 | ssA(n1,n7) = n7 | ssA(n1,n8) = n7 | ssA(n1,n9) = n7 )). fof(ax9,axiom, ( ssA(n1,n1) = n8 | ssA(n1,n2) = n8 | ssA(n1,n3) = n8 | ssA(n1,n4) = n8 | ssA(n1,n5) = n8 | ssA(n1,n6) = n8 | ssA(n1,n7) = n8 | ssA(n1,n8) = n8 | ssA(n1,n9) = n8 )). fof(ax10,axiom, ( ssA(n1,n1) = n9 | ssA(n1,n2) = n9 | ssA(n1,n3) = n9 | ssA(n1,n4) = n9 | ssA(n1,n5) = n9 | ssA(n1,n6) = n9 | ssA(n1,n7) = n9 | ssA(n1,n8) = n9 | ssA(n1,n9) = n9 )). fof(ax11,axiom, ( ssA(n1,n1) != ssA(n1,n2) & ssA(n1,n1) != ssA(n1,n3) & ssA(n1,n1) != ssA(n1,n4) & ssA(n1,n1) != ssA(n1,n5) & ssA(n1,n1) != ssA(n1,n6) & ssA(n1,n1) != ssA(n1,n7) & ssA(n1,n1) != ssA(n1,n8) & ssA(n1,n1) != ssA(n1,n9) & ssA(n1,n2) != ssA(n1,n3) & ssA(n1,n2) != ssA(n1,n4) & ssA(n1,n2) != ssA(n1,n5) & ssA(n1,n2) != ssA(n1,n6) & ssA(n1,n2) != ssA(n1,n7) & ssA(n1,n2) != ssA(n1,n8) & ssA(n1,n2) != ssA(n1,n9) & ssA(n1,n3) != ssA(n1,n4) & ssA(n1,n3) != ssA(n1,n5) & ssA(n1,n3) != ssA(n1,n6) & ssA(n1,n3) != ssA(n1,n7) & ssA(n1,n3) != ssA(n1,n8) & ssA(n1,n3) != ssA(n1,n9) & ssA(n1,n4) != ssA(n1,n5) & ssA(n1,n4) != ssA(n1,n6) & ssA(n1,n4) != ssA(n1,n7) & ssA(n1,n4) != ssA(n1,n8) & ssA(n1,n4) != ssA(n1,n9) & ssA(n1,n5) != ssA(n1,n6) & ssA(n1,n5) != ssA(n1,n7) & ssA(n1,n5) != ssA(n1,n8) & ssA(n1,n5) != ssA(n1,n9) & ssA(n1,n6) != ssA(n1,n7) & ssA(n1,n6) != ssA(n1,n8) & ssA(n1,n6) != ssA(n1,n9) & ssA(n1,n7) != ssA(n1,n8) & ssA(n1,n7) != ssA(n1,n9) & ssA(n1,n8) != ssA(n1,n9) )). fof(ax12,axiom, ( ssA(n2,n1) = n1 | ssA(n2,n2) = n1 | ssA(n2,n3) = n1 | ssA(n2,n4) = n1 | ssA(n2,n5) = n1 | ssA(n2,n6) = n1 | ssA(n2,n7) = n1 | ssA(n2,n8) = n1 | ssA(n2,n9) = n1 )). fof(ax13,axiom, ( ssA(n2,n1) = n2 | ssA(n2,n2) = n2 | ssA(n2,n3) = n2 | ssA(n2,n4) = n2 | ssA(n2,n5) = n2 | ssA(n2,n6) = n2 | ssA(n2,n7) = n2 | ssA(n2,n8) = n2 | ssA(n2,n9) = n2 )). fof(ax14,axiom, ( ssA(n2,n1) = n3 | ssA(n2,n2) = n3 | ssA(n2,n3) = n3 | ssA(n2,n4) = n3 | ssA(n2,n5) = n3 | ssA(n2,n6) = n3 | ssA(n2,n7) = n3 | ssA(n2,n8) = n3 | ssA(n2,n9) = n3 )). fof(ax15,axiom, ( ssA(n2,n1) = n4 | ssA(n2,n2) = n4 | ssA(n2,n3) = n4 | ssA(n2,n4) = n4 | ssA(n2,n5) = n4 | ssA(n2,n6) = n4 | ssA(n2,n7) = n4 | ssA(n2,n8) = n4 | ssA(n2,n9) = n4 )). fof(ax16,axiom, ( ssA(n2,n1) = n5 | ssA(n2,n2) = n5 | ssA(n2,n3) = n5 | ssA(n2,n4) = n5 | ssA(n2,n5) = n5 | ssA(n2,n6) = n5 | ssA(n2,n7) = n5 | ssA(n2,n8) = n5 | ssA(n2,n9) = n5 )). fof(ax17,axiom, ( ssA(n2,n1) = n6 | ssA(n2,n2) = n6 | ssA(n2,n3) = n6 | ssA(n2,n4) = n6 | ssA(n2,n5) = n6 | ssA(n2,n6) = n6 | ssA(n2,n7) = n6 | ssA(n2,n8) = n6 | ssA(n2,n9) = n6 )). fof(ax18,axiom, ( ssA(n2,n1) = n7 | ssA(n2,n2) = n7 | ssA(n2,n3) = n7 | ssA(n2,n4) = n7 | ssA(n2,n5) = n7 | ssA(n2,n6) = n7 | ssA(n2,n7) = n7 | ssA(n2,n8) = n7 | ssA(n2,n9) = n7 )). fof(ax19,axiom, ( ssA(n2,n1) = n8 | ssA(n2,n2) = n8 | ssA(n2,n3) = n8 | ssA(n2,n4) = n8 | ssA(n2,n5) = n8 | ssA(n2,n6) = n8 | ssA(n2,n7) = n8 | ssA(n2,n8) = n8 | ssA(n2,n9) = n8 )). fof(ax20,axiom, ( ssA(n2,n1) = n9 | ssA(n2,n2) = n9 | ssA(n2,n3) = n9 | ssA(n2,n4) = n9 | ssA(n2,n5) = n9 | ssA(n2,n6) = n9 | ssA(n2,n7) = n9 | ssA(n2,n8) = n9 | ssA(n2,n9) = n9 )). fof(ax21,axiom, ( ssA(n2,n1) != ssA(n2,n2) & ssA(n2,n1) != ssA(n2,n3) & ssA(n2,n1) != ssA(n2,n4) & ssA(n2,n1) != ssA(n2,n5) & ssA(n2,n1) != ssA(n2,n6) & ssA(n2,n1) != ssA(n2,n7) & ssA(n2,n1) != ssA(n2,n8) & ssA(n2,n1) != ssA(n2,n9) & ssA(n2,n2) != ssA(n2,n3) & ssA(n2,n2) != ssA(n2,n4) & ssA(n2,n2) != ssA(n2,n5) & ssA(n2,n2) != ssA(n2,n6) & ssA(n2,n2) != ssA(n2,n7) & ssA(n2,n2) != ssA(n2,n8) & ssA(n2,n2) != ssA(n2,n9) & ssA(n2,n3) != ssA(n2,n4) & ssA(n2,n3) != ssA(n2,n5) & ssA(n2,n3) != ssA(n2,n6) & ssA(n2,n3) != ssA(n2,n7) & ssA(n2,n3) != ssA(n2,n8) & ssA(n2,n3) != ssA(n2,n9) & ssA(n2,n4) != ssA(n2,n5) & ssA(n2,n4) != ssA(n2,n6) & ssA(n2,n4) != ssA(n2,n7) & ssA(n2,n4) != ssA(n2,n8) & ssA(n2,n4) != ssA(n2,n9) & ssA(n2,n5) != ssA(n2,n6) & ssA(n2,n5) != ssA(n2,n7) & ssA(n2,n5) != ssA(n2,n8) & ssA(n2,n5) != ssA(n2,n9) & ssA(n2,n6) != ssA(n2,n7) & ssA(n2,n6) != ssA(n2,n8) & ssA(n2,n6) != ssA(n2,n9) & ssA(n2,n7) != ssA(n2,n8) & ssA(n2,n7) != ssA(n2,n9) & ssA(n2,n8) != ssA(n2,n9) )). fof(ax22,axiom, ( ssA(n3,n1) = n1 | ssA(n3,n2) = n1 | ssA(n3,n3) = n1 | ssA(n3,n4) = n1 | ssA(n3,n5) = n1 | ssA(n3,n6) = n1 | ssA(n3,n7) = n1 | ssA(n3,n8) = n1 | ssA(n3,n9) = n1 )). fof(ax23,axiom, ( ssA(n3,n1) = n2 | ssA(n3,n2) = n2 | ssA(n3,n3) = n2 | ssA(n3,n4) = n2 | ssA(n3,n5) = n2 | ssA(n3,n6) = n2 | ssA(n3,n7) = n2 | ssA(n3,n8) = n2 | ssA(n3,n9) = n2 )). fof(ax24,axiom, ( ssA(n3,n1) = n3 | ssA(n3,n2) = n3 | ssA(n3,n3) = n3 | ssA(n3,n4) = n3 | ssA(n3,n5) = n3 | ssA(n3,n6) = n3 | ssA(n3,n7) = n3 | ssA(n3,n8) = n3 | ssA(n3,n9) = n3 )). fof(ax25,axiom, ( ssA(n3,n1) = n4 | ssA(n3,n2) = n4 | ssA(n3,n3) = n4 | ssA(n3,n4) = n4 | ssA(n3,n5) = n4 | ssA(n3,n6) = n4 | ssA(n3,n7) = n4 | ssA(n3,n8) = n4 | ssA(n3,n9) = n4 )). fof(ax26,axiom, ( ssA(n3,n1) = n5 | ssA(n3,n2) = n5 | ssA(n3,n3) = n5 | ssA(n3,n4) = n5 | ssA(n3,n5) = n5 | ssA(n3,n6) = n5 | ssA(n3,n7) = n5 | ssA(n3,n8) = n5 | ssA(n3,n9) = n5 )). fof(ax27,axiom, ( ssA(n3,n1) = n6 | ssA(n3,n2) = n6 | ssA(n3,n3) = n6 | ssA(n3,n4) = n6 | ssA(n3,n5) = n6 | ssA(n3,n6) = n6 | ssA(n3,n7) = n6 | ssA(n3,n8) = n6 | ssA(n3,n9) = n6 )). fof(ax28,axiom, ( ssA(n3,n1) = n7 | ssA(n3,n2) = n7 | ssA(n3,n3) = n7 | ssA(n3,n4) = n7 | ssA(n3,n5) = n7 | ssA(n3,n6) = n7 | ssA(n3,n7) = n7 | ssA(n3,n8) = n7 | ssA(n3,n9) = n7 )). fof(ax29,axiom, ( ssA(n3,n1) = n8 | ssA(n3,n2) = n8 | ssA(n3,n3) = n8 | ssA(n3,n4) = n8 | ssA(n3,n5) = n8 | ssA(n3,n6) = n8 | ssA(n3,n7) = n8 | ssA(n3,n8) = n8 | ssA(n3,n9) = n8 )). fof(ax30,axiom, ( ssA(n3,n1) = n9 | ssA(n3,n2) = n9 | ssA(n3,n3) = n9 | ssA(n3,n4) = n9 | ssA(n3,n5) = n9 | ssA(n3,n6) = n9 | ssA(n3,n7) = n9 | ssA(n3,n8) = n9 | ssA(n3,n9) = n9 )). fof(ax31,axiom, ( ssA(n3,n1) != ssA(n3,n2) & ssA(n3,n1) != ssA(n3,n3) & ssA(n3,n1) != ssA(n3,n4) & ssA(n3,n1) != ssA(n3,n5) & ssA(n3,n1) != ssA(n3,n6) & ssA(n3,n1) != ssA(n3,n7) & ssA(n3,n1) != ssA(n3,n8) & ssA(n3,n1) != ssA(n3,n9) & ssA(n3,n2) != ssA(n3,n3) & ssA(n3,n2) != ssA(n3,n4) & ssA(n3,n2) != ssA(n3,n5) & ssA(n3,n2) != ssA(n3,n6) & ssA(n3,n2) != ssA(n3,n7) & ssA(n3,n2) != ssA(n3,n8) & ssA(n3,n2) != ssA(n3,n9) & ssA(n3,n3) != ssA(n3,n4) & ssA(n3,n3) != ssA(n3,n5) & ssA(n3,n3) != ssA(n3,n6) & ssA(n3,n3) != ssA(n3,n7) & ssA(n3,n3) != ssA(n3,n8) & ssA(n3,n3) != ssA(n3,n9) & ssA(n3,n4) != ssA(n3,n5) & ssA(n3,n4) != ssA(n3,n6) & ssA(n3,n4) != ssA(n3,n7) & ssA(n3,n4) != ssA(n3,n8) & ssA(n3,n4) != ssA(n3,n9) & ssA(n3,n5) != ssA(n3,n6) & ssA(n3,n5) != ssA(n3,n7) & ssA(n3,n5) != ssA(n3,n8) & ssA(n3,n5) != ssA(n3,n9) & ssA(n3,n6) != ssA(n3,n7) & ssA(n3,n6) != ssA(n3,n8) & ssA(n3,n6) != ssA(n3,n9) & ssA(n3,n7) != ssA(n3,n8) & ssA(n3,n7) != ssA(n3,n9) & ssA(n3,n8) != ssA(n3,n9) )). fof(ax32,axiom, ( ssA(n4,n1) = n1 | ssA(n4,n2) = n1 | ssA(n4,n3) = n1 | ssA(n4,n4) = n1 | ssA(n4,n5) = n1 | ssA(n4,n6) = n1 | ssA(n4,n7) = n1 | ssA(n4,n8) = n1 | ssA(n4,n9) = n1 )). fof(ax33,axiom, ( ssA(n4,n1) = n2 | ssA(n4,n2) = n2 | ssA(n4,n3) = n2 | ssA(n4,n4) = n2 | ssA(n4,n5) = n2 | ssA(n4,n6) = n2 | ssA(n4,n7) = n2 | ssA(n4,n8) = n2 | ssA(n4,n9) = n2 )). fof(ax34,axiom, ( ssA(n4,n1) = n3 | ssA(n4,n2) = n3 | ssA(n4,n3) = n3 | ssA(n4,n4) = n3 | ssA(n4,n5) = n3 | ssA(n4,n6) = n3 | ssA(n4,n7) = n3 | ssA(n4,n8) = n3 | ssA(n4,n9) = n3 )). fof(ax35,axiom, ( ssA(n4,n1) = n4 | ssA(n4,n2) = n4 | ssA(n4,n3) = n4 | ssA(n4,n4) = n4 | ssA(n4,n5) = n4 | ssA(n4,n6) = n4 | ssA(n4,n7) = n4 | ssA(n4,n8) = n4 | ssA(n4,n9) = n4 )). fof(ax36,axiom, ( ssA(n4,n1) = n5 | ssA(n4,n2) = n5 | ssA(n4,n3) = n5 | ssA(n4,n4) = n5 | ssA(n4,n5) = n5 | ssA(n4,n6) = n5 | ssA(n4,n7) = n5 | ssA(n4,n8) = n5 | ssA(n4,n9) = n5 )). fof(ax37,axiom, ( ssA(n4,n1) = n6 | ssA(n4,n2) = n6 | ssA(n4,n3) = n6 | ssA(n4,n4) = n6 | ssA(n4,n5) = n6 | ssA(n4,n6) = n6 | ssA(n4,n7) = n6 | ssA(n4,n8) = n6 | ssA(n4,n9) = n6 )). fof(ax38,axiom, ( ssA(n4,n1) = n7 | ssA(n4,n2) = n7 | ssA(n4,n3) = n7 | ssA(n4,n4) = n7 | ssA(n4,n5) = n7 | ssA(n4,n6) = n7 | ssA(n4,n7) = n7 | ssA(n4,n8) = n7 | ssA(n4,n9) = n7 )). fof(ax39,axiom, ( ssA(n4,n1) = n8 | ssA(n4,n2) = n8 | ssA(n4,n3) = n8 | ssA(n4,n4) = n8 | ssA(n4,n5) = n8 | ssA(n4,n6) = n8 | ssA(n4,n7) = n8 | ssA(n4,n8) = n8 | ssA(n4,n9) = n8 )). fof(ax40,axiom, ( ssA(n4,n1) = n9 | ssA(n4,n2) = n9 | ssA(n4,n3) = n9 | ssA(n4,n4) = n9 | ssA(n4,n5) = n9 | ssA(n4,n6) = n9 | ssA(n4,n7) = n9 | ssA(n4,n8) = n9 | ssA(n4,n9) = n9 )). fof(ax41,axiom, ( ssA(n4,n1) != ssA(n4,n2) & ssA(n4,n1) != ssA(n4,n3) & ssA(n4,n1) != ssA(n4,n4) & ssA(n4,n1) != ssA(n4,n5) & ssA(n4,n1) != ssA(n4,n6) & ssA(n4,n1) != ssA(n4,n7) & ssA(n4,n1) != ssA(n4,n8) & ssA(n4,n1) != ssA(n4,n9) & ssA(n4,n2) != ssA(n4,n3) & ssA(n4,n2) != ssA(n4,n4) & ssA(n4,n2) != ssA(n4,n5) & ssA(n4,n2) != ssA(n4,n6) & ssA(n4,n2) != ssA(n4,n7) & ssA(n4,n2) != ssA(n4,n8) & ssA(n4,n2) != ssA(n4,n9) & ssA(n4,n3) != ssA(n4,n4) & ssA(n4,n3) != ssA(n4,n5) & ssA(n4,n3) != ssA(n4,n6) & ssA(n4,n3) != ssA(n4,n7) & ssA(n4,n3) != ssA(n4,n8) & ssA(n4,n3) != ssA(n4,n9) & ssA(n4,n4) != ssA(n4,n5) & ssA(n4,n4) != ssA(n4,n6) & ssA(n4,n4) != ssA(n4,n7) & ssA(n4,n4) != ssA(n4,n8) & ssA(n4,n4) != ssA(n4,n9) & ssA(n4,n5) != ssA(n4,n6) & ssA(n4,n5) != ssA(n4,n7) & ssA(n4,n5) != ssA(n4,n8) & ssA(n4,n5) != ssA(n4,n9) & ssA(n4,n6) != ssA(n4,n7) & ssA(n4,n6) != ssA(n4,n8) & ssA(n4,n6) != ssA(n4,n9) & ssA(n4,n7) != ssA(n4,n8) & ssA(n4,n7) != ssA(n4,n9) & ssA(n4,n8) != ssA(n4,n9) )). fof(ax42,axiom, ( ssA(n5,n1) = n1 | ssA(n5,n2) = n1 | ssA(n5,n3) = n1 | ssA(n5,n4) = n1 | ssA(n5,n5) = n1 | ssA(n5,n6) = n1 | ssA(n5,n7) = n1 | ssA(n5,n8) = n1 | ssA(n5,n9) = n1 )). fof(ax43,axiom, ( ssA(n5,n1) = n2 | ssA(n5,n2) = n2 | ssA(n5,n3) = n2 | ssA(n5,n4) = n2 | ssA(n5,n5) = n2 | ssA(n5,n6) = n2 | ssA(n5,n7) = n2 | ssA(n5,n8) = n2 | ssA(n5,n9) = n2 )). fof(ax44,axiom, ( ssA(n5,n1) = n3 | ssA(n5,n2) = n3 | ssA(n5,n3) = n3 | ssA(n5,n4) = n3 | ssA(n5,n5) = n3 | ssA(n5,n6) = n3 | ssA(n5,n7) = n3 | ssA(n5,n8) = n3 | ssA(n5,n9) = n3 )). fof(ax45,axiom, ( ssA(n5,n1) = n4 | ssA(n5,n2) = n4 | ssA(n5,n3) = n4 | ssA(n5,n4) = n4 | ssA(n5,n5) = n4 | ssA(n5,n6) = n4 | ssA(n5,n7) = n4 | ssA(n5,n8) = n4 | ssA(n5,n9) = n4 )). fof(ax46,axiom, ( ssA(n5,n1) = n5 | ssA(n5,n2) = n5 | ssA(n5,n3) = n5 | ssA(n5,n4) = n5 | ssA(n5,n5) = n5 | ssA(n5,n6) = n5 | ssA(n5,n7) = n5 | ssA(n5,n8) = n5 | ssA(n5,n9) = n5 )). fof(ax47,axiom, ( ssA(n5,n1) = n6 | ssA(n5,n2) = n6 | ssA(n5,n3) = n6 | ssA(n5,n4) = n6 | ssA(n5,n5) = n6 | ssA(n5,n6) = n6 | ssA(n5,n7) = n6 | ssA(n5,n8) = n6 | ssA(n5,n9) = n6 )). fof(ax48,axiom, ( ssA(n5,n1) = n7 | ssA(n5,n2) = n7 | ssA(n5,n3) = n7 | ssA(n5,n4) = n7 | ssA(n5,n5) = n7 | ssA(n5,n6) = n7 | ssA(n5,n7) = n7 | ssA(n5,n8) = n7 | ssA(n5,n9) = n7 )). fof(ax49,axiom, ( ssA(n5,n1) = n8 | ssA(n5,n2) = n8 | ssA(n5,n3) = n8 | ssA(n5,n4) = n8 | ssA(n5,n5) = n8 | ssA(n5,n6) = n8 | ssA(n5,n7) = n8 | ssA(n5,n8) = n8 | ssA(n5,n9) = n8 )). fof(ax50,axiom, ( ssA(n5,n1) = n9 | ssA(n5,n2) = n9 | ssA(n5,n3) = n9 | ssA(n5,n4) = n9 | ssA(n5,n5) = n9 | ssA(n5,n6) = n9 | ssA(n5,n7) = n9 | ssA(n5,n8) = n9 | ssA(n5,n9) = n9 )). fof(ax51,axiom, ( ssA(n5,n1) != ssA(n5,n2) & ssA(n5,n1) != ssA(n5,n3) & ssA(n5,n1) != ssA(n5,n4) & ssA(n5,n1) != ssA(n5,n5) & ssA(n5,n1) != ssA(n5,n6) & ssA(n5,n1) != ssA(n5,n7) & ssA(n5,n1) != ssA(n5,n8) & ssA(n5,n1) != ssA(n5,n9) & ssA(n5,n2) != ssA(n5,n3) & ssA(n5,n2) != ssA(n5,n4) & ssA(n5,n2) != ssA(n5,n5) & ssA(n5,n2) != ssA(n5,n6) & ssA(n5,n2) != ssA(n5,n7) & ssA(n5,n2) != ssA(n5,n8) & ssA(n5,n2) != ssA(n5,n9) & ssA(n5,n3) != ssA(n5,n4) & ssA(n5,n3) != ssA(n5,n5) & ssA(n5,n3) != ssA(n5,n6) & ssA(n5,n3) != ssA(n5,n7) & ssA(n5,n3) != ssA(n5,n8) & ssA(n5,n3) != ssA(n5,n9) & ssA(n5,n4) != ssA(n5,n5) & ssA(n5,n4) != ssA(n5,n6) & ssA(n5,n4) != ssA(n5,n7) & ssA(n5,n4) != ssA(n5,n8) & ssA(n5,n4) != ssA(n5,n9) & ssA(n5,n5) != ssA(n5,n6) & ssA(n5,n5) != ssA(n5,n7) & ssA(n5,n5) != ssA(n5,n8) & ssA(n5,n5) != ssA(n5,n9) & ssA(n5,n6) != ssA(n5,n7) & ssA(n5,n6) != ssA(n5,n8) & ssA(n5,n6) != ssA(n5,n9) & ssA(n5,n7) != ssA(n5,n8) & ssA(n5,n7) != ssA(n5,n9) & ssA(n5,n8) != ssA(n5,n9) )). fof(ax52,axiom, ( ssA(n6,n1) = n1 | ssA(n6,n2) = n1 | ssA(n6,n3) = n1 | ssA(n6,n4) = n1 | ssA(n6,n5) = n1 | ssA(n6,n6) = n1 | ssA(n6,n7) = n1 | ssA(n6,n8) = n1 | ssA(n6,n9) = n1 )). fof(ax53,axiom, ( ssA(n6,n1) = n2 | ssA(n6,n2) = n2 | ssA(n6,n3) = n2 | ssA(n6,n4) = n2 | ssA(n6,n5) = n2 | ssA(n6,n6) = n2 | ssA(n6,n7) = n2 | ssA(n6,n8) = n2 | ssA(n6,n9) = n2 )). fof(ax54,axiom, ( ssA(n6,n1) = n3 | ssA(n6,n2) = n3 | ssA(n6,n3) = n3 | ssA(n6,n4) = n3 | ssA(n6,n5) = n3 | ssA(n6,n6) = n3 | ssA(n6,n7) = n3 | ssA(n6,n8) = n3 | ssA(n6,n9) = n3 )). fof(ax55,axiom, ( ssA(n6,n1) = n4 | ssA(n6,n2) = n4 | ssA(n6,n3) = n4 | ssA(n6,n4) = n4 | ssA(n6,n5) = n4 | ssA(n6,n6) = n4 | ssA(n6,n7) = n4 | ssA(n6,n8) = n4 | ssA(n6,n9) = n4 )). fof(ax56,axiom, ( ssA(n6,n1) = n5 | ssA(n6,n2) = n5 | ssA(n6,n3) = n5 | ssA(n6,n4) = n5 | ssA(n6,n5) = n5 | ssA(n6,n6) = n5 | ssA(n6,n7) = n5 | ssA(n6,n8) = n5 | ssA(n6,n9) = n5 )). fof(ax57,axiom, ( ssA(n6,n1) = n6 | ssA(n6,n2) = n6 | ssA(n6,n3) = n6 | ssA(n6,n4) = n6 | ssA(n6,n5) = n6 | ssA(n6,n6) = n6 | ssA(n6,n7) = n6 | ssA(n6,n8) = n6 | ssA(n6,n9) = n6 )). fof(ax58,axiom, ( ssA(n6,n1) = n7 | ssA(n6,n2) = n7 | ssA(n6,n3) = n7 | ssA(n6,n4) = n7 | ssA(n6,n5) = n7 | ssA(n6,n6) = n7 | ssA(n6,n7) = n7 | ssA(n6,n8) = n7 | ssA(n6,n9) = n7 )). fof(ax59,axiom, ( ssA(n6,n1) = n8 | ssA(n6,n2) = n8 | ssA(n6,n3) = n8 | ssA(n6,n4) = n8 | ssA(n6,n5) = n8 | ssA(n6,n6) = n8 | ssA(n6,n7) = n8 | ssA(n6,n8) = n8 | ssA(n6,n9) = n8 )). fof(ax60,axiom, ( ssA(n6,n1) = n9 | ssA(n6,n2) = n9 | ssA(n6,n3) = n9 | ssA(n6,n4) = n9 | ssA(n6,n5) = n9 | ssA(n6,n6) = n9 | ssA(n6,n7) = n9 | ssA(n6,n8) = n9 | ssA(n6,n9) = n9 )). fof(ax61,axiom, ( ssA(n6,n1) != ssA(n6,n2) & ssA(n6,n1) != ssA(n6,n3) & ssA(n6,n1) != ssA(n6,n4) & ssA(n6,n1) != ssA(n6,n5) & ssA(n6,n1) != ssA(n6,n6) & ssA(n6,n1) != ssA(n6,n7) & ssA(n6,n1) != ssA(n6,n8) & ssA(n6,n1) != ssA(n6,n9) & ssA(n6,n2) != ssA(n6,n3) & ssA(n6,n2) != ssA(n6,n4) & ssA(n6,n2) != ssA(n6,n5) & ssA(n6,n2) != ssA(n6,n6) & ssA(n6,n2) != ssA(n6,n7) & ssA(n6,n2) != ssA(n6,n8) & ssA(n6,n2) != ssA(n6,n9) & ssA(n6,n3) != ssA(n6,n4) & ssA(n6,n3) != ssA(n6,n5) & ssA(n6,n3) != ssA(n6,n6) & ssA(n6,n3) != ssA(n6,n7) & ssA(n6,n3) != ssA(n6,n8) & ssA(n6,n3) != ssA(n6,n9) & ssA(n6,n4) != ssA(n6,n5) & ssA(n6,n4) != ssA(n6,n6) & ssA(n6,n4) != ssA(n6,n7) & ssA(n6,n4) != ssA(n6,n8) & ssA(n6,n4) != ssA(n6,n9) & ssA(n6,n5) != ssA(n6,n6) & ssA(n6,n5) != ssA(n6,n7) & ssA(n6,n5) != ssA(n6,n8) & ssA(n6,n5) != ssA(n6,n9) & ssA(n6,n6) != ssA(n6,n7) & ssA(n6,n6) != ssA(n6,n8) & ssA(n6,n6) != ssA(n6,n9) & ssA(n6,n7) != ssA(n6,n8) & ssA(n6,n7) != ssA(n6,n9) & ssA(n6,n8) != ssA(n6,n9) )). fof(ax62,axiom, ( ssA(n7,n1) = n1 | ssA(n7,n2) = n1 | ssA(n7,n3) = n1 | ssA(n7,n4) = n1 | ssA(n7,n5) = n1 | ssA(n7,n6) = n1 | ssA(n7,n7) = n1 | ssA(n7,n8) = n1 | ssA(n7,n9) = n1 )). fof(ax63,axiom, ( ssA(n7,n1) = n2 | ssA(n7,n2) = n2 | ssA(n7,n3) = n2 | ssA(n7,n4) = n2 | ssA(n7,n5) = n2 | ssA(n7,n6) = n2 | ssA(n7,n7) = n2 | ssA(n7,n8) = n2 | ssA(n7,n9) = n2 )). fof(ax64,axiom, ( ssA(n7,n1) = n3 | ssA(n7,n2) = n3 | ssA(n7,n3) = n3 | ssA(n7,n4) = n3 | ssA(n7,n5) = n3 | ssA(n7,n6) = n3 | ssA(n7,n7) = n3 | ssA(n7,n8) = n3 | ssA(n7,n9) = n3 )). fof(ax65,axiom, ( ssA(n7,n1) = n4 | ssA(n7,n2) = n4 | ssA(n7,n3) = n4 | ssA(n7,n4) = n4 | ssA(n7,n5) = n4 | ssA(n7,n6) = n4 | ssA(n7,n7) = n4 | ssA(n7,n8) = n4 | ssA(n7,n9) = n4 )). fof(ax66,axiom, ( ssA(n7,n1) = n5 | ssA(n7,n2) = n5 | ssA(n7,n3) = n5 | ssA(n7,n4) = n5 | ssA(n7,n5) = n5 | ssA(n7,n6) = n5 | ssA(n7,n7) = n5 | ssA(n7,n8) = n5 | ssA(n7,n9) = n5 )). fof(ax67,axiom, ( ssA(n7,n1) = n6 | ssA(n7,n2) = n6 | ssA(n7,n3) = n6 | ssA(n7,n4) = n6 | ssA(n7,n5) = n6 | ssA(n7,n6) = n6 | ssA(n7,n7) = n6 | ssA(n7,n8) = n6 | ssA(n7,n9) = n6 )). fof(ax68,axiom, ( ssA(n7,n1) = n7 | ssA(n7,n2) = n7 | ssA(n7,n3) = n7 | ssA(n7,n4) = n7 | ssA(n7,n5) = n7 | ssA(n7,n6) = n7 | ssA(n7,n7) = n7 | ssA(n7,n8) = n7 | ssA(n7,n9) = n7 )). fof(ax69,axiom, ( ssA(n7,n1) = n8 | ssA(n7,n2) = n8 | ssA(n7,n3) = n8 | ssA(n7,n4) = n8 | ssA(n7,n5) = n8 | ssA(n7,n6) = n8 | ssA(n7,n7) = n8 | ssA(n7,n8) = n8 | ssA(n7,n9) = n8 )). fof(ax70,axiom, ( ssA(n7,n1) = n9 | ssA(n7,n2) = n9 | ssA(n7,n3) = n9 | ssA(n7,n4) = n9 | ssA(n7,n5) = n9 | ssA(n7,n6) = n9 | ssA(n7,n7) = n9 | ssA(n7,n8) = n9 | ssA(n7,n9) = n9 )). fof(ax71,axiom, ( ssA(n7,n1) != ssA(n7,n2) & ssA(n7,n1) != ssA(n7,n3) & ssA(n7,n1) != ssA(n7,n4) & ssA(n7,n1) != ssA(n7,n5) & ssA(n7,n1) != ssA(n7,n6) & ssA(n7,n1) != ssA(n7,n7) & ssA(n7,n1) != ssA(n7,n8) & ssA(n7,n1) != ssA(n7,n9) & ssA(n7,n2) != ssA(n7,n3) & ssA(n7,n2) != ssA(n7,n4) & ssA(n7,n2) != ssA(n7,n5) & ssA(n7,n2) != ssA(n7,n6) & ssA(n7,n2) != ssA(n7,n7) & ssA(n7,n2) != ssA(n7,n8) & ssA(n7,n2) != ssA(n7,n9) & ssA(n7,n3) != ssA(n7,n4) & ssA(n7,n3) != ssA(n7,n5) & ssA(n7,n3) != ssA(n7,n6) & ssA(n7,n3) != ssA(n7,n7) & ssA(n7,n3) != ssA(n7,n8) & ssA(n7,n3) != ssA(n7,n9) & ssA(n7,n4) != ssA(n7,n5) & ssA(n7,n4) != ssA(n7,n6) & ssA(n7,n4) != ssA(n7,n7) & ssA(n7,n4) != ssA(n7,n8) & ssA(n7,n4) != ssA(n7,n9) & ssA(n7,n5) != ssA(n7,n6) & ssA(n7,n5) != ssA(n7,n7) & ssA(n7,n5) != ssA(n7,n8) & ssA(n7,n5) != ssA(n7,n9) & ssA(n7,n6) != ssA(n7,n7) & ssA(n7,n6) != ssA(n7,n8) & ssA(n7,n6) != ssA(n7,n9) & ssA(n7,n7) != ssA(n7,n8) & ssA(n7,n7) != ssA(n7,n9) & ssA(n7,n8) != ssA(n7,n9) )). fof(ax72,axiom, ( ssA(n8,n1) = n1 | ssA(n8,n2) = n1 | ssA(n8,n3) = n1 | ssA(n8,n4) = n1 | ssA(n8,n5) = n1 | ssA(n8,n6) = n1 | ssA(n8,n7) = n1 | ssA(n8,n8) = n1 | ssA(n8,n9) = n1 )). fof(ax73,axiom, ( ssA(n8,n1) = n2 | ssA(n8,n2) = n2 | ssA(n8,n3) = n2 | ssA(n8,n4) = n2 | ssA(n8,n5) = n2 | ssA(n8,n6) = n2 | ssA(n8,n7) = n2 | ssA(n8,n8) = n2 | ssA(n8,n9) = n2 )). fof(ax74,axiom, ( ssA(n8,n1) = n3 | ssA(n8,n2) = n3 | ssA(n8,n3) = n3 | ssA(n8,n4) = n3 | ssA(n8,n5) = n3 | ssA(n8,n6) = n3 | ssA(n8,n7) = n3 | ssA(n8,n8) = n3 | ssA(n8,n9) = n3 )). fof(ax75,axiom, ( ssA(n8,n1) = n4 | ssA(n8,n2) = n4 | ssA(n8,n3) = n4 | ssA(n8,n4) = n4 | ssA(n8,n5) = n4 | ssA(n8,n6) = n4 | ssA(n8,n7) = n4 | ssA(n8,n8) = n4 | ssA(n8,n9) = n4 )). fof(ax76,axiom, ( ssA(n8,n1) = n5 | ssA(n8,n2) = n5 | ssA(n8,n3) = n5 | ssA(n8,n4) = n5 | ssA(n8,n5) = n5 | ssA(n8,n6) = n5 | ssA(n8,n7) = n5 | ssA(n8,n8) = n5 | ssA(n8,n9) = n5 )). fof(ax77,axiom, ( ssA(n8,n1) = n6 | ssA(n8,n2) = n6 | ssA(n8,n3) = n6 | ssA(n8,n4) = n6 | ssA(n8,n5) = n6 | ssA(n8,n6) = n6 | ssA(n8,n7) = n6 | ssA(n8,n8) = n6 | ssA(n8,n9) = n6 )). fof(ax78,axiom, ( ssA(n8,n1) = n7 | ssA(n8,n2) = n7 | ssA(n8,n3) = n7 | ssA(n8,n4) = n7 | ssA(n8,n5) = n7 | ssA(n8,n6) = n7 | ssA(n8,n7) = n7 | ssA(n8,n8) = n7 | ssA(n8,n9) = n7 )). fof(ax79,axiom, ( ssA(n8,n1) = n8 | ssA(n8,n2) = n8 | ssA(n8,n3) = n8 | ssA(n8,n4) = n8 | ssA(n8,n5) = n8 | ssA(n8,n6) = n8 | ssA(n8,n7) = n8 | ssA(n8,n8) = n8 | ssA(n8,n9) = n8 )). fof(ax80,axiom, ( ssA(n8,n1) = n9 | ssA(n8,n2) = n9 | ssA(n8,n3) = n9 | ssA(n8,n4) = n9 | ssA(n8,n5) = n9 | ssA(n8,n6) = n9 | ssA(n8,n7) = n9 | ssA(n8,n8) = n9 | ssA(n8,n9) = n9 )). fof(ax81,axiom, ( ssA(n8,n1) != ssA(n8,n2) & ssA(n8,n1) != ssA(n8,n3) & ssA(n8,n1) != ssA(n8,n4) & ssA(n8,n1) != ssA(n8,n5) & ssA(n8,n1) != ssA(n8,n6) & ssA(n8,n1) != ssA(n8,n7) & ssA(n8,n1) != ssA(n8,n8) & ssA(n8,n1) != ssA(n8,n9) & ssA(n8,n2) != ssA(n8,n3) & ssA(n8,n2) != ssA(n8,n4) & ssA(n8,n2) != ssA(n8,n5) & ssA(n8,n2) != ssA(n8,n6) & ssA(n8,n2) != ssA(n8,n7) & ssA(n8,n2) != ssA(n8,n8) & ssA(n8,n2) != ssA(n8,n9) & ssA(n8,n3) != ssA(n8,n4) & ssA(n8,n3) != ssA(n8,n5) & ssA(n8,n3) != ssA(n8,n6) & ssA(n8,n3) != ssA(n8,n7) & ssA(n8,n3) != ssA(n8,n8) & ssA(n8,n3) != ssA(n8,n9) & ssA(n8,n4) != ssA(n8,n5) & ssA(n8,n4) != ssA(n8,n6) & ssA(n8,n4) != ssA(n8,n7) & ssA(n8,n4) != ssA(n8,n8) & ssA(n8,n4) != ssA(n8,n9) & ssA(n8,n5) != ssA(n8,n6) & ssA(n8,n5) != ssA(n8,n7) & ssA(n8,n5) != ssA(n8,n8) & ssA(n8,n5) != ssA(n8,n9) & ssA(n8,n6) != ssA(n8,n7) & ssA(n8,n6) != ssA(n8,n8) & ssA(n8,n6) != ssA(n8,n9) & ssA(n8,n7) != ssA(n8,n8) & ssA(n8,n7) != ssA(n8,n9) & ssA(n8,n8) != ssA(n8,n9) )). fof(ax82,axiom, ( ssA(n9,n1) = n1 | ssA(n9,n2) = n1 | ssA(n9,n3) = n1 | ssA(n9,n4) = n1 | ssA(n9,n5) = n1 | ssA(n9,n6) = n1 | ssA(n9,n7) = n1 | ssA(n9,n8) = n1 | ssA(n9,n9) = n1 )). fof(ax83,axiom, ( ssA(n9,n1) = n2 | ssA(n9,n2) = n2 | ssA(n9,n3) = n2 | ssA(n9,n4) = n2 | ssA(n9,n5) = n2 | ssA(n9,n6) = n2 | ssA(n9,n7) = n2 | ssA(n9,n8) = n2 | ssA(n9,n9) = n2 )). fof(ax84,axiom, ( ssA(n9,n1) = n3 | ssA(n9,n2) = n3 | ssA(n9,n3) = n3 | ssA(n9,n4) = n3 | ssA(n9,n5) = n3 | ssA(n9,n6) = n3 | ssA(n9,n7) = n3 | ssA(n9,n8) = n3 | ssA(n9,n9) = n3 )). fof(ax85,axiom, ( ssA(n9,n1) = n4 | ssA(n9,n2) = n4 | ssA(n9,n3) = n4 | ssA(n9,n4) = n4 | ssA(n9,n5) = n4 | ssA(n9,n6) = n4 | ssA(n9,n7) = n4 | ssA(n9,n8) = n4 | ssA(n9,n9) = n4 )). fof(ax86,axiom, ( ssA(n9,n1) = n5 | ssA(n9,n2) = n5 | ssA(n9,n3) = n5 | ssA(n9,n4) = n5 | ssA(n9,n5) = n5 | ssA(n9,n6) = n5 | ssA(n9,n7) = n5 | ssA(n9,n8) = n5 | ssA(n9,n9) = n5 )). fof(ax87,axiom, ( ssA(n9,n1) = n6 | ssA(n9,n2) = n6 | ssA(n9,n3) = n6 | ssA(n9,n4) = n6 | ssA(n9,n5) = n6 | ssA(n9,n6) = n6 | ssA(n9,n7) = n6 | ssA(n9,n8) = n6 | ssA(n9,n9) = n6 )). fof(ax88,axiom, ( ssA(n9,n1) = n7 | ssA(n9,n2) = n7 | ssA(n9,n3) = n7 | ssA(n9,n4) = n7 | ssA(n9,n5) = n7 | ssA(n9,n6) = n7 | ssA(n9,n7) = n7 | ssA(n9,n8) = n7 | ssA(n9,n9) = n7 )). fof(ax89,axiom, ( ssA(n9,n1) = n8 | ssA(n9,n2) = n8 | ssA(n9,n3) = n8 | ssA(n9,n4) = n8 | ssA(n9,n5) = n8 | ssA(n9,n6) = n8 | ssA(n9,n7) = n8 | ssA(n9,n8) = n8 | ssA(n9,n9) = n8 )). fof(ax90,axiom, ( ssA(n9,n1) = n9 | ssA(n9,n2) = n9 | ssA(n9,n3) = n9 | ssA(n9,n4) = n9 | ssA(n9,n5) = n9 | ssA(n9,n6) = n9 | ssA(n9,n7) = n9 | ssA(n9,n8) = n9 | ssA(n9,n9) = n9 )). fof(ax91,axiom, ( ssA(n9,n1) != ssA(n9,n2) & ssA(n9,n1) != ssA(n9,n3) & ssA(n9,n1) != ssA(n9,n4) & ssA(n9,n1) != ssA(n9,n5) & ssA(n9,n1) != ssA(n9,n6) & ssA(n9,n1) != ssA(n9,n7) & ssA(n9,n1) != ssA(n9,n8) & ssA(n9,n1) != ssA(n9,n9) & ssA(n9,n2) != ssA(n9,n3) & ssA(n9,n2) != ssA(n9,n4) & ssA(n9,n2) != ssA(n9,n5) & ssA(n9,n2) != ssA(n9,n6) & ssA(n9,n2) != ssA(n9,n7) & ssA(n9,n2) != ssA(n9,n8) & ssA(n9,n2) != ssA(n9,n9) & ssA(n9,n3) != ssA(n9,n4) & ssA(n9,n3) != ssA(n9,n5) & ssA(n9,n3) != ssA(n9,n6) & ssA(n9,n3) != ssA(n9,n7) & ssA(n9,n3) != ssA(n9,n8) & ssA(n9,n3) != ssA(n9,n9) & ssA(n9,n4) != ssA(n9,n5) & ssA(n9,n4) != ssA(n9,n6) & ssA(n9,n4) != ssA(n9,n7) & ssA(n9,n4) != ssA(n9,n8) & ssA(n9,n4) != ssA(n9,n9) & ssA(n9,n5) != ssA(n9,n6) & ssA(n9,n5) != ssA(n9,n7) & ssA(n9,n5) != ssA(n9,n8) & ssA(n9,n5) != ssA(n9,n9) & ssA(n9,n6) != ssA(n9,n7) & ssA(n9,n6) != ssA(n9,n8) & ssA(n9,n6) != ssA(n9,n9) & ssA(n9,n7) != ssA(n9,n8) & ssA(n9,n7) != ssA(n9,n9) & ssA(n9,n8) != ssA(n9,n9) )). %----column constraints fof(ax92,axiom, ( ssA(n1,n1) = n1 | ssA(n2,n1) = n1 | ssA(n3,n1) = n1 | ssA(n4,n1) = n1 | ssA(n5,n1) = n1 | ssA(n6,n1) = n1 | ssA(n7,n1) = n1 | ssA(n8,n1) = n1 | ssA(n9,n1) = n1 )). fof(ax93,axiom, ( ssA(n1,n1) = n2 | ssA(n2,n1) = n2 | ssA(n3,n1) = n2 | ssA(n4,n1) = n2 | ssA(n5,n1) = n2 | ssA(n6,n1) = n2 | ssA(n7,n1) = n2 | ssA(n8,n1) = n2 | ssA(n9,n1) = n2 )). fof(ax94,axiom, ( ssA(n1,n1) = n3 | ssA(n2,n1) = n3 | ssA(n3,n1) = n3 | ssA(n4,n1) = n3 | ssA(n5,n1) = n3 | ssA(n6,n1) = n3 | ssA(n7,n1) = n3 | ssA(n8,n1) = n3 | ssA(n9,n1) = n3 )). fof(ax95,axiom, ( ssA(n1,n1) = n4 | ssA(n2,n1) = n4 | ssA(n3,n1) = n4 | ssA(n4,n1) = n4 | ssA(n5,n1) = n4 | ssA(n6,n1) = n4 | ssA(n7,n1) = n4 | ssA(n8,n1) = n4 | ssA(n9,n1) = n4 )). fof(ax96,axiom, ( ssA(n1,n1) = n5 | ssA(n2,n1) = n5 | ssA(n3,n1) = n5 | ssA(n4,n1) = n5 | ssA(n5,n1) = n5 | ssA(n6,n1) = n5 | ssA(n7,n1) = n5 | ssA(n8,n1) = n5 | ssA(n9,n1) = n5 )). fof(ax97,axiom, ( ssA(n1,n1) = n6 | ssA(n2,n1) = n6 | ssA(n3,n1) = n6 | ssA(n4,n1) = n6 | ssA(n5,n1) = n6 | ssA(n6,n1) = n6 | ssA(n7,n1) = n6 | ssA(n8,n1) = n6 | ssA(n9,n1) = n6 )). fof(ax98,axiom, ( ssA(n1,n1) = n7 | ssA(n2,n1) = n7 | ssA(n3,n1) = n7 | ssA(n4,n1) = n7 | ssA(n5,n1) = n7 | ssA(n6,n1) = n7 | ssA(n7,n1) = n7 | ssA(n8,n1) = n7 | ssA(n9,n1) = n7 )). fof(ax99,axiom, ( ssA(n1,n1) = n8 | ssA(n2,n1) = n8 | ssA(n3,n1) = n8 | ssA(n4,n1) = n8 | ssA(n5,n1) = n8 | ssA(n6,n1) = n8 | ssA(n7,n1) = n8 | ssA(n8,n1) = n8 | ssA(n9,n1) = n8 )). fof(ax100,axiom, ( ssA(n1,n1) = n9 | ssA(n2,n1) = n9 | ssA(n3,n1) = n9 | ssA(n4,n1) = n9 | ssA(n5,n1) = n9 | ssA(n6,n1) = n9 | ssA(n7,n1) = n9 | ssA(n8,n1) = n9 | ssA(n9,n1) = n9 )). fof(ax101,axiom, ( ssA(n1,n1) != ssA(n2,n1) & ssA(n1,n1) != ssA(n3,n1) & ssA(n1,n1) != ssA(n4,n1) & ssA(n1,n1) != ssA(n5,n1) & ssA(n1,n1) != ssA(n6,n1) & ssA(n1,n1) != ssA(n7,n1) & ssA(n1,n1) != ssA(n8,n1) & ssA(n1,n1) != ssA(n9,n1) & ssA(n2,n1) != ssA(n3,n1) & ssA(n2,n1) != ssA(n4,n1) & ssA(n2,n1) != ssA(n5,n1) & ssA(n2,n1) != ssA(n6,n1) & ssA(n2,n1) != ssA(n7,n1) & ssA(n2,n1) != ssA(n8,n1) & ssA(n2,n1) != ssA(n9,n1) & ssA(n3,n1) != ssA(n4,n1) & ssA(n3,n1) != ssA(n5,n1) & ssA(n3,n1) != ssA(n6,n1) & ssA(n3,n1) != ssA(n7,n1) & ssA(n3,n1) != ssA(n8,n1) & ssA(n3,n1) != ssA(n9,n1) & ssA(n4,n1) != ssA(n5,n1) & ssA(n4,n1) != ssA(n6,n1) & ssA(n4,n1) != ssA(n7,n1) & ssA(n4,n1) != ssA(n8,n1) & ssA(n4,n1) != ssA(n9,n1) & ssA(n5,n1) != ssA(n6,n1) & ssA(n5,n1) != ssA(n7,n1) & ssA(n5,n1) != ssA(n8,n1) & ssA(n5,n1) != ssA(n9,n1) & ssA(n6,n1) != ssA(n7,n1) & ssA(n6,n1) != ssA(n8,n1) & ssA(n6,n1) != ssA(n9,n1) & ssA(n7,n1) != ssA(n8,n1) & ssA(n7,n1) != ssA(n9,n1) & ssA(n8,n1) != ssA(n9,n1) )). fof(ax102,axiom, ( ssA(n1,n2) = n1 | ssA(n2,n2) = n1 | ssA(n3,n2) = n1 | ssA(n4,n2) = n1 | ssA(n5,n2) = n1 | ssA(n6,n2) = n1 | ssA(n7,n2) = n1 | ssA(n8,n2) = n1 | ssA(n9,n2) = n1 )). fof(ax103,axiom, ( ssA(n1,n2) = n2 | ssA(n2,n2) = n2 | ssA(n3,n2) = n2 | ssA(n4,n2) = n2 | ssA(n5,n2) = n2 | ssA(n6,n2) = n2 | ssA(n7,n2) = n2 | ssA(n8,n2) = n2 | ssA(n9,n2) = n2 )). fof(ax104,axiom, ( ssA(n1,n2) = n3 | ssA(n2,n2) = n3 | ssA(n3,n2) = n3 | ssA(n4,n2) = n3 | ssA(n5,n2) = n3 | ssA(n6,n2) = n3 | ssA(n7,n2) = n3 | ssA(n8,n2) = n3 | ssA(n9,n2) = n3 )). fof(ax105,axiom, ( ssA(n1,n2) = n4 | ssA(n2,n2) = n4 | ssA(n3,n2) = n4 | ssA(n4,n2) = n4 | ssA(n5,n2) = n4 | ssA(n6,n2) = n4 | ssA(n7,n2) = n4 | ssA(n8,n2) = n4 | ssA(n9,n2) = n4 )). fof(ax106,axiom, ( ssA(n1,n2) = n5 | ssA(n2,n2) = n5 | ssA(n3,n2) = n5 | ssA(n4,n2) = n5 | ssA(n5,n2) = n5 | ssA(n6,n2) = n5 | ssA(n7,n2) = n5 | ssA(n8,n2) = n5 | ssA(n9,n2) = n5 )). fof(ax107,axiom, ( ssA(n1,n2) = n6 | ssA(n2,n2) = n6 | ssA(n3,n2) = n6 | ssA(n4,n2) = n6 | ssA(n5,n2) = n6 | ssA(n6,n2) = n6 | ssA(n7,n2) = n6 | ssA(n8,n2) = n6 | ssA(n9,n2) = n6 )). fof(ax108,axiom, ( ssA(n1,n2) = n7 | ssA(n2,n2) = n7 | ssA(n3,n2) = n7 | ssA(n4,n2) = n7 | ssA(n5,n2) = n7 | ssA(n6,n2) = n7 | ssA(n7,n2) = n7 | ssA(n8,n2) = n7 | ssA(n9,n2) = n7 )). fof(ax109,axiom, ( ssA(n1,n2) = n8 | ssA(n2,n2) = n8 | ssA(n3,n2) = n8 | ssA(n4,n2) = n8 | ssA(n5,n2) = n8 | ssA(n6,n2) = n8 | ssA(n7,n2) = n8 | ssA(n8,n2) = n8 | ssA(n9,n2) = n8 )). fof(ax110,axiom, ( ssA(n1,n2) = n9 | ssA(n2,n2) = n9 | ssA(n3,n2) = n9 | ssA(n4,n2) = n9 | ssA(n5,n2) = n9 | ssA(n6,n2) = n9 | ssA(n7,n2) = n9 | ssA(n8,n2) = n9 | ssA(n9,n2) = n9 )). fof(ax111,axiom, ( ssA(n1,n2) != ssA(n2,n2) & ssA(n1,n2) != ssA(n3,n2) & ssA(n1,n2) != ssA(n4,n2) & ssA(n1,n2) != ssA(n5,n2) & ssA(n1,n2) != ssA(n6,n2) & ssA(n1,n2) != ssA(n7,n2) & ssA(n1,n2) != ssA(n8,n2) & ssA(n1,n2) != ssA(n9,n2) & ssA(n2,n2) != ssA(n3,n2) & ssA(n2,n2) != ssA(n4,n2) & ssA(n2,n2) != ssA(n5,n2) & ssA(n2,n2) != ssA(n6,n2) & ssA(n2,n2) != ssA(n7,n2) & ssA(n2,n2) != ssA(n8,n2) & ssA(n2,n2) != ssA(n9,n2) & ssA(n3,n2) != ssA(n4,n2) & ssA(n3,n2) != ssA(n5,n2) & ssA(n3,n2) != ssA(n6,n2) & ssA(n3,n2) != ssA(n7,n2) & ssA(n3,n2) != ssA(n8,n2) & ssA(n3,n2) != ssA(n9,n2) & ssA(n4,n2) != ssA(n5,n2) & ssA(n4,n2) != ssA(n6,n2) & ssA(n4,n2) != ssA(n7,n2) & ssA(n4,n2) != ssA(n8,n2) & ssA(n4,n2) != ssA(n9,n2) & ssA(n5,n2) != ssA(n6,n2) & ssA(n5,n2) != ssA(n7,n2) & ssA(n5,n2) != ssA(n8,n2) & ssA(n5,n2) != ssA(n9,n2) & ssA(n6,n2) != ssA(n7,n2) & ssA(n6,n2) != ssA(n8,n2) & ssA(n6,n2) != ssA(n9,n2) & ssA(n7,n2) != ssA(n8,n2) & ssA(n7,n2) != ssA(n9,n2) & ssA(n8,n2) != ssA(n9,n2) )). fof(ax112,axiom, ( ssA(n1,n3) = n1 | ssA(n2,n3) = n1 | ssA(n3,n3) = n1 | ssA(n4,n3) = n1 | ssA(n5,n3) = n1 | ssA(n6,n3) = n1 | ssA(n7,n3) = n1 | ssA(n8,n3) = n1 | ssA(n9,n3) = n1 )). fof(ax113,axiom, ( ssA(n1,n3) = n2 | ssA(n2,n3) = n2 | ssA(n3,n3) = n2 | ssA(n4,n3) = n2 | ssA(n5,n3) = n2 | ssA(n6,n3) = n2 | ssA(n7,n3) = n2 | ssA(n8,n3) = n2 | ssA(n9,n3) = n2 )). fof(ax114,axiom, ( ssA(n1,n3) = n3 | ssA(n2,n3) = n3 | ssA(n3,n3) = n3 | ssA(n4,n3) = n3 | ssA(n5,n3) = n3 | ssA(n6,n3) = n3 | ssA(n7,n3) = n3 | ssA(n8,n3) = n3 | ssA(n9,n3) = n3 )). fof(ax115,axiom, ( ssA(n1,n3) = n4 | ssA(n2,n3) = n4 | ssA(n3,n3) = n4 | ssA(n4,n3) = n4 | ssA(n5,n3) = n4 | ssA(n6,n3) = n4 | ssA(n7,n3) = n4 | ssA(n8,n3) = n4 | ssA(n9,n3) = n4 )). fof(ax116,axiom, ( ssA(n1,n3) = n5 | ssA(n2,n3) = n5 | ssA(n3,n3) = n5 | ssA(n4,n3) = n5 | ssA(n5,n3) = n5 | ssA(n6,n3) = n5 | ssA(n7,n3) = n5 | ssA(n8,n3) = n5 | ssA(n9,n3) = n5 )). fof(ax117,axiom, ( ssA(n1,n3) = n6 | ssA(n2,n3) = n6 | ssA(n3,n3) = n6 | ssA(n4,n3) = n6 | ssA(n5,n3) = n6 | ssA(n6,n3) = n6 | ssA(n7,n3) = n6 | ssA(n8,n3) = n6 | ssA(n9,n3) = n6 )). fof(ax118,axiom, ( ssA(n1,n3) = n7 | ssA(n2,n3) = n7 | ssA(n3,n3) = n7 | ssA(n4,n3) = n7 | ssA(n5,n3) = n7 | ssA(n6,n3) = n7 | ssA(n7,n3) = n7 | ssA(n8,n3) = n7 | ssA(n9,n3) = n7 )). fof(ax119,axiom, ( ssA(n1,n3) = n8 | ssA(n2,n3) = n8 | ssA(n3,n3) = n8 | ssA(n4,n3) = n8 | ssA(n5,n3) = n8 | ssA(n6,n3) = n8 | ssA(n7,n3) = n8 | ssA(n8,n3) = n8 | ssA(n9,n3) = n8 )). fof(ax120,axiom, ( ssA(n1,n3) = n9 | ssA(n2,n3) = n9 | ssA(n3,n3) = n9 | ssA(n4,n3) = n9 | ssA(n5,n3) = n9 | ssA(n6,n3) = n9 | ssA(n7,n3) = n9 | ssA(n8,n3) = n9 | ssA(n9,n3) = n9 )). fof(ax121,axiom, ( ssA(n1,n3) != ssA(n2,n3) & ssA(n1,n3) != ssA(n3,n3) & ssA(n1,n3) != ssA(n4,n3) & ssA(n1,n3) != ssA(n5,n3) & ssA(n1,n3) != ssA(n6,n3) & ssA(n1,n3) != ssA(n7,n3) & ssA(n1,n3) != ssA(n8,n3) & ssA(n1,n3) != ssA(n9,n3) & ssA(n2,n3) != ssA(n3,n3) & ssA(n2,n3) != ssA(n4,n3) & ssA(n2,n3) != ssA(n5,n3) & ssA(n2,n3) != ssA(n6,n3) & ssA(n2,n3) != ssA(n7,n3) & ssA(n2,n3) != ssA(n8,n3) & ssA(n2,n3) != ssA(n9,n3) & ssA(n3,n3) != ssA(n4,n3) & ssA(n3,n3) != ssA(n5,n3) & ssA(n3,n3) != ssA(n6,n3) & ssA(n3,n3) != ssA(n7,n3) & ssA(n3,n3) != ssA(n8,n3) & ssA(n3,n3) != ssA(n9,n3) & ssA(n4,n3) != ssA(n5,n3) & ssA(n4,n3) != ssA(n6,n3) & ssA(n4,n3) != ssA(n7,n3) & ssA(n4,n3) != ssA(n8,n3) & ssA(n4,n3) != ssA(n9,n3) & ssA(n5,n3) != ssA(n6,n3) & ssA(n5,n3) != ssA(n7,n3) & ssA(n5,n3) != ssA(n8,n3) & ssA(n5,n3) != ssA(n9,n3) & ssA(n6,n3) != ssA(n7,n3) & ssA(n6,n3) != ssA(n8,n3) & ssA(n6,n3) != ssA(n9,n3) & ssA(n7,n3) != ssA(n8,n3) & ssA(n7,n3) != ssA(n9,n3) & ssA(n8,n3) != ssA(n9,n3) )). fof(ax122,axiom, ( ssA(n1,n4) = n1 | ssA(n2,n4) = n1 | ssA(n3,n4) = n1 | ssA(n4,n4) = n1 | ssA(n5,n4) = n1 | ssA(n6,n4) = n1 | ssA(n7,n4) = n1 | ssA(n8,n4) = n1 | ssA(n9,n4) = n1 )). fof(ax123,axiom, ( ssA(n1,n4) = n2 | ssA(n2,n4) = n2 | ssA(n3,n4) = n2 | ssA(n4,n4) = n2 | ssA(n5,n4) = n2 | ssA(n6,n4) = n2 | ssA(n7,n4) = n2 | ssA(n8,n4) = n2 | ssA(n9,n4) = n2 )). fof(ax124,axiom, ( ssA(n1,n4) = n3 | ssA(n2,n4) = n3 | ssA(n3,n4) = n3 | ssA(n4,n4) = n3 | ssA(n5,n4) = n3 | ssA(n6,n4) = n3 | ssA(n7,n4) = n3 | ssA(n8,n4) = n3 | ssA(n9,n4) = n3 )). fof(ax125,axiom, ( ssA(n1,n4) = n4 | ssA(n2,n4) = n4 | ssA(n3,n4) = n4 | ssA(n4,n4) = n4 | ssA(n5,n4) = n4 | ssA(n6,n4) = n4 | ssA(n7,n4) = n4 | ssA(n8,n4) = n4 | ssA(n9,n4) = n4 )). fof(ax126,axiom, ( ssA(n1,n4) = n5 | ssA(n2,n4) = n5 | ssA(n3,n4) = n5 | ssA(n4,n4) = n5 | ssA(n5,n4) = n5 | ssA(n6,n4) = n5 | ssA(n7,n4) = n5 | ssA(n8,n4) = n5 | ssA(n9,n4) = n5 )). fof(ax127,axiom, ( ssA(n1,n4) = n6 | ssA(n2,n4) = n6 | ssA(n3,n4) = n6 | ssA(n4,n4) = n6 | ssA(n5,n4) = n6 | ssA(n6,n4) = n6 | ssA(n7,n4) = n6 | ssA(n8,n4) = n6 | ssA(n9,n4) = n6 )). fof(ax128,axiom, ( ssA(n1,n4) = n7 | ssA(n2,n4) = n7 | ssA(n3,n4) = n7 | ssA(n4,n4) = n7 | ssA(n5,n4) = n7 | ssA(n6,n4) = n7 | ssA(n7,n4) = n7 | ssA(n8,n4) = n7 | ssA(n9,n4) = n7 )). fof(ax129,axiom, ( ssA(n1,n4) = n8 | ssA(n2,n4) = n8 | ssA(n3,n4) = n8 | ssA(n4,n4) = n8 | ssA(n5,n4) = n8 | ssA(n6,n4) = n8 | ssA(n7,n4) = n8 | ssA(n8,n4) = n8 | ssA(n9,n4) = n8 )). fof(ax130,axiom, ( ssA(n1,n4) = n9 | ssA(n2,n4) = n9 | ssA(n3,n4) = n9 | ssA(n4,n4) = n9 | ssA(n5,n4) = n9 | ssA(n6,n4) = n9 | ssA(n7,n4) = n9 | ssA(n8,n4) = n9 | ssA(n9,n4) = n9 )). fof(ax131,axiom, ( ssA(n1,n4) != ssA(n2,n4) & ssA(n1,n4) != ssA(n3,n4) & ssA(n1,n4) != ssA(n4,n4) & ssA(n1,n4) != ssA(n5,n4) & ssA(n1,n4) != ssA(n6,n4) & ssA(n1,n4) != ssA(n7,n4) & ssA(n1,n4) != ssA(n8,n4) & ssA(n1,n4) != ssA(n9,n4) & ssA(n2,n4) != ssA(n3,n4) & ssA(n2,n4) != ssA(n4,n4) & ssA(n2,n4) != ssA(n5,n4) & ssA(n2,n4) != ssA(n6,n4) & ssA(n2,n4) != ssA(n7,n4) & ssA(n2,n4) != ssA(n8,n4) & ssA(n2,n4) != ssA(n9,n4) & ssA(n3,n4) != ssA(n4,n4) & ssA(n3,n4) != ssA(n5,n4) & ssA(n3,n4) != ssA(n6,n4) & ssA(n3,n4) != ssA(n7,n4) & ssA(n3,n4) != ssA(n8,n4) & ssA(n3,n4) != ssA(n9,n4) & ssA(n4,n4) != ssA(n5,n4) & ssA(n4,n4) != ssA(n6,n4) & ssA(n4,n4) != ssA(n7,n4) & ssA(n4,n4) != ssA(n8,n4) & ssA(n4,n4) != ssA(n9,n4) & ssA(n5,n4) != ssA(n6,n4) & ssA(n5,n4) != ssA(n7,n4) & ssA(n5,n4) != ssA(n8,n4) & ssA(n5,n4) != ssA(n9,n4) & ssA(n6,n4) != ssA(n7,n4) & ssA(n6,n4) != ssA(n8,n4) & ssA(n6,n4) != ssA(n9,n4) & ssA(n7,n4) != ssA(n8,n4) & ssA(n7,n4) != ssA(n9,n4) & ssA(n8,n4) != ssA(n9,n4) )). fof(ax132,axiom, ( ssA(n1,n5) = n1 | ssA(n2,n5) = n1 | ssA(n3,n5) = n1 | ssA(n4,n5) = n1 | ssA(n5,n5) = n1 | ssA(n6,n5) = n1 | ssA(n7,n5) = n1 | ssA(n8,n5) = n1 | ssA(n9,n5) = n1 )). fof(ax133,axiom, ( ssA(n1,n5) = n2 | ssA(n2,n5) = n2 | ssA(n3,n5) = n2 | ssA(n4,n5) = n2 | ssA(n5,n5) = n2 | ssA(n6,n5) = n2 | ssA(n7,n5) = n2 | ssA(n8,n5) = n2 | ssA(n9,n5) = n2 )). fof(ax134,axiom, ( ssA(n1,n5) = n3 | ssA(n2,n5) = n3 | ssA(n3,n5) = n3 | ssA(n4,n5) = n3 | ssA(n5,n5) = n3 | ssA(n6,n5) = n3 | ssA(n7,n5) = n3 | ssA(n8,n5) = n3 | ssA(n9,n5) = n3 )). fof(ax135,axiom, ( ssA(n1,n5) = n4 | ssA(n2,n5) = n4 | ssA(n3,n5) = n4 | ssA(n4,n5) = n4 | ssA(n5,n5) = n4 | ssA(n6,n5) = n4 | ssA(n7,n5) = n4 | ssA(n8,n5) = n4 | ssA(n9,n5) = n4 )). fof(ax136,axiom, ( ssA(n1,n5) = n5 | ssA(n2,n5) = n5 | ssA(n3,n5) = n5 | ssA(n4,n5) = n5 | ssA(n5,n5) = n5 | ssA(n6,n5) = n5 | ssA(n7,n5) = n5 | ssA(n8,n5) = n5 | ssA(n9,n5) = n5 )). fof(ax137,axiom, ( ssA(n1,n5) = n6 | ssA(n2,n5) = n6 | ssA(n3,n5) = n6 | ssA(n4,n5) = n6 | ssA(n5,n5) = n6 | ssA(n6,n5) = n6 | ssA(n7,n5) = n6 | ssA(n8,n5) = n6 | ssA(n9,n5) = n6 )). fof(ax138,axiom, ( ssA(n1,n5) = n7 | ssA(n2,n5) = n7 | ssA(n3,n5) = n7 | ssA(n4,n5) = n7 | ssA(n5,n5) = n7 | ssA(n6,n5) = n7 | ssA(n7,n5) = n7 | ssA(n8,n5) = n7 | ssA(n9,n5) = n7 )). fof(ax139,axiom, ( ssA(n1,n5) = n8 | ssA(n2,n5) = n8 | ssA(n3,n5) = n8 | ssA(n4,n5) = n8 | ssA(n5,n5) = n8 | ssA(n6,n5) = n8 | ssA(n7,n5) = n8 | ssA(n8,n5) = n8 | ssA(n9,n5) = n8 )). fof(ax140,axiom, ( ssA(n1,n5) = n9 | ssA(n2,n5) = n9 | ssA(n3,n5) = n9 | ssA(n4,n5) = n9 | ssA(n5,n5) = n9 | ssA(n6,n5) = n9 | ssA(n7,n5) = n9 | ssA(n8,n5) = n9 | ssA(n9,n5) = n9 )). fof(ax141,axiom, ( ssA(n1,n5) != ssA(n2,n5) & ssA(n1,n5) != ssA(n3,n5) & ssA(n1,n5) != ssA(n4,n5) & ssA(n1,n5) != ssA(n5,n5) & ssA(n1,n5) != ssA(n6,n5) & ssA(n1,n5) != ssA(n7,n5) & ssA(n1,n5) != ssA(n8,n5) & ssA(n1,n5) != ssA(n9,n5) & ssA(n2,n5) != ssA(n3,n5) & ssA(n2,n5) != ssA(n4,n5) & ssA(n2,n5) != ssA(n5,n5) & ssA(n2,n5) != ssA(n6,n5) & ssA(n2,n5) != ssA(n7,n5) & ssA(n2,n5) != ssA(n8,n5) & ssA(n2,n5) != ssA(n9,n5) & ssA(n3,n5) != ssA(n4,n5) & ssA(n3,n5) != ssA(n5,n5) & ssA(n3,n5) != ssA(n6,n5) & ssA(n3,n5) != ssA(n7,n5) & ssA(n3,n5) != ssA(n8,n5) & ssA(n3,n5) != ssA(n9,n5) & ssA(n4,n5) != ssA(n5,n5) & ssA(n4,n5) != ssA(n6,n5) & ssA(n4,n5) != ssA(n7,n5) & ssA(n4,n5) != ssA(n8,n5) & ssA(n4,n5) != ssA(n9,n5) & ssA(n5,n5) != ssA(n6,n5) & ssA(n5,n5) != ssA(n7,n5) & ssA(n5,n5) != ssA(n8,n5) & ssA(n5,n5) != ssA(n9,n5) & ssA(n6,n5) != ssA(n7,n5) & ssA(n6,n5) != ssA(n8,n5) & ssA(n6,n5) != ssA(n9,n5) & ssA(n7,n5) != ssA(n8,n5) & ssA(n7,n5) != ssA(n9,n5) & ssA(n8,n5) != ssA(n9,n5) )). fof(ax142,axiom, ( ssA(n1,n6) = n1 | ssA(n2,n6) = n1 | ssA(n3,n6) = n1 | ssA(n4,n6) = n1 | ssA(n5,n6) = n1 | ssA(n6,n6) = n1 | ssA(n7,n6) = n1 | ssA(n8,n6) = n1 | ssA(n9,n6) = n1 )). fof(ax143,axiom, ( ssA(n1,n6) = n2 | ssA(n2,n6) = n2 | ssA(n3,n6) = n2 | ssA(n4,n6) = n2 | ssA(n5,n6) = n2 | ssA(n6,n6) = n2 | ssA(n7,n6) = n2 | ssA(n8,n6) = n2 | ssA(n9,n6) = n2 )). fof(ax144,axiom, ( ssA(n1,n6) = n3 | ssA(n2,n6) = n3 | ssA(n3,n6) = n3 | ssA(n4,n6) = n3 | ssA(n5,n6) = n3 | ssA(n6,n6) = n3 | ssA(n7,n6) = n3 | ssA(n8,n6) = n3 | ssA(n9,n6) = n3 )). fof(ax145,axiom, ( ssA(n1,n6) = n4 | ssA(n2,n6) = n4 | ssA(n3,n6) = n4 | ssA(n4,n6) = n4 | ssA(n5,n6) = n4 | ssA(n6,n6) = n4 | ssA(n7,n6) = n4 | ssA(n8,n6) = n4 | ssA(n9,n6) = n4 )). fof(ax146,axiom, ( ssA(n1,n6) = n5 | ssA(n2,n6) = n5 | ssA(n3,n6) = n5 | ssA(n4,n6) = n5 | ssA(n5,n6) = n5 | ssA(n6,n6) = n5 | ssA(n7,n6) = n5 | ssA(n8,n6) = n5 | ssA(n9,n6) = n5 )). fof(ax147,axiom, ( ssA(n1,n6) = n6 | ssA(n2,n6) = n6 | ssA(n3,n6) = n6 | ssA(n4,n6) = n6 | ssA(n5,n6) = n6 | ssA(n6,n6) = n6 | ssA(n7,n6) = n6 | ssA(n8,n6) = n6 | ssA(n9,n6) = n6 )). fof(ax148,axiom, ( ssA(n1,n6) = n7 | ssA(n2,n6) = n7 | ssA(n3,n6) = n7 | ssA(n4,n6) = n7 | ssA(n5,n6) = n7 | ssA(n6,n6) = n7 | ssA(n7,n6) = n7 | ssA(n8,n6) = n7 | ssA(n9,n6) = n7 )). fof(ax149,axiom, ( ssA(n1,n6) = n8 | ssA(n2,n6) = n8 | ssA(n3,n6) = n8 | ssA(n4,n6) = n8 | ssA(n5,n6) = n8 | ssA(n6,n6) = n8 | ssA(n7,n6) = n8 | ssA(n8,n6) = n8 | ssA(n9,n6) = n8 )). fof(ax150,axiom, ( ssA(n1,n6) = n9 | ssA(n2,n6) = n9 | ssA(n3,n6) = n9 | ssA(n4,n6) = n9 | ssA(n5,n6) = n9 | ssA(n6,n6) = n9 | ssA(n7,n6) = n9 | ssA(n8,n6) = n9 | ssA(n9,n6) = n9 )). fof(ax151,axiom, ( ssA(n1,n6) != ssA(n2,n6) & ssA(n1,n6) != ssA(n3,n6) & ssA(n1,n6) != ssA(n4,n6) & ssA(n1,n6) != ssA(n5,n6) & ssA(n1,n6) != ssA(n6,n6) & ssA(n1,n6) != ssA(n7,n6) & ssA(n1,n6) != ssA(n8,n6) & ssA(n1,n6) != ssA(n9,n6) & ssA(n2,n6) != ssA(n3,n6) & ssA(n2,n6) != ssA(n4,n6) & ssA(n2,n6) != ssA(n5,n6) & ssA(n2,n6) != ssA(n6,n6) & ssA(n2,n6) != ssA(n7,n6) & ssA(n2,n6) != ssA(n8,n6) & ssA(n2,n6) != ssA(n9,n6) & ssA(n3,n6) != ssA(n4,n6) & ssA(n3,n6) != ssA(n5,n6) & ssA(n3,n6) != ssA(n6,n6) & ssA(n3,n6) != ssA(n7,n6) & ssA(n3,n6) != ssA(n8,n6) & ssA(n3,n6) != ssA(n9,n6) & ssA(n4,n6) != ssA(n5,n6) & ssA(n4,n6) != ssA(n6,n6) & ssA(n4,n6) != ssA(n7,n6) & ssA(n4,n6) != ssA(n8,n6) & ssA(n4,n6) != ssA(n9,n6) & ssA(n5,n6) != ssA(n6,n6) & ssA(n5,n6) != ssA(n7,n6) & ssA(n5,n6) != ssA(n8,n6) & ssA(n5,n6) != ssA(n9,n6) & ssA(n6,n6) != ssA(n7,n6) & ssA(n6,n6) != ssA(n8,n6) & ssA(n6,n6) != ssA(n9,n6) & ssA(n7,n6) != ssA(n8,n6) & ssA(n7,n6) != ssA(n9,n6) & ssA(n8,n6) != ssA(n9,n6) )). fof(ax152,axiom, ( ssA(n1,n7) = n1 | ssA(n2,n7) = n1 | ssA(n3,n7) = n1 | ssA(n4,n7) = n1 | ssA(n5,n7) = n1 | ssA(n6,n7) = n1 | ssA(n7,n7) = n1 | ssA(n8,n7) = n1 | ssA(n9,n7) = n1 )). fof(ax153,axiom, ( ssA(n1,n7) = n2 | ssA(n2,n7) = n2 | ssA(n3,n7) = n2 | ssA(n4,n7) = n2 | ssA(n5,n7) = n2 | ssA(n6,n7) = n2 | ssA(n7,n7) = n2 | ssA(n8,n7) = n2 | ssA(n9,n7) = n2 )). fof(ax154,axiom, ( ssA(n1,n7) = n3 | ssA(n2,n7) = n3 | ssA(n3,n7) = n3 | ssA(n4,n7) = n3 | ssA(n5,n7) = n3 | ssA(n6,n7) = n3 | ssA(n7,n7) = n3 | ssA(n8,n7) = n3 | ssA(n9,n7) = n3 )). fof(ax155,axiom, ( ssA(n1,n7) = n4 | ssA(n2,n7) = n4 | ssA(n3,n7) = n4 | ssA(n4,n7) = n4 | ssA(n5,n7) = n4 | ssA(n6,n7) = n4 | ssA(n7,n7) = n4 | ssA(n8,n7) = n4 | ssA(n9,n7) = n4 )). fof(ax156,axiom, ( ssA(n1,n7) = n5 | ssA(n2,n7) = n5 | ssA(n3,n7) = n5 | ssA(n4,n7) = n5 | ssA(n5,n7) = n5 | ssA(n6,n7) = n5 | ssA(n7,n7) = n5 | ssA(n8,n7) = n5 | ssA(n9,n7) = n5 )). fof(ax157,axiom, ( ssA(n1,n7) = n6 | ssA(n2,n7) = n6 | ssA(n3,n7) = n6 | ssA(n4,n7) = n6 | ssA(n5,n7) = n6 | ssA(n6,n7) = n6 | ssA(n7,n7) = n6 | ssA(n8,n7) = n6 | ssA(n9,n7) = n6 )). fof(ax158,axiom, ( ssA(n1,n7) = n7 | ssA(n2,n7) = n7 | ssA(n3,n7) = n7 | ssA(n4,n7) = n7 | ssA(n5,n7) = n7 | ssA(n6,n7) = n7 | ssA(n7,n7) = n7 | ssA(n8,n7) = n7 | ssA(n9,n7) = n7 )). fof(ax159,axiom, ( ssA(n1,n7) = n8 | ssA(n2,n7) = n8 | ssA(n3,n7) = n8 | ssA(n4,n7) = n8 | ssA(n5,n7) = n8 | ssA(n6,n7) = n8 | ssA(n7,n7) = n8 | ssA(n8,n7) = n8 | ssA(n9,n7) = n8 )). fof(ax160,axiom, ( ssA(n1,n7) = n9 | ssA(n2,n7) = n9 | ssA(n3,n7) = n9 | ssA(n4,n7) = n9 | ssA(n5,n7) = n9 | ssA(n6,n7) = n9 | ssA(n7,n7) = n9 | ssA(n8,n7) = n9 | ssA(n9,n7) = n9 )). fof(ax161,axiom, ( ssA(n1,n7) != ssA(n2,n7) & ssA(n1,n7) != ssA(n3,n7) & ssA(n1,n7) != ssA(n4,n7) & ssA(n1,n7) != ssA(n5,n7) & ssA(n1,n7) != ssA(n6,n7) & ssA(n1,n7) != ssA(n7,n7) & ssA(n1,n7) != ssA(n8,n7) & ssA(n1,n7) != ssA(n9,n7) & ssA(n2,n7) != ssA(n3,n7) & ssA(n2,n7) != ssA(n4,n7) & ssA(n2,n7) != ssA(n5,n7) & ssA(n2,n7) != ssA(n6,n7) & ssA(n2,n7) != ssA(n7,n7) & ssA(n2,n7) != ssA(n8,n7) & ssA(n2,n7) != ssA(n9,n7) & ssA(n3,n7) != ssA(n4,n7) & ssA(n3,n7) != ssA(n5,n7) & ssA(n3,n7) != ssA(n6,n7) & ssA(n3,n7) != ssA(n7,n7) & ssA(n3,n7) != ssA(n8,n7) & ssA(n3,n7) != ssA(n9,n7) & ssA(n4,n7) != ssA(n5,n7) & ssA(n4,n7) != ssA(n6,n7) & ssA(n4,n7) != ssA(n7,n7) & ssA(n4,n7) != ssA(n8,n7) & ssA(n4,n7) != ssA(n9,n7) & ssA(n5,n7) != ssA(n6,n7) & ssA(n5,n7) != ssA(n7,n7) & ssA(n5,n7) != ssA(n8,n7) & ssA(n5,n7) != ssA(n9,n7) & ssA(n6,n7) != ssA(n7,n7) & ssA(n6,n7) != ssA(n8,n7) & ssA(n6,n7) != ssA(n9,n7) & ssA(n7,n7) != ssA(n8,n7) & ssA(n7,n7) != ssA(n9,n7) & ssA(n8,n7) != ssA(n9,n7) )). fof(ax162,axiom, ( ssA(n1,n8) = n1 | ssA(n2,n8) = n1 | ssA(n3,n8) = n1 | ssA(n4,n8) = n1 | ssA(n5,n8) = n1 | ssA(n6,n8) = n1 | ssA(n7,n8) = n1 | ssA(n8,n8) = n1 | ssA(n9,n8) = n1 )). fof(ax163,axiom, ( ssA(n1,n8) = n2 | ssA(n2,n8) = n2 | ssA(n3,n8) = n2 | ssA(n4,n8) = n2 | ssA(n5,n8) = n2 | ssA(n6,n8) = n2 | ssA(n7,n8) = n2 | ssA(n8,n8) = n2 | ssA(n9,n8) = n2 )). fof(ax164,axiom, ( ssA(n1,n8) = n3 | ssA(n2,n8) = n3 | ssA(n3,n8) = n3 | ssA(n4,n8) = n3 | ssA(n5,n8) = n3 | ssA(n6,n8) = n3 | ssA(n7,n8) = n3 | ssA(n8,n8) = n3 | ssA(n9,n8) = n3 )). fof(ax165,axiom, ( ssA(n1,n8) = n4 | ssA(n2,n8) = n4 | ssA(n3,n8) = n4 | ssA(n4,n8) = n4 | ssA(n5,n8) = n4 | ssA(n6,n8) = n4 | ssA(n7,n8) = n4 | ssA(n8,n8) = n4 | ssA(n9,n8) = n4 )). fof(ax166,axiom, ( ssA(n1,n8) = n5 | ssA(n2,n8) = n5 | ssA(n3,n8) = n5 | ssA(n4,n8) = n5 | ssA(n5,n8) = n5 | ssA(n6,n8) = n5 | ssA(n7,n8) = n5 | ssA(n8,n8) = n5 | ssA(n9,n8) = n5 )). fof(ax167,axiom, ( ssA(n1,n8) = n6 | ssA(n2,n8) = n6 | ssA(n3,n8) = n6 | ssA(n4,n8) = n6 | ssA(n5,n8) = n6 | ssA(n6,n8) = n6 | ssA(n7,n8) = n6 | ssA(n8,n8) = n6 | ssA(n9,n8) = n6 )). fof(ax168,axiom, ( ssA(n1,n8) = n7 | ssA(n2,n8) = n7 | ssA(n3,n8) = n7 | ssA(n4,n8) = n7 | ssA(n5,n8) = n7 | ssA(n6,n8) = n7 | ssA(n7,n8) = n7 | ssA(n8,n8) = n7 | ssA(n9,n8) = n7 )). fof(ax169,axiom, ( ssA(n1,n8) = n8 | ssA(n2,n8) = n8 | ssA(n3,n8) = n8 | ssA(n4,n8) = n8 | ssA(n5,n8) = n8 | ssA(n6,n8) = n8 | ssA(n7,n8) = n8 | ssA(n8,n8) = n8 | ssA(n9,n8) = n8 )). fof(ax170,axiom, ( ssA(n1,n8) = n9 | ssA(n2,n8) = n9 | ssA(n3,n8) = n9 | ssA(n4,n8) = n9 | ssA(n5,n8) = n9 | ssA(n6,n8) = n9 | ssA(n7,n8) = n9 | ssA(n8,n8) = n9 | ssA(n9,n8) = n9 )). fof(ax171,axiom, ( ssA(n1,n8) != ssA(n2,n8) & ssA(n1,n8) != ssA(n3,n8) & ssA(n1,n8) != ssA(n4,n8) & ssA(n1,n8) != ssA(n5,n8) & ssA(n1,n8) != ssA(n6,n8) & ssA(n1,n8) != ssA(n7,n8) & ssA(n1,n8) != ssA(n8,n8) & ssA(n1,n8) != ssA(n9,n8) & ssA(n2,n8) != ssA(n3,n8) & ssA(n2,n8) != ssA(n4,n8) & ssA(n2,n8) != ssA(n5,n8) & ssA(n2,n8) != ssA(n6,n8) & ssA(n2,n8) != ssA(n7,n8) & ssA(n2,n8) != ssA(n8,n8) & ssA(n2,n8) != ssA(n9,n8) & ssA(n3,n8) != ssA(n4,n8) & ssA(n3,n8) != ssA(n5,n8) & ssA(n3,n8) != ssA(n6,n8) & ssA(n3,n8) != ssA(n7,n8) & ssA(n3,n8) != ssA(n8,n8) & ssA(n3,n8) != ssA(n9,n8) & ssA(n4,n8) != ssA(n5,n8) & ssA(n4,n8) != ssA(n6,n8) & ssA(n4,n8) != ssA(n7,n8) & ssA(n4,n8) != ssA(n8,n8) & ssA(n4,n8) != ssA(n9,n8) & ssA(n5,n8) != ssA(n6,n8) & ssA(n5,n8) != ssA(n7,n8) & ssA(n5,n8) != ssA(n8,n8) & ssA(n5,n8) != ssA(n9,n8) & ssA(n6,n8) != ssA(n7,n8) & ssA(n6,n8) != ssA(n8,n8) & ssA(n6,n8) != ssA(n9,n8) & ssA(n7,n8) != ssA(n8,n8) & ssA(n7,n8) != ssA(n9,n8) & ssA(n8,n8) != ssA(n9,n8) )). fof(ax172,axiom, ( ssA(n1,n9) = n1 | ssA(n2,n9) = n1 | ssA(n3,n9) = n1 | ssA(n4,n9) = n1 | ssA(n5,n9) = n1 | ssA(n6,n9) = n1 | ssA(n7,n9) = n1 | ssA(n8,n9) = n1 | ssA(n9,n9) = n1 )). fof(ax173,axiom, ( ssA(n1,n9) = n2 | ssA(n2,n9) = n2 | ssA(n3,n9) = n2 | ssA(n4,n9) = n2 | ssA(n5,n9) = n2 | ssA(n6,n9) = n2 | ssA(n7,n9) = n2 | ssA(n8,n9) = n2 | ssA(n9,n9) = n2 )). fof(ax174,axiom, ( ssA(n1,n9) = n3 | ssA(n2,n9) = n3 | ssA(n3,n9) = n3 | ssA(n4,n9) = n3 | ssA(n5,n9) = n3 | ssA(n6,n9) = n3 | ssA(n7,n9) = n3 | ssA(n8,n9) = n3 | ssA(n9,n9) = n3 )). fof(ax175,axiom, ( ssA(n1,n9) = n4 | ssA(n2,n9) = n4 | ssA(n3,n9) = n4 | ssA(n4,n9) = n4 | ssA(n5,n9) = n4 | ssA(n6,n9) = n4 | ssA(n7,n9) = n4 | ssA(n8,n9) = n4 | ssA(n9,n9) = n4 )). fof(ax176,axiom, ( ssA(n1,n9) = n5 | ssA(n2,n9) = n5 | ssA(n3,n9) = n5 | ssA(n4,n9) = n5 | ssA(n5,n9) = n5 | ssA(n6,n9) = n5 | ssA(n7,n9) = n5 | ssA(n8,n9) = n5 | ssA(n9,n9) = n5 )). fof(ax177,axiom, ( ssA(n1,n9) = n6 | ssA(n2,n9) = n6 | ssA(n3,n9) = n6 | ssA(n4,n9) = n6 | ssA(n5,n9) = n6 | ssA(n6,n9) = n6 | ssA(n7,n9) = n6 | ssA(n8,n9) = n6 | ssA(n9,n9) = n6 )). fof(ax178,axiom, ( ssA(n1,n9) = n7 | ssA(n2,n9) = n7 | ssA(n3,n9) = n7 | ssA(n4,n9) = n7 | ssA(n5,n9) = n7 | ssA(n6,n9) = n7 | ssA(n7,n9) = n7 | ssA(n8,n9) = n7 | ssA(n9,n9) = n7 )). fof(ax179,axiom, ( ssA(n1,n9) = n8 | ssA(n2,n9) = n8 | ssA(n3,n9) = n8 | ssA(n4,n9) = n8 | ssA(n5,n9) = n8 | ssA(n6,n9) = n8 | ssA(n7,n9) = n8 | ssA(n8,n9) = n8 | ssA(n9,n9) = n8 )). fof(ax180,axiom, ( ssA(n1,n9) = n9 | ssA(n2,n9) = n9 | ssA(n3,n9) = n9 | ssA(n4,n9) = n9 | ssA(n5,n9) = n9 | ssA(n6,n9) = n9 | ssA(n7,n9) = n9 | ssA(n8,n9) = n9 | ssA(n9,n9) = n9 )). fof(ax181,axiom, ( ssA(n1,n9) != ssA(n2,n9) & ssA(n1,n9) != ssA(n3,n9) & ssA(n1,n9) != ssA(n4,n9) & ssA(n1,n9) != ssA(n5,n9) & ssA(n1,n9) != ssA(n6,n9) & ssA(n1,n9) != ssA(n7,n9) & ssA(n1,n9) != ssA(n8,n9) & ssA(n1,n9) != ssA(n9,n9) & ssA(n2,n9) != ssA(n3,n9) & ssA(n2,n9) != ssA(n4,n9) & ssA(n2,n9) != ssA(n5,n9) & ssA(n2,n9) != ssA(n6,n9) & ssA(n2,n9) != ssA(n7,n9) & ssA(n2,n9) != ssA(n8,n9) & ssA(n2,n9) != ssA(n9,n9) & ssA(n3,n9) != ssA(n4,n9) & ssA(n3,n9) != ssA(n5,n9) & ssA(n3,n9) != ssA(n6,n9) & ssA(n3,n9) != ssA(n7,n9) & ssA(n3,n9) != ssA(n8,n9) & ssA(n3,n9) != ssA(n9,n9) & ssA(n4,n9) != ssA(n5,n9) & ssA(n4,n9) != ssA(n6,n9) & ssA(n4,n9) != ssA(n7,n9) & ssA(n4,n9) != ssA(n8,n9) & ssA(n4,n9) != ssA(n9,n9) & ssA(n5,n9) != ssA(n6,n9) & ssA(n5,n9) != ssA(n7,n9) & ssA(n5,n9) != ssA(n8,n9) & ssA(n5,n9) != ssA(n9,n9) & ssA(n6,n9) != ssA(n7,n9) & ssA(n6,n9) != ssA(n8,n9) & ssA(n6,n9) != ssA(n9,n9) & ssA(n7,n9) != ssA(n8,n9) & ssA(n7,n9) != ssA(n9,n9) & ssA(n8,n9) != ssA(n9,n9) )). %----Subsquare constraints fof(ax182,axiom, ( ssA(n1,n1) = n1 | ssA(n1,n2) = n1 | ssA(n1,n3) = n1 | ssA(n2,n1) = n1 | ssA(n2,n2) = n1 | ssA(n2,n3) = n1 | ssA(n3,n1) = n1 | ssA(n3,n2) = n1 | ssA(n3,n3) = n1 )). fof(ax183,axiom, ( ssA(n1,n1) = n2 | ssA(n1,n2) = n2 | ssA(n1,n3) = n2 | ssA(n2,n1) = n2 | ssA(n2,n2) = n2 | ssA(n2,n3) = n2 | ssA(n3,n1) = n2 | ssA(n3,n2) = n2 | ssA(n3,n3) = n2 )). fof(ax184,axiom, ( ssA(n1,n1) = n3 | ssA(n1,n2) = n3 | ssA(n1,n3) = n3 | ssA(n2,n1) = n3 | ssA(n2,n2) = n3 | ssA(n2,n3) = n3 | ssA(n3,n1) = n3 | ssA(n3,n2) = n3 | ssA(n3,n3) = n3 )). fof(ax185,axiom, ( ssA(n1,n1) = n4 | ssA(n1,n2) = n4 | ssA(n1,n3) = n4 | ssA(n2,n1) = n4 | ssA(n2,n2) = n4 | ssA(n2,n3) = n4 | ssA(n3,n1) = n4 | ssA(n3,n2) = n4 | ssA(n3,n3) = n4 )). fof(ax186,axiom, ( ssA(n1,n1) = n5 | ssA(n1,n2) = n5 | ssA(n1,n3) = n5 | ssA(n2,n1) = n5 | ssA(n2,n2) = n5 | ssA(n2,n3) = n5 | ssA(n3,n1) = n5 | ssA(n3,n2) = n5 | ssA(n3,n3) = n5 )). fof(ax187,axiom, ( ssA(n1,n1) = n6 | ssA(n1,n2) = n6 | ssA(n1,n3) = n6 | ssA(n2,n1) = n6 | ssA(n2,n2) = n6 | ssA(n2,n3) = n6 | ssA(n3,n1) = n6 | ssA(n3,n2) = n6 | ssA(n3,n3) = n6 )). fof(ax188,axiom, ( ssA(n1,n1) = n7 | ssA(n1,n2) = n7 | ssA(n1,n3) = n7 | ssA(n2,n1) = n7 | ssA(n2,n2) = n7 | ssA(n2,n3) = n7 | ssA(n3,n1) = n7 | ssA(n3,n2) = n7 | ssA(n3,n3) = n7 )). fof(ax189,axiom, ( ssA(n1,n1) = n8 | ssA(n1,n2) = n8 | ssA(n1,n3) = n8 | ssA(n2,n1) = n8 | ssA(n2,n2) = n8 | ssA(n2,n3) = n8 | ssA(n3,n1) = n8 | ssA(n3,n2) = n8 | ssA(n3,n3) = n8 )). fof(ax190,axiom, ( ssA(n1,n1) = n9 | ssA(n1,n2) = n9 | ssA(n1,n3) = n9 | ssA(n2,n1) = n9 | ssA(n2,n2) = n9 | ssA(n2,n3) = n9 | ssA(n3,n1) = n9 | ssA(n3,n2) = n9 | ssA(n3,n3) = n9 )). fof(ax191,axiom, ( ssA(n1,n1) != ssA(n1,n2) & ssA(n1,n1) != ssA(n1,n3) & ssA(n1,n1) != ssA(n2,n1) & ssA(n1,n1) != ssA(n2,n2) & ssA(n1,n1) != ssA(n2,n3) & ssA(n1,n1) != ssA(n3,n1) & ssA(n1,n1) != ssA(n3,n2) & ssA(n1,n1) != ssA(n3,n3) & ssA(n1,n2) != ssA(n1,n3) & ssA(n1,n2) != ssA(n2,n1) & ssA(n1,n2) != ssA(n2,n2) & ssA(n1,n2) != ssA(n2,n3) & ssA(n1,n2) != ssA(n3,n1) & ssA(n1,n2) != ssA(n3,n2) & ssA(n1,n2) != ssA(n3,n3) & ssA(n1,n3) != ssA(n2,n1) & ssA(n1,n3) != ssA(n2,n2) & ssA(n1,n3) != ssA(n2,n3) & ssA(n1,n3) != ssA(n3,n1) & ssA(n1,n3) != ssA(n3,n2) & ssA(n1,n3) != ssA(n3,n3) & ssA(n2,n1) != ssA(n2,n2) & ssA(n2,n1) != ssA(n2,n3) & ssA(n2,n1) != ssA(n3,n1) & ssA(n2,n1) != ssA(n3,n2) & ssA(n2,n1) != ssA(n3,n3) & ssA(n2,n2) != ssA(n2,n3) & ssA(n2,n2) != ssA(n3,n1) & ssA(n2,n2) != ssA(n3,n2) & ssA(n2,n2) != ssA(n3,n3) & ssA(n2,n3) != ssA(n3,n1) & ssA(n2,n3) != ssA(n3,n2) & ssA(n2,n3) != ssA(n3,n3) & ssA(n3,n1) != ssA(n3,n2) & ssA(n3,n1) != ssA(n3,n3) & ssA(n3,n2) != ssA(n3,n3) )). fof(ax192,axiom, ( ssA(n1,n4) = n1 | ssA(n1,n5) = n1 | ssA(n1,n6) = n1 | ssA(n2,n4) = n1 | ssA(n2,n5) = n1 | ssA(n2,n6) = n1 | ssA(n3,n4) = n1 | ssA(n3,n5) = n1 | ssA(n3,n6) = n1 )). fof(ax193,axiom, ( ssA(n1,n4) = n2 | ssA(n1,n5) = n2 | ssA(n1,n6) = n2 | ssA(n2,n4) = n2 | ssA(n2,n5) = n2 | ssA(n2,n6) = n2 | ssA(n3,n4) = n2 | ssA(n3,n5) = n2 | ssA(n3,n6) = n2 )). fof(ax194,axiom, ( ssA(n1,n4) = n3 | ssA(n1,n5) = n3 | ssA(n1,n6) = n3 | ssA(n2,n4) = n3 | ssA(n2,n5) = n3 | ssA(n2,n6) = n3 | ssA(n3,n4) = n3 | ssA(n3,n5) = n3 | ssA(n3,n6) = n3 )). fof(ax195,axiom, ( ssA(n1,n4) = n4 | ssA(n1,n5) = n4 | ssA(n1,n6) = n4 | ssA(n2,n4) = n4 | ssA(n2,n5) = n4 | ssA(n2,n6) = n4 | ssA(n3,n4) = n4 | ssA(n3,n5) = n4 | ssA(n3,n6) = n4 )). fof(ax196,axiom, ( ssA(n1,n4) = n5 | ssA(n1,n5) = n5 | ssA(n1,n6) = n5 | ssA(n2,n4) = n5 | ssA(n2,n5) = n5 | ssA(n2,n6) = n5 | ssA(n3,n4) = n5 | ssA(n3,n5) = n5 | ssA(n3,n6) = n5 )). fof(ax197,axiom, ( ssA(n1,n4) = n6 | ssA(n1,n5) = n6 | ssA(n1,n6) = n6 | ssA(n2,n4) = n6 | ssA(n2,n5) = n6 | ssA(n2,n6) = n6 | ssA(n3,n4) = n6 | ssA(n3,n5) = n6 | ssA(n3,n6) = n6 )). fof(ax198,axiom, ( ssA(n1,n4) = n7 | ssA(n1,n5) = n7 | ssA(n1,n6) = n7 | ssA(n2,n4) = n7 | ssA(n2,n5) = n7 | ssA(n2,n6) = n7 | ssA(n3,n4) = n7 | ssA(n3,n5) = n7 | ssA(n3,n6) = n7 )). fof(ax199,axiom, ( ssA(n1,n4) = n8 | ssA(n1,n5) = n8 | ssA(n1,n6) = n8 | ssA(n2,n4) = n8 | ssA(n2,n5) = n8 | ssA(n2,n6) = n8 | ssA(n3,n4) = n8 | ssA(n3,n5) = n8 | ssA(n3,n6) = n8 )). fof(ax200,axiom, ( ssA(n1,n4) = n9 | ssA(n1,n5) = n9 | ssA(n1,n6) = n9 | ssA(n2,n4) = n9 | ssA(n2,n5) = n9 | ssA(n2,n6) = n9 | ssA(n3,n4) = n9 | ssA(n3,n5) = n9 | ssA(n3,n6) = n9 )). fof(ax201,axiom, ( ssA(n1,n4) != ssA(n1,n5) & ssA(n1,n4) != ssA(n1,n6) & ssA(n1,n4) != ssA(n2,n4) & ssA(n1,n4) != ssA(n2,n5) & ssA(n1,n4) != ssA(n2,n6) & ssA(n1,n4) != ssA(n3,n4) & ssA(n1,n4) != ssA(n3,n5) & ssA(n1,n4) != ssA(n3,n6) & ssA(n1,n5) != ssA(n1,n6) & ssA(n1,n5) != ssA(n2,n4) & ssA(n1,n5) != ssA(n2,n5) & ssA(n1,n5) != ssA(n2,n6) & ssA(n1,n5) != ssA(n3,n4) & ssA(n1,n5) != ssA(n3,n5) & ssA(n1,n5) != ssA(n3,n6) & ssA(n1,n6) != ssA(n2,n4) & ssA(n1,n6) != ssA(n2,n5) & ssA(n1,n6) != ssA(n2,n6) & ssA(n1,n6) != ssA(n3,n4) & ssA(n1,n6) != ssA(n3,n5) & ssA(n1,n6) != ssA(n3,n6) & ssA(n2,n4) != ssA(n2,n5) & ssA(n2,n4) != ssA(n2,n6) & ssA(n2,n4) != ssA(n3,n4) & ssA(n2,n4) != ssA(n3,n5) & ssA(n2,n4) != ssA(n3,n6) & ssA(n2,n5) != ssA(n2,n6) & ssA(n2,n5) != ssA(n3,n4) & ssA(n2,n5) != ssA(n3,n5) & ssA(n2,n5) != ssA(n3,n6) & ssA(n2,n6) != ssA(n3,n4) & ssA(n2,n6) != ssA(n3,n5) & ssA(n2,n6) != ssA(n3,n6) & ssA(n3,n4) != ssA(n3,n5) & ssA(n3,n4) != ssA(n3,n6) & ssA(n3,n5) != ssA(n3,n6) )). fof(ax202,axiom, ( ssA(n1,n7) = n1 | ssA(n1,n8) = n1 | ssA(n1,n9) = n1 | ssA(n2,n7) = n1 | ssA(n2,n8) = n1 | ssA(n2,n9) = n1 | ssA(n3,n7) = n1 | ssA(n3,n8) = n1 | ssA(n3,n9) = n1 )). fof(ax203,axiom, ( ssA(n1,n7) = n2 | ssA(n1,n8) = n2 | ssA(n1,n9) = n2 | ssA(n2,n7) = n2 | ssA(n2,n8) = n2 | ssA(n2,n9) = n2 | ssA(n3,n7) = n2 | ssA(n3,n8) = n2 | ssA(n3,n9) = n2 )). fof(ax204,axiom, ( ssA(n1,n7) = n3 | ssA(n1,n8) = n3 | ssA(n1,n9) = n3 | ssA(n2,n7) = n3 | ssA(n2,n8) = n3 | ssA(n2,n9) = n3 | ssA(n3,n7) = n3 | ssA(n3,n8) = n3 | ssA(n3,n9) = n3 )). fof(ax205,axiom, ( ssA(n1,n7) = n4 | ssA(n1,n8) = n4 | ssA(n1,n9) = n4 | ssA(n2,n7) = n4 | ssA(n2,n8) = n4 | ssA(n2,n9) = n4 | ssA(n3,n7) = n4 | ssA(n3,n8) = n4 | ssA(n3,n9) = n4 )). fof(ax206,axiom, ( ssA(n1,n7) = n5 | ssA(n1,n8) = n5 | ssA(n1,n9) = n5 | ssA(n2,n7) = n5 | ssA(n2,n8) = n5 | ssA(n2,n9) = n5 | ssA(n3,n7) = n5 | ssA(n3,n8) = n5 | ssA(n3,n9) = n5 )). fof(ax207,axiom, ( ssA(n1,n7) = n6 | ssA(n1,n8) = n6 | ssA(n1,n9) = n6 | ssA(n2,n7) = n6 | ssA(n2,n8) = n6 | ssA(n2,n9) = n6 | ssA(n3,n7) = n6 | ssA(n3,n8) = n6 | ssA(n3,n9) = n6 )). fof(ax208,axiom, ( ssA(n1,n7) = n7 | ssA(n1,n8) = n7 | ssA(n1,n9) = n7 | ssA(n2,n7) = n7 | ssA(n2,n8) = n7 | ssA(n2,n9) = n7 | ssA(n3,n7) = n7 | ssA(n3,n8) = n7 | ssA(n3,n9) = n7 )). fof(ax209,axiom, ( ssA(n1,n7) = n8 | ssA(n1,n8) = n8 | ssA(n1,n9) = n8 | ssA(n2,n7) = n8 | ssA(n2,n8) = n8 | ssA(n2,n9) = n8 | ssA(n3,n7) = n8 | ssA(n3,n8) = n8 | ssA(n3,n9) = n8 )). fof(ax210,axiom, ( ssA(n1,n7) = n9 | ssA(n1,n8) = n9 | ssA(n1,n9) = n9 | ssA(n2,n7) = n9 | ssA(n2,n8) = n9 | ssA(n2,n9) = n9 | ssA(n3,n7) = n9 | ssA(n3,n8) = n9 | ssA(n3,n9) = n9 )). fof(ax211,axiom, ( ssA(n1,n7) != ssA(n1,n8) & ssA(n1,n7) != ssA(n1,n9) & ssA(n1,n7) != ssA(n2,n7) & ssA(n1,n7) != ssA(n2,n8) & ssA(n1,n7) != ssA(n2,n9) & ssA(n1,n7) != ssA(n3,n7) & ssA(n1,n7) != ssA(n3,n8) & ssA(n1,n7) != ssA(n3,n9) & ssA(n1,n8) != ssA(n1,n9) & ssA(n1,n8) != ssA(n2,n7) & ssA(n1,n8) != ssA(n2,n8) & ssA(n1,n8) != ssA(n2,n9) & ssA(n1,n8) != ssA(n3,n7) & ssA(n1,n8) != ssA(n3,n8) & ssA(n1,n8) != ssA(n3,n9) & ssA(n1,n9) != ssA(n2,n7) & ssA(n1,n9) != ssA(n2,n8) & ssA(n1,n9) != ssA(n2,n9) & ssA(n1,n9) != ssA(n3,n7) & ssA(n1,n9) != ssA(n3,n8) & ssA(n1,n9) != ssA(n3,n9) & ssA(n2,n7) != ssA(n2,n8) & ssA(n2,n7) != ssA(n2,n9) & ssA(n2,n7) != ssA(n3,n7) & ssA(n2,n7) != ssA(n3,n8) & ssA(n2,n7) != ssA(n3,n9) & ssA(n2,n8) != ssA(n2,n9) & ssA(n2,n8) != ssA(n3,n7) & ssA(n2,n8) != ssA(n3,n8) & ssA(n2,n8) != ssA(n3,n9) & ssA(n2,n9) != ssA(n3,n7) & ssA(n2,n9) != ssA(n3,n8) & ssA(n2,n9) != ssA(n3,n9) & ssA(n3,n7) != ssA(n3,n8) & ssA(n3,n7) != ssA(n3,n9) & ssA(n3,n8) != ssA(n3,n9) )). fof(ax212,axiom, ( ssA(n4,n1) = n1 | ssA(n4,n2) = n1 | ssA(n4,n3) = n1 | ssA(n5,n1) = n1 | ssA(n5,n2) = n1 | ssA(n5,n3) = n1 | ssA(n6,n1) = n1 | ssA(n6,n2) = n1 | ssA(n6,n3) = n1 )). fof(ax213,axiom, ( ssA(n4,n1) = n2 | ssA(n4,n2) = n2 | ssA(n4,n3) = n2 | ssA(n5,n1) = n2 | ssA(n5,n2) = n2 | ssA(n5,n3) = n2 | ssA(n6,n1) = n2 | ssA(n6,n2) = n2 | ssA(n6,n3) = n2 )). fof(ax214,axiom, ( ssA(n4,n1) = n3 | ssA(n4,n2) = n3 | ssA(n4,n3) = n3 | ssA(n5,n1) = n3 | ssA(n5,n2) = n3 | ssA(n5,n3) = n3 | ssA(n6,n1) = n3 | ssA(n6,n2) = n3 | ssA(n6,n3) = n3 )). fof(ax215,axiom, ( ssA(n4,n1) = n4 | ssA(n4,n2) = n4 | ssA(n4,n3) = n4 | ssA(n5,n1) = n4 | ssA(n5,n2) = n4 | ssA(n5,n3) = n4 | ssA(n6,n1) = n4 | ssA(n6,n2) = n4 | ssA(n6,n3) = n4 )). fof(ax216,axiom, ( ssA(n4,n1) = n5 | ssA(n4,n2) = n5 | ssA(n4,n3) = n5 | ssA(n5,n1) = n5 | ssA(n5,n2) = n5 | ssA(n5,n3) = n5 | ssA(n6,n1) = n5 | ssA(n6,n2) = n5 | ssA(n6,n3) = n5 )). fof(ax217,axiom, ( ssA(n4,n1) = n6 | ssA(n4,n2) = n6 | ssA(n4,n3) = n6 | ssA(n5,n1) = n6 | ssA(n5,n2) = n6 | ssA(n5,n3) = n6 | ssA(n6,n1) = n6 | ssA(n6,n2) = n6 | ssA(n6,n3) = n6 )). fof(ax218,axiom, ( ssA(n4,n1) = n7 | ssA(n4,n2) = n7 | ssA(n4,n3) = n7 | ssA(n5,n1) = n7 | ssA(n5,n2) = n7 | ssA(n5,n3) = n7 | ssA(n6,n1) = n7 | ssA(n6,n2) = n7 | ssA(n6,n3) = n7 )). fof(ax219,axiom, ( ssA(n4,n1) = n8 | ssA(n4,n2) = n8 | ssA(n4,n3) = n8 | ssA(n5,n1) = n8 | ssA(n5,n2) = n8 | ssA(n5,n3) = n8 | ssA(n6,n1) = n8 | ssA(n6,n2) = n8 | ssA(n6,n3) = n8 )). fof(ax220,axiom, ( ssA(n4,n1) = n9 | ssA(n4,n2) = n9 | ssA(n4,n3) = n9 | ssA(n5,n1) = n9 | ssA(n5,n2) = n9 | ssA(n5,n3) = n9 | ssA(n6,n1) = n9 | ssA(n6,n2) = n9 | ssA(n6,n3) = n9 )). fof(ax221,axiom, ( ssA(n4,n1) != ssA(n4,n2) & ssA(n4,n1) != ssA(n4,n3) & ssA(n4,n1) != ssA(n5,n1) & ssA(n4,n1) != ssA(n5,n2) & ssA(n4,n1) != ssA(n5,n3) & ssA(n4,n1) != ssA(n6,n1) & ssA(n4,n1) != ssA(n6,n2) & ssA(n4,n1) != ssA(n6,n3) & ssA(n4,n2) != ssA(n4,n3) & ssA(n4,n2) != ssA(n5,n1) & ssA(n4,n2) != ssA(n5,n2) & ssA(n4,n2) != ssA(n5,n3) & ssA(n4,n2) != ssA(n6,n1) & ssA(n4,n2) != ssA(n6,n2) & ssA(n4,n2) != ssA(n6,n3) & ssA(n4,n3) != ssA(n5,n1) & ssA(n4,n3) != ssA(n5,n2) & ssA(n4,n3) != ssA(n5,n3) & ssA(n4,n3) != ssA(n6,n1) & ssA(n4,n3) != ssA(n6,n2) & ssA(n4,n3) != ssA(n6,n3) & ssA(n5,n1) != ssA(n5,n2) & ssA(n5,n1) != ssA(n5,n3) & ssA(n5,n1) != ssA(n6,n1) & ssA(n5,n1) != ssA(n6,n2) & ssA(n5,n1) != ssA(n6,n3) & ssA(n5,n2) != ssA(n5,n3) & ssA(n5,n2) != ssA(n6,n1) & ssA(n5,n2) != ssA(n6,n2) & ssA(n5,n2) != ssA(n6,n3) & ssA(n5,n3) != ssA(n6,n1) & ssA(n5,n3) != ssA(n6,n2) & ssA(n5,n3) != ssA(n6,n3) & ssA(n6,n1) != ssA(n6,n2) & ssA(n6,n1) != ssA(n6,n3) & ssA(n6,n2) != ssA(n6,n3) )). fof(ax222,axiom, ( ssA(n4,n4) = n1 | ssA(n4,n5) = n1 | ssA(n4,n6) = n1 | ssA(n5,n4) = n1 | ssA(n5,n5) = n1 | ssA(n5,n6) = n1 | ssA(n6,n4) = n1 | ssA(n6,n5) = n1 | ssA(n6,n6) = n1 )). fof(ax223,axiom, ( ssA(n4,n4) = n2 | ssA(n4,n5) = n2 | ssA(n4,n6) = n2 | ssA(n5,n4) = n2 | ssA(n5,n5) = n2 | ssA(n5,n6) = n2 | ssA(n6,n4) = n2 | ssA(n6,n5) = n2 | ssA(n6,n6) = n2 )). fof(ax224,axiom, ( ssA(n4,n4) = n3 | ssA(n4,n5) = n3 | ssA(n4,n6) = n3 | ssA(n5,n4) = n3 | ssA(n5,n5) = n3 | ssA(n5,n6) = n3 | ssA(n6,n4) = n3 | ssA(n6,n5) = n3 | ssA(n6,n6) = n3 )). fof(ax225,axiom, ( ssA(n4,n4) = n4 | ssA(n4,n5) = n4 | ssA(n4,n6) = n4 | ssA(n5,n4) = n4 | ssA(n5,n5) = n4 | ssA(n5,n6) = n4 | ssA(n6,n4) = n4 | ssA(n6,n5) = n4 | ssA(n6,n6) = n4 )). fof(ax226,axiom, ( ssA(n4,n4) = n5 | ssA(n4,n5) = n5 | ssA(n4,n6) = n5 | ssA(n5,n4) = n5 | ssA(n5,n5) = n5 | ssA(n5,n6) = n5 | ssA(n6,n4) = n5 | ssA(n6,n5) = n5 | ssA(n6,n6) = n5 )). fof(ax227,axiom, ( ssA(n4,n4) = n6 | ssA(n4,n5) = n6 | ssA(n4,n6) = n6 | ssA(n5,n4) = n6 | ssA(n5,n5) = n6 | ssA(n5,n6) = n6 | ssA(n6,n4) = n6 | ssA(n6,n5) = n6 | ssA(n6,n6) = n6 )). fof(ax228,axiom, ( ssA(n4,n4) = n7 | ssA(n4,n5) = n7 | ssA(n4,n6) = n7 | ssA(n5,n4) = n7 | ssA(n5,n5) = n7 | ssA(n5,n6) = n7 | ssA(n6,n4) = n7 | ssA(n6,n5) = n7 | ssA(n6,n6) = n7 )). fof(ax229,axiom, ( ssA(n4,n4) = n8 | ssA(n4,n5) = n8 | ssA(n4,n6) = n8 | ssA(n5,n4) = n8 | ssA(n5,n5) = n8 | ssA(n5,n6) = n8 | ssA(n6,n4) = n8 | ssA(n6,n5) = n8 | ssA(n6,n6) = n8 )). fof(ax230,axiom, ( ssA(n4,n4) = n9 | ssA(n4,n5) = n9 | ssA(n4,n6) = n9 | ssA(n5,n4) = n9 | ssA(n5,n5) = n9 | ssA(n5,n6) = n9 | ssA(n6,n4) = n9 | ssA(n6,n5) = n9 | ssA(n6,n6) = n9 )). fof(ax231,axiom, ( ssA(n4,n4) != ssA(n4,n5) & ssA(n4,n4) != ssA(n4,n6) & ssA(n4,n4) != ssA(n5,n4) & ssA(n4,n4) != ssA(n5,n5) & ssA(n4,n4) != ssA(n5,n6) & ssA(n4,n4) != ssA(n6,n4) & ssA(n4,n4) != ssA(n6,n5) & ssA(n4,n4) != ssA(n6,n6) & ssA(n4,n5) != ssA(n4,n6) & ssA(n4,n5) != ssA(n5,n4) & ssA(n4,n5) != ssA(n5,n5) & ssA(n4,n5) != ssA(n5,n6) & ssA(n4,n5) != ssA(n6,n4) & ssA(n4,n5) != ssA(n6,n5) & ssA(n4,n5) != ssA(n6,n6) & ssA(n4,n6) != ssA(n5,n4) & ssA(n4,n6) != ssA(n5,n5) & ssA(n4,n6) != ssA(n5,n6) & ssA(n4,n6) != ssA(n6,n4) & ssA(n4,n6) != ssA(n6,n5) & ssA(n4,n6) != ssA(n6,n6) & ssA(n5,n4) != ssA(n5,n5) & ssA(n5,n4) != ssA(n5,n6) & ssA(n5,n4) != ssA(n6,n4) & ssA(n5,n4) != ssA(n6,n5) & ssA(n5,n4) != ssA(n6,n6) & ssA(n5,n5) != ssA(n5,n6) & ssA(n5,n5) != ssA(n6,n4) & ssA(n5,n5) != ssA(n6,n5) & ssA(n5,n5) != ssA(n6,n6) & ssA(n5,n6) != ssA(n6,n4) & ssA(n5,n6) != ssA(n6,n5) & ssA(n5,n6) != ssA(n6,n6) & ssA(n6,n4) != ssA(n6,n5) & ssA(n6,n4) != ssA(n6,n6) & ssA(n6,n5) != ssA(n6,n6) )). fof(ax232,axiom, ( ssA(n4,n7) = n1 | ssA(n4,n8) = n1 | ssA(n4,n9) = n1 | ssA(n5,n7) = n1 | ssA(n5,n8) = n1 | ssA(n5,n9) = n1 | ssA(n6,n7) = n1 | ssA(n6,n8) = n1 | ssA(n6,n9) = n1 )). fof(ax233,axiom, ( ssA(n4,n7) = n2 | ssA(n4,n8) = n2 | ssA(n4,n9) = n2 | ssA(n5,n7) = n2 | ssA(n5,n8) = n2 | ssA(n5,n9) = n2 | ssA(n6,n7) = n2 | ssA(n6,n8) = n2 | ssA(n6,n9) = n2 )). fof(ax234,axiom, ( ssA(n4,n7) = n3 | ssA(n4,n8) = n3 | ssA(n4,n9) = n3 | ssA(n5,n7) = n3 | ssA(n5,n8) = n3 | ssA(n5,n9) = n3 | ssA(n6,n7) = n3 | ssA(n6,n8) = n3 | ssA(n6,n9) = n3 )). fof(ax235,axiom, ( ssA(n4,n7) = n4 | ssA(n4,n8) = n4 | ssA(n4,n9) = n4 | ssA(n5,n7) = n4 | ssA(n5,n8) = n4 | ssA(n5,n9) = n4 | ssA(n6,n7) = n4 | ssA(n6,n8) = n4 | ssA(n6,n9) = n4 )). fof(ax236,axiom, ( ssA(n4,n7) = n5 | ssA(n4,n8) = n5 | ssA(n4,n9) = n5 | ssA(n5,n7) = n5 | ssA(n5,n8) = n5 | ssA(n5,n9) = n5 | ssA(n6,n7) = n5 | ssA(n6,n8) = n5 | ssA(n6,n9) = n5 )). fof(ax237,axiom, ( ssA(n4,n7) = n6 | ssA(n4,n8) = n6 | ssA(n4,n9) = n6 | ssA(n5,n7) = n6 | ssA(n5,n8) = n6 | ssA(n5,n9) = n6 | ssA(n6,n7) = n6 | ssA(n6,n8) = n6 | ssA(n6,n9) = n6 )). fof(ax238,axiom, ( ssA(n4,n7) = n7 | ssA(n4,n8) = n7 | ssA(n4,n9) = n7 | ssA(n5,n7) = n7 | ssA(n5,n8) = n7 | ssA(n5,n9) = n7 | ssA(n6,n7) = n7 | ssA(n6,n8) = n7 | ssA(n6,n9) = n7 )). fof(ax239,axiom, ( ssA(n4,n7) = n8 | ssA(n4,n8) = n8 | ssA(n4,n9) = n8 | ssA(n5,n7) = n8 | ssA(n5,n8) = n8 | ssA(n5,n9) = n8 | ssA(n6,n7) = n8 | ssA(n6,n8) = n8 | ssA(n6,n9) = n8 )). fof(ax240,axiom, ( ssA(n4,n7) = n9 | ssA(n4,n8) = n9 | ssA(n4,n9) = n9 | ssA(n5,n7) = n9 | ssA(n5,n8) = n9 | ssA(n5,n9) = n9 | ssA(n6,n7) = n9 | ssA(n6,n8) = n9 | ssA(n6,n9) = n9 )). fof(ax241,axiom, ( ssA(n4,n7) != ssA(n4,n8) & ssA(n4,n7) != ssA(n4,n9) & ssA(n4,n7) != ssA(n5,n7) & ssA(n4,n7) != ssA(n5,n8) & ssA(n4,n7) != ssA(n5,n9) & ssA(n4,n7) != ssA(n6,n7) & ssA(n4,n7) != ssA(n6,n8) & ssA(n4,n7) != ssA(n6,n9) & ssA(n4,n8) != ssA(n4,n9) & ssA(n4,n8) != ssA(n5,n7) & ssA(n4,n8) != ssA(n5,n8) & ssA(n4,n8) != ssA(n5,n9) & ssA(n4,n8) != ssA(n6,n7) & ssA(n4,n8) != ssA(n6,n8) & ssA(n4,n8) != ssA(n6,n9) & ssA(n4,n9) != ssA(n5,n7) & ssA(n4,n9) != ssA(n5,n8) & ssA(n4,n9) != ssA(n5,n9) & ssA(n4,n9) != ssA(n6,n7) & ssA(n4,n9) != ssA(n6,n8) & ssA(n4,n9) != ssA(n6,n9) & ssA(n5,n7) != ssA(n5,n8) & ssA(n5,n7) != ssA(n5,n9) & ssA(n5,n7) != ssA(n6,n7) & ssA(n5,n7) != ssA(n6,n8) & ssA(n5,n7) != ssA(n6,n9) & ssA(n5,n8) != ssA(n5,n9) & ssA(n5,n8) != ssA(n6,n7) & ssA(n5,n8) != ssA(n6,n8) & ssA(n5,n8) != ssA(n6,n9) & ssA(n5,n9) != ssA(n6,n7) & ssA(n5,n9) != ssA(n6,n8) & ssA(n5,n9) != ssA(n6,n9) & ssA(n6,n7) != ssA(n6,n8) & ssA(n6,n7) != ssA(n6,n9) & ssA(n6,n8) != ssA(n6,n9) )). fof(ax242,axiom, ( ssA(n7,n1) = n1 | ssA(n7,n2) = n1 | ssA(n7,n3) = n1 | ssA(n8,n1) = n1 | ssA(n8,n2) = n1 | ssA(n8,n3) = n1 | ssA(n9,n1) = n1 | ssA(n9,n2) = n1 | ssA(n9,n3) = n1 )). fof(ax243,axiom, ( ssA(n7,n1) = n2 | ssA(n7,n2) = n2 | ssA(n7,n3) = n2 | ssA(n8,n1) = n2 | ssA(n8,n2) = n2 | ssA(n8,n3) = n2 | ssA(n9,n1) = n2 | ssA(n9,n2) = n2 | ssA(n9,n3) = n2 )). fof(ax244,axiom, ( ssA(n7,n1) = n3 | ssA(n7,n2) = n3 | ssA(n7,n3) = n3 | ssA(n8,n1) = n3 | ssA(n8,n2) = n3 | ssA(n8,n3) = n3 | ssA(n9,n1) = n3 | ssA(n9,n2) = n3 | ssA(n9,n3) = n3 )). fof(ax245,axiom, ( ssA(n7,n1) = n4 | ssA(n7,n2) = n4 | ssA(n7,n3) = n4 | ssA(n8,n1) = n4 | ssA(n8,n2) = n4 | ssA(n8,n3) = n4 | ssA(n9,n1) = n4 | ssA(n9,n2) = n4 | ssA(n9,n3) = n4 )). fof(ax246,axiom, ( ssA(n7,n1) = n5 | ssA(n7,n2) = n5 | ssA(n7,n3) = n5 | ssA(n8,n1) = n5 | ssA(n8,n2) = n5 | ssA(n8,n3) = n5 | ssA(n9,n1) = n5 | ssA(n9,n2) = n5 | ssA(n9,n3) = n5 )). fof(ax247,axiom, ( ssA(n7,n1) = n6 | ssA(n7,n2) = n6 | ssA(n7,n3) = n6 | ssA(n8,n1) = n6 | ssA(n8,n2) = n6 | ssA(n8,n3) = n6 | ssA(n9,n1) = n6 | ssA(n9,n2) = n6 | ssA(n9,n3) = n6 )). fof(ax248,axiom, ( ssA(n7,n1) = n7 | ssA(n7,n2) = n7 | ssA(n7,n3) = n7 | ssA(n8,n1) = n7 | ssA(n8,n2) = n7 | ssA(n8,n3) = n7 | ssA(n9,n1) = n7 | ssA(n9,n2) = n7 | ssA(n9,n3) = n7 )). fof(ax249,axiom, ( ssA(n7,n1) = n8 | ssA(n7,n2) = n8 | ssA(n7,n3) = n8 | ssA(n8,n1) = n8 | ssA(n8,n2) = n8 | ssA(n8,n3) = n8 | ssA(n9,n1) = n8 | ssA(n9,n2) = n8 | ssA(n9,n3) = n8 )). fof(ax250,axiom, ( ssA(n7,n1) = n9 | ssA(n7,n2) = n9 | ssA(n7,n3) = n9 | ssA(n8,n1) = n9 | ssA(n8,n2) = n9 | ssA(n8,n3) = n9 | ssA(n9,n1) = n9 | ssA(n9,n2) = n9 | ssA(n9,n3) = n9 )). fof(ax251,axiom, ( ssA(n7,n1) != ssA(n7,n2) & ssA(n7,n1) != ssA(n7,n3) & ssA(n7,n1) != ssA(n8,n1) & ssA(n7,n1) != ssA(n8,n2) & ssA(n7,n1) != ssA(n8,n3) & ssA(n7,n1) != ssA(n9,n1) & ssA(n7,n1) != ssA(n9,n2) & ssA(n7,n1) != ssA(n9,n3) & ssA(n7,n2) != ssA(n7,n3) & ssA(n7,n2) != ssA(n8,n1) & ssA(n7,n2) != ssA(n8,n2) & ssA(n7,n2) != ssA(n8,n3) & ssA(n7,n2) != ssA(n9,n1) & ssA(n7,n2) != ssA(n9,n2) & ssA(n7,n2) != ssA(n9,n3) & ssA(n7,n3) != ssA(n8,n1) & ssA(n7,n3) != ssA(n8,n2) & ssA(n7,n3) != ssA(n8,n3) & ssA(n7,n3) != ssA(n9,n1) & ssA(n7,n3) != ssA(n9,n2) & ssA(n7,n3) != ssA(n9,n3) & ssA(n8,n1) != ssA(n8,n2) & ssA(n8,n1) != ssA(n8,n3) & ssA(n8,n1) != ssA(n9,n1) & ssA(n8,n1) != ssA(n9,n2) & ssA(n8,n1) != ssA(n9,n3) & ssA(n8,n2) != ssA(n8,n3) & ssA(n8,n2) != ssA(n9,n1) & ssA(n8,n2) != ssA(n9,n2) & ssA(n8,n2) != ssA(n9,n3) & ssA(n8,n3) != ssA(n9,n1) & ssA(n8,n3) != ssA(n9,n2) & ssA(n8,n3) != ssA(n9,n3) & ssA(n9,n1) != ssA(n9,n2) & ssA(n9,n1) != ssA(n9,n3) & ssA(n9,n2) != ssA(n9,n3) )). fof(ax252,axiom, ( ssA(n7,n4) = n1 | ssA(n7,n5) = n1 | ssA(n7,n6) = n1 | ssA(n8,n4) = n1 | ssA(n8,n5) = n1 | ssA(n8,n6) = n1 | ssA(n9,n4) = n1 | ssA(n9,n5) = n1 | ssA(n9,n6) = n1 )). fof(ax253,axiom, ( ssA(n7,n4) = n2 | ssA(n7,n5) = n2 | ssA(n7,n6) = n2 | ssA(n8,n4) = n2 | ssA(n8,n5) = n2 | ssA(n8,n6) = n2 | ssA(n9,n4) = n2 | ssA(n9,n5) = n2 | ssA(n9,n6) = n2 )). fof(ax254,axiom, ( ssA(n7,n4) = n3 | ssA(n7,n5) = n3 | ssA(n7,n6) = n3 | ssA(n8,n4) = n3 | ssA(n8,n5) = n3 | ssA(n8,n6) = n3 | ssA(n9,n4) = n3 | ssA(n9,n5) = n3 | ssA(n9,n6) = n3 )). fof(ax255,axiom, ( ssA(n7,n4) = n4 | ssA(n7,n5) = n4 | ssA(n7,n6) = n4 | ssA(n8,n4) = n4 | ssA(n8,n5) = n4 | ssA(n8,n6) = n4 | ssA(n9,n4) = n4 | ssA(n9,n5) = n4 | ssA(n9,n6) = n4 )). fof(ax256,axiom, ( ssA(n7,n4) = n5 | ssA(n7,n5) = n5 | ssA(n7,n6) = n5 | ssA(n8,n4) = n5 | ssA(n8,n5) = n5 | ssA(n8,n6) = n5 | ssA(n9,n4) = n5 | ssA(n9,n5) = n5 | ssA(n9,n6) = n5 )). fof(ax257,axiom, ( ssA(n7,n4) = n6 | ssA(n7,n5) = n6 | ssA(n7,n6) = n6 | ssA(n8,n4) = n6 | ssA(n8,n5) = n6 | ssA(n8,n6) = n6 | ssA(n9,n4) = n6 | ssA(n9,n5) = n6 | ssA(n9,n6) = n6 )). fof(ax258,axiom, ( ssA(n7,n4) = n7 | ssA(n7,n5) = n7 | ssA(n7,n6) = n7 | ssA(n8,n4) = n7 | ssA(n8,n5) = n7 | ssA(n8,n6) = n7 | ssA(n9,n4) = n7 | ssA(n9,n5) = n7 | ssA(n9,n6) = n7 )). fof(ax259,axiom, ( ssA(n7,n4) = n8 | ssA(n7,n5) = n8 | ssA(n7,n6) = n8 | ssA(n8,n4) = n8 | ssA(n8,n5) = n8 | ssA(n8,n6) = n8 | ssA(n9,n4) = n8 | ssA(n9,n5) = n8 | ssA(n9,n6) = n8 )). fof(ax260,axiom, ( ssA(n7,n4) = n9 | ssA(n7,n5) = n9 | ssA(n7,n6) = n9 | ssA(n8,n4) = n9 | ssA(n8,n5) = n9 | ssA(n8,n6) = n9 | ssA(n9,n4) = n9 | ssA(n9,n5) = n9 | ssA(n9,n6) = n9 )). fof(ax261,axiom, ( ssA(n7,n4) != ssA(n7,n5) & ssA(n7,n4) != ssA(n7,n6) & ssA(n7,n4) != ssA(n8,n4) & ssA(n7,n4) != ssA(n8,n5) & ssA(n7,n4) != ssA(n8,n6) & ssA(n7,n4) != ssA(n9,n4) & ssA(n7,n4) != ssA(n9,n5) & ssA(n7,n4) != ssA(n9,n6) & ssA(n7,n5) != ssA(n7,n6) & ssA(n7,n5) != ssA(n8,n4) & ssA(n7,n5) != ssA(n8,n5) & ssA(n7,n5) != ssA(n8,n6) & ssA(n7,n5) != ssA(n9,n4) & ssA(n7,n5) != ssA(n9,n5) & ssA(n7,n5) != ssA(n9,n6) & ssA(n7,n6) != ssA(n8,n4) & ssA(n7,n6) != ssA(n8,n5) & ssA(n7,n6) != ssA(n8,n6) & ssA(n7,n6) != ssA(n9,n4) & ssA(n7,n6) != ssA(n9,n5) & ssA(n7,n6) != ssA(n9,n6) & ssA(n8,n4) != ssA(n8,n5) & ssA(n8,n4) != ssA(n8,n6) & ssA(n8,n4) != ssA(n9,n4) & ssA(n8,n4) != ssA(n9,n5) & ssA(n8,n4) != ssA(n9,n6) & ssA(n8,n5) != ssA(n8,n6) & ssA(n8,n5) != ssA(n9,n4) & ssA(n8,n5) != ssA(n9,n5) & ssA(n8,n5) != ssA(n9,n6) & ssA(n8,n6) != ssA(n9,n4) & ssA(n8,n6) != ssA(n9,n5) & ssA(n8,n6) != ssA(n9,n6) & ssA(n9,n4) != ssA(n9,n5) & ssA(n9,n4) != ssA(n9,n6) & ssA(n9,n5) != ssA(n9,n6) )). fof(ax262,axiom, ( ssA(n7,n7) = n1 | ssA(n7,n8) = n1 | ssA(n7,n9) = n1 | ssA(n8,n7) = n1 | ssA(n8,n8) = n1 | ssA(n8,n9) = n1 | ssA(n9,n7) = n1 | ssA(n9,n8) = n1 | ssA(n9,n9) = n1 )). fof(ax263,axiom, ( ssA(n7,n7) = n2 | ssA(n7,n8) = n2 | ssA(n7,n9) = n2 | ssA(n8,n7) = n2 | ssA(n8,n8) = n2 | ssA(n8,n9) = n2 | ssA(n9,n7) = n2 | ssA(n9,n8) = n2 | ssA(n9,n9) = n2 )). fof(ax264,axiom, ( ssA(n7,n7) = n3 | ssA(n7,n8) = n3 | ssA(n7,n9) = n3 | ssA(n8,n7) = n3 | ssA(n8,n8) = n3 | ssA(n8,n9) = n3 | ssA(n9,n7) = n3 | ssA(n9,n8) = n3 | ssA(n9,n9) = n3 )). fof(ax265,axiom, ( ssA(n7,n7) = n4 | ssA(n7,n8) = n4 | ssA(n7,n9) = n4 | ssA(n8,n7) = n4 | ssA(n8,n8) = n4 | ssA(n8,n9) = n4 | ssA(n9,n7) = n4 | ssA(n9,n8) = n4 | ssA(n9,n9) = n4 )). fof(ax266,axiom, ( ssA(n7,n7) = n5 | ssA(n7,n8) = n5 | ssA(n7,n9) = n5 | ssA(n8,n7) = n5 | ssA(n8,n8) = n5 | ssA(n8,n9) = n5 | ssA(n9,n7) = n5 | ssA(n9,n8) = n5 | ssA(n9,n9) = n5 )). fof(ax267,axiom, ( ssA(n7,n7) = n6 | ssA(n7,n8) = n6 | ssA(n7,n9) = n6 | ssA(n8,n7) = n6 | ssA(n8,n8) = n6 | ssA(n8,n9) = n6 | ssA(n9,n7) = n6 | ssA(n9,n8) = n6 | ssA(n9,n9) = n6 )). fof(ax268,axiom, ( ssA(n7,n7) = n7 | ssA(n7,n8) = n7 | ssA(n7,n9) = n7 | ssA(n8,n7) = n7 | ssA(n8,n8) = n7 | ssA(n8,n9) = n7 | ssA(n9,n7) = n7 | ssA(n9,n8) = n7 | ssA(n9,n9) = n7 )). fof(ax269,axiom, ( ssA(n7,n7) = n8 | ssA(n7,n8) = n8 | ssA(n7,n9) = n8 | ssA(n8,n7) = n8 | ssA(n8,n8) = n8 | ssA(n8,n9) = n8 | ssA(n9,n7) = n8 | ssA(n9,n8) = n8 | ssA(n9,n9) = n8 )). fof(ax270,axiom, ( ssA(n7,n7) = n9 | ssA(n7,n8) = n9 | ssA(n7,n9) = n9 | ssA(n8,n7) = n9 | ssA(n8,n8) = n9 | ssA(n8,n9) = n9 | ssA(n9,n7) = n9 | ssA(n9,n8) = n9 | ssA(n9,n9) = n9 )). fof(ax271,axiom, ( ssA(n7,n7) != ssA(n7,n8) & ssA(n7,n7) != ssA(n7,n9) & ssA(n7,n7) != ssA(n8,n7) & ssA(n7,n7) != ssA(n8,n8) & ssA(n7,n7) != ssA(n8,n9) & ssA(n7,n7) != ssA(n9,n7) & ssA(n7,n7) != ssA(n9,n8) & ssA(n7,n7) != ssA(n9,n9) & ssA(n7,n8) != ssA(n7,n9) & ssA(n7,n8) != ssA(n8,n7) & ssA(n7,n8) != ssA(n8,n8) & ssA(n7,n8) != ssA(n8,n9) & ssA(n7,n8) != ssA(n9,n7) & ssA(n7,n8) != ssA(n9,n8) & ssA(n7,n8) != ssA(n9,n9) & ssA(n7,n9) != ssA(n8,n7) & ssA(n7,n9) != ssA(n8,n8) & ssA(n7,n9) != ssA(n8,n9) & ssA(n7,n9) != ssA(n9,n7) & ssA(n7,n9) != ssA(n9,n8) & ssA(n7,n9) != ssA(n9,n9) & ssA(n8,n7) != ssA(n8,n8) & ssA(n8,n7) != ssA(n8,n9) & ssA(n8,n7) != ssA(n9,n7) & ssA(n8,n7) != ssA(n9,n8) & ssA(n8,n7) != ssA(n9,n9) & ssA(n8,n8) != ssA(n8,n9) & ssA(n8,n8) != ssA(n9,n7) & ssA(n8,n8) != ssA(n9,n8) & ssA(n8,n8) != ssA(n9,n9) & ssA(n8,n9) != ssA(n9,n7) & ssA(n8,n9) != ssA(n9,n8) & ssA(n8,n9) != ssA(n9,n9) & ssA(n9,n7) != ssA(n9,n8) & ssA(n9,n7) != ssA(n9,n9) & ssA(n9,n8) != ssA(n9,n9) )). %----Codomain fof(ax272,axiom, ( ssA(n1,n1) = n1 | ssA(n1,n1) = n2 | ssA(n1,n1) = n3 | ssA(n1,n1) = n4 | ssA(n1,n1) = n5 | ssA(n1,n1) = n6 | ssA(n1,n1) = n7 | ssA(n1,n1) = n8 | ssA(n1,n1) = n9 )). fof(ax273,axiom, ( ssA(n1,n2) = n1 | ssA(n1,n2) = n2 | ssA(n1,n2) = n3 | ssA(n1,n2) = n4 | ssA(n1,n2) = n5 | ssA(n1,n2) = n6 | ssA(n1,n2) = n7 | ssA(n1,n2) = n8 | ssA(n1,n2) = n9 )). fof(ax274,axiom, ( ssA(n1,n3) = n1 | ssA(n1,n3) = n2 | ssA(n1,n3) = n3 | ssA(n1,n3) = n4 | ssA(n1,n3) = n5 | ssA(n1,n3) = n6 | ssA(n1,n3) = n7 | ssA(n1,n3) = n8 | ssA(n1,n3) = n9 )). fof(ax275,axiom, ( ssA(n1,n4) = n1 | ssA(n1,n4) = n2 | ssA(n1,n4) = n3 | ssA(n1,n4) = n4 | ssA(n1,n4) = n5 | ssA(n1,n4) = n6 | ssA(n1,n4) = n7 | ssA(n1,n4) = n8 | ssA(n1,n4) = n9 )). fof(ax276,axiom, ( ssA(n1,n5) = n1 | ssA(n1,n5) = n2 | ssA(n1,n5) = n3 | ssA(n1,n5) = n4 | ssA(n1,n5) = n5 | ssA(n1,n5) = n6 | ssA(n1,n5) = n7 | ssA(n1,n5) = n8 | ssA(n1,n5) = n9 )). fof(ax277,axiom, ( ssA(n1,n6) = n1 | ssA(n1,n6) = n2 | ssA(n1,n6) = n3 | ssA(n1,n6) = n4 | ssA(n1,n6) = n5 | ssA(n1,n6) = n6 | ssA(n1,n6) = n7 | ssA(n1,n6) = n8 | ssA(n1,n6) = n9 )). fof(ax278,axiom, ( ssA(n1,n7) = n1 | ssA(n1,n7) = n2 | ssA(n1,n7) = n3 | ssA(n1,n7) = n4 | ssA(n1,n7) = n5 | ssA(n1,n7) = n6 | ssA(n1,n7) = n7 | ssA(n1,n7) = n8 | ssA(n1,n7) = n9 )). fof(ax279,axiom, ( ssA(n1,n8) = n1 | ssA(n1,n8) = n2 | ssA(n1,n8) = n3 | ssA(n1,n8) = n4 | ssA(n1,n8) = n5 | ssA(n1,n8) = n6 | ssA(n1,n8) = n7 | ssA(n1,n8) = n8 | ssA(n1,n8) = n9 )). fof(ax280,axiom, ( ssA(n1,n9) = n1 | ssA(n1,n9) = n2 | ssA(n1,n9) = n3 | ssA(n1,n9) = n4 | ssA(n1,n9) = n5 | ssA(n1,n9) = n6 | ssA(n1,n9) = n7 | ssA(n1,n9) = n8 | ssA(n1,n9) = n9 )). fof(ax281,axiom, ( ssA(n2,n1) = n1 | ssA(n2,n1) = n2 | ssA(n2,n1) = n3 | ssA(n2,n1) = n4 | ssA(n2,n1) = n5 | ssA(n2,n1) = n6 | ssA(n2,n1) = n7 | ssA(n2,n1) = n8 | ssA(n2,n1) = n9 )). fof(ax282,axiom, ( ssA(n2,n2) = n1 | ssA(n2,n2) = n2 | ssA(n2,n2) = n3 | ssA(n2,n2) = n4 | ssA(n2,n2) = n5 | ssA(n2,n2) = n6 | ssA(n2,n2) = n7 | ssA(n2,n2) = n8 | ssA(n2,n2) = n9 )). fof(ax283,axiom, ( ssA(n2,n3) = n1 | ssA(n2,n3) = n2 | ssA(n2,n3) = n3 | ssA(n2,n3) = n4 | ssA(n2,n3) = n5 | ssA(n2,n3) = n6 | ssA(n2,n3) = n7 | ssA(n2,n3) = n8 | ssA(n2,n3) = n9 )). fof(ax284,axiom, ( ssA(n2,n4) = n1 | ssA(n2,n4) = n2 | ssA(n2,n4) = n3 | ssA(n2,n4) = n4 | ssA(n2,n4) = n5 | ssA(n2,n4) = n6 | ssA(n2,n4) = n7 | ssA(n2,n4) = n8 | ssA(n2,n4) = n9 )). fof(ax285,axiom, ( ssA(n2,n5) = n1 | ssA(n2,n5) = n2 | ssA(n2,n5) = n3 | ssA(n2,n5) = n4 | ssA(n2,n5) = n5 | ssA(n2,n5) = n6 | ssA(n2,n5) = n7 | ssA(n2,n5) = n8 | ssA(n2,n5) = n9 )). fof(ax286,axiom, ( ssA(n2,n6) = n1 | ssA(n2,n6) = n2 | ssA(n2,n6) = n3 | ssA(n2,n6) = n4 | ssA(n2,n6) = n5 | ssA(n2,n6) = n6 | ssA(n2,n6) = n7 | ssA(n2,n6) = n8 | ssA(n2,n6) = n9 )). fof(ax287,axiom, ( ssA(n2,n7) = n1 | ssA(n2,n7) = n2 | ssA(n2,n7) = n3 | ssA(n2,n7) = n4 | ssA(n2,n7) = n5 | ssA(n2,n7) = n6 | ssA(n2,n7) = n7 | ssA(n2,n7) = n8 | ssA(n2,n7) = n9 )). fof(ax288,axiom, ( ssA(n2,n8) = n1 | ssA(n2,n8) = n2 | ssA(n2,n8) = n3 | ssA(n2,n8) = n4 | ssA(n2,n8) = n5 | ssA(n2,n8) = n6 | ssA(n2,n8) = n7 | ssA(n2,n8) = n8 | ssA(n2,n8) = n9 )). fof(ax289,axiom, ( ssA(n2,n9) = n1 | ssA(n2,n9) = n2 | ssA(n2,n9) = n3 | ssA(n2,n9) = n4 | ssA(n2,n9) = n5 | ssA(n2,n9) = n6 | ssA(n2,n9) = n7 | ssA(n2,n9) = n8 | ssA(n2,n9) = n9 )). fof(ax290,axiom, ( ssA(n3,n1) = n1 | ssA(n3,n1) = n2 | ssA(n3,n1) = n3 | ssA(n3,n1) = n4 | ssA(n3,n1) = n5 | ssA(n3,n1) = n6 | ssA(n3,n1) = n7 | ssA(n3,n1) = n8 | ssA(n3,n1) = n9 )). fof(ax291,axiom, ( ssA(n3,n2) = n1 | ssA(n3,n2) = n2 | ssA(n3,n2) = n3 | ssA(n3,n2) = n4 | ssA(n3,n2) = n5 | ssA(n3,n2) = n6 | ssA(n3,n2) = n7 | ssA(n3,n2) = n8 | ssA(n3,n2) = n9 )). fof(ax292,axiom, ( ssA(n3,n3) = n1 | ssA(n3,n3) = n2 | ssA(n3,n3) = n3 | ssA(n3,n3) = n4 | ssA(n3,n3) = n5 | ssA(n3,n3) = n6 | ssA(n3,n3) = n7 | ssA(n3,n3) = n8 | ssA(n3,n3) = n9 )). fof(ax293,axiom, ( ssA(n3,n4) = n1 | ssA(n3,n4) = n2 | ssA(n3,n4) = n3 | ssA(n3,n4) = n4 | ssA(n3,n4) = n5 | ssA(n3,n4) = n6 | ssA(n3,n4) = n7 | ssA(n3,n4) = n8 | ssA(n3,n4) = n9 )). fof(ax294,axiom, ( ssA(n3,n5) = n1 | ssA(n3,n5) = n2 | ssA(n3,n5) = n3 | ssA(n3,n5) = n4 | ssA(n3,n5) = n5 | ssA(n3,n5) = n6 | ssA(n3,n5) = n7 | ssA(n3,n5) = n8 | ssA(n3,n5) = n9 )). fof(ax295,axiom, ( ssA(n3,n6) = n1 | ssA(n3,n6) = n2 | ssA(n3,n6) = n3 | ssA(n3,n6) = n4 | ssA(n3,n6) = n5 | ssA(n3,n6) = n6 | ssA(n3,n6) = n7 | ssA(n3,n6) = n8 | ssA(n3,n6) = n9 )). fof(ax296,axiom, ( ssA(n3,n7) = n1 | ssA(n3,n7) = n2 | ssA(n3,n7) = n3 | ssA(n3,n7) = n4 | ssA(n3,n7) = n5 | ssA(n3,n7) = n6 | ssA(n3,n7) = n7 | ssA(n3,n7) = n8 | ssA(n3,n7) = n9 )). fof(ax297,axiom, ( ssA(n3,n8) = n1 | ssA(n3,n8) = n2 | ssA(n3,n8) = n3 | ssA(n3,n8) = n4 | ssA(n3,n8) = n5 | ssA(n3,n8) = n6 | ssA(n3,n8) = n7 | ssA(n3,n8) = n8 | ssA(n3,n8) = n9 )). fof(ax298,axiom, ( ssA(n3,n9) = n1 | ssA(n3,n9) = n2 | ssA(n3,n9) = n3 | ssA(n3,n9) = n4 | ssA(n3,n9) = n5 | ssA(n3,n9) = n6 | ssA(n3,n9) = n7 | ssA(n3,n9) = n8 | ssA(n3,n9) = n9 )). fof(ax299,axiom, ( ssA(n4,n1) = n1 | ssA(n4,n1) = n2 | ssA(n4,n1) = n3 | ssA(n4,n1) = n4 | ssA(n4,n1) = n5 | ssA(n4,n1) = n6 | ssA(n4,n1) = n7 | ssA(n4,n1) = n8 | ssA(n4,n1) = n9 )). fof(ax300,axiom, ( ssA(n4,n2) = n1 | ssA(n4,n2) = n2 | ssA(n4,n2) = n3 | ssA(n4,n2) = n4 | ssA(n4,n2) = n5 | ssA(n4,n2) = n6 | ssA(n4,n2) = n7 | ssA(n4,n2) = n8 | ssA(n4,n2) = n9 )). fof(ax301,axiom, ( ssA(n4,n3) = n1 | ssA(n4,n3) = n2 | ssA(n4,n3) = n3 | ssA(n4,n3) = n4 | ssA(n4,n3) = n5 | ssA(n4,n3) = n6 | ssA(n4,n3) = n7 | ssA(n4,n3) = n8 | ssA(n4,n3) = n9 )). fof(ax302,axiom, ( ssA(n4,n4) = n1 | ssA(n4,n4) = n2 | ssA(n4,n4) = n3 | ssA(n4,n4) = n4 | ssA(n4,n4) = n5 | ssA(n4,n4) = n6 | ssA(n4,n4) = n7 | ssA(n4,n4) = n8 | ssA(n4,n4) = n9 )). fof(ax303,axiom, ( ssA(n4,n5) = n1 | ssA(n4,n5) = n2 | ssA(n4,n5) = n3 | ssA(n4,n5) = n4 | ssA(n4,n5) = n5 | ssA(n4,n5) = n6 | ssA(n4,n5) = n7 | ssA(n4,n5) = n8 | ssA(n4,n5) = n9 )). fof(ax304,axiom, ( ssA(n4,n6) = n1 | ssA(n4,n6) = n2 | ssA(n4,n6) = n3 | ssA(n4,n6) = n4 | ssA(n4,n6) = n5 | ssA(n4,n6) = n6 | ssA(n4,n6) = n7 | ssA(n4,n6) = n8 | ssA(n4,n6) = n9 )). fof(ax305,axiom, ( ssA(n4,n7) = n1 | ssA(n4,n7) = n2 | ssA(n4,n7) = n3 | ssA(n4,n7) = n4 | ssA(n4,n7) = n5 | ssA(n4,n7) = n6 | ssA(n4,n7) = n7 | ssA(n4,n7) = n8 | ssA(n4,n7) = n9 )). fof(ax306,axiom, ( ssA(n4,n8) = n1 | ssA(n4,n8) = n2 | ssA(n4,n8) = n3 | ssA(n4,n8) = n4 | ssA(n4,n8) = n5 | ssA(n4,n8) = n6 | ssA(n4,n8) = n7 | ssA(n4,n8) = n8 | ssA(n4,n8) = n9 )). fof(ax307,axiom, ( ssA(n4,n9) = n1 | ssA(n4,n9) = n2 | ssA(n4,n9) = n3 | ssA(n4,n9) = n4 | ssA(n4,n9) = n5 | ssA(n4,n9) = n6 | ssA(n4,n9) = n7 | ssA(n4,n9) = n8 | ssA(n4,n9) = n9 )). fof(ax308,axiom, ( ssA(n5,n1) = n1 | ssA(n5,n1) = n2 | ssA(n5,n1) = n3 | ssA(n5,n1) = n4 | ssA(n5,n1) = n5 | ssA(n5,n1) = n6 | ssA(n5,n1) = n7 | ssA(n5,n1) = n8 | ssA(n5,n1) = n9 )). fof(ax309,axiom, ( ssA(n5,n2) = n1 | ssA(n5,n2) = n2 | ssA(n5,n2) = n3 | ssA(n5,n2) = n4 | ssA(n5,n2) = n5 | ssA(n5,n2) = n6 | ssA(n5,n2) = n7 | ssA(n5,n2) = n8 | ssA(n5,n2) = n9 )). fof(ax310,axiom, ( ssA(n5,n3) = n1 | ssA(n5,n3) = n2 | ssA(n5,n3) = n3 | ssA(n5,n3) = n4 | ssA(n5,n3) = n5 | ssA(n5,n3) = n6 | ssA(n5,n3) = n7 | ssA(n5,n3) = n8 | ssA(n5,n3) = n9 )). fof(ax311,axiom, ( ssA(n5,n4) = n1 | ssA(n5,n4) = n2 | ssA(n5,n4) = n3 | ssA(n5,n4) = n4 | ssA(n5,n4) = n5 | ssA(n5,n4) = n6 | ssA(n5,n4) = n7 | ssA(n5,n4) = n8 | ssA(n5,n4) = n9 )). fof(ax312,axiom, ( ssA(n5,n5) = n1 | ssA(n5,n5) = n2 | ssA(n5,n5) = n3 | ssA(n5,n5) = n4 | ssA(n5,n5) = n5 | ssA(n5,n5) = n6 | ssA(n5,n5) = n7 | ssA(n5,n5) = n8 | ssA(n5,n5) = n9 )). fof(ax313,axiom, ( ssA(n5,n6) = n1 | ssA(n5,n6) = n2 | ssA(n5,n6) = n3 | ssA(n5,n6) = n4 | ssA(n5,n6) = n5 | ssA(n5,n6) = n6 | ssA(n5,n6) = n7 | ssA(n5,n6) = n8 | ssA(n5,n6) = n9 )). fof(ax314,axiom, ( ssA(n5,n7) = n1 | ssA(n5,n7) = n2 | ssA(n5,n7) = n3 | ssA(n5,n7) = n4 | ssA(n5,n7) = n5 | ssA(n5,n7) = n6 | ssA(n5,n7) = n7 | ssA(n5,n7) = n8 | ssA(n5,n7) = n9 )). fof(ax315,axiom, ( ssA(n5,n8) = n1 | ssA(n5,n8) = n2 | ssA(n5,n8) = n3 | ssA(n5,n8) = n4 | ssA(n5,n8) = n5 | ssA(n5,n8) = n6 | ssA(n5,n8) = n7 | ssA(n5,n8) = n8 | ssA(n5,n8) = n9 )). fof(ax316,axiom, ( ssA(n5,n9) = n1 | ssA(n5,n9) = n2 | ssA(n5,n9) = n3 | ssA(n5,n9) = n4 | ssA(n5,n9) = n5 | ssA(n5,n9) = n6 | ssA(n5,n9) = n7 | ssA(n5,n9) = n8 | ssA(n5,n9) = n9 )). fof(ax317,axiom, ( ssA(n6,n1) = n1 | ssA(n6,n1) = n2 | ssA(n6,n1) = n3 | ssA(n6,n1) = n4 | ssA(n6,n1) = n5 | ssA(n6,n1) = n6 | ssA(n6,n1) = n7 | ssA(n6,n1) = n8 | ssA(n6,n1) = n9 )). fof(ax318,axiom, ( ssA(n6,n2) = n1 | ssA(n6,n2) = n2 | ssA(n6,n2) = n3 | ssA(n6,n2) = n4 | ssA(n6,n2) = n5 | ssA(n6,n2) = n6 | ssA(n6,n2) = n7 | ssA(n6,n2) = n8 | ssA(n6,n2) = n9 )). fof(ax319,axiom, ( ssA(n6,n3) = n1 | ssA(n6,n3) = n2 | ssA(n6,n3) = n3 | ssA(n6,n3) = n4 | ssA(n6,n3) = n5 | ssA(n6,n3) = n6 | ssA(n6,n3) = n7 | ssA(n6,n3) = n8 | ssA(n6,n3) = n9 )). fof(ax320,axiom, ( ssA(n6,n4) = n1 | ssA(n6,n4) = n2 | ssA(n6,n4) = n3 | ssA(n6,n4) = n4 | ssA(n6,n4) = n5 | ssA(n6,n4) = n6 | ssA(n6,n4) = n7 | ssA(n6,n4) = n8 | ssA(n6,n4) = n9 )). fof(ax321,axiom, ( ssA(n6,n5) = n1 | ssA(n6,n5) = n2 | ssA(n6,n5) = n3 | ssA(n6,n5) = n4 | ssA(n6,n5) = n5 | ssA(n6,n5) = n6 | ssA(n6,n5) = n7 | ssA(n6,n5) = n8 | ssA(n6,n5) = n9 )). fof(ax322,axiom, ( ssA(n6,n6) = n1 | ssA(n6,n6) = n2 | ssA(n6,n6) = n3 | ssA(n6,n6) = n4 | ssA(n6,n6) = n5 | ssA(n6,n6) = n6 | ssA(n6,n6) = n7 | ssA(n6,n6) = n8 | ssA(n6,n6) = n9 )). fof(ax323,axiom, ( ssA(n6,n7) = n1 | ssA(n6,n7) = n2 | ssA(n6,n7) = n3 | ssA(n6,n7) = n4 | ssA(n6,n7) = n5 | ssA(n6,n7) = n6 | ssA(n6,n7) = n7 | ssA(n6,n7) = n8 | ssA(n6,n7) = n9 )). fof(ax324,axiom, ( ssA(n6,n8) = n1 | ssA(n6,n8) = n2 | ssA(n6,n8) = n3 | ssA(n6,n8) = n4 | ssA(n6,n8) = n5 | ssA(n6,n8) = n6 | ssA(n6,n8) = n7 | ssA(n6,n8) = n8 | ssA(n6,n8) = n9 )). fof(ax325,axiom, ( ssA(n6,n9) = n1 | ssA(n6,n9) = n2 | ssA(n6,n9) = n3 | ssA(n6,n9) = n4 | ssA(n6,n9) = n5 | ssA(n6,n9) = n6 | ssA(n6,n9) = n7 | ssA(n6,n9) = n8 | ssA(n6,n9) = n9 )). fof(ax326,axiom, ( ssA(n7,n1) = n1 | ssA(n7,n1) = n2 | ssA(n7,n1) = n3 | ssA(n7,n1) = n4 | ssA(n7,n1) = n5 | ssA(n7,n1) = n6 | ssA(n7,n1) = n7 | ssA(n7,n1) = n8 | ssA(n7,n1) = n9 )). fof(ax327,axiom, ( ssA(n7,n2) = n1 | ssA(n7,n2) = n2 | ssA(n7,n2) = n3 | ssA(n7,n2) = n4 | ssA(n7,n2) = n5 | ssA(n7,n2) = n6 | ssA(n7,n2) = n7 | ssA(n7,n2) = n8 | ssA(n7,n2) = n9 )). fof(ax328,axiom, ( ssA(n7,n3) = n1 | ssA(n7,n3) = n2 | ssA(n7,n3) = n3 | ssA(n7,n3) = n4 | ssA(n7,n3) = n5 | ssA(n7,n3) = n6 | ssA(n7,n3) = n7 | ssA(n7,n3) = n8 | ssA(n7,n3) = n9 )). fof(ax329,axiom, ( ssA(n7,n4) = n1 | ssA(n7,n4) = n2 | ssA(n7,n4) = n3 | ssA(n7,n4) = n4 | ssA(n7,n4) = n5 | ssA(n7,n4) = n6 | ssA(n7,n4) = n7 | ssA(n7,n4) = n8 | ssA(n7,n4) = n9 )). fof(ax330,axiom, ( ssA(n7,n5) = n1 | ssA(n7,n5) = n2 | ssA(n7,n5) = n3 | ssA(n7,n5) = n4 | ssA(n7,n5) = n5 | ssA(n7,n5) = n6 | ssA(n7,n5) = n7 | ssA(n7,n5) = n8 | ssA(n7,n5) = n9 )). fof(ax331,axiom, ( ssA(n7,n6) = n1 | ssA(n7,n6) = n2 | ssA(n7,n6) = n3 | ssA(n7,n6) = n4 | ssA(n7,n6) = n5 | ssA(n7,n6) = n6 | ssA(n7,n6) = n7 | ssA(n7,n6) = n8 | ssA(n7,n6) = n9 )). fof(ax332,axiom, ( ssA(n7,n7) = n1 | ssA(n7,n7) = n2 | ssA(n7,n7) = n3 | ssA(n7,n7) = n4 | ssA(n7,n7) = n5 | ssA(n7,n7) = n6 | ssA(n7,n7) = n7 | ssA(n7,n7) = n8 | ssA(n7,n7) = n9 )). fof(ax333,axiom, ( ssA(n7,n8) = n1 | ssA(n7,n8) = n2 | ssA(n7,n8) = n3 | ssA(n7,n8) = n4 | ssA(n7,n8) = n5 | ssA(n7,n8) = n6 | ssA(n7,n8) = n7 | ssA(n7,n8) = n8 | ssA(n7,n8) = n9 )). fof(ax334,axiom, ( ssA(n7,n9) = n1 | ssA(n7,n9) = n2 | ssA(n7,n9) = n3 | ssA(n7,n9) = n4 | ssA(n7,n9) = n5 | ssA(n7,n9) = n6 | ssA(n7,n9) = n7 | ssA(n7,n9) = n8 | ssA(n7,n9) = n9 )). fof(ax335,axiom, ( ssA(n8,n1) = n1 | ssA(n8,n1) = n2 | ssA(n8,n1) = n3 | ssA(n8,n1) = n4 | ssA(n8,n1) = n5 | ssA(n8,n1) = n6 | ssA(n8,n1) = n7 | ssA(n8,n1) = n8 | ssA(n8,n1) = n9 )). fof(ax336,axiom, ( ssA(n8,n2) = n1 | ssA(n8,n2) = n2 | ssA(n8,n2) = n3 | ssA(n8,n2) = n4 | ssA(n8,n2) = n5 | ssA(n8,n2) = n6 | ssA(n8,n2) = n7 | ssA(n8,n2) = n8 | ssA(n8,n2) = n9 )). fof(ax337,axiom, ( ssA(n8,n3) = n1 | ssA(n8,n3) = n2 | ssA(n8,n3) = n3 | ssA(n8,n3) = n4 | ssA(n8,n3) = n5 | ssA(n8,n3) = n6 | ssA(n8,n3) = n7 | ssA(n8,n3) = n8 | ssA(n8,n3) = n9 )). fof(ax338,axiom, ( ssA(n8,n4) = n1 | ssA(n8,n4) = n2 | ssA(n8,n4) = n3 | ssA(n8,n4) = n4 | ssA(n8,n4) = n5 | ssA(n8,n4) = n6 | ssA(n8,n4) = n7 | ssA(n8,n4) = n8 | ssA(n8,n4) = n9 )). fof(ax339,axiom, ( ssA(n8,n5) = n1 | ssA(n8,n5) = n2 | ssA(n8,n5) = n3 | ssA(n8,n5) = n4 | ssA(n8,n5) = n5 | ssA(n8,n5) = n6 | ssA(n8,n5) = n7 | ssA(n8,n5) = n8 | ssA(n8,n5) = n9 )). fof(ax340,axiom, ( ssA(n8,n6) = n1 | ssA(n8,n6) = n2 | ssA(n8,n6) = n3 | ssA(n8,n6) = n4 | ssA(n8,n6) = n5 | ssA(n8,n6) = n6 | ssA(n8,n6) = n7 | ssA(n8,n6) = n8 | ssA(n8,n6) = n9 )). fof(ax341,axiom, ( ssA(n8,n7) = n1 | ssA(n8,n7) = n2 | ssA(n8,n7) = n3 | ssA(n8,n7) = n4 | ssA(n8,n7) = n5 | ssA(n8,n7) = n6 | ssA(n8,n7) = n7 | ssA(n8,n7) = n8 | ssA(n8,n7) = n9 )). fof(ax342,axiom, ( ssA(n8,n8) = n1 | ssA(n8,n8) = n2 | ssA(n8,n8) = n3 | ssA(n8,n8) = n4 | ssA(n8,n8) = n5 | ssA(n8,n8) = n6 | ssA(n8,n8) = n7 | ssA(n8,n8) = n8 | ssA(n8,n8) = n9 )). fof(ax343,axiom, ( ssA(n8,n9) = n1 | ssA(n8,n9) = n2 | ssA(n8,n9) = n3 | ssA(n8,n9) = n4 | ssA(n8,n9) = n5 | ssA(n8,n9) = n6 | ssA(n8,n9) = n7 | ssA(n8,n9) = n8 | ssA(n8,n9) = n9 )). fof(ax344,axiom, ( ssA(n9,n1) = n1 | ssA(n9,n1) = n2 | ssA(n9,n1) = n3 | ssA(n9,n1) = n4 | ssA(n9,n1) = n5 | ssA(n9,n1) = n6 | ssA(n9,n1) = n7 | ssA(n9,n1) = n8 | ssA(n9,n1) = n9 )). fof(ax345,axiom, ( ssA(n9,n2) = n1 | ssA(n9,n2) = n2 | ssA(n9,n2) = n3 | ssA(n9,n2) = n4 | ssA(n9,n2) = n5 | ssA(n9,n2) = n6 | ssA(n9,n2) = n7 | ssA(n9,n2) = n8 | ssA(n9,n2) = n9 )). fof(ax346,axiom, ( ssA(n9,n3) = n1 | ssA(n9,n3) = n2 | ssA(n9,n3) = n3 | ssA(n9,n3) = n4 | ssA(n9,n3) = n5 | ssA(n9,n3) = n6 | ssA(n9,n3) = n7 | ssA(n9,n3) = n8 | ssA(n9,n3) = n9 )). fof(ax347,axiom, ( ssA(n9,n4) = n1 | ssA(n9,n4) = n2 | ssA(n9,n4) = n3 | ssA(n9,n4) = n4 | ssA(n9,n4) = n5 | ssA(n9,n4) = n6 | ssA(n9,n4) = n7 | ssA(n9,n4) = n8 | ssA(n9,n4) = n9 )). fof(ax348,axiom, ( ssA(n9,n5) = n1 | ssA(n9,n5) = n2 | ssA(n9,n5) = n3 | ssA(n9,n5) = n4 | ssA(n9,n5) = n5 | ssA(n9,n5) = n6 | ssA(n9,n5) = n7 | ssA(n9,n5) = n8 | ssA(n9,n5) = n9 )). fof(ax349,axiom, ( ssA(n9,n6) = n1 | ssA(n9,n6) = n2 | ssA(n9,n6) = n3 | ssA(n9,n6) = n4 | ssA(n9,n6) = n5 | ssA(n9,n6) = n6 | ssA(n9,n6) = n7 | ssA(n9,n6) = n8 | ssA(n9,n6) = n9 )). fof(ax350,axiom, ( ssA(n9,n7) = n1 | ssA(n9,n7) = n2 | ssA(n9,n7) = n3 | ssA(n9,n7) = n4 | ssA(n9,n7) = n5 | ssA(n9,n7) = n6 | ssA(n9,n7) = n7 | ssA(n9,n7) = n8 | ssA(n9,n7) = n9 )). fof(ax351,axiom, ( ssA(n9,n8) = n1 | ssA(n9,n8) = n2 | ssA(n9,n8) = n3 | ssA(n9,n8) = n4 | ssA(n9,n8) = n5 | ssA(n9,n8) = n6 | ssA(n9,n8) = n7 | ssA(n9,n8) = n8 | ssA(n9,n8) = n9 )). fof(ax352,axiom, ( ssA(n9,n9) = n1 | ssA(n9,n9) = n2 | ssA(n9,n9) = n3 | ssA(n9,n9) = n4 | ssA(n9,n9) = n5 | ssA(n9,n9) = n6 | ssA(n9,n9) = n7 | ssA(n9,n9) = n8 | ssA(n9,n9) = n9 )). %---Output fof(ax370,axiom,( ssP(ssA(n1,n1),ssA(n1,n2),ssA(n1,n3),ssA(n1,n4),ssA(n1,n5),ssA(n1,n6),ssA(n1,n7),ssA(n1,n8),ssA(n1,n9),ssA(n2,n1),ssA(n2,n2),ssA(n2,n3),ssA(n2,n4),ssA(n2,n5),ssA(n2,n6),ssA(n2,n7),ssA(n2,n8),ssA(n2,n9),ssA(n3,n1),ssA(n3,n2),ssA(n3,n3),ssA(n3,n4),ssA(n3,n5),ssA(n3,n6),ssA(n3,n7),ssA(n3,n8),ssA(n3,n9),ssA(n4,n1),ssA(n4,n2),ssA(n4,n3),ssA(n4,n4),ssA(n4,n5),ssA(n4,n6),ssA(n4,n7),ssA(n4,n8),ssA(n4,n9),ssA(n5,n1),ssA(n5,n2),ssA(n5,n3),ssA(n5,n4),ssA(n5,n5),ssA(n5,n6),ssA(n5,n7),ssA(n5,n8),ssA(n5,n9),ssA(n6,n1),ssA(n6,n2),ssA(n6,n3),ssA(n6,n4),ssA(n6,n5),ssA(n6,n6),ssA(n6,n7),ssA(n6,n8),ssA(n6,n9),ssA(n7,n1),ssA(n7,n2),ssA(n7,n3),ssA(n7,n4),ssA(n7,n5),ssA(n7,n6),ssA(n7,n7),ssA(n7,n8),ssA(n7,n9),ssA(n8,n1),ssA(n8,n2),ssA(n8,n3),ssA(n8,n4),ssA(n8,n5),ssA(n8,n6),ssA(n8,n7),ssA(n8,n8),ssA(n8,n9),ssA(n9,n1),ssA(n9,n2),ssA(n9,n3),ssA(n9,n4),ssA(n9,n5),ssA(n9,n6),ssA(n9,n7),ssA(n9,n8),ssA(n9,n9)) )). %------------------------------------------------------------------------------