The lion chases the mouse. The lion is not big. The lion is kind. The lion sees the mouse. The lion does not see the rabbit. The mouse chases the rabbit. The mouse is green. The rabbit chases the lion. The rabbit chases the mouse. The rabbit is big. The rabbit is cold. The rabbit likes the lion. The rabbit likes the mouse. The rabbit sees the lion. The rabbit sees the mouse. If something is kind then it does not like the lion. If something is big then it chases the lion. If something sees the mouse and it does not like the lion then it does not see the lion.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is green.
("mouse" "is" "green" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something is kind then it does not like the lion.
((("something" "is" "kind" "+")) -> ("something" "likes" "lion" "-"))
If something is big then it chases the lion.
((("something" "is" "big" "+")) -> ("something" "chases" "lion" "+"))
If something sees the mouse and it does not like the lion then it does not see the lion.
((("something" "sees" "mouse" "+") ("something" "likes" "lion" "~")) -> ("something" "sees" "lion" "-"))
The lion is not big.
True
1
proof
[(triple2)]
("lion" "is" "big" "-")
triple2
The lion sees the rabbit.
False
1
inv-proof
[(triple5)]
("lion" "sees" "rabbit" "+")
triple5
The lion does not like the lion.
True
2
proof
[(((triple3) -> rule1))]
("lion" "likes" "lion" "-")
((triple3) -> (rule1 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion likes the lion.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "likes" "lion" "+")
((triple3) -> (rule1 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion does not see the lion.
True
4
proof
[(((triple4 ((triple3) -> rule1)) -> rule3))]
("lion" "sees" "lion" "-")
((triple4 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion does not like the lion.
("lion" "likes" "lion" "-")
int2
The lion sees the lion.
False
4
inv-proof
[(((triple4 ((triple3) -> rule1)) -> rule3))]
("lion" "sees" "lion" "+")
((triple4 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion does not like the lion.
("lion" "likes" "lion" "-")
int2
The lion does not chase the lion.
Unknown
inv-rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "lion" "-")
The mouse chases the lion.
Unknown
rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "lion" "+")
The mouse does not see the lion.
Unknown
inv-random
[@0: The mouse sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "lion" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The mouse does not like the rabbit.
Unknown
inv-random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "-")
The lion chases the rabbit.
Unknown
random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "+")
@0: The lion chases the mouse.[(triple1)] The lion does not see the rabbit.[(triple5)] The lion is kind.[(triple3)] The lion is not big.[(triple2)] The lion sees the mouse.[(triple4)] The mouse chases the rabbit.[(triple6)] The mouse is green.[(triple7)] The rabbit chases the lion.[(triple8 OR ((triple10) -> rule2))] The rabbit chases the mouse.[(triple9)] The rabbit is big.[(triple10)] The rabbit is cold.[(triple11)] The rabbit likes the lion.[(triple12)] The rabbit likes the mouse.[(triple13)] The rabbit sees the lion.[(triple14)] The rabbit sees the mouse.[(triple15)] @1: The lion does not like the lion.[(((triple3) -> rule1))] @2: The lion does not see the lion.[(((triple4 ((triple3) -> rule1)) -> rule3))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is not big.
("lion" "is" "big" "-")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple4
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple8
((triple10) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple11
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple12
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple13
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple14
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The lion does not like the lion.
("lion" "likes" "lion" "-")
((triple3) -> (rule1 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion does not see the lion.
("lion" "sees" "lion" "-")
((triple4 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion does not like the lion.
("lion" "likes" "lion" "-")
int2