The cat eats the dog. The dog sees the cat. The rabbit is nice. The tiger sees the cat. If something is green then it eats the rabbit. If the cat eats the rabbit and the rabbit is cold then the rabbit needs the cat. If something needs the dog and it needs the cat then it eats the rabbit. If something needs the tiger and it sees the tiger then the tiger is green. If something eats the cat and the cat needs the dog then the cat needs the tiger. If something sees the cat then the cat is rough.
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something is green then it eats the rabbit.
((("something" "is" "green" "+")) -> ("something" "eats" "rabbit" "+"))
If the cat eats the rabbit and the rabbit is cold then the rabbit needs the cat.
((("cat" "eats" "rabbit" "+") ("rabbit" "is" "cold" "+")) -> ("rabbit" "needs" "cat" "+"))
If something needs the dog and it needs the cat then it eats the rabbit.
((("something" "needs" "dog" "+") ("something" "needs" "cat" "+")) -> ("something" "eats" "rabbit" "+"))
If something needs the tiger and it sees the tiger then the tiger is green.
((("something" "needs" "tiger" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something eats the cat and the cat needs the dog then the cat needs the tiger.
((("something" "eats" "cat" "+") ("cat" "needs" "dog" "+")) -> ("cat" "needs" "tiger" "+"))
If something sees the cat then the cat is rough.
((("something" "sees" "cat" "+")) -> ("cat" "is" "rough" "+"))
The dog sees the cat.
True
1
proof
[(triple2)]
("dog" "sees" "cat" "+")
triple2
The rabbit is not nice.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "nice" "-")
triple3
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cat eats the dog.[(triple1)] The dog sees the cat.[(triple2)] The rabbit is nice.[(triple3)] The tiger sees the cat.[(triple4)] @1: The cat is rough.[(((triple2) -> rule6) OR ((triple4) -> rule6))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The dog sees the cat.
("dog" "sees" "cat" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
((triple2) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple4) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1