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