The cat is cold. The cow needs the lion. The lion likes the cat. The mouse visits the cat. If someone visits the mouse then they need the lion. If someone is cold then they visit the mouse.
The cat is cold.
("cat" "is" "cold" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If someone visits the mouse then they need the lion.
((("someone" "visits" "mouse" "+")) -> ("someone" "needs" "lion" "+"))
If someone is cold then they visit the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "mouse" "+"))
The lion likes the cat.
True
1
proof
[(triple3)]
("lion" "likes" "cat" "+")
triple3
The lion does not like the cat.
False
1
inv-proof
[(triple3)]
("lion" "likes" "cat" "-")
triple3
The cat visits the mouse.
True
2
proof
[(((triple1) -> rule2))]
("cat" "visits" "mouse" "+")
((triple1) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat does not visit the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "visits" "mouse" "-")
((triple1) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The lion does not visit the mouse.
Unknown
inv-rconc
[@1: The lion visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "mouse" "-")
The lion needs the lion.
Unknown
rconc
[@2: The lion needs the lion.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The lion visits the cat.
Unknown
random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "+")
@0: The cat is cold.[(triple1)] The cow needs the lion.[(triple2)] The lion likes the cat.[(triple3)] The mouse visits the cat.[(triple4)] @1: The cat visits the mouse.[(((triple1) -> rule2))] @2: The cat needs the lion.[(((((triple1) -> rule2)) -> rule1))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The lion likes the cat.
("lion" "likes" "cat" "+")
triple3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple1) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2