21 forall([P, Q, R], |
21 forall([P, Q, R], |
22 or( equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q)))), |
22 or( equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q)))), |
23 a5 ). |
23 a5 ). |
24 |
24 |
25 clause( |
25 clause( |
26 or( not(equal(c_COMBI,c_COMBK))), |
|
27 a6 ). |
|
28 |
|
29 clause( |
|
30 or( not(equal(c_COMBI,c_COMBB))), |
|
31 a8 ). |
|
32 |
|
33 clause( |
|
34 or( not(equal(c_COMBI,c_COMBC))), |
|
35 a9 ). |
|
36 |
|
37 clause( |
|
38 or( not(equal(c_COMBK,c_COMBB))), |
|
39 a11 ). |
|
40 |
|
41 clause( |
|
42 or( not(equal(c_COMBK,c_COMBC))), |
|
43 a12 ). |
|
44 |
|
45 clause( |
|
46 or( not(equal(c_COMBB,c_COMBC))), |
|
47 a15 ). |
|
48 |
|
49 clause( |
|
50 forall([X, Y], |
26 forall([X, Y], |
51 or( not(hBOOL(hAPP(hAPP(fequal,X),Y))), |
27 or( not(hBOOL(hAPP(hAPP(fequal,X),Y))), |
52 equal(X,Y))), |
28 equal(X,Y))), |
53 a16 ). |
29 a6 ). |
54 |
30 |
55 clause( |
31 clause( |
56 forall([X, Y], |
32 forall([X, Y], |
57 or( not(equal(X,Y)), |
33 or( not(equal(X,Y)), |
58 hBOOL(hAPP(hAPP(fequal,X),Y)))), |
34 hBOOL(hAPP(hAPP(fequal,X),Y)))), |
59 a17 ). |
35 a7 ). |
60 |
36 |