% File: 30instances.goals % % All 30 instances of the 3 aa goals by renaming a single variable. formulas(goals). % a(a(x,y,z),u,w) = 1 *** original goal *** a(a(x,x,z),u,w) = 1 # label("aa1{x1/x2}"). a(a(x,y,x),u,w) = 1 # label("aa1{x1/x3}"). a(a(x,y,z),x,w) = 1 # label("aa1{x1/x4}"). a(a(x,y,z),u,x) = 1 # label("aa1{x1/x5}"). a(a(x,y,y),u,w) = 1 # label("aa1{x2/x3}"). a(a(x,y,z),y,w) = 1 # label("aa1{x2/x4}"). a(a(x,y,z),u,y) = 1 # label("aa1{x2/x5}"). a(a(x,y,z),z,w) = 1 # label("aa1{x3/x4}"). a(a(x,y,z),u,z) = 1 # label("aa1{x3/x5}"). a(a(x,y,z),u,u) = 1 # label("aa1{x4/x5}"). % a(x,a(y,z,u),w) = 1 *** original goal *** a(x,a(x,z,u),w) = 1 # label("aa2{x1/x2}"). a(x,a(y,x,u),w) = 1 # label("aa2{x1/x3}"). a(x,a(y,z,x),w) = 1 # label("aa2{x1/x4}"). a(x,a(y,z,u),x) = 1 # label("aa2{x1/x5}"). a(x,a(y,y,u),w) = 1 # label("aa2{x2/x3}"). a(x,a(y,z,y),w) = 1 # label("aa2{x2/x4}"). a(x,a(y,z,u),y) = 1 # label("aa2{x2/x5}"). a(x,a(y,z,z),w) = 1 # label("aa2{x3/x4}"). a(x,a(y,z,u),z) = 1 # label("aa2{x3/x5}"). a(x,a(y,z,u),u) = 1 # label("aa2{x4/x5}"). a(x,y,a(z,u,w)) = 1 *** original goal *** a(x,x,a(z,u,w)) = 1 # label("aa3{x1/x2}"). a(x,y,a(x,u,w)) = 1 # label("aa3{x1/x3}"). a(x,y,a(z,x,w)) = 1 # label("aa3{x1/x4}"). a(x,y,a(z,u,x)) = 1 # label("aa3{x1/x5}"). a(x,y,a(y,u,w)) = 1 # label("aa3{x2/x3}"). a(x,y,a(z,y,w)) = 1 # label("aa3{x2/x4}"). a(x,y,a(z,u,y)) = 1 # label("aa3{x2/x5}"). a(x,y,a(z,z,w)) = 1 # label("aa3{x3/x4}"). a(x,y,a(z,u,z)) = 1 # label("aa3{x3/x5}"). a(x,y,a(z,u,u)) = 1 # label("aa3{x4/x5}"). end_of_list.