The bear is red. The bear visits the tiger. The cow eats the tiger. The mouse eats the tiger. The mouse is cold. The mouse is not green. The mouse sees the cow. The mouse does not visit the bear. The tiger eats the cow. The tiger sees the bear. If someone sees the bear and they eat the cow then they visit the bear. If someone eats the cow then they are young. If someone visits the bear then they are not green. If someone visits the bear then they are not red. If the bear eats the tiger and the bear visits the tiger then the bear does not eat the mouse. If the bear is green and the bear visits the tiger then the tiger does not see the cow.
The bear is red.
("bear" "is" "red" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If someone sees the bear and they eat the cow then they visit the bear.
((("someone" "sees" "bear" "+") ("someone" "eats" "cow" "+")) -> ("someone" "visits" "bear" "+"))
If someone eats the cow then they are young.
((("someone" "eats" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone visits the bear then they are not green.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "green" "-"))
If someone visits the bear then they are not red.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "red" "-"))
If the bear eats the tiger and the bear visits the tiger then the bear does not eat the mouse.
((("bear" "eats" "tiger" "+") ("bear" "visits" "tiger" "+")) -> ("bear" "eats" "mouse" "-"))
If the bear is green and the bear visits the tiger then the tiger does not see the cow.
((("bear" "is" "green" "+") ("bear" "visits" "tiger" "+")) -> ("tiger" "sees" "cow" "-"))
The tiger sees the bear.
True
1
proof
[(triple10)]
("tiger" "sees" "bear" "+")
triple10
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The tiger is young.
True
2
proof
[(((triple9) -> rule2))]
("tiger" "is" "young" "+")
((triple9) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger does not visit the bear.
False
3
inv-proof
[(((triple10 triple9) -> rule1))]
("tiger" "visits" "bear" "-")
((triple10 triple9) -> (rule1 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is not green.
True
4
proof
[(((((triple10 triple9) -> rule1)) -> rule3))]
("tiger" "is" "green" "-")
((((triple10 triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is green.
False
4
inv-proof
[(((((triple10 triple9) -> rule1)) -> rule3))]
("tiger" "is" "green" "+")
((((triple10 triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The cow does not visit the bear.
Unknown
inv-rconc
[@1: The cow visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "bear" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "+")
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "young" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The tiger does not eat the mouse.
Unknown
inv-random
[@0: The tiger eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "mouse" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear is red.[(triple1)] The bear visits the tiger.[(triple2)] The cow eats the tiger.[(triple3)] The mouse does not visit the bear.[(triple8)] The mouse eats the tiger.[(triple4)] The mouse is cold.[(triple5)] The mouse is not green.[(triple6)] The mouse sees the cow.[(triple7)] The tiger eats the cow.[(triple9)] The tiger sees the bear.[(triple10)] @1: The tiger is young.[(((triple9) -> rule2))] The tiger visits the bear.[(((triple10 triple9) -> rule1))] @2: The tiger is not green.[(((((triple10 triple9) -> rule1)) -> rule3))] The tiger is not red.[(((((triple10 triple9) -> rule1)) -> rule4))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple3
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
triple8
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple4
The mouse is cold.
("mouse" "is" "cold" "+")
triple5
The mouse is not green.
("mouse" "is" "green" "-")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple9
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
((triple9) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((triple10 triple9) -> (rule1 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is not green.
("tiger" "is" "green" "-")
((((triple10 triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
((((triple10 triple9) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2