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