The cat likes the mouse. The dog is not rough. The dog likes the mouse. The lion likes the dog. The lion sees the dog. The lion sees the mouse. The mouse likes the dog. If something likes the mouse and it is green then the mouse is not kind. If the lion likes the mouse then the lion does not eat the dog. If something eats the mouse and the mouse is rough then it does not like the cat. If the mouse is green and the mouse sees the dog then the mouse sees the cat. If something sees the dog and it likes the dog then it sees the cat. If something sees the cat then the cat is not nice.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The dog is not rough.
("dog" "is" "rough" "-")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
If something likes the mouse and it is green then the mouse is not kind.
((("something" "likes" "mouse" "+") ("something" "is" "green" "+")) -> ("mouse" "is" "kind" "-"))
If the lion likes the mouse then the lion does not eat the dog.
((("lion" "likes" "mouse" "+")) -> ("lion" "eats" "dog" "-"))
If something eats the mouse and the mouse is rough then it does not like the cat.
((("something" "eats" "mouse" "+") ("mouse" "is" "rough" "+")) -> ("something" "likes" "cat" "-"))
If the mouse is green and the mouse sees the dog then the mouse sees the cat.
((("mouse" "is" "green" "+") ("mouse" "sees" "dog" "+")) -> ("mouse" "sees" "cat" "+"))
If something sees the dog and it likes the dog then it sees the cat.
((("something" "sees" "dog" "+") ("something" "likes" "dog" "+")) -> ("something" "sees" "cat" "+"))
If something sees the cat then the cat is not nice.
((("something" "sees" "cat" "+")) -> ("cat" "is" "nice" "-"))
The cat likes the mouse.
True
1
proof
[(triple1)]
("cat" "likes" "mouse" "+")
triple1
The dog does not like the mouse.
False
1
inv-proof
[(triple3)]
("dog" "likes" "mouse" "-")
triple3
The lion sees the cat.
True
3
proof
[(((triple5 triple4) -> rule5))]
("lion" "sees" "cat" "+")
((triple5 triple4) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion does not see the cat.
False
3
inv-proof
[(((triple5 triple4) -> rule5))]
("lion" "sees" "cat" "-")
((triple5 triple4) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The cat is not nice.
True
4
proof
[(((((triple5 triple4) -> rule5)) -> rule6))]
("cat" "is" "nice" "-")
((((triple5 triple4) -> (rule5 % int2))) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat is nice.
False
4
inv-proof
[(((((triple5 triple4) -> rule5)) -> rule6))]
("cat" "is" "nice" "+")
((((triple5 triple4) -> (rule5 % int2))) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "cat" "-")
The dog sees the cat.
Unknown
rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "cat" "+")
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "cat" "-")
The cat sees the mouse.
Unknown
random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The mouse sees the lion.
Unknown
random
[@0: The mouse sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "lion" "+")
@0: The cat likes the mouse.[(triple1)] The dog is not rough.[(triple2)] The dog likes the mouse.[(triple3)] The lion likes the dog.[(triple4)] The lion sees the dog.[(triple5)] The lion sees the mouse.[(triple6)] The mouse likes the dog.[(triple7)] @1: The lion sees the cat.[(((triple5 triple4) -> rule5))] @2: The cat is not nice.[(((((triple5 triple4) -> rule5)) -> rule6))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The dog is not rough.
("dog" "is" "rough" "-")
triple2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple3
The lion likes the dog.
("lion" "likes" "dog" "+")
triple4
The lion sees the dog.
("lion" "sees" "dog" "+")
triple5
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple6
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple7
The lion sees the cat.
("lion" "sees" "cat" "+")
((triple5 triple4) -> (rule5 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The cat is not nice.
("cat" "is" "nice" "-")
((((triple5 triple4) -> (rule5 % int2))) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2