The bear is rough. The bear is young. The bear needs the dog. The bear sees the tiger. The bear visits the dog. The dog is cold. The dog needs the bear. The dog needs the tiger. The dog sees the tiger. The tiger is kind. The tiger is rough. The tiger is round. The tiger is young. The tiger visits the bear. The tiger visits the dog. If something needs the dog then it visits the tiger.
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something needs the dog then it visits the tiger.
((("something" "needs" "dog" "+")) -> ("something" "visits" "tiger" "+"))
The tiger is kind.
True
1
proof
[(triple10)]
("tiger" "is" "kind" "+")
triple10
The bear does not see the tiger.
False
1
inv-proof
[(triple4)]
("bear" "sees" "tiger" "-")
triple4
The bear visits the tiger.
True
2
proof
[(((triple3) -> rule1))]
("bear" "visits" "tiger" "+")
((triple3) -> (rule1 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "visits" "tiger" "-")
((triple3) -> (rule1 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "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 bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear is rough.[(triple1)] The bear is young.[(triple2)] The bear needs the dog.[(triple3)] The bear sees the tiger.[(triple4)] The bear visits the dog.[(triple5)] The dog is cold.[(triple6)] The dog needs the bear.[(triple7)] The dog needs the tiger.[(triple8)] The dog sees the tiger.[(triple9)] The tiger is kind.[(triple10)] The tiger is rough.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger visits the bear.[(triple14)] The tiger visits the dog.[(triple15)] @1: The bear visits the tiger.[(((triple3) -> rule1))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear needs the dog.
("bear" "needs" "dog" "+")
triple3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple4
The bear visits the dog.
("bear" "visits" "dog" "+")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The dog needs the bear.
("dog" "needs" "bear" "+")
triple7
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple8
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple14
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple15
The bear visits the tiger.
("bear" "visits" "tiger" "+")
((triple3) -> (rule1 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1