The bear is round. The bear is young. The bear needs the lion. The bear sees the dog. The dog is young. The dog likes the bear. The dog sees the bear. The dog sees the lion. The lion is nice. The lion is rough. If the dog is rough and the dog likes the bear then the dog is blue. If someone is young then they like the dog.
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
If the dog is rough and the dog likes the bear then the dog is blue.
((("dog" "is" "rough" "+") ("dog" "likes" "bear" "+")) -> ("dog" "is" "blue" "+"))
If someone is young then they like the dog.
((("someone" "is" "young" "+")) -> ("someone" "likes" "dog" "+"))
The bear is young.
True
1
proof
[(triple2)]
("bear" "is" "young" "+")
triple2
The lion is not nice.
False
1
inv-proof
[(triple9)]
("lion" "is" "nice" "-")
triple9
The dog likes the dog.
True
2
proof
[(((triple5) -> rule2))]
("dog" "likes" "dog" "+")
((triple5) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The bear does not like the dog.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "likes" "dog" "-")
((triple2) -> (rule2 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The lion does not like the dog.
Unknown
inv-rconc
[@1: The lion likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "dog" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "blue" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The bear is round.[(triple1)] The bear is young.[(triple2)] The bear needs the lion.[(triple3)] The bear sees the dog.[(triple4)] The dog is young.[(triple5)] The dog likes the bear.[(triple6)] The dog sees the bear.[(triple7)] The dog sees the lion.[(triple8)] The lion is nice.[(triple9)] The lion is rough.[(triple10)] @1: The bear likes the dog.[(((triple2) -> rule2))] The dog likes the dog.[(((triple5) -> rule2))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear needs the lion.
("bear" "needs" "lion" "+")
triple3
The bear sees the dog.
("bear" "sees" "dog" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog likes the bear.
("dog" "likes" "bear" "+")
triple6
The dog sees the bear.
("dog" "sees" "bear" "+")
triple7
The dog sees the lion.
("dog" "sees" "lion" "+")
triple8
The lion is nice.
("lion" "is" "nice" "+")
triple9
The lion is rough.
("lion" "is" "rough" "+")
triple10
The bear likes the dog.
("bear" "likes" "dog" "+")
((triple2) -> (rule2 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple5) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1