Length of proof is 356. Level of proof is 140. ---------------- PROOF ---------------- 2 [] f(f(v0,v2),f(f(f(v2,v2),v1),f(f(f(f(f(v2,v0),v1),v1),v2),f(v2,v3))))=v2 # label("C_6 (Job 785)"). 3 [] f(X,f(f(X,f(Y,Y)),f(X,Z)))!=f(X,f(Y,f(X,Z))) # label("Modularity (version 1)"). 369 [para_into,2.1.1.2.2.1.1.1.1,2.1.1] f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),f(f(z,x),w))))=f(z,x). 370 [para_into,2.1.1.2.2.2,2.1.1] f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z)))=f(y,z). 371 [para_into,370.1.1.1.2,2.1.1] f(f(x,y),f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),w),f(f(f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),x),w),w),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))))=f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))). 372 [para_into,370.1.1.2.2.1.1.1.1,2.1.1] f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),x)))=f(z,x). 373 [para_into,371.1.1.2.1.1.1,2.1.1] f(f(x,y),f(f(f(y,f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),w),f(f(f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),x),w),w),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))))=f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))). 374 [para_into,373.1.1.2.1.1.2,2.1.1] f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))),x),z),z),f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))))=f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))). 375 [para_into,374.1.1.2.2.1.1.1.1.1,2.1.1] f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))))=f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))). 376 [para_into,375.1.1.2.2.1.2,2.1.1] f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w))))))=f(f(v,y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))). 377 [para_into,376.1.2,2.1.1] f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w))))))=y. 378 [para_into,377.1.1.2.2,2.1.1] f(f(x,y),f(f(f(y,y),z),y))=y. 379 [para_into,378.1.1.2.1,378.1.1] f(f(x,y),f(y,y))=y. 380 [para_into,378.1.1.2,378.1.1] f(f(x,f(f(f(y,y),z),y)),y)=f(f(f(y,y),z),y). 381 [para_from,378.1.1,2.1.1.2.1] f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),y)),f(f(f(y,y),z),y)),y),f(y,u))))=y. 382 [para_into,379.1.1.2,379.1.1] f(f(x,f(y,y)),y)=f(y,y). 383 [para_from,379.1.1,378.1.1.2.1.1] f(f(x,f(y,y)),f(f(y,z),f(y,y)))=f(y,y). 384 [para_from,379.1.1,370.1.1.2.2.1.1.1.1] f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x)))=f(y,x). 385 [para_from,379.1.1,370.1.1.2.2.1.1.1] f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z)))=f(y,z). 386 [para_from,379.1.1,2.1.1.2.2.1.1.1] f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z))))=y. 387 [para_into,382.1.1.1,372.1.1,flip.1] f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(x,x),x),f(f(x,x),x)),x))=f(f(f(x,x),x),f(f(f(f(x,x),x),f(f(x,x),x)),x)). 388 [para_from,382.1.2,379.1.1.2] f(f(x,y),f(f(z,f(y,y)),y))=y. 389 [para_from,382.1.2,378.1.1.2.1.1] f(f(x,y),f(f(f(f(z,f(y,y)),y),u),y))=y. 390 [para_into,388.1.1.2.1.2,379.1.1] f(f(x,f(y,y)),f(f(z,y),f(y,y)))=f(y,y). 391 [para_from,383.1.2,378.1.1.2.1.1] f(f(x,y),f(f(f(f(z,f(y,y)),f(f(y,u),f(y,y))),v),y))=y. 392 [para_into,380.1.1.1,378.1.1,flip.1] f(f(f(x,x),y),x)=f(x,x). 393 [para_into,392.1.1.1.1,392.1.2] f(f(f(f(f(x,x),y),x),z),x)=f(x,x). 394 [para_into,392.1.1.1.1,379.1.1] f(f(x,y),f(x,x))=f(f(x,x),f(x,x)). 395 [para_from,392.1.1,2.1.1.2.2.1.1] f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))))=x. 397 [para_into,394.1.2,379.1.1] f(f(x,y),f(x,x))=x. 398 [para_into,397.1.1.1,397.1.1] f(x,f(f(x,y),f(x,y)))=f(x,y). 399 [para_into,397.1.1.1,389.1.1] f(x,f(f(y,x),f(y,x)))=f(y,x). 400 [para_into,397.1.1.2,382.1.2] f(f(x,y),f(f(z,f(x,x)),x))=x. 401 [para_from,397.1.1,370.1.1.2.2.1.1] f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(f(y,z),x),f(f(y,z),x))),f(f(f(f(y,z),x),f(y,z)),z)))=f(y,z). 402 [para_from,397.1.1,2.1.1.2.2.1.1.1.1] f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),f(f(x,y),u))))=f(x,y). 403 [para_from,397.1.1,2.1.1.2.2.1.1] f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z))))=y. 404 [para_from,398.1.1,2.1.1.2.2.1.1.1.1] f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u))))=x. 405 [para_into,399.1.1.2.1,2.1.1] f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,f(f(z,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))))))=f(f(z,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))). 406 [para_into,399.1.1.2,392.1.2] f(x,f(f(f(f(y,x),f(y,x)),z),f(y,x)))=f(y,x). 407 [para_from,399.1.1,2.1.1.2.2.2] f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y))))=y. 408 [para_into,395.1.1.2.2.2,406.1.1] f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))))=x. 409 [para_from,395.1.1,399.1.1.2.2] f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))),x))=f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))). 410 [para_into,408.1.1.1,397.1.1] f(x,f(f(f(f(x,x),f(x,x)),f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x). 411 [para_into,386.1.1.2.2.1,397.1.1] f(f(x,f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(x,f(f(x,x),y))))=f(x,x). 412 [para_into,386.1.1.2.2.2,400.1.1] f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y)))=f(y,z). 413 [para_into,407.1.1.2.1.1,397.1.1] f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(u,f(y,y)))))=f(y,y). 414 [para_into,411.1.1.2.1.1,397.1.1] f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(f(x,x),y))))=f(x,x). 415 [para_into,381.1.1.2.2.1,380.1.1] f(f(x,y),f(y,f(f(f(f(y,y),z),y),f(y,u))))=y. 416 [para_into,415.1.1.2.2.1.1,415.1.1] f(f(x,y),f(y,f(f(y,y),f(y,z))))=y. 418 [para_into,416.1.1,393.1.1] f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y))))=x. 419 [para_from,418.1.1,398.1.1.2,flip.1] f(x,f(f(x,x),f(x,y)))=f(x,x). 420 [para_into,419.1.1.2.1,397.1.1] f(f(x,x),f(x,f(f(x,x),y)))=f(f(x,x),f(x,x)). 421 [para_into,419.1.1.2.2,416.1.1] f(f(x,y),f(f(f(x,y),f(x,y)),y))=f(f(x,y),f(x,y)). 422 [para_into,419.1.1.2.2,400.1.1] f(f(x,y),f(f(f(x,y),f(x,y)),x))=f(f(x,y),f(x,y)). 425 [para_into,420.1.2,397.1.1] f(f(x,x),f(x,f(f(x,x),y)))=x. 427 [para_into,425.1.1.2.2,406.1.1] f(f(x,x),f(x,f(y,f(x,x))))=x. 428 [para_into,384.1.1.2.2.1.1,397.1.1] f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x)))=f(y,x). 429 [para_into,385.1.1.2.2.1,414.1.1] f(f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(f(f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(x,x)),f(f(x,x),f(x,f(f(x,x),y)))))=f(f(x,f(x,x)),f(x,f(f(x,x),y))). 430 [para_into,385.1.1.2.2.1,403.1.1] f(f(x,f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 431 [para_into,412.1.1.1,422.1.1] f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),x),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y)))))=f(f(f(x,y),f(x,y)),x). 432 [para_into,412.1.1.1,427.1.1] f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),f(f(x,x),f(x,x))),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(y,f(x,x)))),x)))=f(x,f(y,f(x,x))). 433 [para_into,412.1.1.1,419.1.1] f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),f(x,x)),f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x))))=f(f(x,x),f(x,y)). 434 [para_into,410.1.1.2.1.1,397.1.1] f(x,f(f(x,f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x). 435 [para_into,434.1.1.2.2.1.1,397.1.1] f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))))=f(x,x). 436 [para_from,435.1.1,399.1.1.2.2] f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),f(f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))),f(x,x)))=f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))). 437 [para_into,387.1.2,421.1.1] f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(x,x),x),f(f(x,x),x)),x))=f(f(f(x,x),x),f(f(x,x),x)). 438 [para_from,437.1.1,398.1.1.2] f(f(f(f(x,x),x),f(f(x,x),x)),f(f(f(x,x),x),f(f(x,x),x)))=f(f(f(f(x,x),x),f(f(x,x),x)),x). 439 [para_into,438.1.1,397.1.1,flip.1] f(f(f(f(x,x),x),f(f(x,x),x)),x)=f(f(x,x),x). 441 [para_from,439.1.1,402.1.1.2.1] f(f(f(f(x,x),f(x,x)),f(f(x,x),x)),f(f(f(x,x),x),f(f(f(f(f(x,x),x),x),f(f(x,x),x)),f(f(f(x,x),x),y))))=f(f(x,x),x). 442 [para_into,441.1.1.1.1,397.1.1] f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(f(f(f(f(x,x),x),x),f(f(x,x),x)),f(f(f(x,x),x),y))))=f(f(x,x),x). 443 [para_into,442.1.1.2.2.1.1,392.1.1] f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(f(f(x,x),f(f(x,x),x)),f(f(f(x,x),x),y))))=f(f(x,x),x). 445 [para_into,432.1.1.2.1.2,397.1.1] f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(y,f(x,x)))),x)))=f(x,f(y,f(x,x))). 446 [para_into,445.1.1.2.2.1.1.2,397.1.1] f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x)))=f(x,f(y,f(x,x))). 447 [para_into,409.1.1.2.1,395.1.1] f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x))=f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))). 449 [para_into,447.1.2,395.1.1] f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x))=x. 450 [para_into,436.1.1.2,397.1.1] f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x)=f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))). 451 [para_into,450.1.2,435.1.1] f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x)=f(x,x). 453 [para_from,451.1.1,386.1.1.2.2.1] f(f(f(x,f(x,x)),x),f(f(f(x,x),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,y))))=x. 454 [para_into,453.1.1.1,382.1.1] f(f(x,x),f(f(f(x,x),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,y))))=x. 456 [para_into,454.1.1.2.1,399.1.1] f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y))))=x. 457 [para_into,456.1.1.1,397.1.1] f(x,f(f(f(x,x),f(f(x,x),f(x,x))),f(f(f(x,x),f(x,x)),f(f(x,x),y))))=f(x,x). 458 [para_into,457.1.1.2.1.2,397.1.1] f(x,f(f(f(x,x),x),f(f(f(x,x),f(x,x)),f(f(x,x),y))))=f(x,x). 459 [para_into,458.1.1.2.2.1,397.1.1] f(x,f(f(f(x,x),x),f(x,f(f(x,x),y))))=f(x,x). 460 [para_into,405.1.1.2.2,2.1.1] f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x))=f(f(z,x),f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u)))). 461 [para_into,460.1.2,2.1.1] f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(x,x))=x. 462 [para_into,429.1.1.2.2,425.1.1] f(f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(f(f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(x,x)),x))=f(f(x,f(x,x)),f(x,f(f(x,x),y))). 463 [para_into,462.1.1,400.1.1,flip.1] f(f(x,f(x,x)),f(x,f(f(x,x),y)))=x. 464 [para_into,463.1.1.2.2,406.1.1] f(f(x,f(x,x)),f(x,f(y,f(x,x))))=x. 465 [para_into,464.1.1.1.2,397.1.1] f(f(f(x,x),x),f(f(x,x),f(y,f(f(x,x),f(x,x)))))=f(x,x). 466 [para_into,465.1.1.2.2.2,397.1.1] f(f(f(x,x),x),f(f(x,x),f(y,x)))=f(x,x). 467 [para_from,466.1.1,401.1.1.2.1.2.1] f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),f(f(f(x,x),x),f(f(x,x),f(y,x))))),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x). 468 [para_into,467.1.1.2.1.2.2,466.1.1] f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),f(x,x))),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x). 470 [para_into,468.1.1.2.1.2,397.1.1] f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x). 471 [para_into,470.1.1.2.1,439.1.1] f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(x,x),x),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x). 472 [para_into,471.1.1.2.2.1.1,466.1.1] f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(x,x),x),f(f(f(x,x),f(f(x,x),x)),x)))=f(f(x,x),x). 474 [para_into,472.1.1.2,378.1.1] f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),x)=f(f(x,x),x). 475 [para_from,474.1.1,413.1.1.2.2.1] f(f(f(x,x),f(x,x)),f(f(x,f(f(f(x,x),f(x,x)),f(x,x))),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x). 476 [para_into,475.1.1.1,397.1.1] f(x,f(f(x,f(f(f(x,x),f(x,x)),f(x,x))),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x). 477 [para_into,476.1.1.2.1.2.1,397.1.1] f(x,f(f(x,f(x,f(x,x))),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x). 478 [para_into,477.1.1.2.2.1.1,397.1.1] f(x,f(f(x,f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))))=f(x,x). 479 [para_into,478.1.1.2,379.1.1] f(x,f(x,f(x,x)))=f(x,x). 480 [para_into,479.1.1.2.2,397.1.1] f(f(x,x),f(f(x,x),x))=f(f(x,x),f(x,x)). 481 [para_into,480.1.2,397.1.1] f(f(x,x),f(f(x,x),x))=x. 482 [para_from,481.1.1,443.1.1.2.2.1] f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(x,f(f(f(x,x),x),y))))=f(f(x,x),x). 483 [para_into,482.1.1.2.2.2,406.1.1] f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(x,f(y,f(f(x,x),x)))))=f(f(x,x),x). 484 [para_into,430.1.1.1.2.1.1,397.1.1] f(f(x,f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 485 [para_into,484.1.1.1.2.1,399.1.1] f(f(x,f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 486 [para_into,485.1.1.1.2.2.1,379.1.1] f(f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 487 [para_into,486.1.1.1,459.1.1] f(f(x,x),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 489 [para_into,487.1.1.2.1.1.1.1.1,397.1.1] f(f(x,x),f(f(f(f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 490 [para_into,489.1.1.2.1.1.1.1,399.1.1] f(f(x,x),f(f(f(f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 491 [para_into,490.1.1.2.1.1.1.2.1,379.1.1] f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 492 [para_into,491.1.1.2.1.1.2.1.1,397.1.1] f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 493 [para_into,492.1.1.2.1.1.2.1,399.1.1] f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 494 [para_into,493.1.1.2.1.1.2.2.1,379.1.1] f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 495 [para_into,494.1.1.2.2.2.1,379.1.1] f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),f(f(x,x),f(x,f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 496 [para_into,495.1.1.2.2,425.1.1] f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),x))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))). 497 [para_into,496.1.1,400.1.1,flip.1] f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))=x. 498 [para_into,497.1.1.1.1,397.1.1] f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))=x. 499 [para_into,498.1.1.1,399.1.1] f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))=x. 500 [para_into,499.1.1.2.1,379.1.1] f(f(f(x,x),x),f(x,f(f(x,x),y)))=x. 501 [para_into,500.1.1.1.1,397.1.1] f(f(x,f(x,x)),f(f(x,x),f(f(f(x,x),f(x,x)),y)))=f(x,x). 502 [para_into,500.1.1.2.2,406.1.1] f(f(f(x,x),x),f(x,f(y,f(x,x))))=x. 503 [para_from,502.1.1,446.1.1.2.2.1] f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(x,x)))=f(x,f(y,f(x,x))). 504 [para_into,501.1.1.2.2.1,397.1.1] f(f(x,f(x,x)),f(f(x,x),f(x,y)))=f(x,x). 505 [para_into,504.1.1.2.2,400.1.1] f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x))=f(f(x,y),f(x,y)). 510 [para_from,505.1.1,431.1.1.2.2.1] f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),x),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y)))))=f(f(f(x,y),f(x,y)),x). 511 [para_into,503.1.1.2,379.1.1,flip.1] f(x,f(y,f(x,x)))=f(x,x). 515 [para_from,511.1.2,397.1.1.2] f(f(x,y),f(x,f(z,f(x,x))))=x. 518 [para_into,510.1.1.2,390.1.1] f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y)))=f(f(f(x,y),f(x,y)),x). 522 [para_into,518.1.1,397.1.1,flip.1] f(f(f(x,y),f(x,y)),x)=f(x,y). 524 [para_from,522.1.1,433.1.1.2.1] f(f(x,x),f(f(f(x,x),f(x,y)),f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x))))=f(f(x,x),f(x,y)). 525 [para_from,522.1.1,511.1.1.2] f(x,f(f(x,x),y))=f(x,x). 526 [para_from,522.1.1,404.1.1.1] f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u))))=x. 527 [para_from,522.1.1,515.1.1.2.2] f(f(x,y),f(x,f(f(x,x),z)))=x. 531 [para_from,525.1.1,483.1.1.1] f(f(x,x),f(f(f(x,x),x),f(x,f(y,f(f(x,x),x)))))=f(f(x,x),x). 537 [para_from,525.1.2,392.1.1.1.1] f(f(f(x,f(f(x,x),y)),z),x)=f(x,x). 539 [para_into,524.1.1.2.2.1,504.1.1] f(f(x,x),f(f(f(x,x),f(x,y)),f(f(x,x),f(x,x))))=f(f(x,x),f(x,y)). 541 [para_into,539.1.1.2,397.1.1] f(f(x,x),f(x,x))=f(f(x,x),f(x,y)). 547 [para_into,541.1.1,397.1.1,flip.1] f(f(x,x),f(x,y))=x. 551 [para_into,547.1.1.2,406.1.1] f(f(x,x),f(y,x))=x. 552 [para_from,547.1.1,407.1.1.2.1] f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y))))=y. 555 [para_from,551.1.1,428.1.1.1] f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x)))=f(y,x). 556 [para_from,551.1.1,407.1.1.2.1] f(f(x,y),f(y,f(f(f(f(f(y,x),f(z,y)),f(z,y)),y),f(u,y))))=y. 558 [para_into,552.1.1.1,551.1.1] f(x,f(f(y,x),f(f(f(f(f(f(y,x),f(x,x)),f(f(y,x),z)),f(f(y,x),z)),f(y,x)),f(u,f(y,x)))))=f(y,x). 559 [para_into,552.1.1.2,399.1.1] f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y))=y. 560 [para_into,559.1.1.1,551.1.1] f(x,f(f(f(f(f(y,x),f(x,x)),f(f(y,x),z)),f(f(y,x),z)),f(y,x)))=f(y,x). 561 [para_into,559.1.1.1,547.1.1] f(x,f(f(f(f(f(x,y),f(x,x)),f(f(x,y),z)),f(f(x,y),z)),f(x,y)))=f(x,y). 562 [para_into,556.1.1.2,399.1.1] f(f(x,y),f(f(f(f(y,x),f(z,y)),f(z,y)),y))=y. 563 [para_into,562.1.1.1,522.1.1] f(f(x,y),f(f(f(f(x,f(f(x,y),f(x,y))),f(z,x)),f(z,x)),x))=x. 564 [para_into,563.1.1.2.1.1.1,398.1.1] f(f(x,y),f(f(f(f(x,y),f(z,x)),f(z,x)),x))=x. 565 [para_into,560.1.1.2.1.1.1,379.1.1] f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)))=f(y,x). 566 [para_into,565.1.1.2.1.1.2,564.1.1] f(x,f(f(f(x,y),f(f(y,x),f(f(f(f(y,x),f(z,y)),f(z,y)),y))),f(y,x)))=f(y,x). 567 [para_into,561.1.1.2.1.1.1,397.1.1] f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y)))=f(x,y). 568 [para_into,567.1.1.2.1.1.2,564.1.1] f(x,f(f(f(x,x),f(f(x,y),f(f(f(f(x,y),f(z,x)),f(z,x)),x))),f(x,y)))=f(x,y). 569 [para_into,566.1.1.2.1.2,564.1.1] f(x,f(f(f(x,y),y),f(y,x)))=f(y,x). 570 [para_into,569.1.1.2.1,397.1.1] f(x,f(x,f(f(x,x),x)))=f(f(x,x),x). 571 [para_into,570.1.1.2,525.1.1,flip.1] f(f(x,x),x)=f(x,f(x,x)). 573 [para_from,571.1.1,531.1.1.2.1] f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(f(x,x),x)))))=f(f(x,x),x). 574 [para_from,571.1.1,449.1.1.1.1] f(f(f(x,f(x,x)),f(f(f(x,x),x),f(x,y))),f(x,x))=x. 575 [para_from,571.1.1,395.1.1.2.1] f(f(x,x),f(f(x,f(x,x)),f(f(f(x,x),x),f(x,y))))=x. 576 [para_into,574.1.1.1.2.1,571.1.1] f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x))=x. 577 [para_into,575.1.1.2.2.1,571.1.1] f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))))=x. 578 [para_into,573.1.1.2.2.2.2,571.1.1] f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,f(x,x))))))=f(f(x,x),x). 579 [para_into,578.1.2,571.1.1] f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,f(x,x))))))=f(x,f(x,x)). 580 [para_into,579.1.1.2.2.2,577.1.1] f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,f(x,x)),x)))=f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))). 581 [para_into,568.1.1.2.1.2,564.1.1] f(x,f(f(f(x,x),x),f(x,y)))=f(x,y). 583 [para_into,558.1.1.2.2.1.1.1.1,379.1.1] f(x,f(f(y,x),f(f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)),f(u,f(y,x)))))=f(y,x). 584 [para_from,583.1.1,581.1.1.2.2,flip.1] f(x,f(f(y,x),f(f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)),f(u,f(y,x)))))=f(x,f(f(f(x,x),x),f(y,x))). 585 [para_into,584.1.1,583.1.1,flip.1] f(x,f(f(f(x,x),x),f(y,x)))=f(y,x). 586 [para_into,585.1.1.2.1.1,551.1.1] f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x))))=f(y,f(x,x)). 587 [para_into,580.1.1.2.2,382.1.1] f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(x,x)))=f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))). 589 [para_into,587.1.1.2,576.1.1,flip.1] f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x))))=f(f(f(x,f(x,x)),f(x,f(x,x))),x). 590 [para_into,589.1.2,522.1.1] f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x))))=f(x,f(x,x)). 591 [para_from,590.1.1,586.1.1.2.1] f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(f(x,f(x,x)),f(x,f(x,x))))))=f(y,f(f(x,f(x,x)),f(x,f(x,x)))). 592 [para_into,591.1.1,547.1.1,flip.1] f(x,f(f(y,f(y,y)),f(y,f(y,y))))=f(y,f(y,y)). 594 [para_from,592.1.1,537.1.1.1] f(f(x,f(x,x)),y)=f(y,y). 595 [para_from,592.1.1,527.1.1.2.2] f(f(x,y),f(x,f(z,f(z,z))))=x. 596 [para_from,592.1.1,391.1.1.2.1] f(f(x,y),f(f(z,f(z,z)),y))=y. 597 [para_from,592.1.1,406.1.1.2.1] f(x,f(f(y,f(y,y)),f(z,x)))=f(z,x). 598 [para_from,592.1.1,547.1.1.2] f(f(x,x),f(y,f(y,y)))=x. 601 [para_from,592.1.1,397.1.1.1] f(f(x,f(x,x)),f(y,y))=y. 602 [para_from,592.1.1,525.1.1.2] f(x,f(y,f(y,y)))=f(x,x). 603 [para_from,592.1.1,393.1.1.1.1.1] f(f(f(f(x,f(x,x)),y),z),y)=f(y,y). 610 [para_from,594.1.2,522.1.1.1] f(f(f(x,f(x,x)),f(y,z)),y)=f(y,z). 611 [para_from,594.1.2,398.1.1.2] f(x,f(f(y,f(y,y)),f(x,z)))=f(x,z). 614 [para_from,594.1.2,397.1.1.2] f(f(x,y),f(f(z,f(z,z)),x))=x. 616 [para_from,598.1.1,579.1.1.2.2.2] f(f(x,x),f(f(x,f(x,x)),f(x,y)))=f(x,f(x,x)). 621 [para_from,602.1.1,526.1.1.2.2.1.1.1] f(f(x,y),f(f(f(x,x),f(z,f(z,z))),f(f(f(f(f(x,y),f(x,y)),f(z,f(z,z))),x),f(x,u))))=x. 622 [para_from,602.1.2,399.1.1.2] f(x,f(f(y,x),f(z,f(z,z))))=f(y,x). 623 [para_from,602.1.2,601.1.1.2] f(f(x,f(x,x)),f(y,f(z,f(z,z))))=y. 624 [para_from,602.1.2,598.1.1.1] f(f(x,f(y,f(y,y))),f(z,f(z,z)))=x. 625 [para_from,602.1.2,551.1.1.1] f(f(x,f(y,f(y,y))),f(z,x))=x. 626 [para_from,602.1.2,547.1.1.1] f(f(x,f(y,f(y,y))),f(x,z))=x. 629 [para_into,596.1.1,595.1.1] f(x,f(x,x))=f(y,f(y,y)). 634 [para_into,629.1.2.2,551.1.1] f(x,f(x,x))=f(f(y,y),y). 672 [para_from,634.1.2,407.1.1.2.1] f(f(x,y),f(f(z,f(z,z)),f(f(f(f(f(y,x),y),y),y),f(u,y))))=y. 673 [para_from,634.1.2,461.1.1.1.1] f(f(f(x,f(x,x)),f(f(f(f(f(y,z),y),y),y),f(y,u))),f(y,y))=y. 680 [para_into,623.1.1.2.2.2,594.1.2] f(f(x,f(x,x)),f(y,f(z,f(f(u,f(u,u)),z))))=y. 683 [para_from,624.1.1,567.1.1.2.1] f(x,f(x,f(x,y)))=f(x,y). 684 [para_from,624.1.1,565.1.1.2.1] f(x,f(x,f(y,x)))=f(y,x). 700 [para_into,616.1.1.2,594.1.1] f(f(x,x),f(f(x,y),f(x,y)))=f(x,f(x,x)). 705 [para_into,700.1.1.2,388.1.1,flip.1] f(f(x,f(y,y)),f(f(x,f(y,y)),f(x,f(y,y))))=f(f(f(x,f(y,y)),f(x,f(y,y))),y). 709 [para_into,672.1.1,597.1.1] f(f(f(f(f(x,y),x),x),x),f(y,x))=x. 714 [para_into,705.1.2.1.1.2,551.1.1] f(f(x,f(f(y,y),f(y,y))),f(f(x,f(f(y,y),f(y,y))),f(x,f(f(y,y),f(y,y)))))=f(f(f(x,y),f(x,f(f(y,y),f(y,y)))),f(y,y)). 719 [para_into,621.1.1.2.1,598.1.1] f(f(x,y),f(x,f(f(f(f(f(x,y),f(x,y)),f(z,f(z,z))),x),f(x,u))))=x. 720 [para_into,719.1.1.2.2.1.1,598.1.1] f(f(x,y),f(x,f(f(f(x,y),x),f(x,z))))=x. 722 [para_into,714.1.2.1.2.2,551.1.1] f(f(x,f(f(y,y),f(y,y))),f(f(x,f(f(y,y),f(y,y))),f(x,f(f(y,y),f(y,y)))))=f(f(f(x,y),f(x,y)),f(y,y)). 723 [para_into,722.1.1,629.1.2,flip.1] f(f(f(x,y),f(x,y)),f(y,y))=f(z,f(z,z)). 726 [para_from,723.1.1,555.1.1.2.1] f(x,f(f(y,f(y,y)),f(f(x,f(z,x)),x)))=f(z,x). 728 [para_into,726.1.1,597.1.1] f(f(x,f(y,x)),x)=f(y,x). 729 [para_into,728.1.1.1.2,610.1.1,flip.1] f(f(f(x,f(x,x)),f(y,z)),y)=f(f(y,f(y,z)),y). 730 [para_from,728.1.1,673.1.1.1.2.1.1.1] f(f(f(x,f(x,x)),f(f(f(f(y,z),z),z),f(z,u))),f(z,z))=z. 731 [para_from,728.1.1,720.1.1.2.2.1] f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z))))=x. 733 [para_into,731.1.1.2,622.1.1] f(f(x,f(y,x)),f(y,x))=x. 737 [para_into,729.1.1,610.1.1,flip.1] f(f(x,f(x,y)),x)=f(x,y). 738 [para_into,737.1.1.1,684.1.1] f(f(x,y),y)=f(y,f(x,y)). 739 [para_into,737.1.1.1,683.1.1] f(f(x,y),x)=f(x,f(x,y)). 740 [para_into,738.1.1,733.1.1,flip.1] f(f(x,y),f(y,f(x,y)))=y. 741 [para_from,738.1.1,569.1.1.2.1] f(x,f(f(y,f(x,y)),f(y,x)))=f(y,x). 743 [para_from,739.1.2,737.1.1.1] f(f(f(x,y),x),x)=f(x,y). 744 [para_from,739.1.2,683.1.1.2] f(x,f(f(x,y),x))=f(x,y). 746 [para_from,743.1.1,709.1.1.1.1] f(f(f(x,y),x),f(y,x))=x. 747 [para_from,743.1.1,672.1.1.2.2.1.1] f(f(x,y),f(f(z,f(z,z)),f(f(f(y,x),y),f(u,y))))=y. 752 [para_from,744.1.1,740.1.1.2] f(f(f(x,y),x),f(x,y))=x. 754 [para_into,746.1.1.1,739.1.1] f(f(x,f(x,y)),f(y,x))=x. 755 [para_into,752.1.1.1,739.1.1] f(f(x,f(x,y)),f(x,y))=x. 759 [para_from,755.1.1,2.1.1.2.2.1.1] f(f(x,y),f(f(f(y,y),f(f(y,x),z)),f(f(f(y,x),y),f(y,u))))=y. 765 [para_into,747.1.1.2.2.1,739.1.1] f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(u,y))))=y. 767 [para_into,765.1.1.1,610.1.1] f(f(x,y),f(f(z,f(z,z)),f(f(x,f(x,f(f(u,f(u,u)),f(x,y)))),f(v,x))))=x. 769 [para_into,730.1.1.1.2.1.1,743.1.1] f(f(f(x,f(x,x)),f(f(f(y,z),y),f(y,u))),f(y,y))=y. 774 [para_into,769.1.1.1.2.1,728.1.1] f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z))=z. 777 [para_into,774.1.1.1.2.2,741.1.1] f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z))=z. 778 [para_from,774.1.1,603.1.1.1,flip.1] f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(y,f(f(x,y),f(y,z))). 779 [para_into,777.1.1.1.2.1,743.1.1] f(f(f(x,f(x,x)),f(f(y,z),f(u,y))),f(y,y))=y. 781 [para_from,779.1.1,603.1.1.1,flip.1] f(f(f(x,y),f(z,x)),f(f(x,y),f(z,x)))=f(x,f(f(x,y),f(z,x))). 784 [para_into,759.1.1.2.1,683.1.1] f(f(x,x),f(f(f(x,x),y),f(f(f(x,x),x),f(x,z))))=x. 786 [para_into,784.1.1.2.2.1,634.1.2] f(f(x,x),f(f(f(x,x),y),f(f(z,f(z,z)),f(x,u))))=x. 792 [para_from,778.1.1,399.1.1.2] f(f(x,y),f(x,f(f(z,x),f(x,y))))=f(f(z,x),f(x,y)). 793 [para_from,781.1.1,399.1.1.2] f(f(x,y),f(y,f(f(y,z),f(x,y))))=f(f(y,z),f(x,y)). 794 [para_into,767.1.1.2.2.1.2,611.1.1] f(f(x,y),f(f(z,f(z,z)),f(f(x,f(x,y)),f(u,x))))=x. 796 [para_from,794.1.1,792.1.1.1] f(x,f(f(x,y),f(f(z,f(x,y)),f(f(x,y),f(f(u,f(u,u)),f(f(x,f(x,y)),f(v,x)))))))=f(f(z,f(x,y)),f(f(x,y),f(f(u,f(u,u)),f(f(x,f(x,y)),f(v,x))))). 798 [para_into,796.1.1.2.2.2,794.1.1,flip.1] f(f(x,f(y,z)),f(f(y,z),f(f(u,f(u,u)),f(f(y,f(y,z)),f(v,y)))))=f(y,f(f(y,z),f(f(x,f(y,z)),y))). 799 [para_into,798.1.1.2,794.1.1,flip.1] f(x,f(f(x,y),f(f(z,f(x,y)),x)))=f(f(z,f(x,y)),x). 800 [para_into,799.1.1.2.2.1,754.1.1,flip.1] f(f(f(x,f(x,y)),f(y,x)),y)=f(y,f(f(y,x),f(x,y))). 801 [para_into,800.1.1.1,754.1.1,flip.1] f(x,f(f(x,y),f(y,x)))=f(y,x). 802 [para_from,801.1.1,793.1.1.2] f(f(x,y),f(x,y))=f(f(y,x),f(x,y)). 803 [para_into,802.1.1,602.1.2] f(f(x,y),f(z,f(z,z)))=f(f(y,x),f(x,y)). 805 [para_from,802.1.1,398.1.1.2] f(x,f(f(y,x),f(x,y)))=f(x,y). 806 [para_from,802.1.1,547.1.1.1] f(f(f(x,y),f(y,x)),f(f(y,x),z))=f(y,x). 808 [para_from,805.1.1,731.1.1.2] f(f(x,f(y,x)),f(x,y))=x. 809 [para_into,808.1.1.1,738.1.2] f(f(f(x,y),y),f(y,x))=y. 810 [para_from,808.1.1,741.1.1.2] f(x,y)=f(y,x). 812 [para_into,810.1.1,777.1.1,flip.1] f(f(x,x),f(f(y,f(y,y)),f(f(z,x),f(u,x))))=x. 816 [para_into,810.1.1,2.1.1,flip.1] f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x))=x. 818 [para_from,810.1.1,2.1.1.2.2.1.1.1.1] f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u))))=y. 821 [para_into,806.1.1.2.1,810.1.2] f(f(f(x,y),f(y,x)),f(f(x,y),z))=f(y,x). 823 [para_into,806.1.1,803.1.2] f(f(f(x,y),f(y,x)),f(z,f(z,z)))=f(x,y). 828 [para_from,821.1.1,625.1.1.2] f(f(f(f(x,y),z),f(u,f(u,u))),f(y,x))=f(f(x,y),z). 832 [para_from,823.1.1,680.1.1.2] f(f(x,f(x,x)),f(y,z))=f(f(y,z),f(z,y)). 834 [para_from,832.1.2,806.1.1.1] f(f(f(x,f(x,x)),f(y,z)),f(f(z,y),u))=f(z,y). 843 [para_from,816.1.1,369.1.1.1] f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u))))=f(y,x). 845 [para_into,843.1.1.2.1,522.1.1] f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z))))=f(y,x). 846 [para_into,845.1.1.2.2.1,809.1.1] f(x,f(f(y,x),f(y,f(f(y,x),z))))=f(y,x). 847 [para_into,846.1.1.2.2.2,846.1.1] f(x,f(f(y,x),f(y,f(z,f(y,x)))))=f(y,x). 850 [para_into,847.1.1.2,792.1.1] f(x,f(f(y,z),f(z,x)))=f(z,x). 857 [para_into,850.1.1.2.2,810.1.2] f(x,f(f(y,z),f(x,z)))=f(z,x). 860 [para_into,857.1.1.2.1,816.1.1] f(x,f(y,f(x,f(z,y))))=f(f(z,y),x). 863 [para_into,857.1.1.2,810.1.2] f(x,f(f(x,y),f(z,y)))=f(y,x). 865 [para_into,863.1.1.2.2,816.1.1] f(x,f(f(x,f(y,z)),z))=f(f(y,z),x). 866 [para_into,863.1.1.2.2,809.1.1] f(x,f(f(x,f(y,z)),y))=f(f(y,z),x). 868 [para_into,863.1.1,810.1.2] f(f(f(x,y),f(z,y)),x)=f(y,x). 870 [para_into,868.1.1.1.2,816.1.1] f(f(f(x,f(y,z)),z),x)=f(f(y,z),x). 874 [para_into,860.1.2,810.1.2] f(x,f(y,f(x,f(z,y))))=f(x,f(z,y)). 875 [para_into,865.1.1.2.1,810.1.2] f(x,f(f(f(y,z),x),z))=f(f(y,z),x). 877 [para_into,865.1.1,786.1.1,flip.1] f(f(x,f(f(y,f(y,y)),f(z,u))),f(z,z))=z. 879 [para_into,866.1.1.2.1,810.1.2] f(x,f(f(f(y,z),x),y))=f(f(y,z),x). 882 [para_into,870.1.1.1.1,810.1.2] f(f(f(f(x,y),z),y),z)=f(f(x,y),z). 885 [para_into,874.1.1.2.2.2,626.1.1,flip.1] f(x,f(f(y,f(z,f(z,z))),f(y,u)))=f(x,f(f(y,u),f(x,y))). 891 [para_into,875.1.1.2,603.1.1,flip.1] f(f(f(x,f(x,x)),y),z)=f(z,f(y,y)). 901 [para_into,891.1.1.1,810.1.2] f(f(x,f(y,f(y,y))),z)=f(z,f(x,x)). 905 [para_into,901.1.1.1,834.1.1,flip.1] f(x,f(f(f(y,f(y,y)),f(z,u)),f(f(y,f(y,y)),f(z,u))))=f(f(u,z),x). 910 [para_into,877.1.1.1.2,390.1.1] f(f(x,f(y,y)),f(f(z,y),f(z,y)))=f(z,y). 911 [para_into,877.1.1,810.1.2] f(f(x,x),f(y,f(f(z,f(z,z)),f(x,u))))=x. 915 [para_into,910.1.1.1,828.1.1] f(f(f(x,x),y),f(f(z,x),f(z,x)))=f(z,x). 923 [para_into,911.1.1.2.2.2,863.1.1] f(f(x,x),f(y,f(f(z,f(z,z)),f(u,x))))=x. 938 [para_into,885.1.1.2,626.1.1,flip.1] f(x,f(f(y,z),f(x,y)))=f(x,y). 939 [para_into,938.1.1.2.2,746.1.1] f(f(f(x,y),x),f(f(f(y,x),z),x))=f(f(f(x,y),x),f(y,x)). 940 [para_into,938.1.1.2,879.1.1] f(f(f(x,y),f(x,z)),f(f(x,y),f(x,z)))=f(f(f(x,y),f(x,z)),x). 942 [para_into,938.1.1.2,810.1.2] f(x,f(f(x,y),f(y,z)))=f(x,y). 947 [para_into,942.1.1,810.1.2] f(f(f(x,y),f(y,z)),x)=f(x,y). 955 [para_into,939.1.2,746.1.1] f(f(f(x,y),x),f(f(f(y,x),z),x))=x. 967 [para_from,940.1.2,923.1.1.2.2.2] f(f(x,x),f(y,f(f(z,f(z,z)),f(f(f(x,u),f(x,v)),f(f(x,u),f(x,v))))))=x. 969 [para_into,905.1.1.2,596.1.1] f(x,f(y,z))=f(f(z,y),x). 978 [para_into,969.1.2.1,901.1.1] f(x,f(y,f(z,f(u,f(u,u)))))=f(f(y,f(z,z)),x). 983 [para_into,969.1.2.1,397.1.1] f(x,f(f(y,y),f(y,z)))=f(y,x). 984 [para_into,969.1.2,942.1.1] f(f(f(f(x,y),z),f(z,u)),f(y,x))=f(f(x,y),z). 986 [para_into,969.1.2,810.1.2] f(x,f(y,z))=f(x,f(z,y)). 991 [para_from,969.1.2,850.1.1.2] f(x,f(f(y,x),f(y,z)))=f(y,x). 995 [para_from,969.1.2,547.1.1.2] f(f(f(x,y),f(x,y)),f(z,f(y,x)))=f(x,y). 1003 [para_into,986.1.1,810.1.2] f(f(x,y),z)=f(z,f(y,x)). 1009 [para_into,1003.1.1.1,1003.1.2] f(f(f(x,y),z),u)=f(u,f(f(y,x),z)). 1010 [para_into,1003.1.1.1,1003.1.1] f(f(x,f(y,z)),u)=f(u,f(x,f(z,y))). 1011 [para_into,1003.1.1.1,986.1.2] f(f(x,f(y,z)),u)=f(u,f(f(z,y),x)). 1012 [para_into,1003.1.2.2,986.1.2] f(f(f(x,y),z),u)=f(u,f(z,f(y,x))). 1029 [para_into,991.1.1.2.2,915.1.1] f(x,f(f(f(f(y,y),z),x),f(u,y)))=f(f(f(y,y),z),x). 1047 [para_into,1009.1.1.1.1,1003.1.1] f(f(f(x,f(y,z)),u),v)=f(v,f(f(x,f(z,y)),u)). 1075 [para_from,995.1.1,812.1.1.2.2.1] f(f(f(x,f(y,z)),f(x,f(y,z))),f(f(u,f(u,u)),f(f(z,y),f(v,f(x,f(y,z))))))=f(x,f(y,z)). 1083 [para_into,1029.1.1.2,1003.1.2] f(x,f(f(y,z),f(f(f(y,y),u),x)))=f(f(f(y,y),u),x). 1084 [para_from,1083.1.1,991.1.1.2] f(x,f(f(f(y,y),z),f(f(y,u),x)))=f(f(y,u),x). 1093 [para_into,967.1.1.2.2,915.1.1] f(f(x,x),f(y,f(f(x,z),f(x,u))))=x. 1103 [para_into,1093.1.1,1010.1.2] f(f(x,f(f(y,z),f(y,u))),f(y,y))=y. 1112 [para_into,1103.1.1,828.1.2] f(f(f(f(x,f(f(y,z),f(y,u))),f(y,y)),f(v,f(v,v))),f(f(f(y,z),f(y,u)),x))=y. 1114 [para_into,1112.1.1.1.1,1103.1.1] f(f(x,f(y,f(y,y))),f(f(f(x,z),f(x,u)),v))=x. 1115 [para_into,1075.1.1.1,778.1.1] f(f(x,f(f(y,x),f(x,z))),f(f(u,f(u,u)),f(f(z,x),f(v,f(f(y,x),f(x,z))))))=f(f(y,x),f(x,z)). 1116 [para_into,1115.1.1.2.2,818.1.1] f(f(x,f(f(f(f(f(y,x),z),z),x),f(x,y))),f(f(u,f(u,u)),x))=f(f(f(f(f(y,x),z),z),x),f(x,y)). 1117 [para_into,1116.1.1,614.1.1,flip.1] f(f(f(f(f(x,y),z),z),y),f(y,x))=y. 1118 [para_into,1117.1.1.1.1,1003.1.1] f(f(f(x,f(x,f(y,z))),z),f(z,y))=z. 1119 [para_into,1117.1.1.1,1012.1.1] f(f(x,f(y,f(y,f(z,x)))),f(x,z))=x. 1121 [para_into,1118.1.1.2,810.1.2] f(f(f(x,f(x,f(y,z))),z),f(y,z))=z. 1122 [para_into,1118.1.1,1003.1.2] f(f(x,y),f(f(z,f(z,f(x,y))),y))=y. 1123 [para_into,1121.1.1.1.1.2,1003.1.2] f(f(f(x,f(f(y,z),x)),y),f(z,y))=y. 1125 [para_into,1122.1.1.1,1119.1.1] f(x,f(f(y,f(y,f(f(x,f(z,f(z,f(u,x)))),f(x,u)))),f(x,u)))=f(x,u). 1126 [para_into,1122.1.1.2.1.2,1003.1.2] f(f(x,y),f(f(z,f(f(y,x),z)),y))=y. 1127 [para_into,1123.1.1,857.1.2] f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),f(f(x,y),f(f(u,f(f(y,x),u)),y))))=y. 1128 [para_into,1125.1.1.2.1.2.2,1119.1.1] f(x,f(f(y,f(y,x)),f(x,z)))=f(x,z). 1131 [para_into,1127.1.1.2.2,1126.1.1] f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y))=y. 1132 [para_from,1131.1.1,1084.1.1.2,flip.1] f(f(x,f(f(y,f(f(z,f(x,x)),y)),z)),z)=f(z,z). 1133 [para_into,1132.1.1.1,1047.1.2] f(f(f(f(x,f(x,f(y,f(z,z)))),y),z),y)=f(y,y). 1134 [para_from,1132.1.1,870.1.1.1,flip.1] f(f(f(x,f(f(y,f(z,z)),x)),y),z)=f(f(y,y),z). 1135 [para_from,1133.1.1,882.1.1.1,flip.1] f(f(f(x,f(x,f(y,f(z,z)))),y),z)=f(f(y,y),z). 1136 [para_into,1134.1.1.1.1.2,882.1.1] f(f(f(x,f(f(y,f(z,z)),x)),f(f(y,f(z,z)),x)),z)=f(f(f(f(y,f(z,z)),x),f(f(y,f(z,z)),x)),z). 1137 [para_into,1134.1.1.1,947.1.1] f(f(x,f(x,f(y,y))),y)=f(f(x,x),y). 1138 [para_into,1137.1.1.1.2,891.1.2] f(f(x,f(f(f(y,f(y,y)),z),x)),z)=f(f(x,x),z). 1140 [para_into,1135.1.1.1.1.2,955.1.1] f(f(f(f(f(f(x,x),y),f(x,x)),f(x,x)),f(f(y,f(x,x)),z)),x)=f(f(f(f(y,f(x,x)),z),f(f(y,f(x,x)),z)),x). 1141 [para_into,1136.1.1.1,733.1.1,flip.1] f(f(f(f(x,f(y,y)),z),f(f(x,f(y,y)),z)),y)=f(z,y). 1142 [para_into,1140.1.1.1.1,743.1.1,flip.1] f(f(f(f(x,f(y,y)),z),f(f(x,f(y,y)),z)),y)=f(f(f(f(y,y),x),f(f(x,f(y,y)),z)),y). 1143 [para_into,1142.1.1,1141.1.1,flip.1] f(f(f(f(x,x),y),f(f(y,f(x,x)),z)),x)=f(z,x). 1144 [para_into,1143.1.1.1.2,1010.1.1] f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x)=f(z,x). 1145 [para_into,1143.1.1.1.2,991.1.1] f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x)=f(f(f(z,f(y,f(x,x))),f(z,u)),x). 1149 [para_into,1145.1.1,1144.1.1,flip.1] f(f(f(x,f(y,f(z,z))),f(x,u)),z)=f(x,z). 1150 [para_into,1149.1.1.1.1.2.2,551.1.1] f(f(f(x,f(y,z)),f(x,u)),f(z,z))=f(x,f(z,z)). 1152 [para_into,1149.1.1.1,1010.1.1] f(f(f(x,y),f(x,f(f(z,z),u))),z)=f(x,z). 1154 [para_into,1152.1.1.1.2.2.1,551.1.1] f(f(f(x,y),f(x,f(z,u))),f(z,z))=f(x,f(z,z)). 1159 [para_into,1150.1.1,1011.1.1] f(f(x,x),f(f(y,z),f(z,f(u,x))))=f(z,f(x,x)). 1164 [para_into,1159.1.1.2,984.1.1] f(f(x,x),f(f(f(y,x),f(z,u)),z))=f(f(z,u),f(x,x)). 1166 [para_into,1159.1.2,1003.1.2] f(f(x,x),f(f(y,z),f(z,f(u,x))))=f(f(x,x),z). 1171 [para_into,1166.1.1.2.2,978.1.1] f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),f(f(z,u),f(f(v,f(x,x)),u)))=f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),u). 1180 [para_into,1171.1.1.1,626.1.1,flip.1] f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z)=f(x,f(f(u,z),f(f(v,f(x,x)),z))). 1184 [para_into,1180.1.1.1,626.1.1,flip.1] f(x,f(f(y,z),f(f(u,f(x,x)),z)))=f(x,z). 1185 [para_into,1184.1.1.2.2.1,1114.1.1] f(f(f(x,y),f(x,z)),f(f(u,v),f(x,v)))=f(f(f(x,y),f(x,z)),v). 1193 [para_into,1185.1.1,1154.1.1,flip.1] f(f(f(x,y),f(x,f(f(x,z),u))),z)=f(x,f(f(x,z),f(x,z))). 1202 [para_into,1193.1.2,863.1.1] f(f(f(x,y),f(x,f(f(x,z),u))),z)=f(z,x). 1206 [para_from,1202.1.1,1138.1.1.1.2] f(f(x,f(x,y)),f(y,f(f(y,x),z)))=f(f(x,x),f(y,f(f(y,x),z))). 1207 [para_from,1206.1.1,1128.1.1.2] f(x,f(f(y,y),f(x,f(f(x,y),z))))=f(x,f(f(x,y),z)). 1208 [para_into,1207.1.1.2.2,810.1.2] f(x,f(f(y,y),f(f(f(x,y),z),x)))=f(x,f(f(x,y),z)). 1209 [para_into,1208.1.1.2,1164.1.1] f(x,f(f(x,y),f(z,z)))=f(x,f(f(x,z),f(x,y))). 1210 [para_into,1209.1.1.2,983.1.1,flip.1] f(x,f(f(x,f(y,y)),f(x,z)))=f(x,f(y,f(x,z))). 1211 [binary,1210.1,3.1] $F. ------------ end of proof -------------