Proof that if every member of x is closed under f then the intersection of x is closed under f

Proof that if every member of `x` is closed under `f` then the intersection of `x` is closed under `f`

Note how the clause with variable x is placed in the usable list and the clause with no variables in the set of support: The clause bads x != p1 | closedunder pair(x,badf) != p2 | $ans(x) is in the usable list, while the clause closedunder pair(kintersection bads bad,badf) != p1 is in the set of support. This allows the use of the standard technique of assigning a high wait to variables, purging all clauses with variables from the set of support, keeping the search focused on the "bad" constants whose existence is to be refuted.

----> UNIT CONFLICT at  23.89 sec ----> 7510 [binary,7509.1,19.1] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf))).

Length of proof is 8.  Level of proof is 5.

Proof



19 [reference] p2!=p1.
45 [reference] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1.
46 [reference] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1.
47 [reference] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1.
54 [reference] kintersection xf y x=p2|xf z !=p1|z x =p1.
55 [reference] kintersection xf y x=p1|xf notinint(xf,x) =p1.
56 [reference] kintersection xf y x=p1|notinint(xf,x) x !=p1.
63 [assumption to refute] bads x!=p1|closedunder pair(x,badf) !=p2|$ans(x).
64 [assumption to refute] closedunder pair(kintersection bads bad,badf)!=p1.
65 [hyper,64,46] kintersection bads bad notclosed(kintersection bads bad,badf)=p1.
78 [neg_hyper,64,47] kintersection bads bad (badf notclosed(kintersection bads bad,badf))!=p1.
148 [hyper,78,55] bads notinint(bads,badf notclosed(kintersection bads bad,badf))=p1.
159 [neg_hyper,78,56] notinint(bads,badf notclosed(kintersection bads bad,badf)) (badf notclosed(kintersection bads bad,badf))!=
p1.
160 [neg_hyper,78,55,63] closedunder pair(notinint(bads,badf notclosed(kintersection bads bad,badf)),badf)!=p2|$ans(notinint(bad
s,badf notclosed(kintersection bads bad,badf))).
695 [neg_hyper,159,45,160] notinint(bads,badf notclosed(kintersection bads bad,badf)) notclosed(kintersection bads bad,badf)!=p1
|$ans(notinint(bads,badf notclosed(kintersection bads bad,badf))).
7482 [ur,695,54,148] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf)))|kintersection bads x notclosed(kintersecti
on bads bad,badf) =p2.
7509 [para_into,7482.2.1,65.1.1,flip.2] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf)))|p2=p1.
7510 [binary,7509.1,19.1] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf))).