The dog likes the mouse. The mouse visits the dog. If someone visits the dog and the dog visits the mouse then they are red. If someone needs the mouse and they like the dog then they visit the mouse. If someone likes the mouse and the mouse likes the dog then they visit the dog. If someone is young then they need the mouse. If someone is young and they visit the dog then they need the mouse. If someone visits the dog then they like the dog.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If someone visits the dog and the dog visits the mouse then they are red.
((("someone" "visits" "dog" "+") ("dog" "visits" "mouse" "+")) -> ("someone" "is" "red" "+"))
If someone needs the mouse and they like the dog then they visit the mouse.
((("someone" "needs" "mouse" "+") ("someone" "likes" "dog" "+")) -> ("someone" "visits" "mouse" "+"))
If someone likes the mouse and the mouse likes the dog then they visit the dog.
((("someone" "likes" "mouse" "+") ("mouse" "likes" "dog" "+")) -> ("someone" "visits" "dog" "+"))
If someone is young then they need the mouse.
((("someone" "is" "young" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is young and they visit the dog then they need the mouse.
((("someone" "is" "young" "+") ("someone" "visits" "dog" "+")) -> ("someone" "needs" "mouse" "+"))
If someone visits the dog then they like the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "likes" "dog" "+"))
The mouse visits the dog.
True
1
proof
[(triple2)]
("mouse" "visits" "dog" "+")
triple2
The dog does not like the mouse.
False
1
inv-proof
[(triple1)]
("dog" "likes" "mouse" "-")
triple1
The mouse likes the dog.
True
2
proof
[(((triple2) -> rule6))]
("mouse" "likes" "dog" "+")
((triple2) -> (rule6 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse does not like the dog.
False
2
inv-proof
[(((triple2) -> rule6))]
("mouse" "likes" "dog" "-")
((triple2) -> (rule6 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog visits the dog.
True
4
proof
[(((triple1 ((triple2) -> rule6)) -> rule3))]
("dog" "visits" "dog" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog does not visit the dog.
False
4
inv-proof
[(((triple1 ((triple2) -> rule6)) -> rule3))]
("dog" "visits" "dog" "-")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog likes the dog.
True
5
proof
[(((((triple1 ((triple2) -> rule6)) -> rule3)) -> rule6))]
("dog" "likes" "dog" "+")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog does not like the dog.
False
5
inv-proof
[(((((triple1 ((triple2) -> rule6)) -> rule3)) -> rule6))]
("dog" "likes" "dog" "-")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog does not visit the mouse.
Unknown
inv-rconc
[@2: The dog visits the mouse.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("dog" "visits" "mouse" "-")
The dog is red.
Unknown
rconc
[@3: The dog is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- FAIL)]]
("dog" "is" "red" "+")
The mouse is not red.
Unknown
inv-rconc
[@3: The mouse is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- FAIL)]]
("mouse" "is" "red" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
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 mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The dog likes the mouse.[(triple1)] The mouse visits the dog.[(triple2)] @1: The mouse likes the dog.[(((triple2) -> rule6))] @2: The dog visits the dog.[(((triple1 ((triple2) -> rule6)) -> rule3))] @3: The dog likes the dog.[(((((triple1 ((triple2) -> rule6)) -> rule3)) -> rule6))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
((triple2) -> (rule6 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3