The cat sees the cow. The cat visits the lion. The cow is nice. The cow likes the cat. The cow sees the cat. The cow visits the lion. The lion is big. If something visits the cow then it likes the cat. If something visits the cow and the cow is big then it likes the cow. If something sees the cat and it is big then the cat likes the cow. If the cow visits the cat then the cow visits the lion. If the cow is round and the cow visits the cat then the cow sees the lion. If the cow likes the cat then the cow likes the lion.
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
If something visits the cow then it likes the cat.
((("something" "visits" "cow" "+")) -> ("something" "likes" "cat" "+"))
If something visits the cow and the cow is big then it likes the cow.
((("something" "visits" "cow" "+") ("cow" "is" "big" "+")) -> ("something" "likes" "cow" "+"))
If something sees the cat and it is big then the cat likes the cow.
((("something" "sees" "cat" "+") ("something" "is" "big" "+")) -> ("cat" "likes" "cow" "+"))
If the cow visits the cat then the cow visits the lion.
((("cow" "visits" "cat" "+")) -> ("cow" "visits" "lion" "+"))
If the cow is round and the cow visits the cat then the cow sees the lion.
((("cow" "is" "round" "+") ("cow" "visits" "cat" "+")) -> ("cow" "sees" "lion" "+"))
If the cow likes the cat then the cow likes the lion.
((("cow" "likes" "cat" "+")) -> ("cow" "likes" "lion" "+"))
The cat visits the lion.
True
1
proof
[(triple2)]
("cat" "visits" "lion" "+")
triple2
The cow does not see the cat.
False
1
inv-proof
[(triple5)]
("cow" "sees" "cat" "-")
triple5
The cow likes the lion.
True
2
proof
[(((triple4) -> rule6))]
("cow" "likes" "lion" "+")
((triple4) -> (rule6 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow does not like the lion.
False
2
inv-proof
[(((triple4) -> rule6))]
("cow" "likes" "lion" "-")
((triple4) -> (rule6 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "cow" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "cow" "+")
The cow does not visit the cat.
Unknown
inv-random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The cat sees the cow.[(triple1)] The cat visits the lion.[(triple2)] The cow is nice.[(triple3)] The cow likes the cat.[(triple4)] The cow sees the cat.[(triple5)] The cow visits the lion.[(triple6)] The lion is big.[(triple7)] @1: The cow likes the lion.[(((triple4) -> rule6))]
The cat sees the cow.
("cat" "sees" "cow" "+")
triple1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow likes the cat.
("cow" "likes" "cat" "+")
triple4
The cow sees the cat.
("cow" "sees" "cat" "+")
triple5
The cow visits the lion.
("cow" "visits" "lion" "+")
triple6
The lion is big.
("lion" "is" "big" "+")
triple7
The cow likes the lion.
("cow" "likes" "lion" "+")
((triple4) -> (rule6 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1