The bear eats the dog. The bear is kind. The bear sees the cat. The bear sees the dog. The cat eats the bear. The cat eats the lion. The cat is kind. The dog needs the bear. The dog needs the lion. The lion is nice. The lion is red. The lion is round. The lion does not need the dog. The lion sees the bear. The lion does not see the cat. If something needs the dog then the dog eats the bear. If something is round and it eats the cat then the cat sees the lion. If the lion sees the bear and the lion is nice then the bear is round. If something eats the dog and it eats the bear then the bear is kind. If the dog is not round then the dog is nice. If something sees the dog then it eats the cat.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is kind.
("cat" "is" "kind" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion does not need the dog.
("lion" "needs" "dog" "-")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion does not see the cat.
("lion" "sees" "cat" "-")
If something needs the dog then the dog eats the bear.
((("something" "needs" "dog" "+")) -> ("dog" "eats" "bear" "+"))
If something is round and it eats the cat then the cat sees the lion.
((("something" "is" "round" "+") ("something" "eats" "cat" "+")) -> ("cat" "sees" "lion" "+"))
If the lion sees the bear and the lion is nice then the bear is round.
((("lion" "sees" "bear" "+") ("lion" "is" "nice" "+")) -> ("bear" "is" "round" "+"))
If something eats the dog and it eats the bear then the bear is kind.
((("something" "eats" "dog" "+") ("something" "eats" "bear" "+")) -> ("bear" "is" "kind" "+"))
If the dog is not round then the dog is nice.
((("dog" "is" "round" "~")) -> ("dog" "is" "nice" "+"))
If something sees the dog then it eats the cat.
((("something" "sees" "dog" "+")) -> ("something" "eats" "cat" "+"))
The bear sees the cat.
True
1
proof
[(triple3)]
("bear" "sees" "cat" "+")
triple3
The lion is not nice.
False
1
inv-proof
[(triple10)]
("lion" "is" "nice" "-")
triple10
The bear is round.
True
3
proof
[(((triple14 triple10) -> rule3))]
("bear" "is" "round" "+")
((triple14 triple10) -> (rule3 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear does not eat the cat.
False
2
inv-proof
[(((triple4) -> rule6))]
("bear" "eats" "cat" "-")
((triple4) -> (rule6 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat sees the lion.
True
6
proof
[(((((triple14 triple10) -> rule3) ((triple4) -> rule6)) -> rule2))]
("cat" "sees" "lion" "+")
((((triple14 triple10) -> (rule3 % int3)) ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The cat does not see the lion.
False
6
inv-proof
[(((((triple14 triple10) -> rule3) ((triple4) -> rule6)) -> rule2))]
("cat" "sees" "lion" "-")
((((triple14 triple10) -> (rule3 % int3)) ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The dog does not eat the bear.
Unknown
inv-rconc
[@1: The dog eats the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "bear" "-")
The lion eats the cat.
Unknown
rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "cat" "+")
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "nice" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The lion eats the dog.
Unknown
random
[@0: The lion eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "dog" "+")
@0: The bear eats the dog.[(triple1)] The bear is kind.[(triple2)] The bear sees the cat.[(triple3)] The bear sees the dog.[(triple4)] The cat eats the bear.[(triple5)] The cat eats the lion.[(triple6)] The cat is kind.[(triple7)] The dog needs the bear.[(triple8)] The dog needs the lion.[(triple9)] The lion does not need the dog.[(triple13)] The lion does not see the cat.[(triple15)] The lion is nice.[(triple10)] The lion is red.[(triple11)] The lion is round.[(triple12)] The lion sees the bear.[(triple14)] @1: The bear eats the cat.[(((triple4) -> rule6))] The bear is round.[(((triple14 triple10) -> rule3))] @2: The cat sees the lion.[(((((triple14 triple10) -> rule3) ((triple4) -> rule6)) -> rule2))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear sees the cat.
("bear" "sees" "cat" "+")
triple3
The bear sees the dog.
("bear" "sees" "dog" "+")
triple4
The cat eats the bear.
("cat" "eats" "bear" "+")
triple5
The cat eats the lion.
("cat" "eats" "lion" "+")
triple6
The cat is kind.
("cat" "is" "kind" "+")
triple7
The dog needs the bear.
("dog" "needs" "bear" "+")
triple8
The dog needs the lion.
("dog" "needs" "lion" "+")
triple9
The lion does not need the dog.
("lion" "needs" "dog" "-")
triple13
The lion does not see the cat.
("lion" "sees" "cat" "-")
triple15
The lion is nice.
("lion" "is" "nice" "+")
triple10
The lion is red.
("lion" "is" "red" "+")
triple11
The lion is round.
("lion" "is" "round" "+")
triple12
The lion sees the bear.
("lion" "sees" "bear" "+")
triple14
The bear eats the cat.
("bear" "eats" "cat" "+")
((triple4) -> (rule6 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear is round.
("bear" "is" "round" "+")
((triple14 triple10) -> (rule3 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
((((triple14 triple10) -> (rule3 % int3)) ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3