The lion is blue. The lion is red. The lion does not like the mouse. The lion needs the mouse. The lion needs the tiger. The lion visits the mouse. The lion visits the tiger. The mouse is rough. The tiger is big. The tiger visits the lion. If someone visits the lion then they do not like the tiger. If someone is blue and not red then they need the lion. If someone is red and they need the tiger then they are big. If someone is rough and they like the lion then the lion is big. If the lion is big and the lion is nice then the lion does not like the mouse. If someone is big and they do not like the mouse then the mouse does not visit the tiger. If someone needs the mouse and the mouse does not need the lion then they visit the mouse. If someone visits the mouse then the mouse is not nice.
The lion is blue.
("lion" "is" "blue" "+")
The lion is red.
("lion" "is" "red" "+")
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone visits the lion then they do not like the tiger.
((("someone" "visits" "lion" "+")) -> ("someone" "likes" "tiger" "-"))
If someone is blue and not red then they need the lion.
((("someone" "is" "blue" "+") ("someone" "is" "red" "~")) -> ("someone" "needs" "lion" "+"))
If someone is red and they need the tiger then they are big.
((("someone" "is" "red" "+") ("someone" "needs" "tiger" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and they like the lion then the lion is big.
((("someone" "is" "rough" "+") ("someone" "likes" "lion" "+")) -> ("lion" "is" "big" "+"))
If the lion is big and the lion is nice then the lion does not like the mouse.
((("lion" "is" "big" "+") ("lion" "is" "nice" "+")) -> ("lion" "likes" "mouse" "-"))
If someone is big and they do not like the mouse then the mouse does not visit the tiger.
((("someone" "is" "big" "+") ("someone" "likes" "mouse" "~")) -> ("mouse" "visits" "tiger" "-"))
If someone needs the mouse and the mouse does not need the lion then they visit the mouse.
((("someone" "needs" "mouse" "+") ("mouse" "needs" "lion" "~")) -> ("someone" "visits" "mouse" "+"))
If someone visits the mouse then the mouse is not nice.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "nice" "-"))
The lion needs the tiger.
True
1
proof
[(triple5)]
("lion" "needs" "tiger" "+")
triple5
The lion does not visit the mouse.
False
1
inv-proof
[(triple6)]
("lion" "visits" "mouse" "-")
triple6
The lion is big.
True
3
proof
[(((triple2 triple5) -> rule3))]
("lion" "is" "big" "+")
((triple2 triple5) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
3
inv-proof
[(((triple2 triple5) -> rule3))]
("lion" "is" "big" "-")
((triple2 triple5) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse does not visit the tiger.
True
5
proof
[(((((triple2 triple5) -> rule3) triple3) -> rule6))]
("mouse" "visits" "tiger" "-")
((((triple2 triple5) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse visits the tiger.
False
5
inv-proof
[(((((triple2 triple5) -> rule3) triple3) -> rule6))]
("mouse" "visits" "tiger" "+")
((((triple2 triple5) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "lion" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The tiger does not visit the mouse.
Unknown
inv-rconc
[@1: The tiger visits the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "visits" "mouse" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The lion does not like the mouse.[(triple3)] The lion is blue.[(triple1)] The lion is red.[(triple2)] The lion needs the mouse.[(triple4)] The lion needs the tiger.[(triple5)] The lion visits the mouse.[(triple6)] The lion visits the tiger.[(triple7)] The mouse is rough.[(triple8)] The tiger is big.[(triple9)] The tiger visits the lion.[(triple10)] @1: The lion is big.[(((triple2 triple5) -> rule3))] The mouse is not nice.[(((triple6) -> rule8))] The tiger does not like the tiger.[(((triple10) -> rule1))] @2: The mouse does not visit the tiger.[(((((triple2 triple5) -> rule3) triple3) -> rule6))]
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple4
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple5
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple6
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple7
The mouse is rough.
("mouse" "is" "rough" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple10
The lion is big.
("lion" "is" "big" "+")
((triple2 triple5) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse is not nice.
("mouse" "is" "nice" "-")
((triple6) -> (rule8 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
((triple10) -> (rule1 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
((((triple2 triple5) -> (rule3 % int2)) triple3) -> (rule6 % int1))
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
int1
The lion is big.
("lion" "is" "big" "+")
int2