The bear is blue. The bear is cold. The bear is green. The bear is kind. The bear is red. The bear likes the tiger. The bear sees the tiger. The tiger is blue. The tiger is cold. The tiger is green. The tiger sees the bear. The tiger visits the bear. If someone sees the bear then the bear sees the tiger. If someone sees the bear and the bear likes the tiger then the tiger is kind. If someone likes the tiger then the tiger is blue.
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone sees the bear then the bear sees the tiger.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "tiger" "+"))
If someone sees the bear and the bear likes the tiger then the tiger is kind.
((("someone" "sees" "bear" "+") ("bear" "likes" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone likes the tiger then the tiger is blue.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
The bear is green.
True
1
proof
[(triple3)]
("bear" "is" "green" "+")
triple3
The tiger is not blue.
False
1
inv-proof
[(triple8 OR ((triple6) -> rule3))]
("tiger" "is" "blue" "-")
triple8
((triple6) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is blue.[(triple1)] The bear is cold.[(triple2)] The bear is green.[(triple3)] The bear is kind.[(triple4)] The bear is red.[(triple5)] The bear likes the tiger.[(triple6)] The bear sees the tiger.[(triple7 OR ((triple11) -> rule1))] The tiger is blue.[(triple8 OR ((triple6) -> rule3))] The tiger is cold.[(triple9)] The tiger is green.[(triple10)] The tiger sees the bear.[(triple11)] The tiger visits the bear.[(triple12)] @1: The tiger is kind.[(((triple11 triple6) -> rule2))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear is kind.
("bear" "is" "kind" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
triple5
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple6
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple7
((triple11) -> (rule1 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
((triple6) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple11
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
((triple11 triple6) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1