The bear is blue. The bear is young. The bear does not visit the rabbit. The lion chases the bear. The lion is not blue. The lion is not cold. The mouse chases the bear. The mouse is young. The mouse visits the bear. The mouse visits the lion. The rabbit chases the bear. The rabbit chases the lion. The rabbit is not green. The rabbit is young. The rabbit visits the bear. If someone visits the lion and they are not cold then they are young. If someone chases the bear then they are rough. If the bear chases the lion and the lion is cold then the lion chases the bear. If the rabbit is not cold then the rabbit does not see the bear. If the rabbit chases the lion and the rabbit visits the mouse then the rabbit visits the lion. If someone is rough then they visit the lion. If the lion is not blue then the lion visits the mouse. If someone chases the lion then they visit the mouse.
The bear is blue.
("bear" "is" "blue" "+")
The bear is young.
("bear" "is" "young" "+")
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is not cold.
("lion" "is" "cold" "-")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
If someone visits the lion and they are not cold then they are young.
((("someone" "visits" "lion" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "young" "+"))
If someone chases the bear then they are rough.
((("someone" "chases" "bear" "+")) -> ("someone" "is" "rough" "+"))
If the bear chases the lion and the lion is cold then the lion chases the bear.
((("bear" "chases" "lion" "+") ("lion" "is" "cold" "+")) -> ("lion" "chases" "bear" "+"))
If the rabbit is not cold then the rabbit does not see the bear.
((("rabbit" "is" "cold" "~")) -> ("rabbit" "sees" "bear" "-"))
If the rabbit chases the lion and the rabbit visits the mouse then the rabbit visits the lion.
((("rabbit" "chases" "lion" "+") ("rabbit" "visits" "mouse" "+")) -> ("rabbit" "visits" "lion" "+"))
If someone is rough then they visit the lion.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "lion" "+"))
If the lion is not blue then the lion visits the mouse.
((("lion" "is" "blue" "~")) -> ("lion" "visits" "mouse" "+"))
If someone chases the lion then they visit the mouse.
((("someone" "chases" "lion" "+")) -> ("someone" "visits" "mouse" "+"))
The mouse visits the lion.
True
1
proof
[(triple10 OR ((((triple7) -> rule2)) -> rule6))]
("mouse" "visits" "lion" "+")
triple10
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bear is not blue.
False
1
inv-proof
[(triple1)]
("bear" "is" "blue" "-")
triple1
The rabbit visits the mouse.
True
2
proof
[(((triple12) -> rule8))]
("rabbit" "visits" "mouse" "+")
((triple12) -> (rule8 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The rabbit does not visit the mouse.
False
2
inv-proof
[(((triple12) -> rule8))]
("rabbit" "visits" "mouse" "-")
((triple12) -> (rule8 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The lion visits the lion.
True
3
proof
[(((((triple4) -> rule2)) -> rule6))]
("lion" "visits" "lion" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The rabbit does not visit the lion.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule6) OR ((triple12 ((triple12) -> rule8)) -> rule5))]
("rabbit" "visits" "lion" "-")
((((triple11) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
((triple12 ((triple12) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The lion is young.
True
5
proof
[(((((((triple4) -> rule2)) -> rule6) triple6) -> rule1))]
("lion" "is" "young" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2)) triple6) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion is not young.
False
5
inv-proof
[(((((((triple4) -> rule2)) -> rule6) triple6) -> rule1))]
("lion" "is" "young" "-")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2)) triple6) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The bear does not visit the mouse.
Unknown
inv-rconc
[@1: The bear visits the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "visits" "mouse" "-")
The bear visits the lion.
Unknown
rconc
[@2: The bear visits the lion.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("bear" "visits" "lion" "+")
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The bear is rough.
Unknown
rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "rough" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
The rabbit does not chase the mouse.
Unknown
inv-random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "-")
The lion sees the rabbit.
Unknown
random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "+")
@0: The bear does not visit the rabbit.[(triple3)] The bear is blue.[(triple1)] The bear is young.[(triple2)] The lion chases the bear.[(triple4)] The lion is not blue.[(triple5)] The lion is not cold.[(triple6)] The mouse chases the bear.[(triple7)] The mouse is young.[(triple8)] The mouse visits the bear.[(triple9)] The mouse visits the lion.[(triple10 OR ((((triple7) -> rule2)) -> rule6))] The rabbit chases the bear.[(triple11)] The rabbit chases the lion.[(triple12)] The rabbit is not green.[(triple13)] The rabbit is young.[(triple14)] The rabbit visits the bear.[(triple15)] @1: The lion is rough.[(((triple4) -> rule2))] The lion visits the mouse.[(((triple5) -> rule7))] The mouse is rough.[(((triple7) -> rule2))] The rabbit is rough.[(((triple11) -> rule2))] The rabbit visits the mouse.[(((triple12) -> rule8))] @2: The lion visits the lion.[(((((triple4) -> rule2)) -> rule6))] The rabbit visits the lion.[(((((triple11) -> rule2)) -> rule6) OR ((triple12 ((triple12) -> rule8)) -> rule5))] @3: The lion is young.[(((((((triple4) -> rule2)) -> rule6) triple6) -> rule1))]
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
triple3
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The lion chases the bear.
("lion" "chases" "bear" "+")
triple4
The lion is not blue.
("lion" "is" "blue" "-")
triple5
The lion is not cold.
("lion" "is" "cold" "-")
triple6
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple8
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple11
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple12
The rabbit is not green.
("rabbit" "is" "green" "-")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple15
The lion is rough.
("lion" "is" "rough" "+")
((triple4) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((triple5) -> (rule7 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple7) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple11) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
((triple12) -> (rule8 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((((triple11) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
((triple12 ((triple12) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2)) triple6) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3