The cat likes the cow. The cat likes the lion. The cat needs the cow. The cat needs the lion. The cat sees the cow. The cat sees the lion. The cow likes the lion. The lion is big. The lion is cold. The lion is rough. The lion likes the cat. The lion likes the cow. The lion needs the cow. The lion sees the cat. The lion sees the cow. If something likes the cow and it likes the cat then it sees the lion.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If something likes the cow and it likes the cat then it sees the lion.
((("something" "likes" "cow" "+") ("something" "likes" "cat" "+")) -> ("something" "sees" "lion" "+"))
The cow likes the lion.
True
1
proof
[(triple7)]
("cow" "likes" "lion" "+")
triple7
The lion is not cold.
False
1
inv-proof
[(triple9)]
("lion" "is" "cold" "-")
triple9
The lion sees the lion.
True
3
proof
[(((triple12 triple11) -> rule1))]
("lion" "sees" "lion" "+")
((triple12 triple11) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
3
inv-proof
[(((triple12 triple11) -> rule1))]
("lion" "sees" "lion" "-")
((triple12 triple11) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The cow does not see the lion.
Unknown
inv-rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "lion" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cat likes the cow.[(triple1)] The cat likes the lion.[(triple2)] The cat needs the cow.[(triple3)] The cat needs the lion.[(triple4)] The cat sees the cow.[(triple5)] The cat sees the lion.[(triple6)] The cow likes the lion.[(triple7)] The lion is big.[(triple8)] The lion is cold.[(triple9)] The lion is rough.[(triple10)] The lion likes the cat.[(triple11)] The lion likes the cow.[(triple12)] The lion needs the cow.[(triple13)] The lion sees the cat.[(triple14)] The lion sees the cow.[(triple15)] @1: The lion sees the lion.[(((triple12 triple11) -> rule1))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cat needs the lion.
("cat" "needs" "lion" "+")
triple4
The cat sees the cow.
("cat" "sees" "cow" "+")
triple5
The cat sees the lion.
("cat" "sees" "lion" "+")
triple6
The cow likes the lion.
("cow" "likes" "lion" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion is cold.
("lion" "is" "cold" "+")
triple9
The lion is rough.
("lion" "is" "rough" "+")
triple10
The lion likes the cat.
("lion" "likes" "cat" "+")
triple11
The lion likes the cow.
("lion" "likes" "cow" "+")
triple12
The lion needs the cow.
("lion" "needs" "cow" "+")
triple13
The lion sees the cat.
("lion" "sees" "cat" "+")
triple14
The lion sees the cow.
("lion" "sees" "cow" "+")
triple15
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple12 triple11) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1