The cat visits the cow. The cow is blue. The cow visits the cat. If someone visits the cow and the cow is blue then the cow is kind.
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If someone visits the cow and the cow is blue then the cow is kind.
((("someone" "visits" "cow" "+") ("cow" "is" "blue" "+")) -> ("cow" "is" "kind" "+"))
The cow is blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "+")
triple2
The cow is not blue.
False
1
inv-proof
[(triple2)]
("cow" "is" "blue" "-")
triple2
The cow is kind.
True
3
proof
[(((triple1 triple2) -> rule1))]
("cow" "is" "kind" "+")
((triple1 triple2) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("cow" "is" "kind" "-")
((triple1 triple2) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cat visits the cow.[(triple1)] The cow is blue.[(triple2)] The cow visits the cat.[(triple3)] @1: The cow is kind.[(((triple1 triple2) -> rule1))]
The cat visits the cow.
("cat" "visits" "cow" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow visits the cat.
("cow" "visits" "cat" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
((triple1 triple2) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1