% File: 120aaeq.goals % % 60/120 proved permutations of aa3 in aa1_eq_aa3 % 60/120 proved permutations of aa3 in aa2_eq_aa3 formulas(goals). % aa1_eq_aa3: 60/120 permutations of aa3 a(a(x,y,z),u,w) = a(x,y,a(z,u,w)) # label("aa1_eq_aa3 (12345)"). a(a(x,y,z),u,w) = a(x,y,a(u,w,z)) # label("aa1_eq_aa3 (12453)"). a(a(x,y,z),u,w) = a(x,y,a(w,z,u)) # label("aa1_eq_aa3 (12534)"). a(a(x,y,z),u,w) = a(x,z,a(y,w,u)) # label("aa1_eq_aa3 (13254)"). a(a(x,y,z),u,w) = a(x,z,a(u,y,w)) # label("aa1_eq_aa3 (13425)"). a(a(x,y,z),u,w) = a(x,z,a(w,u,y)) # label("aa1_eq_aa3 (13542)"). a(a(x,y,z),u,w) = a(x,u,a(y,z,w)) # label("aa1_eq_aa3 (14235)"). a(a(x,y,z),u,w) = a(x,u,a(z,w,y)) # label("aa1_eq_aa3 (14352)"). a(a(x,y,z),u,w) = a(x,u,a(w,y,z)) # label("aa1_eq_aa3 (14523)"). a(a(x,y,z),u,w) = a(x,w,a(y,u,z)) # label("aa1_eq_aa3 (15243)"). a(a(x,y,z),u,w) = a(x,w,a(z,y,u)) # label("aa1_eq_aa3 (15324)"). a(a(x,y,z),u,w) = a(x,w,a(u,z,y)) # label("aa1_eq_aa3 (15432)"). a(a(x,y,z),u,w) = a(y,x,a(z,w,u)) # label("aa1_eq_aa3 (21354)"). a(a(x,y,z),u,w) = a(y,x,a(u,z,w)) # label("aa1_eq_aa3 (21435)"). a(a(x,y,z),u,w) = a(y,x,a(w,u,z)) # label("aa1_eq_aa3 (21543)"). a(a(x,y,z),u,w) = a(y,z,a(x,u,w)) # label("aa1_eq_aa3 (23145)"). a(a(x,y,z),u,w) = a(y,z,a(u,w,x)) # label("aa1_eq_aa3 (23451)"). a(a(x,y,z),u,w) = a(y,z,a(w,x,u)) # label("aa1_eq_aa3 (23514)"). a(a(x,y,z),u,w) = a(y,u,a(x,w,z)) # label("aa1_eq_aa3 (24153)"). a(a(x,y,z),u,w) = a(y,u,a(z,x,w)) # label("aa1_eq_aa3 (24315)"). a(a(x,y,z),u,w) = a(y,u,a(w,z,x)) # label("aa1_eq_aa3 (24531)"). a(a(x,y,z),u,w) = a(y,w,a(x,z,u)) # label("aa1_eq_aa3 (25134)"). a(a(x,y,z),u,w) = a(y,w,a(z,u,x)) # label("aa1_eq_aa3 (25341)"). a(a(x,y,z),u,w) = a(y,w,a(u,x,z)) # label("aa1_eq_aa3 (25413)"). a(a(x,y,z),u,w) = a(z,x,a(y,u,w)) # label("aa1_eq_aa3 (31245)"). a(a(x,y,z),u,w) = a(z,x,a(u,w,y)) # label("aa1_eq_aa3 (31452)"). a(a(x,y,z),u,w) = a(z,x,a(w,y,u)) # label("aa1_eq_aa3 (31524)"). a(a(x,y,z),u,w) = a(z,y,a(x,w,u)) # label("aa1_eq_aa3 (32154)"). a(a(x,y,z),u,w) = a(z,y,a(u,x,w)) # label("aa1_eq_aa3 (32415)"). a(a(x,y,z),u,w) = a(z,y,a(w,u,x)) # label("aa1_eq_aa3 (32541)"). a(a(x,y,z),u,w) = a(z,u,a(x,y,w)) # label("aa1_eq_aa3 (34125)"). a(a(x,y,z),u,w) = a(z,u,a(y,w,x)) # label("aa1_eq_aa3 (34251)"). a(a(x,y,z),u,w) = a(z,u,a(w,x,y)) # label("aa1_eq_aa3 (34512)"). a(a(x,y,z),u,w) = a(z,w,a(x,u,y)) # label("aa1_eq_aa3 (35142)"). a(a(x,y,z),u,w) = a(z,w,a(y,x,u)) # label("aa1_eq_aa3 (35214)"). a(a(x,y,z),u,w) = a(z,w,a(u,y,x)) # label("aa1_eq_aa3 (35421)"). a(a(x,y,z),u,w) = a(u,x,a(y,w,z)) # label("aa1_eq_aa3 (41253)"). a(a(x,y,z),u,w) = a(u,x,a(z,y,w)) # label("aa1_eq_aa3 (41325)"). a(a(x,y,z),u,w) = a(u,x,a(w,z,y)) # label("aa1_eq_aa3 (41532)"). a(a(x,y,z),u,w) = a(u,y,a(x,z,w)) # label("aa1_eq_aa3 (42135)"). a(a(x,y,z),u,w) = a(u,y,a(z,w,x)) # label("aa1_eq_aa3 (42351)"). a(a(x,y,z),u,w) = a(u,y,a(w,x,z)) # label("aa1_eq_aa3 (42513)"). a(a(x,y,z),u,w) = a(u,z,a(x,w,y)) # label("aa1_eq_aa3 (43152)"). a(a(x,y,z),u,w) = a(u,z,a(y,x,w)) # label("aa1_eq_aa3 (43215)"). a(a(x,y,z),u,w) = a(u,z,a(w,y,x)) # label("aa1_eq_aa3 (43521)"). a(a(x,y,z),u,w) = a(u,w,a(x,y,z)) # label("aa1_eq_aa3 (45123)"). a(a(x,y,z),u,w) = a(u,w,a(y,z,x)) # label("aa1_eq_aa3 (45231)"). a(a(x,y,z),u,w) = a(u,w,a(z,x,y)) # label("aa1_eq_aa3 (45312)"). a(a(x,y,z),u,w) = a(w,x,a(y,z,u)) # label("aa1_eq_aa3 (51234)"). a(a(x,y,z),u,w) = a(w,x,a(z,u,y)) # label("aa1_eq_aa3 (51342)"). a(a(x,y,z),u,w) = a(w,x,a(u,y,z)) # label("aa1_eq_aa3 (51423)"). a(a(x,y,z),u,w) = a(w,y,a(x,u,z)) # label("aa1_eq_aa3 (52143)"). a(a(x,y,z),u,w) = a(w,y,a(z,x,u)) # label("aa1_eq_aa3 (52314)"). a(a(x,y,z),u,w) = a(w,y,a(u,z,x)) # label("aa1_eq_aa3 (52431)"). a(a(x,y,z),u,w) = a(w,z,a(x,y,u)) # label("aa1_eq_aa3 (53124)"). a(a(x,y,z),u,w) = a(w,z,a(y,u,x)) # label("aa1_eq_aa3 (53241)"). a(a(x,y,z),u,w) = a(w,z,a(u,x,y)) # label("aa1_eq_aa3 (53412)"). a(a(x,y,z),u,w) = a(w,u,a(x,z,y)) # label("aa1_eq_aa3 (54132)"). a(a(x,y,z),u,w) = a(w,u,a(y,x,z)) # label("aa1_eq_aa3 (54213)"). a(a(x,y,z),u,w) = a(w,u,a(z,y,x)) # label("aa1_eq_aa3 (54321)"). % aa2_eq_aa3: 60/120 permutations of aa3 a(x,a(y,z,u),w) = a(x,y,a(z,u,w)) # label("aa2_eq_aa3 (12345)"). a(x,a(y,z,u),w) = a(x,y,a(u,w,z)) # label("aa2_eq_aa3 (12453)"). a(x,a(y,z,u),w) = a(x,y,a(w,z,u)) # label("aa2_eq_aa3 (12534)"). a(x,a(y,z,u),w) = a(x,z,a(y,w,u)) # label("aa2_eq_aa3 (13254)"). a(x,a(y,z,u),w) = a(x,z,a(u,y,w)) # label("aa2_eq_aa3 (13425)"). a(x,a(y,z,u),w) = a(x,z,a(w,u,y)) # label("aa2_eq_aa3 (13542)"). a(x,a(y,z,u),w) = a(x,u,a(y,z,w)) # label("aa2_eq_aa3 (14235)"). a(x,a(y,z,u),w) = a(x,u,a(z,w,y)) # label("aa2_eq_aa3 (14352)"). a(x,a(y,z,u),w) = a(x,u,a(w,y,z)) # label("aa2_eq_aa3 (14523)"). a(x,a(y,z,u),w) = a(x,w,a(y,u,z)) # label("aa2_eq_aa3 (15243)"). a(x,a(y,z,u),w) = a(x,w,a(z,y,u)) # label("aa2_eq_aa3 (15324)"). a(x,a(y,z,u),w) = a(x,w,a(u,z,y)) # label("aa2_eq_aa3 (15432)"). a(x,a(y,z,u),w) = a(y,x,a(z,w,u)) # label("aa2_eq_aa3 (21354)"). a(x,a(y,z,u),w) = a(y,x,a(u,z,w)) # label("aa2_eq_aa3 (21435)"). a(x,a(y,z,u),w) = a(y,x,a(w,u,z)) # label("aa2_eq_aa3 (21543)"). a(x,a(y,z,u),w) = a(y,z,a(x,u,w)) # label("aa2_eq_aa3 (23145)"). a(x,a(y,z,u),w) = a(y,z,a(u,w,x)) # label("aa2_eq_aa3 (23451)"). a(x,a(y,z,u),w) = a(y,z,a(w,x,u)) # label("aa2_eq_aa3 (23514)"). a(x,a(y,z,u),w) = a(y,u,a(x,w,z)) # label("aa2_eq_aa3 (24153)"). a(x,a(y,z,u),w) = a(y,u,a(z,x,w)) # label("aa2_eq_aa3 (24315)"). a(x,a(y,z,u),w) = a(y,u,a(w,z,x)) # label("aa2_eq_aa3 (24531)"). a(x,a(y,z,u),w) = a(y,w,a(x,z,u)) # label("aa2_eq_aa3 (25134)"). a(x,a(y,z,u),w) = a(y,w,a(z,u,x)) # label("aa2_eq_aa3 (25341)"). a(x,a(y,z,u),w) = a(y,w,a(u,x,z)) # label("aa2_eq_aa3 (25413)"). a(x,a(y,z,u),w) = a(z,x,a(y,u,w)) # label("aa2_eq_aa3 (31245)"). a(x,a(y,z,u),w) = a(z,x,a(u,w,y)) # label("aa2_eq_aa3 (31452)"). a(x,a(y,z,u),w) = a(z,x,a(w,y,u)) # label("aa2_eq_aa3 (31524)"). a(x,a(y,z,u),w) = a(z,y,a(x,w,u)) # label("aa2_eq_aa3 (32154)"). a(x,a(y,z,u),w) = a(z,y,a(u,x,w)) # label("aa2_eq_aa3 (32415)"). a(x,a(y,z,u),w) = a(z,y,a(w,u,x)) # label("aa2_eq_aa3 (32541)"). a(x,a(y,z,u),w) = a(z,u,a(x,y,w)) # label("aa2_eq_aa3 (34125)"). a(x,a(y,z,u),w) = a(z,u,a(y,w,x)) # label("aa2_eq_aa3 (34251)"). a(x,a(y,z,u),w) = a(z,u,a(w,x,y)) # label("aa2_eq_aa3 (34512)"). a(x,a(y,z,u),w) = a(z,w,a(x,u,y)) # label("aa2_eq_aa3 (35142)"). a(x,a(y,z,u),w) = a(z,w,a(y,x,u)) # label("aa2_eq_aa3 (35214)"). a(x,a(y,z,u),w) = a(z,w,a(u,y,x)) # label("aa2_eq_aa3 (35421)"). a(x,a(y,z,u),w) = a(u,x,a(y,w,z)) # label("aa2_eq_aa3 (41253)"). a(x,a(y,z,u),w) = a(u,x,a(z,y,w)) # label("aa2_eq_aa3 (41325)"). a(x,a(y,z,u),w) = a(u,x,a(w,z,y)) # label("aa2_eq_aa3 (41532)"). a(x,a(y,z,u),w) = a(u,y,a(x,z,w)) # label("aa2_eq_aa3 (42135)"). a(x,a(y,z,u),w) = a(u,y,a(z,w,x)) # label("aa2_eq_aa3 (42351)"). a(x,a(y,z,u),w) = a(u,y,a(w,x,z)) # label("aa2_eq_aa3 (42513)"). a(x,a(y,z,u),w) = a(u,z,a(x,w,y)) # label("aa2_eq_aa3 (43152)"). a(x,a(y,z,u),w) = a(u,z,a(y,x,w)) # label("aa2_eq_aa3 (43215)"). a(x,a(y,z,u),w) = a(u,z,a(w,y,x)) # label("aa2_eq_aa3 (43521)"). a(x,a(y,z,u),w) = a(u,w,a(x,y,z)) # label("aa2_eq_aa3 (45123)"). a(x,a(y,z,u),w) = a(u,w,a(y,z,x)) # label("aa2_eq_aa3 (45231)"). a(x,a(y,z,u),w) = a(u,w,a(z,x,y)) # label("aa2_eq_aa3 (45312)"). a(x,a(y,z,u),w) = a(w,x,a(y,z,u)) # label("aa2_eq_aa3 (51234)"). a(x,a(y,z,u),w) = a(w,x,a(z,u,y)) # label("aa2_eq_aa3 (51342)"). a(x,a(y,z,u),w) = a(w,x,a(u,y,z)) # label("aa2_eq_aa3 (51423)"). a(x,a(y,z,u),w) = a(w,y,a(x,u,z)) # label("aa2_eq_aa3 (52143)"). a(x,a(y,z,u),w) = a(w,y,a(z,x,u)) # label("aa2_eq_aa3 (52314)"). a(x,a(y,z,u),w) = a(w,y,a(u,z,x)) # label("aa2_eq_aa3 (52431)"). a(x,a(y,z,u),w) = a(w,z,a(x,y,u)) # label("aa2_eq_aa3 (53124)"). a(x,a(y,z,u),w) = a(w,z,a(y,u,x)) # label("aa2_eq_aa3 (53241)"). a(x,a(y,z,u),w) = a(w,z,a(u,x,y)) # label("aa2_eq_aa3 (53412)"). a(x,a(y,z,u),w) = a(w,u,a(x,z,y)) # label("aa2_eq_aa3 (54132)"). a(x,a(y,z,u),w) = a(w,u,a(y,x,z)) # label("aa2_eq_aa3 (54213)"). a(x,a(y,z,u),w) = a(w,u,a(z,y,x)) # label("aa2_eq_aa3 (54321)"). end_of_list.