The cat is nice. The cat needs the dog. The cat sees the lion. The dog eats the cat. The lion eats the dog. The lion needs the cat. The lion sees the dog. The rabbit eats the cat. The rabbit needs the cat. The rabbit sees the lion. If someone needs the lion and the lion needs the cat then they need the dog. If the rabbit eats the lion then the rabbit needs the dog. If someone is kind then they see the lion. If the dog is green then the dog is young. If someone needs the dog and the dog is green then the dog is blue. If someone eats the lion then the lion needs the rabbit. If someone needs the rabbit and they are blue then they eat the cat. If someone needs the dog then they see the cat.
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone needs the lion and the lion needs the cat then they need the dog.
((("someone" "needs" "lion" "+") ("lion" "needs" "cat" "+")) -> ("someone" "needs" "dog" "+"))
If the rabbit eats the lion then the rabbit needs the dog.
((("rabbit" "eats" "lion" "+")) -> ("rabbit" "needs" "dog" "+"))
If someone is kind then they see the lion.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "lion" "+"))
If the dog is green then the dog is young.
((("dog" "is" "green" "+")) -> ("dog" "is" "young" "+"))
If someone needs the dog and the dog is green then the dog is blue.
((("someone" "needs" "dog" "+") ("dog" "is" "green" "+")) -> ("dog" "is" "blue" "+"))
If someone eats the lion then the lion needs the rabbit.
((("someone" "eats" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
If someone needs the rabbit and they are blue then they eat the cat.
((("someone" "needs" "rabbit" "+") ("someone" "is" "blue" "+")) -> ("someone" "eats" "cat" "+"))
If someone needs the dog then they see the cat.
((("someone" "needs" "dog" "+")) -> ("someone" "sees" "cat" "+"))
The cat sees the lion.
True
1
proof
[(triple3)]
("cat" "sees" "lion" "+")
triple3
The lion does not eat the dog.
False
1
inv-proof
[(triple5)]
("lion" "eats" "dog" "-")
triple5
The cat sees the cat.
True
2
proof
[(((triple2) -> rule8))]
("cat" "sees" "cat" "+")
((triple2) -> (rule8 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple2) -> rule8))]
("cat" "sees" "cat" "-")
((triple2) -> (rule8 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The lion does not need the rabbit.
Unknown
inv-rconc
[@1: The lion needs the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "needs" "rabbit" "-")
The dog sees the lion.
Unknown
rconc
[@1: The dog sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "lion" "+")
The dog does not see the rabbit.
Unknown
inv-random
[@0: The dog sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "rabbit" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
@0: The cat is nice.[(triple1)] The cat needs the dog.[(triple2)] The cat sees the lion.[(triple3)] The dog eats the cat.[(triple4)] The lion eats the dog.[(triple5)] The lion needs the cat.[(triple6)] The lion sees the dog.[(triple7)] The rabbit eats the cat.[(triple8)] The rabbit needs the cat.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The cat sees the cat.[(((triple2) -> rule8))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The dog eats the cat.
("dog" "eats" "cat" "+")
triple4
The lion eats the dog.
("lion" "eats" "dog" "+")
triple5
The lion needs the cat.
("lion" "needs" "cat" "+")
triple6
The lion sees the dog.
("lion" "sees" "dog" "+")
triple7
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple8
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple2) -> (rule8 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1