The cat eats the dog. The dog sees the cat. The lion is green. The squirrel likes the cat. If something is green and it likes the squirrel then the squirrel likes the lion. If something sees the squirrel and it sees the cat then the squirrel likes the lion. If something sees the dog and it eats the squirrel then the squirrel does not like the dog. If something eats the squirrel then it sees the dog. If something is green then it does not like the cat. If something sees the cat then the cat eats the lion.
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The lion is green.
("lion" "is" "green" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If something is green and it likes the squirrel then the squirrel likes the lion.
((("something" "is" "green" "+") ("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "lion" "+"))
If something sees the squirrel and it sees the cat then the squirrel likes the lion.
((("something" "sees" "squirrel" "+") ("something" "sees" "cat" "+")) -> ("squirrel" "likes" "lion" "+"))
If something sees the dog and it eats the squirrel then the squirrel does not like the dog.
((("something" "sees" "dog" "+") ("something" "eats" "squirrel" "+")) -> ("squirrel" "likes" "dog" "-"))
If something eats the squirrel then it sees the dog.
((("something" "eats" "squirrel" "+")) -> ("something" "sees" "dog" "+"))
If something is green then it does not like the cat.
((("something" "is" "green" "+")) -> ("something" "likes" "cat" "-"))
If something sees the cat then the cat eats the lion.
((("something" "sees" "cat" "+")) -> ("cat" "eats" "lion" "+"))
The cat eats the dog.
True
1
proof
[(triple1)]
("cat" "eats" "dog" "+")
triple1
The lion is not green.
False
1
inv-proof
[(triple3)]
("lion" "is" "green" "-")
triple3
The cat eats the lion.
True
2
proof
[(((triple2) -> rule6))]
("cat" "eats" "lion" "+")
((triple2) -> (rule6 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule6))]
("cat" "eats" "lion" "-")
((triple2) -> (rule6 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The lion does not see the dog.
Unknown
inv-rconc
[@1: The lion sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "dog" "-")
The cat sees the dog.
Unknown
rconc
[@1: The cat sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "dog" "+")
The dog does not like the lion.
Unknown
inv-random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The cat eats the dog.[(triple1)] The dog sees the cat.[(triple2)] The lion is green.[(triple3)] The squirrel likes the cat.[(triple4)] @1: The cat eats the lion.[(((triple2) -> rule6))] The lion does not like the cat.[(((triple3) -> rule5))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The dog sees the cat.
("dog" "sees" "cat" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple4
The cat eats the lion.
("cat" "eats" "lion" "+")
((triple2) -> (rule6 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The lion does not like the cat.
("lion" "likes" "cat" "-")
((triple3) -> (rule5 % int1))
The lion does not like the cat.
("lion" "likes" "cat" "-")
int1