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