The cat eats the rabbit. The cat eats the squirrel. The cat likes the rabbit. The cat likes the squirrel. The cat sees the rabbit. The dog is blue. The rabbit does not eat the cat. The rabbit is big. The rabbit is cold. The rabbit likes the dog. The rabbit likes the squirrel. The rabbit sees the dog. The squirrel does not eat the rabbit. The squirrel is young. The squirrel likes the rabbit. If the rabbit likes the squirrel and the rabbit is cold then the squirrel is not round. If the dog likes the squirrel then the squirrel is blue. If something likes the cat then it is young. If something eats the rabbit then it likes the cat. If something likes the dog then it sees the dog. If something is round then it eats the dog. If the rabbit sees the squirrel and the rabbit likes the dog then the squirrel eats the cat. If something eats the squirrel then it does not see the cat.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The dog is blue.
("dog" "is" "blue" "+")
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The squirrel does not eat the rabbit.
("squirrel" "eats" "rabbit" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
If the rabbit likes the squirrel and the rabbit is cold then the squirrel is not round.
((("rabbit" "likes" "squirrel" "+") ("rabbit" "is" "cold" "+")) -> ("squirrel" "is" "round" "-"))
If the dog likes the squirrel then the squirrel is blue.
((("dog" "likes" "squirrel" "+")) -> ("squirrel" "is" "blue" "+"))
If something likes the cat then it is young.
((("something" "likes" "cat" "+")) -> ("something" "is" "young" "+"))
If something eats the rabbit then it likes the cat.
((("something" "eats" "rabbit" "+")) -> ("something" "likes" "cat" "+"))
If something likes the dog then it sees the dog.
((("something" "likes" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something is round then it eats the dog.
((("something" "is" "round" "+")) -> ("something" "eats" "dog" "+"))
If the rabbit sees the squirrel and the rabbit likes the dog then the squirrel eats the cat.
((("rabbit" "sees" "squirrel" "+") ("rabbit" "likes" "dog" "+")) -> ("squirrel" "eats" "cat" "+"))
If something eats the squirrel then it does not see the cat.
((("something" "eats" "squirrel" "+")) -> ("something" "sees" "cat" "-"))
The rabbit does not eat the cat.
True
1
proof
[(triple7)]
("rabbit" "eats" "cat" "-")
triple7
The cat does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("cat" "eats" "squirrel" "-")
triple2
The cat does not see the cat.
True
2
proof
[(((triple2) -> rule8))]
("cat" "sees" "cat" "-")
((triple2) -> (rule8 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat sees the cat.
False
2
inv-proof
[(((triple2) -> rule8))]
("cat" "sees" "cat" "+")
((triple2) -> (rule8 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat is young.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("cat" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is not young.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("cat" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The rabbit does not eat the dog.
Unknown
inv-rconc
[@1: The rabbit eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "dog" "-")
The squirrel sees the dog.
Unknown
rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "dog" "+")
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "dog" "-")
The cat sees the squirrel.
Unknown
random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The cat eats the squirrel.[(triple2)] The cat likes the rabbit.[(triple3)] The cat likes the squirrel.[(triple4)] The cat sees the rabbit.[(triple5)] The dog is blue.[(triple6)] The rabbit does not eat the cat.[(triple7)] The rabbit is big.[(triple8)] The rabbit is cold.[(triple9)] The rabbit likes the dog.[(triple10)] The rabbit likes the squirrel.[(triple11)] The rabbit sees the dog.[(triple12 OR ((triple10) -> rule5))] The squirrel does not eat the rabbit.[(triple13)] The squirrel is young.[(triple14)] The squirrel likes the rabbit.[(triple15)] @1: The cat does not see the cat.[(((triple2) -> rule8))] The cat likes the cat.[(((triple1) -> rule4))] The squirrel is not round.[(((triple11 triple9) -> rule1))] @2: The cat is young.[(((((triple1) -> rule4)) -> rule3))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple10
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple11
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple12
((triple10) -> (rule5 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The squirrel does not eat the rabbit.
("squirrel" "eats" "rabbit" "-")
triple13
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple15
The cat does not see the cat.
("cat" "sees" "cat" "-")
((triple2) -> (rule8 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple1) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The squirrel is not round.
("squirrel" "is" "round" "-")
((triple11 triple9) -> (rule1 % int1))
The squirrel is not round.
("squirrel" "is" "round" "-")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2