The cow is red. If the cow is big and the cow is not green then the cow is not nice. If the cow is red then the cow is nice. If the cow is green and the cow is not nice then the cow is young.
The cow is red.
("cow" "is" "red" "+")
If the cow is big and the cow is not green then the cow is not nice.
((("cow" "is" "big" "+") ("cow" "is" "green" "~")) -> ("cow" "is" "nice" "-"))
If the cow is red then the cow is nice.
((("cow" "is" "red" "+")) -> ("cow" "is" "nice" "+"))
If the cow is green and the cow is not nice then the cow is young.
((("cow" "is" "green" "+") ("cow" "is" "nice" "~")) -> ("cow" "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 nice.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "nice" "+")
((triple1) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "nice" "-")
((triple1) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "young" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow is red.[(triple1)] @1: The cow is nice.[(((triple1) -> rule2))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1