The cat is kind. The cat is nice. The cat is red. The cat is rough. The cat is young. The cat likes the cow. The cat sees the cow. The cat visits the cow. The cow is kind. The cow does not like the cat. The cow sees the cat. The cow visits the cat. If someone visits the cow and the cow sees the cat then they see the cow. If someone is rough then they see the cat.
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow does not like the cat.
("cow" "likes" "cat" "-")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If someone visits the cow and the cow sees the cat then they see the cow.
((("someone" "visits" "cow" "+") ("cow" "sees" "cat" "+")) -> ("someone" "sees" "cow" "+"))
If someone is rough then they see the cat.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "cat" "+"))
The cat likes the cow.
True
1
proof
[(triple6)]
("cat" "likes" "cow" "+")
triple6
The cat is not red.
False
1
inv-proof
[(triple3)]
("cat" "is" "red" "-")
triple3
The cat sees the cat.
True
2
proof
[(((triple4) -> rule2))]
("cat" "sees" "cat" "+")
((triple4) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple4) -> rule2))]
("cat" "sees" "cat" "-")
((triple4) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is kind.[(triple1)] The cat is nice.[(triple2)] The cat is red.[(triple3)] The cat is rough.[(triple4)] The cat is young.[(triple5)] The cat likes the cow.[(triple6)] The cat sees the cow.[(triple7 OR ((triple8 triple11) -> rule1))] The cat visits the cow.[(triple8)] The cow does not like the cat.[(triple10)] The cow is kind.[(triple9)] The cow sees the cat.[(triple11)] The cow visits the cat.[(triple12)] @1: The cat sees the cat.[(((triple4) -> rule2))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the cow.
("cat" "likes" "cow" "+")
triple6
The cat sees the cow.
("cat" "sees" "cow" "+")
triple7
((triple8 triple11) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple8
The cow does not like the cat.
("cow" "likes" "cat" "-")
triple10
The cow is kind.
("cow" "is" "kind" "+")
triple9
The cow sees the cat.
("cow" "sees" "cat" "+")
triple11
The cow visits the cat.
("cow" "visits" "cat" "+")
triple12
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple4) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1