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