The cat chases the dog. The cat is big. The cat is blue. The cat is green. The cat is kind. The cat is round. The cat likes the dog. The cat needs the dog. The dog chases the cat. The dog is big. The dog is blue. The dog is green. The dog is kind. The dog is round. The dog likes the cat. The dog needs the cat. If something is green then it likes the cat. If something likes the cat then the cat is big. If something needs the cat then the cat needs the dog.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is round.
("cat" "is" "round" "+")
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 big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
If something is green then it likes the cat.
((("something" "is" "green" "+")) -> ("something" "likes" "cat" "+"))
If something likes the cat then the cat is big.
((("something" "likes" "cat" "+")) -> ("cat" "is" "big" "+"))
If something needs the cat then the cat needs the dog.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "dog" "+"))
The dog likes the cat.
True
1
proof
[(triple15 OR ((triple12) -> rule1))]
("dog" "likes" "cat" "+")
triple15
((triple12) -> (rule1 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The cat is not big.
False
1
inv-proof
[(triple2 OR ((triple15) -> rule2) OR ((((triple12) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("cat" "is" "big" "-")
triple2
((triple15) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cat.
True
2
proof
[(((triple4) -> rule1))]
("cat" "likes" "cat" "+")
((triple4) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat does not like the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("cat" "likes" "cat" "-")
((triple4) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
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 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 chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (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" "+")
@0: The cat chases the dog.[(triple1)] The cat is big.[(triple2 OR ((triple15) -> rule2) OR ((((triple12) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] The cat is blue.[(triple3)] The cat is green.[(triple4)] The cat is kind.[(triple5)] The cat is round.[(triple6)] The cat likes the dog.[(triple7)] The cat needs the dog.[(triple8 OR ((triple16) -> rule3))] The dog chases the cat.[(triple9)] The dog is big.[(triple10)] The dog is blue.[(triple11)] The dog is green.[(triple12)] The dog is kind.[(triple13)] The dog is round.[(triple14)] The dog likes the cat.[(triple15 OR ((triple12) -> rule1))] The dog needs the cat.[(triple16)] @1: The cat likes the cat.[(((triple4) -> rule1))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
((triple15) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat likes the dog.
("cat" "likes" "dog" "+")
triple7
The cat needs the dog.
("cat" "needs" "dog" "+")
triple8
((triple16) -> (rule3 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
triple9
The dog is big.
("dog" "is" "big" "+")
triple10
The dog is blue.
("dog" "is" "blue" "+")
triple11
The dog is green.
("dog" "is" "green" "+")
triple12
The dog is kind.
("dog" "is" "kind" "+")
triple13
The dog is round.
("dog" "is" "round" "+")
triple14
The dog likes the cat.
("dog" "likes" "cat" "+")
triple15
((triple12) -> (rule1 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple16
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple4) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1