The cat is not red. The lion chases the rabbit. The mouse is red. The rabbit is cold. If something is cold then it is not red. If the rabbit likes the cat then the rabbit is not cold. If something eats the rabbit and it chases the lion then the rabbit likes the mouse. If the lion likes the mouse then the mouse likes the rabbit. If something likes the mouse then it chases the mouse. If something is blue and it likes the lion then the lion is blue. If something chases the rabbit then it does not eat the rabbit. If the cat does not chase the mouse then the mouse chases the cat.
The cat is not red.
("cat" "is" "red" "-")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
If something is cold then it is not red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
If the rabbit likes the cat then the rabbit is not cold.
((("rabbit" "likes" "cat" "+")) -> ("rabbit" "is" "cold" "-"))
If something eats the rabbit and it chases the lion then the rabbit likes the mouse.
((("something" "eats" "rabbit" "+") ("something" "chases" "lion" "+")) -> ("rabbit" "likes" "mouse" "+"))
If the lion likes the mouse then the mouse likes the rabbit.
((("lion" "likes" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
If something likes the mouse then it chases the mouse.
((("something" "likes" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something is blue and it likes the lion then the lion is blue.
((("something" "is" "blue" "+") ("something" "likes" "lion" "+")) -> ("lion" "is" "blue" "+"))
If something chases the rabbit then it does not eat the rabbit.
((("something" "chases" "rabbit" "+")) -> ("something" "eats" "rabbit" "-"))
If the cat does not chase the mouse then the mouse chases the cat.
((("cat" "chases" "mouse" "~")) -> ("mouse" "chases" "cat" "+"))
The mouse is red.
True
1
proof
[(triple3)]
("mouse" "is" "red" "+")
triple3
The lion does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("lion" "chases" "rabbit" "-")
triple2
The rabbit is not red.
True
2
proof
[(((triple4) -> rule1))]
("rabbit" "is" "red" "-")
((triple4) -> (rule1 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1
The lion eats the rabbit.
False
2
inv-proof
[(((triple2) -> rule7))]
("lion" "eats" "rabbit" "+")
((triple2) -> (rule7 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@2: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The rabbit likes the mouse.
Unknown
rconc
[@1: The rabbit likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "mouse" "+")
The cat does not eat the lion.
Unknown
inv-random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The cat is not red.[(triple1)] The lion chases the rabbit.[(triple2)] The mouse is red.[(triple3)] The rabbit is cold.[(triple4)] @1: The lion does not eat the rabbit.[(((triple2) -> rule7))] The rabbit is not red.[(((triple4) -> rule1))]
The cat is not red.
("cat" "is" "red" "-")
triple1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
((triple2) -> (rule7 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The rabbit is not red.
("rabbit" "is" "red" "-")
((triple4) -> (rule1 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1