The cow is red. Red people are nice. If the cow is round then the cow is kind. If the cow is nice then the cow is kind. All young people are nice. Young people are red. If the cow is kind then the cow is nice. Young, red people are nice. Round, nice people are young.
The cow is red.
("cow" "is" "red" "+")
Red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If the cow is round then the cow is kind.
((("cow" "is" "round" "+")) -> ("cow" "is" "kind" "+"))
If the cow is nice then the cow is kind.
((("cow" "is" "nice" "+")) -> ("cow" "is" "kind" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If the cow is kind then the cow is nice.
((("cow" "is" "kind" "+")) -> ("cow" "is" "nice" "+"))
Young, red people are nice.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Round, nice people are young.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
The cow is red.
True
1
proof
[(triple1)]
("cow" "is" "red" "+")
triple1
The cow is not red.
False
1
inv-proof
[(triple1)]
("cow" "is" "red" "-")
triple1
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "young" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is red.[(triple1)] @1: The cow is nice.[(((triple1) -> rule1))] @2: The cow is kind.[(((((triple1) -> rule1)) -> rule3))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2