The cat is cold. The cat is round. The cat is young. The cat likes the mouse. The cat sees the lion. The cat visits the lion. The cat visits the mouse. The lion is rough. The lion sees the cat. The lion visits the cat. The mouse is cold. The mouse is young. The mouse likes the cat. The mouse likes the lion. The mouse sees the cat. The mouse visits the cat. If the lion visits the cat then the cat is green.
The cat is cold.
("cat" "is" "cold" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If the lion visits the cat then the cat is green.
((("lion" "visits" "cat" "+")) -> ("cat" "is" "green" "+"))
The mouse visits the cat.
True
1
proof
[(triple16)]
("mouse" "visits" "cat" "+")
triple16
The mouse does not like the lion.
False
1
inv-proof
[(triple14)]
("mouse" "likes" "lion" "-")
triple14
The cat is green.
True
2
proof
[(((triple10) -> rule1))]
("cat" "is" "green" "+")
((triple10) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is not green.
False
2
inv-proof
[(((triple10) -> rule1))]
("cat" "is" "green" "-")
((triple10) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The lion likes the mouse.
Unknown
random
[@0: The lion likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "mouse" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The cat sees the mouse.
Unknown
random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "+")
@0: The cat is cold.[(triple1)] The cat is round.[(triple2)] The cat is young.[(triple3)] The cat likes the mouse.[(triple4)] The cat sees the lion.[(triple5)] The cat visits the lion.[(triple6)] The cat visits the mouse.[(triple7)] The lion is rough.[(triple8)] The lion sees the cat.[(triple9)] The lion visits the cat.[(triple10)] The mouse is cold.[(triple11)] The mouse is young.[(triple12)] The mouse likes the cat.[(triple13)] The mouse likes the lion.[(triple14)] The mouse sees the cat.[(triple15)] The mouse visits the cat.[(triple16)] @1: The cat is green.[(((triple10) -> rule1))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple4
The cat sees the lion.
("cat" "sees" "lion" "+")
triple5
The cat visits the lion.
("cat" "visits" "lion" "+")
triple6
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple7
The lion is rough.
("lion" "is" "rough" "+")
triple8
The lion sees the cat.
("lion" "sees" "cat" "+")
triple9
The lion visits the cat.
("lion" "visits" "cat" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple13
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple14
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple15
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple16
The cat is green.
("cat" "is" "green" "+")
((triple10) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1