The cow eats the lion. The cow is blue. The cow is red. The cow visits the lion. The lion eats the mouse. The lion eats the squirrel. The lion is round. The mouse eats the lion. The mouse likes the cow. The squirrel is cold. The squirrel likes the cow. The squirrel likes the mouse. If something likes the lion and it eats the cow then it visits the lion. If something is blue then it eats the cow.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is red.
("cow" "is" "red" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is round.
("lion" "is" "round" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If something likes the lion and it eats the cow then it visits the lion.
((("something" "likes" "lion" "+") ("something" "eats" "cow" "+")) -> ("something" "visits" "lion" "+"))
If something is blue then it eats the cow.
((("something" "is" "blue" "+")) -> ("something" "eats" "cow" "+"))
The cow is blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "+")
triple2
The lion is not round.
False
1
inv-proof
[(triple7)]
("lion" "is" "round" "-")
triple7
The cow eats the cow.
True
2
proof
[(((triple2) -> rule2))]
("cow" "eats" "cow" "+")
((triple2) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "eats" "cow" "-")
((triple2) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The squirrel does not eat the cow.
Unknown
inv-rconc
[@1: The squirrel eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "cow" "-")
The mouse eats the cow.
Unknown
rconc
[@1: The mouse eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "cow" "+")
The squirrel does not like the lion.
Unknown
inv-random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
@0: The cow eats the lion.[(triple1)] The cow is blue.[(triple2)] The cow is red.[(triple3)] The cow visits the lion.[(triple4)] The lion eats the mouse.[(triple5)] The lion eats the squirrel.[(triple6)] The lion is round.[(triple7)] The mouse eats the lion.[(triple8)] The mouse likes the cow.[(triple9)] The squirrel is cold.[(triple10)] The squirrel likes the cow.[(triple11)] The squirrel likes the mouse.[(triple12)] @1: The cow eats the cow.[(((triple2) -> rule2))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
triple4
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple5
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple8
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple11
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple12
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple2) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1