The cat likes the dog. The cat needs the dog. The dog is big. The dog is not kind. The dog is not young. The dog likes the cat. The lion eats the cat. The lion is kind. The lion is rough. The lion likes the dog. The lion does not need the cat. The lion needs the dog. If the cat needs the dog then the dog eats the cat. If someone is green then they eat the dog.
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is not kind.
("dog" "is" "kind" "-")
The dog is not young.
("dog" "is" "young" "-")
The dog likes the cat.
("dog" "likes" "cat" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion does not need the cat.
("lion" "needs" "cat" "-")
The lion needs the dog.
("lion" "needs" "dog" "+")
If the cat needs the dog then the dog eats the cat.
((("cat" "needs" "dog" "+")) -> ("dog" "eats" "cat" "+"))
If someone is green then they eat the dog.
((("someone" "is" "green" "+")) -> ("someone" "eats" "dog" "+"))
The lion does not need the cat.
True
1
proof
[(triple11)]
("lion" "needs" "cat" "-")
triple11
The dog is kind.
False
1
inv-proof
[(triple4)]
("dog" "is" "kind" "+")
triple4
The dog eats the cat.
True
2
proof
[(((triple2) -> rule1))]
("dog" "eats" "cat" "+")
((triple2) -> (rule1 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog does not eat the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "eats" "cat" "-")
((triple2) -> (rule1 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The lion does not eat the dog.
Unknown
inv-rconc
[@1: The lion eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "dog" "-")
The dog eats the dog.
Unknown
rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "dog" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The cat likes the dog.[(triple1)] The cat needs the dog.[(triple2)] The dog is big.[(triple3)] The dog is not kind.[(triple4)] The dog is not young.[(triple5)] The dog likes the cat.[(triple6)] The lion does not need the cat.[(triple11)] The lion eats the cat.[(triple7)] The lion is kind.[(triple8)] The lion is rough.[(triple9)] The lion likes the dog.[(triple10)] The lion needs the dog.[(triple12)] @1: The dog eats the cat.[(((triple2) -> rule1))]
The cat likes the dog.
("cat" "likes" "dog" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is not kind.
("dog" "is" "kind" "-")
triple4
The dog is not young.
("dog" "is" "young" "-")
triple5
The dog likes the cat.
("dog" "likes" "cat" "+")
triple6
The lion does not need the cat.
("lion" "needs" "cat" "-")
triple11
The lion eats the cat.
("lion" "eats" "cat" "+")
triple7
The lion is kind.
("lion" "is" "kind" "+")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
The lion likes the dog.
("lion" "likes" "dog" "+")
triple10
The lion needs the dog.
("lion" "needs" "dog" "+")
triple12
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple2) -> (rule1 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1