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