The cat chases the cow. The cat chases the lion. The cat is blue. The cat sees the lion. The cat visits the cow. The cat visits the lion. The cow chases the lion. The cow sees the lion. The cow visits the cat. The cow visits the lion. The lion is blue. The lion sees the cat. The rabbit chases the cow. The rabbit is cold. The rabbit sees the cow. If someone visits the cat then the cat chases the lion. If someone chases the cat and they chase the rabbit then the cat chases the lion. If the lion chases the cat then the lion is blue. If someone sees the lion and the lion is nice then they chase the cat. If someone visits the cow then the cow sees the rabbit. If someone visits the cat then the cat chases the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If someone visits the cat then the cat chases the lion.
((("someone" "visits" "cat" "+")) -> ("cat" "chases" "lion" "+"))
If someone chases the cat and they chase the rabbit then the cat chases the lion.
((("someone" "chases" "cat" "+") ("someone" "chases" "rabbit" "+")) -> ("cat" "chases" "lion" "+"))
If the lion chases the cat then the lion is blue.
((("lion" "chases" "cat" "+")) -> ("lion" "is" "blue" "+"))
If someone sees the lion and the lion is nice then they chase the cat.
((("someone" "sees" "lion" "+") ("lion" "is" "nice" "+")) -> ("someone" "chases" "cat" "+"))
If someone visits the cow then the cow sees the rabbit.
((("someone" "visits" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
If someone visits the cat then the cat chases the cow.
((("someone" "visits" "cat" "+")) -> ("cat" "chases" "cow" "+"))
The cow chases the lion.
True
1
proof
[(triple7)]
("cow" "chases" "lion" "+")
triple7
The cow does not visit the lion.
False
1
inv-proof
[(triple10)]
("cow" "visits" "lion" "-")
triple10
The cow sees the rabbit.
True
2
proof
[(((triple5) -> rule5))]
("cow" "sees" "rabbit" "+")
((triple5) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow does not see the rabbit.
False
2
inv-proof
[(((triple5) -> rule5))]
("cow" "sees" "rabbit" "-")
((triple5) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit does not chase the cat.
Unknown
inv-rconc
[@1: The rabbit chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "cat" "-")
The cow chases the cat.
Unknown
rconc
[@1: The cow chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cat" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat chases the cow.[(triple1 OR ((triple9) -> rule6))] The cat chases the lion.[(triple2 OR ((triple9) -> rule1))] The cat is blue.[(triple3)] The cat sees the lion.[(triple4)] The cat visits the cow.[(triple5)] The cat visits the lion.[(triple6)] The cow chases the lion.[(triple7)] The cow sees the lion.[(triple8)] The cow visits the cat.[(triple9)] The cow visits the lion.[(triple10)] The lion is blue.[(triple11)] The lion sees the cat.[(triple12)] The rabbit chases the cow.[(triple13)] The rabbit is cold.[(triple14)] The rabbit sees the cow.[(triple15)] @1: The cow sees the rabbit.[(((triple5) -> rule5))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
((triple9) -> (rule6 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
triple2
((triple9) -> (rule1 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat sees the lion.
("cat" "sees" "lion" "+")
triple4
The cat visits the cow.
("cat" "visits" "cow" "+")
triple5
The cat visits the lion.
("cat" "visits" "lion" "+")
triple6
The cow chases the lion.
("cow" "chases" "lion" "+")
triple7
The cow sees the lion.
("cow" "sees" "lion" "+")
triple8
The cow visits the cat.
("cow" "visits" "cat" "+")
triple9
The cow visits the lion.
("cow" "visits" "lion" "+")
triple10
The lion is blue.
("lion" "is" "blue" "+")
triple11
The lion sees the cat.
("lion" "sees" "cat" "+")
triple12
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple13
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple14
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple15
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple5) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1