The bear eats the dog. The bear is red. The cat is blue. The cat is not round. The dog does not eat the cat. The dog needs the rabbit. The rabbit eats the bear. The rabbit eats the dog. The rabbit is not round. The rabbit does not need the dog. If someone sees the cat then they do not see the rabbit. If someone is red and not round then they are not kind. If someone eats the bear then they need the rabbit. If the dog eats the bear and the dog does not see the bear then the bear sees the rabbit. If someone sees the dog and the dog sees the bear then the dog does not eat the bear. If someone needs the rabbit then they see the cat.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is red.
("bear" "is" "red" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not round.
("cat" "is" "round" "-")
The dog does not eat the cat.
("dog" "eats" "cat" "-")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
If someone sees the cat then they do not see the rabbit.
((("someone" "sees" "cat" "+")) -> ("someone" "sees" "rabbit" "-"))
If someone is red and not round then they are not kind.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "kind" "-"))
If someone eats the bear then they need the rabbit.
((("someone" "eats" "bear" "+")) -> ("someone" "needs" "rabbit" "+"))
If the dog eats the bear and the dog does not see the bear then the bear sees the rabbit.
((("dog" "eats" "bear" "+") ("dog" "sees" "bear" "~")) -> ("bear" "sees" "rabbit" "+"))
If someone sees the dog and the dog sees the bear then the dog does not eat the bear.
((("someone" "sees" "dog" "+") ("dog" "sees" "bear" "+")) -> ("dog" "eats" "bear" "-"))
If someone needs the rabbit then they see the cat.
((("someone" "needs" "rabbit" "+")) -> ("someone" "sees" "cat" "+"))
The dog does not eat the cat.
True
1
proof
[(triple5)]
("dog" "eats" "cat" "-")
triple5
The cat is round.
False
1
inv-proof
[(triple4)]
("cat" "is" "round" "+")
triple4
The rabbit needs the rabbit.
True
2
proof
[(((triple7) -> rule3))]
("rabbit" "needs" "rabbit" "+")
((triple7) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple7) -> rule3))]
("rabbit" "needs" "rabbit" "-")
((triple7) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The dog does not see the rabbit.
True
3
proof
[(((((triple6) -> rule6)) -> rule1))]
("dog" "sees" "rabbit" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog sees the rabbit.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule1))]
("dog" "sees" "rabbit" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The rabbit does not see the rabbit.
True
4
proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule1))]
("rabbit" "sees" "rabbit" "-")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit sees the rabbit.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule1))]
("rabbit" "sees" "rabbit" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The bear does not see the rabbit.
Unknown
inv-rconc
[@1: The bear sees the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "sees" "rabbit" "-")
The cat needs the rabbit.
Unknown
rconc
[@1: The cat needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "rabbit" "+")
The bear does not need the rabbit.
Unknown
inv-rconc
[@1: The bear needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "rabbit" "-")
The cat sees the cat.
Unknown
rconc
[@2: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat does not eat the bear.
Unknown
inv-random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "-")
The dog needs the bear.
Unknown
random
[@0: The dog needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "bear" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The cat needs the dog.
Unknown
random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "+")
@0: The bear eats the dog.[(triple1)] The bear is red.[(triple2)] The cat is blue.[(triple3)] The cat is not round.[(triple4)] The dog does not eat the cat.[(triple5)] The dog needs the rabbit.[(triple6)] The rabbit does not need the dog.[(triple10)] The rabbit eats the bear.[(triple7)] The rabbit eats the dog.[(triple8)] The rabbit is not round.[(triple9)] @1: The dog sees the cat.[(((triple6) -> rule6))] The rabbit needs the rabbit.[(((triple7) -> rule3))] @2: The dog does not see the rabbit.[(((((triple6) -> rule6)) -> rule1))] The rabbit sees the cat.[(((((triple7) -> rule3)) -> rule6))] @3: The rabbit does not see the rabbit.[(((((((triple7) -> rule3)) -> rule6)) -> rule1))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is not round.
("cat" "is" "round" "-")
triple4
The dog does not eat the cat.
("dog" "eats" "cat" "-")
triple5
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple6
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
triple10
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple7
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple8
The rabbit is not round.
("rabbit" "is" "round" "-")
triple9
The dog sees the cat.
("dog" "sees" "cat" "+")
((triple6) -> (rule6 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple7) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3