The cat eats the dog. The cat eats the tiger. The dog is blue. The dog is kind. The dog likes the cat. The dog needs the tiger. The tiger is blue. If the dog is not big then the dog eats the cat. If something is nice and kind then it likes the dog.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If the dog is not big then the dog eats the cat.
((("dog" "is" "big" "~")) -> ("dog" "eats" "cat" "+"))
If something is nice and kind then it likes the dog.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "likes" "dog" "+"))
The dog likes the cat.
True
1
proof
[(triple5)]
("dog" "likes" "cat" "+")
triple5
The dog does not need the tiger.
False
1
inv-proof
[(triple6)]
("dog" "needs" "tiger" "-")
triple6
The dog does not eat the cat.
Unknown
inv-rconc
[@1: The dog eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "cat" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The cat eats the dog.[(triple1)] The cat eats the tiger.[(triple2)] The dog is blue.[(triple3)] The dog is kind.[(triple4)] The dog likes the cat.[(triple5)] The dog needs the tiger.[(triple6)] The tiger is blue.[(triple7)]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog likes the cat.
("dog" "likes" "cat" "+")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7