The dog chases the mouse. The dog likes the mouse. The dog sees the mouse. The dog sees the rabbit. The mouse chases the rabbit. The mouse is blue. The mouse is nice. The mouse likes the dog. The mouse likes the rabbit. The mouse sees the rabbit. The rabbit is round. The rabbit likes the dog. The rabbit likes the mouse. The rabbit sees the dog. The rabbit sees the mouse. If something is round then it sees the mouse. If something is blue then it chases the mouse. If something is blue then it likes the mouse.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something is round then it sees the mouse.
((("something" "is" "round" "+")) -> ("something" "sees" "mouse" "+"))
If something is blue then it chases the mouse.
((("something" "is" "blue" "+")) -> ("something" "chases" "mouse" "+"))
If something is blue then it likes the mouse.
((("something" "is" "blue" "+")) -> ("something" "likes" "mouse" "+"))
The dog chases the mouse.
True
1
proof
[(triple1)]
("dog" "chases" "mouse" "+")
triple1
The rabbit does not like the mouse.
False
1
inv-proof
[(triple13)]
("rabbit" "likes" "mouse" "-")
triple13
The mouse likes the mouse.
True
2
proof
[(((triple6) -> rule3))]
("mouse" "likes" "mouse" "+")
((triple6) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple6) -> rule3))]
("mouse" "likes" "mouse" "-")
((triple6) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The dog likes the rabbit.
Unknown
random
[@0: The dog likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "rabbit" "+")
@0: The dog chases the mouse.[(triple1)] The dog likes the mouse.[(triple2)] The dog sees the mouse.[(triple3)] The dog sees the rabbit.[(triple4)] The mouse chases the rabbit.[(triple5)] The mouse is blue.[(triple6)] The mouse is nice.[(triple7)] The mouse likes the dog.[(triple8)] The mouse likes the rabbit.[(triple9)] The mouse sees the rabbit.[(triple10)] The rabbit is round.[(triple11)] The rabbit likes the dog.[(triple12)] The rabbit likes the mouse.[(triple13)] The rabbit sees the dog.[(triple14)] The rabbit sees the mouse.[(triple15 OR ((triple11) -> rule1))] @1: The mouse chases the mouse.[(((triple6) -> rule2))] The mouse likes the mouse.[(((triple6) -> rule3))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple4
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is nice.
("mouse" "is" "nice" "+")
triple7
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple8
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple9
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple12
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple13
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple14
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
((triple11) -> (rule1 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple6) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple6) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1