The bear is round. The cat is kind. The dog needs the cat. If someone needs the bear then the bear likes the dog. If the bear likes the dog and the dog chases the bear then the bear is big. If someone needs the bear and they chase the bear then they are blue. If someone is big and they chase the dog then the dog is cold. If someone likes the dog then the dog needs the bear. If the dog needs the cat then the cat likes the dog. If someone needs the dog then they are big. If someone is kind then they chase the bear.
The bear is round.
("bear" "is" "round" "+")
The cat is kind.
("cat" "is" "kind" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
If someone needs the bear then the bear likes the dog.
((("someone" "needs" "bear" "+")) -> ("bear" "likes" "dog" "+"))
If the bear likes the dog and the dog chases the bear then the bear is big.
((("bear" "likes" "dog" "+") ("dog" "chases" "bear" "+")) -> ("bear" "is" "big" "+"))
If someone needs the bear and they chase the bear then they are blue.
((("someone" "needs" "bear" "+") ("someone" "chases" "bear" "+")) -> ("someone" "is" "blue" "+"))
If someone is big and they chase the dog then the dog is cold.
((("someone" "is" "big" "+") ("someone" "chases" "dog" "+")) -> ("dog" "is" "cold" "+"))
If someone likes the dog then the dog needs the bear.
((("someone" "likes" "dog" "+")) -> ("dog" "needs" "bear" "+"))
If the dog needs the cat then the cat likes the dog.
((("dog" "needs" "cat" "+")) -> ("cat" "likes" "dog" "+"))
If someone needs the dog then they are big.
((("someone" "needs" "dog" "+")) -> ("someone" "is" "big" "+"))
If someone is kind then they chase the bear.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "bear" "+"))
The cat is kind.
True
1
proof
[(triple2)]
("cat" "is" "kind" "+")
triple2
The cat is not kind.
False
1
inv-proof
[(triple2)]
("cat" "is" "kind" "-")
triple2
The cat likes the dog.
True
2
proof
[(((triple3) -> rule6))]
("cat" "likes" "dog" "+")
((triple3) -> (rule6 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat does not like the dog.
False
2
inv-proof
[(((triple3) -> rule6))]
("cat" "likes" "dog" "-")
((triple3) -> (rule6 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The dog needs the bear.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("dog" "needs" "bear" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The dog does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("dog" "needs" "bear" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The bear likes the dog.
True
4
proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule1))]
("bear" "likes" "dog" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The cat likes the dog.
("cat" "likes" "dog" "+")
int3
The bear does not like the dog.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule1))]
("bear" "likes" "dog" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The cat likes the dog.
("cat" "likes" "dog" "+")
int3
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "blue" "-")
The dog chases the bear.
Unknown
rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "chases" "bear" "+")
The dog is not blue.
Unknown
inv-rconc
[@2: The dog is blue.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("dog" "is" "blue" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "chases" "bear" "+")
The bear does not chase the cat.
Unknown
inv-random
[@0: The bear chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cat" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The dog does not chase the cat.
Unknown
inv-random
[@0: The dog chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cat" "-")
The cat needs the bear.
Unknown
random
[@0: The cat needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bear" "+")
@0: The bear is round.[(triple1)] The cat is kind.[(triple2)] The dog needs the cat.[(triple3)] @1: The cat chases the bear.[(((triple2) -> rule8))] The cat likes the dog.[(((triple3) -> rule6))] @2: The dog needs the bear.[(((((triple3) -> rule6)) -> rule5))] @3: The bear likes the dog.[(((((((triple3) -> rule6)) -> rule5)) -> rule1))]
The bear is round.
("bear" "is" "round" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The dog needs the cat.
("dog" "needs" "cat" "+")
triple3
The cat chases the bear.
("cat" "chases" "bear" "+")
((triple2) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
((triple3) -> (rule6 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The cat likes the dog.
("cat" "likes" "dog" "+")
int3