The cat is green. The dog eats the mouse. The lion likes the cat. The mouse likes the cat. If something chases the cat and the cat does not chase the lion then it eats the cat. If something is green then it is big. If something is green and big then it likes the dog.
The cat is green.
("cat" "is" "green" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If something chases the cat and the cat does not chase the lion then it eats the cat.
((("something" "chases" "cat" "+") ("cat" "chases" "lion" "~")) -> ("something" "eats" "cat" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is green and big then it likes the dog.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
The mouse likes the cat.
True
1
proof
[(triple4)]
("mouse" "likes" "cat" "+")
triple4
The cat is not green.
False
1
inv-proof
[(triple1)]
("cat" "is" "green" "-")
triple1
The cat is big.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "big" "+")
((triple1) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "is" "big" "-")
((triple1) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat likes the dog.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("cat" "likes" "dog" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat does not like the dog.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("cat" "likes" "dog" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "big" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "dog" "+")
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "-")
The dog chases the lion.
Unknown
random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "+")
The mouse does not chase the dog.
Unknown
inv-random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "-")
The mouse chases the cat.
Unknown
random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "+")
@0: The cat is green.[(triple1)] The dog eats the mouse.[(triple2)] The lion likes the cat.[(triple3)] The mouse likes the cat.[(triple4)] @1: The cat is big.[(((triple1) -> rule2))] @2: The cat likes the dog.[(((triple1 ((triple1) -> rule2)) -> rule3))]
The cat is green.
("cat" "is" "green" "+")
triple1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple2
The lion likes the cat.
("lion" "likes" "cat" "+")
triple3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
((triple1) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2