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