The dog chases the rabbit. The lion chases the rabbit. The mouse chases the rabbit. The rabbit needs the lion. If someone needs the mouse and they see the rabbit then the mouse sees the dog. If the mouse chases the rabbit then the rabbit chases the mouse. If someone chases the mouse then the mouse does not chase the dog.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If someone needs the mouse and they see the rabbit then the mouse sees the dog.
((("someone" "needs" "mouse" "+") ("someone" "sees" "rabbit" "+")) -> ("mouse" "sees" "dog" "+"))
If the mouse chases the rabbit then the rabbit chases the mouse.
((("mouse" "chases" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If someone chases the mouse then the mouse does not chase the dog.
((("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "dog" "-"))
The lion chases the rabbit.
True
1
proof
[(triple2)]
("lion" "chases" "rabbit" "+")
triple2
The rabbit does not need the lion.
False
1
inv-proof
[(triple4)]
("rabbit" "needs" "lion" "-")
triple4
The rabbit chases the mouse.
True
2
proof
[(((triple3) -> rule2))]
("rabbit" "chases" "mouse" "+")
((triple3) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not chase the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("rabbit" "chases" "mouse" "-")
((triple3) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The mouse does not chase the dog.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "chases" "dog" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse chases the dog.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "chases" "dog" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse does not see the dog.
Unknown
inv-rconc
[@1: The mouse sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "dog" "-")
The lion needs the rabbit.
Unknown
random
[@0: The lion needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "rabbit" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The dog chases the rabbit.[(triple1)] The lion chases the rabbit.[(triple2)] The mouse chases the rabbit.[(triple3)] The rabbit needs the lion.[(triple4)] @1: The rabbit chases the mouse.[(((triple3) -> rule2))] @2: The mouse does not chase the dog.[(((((triple3) -> rule2)) -> rule3))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple4
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple3) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2