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