The bear is young. The bear likes the tiger. The bear needs the tiger. The bear sees the tiger. The tiger is cold. The tiger is round. The tiger is young. The tiger likes the bear. The tiger needs the bear. The tiger sees the bear. If something needs the tiger and it is young then the tiger is cold. If something likes the tiger then it needs the bear.
The bear is young.
("bear" "is" "young" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something needs the tiger and it is young then the tiger is cold.
((("something" "needs" "tiger" "+") ("something" "is" "young" "+")) -> ("tiger" "is" "cold" "+"))
If something likes the tiger then it needs the bear.
((("something" "likes" "tiger" "+")) -> ("something" "needs" "bear" "+"))
The tiger is cold.
True
1
proof
[(triple5 OR ((triple3 triple1) -> rule1))]
("tiger" "is" "cold" "+")
triple5
((triple3 triple1) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger does not like the bear.
False
1
inv-proof
[(triple8)]
("tiger" "likes" "bear" "-")
triple8
The bear needs the bear.
True
2
proof
[(((triple2) -> rule2))]
("bear" "needs" "bear" "+")
((triple2) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "needs" "bear" "-")
((triple2) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
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 tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The bear is young.[(triple1)] The bear likes the tiger.[(triple2)] The bear needs the tiger.[(triple3)] The bear sees the tiger.[(triple4)] The tiger is cold.[(triple5 OR ((triple3 triple1) -> rule1))] The tiger is round.[(triple6)] The tiger is young.[(triple7)] The tiger likes the bear.[(triple8)] The tiger needs the bear.[(triple9)] The tiger sees the bear.[(triple10)] @1: The bear needs the bear.[(((triple2) -> rule2))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
((triple3 triple1) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple6
The tiger is young.
("tiger" "is" "young" "+")
triple7
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple8
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple9
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple10
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple2) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1