The lion eats the tiger. The lion is nice. The lion visits the tiger. The mouse is nice. The mouse visits the tiger. The tiger is green. The tiger is kind. The tiger is nice. The tiger is red. The tiger likes the lion. The tiger likes the mouse. The tiger visits the lion. If something visits the lion and it likes the tiger then the lion eats the tiger. If something visits the tiger then the tiger likes the lion. If something is green then it eats the mouse. If the tiger eats the mouse then the tiger likes the lion. If something is kind then it visits the mouse. If something likes the tiger then the tiger is green. If something visits the lion and the lion eats the mouse then the lion is green. If something visits the tiger and the tiger eats the lion then it eats the tiger.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
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 visits the lion and it likes the tiger then the lion eats the tiger.
((("something" "visits" "lion" "+") ("something" "likes" "tiger" "+")) -> ("lion" "eats" "tiger" "+"))
If something visits the tiger then the tiger likes the lion.
((("something" "visits" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
If something is green then it eats the mouse.
((("something" "is" "green" "+")) -> ("something" "eats" "mouse" "+"))
If the tiger eats the mouse then the tiger likes the lion.
((("tiger" "eats" "mouse" "+")) -> ("tiger" "likes" "lion" "+"))
If something is kind then it visits the mouse.
((("something" "is" "kind" "+")) -> ("something" "visits" "mouse" "+"))
If something likes the tiger then the tiger is green.
((("something" "likes" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something visits the lion and the lion eats the mouse then the lion is green.
((("something" "visits" "lion" "+") ("lion" "eats" "mouse" "+")) -> ("lion" "is" "green" "+"))
If something visits the tiger and the tiger eats the lion then it eats the tiger.
((("something" "visits" "tiger" "+") ("tiger" "eats" "lion" "+")) -> ("something" "eats" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple8)]
("tiger" "is" "nice" "+")
triple8
The tiger does not like the lion.
False
1
inv-proof
[(triple10 OR ((triple3) -> rule2) OR ((triple5) -> rule2) OR ((((triple6) -> rule3)) -> rule4))]
("tiger" "likes" "lion" "-")
triple10
((triple3) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
((triple5) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The lion eats the tiger.[(triple1)] The lion is nice.[(triple2)] The lion visits the tiger.[(triple3)] The mouse is nice.[(triple4)] The mouse visits the tiger.[(triple5)] The tiger is green.[(triple6)] The tiger is kind.[(triple7)] The tiger is nice.[(triple8)] The tiger is red.[(triple9)] The tiger likes the lion.[(triple10 OR ((triple3) -> rule2) OR ((triple5) -> rule2) OR ((((triple6) -> rule3)) -> rule4))] The tiger likes the mouse.[(triple11)] The tiger visits the lion.[(triple12)] @1: The tiger eats the mouse.[(((triple6) -> rule3))] The tiger visits the mouse.[(((triple7) -> rule5))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple10
((triple3) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
((triple5) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple11
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple6) -> (rule3 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((triple7) -> (rule5 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1