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