The cat needs the dog. The dog likes the cat. If someone is round then they eat the cat. If someone eats the cat then the cat is not kind. If someone eats the dog then the dog is big. If the cat likes the dog then the dog is round. If someone needs the dog and the dog needs the cat then the cat likes the dog. If someone likes the cat and the cat needs the dog then the cat is round.
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
If someone is round then they eat the cat.
((("someone" "is" "round" "+")) -> ("someone" "eats" "cat" "+"))
If someone eats the cat then the cat is not kind.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "kind" "-"))
If someone eats the dog then the dog is big.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "big" "+"))
If the cat likes the dog then the dog is round.
((("cat" "likes" "dog" "+")) -> ("dog" "is" "round" "+"))
If someone needs the dog and the dog needs the cat then the cat likes the dog.
((("someone" "needs" "dog" "+") ("dog" "needs" "cat" "+")) -> ("cat" "likes" "dog" "+"))
If someone likes the cat and the cat needs the dog then the cat is round.
((("someone" "likes" "cat" "+") ("cat" "needs" "dog" "+")) -> ("cat" "is" "round" "+"))
The dog likes the cat.
True
1
proof
[(triple2)]
("dog" "likes" "cat" "+")
triple2
The dog does not like the cat.
False
1
inv-proof
[(triple2)]
("dog" "likes" "cat" "-")
triple2
The cat is round.
True
3
proof
[(((triple2 triple1) -> rule6))]
("cat" "is" "round" "+")
((triple2 triple1) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not round.
False
3
inv-proof
[(((triple2 triple1) -> rule6))]
("cat" "is" "round" "-")
((triple2 triple1) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat eats the cat.
True
4
proof
[(((((triple2 triple1) -> rule6)) -> rule1))]
("cat" "eats" "cat" "+")
((((triple2 triple1) -> (rule6 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not eat the cat.
False
4
inv-proof
[(((((triple2 triple1) -> rule6)) -> rule1))]
("cat" "eats" "cat" "-")
((((triple2 triple1) -> (rule6 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not kind.
True
5
proof
[(((((((triple2 triple1) -> rule6)) -> rule1)) -> rule2))]
("cat" "is" "kind" "-")
((((((triple2 triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is kind.
False
5
inv-proof
[(((((((triple2 triple1) -> rule6)) -> rule1)) -> rule2))]
("cat" "is" "kind" "+")
((((((triple2 triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "big" "-")
The dog is round.
Unknown
rconc
[@2: The dog is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("dog" "is" "round" "+")
The dog does not eat the cat.
Unknown
inv-rconc
[@3: The dog eats the cat.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule5 <- FAIL)]]
("dog" "eats" "cat" "-")
The cat likes the dog.
Unknown
rconc
[@1: The cat likes the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
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 dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The cat needs the dog.[(triple1)] The dog likes the cat.[(triple2)] @1: The cat is round.[(((triple2 triple1) -> rule6))] @2: The cat eats the cat.[(((((triple2 triple1) -> rule6)) -> rule1))] @3: The cat is not kind.[(((((((triple2 triple1) -> rule6)) -> rule1)) -> rule2))]
The cat needs the dog.
("cat" "needs" "dog" "+")
triple1
The dog likes the cat.
("dog" "likes" "cat" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
((triple2 triple1) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple2 triple1) -> (rule6 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not kind.
("cat" "is" "kind" "-")
((((((triple2 triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3