The bear visits the tiger. The mouse is kind. The tiger sees the mouse. Kind things are young. If something sees the tiger then the tiger is big. If the mouse eats the bear and the bear sees the tiger then the tiger eats the bear. If something visits the bear then the bear sees the mouse. If something visits the tiger then it visits the mouse. All cold things are kind. If something sees the mouse then it visits the bear. If something sees the tiger then the tiger sees the mouse.
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something sees the tiger then the tiger is big.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If the mouse eats the bear and the bear sees the tiger then the tiger eats the bear.
((("mouse" "eats" "bear" "+") ("bear" "sees" "tiger" "+")) -> ("tiger" "eats" "bear" "+"))
If something visits the bear then the bear sees the mouse.
((("something" "visits" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If something visits the tiger then it visits the mouse.
((("something" "visits" "tiger" "+")) -> ("something" "visits" "mouse" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something sees the mouse then it visits the bear.
((("something" "sees" "mouse" "+")) -> ("something" "visits" "bear" "+"))
If something sees the tiger then the tiger sees the mouse.
((("something" "sees" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
The bear visits the tiger.
True
1
proof
[(triple1)]
("bear" "visits" "tiger" "+")
triple1
The tiger does not see the mouse.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "mouse" "-")
triple3
The mouse is young.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "is" "young" "+")
((triple2) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "is" "young" "-")
((triple2) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The bear sees the mouse.
True
3
proof
[(((((triple3) -> rule7)) -> rule4))]
("bear" "sees" "mouse" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The bear does not see the mouse.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule4))]
("bear" "sees" "mouse" "-")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "kind" "-")
The tiger eats the bear.
Unknown
rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "eats" "bear" "+")
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "kind" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The tiger does not see the bear.
Unknown
inv-random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The bear visits the tiger.[(triple1)] The mouse is kind.[(triple2)] The tiger sees the mouse.[(triple3)] @1: The bear visits the mouse.[(((triple1) -> rule5))] The mouse is young.[(((triple2) -> rule1))] The tiger visits the bear.[(((triple3) -> rule7))] @2: The bear sees the mouse.[(((((triple3) -> rule7)) -> rule4))] @3: The bear visits the bear.[(((((((triple3) -> rule7)) -> rule4)) -> rule7))]
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
((triple1) -> (rule5 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple2) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((triple3) -> (rule7 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3