The lion does not eat the mouse. The lion eats the tiger. The lion is green. The lion is not red. The mouse eats the lion. The mouse eats the tiger. The mouse is not rough. The mouse visits the lion. The tiger does not eat the mouse. The tiger is not red. The tiger needs the lion. The tiger visits the mouse. If something is green then it does not visit the tiger.
The lion does not eat the mouse.
("lion" "eats" "mouse" "-")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not red.
("lion" "is" "red" "-")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something is green then it does not visit the tiger.
((("something" "is" "green" "+")) -> ("something" "visits" "tiger" "-"))
The tiger does not eat the mouse.
True
1
proof
[(triple9)]
("tiger" "eats" "mouse" "-")
triple9
The mouse does not visit the lion.
False
1
inv-proof
[(triple8)]
("mouse" "visits" "lion" "-")
triple8
The lion does not visit the tiger.
True
2
proof
[(((triple3) -> rule1))]
("lion" "visits" "tiger" "-")
((triple3) -> (rule1 % int1))
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
int1
The lion visits the tiger.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "visits" "tiger" "+")
((triple3) -> (rule1 % int1))
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
int1
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The lion does not eat the mouse.[(triple1)] The lion eats the tiger.[(triple2)] The lion is green.[(triple3)] The lion is not red.[(triple4)] The mouse eats the lion.[(triple5)] The mouse eats the tiger.[(triple6)] The mouse is not rough.[(triple7)] The mouse visits the lion.[(triple8)] The tiger does not eat the mouse.[(triple9)] The tiger is not red.[(triple10)] The tiger needs the lion.[(triple11)] The tiger visits the mouse.[(triple12)] @1: The lion does not visit the tiger.[(((triple3) -> rule1))]
The lion does not eat the mouse.
("lion" "eats" "mouse" "-")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is not red.
("lion" "is" "red" "-")
triple4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple5
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple6
The mouse is not rough.
("mouse" "is" "rough" "-")
triple7
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple8
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
triple9
The tiger is not red.
("tiger" "is" "red" "-")
triple10
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple11
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple12
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
((triple3) -> (rule1 % int1))
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
int1