The cat chases the dog. The cat is blue. The cat is kind. The cat is red. The cat is not rough. The cat is young. The cat likes the dog. The cat needs the dog. The dog chases the cat. The dog is blue. The dog is kind. The dog is red. The dog is rough. The dog is young. The dog likes the cat. The dog does not need the cat. If someone likes the cat and they are red then they are blue. If someone needs the dog then they chase the dog. If someone is red and they chase the cat then they like the cat. If someone is red then they chase the cat. If the cat does not chase the dog then the dog needs the cat. If the cat does not need the dog then the dog needs the cat. If someone likes the dog and the dog does not chase the cat then the cat is not young. If someone needs the cat and they like the cat then the cat likes the dog.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is not rough.
("cat" "is" "rough" "-")
The cat is young.
("cat" "is" "young" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog does not need the cat.
("dog" "needs" "cat" "-")
If someone likes the cat and they are red then they are blue.
((("someone" "likes" "cat" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone needs the dog then they chase the dog.
((("someone" "needs" "dog" "+")) -> ("someone" "chases" "dog" "+"))
If someone is red and they chase the cat then they like the cat.
((("someone" "is" "red" "+") ("someone" "chases" "cat" "+")) -> ("someone" "likes" "cat" "+"))
If someone is red then they chase the cat.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cat" "+"))
If the cat does not chase the dog then the dog needs the cat.
((("cat" "chases" "dog" "~")) -> ("dog" "needs" "cat" "+"))
If the cat does not need the dog then the dog needs the cat.
((("cat" "needs" "dog" "~")) -> ("dog" "needs" "cat" "+"))
If someone likes the dog and the dog does not chase the cat then the cat is not young.
((("someone" "likes" "dog" "+") ("dog" "chases" "cat" "~")) -> ("cat" "is" "young" "-"))
If someone needs the cat and they like the cat then the cat likes the dog.
((("someone" "needs" "cat" "+") ("someone" "likes" "cat" "+")) -> ("cat" "likes" "dog" "+"))
The cat is red.
True
1
proof
[(triple4)]
("cat" "is" "red" "+")
triple4
The cat is rough.
False
1
inv-proof
[(triple5)]
("cat" "is" "rough" "+")
triple5
The cat chases the cat.
True
2
proof
[(((triple4) -> rule4))]
("cat" "chases" "cat" "+")
((triple4) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat does not chase the cat.
False
2
inv-proof
[(((triple4) -> rule4))]
("cat" "chases" "cat" "-")
((triple4) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
True
4
proof
[(((triple4 ((triple4) -> rule4)) -> rule3))]
("cat" "likes" "cat" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat does not like the cat.
False
4
inv-proof
[(((triple4 ((triple4) -> rule4)) -> rule3))]
("cat" "likes" "cat" "-")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The cat chases the dog.[(triple1 OR ((triple8) -> rule2))] The cat is blue.[(triple2 OR ((((triple4 ((triple4) -> rule4)) -> rule3) triple4) -> rule1))] The cat is kind.[(triple3)] The cat is not rough.[(triple5)] The cat is red.[(triple4)] The cat is young.[(triple6)] The cat likes the dog.[(triple7)] The cat needs the dog.[(triple8)] The dog chases the cat.[(triple9 OR ((triple12) -> rule4))] The dog does not need the cat.[(triple16)] The dog is blue.[(triple10 OR ((triple15 triple12) -> rule1) OR ((((triple12 triple9) -> rule3) triple12) -> rule1) OR ((((triple12 ((triple12) -> rule4)) -> rule3) triple12) -> rule1))] The dog is kind.[(triple11)] The dog is red.[(triple12)] The dog is rough.[(triple13)] The dog is young.[(triple14)] The dog likes the cat.[(triple15 OR ((triple12 triple9) -> rule3) OR ((triple12 ((triple12) -> rule4)) -> rule3))] @1: The cat chases the cat.[(((triple4) -> rule4))] @2: The cat likes the cat.[(((triple4 ((triple4) -> rule4)) -> rule3))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
((triple8) -> (rule2 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
triple2
((((triple4 ((triple4) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is not rough.
("cat" "is" "rough" "-")
triple5
The cat is red.
("cat" "is" "red" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple6
The cat likes the dog.
("cat" "likes" "dog" "+")
triple7
The cat needs the dog.
("cat" "needs" "dog" "+")
triple8
The dog chases the cat.
("dog" "chases" "cat" "+")
triple9
((triple12) -> (rule4 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog does not need the cat.
("dog" "needs" "cat" "-")
triple16
The dog is blue.
("dog" "is" "blue" "+")
triple10
((triple15 triple12) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((((triple12 triple9) -> (rule3 % int2)) triple12) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
((((triple12 ((triple12) -> (rule4 % int3))) -> (rule3 % int2)) triple12) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The dog chases the cat.
("dog" "chases" "cat" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
triple11
The dog is red.
("dog" "is" "red" "+")
triple12
The dog is rough.
("dog" "is" "rough" "+")
triple13
The dog is young.
("dog" "is" "young" "+")
triple14
The dog likes the cat.
("dog" "likes" "cat" "+")
triple15
((triple12 triple9) -> (rule3 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
((triple12 ((triple12) -> (rule4 % int2))) -> (rule3 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple4) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2