The bear is red. The bear is round. The bear is young. The bear likes the dog. The bear sees the dog. The bear sees the tiger. The bear visits the dog. The bear visits the tiger. The dog likes the bear. The dog sees the bear. The dog visits the bear. The tiger is red. The tiger is young. The tiger sees the dog. The tiger visits the dog. If the bear is young then the bear is red. If the tiger visits the dog then the dog is not young. If the dog is red and the dog does not visit the bear then the bear does not like the dog. If the tiger visits the dog and the bear does not visit the tiger then the tiger is young. If someone visits the tiger and the tiger does not visit the dog then they see the tiger. If someone sees the tiger then they do not see the bear.
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If the bear is young then the bear is red.
((("bear" "is" "young" "+")) -> ("bear" "is" "red" "+"))
If the tiger visits the dog then the dog is not young.
((("tiger" "visits" "dog" "+")) -> ("dog" "is" "young" "-"))
If the dog is red and the dog does not visit the bear then the bear does not like the dog.
((("dog" "is" "red" "+") ("dog" "visits" "bear" "~")) -> ("bear" "likes" "dog" "-"))
If the tiger visits the dog and the bear does not visit the tiger then the tiger is young.
((("tiger" "visits" "dog" "+") ("bear" "visits" "tiger" "~")) -> ("tiger" "is" "young" "+"))
If someone visits the tiger and the tiger does not visit the dog then they see the tiger.
((("someone" "visits" "tiger" "+") ("tiger" "visits" "dog" "~")) -> ("someone" "sees" "tiger" "+"))
If someone sees the tiger then they do not see the bear.
((("someone" "sees" "tiger" "+")) -> ("someone" "sees" "bear" "-"))
The bear visits the dog.
True
1
proof
[(triple7)]
("bear" "visits" "dog" "+")
triple7
The tiger does not visit the dog.
False
1
inv-proof
[(triple15)]
("tiger" "visits" "dog" "-")
triple15
The dog is not young.
True
2
proof
[(((triple15) -> rule2))]
("dog" "is" "young" "-")
((triple15) -> (rule2 % int1))
The dog is not young.
("dog" "is" "young" "-")
int1
The bear sees the bear.
False
2
inv-proof
[(((triple6) -> rule6))]
("bear" "sees" "bear" "+")
((triple6) -> (rule6 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The dog sees the tiger.
Unknown
rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "tiger" "+")
The tiger does not see the bear.
Unknown
inv-random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The bear is red.[(triple1 OR ((triple3) -> rule1))] The bear is round.[(triple2)] The bear is young.[(triple3)] The bear likes the dog.[(triple4)] The bear sees the dog.[(triple5)] The bear sees the tiger.[(triple6)] The bear visits the dog.[(triple7)] The bear visits the tiger.[(triple8)] The dog likes the bear.[(triple9)] The dog sees the bear.[(triple10)] The dog visits the bear.[(triple11)] The tiger is red.[(triple12)] The tiger is young.[(triple13)] The tiger sees the dog.[(triple14)] The tiger visits the dog.[(triple15)] @1: The bear does not see the bear.[(((triple6) -> rule6))] The dog is not young.[(((triple15) -> rule2))]
The bear is red.
("bear" "is" "red" "+")
triple1
((triple3) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear likes the dog.
("bear" "likes" "dog" "+")
triple4
The bear sees the dog.
("bear" "sees" "dog" "+")
triple5
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple6
The bear visits the dog.
("bear" "visits" "dog" "+")
triple7
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple8
The dog likes the bear.
("dog" "likes" "bear" "+")
triple9
The dog sees the bear.
("dog" "sees" "bear" "+")
triple10
The dog visits the bear.
("dog" "visits" "bear" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple14
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple15
The bear does not see the bear.
("bear" "sees" "bear" "-")
((triple6) -> (rule6 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The dog is not young.
("dog" "is" "young" "-")
((triple15) -> (rule2 % int1))
The dog is not young.
("dog" "is" "young" "-")
int1