helm/software/components/binaries/matitaprover/benchmarks/log.090625

   1 BOO007-2
   2 Order
   3  == is 100
   4  _ is 99
   5  a is 98
   6  add is 93
   7  additive_id1 is 77
   8  additive_id2 is 76
   9  additive_identity is 82
  10  additive_inverse1 is 84
  11  additive_inverse2 is 83
  12  b is 97
  13  c is 96
  14  commutativity_of_add is 92
  15  commutativity_of_multiply is 91
  16  distributivity1 is 90
  17  distributivity2 is 89
  18  distributivity3 is 88
  19  distributivity4 is 87
  20  inverse is 86
  21  multiplicative_id1 is 79
  22  multiplicative_id2 is 78
  23  multiplicative_identity is 85
  24  multiplicative_inverse1 is 81
  25  multiplicative_inverse2 is 80
  26  multiply is 95
  27  prove_associativity is 94
  28 Facts
  29  Id :   4, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
  30  Id :   6, {_}:
  31           multiply ?5 ?6 =?= multiply ?6 ?5
  32           [6, 5] by commutativity_of_multiply ?5 ?6
  33  Id :   8, {_}:
  34           add (multiply ?8 ?9) ?10 =<= multiply (add ?8 ?10) (add ?9 ?10)
  35           [10, 9, 8] by distributivity1 ?8 ?9 ?10
  36  Id :  10, {_}:
  37           add ?12 (multiply ?13 ?14) =<= multiply (add ?12 ?13) (add ?12 ?14)
  38           [14, 13, 12] by distributivity2 ?12 ?13 ?14
  39  Id :  12, {_}:
  40           multiply (add ?16 ?17) ?18
  41           =<=
  42           add (multiply ?16 ?18) (multiply ?17 ?18)
  43           [18, 17, 16] by distributivity3 ?16 ?17 ?18
  44  Id :  14, {_}:
  45           multiply ?20 (add ?21 ?22)
  46           =<=
  47           add (multiply ?20 ?21) (multiply ?20 ?22)
  48           [22, 21, 20] by distributivity4 ?20 ?21 ?22
  49  Id :  16, {_}:
  50           add ?24 (inverse ?24) =>= multiplicative_identity
  51           [24] by additive_inverse1 ?24
  52  Id :  18, {_}:
  53           add (inverse ?26) ?26 =>= multiplicative_identity
  54           [26] by additive_inverse2 ?26
  55  Id :  20, {_}:
  56           multiply ?28 (inverse ?28) =>= additive_identity
  57           [28] by multiplicative_inverse1 ?28
  58  Id :  22, {_}:
  59           multiply (inverse ?30) ?30 =>= additive_identity
  60           [30] by multiplicative_inverse2 ?30
  61  Id :  24, {_}:
  62           multiply ?32 multiplicative_identity =>= ?32
  63           [32] by multiplicative_id1 ?32
  64  Id :  26, {_}:
  65           multiply multiplicative_identity ?34 =>= ?34
  66           [34] by multiplicative_id2 ?34
  67  Id :  28, {_}: add ?36 additive_identity =>= ?36 [36] by additive_id1 ?36
  68  Id :  30, {_}: add additive_identity ?38 =>= ?38 [38] by additive_id2 ?38
  69 Goal
  70  Id :   2, {_}:
  71           multiply a (multiply b c) =<= multiply (multiply a b) c
  72           [] by prove_associativity
  73 Found proof, 6.095314s
  74 BOO007-4
  75 Order
  76  == is 100
  77  _ is 99
  78  a is 98
  79  add is 93
  80  additive_id1 is 87
  81  additive_identity is 88
  82  additive_inverse1 is 83
  83  b is 97
  84  c is 96
  85  commutativity_of_add is 92
  86  commutativity_of_multiply is 91
  87  distributivity1 is 90
  88  distributivity2 is 89
  89  inverse is 84
  90  multiplicative_id1 is 85
  91  multiplicative_identity is 86
  92  multiplicative_inverse1 is 82
  93  multiply is 95
  94  prove_associativity is 94
  95 Facts
  96  Id :   4, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
  97  Id :   6, {_}:
  98           multiply ?5 ?6 =?= multiply ?6 ?5
  99           [6, 5] by commutativity_of_multiply ?5 ?6
 100  Id :   8, {_}:
 101           add ?8 (multiply ?9 ?10) =<= multiply (add ?8 ?9) (add ?8 ?10)
 102           [10, 9, 8] by distributivity1 ?8 ?9 ?10
 103  Id :  10, {_}:
 104           multiply ?12 (add ?13 ?14)
 105           =<=
 106           add (multiply ?12 ?13) (multiply ?12 ?14)
 107           [14, 13, 12] by distributivity2 ?12 ?13 ?14
 108  Id :  12, {_}: add ?16 additive_identity =>= ?16 [16] by additive_id1 ?16
 109  Id :  14, {_}:
 110           multiply ?18 multiplicative_identity =>= ?18
 111           [18] by multiplicative_id1 ?18
 112  Id :  16, {_}:
 113           add ?20 (inverse ?20) =>= multiplicative_identity
 114           [20] by additive_inverse1 ?20
 115  Id :  18, {_}:
 116           multiply ?22 (inverse ?22) =>= additive_identity
 117           [22] by multiplicative_inverse1 ?22
 118 Goal
 119  Id :   2, {_}:
 120           multiply a (multiply b c) =<= multiply (multiply a b) c
 121           [] by prove_associativity
 122 Timeout !
 123 FAILURE in 625 iterations
 124 BOO031-1
 125 Order
 126  == is 100
 127  _ is 99
 128  a is 98
 129  add is 95
 130  additive_inverse is 83
 131  associativity_of_add is 80
 132  associativity_of_multiply is 79
 133  b is 97
 134  c is 96
 135  distributivity is 92
 136  inverse is 89
 137  l1 is 91
 138  l2 is 87
 139  l3 is 90
 140  l4 is 86
 141  multiplicative_inverse is 81
 142  multiply is 94
 143  n0 is 82
 144  n1 is 84
 145  property3 is 88
 146  property3_dual is 85
 147  prove_multiply_add_property is 93
 148 Facts
 149  Id :   4, {_}:
 150           add (multiply ?2 ?3) (add (multiply ?3 ?4) (multiply ?4 ?2))
 151           =>=
 152           multiply (add ?2 ?3) (multiply (add ?3 ?4) (add ?4 ?2))
 153           [4, 3, 2] by distributivity ?2 ?3 ?4
 154  Id :   6, {_}:
 155           add ?6 (multiply ?7 (multiply ?6 ?8)) =>= ?6
 156           [8, 7, 6] by l1 ?6 ?7 ?8
 157  Id :   8, {_}:
 158           add (add (multiply ?10 ?11) (multiply ?11 ?12)) ?11 =>= ?11
 159           [12, 11, 10] by l3 ?10 ?11 ?12
 160  Id :  10, {_}:
 161           multiply (add ?14 (inverse ?14)) ?15 =>= ?15
 162           [15, 14] by property3 ?14 ?15
 163  Id :  12, {_}:
 164           multiply ?17 (add ?18 (add ?17 ?19)) =>= ?17
 165           [19, 18, 17] by l2 ?17 ?18 ?19
 166  Id :  14, {_}:
 167           multiply (multiply (add ?21 ?22) (add ?22 ?23)) ?22 =>= ?22
 168           [23, 22, 21] by l4 ?21 ?22 ?23
 169  Id :  16, {_}:
 170           add (multiply ?25 (inverse ?25)) ?26 =>= ?26
 171           [26, 25] by property3_dual ?25 ?26
 172  Id :  18, {_}: add ?28 (inverse ?28) =>= n1 [28] by additive_inverse ?28
 173  Id :  20, {_}:
 174           multiply ?30 (inverse ?30) =>= n0
 175           [30] by multiplicative_inverse ?30
 176  Id :  22, {_}:
 177           add (add ?32 ?33) ?34 =?= add ?32 (add ?33 ?34)
 178           [34, 33, 32] by associativity_of_add ?32 ?33 ?34
 179  Id :  24, {_}:
 180           multiply (multiply ?36 ?37) ?38 =?= multiply ?36 (multiply ?37 ?38)
 181           [38, 37, 36] by associativity_of_multiply ?36 ?37 ?38
 182 Goal
 183  Id :   2, {_}:
 184           multiply a (add b c) =<= add (multiply b a) (multiply c a)
 185           [] by prove_multiply_add_property
 186 Timeout !
 187 FAILURE in 413 iterations
 188 BOO034-1
 189 Order
 190  == is 100
 191  _ is 99
 192  a is 98
 193  associativity is 88
 194  b is 96
 195  c is 94
 196  d is 93
 197  e is 92
 198  f is 91
 199  g is 90
 200  inverse is 97
 201  left_inverse is 85
 202  multiply is 95
 203  prove_single_axiom is 89
 204  right_inverse is 84
 205  ternary_multiply_1 is 87
 206  ternary_multiply_2 is 86
 207 Facts
 208  Id :   4, {_}:
 209           multiply (multiply ?2 ?3 ?4) ?5 (multiply ?2 ?3 ?6)
 210           =>=
 211           multiply ?2 ?3 (multiply ?4 ?5 ?6)
 212           [6, 5, 4, 3, 2] by associativity ?2 ?3 ?4 ?5 ?6
 213  Id :   6, {_}: multiply ?8 ?9 ?9 =>= ?9 [9, 8] by ternary_multiply_1 ?8 ?9
 214  Id :   8, {_}:
 215           multiply ?11 ?11 ?12 =>= ?11
 216           [12, 11] by ternary_multiply_2 ?11 ?12
 217  Id :  10, {_}:
 218           multiply (inverse ?14) ?14 ?15 =>= ?15
 219           [15, 14] by left_inverse ?14 ?15
 220  Id :  12, {_}:
 221           multiply ?17 ?18 (inverse ?18) =>= ?17
 222           [18, 17] by right_inverse ?17 ?18
 223 Goal
 224  Id :   2, {_}:
 225           multiply (multiply a (inverse a) b)
 226             (inverse (multiply (multiply c d e) f (multiply c d g)))
 227             (multiply d (multiply g f e) c)
 228           =>=
 229           b
 230           [] by prove_single_axiom
 231 Timeout !
 232 FAILURE in 424 iterations
 233 BOO072-1
 234 Order
 235  == is 100
 236  _ is 99
 237  a is 97
 238  add is 96
 239  b is 98
 240  dn1 is 93
 241  huntinton_1 is 95
 242  inverse is 94
 243 Facts
 244  Id :   4, {_}:
 245           inverse
 246             (add (inverse (add (inverse (add ?2 ?3)) ?4))
 247               (inverse
 248                 (add ?2 (inverse (add (inverse ?4) (inverse (add ?4 ?5)))))))
 249           =>=
 250           ?4
 251           [5, 4, 3, 2] by dn1 ?2 ?3 ?4 ?5
 252 Goal
 253  Id :   2, {_}: add b a =>= add a b [] by huntinton_1
 254 Found proof, 0.440809s
 255 BOO073-1
 256 Order
 257  == is 100
 258  _ is 99
 259  a is 98
 260  add is 96
 261  b is 97
 262  c is 95
 263  dn1 is 92
 264  huntinton_2 is 94
 265  inverse is 93
 266 Facts
 267  Id :   4, {_}:
 268           inverse
 269             (add (inverse (add (inverse (add ?2 ?3)) ?4))
 270               (inverse
 271                 (add ?2 (inverse (add (inverse ?4) (inverse (add ?4 ?5)))))))
 272           =>=
 273           ?4
 274           [5, 4, 3, 2] by dn1 ?2 ?3 ?4 ?5
 275 Goal
 276  Id :   2, {_}: add (add a b) c =>= add a (add b c) [] by huntinton_2
 277 Found proof, 95.580028s
 278 BOO076-1
 279 Order
 280  == is 100
 281  _ is 99
 282  a is 98
 283  b is 97
 284  c is 96
 285  nand is 95
 286  prove_meredith_2_basis_2 is 94
 287  sh_1 is 93
 288 Facts
 289  Id :   4, {_}:
 290           nand (nand ?2 (nand (nand ?3 ?2) ?2)) (nand ?3 (nand ?4 ?2)) =>= ?3
 291           [4, 3, 2] by sh_1 ?2 ?3 ?4
 292 Goal
 293  Id :   2, {_}:
 294           nand a (nand b (nand a c)) =<= nand (nand (nand c b) b) a
 295           [] by prove_meredith_2_basis_2
 296 Timeout !
 297 FAILURE in 277 iterations
 298 COL003-1
 299 Order
 300  == is 100
 301  _ is 99
 302  apply is 97
 303  b is 95
 304  b_definition is 94
 305  f is 98
 306  prove_strong_fixed_point is 96
 307  w is 93
 308  w_definition is 92
 309 Facts
 310  Id :   4, {_}:
 311           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 312           [5, 4, 3] by b_definition ?3 ?4 ?5
 313  Id :   6, {_}:
 314           apply (apply w ?7) ?8 =?= apply (apply ?7 ?8) ?8
 315           [8, 7] by w_definition ?7 ?8
 316 Goal
 317  Id :   2, {_}:
 318           apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
 319           [1] by prove_strong_fixed_point ?1
 320 Timeout !
 321 FAILURE in 1120 iterations
 322 COL003-12
 323 Order
 324  == is 100
 325  _ is 99
 326  apply is 96
 327  b is 94
 328  b_definition is 93
 329  fixed_pt is 97
 330  prove_strong_fixed_point is 95
 331  strong_fixed_point is 98
 332  w is 92
 333  w_definition is 91
 334 Facts
 335  Id :   4, {_}:
 336           apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
 337           [4, 3, 2] by b_definition ?2 ?3 ?4
 338  Id :   6, {_}:
 339           apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7
 340           [7, 6] by w_definition ?6 ?7
 341  Id :   8, {_}:
 342           strong_fixed_point
 343           =<=
 344           apply (apply b (apply w w))
 345             (apply (apply b w) (apply (apply b b) b))
 346           [] by strong_fixed_point
 347 Goal
 348  Id :   2, {_}:
 349           apply strong_fixed_point fixed_pt
 350           =<=
 351           apply fixed_pt (apply strong_fixed_point fixed_pt)
 352           [] by prove_strong_fixed_point
 353 Timeout !
 354 FAILURE in 1252 iterations
 355 COL003-20
 356 Order
 357  == is 100
 358  _ is 99
 359  apply is 96
 360  b is 94
 361  b_definition is 93
 362  fixed_pt is 97
 363  prove_strong_fixed_point is 95
 364  strong_fixed_point is 98
 365  w is 92
 366  w_definition is 91
 367 Facts
 368  Id :   4, {_}:
 369           apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
 370           [4, 3, 2] by b_definition ?2 ?3 ?4
 371  Id :   6, {_}:
 372           apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7
 373           [7, 6] by w_definition ?6 ?7
 374  Id :   8, {_}:
 375           strong_fixed_point
 376           =<=
 377           apply (apply b (apply w w))
 378             (apply (apply b (apply b w)) (apply (apply b b) b))
 379           [] by strong_fixed_point
 380 Goal
 381  Id :   2, {_}:
 382           apply strong_fixed_point fixed_pt
 383           =<=
 384           apply fixed_pt (apply strong_fixed_point fixed_pt)
 385           [] by prove_strong_fixed_point
 386 Timeout !
 387 FAILURE in 1223 iterations
 388 COL006-6
 389 Order
 390  == is 100
 391  _ is 99
 392  apply is 96
 393  fixed_pt is 97
 394  k is 92
 395  k_definition is 91
 396  prove_strong_fixed_point is 95
 397  s is 94
 398  s_definition is 93
 399  strong_fixed_point is 98
 400 Facts
 401  Id :   4, {_}:
 402           apply (apply (apply s ?2) ?3) ?4
 403           =?=
 404           apply (apply ?2 ?4) (apply ?3 ?4)
 405           [4, 3, 2] by s_definition ?2 ?3 ?4
 406  Id :   6, {_}: apply (apply k ?6) ?7 =>= ?6 [7, 6] by k_definition ?6 ?7
 407  Id :   8, {_}:
 408           strong_fixed_point
 409           =<=
 410           apply
 411             (apply s
 412               (apply k
 413                 (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))))
 414             (apply (apply s (apply (apply s (apply k s)) k))
 415               (apply k
 416                 (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))))
 417           [] by strong_fixed_point
 418 Goal
 419  Id :   2, {_}:
 420           apply strong_fixed_point fixed_pt
 421           =<=
 422           apply fixed_pt (apply strong_fixed_point fixed_pt)
 423           [] by prove_strong_fixed_point
 424 Timeout !
 425 FAILURE in 1708 iterations
 426 COL011-1
 427 Order
 428  == is 100
 429  _ is 99
 430  apply is 97
 431  combinator is 98
 432  o is 95
 433  o_definition is 94
 434  prove_fixed_point is 96
 435  q1 is 93
 436  q1_definition is 92
 437 Facts
 438  Id :   4, {_}:
 439           apply (apply o ?3) ?4 =?= apply ?4 (apply ?3 ?4)
 440           [4, 3] by o_definition ?3 ?4
 441  Id :   6, {_}:
 442           apply (apply (apply q1 ?6) ?7) ?8 =>= apply ?6 (apply ?8 ?7)
 443           [8, 7, 6] by q1_definition ?6 ?7 ?8
 444 Goal
 445  Id :   2, {_}: ?1 =<= apply combinator ?1 [1] by prove_fixed_point ?1
 446 Timeout !
 447 FAILURE in 1839 iterations
 448 COL037-1
 449 Order
 450  == is 100
 451  _ is 99
 452  apply is 97
 453  b is 93
 454  b_definition is 92
 455  c is 91
 456  c_definition is 90
 457  f is 98
 458  prove_fixed_point is 96
 459  s is 95
 460  s_definition is 94
 461 Facts
 462  Id :   4, {_}:
 463           apply (apply (apply s ?3) ?4) ?5
 464           =?=
 465           apply (apply ?3 ?5) (apply ?4 ?5)
 466           [5, 4, 3] by s_definition ?3 ?4 ?5
 467  Id :   6, {_}:
 468           apply (apply (apply b ?7) ?8) ?9 =>= apply ?7 (apply ?8 ?9)
 469           [9, 8, 7] by b_definition ?7 ?8 ?9
 470  Id :   8, {_}:
 471           apply (apply (apply c ?11) ?12) ?13 =>= apply (apply ?11 ?13) ?12
 472           [13, 12, 11] by c_definition ?11 ?12 ?13
 473 Goal
 474  Id :   2, {_}:
 475           apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
 476           [1] by prove_fixed_point ?1
 477 Timeout !
 478 FAILURE in 944 iterations
 479 COL038-1
 480 Order
 481  == is 100
 482  _ is 99
 483  apply is 97
 484  b is 95
 485  b_definition is 94
 486  f is 98
 487  m is 93
 488  m_definition is 92
 489  prove_fixed_point is 96
 490  v is 91
 491  v_definition is 90
 492 Facts
 493  Id :   4, {_}:
 494           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 495           [5, 4, 3] by b_definition ?3 ?4 ?5
 496  Id :   6, {_}: apply m ?7 =?= apply ?7 ?7 [7] by m_definition ?7
 497  Id :   8, {_}:
 498           apply (apply (apply v ?9) ?10) ?11 =>= apply (apply ?11 ?9) ?10
 499           [11, 10, 9] by v_definition ?9 ?10 ?11
 500 Goal
 501  Id :   2, {_}:
 502           apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
 503           [1] by prove_fixed_point ?1
 504 Timeout !
 505 FAILURE in 1682 iterations
 506 COL043-3
 507 Order
 508  == is 100
 509  _ is 99
 510  apply is 96
 511  b is 94
 512  b_definition is 93
 513  fixed_pt is 97
 514  h is 92
 515  h_definition is 91
 516  prove_strong_fixed_point is 95
 517  strong_fixed_point is 98
 518 Facts
 519  Id :   4, {_}:
 520           apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
 521           [4, 3, 2] by b_definition ?2 ?3 ?4
 522  Id :   6, {_}:
 523           apply (apply (apply h ?6) ?7) ?8
 524           =?=
 525           apply (apply (apply ?6 ?7) ?8) ?7
 526           [8, 7, 6] by h_definition ?6 ?7 ?8
 527  Id :   8, {_}:
 528           strong_fixed_point
 529           =<=
 530           apply
 531             (apply b
 532               (apply
 533                 (apply b
 534                   (apply
 535                     (apply h
 536                       (apply (apply b (apply (apply b h) (apply b b)))
 537                         (apply h (apply (apply b h) (apply b b))))) h)) b)) b
 538           [] by strong_fixed_point
 539 Goal
 540  Id :   2, {_}:
 541           apply strong_fixed_point fixed_pt
 542           =<=
 543           apply fixed_pt (apply strong_fixed_point fixed_pt)
 544           [] by prove_strong_fixed_point
 545 Timeout !
 546 FAILURE in 1406 iterations
 547 COL044-8
 548 Order
 549  == is 100
 550  _ is 99
 551  apply is 96
 552  b is 94
 553  b_definition is 93
 554  fixed_pt is 97
 555  n is 92
 556  n_definition is 91
 557  prove_strong_fixed_point is 95
 558  strong_fixed_point is 98
 559 Facts
 560  Id :   4, {_}:
 561           apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
 562           [4, 3, 2] by b_definition ?2 ?3 ?4
 563  Id :   6, {_}:
 564           apply (apply (apply n ?6) ?7) ?8
 565           =?=
 566           apply (apply (apply ?6 ?8) ?7) ?8
 567           [8, 7, 6] by n_definition ?6 ?7 ?8
 568  Id :   8, {_}:
 569           strong_fixed_point
 570           =<=
 571           apply
 572             (apply b
 573               (apply
 574                 (apply b
 575                   (apply
 576                     (apply n
 577                       (apply n
 578                         (apply (apply b (apply b b))
 579                           (apply n (apply (apply b b) n))))) n)) b)) b
 580           [] by strong_fixed_point
 581 Goal
 582  Id :   2, {_}:
 583           apply strong_fixed_point fixed_pt
 584           =<=
 585           apply fixed_pt (apply strong_fixed_point fixed_pt)
 586           [] by prove_strong_fixed_point
 587 Timeout !
 588 FAILURE in 1249 iterations
 589 COL046-1
 590 Order
 591  == is 100
 592  _ is 99
 593  apply is 97
 594  b is 93
 595  b_definition is 92
 596  f is 98
 597  m is 91
 598  m_definition is 90
 599  prove_fixed_point is 96
 600  s is 95
 601  s_definition is 94
 602 Facts
 603  Id :   4, {_}:
 604           apply (apply (apply s ?3) ?4) ?5
 605           =?=
 606           apply (apply ?3 ?5) (apply ?4 ?5)
 607           [5, 4, 3] by s_definition ?3 ?4 ?5
 608  Id :   6, {_}:
 609           apply (apply (apply b ?7) ?8) ?9 =>= apply ?7 (apply ?8 ?9)
 610           [9, 8, 7] by b_definition ?7 ?8 ?9
 611  Id :   8, {_}: apply m ?11 =?= apply ?11 ?11 [11] by m_definition ?11
 612 Goal
 613  Id :   2, {_}:
 614           apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
 615           [1] by prove_fixed_point ?1
 616 Timeout !
 617 FAILURE in 1258 iterations
 618 COL049-1
 619 Order
 620  == is 100
 621  _ is 99
 622  apply is 97
 623  b is 95
 624  b_definition is 94
 625  f is 98
 626  m is 91
 627  m_definition is 90
 628  prove_strong_fixed_point is 96
 629  w is 93
 630  w_definition is 92
 631 Facts
 632  Id :   4, {_}:
 633           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 634           [5, 4, 3] by b_definition ?3 ?4 ?5
 635  Id :   6, {_}:
 636           apply (apply w ?7) ?8 =?= apply (apply ?7 ?8) ?8
 637           [8, 7] by w_definition ?7 ?8
 638  Id :   8, {_}: apply m ?10 =?= apply ?10 ?10 [10] by m_definition ?10
 639 Goal
 640  Id :   2, {_}:
 641           apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
 642           [1] by prove_strong_fixed_point ?1
 643 Timeout !
 644 FAILURE in 1565 iterations
 645 COL057-1
 646 Order
 647  == is 100
 648  _ is 99
 649  apply is 97
 650  b is 93
 651  b_definition is 92
 652  c is 91
 653  c_definition is 90
 654  f is 98
 655  i is 89
 656  i_definition is 88
 657  prove_strong_fixed_point is 96
 658  s is 95
 659  s_definition is 94
 660 Facts
 661  Id :   4, {_}:
 662           apply (apply (apply s ?3) ?4) ?5
 663           =?=
 664           apply (apply ?3 ?5) (apply ?4 ?5)
 665           [5, 4, 3] by s_definition ?3 ?4 ?5
 666  Id :   6, {_}:
 667           apply (apply (apply b ?7) ?8) ?9 =>= apply ?7 (apply ?8 ?9)
 668           [9, 8, 7] by b_definition ?7 ?8 ?9
 669  Id :   8, {_}:
 670           apply (apply (apply c ?11) ?12) ?13 =>= apply (apply ?11 ?13) ?12
 671           [13, 12, 11] by c_definition ?11 ?12 ?13
 672  Id :  10, {_}: apply i ?15 =>= ?15 [15] by i_definition ?15
 673 Goal
 674  Id :   2, {_}:
 675           apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
 676           [1] by prove_strong_fixed_point ?1
 677 Timeout !
 678 FAILURE in 1505 iterations
 679 COL060-1
 680 Order
 681  == is 100
 682  _ is 99
 683  apply is 97
 684  b is 93
 685  b_definition is 92
 686  f is 98
 687  g is 96
 688  h is 95
 689  prove_q_combinator is 94
 690  t is 91
 691  t_definition is 90
 692 Facts
 693  Id :   4, {_}:
 694           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 695           [5, 4, 3] by b_definition ?3 ?4 ?5
 696  Id :   6, {_}:
 697           apply (apply t ?7) ?8 =>= apply ?8 ?7
 698           [8, 7] by t_definition ?7 ?8
 699 Goal
 700  Id :   2, {_}:
 701           apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
 702           =>=
 703           apply (g ?1) (apply (f ?1) (h ?1))
 704           [1] by prove_q_combinator ?1
 705 Found proof, 0.103279s
 706 COL061-1
 707 Order
 708  == is 100
 709  _ is 99
 710  apply is 97
 711  b is 93
 712  b_definition is 92
 713  f is 98
 714  g is 96
 715  h is 95
 716  prove_q1_combinator is 94
 717  t is 91
 718  t_definition is 90
 719 Facts
 720  Id :   4, {_}:
 721           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 722           [5, 4, 3] by b_definition ?3 ?4 ?5
 723  Id :   6, {_}:
 724           apply (apply t ?7) ?8 =>= apply ?8 ?7
 725           [8, 7] by t_definition ?7 ?8
 726 Goal
 727  Id :   2, {_}:
 728           apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
 729           =>=
 730           apply (f ?1) (apply (h ?1) (g ?1))
 731           [1] by prove_q1_combinator ?1
 732 Found proof, 0.116546s
 733 COL063-1
 734 Order
 735  == is 100
 736  _ is 99
 737  apply is 97
 738  b is 93
 739  b_definition is 92
 740  f is 98
 741  g is 96
 742  h is 95
 743  prove_f_combinator is 94
 744  t is 91
 745  t_definition is 90
 746 Facts
 747  Id :   4, {_}:
 748           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 749           [5, 4, 3] by b_definition ?3 ?4 ?5
 750  Id :   6, {_}:
 751           apply (apply t ?7) ?8 =>= apply ?8 ?7
 752           [8, 7] by t_definition ?7 ?8
 753 Goal
 754  Id :   2, {_}:
 755           apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
 756           =>=
 757           apply (apply (h ?1) (g ?1)) (f ?1)
 758           [1] by prove_f_combinator ?1
 759 Found proof, 1.828433s
 760 COL064-1
 761 Order
 762  == is 100
 763  _ is 99
 764  apply is 97
 765  b is 93
 766  b_definition is 92
 767  f is 98
 768  g is 96
 769  h is 95
 770  prove_v_combinator is 94
 771  t is 91
 772  t_definition is 90
 773 Facts
 774  Id :   4, {_}:
 775           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 776           [5, 4, 3] by b_definition ?3 ?4 ?5
 777  Id :   6, {_}:
 778           apply (apply t ?7) ?8 =>= apply ?8 ?7
 779           [8, 7] by t_definition ?7 ?8
 780 Goal
 781  Id :   2, {_}:
 782           apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
 783           =>=
 784           apply (apply (h ?1) (f ?1)) (g ?1)
 785           [1] by prove_v_combinator ?1
 786 Found proof, 13.759082s
 787 COL065-1
 788 Order
 789  == is 100
 790  _ is 99
 791  apply is 97
 792  b is 92
 793  b_definition is 91
 794  f is 98
 795  g is 96
 796  h is 95
 797  i is 94
 798  prove_g_combinator is 93
 799  t is 90
 800  t_definition is 89
 801 Facts
 802  Id :   4, {_}:
 803           apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
 804           [5, 4, 3] by b_definition ?3 ?4 ?5
 805  Id :   6, {_}:
 806           apply (apply t ?7) ?8 =>= apply ?8 ?7
 807           [8, 7] by t_definition ?7 ?8
 808 Goal
 809  Id :   2, {_}:
 810           apply (apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)) (i ?1)
 811           =>=
 812           apply (apply (f ?1) (i ?1)) (apply (g ?1) (h ?1))
 813           [1] by prove_g_combinator ?1
 814 Found proof, 68.133820s
 815 GRP014-1
 816 Order
 817  == is 100
 818  _ is 99
 819  a is 98
 820  b is 97
 821  c is 96
 822  group_axiom is 92
 823  inverse is 93
 824  multiply is 95
 825  prove_associativity is 94
 826 Facts
 827  Id :   4, {_}:
 828           multiply ?2
 829             (inverse
 830               (multiply
 831                 (multiply
 832                   (inverse
 833                     (multiply (inverse ?3) (multiply (inverse ?2) ?4))) ?5)
 834                 (inverse (multiply ?3 ?5))))
 835           =>=
 836           ?4
 837           [5, 4, 3, 2] by group_axiom ?2 ?3 ?4 ?5
 838 Goal
 839  Id :   2, {_}:
 840           multiply a (multiply b c) =<= multiply (multiply a b) c
 841           [] by prove_associativity
 842 Found proof, 3.453474s
 843 GRP024-5
 844 Order
 845  == is 100
 846  _ is 99
 847  a is 98
 848  associativity is 88
 849  associativity_of_commutator is 86
 850  b is 97
 851  c is 96
 852  commutator is 95
 853  identity is 92
 854  inverse is 90
 855  left_identity is 91
 856  left_inverse is 89
 857  multiply is 94
 858  name is 87
 859  prove_center is 93
 860 Facts
 861  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
 862  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
 863  Id :   8, {_}:
 864           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
 865           [8, 7, 6] by associativity ?6 ?7 ?8
 866  Id :  10, {_}:
 867           commutator ?10 ?11
 868           =<=
 869           multiply (inverse ?10) (multiply (inverse ?11) (multiply ?10 ?11))
 870           [11, 10] by name ?10 ?11
 871  Id :  12, {_}:
 872           commutator (commutator ?13 ?14) ?15
 873           =?=
 874           commutator ?13 (commutator ?14 ?15)
 875           [15, 14, 13] by associativity_of_commutator ?13 ?14 ?15
 876 Goal
 877  Id :   2, {_}:
 878           multiply a (commutator b c) =<= multiply (commutator b c) a
 879           [] by prove_center
 880 Timeout !
 881 FAILURE in 602 iterations
 882 GRP114-1
 883 Order
 884  == is 100
 885  _ is 99
 886  a is 98
 887  associativity is 89
 888  identity is 93
 889  intersection is 85
 890  intersection_associative is 79
 891  intersection_commutative is 81
 892  intersection_idempotent is 84
 893  intersection_union_absorbtion is 76
 894  inverse is 91
 895  inverse_involution is 87
 896  inverse_of_identity is 88
 897  inverse_product_lemma is 86
 898  left_identity is 92
 899  left_inverse is 90
 900  multiply is 95
 901  multiply_intersection1 is 74
 902  multiply_intersection2 is 72
 903  multiply_union1 is 75
 904  multiply_union2 is 73
 905  negative_part is 96
 906  positive_part is 97
 907  prove_product is 94
 908  union is 83
 909  union_associative is 78
 910  union_commutative is 80
 911  union_idempotent is 82
 912  union_intersection_absorbtion is 77
 913 Facts
 914  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
 915  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
 916  Id :   8, {_}:
 917           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
 918           [8, 7, 6] by associativity ?6 ?7 ?8
 919  Id :  10, {_}: inverse identity =>= identity [] by inverse_of_identity
 920  Id :  12, {_}: inverse (inverse ?11) =>= ?11 [11] by inverse_involution ?11
 921  Id :  14, {_}:
 922           inverse (multiply ?13 ?14) =<= multiply (inverse ?14) (inverse ?13)
 923           [14, 13] by inverse_product_lemma ?13 ?14
 924  Id :  16, {_}:
 925           intersection ?16 ?16 =>= ?16
 926           [16] by intersection_idempotent ?16
 927  Id :  18, {_}: union ?18 ?18 =>= ?18 [18] by union_idempotent ?18
 928  Id :  20, {_}:
 929           intersection ?20 ?21 =?= intersection ?21 ?20
 930           [21, 20] by intersection_commutative ?20 ?21
 931  Id :  22, {_}:
 932           union ?23 ?24 =?= union ?24 ?23
 933           [24, 23] by union_commutative ?23 ?24
 934  Id :  24, {_}:
 935           intersection ?26 (intersection ?27 ?28)
 936           =?=
 937           intersection (intersection ?26 ?27) ?28
 938           [28, 27, 26] by intersection_associative ?26 ?27 ?28
 939  Id :  26, {_}:
 940           union ?30 (union ?31 ?32) =?= union (union ?30 ?31) ?32
 941           [32, 31, 30] by union_associative ?30 ?31 ?32
 942  Id :  28, {_}:
 943           union (intersection ?34 ?35) ?35 =>= ?35
 944           [35, 34] by union_intersection_absorbtion ?34 ?35
 945  Id :  30, {_}:
 946           intersection (union ?37 ?38) ?38 =>= ?38
 947           [38, 37] by intersection_union_absorbtion ?37 ?38
 948  Id :  32, {_}:
 949           multiply ?40 (union ?41 ?42)
 950           =<=
 951           union (multiply ?40 ?41) (multiply ?40 ?42)
 952           [42, 41, 40] by multiply_union1 ?40 ?41 ?42
 953  Id :  34, {_}:
 954           multiply ?44 (intersection ?45 ?46)
 955           =<=
 956           intersection (multiply ?44 ?45) (multiply ?44 ?46)
 957           [46, 45, 44] by multiply_intersection1 ?44 ?45 ?46
 958  Id :  36, {_}:
 959           multiply (union ?48 ?49) ?50
 960           =<=
 961           union (multiply ?48 ?50) (multiply ?49 ?50)
 962           [50, 49, 48] by multiply_union2 ?48 ?49 ?50
 963  Id :  38, {_}:
 964           multiply (intersection ?52 ?53) ?54
 965           =<=
 966           intersection (multiply ?52 ?54) (multiply ?53 ?54)
 967           [54, 53, 52] by multiply_intersection2 ?52 ?53 ?54
 968  Id :  40, {_}:
 969           positive_part ?56 =<= union ?56 identity
 970           [56] by positive_part ?56
 971  Id :  42, {_}:
 972           negative_part ?58 =<= intersection ?58 identity
 973           [58] by negative_part ?58
 974 Goal
 975  Id :   2, {_}:
 976           multiply (positive_part a) (negative_part a) =>= a
 977           [] by prove_product
 978 Timeout !
 979 FAILURE in 1190 iterations
 980 GRP164-2
 981 Order
 982  == is 100
 983  _ is 99
 984  a is 98
 985  associativity is 87
 986  associativity_of_glb is 84
 987  associativity_of_lub is 83
 988  b is 97
 989  c is 96
 990  glb_absorbtion is 79
 991  greatest_lower_bound is 94
 992  idempotence_of_gld is 81
 993  idempotence_of_lub is 82
 994  identity is 92
 995  inverse is 89
 996  least_upper_bound is 95
 997  left_identity is 90
 998  left_inverse is 88
 999  lub_absorbtion is 80
1000  monotony_glb1 is 77
1001  monotony_glb2 is 75
1002  monotony_lub1 is 78
1003  monotony_lub2 is 76
1004  multiply is 91
1005  prove_distrun is 93
1006  symmetry_of_glb is 86
1007  symmetry_of_lub is 85
1008 Facts
1009  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1010  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1011  Id :   8, {_}:
1012           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1013           [8, 7, 6] by associativity ?6 ?7 ?8
1014  Id :  10, {_}:
1015           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1016           [11, 10] by symmetry_of_glb ?10 ?11
1017  Id :  12, {_}:
1018           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1019           [14, 13] by symmetry_of_lub ?13 ?14
1020  Id :  14, {_}:
1021           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1022           =?=
1023           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1024           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1025  Id :  16, {_}:
1026           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1027           =?=
1028           least_upper_bound (least_upper_bound ?20 ?21) ?22
1029           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1030  Id :  18, {_}:
1031           least_upper_bound ?24 ?24 =>= ?24
1032           [24] by idempotence_of_lub ?24
1033  Id :  20, {_}:
1034           greatest_lower_bound ?26 ?26 =>= ?26
1035           [26] by idempotence_of_gld ?26
1036  Id :  22, {_}:
1037           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1038           [29, 28] by lub_absorbtion ?28 ?29
1039  Id :  24, {_}:
1040           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1041           [32, 31] by glb_absorbtion ?31 ?32
1042  Id :  26, {_}:
1043           multiply ?34 (least_upper_bound ?35 ?36)
1044           =<=
1045           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1046           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1047  Id :  28, {_}:
1048           multiply ?38 (greatest_lower_bound ?39 ?40)
1049           =<=
1050           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1051           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1052  Id :  30, {_}:
1053           multiply (least_upper_bound ?42 ?43) ?44
1054           =<=
1055           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1056           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1057  Id :  32, {_}:
1058           multiply (greatest_lower_bound ?46 ?47) ?48
1059           =<=
1060           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1061           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1062 Goal
1063  Id :   2, {_}:
1064           greatest_lower_bound a (least_upper_bound b c)
1065           =<=
1066           least_upper_bound (greatest_lower_bound a b)
1067             (greatest_lower_bound a c)
1068           [] by prove_distrun
1069 Timeout !
1070 FAILURE in 1400 iterations
1071 GRP167-1
1072 Order
1073  == is 100
1074  _ is 99
1075  a is 98
1076  associativity is 89
1077  associativity_of_glb is 84
1078  associativity_of_lub is 83
1079  glb_absorbtion is 79
1080  greatest_lower_bound is 88
1081  idempotence_of_gld is 81
1082  idempotence_of_lub is 82
1083  identity is 93
1084  inverse is 91
1085  lat4_1 is 74
1086  lat4_2 is 73
1087  lat4_3 is 72
1088  lat4_4 is 71
1089  least_upper_bound is 86
1090  left_identity is 92
1091  left_inverse is 90
1092  lub_absorbtion is 80
1093  monotony_glb1 is 77
1094  monotony_glb2 is 75
1095  monotony_lub1 is 78
1096  monotony_lub2 is 76
1097  multiply is 95
1098  negative_part is 96
1099  positive_part is 97
1100  prove_lat4 is 94
1101  symmetry_of_glb is 87
1102  symmetry_of_lub is 85
1103 Facts
1104  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1105  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1106  Id :   8, {_}:
1107           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1108           [8, 7, 6] by associativity ?6 ?7 ?8
1109  Id :  10, {_}:
1110           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1111           [11, 10] by symmetry_of_glb ?10 ?11
1112  Id :  12, {_}:
1113           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1114           [14, 13] by symmetry_of_lub ?13 ?14
1115  Id :  14, {_}:
1116           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1117           =?=
1118           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1119           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1120  Id :  16, {_}:
1121           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1122           =?=
1123           least_upper_bound (least_upper_bound ?20 ?21) ?22
1124           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1125  Id :  18, {_}:
1126           least_upper_bound ?24 ?24 =>= ?24
1127           [24] by idempotence_of_lub ?24
1128  Id :  20, {_}:
1129           greatest_lower_bound ?26 ?26 =>= ?26
1130           [26] by idempotence_of_gld ?26
1131  Id :  22, {_}:
1132           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1133           [29, 28] by lub_absorbtion ?28 ?29
1134  Id :  24, {_}:
1135           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1136           [32, 31] by glb_absorbtion ?31 ?32
1137  Id :  26, {_}:
1138           multiply ?34 (least_upper_bound ?35 ?36)
1139           =<=
1140           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1141           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1142  Id :  28, {_}:
1143           multiply ?38 (greatest_lower_bound ?39 ?40)
1144           =<=
1145           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1146           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1147  Id :  30, {_}:
1148           multiply (least_upper_bound ?42 ?43) ?44
1149           =<=
1150           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1151           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1152  Id :  32, {_}:
1153           multiply (greatest_lower_bound ?46 ?47) ?48
1154           =<=
1155           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1156           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1157  Id :  34, {_}:
1158           positive_part ?50 =<= least_upper_bound ?50 identity
1159           [50] by lat4_1 ?50
1160  Id :  36, {_}:
1161           negative_part ?52 =<= greatest_lower_bound ?52 identity
1162           [52] by lat4_2 ?52
1163  Id :  38, {_}:
1164           least_upper_bound ?54 (greatest_lower_bound ?55 ?56)
1165           =<=
1166           greatest_lower_bound (least_upper_bound ?54 ?55)
1167             (least_upper_bound ?54 ?56)
1168           [56, 55, 54] by lat4_3 ?54 ?55 ?56
1169  Id :  40, {_}:
1170           greatest_lower_bound ?58 (least_upper_bound ?59 ?60)
1171           =<=
1172           least_upper_bound (greatest_lower_bound ?58 ?59)
1173             (greatest_lower_bound ?58 ?60)
1174           [60, 59, 58] by lat4_4 ?58 ?59 ?60
1175 Goal
1176  Id :   2, {_}:
1177           a =<= multiply (positive_part a) (negative_part a)
1178           [] by prove_lat4
1179 Timeout !
1180 FAILURE in 1375 iterations
1181 GRP178-2
1182 Order
1183  == is 100
1184  _ is 99
1185  a is 98
1186  associativity is 88
1187  associativity_of_glb is 84
1188  associativity_of_lub is 83
1189  b is 97
1190  c is 96
1191  glb_absorbtion is 79
1192  greatest_lower_bound is 94
1193  idempotence_of_gld is 81
1194  idempotence_of_lub is 82
1195  identity is 92
1196  inverse is 90
1197  least_upper_bound is 86
1198  left_identity is 91
1199  left_inverse is 89
1200  lub_absorbtion is 80
1201  monotony_glb1 is 77
1202  monotony_glb2 is 75
1203  monotony_lub1 is 78
1204  monotony_lub2 is 76
1205  multiply is 95
1206  p09b_1 is 74
1207  p09b_2 is 73
1208  p09b_3 is 72
1209  p09b_4 is 71
1210  prove_p09b is 93
1211  symmetry_of_glb is 87
1212  symmetry_of_lub is 85
1213 Facts
1214  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1215  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1216  Id :   8, {_}:
1217           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1218           [8, 7, 6] by associativity ?6 ?7 ?8
1219  Id :  10, {_}:
1220           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1221           [11, 10] by symmetry_of_glb ?10 ?11
1222  Id :  12, {_}:
1223           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1224           [14, 13] by symmetry_of_lub ?13 ?14
1225  Id :  14, {_}:
1226           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1227           =?=
1228           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1229           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1230  Id :  16, {_}:
1231           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1232           =?=
1233           least_upper_bound (least_upper_bound ?20 ?21) ?22
1234           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1235  Id :  18, {_}:
1236           least_upper_bound ?24 ?24 =>= ?24
1237           [24] by idempotence_of_lub ?24
1238  Id :  20, {_}:
1239           greatest_lower_bound ?26 ?26 =>= ?26
1240           [26] by idempotence_of_gld ?26
1241  Id :  22, {_}:
1242           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1243           [29, 28] by lub_absorbtion ?28 ?29
1244  Id :  24, {_}:
1245           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1246           [32, 31] by glb_absorbtion ?31 ?32
1247  Id :  26, {_}:
1248           multiply ?34 (least_upper_bound ?35 ?36)
1249           =<=
1250           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1251           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1252  Id :  28, {_}:
1253           multiply ?38 (greatest_lower_bound ?39 ?40)
1254           =<=
1255           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1256           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1257  Id :  30, {_}:
1258           multiply (least_upper_bound ?42 ?43) ?44
1259           =<=
1260           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1261           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1262  Id :  32, {_}:
1263           multiply (greatest_lower_bound ?46 ?47) ?48
1264           =<=
1265           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1266           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1267  Id :  34, {_}: greatest_lower_bound identity a =>= identity [] by p09b_1
1268  Id :  36, {_}: greatest_lower_bound identity b =>= identity [] by p09b_2
1269  Id :  38, {_}: greatest_lower_bound identity c =>= identity [] by p09b_3
1270  Id :  40, {_}: greatest_lower_bound a b =>= identity [] by p09b_4
1271 Goal
1272  Id :   2, {_}:
1273           greatest_lower_bound a (multiply b c) =>= greatest_lower_bound a c
1274           [] by prove_p09b
1275 Timeout !
1276 FAILURE in 2472 iterations
1277 GRP181-4
1278 Order
1279  == is 100
1280  _ is 99
1281  a is 98
1282  associativity is 90
1283  associativity_of_glb is 85
1284  associativity_of_lub is 84
1285  b is 97
1286  c is 72
1287  glb_absorbtion is 80
1288  greatest_lower_bound is 89
1289  idempotence_of_gld is 82
1290  idempotence_of_lub is 83
1291  identity is 95
1292  inverse is 92
1293  least_upper_bound is 87
1294  left_identity is 93
1295  left_inverse is 91
1296  lub_absorbtion is 81
1297  monotony_glb1 is 78
1298  monotony_glb2 is 76
1299  monotony_lub1 is 79
1300  monotony_lub2 is 77
1301  multiply is 94
1302  p12x_1 is 75
1303  p12x_2 is 74
1304  p12x_3 is 73
1305  p12x_4 is 71
1306  p12x_5 is 70
1307  p12x_6 is 69
1308  p12x_7 is 68
1309  prove_p12x is 96
1310  symmetry_of_glb is 88
1311  symmetry_of_lub is 86
1312 Facts
1313  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1314  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1315  Id :   8, {_}:
1316           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1317           [8, 7, 6] by associativity ?6 ?7 ?8
1318  Id :  10, {_}:
1319           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1320           [11, 10] by symmetry_of_glb ?10 ?11
1321  Id :  12, {_}:
1322           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1323           [14, 13] by symmetry_of_lub ?13 ?14
1324  Id :  14, {_}:
1325           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1326           =?=
1327           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1328           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1329  Id :  16, {_}:
1330           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1331           =?=
1332           least_upper_bound (least_upper_bound ?20 ?21) ?22
1333           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1334  Id :  18, {_}:
1335           least_upper_bound ?24 ?24 =>= ?24
1336           [24] by idempotence_of_lub ?24
1337  Id :  20, {_}:
1338           greatest_lower_bound ?26 ?26 =>= ?26
1339           [26] by idempotence_of_gld ?26
1340  Id :  22, {_}:
1341           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1342           [29, 28] by lub_absorbtion ?28 ?29
1343  Id :  24, {_}:
1344           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1345           [32, 31] by glb_absorbtion ?31 ?32
1346  Id :  26, {_}:
1347           multiply ?34 (least_upper_bound ?35 ?36)
1348           =<=
1349           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1350           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1351  Id :  28, {_}:
1352           multiply ?38 (greatest_lower_bound ?39 ?40)
1353           =<=
1354           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1355           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1356  Id :  30, {_}:
1357           multiply (least_upper_bound ?42 ?43) ?44
1358           =<=
1359           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1360           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1361  Id :  32, {_}:
1362           multiply (greatest_lower_bound ?46 ?47) ?48
1363           =<=
1364           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1365           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1366  Id :  34, {_}: inverse identity =>= identity [] by p12x_1
1367  Id :  36, {_}: inverse (inverse ?51) =>= ?51 [51] by p12x_2 ?51
1368  Id :  38, {_}:
1369           inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
1370           [54, 53] by p12x_3 ?53 ?54
1371  Id :  40, {_}:
1372           greatest_lower_bound a c =>= greatest_lower_bound b c
1373           [] by p12x_4
1374  Id :  42, {_}: least_upper_bound a c =>= least_upper_bound b c [] by p12x_5
1375  Id :  44, {_}:
1376           inverse (greatest_lower_bound ?58 ?59)
1377           =<=
1378           least_upper_bound (inverse ?58) (inverse ?59)
1379           [59, 58] by p12x_6 ?58 ?59
1380  Id :  46, {_}:
1381           inverse (least_upper_bound ?61 ?62)
1382           =<=
1383           greatest_lower_bound (inverse ?61) (inverse ?62)
1384           [62, 61] by p12x_7 ?61 ?62
1385 Goal
1386  Id :   2, {_}: a =>= b [] by prove_p12x
1387 Timeout !
1388 FAILURE in 1207 iterations
1389 GRP183-4
1390 Order
1391  == is 100
1392  _ is 99
1393  a is 98
1394  associativity is 89
1395  associativity_of_glb is 86
1396  associativity_of_lub is 85
1397  glb_absorbtion is 81
1398  greatest_lower_bound is 94
1399  idempotence_of_gld is 83
1400  idempotence_of_lub is 84
1401  identity is 97
1402  inverse is 95
1403  least_upper_bound is 96
1404  left_identity is 91
1405  left_inverse is 90
1406  lub_absorbtion is 82
1407  monotony_glb1 is 79
1408  monotony_glb2 is 77
1409  monotony_lub1 is 80
1410  monotony_lub2 is 78
1411  multiply is 92
1412  p20x_1 is 76
1413  p20x_3 is 75
1414  prove_20x is 93
1415  symmetry_of_glb is 88
1416  symmetry_of_lub is 87
1417 Facts
1418  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1419  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1420  Id :   8, {_}:
1421           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1422           [8, 7, 6] by associativity ?6 ?7 ?8
1423  Id :  10, {_}:
1424           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1425           [11, 10] by symmetry_of_glb ?10 ?11
1426  Id :  12, {_}:
1427           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1428           [14, 13] by symmetry_of_lub ?13 ?14
1429  Id :  14, {_}:
1430           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1431           =?=
1432           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1433           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1434  Id :  16, {_}:
1435           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1436           =?=
1437           least_upper_bound (least_upper_bound ?20 ?21) ?22
1438           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1439  Id :  18, {_}:
1440           least_upper_bound ?24 ?24 =>= ?24
1441           [24] by idempotence_of_lub ?24
1442  Id :  20, {_}:
1443           greatest_lower_bound ?26 ?26 =>= ?26
1444           [26] by idempotence_of_gld ?26
1445  Id :  22, {_}:
1446           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1447           [29, 28] by lub_absorbtion ?28 ?29
1448  Id :  24, {_}:
1449           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1450           [32, 31] by glb_absorbtion ?31 ?32
1451  Id :  26, {_}:
1452           multiply ?34 (least_upper_bound ?35 ?36)
1453           =<=
1454           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1455           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1456  Id :  28, {_}:
1457           multiply ?38 (greatest_lower_bound ?39 ?40)
1458           =<=
1459           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1460           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1461  Id :  30, {_}:
1462           multiply (least_upper_bound ?42 ?43) ?44
1463           =<=
1464           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1465           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1466  Id :  32, {_}:
1467           multiply (greatest_lower_bound ?46 ?47) ?48
1468           =<=
1469           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1470           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1471  Id :  34, {_}: inverse identity =>= identity [] by p20x_1
1472  Id :  36, {_}: inverse (inverse ?51) =>= ?51 [51] by p20x_1 ?51
1473  Id :  38, {_}:
1474           inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
1475           [54, 53] by p20x_3 ?53 ?54
1476 Goal
1477  Id :   2, {_}:
1478           greatest_lower_bound (least_upper_bound a identity)
1479             (least_upper_bound (inverse a) identity)
1480           =>=
1481           identity
1482           [] by prove_20x
1483 Timeout !
1484 FAILURE in 933 iterations
1485 GRP184-1
1486 Order
1487  == is 100
1488  _ is 99
1489  a is 98
1490  associativity is 89
1491  associativity_of_glb is 86
1492  associativity_of_lub is 85
1493  glb_absorbtion is 81
1494  greatest_lower_bound is 95
1495  idempotence_of_gld is 83
1496  idempotence_of_lub is 84
1497  identity is 97
1498  inverse is 94
1499  least_upper_bound is 96
1500  left_identity is 91
1501  left_inverse is 90
1502  lub_absorbtion is 82
1503  monotony_glb1 is 79
1504  monotony_glb2 is 77
1505  monotony_lub1 is 80
1506  monotony_lub2 is 78
1507  multiply is 93
1508  prove_p21 is 92
1509  symmetry_of_glb is 88
1510  symmetry_of_lub is 87
1511 Facts
1512  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1513  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1514  Id :   8, {_}:
1515           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1516           [8, 7, 6] by associativity ?6 ?7 ?8
1517  Id :  10, {_}:
1518           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1519           [11, 10] by symmetry_of_glb ?10 ?11
1520  Id :  12, {_}:
1521           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1522           [14, 13] by symmetry_of_lub ?13 ?14
1523  Id :  14, {_}:
1524           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1525           =?=
1526           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1527           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1528  Id :  16, {_}:
1529           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1530           =?=
1531           least_upper_bound (least_upper_bound ?20 ?21) ?22
1532           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1533  Id :  18, {_}:
1534           least_upper_bound ?24 ?24 =>= ?24
1535           [24] by idempotence_of_lub ?24
1536  Id :  20, {_}:
1537           greatest_lower_bound ?26 ?26 =>= ?26
1538           [26] by idempotence_of_gld ?26
1539  Id :  22, {_}:
1540           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1541           [29, 28] by lub_absorbtion ?28 ?29
1542  Id :  24, {_}:
1543           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1544           [32, 31] by glb_absorbtion ?31 ?32
1545  Id :  26, {_}:
1546           multiply ?34 (least_upper_bound ?35 ?36)
1547           =<=
1548           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1549           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1550  Id :  28, {_}:
1551           multiply ?38 (greatest_lower_bound ?39 ?40)
1552           =<=
1553           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1554           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1555  Id :  30, {_}:
1556           multiply (least_upper_bound ?42 ?43) ?44
1557           =<=
1558           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1559           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1560  Id :  32, {_}:
1561           multiply (greatest_lower_bound ?46 ?47) ?48
1562           =<=
1563           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1564           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1565 Goal
1566  Id :   2, {_}:
1567           multiply (least_upper_bound a identity)
1568             (inverse (greatest_lower_bound a identity))
1569           =>=
1570           multiply (inverse (greatest_lower_bound a identity))
1571             (least_upper_bound a identity)
1572           [] by prove_p21
1573 Timeout !
1574 FAILURE in 1398 iterations
1575 GRP184-3
1576 Order
1577  == is 100
1578  _ is 99
1579  a is 98
1580  associativity is 89
1581  associativity_of_glb is 86
1582  associativity_of_lub is 85
1583  glb_absorbtion is 81
1584  greatest_lower_bound is 95
1585  idempotence_of_gld is 83
1586  idempotence_of_lub is 84
1587  identity is 97
1588  inverse is 94
1589  least_upper_bound is 96
1590  left_identity is 91
1591  left_inverse is 90
1592  lub_absorbtion is 82
1593  monotony_glb1 is 79
1594  monotony_glb2 is 77
1595  monotony_lub1 is 80
1596  monotony_lub2 is 78
1597  multiply is 93
1598  prove_p21x is 92
1599  symmetry_of_glb is 88
1600  symmetry_of_lub is 87
1601 Facts
1602  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1603  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1604  Id :   8, {_}:
1605           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1606           [8, 7, 6] by associativity ?6 ?7 ?8
1607  Id :  10, {_}:
1608           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1609           [11, 10] by symmetry_of_glb ?10 ?11
1610  Id :  12, {_}:
1611           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1612           [14, 13] by symmetry_of_lub ?13 ?14
1613  Id :  14, {_}:
1614           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1615           =?=
1616           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1617           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1618  Id :  16, {_}:
1619           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1620           =?=
1621           least_upper_bound (least_upper_bound ?20 ?21) ?22
1622           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1623  Id :  18, {_}:
1624           least_upper_bound ?24 ?24 =>= ?24
1625           [24] by idempotence_of_lub ?24
1626  Id :  20, {_}:
1627           greatest_lower_bound ?26 ?26 =>= ?26
1628           [26] by idempotence_of_gld ?26
1629  Id :  22, {_}:
1630           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1631           [29, 28] by lub_absorbtion ?28 ?29
1632  Id :  24, {_}:
1633           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1634           [32, 31] by glb_absorbtion ?31 ?32
1635  Id :  26, {_}:
1636           multiply ?34 (least_upper_bound ?35 ?36)
1637           =<=
1638           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1639           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1640  Id :  28, {_}:
1641           multiply ?38 (greatest_lower_bound ?39 ?40)
1642           =<=
1643           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1644           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1645  Id :  30, {_}:
1646           multiply (least_upper_bound ?42 ?43) ?44
1647           =<=
1648           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1649           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1650  Id :  32, {_}:
1651           multiply (greatest_lower_bound ?46 ?47) ?48
1652           =<=
1653           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1654           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1655 Goal
1656  Id :   2, {_}:
1657           multiply (least_upper_bound a identity)
1658             (inverse (greatest_lower_bound a identity))
1659           =>=
1660           multiply (inverse (greatest_lower_bound a identity))
1661             (least_upper_bound a identity)
1662           [] by prove_p21x
1663 Timeout !
1664 FAILURE in 1398 iterations
1665 GRP185-2
1666 Order
1667  == is 100
1668  _ is 99
1669  a is 98
1670  associativity is 89
1671  associativity_of_glb is 85
1672  associativity_of_lub is 84
1673  b is 97
1674  glb_absorbtion is 80
1675  greatest_lower_bound is 88
1676  idempotence_of_gld is 82
1677  idempotence_of_lub is 83
1678  identity is 95
1679  inverse is 91
1680  least_upper_bound is 94
1681  left_identity is 92
1682  left_inverse is 90
1683  lub_absorbtion is 81
1684  monotony_glb1 is 78
1685  monotony_glb2 is 76
1686  monotony_lub1 is 79
1687  monotony_lub2 is 77
1688  multiply is 96
1689  p22a_1 is 75
1690  p22a_2 is 74
1691  p22a_3 is 73
1692  prove_p22a is 93
1693  symmetry_of_glb is 87
1694  symmetry_of_lub is 86
1695 Facts
1696  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1697  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1698  Id :   8, {_}:
1699           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1700           [8, 7, 6] by associativity ?6 ?7 ?8
1701  Id :  10, {_}:
1702           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1703           [11, 10] by symmetry_of_glb ?10 ?11
1704  Id :  12, {_}:
1705           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1706           [14, 13] by symmetry_of_lub ?13 ?14
1707  Id :  14, {_}:
1708           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1709           =?=
1710           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1711           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1712  Id :  16, {_}:
1713           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1714           =?=
1715           least_upper_bound (least_upper_bound ?20 ?21) ?22
1716           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1717  Id :  18, {_}:
1718           least_upper_bound ?24 ?24 =>= ?24
1719           [24] by idempotence_of_lub ?24
1720  Id :  20, {_}:
1721           greatest_lower_bound ?26 ?26 =>= ?26
1722           [26] by idempotence_of_gld ?26
1723  Id :  22, {_}:
1724           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1725           [29, 28] by lub_absorbtion ?28 ?29
1726  Id :  24, {_}:
1727           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1728           [32, 31] by glb_absorbtion ?31 ?32
1729  Id :  26, {_}:
1730           multiply ?34 (least_upper_bound ?35 ?36)
1731           =<=
1732           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1733           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1734  Id :  28, {_}:
1735           multiply ?38 (greatest_lower_bound ?39 ?40)
1736           =<=
1737           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1738           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1739  Id :  30, {_}:
1740           multiply (least_upper_bound ?42 ?43) ?44
1741           =<=
1742           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1743           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1744  Id :  32, {_}:
1745           multiply (greatest_lower_bound ?46 ?47) ?48
1746           =<=
1747           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1748           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1749  Id :  34, {_}: inverse identity =>= identity [] by p22a_1
1750  Id :  36, {_}: inverse (inverse ?51) =>= ?51 [51] by p22a_2 ?51
1751  Id :  38, {_}:
1752           inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
1753           [54, 53] by p22a_3 ?53 ?54
1754 Goal
1755  Id :   2, {_}:
1756           least_upper_bound (least_upper_bound (multiply a b) identity)
1757             (multiply (least_upper_bound a identity)
1758               (least_upper_bound b identity))
1759           =>=
1760           multiply (least_upper_bound a identity)
1761             (least_upper_bound b identity)
1762           [] by prove_p22a
1763 Timeout !
1764 FAILURE in 944 iterations
1765 GRP185-3
1766 Order
1767  == is 100
1768  _ is 99
1769  a is 98
1770  associativity is 88
1771  associativity_of_glb is 85
1772  associativity_of_lub is 84
1773  b is 97
1774  glb_absorbtion is 80
1775  greatest_lower_bound is 93
1776  idempotence_of_gld is 82
1777  idempotence_of_lub is 83
1778  identity is 95
1779  inverse is 90
1780  least_upper_bound is 94
1781  left_identity is 91
1782  left_inverse is 89
1783  lub_absorbtion is 81
1784  monotony_glb1 is 78
1785  monotony_glb2 is 76
1786  monotony_lub1 is 79
1787  monotony_lub2 is 77
1788  multiply is 96
1789  prove_p22b is 92
1790  symmetry_of_glb is 87
1791  symmetry_of_lub is 86
1792 Facts
1793  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1794  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1795  Id :   8, {_}:
1796           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1797           [8, 7, 6] by associativity ?6 ?7 ?8
1798  Id :  10, {_}:
1799           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1800           [11, 10] by symmetry_of_glb ?10 ?11
1801  Id :  12, {_}:
1802           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1803           [14, 13] by symmetry_of_lub ?13 ?14
1804  Id :  14, {_}:
1805           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1806           =?=
1807           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1808           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1809  Id :  16, {_}:
1810           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1811           =?=
1812           least_upper_bound (least_upper_bound ?20 ?21) ?22
1813           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1814  Id :  18, {_}:
1815           least_upper_bound ?24 ?24 =>= ?24
1816           [24] by idempotence_of_lub ?24
1817  Id :  20, {_}:
1818           greatest_lower_bound ?26 ?26 =>= ?26
1819           [26] by idempotence_of_gld ?26
1820  Id :  22, {_}:
1821           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1822           [29, 28] by lub_absorbtion ?28 ?29
1823  Id :  24, {_}:
1824           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1825           [32, 31] by glb_absorbtion ?31 ?32
1826  Id :  26, {_}:
1827           multiply ?34 (least_upper_bound ?35 ?36)
1828           =<=
1829           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1830           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1831  Id :  28, {_}:
1832           multiply ?38 (greatest_lower_bound ?39 ?40)
1833           =<=
1834           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1835           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1836  Id :  30, {_}:
1837           multiply (least_upper_bound ?42 ?43) ?44
1838           =<=
1839           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1840           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1841  Id :  32, {_}:
1842           multiply (greatest_lower_bound ?46 ?47) ?48
1843           =<=
1844           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1845           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1846 Goal
1847  Id :   2, {_}:
1848           greatest_lower_bound (least_upper_bound (multiply a b) identity)
1849             (multiply (least_upper_bound a identity)
1850               (least_upper_bound b identity))
1851           =>=
1852           least_upper_bound (multiply a b) identity
1853           [] by prove_p22b
1854 Timeout !
1855 FAILURE in 1232 iterations
1856 GRP186-1
1857 Order
1858  == is 100
1859  _ is 99
1860  a is 98
1861  associativity is 88
1862  associativity_of_glb is 85
1863  associativity_of_lub is 84
1864  b is 97
1865  glb_absorbtion is 80
1866  greatest_lower_bound is 92
1867  idempotence_of_gld is 82
1868  idempotence_of_lub is 83
1869  identity is 95
1870  inverse is 93
1871  least_upper_bound is 94
1872  left_identity is 90
1873  left_inverse is 89
1874  lub_absorbtion is 81
1875  monotony_glb1 is 78
1876  monotony_glb2 is 76
1877  monotony_lub1 is 79
1878  monotony_lub2 is 77
1879  multiply is 96
1880  prove_p23 is 91
1881  symmetry_of_glb is 87
1882  symmetry_of_lub is 86
1883 Facts
1884  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1885  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1886  Id :   8, {_}:
1887           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1888           [8, 7, 6] by associativity ?6 ?7 ?8
1889  Id :  10, {_}:
1890           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1891           [11, 10] by symmetry_of_glb ?10 ?11
1892  Id :  12, {_}:
1893           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1894           [14, 13] by symmetry_of_lub ?13 ?14
1895  Id :  14, {_}:
1896           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1897           =?=
1898           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1899           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1900  Id :  16, {_}:
1901           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1902           =?=
1903           least_upper_bound (least_upper_bound ?20 ?21) ?22
1904           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1905  Id :  18, {_}:
1906           least_upper_bound ?24 ?24 =>= ?24
1907           [24] by idempotence_of_lub ?24
1908  Id :  20, {_}:
1909           greatest_lower_bound ?26 ?26 =>= ?26
1910           [26] by idempotence_of_gld ?26
1911  Id :  22, {_}:
1912           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1913           [29, 28] by lub_absorbtion ?28 ?29
1914  Id :  24, {_}:
1915           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1916           [32, 31] by glb_absorbtion ?31 ?32
1917  Id :  26, {_}:
1918           multiply ?34 (least_upper_bound ?35 ?36)
1919           =<=
1920           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1921           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1922  Id :  28, {_}:
1923           multiply ?38 (greatest_lower_bound ?39 ?40)
1924           =<=
1925           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1926           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1927  Id :  30, {_}:
1928           multiply (least_upper_bound ?42 ?43) ?44
1929           =<=
1930           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1931           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1932  Id :  32, {_}:
1933           multiply (greatest_lower_bound ?46 ?47) ?48
1934           =<=
1935           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1936           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1937 Goal
1938  Id :   2, {_}:
1939           least_upper_bound (multiply a b) identity
1940           =<=
1941           multiply a (inverse (greatest_lower_bound a (inverse b)))
1942           [] by prove_p23
1943 Timeout !
1944 FAILURE in 1205 iterations
1945 GRP186-2
1946 Order
1947  == is 100
1948  _ is 99
1949  a is 98
1950  associativity is 88
1951  associativity_of_glb is 85
1952  associativity_of_lub is 84
1953  b is 97
1954  glb_absorbtion is 80
1955  greatest_lower_bound is 92
1956  idempotence_of_gld is 82
1957  idempotence_of_lub is 83
1958  identity is 95
1959  inverse is 93
1960  least_upper_bound is 94
1961  left_identity is 90
1962  left_inverse is 89
1963  lub_absorbtion is 81
1964  monotony_glb1 is 78
1965  monotony_glb2 is 76
1966  monotony_lub1 is 79
1967  monotony_lub2 is 77
1968  multiply is 96
1969  p23_1 is 75
1970  p23_2 is 74
1971  p23_3 is 73
1972  prove_p23 is 91
1973  symmetry_of_glb is 87
1974  symmetry_of_lub is 86
1975 Facts
1976  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1977  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1978  Id :   8, {_}:
1979           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1980           [8, 7, 6] by associativity ?6 ?7 ?8
1981  Id :  10, {_}:
1982           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1983           [11, 10] by symmetry_of_glb ?10 ?11
1984  Id :  12, {_}:
1985           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1986           [14, 13] by symmetry_of_lub ?13 ?14
1987  Id :  14, {_}:
1988           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1989           =?=
1990           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1991           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1992  Id :  16, {_}:
1993           least_upper_bound ?20 (least_upper_bound ?21 ?22)
1994           =?=
1995           least_upper_bound (least_upper_bound ?20 ?21) ?22
1996           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1997  Id :  18, {_}:
1998           least_upper_bound ?24 ?24 =>= ?24
1999           [24] by idempotence_of_lub ?24
2000  Id :  20, {_}:
2001           greatest_lower_bound ?26 ?26 =>= ?26
2002           [26] by idempotence_of_gld ?26
2003  Id :  22, {_}:
2004           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
2005           [29, 28] by lub_absorbtion ?28 ?29
2006  Id :  24, {_}:
2007           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
2008           [32, 31] by glb_absorbtion ?31 ?32
2009  Id :  26, {_}:
2010           multiply ?34 (least_upper_bound ?35 ?36)
2011           =<=
2012           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
2013           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
2014  Id :  28, {_}:
2015           multiply ?38 (greatest_lower_bound ?39 ?40)
2016           =<=
2017           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
2018           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
2019  Id :  30, {_}:
2020           multiply (least_upper_bound ?42 ?43) ?44
2021           =<=
2022           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
2023           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
2024  Id :  32, {_}:
2025           multiply (greatest_lower_bound ?46 ?47) ?48
2026           =<=
2027           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
2028           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
2029  Id :  34, {_}: inverse identity =>= identity [] by p23_1
2030  Id :  36, {_}: inverse (inverse ?51) =>= ?51 [51] by p23_2 ?51
2031  Id :  38, {_}:
2032           inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
2033           [54, 53] by p23_3 ?53 ?54
2034 Goal
2035  Id :   2, {_}:
2036           least_upper_bound (multiply a b) identity
2037           =<=
2038           multiply a (inverse (greatest_lower_bound a (inverse b)))
2039           [] by prove_p23
2040 Timeout !
2041 FAILURE in 964 iterations
2042 GRP187-1
2043 Order
2044  == is 100
2045  _ is 99
2046  a is 98
2047  associativity is 90
2048  associativity_of_glb is 85
2049  associativity_of_lub is 84
2050  b is 97
2051  glb_absorbtion is 80
2052  greatest_lower_bound is 89
2053  idempotence_of_gld is 82
2054  idempotence_of_lub is 83
2055  identity is 94
2056  inverse is 92
2057  least_upper_bound is 87
2058  left_identity is 93
2059  left_inverse is 91
2060  lub_absorbtion is 81
2061  monotony_glb1 is 78
2062  monotony_glb2 is 76
2063  monotony_lub1 is 79
2064  monotony_lub2 is 77
2065  multiply is 96
2066  p33_1 is 75
2067  prove_p33 is 95
2068  symmetry_of_glb is 88
2069  symmetry_of_lub is 86
2070 Facts
2071  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
2072  Id :   6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
2073  Id :   8, {_}:
2074           multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
2075           [8, 7, 6] by associativity ?6 ?7 ?8
2076  Id :  10, {_}:
2077           greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
2078           [11, 10] by symmetry_of_glb ?10 ?11
2079  Id :  12, {_}:
2080           least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
2081           [14, 13] by symmetry_of_lub ?13 ?14
2082  Id :  14, {_}:
2083           greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
2084           =?=
2085           greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
2086           [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
2087  Id :  16, {_}:
2088           least_upper_bound ?20 (least_upper_bound ?21 ?22)
2089           =?=
2090           least_upper_bound (least_upper_bound ?20 ?21) ?22
2091           [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
2092  Id :  18, {_}:
2093           least_upper_bound ?24 ?24 =>= ?24
2094           [24] by idempotence_of_lub ?24
2095  Id :  20, {_}:
2096           greatest_lower_bound ?26 ?26 =>= ?26
2097           [26] by idempotence_of_gld ?26
2098  Id :  22, {_}:
2099           least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
2100           [29, 28] by lub_absorbtion ?28 ?29
2101  Id :  24, {_}:
2102           greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
2103           [32, 31] by glb_absorbtion ?31 ?32
2104  Id :  26, {_}:
2105           multiply ?34 (least_upper_bound ?35 ?36)
2106           =<=
2107           least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
2108           [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
2109  Id :  28, {_}:
2110           multiply ?38 (greatest_lower_bound ?39 ?40)
2111           =<=
2112           greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
2113           [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
2114  Id :  30, {_}:
2115           multiply (least_upper_bound ?42 ?43) ?44
2116           =<=
2117           least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
2118           [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
2119  Id :  32, {_}:
2120           multiply (greatest_lower_bound ?46 ?47) ?48
2121           =<=
2122           greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
2123           [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
2124  Id :  34, {_}:
2125           greatest_lower_bound (least_upper_bound a (inverse a))
2126             (least_upper_bound b (inverse b))
2127           =>=
2128           identity
2129           [] by p33_1
2130 Goal
2131  Id :   2, {_}: multiply a b =>= multiply b a [] by prove_p33
2132 Timeout !
2133 FAILURE in 1541 iterations
2134 GRP200-1
2135 Order
2136  == is 100
2137  _ is 99
2138  a is 98
2139  b is 97
2140  c is 95
2141  identity is 93
2142  left_division is 90
2143  left_division_multiply is 88
2144  left_identity is 92
2145  left_inverse is 83
2146  moufang1 is 82
2147  multiply is 96
2148  multiply_left_division is 89
2149  multiply_right_division is 86
2150  prove_moufang2 is 94
2151  right_division is 87
2152  right_division_multiply is 85
2153  right_identity is 91
2154  right_inverse is 84
2155 Facts
2156  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
2157  Id :   6, {_}: multiply ?4 identity =>= ?4 [4] by right_identity ?4
2158  Id :   8, {_}:
2159           multiply ?6 (left_division ?6 ?7) =>= ?7
2160           [7, 6] by multiply_left_division ?6 ?7
2161  Id :  10, {_}:
2162           left_division ?9 (multiply ?9 ?10) =>= ?10
2163           [10, 9] by left_division_multiply ?9 ?10
2164  Id :  12, {_}:
2165           multiply (right_division ?12 ?13) ?13 =>= ?12
2166           [13, 12] by multiply_right_division ?12 ?13
2167  Id :  14, {_}:
2168           right_division (multiply ?15 ?16) ?16 =>= ?15
2169           [16, 15] by right_division_multiply ?15 ?16
2170  Id :  16, {_}:
2171           multiply ?18 (right_inverse ?18) =>= identity
2172           [18] by right_inverse ?18
2173  Id :  18, {_}:
2174           multiply (left_inverse ?20) ?20 =>= identity
2175           [20] by left_inverse ?20
2176  Id :  20, {_}:
2177           multiply (multiply ?22 (multiply ?23 ?24)) ?22
2178           =?=
2179           multiply (multiply ?22 ?23) (multiply ?24 ?22)
2180           [24, 23, 22] by moufang1 ?22 ?23 ?24
2181 Goal
2182  Id :   2, {_}:
2183           multiply (multiply (multiply a b) c) b
2184           =>=
2185           multiply a (multiply b (multiply c b))
2186           [] by prove_moufang2
2187 Timeout !
2188 FAILURE in 712 iterations
2189 GRP202-1
2190 Order
2191  == is 100
2192  _ is 99
2193  a is 98
2194  b is 97
2195  c is 96
2196  identity is 93
2197  left_division is 90
2198  left_division_multiply is 88
2199  left_identity is 92
2200  left_inverse is 83
2201  moufang3 is 82
2202  multiply is 95
2203  multiply_left_division is 89
2204  multiply_right_division is 86
2205  prove_moufang1 is 94
2206  right_division is 87
2207  right_division_multiply is 85
2208  right_identity is 91
2209  right_inverse is 84
2210 Facts
2211  Id :   4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
2212  Id :   6, {_}: multiply ?4 identity =>= ?4 [4] by right_identity ?4
2213  Id :   8, {_}:
2214           multiply ?6 (left_division ?6 ?7) =>= ?7
2215           [7, 6] by multiply_left_division ?6 ?7
2216  Id :  10, {_}:
2217           left_division ?9 (multiply ?9 ?10) =>= ?10
2218           [10, 9] by left_division_multiply ?9 ?10
2219  Id :  12, {_}:
2220           multiply (right_division ?12 ?13) ?13 =>= ?12
2221           [13, 12] by multiply_right_division ?12 ?13
2222  Id :  14, {_}:
2223           right_division (multiply ?15 ?16) ?16 =>= ?15
2224           [16, 15] by right_division_multiply ?15 ?16
2225  Id :  16, {_}:
2226           multiply ?18 (right_inverse ?18) =>= identity
2227           [18] by right_inverse ?18
2228  Id :  18, {_}:
2229           multiply (left_inverse ?20) ?20 =>= identity
2230           [20] by left_inverse ?20
2231  Id :  20, {_}:
2232           multiply (multiply (multiply ?22 ?23) ?22) ?24
2233           =?=
2234           multiply ?22 (multiply ?23 (multiply ?22 ?24))
2235           [24, 23, 22] by moufang3 ?22 ?23 ?24
2236 Goal
2237  Id :   2, {_}:
2238           multiply (multiply a (multiply b c)) a
2239           =>=
2240           multiply (multiply a b) (multiply c a)
2241           [] by prove_moufang1
2242 Timeout !
2243 FAILURE in 674 iterations
2244 GRP404-1
2245 Order
2246  == is 100
2247  _ is 99
2248  a2 is 95
2249  b2 is 98
2250  inverse is 97
2251  multiply is 96
2252  prove_these_axioms_2 is 94
2253  single_axiom is 93
2254 Facts
2255  Id :   4, {_}:
2256           multiply ?2
2257             (inverse
2258               (multiply (inverse (multiply (inverse (multiply ?2 ?3)) ?4))
2259                 (inverse (multiply ?3 (multiply (inverse ?3) ?3)))))
2260           =>=
2261           ?4
2262           [4, 3, 2] by single_axiom ?2 ?3 ?4
2263 Goal
2264  Id :   2, {_}:
2265           multiply (multiply (inverse b2) b2) a2 =>= a2
2266           [] by prove_these_axioms_2
2267 Timeout !
2268 FAILURE in 342 iterations
2269 GRP405-1
2270 Order
2271  == is 100
2272  _ is 99
2273  a3 is 98
2274  b3 is 97
2275  c3 is 95
2276  inverse is 93
2277  multiply is 96
2278  prove_these_axioms_3 is 94
2279  single_axiom is 92
2280 Facts
2281  Id :   4, {_}:
2282           multiply ?2
2283             (inverse
2284               (multiply (inverse (multiply (inverse (multiply ?2 ?3)) ?4))
2285                 (inverse (multiply ?3 (multiply (inverse ?3) ?3)))))
2286           =>=
2287           ?4
2288           [4, 3, 2] by single_axiom ?2 ?3 ?4
2289 Goal
2290  Id :   2, {_}:
2291           multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2292           [] by prove_these_axioms_3
2293 Found proof, 234.971871s
2294 GRP422-1
2295 Order
2296  == is 100
2297  _ is 99
2298  a2 is 95
2299  b2 is 98
2300  inverse is 97
2301  multiply is 96
2302  prove_these_axioms_2 is 94
2303  single_axiom is 93
2304 Facts
2305  Id :   4, {_}:
2306           inverse
2307             (multiply
2308               (inverse
2309                 (multiply ?2
2310                   (inverse
2311                     (multiply (inverse ?3)
2312                       (multiply (inverse ?4)
2313                         (inverse (multiply (inverse ?4) ?4)))))))
2314               (multiply ?2 ?4))
2315           =>=
2316           ?3
2317           [4, 3, 2] by single_axiom ?2 ?3 ?4
2318 Goal
2319  Id :   2, {_}:
2320           multiply (multiply (inverse b2) b2) a2 =>= a2
2321           [] by prove_these_axioms_2
2322 Found proof, 14.541466s
2323 GRP423-1
2324 Order
2325  == is 100
2326  _ is 99
2327  a3 is 98
2328  b3 is 97
2329  c3 is 95
2330  inverse is 93
2331  multiply is 96
2332  prove_these_axioms_3 is 94
2333  single_axiom is 92
2334 Facts
2335  Id :   4, {_}:
2336           inverse
2337             (multiply
2338               (inverse
2339                 (multiply ?2
2340                   (inverse
2341                     (multiply (inverse ?3)
2342                       (multiply (inverse ?4)
2343                         (inverse (multiply (inverse ?4) ?4)))))))
2344               (multiply ?2 ?4))
2345           =>=
2346           ?3
2347           [4, 3, 2] by single_axiom ?2 ?3 ?4
2348 Goal
2349  Id :   2, {_}:
2350           multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2351           [] by prove_these_axioms_3
2352 Found proof, 12.056212s
2353 GRP444-1
2354 Order
2355  == is 100
2356  _ is 99
2357  a3 is 98
2358  b3 is 97
2359  c3 is 95
2360  inverse is 93
2361  multiply is 96
2362  prove_these_axioms_3 is 94
2363  single_axiom is 92
2364 Facts
2365  Id :   4, {_}:
2366           inverse
2367             (multiply ?2
2368               (multiply ?3
2369                 (multiply (multiply ?4 (inverse ?4))
2370                   (inverse (multiply ?5 (multiply ?2 ?3))))))
2371           =>=
2372           ?5
2373           [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
2374 Goal
2375  Id :   2, {_}:
2376           multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2377           [] by prove_these_axioms_3
2378 Found proof, 21.164993s
2379 GRP452-1
2380 Order
2381  == is 100
2382  _ is 99
2383  a2 is 95
2384  b2 is 98
2385  divide is 93
2386  inverse is 97
2387  multiply is 96
2388  prove_these_axioms_2 is 94
2389  single_axiom is 92
2390 Facts
2391  Id :   4, {_}:
2392           divide
2393             (divide (divide ?2 ?2)
2394               (divide ?2 (divide ?3 (divide (divide (divide ?2 ?2) ?2) ?4))))
2395             ?4
2396           =>=
2397           ?3
2398           [4, 3, 2] by single_axiom ?2 ?3 ?4
2399  Id :   6, {_}:
2400           multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7)
2401           [8, 7, 6] by multiply ?6 ?7 ?8
2402  Id :   8, {_}:
2403           inverse ?10 =<= divide (divide ?11 ?11) ?10
2404           [11, 10] by inverse ?10 ?11
2405 Goal
2406  Id :   2, {_}:
2407           multiply (multiply (inverse b2) b2) a2 =>= a2
2408           [] by prove_these_axioms_2
2409 Found proof, 0.549585s
2410 GRP453-1
2411 Order
2412  == is 100
2413  _ is 99
2414  a3 is 98
2415  b3 is 97
2416  c3 is 95
2417  divide is 93
2418  inverse is 91
2419  multiply is 96
2420  prove_these_axioms_3 is 94
2421  single_axiom is 92
2422 Facts
2423  Id :   4, {_}:
2424           divide
2425             (divide (divide ?2 ?2)
2426               (divide ?2 (divide ?3 (divide (divide (divide ?2 ?2) ?2) ?4))))
2427             ?4
2428           =>=
2429           ?3
2430           [4, 3, 2] by single_axiom ?2 ?3 ?4
2431  Id :   6, {_}:
2432           multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7)
2433           [8, 7, 6] by multiply ?6 ?7 ?8
2434  Id :   8, {_}:
2435           inverse ?10 =<= divide (divide ?11 ?11) ?10
2436           [11, 10] by inverse ?10 ?11
2437 Goal
2438  Id :   2, {_}:
2439           multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2440           [] by prove_these_axioms_3
2441 Found proof, 0.716819s
2442 GRP471-1
2443 Order
2444  == is 100
2445  _ is 99
2446  a3 is 98
2447  b3 is 97
2448  c3 is 95
2449  divide is 93
2450  inverse is 92
2451  multiply is 96
2452  prove_these_axioms_3 is 94
2453  single_axiom is 91
2454 Facts
2455  Id :   4, {_}:
2456           divide (inverse (divide ?2 (divide ?3 (divide ?4 ?5))))
2457             (divide (divide ?5 ?4) ?2)
2458           =>=
2459           ?3
2460           [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
2461  Id :   6, {_}:
2462           multiply ?7 ?8 =<= divide ?7 (inverse ?8)
2463           [8, 7] by multiply ?7 ?8
2464 Goal
2465  Id :   2, {_}:
2466           multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2467           [] by prove_these_axioms_3
2468 Found proof, 115.504740s
2469 GRP477-1
2470 Order
2471  == is 100
2472  _ is 99
2473  a3 is 98
2474  b3 is 97
2475  c3 is 95
2476  divide is 93
2477  inverse is 92
2478  multiply is 96
2479  prove_these_axioms_3 is 94
2480  single_axiom is 91
2481 Facts
2482  Id :   4, {_}:
2483           divide (inverse (divide (divide (divide ?2 ?3) ?4) (divide ?5 ?4)))
2484             (divide ?3 ?2)
2485           =>=
2486           ?5
2487           [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
2488  Id :   6, {_}:
2489           multiply ?7 ?8 =<= divide ?7 (inverse ?8)
2490           [8, 7] by multiply ?7 ?8
2491 Goal
2492  Id :   2, {_}:
2493           multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2494           [] by prove_these_axioms_3
2495 Found proof, 11.020022s
2496 GRP506-1
2497 Order
2498  == is 100
2499  _ is 99
2500  a2 is 95
2501  b2 is 98
2502  inverse is 97
2503  multiply is 96
2504  prove_these_axioms_2 is 94
2505  single_axiom is 93
2506 Facts
2507  Id :   4, {_}:
2508           multiply
2509             (inverse
2510               (multiply
2511                 (inverse
2512                   (multiply (inverse (multiply ?2 ?3)) (multiply ?3 ?2)))
2513                 (multiply (inverse (multiply ?4 ?5))
2514                   (multiply ?4
2515                     (inverse
2516                       (multiply (multiply ?6 (inverse ?7)) (inverse ?5)))))))
2517             ?7
2518           =>=
2519           ?6
2520           [7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7
2521 Goal
2522  Id :   2, {_}:
2523           multiply (multiply (inverse b2) b2) a2 =>= a2
2524           [] by prove_these_axioms_2
2525 Timeout !
2526 FAILURE in 184 iterations
2527 GRP508-1
2528 Order
2529  == is 100
2530  _ is 99
2531  a is 98
2532  b is 97
2533  inverse is 94
2534  multiply is 96
2535  prove_these_axioms_4 is 95
2536  single_axiom is 93
2537 Facts
2538  Id :   4, {_}:
2539           multiply
2540             (inverse
2541               (multiply
2542                 (inverse
2543                   (multiply (inverse (multiply ?2 ?3)) (multiply ?3 ?2)))
2544                 (multiply (inverse (multiply ?4 ?5))
2545                   (multiply ?4
2546                     (inverse
2547                       (multiply (multiply ?6 (inverse ?7)) (inverse ?5)))))))
2548             ?7
2549           =>=
2550           ?6
2551           [7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7
2552 Goal
2553  Id :   2, {_}: multiply a b =>= multiply b a [] by prove_these_axioms_4
2554 Timeout !
2555 FAILURE in 183 iterations
2556 LAT080-1
2557 Order
2558  == is 100
2559  _ is 99
2560  a is 98
2561  join is 95
2562  meet is 97
2563  prove_normal_axioms_1 is 96
2564  single_axiom is 94
2565 Facts
2566  Id :   4, {_}:
2567           join (meet (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4)
2568             (meet
2569               (join (meet ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))
2570                 (meet
2571                   (join
2572                     (meet ?3
2573                       (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))
2574                     (meet ?8
2575                       (join ?3
2576                         (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))))
2577                   (join ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))))
2578               (join (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4))
2579           =>=
2580           ?3
2581           [8, 7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7 ?8
2582 Goal
2583  Id :   2, {_}: meet a a =>= a [] by prove_normal_axioms_1
2584 Found proof, 13.776911s
2585 LAT087-1
2586 Order
2587  == is 100
2588  _ is 99
2589  a is 98
2590  b is 97
2591  join is 95
2592  meet is 96
2593  prove_normal_axioms_8 is 94
2594  single_axiom is 93
2595 Facts
2596  Id :   4, {_}:
2597           join (meet (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4)
2598             (meet
2599               (join (meet ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))
2600                 (meet
2601                   (join
2602                     (meet ?3
2603                       (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))
2604                     (meet ?8
2605                       (join ?3
2606                         (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))))
2607                   (join ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))))
2608               (join (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4))
2609           =>=
2610           ?3
2611           [8, 7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7 ?8
2612 Goal
2613  Id :   2, {_}: join a (meet a b) =>= a [] by prove_normal_axioms_8
2614 Found proof, 13.866156s
2615 LAT093-1
2616 Order
2617  == is 100
2618  _ is 99
2619  a is 97
2620  b is 98
2621  join is 94
2622  meet is 96
2623  prove_wal_axioms_2 is 95
2624  single_axiom is 93
2625 Facts
2626  Id :   4, {_}:
2627           join (meet (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4)
2628             (meet
2629               (join (meet ?2 (join (join (meet ?3 ?5) (meet ?6 ?3)) ?3))
2630                 (meet
2631                   (join (meet ?3 (meet (meet (join ?3 ?5) (join ?6 ?3)) ?3))
2632                     (meet ?7
2633                       (join ?3 (meet (meet (join ?3 ?5) (join ?6 ?3)) ?3))))
2634                   (join ?2 (join (join (meet ?3 ?5) (meet ?6 ?3)) ?3))))
2635               (join (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4))
2636           =>=
2637           ?3
2638           [7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7
2639 Goal
2640  Id :   2, {_}: meet b a =>= meet a b [] by prove_wal_axioms_2
2641 Found proof, 13.533964s
2642 LAT138-1
2643 Order
2644  == is 100
2645  _ is 99
2646  a is 98
2647  absorption1 is 90
2648  absorption2 is 89
2649  associativity_of_join is 85
2650  associativity_of_meet is 86
2651  b is 97
2652  c is 96
2653  commutativity_of_join is 87
2654  commutativity_of_meet is 88
2655  equation_H7 is 84
2656  idempotence_of_join is 91
2657  idempotence_of_meet is 92
2658  join is 94
2659  meet is 95
2660  prove_H6 is 93
2661 Facts
2662  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2663  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2664  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2665  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2666  Id :  12, {_}:
2667           meet ?12 ?13 =?= meet ?13 ?12
2668           [13, 12] by commutativity_of_meet ?12 ?13
2669  Id :  14, {_}:
2670           join ?15 ?16 =?= join ?16 ?15
2671           [16, 15] by commutativity_of_join ?15 ?16
2672  Id :  16, {_}:
2673           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2674           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2675  Id :  18, {_}:
2676           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2677           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2678  Id :  20, {_}:
2679           meet ?26 (join ?27 (meet ?26 ?28))
2680           =<=
2681           meet ?26
2682             (join ?27
2683               (meet ?26 (join (meet ?26 ?27) (meet ?28 (join ?26 ?27)))))
2684           [28, 27, 26] by equation_H7 ?26 ?27 ?28
2685 Goal
2686  Id :   2, {_}:
2687           meet a (join b (meet a c))
2688           =<=
2689           meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
2690           [] by prove_H6
2691 Timeout !
2692 FAILURE in 250 iterations
2693 LAT140-1
2694 Order
2695  == is 100
2696  _ is 99
2697  a is 98
2698  absorption1 is 90
2699  absorption2 is 89
2700  associativity_of_join is 85
2701  associativity_of_meet is 86
2702  b is 97
2703  c is 96
2704  commutativity_of_join is 87
2705  commutativity_of_meet is 88
2706  equation_H21 is 84
2707  idempotence_of_join is 91
2708  idempotence_of_meet is 92
2709  join is 94
2710  meet is 95
2711  prove_H2 is 93
2712 Facts
2713  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2714  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2715  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2716  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2717  Id :  12, {_}:
2718           meet ?12 ?13 =?= meet ?13 ?12
2719           [13, 12] by commutativity_of_meet ?12 ?13
2720  Id :  14, {_}:
2721           join ?15 ?16 =?= join ?16 ?15
2722           [16, 15] by commutativity_of_join ?15 ?16
2723  Id :  16, {_}:
2724           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2725           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2726  Id :  18, {_}:
2727           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2728           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2729  Id :  20, {_}:
2730           join (meet ?26 ?27) (meet ?26 ?28)
2731           =<=
2732           meet ?26
2733             (join (meet ?27 (join ?26 (meet ?27 ?28)))
2734               (meet ?28 (join ?26 ?27)))
2735           [28, 27, 26] by equation_H21 ?26 ?27 ?28
2736 Goal
2737  Id :   2, {_}:
2738           meet a (join b (meet a c))
2739           =<=
2740           meet a (join b (meet c (join (meet a (join b c)) (meet b c))))
2741           [] by prove_H2
2742 Timeout !
2743 FAILURE in 250 iterations
2744 LAT146-1
2745 Order
2746  == is 100
2747  _ is 99
2748  a is 98
2749  absorption1 is 89
2750  absorption2 is 88
2751  associativity_of_join is 84
2752  associativity_of_meet is 85
2753  b is 97
2754  c is 96
2755  commutativity_of_join is 86
2756  commutativity_of_meet is 87
2757  d is 95
2758  equation_H34 is 83
2759  idempotence_of_join is 90
2760  idempotence_of_meet is 91
2761  join is 93
2762  meet is 94
2763  prove_H28 is 92
2764 Facts
2765  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2766  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2767  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2768  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2769  Id :  12, {_}:
2770           meet ?12 ?13 =?= meet ?13 ?12
2771           [13, 12] by commutativity_of_meet ?12 ?13
2772  Id :  14, {_}:
2773           join ?15 ?16 =?= join ?16 ?15
2774           [16, 15] by commutativity_of_join ?15 ?16
2775  Id :  16, {_}:
2776           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2777           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2778  Id :  18, {_}:
2779           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2780           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2781  Id :  20, {_}:
2782           meet ?26 (join ?27 (meet ?28 ?29))
2783           =<=
2784           meet ?26 (join ?27 (meet ?28 (join ?27 (meet ?29 (join ?27 ?28)))))
2785           [29, 28, 27, 26] by equation_H34 ?26 ?27 ?28 ?29
2786 Goal
2787  Id :   2, {_}:
2788           meet a (join b (meet a (meet c d)))
2789           =<=
2790           meet a (join b (meet c (meet d (join a (meet b d)))))
2791           [] by prove_H28
2792 Timeout !
2793 FAILURE in 250 iterations
2794 LAT148-1
2795 Order
2796  == is 100
2797  _ is 99
2798  a is 98
2799  absorption1 is 90
2800  absorption2 is 89
2801  associativity_of_join is 85
2802  associativity_of_meet is 86
2803  b is 97
2804  c is 96
2805  commutativity_of_join is 87
2806  commutativity_of_meet is 88
2807  equation_H34 is 84
2808  idempotence_of_join is 91
2809  idempotence_of_meet is 92
2810  join is 94
2811  meet is 95
2812  prove_H7 is 93
2813 Facts
2814  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2815  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2816  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2817  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2818  Id :  12, {_}:
2819           meet ?12 ?13 =?= meet ?13 ?12
2820           [13, 12] by commutativity_of_meet ?12 ?13
2821  Id :  14, {_}:
2822           join ?15 ?16 =?= join ?16 ?15
2823           [16, 15] by commutativity_of_join ?15 ?16
2824  Id :  16, {_}:
2825           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2826           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2827  Id :  18, {_}:
2828           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2829           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2830  Id :  20, {_}:
2831           meet ?26 (join ?27 (meet ?28 ?29))
2832           =<=
2833           meet ?26 (join ?27 (meet ?28 (join ?27 (meet ?29 (join ?27 ?28)))))
2834           [29, 28, 27, 26] by equation_H34 ?26 ?27 ?28 ?29
2835 Goal
2836  Id :   2, {_}:
2837           meet a (join b (meet a c))
2838           =<=
2839           meet a (join b (meet a (join (meet a b) (meet c (join a b)))))
2840           [] by prove_H7
2841 Timeout !
2842 FAILURE in 250 iterations
2843 LAT152-1
2844 Order
2845  == is 100
2846  _ is 99
2847  a is 98
2848  absorption1 is 90
2849  absorption2 is 89
2850  associativity_of_join is 85
2851  associativity_of_meet is 86
2852  b is 97
2853  c is 96
2854  commutativity_of_join is 87
2855  commutativity_of_meet is 88
2856  equation_H40 is 84
2857  idempotence_of_join is 91
2858  idempotence_of_meet is 92
2859  join is 94
2860  meet is 95
2861  prove_H6 is 93
2862 Facts
2863  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2864  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2865  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2866  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2867  Id :  12, {_}:
2868           meet ?12 ?13 =?= meet ?13 ?12
2869           [13, 12] by commutativity_of_meet ?12 ?13
2870  Id :  14, {_}:
2871           join ?15 ?16 =?= join ?16 ?15
2872           [16, 15] by commutativity_of_join ?15 ?16
2873  Id :  16, {_}:
2874           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2875           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2876  Id :  18, {_}:
2877           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2878           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2879  Id :  20, {_}:
2880           meet ?26 (join ?27 (meet ?28 (join ?26 ?29)))
2881           =<=
2882           meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?28 (join ?26 ?27)))))
2883           [29, 28, 27, 26] by equation_H40 ?26 ?27 ?28 ?29
2884 Goal
2885  Id :   2, {_}:
2886           meet a (join b (meet a c))
2887           =<=
2888           meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
2889           [] by prove_H6
2890 Timeout !
2891 FAILURE in 249 iterations
2892 LAT156-1
2893 Order
2894  == is 100
2895  _ is 99
2896  a is 98
2897  absorption1 is 90
2898  absorption2 is 89
2899  associativity_of_join is 85
2900  associativity_of_meet is 86
2901  b is 97
2902  c is 96
2903  commutativity_of_join is 87
2904  commutativity_of_meet is 88
2905  equation_H49 is 84
2906  idempotence_of_join is 91
2907  idempotence_of_meet is 92
2908  join is 94
2909  meet is 95
2910  prove_H6 is 93
2911 Facts
2912  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2913  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2914  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2915  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2916  Id :  12, {_}:
2917           meet ?12 ?13 =?= meet ?13 ?12
2918           [13, 12] by commutativity_of_meet ?12 ?13
2919  Id :  14, {_}:
2920           join ?15 ?16 =?= join ?16 ?15
2921           [16, 15] by commutativity_of_join ?15 ?16
2922  Id :  16, {_}:
2923           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2924           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2925  Id :  18, {_}:
2926           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2927           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2928  Id :  20, {_}:
2929           meet ?26 (join ?27 (meet ?28 (join ?26 ?29)))
2930           =<=
2931           meet ?26 (join ?27 (join (meet ?26 ?28) (meet ?28 (join ?27 ?29))))
2932           [29, 28, 27, 26] by equation_H49 ?26 ?27 ?28 ?29
2933 Goal
2934  Id :   2, {_}:
2935           meet a (join b (meet a c))
2936           =<=
2937           meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
2938           [] by prove_H6
2939 Timeout !
2940 FAILURE in 249 iterations
2941 LAT159-1
2942 Order
2943  == is 100
2944  _ is 99
2945  a is 98
2946  absorption1 is 90
2947  absorption2 is 89
2948  associativity_of_join is 85
2949  associativity_of_meet is 86
2950  b is 97
2951  c is 96
2952  commutativity_of_join is 87
2953  commutativity_of_meet is 88
2954  equation_H50 is 84
2955  idempotence_of_join is 91
2956  idempotence_of_meet is 92
2957  join is 94
2958  meet is 95
2959  prove_H7 is 93
2960 Facts
2961  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2962  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2963  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2964  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2965  Id :  12, {_}:
2966           meet ?12 ?13 =?= meet ?13 ?12
2967           [13, 12] by commutativity_of_meet ?12 ?13
2968  Id :  14, {_}:
2969           join ?15 ?16 =?= join ?16 ?15
2970           [16, 15] by commutativity_of_join ?15 ?16
2971  Id :  16, {_}:
2972           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2973           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2974  Id :  18, {_}:
2975           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2976           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2977  Id :  20, {_}:
2978           meet ?26 (join ?27 (meet ?28 (join ?26 ?29)))
2979           =<=
2980           meet ?26 (join ?27 (meet ?28 (join ?26 (meet ?28 (join ?27 ?29)))))
2981           [29, 28, 27, 26] by equation_H50 ?26 ?27 ?28 ?29
2982 Goal
2983  Id :   2, {_}:
2984           meet a (join b (meet a c))
2985           =<=
2986           meet a (join b (meet a (join (meet a b) (meet c (join a b)))))
2987           [] by prove_H7
2988 Timeout !
2989 FAILURE in 250 iterations
2990 LAT164-1
2991 Order
2992  == is 100
2993  _ is 99
2994  a is 98
2995  absorption1 is 90
2996  absorption2 is 89
2997  associativity_of_join is 85
2998  associativity_of_meet is 86
2999  b is 97
3000  c is 96
3001  commutativity_of_join is 87
3002  commutativity_of_meet is 88
3003  equation_H76 is 84
3004  idempotence_of_join is 91
3005  idempotence_of_meet is 92
3006  join is 94
3007  meet is 95
3008  prove_H6 is 93
3009 Facts
3010  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3011  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3012  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3013  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3014  Id :  12, {_}:
3015           meet ?12 ?13 =?= meet ?13 ?12
3016           [13, 12] by commutativity_of_meet ?12 ?13
3017  Id :  14, {_}:
3018           join ?15 ?16 =?= join ?16 ?15
3019           [16, 15] by commutativity_of_join ?15 ?16
3020  Id :  16, {_}:
3021           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3022           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3023  Id :  18, {_}:
3024           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3025           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3026  Id :  20, {_}:
3027           meet ?26 (join ?27 (meet ?28 (join ?27 ?29)))
3028           =<=
3029           meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?26 ?27))))
3030           [29, 28, 27, 26] by equation_H76 ?26 ?27 ?28 ?29
3031 Goal
3032  Id :   2, {_}:
3033           meet a (join b (meet a c))
3034           =<=
3035           meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
3036           [] by prove_H6
3037 Timeout !
3038 FAILURE in 250 iterations
3039 LAT165-1
3040 Order
3041  == is 100
3042  _ is 99
3043  a is 98
3044  absorption1 is 89
3045  absorption2 is 88
3046  associativity_of_join is 84
3047  associativity_of_meet is 85
3048  b is 97
3049  c is 96
3050  commutativity_of_join is 86
3051  commutativity_of_meet is 87
3052  d is 95
3053  equation_H76 is 83
3054  idempotence_of_join is 90
3055  idempotence_of_meet is 91
3056  join is 94
3057  meet is 93
3058  prove_H77 is 92
3059 Facts
3060  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3061  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3062  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3063  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3064  Id :  12, {_}:
3065           meet ?12 ?13 =?= meet ?13 ?12
3066           [13, 12] by commutativity_of_meet ?12 ?13
3067  Id :  14, {_}:
3068           join ?15 ?16 =?= join ?16 ?15
3069           [16, 15] by commutativity_of_join ?15 ?16
3070  Id :  16, {_}:
3071           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3072           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3073  Id :  18, {_}:
3074           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3075           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3076  Id :  20, {_}:
3077           meet ?26 (join ?27 (meet ?28 (join ?27 ?29)))
3078           =<=
3079           meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?26 ?27))))
3080           [29, 28, 27, 26] by equation_H76 ?26 ?27 ?28 ?29
3081 Goal
3082  Id :   2, {_}:
3083           meet a (join b (meet c (join b d)))
3084           =<=
3085           meet a (join b (meet c (join d (meet a (meet b c)))))
3086           [] by prove_H77
3087 Timeout !
3088 FAILURE in 269 iterations
3089 LAT166-1
3090 Order
3091  == is 100
3092  _ is 99
3093  a is 98
3094  absorption1 is 89
3095  absorption2 is 88
3096  associativity_of_join is 84
3097  associativity_of_meet is 85
3098  b is 97
3099  c is 96
3100  commutativity_of_join is 86
3101  commutativity_of_meet is 87
3102  d is 95
3103  equation_H77 is 83
3104  idempotence_of_join is 90
3105  idempotence_of_meet is 91
3106  join is 94
3107  meet is 93
3108  prove_H78 is 92
3109 Facts
3110  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3111  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3112  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3113  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3114  Id :  12, {_}:
3115           meet ?12 ?13 =?= meet ?13 ?12
3116           [13, 12] by commutativity_of_meet ?12 ?13
3117  Id :  14, {_}:
3118           join ?15 ?16 =?= join ?16 ?15
3119           [16, 15] by commutativity_of_join ?15 ?16
3120  Id :  16, {_}:
3121           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3122           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3123  Id :  18, {_}:
3124           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3125           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3126  Id :  20, {_}:
3127           meet ?26 (join ?27 (meet ?28 (join ?27 ?29)))
3128           =<=
3129           meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?26 (meet ?27 ?28)))))
3130           [29, 28, 27, 26] by equation_H77 ?26 ?27 ?28 ?29
3131 Goal
3132  Id :   2, {_}:
3133           meet a (join b (meet c (join b d)))
3134           =<=
3135           meet a (join b (meet c (join d (meet b (join a d)))))
3136           [] by prove_H78
3137 Timeout !
3138 FAILURE in 269 iterations
3139 LAT169-1
3140 Order
3141  == is 100
3142  _ is 99
3143  a is 98
3144  absorption1 is 90
3145  absorption2 is 89
3146  associativity_of_join is 85
3147  associativity_of_meet is 86
3148  b is 97
3149  c is 96
3150  commutativity_of_join is 87
3151  commutativity_of_meet is 88
3152  equation_H21_dual is 84
3153  idempotence_of_join is 91
3154  idempotence_of_meet is 92
3155  join is 95
3156  meet is 94
3157  prove_H58 is 93
3158 Facts
3159  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3160  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3161  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3162  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3163  Id :  12, {_}:
3164           meet ?12 ?13 =?= meet ?13 ?12
3165           [13, 12] by commutativity_of_meet ?12 ?13
3166  Id :  14, {_}:
3167           join ?15 ?16 =?= join ?16 ?15
3168           [16, 15] by commutativity_of_join ?15 ?16
3169  Id :  16, {_}:
3170           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3171           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3172  Id :  18, {_}:
3173           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3174           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3175  Id :  20, {_}:
3176           meet (join ?26 ?27) (join ?26 ?28)
3177           =<=
3178           join ?26
3179             (meet (join ?27 (meet ?26 (join ?27 ?28)))
3180               (join ?28 (meet ?26 ?27)))
3181           [28, 27, 26] by equation_H21_dual ?26 ?27 ?28
3182 Goal
3183  Id :   2, {_}:
3184           meet a (join b c)
3185           =<=
3186           meet a (join b (meet (join a b) (join c (meet a b))))
3187           [] by prove_H58
3188 Timeout !
3189 FAILURE in 268 iterations
3190 LAT170-1
3191 Order
3192  == is 100
3193  _ is 99
3194  a is 98
3195  absorption1 is 90
3196  absorption2 is 89
3197  associativity_of_join is 85
3198  associativity_of_meet is 86
3199  b is 97
3200  c is 96
3201  commutativity_of_join is 87
3202  commutativity_of_meet is 88
3203  equation_H49_dual is 84
3204  idempotence_of_join is 91
3205  idempotence_of_meet is 92
3206  join is 95
3207  meet is 94
3208  prove_H58 is 93
3209 Facts
3210  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3211  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3212  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3213  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3214  Id :  12, {_}:
3215           meet ?12 ?13 =?= meet ?13 ?12
3216           [13, 12] by commutativity_of_meet ?12 ?13
3217  Id :  14, {_}:
3218           join ?15 ?16 =?= join ?16 ?15
3219           [16, 15] by commutativity_of_join ?15 ?16
3220  Id :  16, {_}:
3221           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3222           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3223  Id :  18, {_}:
3224           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3225           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3226  Id :  20, {_}:
3227           join ?26 (meet ?27 (join ?28 (meet ?26 ?29)))
3228           =<=
3229           join ?26 (meet ?27 (meet (join ?26 ?28) (join ?28 (meet ?27 ?29))))
3230           [29, 28, 27, 26] by equation_H49_dual ?26 ?27 ?28 ?29
3231 Goal
3232  Id :   2, {_}:
3233           meet a (join b c)
3234           =<=
3235           meet a (join b (meet (join a b) (join c (meet a b))))
3236           [] by prove_H58
3237 Timeout !
3238 FAILURE in 269 iterations
3239 LAT173-1
3240 Order
3241  == is 100
3242  _ is 99
3243  a is 98
3244  absorption1 is 89
3245  absorption2 is 88
3246  associativity_of_join is 84
3247  associativity_of_meet is 85
3248  b is 97
3249  c is 96
3250  commutativity_of_join is 86
3251  commutativity_of_meet is 87
3252  d is 95
3253  equation_H76_dual is 83
3254  idempotence_of_join is 90
3255  idempotence_of_meet is 91
3256  join is 94
3257  meet is 93
3258  prove_H40 is 92
3259 Facts
3260  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3261  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3262  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3263  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3264  Id :  12, {_}:
3265           meet ?12 ?13 =?= meet ?13 ?12
3266           [13, 12] by commutativity_of_meet ?12 ?13
3267  Id :  14, {_}:
3268           join ?15 ?16 =?= join ?16 ?15
3269           [16, 15] by commutativity_of_join ?15 ?16
3270  Id :  16, {_}:
3271           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3272           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3273  Id :  18, {_}:
3274           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3275           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3276  Id :  20, {_}:
3277           join ?26 (meet ?27 (join ?28 (meet ?27 ?29)))
3278           =<=
3279           join ?26 (meet ?27 (join ?28 (meet ?29 (join ?26 ?27))))
3280           [29, 28, 27, 26] by equation_H76_dual ?26 ?27 ?28 ?29
3281 Goal
3282  Id :   2, {_}:
3283           meet a (join b (meet c (join a d)))
3284           =<=
3285           meet a (join b (meet c (join d (meet c (join a b)))))
3286           [] by prove_H40
3287 Timeout !
3288 FAILURE in 269 iterations
3289 LAT175-1
3290 Order
3291  == is 100
3292  _ is 99
3293  a is 98
3294  absorption1 is 89
3295  absorption2 is 88
3296  associativity_of_join is 84
3297  associativity_of_meet is 85
3298  b is 97
3299  c is 96
3300  commutativity_of_join is 86
3301  commutativity_of_meet is 87
3302  d is 95
3303  equation_H79_dual is 83
3304  idempotence_of_join is 90
3305  idempotence_of_meet is 91
3306  join is 93
3307  meet is 94
3308  prove_H32 is 92
3309 Facts
3310  Id :   4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3311  Id :   6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3312  Id :   8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3313  Id :  10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3314  Id :  12, {_}:
3315           meet ?12 ?13 =?= meet ?13 ?12
3316           [13, 12] by commutativity_of_meet ?12 ?13
3317  Id :  14, {_}:
3318           join ?15 ?16 =?= join ?16 ?15
3319           [16, 15] by commutativity_of_join ?15 ?16
3320  Id :  16, {_}:
3321           meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3322           [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3323  Id :  18, {_}:
3324           join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3325           [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3326  Id :  20, {_}:
3327           join ?26 (meet ?27 (join ?28 (meet ?26 ?29)))
3328           =<=
3329           join ?26 (meet (join ?26 (meet ?27 (join ?26 ?28))) (join ?28 ?29))
3330           [29, 28, 27, 26] by equation_H79_dual ?26 ?27 ?28 ?29
3331 Goal
3332  Id :   2, {_}:
3333           meet a (join b (meet a (meet c d)))
3334           =<=
3335           meet a (join b (meet c (join (meet a d) (meet b d))))
3336           [] by prove_H32
3337 Timeout !
3338 FAILURE in 250 iterations
3339 RNG009-7
3340 Fatal error: exception Assert_failure("tptp_cnf.ml", 4, 25)
3341 RNG019-6
3342 Order
3343  == is 100
3344  _ is 99
3345  add is 94
3346  additive_identity is 91
3347  additive_inverse is 85
3348  additive_inverse_additive_inverse is 82
3349  associativity_for_addition is 78
3350  associator is 93
3351  commutativity_for_addition is 79
3352  commutator is 75
3353  distribute1 is 81
3354  distribute2 is 80
3355  left_additive_identity is 90
3356  left_additive_inverse is 84
3357  left_alternative is 76
3358  left_multiplicative_zero is 87
3359  multiply is 88
3360  prove_linearised_form1 is 92
3361  right_additive_identity is 89
3362  right_additive_inverse is 83
3363  right_alternative is 77
3364  right_multiplicative_zero is 86
3365  u is 96
3366  v is 95
3367  x is 98
3368  y is 97
3369 Facts
3370  Id :   4, {_}:
3371           add additive_identity ?2 =>= ?2
3372           [2] by left_additive_identity ?2
3373  Id :   6, {_}:
3374           add ?4 additive_identity =>= ?4
3375           [4] by right_additive_identity ?4
3376  Id :   8, {_}:
3377           multiply additive_identity ?6 =>= additive_identity
3378           [6] by left_multiplicative_zero ?6
3379  Id :  10, {_}:
3380           multiply ?8 additive_identity =>= additive_identity
3381           [8] by right_multiplicative_zero ?8
3382  Id :  12, {_}:
3383           add (additive_inverse ?10) ?10 =>= additive_identity
3384           [10] by left_additive_inverse ?10
3385  Id :  14, {_}:
3386           add ?12 (additive_inverse ?12) =>= additive_identity
3387           [12] by right_additive_inverse ?12
3388  Id :  16, {_}:
3389           additive_inverse (additive_inverse ?14) =>= ?14
3390           [14] by additive_inverse_additive_inverse ?14
3391  Id :  18, {_}:
3392           multiply ?16 (add ?17 ?18)
3393           =<=
3394           add (multiply ?16 ?17) (multiply ?16 ?18)
3395           [18, 17, 16] by distribute1 ?16 ?17 ?18
3396  Id :  20, {_}:
3397           multiply (add ?20 ?21) ?22
3398           =<=
3399           add (multiply ?20 ?22) (multiply ?21 ?22)
3400           [22, 21, 20] by distribute2 ?20 ?21 ?22
3401  Id :  22, {_}:
3402           add ?24 ?25 =?= add ?25 ?24
3403           [25, 24] by commutativity_for_addition ?24 ?25
3404  Id :  24, {_}:
3405           add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3406           [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3407  Id :  26, {_}:
3408           multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3409           [32, 31] by right_alternative ?31 ?32
3410  Id :  28, {_}:
3411           multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3412           [35, 34] by left_alternative ?34 ?35
3413  Id :  30, {_}:
3414           associator ?37 ?38 ?39
3415           =<=
3416           add (multiply (multiply ?37 ?38) ?39)
3417             (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3418           [39, 38, 37] by associator ?37 ?38 ?39
3419  Id :  32, {_}:
3420           commutator ?41 ?42
3421           =<=
3422           add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3423           [42, 41] by commutator ?41 ?42
3424 Goal
3425  Id :   2, {_}:
3426           associator x y (add u v)
3427           =<=
3428           add (associator x y u) (associator x y v)
3429           [] by prove_linearised_form1
3430 Timeout !
3431 FAILURE in 393 iterations
3432 RNG019-7
3433 Order
3434  == is 100
3435  _ is 99
3436  add is 94
3437  additive_identity is 91
3438  additive_inverse is 85
3439  additive_inverse_additive_inverse is 82
3440  associativity_for_addition is 78
3441  associator is 93
3442  commutativity_for_addition is 79
3443  commutator is 75
3444  distribute1 is 81
3445  distribute2 is 80
3446  distributivity_of_difference1 is 71
3447  distributivity_of_difference2 is 70
3448  distributivity_of_difference3 is 69
3449  distributivity_of_difference4 is 68
3450  inverse_product1 is 73
3451  inverse_product2 is 72
3452  left_additive_identity is 90
3453  left_additive_inverse is 84
3454  left_alternative is 76
3455  left_multiplicative_zero is 87
3456  multiply is 88
3457  product_of_inverses is 74
3458  prove_linearised_form1 is 92
3459  right_additive_identity is 89
3460  right_additive_inverse is 83
3461  right_alternative is 77
3462  right_multiplicative_zero is 86
3463  u is 96
3464  v is 95
3465  x is 98
3466  y is 97
3467 Facts
3468  Id :   4, {_}:
3469           add additive_identity ?2 =>= ?2
3470           [2] by left_additive_identity ?2
3471  Id :   6, {_}:
3472           add ?4 additive_identity =>= ?4
3473           [4] by right_additive_identity ?4
3474  Id :   8, {_}:
3475           multiply additive_identity ?6 =>= additive_identity
3476           [6] by left_multiplicative_zero ?6
3477  Id :  10, {_}:
3478           multiply ?8 additive_identity =>= additive_identity
3479           [8] by right_multiplicative_zero ?8
3480  Id :  12, {_}:
3481           add (additive_inverse ?10) ?10 =>= additive_identity
3482           [10] by left_additive_inverse ?10
3483  Id :  14, {_}:
3484           add ?12 (additive_inverse ?12) =>= additive_identity
3485           [12] by right_additive_inverse ?12
3486  Id :  16, {_}:
3487           additive_inverse (additive_inverse ?14) =>= ?14
3488           [14] by additive_inverse_additive_inverse ?14
3489  Id :  18, {_}:
3490           multiply ?16 (add ?17 ?18)
3491           =<=
3492           add (multiply ?16 ?17) (multiply ?16 ?18)
3493           [18, 17, 16] by distribute1 ?16 ?17 ?18
3494  Id :  20, {_}:
3495           multiply (add ?20 ?21) ?22
3496           =<=
3497           add (multiply ?20 ?22) (multiply ?21 ?22)
3498           [22, 21, 20] by distribute2 ?20 ?21 ?22
3499  Id :  22, {_}:
3500           add ?24 ?25 =?= add ?25 ?24
3501           [25, 24] by commutativity_for_addition ?24 ?25
3502  Id :  24, {_}:
3503           add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3504           [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3505  Id :  26, {_}:
3506           multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3507           [32, 31] by right_alternative ?31 ?32
3508  Id :  28, {_}:
3509           multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3510           [35, 34] by left_alternative ?34 ?35
3511  Id :  30, {_}:
3512           associator ?37 ?38 ?39
3513           =<=
3514           add (multiply (multiply ?37 ?38) ?39)
3515             (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3516           [39, 38, 37] by associator ?37 ?38 ?39
3517  Id :  32, {_}:
3518           commutator ?41 ?42
3519           =<=
3520           add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3521           [42, 41] by commutator ?41 ?42
3522  Id :  34, {_}:
3523           multiply (additive_inverse ?44) (additive_inverse ?45)
3524           =>=
3525           multiply ?44 ?45
3526           [45, 44] by product_of_inverses ?44 ?45
3527  Id :  36, {_}:
3528           multiply (additive_inverse ?47) ?48
3529           =>=
3530           additive_inverse (multiply ?47 ?48)
3531           [48, 47] by inverse_product1 ?47 ?48
3532  Id :  38, {_}:
3533           multiply ?50 (additive_inverse ?51)
3534           =>=
3535           additive_inverse (multiply ?50 ?51)
3536           [51, 50] by inverse_product2 ?50 ?51
3537  Id :  40, {_}:
3538           multiply ?53 (add ?54 (additive_inverse ?55))
3539           =<=
3540           add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
3541           [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
3542  Id :  42, {_}:
3543           multiply (add ?57 (additive_inverse ?58)) ?59
3544           =<=
3545           add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
3546           [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
3547  Id :  44, {_}:
3548           multiply (additive_inverse ?61) (add ?62 ?63)
3549           =<=
3550           add (additive_inverse (multiply ?61 ?62))
3551             (additive_inverse (multiply ?61 ?63))
3552           [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
3553  Id :  46, {_}:
3554           multiply (add ?65 ?66) (additive_inverse ?67)
3555           =<=
3556           add (additive_inverse (multiply ?65 ?67))
3557             (additive_inverse (multiply ?66 ?67))
3558           [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
3559 Goal
3560  Id :   2, {_}:
3561           associator x y (add u v)
3562           =<=
3563           add (associator x y u) (associator x y v)
3564           [] by prove_linearised_form1
3565 Timeout !
3566 FAILURE in 546 iterations
3567 RNG020-6
3568 Order
3569  == is 100
3570  _ is 99
3571  add is 95
3572  additive_identity is 91
3573  additive_inverse is 85
3574  additive_inverse_additive_inverse is 82
3575  associativity_for_addition is 78
3576  associator is 93
3577  commutativity_for_addition is 79
3578  commutator is 75
3579  distribute1 is 81
3580  distribute2 is 80
3581  left_additive_identity is 90
3582  left_additive_inverse is 84
3583  left_alternative is 76
3584  left_multiplicative_zero is 87
3585  multiply is 88
3586  prove_linearised_form2 is 92
3587  right_additive_identity is 89
3588  right_additive_inverse is 83
3589  right_alternative is 77
3590  right_multiplicative_zero is 86
3591  u is 97
3592  v is 96
3593  x is 98
3594  y is 94
3595 Facts
3596  Id :   4, {_}:
3597           add additive_identity ?2 =>= ?2
3598           [2] by left_additive_identity ?2
3599  Id :   6, {_}:
3600           add ?4 additive_identity =>= ?4
3601           [4] by right_additive_identity ?4
3602  Id :   8, {_}:
3603           multiply additive_identity ?6 =>= additive_identity
3604           [6] by left_multiplicative_zero ?6
3605  Id :  10, {_}:
3606           multiply ?8 additive_identity =>= additive_identity
3607           [8] by right_multiplicative_zero ?8
3608  Id :  12, {_}:
3609           add (additive_inverse ?10) ?10 =>= additive_identity
3610           [10] by left_additive_inverse ?10
3611  Id :  14, {_}:
3612           add ?12 (additive_inverse ?12) =>= additive_identity
3613           [12] by right_additive_inverse ?12
3614  Id :  16, {_}:
3615           additive_inverse (additive_inverse ?14) =>= ?14
3616           [14] by additive_inverse_additive_inverse ?14
3617  Id :  18, {_}:
3618           multiply ?16 (add ?17 ?18)
3619           =<=
3620           add (multiply ?16 ?17) (multiply ?16 ?18)
3621           [18, 17, 16] by distribute1 ?16 ?17 ?18
3622  Id :  20, {_}:
3623           multiply (add ?20 ?21) ?22
3624           =<=
3625           add (multiply ?20 ?22) (multiply ?21 ?22)
3626           [22, 21, 20] by distribute2 ?20 ?21 ?22
3627  Id :  22, {_}:
3628           add ?24 ?25 =?= add ?25 ?24
3629           [25, 24] by commutativity_for_addition ?24 ?25
3630  Id :  24, {_}:
3631           add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3632           [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3633  Id :  26, {_}:
3634           multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3635           [32, 31] by right_alternative ?31 ?32
3636  Id :  28, {_}:
3637           multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3638           [35, 34] by left_alternative ?34 ?35
3639  Id :  30, {_}:
3640           associator ?37 ?38 ?39
3641           =<=
3642           add (multiply (multiply ?37 ?38) ?39)
3643             (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3644           [39, 38, 37] by associator ?37 ?38 ?39
3645  Id :  32, {_}:
3646           commutator ?41 ?42
3647           =<=
3648           add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3649           [42, 41] by commutator ?41 ?42
3650 Goal
3651  Id :   2, {_}:
3652           associator x (add u v) y
3653           =<=
3654           add (associator x u y) (associator x v y)
3655           [] by prove_linearised_form2
3656 Timeout !
3657 FAILURE in 398 iterations
3658 RNG026-6
3659 Order
3660  == is 100
3661  _ is 99
3662  a is 98
3663  add is 92
3664  additive_identity is 90
3665  additive_inverse is 91
3666  additive_inverse_additive_inverse is 82
3667  associativity_for_addition is 78
3668  associator is 93
3669  b is 97
3670  c is 95
3671  commutativity_for_addition is 79
3672  commutator is 75
3673  d is 94
3674  distribute1 is 81
3675  distribute2 is 80
3676  left_additive_identity is 88
3677  left_additive_inverse is 84
3678  left_alternative is 76
3679  left_multiplicative_zero is 86
3680  multiply is 96
3681  prove_teichmuller_identity is 89
3682  right_additive_identity is 87
3683  right_additive_inverse is 83
3684  right_alternative is 77
3685  right_multiplicative_zero is 85
3686 Facts
3687  Id :   4, {_}:
3688           add additive_identity ?2 =>= ?2
3689           [2] by left_additive_identity ?2
3690  Id :   6, {_}:
3691           add ?4 additive_identity =>= ?4
3692           [4] by right_additive_identity ?4
3693  Id :   8, {_}:
3694           multiply additive_identity ?6 =>= additive_identity
3695           [6] by left_multiplicative_zero ?6
3696  Id :  10, {_}:
3697           multiply ?8 additive_identity =>= additive_identity
3698           [8] by right_multiplicative_zero ?8
3699  Id :  12, {_}:
3700           add (additive_inverse ?10) ?10 =>= additive_identity
3701           [10] by left_additive_inverse ?10
3702  Id :  14, {_}:
3703           add ?12 (additive_inverse ?12) =>= additive_identity
3704           [12] by right_additive_inverse ?12
3705  Id :  16, {_}:
3706           additive_inverse (additive_inverse ?14) =>= ?14
3707           [14] by additive_inverse_additive_inverse ?14
3708  Id :  18, {_}:
3709           multiply ?16 (add ?17 ?18)
3710           =<=
3711           add (multiply ?16 ?17) (multiply ?16 ?18)
3712           [18, 17, 16] by distribute1 ?16 ?17 ?18
3713  Id :  20, {_}:
3714           multiply (add ?20 ?21) ?22
3715           =<=
3716           add (multiply ?20 ?22) (multiply ?21 ?22)
3717           [22, 21, 20] by distribute2 ?20 ?21 ?22
3718  Id :  22, {_}:
3719           add ?24 ?25 =?= add ?25 ?24
3720           [25, 24] by commutativity_for_addition ?24 ?25
3721  Id :  24, {_}:
3722           add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3723           [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3724  Id :  26, {_}:
3725           multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3726           [32, 31] by right_alternative ?31 ?32
3727  Id :  28, {_}:
3728           multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3729           [35, 34] by left_alternative ?34 ?35
3730  Id :  30, {_}:
3731           associator ?37 ?38 ?39
3732           =<=
3733           add (multiply (multiply ?37 ?38) ?39)
3734             (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3735           [39, 38, 37] by associator ?37 ?38 ?39
3736  Id :  32, {_}:
3737           commutator ?41 ?42
3738           =<=
3739           add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3740           [42, 41] by commutator ?41 ?42
3741 Goal
3742  Id :   2, {_}:
3743           add
3744             (add (associator (multiply a b) c d)
3745               (associator a b (multiply c d)))
3746             (additive_inverse
3747               (add
3748                 (add (associator a (multiply b c) d)
3749                   (multiply a (associator b c d)))
3750                 (multiply (associator a b c) d)))
3751           =>=
3752           additive_identity
3753           [] by prove_teichmuller_identity
3754 Timeout !
3755 FAILURE in 406 iterations
3756 RNG027-7
3757 Order
3758  == is 100
3759  _ is 99
3760  add is 92
3761  additive_identity is 93
3762  additive_inverse is 87
3763  additive_inverse_additive_inverse is 84
3764  associativity_for_addition is 80
3765  associator is 77
3766  commutativity_for_addition is 81
3767  commutator is 76
3768  cx is 97
3769  cy is 96
3770  cz is 98
3771  distribute1 is 83
3772  distribute2 is 82
3773  distributivity_of_difference1 is 72
3774  distributivity_of_difference2 is 71
3775  distributivity_of_difference3 is 70
3776  distributivity_of_difference4 is 69
3777  inverse_product1 is 74
3778  inverse_product2 is 73
3779  left_additive_identity is 91
3780  left_additive_inverse is 86
3781  left_alternative is 78
3782  left_multiplicative_zero is 89
3783  multiply is 95
3784  product_of_inverses is 75
3785  prove_right_moufang is 94
3786  right_additive_identity is 90
3787  right_additive_inverse is 85
3788  right_alternative is 79
3789  right_multiplicative_zero is 88
3790 Facts
3791  Id :   4, {_}:
3792           add additive_identity ?2 =>= ?2
3793           [2] by left_additive_identity ?2
3794  Id :   6, {_}:
3795           add ?4 additive_identity =>= ?4
3796           [4] by right_additive_identity ?4
3797  Id :   8, {_}:
3798           multiply additive_identity ?6 =>= additive_identity
3799           [6] by left_multiplicative_zero ?6
3800  Id :  10, {_}:
3801           multiply ?8 additive_identity =>= additive_identity
3802           [8] by right_multiplicative_zero ?8
3803  Id :  12, {_}:
3804           add (additive_inverse ?10) ?10 =>= additive_identity
3805           [10] by left_additive_inverse ?10
3806  Id :  14, {_}:
3807           add ?12 (additive_inverse ?12) =>= additive_identity
3808           [12] by right_additive_inverse ?12
3809  Id :  16, {_}:
3810           additive_inverse (additive_inverse ?14) =>= ?14
3811           [14] by additive_inverse_additive_inverse ?14
3812  Id :  18, {_}:
3813           multiply ?16 (add ?17 ?18)
3814           =<=
3815           add (multiply ?16 ?17) (multiply ?16 ?18)
3816           [18, 17, 16] by distribute1 ?16 ?17 ?18
3817  Id :  20, {_}:
3818           multiply (add ?20 ?21) ?22
3819           =<=
3820           add (multiply ?20 ?22) (multiply ?21 ?22)
3821           [22, 21, 20] by distribute2 ?20 ?21 ?22
3822  Id :  22, {_}:
3823           add ?24 ?25 =?= add ?25 ?24
3824           [25, 24] by commutativity_for_addition ?24 ?25
3825  Id :  24, {_}:
3826           add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3827           [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3828  Id :  26, {_}:
3829           multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3830           [32, 31] by right_alternative ?31 ?32
3831  Id :  28, {_}:
3832           multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3833           [35, 34] by left_alternative ?34 ?35
3834  Id :  30, {_}:
3835           associator ?37 ?38 ?39
3836           =<=
3837           add (multiply (multiply ?37 ?38) ?39)
3838             (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3839           [39, 38, 37] by associator ?37 ?38 ?39
3840  Id :  32, {_}:
3841           commutator ?41 ?42
3842           =<=
3843           add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3844           [42, 41] by commutator ?41 ?42
3845  Id :  34, {_}:
3846           multiply (additive_inverse ?44) (additive_inverse ?45)
3847           =>=
3848           multiply ?44 ?45
3849           [45, 44] by product_of_inverses ?44 ?45
3850  Id :  36, {_}:
3851           multiply (additive_inverse ?47) ?48
3852           =>=
3853           additive_inverse (multiply ?47 ?48)
3854           [48, 47] by inverse_product1 ?47 ?48
3855  Id :  38, {_}:
3856           multiply ?50 (additive_inverse ?51)
3857           =>=
3858           additive_inverse (multiply ?50 ?51)
3859           [51, 50] by inverse_product2 ?50 ?51
3860  Id :  40, {_}:
3861           multiply ?53 (add ?54 (additive_inverse ?55))
3862           =<=
3863           add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
3864           [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
3865  Id :  42, {_}:
3866           multiply (add ?57 (additive_inverse ?58)) ?59
3867           =<=
3868           add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
3869           [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
3870  Id :  44, {_}:
3871           multiply (additive_inverse ?61) (add ?62 ?63)
3872           =<=
3873           add (additive_inverse (multiply ?61 ?62))
3874             (additive_inverse (multiply ?61 ?63))
3875           [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
3876  Id :  46, {_}:
3877           multiply (add ?65 ?66) (additive_inverse ?67)
3878           =<=
3879           add (additive_inverse (multiply ?65 ?67))
3880             (additive_inverse (multiply ?66 ?67))
3881           [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
3882 Goal
3883  Id :   2, {_}:
3884           multiply cz (multiply cx (multiply cy cx))
3885           =<=
3886           multiply (multiply (multiply cz cx) cy) cx
3887           [] by prove_right_moufang
3888 Timeout !
3889 FAILURE in 538 iterations
3890 RNG028-9
3891 Order
3892  == is 100
3893  _ is 99
3894  add is 91
3895  additive_identity is 92
3896  additive_inverse is 86
3897  additive_inverse_additive_inverse is 83
3898  associativity_for_addition is 79
3899  associator is 94
3900  commutativity_for_addition is 80
3901  commutator is 76
3902  distribute1 is 82
3903  distribute2 is 81
3904  distributivity_of_difference1 is 72
3905  distributivity_of_difference2 is 71
3906  distributivity_of_difference3 is 70
3907  distributivity_of_difference4 is 69
3908  inverse_product1 is 74
3909  inverse_product2 is 73
3910  left_additive_identity is 90
3911  left_additive_inverse is 85
3912  left_alternative is 77
3913  left_multiplicative_zero is 88
3914  multiply is 96
3915  product_of_inverses is 75
3916  prove_left_moufang is 93
3917  right_additive_identity is 89
3918  right_additive_inverse is 84
3919  right_alternative is 78
3920  right_multiplicative_zero is 87
3921  x is 98
3922  y is 97
3923  z is 95
3924 Facts
3925  Id :   4, {_}:
3926           add additive_identity ?2 =>= ?2
3927           [2] by left_additive_identity ?2
3928  Id :   6, {_}:
3929           add ?4 additive_identity =>= ?4
3930           [4] by right_additive_identity ?4
3931  Id :   8, {_}:
3932           multiply additive_identity ?6 =>= additive_identity
3933           [6] by left_multiplicative_zero ?6
3934  Id :  10, {_}:
3935           multiply ?8 additive_identity =>= additive_identity
3936           [8] by right_multiplicative_zero ?8
3937  Id :  12, {_}:
3938           add (additive_inverse ?10) ?10 =>= additive_identity
3939           [10] by left_additive_inverse ?10
3940  Id :  14, {_}:
3941           add ?12 (additive_inverse ?12) =>= additive_identity
3942           [12] by right_additive_inverse ?12
3943  Id :  16, {_}:
3944           additive_inverse (additive_inverse ?14) =>= ?14
3945           [14] by additive_inverse_additive_inverse ?14
3946  Id :  18, {_}:
3947           multiply ?16 (add ?17 ?18)
3948           =<=
3949           add (multiply ?16 ?17) (multiply ?16 ?18)
3950           [18, 17, 16] by distribute1 ?16 ?17 ?18
3951  Id :  20, {_}:
3952           multiply (add ?20 ?21) ?22
3953           =<=
3954           add (multiply ?20 ?22) (multiply ?21 ?22)
3955           [22, 21, 20] by distribute2 ?20 ?21 ?22
3956  Id :  22, {_}:
3957           add ?24 ?25 =?= add ?25 ?24
3958           [25, 24] by commutativity_for_addition ?24 ?25
3959  Id :  24, {_}:
3960           add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3961           [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3962  Id :  26, {_}:
3963           multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3964           [32, 31] by right_alternative ?31 ?32
3965  Id :  28, {_}:
3966           multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3967           [35, 34] by left_alternative ?34 ?35
3968  Id :  30, {_}:
3969           associator ?37 ?38 ?39
3970           =<=
3971           add (multiply (multiply ?37 ?38) ?39)
3972             (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3973           [39, 38, 37] by associator ?37 ?38 ?39
3974  Id :  32, {_}:
3975           commutator ?41 ?42
3976           =<=
3977           add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3978           [42, 41] by commutator ?41 ?42
3979  Id :  34, {_}:
3980           multiply (additive_inverse ?44) (additive_inverse ?45)
3981           =>=
3982           multiply ?44 ?45
3983           [45, 44] by product_of_inverses ?44 ?45
3984  Id :  36, {_}:
3985           multiply (additive_inverse ?47) ?48
3986           =>=
3987           additive_inverse (multiply ?47 ?48)
3988           [48, 47] by inverse_product1 ?47 ?48
3989  Id :  38, {_}:
3990           multiply ?50 (additive_inverse ?51)
3991           =>=
3992           additive_inverse (multiply ?50 ?51)
3993           [51, 50] by inverse_product2 ?50 ?51
3994  Id :  40, {_}:
3995           multiply ?53 (add ?54 (additive_inverse ?55))
3996           =<=
3997           add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
3998           [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
3999  Id :  42, {_}:
4000           multiply (add ?57 (additive_inverse ?58)) ?59
4001           =<=
4002           add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
4003           [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
4004  Id :  44, {_}:
4005           multiply (additive_inverse ?61) (add ?62 ?63)
4006           =<=
4007           add (additive_inverse (multiply ?61 ?62))
4008             (additive_inverse (multiply ?61 ?63))
4009           [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
4010  Id :  46, {_}:
4011           multiply (add ?65 ?66) (additive_inverse ?67)
4012           =<=
4013           add (additive_inverse (multiply ?65 ?67))
4014             (additive_inverse (multiply ?66 ?67))
4015           [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
4016 Goal
4017  Id :   2, {_}:
4018           associator x (multiply y x) z =<= multiply x (associator x y z)
4019           [] by prove_left_moufang
4020 Timeout !
4021 FAILURE in 537 iterations
4022 RNG029-7
4023 Order
4024  == is 100
4025  _ is 99
4026  add is 92
4027  additive_identity is 93
4028  additive_inverse is 87
4029  additive_inverse_additive_inverse is 84
4030  associativity_for_addition is 80
4031  associator is 77
4032  commutativity_for_addition is 81
4033  commutator is 76
4034  distribute1 is 83
4035  distribute2 is 82
4036  distributivity_of_difference1 is 72
4037  distributivity_of_difference2 is 71
4038  distributivity_of_difference3 is 70
4039  distributivity_of_difference4 is 69
4040  inverse_product1 is 74
4041  inverse_product2 is 73
4042  left_additive_identity is 91
4043  left_additive_inverse is 86
4044  left_alternative is 78
4045  left_multiplicative_zero is 89
4046  multiply is 96
4047  product_of_inverses is 75
4048  prove_middle_moufang is 94
4049  right_additive_identity is 90
4050  right_additive_inverse is 85
4051  right_alternative is 79
4052  right_multiplicative_zero is 88
4053  x is 98
4054  y is 97
4055  z is 95
4056 Facts
4057  Id :   4, {_}:
4058           add additive_identity ?2 =>= ?2
4059           [2] by left_additive_identity ?2
4060  Id :   6, {_}:
4061           add ?4 additive_identity =>= ?4
4062           [4] by right_additive_identity ?4
4063  Id :   8, {_}:
4064           multiply additive_identity ?6 =>= additive_identity
4065           [6] by left_multiplicative_zero ?6
4066  Id :  10, {_}:
4067           multiply ?8 additive_identity =>= additive_identity
4068           [8] by right_multiplicative_zero ?8
4069  Id :  12, {_}:
4070           add (additive_inverse ?10) ?10 =>= additive_identity
4071           [10] by left_additive_inverse ?10
4072  Id :  14, {_}:
4073           add ?12 (additive_inverse ?12) =>= additive_identity
4074           [12] by right_additive_inverse ?12
4075  Id :  16, {_}:
4076           additive_inverse (additive_inverse ?14) =>= ?14
4077           [14] by additive_inverse_additive_inverse ?14
4078  Id :  18, {_}:
4079           multiply ?16 (add ?17 ?18)
4080           =<=
4081           add (multiply ?16 ?17) (multiply ?16 ?18)
4082           [18, 17, 16] by distribute1 ?16 ?17 ?18
4083  Id :  20, {_}:
4084           multiply (add ?20 ?21) ?22
4085           =<=
4086           add (multiply ?20 ?22) (multiply ?21 ?22)
4087           [22, 21, 20] by distribute2 ?20 ?21 ?22
4088  Id :  22, {_}:
4089           add ?24 ?25 =?= add ?25 ?24
4090           [25, 24] by commutativity_for_addition ?24 ?25
4091  Id :  24, {_}:
4092           add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
4093           [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
4094  Id :  26, {_}:
4095           multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
4096           [32, 31] by right_alternative ?31 ?32
4097  Id :  28, {_}:
4098           multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
4099           [35, 34] by left_alternative ?34 ?35
4100  Id :  30, {_}:
4101           associator ?37 ?38 ?39
4102           =<=
4103           add (multiply (multiply ?37 ?38) ?39)
4104             (additive_inverse (multiply ?37 (multiply ?38 ?39)))
4105           [39, 38, 37] by associator ?37 ?38 ?39
4106  Id :  32, {_}:
4107           commutator ?41 ?42
4108           =<=
4109           add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
4110           [42, 41] by commutator ?41 ?42
4111  Id :  34, {_}:
4112           multiply (additive_inverse ?44) (additive_inverse ?45)
4113           =>=
4114           multiply ?44 ?45
4115           [45, 44] by product_of_inverses ?44 ?45
4116  Id :  36, {_}:
4117           multiply (additive_inverse ?47) ?48
4118           =>=
4119           additive_inverse (multiply ?47 ?48)
4120           [48, 47] by inverse_product1 ?47 ?48
4121  Id :  38, {_}:
4122           multiply ?50 (additive_inverse ?51)
4123           =>=
4124           additive_inverse (multiply ?50 ?51)
4125           [51, 50] by inverse_product2 ?50 ?51
4126  Id :  40, {_}:
4127           multiply ?53 (add ?54 (additive_inverse ?55))
4128           =<=
4129           add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
4130           [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
4131  Id :  42, {_}:
4132           multiply (add ?57 (additive_inverse ?58)) ?59
4133           =<=
4134           add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
4135           [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
4136  Id :  44, {_}:
4137           multiply (additive_inverse ?61) (add ?62 ?63)
4138           =<=
4139           add (additive_inverse (multiply ?61 ?62))
4140             (additive_inverse (multiply ?61 ?63))
4141           [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
4142  Id :  46, {_}:
4143           multiply (add ?65 ?66) (additive_inverse ?67)
4144           =<=
4145           add (additive_inverse (multiply ?65 ?67))
4146             (additive_inverse (multiply ?66 ?67))
4147           [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
4148 Goal
4149  Id :   2, {_}:
4150           multiply (multiply x y) (multiply z x)
4151           =<=
4152           multiply (multiply x (multiply y z)) x
4153           [] by prove_middle_moufang
4154 Timeout !
4155 FAILURE in 537 iterations
4156 RNG035-7
4157 Fatal error: exception Assert_failure("tptp_cnf.ml", 4, 25)
4158 ROB006-1
4159 Order
4160  == is 100
4161  _ is 99
4162  a is 98
4163  absorbtion is 88
4164  add is 95
4165  associativity_of_add is 92
4166  b is 97
4167  c is 90
4168  commutativity_of_add is 93
4169  d is 89
4170  negate is 96
4171  prove_huntingtons_axiom is 94
4172  robbins_axiom is 91
4173 Facts
4174  Id :   4, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
4175  Id :   6, {_}:
4176           add (add ?5 ?6) ?7 =?= add ?5 (add ?6 ?7)
4177           [7, 6, 5] by associativity_of_add ?5 ?6 ?7
4178  Id :   8, {_}:
4179           negate (add (negate (add ?9 ?10)) (negate (add ?9 (negate ?10))))
4180           =>=
4181           ?9
4182           [10, 9] by robbins_axiom ?9 ?10
4183  Id :  10, {_}: add c d =>= d [] by absorbtion
4184 Goal
4185  Id :   2, {_}:
4186           add (negate (add a (negate b)))
4187             (negate (add (negate a) (negate b)))
4188           =>=
4189           b
4190           [] by prove_huntingtons_axiom
4191 Timeout !
4192 FAILURE in 163 iterations
4193 ROB006-2
4194 Order
4195  == is 100
4196  _ is 99
4197  absorbtion is 90
4198  add is 98
4199  associativity_of_add is 95
4200  c is 92
4201  commutativity_of_add is 96
4202  d is 91
4203  negate is 94
4204  prove_idempotence is 97
4205  robbins_axiom is 93
4206 Facts
4207  Id :   4, {_}: add ?3 ?4 =?= add ?4 ?3 [4, 3] by commutativity_of_add ?3 ?4
4208  Id :   6, {_}:
4209           add (add ?6 ?7) ?8 =?= add ?6 (add ?7 ?8)
4210           [8, 7, 6] by associativity_of_add ?6 ?7 ?8
4211  Id :   8, {_}:
4212           negate (add (negate (add ?10 ?11)) (negate (add ?10 (negate ?11))))
4213           =>=
4214           ?10
4215           [11, 10] by robbins_axiom ?10 ?11
4216  Id :  10, {_}: add c d =>= d [] by absorbtion
4217 Goal
4218  Id :   2, {_}: add ?1 ?1 =>= ?1 [1] by prove_idempotence ?1
4219 Timeout !
4220 FAILURE in 253 iterations