set(hyper_res). assign(max_mem,900000). % assign(max_seconds,10). % set(sos_queue). assign(max_weight,48). assign(max_proofs,9). assign(pick_given_ratio,4). assign(bsub_hint_wt,1). clear(keep_hint_subsumers). set(keep_hint_equivalents). % set(ancestor_subsume). set(back_sub). set(order_history). % set(process_input). clear(print_kept). % clear(print_given). % clear(print_proofs). list(hints). % Following 90 srted from uu, proing the various shortest single P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),v6),e(w,v6))). P(e(e(e(e(e(e(e(x,y),e(z,y)),z),x),u),e(v,u)),v)). P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),e(e(e(w,v6),e(v7,v6)),v7)),w)). P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))). P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),v7),e(v6,v7))). P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w)),e(v6,e(e(e(v6,v7),e(v8,v7)),v8)))). P(e(e(e(e(e(x,e(x,y)),y),z),e(u,z)),u)). P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)). P(e(e(e(e(e(x,y),e(e(y,z),e(x,z))),u),e(v,u)),v)). P(e(e(e(e(e(x,y),e(z,y)),z),u),e(x,u))). P(e(e(e(e(e(x,y),x),z),u),e(e(y,z),u))). P(e(e(e(e(e(x,y),z),e(y,z)),u),e(x,u))). P(e(e(e(e(e(x,y),z),x),z),y)). P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),e(v7,v6)),v7)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(u,v),e(w,v)),w),u),v6)),v7),e(v6,v7))). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9))),v10),e(v9,v10))). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))). P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). P(e(e(e(e(x,e(x,y)),y),z),z)). P(e(e(e(e(x,x),y),e(z,y)),z)). P(e(e(e(e(x,x),y),z),e(y,z))). P(e(e(e(e(x,y),e(z,y)),u),e(e(z,x),u))). P(e(e(e(e(x,y),e(z,y)),z),x)). P(e(e(e(e(x,y),x),z),e(y,z))). P(e(e(e(e(x,y),y),z),e(x,z))). P(e(e(e(e(x,y),z),e(y,z)),x)). P(e(e(e(e(x,y),z),u),e(u,e(x,e(y,z))))). P(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(e(e(v,w),e(v6,w)),v6)),v)). P(e(e(e(x,e(e(y,z),y)),x),z)). P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))). P(e(e(e(x,e(y,e(y,z))),x),z)). P(e(e(e(x,e(y,z)),y),e(z,x))). P(e(e(e(x,e(y,z)),z),e(y,x))). P(e(e(e(x,x),y),y)). P(e(e(e(x,y),e(x,z)),e(z,y))). P(e(e(e(x,y),x),y)). P(e(e(e(x,y),y),x)). P(e(e(e(x,y),z),e(e(y,x),z))). P(e(e(e(x,y),z),e(e(z,x),y))). P(e(e(e(x,y),z),e(x,e(y,z)))). P(e(e(e(x,y),z),e(y,e(x,z)))). P(e(e(e(x,y),z),e(y,e(z,x)))). P(e(e(x,e(e(y,z),e(x,y))),z)). P(e(e(x,e(e(y,z),y)),e(z,x))). P(e(e(x,e(x,y)),y)). P(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x)). P(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(v,e(x,v)))). P(e(e(x,e(y,e(e(z,y),z))),x)). P(e(e(x,e(y,e(y,z))),e(x,z))). P(e(e(x,e(y,x)),y)). P(e(e(x,e(y,y)),x)). P(e(e(x,e(y,z)),e(e(u,y),e(x,e(u,z))))). P(e(e(x,e(y,z)),e(e(x,e(u,z)),e(u,y)))). P(e(e(x,e(y,z)),e(e(y,x),z))). P(e(e(x,e(y,z)),e(e(z,y),x))). P(e(e(x,e(y,z)),e(x,e(z,y)))). P(e(e(x,e(y,z)),e(z,e(x,y)))). P(e(e(x,e(y,z)),e(z,e(y,x)))). P(e(e(x,x),e(y,y))). P(e(e(x,y),e(e(e(z,x),z),y))). P(e(e(x,y),e(e(x,z),e(z,y)))). P(e(e(x,y),e(e(y,e(x,z)),z))). P(e(e(x,y),e(e(y,z),e(x,z)))). P(e(e(x,y),e(e(z,x),e(y,z)))). P(e(e(x,y),e(e(z,y),e(x,z)))). P(e(e(x,y),e(y,x))). P(e(e(x,y),e(z,e(e(y,z),x)))). P(e(e(x,y),e(z,e(e(z,y),x)))). P(e(e(x,y),e(z,e(y,e(x,z))))). P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),x)),v7),e(v8,v7)),v8))). P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))). P(e(x,e(e(e(x,y),z),e(y,z)))). P(e(x,e(e(e(x,y),z),e(z,y)))). P(e(x,e(e(x,y),y))). P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(x,e(v,e(e(e(v,w),e(v6,w)),v6)))))). P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). P(e(x,e(e(y,e(x,z)),e(z,y)))). P(e(x,e(e(y,e(z,x)),e(z,y)))). P(e(x,e(e(y,x),y))). P(e(x,e(e(y,y),x))). P(e(x,e(e(y,z),e(e(x,z),y)))). P(e(x,e(e(y,z),e(e(y,x),z)))). P(e(x,e(e(y,z),e(e(z,x),y)))). P(e(x,e(x,e(y,y)))). P(e(x,e(y,e(e(e(x,z),y),z)))). P(e(x,e(y,e(x,y)))). P(e(x,e(y,e(y,x)))). P(e(x,x)). % Following 25/19? prove the independent join, from temp.xcb.exp6.out9p, but the 17th replaced by an Ulrich simplification P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))). P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))). P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),v6),e(w,v6))). P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),x)),v7),e(v8,v7)),v8))). P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),e(v7,v6)),v7)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9))),v10),e(v9,v10))). P(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x)). P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),v7),e(v6,v7))). P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)). P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w)),e(v6,e(e(e(v6,v7),e(v8,v7)),v8)))). P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))). P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))). P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,v),e(w,v)),w)),u)). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),e(e(e(w,v6),e(v7,v6)),v7)),w)). P(e(e(e(e(x,y),e(z,y)),z),x)). P(e(e(e(e(e(e(e(x,y),e(z,y)),z),x),u),e(v,u)),v)). P(e(e(e(x,y),x),y)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(u,v),e(w,v)),w),u),v6)),v7),e(v6,v7))). P(e(e(x,y),e(e(y,z),e(x,z)))). P(e(e(x,y),e(e(e(z,x),z),y))). P(e(e(e(e(e(x,y),x),z),u),e(e(y,z),u))). P(e(e(x,y),e(y,x))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),v6),e(w,v6))). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),x)),v7),e(v8,v7)),v8))). % P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),e(v7,v6)),v7)). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9))),v10),e(v9,v10))). % P(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),v7),e(v6,v7))). % P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)). % P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). % P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w)),e(v6,e(e(e(v6,v7),e(v8,v7)),v8)))). % P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))). % P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),e(e(e(w,v6),e(v7,v6)),v7)),w)). % P(e(e(e(e(x,y),e(z,y)),z),x)). % P(e(x,x)). % P(e(e(e(e(e(e(e(x,y),e(z,y)),z),x),u),e(v,u)),v)). % P(e(e(e(e(x,x),y),e(z,y)),z)). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(u,v),e(w,v)),w),u),v6)),v7),e(v6,v7))). % P(e(e(x,y),e(e(y,z),e(x,z)))). % P(e(e(e(e(x,y),e(z,y)),u),e(e(z,x),u))). % P(e(e(x,e(y,y)),x)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))). P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))). P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),v6),e(w,v6))). P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),x)),v7),e(v8,v7)),v8))). P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),e(v7,v6)),v7)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9))),v10),e(v9,v10))). P(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x)). P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),v7),e(v6,v7))). P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)). P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w)),e(v6,e(e(e(v6,v7),e(v8,v7)),v8)))). P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))). P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))). P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),e(e(e(w,v6),e(v7,v6)),v7)),w)). P(e(e(e(e(x,y),e(z,y)),z),x)). P(e(e(e(e(e(e(e(x,y),e(z,y)),z),x),u),e(v,u)),v)). P(e(e(e(x,y),x),y)). P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(u,v),e(w,v)),w),u),v6)),v7),e(v6,v7))). P(e(e(x,y),e(e(y,z),e(x,z)))). P(e(e(x,y),e(e(e(z,x),z),y))). P(e(e(e(e(e(x,y),x),z),u),e(e(y,z),u))). P(e(e(x,y),e(y,x))). % P(e(e(x,y),e(y,x))). % % Following Proof of Reflexivity from XCB % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(v6,w)),v6)). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6))). % P(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x)). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6)),v7),v8),v9),e(v8,v9))),v10),e(v11,v10)),v11)). % P(e(e(x,e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),e(v10,v9))),v10)),x)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6))),v7)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u)). % P(e(x,x)). % % Following 13 prove a generalization of a Wajsberg, from temp.xcb.exp2.out1 % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). % P(e(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w)). % P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),w),e(v,w))). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w))). % P(e(x,e(e(y,e(e(z,e(e(e(z,u),e(v,u)),v)),y)),x))). % P(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6)))). % P(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(u,v),e(w,v)),w))). % P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),e(v8,v7)),v8)). % P(e(e(e(x,y),x),y)). % % Following 71 sorted prove f7b and f7e, queue, from temp.xcb.exp1.out1. % P(e(e(e(e(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w),v6),e(v7,v6)),v7),v8),e(v9,v8)),v9)). % P(e(e(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6)),v7),e(v8,v7)),v8)). % P(e(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),e(v7,v6)),v7),v8),e(v9,v8)),v9)). % P(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(v6,w)),v6),e(e(e(e(v7,e(e(e(v7,v8),e(v9,v8)),v9)),v10),v11),e(v10,v11)))). % P(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6)),e(e(e(e(v7,e(e(e(v7,v8),e(v9,v8)),v9)),v10),v11),e(v10,v11)))). % P(e(e(e(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x),v),e(w,v)),w),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)),v10),e(v11,v10)),v11)). % P(e(e(e(e(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)),v10),v11),e(v10,v11))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(e(w,v6),w),v6),v7)),v8),e(v7,v8))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),e(v8,v7)),v8)). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),w),e(v,w)),e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v10),e(v9,v10)))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),v6),e(w,v6))). % P(e(e(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x),v),e(w,v)),w),e(e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v9),v10),v11)),e(v10,v11))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v9)),e(v8,v9))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(e(e(w,v6),e(v7,v6)),v7))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),e(e(e(v7,v8),e(v9,v8)),v9))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w)). % P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))). % P(e(e(e(e(e(e(x,y),x),y),z),e(u,z)),u)). % P(e(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),w),e(v,w))),x),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6),v7),e(v8,v7)),v8)),v9),e(v10,v9)),v10)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6)),v7),e(v8,v7)),v8)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6)),v7),v8),e(v7,v8))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(e(e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),e(v9,v8)),v9),v10),v11),e(v10,v11)))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(e(e(v,w),e(v6,w)),v6))). % P(e(e(e(e(e(x,e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),v)),x),w),e(v6,w)),v6)). % P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v8)),v))),x),v9),e(v10,v9)),v10)). % P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w)),e(v6,e(e(e(v6,v7),e(v8,v7)),v8)))). % P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)). % P(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x),v),e(w,v)),w)). % P(e(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),e(v9,v8)),v9)). % P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v9),v10)),v11),e(v10,v11))). % P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),e(v7,v6)),v7)). % P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),v7),e(v6,v7))). % P(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),w),e(v,w))),x),e(e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v9),v10),e(v11,v10))),v11)). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9))),v10),e(v9,v10))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(v7,e(e(e(v7,v8),e(v9,v8)),v9)),v6)),v10))),v11),e(v10,v11))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(e(e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),v8),v9),e(v8,v9)))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(e(e(e(e(v,e(e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v9),e(v8,v9))),v),v10),v11),e(v10,v11)))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(v,e(e(e(v,w),e(v6,w)),v6)))). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v8)),v))),x),e(e(e(v9,v10),e(v11,v10)),v11)),v9)). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v)),x))),v8),e(v9,v8)),v9)). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w))). % P(e(e(e(e(x,y),e(z,y)),z),x)). % P(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),v8)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6),v7),e(v8,v7))),v8)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),v8),v9),e(v8,v9)))),u)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(v,e(e(e(v,w),e(v6,w)),v6)))),u)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),v8),e(v9,v8)),v9),u))). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),u))). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(u,v),e(w,v)),w))). % P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))). % P(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),w),e(v,w))),x)). % P(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6)),v7))). % P(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v7),e(v6,v7)))). % P(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v8)),v))),x)). % P(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x)). % P(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x)). % P(e(e(x,e(y,x)),y)). % P(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),v6),e(v7,v6)),v7),x))). % P(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7))). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),x)),v7),e(v8,v7)),v8))). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x))). % P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). % P(e(x,e(y,e(x,y)))). % % Following 30 sorted from temp.xcb.exp2.ot3a purport to prove the remaining of the 15 7-symbol, including symmetry, excluding f7k. % P(e(e(e(e(e(e(x,y),x),y),z),u),e(z,u))). % P(e(e(e(e(e(x,e(y,x)),z),e(u,z)),u),y)). % P(e(e(e(e(e(x,e(y,y)),x),z),e(u,z)),u)). % P(e(e(e(e(e(x,e(y,y)),x),z),u),e(z,u))). % P(e(e(e(e(e(x,x),e(y,y)),z),e(u,z)),u)). % P(e(e(e(e(e(x,x),e(y,y)),z),u),e(z,u))). % P(e(e(e(e(x,e(y,e(x,y))),z),e(u,z)),u)). % P(e(e(e(e(x,e(y,e(x,y))),z),u),e(z,u))). % P(e(e(e(e(x,x),y),e(z,y)),z)). % P(e(e(e(e(x,y),e(z,y)),z),e(e(u,x),u))). % P(e(e(e(e(x,y),x),z),e(y,z))). % P(e(e(e(e(x,y),y),z),e(x,z))). % P(e(e(e(e(x,y),z),e(y,z)),x)). % P(e(e(e(x,e(y,x)),z),e(y,z))). % P(e(e(e(x,x),y),y)). % P(e(e(e(x,y),e(e(e(y,z),e(u,z)),u)),x)). % P(e(e(e(x,y),x),e(z,e(z,y)))). % P(e(e(e(x,y),y),x)). % P(e(e(x,e(x,y)),y)). % P(e(e(x,e(y,y)),x)). % P(e(e(x,x),e(e(e(y,z),y),z))). % P(e(e(x,x),e(y,y))). % P(e(e(x,y),e(e(e(z,x),z),y))). % P(e(e(x,y),e(y,x))). % P(e(x,e(e(e(y,z),y),e(x,z)))). % P(e(x,e(e(x,y),y))). % P(e(x,e(e(y,x),y))). % P(e(x,e(e(y,y),x))). % P(e(x,e(x,e(y,y)))). % P(e(x,e(y,e(y,x)))). % % % Following Proof of Reflexivity from XCB % % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)). % % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(v6,w)),v6)). % % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))). % % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6))). % % P(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x)). % % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))). % % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6)),v7),v8),v9),e(v8,v9))),v10),e(v11,v10)),v11)). % % P(e(e(x,e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),e(v10,v9))),v10)),x)). % % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6))),v7)). % % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u)). % % P(e(x,x)). % % % Following are proof steps for XHN implies UM. % % P(e(e(x,y),e(e(y,e(z,e(e(u,v),e(e(v,z),u)))),x))). % % P(e(e(e(e(x,e(y,e(e(z,u),e(e(u,y),z)))),v),e(w,e(e(v6,v7),e(e(v7,w),v6)))),e(v,x))). % % P(e(e(e(e(x,y),e(e(y,z),x)),e(u,e(e(v,w),e(e(w,u),v)))),z)). % % P(e(e(x,e(e(y,z),e(e(z,x),y))),e(e(e(u,v),e(e(v,e(w,e(v6,e(e(v7,v8),e(e(v8,v6),v7))))),u)),w))). % % P(e(e(x,e(y,e(e(z,u),e(e(u,y),z)))),e(e(e(v,w),e(e(w,x),v)),e(v6,e(e(v7,v8),e(e(v8,v6),v7)))))). % % P(e(e(e(x,y),e(e(y,e(z,e(u,e(e(v,w),e(e(w,u),v))))),x)),z)). % % P(e(e(x,y),e(e(y,e(e(e(z,u),e(e(u,e(v,e(w,e(e(v6,v7),e(e(v7,w),v6))))),z)),v)),x))). % % P(e(e(e(e(x,y),e(e(y,z),x)),e(e(e(u,v),e(e(v,e(w,e(v6,e(e(v7,v8),e(e(v8,v6),v7))))),u)),w)),z)). % % P(e(e(x,e(e(x,y),e(z,e(e(u,v),e(e(v,z),u))))),e(y,e(w,e(e(v6,v7),e(e(v7,w),v6)))))). % % P(e(e(e(e(x,e(e(y,z),e(e(z,x),y))),u),u),e(v,e(e(w,v6),e(e(v6,v),w))))). % % P(e(e(e(x,y),e(e(y,e(e(e(z,e(e(u,v),e(e(v,z),u))),w),w)),x)),e(v6,e(e(v7,v8),e(e(v8,v6),v7))))). % % P(e(e(e(x,e(e(y,z),e(e(z,x),y))),u),u)). % % P(e(e(e(e(x,e(e(y,z),e(e(z,x),y))),e(e(e(u,e(e(v,w),e(e(w,u),v))),v6),v6)),v7),v7)). % % P(e(e(e(e(x,y),z),e(y,e(u,e(e(v,w),e(e(w,u),v))))),e(z,x))). % % P(e(e(x,y),e(e(y,e(e(z,e(e(u,v),e(e(v,z),u))),e(e(e(w,e(e(v6,v7),e(e(v7,w),v6))),v8),v8))),x))). % % P(e(e(x,e(e(y,z),e(e(z,e(u,x)),y))),u)). % % P(e(e(e(e(e(x,e(e(y,z),e(e(z,x),y))),u),u),v),e(e(w,v6),e(e(v6,v),w)))). % % P(e(x,e(e(y,e(e(z,u),e(e(u,y),z))),e(e(e(v,w),e(e(w,e(v6,x)),v)),v6)))). % % P(e(e(e(x,y),z),e(y,e(z,x)))). end_of_list. list(usable). % -P(e(x,y)) | -P(x) | P(y). -P(e(x,y)) | -P(x) | P(y) | $Ans(clause_number=$NEXT_CL_NUM, length_major=count(e(x,y)), length_minor=count(x), length_conclusion=count(y)). -P(e(e(a,b),e(b,a))) | -P(e(e(a,b),e(e(b,c),e(a,c)))) | $ANSWER(all_s_t_indep). end_of_list. list(sos). P(e(x,e(e(e(x,y),e(z,y)),z))). % XCB % % Following Proof of Reflexivity from XCB % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(v6,w)),v6)). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6))). % P(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x)). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6)),v7),v8),v9),e(v8,v9))),v10),e(v11,v10)),v11)). % P(e(e(x,e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),e(v10,v9))),v10)),x)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6))),v7)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u)). % P(e(x,x)). % % Following 13 prove a generalization of a Wajsberg, from temp.xcb.exp2.out1 % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). % P(e(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w)). % P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),w),e(v,w))). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w))). % P(e(x,e(e(y,e(e(z,e(e(e(z,u),e(v,u)),v)),y)),x))). % P(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6)))). % P(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(u,v),e(w,v)),w))). % P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),e(v8,v7)),v8)). % P(e(e(e(x,y),x),y)). % % Following 71 sorted prove f7b and f7e, queue, from temp.xcb.exp1.out1. % P(e(e(e(e(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w),v6),e(v7,v6)),v7),v8),e(v9,v8)),v9)). % P(e(e(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6)),v7),e(v8,v7)),v8)). % P(e(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),e(v7,v6)),v7),v8),e(v9,v8)),v9)). % P(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(v6,w)),v6),e(e(e(e(v7,e(e(e(v7,v8),e(v9,v8)),v9)),v10),v11),e(v10,v11)))). % P(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6)),e(e(e(e(v7,e(e(e(v7,v8),e(v9,v8)),v9)),v10),v11),e(v10,v11)))). % P(e(e(e(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x),v),e(w,v)),w),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)),v10),e(v11,v10)),v11)). % P(e(e(e(e(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)),v10),v11),e(v10,v11))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(e(w,v6),w),v6),v7)),v8),e(v7,v8))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),e(v8,v7)),v8)). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),w),e(v,w)),e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v10),e(v9,v10)))). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),e(v6,w)),v6)). % P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),w),v6),e(w,v6))). % P(e(e(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x),v),e(w,v)),w),e(e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v9),v10),v11)),e(v10,v11))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v9)),e(v8,v9))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(e(e(w,v6),e(v7,v6)),v7))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),e(e(e(v7,v8),e(v9,v8)),v9))). % P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(w,v)),w)). % P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))). % P(e(e(e(e(e(e(x,y),x),y),z),e(u,z)),u)). % P(e(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),w),e(v,w))),x),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6),v7),e(v8,v7)),v8)),v9),e(v10,v9)),v10)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6)),v7),e(v8,v7)),v8)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6)),v7),v8),e(v7,v8))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(u,v),e(w,v)),w))),v6),e(v7,v6)),v7)). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(e(e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),e(v9,v8)),v9),v10),v11),e(v10,v11)))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),e(e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)))). % P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),v),e(e(e(v,w),e(v6,w)),v6))). % P(e(e(e(e(e(x,e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),v)),x),w),e(v6,w)),v6)). % P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v8)),v))),x),v9),e(v10,v9)),v10)). % P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w)),e(v6,e(e(e(v6,v7),e(v8,v7)),v8)))). % P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)). % P(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x),v),e(w,v)),w)). % P(e(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),e(v9,v8)),v9)). % P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v9),v10)),v11),e(v10,v11))). % P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),e(v7,v6)),v7)). % P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w)),v6),v7),e(v6,v7))). % P(e(e(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),w),e(v,w))),x),e(e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v9),v10),e(v11,v10))),v11)). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9))),v10),e(v9,v10))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(u,e(e(e(u,v),e(w,v)),w)),e(e(v6,e(e(v7,e(e(e(v7,v8),e(v9,v8)),v9)),v6)),v10))),v11),e(v10,v11))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(e(e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),v8),v9),e(v8,v9)))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(e(e(e(e(v,e(e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v9),e(v8,v9))),v),v10),v11),e(v10,v11)))). % P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u),e(v,e(e(e(v,w),e(v6,w)),v6)))). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v8)),v))),x),e(e(e(v9,v10),e(v11,v10)),v11)),v9)). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v)),x))),v8),e(v9,v8)),v9)). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),e(w,v)),w)). % P(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),v),w),e(v,w))). % P(e(e(e(e(x,y),e(z,y)),z),x)). % P(e(e(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7)),v8),v8)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v6),v7),e(v8,v7))),v8)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(e(e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),v8),v9),e(v8,v9)))),u)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(u,e(v,e(e(e(v,w),e(v6,w)),v6)))),u)). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),v8),e(v9,v8)),v9),u))). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(e(v,e(e(e(v,w),e(v6,w)),v6)),v7),v7),u))). % P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(e(e(u,v),e(w,v)),w))). % P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))). % P(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),w),e(v,w))),x)). % P(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6)),v7))). % P(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),v7),e(v6,v7)))). % P(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),v8),v8)),v))),x)). % P(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x)). % P(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),x)). % P(e(e(x,e(y,x)),y)). % P(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),v6),e(v7,v6)),v7),x))). % P(e(x,e(e(e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x),v6),e(v7,v6)),v7))). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),x)),v7),e(v8,v7)),v8))). % P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),x))). % P(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x))). % P(e(x,e(y,e(x,y)))). % % Following 30 sorted from temp.xcb.exp2.ot3a purport to prove the remaining of the 15 7-symbol, including symmetry, excluding f7k. % P(e(e(e(e(e(e(x,y),x),y),z),u),e(z,u))). % P(e(e(e(e(e(x,e(y,x)),z),e(u,z)),u),y)). % P(e(e(e(e(e(x,e(y,y)),x),z),e(u,z)),u)). % P(e(e(e(e(e(x,e(y,y)),x),z),u),e(z,u))). % P(e(e(e(e(e(x,x),e(y,y)),z),e(u,z)),u)). % P(e(e(e(e(e(x,x),e(y,y)),z),u),e(z,u))). % P(e(e(e(e(x,e(y,e(x,y))),z),e(u,z)),u)). % P(e(e(e(e(x,e(y,e(x,y))),z),u),e(z,u))). % P(e(e(e(e(x,x),y),e(z,y)),z)). % P(e(e(e(e(x,y),e(z,y)),z),e(e(u,x),u))). % P(e(e(e(e(x,y),x),z),e(y,z))). % P(e(e(e(e(x,y),y),z),e(x,z))). % P(e(e(e(e(x,y),z),e(y,z)),x)). % P(e(e(e(x,e(y,x)),z),e(y,z))). % P(e(e(e(x,x),y),y)). % P(e(e(e(x,y),e(e(e(y,z),e(u,z)),u)),x)). % P(e(e(e(x,y),x),e(z,e(z,y)))). % P(e(e(e(x,y),y),x)). % P(e(e(x,e(x,y)),y)). % P(e(e(x,e(y,y)),x)). % P(e(e(x,x),e(e(e(y,z),y),z))). % P(e(e(x,x),e(y,y))). % P(e(e(x,y),e(e(e(z,x),z),y))). % P(e(e(x,y),e(y,x))). % P(e(x,e(e(e(y,z),y),e(x,z)))). % P(e(x,e(e(x,y),y))). % P(e(x,e(e(y,x),y))). % P(e(x,e(e(y,y),x))). % P(e(x,e(x,e(y,y)))). % P(e(x,e(y,e(y,x)))). end_of_list. list(passive). % % Following are negations of the 15 length 7 theorems. % -P(e(e(e(a,b),a),b)) | $ANS(f7a). % -P(e(e(a,e(b,a)),b)) | $ANS(f7b). % -P(e(e(a,b),e(a,b))) | $ANS(f7c). % -P(e(a,e(e(b,a),b))) | $ANS(f7d). % -P(e(a,e(b,e(a,b)))) | $ANS(f7e). % -P(e(e(e(a,b),b),a)) | $ANS(f7f). % -P(e(e(a,e(b,b)),a)) | $ANS(f7g). % -P(e(e(a,b),e(b,a))) | $ANS(f7h). % -P(e(a,e(e(b,b),a))) | $ANS(f7i). % -P(e(a,e(b,e(b,a)))) | $ANS(f7j). % -P(e(e(e(a,a),b),b)) | $ANS(k7f). % -P(e(e(a,e(a,b)),b)) | $ANS(f7l). % -P(e(e(a,a),e(b,b))) | $ANS(f7m). % -P(e(a,e(e(a,b),b))) | $ANS(f7n). % -P(e(a,e(a,e(b,b)))) | $ANS(f7o). % -P(e(a,a)) | $ANSWER(reflex). % Following are axioms for EC and other targets. % negations of known theorems and axioms -P(e(e(a,b),e(e(c,b),e(a,c)))) | $ANSWER(P1_YQL). -P(e(e(a,b),e(e(a,c),e(c,b)))) | $ANSWER(P2_YQF). -P(e(e(a,b),e(e(c,a),e(b,c)))) | $ANSWER(P3_YQJ). -P(e(e(e(a,b),c),e(b,e(c,a)))) | $ANSWER(P4_UM). -P(e(a,e(e(b,e(a,c)),e(c,b)))) | $ANSWER(P5_XGF). -P(e(e(a,e(b,c)),e(c,e(a,b)))) | $ANSWER(P7_WN). -P(e(e(a,b),e(c,e(e(b,c),a)))) | $ANSWER(P8_YRM). -P(e(e(a,b),e(c,e(e(c,b),a)))) | $ANSWER(P9_YRO). -P(e(e(e(a,e(b,c)),c),e(b,a))) | $ANSWER(PYO). -P(e(e(e(a,e(b,c)),b),e(c,a))) | $ANSWER(PYM). -P(e(a,e(e(b,e(c,a)),e(c,b)))) | $ANSWER(XGK). -P(e(a,e(e(b,c),e(e(a,c),b)))) | $ANSWER(XHK). -P(e(a,e(e(b,c),e(e(c,a),b)))) | $ANSWER(XHN). -P(e(a,a)) | $ANSWER(reflex). -P(e(e(a,b),e(b,a))) | $ANSWER(symm). -P(e(e(a,b),e(e(b,c),e(a,c)))) | $ANSWER(trans). -P(e(e(e(c1,c2),c3),e(c1,e(c2,c3)))) | $ANSWER(Wajsberg_1). -P(e(e(e(c1,c1),c1),c1)) | $ANSWER(Wajsberg_2). -P(e(e(c1,e(c2,c3)),e(c3,e(c2,c1)))) | $ANSWER(Wajsberg_3). -P(e(e(e(c1,e(c2,c3)),e(e(c3,c4),c4)),e(c1,c2))) | $ANSWER(Wajsberg_4_sing). -P(e(e(e(e(c1,c2),c3),c4),e(c4,e(c1,e(c2,c3))))) | $ANSWER(Wajsberg_5_sing). -P(e(e(c1,e(c2,c3)),e(e(c2,e(c4,c3)),e(c4,c1)))) | $ANSWER(Bryman_sing). -P(e(e(c1,e(c2,c3)),e(e(c2,e(c3,c4)),e(c4,c1)))) | $ANSWER(Luka_1_sing). -P(e(e(c4,e(c1,e(c2,c3))),e(e(c1,c2),e(c3,c4)))) | $ANSWER(Luka_2_sing). -P(e(e(c1,e(c2,c3)),e(e(c1,e(c3,c4)),e(c4,c2)))) | $ANSWER(Sobo_1_sing). -P(e(e(c1,e(c2,c3)),e(e(c1,e(c4,c3)),e(c4,c2)))) | $ANSWER(Sobo_2_sing). % Following are negations of the 19-step proof that XHN implies UM. -P(e(e(a,b),e(e(b,e(c,e(e(d,a0),e(e(a0,c),d)))),a))) | $ANS(step_xhn). -P(e(e(e(e(a,e(b,e(e(c,d),e(e(d,b),c)))),a0),e(a1,e(e(a2,a3),e(e(a3,a1),a2)))),e(a0,a))) | $ANS(step_xhn). -P(e(e(e(e(a,b),e(e(b,c),a)),e(d,e(e(a0,a1),e(e(a1,d),a0)))),c)) | $ANS(step_xhn). -P(e(e(a,e(e(b,c),e(e(c,a),b))),e(e(e(d,a0),e(e(a0,e(a1,e(a2,e(e(a3,a4),e(e(a4,a2),a3))))),d)),a1))) | $ANS(step_xhn). -P(e(e(a,e(b,e(e(c,d),e(e(d,b),c)))),e(e(e(a0,a1),e(e(a1,a),a0)),e(a2,e(e(a3,a4),e(e(a4,a2),a3)))))) | $ANS(step_xhn). -P(e(e(e(a,b),e(e(b,e(c,e(d,e(e(a0,a1),e(e(a1,d),a0))))),a)),c)) | $ANS(step_xhn). -P(e(e(a,b),e(e(b,e(e(e(c,d),e(e(d,e(a0,e(a1,e(e(a2,a3),e(e(a3,a1),a2))))),c)),a0)),a))) | $ANS(step_xhn). -P(e(e(e(e(a,b),e(e(b,c),a)),e(e(e(d,a0),e(e(a0,e(a1,e(a2,e(e(a3,a4),e(e(a4,a2),a3))))),d)),a1)),c)) | $ANS(step_xhn). -P(e(e(a,e(e(a,b),e(c,e(e(d,a0),e(e(a0,c),d))))),e(b,e(a1,e(e(a2,a3),e(e(a3,a1),a2)))))) | $ANS(step_xhn). -P(e(e(e(e(a,e(e(b,c),e(e(c,a),b))),d),d),e(a0,e(e(a1,a2),e(e(a2,a0),a1))))) | $ANS(step_xhn). -P(e(e(e(a,b),e(e(b,e(e(e(c,e(e(d,a0),e(e(a0,c),d))),a1),a1)),a)),e(a2,e(e(a3,a4),e(e(a4,a2),a3))))) | $ANS(step_xhn). -P(e(e(e(a,e(e(b,c),e(e(c,a),b))),d),d)) | $ANS(step_xhn). -P(e(e(e(e(a,e(e(b,c),e(e(c,a),b))),e(e(e(d,e(e(a0,a1),e(e(a1,d),a0))),a2),a2)),a3),a3)) | $ANS(step_xhn). -P(e(e(e(e(a,b),c),e(b,e(d,e(e(a0,a1),e(e(a1,d),a0))))),e(c,a))) | $ANS(step_xhn). -P(e(e(a,b),e(e(b,e(e(c,e(e(d,a0),e(e(a0,c),d))),e(e(e(a1,e(e(a2,a3),e(e(a3,a1),a2))),a4),a4))),a))) | $ANS(step_xhn). -P(e(e(a,e(e(b,c),e(e(c,e(d,a)),b))),d)) | $ANS(step_xhn). -P(e(e(e(e(e(a,e(e(b,c),e(e(c,a),b))),d),d),a0),e(e(a1,a2),e(e(a2,a0),a1)))) | $ANS(step_xhn). -P(e(a,e(e(b,e(e(c,d),e(e(d,b),c))),e(e(e(a0,a1),e(e(a1,e(a2,a)),a0)),a2)))) | $ANS(step_xhn). -P(e(e(e(a,b),c),e(b,e(c,a)))) | $ANS(step_xhn). end_of_list. list(demodulators). % (P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),e(e(e(w,v6),e(v7,v6)),v7)),w)) = junk). % (e(e(x,x),y) = junk). % (e(y,e(x,x)) = junk). (e(x,junk) = junk). (e(junk,x) = junk). (P(junk) = $T). end_of_list. make_evaluable(_+_, $SUM(_,_)). clear(demod_history). assign(demod_limit, -1). list(demodulators). count(e(x,y)) = count(x) + count(y) + 1. $VAR(x) -> count(x) = 1. end_of_list.