The cow is cold. The cow likes the lion. The cow sees the squirrel. The cow visits the squirrel. The lion is green. The lion visits the cow. The mouse is cold. The mouse likes the cow. The mouse sees the lion. The mouse visits the lion. The mouse visits the squirrel. The squirrel sees the cow. If someone likes the mouse then they like the squirrel. If the cow is cold then the cow likes the mouse.
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If someone likes the mouse then they like the squirrel.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "squirrel" "+"))
If the cow is cold then the cow likes the mouse.
((("cow" "is" "cold" "+")) -> ("cow" "likes" "mouse" "+"))
The squirrel sees the cow.
True
1
proof
[(triple12)]
("squirrel" "sees" "cow" "+")
triple12
The cow does not see the squirrel.
False
1
inv-proof
[(triple3)]
("cow" "sees" "squirrel" "-")
triple3
The cow likes the mouse.
True
2
proof
[(((triple1) -> rule2))]
("cow" "likes" "mouse" "+")
((triple1) -> (rule2 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow does not like the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "likes" "mouse" "-")
((triple1) -> (rule2 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse does not like the squirrel.
Unknown
inv-rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The lion likes the squirrel.
Unknown
rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "squirrel" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow is cold.[(triple1)] The cow likes the lion.[(triple2)] The cow sees the squirrel.[(triple3)] The cow visits the squirrel.[(triple4)] The lion is green.[(triple5)] The lion visits the cow.[(triple6)] The mouse is cold.[(triple7)] The mouse likes the cow.[(triple8)] The mouse sees the lion.[(triple9)] The mouse visits the lion.[(triple10)] The mouse visits the squirrel.[(triple11)] The squirrel sees the cow.[(triple12)] @1: The cow likes the mouse.[(((triple1) -> rule2))] @2: The cow likes the squirrel.[(((((triple1) -> rule2)) -> rule1))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow likes the lion.
("cow" "likes" "lion" "+")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple4
The lion is green.
("lion" "is" "green" "+")
triple5
The lion visits the cow.
("lion" "visits" "cow" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple8
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple11
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple12
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((triple1) -> (rule2 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2