The mouse likes the rabbit. The mouse visits the rabbit. The rabbit chases the mouse. If something visits the mouse then it does not visit the rabbit. If something chases the mouse and the mouse visits the rabbit then the mouse is green. If something chases the rabbit then it chases the mouse. If something is green then it chases the rabbit. If something is kind then it likes the rabbit. If something chases the rabbit and it likes the rabbit then the rabbit likes the mouse. If something visits the rabbit and the rabbit visits the mouse then the rabbit likes the mouse. If something is red and it does not chase the mouse then the mouse does not like the rabbit.
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
If something visits the mouse then it does not visit the rabbit.
((("something" "visits" "mouse" "+")) -> ("something" "visits" "rabbit" "-"))
If something chases the mouse and the mouse visits the rabbit then the mouse is green.
((("something" "chases" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("mouse" "is" "green" "+"))
If something chases the rabbit then it chases the mouse.
((("something" "chases" "rabbit" "+")) -> ("something" "chases" "mouse" "+"))
If something is green then it chases the rabbit.
((("something" "is" "green" "+")) -> ("something" "chases" "rabbit" "+"))
If something is kind then it likes the rabbit.
((("something" "is" "kind" "+")) -> ("something" "likes" "rabbit" "+"))
If something chases the rabbit and it likes the rabbit then the rabbit likes the mouse.
((("something" "chases" "rabbit" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something visits the rabbit and the rabbit visits the mouse then the rabbit likes the mouse.
((("something" "visits" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something is red and it does not chase the mouse then the mouse does not like the rabbit.
((("something" "is" "red" "+") ("something" "chases" "mouse" "~")) -> ("mouse" "likes" "rabbit" "-"))
The mouse likes the rabbit.
True
1
proof
[(triple1)]
("mouse" "likes" "rabbit" "+")
triple1
The mouse does not like the rabbit.
False
1
inv-proof
[(triple1)]
("mouse" "likes" "rabbit" "-")
triple1
The mouse is green.
True
3
proof
[(((triple3 triple2) -> rule2))]
("mouse" "is" "green" "+")
((triple3 triple2) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not green.
False
3
inv-proof
[(((triple3 triple2) -> rule2))]
("mouse" "is" "green" "-")
((triple3 triple2) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse chases the rabbit.
True
4
proof
[(((((triple3 triple2) -> rule2)) -> rule4))]
("mouse" "chases" "rabbit" "+")
((((triple3 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse does not chase the rabbit.
False
4
inv-proof
[(((((triple3 triple2) -> rule2)) -> rule4))]
("mouse" "chases" "rabbit" "-")
((((triple3 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse chases the mouse.
True
5
proof
[(((((((triple3 triple2) -> rule2)) -> rule4)) -> rule3))]
("mouse" "chases" "mouse" "+")
((((((triple3 triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse does not chase the mouse.
False
5
inv-proof
[(((((((triple3 triple2) -> rule2)) -> rule4)) -> rule3))]
("mouse" "chases" "mouse" "-")
((((((triple3 triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The rabbit visits the mouse.
Unknown
random
[@0: The rabbit visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "mouse" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The mouse likes the rabbit.[(triple1)] The mouse visits the rabbit.[(triple2)] The rabbit chases the mouse.[(triple3)] @1: The mouse is green.[(((triple3 triple2) -> rule2))] @2: The mouse chases the rabbit.[(((((triple3 triple2) -> rule2)) -> rule4))] @3: The mouse chases the mouse.[(((((((triple3 triple2) -> rule2)) -> rule4)) -> rule3))] The rabbit likes the mouse.[(((((((triple3 triple2) -> rule2)) -> rule4) triple1) -> rule6))]
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple3
The mouse is green.
("mouse" "is" "green" "+")
((triple3 triple2) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((((triple3 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple3 triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((((triple3 triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3