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