The cow is red. The cow needs the lion. The cow needs the tiger. The cow visits the lion. The cow visits the mouse. The lion visits the cow. The lion visits the mouse. The lion visits the tiger. The mouse is kind. The mouse is young. The mouse visits the lion. The tiger is young. The tiger needs the cow. The tiger visits the lion. The tiger visits the mouse. If the lion visits the cow and the cow visits the lion then the cow sees the lion.
The cow is red.
("cow" "is" "red" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If the lion visits the cow and the cow visits the lion then the cow sees the lion.
((("lion" "visits" "cow" "+") ("cow" "visits" "lion" "+")) -> ("cow" "sees" "lion" "+"))
The tiger is young.
True
1
proof
[(triple12)]
("tiger" "is" "young" "+")
triple12
The cow does not visit the mouse.
False
1
inv-proof
[(triple5)]
("cow" "visits" "mouse" "-")
triple5
The cow sees the lion.
True
3
proof
[(((triple6 triple4) -> rule1))]
("cow" "sees" "lion" "+")
((triple6 triple4) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The cow does not see the lion.
False
3
inv-proof
[(((triple6 triple4) -> rule1))]
("cow" "sees" "lion" "-")
((triple6 triple4) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The mouse does not see the tiger.
Unknown
inv-random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
@0: The cow is red.[(triple1)] The cow needs the lion.[(triple2)] The cow needs the tiger.[(triple3)] The cow visits the lion.[(triple4)] The cow visits the mouse.[(triple5)] The lion visits the cow.[(triple6)] The lion visits the mouse.[(triple7)] The lion visits the tiger.[(triple8)] The mouse is kind.[(triple9)] The mouse is young.[(triple10)] The mouse visits the lion.[(triple11)] The tiger is young.[(triple12)] The tiger needs the cow.[(triple13)] The tiger visits the lion.[(triple14)] The tiger visits the mouse.[(triple15)] @1: The cow sees the lion.[(((triple6 triple4) -> rule1))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
triple4
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple5
The lion visits the cow.
("lion" "visits" "cow" "+")
triple6
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple7
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The mouse is young.
("mouse" "is" "young" "+")
triple10
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple11
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple13
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple14
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
The cow sees the lion.
("cow" "sees" "lion" "+")
((triple6 triple4) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1