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